%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV570-1.049 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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.15s 5.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV570-1.049 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n001.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 09:16:36 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 0.15/5.67 % Refutation found
% 0.15/5.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.67 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.67 fof(f3,axiom,(
% 0.15/5.67 (![A,E]: (rselect_seq(rstore_seq(A,E)) = E ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f4,axiom,(
% 0.15/5.67 (![A,E]: (rselect_head(rstore_head(A,E)) = E ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f5,axiom,(
% 0.15/5.67 (![A,E]: (rselect_tail(rstore_tail(A,E)) = E ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f7,axiom,(
% 0.15/5.67 (![A,E]: (rselect_seq(rstore_tail(A,E)) = rselect_seq(A) ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f8,axiom,(
% 0.15/5.67 (![A,E]: (rselect_head(rstore_tail(A,E)) = rselect_head(A) ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f9,axiom,(
% 0.15/5.67 (![A,E]: (rselect_head(rstore_seq(A,E)) = rselect_head(A) ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f11,axiom,(
% 0.15/5.67 (![A,E]: (rselect_tail(rstore_head(A,E)) = rselect_tail(A) ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f12,axiom,(
% 0.15/5.67 (![X]: (p(s(X)) = X ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f16,axiom,(
% 0.15/5.67 (![X]: (s(s(s(X))) = X ))),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f90,hypothesis,(
% 0.15/5.67 earray_296 = rselect_seq(q49) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f116,hypothesis,(
% 0.15/5.67 elem_298 = select(earray_296,index_297) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f117,hypothesis,(
% 0.15/5.67 elem_301 = select(earray_296,index_300) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f118,hypothesis,(
% 0.15/5.67 index_0 = rselect_tail(q) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f119,hypothesis,(
% 0.15/5.67 index_102 = s(index_99) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f120,hypothesis,(
% 0.15/5.67 index_105 = rselect_tail(q24) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f121,hypothesis,(
% 0.15/5.67 index_108 = s(index_105) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f122,hypothesis,(
% 0.15/5.67 index_111 = rselect_tail(q25) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f123,hypothesis,(
% 0.15/5.67 index_114 = s(index_111) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f124,hypothesis,(
% 0.15/5.67 index_117 = rselect_tail(q26) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f125,hypothesis,(
% 0.15/5.67 index_12 = s(index_9) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f126,hypothesis,(
% 0.15/5.67 index_120 = s(index_117) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f127,hypothesis,(
% 0.15/5.67 index_123 = rselect_tail(q27) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f128,hypothesis,(
% 0.15/5.67 index_126 = s(index_123) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f129,hypothesis,(
% 0.15/5.67 index_129 = rselect_tail(q28) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f130,hypothesis,(
% 0.15/5.67 index_132 = s(index_129) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f131,hypothesis,(
% 0.15/5.67 index_135 = rselect_tail(q2) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f132,hypothesis,(
% 0.15/5.67 index_138 = s(index_135) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f133,hypothesis,(
% 0.15/5.67 index_141 = rselect_tail(q29) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f134,hypothesis,(
% 0.15/5.67 index_144 = s(index_141) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f135,hypothesis,(
% 0.15/5.67 index_147 = rselect_tail(q30) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f136,hypothesis,(
% 0.15/5.67 index_15 = rselect_tail(q10) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f137,hypothesis,(
% 0.15/5.67 index_150 = s(index_147) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.67 fof(f138,hypothesis,(
% 0.15/5.67 index_153 = rselect_tail(q31) ),
% 0.15/5.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f139,hypothesis,(
% 0.15/5.68 index_156 = s(index_153) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f140,hypothesis,(
% 0.15/5.68 index_159 = rselect_tail(q32) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f141,hypothesis,(
% 0.15/5.68 index_162 = s(index_159) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f142,hypothesis,(
% 0.15/5.68 index_165 = rselect_tail(q33) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f143,hypothesis,(
% 0.15/5.68 index_168 = s(index_165) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f144,hypothesis,(
% 0.15/5.68 index_171 = rselect_tail(q34) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f145,hypothesis,(
% 0.15/5.68 index_174 = s(index_171) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f146,hypothesis,(
% 0.15/5.68 index_177 = rselect_tail(q35) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f147,hypothesis,(
% 0.15/5.68 index_18 = s(index_15) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f148,hypothesis,(
% 0.15/5.68 index_180 = s(index_177) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f149,hypothesis,(
% 0.15/5.68 index_183 = rselect_tail(q36) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f150,hypothesis,(
% 0.15/5.68 index_186 = s(index_183) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f151,hypothesis,(
% 0.15/5.68 index_189 = rselect_tail(q37) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f152,hypothesis,(
% 0.15/5.68 index_192 = s(index_189) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f153,hypothesis,(
% 0.15/5.68 index_195 = rselect_tail(q38) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f154,hypothesis,(
% 0.15/5.68 index_198 = s(index_195) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f155,hypothesis,(
% 0.15/5.68 index_201 = rselect_tail(q3) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f156,hypothesis,(
% 0.15/5.68 index_204 = s(index_201) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f157,hypothesis,(
% 0.15/5.68 index_207 = rselect_tail(q39) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f158,hypothesis,(
% 0.15/5.68 index_21 = rselect_tail(q11) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f159,hypothesis,(
% 0.15/5.68 index_210 = s(index_207) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f160,hypothesis,(
% 0.15/5.68 index_213 = rselect_tail(q40) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f161,hypothesis,(
% 0.15/5.68 index_216 = s(index_213) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f162,hypothesis,(
% 0.15/5.68 index_219 = rselect_tail(q41) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f163,hypothesis,(
% 0.15/5.68 index_222 = s(index_219) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f164,hypothesis,(
% 0.15/5.68 index_225 = rselect_tail(q42) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f165,hypothesis,(
% 0.15/5.68 index_228 = s(index_225) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f166,hypothesis,(
% 0.15/5.68 index_231 = rselect_tail(q43) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f167,hypothesis,(
% 0.15/5.68 index_234 = s(index_231) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f168,hypothesis,(
% 0.15/5.68 index_237 = rselect_tail(q44) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f169,hypothesis,(
% 0.15/5.68 index_24 = s(index_21) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f170,hypothesis,(
% 0.15/5.68 index_240 = s(index_237) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f171,hypothesis,(
% 0.15/5.68 index_243 = rselect_tail(q45) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f172,hypothesis,(
% 0.15/5.68 index_246 = s(index_243) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f173,hypothesis,(
% 0.15/5.68 index_249 = rselect_tail(q46) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f174,hypothesis,(
% 0.15/5.68 index_252 = s(index_249) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f175,hypothesis,(
% 0.15/5.68 index_255 = rselect_tail(q47) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f176,hypothesis,(
% 0.15/5.68 index_258 = s(index_255) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f177,hypothesis,(
% 0.15/5.68 index_261 = rselect_tail(q48) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f178,hypothesis,(
% 0.15/5.68 index_264 = s(index_261) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f179,hypothesis,(
% 0.15/5.68 index_267 = rselect_tail(q4) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f180,hypothesis,(
% 0.15/5.68 index_27 = rselect_tail(q12) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f181,hypothesis,(
% 0.15/5.68 index_270 = s(index_267) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f182,hypothesis,(
% 0.15/5.68 index_273 = rselect_tail(q5) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f183,hypothesis,(
% 0.15/5.68 index_276 = s(index_273) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f184,hypothesis,(
% 0.15/5.68 index_279 = rselect_tail(q6) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f185,hypothesis,(
% 0.15/5.68 index_282 = s(index_279) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f186,hypothesis,(
% 0.15/5.68 index_285 = rselect_tail(q7) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f187,hypothesis,(
% 0.15/5.68 index_288 = s(index_285) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f188,hypothesis,(
% 0.15/5.68 index_291 = rselect_tail(q8) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f189,hypothesis,(
% 0.15/5.68 index_294 = s(index_291) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f190,hypothesis,(
% 0.15/5.68 index_297 = rselect_head(q49) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f191,hypothesis,(
% 0.15/5.68 index_299 = rselect_tail(q49) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f192,hypothesis,(
% 0.15/5.68 index_3 = rselect_tail(q0) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f193,hypothesis,(
% 0.15/5.68 index_30 = s(index_27) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f194,hypothesis,(
% 0.15/5.68 s(index_300) = index_299 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f195,hypothesis,(
% 0.15/5.68 index_33 = rselect_tail(q13) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f196,hypothesis,(
% 0.15/5.68 index_36 = s(index_33) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f197,hypothesis,(
% 0.15/5.68 index_39 = rselect_tail(q14) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f198,hypothesis,(
% 0.15/5.68 index_42 = s(index_39) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f199,hypothesis,(
% 0.15/5.68 index_45 = rselect_tail(q15) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f200,hypothesis,(
% 0.15/5.68 index_48 = s(index_45) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f201,hypothesis,(
% 0.15/5.68 index_51 = rselect_tail(q16) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f202,hypothesis,(
% 0.15/5.68 index_54 = s(index_51) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f203,hypothesis,(
% 0.15/5.68 index_57 = rselect_tail(q17) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f204,hypothesis,(
% 0.15/5.68 index_6 = s(index_3) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f205,hypothesis,(
% 0.15/5.68 index_60 = s(index_57) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f206,hypothesis,(
% 0.15/5.68 index_63 = rselect_tail(q18) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f207,hypothesis,(
% 0.15/5.68 index_66 = s(index_63) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f208,hypothesis,(
% 0.15/5.68 index_69 = rselect_tail(q1) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f209,hypothesis,(
% 0.15/5.68 index_72 = s(index_69) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f210,hypothesis,(
% 0.15/5.68 index_75 = rselect_tail(q19) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f211,hypothesis,(
% 0.15/5.68 index_78 = s(index_75) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f212,hypothesis,(
% 0.15/5.68 index_81 = rselect_tail(q20) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f213,hypothesis,(
% 0.15/5.68 index_84 = s(index_81) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f214,hypothesis,(
% 0.15/5.68 index_87 = rselect_tail(q21) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f215,hypothesis,(
% 0.15/5.68 index_9 = rselect_tail(q9) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f216,hypothesis,(
% 0.15/5.68 index_90 = s(index_87) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f217,hypothesis,(
% 0.15/5.68 index_93 = rselect_tail(q22) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f218,hypothesis,(
% 0.15/5.68 index_96 = s(index_93) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f219,hypothesis,(
% 0.15/5.68 index_99 = rselect_tail(q23) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f220,hypothesis,(
% 0.15/5.68 queue_1 = rstore_head(q,index_0) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f221,hypothesis,(
% 0.15/5.68 queue_101 = rstore_seq(q23,earray_100) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f222,hypothesis,(
% 0.15/5.68 queue_103 = rstore_tail(queue_101,index_102) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f223,hypothesis,(
% 0.15/5.68 queue_107 = rstore_seq(q24,earray_106) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f224,hypothesis,(
% 0.15/5.68 queue_109 = rstore_tail(queue_107,index_108) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f225,hypothesis,(
% 0.15/5.68 queue_11 = rstore_seq(q9,earray_10) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f226,hypothesis,(
% 0.15/5.68 queue_113 = rstore_seq(q25,earray_112) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f227,hypothesis,(
% 0.15/5.68 queue_115 = rstore_tail(queue_113,index_114) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f228,hypothesis,(
% 0.15/5.68 queue_119 = rstore_seq(q26,earray_118) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f229,hypothesis,(
% 0.15/5.68 queue_121 = rstore_tail(queue_119,index_120) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f230,hypothesis,(
% 0.15/5.68 queue_125 = rstore_seq(q27,earray_124) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f231,hypothesis,(
% 0.15/5.68 queue_127 = rstore_tail(queue_125,index_126) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f232,hypothesis,(
% 0.15/5.68 queue_13 = rstore_tail(queue_11,index_12) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f233,hypothesis,(
% 0.15/5.68 queue_131 = rstore_seq(q28,earray_130) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f234,hypothesis,(
% 0.15/5.68 queue_133 = rstore_tail(queue_131,index_132) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f235,hypothesis,(
% 0.15/5.68 queue_137 = rstore_seq(q2,earray_136) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f236,hypothesis,(
% 0.15/5.68 queue_139 = rstore_tail(queue_137,index_138) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f237,hypothesis,(
% 0.15/5.68 queue_143 = rstore_seq(q29,earray_142) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f238,hypothesis,(
% 0.15/5.68 queue_145 = rstore_tail(queue_143,index_144) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f239,hypothesis,(
% 0.15/5.68 queue_149 = rstore_seq(q30,earray_148) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f240,hypothesis,(
% 0.15/5.68 queue_151 = rstore_tail(queue_149,index_150) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f241,hypothesis,(
% 0.15/5.68 queue_155 = rstore_seq(q31,earray_154) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f242,hypothesis,(
% 0.15/5.68 queue_157 = rstore_tail(queue_155,index_156) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f243,hypothesis,(
% 0.15/5.68 queue_161 = rstore_seq(q32,earray_160) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f244,hypothesis,(
% 0.15/5.68 queue_163 = rstore_tail(queue_161,index_162) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f245,hypothesis,(
% 0.15/5.68 queue_167 = rstore_seq(q33,earray_166) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f246,hypothesis,(
% 0.15/5.68 queue_169 = rstore_tail(queue_167,index_168) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f247,hypothesis,(
% 0.15/5.68 queue_17 = rstore_seq(q10,earray_16) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f248,hypothesis,(
% 0.15/5.68 queue_173 = rstore_seq(q34,earray_172) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f249,hypothesis,(
% 0.15/5.68 queue_175 = rstore_tail(queue_173,index_174) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f250,hypothesis,(
% 0.15/5.68 queue_179 = rstore_seq(q35,earray_178) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f251,hypothesis,(
% 0.15/5.68 queue_181 = rstore_tail(queue_179,index_180) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f252,hypothesis,(
% 0.15/5.68 queue_185 = rstore_seq(q36,earray_184) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f253,hypothesis,(
% 0.15/5.68 queue_187 = rstore_tail(queue_185,index_186) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f254,hypothesis,(
% 0.15/5.68 queue_19 = rstore_tail(queue_17,index_18) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f255,hypothesis,(
% 0.15/5.68 queue_191 = rstore_seq(q37,earray_190) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f256,hypothesis,(
% 0.15/5.68 queue_193 = rstore_tail(queue_191,index_192) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f257,hypothesis,(
% 0.15/5.68 queue_197 = rstore_seq(q38,earray_196) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f258,hypothesis,(
% 0.15/5.68 queue_199 = rstore_tail(queue_197,index_198) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f259,hypothesis,(
% 0.15/5.68 queue_203 = rstore_seq(q3,earray_202) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f260,hypothesis,(
% 0.15/5.68 queue_205 = rstore_tail(queue_203,index_204) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f261,hypothesis,(
% 0.15/5.68 queue_209 = rstore_seq(q39,earray_208) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f262,hypothesis,(
% 0.15/5.68 queue_211 = rstore_tail(queue_209,index_210) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f263,hypothesis,(
% 0.15/5.68 queue_215 = rstore_seq(q40,earray_214) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f264,hypothesis,(
% 0.15/5.68 queue_217 = rstore_tail(queue_215,index_216) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f265,hypothesis,(
% 0.15/5.68 queue_221 = rstore_seq(q41,earray_220) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f266,hypothesis,(
% 0.15/5.68 queue_223 = rstore_tail(queue_221,index_222) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f267,hypothesis,(
% 0.15/5.68 queue_227 = rstore_seq(q42,earray_226) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f268,hypothesis,(
% 0.15/5.68 queue_229 = rstore_tail(queue_227,index_228) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f269,hypothesis,(
% 0.15/5.68 queue_23 = rstore_seq(q11,earray_22) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f270,hypothesis,(
% 0.15/5.68 queue_233 = rstore_seq(q43,earray_232) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f271,hypothesis,(
% 0.15/5.68 queue_235 = rstore_tail(queue_233,index_234) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f272,hypothesis,(
% 0.15/5.68 queue_239 = rstore_seq(q44,earray_238) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f273,hypothesis,(
% 0.15/5.68 queue_241 = rstore_tail(queue_239,index_240) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f274,hypothesis,(
% 0.15/5.68 queue_245 = rstore_seq(q45,earray_244) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f275,hypothesis,(
% 0.15/5.68 queue_247 = rstore_tail(queue_245,index_246) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f276,hypothesis,(
% 0.15/5.68 queue_25 = rstore_tail(queue_23,index_24) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f277,hypothesis,(
% 0.15/5.68 queue_251 = rstore_seq(q46,earray_250) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f278,hypothesis,(
% 0.15/5.68 queue_253 = rstore_tail(queue_251,index_252) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f279,hypothesis,(
% 0.15/5.68 queue_257 = rstore_seq(q47,earray_256) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f280,hypothesis,(
% 0.15/5.68 queue_259 = rstore_tail(queue_257,index_258) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f281,hypothesis,(
% 0.15/5.68 queue_263 = rstore_seq(q48,earray_262) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f282,hypothesis,(
% 0.15/5.68 queue_265 = rstore_tail(queue_263,index_264) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f283,hypothesis,(
% 0.15/5.68 queue_269 = rstore_seq(q4,earray_268) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f284,hypothesis,(
% 0.15/5.68 queue_271 = rstore_tail(queue_269,index_270) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f285,hypothesis,(
% 0.15/5.68 queue_275 = rstore_seq(q5,earray_274) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f286,hypothesis,(
% 0.15/5.68 queue_277 = rstore_tail(queue_275,index_276) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f287,hypothesis,(
% 0.15/5.68 queue_281 = rstore_seq(q6,earray_280) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f288,hypothesis,(
% 0.15/5.68 queue_283 = rstore_tail(queue_281,index_282) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f289,hypothesis,(
% 0.15/5.68 queue_287 = rstore_seq(q7,earray_286) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f290,hypothesis,(
% 0.15/5.68 queue_289 = rstore_tail(queue_287,index_288) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f291,hypothesis,(
% 0.15/5.68 queue_29 = rstore_seq(q12,earray_28) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f292,hypothesis,(
% 0.15/5.68 queue_293 = rstore_seq(q8,earray_292) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f293,hypothesis,(
% 0.15/5.68 queue_295 = rstore_tail(queue_293,index_294) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f294,hypothesis,(
% 0.15/5.68 queue_31 = rstore_tail(queue_29,index_30) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f295,hypothesis,(
% 0.15/5.68 queue_35 = rstore_seq(q13,earray_34) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f296,hypothesis,(
% 0.15/5.68 queue_37 = rstore_tail(queue_35,index_36) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f297,hypothesis,(
% 0.15/5.68 queue_41 = rstore_seq(q14,earray_40) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f298,hypothesis,(
% 0.15/5.68 queue_43 = rstore_tail(queue_41,index_42) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f299,hypothesis,(
% 0.15/5.68 queue_47 = rstore_seq(q15,earray_46) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f300,hypothesis,(
% 0.15/5.68 queue_49 = rstore_tail(queue_47,index_48) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f301,hypothesis,(
% 0.15/5.68 queue_5 = rstore_seq(q0,earray_4) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f302,hypothesis,(
% 0.15/5.68 queue_53 = rstore_seq(q16,earray_52) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f303,hypothesis,(
% 0.15/5.68 queue_55 = rstore_tail(queue_53,index_54) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f304,hypothesis,(
% 0.15/5.68 queue_59 = rstore_seq(q17,earray_58) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f305,hypothesis,(
% 0.15/5.68 queue_61 = rstore_tail(queue_59,index_60) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f306,hypothesis,(
% 0.15/5.68 queue_65 = rstore_seq(q18,earray_64) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f307,hypothesis,(
% 0.15/5.68 queue_67 = rstore_tail(queue_65,index_66) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f308,hypothesis,(
% 0.15/5.68 queue_7 = rstore_tail(queue_5,index_6) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f309,hypothesis,(
% 0.15/5.68 queue_71 = rstore_seq(q1,earray_70) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f310,hypothesis,(
% 0.15/5.68 queue_73 = rstore_tail(queue_71,index_72) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f311,hypothesis,(
% 0.15/5.68 queue_77 = rstore_seq(q19,earray_76) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f312,hypothesis,(
% 0.15/5.68 queue_79 = rstore_tail(queue_77,index_78) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f313,hypothesis,(
% 0.15/5.68 queue_83 = rstore_seq(q20,earray_82) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f314,hypothesis,(
% 0.15/5.68 queue_85 = rstore_tail(queue_83,index_84) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f315,hypothesis,(
% 0.15/5.68 queue_89 = rstore_seq(q21,earray_88) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f316,hypothesis,(
% 0.15/5.68 queue_91 = rstore_tail(queue_89,index_90) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f317,hypothesis,(
% 0.15/5.68 queue_95 = rstore_seq(q22,earray_94) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f318,hypothesis,(
% 0.15/5.68 queue_97 = rstore_tail(queue_95,index_96) ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f319,hypothesis,(
% 0.15/5.68 q0 = queue_1 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f320,hypothesis,(
% 0.15/5.68 q1 = queue_7 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f321,hypothesis,(
% 0.15/5.68 q10 = queue_13 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f322,hypothesis,(
% 0.15/5.68 q11 = queue_19 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f323,hypothesis,(
% 0.15/5.68 q12 = queue_25 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f324,hypothesis,(
% 0.15/5.68 q13 = queue_31 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f325,hypothesis,(
% 0.15/5.68 q14 = queue_37 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f326,hypothesis,(
% 0.15/5.68 q15 = queue_43 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f327,hypothesis,(
% 0.15/5.68 q16 = queue_49 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f328,hypothesis,(
% 0.15/5.68 q17 = queue_55 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f329,hypothesis,(
% 0.15/5.68 q18 = queue_61 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f330,hypothesis,(
% 0.15/5.68 q19 = queue_67 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f331,hypothesis,(
% 0.15/5.68 q2 = queue_73 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f332,hypothesis,(
% 0.15/5.68 q20 = queue_79 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f333,hypothesis,(
% 0.15/5.68 q21 = queue_85 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f334,hypothesis,(
% 0.15/5.68 q22 = queue_91 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f335,hypothesis,(
% 0.15/5.68 q23 = queue_97 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f336,hypothesis,(
% 0.15/5.68 q24 = queue_103 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f337,hypothesis,(
% 0.15/5.68 q25 = queue_109 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f338,hypothesis,(
% 0.15/5.68 q26 = queue_115 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f339,hypothesis,(
% 0.15/5.68 q27 = queue_121 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f340,hypothesis,(
% 0.15/5.68 q28 = queue_127 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f341,hypothesis,(
% 0.15/5.68 q29 = queue_133 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f342,hypothesis,(
% 0.15/5.68 q3 = queue_139 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f343,hypothesis,(
% 0.15/5.68 q30 = queue_145 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f344,hypothesis,(
% 0.15/5.68 q31 = queue_151 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f345,hypothesis,(
% 0.15/5.68 q32 = queue_157 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f346,hypothesis,(
% 0.15/5.68 q33 = queue_163 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f347,hypothesis,(
% 0.15/5.68 q34 = queue_169 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f348,hypothesis,(
% 0.15/5.68 q35 = queue_175 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f349,hypothesis,(
% 0.15/5.68 q36 = queue_181 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f350,hypothesis,(
% 0.15/5.68 q37 = queue_187 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f351,hypothesis,(
% 0.15/5.68 q38 = queue_193 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f352,hypothesis,(
% 0.15/5.68 q39 = queue_199 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f353,hypothesis,(
% 0.15/5.68 q4 = queue_205 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f354,hypothesis,(
% 0.15/5.68 q40 = queue_211 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f355,hypothesis,(
% 0.15/5.68 q41 = queue_217 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f356,hypothesis,(
% 0.15/5.68 q42 = queue_223 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f357,hypothesis,(
% 0.15/5.68 q43 = queue_229 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f358,hypothesis,(
% 0.15/5.68 q44 = queue_235 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f359,hypothesis,(
% 0.15/5.68 q45 = queue_241 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f360,hypothesis,(
% 0.15/5.68 q46 = queue_247 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f361,hypothesis,(
% 0.15/5.68 q47 = queue_253 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f362,hypothesis,(
% 0.15/5.68 q48 = queue_259 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f363,hypothesis,(
% 0.15/5.68 q49 = queue_265 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f364,hypothesis,(
% 0.15/5.68 q5 = queue_271 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f365,hypothesis,(
% 0.15/5.68 q6 = queue_277 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f366,hypothesis,(
% 0.15/5.68 q7 = queue_283 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f367,hypothesis,(
% 0.15/5.68 q8 = queue_289 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f368,hypothesis,(
% 0.15/5.68 q9 = queue_295 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f369,negated_conjecture,(
% 0.15/5.68 elem_298 != elem_301 ),
% 0.15/5.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.68 fof(f373,plain,(
% 0.15/5.68 ![X0,X1]: (rselect_seq(rstore_seq(X0,X1))=X1)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/5.68 fof(f374,plain,(
% 0.15/5.68 ![X0,X1]: (rselect_head(rstore_head(X0,X1))=X1)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/5.68 fof(f375,plain,(
% 0.15/5.68 ![X0,X1]: (rselect_tail(rstore_tail(X0,X1))=X1)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/5.68 fof(f377,plain,(
% 0.15/5.68 ![X0,X1]: (rselect_seq(rstore_tail(X0,X1))=rselect_seq(X0))),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f7])).
% 0.15/5.68 fof(f378,plain,(
% 0.15/5.68 ![X0,X1]: (rselect_head(rstore_tail(X0,X1))=rselect_head(X0))),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f8])).
% 0.15/5.68 fof(f379,plain,(
% 0.15/5.68 ![X0,X1]: (rselect_head(rstore_seq(X0,X1))=rselect_head(X0))),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f9])).
% 0.15/5.68 fof(f381,plain,(
% 0.15/5.68 ![X0,X1]: (rselect_tail(rstore_head(X0,X1))=rselect_tail(X0))),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f11])).
% 0.15/5.68 fof(f382,plain,(
% 0.15/5.68 ![X0]: (p(s(X0))=X0)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f12])).
% 0.15/5.68 fof(f386,plain,(
% 0.15/5.68 ![X0]: (s(s(s(X0)))=X0)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/5.68 fof(f460,plain,(
% 0.15/5.68 earray_296=rselect_seq(q49)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f90])).
% 0.15/5.68 fof(f486,plain,(
% 0.15/5.68 elem_298=select(earray_296,index_297)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f116])).
% 0.15/5.68 fof(f487,plain,(
% 0.15/5.68 elem_301=select(earray_296,index_300)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f117])).
% 0.15/5.68 fof(f488,plain,(
% 0.15/5.68 index_0=rselect_tail(q)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f118])).
% 0.15/5.68 fof(f489,plain,(
% 0.15/5.68 index_102=s(index_99)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f119])).
% 0.15/5.68 fof(f490,plain,(
% 0.15/5.68 index_105=rselect_tail(q24)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f120])).
% 0.15/5.68 fof(f491,plain,(
% 0.15/5.68 index_108=s(index_105)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f121])).
% 0.15/5.68 fof(f492,plain,(
% 0.15/5.68 index_111=rselect_tail(q25)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f122])).
% 0.15/5.68 fof(f493,plain,(
% 0.15/5.68 index_114=s(index_111)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f123])).
% 0.15/5.68 fof(f494,plain,(
% 0.15/5.68 index_117=rselect_tail(q26)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f124])).
% 0.15/5.68 fof(f495,plain,(
% 0.15/5.68 index_12=s(index_9)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f125])).
% 0.15/5.68 fof(f496,plain,(
% 0.15/5.68 index_120=s(index_117)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f126])).
% 0.15/5.68 fof(f497,plain,(
% 0.15/5.68 index_123=rselect_tail(q27)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/5.68 fof(f498,plain,(
% 0.15/5.68 index_126=s(index_123)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f128])).
% 0.15/5.68 fof(f499,plain,(
% 0.15/5.68 index_129=rselect_tail(q28)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f129])).
% 0.15/5.68 fof(f500,plain,(
% 0.15/5.68 index_132=s(index_129)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f130])).
% 0.15/5.68 fof(f501,plain,(
% 0.15/5.68 index_135=rselect_tail(q2)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f131])).
% 0.15/5.68 fof(f502,plain,(
% 0.15/5.68 index_138=s(index_135)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f132])).
% 0.15/5.68 fof(f503,plain,(
% 0.15/5.68 index_141=rselect_tail(q29)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f133])).
% 0.15/5.68 fof(f504,plain,(
% 0.15/5.68 index_144=s(index_141)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f134])).
% 0.15/5.68 fof(f505,plain,(
% 0.15/5.68 index_147=rselect_tail(q30)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f135])).
% 0.15/5.68 fof(f506,plain,(
% 0.15/5.68 index_15=rselect_tail(q10)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f136])).
% 0.15/5.68 fof(f507,plain,(
% 0.15/5.68 index_150=s(index_147)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f137])).
% 0.15/5.68 fof(f508,plain,(
% 0.15/5.68 index_153=rselect_tail(q31)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f138])).
% 0.15/5.68 fof(f509,plain,(
% 0.15/5.68 index_156=s(index_153)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f139])).
% 0.15/5.68 fof(f510,plain,(
% 0.15/5.68 index_159=rselect_tail(q32)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f140])).
% 0.15/5.68 fof(f511,plain,(
% 0.15/5.68 index_162=s(index_159)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f141])).
% 0.15/5.68 fof(f512,plain,(
% 0.15/5.68 index_165=rselect_tail(q33)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f142])).
% 0.15/5.68 fof(f513,plain,(
% 0.15/5.68 index_168=s(index_165)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f143])).
% 0.15/5.68 fof(f514,plain,(
% 0.15/5.68 index_171=rselect_tail(q34)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f144])).
% 0.15/5.68 fof(f515,plain,(
% 0.15/5.68 index_174=s(index_171)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f145])).
% 0.15/5.68 fof(f516,plain,(
% 0.15/5.68 index_177=rselect_tail(q35)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f146])).
% 0.15/5.68 fof(f517,plain,(
% 0.15/5.68 index_18=s(index_15)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f147])).
% 0.15/5.68 fof(f518,plain,(
% 0.15/5.68 index_180=s(index_177)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f148])).
% 0.15/5.68 fof(f519,plain,(
% 0.15/5.68 index_183=rselect_tail(q36)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f149])).
% 0.15/5.68 fof(f520,plain,(
% 0.15/5.68 index_186=s(index_183)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f150])).
% 0.15/5.68 fof(f521,plain,(
% 0.15/5.68 index_189=rselect_tail(q37)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f151])).
% 0.15/5.68 fof(f522,plain,(
% 0.15/5.68 index_192=s(index_189)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f152])).
% 0.15/5.68 fof(f523,plain,(
% 0.15/5.68 index_195=rselect_tail(q38)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f153])).
% 0.15/5.68 fof(f524,plain,(
% 0.15/5.68 index_198=s(index_195)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f154])).
% 0.15/5.68 fof(f525,plain,(
% 0.15/5.68 index_201=rselect_tail(q3)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f155])).
% 0.15/5.68 fof(f526,plain,(
% 0.15/5.68 index_204=s(index_201)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f156])).
% 0.15/5.68 fof(f527,plain,(
% 0.15/5.68 index_207=rselect_tail(q39)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f157])).
% 0.15/5.68 fof(f528,plain,(
% 0.15/5.68 index_21=rselect_tail(q11)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f158])).
% 0.15/5.68 fof(f529,plain,(
% 0.15/5.68 index_210=s(index_207)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f159])).
% 0.15/5.68 fof(f530,plain,(
% 0.15/5.68 index_213=rselect_tail(q40)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f160])).
% 0.15/5.68 fof(f531,plain,(
% 0.15/5.68 index_216=s(index_213)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f161])).
% 0.15/5.68 fof(f532,plain,(
% 0.15/5.68 index_219=rselect_tail(q41)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f162])).
% 0.15/5.68 fof(f533,plain,(
% 0.15/5.68 index_222=s(index_219)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f163])).
% 0.15/5.68 fof(f534,plain,(
% 0.15/5.68 index_225=rselect_tail(q42)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f164])).
% 0.15/5.68 fof(f535,plain,(
% 0.15/5.68 index_228=s(index_225)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f165])).
% 0.15/5.68 fof(f536,plain,(
% 0.15/5.68 index_231=rselect_tail(q43)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f166])).
% 0.15/5.68 fof(f537,plain,(
% 0.15/5.68 index_234=s(index_231)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f167])).
% 0.15/5.68 fof(f538,plain,(
% 0.15/5.68 index_237=rselect_tail(q44)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f168])).
% 0.15/5.68 fof(f539,plain,(
% 0.15/5.68 index_24=s(index_21)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f169])).
% 0.15/5.68 fof(f540,plain,(
% 0.15/5.68 index_240=s(index_237)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f170])).
% 0.15/5.68 fof(f541,plain,(
% 0.15/5.68 index_243=rselect_tail(q45)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f171])).
% 0.15/5.68 fof(f542,plain,(
% 0.15/5.68 index_246=s(index_243)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f172])).
% 0.15/5.68 fof(f543,plain,(
% 0.15/5.68 index_249=rselect_tail(q46)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f173])).
% 0.15/5.68 fof(f544,plain,(
% 0.15/5.68 index_252=s(index_249)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f174])).
% 0.15/5.68 fof(f545,plain,(
% 0.15/5.68 index_255=rselect_tail(q47)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f175])).
% 0.15/5.68 fof(f546,plain,(
% 0.15/5.68 index_258=s(index_255)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f176])).
% 0.15/5.68 fof(f547,plain,(
% 0.15/5.68 index_261=rselect_tail(q48)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f177])).
% 0.15/5.68 fof(f548,plain,(
% 0.15/5.68 index_264=s(index_261)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f178])).
% 0.15/5.68 fof(f549,plain,(
% 0.15/5.68 index_267=rselect_tail(q4)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f179])).
% 0.15/5.68 fof(f550,plain,(
% 0.15/5.68 index_27=rselect_tail(q12)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f180])).
% 0.15/5.68 fof(f551,plain,(
% 0.15/5.68 index_270=s(index_267)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f181])).
% 0.15/5.68 fof(f552,plain,(
% 0.15/5.68 index_273=rselect_tail(q5)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f182])).
% 0.15/5.68 fof(f553,plain,(
% 0.15/5.68 index_276=s(index_273)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f183])).
% 0.15/5.68 fof(f554,plain,(
% 0.15/5.68 index_279=rselect_tail(q6)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f184])).
% 0.15/5.68 fof(f555,plain,(
% 0.15/5.68 index_282=s(index_279)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f185])).
% 0.15/5.68 fof(f556,plain,(
% 0.15/5.68 index_285=rselect_tail(q7)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f186])).
% 0.15/5.68 fof(f557,plain,(
% 0.15/5.68 index_288=s(index_285)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f187])).
% 0.15/5.68 fof(f558,plain,(
% 0.15/5.68 index_291=rselect_tail(q8)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f188])).
% 0.15/5.68 fof(f559,plain,(
% 0.15/5.68 index_294=s(index_291)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f189])).
% 0.15/5.68 fof(f560,plain,(
% 0.15/5.68 index_297=rselect_head(q49)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f190])).
% 0.15/5.68 fof(f561,plain,(
% 0.15/5.68 index_299=rselect_tail(q49)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f191])).
% 0.15/5.68 fof(f562,plain,(
% 0.15/5.68 index_3=rselect_tail(q0)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f192])).
% 0.15/5.68 fof(f563,plain,(
% 0.15/5.68 index_30=s(index_27)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f193])).
% 0.15/5.68 fof(f564,plain,(
% 0.15/5.68 s(index_300)=index_299),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f194])).
% 0.15/5.68 fof(f565,plain,(
% 0.15/5.68 index_33=rselect_tail(q13)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f195])).
% 0.15/5.68 fof(f566,plain,(
% 0.15/5.68 index_36=s(index_33)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f196])).
% 0.15/5.68 fof(f567,plain,(
% 0.15/5.68 index_39=rselect_tail(q14)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f197])).
% 0.15/5.68 fof(f568,plain,(
% 0.15/5.68 index_42=s(index_39)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f198])).
% 0.15/5.68 fof(f569,plain,(
% 0.15/5.68 index_45=rselect_tail(q15)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f199])).
% 0.15/5.68 fof(f570,plain,(
% 0.15/5.68 index_48=s(index_45)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f200])).
% 0.15/5.68 fof(f571,plain,(
% 0.15/5.68 index_51=rselect_tail(q16)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f201])).
% 0.15/5.68 fof(f572,plain,(
% 0.15/5.68 index_54=s(index_51)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f202])).
% 0.15/5.68 fof(f573,plain,(
% 0.15/5.68 index_57=rselect_tail(q17)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f203])).
% 0.15/5.68 fof(f574,plain,(
% 0.15/5.68 index_6=s(index_3)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f204])).
% 0.15/5.68 fof(f575,plain,(
% 0.15/5.68 index_60=s(index_57)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f205])).
% 0.15/5.68 fof(f576,plain,(
% 0.15/5.68 index_63=rselect_tail(q18)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f206])).
% 0.15/5.68 fof(f577,plain,(
% 0.15/5.68 index_66=s(index_63)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f207])).
% 0.15/5.68 fof(f578,plain,(
% 0.15/5.68 index_69=rselect_tail(q1)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f208])).
% 0.15/5.68 fof(f579,plain,(
% 0.15/5.68 index_72=s(index_69)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f209])).
% 0.15/5.68 fof(f580,plain,(
% 0.15/5.68 index_75=rselect_tail(q19)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f210])).
% 0.15/5.68 fof(f581,plain,(
% 0.15/5.68 index_78=s(index_75)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f211])).
% 0.15/5.68 fof(f582,plain,(
% 0.15/5.68 index_81=rselect_tail(q20)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f212])).
% 0.15/5.68 fof(f583,plain,(
% 0.15/5.68 index_84=s(index_81)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f213])).
% 0.15/5.68 fof(f584,plain,(
% 0.15/5.68 index_87=rselect_tail(q21)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f214])).
% 0.15/5.68 fof(f585,plain,(
% 0.15/5.68 index_9=rselect_tail(q9)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f215])).
% 0.15/5.68 fof(f586,plain,(
% 0.15/5.68 index_90=s(index_87)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f216])).
% 0.15/5.68 fof(f587,plain,(
% 0.15/5.68 index_93=rselect_tail(q22)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f217])).
% 0.15/5.68 fof(f588,plain,(
% 0.15/5.68 index_96=s(index_93)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f218])).
% 0.15/5.68 fof(f589,plain,(
% 0.15/5.68 index_99=rselect_tail(q23)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f219])).
% 0.15/5.68 fof(f590,plain,(
% 0.15/5.68 queue_1=rstore_head(q,index_0)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f220])).
% 0.15/5.68 fof(f591,plain,(
% 0.15/5.68 queue_101=rstore_seq(q23,earray_100)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f221])).
% 0.15/5.68 fof(f592,plain,(
% 0.15/5.68 queue_103=rstore_tail(queue_101,index_102)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f222])).
% 0.15/5.68 fof(f593,plain,(
% 0.15/5.68 queue_107=rstore_seq(q24,earray_106)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f223])).
% 0.15/5.68 fof(f594,plain,(
% 0.15/5.68 queue_109=rstore_tail(queue_107,index_108)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f224])).
% 0.15/5.68 fof(f595,plain,(
% 0.15/5.68 queue_11=rstore_seq(q9,earray_10)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f225])).
% 0.15/5.68 fof(f596,plain,(
% 0.15/5.68 queue_113=rstore_seq(q25,earray_112)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f226])).
% 0.15/5.68 fof(f597,plain,(
% 0.15/5.68 queue_115=rstore_tail(queue_113,index_114)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f227])).
% 0.15/5.68 fof(f598,plain,(
% 0.15/5.68 queue_119=rstore_seq(q26,earray_118)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f228])).
% 0.15/5.68 fof(f599,plain,(
% 0.15/5.68 queue_121=rstore_tail(queue_119,index_120)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f229])).
% 0.15/5.68 fof(f600,plain,(
% 0.15/5.68 queue_125=rstore_seq(q27,earray_124)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f230])).
% 0.15/5.68 fof(f601,plain,(
% 0.15/5.68 queue_127=rstore_tail(queue_125,index_126)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f231])).
% 0.15/5.68 fof(f602,plain,(
% 0.15/5.68 queue_13=rstore_tail(queue_11,index_12)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f232])).
% 0.15/5.68 fof(f603,plain,(
% 0.15/5.68 queue_131=rstore_seq(q28,earray_130)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f233])).
% 0.15/5.68 fof(f604,plain,(
% 0.15/5.68 queue_133=rstore_tail(queue_131,index_132)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f234])).
% 0.15/5.68 fof(f605,plain,(
% 0.15/5.68 queue_137=rstore_seq(q2,earray_136)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f235])).
% 0.15/5.68 fof(f606,plain,(
% 0.15/5.68 queue_139=rstore_tail(queue_137,index_138)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f236])).
% 0.15/5.68 fof(f607,plain,(
% 0.15/5.68 queue_143=rstore_seq(q29,earray_142)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f237])).
% 0.15/5.68 fof(f608,plain,(
% 0.15/5.68 queue_145=rstore_tail(queue_143,index_144)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f238])).
% 0.15/5.68 fof(f609,plain,(
% 0.15/5.68 queue_149=rstore_seq(q30,earray_148)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f239])).
% 0.15/5.68 fof(f610,plain,(
% 0.15/5.68 queue_151=rstore_tail(queue_149,index_150)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f240])).
% 0.15/5.68 fof(f611,plain,(
% 0.15/5.68 queue_155=rstore_seq(q31,earray_154)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f241])).
% 0.15/5.68 fof(f612,plain,(
% 0.15/5.68 queue_157=rstore_tail(queue_155,index_156)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f242])).
% 0.15/5.68 fof(f613,plain,(
% 0.15/5.68 queue_161=rstore_seq(q32,earray_160)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f243])).
% 0.15/5.68 fof(f614,plain,(
% 0.15/5.68 queue_163=rstore_tail(queue_161,index_162)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f244])).
% 0.15/5.68 fof(f615,plain,(
% 0.15/5.68 queue_167=rstore_seq(q33,earray_166)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f245])).
% 0.15/5.68 fof(f616,plain,(
% 0.15/5.68 queue_169=rstore_tail(queue_167,index_168)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f246])).
% 0.15/5.68 fof(f617,plain,(
% 0.15/5.68 queue_17=rstore_seq(q10,earray_16)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f247])).
% 0.15/5.68 fof(f618,plain,(
% 0.15/5.68 queue_173=rstore_seq(q34,earray_172)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f248])).
% 0.15/5.68 fof(f619,plain,(
% 0.15/5.68 queue_175=rstore_tail(queue_173,index_174)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f249])).
% 0.15/5.68 fof(f620,plain,(
% 0.15/5.68 queue_179=rstore_seq(q35,earray_178)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f250])).
% 0.15/5.68 fof(f621,plain,(
% 0.15/5.68 queue_181=rstore_tail(queue_179,index_180)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f251])).
% 0.15/5.68 fof(f622,plain,(
% 0.15/5.68 queue_185=rstore_seq(q36,earray_184)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f252])).
% 0.15/5.68 fof(f623,plain,(
% 0.15/5.68 queue_187=rstore_tail(queue_185,index_186)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f253])).
% 0.15/5.68 fof(f624,plain,(
% 0.15/5.68 queue_19=rstore_tail(queue_17,index_18)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f254])).
% 0.15/5.68 fof(f625,plain,(
% 0.15/5.68 queue_191=rstore_seq(q37,earray_190)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f255])).
% 0.15/5.68 fof(f626,plain,(
% 0.15/5.68 queue_193=rstore_tail(queue_191,index_192)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f256])).
% 0.15/5.68 fof(f627,plain,(
% 0.15/5.68 queue_197=rstore_seq(q38,earray_196)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f257])).
% 0.15/5.68 fof(f628,plain,(
% 0.15/5.68 queue_199=rstore_tail(queue_197,index_198)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f258])).
% 0.15/5.68 fof(f629,plain,(
% 0.15/5.68 queue_203=rstore_seq(q3,earray_202)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f259])).
% 0.15/5.68 fof(f630,plain,(
% 0.15/5.68 queue_205=rstore_tail(queue_203,index_204)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f260])).
% 0.15/5.68 fof(f631,plain,(
% 0.15/5.68 queue_209=rstore_seq(q39,earray_208)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f261])).
% 0.15/5.68 fof(f632,plain,(
% 0.15/5.68 queue_211=rstore_tail(queue_209,index_210)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f262])).
% 0.15/5.68 fof(f633,plain,(
% 0.15/5.68 queue_215=rstore_seq(q40,earray_214)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f263])).
% 0.15/5.68 fof(f634,plain,(
% 0.15/5.68 queue_217=rstore_tail(queue_215,index_216)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f264])).
% 0.15/5.68 fof(f635,plain,(
% 0.15/5.68 queue_221=rstore_seq(q41,earray_220)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f265])).
% 0.15/5.68 fof(f636,plain,(
% 0.15/5.68 queue_223=rstore_tail(queue_221,index_222)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f266])).
% 0.15/5.68 fof(f637,plain,(
% 0.15/5.68 queue_227=rstore_seq(q42,earray_226)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f267])).
% 0.15/5.68 fof(f638,plain,(
% 0.15/5.68 queue_229=rstore_tail(queue_227,index_228)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f268])).
% 0.15/5.68 fof(f639,plain,(
% 0.15/5.68 queue_23=rstore_seq(q11,earray_22)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f269])).
% 0.15/5.68 fof(f640,plain,(
% 0.15/5.68 queue_233=rstore_seq(q43,earray_232)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f270])).
% 0.15/5.68 fof(f641,plain,(
% 0.15/5.68 queue_235=rstore_tail(queue_233,index_234)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f271])).
% 0.15/5.68 fof(f642,plain,(
% 0.15/5.68 queue_239=rstore_seq(q44,earray_238)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f272])).
% 0.15/5.68 fof(f643,plain,(
% 0.15/5.68 queue_241=rstore_tail(queue_239,index_240)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f273])).
% 0.15/5.68 fof(f644,plain,(
% 0.15/5.68 queue_245=rstore_seq(q45,earray_244)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f274])).
% 0.15/5.68 fof(f645,plain,(
% 0.15/5.68 queue_247=rstore_tail(queue_245,index_246)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f275])).
% 0.15/5.68 fof(f646,plain,(
% 0.15/5.68 queue_25=rstore_tail(queue_23,index_24)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f276])).
% 0.15/5.68 fof(f647,plain,(
% 0.15/5.68 queue_251=rstore_seq(q46,earray_250)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f277])).
% 0.15/5.68 fof(f648,plain,(
% 0.15/5.68 queue_253=rstore_tail(queue_251,index_252)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f278])).
% 0.15/5.68 fof(f649,plain,(
% 0.15/5.68 queue_257=rstore_seq(q47,earray_256)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f279])).
% 0.15/5.68 fof(f650,plain,(
% 0.15/5.68 queue_259=rstore_tail(queue_257,index_258)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f280])).
% 0.15/5.68 fof(f651,plain,(
% 0.15/5.68 queue_263=rstore_seq(q48,earray_262)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f281])).
% 0.15/5.68 fof(f652,plain,(
% 0.15/5.68 queue_265=rstore_tail(queue_263,index_264)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f282])).
% 0.15/5.68 fof(f653,plain,(
% 0.15/5.68 queue_269=rstore_seq(q4,earray_268)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f283])).
% 0.15/5.68 fof(f654,plain,(
% 0.15/5.68 queue_271=rstore_tail(queue_269,index_270)),
% 0.15/5.68 inference(cnf_transformation,[status(thm)],[f284])).
% 0.15/5.69 fof(f655,plain,(
% 0.15/5.69 queue_275=rstore_seq(q5,earray_274)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f285])).
% 0.15/5.69 fof(f656,plain,(
% 0.15/5.69 queue_277=rstore_tail(queue_275,index_276)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f286])).
% 0.15/5.69 fof(f657,plain,(
% 0.15/5.69 queue_281=rstore_seq(q6,earray_280)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f287])).
% 0.15/5.69 fof(f658,plain,(
% 0.15/5.69 queue_283=rstore_tail(queue_281,index_282)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f288])).
% 0.15/5.69 fof(f659,plain,(
% 0.15/5.69 queue_287=rstore_seq(q7,earray_286)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f289])).
% 0.15/5.69 fof(f660,plain,(
% 0.15/5.69 queue_289=rstore_tail(queue_287,index_288)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f290])).
% 0.15/5.69 fof(f661,plain,(
% 0.15/5.69 queue_29=rstore_seq(q12,earray_28)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f291])).
% 0.15/5.69 fof(f662,plain,(
% 0.15/5.69 queue_293=rstore_seq(q8,earray_292)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f292])).
% 0.15/5.69 fof(f663,plain,(
% 0.15/5.69 queue_295=rstore_tail(queue_293,index_294)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f293])).
% 0.15/5.69 fof(f664,plain,(
% 0.15/5.69 queue_31=rstore_tail(queue_29,index_30)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f294])).
% 0.15/5.69 fof(f665,plain,(
% 0.15/5.69 queue_35=rstore_seq(q13,earray_34)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f295])).
% 0.15/5.69 fof(f666,plain,(
% 0.15/5.69 queue_37=rstore_tail(queue_35,index_36)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f296])).
% 0.15/5.69 fof(f667,plain,(
% 0.15/5.69 queue_41=rstore_seq(q14,earray_40)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f297])).
% 0.15/5.69 fof(f668,plain,(
% 0.15/5.69 queue_43=rstore_tail(queue_41,index_42)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f298])).
% 0.15/5.69 fof(f669,plain,(
% 0.15/5.69 queue_47=rstore_seq(q15,earray_46)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f299])).
% 0.15/5.69 fof(f670,plain,(
% 0.15/5.69 queue_49=rstore_tail(queue_47,index_48)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f300])).
% 0.15/5.69 fof(f671,plain,(
% 0.15/5.69 queue_5=rstore_seq(q0,earray_4)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f301])).
% 0.15/5.69 fof(f672,plain,(
% 0.15/5.69 queue_53=rstore_seq(q16,earray_52)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f302])).
% 0.15/5.69 fof(f673,plain,(
% 0.15/5.69 queue_55=rstore_tail(queue_53,index_54)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f303])).
% 0.15/5.69 fof(f674,plain,(
% 0.15/5.69 queue_59=rstore_seq(q17,earray_58)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f304])).
% 0.15/5.69 fof(f675,plain,(
% 0.15/5.69 queue_61=rstore_tail(queue_59,index_60)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f305])).
% 0.15/5.69 fof(f676,plain,(
% 0.15/5.69 queue_65=rstore_seq(q18,earray_64)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f306])).
% 0.15/5.69 fof(f677,plain,(
% 0.15/5.69 queue_67=rstore_tail(queue_65,index_66)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f307])).
% 0.15/5.69 fof(f678,plain,(
% 0.15/5.69 queue_7=rstore_tail(queue_5,index_6)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f308])).
% 0.15/5.69 fof(f679,plain,(
% 0.15/5.69 queue_71=rstore_seq(q1,earray_70)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f309])).
% 0.15/5.69 fof(f680,plain,(
% 0.15/5.69 queue_73=rstore_tail(queue_71,index_72)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f310])).
% 0.15/5.69 fof(f681,plain,(
% 0.15/5.69 queue_77=rstore_seq(q19,earray_76)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f311])).
% 0.15/5.69 fof(f682,plain,(
% 0.15/5.69 queue_79=rstore_tail(queue_77,index_78)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f312])).
% 0.15/5.69 fof(f683,plain,(
% 0.15/5.69 queue_83=rstore_seq(q20,earray_82)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f313])).
% 0.15/5.69 fof(f684,plain,(
% 0.15/5.69 queue_85=rstore_tail(queue_83,index_84)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f314])).
% 0.15/5.69 fof(f685,plain,(
% 0.15/5.69 queue_89=rstore_seq(q21,earray_88)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f315])).
% 0.15/5.69 fof(f686,plain,(
% 0.15/5.69 queue_91=rstore_tail(queue_89,index_90)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f316])).
% 0.15/5.69 fof(f687,plain,(
% 0.15/5.69 queue_95=rstore_seq(q22,earray_94)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f317])).
% 0.15/5.69 fof(f688,plain,(
% 0.15/5.69 queue_97=rstore_tail(queue_95,index_96)),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f318])).
% 0.15/5.69 fof(f689,plain,(
% 0.15/5.69 q0=queue_1),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f319])).
% 0.15/5.69 fof(f690,plain,(
% 0.15/5.69 q1=queue_7),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f320])).
% 0.15/5.69 fof(f691,plain,(
% 0.15/5.69 q10=queue_13),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f321])).
% 0.15/5.69 fof(f692,plain,(
% 0.15/5.69 q11=queue_19),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f322])).
% 0.15/5.69 fof(f693,plain,(
% 0.15/5.69 q12=queue_25),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f323])).
% 0.15/5.69 fof(f694,plain,(
% 0.15/5.69 q13=queue_31),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f324])).
% 0.15/5.69 fof(f695,plain,(
% 0.15/5.69 q14=queue_37),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f325])).
% 0.15/5.69 fof(f696,plain,(
% 0.15/5.69 q15=queue_43),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f326])).
% 0.15/5.69 fof(f697,plain,(
% 0.15/5.69 q16=queue_49),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f327])).
% 0.15/5.69 fof(f698,plain,(
% 0.15/5.69 q17=queue_55),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f328])).
% 0.15/5.69 fof(f699,plain,(
% 0.15/5.69 q18=queue_61),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f329])).
% 0.15/5.69 fof(f700,plain,(
% 0.15/5.69 q19=queue_67),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f330])).
% 0.15/5.69 fof(f701,plain,(
% 0.15/5.69 q2=queue_73),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f331])).
% 0.15/5.69 fof(f702,plain,(
% 0.15/5.69 q20=queue_79),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f332])).
% 0.15/5.69 fof(f703,plain,(
% 0.15/5.69 q21=queue_85),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f333])).
% 0.15/5.69 fof(f704,plain,(
% 0.15/5.69 q22=queue_91),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f334])).
% 0.15/5.69 fof(f705,plain,(
% 0.15/5.69 q23=queue_97),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f335])).
% 0.15/5.69 fof(f706,plain,(
% 0.15/5.69 q24=queue_103),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f336])).
% 0.15/5.69 fof(f707,plain,(
% 0.15/5.69 q25=queue_109),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f337])).
% 0.15/5.69 fof(f708,plain,(
% 0.15/5.69 q26=queue_115),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f338])).
% 0.15/5.69 fof(f709,plain,(
% 0.15/5.69 q27=queue_121),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f339])).
% 0.15/5.69 fof(f710,plain,(
% 0.15/5.69 q28=queue_127),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f340])).
% 0.15/5.69 fof(f711,plain,(
% 0.15/5.69 q29=queue_133),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f341])).
% 0.15/5.69 fof(f712,plain,(
% 0.15/5.69 q3=queue_139),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f342])).
% 0.15/5.69 fof(f713,plain,(
% 0.15/5.69 q30=queue_145),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f343])).
% 0.15/5.69 fof(f714,plain,(
% 0.15/5.69 q31=queue_151),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f344])).
% 0.15/5.69 fof(f715,plain,(
% 0.15/5.69 q32=queue_157),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f345])).
% 0.15/5.69 fof(f716,plain,(
% 0.15/5.69 q33=queue_163),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f346])).
% 0.15/5.69 fof(f717,plain,(
% 0.15/5.69 q34=queue_169),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f347])).
% 0.15/5.69 fof(f718,plain,(
% 0.15/5.69 q35=queue_175),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f348])).
% 0.15/5.69 fof(f719,plain,(
% 0.15/5.69 q36=queue_181),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f349])).
% 0.15/5.69 fof(f720,plain,(
% 0.15/5.69 q37=queue_187),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f350])).
% 0.15/5.69 fof(f721,plain,(
% 0.15/5.69 q38=queue_193),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f351])).
% 0.15/5.69 fof(f722,plain,(
% 0.15/5.69 q39=queue_199),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f352])).
% 0.15/5.69 fof(f723,plain,(
% 0.15/5.69 q4=queue_205),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f353])).
% 0.15/5.69 fof(f724,plain,(
% 0.15/5.69 q40=queue_211),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f354])).
% 0.15/5.69 fof(f725,plain,(
% 0.15/5.69 q41=queue_217),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f355])).
% 0.15/5.69 fof(f726,plain,(
% 0.15/5.69 q42=queue_223),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f356])).
% 0.15/5.69 fof(f727,plain,(
% 0.15/5.69 q43=queue_229),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f357])).
% 0.15/5.69 fof(f728,plain,(
% 0.15/5.69 q44=queue_235),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f358])).
% 0.15/5.69 fof(f729,plain,(
% 0.15/5.69 q45=queue_241),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f359])).
% 0.15/5.69 fof(f730,plain,(
% 0.15/5.69 q46=queue_247),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f360])).
% 0.15/5.69 fof(f731,plain,(
% 0.15/5.69 q47=queue_253),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f361])).
% 0.15/5.69 fof(f732,plain,(
% 0.15/5.69 q48=queue_259),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f362])).
% 0.15/5.69 fof(f733,plain,(
% 0.15/5.69 q49=queue_265),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f363])).
% 0.15/5.69 fof(f734,plain,(
% 0.15/5.69 q5=queue_271),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f364])).
% 0.15/5.69 fof(f735,plain,(
% 0.15/5.69 q6=queue_277),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f365])).
% 0.15/5.69 fof(f736,plain,(
% 0.15/5.69 q7=queue_283),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f366])).
% 0.15/5.69 fof(f737,plain,(
% 0.15/5.69 q8=queue_289),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f367])).
% 0.15/5.69 fof(f738,plain,(
% 0.15/5.69 q9=queue_295),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f368])).
% 0.15/5.69 fof(f739,plain,(
% 0.15/5.69 ~elem_298=elem_301),
% 0.15/5.69 inference(cnf_transformation,[status(thm)],[f369])).
% 0.15/5.69 fof(f866,plain,(
% 0.15/5.69 p(index_12)=index_9),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f495,f382])).
% 0.15/5.69 fof(f910,plain,(
% 0.15/5.69 p(index_18)=index_15),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f517,f382])).
% 0.15/5.69 fof(f930,plain,(
% 0.15/5.69 p(index_204)=index_201),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f526,f382])).
% 0.15/5.69 fof(f978,plain,(
% 0.15/5.69 p(index_270)=index_267),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f551,f382])).
% 0.15/5.69 fof(f986,plain,(
% 0.15/5.69 p(index_282)=index_279),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f555,f382])).
% 0.15/5.69 fof(f990,plain,(
% 0.15/5.69 p(index_288)=index_285),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f557,f382])).
% 0.15/5.69 fof(f998,plain,(
% 0.15/5.69 p(index_30)=index_27),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f563,f382])).
% 0.15/5.69 fof(f1002,plain,(
% 0.15/5.69 p(index_299)=index_300),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f564,f382])).
% 0.15/5.69 fof(f1052,plain,(
% 0.15/5.69 q0=rstore_head(q,index_0)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f689,f590])).
% 0.15/5.69 fof(f1053,plain,(
% 0.15/5.69 rselect_tail(q0)=rselect_tail(q)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1052,f381])).
% 0.15/5.69 fof(f1055,plain,(
% 0.15/5.69 rselect_head(q0)=index_0),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1052,f374])).
% 0.15/5.69 fof(f1056,plain,(
% 0.15/5.69 index_3=rselect_tail(q)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f562,f1053])).
% 0.15/5.69 fof(f1059,plain,(
% 0.15/5.69 rselect_head(queue_101)=rselect_head(q23)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f591,f379])).
% 0.15/5.69 fof(f1062,plain,(
% 0.15/5.69 q24=rstore_tail(queue_101,index_102)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f706,f592])).
% 0.15/5.69 fof(f1063,plain,(
% 0.15/5.69 rselect_head(q24)=rselect_head(queue_101)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1062,f378])).
% 0.15/5.69 fof(f1065,plain,(
% 0.15/5.69 rselect_tail(q24)=index_102),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1062,f375])).
% 0.15/5.69 fof(f1067,plain,(
% 0.15/5.69 index_105=index_102),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f490,f1065])).
% 0.15/5.69 fof(f1070,plain,(
% 0.15/5.69 index_105=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1067,f489])).
% 0.15/5.69 fof(f1072,plain,(
% 0.15/5.69 rselect_head(queue_107)=rselect_head(q24)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f593,f379])).
% 0.15/5.69 fof(f1076,plain,(
% 0.15/5.69 q25=rstore_tail(queue_107,index_108)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f707,f594])).
% 0.15/5.69 fof(f1077,plain,(
% 0.15/5.69 rselect_head(q25)=rselect_head(queue_107)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1076,f378])).
% 0.15/5.69 fof(f1079,plain,(
% 0.15/5.69 rselect_tail(q25)=index_108),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1076,f375])).
% 0.15/5.69 fof(f1081,plain,(
% 0.15/5.69 index_111=index_108),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f492,f1079])).
% 0.15/5.69 fof(f1083,plain,(
% 0.15/5.69 rselect_head(queue_11)=rselect_head(q9)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f595,f379])).
% 0.15/5.69 fof(f1088,plain,(
% 0.15/5.69 index_111=s(index_105)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1081,f491])).
% 0.15/5.69 fof(f1091,plain,(
% 0.15/5.69 rselect_head(queue_113)=rselect_head(q25)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f596,f379])).
% 0.15/5.69 fof(f1094,plain,(
% 0.15/5.69 q26=rstore_tail(queue_113,index_114)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f708,f597])).
% 0.15/5.69 fof(f1095,plain,(
% 0.15/5.69 rselect_head(q26)=rselect_head(queue_113)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1094,f378])).
% 0.15/5.69 fof(f1097,plain,(
% 0.15/5.69 rselect_tail(q26)=index_114),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1094,f375])).
% 0.15/5.69 fof(f1099,plain,(
% 0.15/5.69 index_117=index_114),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f494,f1097])).
% 0.15/5.69 fof(f1101,plain,(
% 0.15/5.69 rselect_head(queue_119)=rselect_head(q26)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f598,f379])).
% 0.15/5.69 fof(f1106,plain,(
% 0.15/5.69 index_117=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1099,f493])).
% 0.15/5.69 fof(f1107,plain,(
% 0.15/5.69 q27=rstore_tail(queue_119,index_120)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f709,f599])).
% 0.15/5.69 fof(f1108,plain,(
% 0.15/5.69 rselect_head(q27)=rselect_head(queue_119)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1107,f378])).
% 0.15/5.69 fof(f1110,plain,(
% 0.15/5.69 rselect_tail(q27)=index_120),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1107,f375])).
% 0.15/5.69 fof(f1112,plain,(
% 0.15/5.69 index_123=index_120),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f497,f1110])).
% 0.15/5.69 fof(f1115,plain,(
% 0.15/5.69 index_123=s(index_117)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1112,f496])).
% 0.15/5.69 fof(f1117,plain,(
% 0.15/5.69 rselect_head(queue_125)=rselect_head(q27)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f600,f379])).
% 0.15/5.69 fof(f1120,plain,(
% 0.15/5.69 q28=rstore_tail(queue_125,index_126)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f710,f601])).
% 0.15/5.69 fof(f1121,plain,(
% 0.15/5.69 rselect_head(q28)=rselect_head(queue_125)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1120,f378])).
% 0.15/5.69 fof(f1123,plain,(
% 0.15/5.69 rselect_tail(q28)=index_126),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1120,f375])).
% 0.15/5.69 fof(f1125,plain,(
% 0.15/5.69 index_129=index_126),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f499,f1123])).
% 0.15/5.69 fof(f1128,plain,(
% 0.15/5.69 index_129=s(index_123)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1125,f498])).
% 0.15/5.69 fof(f1129,plain,(
% 0.15/5.69 q10=rstore_tail(queue_11,index_12)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f691,f602])).
% 0.15/5.69 fof(f1130,plain,(
% 0.15/5.69 rselect_head(q10)=rselect_head(queue_11)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1129,f378])).
% 0.15/5.69 fof(f1132,plain,(
% 0.15/5.69 rselect_tail(q10)=index_12),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1129,f375])).
% 0.15/5.69 fof(f1134,plain,(
% 0.15/5.69 index_15=index_12),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f506,f1132])).
% 0.15/5.69 fof(f1136,plain,(
% 0.15/5.69 rselect_head(queue_131)=rselect_head(q28)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f603,f379])).
% 0.15/5.69 fof(f1139,plain,(
% 0.15/5.69 q29=rstore_tail(queue_131,index_132)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f711,f604])).
% 0.15/5.69 fof(f1140,plain,(
% 0.15/5.69 rselect_head(q29)=rselect_head(queue_131)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1139,f378])).
% 0.15/5.69 fof(f1142,plain,(
% 0.15/5.69 rselect_tail(q29)=index_132),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1139,f375])).
% 0.15/5.69 fof(f1144,plain,(
% 0.15/5.69 index_141=index_132),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f503,f1142])).
% 0.15/5.69 fof(f1147,plain,(
% 0.15/5.69 index_15=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1134,f495])).
% 0.15/5.69 fof(f1149,plain,(
% 0.15/5.69 rselect_head(queue_137)=rselect_head(q2)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f605,f379])).
% 0.15/5.69 fof(f1154,plain,(
% 0.15/5.69 index_141=s(index_129)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1144,f500])).
% 0.15/5.69 fof(f1155,plain,(
% 0.15/5.69 q3=rstore_tail(queue_137,index_138)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f712,f606])).
% 0.15/5.69 fof(f1156,plain,(
% 0.15/5.69 rselect_head(q3)=rselect_head(queue_137)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1155,f378])).
% 0.15/5.69 fof(f1158,plain,(
% 0.15/5.69 rselect_tail(q3)=index_138),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1155,f375])).
% 0.15/5.69 fof(f1160,plain,(
% 0.15/5.69 index_201=index_138),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f525,f1158])).
% 0.15/5.69 fof(f1162,plain,(
% 0.15/5.69 rselect_head(queue_143)=rselect_head(q29)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f607,f379])).
% 0.15/5.69 fof(f1167,plain,(
% 0.15/5.69 index_201=s(index_135)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1160,f502])).
% 0.15/5.69 fof(f1168,plain,(
% 0.15/5.69 q30=rstore_tail(queue_143,index_144)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f713,f608])).
% 0.15/5.69 fof(f1169,plain,(
% 0.15/5.69 rselect_head(q30)=rselect_head(queue_143)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1168,f378])).
% 0.15/5.69 fof(f1171,plain,(
% 0.15/5.69 rselect_tail(q30)=index_144),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1168,f375])).
% 0.15/5.69 fof(f1173,plain,(
% 0.15/5.69 index_147=index_144),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f505,f1171])).
% 0.15/5.69 fof(f1175,plain,(
% 0.15/5.69 rselect_head(queue_149)=rselect_head(q30)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f609,f379])).
% 0.15/5.69 fof(f1178,plain,(
% 0.15/5.69 q31=rstore_tail(queue_149,index_150)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f714,f610])).
% 0.15/5.69 fof(f1179,plain,(
% 0.15/5.69 rselect_head(q31)=rselect_head(queue_149)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1178,f378])).
% 0.15/5.69 fof(f1181,plain,(
% 0.15/5.69 rselect_tail(q31)=index_150),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1178,f375])).
% 0.15/5.69 fof(f1183,plain,(
% 0.15/5.69 index_153=index_150),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f508,f1181])).
% 0.15/5.69 fof(f1186,plain,(
% 0.15/5.69 index_147=s(index_141)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1173,f504])).
% 0.15/5.69 fof(f1188,plain,(
% 0.15/5.69 rselect_head(queue_155)=rselect_head(q31)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f611,f379])).
% 0.15/5.69 fof(f1193,plain,(
% 0.15/5.69 index_153=s(index_147)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1183,f507])).
% 0.15/5.69 fof(f1194,plain,(
% 0.15/5.69 q32=rstore_tail(queue_155,index_156)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f715,f612])).
% 0.15/5.69 fof(f1195,plain,(
% 0.15/5.69 rselect_head(q32)=rselect_head(queue_155)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1194,f378])).
% 0.15/5.69 fof(f1197,plain,(
% 0.15/5.69 rselect_tail(q32)=index_156),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1194,f375])).
% 0.15/5.69 fof(f1199,plain,(
% 0.15/5.69 index_159=index_156),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f510,f1197])).
% 0.15/5.69 fof(f1201,plain,(
% 0.15/5.69 rselect_head(queue_161)=rselect_head(q32)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f613,f379])).
% 0.15/5.69 fof(f1206,plain,(
% 0.15/5.69 index_159=s(index_153)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1199,f509])).
% 0.15/5.69 fof(f1207,plain,(
% 0.15/5.69 q33=rstore_tail(queue_161,index_162)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f716,f614])).
% 0.15/5.69 fof(f1208,plain,(
% 0.15/5.69 rselect_head(q33)=rselect_head(queue_161)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1207,f378])).
% 0.15/5.69 fof(f1210,plain,(
% 0.15/5.69 rselect_tail(q33)=index_162),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1207,f375])).
% 0.15/5.69 fof(f1212,plain,(
% 0.15/5.69 index_165=index_162),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f512,f1210])).
% 0.15/5.69 fof(f1214,plain,(
% 0.15/5.69 rselect_head(queue_167)=rselect_head(q33)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f615,f379])).
% 0.15/5.69 fof(f1217,plain,(
% 0.15/5.69 q34=rstore_tail(queue_167,index_168)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f717,f616])).
% 0.15/5.69 fof(f1218,plain,(
% 0.15/5.69 rselect_head(q34)=rselect_head(queue_167)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1217,f378])).
% 0.15/5.69 fof(f1220,plain,(
% 0.15/5.69 rselect_tail(q34)=index_168),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1217,f375])).
% 0.15/5.69 fof(f1222,plain,(
% 0.15/5.69 index_171=index_168),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f514,f1220])).
% 0.15/5.69 fof(f1225,plain,(
% 0.15/5.69 index_165=s(index_159)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1212,f511])).
% 0.15/5.69 fof(f1227,plain,(
% 0.15/5.69 rselect_head(queue_17)=rselect_head(q10)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f617,f379])).
% 0.15/5.69 fof(f1232,plain,(
% 0.15/5.69 index_171=s(index_165)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1222,f513])).
% 0.15/5.69 fof(f1234,plain,(
% 0.15/5.69 rselect_head(queue_173)=rselect_head(q34)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f618,f379])).
% 0.15/5.69 fof(f1237,plain,(
% 0.15/5.69 q35=rstore_tail(queue_173,index_174)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f718,f619])).
% 0.15/5.69 fof(f1238,plain,(
% 0.15/5.69 rselect_head(q35)=rselect_head(queue_173)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1237,f378])).
% 0.15/5.69 fof(f1240,plain,(
% 0.15/5.69 rselect_tail(q35)=index_174),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1237,f375])).
% 0.15/5.69 fof(f1242,plain,(
% 0.15/5.69 index_177=index_174),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f516,f1240])).
% 0.15/5.69 fof(f1245,plain,(
% 0.15/5.69 index_177=s(index_171)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1242,f515])).
% 0.15/5.69 fof(f1247,plain,(
% 0.15/5.69 rselect_head(queue_179)=rselect_head(q35)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f620,f379])).
% 0.15/5.69 fof(f1250,plain,(
% 0.15/5.69 q36=rstore_tail(queue_179,index_180)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f719,f621])).
% 0.15/5.69 fof(f1251,plain,(
% 0.15/5.69 rselect_head(q36)=rselect_head(queue_179)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1250,f378])).
% 0.15/5.69 fof(f1253,plain,(
% 0.15/5.69 rselect_tail(q36)=index_180),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1250,f375])).
% 0.15/5.69 fof(f1255,plain,(
% 0.15/5.69 index_183=index_180),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f519,f1253])).
% 0.15/5.69 fof(f1257,plain,(
% 0.15/5.69 rselect_head(queue_185)=rselect_head(q36)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f622,f379])).
% 0.15/5.69 fof(f1262,plain,(
% 0.15/5.69 index_183=s(index_177)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1255,f518])).
% 0.15/5.69 fof(f1263,plain,(
% 0.15/5.69 q37=rstore_tail(queue_185,index_186)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f720,f623])).
% 0.15/5.69 fof(f1264,plain,(
% 0.15/5.69 rselect_head(q37)=rselect_head(queue_185)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1263,f378])).
% 0.15/5.69 fof(f1266,plain,(
% 0.15/5.69 rselect_tail(q37)=index_186),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1263,f375])).
% 0.15/5.69 fof(f1268,plain,(
% 0.15/5.69 index_189=index_186),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f521,f1266])).
% 0.15/5.69 fof(f1271,plain,(
% 0.15/5.69 index_189=s(index_183)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1268,f520])).
% 0.15/5.69 fof(f1272,plain,(
% 0.15/5.69 q11=rstore_tail(queue_17,index_18)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f692,f624])).
% 0.15/5.69 fof(f1273,plain,(
% 0.15/5.69 rselect_head(q11)=rselect_head(queue_17)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1272,f378])).
% 0.15/5.69 fof(f1275,plain,(
% 0.15/5.69 rselect_tail(q11)=index_18),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1272,f375])).
% 0.15/5.69 fof(f1277,plain,(
% 0.15/5.69 index_21=index_18),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f528,f1275])).
% 0.15/5.69 fof(f1279,plain,(
% 0.15/5.69 rselect_head(queue_191)=rselect_head(q37)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f625,f379])).
% 0.15/5.69 fof(f1284,plain,(
% 0.15/5.69 index_21=s(index_15)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1277,f517])).
% 0.15/5.69 fof(f1285,plain,(
% 0.15/5.69 q38=rstore_tail(queue_191,index_192)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f721,f626])).
% 0.15/5.69 fof(f1286,plain,(
% 0.15/5.69 rselect_head(q38)=rselect_head(queue_191)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1285,f378])).
% 0.15/5.69 fof(f1288,plain,(
% 0.15/5.69 rselect_tail(q38)=index_192),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1285,f375])).
% 0.15/5.69 fof(f1290,plain,(
% 0.15/5.69 index_195=index_192),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f523,f1288])).
% 0.15/5.69 fof(f1292,plain,(
% 0.15/5.69 rselect_head(queue_197)=rselect_head(q38)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f627,f379])).
% 0.15/5.69 fof(f1295,plain,(
% 0.15/5.69 q39=rstore_tail(queue_197,index_198)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f722,f628])).
% 0.15/5.69 fof(f1296,plain,(
% 0.15/5.69 rselect_head(q39)=rselect_head(queue_197)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1295,f378])).
% 0.15/5.69 fof(f1298,plain,(
% 0.15/5.69 rselect_tail(q39)=index_198),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1295,f375])).
% 0.15/5.69 fof(f1300,plain,(
% 0.15/5.69 index_207=index_198),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f527,f1298])).
% 0.15/5.69 fof(f1303,plain,(
% 0.15/5.69 index_195=s(index_189)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1290,f522])).
% 0.15/5.69 fof(f1305,plain,(
% 0.15/5.69 rselect_head(queue_203)=rselect_head(q3)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f629,f379])).
% 0.15/5.69 fof(f1310,plain,(
% 0.15/5.69 index_207=s(index_195)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1300,f524])).
% 0.15/5.69 fof(f1311,plain,(
% 0.15/5.69 q4=rstore_tail(queue_203,index_204)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f723,f630])).
% 0.15/5.69 fof(f1312,plain,(
% 0.15/5.69 rselect_head(q4)=rselect_head(queue_203)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1311,f378])).
% 0.15/5.69 fof(f1314,plain,(
% 0.15/5.69 rselect_tail(q4)=index_204),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1311,f375])).
% 0.15/5.69 fof(f1316,plain,(
% 0.15/5.69 index_267=index_204),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f549,f1314])).
% 0.15/5.69 fof(f1318,plain,(
% 0.15/5.69 rselect_head(queue_209)=rselect_head(q39)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f631,f379])).
% 0.15/5.69 fof(f1323,plain,(
% 0.15/5.69 index_267=s(index_201)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1316,f526])).
% 0.15/5.69 fof(f1324,plain,(
% 0.15/5.69 q40=rstore_tail(queue_209,index_210)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f724,f632])).
% 0.15/5.69 fof(f1325,plain,(
% 0.15/5.69 rselect_head(q40)=rselect_head(queue_209)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1324,f378])).
% 0.15/5.69 fof(f1327,plain,(
% 0.15/5.69 rselect_tail(q40)=index_210),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1324,f375])).
% 0.15/5.69 fof(f1329,plain,(
% 0.15/5.69 index_213=index_210),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f530,f1327])).
% 0.15/5.69 fof(f1331,plain,(
% 0.15/5.69 rselect_head(queue_215)=rselect_head(q40)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f633,f379])).
% 0.15/5.69 fof(f1334,plain,(
% 0.15/5.69 q41=rstore_tail(queue_215,index_216)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f725,f634])).
% 0.15/5.69 fof(f1335,plain,(
% 0.15/5.69 rselect_head(q41)=rselect_head(queue_215)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1334,f378])).
% 0.15/5.69 fof(f1337,plain,(
% 0.15/5.69 rselect_tail(q41)=index_216),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1334,f375])).
% 0.15/5.69 fof(f1339,plain,(
% 0.15/5.69 index_219=index_216),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f532,f1337])).
% 0.15/5.69 fof(f1342,plain,(
% 0.15/5.69 index_213=s(index_207)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1329,f529])).
% 0.15/5.69 fof(f1344,plain,(
% 0.15/5.69 rselect_head(queue_221)=rselect_head(q41)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f635,f379])).
% 0.15/5.69 fof(f1349,plain,(
% 0.15/5.69 index_219=s(index_213)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1339,f531])).
% 0.15/5.69 fof(f1350,plain,(
% 0.15/5.69 q42=rstore_tail(queue_221,index_222)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f726,f636])).
% 0.15/5.69 fof(f1351,plain,(
% 0.15/5.69 rselect_head(q42)=rselect_head(queue_221)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1350,f378])).
% 0.15/5.69 fof(f1353,plain,(
% 0.15/5.69 rselect_tail(q42)=index_222),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1350,f375])).
% 0.15/5.69 fof(f1355,plain,(
% 0.15/5.69 index_225=index_222),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f534,f1353])).
% 0.15/5.69 fof(f1357,plain,(
% 0.15/5.69 rselect_head(queue_227)=rselect_head(q42)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f637,f379])).
% 0.15/5.69 fof(f1362,plain,(
% 0.15/5.69 index_225=s(index_219)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1355,f533])).
% 0.15/5.69 fof(f1363,plain,(
% 0.15/5.69 q43=rstore_tail(queue_227,index_228)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f727,f638])).
% 0.15/5.69 fof(f1364,plain,(
% 0.15/5.69 rselect_head(q43)=rselect_head(queue_227)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1363,f378])).
% 0.15/5.69 fof(f1366,plain,(
% 0.15/5.69 rselect_tail(q43)=index_228),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1363,f375])).
% 0.15/5.69 fof(f1368,plain,(
% 0.15/5.69 index_231=index_228),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f536,f1366])).
% 0.15/5.69 fof(f1370,plain,(
% 0.15/5.69 rselect_head(queue_23)=rselect_head(q11)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f639,f379])).
% 0.15/5.69 fof(f1374,plain,(
% 0.15/5.69 rselect_head(queue_233)=rselect_head(q43)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f640,f379])).
% 0.15/5.69 fof(f1379,plain,(
% 0.15/5.69 index_231=s(index_225)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1368,f535])).
% 0.15/5.69 fof(f1380,plain,(
% 0.15/5.69 q44=rstore_tail(queue_233,index_234)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f728,f641])).
% 0.15/5.69 fof(f1381,plain,(
% 0.15/5.69 rselect_head(q44)=rselect_head(queue_233)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1380,f378])).
% 0.15/5.69 fof(f1383,plain,(
% 0.15/5.69 rselect_tail(q44)=index_234),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1380,f375])).
% 0.15/5.69 fof(f1385,plain,(
% 0.15/5.69 index_237=index_234),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f538,f1383])).
% 0.15/5.69 fof(f1388,plain,(
% 0.15/5.69 index_237=s(index_231)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1385,f537])).
% 0.15/5.69 fof(f1390,plain,(
% 0.15/5.69 rselect_head(queue_239)=rselect_head(q44)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f642,f379])).
% 0.15/5.69 fof(f1393,plain,(
% 0.15/5.69 q45=rstore_tail(queue_239,index_240)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f729,f643])).
% 0.15/5.69 fof(f1394,plain,(
% 0.15/5.69 rselect_head(q45)=rselect_head(queue_239)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1393,f378])).
% 0.15/5.69 fof(f1396,plain,(
% 0.15/5.69 rselect_tail(q45)=index_240),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1393,f375])).
% 0.15/5.69 fof(f1398,plain,(
% 0.15/5.69 index_243=index_240),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f541,f1396])).
% 0.15/5.69 fof(f1401,plain,(
% 0.15/5.69 index_243=s(index_237)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1398,f540])).
% 0.15/5.69 fof(f1403,plain,(
% 0.15/5.69 rselect_head(queue_245)=rselect_head(q45)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f644,f379])).
% 0.15/5.69 fof(f1406,plain,(
% 0.15/5.69 q46=rstore_tail(queue_245,index_246)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f730,f645])).
% 0.15/5.69 fof(f1407,plain,(
% 0.15/5.69 rselect_head(q46)=rselect_head(queue_245)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1406,f378])).
% 0.15/5.69 fof(f1409,plain,(
% 0.15/5.69 rselect_tail(q46)=index_246),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1406,f375])).
% 0.15/5.69 fof(f1411,plain,(
% 0.15/5.69 index_249=index_246),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f543,f1409])).
% 0.15/5.69 fof(f1412,plain,(
% 0.15/5.69 q12=rstore_tail(queue_23,index_24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f693,f646])).
% 0.15/5.69 fof(f1413,plain,(
% 0.15/5.69 rselect_head(q12)=rselect_head(queue_23)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1412,f378])).
% 0.15/5.69 fof(f1415,plain,(
% 0.15/5.69 rselect_tail(q12)=index_24),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1412,f375])).
% 0.15/5.69 fof(f1417,plain,(
% 0.15/5.69 index_27=index_24),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f550,f1415])).
% 0.15/5.69 fof(f1420,plain,(
% 0.15/5.69 index_249=s(index_243)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1411,f542])).
% 0.15/5.69 fof(f1422,plain,(
% 0.15/5.69 rselect_head(queue_251)=rselect_head(q46)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f647,f379])).
% 0.15/5.69 fof(f1427,plain,(
% 0.15/5.69 index_27=s(index_21)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1417,f539])).
% 0.15/5.69 fof(f1428,plain,(
% 0.15/5.69 q47=rstore_tail(queue_251,index_252)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f731,f648])).
% 0.15/5.69 fof(f1429,plain,(
% 0.15/5.69 rselect_head(q47)=rselect_head(queue_251)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1428,f378])).
% 0.15/5.69 fof(f1431,plain,(
% 0.15/5.69 rselect_tail(q47)=index_252),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1428,f375])).
% 0.15/5.69 fof(f1433,plain,(
% 0.15/5.69 index_255=index_252),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f545,f1431])).
% 0.15/5.69 fof(f1435,plain,(
% 0.15/5.69 rselect_head(queue_257)=rselect_head(q47)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f649,f379])).
% 0.15/5.69 fof(f1440,plain,(
% 0.15/5.69 index_255=s(index_249)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1433,f544])).
% 0.15/5.69 fof(f1441,plain,(
% 0.15/5.69 q48=rstore_tail(queue_257,index_258)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f732,f650])).
% 0.15/5.69 fof(f1442,plain,(
% 0.15/5.69 rselect_head(q48)=rselect_head(queue_257)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1441,f378])).
% 0.15/5.69 fof(f1444,plain,(
% 0.15/5.69 rselect_tail(q48)=index_258),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1441,f375])).
% 0.15/5.69 fof(f1446,plain,(
% 0.15/5.69 index_261=index_258),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f547,f1444])).
% 0.15/5.69 fof(f1448,plain,(
% 0.15/5.69 rselect_head(queue_263)=rselect_head(q48)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f651,f379])).
% 0.15/5.69 fof(f1449,plain,(
% 0.15/5.69 rselect_seq(queue_263)=earray_262),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f651,f373])).
% 0.15/5.69 fof(f1451,plain,(
% 0.15/5.69 q49=rstore_tail(queue_263,index_264)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f733,f652])).
% 0.15/5.69 fof(f1453,plain,(
% 0.15/5.69 rselect_seq(q49)=rselect_seq(queue_263)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1451,f377])).
% 0.15/5.69 fof(f1454,plain,(
% 0.15/5.69 rselect_tail(q49)=index_264),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1451,f375])).
% 0.15/5.69 fof(f1456,plain,(
% 0.15/5.69 earray_296=rselect_seq(queue_263)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f460,f1453])).
% 0.15/5.69 fof(f1459,plain,(
% 0.15/5.69 index_261=s(index_255)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1446,f546])).
% 0.15/5.69 fof(f1461,plain,(
% 0.15/5.69 rselect_head(queue_269)=rselect_head(q4)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f653,f379])).
% 0.15/5.69 fof(f1468,plain,(
% 0.15/5.69 q5=rstore_tail(queue_269,index_270)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f734,f654])).
% 0.15/5.69 fof(f1469,plain,(
% 0.15/5.69 rselect_head(q5)=rselect_head(queue_269)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1468,f378])).
% 0.15/5.69 fof(f1471,plain,(
% 0.15/5.69 rselect_tail(q5)=index_270),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1468,f375])).
% 0.15/5.69 fof(f1473,plain,(
% 0.15/5.69 index_273=index_270),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f552,f1471])).
% 0.15/5.69 fof(f1475,plain,(
% 0.15/5.69 rselect_head(queue_275)=rselect_head(q5)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f655,f379])).
% 0.15/5.69 fof(f1480,plain,(
% 0.15/5.69 index_273=s(index_267)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1473,f551])).
% 0.15/5.69 fof(f1482,plain,(
% 0.15/5.69 q6=rstore_tail(queue_275,index_276)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f735,f656])).
% 0.15/5.69 fof(f1483,plain,(
% 0.15/5.69 rselect_head(q6)=rselect_head(queue_275)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1482,f378])).
% 0.15/5.69 fof(f1485,plain,(
% 0.15/5.69 rselect_tail(q6)=index_276),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1482,f375])).
% 0.15/5.69 fof(f1487,plain,(
% 0.15/5.69 index_279=index_276),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f554,f1485])).
% 0.15/5.69 fof(f1489,plain,(
% 0.15/5.69 rselect_head(queue_281)=rselect_head(q6)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f657,f379])).
% 0.15/5.69 fof(f1492,plain,(
% 0.15/5.69 q7=rstore_tail(queue_281,index_282)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f736,f658])).
% 0.15/5.69 fof(f1493,plain,(
% 0.15/5.69 rselect_head(q7)=rselect_head(queue_281)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1492,f378])).
% 0.15/5.69 fof(f1495,plain,(
% 0.15/5.69 rselect_tail(q7)=index_282),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1492,f375])).
% 0.15/5.69 fof(f1497,plain,(
% 0.15/5.69 index_285=index_282),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f556,f1495])).
% 0.15/5.69 fof(f1500,plain,(
% 0.15/5.69 index_279=s(index_273)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1487,f553])).
% 0.15/5.69 fof(f1502,plain,(
% 0.15/5.69 rselect_head(queue_287)=rselect_head(q7)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f659,f379])).
% 0.15/5.69 fof(f1508,plain,(
% 0.15/5.69 q8=rstore_tail(queue_287,index_288)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f737,f660])).
% 0.15/5.69 fof(f1509,plain,(
% 0.15/5.69 rselect_head(q8)=rselect_head(queue_287)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1508,f378])).
% 0.15/5.69 fof(f1511,plain,(
% 0.15/5.69 rselect_tail(q8)=index_288),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1508,f375])).
% 0.15/5.69 fof(f1513,plain,(
% 0.15/5.69 index_291=index_288),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f558,f1511])).
% 0.15/5.69 fof(f1515,plain,(
% 0.15/5.69 rselect_head(queue_29)=rselect_head(q12)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f661,f379])).
% 0.15/5.69 fof(f1522,plain,(
% 0.15/5.69 rselect_head(queue_293)=rselect_head(q8)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f662,f379])).
% 0.15/5.69 fof(f1525,plain,(
% 0.15/5.69 q9=rstore_tail(queue_293,index_294)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f738,f663])).
% 0.15/5.69 fof(f1526,plain,(
% 0.15/5.69 rselect_head(q9)=rselect_head(queue_293)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1525,f378])).
% 0.15/5.69 fof(f1528,plain,(
% 0.15/5.69 rselect_tail(q9)=index_294),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1525,f375])).
% 0.15/5.69 fof(f1530,plain,(
% 0.15/5.69 index_9=index_294),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f585,f1528])).
% 0.15/5.69 fof(f1531,plain,(
% 0.15/5.69 q13=rstore_tail(queue_29,index_30)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f694,f664])).
% 0.15/5.69 fof(f1532,plain,(
% 0.15/5.69 rselect_head(q13)=rselect_head(queue_29)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1531,f378])).
% 0.15/5.69 fof(f1534,plain,(
% 0.15/5.69 rselect_tail(q13)=index_30),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1531,f375])).
% 0.15/5.69 fof(f1536,plain,(
% 0.15/5.69 index_33=index_30),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f565,f1534])).
% 0.15/5.69 fof(f1539,plain,(
% 0.15/5.69 index_9=s(index_291)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1530,f559])).
% 0.15/5.69 fof(f1541,plain,(
% 0.15/5.69 rselect_head(queue_35)=rselect_head(q13)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f665,f379])).
% 0.15/5.69 fof(f1546,plain,(
% 0.15/5.69 index_33=s(index_27)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1536,f563])).
% 0.15/5.69 fof(f1547,plain,(
% 0.15/5.69 q14=rstore_tail(queue_35,index_36)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f695,f666])).
% 0.15/5.69 fof(f1548,plain,(
% 0.15/5.69 rselect_head(q14)=rselect_head(queue_35)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1547,f378])).
% 0.15/5.69 fof(f1550,plain,(
% 0.15/5.69 rselect_tail(q14)=index_36),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1547,f375])).
% 0.15/5.69 fof(f1552,plain,(
% 0.15/5.69 index_39=index_36),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f567,f1550])).
% 0.15/5.69 fof(f1554,plain,(
% 0.15/5.69 rselect_head(queue_41)=rselect_head(q14)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f667,f379])).
% 0.15/5.69 fof(f1559,plain,(
% 0.15/5.69 index_39=s(index_33)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1552,f566])).
% 0.15/5.69 fof(f1560,plain,(
% 0.15/5.69 q15=rstore_tail(queue_41,index_42)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f696,f668])).
% 0.15/5.69 fof(f1561,plain,(
% 0.15/5.69 rselect_head(q15)=rselect_head(queue_41)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1560,f378])).
% 0.15/5.69 fof(f1563,plain,(
% 0.15/5.69 rselect_tail(q15)=index_42),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1560,f375])).
% 0.15/5.69 fof(f1565,plain,(
% 0.15/5.69 index_45=index_42),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f569,f1563])).
% 0.15/5.69 fof(f1567,plain,(
% 0.15/5.69 rselect_head(queue_47)=rselect_head(q15)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f669,f379])).
% 0.15/5.69 fof(f1570,plain,(
% 0.15/5.69 q16=rstore_tail(queue_47,index_48)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f697,f670])).
% 0.15/5.69 fof(f1571,plain,(
% 0.15/5.69 rselect_head(q16)=rselect_head(queue_47)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1570,f378])).
% 0.15/5.69 fof(f1573,plain,(
% 0.15/5.69 rselect_tail(q16)=index_48),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1570,f375])).
% 0.15/5.69 fof(f1575,plain,(
% 0.15/5.69 index_51=index_48),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f571,f1573])).
% 0.15/5.69 fof(f1578,plain,(
% 0.15/5.69 index_45=s(index_39)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1565,f568])).
% 0.15/5.69 fof(f1580,plain,(
% 0.15/5.69 rselect_head(queue_5)=rselect_head(q0)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f671,f379])).
% 0.15/5.69 fof(f1585,plain,(
% 0.15/5.69 index_51=s(index_45)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1575,f570])).
% 0.15/5.69 fof(f1587,plain,(
% 0.15/5.69 rselect_head(queue_53)=rselect_head(q16)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f672,f379])).
% 0.15/5.69 fof(f1590,plain,(
% 0.15/5.69 q17=rstore_tail(queue_53,index_54)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f698,f673])).
% 0.15/5.69 fof(f1591,plain,(
% 0.15/5.69 rselect_head(q17)=rselect_head(queue_53)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1590,f378])).
% 0.15/5.69 fof(f1593,plain,(
% 0.15/5.69 rselect_tail(q17)=index_54),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1590,f375])).
% 0.15/5.69 fof(f1595,plain,(
% 0.15/5.69 index_57=index_54),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f573,f1593])).
% 0.15/5.69 fof(f1598,plain,(
% 0.15/5.69 index_57=s(index_51)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1595,f572])).
% 0.15/5.69 fof(f1600,plain,(
% 0.15/5.69 rselect_head(queue_59)=rselect_head(q17)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f674,f379])).
% 0.15/5.69 fof(f1603,plain,(
% 0.15/5.69 q18=rstore_tail(queue_59,index_60)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f699,f675])).
% 0.15/5.69 fof(f1604,plain,(
% 0.15/5.69 rselect_head(q18)=rselect_head(queue_59)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1603,f378])).
% 0.15/5.69 fof(f1606,plain,(
% 0.15/5.69 rselect_tail(q18)=index_60),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1603,f375])).
% 0.15/5.69 fof(f1608,plain,(
% 0.15/5.69 index_63=index_60),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f576,f1606])).
% 0.15/5.69 fof(f1610,plain,(
% 0.15/5.69 rselect_head(queue_65)=rselect_head(q18)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f676,f379])).
% 0.15/5.69 fof(f1615,plain,(
% 0.15/5.69 index_63=s(index_57)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1608,f575])).
% 0.15/5.69 fof(f1616,plain,(
% 0.15/5.69 q19=rstore_tail(queue_65,index_66)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f700,f677])).
% 0.15/5.69 fof(f1617,plain,(
% 0.15/5.69 rselect_head(q19)=rselect_head(queue_65)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1616,f378])).
% 0.15/5.69 fof(f1619,plain,(
% 0.15/5.69 rselect_tail(q19)=index_66),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1616,f375])).
% 0.15/5.69 fof(f1621,plain,(
% 0.15/5.69 index_75=index_66),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f580,f1619])).
% 0.15/5.69 fof(f1624,plain,(
% 0.15/5.69 index_75=s(index_63)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1621,f577])).
% 0.15/5.69 fof(f1625,plain,(
% 0.15/5.69 q1=rstore_tail(queue_5,index_6)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f690,f678])).
% 0.15/5.69 fof(f1626,plain,(
% 0.15/5.69 rselect_head(q1)=rselect_head(queue_5)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1625,f378])).
% 0.15/5.69 fof(f1628,plain,(
% 0.15/5.69 rselect_tail(q1)=index_6),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1625,f375])).
% 0.15/5.69 fof(f1630,plain,(
% 0.15/5.69 index_69=index_6),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f578,f1628])).
% 0.15/5.69 fof(f1632,plain,(
% 0.15/5.69 rselect_head(queue_71)=rselect_head(q1)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f679,f379])).
% 0.15/5.69 fof(f1637,plain,(
% 0.15/5.69 index_69=s(index_3)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1630,f574])).
% 0.15/5.69 fof(f1638,plain,(
% 0.15/5.69 q2=rstore_tail(queue_71,index_72)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f701,f680])).
% 0.15/5.69 fof(f1639,plain,(
% 0.15/5.69 rselect_head(q2)=rselect_head(queue_71)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1638,f378])).
% 0.15/5.69 fof(f1641,plain,(
% 0.15/5.69 rselect_tail(q2)=index_72),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1638,f375])).
% 0.15/5.69 fof(f1643,plain,(
% 0.15/5.69 index_135=index_72),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f501,f1641])).
% 0.15/5.69 fof(f1645,plain,(
% 0.15/5.69 rselect_head(queue_77)=rselect_head(q19)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f681,f379])).
% 0.15/5.69 fof(f1648,plain,(
% 0.15/5.69 q20=rstore_tail(queue_77,index_78)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f702,f682])).
% 0.15/5.69 fof(f1649,plain,(
% 0.15/5.69 rselect_head(q20)=rselect_head(queue_77)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1648,f378])).
% 0.15/5.69 fof(f1651,plain,(
% 0.15/5.69 rselect_tail(q20)=index_78),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1648,f375])).
% 0.15/5.69 fof(f1653,plain,(
% 0.15/5.69 index_81=index_78),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f582,f1651])).
% 0.15/5.69 fof(f1656,plain,(
% 0.15/5.69 index_135=s(index_69)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1643,f579])).
% 0.15/5.69 fof(f1658,plain,(
% 0.15/5.69 rselect_head(queue_83)=rselect_head(q20)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f683,f379])).
% 0.15/5.69 fof(f1663,plain,(
% 0.15/5.69 index_81=s(index_75)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1653,f581])).
% 0.15/5.69 fof(f1664,plain,(
% 0.15/5.69 q21=rstore_tail(queue_83,index_84)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f703,f684])).
% 0.15/5.69 fof(f1665,plain,(
% 0.15/5.69 rselect_head(q21)=rselect_head(queue_83)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1664,f378])).
% 0.15/5.69 fof(f1667,plain,(
% 0.15/5.69 rselect_tail(q21)=index_84),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1664,f375])).
% 0.15/5.69 fof(f1669,plain,(
% 0.15/5.69 index_87=index_84),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f584,f1667])).
% 0.15/5.69 fof(f1671,plain,(
% 0.15/5.69 rselect_head(queue_89)=rselect_head(q21)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f685,f379])).
% 0.15/5.69 fof(f1676,plain,(
% 0.15/5.69 index_87=s(index_81)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1669,f583])).
% 0.15/5.69 fof(f1677,plain,(
% 0.15/5.69 q22=rstore_tail(queue_89,index_90)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f704,f686])).
% 0.15/5.69 fof(f1678,plain,(
% 0.15/5.69 rselect_head(q22)=rselect_head(queue_89)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1677,f378])).
% 0.15/5.69 fof(f1680,plain,(
% 0.15/5.69 rselect_tail(q22)=index_90),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1677,f375])).
% 0.15/5.69 fof(f1682,plain,(
% 0.15/5.69 index_93=index_90),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f587,f1680])).
% 0.15/5.69 fof(f1684,plain,(
% 0.15/5.69 rselect_head(queue_95)=rselect_head(q22)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f687,f379])).
% 0.15/5.69 fof(f1687,plain,(
% 0.15/5.69 q23=rstore_tail(queue_95,index_96)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f705,f688])).
% 0.15/5.69 fof(f1688,plain,(
% 0.15/5.69 rselect_head(q23)=rselect_head(queue_95)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1687,f378])).
% 0.15/5.69 fof(f1690,plain,(
% 0.15/5.69 rselect_tail(q23)=index_96),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1687,f375])).
% 0.15/5.69 fof(f1692,plain,(
% 0.15/5.69 index_99=index_96),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f589,f1690])).
% 0.15/5.69 fof(f1695,plain,(
% 0.15/5.69 index_93=s(index_87)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1682,f586])).
% 0.15/5.69 fof(f1702,plain,(
% 0.15/5.69 index_99=s(index_93)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1692,f588])).
% 0.15/5.69 fof(f1748,plain,(
% 0.15/5.69 p(index_15)=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1134,f866])).
% 0.15/5.69 fof(f1917,plain,(
% 0.15/5.69 p(index_21)=index_15),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1277,f910])).
% 0.15/5.69 fof(f2000,plain,(
% 0.15/5.69 p(index_267)=index_201),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1316,f930])).
% 0.15/5.69 fof(f2172,plain,(
% 0.15/5.69 s(s(index_9))=index_291),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1539,f386])).
% 0.15/5.69 fof(f2176,plain,(
% 0.15/5.69 s(index_15)=index_291),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1147,f2172])).
% 0.15/5.69 fof(f2177,plain,(
% 0.15/5.69 index_21=index_291),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1284,f2176])).
% 0.15/5.69 fof(f2188,plain,(
% 0.15/5.69 index_9=s(index_21)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2177,f1539])).
% 0.15/5.69 fof(f2193,plain,(
% 0.15/5.69 index_21=index_288),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2177,f1513])).
% 0.15/5.69 fof(f2230,plain,(
% 0.15/5.69 p(index_273)=index_267),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1473,f978])).
% 0.15/5.69 fof(f2251,plain,(
% 0.15/5.69 p(index_285)=index_279),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1497,f986])).
% 0.15/5.69 fof(f2273,plain,(
% 0.15/5.69 p(index_21)=index_285),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2193,f990])).
% 0.15/5.69 fof(f2275,plain,(
% 0.15/5.69 p(index_15)=index_279),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2285,f2251])).
% 0.15/5.69 fof(f2285,plain,(
% 0.15/5.69 index_15=index_285),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1917,f2273])).
% 0.15/5.69 fof(f2286,plain,(
% 0.15/5.69 index_9=index_279),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1748,f2275])).
% 0.15/5.69 fof(f2290,plain,(
% 0.15/5.69 index_9=s(index_273)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2286,f1500])).
% 0.15/5.69 fof(f2306,plain,(
% 0.15/5.69 s(s(index_135))=index_69),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1656,f386])).
% 0.15/5.69 fof(f2310,plain,(
% 0.15/5.69 s(index_201)=index_69),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1167,f2306])).
% 0.15/5.69 fof(f2311,plain,(
% 0.15/5.69 index_267=index_69),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1323,f2310])).
% 0.15/5.69 fof(f2333,plain,(
% 0.15/5.69 index_135=s(index_267)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2311,f1656])).
% 0.15/5.69 fof(f2334,plain,(
% 0.15/5.69 index_267=s(index_3)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2311,f1637])).
% 0.15/5.69 fof(f2350,plain,(
% 0.15/5.69 s(s(index_99))=index_93),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f1702,f386])).
% 0.15/5.69 fof(f2354,plain,(
% 0.15/5.69 s(index_105)=index_93),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1070,f2350])).
% 0.15/5.69 fof(f2355,plain,(
% 0.15/5.69 index_111=index_93),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1088,f2354])).
% 0.15/5.69 fof(f2357,plain,(
% 0.15/5.69 index_27=index_9),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2188,f1427])).
% 0.15/5.69 fof(f2364,plain,(
% 0.15/5.69 index_99=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2355,f1702])).
% 0.15/5.69 fof(f2365,plain,(
% 0.15/5.69 index_111=s(index_87)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2355,f1695])).
% 0.15/5.69 fof(f2378,plain,(
% 0.15/5.69 index_33=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2357,f1546])).
% 0.15/5.69 fof(f2387,plain,(
% 0.15/5.69 index_33=index_15),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1147,f2378])).
% 0.15/5.69 fof(f2395,plain,(
% 0.15/5.69 index_39=s(index_15)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2387,f1559])).
% 0.15/5.69 fof(f2399,plain,(
% 0.15/5.69 index_15=index_30),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2387,f1536])).
% 0.15/5.69 fof(f2402,plain,(
% 0.15/5.69 index_39=index_21),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1284,f2395])).
% 0.15/5.69 fof(f2406,plain,(
% 0.15/5.69 index_45=s(index_21)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2402,f1578])).
% 0.15/5.69 fof(f2412,plain,(
% 0.15/5.69 index_45=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2188,f2406])).
% 0.15/5.69 fof(f2414,plain,(
% 0.15/5.69 s(s(index_9))=index_273),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f2290,f386])).
% 0.15/5.69 fof(f2418,plain,(
% 0.15/5.69 s(index_15)=index_273),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1147,f2414])).
% 0.15/5.69 fof(f2419,plain,(
% 0.15/5.69 index_21=index_273),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1284,f2418])).
% 0.15/5.69 fof(f2427,plain,(
% 0.15/5.69 index_51=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2412,f1585])).
% 0.15/5.69 fof(f2433,plain,(
% 0.15/5.69 index_51=index_15),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1147,f2427])).
% 0.15/5.69 fof(f2435,plain,(
% 0.15/5.69 index_273=index_135),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2333,f1480])).
% 0.15/5.69 fof(f2442,plain,(
% 0.15/5.69 s(s(index_267))=index_3),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f2334,f386])).
% 0.15/5.69 fof(f2446,plain,(
% 0.15/5.69 s(index_135)=index_3),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2333,f2442])).
% 0.15/5.69 fof(f2447,plain,(
% 0.15/5.69 index_201=index_3),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1167,f2446])).
% 0.15/5.69 fof(f2453,plain,(
% 0.15/5.69 p(index_21)=index_267),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2419,f2230])).
% 0.15/5.69 fof(f2460,plain,(
% 0.15/5.69 index_15=index_267),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1917,f2453])).
% 0.15/5.69 fof(f2461,plain,(
% 0.15/5.69 index_57=s(index_15)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2433,f1598])).
% 0.15/5.69 fof(f2467,plain,(
% 0.15/5.69 index_57=index_21),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1284,f2461])).
% 0.15/5.69 fof(f2475,plain,(
% 0.15/5.69 index_117=index_99),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2364,f1106])).
% 0.15/5.69 fof(f2482,plain,(
% 0.15/5.69 index_21=index_135),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2435,f2419])).
% 0.15/5.69 fof(f2483,plain,(
% 0.15/5.69 s(s(index_111))=index_87),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f2365,f386])).
% 0.15/5.69 fof(f2487,plain,(
% 0.15/5.69 s(index_99)=index_87),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2364,f2483])).
% 0.15/5.69 fof(f2488,plain,(
% 0.15/5.69 index_105=index_87),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1070,f2487])).
% 0.15/5.69 fof(f2509,plain,(
% 0.15/5.69 index_135=s(index_15)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2460,f2333])).
% 0.15/5.69 fof(f2513,plain,(
% 0.15/5.69 p(index_15)=index_201),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2460,f2000])).
% 0.15/5.69 fof(f2521,plain,(
% 0.15/5.69 index_9=index_201),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1748,f2513])).
% 0.15/5.69 fof(f2529,plain,(
% 0.15/5.69 index_63=s(index_21)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2467,f1615])).
% 0.15/5.69 fof(f2535,plain,(
% 0.15/5.69 index_63=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2188,f2529])).
% 0.15/5.69 fof(f2545,plain,(
% 0.15/5.69 index_123=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2475,f1115])).
% 0.15/5.69 fof(f2554,plain,(
% 0.15/5.69 index_123=index_105),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1070,f2545])).
% 0.15/5.69 fof(f2565,plain,(
% 0.15/5.69 index_9=s(index_135)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2482,f2188])).
% 0.15/5.69 fof(f2585,plain,(
% 0.15/5.69 index_105=s(index_81)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2488,f1676])).
% 0.15/5.69 fof(f2600,plain,(
% 0.15/5.69 index_9=index_3),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2521,f2447])).
% 0.15/5.69 fof(f2619,plain,(
% 0.15/5.69 index_75=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2535,f1624])).
% 0.15/5.69 fof(f2625,plain,(
% 0.15/5.69 index_75=index_15),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1147,f2619])).
% 0.15/5.69 fof(f2636,plain,(
% 0.15/5.69 index_129=s(index_105)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2554,f1128])).
% 0.15/5.69 fof(f2643,plain,(
% 0.15/5.69 index_129=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1088,f2636])).
% 0.15/5.69 fof(f2691,plain,(
% 0.15/5.69 index_81=s(index_15)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2625,f1663])).
% 0.15/5.69 fof(f2697,plain,(
% 0.15/5.69 index_81=index_135),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2509,f2691])).
% 0.15/5.69 fof(f2708,plain,(
% 0.15/5.69 index_141=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2643,f1154])).
% 0.15/5.69 fof(f2714,plain,(
% 0.15/5.69 index_141=index_99),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2364,f2708])).
% 0.15/5.69 fof(f2728,plain,(
% 0.15/5.69 index_105=s(index_135)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2697,f2585])).
% 0.15/5.69 fof(f2734,plain,(
% 0.15/5.69 index_105=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2565,f2728])).
% 0.15/5.69 fof(f2745,plain,(
% 0.15/5.69 index_147=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2714,f1186])).
% 0.15/5.69 fof(f2751,plain,(
% 0.15/5.69 index_147=index_105),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1070,f2745])).
% 0.15/5.69 fof(f2775,plain,(
% 0.15/5.69 index_111=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2734,f1088])).
% 0.15/5.69 fof(f2777,plain,(
% 0.15/5.69 index_9=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2734,f1070])).
% 0.15/5.69 fof(f2799,plain,(
% 0.15/5.69 index_153=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2805,f1193])).
% 0.15/5.69 fof(f2805,plain,(
% 0.15/5.69 index_147=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2734,f2751])).
% 0.15/5.69 fof(f2872,plain,(
% 0.15/5.69 index_15=index_111),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2775,f1147])).
% 0.15/5.69 fof(f2895,plain,(
% 0.15/5.69 index_159=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2901,f1206])).
% 0.15/5.69 fof(f2901,plain,(
% 0.15/5.69 index_153=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2775,f2799])).
% 0.15/5.69 fof(f2902,plain,(
% 0.15/5.69 index_159=index_99),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2364,f2895])).
% 0.15/5.69 fof(f2943,plain,(
% 0.15/5.69 index_111=index_30),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2872,f2399])).
% 0.15/5.69 fof(f2965,plain,(
% 0.15/5.69 index_165=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2902,f1225])).
% 0.15/5.69 fof(f2971,plain,(
% 0.15/5.69 index_165=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2777,f2965])).
% 0.15/5.69 fof(f3003,plain,(
% 0.15/5.69 index_171=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f2971,f1232])).
% 0.15/5.69 fof(f3009,plain,(
% 0.15/5.69 index_171=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2775,f3003])).
% 0.15/5.69 fof(f3026,plain,(
% 0.15/5.69 index_177=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3009,f1245])).
% 0.15/5.69 fof(f3032,plain,(
% 0.15/5.69 index_177=index_99),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2364,f3026])).
% 0.15/5.69 fof(f3045,plain,(
% 0.15/5.69 index_183=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3032,f1262])).
% 0.15/5.69 fof(f3051,plain,(
% 0.15/5.69 index_183=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2777,f3045])).
% 0.15/5.69 fof(f3060,plain,(
% 0.15/5.69 index_189=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3051,f1271])).
% 0.15/5.69 fof(f3066,plain,(
% 0.15/5.69 index_189=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2775,f3060])).
% 0.15/5.69 fof(f3083,plain,(
% 0.15/5.69 index_195=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3066,f1303])).
% 0.15/5.69 fof(f3089,plain,(
% 0.15/5.69 index_195=index_99),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2364,f3083])).
% 0.15/5.69 fof(f3104,plain,(
% 0.15/5.69 index_207=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3089,f1310])).
% 0.15/5.69 fof(f3110,plain,(
% 0.15/5.69 index_207=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2777,f3104])).
% 0.15/5.69 fof(f3117,plain,(
% 0.15/5.69 index_213=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3110,f1342])).
% 0.15/5.69 fof(f3123,plain,(
% 0.15/5.69 index_213=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2775,f3117])).
% 0.15/5.69 fof(f3140,plain,(
% 0.15/5.69 index_219=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3123,f1349])).
% 0.15/5.69 fof(f3146,plain,(
% 0.15/5.69 index_219=index_99),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2364,f3140])).
% 0.15/5.69 fof(f3161,plain,(
% 0.15/5.69 index_225=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3146,f1362])).
% 0.15/5.69 fof(f3167,plain,(
% 0.15/5.69 index_225=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2777,f3161])).
% 0.15/5.69 fof(f3174,plain,(
% 0.15/5.69 index_231=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3167,f1379])).
% 0.15/5.69 fof(f3180,plain,(
% 0.15/5.69 index_231=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2775,f3174])).
% 0.15/5.69 fof(f3197,plain,(
% 0.15/5.69 index_237=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3180,f1388])).
% 0.15/5.69 fof(f3203,plain,(
% 0.15/5.69 index_237=index_99),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2364,f3197])).
% 0.15/5.69 fof(f3218,plain,(
% 0.15/5.69 index_243=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3203,f1401])).
% 0.15/5.69 fof(f3224,plain,(
% 0.15/5.69 index_243=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2777,f3218])).
% 0.15/5.69 fof(f3231,plain,(
% 0.15/5.69 index_249=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3224,f1420])).
% 0.15/5.69 fof(f3237,plain,(
% 0.15/5.69 index_249=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2775,f3231])).
% 0.15/5.69 fof(f3254,plain,(
% 0.15/5.69 index_255=s(index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3237,f1440])).
% 0.15/5.69 fof(f3260,plain,(
% 0.15/5.69 index_255=index_99),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2364,f3254])).
% 0.15/5.69 fof(f3275,plain,(
% 0.15/5.69 index_261=s(index_99)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3260,f1459])).
% 0.15/5.69 fof(f3281,plain,(
% 0.15/5.69 index_261=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2777,f3275])).
% 0.15/5.69 fof(f3291,plain,(
% 0.15/5.69 index_264=s(index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3281,f548])).
% 0.15/5.69 fof(f3294,plain,(
% 0.15/5.69 index_264=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2775,f3291])).
% 0.15/5.69 fof(f3310,plain,(
% 0.15/5.69 q49=rstore_tail(queue_263,index_111)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3294,f1451])).
% 0.15/5.69 fof(f3333,plain,(
% 0.15/5.69 p(index_111)=index_27),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2943,f998])).
% 0.15/5.69 fof(f3334,plain,(
% 0.15/5.69 p(index_111)=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2357,f3333])).
% 0.15/5.69 fof(f3347,plain,(
% 0.15/5.69 rselect_head(q49)=rselect_head(queue_263)),
% 0.15/5.69 inference(paramodulation,[status(thm)],[f3310,f378])).
% 0.15/5.69 fof(f3350,plain,(
% 0.15/5.69 index_297=rselect_head(queue_263)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f560,f3347])).
% 0.15/5.69 fof(f3507,plain,(
% 0.15/5.69 index_0=index_9),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3508,f488])).
% 0.15/5.69 fof(f3508,plain,(
% 0.15/5.69 index_9=rselect_tail(q)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f2600,f1056])).
% 0.15/5.69 fof(f3524,plain,(
% 0.15/5.69 rselect_head(q0)=index_9),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f3507,f1055])).
% 0.15/5.69 fof(f3866,plain,(
% 0.15/5.69 elem_301=select(earray_262,index_300)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3868,f487])).
% 0.15/5.69 fof(f3867,plain,(
% 0.15/5.69 elem_298=select(earray_262,index_297)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3868,f486])).
% 0.15/5.69 fof(f3868,plain,(
% 0.15/5.69 earray_296=earray_262),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1449,f1456])).
% 0.15/5.69 fof(f3869,plain,(
% 0.15/5.69 index_299=index_111),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3870,f561])).
% 0.15/5.69 fof(f3870,plain,(
% 0.15/5.69 rselect_tail(q49)=index_111),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f3294,f1454])).
% 0.15/5.69 fof(f3871,plain,(
% 0.15/5.69 p(index_111)=index_300),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3869,f1002])).
% 0.15/5.69 fof(f3875,plain,(
% 0.15/5.69 index_9=index_300),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f3334,f3871])).
% 0.15/5.69 fof(f3877,plain,(
% 0.15/5.69 elem_301=select(earray_262,index_9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3875,f3866])).
% 0.15/5.69 fof(f3932,definition,(
% 0.15/5.69 sQ31_spl <=> (index_9=index_297)),
% 0.15/5.69 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.15/5.69 fof(f3933,plain,(
% 0.15/5.69 index_9=index_297|~sQ31_spl),
% 0.15/5.69 inference(component_clause,[status(thm)],[f3932])).
% 0.15/5.69 fof(f3934,plain,(
% 0.15/5.69 ~index_9=index_297|sQ31_spl),
% 0.15/5.69 inference(component_clause,[status(thm)],[f3932])).
% 0.15/5.69 fof(f3941,plain,(
% 0.15/5.69 elem_298=select(earray_262,index_9)|~sQ31_spl),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3933,f3867])).
% 0.15/5.69 fof(f3944,plain,(
% 0.15/5.69 elem_301=elem_298|~sQ31_spl),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f3941,f3877])).
% 0.15/5.69 fof(f3947,plain,(
% 0.15/5.69 $false|~sQ31_spl),
% 0.15/5.69 inference(forward_subsumption_resolution,[status(thm)],[f3944,f739])).
% 0.15/5.69 fof(f3948,plain,(
% 0.15/5.69 ~sQ31_spl),
% 0.15/5.69 inference(contradiction_clause,[status(thm)],[f3947])).
% 0.15/5.69 fof(f4771,plain,(
% 0.15/5.69 rselect_head(q24)=rselect_head(q23)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1063,f1059])).
% 0.15/5.69 fof(f4778,plain,(
% 0.15/5.69 rselect_head(q25)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1072,f1077])).
% 0.15/5.69 fof(f4781,plain,(
% 0.15/5.69 rselect_head(queue_113)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4778,f1091])).
% 0.15/5.69 fof(f4786,plain,(
% 0.15/5.69 rselect_head(q26)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4781,f1095])).
% 0.15/5.69 fof(f4787,plain,(
% 0.15/5.69 rselect_head(queue_119)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4786,f1101])).
% 0.15/5.69 fof(f4794,plain,(
% 0.15/5.69 rselect_head(q27)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4787,f1108])).
% 0.15/5.69 fof(f4795,plain,(
% 0.15/5.69 rselect_head(queue_125)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4794,f1117])).
% 0.15/5.69 fof(f4796,plain,(
% 0.15/5.69 rselect_head(q28)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4795,f1121])).
% 0.15/5.69 fof(f4799,plain,(
% 0.15/5.69 rselect_head(q10)=rselect_head(q9)),
% 0.15/5.69 inference(backward_demodulation,[status(thm)],[f1130,f1083])).
% 0.15/5.69 fof(f4804,plain,(
% 0.15/5.69 rselect_head(queue_131)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4796,f1136])).
% 0.15/5.69 fof(f4805,plain,(
% 0.15/5.69 rselect_head(q29)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4804,f1140])).
% 0.15/5.69 fof(f4811,plain,(
% 0.15/5.69 rselect_head(q3)=rselect_head(q2)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f1149,f1156])).
% 0.15/5.69 fof(f4812,plain,(
% 0.15/5.69 rselect_head(queue_143)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4805,f1162])).
% 0.15/5.69 fof(f4815,plain,(
% 0.15/5.69 rselect_head(q30)=rselect_head(q24)),
% 0.15/5.69 inference(forward_demodulation,[status(thm)],[f4812,f1169])).
% 0.15/5.70 fof(f4820,plain,(
% 0.15/5.70 rselect_head(queue_149)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4815,f1175])).
% 0.15/5.70 fof(f4821,plain,(
% 0.15/5.70 rselect_head(q31)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4820,f1179])).
% 0.15/5.70 fof(f4828,plain,(
% 0.15/5.70 rselect_head(queue_155)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4821,f1188])).
% 0.15/5.70 fof(f4829,plain,(
% 0.15/5.70 rselect_head(q32)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4828,f1195])).
% 0.15/5.70 fof(f4830,plain,(
% 0.15/5.70 rselect_head(queue_161)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4829,f1201])).
% 0.15/5.70 fof(f4833,plain,(
% 0.15/5.70 rselect_head(q33)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4830,f1208])).
% 0.15/5.70 fof(f4838,plain,(
% 0.15/5.70 rselect_head(queue_167)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4833,f1214])).
% 0.15/5.70 fof(f4839,plain,(
% 0.15/5.70 rselect_head(q34)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4838,f1218])).
% 0.15/5.70 fof(f4846,plain,(
% 0.15/5.70 rselect_head(queue_173)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4839,f1234])).
% 0.15/5.70 fof(f4847,plain,(
% 0.15/5.70 rselect_head(q35)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4846,f1238])).
% 0.15/5.70 fof(f4850,plain,(
% 0.15/5.70 rselect_head(queue_179)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4847,f1247])).
% 0.15/5.70 fof(f4852,plain,(
% 0.15/5.70 rselect_head(q36)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4850,f1251])).
% 0.15/5.70 fof(f4853,plain,(
% 0.15/5.70 rselect_head(queue_185)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4852,f1257])).
% 0.15/5.70 fof(f4860,plain,(
% 0.15/5.70 rselect_head(q37)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4853,f1264])).
% 0.15/5.70 fof(f4861,plain,(
% 0.15/5.70 rselect_head(q11)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f1227,f1273])).
% 0.15/5.70 fof(f4862,plain,(
% 0.15/5.70 rselect_head(queue_191)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4860,f1279])).
% 0.15/5.70 fof(f4864,plain,(
% 0.15/5.70 rselect_head(q38)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4862,f1286])).
% 0.15/5.70 fof(f4870,plain,(
% 0.15/5.70 rselect_head(queue_197)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4864,f1292])).
% 0.15/5.70 fof(f4871,plain,(
% 0.15/5.70 rselect_head(q39)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4870,f1296])).
% 0.15/5.70 fof(f4878,plain,(
% 0.15/5.70 rselect_head(queue_203)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4811,f1305])).
% 0.15/5.70 fof(f4879,plain,(
% 0.15/5.70 rselect_head(q4)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4878,f1312])).
% 0.15/5.70 fof(f4880,plain,(
% 0.15/5.70 rselect_head(queue_209)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4871,f1318])).
% 0.15/5.70 fof(f4882,plain,(
% 0.15/5.70 rselect_head(q40)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4880,f1325])).
% 0.15/5.70 fof(f4888,plain,(
% 0.15/5.70 rselect_head(queue_215)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4882,f1331])).
% 0.15/5.70 fof(f4889,plain,(
% 0.15/5.70 rselect_head(q41)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4888,f1335])).
% 0.15/5.70 fof(f4896,plain,(
% 0.15/5.70 rselect_head(queue_221)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4889,f1344])).
% 0.15/5.70 fof(f4897,plain,(
% 0.15/5.70 rselect_head(q42)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4896,f1351])).
% 0.15/5.70 fof(f4898,plain,(
% 0.15/5.70 rselect_head(queue_227)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4897,f1357])).
% 0.15/5.70 fof(f4900,plain,(
% 0.15/5.70 rselect_head(q43)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4898,f1364])).
% 0.15/5.70 fof(f4906,plain,(
% 0.15/5.70 rselect_head(queue_23)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4861,f1370])).
% 0.15/5.70 fof(f4907,plain,(
% 0.15/5.70 rselect_head(queue_233)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4900,f1374])).
% 0.15/5.70 fof(f4914,plain,(
% 0.15/5.70 rselect_head(q44)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4907,f1381])).
% 0.15/5.70 fof(f4915,plain,(
% 0.15/5.70 rselect_head(queue_239)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4914,f1390])).
% 0.15/5.70 fof(f4916,plain,(
% 0.15/5.70 rselect_head(q45)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4915,f1394])).
% 0.15/5.70 fof(f4918,plain,(
% 0.15/5.70 rselect_head(queue_245)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4916,f1403])).
% 0.15/5.70 fof(f4923,plain,(
% 0.15/5.70 rselect_head(q46)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4918,f1407])).
% 0.15/5.70 fof(f4924,plain,(
% 0.15/5.70 rselect_head(q12)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4906,f1413])).
% 0.15/5.70 fof(f4929,plain,(
% 0.15/5.70 rselect_head(queue_251)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4923,f1422])).
% 0.15/5.70 fof(f4930,plain,(
% 0.15/5.70 rselect_head(q47)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4929,f1429])).
% 0.15/5.70 fof(f4931,plain,(
% 0.15/5.70 rselect_head(queue_257)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4930,f1435])).
% 0.15/5.70 fof(f4933,plain,(
% 0.15/5.70 rselect_head(q48)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4931,f1442])).
% 0.15/5.70 fof(f4939,plain,(
% 0.15/5.70 rselect_head(queue_263)=rselect_head(q24)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4933,f1448])).
% 0.15/5.70 fof(f4940,plain,(
% 0.15/5.70 rselect_head(queue_269)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4879,f1461])).
% 0.15/5.70 fof(f4947,plain,(
% 0.15/5.70 rselect_head(q5)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4940,f1469])).
% 0.15/5.70 fof(f4948,plain,(
% 0.15/5.70 rselect_head(queue_275)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4947,f1475])).
% 0.15/5.70 fof(f4949,plain,(
% 0.15/5.70 rselect_head(q6)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4948,f1483])).
% 0.15/5.70 fof(f4951,plain,(
% 0.15/5.70 rselect_head(queue_281)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4949,f1489])).
% 0.15/5.70 fof(f4957,plain,(
% 0.15/5.70 rselect_head(q7)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4951,f1493])).
% 0.15/5.70 fof(f4958,plain,(
% 0.15/5.70 rselect_head(queue_287)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4957,f1502])).
% 0.15/5.70 fof(f4961,plain,(
% 0.15/5.70 rselect_head(q8)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4958,f1509])).
% 0.15/5.70 fof(f4962,plain,(
% 0.15/5.70 rselect_head(queue_29)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4924,f1515])).
% 0.15/5.70 fof(f4963,plain,(
% 0.15/5.70 rselect_head(queue_293)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4961,f1522])).
% 0.15/5.70 fof(f4965,plain,(
% 0.15/5.70 rselect_head(q9)=rselect_head(q2)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4963,f1526])).
% 0.15/5.70 fof(f4968,plain,(
% 0.15/5.70 rselect_head(q13)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4962,f1532])).
% 0.15/5.70 fof(f4969,plain,(
% 0.15/5.70 rselect_head(queue_35)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4968,f1541])).
% 0.15/5.70 fof(f4973,plain,(
% 0.15/5.70 rselect_head(q14)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4969,f1548])).
% 0.15/5.70 fof(f4974,plain,(
% 0.15/5.70 rselect_head(queue_41)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4973,f1554])).
% 0.15/5.70 fof(f4975,plain,(
% 0.15/5.70 rselect_head(q15)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4974,f1561])).
% 0.15/5.70 fof(f4977,plain,(
% 0.15/5.70 rselect_head(queue_47)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4975,f1567])).
% 0.15/5.70 fof(f4980,plain,(
% 0.15/5.70 rselect_head(q16)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4977,f1571])).
% 0.15/5.70 fof(f4981,plain,(
% 0.15/5.70 rselect_head(queue_5)=index_9),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f3524,f1580])).
% 0.15/5.70 fof(f4984,plain,(
% 0.15/5.70 rselect_head(queue_53)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4980,f1587])).
% 0.15/5.70 fof(f4985,plain,(
% 0.15/5.70 rselect_head(q17)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4984,f1591])).
% 0.15/5.70 fof(f4986,plain,(
% 0.15/5.70 rselect_head(queue_59)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4985,f1600])).
% 0.15/5.70 fof(f4988,plain,(
% 0.15/5.70 rselect_head(q18)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4986,f1604])).
% 0.15/5.70 fof(f4990,plain,(
% 0.15/5.70 rselect_head(queue_65)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4988,f1610])).
% 0.15/5.70 fof(f4991,plain,(
% 0.15/5.70 rselect_head(q19)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4990,f1617])).
% 0.15/5.70 fof(f4994,plain,(
% 0.15/5.70 rselect_head(q1)=index_9),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4981,f1626])).
% 0.15/5.70 fof(f4995,plain,(
% 0.15/5.70 rselect_head(queue_71)=index_9),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4994,f1632])).
% 0.15/5.70 fof(f4996,plain,(
% 0.15/5.70 rselect_head(q9)=index_9),
% 0.15/5.70 inference(backward_demodulation,[status(thm)],[f5010,f4965])).
% 0.15/5.70 fof(f5010,plain,(
% 0.15/5.70 rselect_head(q2)=index_9),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4995,f1639])).
% 0.15/5.70 fof(f5012,plain,(
% 0.15/5.70 rselect_head(queue_77)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4991,f1645])).
% 0.15/5.70 fof(f5015,plain,(
% 0.15/5.70 rselect_head(q20)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f5012,f1649])).
% 0.15/5.70 fof(f5016,plain,(
% 0.15/5.70 rselect_head(queue_83)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f5015,f1658])).
% 0.15/5.70 fof(f5020,plain,(
% 0.15/5.70 rselect_head(q21)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f5016,f1665])).
% 0.15/5.70 fof(f5021,plain,(
% 0.15/5.70 rselect_head(queue_89)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f5020,f1671])).
% 0.15/5.70 fof(f5022,plain,(
% 0.15/5.70 rselect_head(q22)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f5021,f1678])).
% 0.15/5.70 fof(f5023,plain,(
% 0.15/5.70 rselect_head(queue_95)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f5022,f1684])).
% 0.15/5.70 fof(f5026,plain,(
% 0.15/5.70 rselect_head(q23)=rselect_head(q10)),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f5023,f1688])).
% 0.15/5.70 fof(f5316,plain,(
% 0.15/5.70 index_297=rselect_head(q24)),
% 0.15/5.70 inference(backward_demodulation,[status(thm)],[f3350,f4939])).
% 0.15/5.70 fof(f6129,plain,(
% 0.15/5.70 rselect_head(q10)=index_9),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f4996,f4799])).
% 0.15/5.70 fof(f6133,plain,(
% 0.15/5.70 rselect_head(q23)=index_9),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f6129,f5026])).
% 0.15/5.70 fof(f6450,plain,(
% 0.15/5.70 rselect_head(q24)=index_9),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f6133,f4771])).
% 0.15/5.70 fof(f6451,plain,(
% 0.15/5.70 index_297=index_9),
% 0.15/5.70 inference(forward_demodulation,[status(thm)],[f6450,f5316])).
% 0.15/5.70 fof(f6452,plain,(
% 0.15/5.70 $false|sQ31_spl),
% 0.15/5.70 inference(forward_subsumption_resolution,[status(thm)],[f6451,f3934])).
% 0.15/5.70 fof(f6453,plain,(
% 0.15/5.70 sQ31_spl),
% 0.15/5.70 inference(contradiction_clause,[status(thm)],[f6452])).
% 0.15/5.70 fof(f6454,plain,(
% 0.15/5.70 $false),
% 0.15/5.70 inference(sat_refutation,[status(thm)],[f3948,f6453])).
% 0.15/5.70 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.70 % Elapsed time: 0.314641 seconds
% 0.15/5.70 % CPU time: 2.263783 seconds
% 0.15/5.70 % Total memory used: 148.069 MB
% 0.15/5.70 % Net memory used: 146.927 MB
%------------------------------------------------------------------------------