%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV570-1.043 : 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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:52:50 PM UTC 2026
% Result : Unsatisfiable 0.36s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.40 % Computer : n026.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Mon Sep 21 09:13:39 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.42 % Drodi V4.1.1
% 0.36/0.47 % Refutation found
% 0.36/0.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.36/0.47 % SZS output start CNFRefutation for theBenchmark
% 0.36/0.47 fof(f1,axiom,(
% 0.36/0.47 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f3,axiom,(
% 0.36/0.47 (![A,E]: (rselect_seq(rstore_seq(A,E)) = E ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f4,axiom,(
% 0.36/0.47 (![A,E]: (rselect_head(rstore_head(A,E)) = E ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f5,axiom,(
% 0.36/0.47 (![A,E]: (rselect_tail(rstore_tail(A,E)) = E ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f7,axiom,(
% 0.36/0.47 (![A,E]: (rselect_seq(rstore_tail(A,E)) = rselect_seq(A) ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f8,axiom,(
% 0.36/0.47 (![A,E]: (rselect_head(rstore_tail(A,E)) = rselect_head(A) ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f9,axiom,(
% 0.36/0.47 (![A,E]: (rselect_head(rstore_seq(A,E)) = rselect_head(A) ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f11,axiom,(
% 0.36/0.47 (![A,E]: (rselect_tail(rstore_head(A,E)) = rselect_tail(A) ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f12,axiom,(
% 0.36/0.47 (![X]: (p(s(X)) = X ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f13,axiom,(
% 0.36/0.47 (![X]: (s(p(X)) = X ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f16,axiom,(
% 0.36/0.47 (![X]: (s(s(s(X))) = X ))),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f65,hypothesis,(
% 0.36/0.47 earray_226 = store(earray_224,index_225,e42) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f77,hypothesis,(
% 0.36/0.47 earray_260 = rselect_seq(q43) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f104,hypothesis,(
% 0.36/0.47 elem_262 = select(earray_260,index_261) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f105,hypothesis,(
% 0.36/0.47 elem_265 = select(earray_260,index_264) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f106,hypothesis,(
% 0.36/0.47 index_0 = rselect_tail(q) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f107,hypothesis,(
% 0.36/0.47 index_102 = s(index_99) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f108,hypothesis,(
% 0.36/0.47 index_105 = rselect_tail(q24) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f109,hypothesis,(
% 0.36/0.47 index_108 = s(index_105) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f110,hypothesis,(
% 0.36/0.47 index_111 = rselect_tail(q25) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f111,hypothesis,(
% 0.36/0.47 index_114 = s(index_111) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f112,hypothesis,(
% 0.36/0.47 index_117 = rselect_tail(q26) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f113,hypothesis,(
% 0.36/0.47 index_12 = s(index_9) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f114,hypothesis,(
% 0.36/0.47 index_120 = s(index_117) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f115,hypothesis,(
% 0.36/0.47 index_123 = rselect_tail(q27) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f116,hypothesis,(
% 0.36/0.47 index_126 = s(index_123) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f117,hypothesis,(
% 0.36/0.47 index_129 = rselect_tail(q28) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f118,hypothesis,(
% 0.36/0.47 index_132 = s(index_129) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f119,hypothesis,(
% 0.36/0.47 index_135 = rselect_tail(q2) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f120,hypothesis,(
% 0.36/0.47 index_138 = s(index_135) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f121,hypothesis,(
% 0.36/0.47 index_141 = rselect_tail(q29) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f122,hypothesis,(
% 0.36/0.47 index_144 = s(index_141) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f123,hypothesis,(
% 0.36/0.47 index_147 = rselect_tail(q30) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f124,hypothesis,(
% 0.36/0.47 index_15 = rselect_tail(q10) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f125,hypothesis,(
% 0.36/0.47 index_150 = s(index_147) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f126,hypothesis,(
% 0.36/0.47 index_153 = rselect_tail(q31) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f127,hypothesis,(
% 0.36/0.47 index_156 = s(index_153) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f128,hypothesis,(
% 0.36/0.47 index_159 = rselect_tail(q32) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f129,hypothesis,(
% 0.36/0.47 index_162 = s(index_159) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f130,hypothesis,(
% 0.36/0.47 index_165 = rselect_tail(q33) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f131,hypothesis,(
% 0.36/0.47 index_168 = s(index_165) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f132,hypothesis,(
% 0.36/0.47 index_171 = rselect_tail(q34) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f133,hypothesis,(
% 0.36/0.47 index_174 = s(index_171) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f134,hypothesis,(
% 0.36/0.47 index_177 = rselect_tail(q35) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f135,hypothesis,(
% 0.36/0.47 index_18 = s(index_15) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f136,hypothesis,(
% 0.36/0.47 index_180 = s(index_177) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f137,hypothesis,(
% 0.36/0.47 index_183 = rselect_tail(q36) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f138,hypothesis,(
% 0.36/0.47 index_186 = s(index_183) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f139,hypothesis,(
% 0.36/0.47 index_189 = rselect_tail(q37) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f140,hypothesis,(
% 0.36/0.47 index_192 = s(index_189) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f141,hypothesis,(
% 0.36/0.47 index_195 = rselect_tail(q38) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f142,hypothesis,(
% 0.36/0.47 index_198 = s(index_195) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f143,hypothesis,(
% 0.36/0.47 index_201 = rselect_tail(q3) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f144,hypothesis,(
% 0.36/0.47 index_204 = s(index_201) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f145,hypothesis,(
% 0.36/0.47 index_207 = rselect_tail(q39) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f146,hypothesis,(
% 0.36/0.47 index_21 = rselect_tail(q11) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f147,hypothesis,(
% 0.36/0.47 index_210 = s(index_207) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f148,hypothesis,(
% 0.36/0.47 index_213 = rselect_tail(q40) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f149,hypothesis,(
% 0.36/0.47 index_216 = s(index_213) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f150,hypothesis,(
% 0.36/0.47 index_219 = rselect_tail(q41) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f151,hypothesis,(
% 0.36/0.47 index_222 = s(index_219) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f152,hypothesis,(
% 0.36/0.47 index_225 = rselect_tail(q42) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f153,hypothesis,(
% 0.36/0.47 index_228 = s(index_225) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f154,hypothesis,(
% 0.36/0.47 index_231 = rselect_tail(q4) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f155,hypothesis,(
% 0.36/0.47 index_234 = s(index_231) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f156,hypothesis,(
% 0.36/0.47 index_237 = rselect_tail(q5) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f157,hypothesis,(
% 0.36/0.47 index_24 = s(index_21) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f158,hypothesis,(
% 0.36/0.47 index_240 = s(index_237) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f159,hypothesis,(
% 0.36/0.47 index_243 = rselect_tail(q6) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f160,hypothesis,(
% 0.36/0.47 index_246 = s(index_243) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f161,hypothesis,(
% 0.36/0.47 index_249 = rselect_tail(q7) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f162,hypothesis,(
% 0.36/0.47 index_252 = s(index_249) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f163,hypothesis,(
% 0.36/0.47 index_255 = rselect_tail(q8) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f164,hypothesis,(
% 0.36/0.47 index_258 = s(index_255) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f165,hypothesis,(
% 0.36/0.47 index_261 = rselect_head(q43) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f166,hypothesis,(
% 0.36/0.47 index_263 = rselect_tail(q43) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f167,hypothesis,(
% 0.36/0.47 s(index_264) = index_263 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f168,hypothesis,(
% 0.36/0.47 index_27 = rselect_tail(q12) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f169,hypothesis,(
% 0.36/0.47 index_3 = rselect_tail(q0) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f170,hypothesis,(
% 0.36/0.47 index_30 = s(index_27) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f171,hypothesis,(
% 0.36/0.47 index_33 = rselect_tail(q13) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f172,hypothesis,(
% 0.36/0.47 index_36 = s(index_33) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f173,hypothesis,(
% 0.36/0.47 index_39 = rselect_tail(q14) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f174,hypothesis,(
% 0.36/0.47 index_42 = s(index_39) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f175,hypothesis,(
% 0.36/0.47 index_45 = rselect_tail(q15) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f176,hypothesis,(
% 0.36/0.47 index_48 = s(index_45) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f177,hypothesis,(
% 0.36/0.47 index_51 = rselect_tail(q16) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f178,hypothesis,(
% 0.36/0.47 index_54 = s(index_51) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f179,hypothesis,(
% 0.36/0.47 index_57 = rselect_tail(q17) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f180,hypothesis,(
% 0.36/0.47 index_6 = s(index_3) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f181,hypothesis,(
% 0.36/0.47 index_60 = s(index_57) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f182,hypothesis,(
% 0.36/0.47 index_63 = rselect_tail(q18) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f183,hypothesis,(
% 0.36/0.47 index_66 = s(index_63) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f184,hypothesis,(
% 0.36/0.47 index_69 = rselect_tail(q1) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f185,hypothesis,(
% 0.36/0.47 index_72 = s(index_69) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f186,hypothesis,(
% 0.36/0.47 index_75 = rselect_tail(q19) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f187,hypothesis,(
% 0.36/0.47 index_78 = s(index_75) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f188,hypothesis,(
% 0.36/0.47 index_81 = rselect_tail(q20) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f189,hypothesis,(
% 0.36/0.47 index_84 = s(index_81) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f190,hypothesis,(
% 0.36/0.47 index_87 = rselect_tail(q21) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f191,hypothesis,(
% 0.36/0.47 index_9 = rselect_tail(q9) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f192,hypothesis,(
% 0.36/0.47 index_90 = s(index_87) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f193,hypothesis,(
% 0.36/0.47 index_93 = rselect_tail(q22) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f194,hypothesis,(
% 0.36/0.47 index_96 = s(index_93) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f195,hypothesis,(
% 0.36/0.47 index_99 = rselect_tail(q23) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f196,hypothesis,(
% 0.36/0.47 queue_1 = rstore_head(q,index_0) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f197,hypothesis,(
% 0.36/0.47 queue_101 = rstore_seq(q23,earray_100) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f198,hypothesis,(
% 0.36/0.47 queue_103 = rstore_tail(queue_101,index_102) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f199,hypothesis,(
% 0.36/0.47 queue_107 = rstore_seq(q24,earray_106) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f200,hypothesis,(
% 0.36/0.47 queue_109 = rstore_tail(queue_107,index_108) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f201,hypothesis,(
% 0.36/0.47 queue_11 = rstore_seq(q9,earray_10) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f202,hypothesis,(
% 0.36/0.47 queue_113 = rstore_seq(q25,earray_112) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f203,hypothesis,(
% 0.36/0.47 queue_115 = rstore_tail(queue_113,index_114) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f204,hypothesis,(
% 0.36/0.47 queue_119 = rstore_seq(q26,earray_118) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f205,hypothesis,(
% 0.36/0.47 queue_121 = rstore_tail(queue_119,index_120) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f206,hypothesis,(
% 0.36/0.47 queue_125 = rstore_seq(q27,earray_124) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f207,hypothesis,(
% 0.36/0.47 queue_127 = rstore_tail(queue_125,index_126) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f208,hypothesis,(
% 0.36/0.47 queue_13 = rstore_tail(queue_11,index_12) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f209,hypothesis,(
% 0.36/0.47 queue_131 = rstore_seq(q28,earray_130) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f210,hypothesis,(
% 0.36/0.47 queue_133 = rstore_tail(queue_131,index_132) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f211,hypothesis,(
% 0.36/0.47 queue_137 = rstore_seq(q2,earray_136) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f212,hypothesis,(
% 0.36/0.47 queue_139 = rstore_tail(queue_137,index_138) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f213,hypothesis,(
% 0.36/0.47 queue_143 = rstore_seq(q29,earray_142) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f214,hypothesis,(
% 0.36/0.47 queue_145 = rstore_tail(queue_143,index_144) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f215,hypothesis,(
% 0.36/0.47 queue_149 = rstore_seq(q30,earray_148) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f216,hypothesis,(
% 0.36/0.47 queue_151 = rstore_tail(queue_149,index_150) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f217,hypothesis,(
% 0.36/0.47 queue_155 = rstore_seq(q31,earray_154) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f218,hypothesis,(
% 0.36/0.47 queue_157 = rstore_tail(queue_155,index_156) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f219,hypothesis,(
% 0.36/0.47 queue_161 = rstore_seq(q32,earray_160) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f220,hypothesis,(
% 0.36/0.47 queue_163 = rstore_tail(queue_161,index_162) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f221,hypothesis,(
% 0.36/0.47 queue_167 = rstore_seq(q33,earray_166) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f222,hypothesis,(
% 0.36/0.47 queue_169 = rstore_tail(queue_167,index_168) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f223,hypothesis,(
% 0.36/0.47 queue_17 = rstore_seq(q10,earray_16) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f224,hypothesis,(
% 0.36/0.47 queue_173 = rstore_seq(q34,earray_172) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f225,hypothesis,(
% 0.36/0.47 queue_175 = rstore_tail(queue_173,index_174) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f226,hypothesis,(
% 0.36/0.47 queue_179 = rstore_seq(q35,earray_178) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f227,hypothesis,(
% 0.36/0.47 queue_181 = rstore_tail(queue_179,index_180) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f228,hypothesis,(
% 0.36/0.47 queue_185 = rstore_seq(q36,earray_184) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f229,hypothesis,(
% 0.36/0.47 queue_187 = rstore_tail(queue_185,index_186) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f230,hypothesis,(
% 0.36/0.47 queue_19 = rstore_tail(queue_17,index_18) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f231,hypothesis,(
% 0.36/0.47 queue_191 = rstore_seq(q37,earray_190) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f232,hypothesis,(
% 0.36/0.47 queue_193 = rstore_tail(queue_191,index_192) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f233,hypothesis,(
% 0.36/0.47 queue_197 = rstore_seq(q38,earray_196) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f234,hypothesis,(
% 0.36/0.47 queue_199 = rstore_tail(queue_197,index_198) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f235,hypothesis,(
% 0.36/0.47 queue_203 = rstore_seq(q3,earray_202) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f236,hypothesis,(
% 0.36/0.47 queue_205 = rstore_tail(queue_203,index_204) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f237,hypothesis,(
% 0.36/0.47 queue_209 = rstore_seq(q39,earray_208) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f238,hypothesis,(
% 0.36/0.47 queue_211 = rstore_tail(queue_209,index_210) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f239,hypothesis,(
% 0.36/0.47 queue_215 = rstore_seq(q40,earray_214) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f240,hypothesis,(
% 0.36/0.47 queue_217 = rstore_tail(queue_215,index_216) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f241,hypothesis,(
% 0.36/0.47 queue_221 = rstore_seq(q41,earray_220) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f242,hypothesis,(
% 0.36/0.47 queue_223 = rstore_tail(queue_221,index_222) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f243,hypothesis,(
% 0.36/0.47 queue_227 = rstore_seq(q42,earray_226) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f244,hypothesis,(
% 0.36/0.47 queue_229 = rstore_tail(queue_227,index_228) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f245,hypothesis,(
% 0.36/0.47 queue_23 = rstore_seq(q11,earray_22) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f246,hypothesis,(
% 0.36/0.47 queue_233 = rstore_seq(q4,earray_232) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f247,hypothesis,(
% 0.36/0.47 queue_235 = rstore_tail(queue_233,index_234) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f248,hypothesis,(
% 0.36/0.47 queue_239 = rstore_seq(q5,earray_238) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f249,hypothesis,(
% 0.36/0.47 queue_241 = rstore_tail(queue_239,index_240) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f250,hypothesis,(
% 0.36/0.47 queue_245 = rstore_seq(q6,earray_244) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f251,hypothesis,(
% 0.36/0.47 queue_247 = rstore_tail(queue_245,index_246) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f252,hypothesis,(
% 0.36/0.47 queue_25 = rstore_tail(queue_23,index_24) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f253,hypothesis,(
% 0.36/0.47 queue_251 = rstore_seq(q7,earray_250) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f254,hypothesis,(
% 0.36/0.47 queue_253 = rstore_tail(queue_251,index_252) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f255,hypothesis,(
% 0.36/0.47 queue_257 = rstore_seq(q8,earray_256) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f256,hypothesis,(
% 0.36/0.47 queue_259 = rstore_tail(queue_257,index_258) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f257,hypothesis,(
% 0.36/0.47 queue_29 = rstore_seq(q12,earray_28) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f258,hypothesis,(
% 0.36/0.47 queue_31 = rstore_tail(queue_29,index_30) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f259,hypothesis,(
% 0.36/0.47 queue_35 = rstore_seq(q13,earray_34) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f260,hypothesis,(
% 0.36/0.47 queue_37 = rstore_tail(queue_35,index_36) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f261,hypothesis,(
% 0.36/0.47 queue_41 = rstore_seq(q14,earray_40) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f262,hypothesis,(
% 0.36/0.47 queue_43 = rstore_tail(queue_41,index_42) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f263,hypothesis,(
% 0.36/0.47 queue_47 = rstore_seq(q15,earray_46) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f264,hypothesis,(
% 0.36/0.47 queue_49 = rstore_tail(queue_47,index_48) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f265,hypothesis,(
% 0.36/0.47 queue_5 = rstore_seq(q0,earray_4) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f266,hypothesis,(
% 0.36/0.47 queue_53 = rstore_seq(q16,earray_52) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f267,hypothesis,(
% 0.36/0.47 queue_55 = rstore_tail(queue_53,index_54) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f268,hypothesis,(
% 0.36/0.47 queue_59 = rstore_seq(q17,earray_58) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f269,hypothesis,(
% 0.36/0.47 queue_61 = rstore_tail(queue_59,index_60) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f270,hypothesis,(
% 0.36/0.47 queue_65 = rstore_seq(q18,earray_64) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f271,hypothesis,(
% 0.36/0.47 queue_67 = rstore_tail(queue_65,index_66) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f272,hypothesis,(
% 0.36/0.47 queue_7 = rstore_tail(queue_5,index_6) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f273,hypothesis,(
% 0.36/0.47 queue_71 = rstore_seq(q1,earray_70) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f274,hypothesis,(
% 0.36/0.47 queue_73 = rstore_tail(queue_71,index_72) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f275,hypothesis,(
% 0.36/0.47 queue_77 = rstore_seq(q19,earray_76) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f276,hypothesis,(
% 0.36/0.47 queue_79 = rstore_tail(queue_77,index_78) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f277,hypothesis,(
% 0.36/0.47 queue_83 = rstore_seq(q20,earray_82) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f278,hypothesis,(
% 0.36/0.47 queue_85 = rstore_tail(queue_83,index_84) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f279,hypothesis,(
% 0.36/0.47 queue_89 = rstore_seq(q21,earray_88) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f280,hypothesis,(
% 0.36/0.47 queue_91 = rstore_tail(queue_89,index_90) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f281,hypothesis,(
% 0.36/0.47 queue_95 = rstore_seq(q22,earray_94) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f282,hypothesis,(
% 0.36/0.47 queue_97 = rstore_tail(queue_95,index_96) ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f283,hypothesis,(
% 0.36/0.47 q0 = queue_1 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f284,hypothesis,(
% 0.36/0.47 q1 = queue_7 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f285,hypothesis,(
% 0.36/0.47 q10 = queue_13 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f286,hypothesis,(
% 0.36/0.47 q11 = queue_19 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f287,hypothesis,(
% 0.36/0.47 q12 = queue_25 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f288,hypothesis,(
% 0.36/0.47 q13 = queue_31 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f289,hypothesis,(
% 0.36/0.47 q14 = queue_37 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f290,hypothesis,(
% 0.36/0.47 q15 = queue_43 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f291,hypothesis,(
% 0.36/0.47 q16 = queue_49 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f292,hypothesis,(
% 0.36/0.47 q17 = queue_55 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f293,hypothesis,(
% 0.36/0.47 q18 = queue_61 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f294,hypothesis,(
% 0.36/0.47 q19 = queue_67 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f295,hypothesis,(
% 0.36/0.47 q2 = queue_73 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f296,hypothesis,(
% 0.36/0.47 q20 = queue_79 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f297,hypothesis,(
% 0.36/0.47 q21 = queue_85 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f298,hypothesis,(
% 0.36/0.47 q22 = queue_91 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f299,hypothesis,(
% 0.36/0.47 q23 = queue_97 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f300,hypothesis,(
% 0.36/0.47 q24 = queue_103 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f301,hypothesis,(
% 0.36/0.47 q25 = queue_109 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f302,hypothesis,(
% 0.36/0.47 q26 = queue_115 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f303,hypothesis,(
% 0.36/0.47 q27 = queue_121 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f304,hypothesis,(
% 0.36/0.47 q28 = queue_127 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f305,hypothesis,(
% 0.36/0.47 q29 = queue_133 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f306,hypothesis,(
% 0.36/0.47 q3 = queue_139 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f307,hypothesis,(
% 0.36/0.47 q30 = queue_145 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f308,hypothesis,(
% 0.36/0.47 q31 = queue_151 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f309,hypothesis,(
% 0.36/0.47 q32 = queue_157 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f310,hypothesis,(
% 0.36/0.47 q33 = queue_163 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f311,hypothesis,(
% 0.36/0.47 q34 = queue_169 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f312,hypothesis,(
% 0.36/0.47 q35 = queue_175 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f313,hypothesis,(
% 0.36/0.47 q36 = queue_181 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f314,hypothesis,(
% 0.36/0.47 q37 = queue_187 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f315,hypothesis,(
% 0.36/0.47 q38 = queue_193 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f316,hypothesis,(
% 0.36/0.47 q39 = queue_199 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f317,hypothesis,(
% 0.36/0.47 q4 = queue_205 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f318,hypothesis,(
% 0.36/0.47 q40 = queue_211 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f319,hypothesis,(
% 0.36/0.47 q41 = queue_217 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f320,hypothesis,(
% 0.36/0.47 q42 = queue_223 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f321,hypothesis,(
% 0.36/0.47 q43 = queue_229 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f322,hypothesis,(
% 0.36/0.47 q5 = queue_235 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f323,hypothesis,(
% 0.36/0.47 q6 = queue_241 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f324,hypothesis,(
% 0.36/0.47 q7 = queue_247 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f325,hypothesis,(
% 0.36/0.47 q8 = queue_253 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f326,hypothesis,(
% 0.36/0.47 q9 = queue_259 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f327,negated_conjecture,(
% 0.36/0.47 elem_262 != elem_265 ),
% 0.36/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.36/0.47 fof(f328,plain,(
% 0.36/0.47 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f1])).
% 0.36/0.47 fof(f331,plain,(
% 0.36/0.47 ![X0,X1]: (rselect_seq(rstore_seq(X0,X1))=X1)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f3])).
% 0.36/0.47 fof(f332,plain,(
% 0.36/0.47 ![X0,X1]: (rselect_head(rstore_head(X0,X1))=X1)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f4])).
% 0.36/0.47 fof(f333,plain,(
% 0.36/0.47 ![X0,X1]: (rselect_tail(rstore_tail(X0,X1))=X1)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f5])).
% 0.36/0.47 fof(f335,plain,(
% 0.36/0.47 ![X0,X1]: (rselect_seq(rstore_tail(X0,X1))=rselect_seq(X0))),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f7])).
% 0.36/0.47 fof(f336,plain,(
% 0.36/0.47 ![X0,X1]: (rselect_head(rstore_tail(X0,X1))=rselect_head(X0))),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f8])).
% 0.36/0.47 fof(f337,plain,(
% 0.36/0.47 ![X0,X1]: (rselect_head(rstore_seq(X0,X1))=rselect_head(X0))),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f9])).
% 0.36/0.47 fof(f339,plain,(
% 0.36/0.47 ![X0,X1]: (rselect_tail(rstore_head(X0,X1))=rselect_tail(X0))),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f11])).
% 0.36/0.47 fof(f340,plain,(
% 0.36/0.47 ![X0]: (p(s(X0))=X0)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f12])).
% 0.36/0.47 fof(f341,plain,(
% 0.36/0.47 ![X0]: (s(p(X0))=X0)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f13])).
% 0.36/0.47 fof(f344,plain,(
% 0.36/0.47 ![X0]: (s(s(s(X0)))=X0)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f16])).
% 0.36/0.47 fof(f393,plain,(
% 0.36/0.47 earray_226=store(earray_224,index_225,e42)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f65])).
% 0.36/0.47 fof(f405,plain,(
% 0.36/0.47 earray_260=rselect_seq(q43)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f77])).
% 0.36/0.47 fof(f432,plain,(
% 0.36/0.47 elem_262=select(earray_260,index_261)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f104])).
% 0.36/0.47 fof(f433,plain,(
% 0.36/0.47 elem_265=select(earray_260,index_264)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f105])).
% 0.36/0.47 fof(f434,plain,(
% 0.36/0.47 index_0=rselect_tail(q)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f106])).
% 0.36/0.47 fof(f435,plain,(
% 0.36/0.47 index_102=s(index_99)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f107])).
% 0.36/0.47 fof(f436,plain,(
% 0.36/0.47 index_105=rselect_tail(q24)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f108])).
% 0.36/0.47 fof(f437,plain,(
% 0.36/0.47 index_108=s(index_105)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f109])).
% 0.36/0.47 fof(f438,plain,(
% 0.36/0.47 index_111=rselect_tail(q25)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f110])).
% 0.36/0.47 fof(f439,plain,(
% 0.36/0.47 index_114=s(index_111)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f111])).
% 0.36/0.47 fof(f440,plain,(
% 0.36/0.47 index_117=rselect_tail(q26)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f112])).
% 0.36/0.47 fof(f441,plain,(
% 0.36/0.47 index_12=s(index_9)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f113])).
% 0.36/0.47 fof(f442,plain,(
% 0.36/0.47 index_120=s(index_117)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f114])).
% 0.36/0.47 fof(f443,plain,(
% 0.36/0.47 index_123=rselect_tail(q27)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f115])).
% 0.36/0.47 fof(f444,plain,(
% 0.36/0.47 index_126=s(index_123)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f116])).
% 0.36/0.47 fof(f445,plain,(
% 0.36/0.47 index_129=rselect_tail(q28)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f117])).
% 0.36/0.47 fof(f446,plain,(
% 0.36/0.47 index_132=s(index_129)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f118])).
% 0.36/0.47 fof(f447,plain,(
% 0.36/0.47 index_135=rselect_tail(q2)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f119])).
% 0.36/0.47 fof(f448,plain,(
% 0.36/0.47 index_138=s(index_135)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f120])).
% 0.36/0.47 fof(f449,plain,(
% 0.36/0.47 index_141=rselect_tail(q29)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f121])).
% 0.36/0.47 fof(f450,plain,(
% 0.36/0.47 index_144=s(index_141)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f122])).
% 0.36/0.47 fof(f451,plain,(
% 0.36/0.47 index_147=rselect_tail(q30)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f123])).
% 0.36/0.47 fof(f452,plain,(
% 0.36/0.47 index_15=rselect_tail(q10)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f124])).
% 0.36/0.47 fof(f453,plain,(
% 0.36/0.47 index_150=s(index_147)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f125])).
% 0.36/0.47 fof(f454,plain,(
% 0.36/0.47 index_153=rselect_tail(q31)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f126])).
% 0.36/0.47 fof(f455,plain,(
% 0.36/0.47 index_156=s(index_153)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f127])).
% 0.36/0.47 fof(f456,plain,(
% 0.36/0.47 index_159=rselect_tail(q32)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f128])).
% 0.36/0.47 fof(f457,plain,(
% 0.36/0.47 index_162=s(index_159)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f129])).
% 0.36/0.47 fof(f458,plain,(
% 0.36/0.47 index_165=rselect_tail(q33)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f130])).
% 0.36/0.47 fof(f459,plain,(
% 0.36/0.47 index_168=s(index_165)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f131])).
% 0.36/0.47 fof(f460,plain,(
% 0.36/0.47 index_171=rselect_tail(q34)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f132])).
% 0.36/0.47 fof(f461,plain,(
% 0.36/0.47 index_174=s(index_171)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f133])).
% 0.36/0.47 fof(f462,plain,(
% 0.36/0.47 index_177=rselect_tail(q35)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f134])).
% 0.36/0.47 fof(f463,plain,(
% 0.36/0.47 index_18=s(index_15)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f135])).
% 0.36/0.47 fof(f464,plain,(
% 0.36/0.47 index_180=s(index_177)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f136])).
% 0.36/0.47 fof(f465,plain,(
% 0.36/0.47 index_183=rselect_tail(q36)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f137])).
% 0.36/0.47 fof(f466,plain,(
% 0.36/0.47 index_186=s(index_183)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f138])).
% 0.36/0.47 fof(f467,plain,(
% 0.36/0.47 index_189=rselect_tail(q37)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f139])).
% 0.36/0.47 fof(f468,plain,(
% 0.36/0.47 index_192=s(index_189)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f140])).
% 0.36/0.47 fof(f469,plain,(
% 0.36/0.47 index_195=rselect_tail(q38)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f141])).
% 0.36/0.47 fof(f470,plain,(
% 0.36/0.47 index_198=s(index_195)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f142])).
% 0.36/0.47 fof(f471,plain,(
% 0.36/0.47 index_201=rselect_tail(q3)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f143])).
% 0.36/0.47 fof(f472,plain,(
% 0.36/0.47 index_204=s(index_201)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f144])).
% 0.36/0.47 fof(f473,plain,(
% 0.36/0.47 index_207=rselect_tail(q39)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f145])).
% 0.36/0.47 fof(f474,plain,(
% 0.36/0.47 index_21=rselect_tail(q11)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f146])).
% 0.36/0.47 fof(f475,plain,(
% 0.36/0.47 index_210=s(index_207)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f147])).
% 0.36/0.47 fof(f476,plain,(
% 0.36/0.47 index_213=rselect_tail(q40)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f148])).
% 0.36/0.47 fof(f477,plain,(
% 0.36/0.47 index_216=s(index_213)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f149])).
% 0.36/0.47 fof(f478,plain,(
% 0.36/0.47 index_219=rselect_tail(q41)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f150])).
% 0.36/0.47 fof(f479,plain,(
% 0.36/0.47 index_222=s(index_219)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f151])).
% 0.36/0.47 fof(f480,plain,(
% 0.36/0.47 index_225=rselect_tail(q42)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f152])).
% 0.36/0.47 fof(f481,plain,(
% 0.36/0.47 index_228=s(index_225)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f153])).
% 0.36/0.47 fof(f482,plain,(
% 0.36/0.47 index_231=rselect_tail(q4)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f154])).
% 0.36/0.47 fof(f483,plain,(
% 0.36/0.47 index_234=s(index_231)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f155])).
% 0.36/0.47 fof(f484,plain,(
% 0.36/0.47 index_237=rselect_tail(q5)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f156])).
% 0.36/0.47 fof(f485,plain,(
% 0.36/0.47 index_24=s(index_21)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f157])).
% 0.36/0.47 fof(f486,plain,(
% 0.36/0.47 index_240=s(index_237)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f158])).
% 0.36/0.47 fof(f487,plain,(
% 0.36/0.47 index_243=rselect_tail(q6)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f159])).
% 0.36/0.47 fof(f488,plain,(
% 0.36/0.47 index_246=s(index_243)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f160])).
% 0.36/0.47 fof(f489,plain,(
% 0.36/0.47 index_249=rselect_tail(q7)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f161])).
% 0.36/0.47 fof(f490,plain,(
% 0.36/0.47 index_252=s(index_249)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f162])).
% 0.36/0.47 fof(f491,plain,(
% 0.36/0.47 index_255=rselect_tail(q8)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f163])).
% 0.36/0.47 fof(f492,plain,(
% 0.36/0.47 index_258=s(index_255)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f164])).
% 0.36/0.47 fof(f493,plain,(
% 0.36/0.47 index_261=rselect_head(q43)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f165])).
% 0.36/0.47 fof(f494,plain,(
% 0.36/0.47 index_263=rselect_tail(q43)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f166])).
% 0.36/0.47 fof(f495,plain,(
% 0.36/0.47 s(index_264)=index_263),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f167])).
% 0.36/0.47 fof(f496,plain,(
% 0.36/0.47 index_27=rselect_tail(q12)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f168])).
% 0.36/0.47 fof(f497,plain,(
% 0.36/0.47 index_3=rselect_tail(q0)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f169])).
% 0.36/0.47 fof(f498,plain,(
% 0.36/0.47 index_30=s(index_27)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f170])).
% 0.36/0.47 fof(f499,plain,(
% 0.36/0.47 index_33=rselect_tail(q13)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f171])).
% 0.36/0.47 fof(f500,plain,(
% 0.36/0.47 index_36=s(index_33)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f172])).
% 0.36/0.47 fof(f501,plain,(
% 0.36/0.47 index_39=rselect_tail(q14)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f173])).
% 0.36/0.47 fof(f502,plain,(
% 0.36/0.47 index_42=s(index_39)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f174])).
% 0.36/0.47 fof(f503,plain,(
% 0.36/0.47 index_45=rselect_tail(q15)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f175])).
% 0.36/0.47 fof(f504,plain,(
% 0.36/0.47 index_48=s(index_45)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f176])).
% 0.36/0.47 fof(f505,plain,(
% 0.36/0.47 index_51=rselect_tail(q16)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f177])).
% 0.36/0.47 fof(f506,plain,(
% 0.36/0.47 index_54=s(index_51)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f178])).
% 0.36/0.47 fof(f507,plain,(
% 0.36/0.47 index_57=rselect_tail(q17)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f179])).
% 0.36/0.47 fof(f508,plain,(
% 0.36/0.47 index_6=s(index_3)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f180])).
% 0.36/0.47 fof(f509,plain,(
% 0.36/0.47 index_60=s(index_57)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f181])).
% 0.36/0.47 fof(f510,plain,(
% 0.36/0.47 index_63=rselect_tail(q18)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f182])).
% 0.36/0.47 fof(f511,plain,(
% 0.36/0.47 index_66=s(index_63)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f183])).
% 0.36/0.47 fof(f512,plain,(
% 0.36/0.47 index_69=rselect_tail(q1)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f184])).
% 0.36/0.47 fof(f513,plain,(
% 0.36/0.47 index_72=s(index_69)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f185])).
% 0.36/0.47 fof(f514,plain,(
% 0.36/0.47 index_75=rselect_tail(q19)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f186])).
% 0.36/0.47 fof(f515,plain,(
% 0.36/0.47 index_78=s(index_75)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f187])).
% 0.36/0.47 fof(f516,plain,(
% 0.36/0.47 index_81=rselect_tail(q20)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f188])).
% 0.36/0.47 fof(f517,plain,(
% 0.36/0.47 index_84=s(index_81)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f189])).
% 0.36/0.47 fof(f518,plain,(
% 0.36/0.47 index_87=rselect_tail(q21)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f190])).
% 0.36/0.47 fof(f519,plain,(
% 0.36/0.47 index_9=rselect_tail(q9)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f191])).
% 0.36/0.47 fof(f520,plain,(
% 0.36/0.47 index_90=s(index_87)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f192])).
% 0.36/0.47 fof(f521,plain,(
% 0.36/0.47 index_93=rselect_tail(q22)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f193])).
% 0.36/0.47 fof(f522,plain,(
% 0.36/0.47 index_96=s(index_93)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f194])).
% 0.36/0.47 fof(f523,plain,(
% 0.36/0.47 index_99=rselect_tail(q23)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f195])).
% 0.36/0.47 fof(f524,plain,(
% 0.36/0.47 queue_1=rstore_head(q,index_0)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f196])).
% 0.36/0.47 fof(f525,plain,(
% 0.36/0.47 queue_101=rstore_seq(q23,earray_100)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f197])).
% 0.36/0.47 fof(f526,plain,(
% 0.36/0.47 queue_103=rstore_tail(queue_101,index_102)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f198])).
% 0.36/0.47 fof(f527,plain,(
% 0.36/0.47 queue_107=rstore_seq(q24,earray_106)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f199])).
% 0.36/0.47 fof(f528,plain,(
% 0.36/0.47 queue_109=rstore_tail(queue_107,index_108)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f200])).
% 0.36/0.47 fof(f529,plain,(
% 0.36/0.47 queue_11=rstore_seq(q9,earray_10)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f201])).
% 0.36/0.47 fof(f530,plain,(
% 0.36/0.47 queue_113=rstore_seq(q25,earray_112)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f202])).
% 0.36/0.47 fof(f531,plain,(
% 0.36/0.47 queue_115=rstore_tail(queue_113,index_114)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f203])).
% 0.36/0.47 fof(f532,plain,(
% 0.36/0.47 queue_119=rstore_seq(q26,earray_118)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f204])).
% 0.36/0.47 fof(f533,plain,(
% 0.36/0.47 queue_121=rstore_tail(queue_119,index_120)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f205])).
% 0.36/0.47 fof(f534,plain,(
% 0.36/0.47 queue_125=rstore_seq(q27,earray_124)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f206])).
% 0.36/0.47 fof(f535,plain,(
% 0.36/0.47 queue_127=rstore_tail(queue_125,index_126)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f207])).
% 0.36/0.47 fof(f536,plain,(
% 0.36/0.47 queue_13=rstore_tail(queue_11,index_12)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f208])).
% 0.36/0.47 fof(f537,plain,(
% 0.36/0.47 queue_131=rstore_seq(q28,earray_130)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f209])).
% 0.36/0.47 fof(f538,plain,(
% 0.36/0.47 queue_133=rstore_tail(queue_131,index_132)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f210])).
% 0.36/0.47 fof(f539,plain,(
% 0.36/0.47 queue_137=rstore_seq(q2,earray_136)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f211])).
% 0.36/0.47 fof(f540,plain,(
% 0.36/0.47 queue_139=rstore_tail(queue_137,index_138)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f212])).
% 0.36/0.47 fof(f541,plain,(
% 0.36/0.47 queue_143=rstore_seq(q29,earray_142)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f213])).
% 0.36/0.47 fof(f542,plain,(
% 0.36/0.47 queue_145=rstore_tail(queue_143,index_144)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f214])).
% 0.36/0.47 fof(f543,plain,(
% 0.36/0.47 queue_149=rstore_seq(q30,earray_148)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f215])).
% 0.36/0.47 fof(f544,plain,(
% 0.36/0.47 queue_151=rstore_tail(queue_149,index_150)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f216])).
% 0.36/0.47 fof(f545,plain,(
% 0.36/0.47 queue_155=rstore_seq(q31,earray_154)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f217])).
% 0.36/0.47 fof(f546,plain,(
% 0.36/0.47 queue_157=rstore_tail(queue_155,index_156)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f218])).
% 0.36/0.47 fof(f547,plain,(
% 0.36/0.47 queue_161=rstore_seq(q32,earray_160)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f219])).
% 0.36/0.47 fof(f548,plain,(
% 0.36/0.47 queue_163=rstore_tail(queue_161,index_162)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f220])).
% 0.36/0.47 fof(f549,plain,(
% 0.36/0.47 queue_167=rstore_seq(q33,earray_166)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f221])).
% 0.36/0.47 fof(f550,plain,(
% 0.36/0.47 queue_169=rstore_tail(queue_167,index_168)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f222])).
% 0.36/0.47 fof(f551,plain,(
% 0.36/0.47 queue_17=rstore_seq(q10,earray_16)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f223])).
% 0.36/0.47 fof(f552,plain,(
% 0.36/0.47 queue_173=rstore_seq(q34,earray_172)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f224])).
% 0.36/0.47 fof(f553,plain,(
% 0.36/0.47 queue_175=rstore_tail(queue_173,index_174)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f225])).
% 0.36/0.47 fof(f554,plain,(
% 0.36/0.47 queue_179=rstore_seq(q35,earray_178)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f226])).
% 0.36/0.47 fof(f555,plain,(
% 0.36/0.47 queue_181=rstore_tail(queue_179,index_180)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f227])).
% 0.36/0.47 fof(f556,plain,(
% 0.36/0.47 queue_185=rstore_seq(q36,earray_184)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f228])).
% 0.36/0.47 fof(f557,plain,(
% 0.36/0.47 queue_187=rstore_tail(queue_185,index_186)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f229])).
% 0.36/0.47 fof(f558,plain,(
% 0.36/0.47 queue_19=rstore_tail(queue_17,index_18)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f230])).
% 0.36/0.47 fof(f559,plain,(
% 0.36/0.47 queue_191=rstore_seq(q37,earray_190)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f231])).
% 0.36/0.47 fof(f560,plain,(
% 0.36/0.47 queue_193=rstore_tail(queue_191,index_192)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f232])).
% 0.36/0.47 fof(f561,plain,(
% 0.36/0.47 queue_197=rstore_seq(q38,earray_196)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f233])).
% 0.36/0.47 fof(f562,plain,(
% 0.36/0.47 queue_199=rstore_tail(queue_197,index_198)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f234])).
% 0.36/0.47 fof(f563,plain,(
% 0.36/0.47 queue_203=rstore_seq(q3,earray_202)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f235])).
% 0.36/0.47 fof(f564,plain,(
% 0.36/0.47 queue_205=rstore_tail(queue_203,index_204)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f236])).
% 0.36/0.47 fof(f565,plain,(
% 0.36/0.47 queue_209=rstore_seq(q39,earray_208)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f237])).
% 0.36/0.47 fof(f566,plain,(
% 0.36/0.47 queue_211=rstore_tail(queue_209,index_210)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f238])).
% 0.36/0.47 fof(f567,plain,(
% 0.36/0.47 queue_215=rstore_seq(q40,earray_214)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f239])).
% 0.36/0.47 fof(f568,plain,(
% 0.36/0.47 queue_217=rstore_tail(queue_215,index_216)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f240])).
% 0.36/0.47 fof(f569,plain,(
% 0.36/0.47 queue_221=rstore_seq(q41,earray_220)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f241])).
% 0.36/0.47 fof(f570,plain,(
% 0.36/0.47 queue_223=rstore_tail(queue_221,index_222)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f242])).
% 0.36/0.47 fof(f571,plain,(
% 0.36/0.47 queue_227=rstore_seq(q42,earray_226)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f243])).
% 0.36/0.47 fof(f572,plain,(
% 0.36/0.47 queue_229=rstore_tail(queue_227,index_228)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f244])).
% 0.36/0.47 fof(f573,plain,(
% 0.36/0.47 queue_23=rstore_seq(q11,earray_22)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f245])).
% 0.36/0.47 fof(f574,plain,(
% 0.36/0.47 queue_233=rstore_seq(q4,earray_232)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f246])).
% 0.36/0.47 fof(f575,plain,(
% 0.36/0.47 queue_235=rstore_tail(queue_233,index_234)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f247])).
% 0.36/0.47 fof(f576,plain,(
% 0.36/0.47 queue_239=rstore_seq(q5,earray_238)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f248])).
% 0.36/0.47 fof(f577,plain,(
% 0.36/0.47 queue_241=rstore_tail(queue_239,index_240)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f249])).
% 0.36/0.47 fof(f578,plain,(
% 0.36/0.47 queue_245=rstore_seq(q6,earray_244)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f250])).
% 0.36/0.47 fof(f579,plain,(
% 0.36/0.47 queue_247=rstore_tail(queue_245,index_246)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f251])).
% 0.36/0.47 fof(f580,plain,(
% 0.36/0.47 queue_25=rstore_tail(queue_23,index_24)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f252])).
% 0.36/0.47 fof(f581,plain,(
% 0.36/0.47 queue_251=rstore_seq(q7,earray_250)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f253])).
% 0.36/0.47 fof(f582,plain,(
% 0.36/0.47 queue_253=rstore_tail(queue_251,index_252)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f254])).
% 0.36/0.47 fof(f583,plain,(
% 0.36/0.47 queue_257=rstore_seq(q8,earray_256)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f255])).
% 0.36/0.47 fof(f584,plain,(
% 0.36/0.47 queue_259=rstore_tail(queue_257,index_258)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f256])).
% 0.36/0.47 fof(f585,plain,(
% 0.36/0.47 queue_29=rstore_seq(q12,earray_28)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f257])).
% 0.36/0.47 fof(f586,plain,(
% 0.36/0.47 queue_31=rstore_tail(queue_29,index_30)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f258])).
% 0.36/0.47 fof(f587,plain,(
% 0.36/0.47 queue_35=rstore_seq(q13,earray_34)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f259])).
% 0.36/0.47 fof(f588,plain,(
% 0.36/0.47 queue_37=rstore_tail(queue_35,index_36)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f260])).
% 0.36/0.47 fof(f589,plain,(
% 0.36/0.47 queue_41=rstore_seq(q14,earray_40)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f261])).
% 0.36/0.47 fof(f590,plain,(
% 0.36/0.47 queue_43=rstore_tail(queue_41,index_42)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f262])).
% 0.36/0.47 fof(f591,plain,(
% 0.36/0.47 queue_47=rstore_seq(q15,earray_46)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f263])).
% 0.36/0.47 fof(f592,plain,(
% 0.36/0.47 queue_49=rstore_tail(queue_47,index_48)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f264])).
% 0.36/0.47 fof(f593,plain,(
% 0.36/0.47 queue_5=rstore_seq(q0,earray_4)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f265])).
% 0.36/0.47 fof(f594,plain,(
% 0.36/0.47 queue_53=rstore_seq(q16,earray_52)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f266])).
% 0.36/0.47 fof(f595,plain,(
% 0.36/0.47 queue_55=rstore_tail(queue_53,index_54)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f267])).
% 0.36/0.47 fof(f596,plain,(
% 0.36/0.47 queue_59=rstore_seq(q17,earray_58)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f268])).
% 0.36/0.47 fof(f597,plain,(
% 0.36/0.47 queue_61=rstore_tail(queue_59,index_60)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f269])).
% 0.36/0.47 fof(f598,plain,(
% 0.36/0.47 queue_65=rstore_seq(q18,earray_64)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f270])).
% 0.36/0.47 fof(f599,plain,(
% 0.36/0.47 queue_67=rstore_tail(queue_65,index_66)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f271])).
% 0.36/0.47 fof(f600,plain,(
% 0.36/0.47 queue_7=rstore_tail(queue_5,index_6)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f272])).
% 0.36/0.47 fof(f601,plain,(
% 0.36/0.47 queue_71=rstore_seq(q1,earray_70)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f273])).
% 0.36/0.47 fof(f602,plain,(
% 0.36/0.47 queue_73=rstore_tail(queue_71,index_72)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f274])).
% 0.36/0.47 fof(f603,plain,(
% 0.36/0.47 queue_77=rstore_seq(q19,earray_76)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f275])).
% 0.36/0.47 fof(f604,plain,(
% 0.36/0.47 queue_79=rstore_tail(queue_77,index_78)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f276])).
% 0.36/0.47 fof(f605,plain,(
% 0.36/0.47 queue_83=rstore_seq(q20,earray_82)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f277])).
% 0.36/0.47 fof(f606,plain,(
% 0.36/0.47 queue_85=rstore_tail(queue_83,index_84)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f278])).
% 0.36/0.47 fof(f607,plain,(
% 0.36/0.47 queue_89=rstore_seq(q21,earray_88)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f279])).
% 0.36/0.47 fof(f608,plain,(
% 0.36/0.47 queue_91=rstore_tail(queue_89,index_90)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f280])).
% 0.36/0.47 fof(f609,plain,(
% 0.36/0.47 queue_95=rstore_seq(q22,earray_94)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f281])).
% 0.36/0.47 fof(f610,plain,(
% 0.36/0.47 queue_97=rstore_tail(queue_95,index_96)),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f282])).
% 0.36/0.47 fof(f611,plain,(
% 0.36/0.47 q0=queue_1),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f283])).
% 0.36/0.47 fof(f612,plain,(
% 0.36/0.47 q1=queue_7),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f284])).
% 0.36/0.47 fof(f613,plain,(
% 0.36/0.47 q10=queue_13),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f285])).
% 0.36/0.47 fof(f614,plain,(
% 0.36/0.47 q11=queue_19),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f286])).
% 0.36/0.47 fof(f615,plain,(
% 0.36/0.47 q12=queue_25),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f287])).
% 0.36/0.47 fof(f616,plain,(
% 0.36/0.47 q13=queue_31),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f288])).
% 0.36/0.47 fof(f617,plain,(
% 0.36/0.47 q14=queue_37),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f289])).
% 0.36/0.47 fof(f618,plain,(
% 0.36/0.47 q15=queue_43),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f290])).
% 0.36/0.47 fof(f619,plain,(
% 0.36/0.47 q16=queue_49),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f291])).
% 0.36/0.47 fof(f620,plain,(
% 0.36/0.47 q17=queue_55),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f292])).
% 0.36/0.47 fof(f621,plain,(
% 0.36/0.47 q18=queue_61),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f293])).
% 0.36/0.47 fof(f622,plain,(
% 0.36/0.47 q19=queue_67),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f294])).
% 0.36/0.47 fof(f623,plain,(
% 0.36/0.47 q2=queue_73),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f295])).
% 0.36/0.47 fof(f624,plain,(
% 0.36/0.47 q20=queue_79),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f296])).
% 0.36/0.47 fof(f625,plain,(
% 0.36/0.47 q21=queue_85),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f297])).
% 0.36/0.47 fof(f626,plain,(
% 0.36/0.47 q22=queue_91),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f298])).
% 0.36/0.47 fof(f627,plain,(
% 0.36/0.47 q23=queue_97),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f299])).
% 0.36/0.47 fof(f628,plain,(
% 0.36/0.47 q24=queue_103),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f300])).
% 0.36/0.47 fof(f629,plain,(
% 0.36/0.47 q25=queue_109),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f301])).
% 0.36/0.47 fof(f630,plain,(
% 0.36/0.47 q26=queue_115),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f302])).
% 0.36/0.47 fof(f631,plain,(
% 0.36/0.47 q27=queue_121),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f303])).
% 0.36/0.47 fof(f632,plain,(
% 0.36/0.47 q28=queue_127),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f304])).
% 0.36/0.47 fof(f633,plain,(
% 0.36/0.47 q29=queue_133),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f305])).
% 0.36/0.47 fof(f634,plain,(
% 0.36/0.47 q3=queue_139),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f306])).
% 0.36/0.47 fof(f635,plain,(
% 0.36/0.47 q30=queue_145),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f307])).
% 0.36/0.47 fof(f636,plain,(
% 0.36/0.47 q31=queue_151),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f308])).
% 0.36/0.47 fof(f637,plain,(
% 0.36/0.47 q32=queue_157),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f309])).
% 0.36/0.47 fof(f638,plain,(
% 0.36/0.47 q33=queue_163),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f310])).
% 0.36/0.47 fof(f639,plain,(
% 0.36/0.47 q34=queue_169),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f311])).
% 0.36/0.47 fof(f640,plain,(
% 0.36/0.47 q35=queue_175),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f312])).
% 0.36/0.47 fof(f641,plain,(
% 0.36/0.47 q36=queue_181),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f313])).
% 0.36/0.47 fof(f642,plain,(
% 0.36/0.47 q37=queue_187),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f314])).
% 0.36/0.47 fof(f643,plain,(
% 0.36/0.47 q38=queue_193),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f315])).
% 0.36/0.47 fof(f644,plain,(
% 0.36/0.47 q39=queue_199),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f316])).
% 0.36/0.47 fof(f645,plain,(
% 0.36/0.47 q4=queue_205),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f317])).
% 0.36/0.47 fof(f646,plain,(
% 0.36/0.47 q40=queue_211),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f318])).
% 0.36/0.47 fof(f647,plain,(
% 0.36/0.47 q41=queue_217),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f319])).
% 0.36/0.47 fof(f648,plain,(
% 0.36/0.47 q42=queue_223),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f320])).
% 0.36/0.47 fof(f649,plain,(
% 0.36/0.47 q43=queue_229),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f321])).
% 0.36/0.47 fof(f650,plain,(
% 0.36/0.47 q5=queue_235),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f322])).
% 0.36/0.47 fof(f651,plain,(
% 0.36/0.47 q6=queue_241),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f323])).
% 0.36/0.47 fof(f652,plain,(
% 0.36/0.47 q7=queue_247),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f324])).
% 0.36/0.47 fof(f653,plain,(
% 0.36/0.47 q8=queue_253),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f325])).
% 0.36/0.47 fof(f654,plain,(
% 0.36/0.47 q9=queue_259),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f326])).
% 0.36/0.47 fof(f655,plain,(
% 0.36/0.47 ~elem_262=elem_265),
% 0.36/0.47 inference(cnf_transformation,[status(thm)],[f327])).
% 0.36/0.47 fof(f656,plain,(
% 0.36/0.47 q0=rstore_head(q,index_0)),
% 0.36/0.47 inference(backward_demodulation,[status(thm)],[f611,f524])).
% 0.36/0.47 fof(f657,plain,(
% 0.36/0.47 q1=rstore_tail(queue_5,index_6)),
% 0.36/0.47 inference(backward_demodulation,[status(thm)],[f612,f600])).
% 0.36/0.47 fof(f658,plain,(
% 0.36/0.47 q10=rstore_tail(queue_11,index_12)),
% 0.36/0.47 inference(backward_demodulation,[status(thm)],[f613,f536])).
% 0.36/0.47 fof(f659,plain,(
% 0.36/0.47 q11=rstore_tail(queue_17,index_18)),
% 0.36/0.47 inference(backward_demodulation,[status(thm)],[f614,f558])).
% 0.36/0.47 fof(f660,plain,(
% 0.36/0.47 q12=rstore_tail(queue_23,index_24)),
% 0.36/0.47 inference(backward_demodulation,[status(thm)],[f615,f580])).
% 0.36/0.47 fof(f661,plain,(
% 0.36/0.47 q13=rstore_tail(queue_29,index_30)),
% 0.36/0.47 inference(backward_demodulation,[status(thm)],[f616,f586])).
% 0.36/0.47 fof(f662,plain,(
% 0.36/0.48 q14=rstore_tail(queue_35,index_36)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f617,f588])).
% 0.36/0.48 fof(f663,plain,(
% 0.36/0.48 q15=rstore_tail(queue_41,index_42)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f618,f590])).
% 0.36/0.48 fof(f664,plain,(
% 0.36/0.48 q16=rstore_tail(queue_47,index_48)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f619,f592])).
% 0.36/0.48 fof(f665,plain,(
% 0.36/0.48 q17=rstore_tail(queue_53,index_54)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f620,f595])).
% 0.36/0.48 fof(f666,plain,(
% 0.36/0.48 q18=rstore_tail(queue_59,index_60)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f621,f597])).
% 0.36/0.48 fof(f667,plain,(
% 0.36/0.48 q19=rstore_tail(queue_65,index_66)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f622,f599])).
% 0.36/0.48 fof(f668,plain,(
% 0.36/0.48 q2=rstore_tail(queue_71,index_72)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f623,f602])).
% 0.36/0.48 fof(f669,plain,(
% 0.36/0.48 q20=rstore_tail(queue_77,index_78)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f624,f604])).
% 0.36/0.48 fof(f670,plain,(
% 0.36/0.48 q21=rstore_tail(queue_83,index_84)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f625,f606])).
% 0.36/0.48 fof(f671,plain,(
% 0.36/0.48 q22=rstore_tail(queue_89,index_90)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f626,f608])).
% 0.36/0.48 fof(f672,plain,(
% 0.36/0.48 q23=rstore_tail(queue_95,index_96)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f627,f610])).
% 0.36/0.48 fof(f673,plain,(
% 0.36/0.48 q24=rstore_tail(queue_101,index_102)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f628,f526])).
% 0.36/0.48 fof(f674,plain,(
% 0.36/0.48 q25=rstore_tail(queue_107,index_108)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f629,f528])).
% 0.36/0.48 fof(f675,plain,(
% 0.36/0.48 q26=rstore_tail(queue_113,index_114)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f630,f531])).
% 0.36/0.48 fof(f676,plain,(
% 0.36/0.48 q27=rstore_tail(queue_119,index_120)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f631,f533])).
% 0.36/0.48 fof(f677,plain,(
% 0.36/0.48 q28=rstore_tail(queue_125,index_126)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f632,f535])).
% 0.36/0.48 fof(f678,plain,(
% 0.36/0.48 q29=rstore_tail(queue_131,index_132)),
% 0.36/0.48 inference(backward_demodulation,[status(thm)],[f633,f538])).
% 0.36/0.48 fof(f679,plain,(
% 0.36/0.48 q3=rstore_tail(queue_137,index_138)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f634,f540])).
% 0.36/0.49 fof(f680,plain,(
% 0.36/0.49 q30=rstore_tail(queue_143,index_144)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f635,f542])).
% 0.36/0.49 fof(f681,plain,(
% 0.36/0.49 q31=rstore_tail(queue_149,index_150)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f636,f544])).
% 0.36/0.49 fof(f682,plain,(
% 0.36/0.49 q32=rstore_tail(queue_155,index_156)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f637,f546])).
% 0.36/0.49 fof(f683,plain,(
% 0.36/0.49 q33=rstore_tail(queue_161,index_162)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f638,f548])).
% 0.36/0.49 fof(f684,plain,(
% 0.36/0.49 q34=rstore_tail(queue_167,index_168)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f639,f550])).
% 0.36/0.49 fof(f685,plain,(
% 0.36/0.49 q35=rstore_tail(queue_173,index_174)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f640,f553])).
% 0.36/0.49 fof(f686,plain,(
% 0.36/0.49 q36=rstore_tail(queue_179,index_180)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f641,f555])).
% 0.36/0.49 fof(f687,plain,(
% 0.36/0.49 q37=rstore_tail(queue_185,index_186)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f642,f557])).
% 0.36/0.49 fof(f688,plain,(
% 0.36/0.49 q38=rstore_tail(queue_191,index_192)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f643,f560])).
% 0.36/0.49 fof(f689,plain,(
% 0.36/0.49 q39=rstore_tail(queue_197,index_198)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f644,f562])).
% 0.36/0.49 fof(f690,plain,(
% 0.36/0.49 q4=rstore_tail(queue_203,index_204)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f645,f564])).
% 0.36/0.49 fof(f691,plain,(
% 0.36/0.49 q40=rstore_tail(queue_209,index_210)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f646,f566])).
% 0.36/0.49 fof(f692,plain,(
% 0.36/0.49 q41=rstore_tail(queue_215,index_216)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f647,f568])).
% 0.36/0.49 fof(f693,plain,(
% 0.36/0.49 q42=rstore_tail(queue_221,index_222)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f648,f570])).
% 0.36/0.49 fof(f694,plain,(
% 0.36/0.49 q43=rstore_tail(queue_227,index_228)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f649,f572])).
% 0.36/0.49 fof(f695,plain,(
% 0.36/0.49 q5=rstore_tail(queue_233,index_234)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f650,f575])).
% 0.36/0.49 fof(f696,plain,(
% 0.36/0.49 q6=rstore_tail(queue_239,index_240)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f651,f577])).
% 0.36/0.49 fof(f697,plain,(
% 0.36/0.49 q7=rstore_tail(queue_245,index_246)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f652,f579])).
% 0.36/0.49 fof(f698,plain,(
% 0.36/0.49 q8=rstore_tail(queue_251,index_252)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f653,f582])).
% 0.36/0.49 fof(f699,plain,(
% 0.36/0.49 q9=rstore_tail(queue_257,index_258)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f654,f584])).
% 0.36/0.49 fof(f708,plain,(
% 0.36/0.49 ![X0]: (s(s(X0))=p(X0))),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f341,f344])).
% 0.36/0.49 fof(f767,plain,(
% 0.36/0.49 select(earray_226,index_225)=e42),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f393,f328])).
% 0.36/0.49 fof(f772,plain,(
% 0.36/0.49 p(index_108)=index_105),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f437,f340])).
% 0.36/0.49 fof(f784,plain,(
% 0.36/0.49 p(index_12)=index_9),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f441,f340])).
% 0.36/0.49 fof(f792,plain,(
% 0.36/0.49 p(index_126)=index_123),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f444,f340])).
% 0.36/0.49 fof(f804,plain,(
% 0.36/0.49 p(index_138)=index_135),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f448,f340])).
% 0.36/0.49 fof(f812,plain,(
% 0.36/0.49 p(index_150)=index_147),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f453,f340])).
% 0.36/0.49 fof(f828,plain,(
% 0.36/0.49 p(index_168)=index_165),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f459,f340])).
% 0.36/0.49 fof(f832,plain,(
% 0.36/0.49 p(index_18)=index_15),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f463,f340])).
% 0.36/0.49 fof(f836,plain,(
% 0.36/0.49 p(index_186)=index_183),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f466,f340])).
% 0.36/0.49 fof(f842,plain,(
% 0.36/0.49 p(index_204)=index_201),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f472,f340])).
% 0.36/0.49 fof(f844,plain,(
% 0.36/0.49 p(index_210)=index_207),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f475,f340])).
% 0.36/0.49 fof(f850,plain,(
% 0.36/0.49 p(index_228)=index_225),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f481,f340])).
% 0.36/0.49 fof(f856,plain,(
% 0.36/0.49 p(index_240)=index_237),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f486,f340])).
% 0.36/0.49 fof(f864,plain,(
% 0.36/0.49 p(index_263)=index_264),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f495,f340])).
% 0.36/0.49 fof(f868,plain,(
% 0.36/0.49 p(index_36)=index_33),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f500,f340])).
% 0.36/0.49 fof(f874,plain,(
% 0.36/0.49 p(index_54)=index_51),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f506,f340])).
% 0.36/0.49 fof(f876,plain,(
% 0.36/0.49 p(index_6)=index_3),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f508,f340])).
% 0.36/0.49 fof(f884,plain,(
% 0.36/0.49 p(index_78)=index_75),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f515,f340])).
% 0.36/0.49 fof(f893,plain,(
% 0.36/0.49 rselect_head(queue_101)=rselect_head(q23)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f525,f337])).
% 0.36/0.49 fof(f897,plain,(
% 0.36/0.49 rselect_head(queue_107)=rselect_head(q24)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f527,f337])).
% 0.36/0.49 fof(f901,plain,(
% 0.36/0.49 rselect_head(queue_11)=rselect_head(q9)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f529,f337])).
% 0.36/0.49 fof(f910,plain,(
% 0.36/0.49 rselect_head(queue_113)=rselect_head(q25)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f530,f337])).
% 0.36/0.49 fof(f926,plain,(
% 0.36/0.49 rselect_head(queue_119)=rselect_head(q26)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f532,f337])).
% 0.36/0.49 fof(f930,plain,(
% 0.36/0.49 rselect_head(queue_125)=rselect_head(q27)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f534,f337])).
% 0.36/0.49 fof(f952,plain,(
% 0.36/0.49 rselect_head(queue_131)=rselect_head(q28)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f537,f337])).
% 0.36/0.49 fof(f956,plain,(
% 0.36/0.49 rselect_head(queue_137)=rselect_head(q2)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f539,f337])).
% 0.36/0.49 fof(f960,plain,(
% 0.36/0.49 rselect_head(queue_143)=rselect_head(q29)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f541,f337])).
% 0.36/0.49 fof(f970,plain,(
% 0.36/0.49 rselect_head(queue_149)=rselect_head(q30)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f543,f337])).
% 0.36/0.49 fof(f986,plain,(
% 0.36/0.49 rselect_head(queue_155)=rselect_head(q31)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f545,f337])).
% 0.36/0.49 fof(f990,plain,(
% 0.36/0.49 rselect_head(queue_161)=rselect_head(q32)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f547,f337])).
% 0.36/0.49 fof(f1012,plain,(
% 0.36/0.49 rselect_head(queue_167)=rselect_head(q33)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f549,f337])).
% 0.36/0.49 fof(f1016,plain,(
% 0.36/0.49 rselect_head(queue_17)=rselect_head(q10)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f551,f337])).
% 0.36/0.49 fof(f1020,plain,(
% 0.36/0.49 rselect_head(queue_173)=rselect_head(q34)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f552,f337])).
% 0.36/0.49 fof(f1030,plain,(
% 0.36/0.49 rselect_head(queue_179)=rselect_head(q35)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f554,f337])).
% 0.36/0.49 fof(f1046,plain,(
% 0.36/0.49 rselect_head(queue_185)=rselect_head(q36)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f556,f337])).
% 0.36/0.49 fof(f1050,plain,(
% 0.36/0.49 rselect_head(queue_191)=rselect_head(q37)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f559,f337])).
% 0.36/0.49 fof(f1072,plain,(
% 0.36/0.49 rselect_head(queue_197)=rselect_head(q38)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f561,f337])).
% 0.36/0.49 fof(f1076,plain,(
% 0.36/0.49 rselect_head(queue_203)=rselect_head(q3)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f563,f337])).
% 0.36/0.49 fof(f1080,plain,(
% 0.36/0.49 rselect_head(queue_209)=rselect_head(q39)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f565,f337])).
% 0.36/0.49 fof(f1090,plain,(
% 0.36/0.49 rselect_head(queue_215)=rselect_head(q40)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f567,f337])).
% 0.36/0.49 fof(f1106,plain,(
% 0.36/0.49 rselect_head(queue_221)=rselect_head(q41)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f569,f337])).
% 0.36/0.49 fof(f1110,plain,(
% 0.36/0.49 rselect_head(queue_227)=rselect_head(q42)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f571,f337])).
% 0.36/0.49 fof(f1111,plain,(
% 0.36/0.49 rselect_seq(queue_227)=earray_226),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f571,f331])).
% 0.36/0.49 fof(f1123,plain,(
% 0.36/0.49 rselect_head(queue_23)=rselect_head(q11)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f573,f337])).
% 0.36/0.49 fof(f1127,plain,(
% 0.36/0.49 rselect_head(queue_233)=rselect_head(q4)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f574,f337])).
% 0.36/0.49 fof(f1131,plain,(
% 0.36/0.49 rselect_head(queue_239)=rselect_head(q5)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f576,f337])).
% 0.36/0.49 fof(f1135,plain,(
% 0.36/0.49 rselect_head(queue_245)=rselect_head(q6)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f578,f337])).
% 0.36/0.49 fof(f1139,plain,(
% 0.36/0.49 rselect_head(queue_251)=rselect_head(q7)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f581,f337])).
% 0.36/0.49 fof(f1143,plain,(
% 0.36/0.49 rselect_head(queue_257)=rselect_head(q8)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f583,f337])).
% 0.36/0.49 fof(f1147,plain,(
% 0.36/0.49 rselect_head(queue_29)=rselect_head(q12)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f585,f337])).
% 0.36/0.49 fof(f1151,plain,(
% 0.36/0.49 rselect_head(queue_35)=rselect_head(q13)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f587,f337])).
% 0.36/0.49 fof(f1155,plain,(
% 0.36/0.49 rselect_head(queue_41)=rselect_head(q14)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f589,f337])).
% 0.36/0.49 fof(f1159,plain,(
% 0.36/0.49 rselect_head(queue_47)=rselect_head(q15)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f591,f337])).
% 0.36/0.49 fof(f1163,plain,(
% 0.36/0.49 rselect_head(queue_5)=rselect_head(q0)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f593,f337])).
% 0.36/0.49 fof(f1167,plain,(
% 0.36/0.49 rselect_head(queue_53)=rselect_head(q16)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f594,f337])).
% 0.36/0.49 fof(f1171,plain,(
% 0.36/0.49 rselect_head(queue_59)=rselect_head(q17)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f596,f337])).
% 0.36/0.49 fof(f1175,plain,(
% 0.36/0.49 rselect_head(queue_65)=rselect_head(q18)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f598,f337])).
% 0.36/0.49 fof(f1179,plain,(
% 0.36/0.49 rselect_head(queue_71)=rselect_head(q1)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f601,f337])).
% 0.36/0.49 fof(f1183,plain,(
% 0.36/0.49 rselect_head(queue_77)=rselect_head(q19)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f603,f337])).
% 0.36/0.49 fof(f1187,plain,(
% 0.36/0.49 rselect_head(queue_83)=rselect_head(q20)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f605,f337])).
% 0.36/0.49 fof(f1191,plain,(
% 0.36/0.49 rselect_head(queue_89)=rselect_head(q21)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f607,f337])).
% 0.36/0.49 fof(f1195,plain,(
% 0.36/0.49 rselect_head(queue_95)=rselect_head(q22)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f609,f337])).
% 0.36/0.49 fof(f1198,plain,(
% 0.36/0.49 rselect_tail(q0)=rselect_tail(q)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f656,f339])).
% 0.36/0.49 fof(f1200,plain,(
% 0.36/0.49 rselect_head(q0)=index_0),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f656,f332])).
% 0.36/0.49 fof(f1201,plain,(
% 0.36/0.49 index_0=index_3),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1202,f434])).
% 0.36/0.49 fof(f1202,plain,(
% 0.36/0.49 index_3=rselect_tail(q)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f497,f1198])).
% 0.36/0.49 fof(f1204,plain,(
% 0.36/0.49 rselect_head(queue_5)=index_0),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1200,f1163])).
% 0.36/0.49 fof(f1207,plain,(
% 0.36/0.49 rselect_head(queue_5)=index_3),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1201,f1204])).
% 0.36/0.49 fof(f1208,plain,(
% 0.36/0.49 rselect_head(q1)=rselect_head(queue_5)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f657,f336])).
% 0.36/0.49 fof(f1210,plain,(
% 0.36/0.49 rselect_tail(q1)=index_6),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f657,f333])).
% 0.36/0.49 fof(f1211,plain,(
% 0.36/0.49 rselect_head(queue_71)=index_3),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1212,f1179])).
% 0.36/0.49 fof(f1212,plain,(
% 0.36/0.49 rselect_head(q1)=index_3),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1207,f1208])).
% 0.36/0.49 fof(f1219,plain,(
% 0.36/0.49 p(index_69)=index_3),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1223,f876])).
% 0.36/0.49 fof(f1223,plain,(
% 0.36/0.49 index_69=index_6),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f512,f1210])).
% 0.36/0.49 fof(f1225,plain,(
% 0.36/0.49 rselect_head(q10)=rselect_head(queue_11)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f658,f336])).
% 0.36/0.49 fof(f1227,plain,(
% 0.36/0.49 rselect_tail(q10)=index_12),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f658,f333])).
% 0.36/0.49 fof(f1228,plain,(
% 0.36/0.49 rselect_head(q10)=rselect_head(q9)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1225,f901])).
% 0.36/0.49 fof(f1236,plain,(
% 0.36/0.49 p(index_15)=index_9),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1239,f784])).
% 0.36/0.49 fof(f1239,plain,(
% 0.36/0.49 index_15=index_12),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f452,f1227])).
% 0.36/0.49 fof(f1241,plain,(
% 0.36/0.49 rselect_head(q11)=rselect_head(queue_17)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f659,f336])).
% 0.36/0.49 fof(f1243,plain,(
% 0.36/0.49 rselect_tail(q11)=index_18),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f659,f333])).
% 0.36/0.49 fof(f1244,plain,(
% 0.36/0.49 rselect_head(queue_23)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1245,f1123])).
% 0.36/0.49 fof(f1245,plain,(
% 0.36/0.49 rselect_head(q11)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1016,f1241])).
% 0.36/0.49 fof(f1253,plain,(
% 0.36/0.49 p(index_21)=index_15),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1257,f832])).
% 0.36/0.49 fof(f1257,plain,(
% 0.36/0.49 index_21=index_18),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f474,f1243])).
% 0.36/0.49 fof(f1259,plain,(
% 0.36/0.49 rselect_head(q12)=rselect_head(queue_23)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f660,f336])).
% 0.36/0.49 fof(f1261,plain,(
% 0.36/0.49 rselect_tail(q12)=index_24),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f660,f333])).
% 0.36/0.49 fof(f1262,plain,(
% 0.36/0.49 rselect_head(queue_29)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1263,f1147])).
% 0.36/0.49 fof(f1263,plain,(
% 0.36/0.49 rselect_head(q12)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1244,f1259])).
% 0.36/0.49 fof(f1272,plain,(
% 0.36/0.49 index_27=s(index_21)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1275,f485])).
% 0.36/0.49 fof(f1275,plain,(
% 0.36/0.49 index_27=index_24),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f496,f1261])).
% 0.36/0.49 fof(f1277,plain,(
% 0.36/0.49 rselect_head(q13)=rselect_head(queue_29)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f661,f336])).
% 0.36/0.49 fof(f1279,plain,(
% 0.36/0.49 rselect_tail(q13)=index_30),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f661,f333])).
% 0.36/0.49 fof(f1280,plain,(
% 0.36/0.49 rselect_head(queue_35)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1281,f1151])).
% 0.36/0.49 fof(f1281,plain,(
% 0.36/0.49 rselect_head(q13)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1262,f1277])).
% 0.36/0.49 fof(f1290,plain,(
% 0.36/0.49 index_33=s(index_27)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1293,f498])).
% 0.36/0.49 fof(f1293,plain,(
% 0.36/0.49 index_33=index_30),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f499,f1279])).
% 0.36/0.49 fof(f1295,plain,(
% 0.36/0.49 rselect_head(q14)=rselect_head(queue_35)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f662,f336])).
% 0.36/0.49 fof(f1297,plain,(
% 0.36/0.49 rselect_tail(q14)=index_36),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f662,f333])).
% 0.36/0.49 fof(f1298,plain,(
% 0.36/0.49 rselect_head(queue_41)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1299,f1155])).
% 0.36/0.49 fof(f1299,plain,(
% 0.36/0.49 rselect_head(q14)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1280,f1295])).
% 0.36/0.49 fof(f1306,plain,(
% 0.36/0.49 p(index_39)=index_33),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1311,f868])).
% 0.36/0.49 fof(f1311,plain,(
% 0.36/0.49 index_39=index_36),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f501,f1297])).
% 0.36/0.49 fof(f1313,plain,(
% 0.36/0.49 rselect_head(q15)=rselect_head(queue_41)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f663,f336])).
% 0.36/0.49 fof(f1315,plain,(
% 0.36/0.49 rselect_tail(q15)=index_42),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f663,f333])).
% 0.36/0.49 fof(f1316,plain,(
% 0.36/0.49 rselect_head(queue_47)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1317,f1159])).
% 0.36/0.49 fof(f1317,plain,(
% 0.36/0.49 rselect_head(q15)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1298,f1313])).
% 0.36/0.49 fof(f1326,plain,(
% 0.36/0.49 index_45=s(index_39)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1329,f502])).
% 0.36/0.49 fof(f1329,plain,(
% 0.36/0.49 index_45=index_42),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f503,f1315])).
% 0.36/0.49 fof(f1331,plain,(
% 0.36/0.49 rselect_head(q16)=rselect_head(queue_47)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f664,f336])).
% 0.36/0.49 fof(f1333,plain,(
% 0.36/0.49 rselect_tail(q16)=index_48),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f664,f333])).
% 0.36/0.49 fof(f1334,plain,(
% 0.36/0.49 rselect_head(queue_53)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1335,f1167])).
% 0.36/0.49 fof(f1335,plain,(
% 0.36/0.49 rselect_head(q16)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1316,f1331])).
% 0.36/0.49 fof(f1344,plain,(
% 0.36/0.49 index_51=s(index_45)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1347,f504])).
% 0.36/0.49 fof(f1347,plain,(
% 0.36/0.49 index_51=index_48),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f505,f1333])).
% 0.36/0.49 fof(f1349,plain,(
% 0.36/0.49 rselect_head(q17)=rselect_head(queue_53)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f665,f336])).
% 0.36/0.49 fof(f1351,plain,(
% 0.36/0.49 rselect_tail(q17)=index_54),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f665,f333])).
% 0.36/0.49 fof(f1352,plain,(
% 0.36/0.49 rselect_head(queue_59)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1353,f1171])).
% 0.36/0.49 fof(f1353,plain,(
% 0.36/0.49 rselect_head(q17)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1334,f1349])).
% 0.36/0.49 fof(f1360,plain,(
% 0.36/0.49 p(index_57)=index_51),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1365,f874])).
% 0.36/0.49 fof(f1365,plain,(
% 0.36/0.49 index_57=index_54),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f507,f1351])).
% 0.36/0.49 fof(f1367,plain,(
% 0.36/0.49 rselect_head(q18)=rselect_head(queue_59)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f666,f336])).
% 0.36/0.49 fof(f1369,plain,(
% 0.36/0.49 rselect_tail(q18)=index_60),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f666,f333])).
% 0.36/0.49 fof(f1370,plain,(
% 0.36/0.49 rselect_head(queue_65)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1371,f1175])).
% 0.36/0.49 fof(f1371,plain,(
% 0.36/0.49 rselect_head(q18)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1352,f1367])).
% 0.36/0.49 fof(f1380,plain,(
% 0.36/0.49 index_63=s(index_57)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1383,f509])).
% 0.36/0.49 fof(f1383,plain,(
% 0.36/0.49 index_63=index_60),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f510,f1369])).
% 0.36/0.49 fof(f1385,plain,(
% 0.36/0.49 rselect_head(q19)=rselect_head(queue_65)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f667,f336])).
% 0.36/0.49 fof(f1387,plain,(
% 0.36/0.49 rselect_tail(q19)=index_66),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f667,f333])).
% 0.36/0.49 fof(f1388,plain,(
% 0.36/0.49 rselect_head(queue_77)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1389,f1183])).
% 0.36/0.49 fof(f1389,plain,(
% 0.36/0.49 rselect_head(q19)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1370,f1385])).
% 0.36/0.49 fof(f1398,plain,(
% 0.36/0.49 index_75=s(index_63)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1401,f511])).
% 0.36/0.49 fof(f1401,plain,(
% 0.36/0.49 index_75=index_66),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f514,f1387])).
% 0.36/0.49 fof(f1403,plain,(
% 0.36/0.49 rselect_head(q2)=rselect_head(queue_71)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f668,f336])).
% 0.36/0.49 fof(f1405,plain,(
% 0.36/0.49 rselect_tail(q2)=index_72),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f668,f333])).
% 0.36/0.49 fof(f1406,plain,(
% 0.36/0.49 rselect_head(queue_137)=index_3),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1407,f956])).
% 0.36/0.49 fof(f1407,plain,(
% 0.36/0.49 rselect_head(q2)=index_3),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1211,f1403])).
% 0.36/0.49 fof(f1414,plain,(
% 0.36/0.49 index_135=s(index_69)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1416,f513])).
% 0.36/0.49 fof(f1416,plain,(
% 0.36/0.49 index_135=index_72),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f447,f1405])).
% 0.36/0.49 fof(f1422,plain,(
% 0.36/0.49 rselect_head(q20)=rselect_head(queue_77)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f669,f336])).
% 0.36/0.49 fof(f1424,plain,(
% 0.36/0.49 rselect_tail(q20)=index_78),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f669,f333])).
% 0.36/0.49 fof(f1425,plain,(
% 0.36/0.49 rselect_head(queue_83)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1426,f1187])).
% 0.36/0.49 fof(f1426,plain,(
% 0.36/0.49 rselect_head(q20)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1388,f1422])).
% 0.36/0.49 fof(f1433,plain,(
% 0.36/0.49 p(index_81)=index_75),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1438,f884])).
% 0.36/0.49 fof(f1438,plain,(
% 0.36/0.49 index_81=index_78),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f516,f1424])).
% 0.36/0.49 fof(f1440,plain,(
% 0.36/0.49 rselect_head(q21)=rselect_head(queue_83)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f670,f336])).
% 0.36/0.49 fof(f1442,plain,(
% 0.36/0.49 rselect_tail(q21)=index_84),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f670,f333])).
% 0.36/0.49 fof(f1443,plain,(
% 0.36/0.49 rselect_head(queue_89)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1444,f1191])).
% 0.36/0.49 fof(f1444,plain,(
% 0.36/0.49 rselect_head(q21)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1425,f1440])).
% 0.36/0.49 fof(f1453,plain,(
% 0.36/0.49 index_87=s(index_81)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1456,f517])).
% 0.36/0.49 fof(f1456,plain,(
% 0.36/0.49 index_87=index_84),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f518,f1442])).
% 0.36/0.49 fof(f1458,plain,(
% 0.36/0.49 rselect_head(q22)=rselect_head(queue_89)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f671,f336])).
% 0.36/0.49 fof(f1460,plain,(
% 0.36/0.49 rselect_tail(q22)=index_90),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f671,f333])).
% 0.36/0.49 fof(f1461,plain,(
% 0.36/0.49 rselect_head(queue_95)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1462,f1195])).
% 0.36/0.49 fof(f1462,plain,(
% 0.36/0.49 rselect_head(q22)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1443,f1458])).
% 0.36/0.49 fof(f1471,plain,(
% 0.36/0.49 index_93=s(index_87)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1474,f520])).
% 0.36/0.49 fof(f1474,plain,(
% 0.36/0.49 index_93=index_90),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f521,f1460])).
% 0.36/0.49 fof(f1476,plain,(
% 0.36/0.49 rselect_head(q23)=rselect_head(queue_95)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f672,f336])).
% 0.36/0.49 fof(f1478,plain,(
% 0.36/0.49 rselect_tail(q23)=index_96),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f672,f333])).
% 0.36/0.49 fof(f1479,plain,(
% 0.36/0.49 rselect_head(queue_101)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1480,f893])).
% 0.36/0.49 fof(f1480,plain,(
% 0.36/0.49 rselect_head(q23)=rselect_head(q10)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1461,f1476])).
% 0.36/0.49 fof(f1486,plain,(
% 0.36/0.49 index_99=s(index_93)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1489,f522])).
% 0.36/0.49 fof(f1489,plain,(
% 0.36/0.49 index_99=index_96),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f523,f1478])).
% 0.36/0.49 fof(f1495,plain,(
% 0.36/0.49 rselect_head(q24)=rselect_head(queue_101)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f673,f336])).
% 0.36/0.49 fof(f1497,plain,(
% 0.36/0.49 rselect_tail(q24)=index_102),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f673,f333])).
% 0.36/0.49 fof(f1498,plain,(
% 0.36/0.49 rselect_head(q24)=rselect_head(q10)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1495,f1479])).
% 0.36/0.49 fof(f1508,plain,(
% 0.36/0.49 index_105=s(index_99)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1510,f435])).
% 0.36/0.49 fof(f1510,plain,(
% 0.36/0.49 index_105=index_102),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f436,f1497])).
% 0.36/0.49 fof(f1536,plain,(
% 0.36/0.49 rselect_head(q24)=rselect_head(q9)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1498,f1228])).
% 0.36/0.49 fof(f1540,plain,(
% 0.36/0.49 rselect_head(q25)=rselect_head(queue_107)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f674,f336])).
% 0.36/0.49 fof(f1542,plain,(
% 0.36/0.49 rselect_tail(q25)=index_108),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f674,f333])).
% 0.36/0.49 fof(f1543,plain,(
% 0.36/0.49 rselect_head(queue_113)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1544,f910])).
% 0.36/0.49 fof(f1544,plain,(
% 0.36/0.49 rselect_head(q25)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f897,f1540])).
% 0.36/0.49 fof(f1552,plain,(
% 0.36/0.49 p(index_111)=index_105),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1556,f772])).
% 0.36/0.49 fof(f1556,plain,(
% 0.36/0.49 index_111=index_108),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f438,f1542])).
% 0.36/0.49 fof(f1558,plain,(
% 0.36/0.49 rselect_head(q26)=rselect_head(queue_113)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f675,f336])).
% 0.36/0.49 fof(f1560,plain,(
% 0.36/0.49 rselect_tail(q26)=index_114),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f675,f333])).
% 0.36/0.49 fof(f1561,plain,(
% 0.36/0.49 rselect_head(queue_119)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1562,f926])).
% 0.36/0.49 fof(f1562,plain,(
% 0.36/0.49 rselect_head(q26)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1543,f1558])).
% 0.36/0.49 fof(f1572,plain,(
% 0.36/0.49 index_117=s(index_111)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1574,f439])).
% 0.36/0.49 fof(f1574,plain,(
% 0.36/0.49 index_117=index_114),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f440,f1560])).
% 0.36/0.49 fof(f1576,plain,(
% 0.36/0.49 rselect_head(q27)=rselect_head(queue_119)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f676,f336])).
% 0.36/0.49 fof(f1578,plain,(
% 0.36/0.49 rselect_tail(q27)=index_120),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f676,f333])).
% 0.36/0.49 fof(f1579,plain,(
% 0.36/0.49 rselect_head(queue_125)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1580,f930])).
% 0.36/0.49 fof(f1580,plain,(
% 0.36/0.49 rselect_head(q27)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1561,f1576])).
% 0.36/0.49 fof(f1590,plain,(
% 0.36/0.49 index_123=s(index_117)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1592,f442])).
% 0.36/0.49 fof(f1592,plain,(
% 0.36/0.49 index_123=index_120),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f443,f1578])).
% 0.36/0.49 fof(f1594,plain,(
% 0.36/0.49 rselect_head(q28)=rselect_head(queue_125)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f677,f336])).
% 0.36/0.49 fof(f1596,plain,(
% 0.36/0.49 rselect_tail(q28)=index_126),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f677,f333])).
% 0.36/0.49 fof(f1597,plain,(
% 0.36/0.49 rselect_head(queue_131)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1598,f952])).
% 0.36/0.49 fof(f1598,plain,(
% 0.36/0.49 rselect_head(q28)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1579,f1594])).
% 0.36/0.49 fof(f1606,plain,(
% 0.36/0.49 p(index_129)=index_123),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1610,f792])).
% 0.36/0.49 fof(f1610,plain,(
% 0.36/0.49 index_129=index_126),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f445,f1596])).
% 0.36/0.49 fof(f1612,plain,(
% 0.36/0.49 rselect_head(q29)=rselect_head(queue_131)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f678,f336])).
% 0.36/0.49 fof(f1614,plain,(
% 0.36/0.49 rselect_tail(q29)=index_132),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f678,f333])).
% 0.36/0.49 fof(f1615,plain,(
% 0.36/0.49 rselect_head(queue_143)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1616,f960])).
% 0.36/0.49 fof(f1616,plain,(
% 0.36/0.49 rselect_head(q29)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1597,f1612])).
% 0.36/0.49 fof(f1626,plain,(
% 0.36/0.49 index_141=s(index_129)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1628,f446])).
% 0.36/0.49 fof(f1628,plain,(
% 0.36/0.49 index_141=index_132),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f449,f1614])).
% 0.36/0.49 fof(f1630,plain,(
% 0.36/0.49 rselect_head(q3)=rselect_head(queue_137)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f679,f336])).
% 0.36/0.49 fof(f1632,plain,(
% 0.36/0.49 rselect_tail(q3)=index_138),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f679,f333])).
% 0.36/0.49 fof(f1633,plain,(
% 0.36/0.49 rselect_head(queue_203)=index_3),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1634,f1076])).
% 0.36/0.49 fof(f1634,plain,(
% 0.36/0.49 rselect_head(q3)=index_3),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1406,f1630])).
% 0.36/0.49 fof(f1642,plain,(
% 0.36/0.49 p(index_201)=index_135),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1646,f804])).
% 0.36/0.49 fof(f1644,plain,(
% 0.36/0.49 index_201=s(index_135)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1646,f448])).
% 0.36/0.49 fof(f1646,plain,(
% 0.36/0.49 index_201=index_138),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f471,f1632])).
% 0.36/0.49 fof(f1648,plain,(
% 0.36/0.49 rselect_head(q30)=rselect_head(queue_143)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f680,f336])).
% 0.36/0.49 fof(f1650,plain,(
% 0.36/0.49 rselect_tail(q30)=index_144),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f680,f333])).
% 0.36/0.49 fof(f1651,plain,(
% 0.36/0.49 rselect_head(queue_149)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1652,f970])).
% 0.36/0.49 fof(f1652,plain,(
% 0.36/0.49 rselect_head(q30)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1615,f1648])).
% 0.36/0.49 fof(f1662,plain,(
% 0.36/0.49 index_147=s(index_141)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1664,f450])).
% 0.36/0.49 fof(f1664,plain,(
% 0.36/0.49 index_147=index_144),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f451,f1650])).
% 0.36/0.49 fof(f1666,plain,(
% 0.36/0.49 rselect_head(q31)=rselect_head(queue_149)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f681,f336])).
% 0.36/0.49 fof(f1668,plain,(
% 0.36/0.49 rselect_tail(q31)=index_150),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f681,f333])).
% 0.36/0.49 fof(f1669,plain,(
% 0.36/0.49 rselect_head(queue_155)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1670,f986])).
% 0.36/0.49 fof(f1670,plain,(
% 0.36/0.49 rselect_head(q31)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1651,f1666])).
% 0.36/0.49 fof(f1678,plain,(
% 0.36/0.49 p(index_153)=index_147),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1682,f812])).
% 0.36/0.49 fof(f1682,plain,(
% 0.36/0.49 index_153=index_150),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f454,f1668])).
% 0.36/0.49 fof(f1684,plain,(
% 0.36/0.49 rselect_head(q32)=rselect_head(queue_155)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f682,f336])).
% 0.36/0.49 fof(f1686,plain,(
% 0.36/0.49 rselect_tail(q32)=index_156),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f682,f333])).
% 0.36/0.49 fof(f1687,plain,(
% 0.36/0.49 rselect_head(queue_161)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1688,f990])).
% 0.36/0.49 fof(f1688,plain,(
% 0.36/0.49 rselect_head(q32)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1669,f1684])).
% 0.36/0.49 fof(f1698,plain,(
% 0.36/0.49 index_159=s(index_153)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1700,f455])).
% 0.36/0.49 fof(f1700,plain,(
% 0.36/0.49 index_159=index_156),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f456,f1686])).
% 0.36/0.49 fof(f1702,plain,(
% 0.36/0.49 rselect_head(q33)=rselect_head(queue_161)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f683,f336])).
% 0.36/0.49 fof(f1704,plain,(
% 0.36/0.49 rselect_tail(q33)=index_162),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f683,f333])).
% 0.36/0.49 fof(f1705,plain,(
% 0.36/0.49 rselect_head(queue_167)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1706,f1012])).
% 0.36/0.49 fof(f1706,plain,(
% 0.36/0.49 rselect_head(q33)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1687,f1702])).
% 0.36/0.49 fof(f1716,plain,(
% 0.36/0.49 index_165=s(index_159)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1718,f457])).
% 0.36/0.49 fof(f1718,plain,(
% 0.36/0.49 index_165=index_162),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f458,f1704])).
% 0.36/0.49 fof(f1720,plain,(
% 0.36/0.49 rselect_head(q34)=rselect_head(queue_167)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f684,f336])).
% 0.36/0.49 fof(f1722,plain,(
% 0.36/0.49 rselect_tail(q34)=index_168),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f684,f333])).
% 0.36/0.49 fof(f1723,plain,(
% 0.36/0.49 rselect_head(queue_173)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1724,f1020])).
% 0.36/0.49 fof(f1724,plain,(
% 0.36/0.49 rselect_head(q34)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1705,f1720])).
% 0.36/0.49 fof(f1732,plain,(
% 0.36/0.49 p(index_171)=index_165),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1736,f828])).
% 0.36/0.49 fof(f1736,plain,(
% 0.36/0.49 index_171=index_168),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f460,f1722])).
% 0.36/0.49 fof(f1738,plain,(
% 0.36/0.49 rselect_head(q35)=rselect_head(queue_173)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f685,f336])).
% 0.36/0.49 fof(f1740,plain,(
% 0.36/0.49 rselect_tail(q35)=index_174),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f685,f333])).
% 0.36/0.49 fof(f1741,plain,(
% 0.36/0.49 rselect_head(queue_179)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1742,f1030])).
% 0.36/0.49 fof(f1742,plain,(
% 0.36/0.49 rselect_head(q35)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1723,f1738])).
% 0.36/0.49 fof(f1752,plain,(
% 0.36/0.49 index_177=s(index_171)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1754,f461])).
% 0.36/0.49 fof(f1754,plain,(
% 0.36/0.49 index_177=index_174),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f462,f1740])).
% 0.36/0.49 fof(f1756,plain,(
% 0.36/0.49 rselect_head(q36)=rselect_head(queue_179)),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f686,f336])).
% 0.36/0.49 fof(f1758,plain,(
% 0.36/0.49 rselect_tail(q36)=index_180),
% 0.36/0.49 inference(paramodulation,[status(thm)],[f686,f333])).
% 0.36/0.49 fof(f1759,plain,(
% 0.36/0.49 rselect_head(queue_185)=rselect_head(q24)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1760,f1046])).
% 0.36/0.49 fof(f1760,plain,(
% 0.36/0.49 rselect_head(q36)=rselect_head(q24)),
% 0.36/0.49 inference(forward_demodulation,[status(thm)],[f1741,f1756])).
% 0.36/0.49 fof(f1770,plain,(
% 0.36/0.49 index_183=s(index_177)),
% 0.36/0.49 inference(backward_demodulation,[status(thm)],[f1772,f464])).
% 0.36/0.49 fof(f1772,plain,(
% 0.36/0.49 index_183=index_180),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f465,f1758])).
% 0.36/0.50 fof(f1774,plain,(
% 0.36/0.50 rselect_head(q37)=rselect_head(queue_185)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f687,f336])).
% 0.36/0.50 fof(f1776,plain,(
% 0.36/0.50 rselect_tail(q37)=index_186),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f687,f333])).
% 0.36/0.50 fof(f1777,plain,(
% 0.36/0.50 rselect_head(queue_191)=rselect_head(q24)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1778,f1050])).
% 0.36/0.50 fof(f1778,plain,(
% 0.36/0.50 rselect_head(q37)=rselect_head(q24)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1759,f1774])).
% 0.36/0.50 fof(f1786,plain,(
% 0.36/0.50 p(index_189)=index_183),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1790,f836])).
% 0.36/0.50 fof(f1790,plain,(
% 0.36/0.50 index_189=index_186),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f467,f1776])).
% 0.36/0.50 fof(f1792,plain,(
% 0.36/0.50 rselect_head(q38)=rselect_head(queue_191)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f688,f336])).
% 0.36/0.50 fof(f1794,plain,(
% 0.36/0.50 rselect_tail(q38)=index_192),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f688,f333])).
% 0.36/0.50 fof(f1795,plain,(
% 0.36/0.50 rselect_head(queue_197)=rselect_head(q24)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1796,f1072])).
% 0.36/0.50 fof(f1796,plain,(
% 0.36/0.50 rselect_head(q38)=rselect_head(q24)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1777,f1792])).
% 0.36/0.50 fof(f1805,plain,(
% 0.36/0.50 index_195=s(index_189)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1808,f468])).
% 0.36/0.50 fof(f1808,plain,(
% 0.36/0.50 index_195=index_192),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f469,f1794])).
% 0.36/0.50 fof(f1810,plain,(
% 0.36/0.50 rselect_head(q39)=rselect_head(queue_197)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f689,f336])).
% 0.36/0.50 fof(f1812,plain,(
% 0.36/0.50 rselect_tail(q39)=index_198),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f689,f333])).
% 0.36/0.50 fof(f1813,plain,(
% 0.36/0.50 rselect_head(queue_209)=rselect_head(q24)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1814,f1080])).
% 0.36/0.50 fof(f1814,plain,(
% 0.36/0.50 rselect_head(q39)=rselect_head(q24)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1795,f1810])).
% 0.36/0.50 fof(f1823,plain,(
% 0.36/0.50 index_207=s(index_195)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1826,f470])).
% 0.36/0.50 fof(f1826,plain,(
% 0.36/0.50 index_207=index_198),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f473,f1812])).
% 0.36/0.50 fof(f1828,plain,(
% 0.36/0.50 rselect_head(q4)=rselect_head(queue_203)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f690,f336])).
% 0.36/0.50 fof(f1830,plain,(
% 0.36/0.50 rselect_tail(q4)=index_204),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f690,f333])).
% 0.36/0.50 fof(f1831,plain,(
% 0.36/0.50 rselect_head(queue_233)=index_3),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1832,f1127])).
% 0.36/0.50 fof(f1832,plain,(
% 0.36/0.50 rselect_head(q4)=index_3),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1633,f1828])).
% 0.36/0.50 fof(f1839,plain,(
% 0.36/0.50 p(index_231)=index_201),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1844,f842])).
% 0.36/0.50 fof(f1841,plain,(
% 0.36/0.50 index_231=s(index_201)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1844,f472])).
% 0.36/0.50 fof(f1844,plain,(
% 0.36/0.50 index_231=index_204),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f482,f1830])).
% 0.36/0.50 fof(f1846,plain,(
% 0.36/0.50 rselect_head(q40)=rselect_head(queue_209)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f691,f336])).
% 0.36/0.50 fof(f1848,plain,(
% 0.36/0.50 rselect_tail(q40)=index_210),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f691,f333])).
% 0.36/0.50 fof(f1849,plain,(
% 0.36/0.50 rselect_head(queue_215)=rselect_head(q24)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1850,f1090])).
% 0.36/0.50 fof(f1850,plain,(
% 0.36/0.50 rselect_head(q40)=rselect_head(q24)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1813,f1846])).
% 0.36/0.50 fof(f1857,plain,(
% 0.36/0.50 p(index_213)=index_207),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1862,f844])).
% 0.36/0.50 fof(f1862,plain,(
% 0.36/0.50 index_213=index_210),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f476,f1848])).
% 0.36/0.50 fof(f1864,plain,(
% 0.36/0.50 rselect_head(q41)=rselect_head(queue_215)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f692,f336])).
% 0.36/0.50 fof(f1866,plain,(
% 0.36/0.50 rselect_tail(q41)=index_216),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f692,f333])).
% 0.36/0.50 fof(f1867,plain,(
% 0.36/0.50 rselect_head(queue_221)=rselect_head(q24)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1868,f1106])).
% 0.36/0.50 fof(f1868,plain,(
% 0.36/0.50 rselect_head(q41)=rselect_head(q24)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1849,f1864])).
% 0.36/0.50 fof(f1877,plain,(
% 0.36/0.50 index_219=s(index_213)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1880,f477])).
% 0.36/0.50 fof(f1880,plain,(
% 0.36/0.50 index_219=index_216),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f478,f1866])).
% 0.36/0.50 fof(f1882,plain,(
% 0.36/0.50 rselect_head(q42)=rselect_head(queue_221)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f693,f336])).
% 0.36/0.50 fof(f1884,plain,(
% 0.36/0.50 rselect_tail(q42)=index_222),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f693,f333])).
% 0.36/0.50 fof(f1885,plain,(
% 0.36/0.50 rselect_head(queue_227)=rselect_head(q24)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1886,f1110])).
% 0.36/0.50 fof(f1886,plain,(
% 0.36/0.50 rselect_head(q42)=rselect_head(q24)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1867,f1882])).
% 0.36/0.50 fof(f1895,plain,(
% 0.36/0.50 index_225=s(index_219)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1898,f479])).
% 0.36/0.50 fof(f1898,plain,(
% 0.36/0.50 index_225=index_222),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f480,f1884])).
% 0.36/0.50 fof(f1900,plain,(
% 0.36/0.50 rselect_head(q43)=rselect_head(queue_227)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f694,f336])).
% 0.36/0.50 fof(f1901,plain,(
% 0.36/0.50 rselect_seq(q43)=rselect_seq(queue_227)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f694,f335])).
% 0.36/0.50 fof(f1902,plain,(
% 0.36/0.50 rselect_tail(q43)=index_228),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f694,f333])).
% 0.36/0.50 fof(f1903,plain,(
% 0.36/0.50 index_261=rselect_head(q24)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1904,f1885])).
% 0.36/0.50 fof(f1904,plain,(
% 0.36/0.50 index_261=rselect_head(queue_227)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f493,f1900])).
% 0.36/0.50 fof(f1905,plain,(
% 0.36/0.50 earray_260=rselect_seq(queue_227)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f405,f1901])).
% 0.36/0.50 fof(f1907,plain,(
% 0.36/0.50 elem_265=select(earray_226,index_264)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1909,f433])).
% 0.36/0.50 fof(f1908,plain,(
% 0.36/0.50 elem_262=select(earray_226,index_261)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1909,f432])).
% 0.36/0.50 fof(f1909,plain,(
% 0.36/0.50 earray_260=earray_226),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1111,f1905])).
% 0.36/0.50 fof(f1910,plain,(
% 0.36/0.50 index_263=index_228),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1902,f494])).
% 0.36/0.50 fof(f1948,plain,(
% 0.36/0.50 index_261=rselect_head(q9)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1903,f1536])).
% 0.36/0.50 fof(f1977,plain,(
% 0.36/0.50 p(index_228)=index_264),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1910,f864])).
% 0.36/0.50 fof(f1981,plain,(
% 0.36/0.50 elem_265=select(earray_226,index_225)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1982,f1907])).
% 0.36/0.50 fof(f1982,plain,(
% 0.36/0.50 index_225=index_264),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f850,f1977])).
% 0.36/0.50 fof(f1986,plain,(
% 0.36/0.50 ~elem_262=e42),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1987,f655])).
% 0.36/0.50 fof(f1987,plain,(
% 0.36/0.50 elem_265=e42),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f767,f1981])).
% 0.36/0.50 fof(f1988,plain,(
% 0.36/0.50 rselect_head(q5)=rselect_head(queue_233)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f695,f336])).
% 0.36/0.50 fof(f1990,plain,(
% 0.36/0.50 rselect_tail(q5)=index_234),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f695,f333])).
% 0.36/0.50 fof(f1991,plain,(
% 0.36/0.50 rselect_head(queue_239)=index_3),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f1992,f1131])).
% 0.36/0.50 fof(f1992,plain,(
% 0.36/0.50 rselect_head(q5)=index_3),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1831,f1988])).
% 0.36/0.50 fof(f2001,plain,(
% 0.36/0.50 index_237=s(index_231)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2004,f483])).
% 0.36/0.50 fof(f2004,plain,(
% 0.36/0.50 index_237=index_234),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f484,f1990])).
% 0.36/0.50 fof(f2006,plain,(
% 0.36/0.50 rselect_head(q6)=rselect_head(queue_239)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f696,f336])).
% 0.36/0.50 fof(f2008,plain,(
% 0.36/0.50 rselect_tail(q6)=index_240),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f696,f333])).
% 0.36/0.50 fof(f2009,plain,(
% 0.36/0.50 rselect_head(queue_245)=index_3),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2010,f1135])).
% 0.36/0.50 fof(f2010,plain,(
% 0.36/0.50 rselect_head(q6)=index_3),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1991,f2006])).
% 0.36/0.50 fof(f2017,plain,(
% 0.36/0.50 p(index_243)=index_237),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2022,f856])).
% 0.36/0.50 fof(f2019,plain,(
% 0.36/0.50 index_243=s(index_237)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2022,f486])).
% 0.36/0.50 fof(f2022,plain,(
% 0.36/0.50 index_243=index_240),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f487,f2008])).
% 0.36/0.50 fof(f2024,plain,(
% 0.36/0.50 rselect_head(q7)=rselect_head(queue_245)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f697,f336])).
% 0.36/0.50 fof(f2026,plain,(
% 0.36/0.50 rselect_tail(q7)=index_246),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f697,f333])).
% 0.36/0.50 fof(f2027,plain,(
% 0.36/0.50 rselect_head(queue_251)=index_3),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2028,f1139])).
% 0.36/0.50 fof(f2028,plain,(
% 0.36/0.50 rselect_head(q7)=index_3),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2009,f2024])).
% 0.36/0.50 fof(f2037,plain,(
% 0.36/0.50 index_249=s(index_243)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2040,f488])).
% 0.36/0.50 fof(f2040,plain,(
% 0.36/0.50 index_249=index_246),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f489,f2026])).
% 0.36/0.50 fof(f2042,plain,(
% 0.36/0.50 rselect_head(q8)=rselect_head(queue_251)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f698,f336])).
% 0.36/0.50 fof(f2044,plain,(
% 0.36/0.50 rselect_tail(q8)=index_252),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f698,f333])).
% 0.36/0.50 fof(f2045,plain,(
% 0.36/0.50 rselect_head(queue_257)=index_3),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2046,f1143])).
% 0.36/0.50 fof(f2046,plain,(
% 0.36/0.50 rselect_head(q8)=index_3),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2027,f2042])).
% 0.36/0.50 fof(f2055,plain,(
% 0.36/0.50 index_255=s(index_249)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2058,f490])).
% 0.36/0.50 fof(f2058,plain,(
% 0.36/0.50 index_255=index_252),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f491,f2044])).
% 0.36/0.50 fof(f2060,plain,(
% 0.36/0.50 rselect_head(q9)=rselect_head(queue_257)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f699,f336])).
% 0.36/0.50 fof(f2062,plain,(
% 0.36/0.50 rselect_tail(q9)=index_258),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f699,f333])).
% 0.36/0.50 fof(f2063,plain,(
% 0.36/0.50 index_261=rselect_head(queue_257)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1948,f2060])).
% 0.36/0.50 fof(f2064,plain,(
% 0.36/0.50 elem_262=select(earray_226,index_3)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2134,f1908])).
% 0.36/0.50 fof(f2134,plain,(
% 0.36/0.50 index_261=index_3),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2045,f2063])).
% 0.36/0.50 fof(f2140,plain,(
% 0.36/0.50 index_9=s(index_255)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2143,f492])).
% 0.36/0.50 fof(f2143,plain,(
% 0.36/0.50 index_9=index_258),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f519,f2062])).
% 0.36/0.50 fof(f2708,plain,(
% 0.36/0.50 s(index_249)=p(index_243)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f2037,f708])).
% 0.36/0.50 fof(f2710,plain,(
% 0.36/0.50 s(index_237)=p(index_231)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f2001,f708])).
% 0.36/0.50 fof(f2712,plain,(
% 0.36/0.50 s(index_219)=p(index_213)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1877,f708])).
% 0.36/0.50 fof(f2714,plain,(
% 0.36/0.50 s(index_231)=p(index_201)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1841,f708])).
% 0.36/0.50 fof(f2716,plain,(
% 0.36/0.50 s(index_195)=p(index_189)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1805,f708])).
% 0.36/0.50 fof(f2719,plain,(
% 0.36/0.50 s(index_177)=p(index_171)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1752,f708])).
% 0.36/0.50 fof(f2722,plain,(
% 0.36/0.50 s(index_159)=p(index_153)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1698,f708])).
% 0.36/0.50 fof(f2726,plain,(
% 0.36/0.50 s(index_141)=p(index_129)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1626,f708])).
% 0.36/0.50 fof(f2729,plain,(
% 0.36/0.50 s(index_117)=p(index_111)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1572,f708])).
% 0.36/0.50 fof(f2732,plain,(
% 0.36/0.50 s(index_99)=p(index_93)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1486,f708])).
% 0.36/0.50 fof(f2734,plain,(
% 0.36/0.50 s(index_87)=p(index_81)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1453,f708])).
% 0.36/0.50 fof(f2736,plain,(
% 0.36/0.50 s(index_135)=p(index_69)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1414,f708])).
% 0.36/0.50 fof(f2738,plain,(
% 0.36/0.50 s(index_63)=p(index_57)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1380,f708])).
% 0.36/0.50 fof(f2741,plain,(
% 0.36/0.50 s(index_45)=p(index_39)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1326,f708])).
% 0.36/0.50 fof(f2744,plain,(
% 0.36/0.50 s(index_27)=p(index_21)),
% 0.36/0.50 inference(paramodulation,[status(thm)],[f1272,f708])).
% 0.36/0.50 fof(f2757,plain,(
% 0.36/0.50 index_255=p(index_243)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2055,f2708])).
% 0.36/0.50 fof(f2759,plain,(
% 0.36/0.50 index_9=s(index_237)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2773,f2140])).
% 0.36/0.50 fof(f2773,plain,(
% 0.36/0.50 index_255=index_237),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2017,f2757])).
% 0.36/0.50 fof(f2788,plain,(
% 0.36/0.50 index_243=p(index_231)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2019,f2710])).
% 0.36/0.50 fof(f2791,plain,(
% 0.36/0.50 index_201=s(index_237)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2800,f2019])).
% 0.36/0.50 fof(f2800,plain,(
% 0.36/0.50 index_243=index_201),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1839,f2788])).
% 0.36/0.50 fof(f2811,plain,(
% 0.36/0.50 index_225=p(index_213)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1895,f2712])).
% 0.36/0.50 fof(f2823,plain,(
% 0.36/0.50 select(earray_226,index_207)=e42),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f2824,f767])).
% 0.36/0.50 fof(f2824,plain,(
% 0.36/0.50 index_225=index_207),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1857,f2811])).
% 0.36/0.50 fof(f2838,plain,(
% 0.36/0.50 index_237=p(index_201)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2001,f2714])).
% 0.36/0.50 fof(f2851,plain,(
% 0.36/0.50 index_237=index_135),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1642,f2838])).
% 0.36/0.50 fof(f2866,plain,(
% 0.36/0.50 index_207=p(index_189)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1823,f2716])).
% 0.36/0.50 fof(f2879,plain,(
% 0.36/0.50 index_207=index_183),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1786,f2866])).
% 0.36/0.50 fof(f2908,plain,(
% 0.36/0.50 index_183=p(index_171)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1770,f2719])).
% 0.36/0.50 fof(f2921,plain,(
% 0.36/0.50 index_183=index_165),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1732,f2908])).
% 0.36/0.50 fof(f2950,plain,(
% 0.36/0.50 index_165=p(index_153)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1716,f2722])).
% 0.36/0.50 fof(f2963,plain,(
% 0.36/0.50 index_165=index_147),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1678,f2950])).
% 0.36/0.50 fof(f2994,plain,(
% 0.36/0.50 index_147=p(index_129)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1662,f2726])).
% 0.36/0.50 fof(f3007,plain,(
% 0.36/0.50 index_147=index_123),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1606,f2994])).
% 0.36/0.50 fof(f3036,plain,(
% 0.36/0.50 index_123=p(index_111)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1590,f2729])).
% 0.36/0.50 fof(f3049,plain,(
% 0.36/0.50 index_123=index_105),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1552,f3036])).
% 0.36/0.50 fof(f3067,plain,(
% 0.36/0.50 index_105=p(index_93)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1508,f2732])).
% 0.36/0.50 fof(f3070,plain,(
% 0.36/0.50 index_93=p(index_81)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1471,f2734])).
% 0.36/0.50 fof(f3082,plain,(
% 0.36/0.50 index_105=p(index_75)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f3085,f3067])).
% 0.36/0.50 fof(f3085,plain,(
% 0.36/0.50 index_93=index_75),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1433,f3070])).
% 0.36/0.50 fof(f3100,plain,(
% 0.36/0.50 index_201=index_3),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f3101,f1219])).
% 0.36/0.50 fof(f3101,plain,(
% 0.36/0.50 index_201=p(index_69)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1644,f2736])).
% 0.36/0.50 fof(f3115,plain,(
% 0.36/0.50 index_75=p(index_57)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1398,f2738])).
% 0.36/0.50 fof(f3128,plain,(
% 0.36/0.50 index_75=index_51),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1360,f3115])).
% 0.36/0.50 fof(f3157,plain,(
% 0.36/0.50 index_51=p(index_39)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1344,f2741])).
% 0.36/0.50 fof(f3170,plain,(
% 0.36/0.50 index_51=index_33),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1306,f3157])).
% 0.36/0.50 fof(f3199,plain,(
% 0.36/0.50 index_33=p(index_21)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1290,f2744])).
% 0.36/0.50 fof(f3212,plain,(
% 0.36/0.50 index_33=index_15),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1253,f3199])).
% 0.36/0.50 fof(f3247,plain,(
% 0.36/0.50 index_9=s(index_135)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2851,f2759])).
% 0.36/0.50 fof(f3305,plain,(
% 0.36/0.50 index_201=s(index_135)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2851,f2791])).
% 0.36/0.50 fof(f3319,plain,(
% 0.36/0.50 index_201=index_9),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f3247,f3305])).
% 0.36/0.50 fof(f3455,plain,(
% 0.36/0.50 select(earray_226,index_183)=e42),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2879,f2823])).
% 0.36/0.50 fof(f3456,plain,(
% 0.36/0.50 select(earray_226,index_165)=e42),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2921,f3455])).
% 0.36/0.50 fof(f3457,plain,(
% 0.36/0.50 select(earray_226,index_147)=e42),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f2963,f3456])).
% 0.36/0.50 fof(f3458,plain,(
% 0.36/0.50 select(earray_226,index_123)=e42),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f3007,f3457])).
% 0.36/0.50 fof(f3459,plain,(
% 0.36/0.50 select(earray_226,index_105)=e42),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f3049,f3458])).
% 0.36/0.50 fof(f3995,plain,(
% 0.36/0.50 index_105=p(index_51)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f3128,f3082])).
% 0.36/0.50 fof(f3996,plain,(
% 0.36/0.50 index_105=p(index_33)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f3170,f3995])).
% 0.36/0.50 fof(f3997,plain,(
% 0.36/0.50 index_105=p(index_15)),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f3212,f3996])).
% 0.36/0.50 fof(f4049,plain,(
% 0.36/0.50 select(earray_226,index_9)=e42),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f4061,f3459])).
% 0.36/0.50 fof(f4061,plain,(
% 0.36/0.50 index_105=index_9),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f1236,f3997])).
% 0.36/0.50 fof(f4144,plain,(
% 0.36/0.50 elem_262=select(earray_226,index_9)),
% 0.36/0.50 inference(backward_demodulation,[status(thm)],[f4211,f2064])).
% 0.36/0.50 fof(f4211,plain,(
% 0.36/0.50 index_9=index_3),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f3319,f3100])).
% 0.36/0.50 fof(f4524,plain,(
% 0.36/0.50 elem_262=e42),
% 0.36/0.50 inference(forward_demodulation,[status(thm)],[f4049,f4144])).
% 0.36/0.50 fof(f4525,plain,(
% 0.36/0.50 $false),
% 0.36/0.50 inference(forward_subsumption_resolution,[status(thm)],[f4524,f1986])).
% 0.36/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.36/0.50 % Elapsed time: 0.093002 seconds
% 0.36/0.50 % CPU time: 0.485787 seconds
% 0.36/0.50 % Total memory used: 79.359 MB
% 0.36/0.50 % Net memory used: 79.232 MB
%------------------------------------------------------------------------------