%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV571-1.046 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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 2.91s 1.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV571-1.046 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.93 % Computer : n006.cluster.edu
% 0.11/0.93 % Model : x86_64 x86_64
% 0.11/0.93 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.93 % Memory : 8046.5625MB
% 0.11/0.93 % OS : Linux 6.8.0-71-generic
% 0.11/0.93 % CPULimit : 300
% 0.11/0.93 % WCLimit : 300
% 0.11/0.93 % DateTime : Mon Sep 21 09:11:15 UTC 2026
% 0.11/0.93 % CPUTime :
% 0.11/0.95 % Drodi V4.1.1
% 2.91/1.40 % Refutation found
% 2.91/1.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.91/1.40 % SZS output start CNFRefutation for theBenchmark
% 2.91/1.40 fof(f1,axiom,(
% 2.91/1.40 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f2,axiom,(
% 2.91/1.40 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f3,axiom,(
% 2.91/1.40 head != tail ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f4,axiom,(
% 2.91/1.40 head != seq ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f6,axiom,(
% 2.91/1.40 (![X]: (p(s(X)) = X ))),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f7,axiom,(
% 2.91/1.40 (![X]: (s(p(X)) = X ))),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f10,axiom,(
% 2.91/1.40 (![X]: (s(s(s(X))) = X ))),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f104,hypothesis,(
% 2.91/1.40 elem_280 = select(earray_278,index_279) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f105,hypothesis,(
% 2.91/1.40 elem_283 = select(earray_278,index_282) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f106,hypothesis,(
% 2.91/1.40 index_0 = select(q,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f107,hypothesis,(
% 2.91/1.40 index_102 = s(index_99) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f108,hypothesis,(
% 2.91/1.40 index_105 = select(q24,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f109,hypothesis,(
% 2.91/1.40 index_108 = s(index_105) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f110,hypothesis,(
% 2.91/1.40 index_111 = select(q25,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f111,hypothesis,(
% 2.91/1.40 index_114 = s(index_111) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f112,hypothesis,(
% 2.91/1.40 index_117 = select(q26,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f113,hypothesis,(
% 2.91/1.40 index_12 = s(index_9) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f114,hypothesis,(
% 2.91/1.40 index_120 = s(index_117) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f115,hypothesis,(
% 2.91/1.40 index_123 = select(q27,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f116,hypothesis,(
% 2.91/1.40 index_126 = s(index_123) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f117,hypothesis,(
% 2.91/1.40 index_129 = select(q28,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f118,hypothesis,(
% 2.91/1.40 index_132 = s(index_129) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f119,hypothesis,(
% 2.91/1.40 index_135 = select(q2,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f120,hypothesis,(
% 2.91/1.40 index_138 = s(index_135) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f121,hypothesis,(
% 2.91/1.40 index_141 = select(q29,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f122,hypothesis,(
% 2.91/1.40 index_144 = s(index_141) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f123,hypothesis,(
% 2.91/1.40 index_147 = select(q30,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f124,hypothesis,(
% 2.91/1.40 index_15 = select(q10,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f125,hypothesis,(
% 2.91/1.40 index_150 = s(index_147) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f126,hypothesis,(
% 2.91/1.40 index_153 = select(q31,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f127,hypothesis,(
% 2.91/1.40 index_156 = s(index_153) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f128,hypothesis,(
% 2.91/1.40 index_159 = select(q32,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f129,hypothesis,(
% 2.91/1.40 index_162 = s(index_159) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f130,hypothesis,(
% 2.91/1.40 index_165 = select(q33,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f131,hypothesis,(
% 2.91/1.40 index_168 = s(index_165) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f132,hypothesis,(
% 2.91/1.40 index_171 = select(q34,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f133,hypothesis,(
% 2.91/1.40 index_174 = s(index_171) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f134,hypothesis,(
% 2.91/1.40 index_177 = select(q35,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f135,hypothesis,(
% 2.91/1.40 index_18 = s(index_15) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f136,hypothesis,(
% 2.91/1.40 index_180 = s(index_177) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f137,hypothesis,(
% 2.91/1.40 index_183 = select(q36,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f138,hypothesis,(
% 2.91/1.40 index_186 = s(index_183) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f139,hypothesis,(
% 2.91/1.40 index_189 = select(q37,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f140,hypothesis,(
% 2.91/1.40 index_192 = s(index_189) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f141,hypothesis,(
% 2.91/1.40 index_195 = select(q38,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f142,hypothesis,(
% 2.91/1.40 index_198 = s(index_195) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f143,hypothesis,(
% 2.91/1.40 index_201 = select(q3,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f144,hypothesis,(
% 2.91/1.40 index_204 = s(index_201) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f145,hypothesis,(
% 2.91/1.40 index_207 = select(q39,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f146,hypothesis,(
% 2.91/1.40 index_21 = select(q11,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f147,hypothesis,(
% 2.91/1.40 index_210 = s(index_207) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f148,hypothesis,(
% 2.91/1.40 index_213 = select(q40,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f149,hypothesis,(
% 2.91/1.40 index_216 = s(index_213) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f150,hypothesis,(
% 2.91/1.40 index_219 = select(q41,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f151,hypothesis,(
% 2.91/1.40 index_222 = s(index_219) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f152,hypothesis,(
% 2.91/1.40 index_225 = select(q42,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f153,hypothesis,(
% 2.91/1.40 index_228 = s(index_225) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f154,hypothesis,(
% 2.91/1.40 index_231 = select(q43,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f155,hypothesis,(
% 2.91/1.40 index_234 = s(index_231) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f156,hypothesis,(
% 2.91/1.40 index_237 = select(q44,tail) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.40 fof(f157,hypothesis,(
% 2.91/1.40 index_24 = s(index_21) ),
% 2.91/1.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f158,hypothesis,(
% 2.91/1.41 index_240 = s(index_237) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f159,hypothesis,(
% 2.91/1.41 index_243 = select(q45,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f160,hypothesis,(
% 2.91/1.41 index_246 = s(index_243) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f161,hypothesis,(
% 2.91/1.41 index_249 = select(q4,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f162,hypothesis,(
% 2.91/1.41 index_252 = s(index_249) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f163,hypothesis,(
% 2.91/1.41 index_255 = select(q5,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f164,hypothesis,(
% 2.91/1.41 index_258 = s(index_255) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f165,hypothesis,(
% 2.91/1.41 index_261 = select(q6,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f166,hypothesis,(
% 2.91/1.41 index_264 = s(index_261) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f167,hypothesis,(
% 2.91/1.41 index_267 = select(q7,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f168,hypothesis,(
% 2.91/1.41 index_27 = select(q12,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f169,hypothesis,(
% 2.91/1.41 index_270 = s(index_267) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f170,hypothesis,(
% 2.91/1.41 index_273 = select(q8,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f171,hypothesis,(
% 2.91/1.41 index_276 = s(index_273) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f172,hypothesis,(
% 2.91/1.41 index_279 = select(q46,head) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f173,hypothesis,(
% 2.91/1.41 index_281 = select(q46,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f174,hypothesis,(
% 2.91/1.41 s(index_282) = index_281 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f175,hypothesis,(
% 2.91/1.41 index_3 = select(q0,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f176,hypothesis,(
% 2.91/1.41 index_30 = s(index_27) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f177,hypothesis,(
% 2.91/1.41 index_33 = select(q13,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f178,hypothesis,(
% 2.91/1.41 index_36 = s(index_33) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f179,hypothesis,(
% 2.91/1.41 index_39 = select(q14,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f180,hypothesis,(
% 2.91/1.41 index_42 = s(index_39) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f181,hypothesis,(
% 2.91/1.41 index_45 = select(q15,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f182,hypothesis,(
% 2.91/1.41 index_48 = s(index_45) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f183,hypothesis,(
% 2.91/1.41 index_51 = select(q16,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f184,hypothesis,(
% 2.91/1.41 index_54 = s(index_51) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f185,hypothesis,(
% 2.91/1.41 index_57 = select(q17,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f186,hypothesis,(
% 2.91/1.41 index_6 = s(index_3) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f187,hypothesis,(
% 2.91/1.41 index_60 = s(index_57) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f188,hypothesis,(
% 2.91/1.41 index_63 = select(q18,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f189,hypothesis,(
% 2.91/1.41 index_66 = s(index_63) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f190,hypothesis,(
% 2.91/1.41 index_69 = select(q1,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f191,hypothesis,(
% 2.91/1.41 index_72 = s(index_69) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f192,hypothesis,(
% 2.91/1.41 index_75 = select(q19,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f193,hypothesis,(
% 2.91/1.41 index_78 = s(index_75) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f194,hypothesis,(
% 2.91/1.41 index_81 = select(q20,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f195,hypothesis,(
% 2.91/1.41 index_84 = s(index_81) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f196,hypothesis,(
% 2.91/1.41 index_87 = select(q21,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f197,hypothesis,(
% 2.91/1.41 index_9 = select(q9,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f198,hypothesis,(
% 2.91/1.41 index_90 = s(index_87) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f199,hypothesis,(
% 2.91/1.41 index_93 = select(q22,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f200,hypothesis,(
% 2.91/1.41 index_96 = s(index_93) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f201,hypothesis,(
% 2.91/1.41 index_99 = select(q23,tail) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f202,hypothesis,(
% 2.91/1.41 queue_1 = store(q,head,index_0) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f203,hypothesis,(
% 2.91/1.41 queue_101 = store(q23,seq,earray_100) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f204,hypothesis,(
% 2.91/1.41 queue_103 = store(queue_101,tail,index_102) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f205,hypothesis,(
% 2.91/1.41 queue_107 = store(q24,seq,earray_106) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f206,hypothesis,(
% 2.91/1.41 queue_109 = store(queue_107,tail,index_108) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f207,hypothesis,(
% 2.91/1.41 queue_11 = store(q9,seq,earray_10) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f208,hypothesis,(
% 2.91/1.41 queue_113 = store(q25,seq,earray_112) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f209,hypothesis,(
% 2.91/1.41 queue_115 = store(queue_113,tail,index_114) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f210,hypothesis,(
% 2.91/1.41 queue_119 = store(q26,seq,earray_118) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f211,hypothesis,(
% 2.91/1.41 queue_121 = store(queue_119,tail,index_120) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f212,hypothesis,(
% 2.91/1.41 queue_125 = store(q27,seq,earray_124) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f213,hypothesis,(
% 2.91/1.41 queue_127 = store(queue_125,tail,index_126) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f214,hypothesis,(
% 2.91/1.41 queue_13 = store(queue_11,tail,index_12) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f215,hypothesis,(
% 2.91/1.41 queue_131 = store(q28,seq,earray_130) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f216,hypothesis,(
% 2.91/1.41 queue_133 = store(queue_131,tail,index_132) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f217,hypothesis,(
% 2.91/1.41 queue_137 = store(q2,seq,earray_136) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f218,hypothesis,(
% 2.91/1.41 queue_139 = store(queue_137,tail,index_138) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f219,hypothesis,(
% 2.91/1.41 queue_143 = store(q29,seq,earray_142) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f220,hypothesis,(
% 2.91/1.41 queue_145 = store(queue_143,tail,index_144) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f221,hypothesis,(
% 2.91/1.41 queue_149 = store(q30,seq,earray_148) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f222,hypothesis,(
% 2.91/1.41 queue_151 = store(queue_149,tail,index_150) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f223,hypothesis,(
% 2.91/1.41 queue_155 = store(q31,seq,earray_154) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f224,hypothesis,(
% 2.91/1.41 queue_157 = store(queue_155,tail,index_156) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f225,hypothesis,(
% 2.91/1.41 queue_161 = store(q32,seq,earray_160) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f226,hypothesis,(
% 2.91/1.41 queue_163 = store(queue_161,tail,index_162) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f227,hypothesis,(
% 2.91/1.41 queue_167 = store(q33,seq,earray_166) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f228,hypothesis,(
% 2.91/1.41 queue_169 = store(queue_167,tail,index_168) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f229,hypothesis,(
% 2.91/1.41 queue_17 = store(q10,seq,earray_16) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f230,hypothesis,(
% 2.91/1.41 queue_173 = store(q34,seq,earray_172) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f231,hypothesis,(
% 2.91/1.41 queue_175 = store(queue_173,tail,index_174) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f232,hypothesis,(
% 2.91/1.41 queue_179 = store(q35,seq,earray_178) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f233,hypothesis,(
% 2.91/1.41 queue_181 = store(queue_179,tail,index_180) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f234,hypothesis,(
% 2.91/1.41 queue_185 = store(q36,seq,earray_184) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f235,hypothesis,(
% 2.91/1.41 queue_187 = store(queue_185,tail,index_186) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f236,hypothesis,(
% 2.91/1.41 queue_19 = store(queue_17,tail,index_18) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f237,hypothesis,(
% 2.91/1.41 queue_191 = store(q37,seq,earray_190) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f238,hypothesis,(
% 2.91/1.41 queue_193 = store(queue_191,tail,index_192) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f239,hypothesis,(
% 2.91/1.41 queue_197 = store(q38,seq,earray_196) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f240,hypothesis,(
% 2.91/1.41 queue_199 = store(queue_197,tail,index_198) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f241,hypothesis,(
% 2.91/1.41 queue_203 = store(q3,seq,earray_202) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f242,hypothesis,(
% 2.91/1.41 queue_205 = store(queue_203,tail,index_204) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f243,hypothesis,(
% 2.91/1.41 queue_209 = store(q39,seq,earray_208) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f244,hypothesis,(
% 2.91/1.41 queue_211 = store(queue_209,tail,index_210) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f245,hypothesis,(
% 2.91/1.41 queue_215 = store(q40,seq,earray_214) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f246,hypothesis,(
% 2.91/1.41 queue_217 = store(queue_215,tail,index_216) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f247,hypothesis,(
% 2.91/1.41 queue_221 = store(q41,seq,earray_220) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f248,hypothesis,(
% 2.91/1.41 queue_223 = store(queue_221,tail,index_222) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f249,hypothesis,(
% 2.91/1.41 queue_227 = store(q42,seq,earray_226) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f250,hypothesis,(
% 2.91/1.41 queue_229 = store(queue_227,tail,index_228) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f251,hypothesis,(
% 2.91/1.41 queue_23 = store(q11,seq,earray_22) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f252,hypothesis,(
% 2.91/1.41 queue_233 = store(q43,seq,earray_232) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f253,hypothesis,(
% 2.91/1.41 queue_235 = store(queue_233,tail,index_234) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f254,hypothesis,(
% 2.91/1.41 queue_239 = store(q44,seq,earray_238) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f255,hypothesis,(
% 2.91/1.41 queue_241 = store(queue_239,tail,index_240) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f256,hypothesis,(
% 2.91/1.41 queue_245 = store(q45,seq,earray_244) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f257,hypothesis,(
% 2.91/1.41 queue_247 = store(queue_245,tail,index_246) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f258,hypothesis,(
% 2.91/1.41 queue_25 = store(queue_23,tail,index_24) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f259,hypothesis,(
% 2.91/1.41 queue_251 = store(q4,seq,earray_250) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f260,hypothesis,(
% 2.91/1.41 queue_253 = store(queue_251,tail,index_252) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f261,hypothesis,(
% 2.91/1.41 queue_257 = store(q5,seq,earray_256) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f262,hypothesis,(
% 2.91/1.41 queue_259 = store(queue_257,tail,index_258) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f263,hypothesis,(
% 2.91/1.41 queue_263 = store(q6,seq,earray_262) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f264,hypothesis,(
% 2.91/1.41 queue_265 = store(queue_263,tail,index_264) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f265,hypothesis,(
% 2.91/1.41 queue_269 = store(q7,seq,earray_268) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f266,hypothesis,(
% 2.91/1.41 queue_271 = store(queue_269,tail,index_270) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f267,hypothesis,(
% 2.91/1.41 queue_275 = store(q8,seq,earray_274) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f268,hypothesis,(
% 2.91/1.41 queue_277 = store(queue_275,tail,index_276) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f269,hypothesis,(
% 2.91/1.41 queue_29 = store(q12,seq,earray_28) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f270,hypothesis,(
% 2.91/1.41 queue_31 = store(queue_29,tail,index_30) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f271,hypothesis,(
% 2.91/1.41 queue_35 = store(q13,seq,earray_34) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f272,hypothesis,(
% 2.91/1.41 queue_37 = store(queue_35,tail,index_36) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f273,hypothesis,(
% 2.91/1.41 queue_41 = store(q14,seq,earray_40) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f274,hypothesis,(
% 2.91/1.41 queue_43 = store(queue_41,tail,index_42) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f275,hypothesis,(
% 2.91/1.41 queue_47 = store(q15,seq,earray_46) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f276,hypothesis,(
% 2.91/1.41 queue_49 = store(queue_47,tail,index_48) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f277,hypothesis,(
% 2.91/1.41 queue_5 = store(q0,seq,earray_4) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f278,hypothesis,(
% 2.91/1.41 queue_53 = store(q16,seq,earray_52) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f279,hypothesis,(
% 2.91/1.41 queue_55 = store(queue_53,tail,index_54) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f280,hypothesis,(
% 2.91/1.41 queue_59 = store(q17,seq,earray_58) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f281,hypothesis,(
% 2.91/1.41 queue_61 = store(queue_59,tail,index_60) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f282,hypothesis,(
% 2.91/1.41 queue_65 = store(q18,seq,earray_64) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f283,hypothesis,(
% 2.91/1.41 queue_67 = store(queue_65,tail,index_66) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f284,hypothesis,(
% 2.91/1.41 queue_7 = store(queue_5,tail,index_6) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f285,hypothesis,(
% 2.91/1.41 queue_71 = store(q1,seq,earray_70) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f286,hypothesis,(
% 2.91/1.41 queue_73 = store(queue_71,tail,index_72) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f287,hypothesis,(
% 2.91/1.41 queue_77 = store(q19,seq,earray_76) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f288,hypothesis,(
% 2.91/1.41 queue_79 = store(queue_77,tail,index_78) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f289,hypothesis,(
% 2.91/1.41 queue_83 = store(q20,seq,earray_82) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f290,hypothesis,(
% 2.91/1.41 queue_85 = store(queue_83,tail,index_84) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f291,hypothesis,(
% 2.91/1.41 queue_89 = store(q21,seq,earray_88) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f292,hypothesis,(
% 2.91/1.41 queue_91 = store(queue_89,tail,index_90) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f293,hypothesis,(
% 2.91/1.41 queue_95 = store(q22,seq,earray_94) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f294,hypothesis,(
% 2.91/1.41 queue_97 = store(queue_95,tail,index_96) ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f295,hypothesis,(
% 2.91/1.41 q0 = queue_1 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f296,hypothesis,(
% 2.91/1.41 q1 = queue_7 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f297,hypothesis,(
% 2.91/1.41 q10 = queue_13 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f298,hypothesis,(
% 2.91/1.41 q11 = queue_19 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f299,hypothesis,(
% 2.91/1.41 q12 = queue_25 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f300,hypothesis,(
% 2.91/1.41 q13 = queue_31 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f301,hypothesis,(
% 2.91/1.41 q14 = queue_37 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f302,hypothesis,(
% 2.91/1.41 q15 = queue_43 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f303,hypothesis,(
% 2.91/1.41 q16 = queue_49 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f304,hypothesis,(
% 2.91/1.41 q17 = queue_55 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f305,hypothesis,(
% 2.91/1.41 q18 = queue_61 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f306,hypothesis,(
% 2.91/1.41 q19 = queue_67 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f307,hypothesis,(
% 2.91/1.41 q2 = queue_73 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f308,hypothesis,(
% 2.91/1.41 q20 = queue_79 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f309,hypothesis,(
% 2.91/1.41 q21 = queue_85 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f310,hypothesis,(
% 2.91/1.41 q22 = queue_91 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f311,hypothesis,(
% 2.91/1.41 q23 = queue_97 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f312,hypothesis,(
% 2.91/1.41 q24 = queue_103 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f313,hypothesis,(
% 2.91/1.41 q25 = queue_109 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f314,hypothesis,(
% 2.91/1.41 q26 = queue_115 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f315,hypothesis,(
% 2.91/1.41 q27 = queue_121 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f316,hypothesis,(
% 2.91/1.41 q28 = queue_127 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f317,hypothesis,(
% 2.91/1.41 q29 = queue_133 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f318,hypothesis,(
% 2.91/1.41 q3 = queue_139 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f319,hypothesis,(
% 2.91/1.41 q30 = queue_145 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f320,hypothesis,(
% 2.91/1.41 q31 = queue_151 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f321,hypothesis,(
% 2.91/1.41 q32 = queue_157 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f322,hypothesis,(
% 2.91/1.41 q33 = queue_163 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f323,hypothesis,(
% 2.91/1.41 q34 = queue_169 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f324,hypothesis,(
% 2.91/1.41 q35 = queue_175 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f325,hypothesis,(
% 2.91/1.41 q36 = queue_181 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f326,hypothesis,(
% 2.91/1.41 q37 = queue_187 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f327,hypothesis,(
% 2.91/1.41 q38 = queue_193 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f328,hypothesis,(
% 2.91/1.41 q39 = queue_199 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f329,hypothesis,(
% 2.91/1.41 q4 = queue_205 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f330,hypothesis,(
% 2.91/1.41 q40 = queue_211 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f331,hypothesis,(
% 2.91/1.41 q41 = queue_217 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f332,hypothesis,(
% 2.91/1.41 q42 = queue_223 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f333,hypothesis,(
% 2.91/1.41 q43 = queue_229 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f334,hypothesis,(
% 2.91/1.41 q44 = queue_235 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f335,hypothesis,(
% 2.91/1.41 q45 = queue_241 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f336,hypothesis,(
% 2.91/1.41 q46 = queue_247 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f337,hypothesis,(
% 2.91/1.41 q5 = queue_253 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f338,hypothesis,(
% 2.91/1.41 q6 = queue_259 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f339,hypothesis,(
% 2.91/1.41 q7 = queue_265 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f340,hypothesis,(
% 2.91/1.41 q8 = queue_271 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f341,hypothesis,(
% 2.91/1.41 q9 = queue_277 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f342,negated_conjecture,(
% 2.91/1.41 elem_280 != elem_283 ),
% 2.91/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.91/1.41 fof(f343,plain,(
% 2.91/1.41 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f1])).
% 2.91/1.41 fof(f344,plain,(
% 2.91/1.41 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 2.91/1.41 inference(miniscoping,[status(thm)],[f2])).
% 2.91/1.41 fof(f345,plain,(
% 2.91/1.41 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f344])).
% 2.91/1.41 fof(f346,plain,(
% 2.91/1.41 ~head=tail),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f3])).
% 2.91/1.41 fof(f347,plain,(
% 2.91/1.41 ~head=seq),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f4])).
% 2.91/1.41 fof(f349,plain,(
% 2.91/1.41 ![X0]: (p(s(X0))=X0)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f6])).
% 2.91/1.41 fof(f350,plain,(
% 2.91/1.41 ![X0]: (s(p(X0))=X0)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f7])).
% 2.91/1.41 fof(f353,plain,(
% 2.91/1.41 ![X0]: (s(s(s(X0)))=X0)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f10])).
% 2.91/1.41 fof(f447,plain,(
% 2.91/1.41 elem_280=select(earray_278,index_279)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f104])).
% 2.91/1.41 fof(f448,plain,(
% 2.91/1.41 elem_283=select(earray_278,index_282)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f105])).
% 2.91/1.41 fof(f449,plain,(
% 2.91/1.41 index_0=select(q,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f106])).
% 2.91/1.41 fof(f450,plain,(
% 2.91/1.41 index_102=s(index_99)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f107])).
% 2.91/1.41 fof(f451,plain,(
% 2.91/1.41 index_105=select(q24,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f108])).
% 2.91/1.41 fof(f452,plain,(
% 2.91/1.41 index_108=s(index_105)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f109])).
% 2.91/1.41 fof(f453,plain,(
% 2.91/1.41 index_111=select(q25,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f110])).
% 2.91/1.41 fof(f454,plain,(
% 2.91/1.41 index_114=s(index_111)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f111])).
% 2.91/1.41 fof(f455,plain,(
% 2.91/1.41 index_117=select(q26,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f112])).
% 2.91/1.41 fof(f456,plain,(
% 2.91/1.41 index_12=s(index_9)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f113])).
% 2.91/1.41 fof(f457,plain,(
% 2.91/1.41 index_120=s(index_117)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f114])).
% 2.91/1.41 fof(f458,plain,(
% 2.91/1.41 index_123=select(q27,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f115])).
% 2.91/1.41 fof(f459,plain,(
% 2.91/1.41 index_126=s(index_123)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f116])).
% 2.91/1.41 fof(f460,plain,(
% 2.91/1.41 index_129=select(q28,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f117])).
% 2.91/1.41 fof(f461,plain,(
% 2.91/1.41 index_132=s(index_129)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f118])).
% 2.91/1.41 fof(f462,plain,(
% 2.91/1.41 index_135=select(q2,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f119])).
% 2.91/1.41 fof(f463,plain,(
% 2.91/1.41 index_138=s(index_135)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f120])).
% 2.91/1.41 fof(f464,plain,(
% 2.91/1.41 index_141=select(q29,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f121])).
% 2.91/1.41 fof(f465,plain,(
% 2.91/1.41 index_144=s(index_141)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f122])).
% 2.91/1.41 fof(f466,plain,(
% 2.91/1.41 index_147=select(q30,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f123])).
% 2.91/1.41 fof(f467,plain,(
% 2.91/1.41 index_15=select(q10,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f124])).
% 2.91/1.41 fof(f468,plain,(
% 2.91/1.41 index_150=s(index_147)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f125])).
% 2.91/1.41 fof(f469,plain,(
% 2.91/1.41 index_153=select(q31,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f126])).
% 2.91/1.41 fof(f470,plain,(
% 2.91/1.41 index_156=s(index_153)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f127])).
% 2.91/1.41 fof(f471,plain,(
% 2.91/1.41 index_159=select(q32,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f128])).
% 2.91/1.41 fof(f472,plain,(
% 2.91/1.41 index_162=s(index_159)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f129])).
% 2.91/1.41 fof(f473,plain,(
% 2.91/1.41 index_165=select(q33,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f130])).
% 2.91/1.41 fof(f474,plain,(
% 2.91/1.41 index_168=s(index_165)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f131])).
% 2.91/1.41 fof(f475,plain,(
% 2.91/1.41 index_171=select(q34,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f132])).
% 2.91/1.41 fof(f476,plain,(
% 2.91/1.41 index_174=s(index_171)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f133])).
% 2.91/1.41 fof(f477,plain,(
% 2.91/1.41 index_177=select(q35,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f134])).
% 2.91/1.41 fof(f478,plain,(
% 2.91/1.41 index_18=s(index_15)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f135])).
% 2.91/1.41 fof(f479,plain,(
% 2.91/1.41 index_180=s(index_177)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f136])).
% 2.91/1.41 fof(f480,plain,(
% 2.91/1.41 index_183=select(q36,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f137])).
% 2.91/1.41 fof(f481,plain,(
% 2.91/1.41 index_186=s(index_183)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f138])).
% 2.91/1.41 fof(f482,plain,(
% 2.91/1.41 index_189=select(q37,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f139])).
% 2.91/1.41 fof(f483,plain,(
% 2.91/1.41 index_192=s(index_189)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f140])).
% 2.91/1.41 fof(f484,plain,(
% 2.91/1.41 index_195=select(q38,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f141])).
% 2.91/1.41 fof(f485,plain,(
% 2.91/1.41 index_198=s(index_195)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f142])).
% 2.91/1.41 fof(f486,plain,(
% 2.91/1.41 index_201=select(q3,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f143])).
% 2.91/1.41 fof(f487,plain,(
% 2.91/1.41 index_204=s(index_201)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f144])).
% 2.91/1.41 fof(f488,plain,(
% 2.91/1.41 index_207=select(q39,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f145])).
% 2.91/1.41 fof(f489,plain,(
% 2.91/1.41 index_21=select(q11,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f146])).
% 2.91/1.41 fof(f490,plain,(
% 2.91/1.41 index_210=s(index_207)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f147])).
% 2.91/1.41 fof(f491,plain,(
% 2.91/1.41 index_213=select(q40,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f148])).
% 2.91/1.41 fof(f492,plain,(
% 2.91/1.41 index_216=s(index_213)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f149])).
% 2.91/1.41 fof(f493,plain,(
% 2.91/1.41 index_219=select(q41,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f150])).
% 2.91/1.41 fof(f494,plain,(
% 2.91/1.41 index_222=s(index_219)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f151])).
% 2.91/1.41 fof(f495,plain,(
% 2.91/1.41 index_225=select(q42,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f152])).
% 2.91/1.41 fof(f496,plain,(
% 2.91/1.41 index_228=s(index_225)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f153])).
% 2.91/1.41 fof(f497,plain,(
% 2.91/1.41 index_231=select(q43,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f154])).
% 2.91/1.41 fof(f498,plain,(
% 2.91/1.41 index_234=s(index_231)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f155])).
% 2.91/1.41 fof(f499,plain,(
% 2.91/1.41 index_237=select(q44,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f156])).
% 2.91/1.41 fof(f500,plain,(
% 2.91/1.41 index_24=s(index_21)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f157])).
% 2.91/1.41 fof(f501,plain,(
% 2.91/1.41 index_240=s(index_237)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f158])).
% 2.91/1.41 fof(f502,plain,(
% 2.91/1.41 index_243=select(q45,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f159])).
% 2.91/1.41 fof(f503,plain,(
% 2.91/1.41 index_246=s(index_243)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f160])).
% 2.91/1.41 fof(f504,plain,(
% 2.91/1.41 index_249=select(q4,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f161])).
% 2.91/1.41 fof(f505,plain,(
% 2.91/1.41 index_252=s(index_249)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f162])).
% 2.91/1.41 fof(f506,plain,(
% 2.91/1.41 index_255=select(q5,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f163])).
% 2.91/1.41 fof(f507,plain,(
% 2.91/1.41 index_258=s(index_255)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f164])).
% 2.91/1.41 fof(f508,plain,(
% 2.91/1.41 index_261=select(q6,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f165])).
% 2.91/1.41 fof(f509,plain,(
% 2.91/1.41 index_264=s(index_261)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f166])).
% 2.91/1.41 fof(f510,plain,(
% 2.91/1.41 index_267=select(q7,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f167])).
% 2.91/1.41 fof(f511,plain,(
% 2.91/1.41 index_27=select(q12,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f168])).
% 2.91/1.41 fof(f512,plain,(
% 2.91/1.41 index_270=s(index_267)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f169])).
% 2.91/1.41 fof(f513,plain,(
% 2.91/1.41 index_273=select(q8,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f170])).
% 2.91/1.41 fof(f514,plain,(
% 2.91/1.41 index_276=s(index_273)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f171])).
% 2.91/1.41 fof(f515,plain,(
% 2.91/1.41 index_279=select(q46,head)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f172])).
% 2.91/1.41 fof(f516,plain,(
% 2.91/1.41 index_281=select(q46,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f173])).
% 2.91/1.41 fof(f517,plain,(
% 2.91/1.41 s(index_282)=index_281),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f174])).
% 2.91/1.41 fof(f518,plain,(
% 2.91/1.41 index_3=select(q0,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f175])).
% 2.91/1.41 fof(f519,plain,(
% 2.91/1.41 index_30=s(index_27)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f176])).
% 2.91/1.41 fof(f520,plain,(
% 2.91/1.41 index_33=select(q13,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f177])).
% 2.91/1.41 fof(f521,plain,(
% 2.91/1.41 index_36=s(index_33)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f178])).
% 2.91/1.41 fof(f522,plain,(
% 2.91/1.41 index_39=select(q14,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f179])).
% 2.91/1.41 fof(f523,plain,(
% 2.91/1.41 index_42=s(index_39)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f180])).
% 2.91/1.41 fof(f524,plain,(
% 2.91/1.41 index_45=select(q15,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f181])).
% 2.91/1.41 fof(f525,plain,(
% 2.91/1.41 index_48=s(index_45)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f182])).
% 2.91/1.41 fof(f526,plain,(
% 2.91/1.41 index_51=select(q16,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f183])).
% 2.91/1.41 fof(f527,plain,(
% 2.91/1.41 index_54=s(index_51)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f184])).
% 2.91/1.41 fof(f528,plain,(
% 2.91/1.41 index_57=select(q17,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f185])).
% 2.91/1.41 fof(f529,plain,(
% 2.91/1.41 index_6=s(index_3)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f186])).
% 2.91/1.41 fof(f530,plain,(
% 2.91/1.41 index_60=s(index_57)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f187])).
% 2.91/1.41 fof(f531,plain,(
% 2.91/1.41 index_63=select(q18,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f188])).
% 2.91/1.41 fof(f532,plain,(
% 2.91/1.41 index_66=s(index_63)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f189])).
% 2.91/1.41 fof(f533,plain,(
% 2.91/1.41 index_69=select(q1,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f190])).
% 2.91/1.41 fof(f534,plain,(
% 2.91/1.41 index_72=s(index_69)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f191])).
% 2.91/1.41 fof(f535,plain,(
% 2.91/1.41 index_75=select(q19,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f192])).
% 2.91/1.41 fof(f536,plain,(
% 2.91/1.41 index_78=s(index_75)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f193])).
% 2.91/1.41 fof(f537,plain,(
% 2.91/1.41 index_81=select(q20,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f194])).
% 2.91/1.41 fof(f538,plain,(
% 2.91/1.41 index_84=s(index_81)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f195])).
% 2.91/1.41 fof(f539,plain,(
% 2.91/1.41 index_87=select(q21,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f196])).
% 2.91/1.41 fof(f540,plain,(
% 2.91/1.41 index_9=select(q9,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f197])).
% 2.91/1.41 fof(f541,plain,(
% 2.91/1.41 index_90=s(index_87)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f198])).
% 2.91/1.41 fof(f542,plain,(
% 2.91/1.41 index_93=select(q22,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f199])).
% 2.91/1.41 fof(f543,plain,(
% 2.91/1.41 index_96=s(index_93)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f200])).
% 2.91/1.41 fof(f544,plain,(
% 2.91/1.41 index_99=select(q23,tail)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f201])).
% 2.91/1.41 fof(f545,plain,(
% 2.91/1.41 queue_1=store(q,head,index_0)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f202])).
% 2.91/1.41 fof(f546,plain,(
% 2.91/1.41 queue_101=store(q23,seq,earray_100)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f203])).
% 2.91/1.41 fof(f547,plain,(
% 2.91/1.41 queue_103=store(queue_101,tail,index_102)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f204])).
% 2.91/1.41 fof(f548,plain,(
% 2.91/1.41 queue_107=store(q24,seq,earray_106)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f205])).
% 2.91/1.41 fof(f549,plain,(
% 2.91/1.41 queue_109=store(queue_107,tail,index_108)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f206])).
% 2.91/1.41 fof(f550,plain,(
% 2.91/1.41 queue_11=store(q9,seq,earray_10)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f207])).
% 2.91/1.41 fof(f551,plain,(
% 2.91/1.41 queue_113=store(q25,seq,earray_112)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f208])).
% 2.91/1.41 fof(f552,plain,(
% 2.91/1.41 queue_115=store(queue_113,tail,index_114)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f209])).
% 2.91/1.41 fof(f553,plain,(
% 2.91/1.41 queue_119=store(q26,seq,earray_118)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f210])).
% 2.91/1.41 fof(f554,plain,(
% 2.91/1.41 queue_121=store(queue_119,tail,index_120)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f211])).
% 2.91/1.41 fof(f555,plain,(
% 2.91/1.41 queue_125=store(q27,seq,earray_124)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f212])).
% 2.91/1.41 fof(f556,plain,(
% 2.91/1.41 queue_127=store(queue_125,tail,index_126)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f213])).
% 2.91/1.41 fof(f557,plain,(
% 2.91/1.41 queue_13=store(queue_11,tail,index_12)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f214])).
% 2.91/1.41 fof(f558,plain,(
% 2.91/1.41 queue_131=store(q28,seq,earray_130)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f215])).
% 2.91/1.41 fof(f559,plain,(
% 2.91/1.41 queue_133=store(queue_131,tail,index_132)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f216])).
% 2.91/1.41 fof(f560,plain,(
% 2.91/1.41 queue_137=store(q2,seq,earray_136)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f217])).
% 2.91/1.41 fof(f561,plain,(
% 2.91/1.41 queue_139=store(queue_137,tail,index_138)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f218])).
% 2.91/1.41 fof(f562,plain,(
% 2.91/1.41 queue_143=store(q29,seq,earray_142)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f219])).
% 2.91/1.41 fof(f563,plain,(
% 2.91/1.41 queue_145=store(queue_143,tail,index_144)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f220])).
% 2.91/1.41 fof(f564,plain,(
% 2.91/1.41 queue_149=store(q30,seq,earray_148)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f221])).
% 2.91/1.41 fof(f565,plain,(
% 2.91/1.41 queue_151=store(queue_149,tail,index_150)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f222])).
% 2.91/1.41 fof(f566,plain,(
% 2.91/1.41 queue_155=store(q31,seq,earray_154)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f223])).
% 2.91/1.41 fof(f567,plain,(
% 2.91/1.41 queue_157=store(queue_155,tail,index_156)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f224])).
% 2.91/1.41 fof(f568,plain,(
% 2.91/1.41 queue_161=store(q32,seq,earray_160)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f225])).
% 2.91/1.41 fof(f569,plain,(
% 2.91/1.41 queue_163=store(queue_161,tail,index_162)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f226])).
% 2.91/1.41 fof(f570,plain,(
% 2.91/1.41 queue_167=store(q33,seq,earray_166)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f227])).
% 2.91/1.41 fof(f571,plain,(
% 2.91/1.41 queue_169=store(queue_167,tail,index_168)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f228])).
% 2.91/1.41 fof(f572,plain,(
% 2.91/1.41 queue_17=store(q10,seq,earray_16)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f229])).
% 2.91/1.41 fof(f573,plain,(
% 2.91/1.41 queue_173=store(q34,seq,earray_172)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f230])).
% 2.91/1.41 fof(f574,plain,(
% 2.91/1.41 queue_175=store(queue_173,tail,index_174)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f231])).
% 2.91/1.41 fof(f575,plain,(
% 2.91/1.41 queue_179=store(q35,seq,earray_178)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f232])).
% 2.91/1.41 fof(f576,plain,(
% 2.91/1.41 queue_181=store(queue_179,tail,index_180)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f233])).
% 2.91/1.41 fof(f577,plain,(
% 2.91/1.41 queue_185=store(q36,seq,earray_184)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f234])).
% 2.91/1.41 fof(f578,plain,(
% 2.91/1.41 queue_187=store(queue_185,tail,index_186)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f235])).
% 2.91/1.41 fof(f579,plain,(
% 2.91/1.41 queue_19=store(queue_17,tail,index_18)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f236])).
% 2.91/1.41 fof(f580,plain,(
% 2.91/1.41 queue_191=store(q37,seq,earray_190)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f237])).
% 2.91/1.41 fof(f581,plain,(
% 2.91/1.41 queue_193=store(queue_191,tail,index_192)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f238])).
% 2.91/1.41 fof(f582,plain,(
% 2.91/1.41 queue_197=store(q38,seq,earray_196)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f239])).
% 2.91/1.41 fof(f583,plain,(
% 2.91/1.41 queue_199=store(queue_197,tail,index_198)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f240])).
% 2.91/1.41 fof(f584,plain,(
% 2.91/1.41 queue_203=store(q3,seq,earray_202)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f241])).
% 2.91/1.41 fof(f585,plain,(
% 2.91/1.41 queue_205=store(queue_203,tail,index_204)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f242])).
% 2.91/1.41 fof(f586,plain,(
% 2.91/1.41 queue_209=store(q39,seq,earray_208)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f243])).
% 2.91/1.41 fof(f587,plain,(
% 2.91/1.41 queue_211=store(queue_209,tail,index_210)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f244])).
% 2.91/1.41 fof(f588,plain,(
% 2.91/1.41 queue_215=store(q40,seq,earray_214)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f245])).
% 2.91/1.41 fof(f589,plain,(
% 2.91/1.41 queue_217=store(queue_215,tail,index_216)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f246])).
% 2.91/1.41 fof(f590,plain,(
% 2.91/1.41 queue_221=store(q41,seq,earray_220)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f247])).
% 2.91/1.41 fof(f591,plain,(
% 2.91/1.41 queue_223=store(queue_221,tail,index_222)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f248])).
% 2.91/1.41 fof(f592,plain,(
% 2.91/1.41 queue_227=store(q42,seq,earray_226)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f249])).
% 2.91/1.41 fof(f593,plain,(
% 2.91/1.41 queue_229=store(queue_227,tail,index_228)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f250])).
% 2.91/1.41 fof(f594,plain,(
% 2.91/1.41 queue_23=store(q11,seq,earray_22)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f251])).
% 2.91/1.41 fof(f595,plain,(
% 2.91/1.41 queue_233=store(q43,seq,earray_232)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f252])).
% 2.91/1.41 fof(f596,plain,(
% 2.91/1.41 queue_235=store(queue_233,tail,index_234)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f253])).
% 2.91/1.41 fof(f597,plain,(
% 2.91/1.41 queue_239=store(q44,seq,earray_238)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f254])).
% 2.91/1.41 fof(f598,plain,(
% 2.91/1.41 queue_241=store(queue_239,tail,index_240)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f255])).
% 2.91/1.41 fof(f599,plain,(
% 2.91/1.41 queue_245=store(q45,seq,earray_244)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f256])).
% 2.91/1.41 fof(f600,plain,(
% 2.91/1.41 queue_247=store(queue_245,tail,index_246)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f257])).
% 2.91/1.41 fof(f601,plain,(
% 2.91/1.41 queue_25=store(queue_23,tail,index_24)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f258])).
% 2.91/1.41 fof(f602,plain,(
% 2.91/1.41 queue_251=store(q4,seq,earray_250)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f259])).
% 2.91/1.41 fof(f603,plain,(
% 2.91/1.41 queue_253=store(queue_251,tail,index_252)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f260])).
% 2.91/1.41 fof(f604,plain,(
% 2.91/1.41 queue_257=store(q5,seq,earray_256)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f261])).
% 2.91/1.41 fof(f605,plain,(
% 2.91/1.41 queue_259=store(queue_257,tail,index_258)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f262])).
% 2.91/1.41 fof(f606,plain,(
% 2.91/1.41 queue_263=store(q6,seq,earray_262)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f263])).
% 2.91/1.41 fof(f607,plain,(
% 2.91/1.41 queue_265=store(queue_263,tail,index_264)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f264])).
% 2.91/1.41 fof(f608,plain,(
% 2.91/1.41 queue_269=store(q7,seq,earray_268)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f265])).
% 2.91/1.41 fof(f609,plain,(
% 2.91/1.41 queue_271=store(queue_269,tail,index_270)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f266])).
% 2.91/1.41 fof(f610,plain,(
% 2.91/1.41 queue_275=store(q8,seq,earray_274)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f267])).
% 2.91/1.41 fof(f611,plain,(
% 2.91/1.41 queue_277=store(queue_275,tail,index_276)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f268])).
% 2.91/1.41 fof(f612,plain,(
% 2.91/1.41 queue_29=store(q12,seq,earray_28)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f269])).
% 2.91/1.41 fof(f613,plain,(
% 2.91/1.41 queue_31=store(queue_29,tail,index_30)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f270])).
% 2.91/1.41 fof(f614,plain,(
% 2.91/1.41 queue_35=store(q13,seq,earray_34)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f271])).
% 2.91/1.41 fof(f615,plain,(
% 2.91/1.41 queue_37=store(queue_35,tail,index_36)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f272])).
% 2.91/1.41 fof(f616,plain,(
% 2.91/1.41 queue_41=store(q14,seq,earray_40)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f273])).
% 2.91/1.41 fof(f617,plain,(
% 2.91/1.41 queue_43=store(queue_41,tail,index_42)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f274])).
% 2.91/1.41 fof(f618,plain,(
% 2.91/1.41 queue_47=store(q15,seq,earray_46)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f275])).
% 2.91/1.41 fof(f619,plain,(
% 2.91/1.41 queue_49=store(queue_47,tail,index_48)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f276])).
% 2.91/1.41 fof(f620,plain,(
% 2.91/1.41 queue_5=store(q0,seq,earray_4)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f277])).
% 2.91/1.41 fof(f621,plain,(
% 2.91/1.41 queue_53=store(q16,seq,earray_52)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f278])).
% 2.91/1.41 fof(f622,plain,(
% 2.91/1.41 queue_55=store(queue_53,tail,index_54)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f279])).
% 2.91/1.41 fof(f623,plain,(
% 2.91/1.41 queue_59=store(q17,seq,earray_58)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f280])).
% 2.91/1.41 fof(f624,plain,(
% 2.91/1.41 queue_61=store(queue_59,tail,index_60)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f281])).
% 2.91/1.41 fof(f625,plain,(
% 2.91/1.41 queue_65=store(q18,seq,earray_64)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f282])).
% 2.91/1.41 fof(f626,plain,(
% 2.91/1.41 queue_67=store(queue_65,tail,index_66)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f283])).
% 2.91/1.41 fof(f627,plain,(
% 2.91/1.41 queue_7=store(queue_5,tail,index_6)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f284])).
% 2.91/1.41 fof(f628,plain,(
% 2.91/1.41 queue_71=store(q1,seq,earray_70)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f285])).
% 2.91/1.41 fof(f629,plain,(
% 2.91/1.41 queue_73=store(queue_71,tail,index_72)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f286])).
% 2.91/1.41 fof(f630,plain,(
% 2.91/1.41 queue_77=store(q19,seq,earray_76)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f287])).
% 2.91/1.41 fof(f631,plain,(
% 2.91/1.41 queue_79=store(queue_77,tail,index_78)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f288])).
% 2.91/1.41 fof(f632,plain,(
% 2.91/1.41 queue_83=store(q20,seq,earray_82)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f289])).
% 2.91/1.41 fof(f633,plain,(
% 2.91/1.41 queue_85=store(queue_83,tail,index_84)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f290])).
% 2.91/1.41 fof(f634,plain,(
% 2.91/1.41 queue_89=store(q21,seq,earray_88)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f291])).
% 2.91/1.41 fof(f635,plain,(
% 2.91/1.41 queue_91=store(queue_89,tail,index_90)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f292])).
% 2.91/1.41 fof(f636,plain,(
% 2.91/1.41 queue_95=store(q22,seq,earray_94)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f293])).
% 2.91/1.41 fof(f637,plain,(
% 2.91/1.41 queue_97=store(queue_95,tail,index_96)),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f294])).
% 2.91/1.41 fof(f638,plain,(
% 2.91/1.41 q0=queue_1),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f295])).
% 2.91/1.41 fof(f639,plain,(
% 2.91/1.41 q1=queue_7),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f296])).
% 2.91/1.41 fof(f640,plain,(
% 2.91/1.41 q10=queue_13),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f297])).
% 2.91/1.41 fof(f641,plain,(
% 2.91/1.41 q11=queue_19),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f298])).
% 2.91/1.41 fof(f642,plain,(
% 2.91/1.41 q12=queue_25),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f299])).
% 2.91/1.41 fof(f643,plain,(
% 2.91/1.41 q13=queue_31),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f300])).
% 2.91/1.41 fof(f644,plain,(
% 2.91/1.41 q14=queue_37),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f301])).
% 2.91/1.41 fof(f645,plain,(
% 2.91/1.41 q15=queue_43),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f302])).
% 2.91/1.41 fof(f646,plain,(
% 2.91/1.41 q16=queue_49),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f303])).
% 2.91/1.41 fof(f647,plain,(
% 2.91/1.41 q17=queue_55),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f304])).
% 2.91/1.41 fof(f648,plain,(
% 2.91/1.41 q18=queue_61),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f305])).
% 2.91/1.41 fof(f649,plain,(
% 2.91/1.41 q19=queue_67),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f306])).
% 2.91/1.41 fof(f650,plain,(
% 2.91/1.41 q2=queue_73),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f307])).
% 2.91/1.41 fof(f651,plain,(
% 2.91/1.41 q20=queue_79),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f308])).
% 2.91/1.41 fof(f652,plain,(
% 2.91/1.41 q21=queue_85),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f309])).
% 2.91/1.41 fof(f653,plain,(
% 2.91/1.41 q22=queue_91),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f310])).
% 2.91/1.41 fof(f654,plain,(
% 2.91/1.41 q23=queue_97),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f311])).
% 2.91/1.41 fof(f655,plain,(
% 2.91/1.41 q24=queue_103),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f312])).
% 2.91/1.41 fof(f656,plain,(
% 2.91/1.41 q25=queue_109),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f313])).
% 2.91/1.41 fof(f657,plain,(
% 2.91/1.41 q26=queue_115),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f314])).
% 2.91/1.41 fof(f658,plain,(
% 2.91/1.41 q27=queue_121),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f315])).
% 2.91/1.41 fof(f659,plain,(
% 2.91/1.41 q28=queue_127),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f316])).
% 2.91/1.41 fof(f660,plain,(
% 2.91/1.41 q29=queue_133),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f317])).
% 2.91/1.41 fof(f661,plain,(
% 2.91/1.41 q3=queue_139),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f318])).
% 2.91/1.41 fof(f662,plain,(
% 2.91/1.41 q30=queue_145),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f319])).
% 2.91/1.41 fof(f663,plain,(
% 2.91/1.41 q31=queue_151),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f320])).
% 2.91/1.41 fof(f664,plain,(
% 2.91/1.41 q32=queue_157),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f321])).
% 2.91/1.41 fof(f665,plain,(
% 2.91/1.41 q33=queue_163),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f322])).
% 2.91/1.41 fof(f666,plain,(
% 2.91/1.41 q34=queue_169),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f323])).
% 2.91/1.41 fof(f667,plain,(
% 2.91/1.41 q35=queue_175),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f324])).
% 2.91/1.41 fof(f668,plain,(
% 2.91/1.41 q36=queue_181),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f325])).
% 2.91/1.41 fof(f669,plain,(
% 2.91/1.41 q37=queue_187),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f326])).
% 2.91/1.41 fof(f670,plain,(
% 2.91/1.41 q38=queue_193),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f327])).
% 2.91/1.41 fof(f671,plain,(
% 2.91/1.41 q39=queue_199),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f328])).
% 2.91/1.41 fof(f672,plain,(
% 2.91/1.41 q4=queue_205),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f329])).
% 2.91/1.41 fof(f673,plain,(
% 2.91/1.41 q40=queue_211),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f330])).
% 2.91/1.41 fof(f674,plain,(
% 2.91/1.41 q41=queue_217),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f331])).
% 2.91/1.41 fof(f675,plain,(
% 2.91/1.41 q42=queue_223),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f332])).
% 2.91/1.41 fof(f676,plain,(
% 2.91/1.41 q43=queue_229),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f333])).
% 2.91/1.41 fof(f677,plain,(
% 2.91/1.41 q44=queue_235),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f334])).
% 2.91/1.41 fof(f678,plain,(
% 2.91/1.41 q45=queue_241),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f335])).
% 2.91/1.41 fof(f679,plain,(
% 2.91/1.41 q46=queue_247),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f336])).
% 2.91/1.41 fof(f680,plain,(
% 2.91/1.41 q5=queue_253),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f337])).
% 2.91/1.41 fof(f681,plain,(
% 2.91/1.41 q6=queue_259),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f338])).
% 2.91/1.41 fof(f682,plain,(
% 2.91/1.41 q7=queue_265),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f339])).
% 2.91/1.41 fof(f683,plain,(
% 2.91/1.41 q8=queue_271),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f340])).
% 2.91/1.41 fof(f684,plain,(
% 2.91/1.41 q9=queue_277),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f341])).
% 2.91/1.41 fof(f685,plain,(
% 2.91/1.41 ~elem_280=elem_283),
% 2.91/1.41 inference(cnf_transformation,[status(thm)],[f342])).
% 2.91/1.41 fof(f694,plain,(
% 2.91/1.41 ![X0]: (s(s(X0))=p(X0))),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f350,f353])).
% 2.91/1.41 fof(f706,plain,(
% 2.91/1.41 p(index_102)=index_99),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f450,f349])).
% 2.91/1.41 fof(f710,plain,(
% 2.91/1.41 p(index_108)=index_105),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f452,f349])).
% 2.91/1.41 fof(f718,plain,(
% 2.91/1.41 p(index_12)=index_9),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f456,f349])).
% 2.91/1.41 fof(f770,plain,(
% 2.91/1.41 p(index_180)=index_177),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f479,f349])).
% 2.91/1.41 fof(f848,plain,(
% 2.91/1.41 p(index_281)=index_282),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f517,f349])).
% 2.91/1.41 fof(f852,plain,(
% 2.91/1.41 p(index_30)=index_27),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f519,f349])).
% 2.91/1.41 fof(f878,plain,(
% 2.91/1.41 p(index_60)=index_57),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f530,f349])).
% 2.91/1.41 fof(f1098,plain,(
% 2.91/1.41 s(index_84)=p(index_81)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f538,f694])).
% 2.91/1.41 fof(f1101,plain,(
% 2.91/1.41 s(index_66)=p(index_63)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f532,f694])).
% 2.91/1.41 fof(f1103,plain,(
% 2.91/1.41 s(index_6)=p(index_3)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f529,f694])).
% 2.91/1.41 fof(f1107,plain,(
% 2.91/1.41 s(index_36)=p(index_33)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f521,f694])).
% 2.91/1.41 fof(f1111,plain,(
% 2.91/1.41 s(index_270)=p(index_267)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f512,f694])).
% 2.91/1.41 fof(f1113,plain,(
% 2.91/1.41 s(index_258)=p(index_255)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f507,f694])).
% 2.91/1.41 fof(f1116,plain,(
% 2.91/1.41 s(index_240)=p(index_237)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f501,f694])).
% 2.91/1.41 fof(f1120,plain,(
% 2.91/1.41 s(index_222)=p(index_219)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f494,f694])).
% 2.91/1.41 fof(f1124,plain,(
% 2.91/1.41 s(index_198)=p(index_195)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f485,f694])).
% 2.91/1.41 fof(f1126,plain,(
% 2.91/1.41 s(index_186)=p(index_183)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f481,f694])).
% 2.91/1.41 fof(f1131,plain,(
% 2.91/1.41 s(index_162)=p(index_159)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f472,f694])).
% 2.91/1.41 fof(f1134,plain,(
% 2.91/1.41 s(index_144)=p(index_141)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f465,f694])).
% 2.91/1.41 fof(f1135,plain,(
% 2.91/1.41 s(index_138)=p(index_135)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f463,f694])).
% 2.91/1.41 fof(f1138,plain,(
% 2.91/1.41 s(index_120)=p(index_117)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f457,f694])).
% 2.91/1.41 fof(f1139,plain,(
% 2.91/1.41 s(index_12)=p(index_9)),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f456,f694])).
% 2.91/1.41 fof(f1144,plain,(
% 2.91/1.41 ![X0]: (s(X0)=p(p(X0)))),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f350,f694])).
% 2.91/1.41 fof(f1268,plain,(
% 2.91/1.41 q0=store(q,head,index_0)),
% 2.91/1.41 inference(forward_demodulation,[status(thm)],[f638,f545])).
% 2.91/1.41 fof(f1269,plain,(
% 2.91/1.41 ![X0]: (head=X0|select(q0,X0)=select(q,X0))),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f1268,f345])).
% 2.91/1.41 fof(f1270,plain,(
% 2.91/1.41 select(q0,head)=index_0),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f1268,f343])).
% 2.91/1.41 fof(f1361,plain,(
% 2.91/1.41 ![X0]: (seq=X0|select(queue_101,X0)=select(q23,X0))),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f546,f345])).
% 2.91/1.41 fof(f1363,plain,(
% 2.91/1.41 q24=store(queue_101,tail,index_102)),
% 2.91/1.41 inference(forward_demodulation,[status(thm)],[f655,f547])).
% 2.91/1.41 fof(f1364,plain,(
% 2.91/1.41 ![X0]: (tail=X0|select(q24,X0)=select(queue_101,X0))),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f1363,f345])).
% 2.91/1.41 fof(f1365,plain,(
% 2.91/1.41 select(q24,tail)=index_102),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f1363,f343])).
% 2.91/1.41 fof(f1366,plain,(
% 2.91/1.41 index_105=index_102),
% 2.91/1.41 inference(forward_demodulation,[status(thm)],[f451,f1365])).
% 2.91/1.41 fof(f1367,plain,(
% 2.91/1.41 ![X0]: (seq=X0|select(queue_107,X0)=select(q24,X0))),
% 2.91/1.41 inference(paramodulation,[status(thm)],[f548,f345])).
% 2.91/1.41 fof(f1370,plain,(
% 2.91/1.41 p(index_105)=index_99),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1366,f706])).
% 2.91/1.42 fof(f1373,plain,(
% 2.91/1.42 index_105=s(index_99)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1366,f450])).
% 2.91/1.42 fof(f1379,plain,(
% 2.91/1.42 s(index_105)=p(index_99)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1373,f694])).
% 2.91/1.42 fof(f1382,plain,(
% 2.91/1.42 index_108=p(index_99)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f452,f1379])).
% 2.91/1.42 fof(f1383,plain,(
% 2.91/1.42 q25=store(queue_107,tail,index_108)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f656,f549])).
% 2.91/1.42 fof(f1384,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q25,X0)=select(queue_107,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1383,f345])).
% 2.91/1.42 fof(f1385,plain,(
% 2.91/1.42 select(q25,tail)=index_108),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1383,f343])).
% 2.91/1.42 fof(f1386,plain,(
% 2.91/1.42 index_111=index_108),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f453,f1385])).
% 2.91/1.42 fof(f1389,plain,(
% 2.91/1.42 p(index_111)=index_105),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1386,f710])).
% 2.91/1.42 fof(f1392,plain,(
% 2.91/1.42 index_111=s(index_105)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1386,f452])).
% 2.91/1.42 fof(f1394,plain,(
% 2.91/1.42 index_111=p(index_99)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1386,f1382])).
% 2.91/1.42 fof(f1403,plain,(
% 2.91/1.42 s(index_111)=p(index_105)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1392,f694])).
% 2.91/1.42 fof(f1406,plain,(
% 2.91/1.42 index_114=p(index_105)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f454,f1403])).
% 2.91/1.42 fof(f1407,plain,(
% 2.91/1.42 index_114=index_99),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1370,f1406])).
% 2.91/1.42 fof(f1423,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_11,X0)=select(q9,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f550,f345])).
% 2.91/1.42 fof(f1425,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_113,X0)=select(q25,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f551,f345])).
% 2.91/1.42 fof(f1511,plain,(
% 2.91/1.42 q26=store(queue_113,tail,index_114)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f657,f552])).
% 2.91/1.42 fof(f1512,plain,(
% 2.91/1.42 q26=store(queue_113,tail,index_99)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1407,f1511])).
% 2.91/1.42 fof(f1513,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q26,X0)=select(queue_113,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1512,f345])).
% 2.91/1.42 fof(f1514,plain,(
% 2.91/1.42 select(q26,tail)=index_99),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1512,f343])).
% 2.91/1.42 fof(f1515,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_119,X0)=select(q26,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f553,f345])).
% 2.91/1.42 fof(f1517,plain,(
% 2.91/1.42 q27=store(queue_119,tail,index_120)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f658,f554])).
% 2.91/1.42 fof(f1518,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q27,X0)=select(queue_119,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1517,f345])).
% 2.91/1.42 fof(f1519,plain,(
% 2.91/1.42 select(q27,tail)=index_120),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1517,f343])).
% 2.91/1.42 fof(f1520,plain,(
% 2.91/1.42 index_123=index_120),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f458,f1519])).
% 2.91/1.42 fof(f1522,plain,(
% 2.91/1.42 s(index_123)=p(index_117)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1520,f1138])).
% 2.91/1.42 fof(f1527,plain,(
% 2.91/1.42 index_126=p(index_117)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f459,f1522])).
% 2.91/1.42 fof(f1531,plain,(
% 2.91/1.42 s(index_126)=index_117),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1527,f350])).
% 2.91/1.42 fof(f1541,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_125,X0)=select(q27,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f555,f345])).
% 2.91/1.42 fof(f1696,plain,(
% 2.91/1.42 q28=store(queue_125,tail,index_126)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f659,f556])).
% 2.91/1.42 fof(f1697,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q28,X0)=select(queue_125,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1696,f345])).
% 2.91/1.42 fof(f1698,plain,(
% 2.91/1.42 select(q28,tail)=index_126),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1696,f343])).
% 2.91/1.42 fof(f1699,plain,(
% 2.91/1.42 index_129=index_126),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f460,f1698])).
% 2.91/1.42 fof(f1700,plain,(
% 2.91/1.42 q10=store(queue_11,tail,index_12)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f640,f557])).
% 2.91/1.42 fof(f1701,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(queue_11,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1700,f345])).
% 2.91/1.42 fof(f1702,plain,(
% 2.91/1.42 select(q10,tail)=index_12),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1700,f343])).
% 2.91/1.42 fof(f1703,plain,(
% 2.91/1.42 index_15=index_12),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f467,f1702])).
% 2.91/1.42 fof(f1705,plain,(
% 2.91/1.42 s(index_129)=index_117),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1699,f1531])).
% 2.91/1.42 fof(f1712,plain,(
% 2.91/1.42 s(index_15)=p(index_9)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1703,f1139])).
% 2.91/1.42 fof(f1713,plain,(
% 2.91/1.42 p(index_15)=index_9),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1703,f718])).
% 2.91/1.42 fof(f1716,plain,(
% 2.91/1.42 index_15=s(index_9)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1703,f456])).
% 2.91/1.42 fof(f1717,plain,(
% 2.91/1.42 index_18=p(index_9)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f478,f1712])).
% 2.91/1.42 fof(f1719,plain,(
% 2.91/1.42 index_132=index_117),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1705,f461])).
% 2.91/1.42 fof(f1749,plain,(
% 2.91/1.42 s(index_18)=index_9),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1717,f350])).
% 2.91/1.42 fof(f1762,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_131,X0)=select(q28,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f558,f345])).
% 2.91/1.42 fof(f1764,plain,(
% 2.91/1.42 q29=store(queue_131,tail,index_132)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f660,f559])).
% 2.91/1.42 fof(f1765,plain,(
% 2.91/1.42 q29=store(queue_131,tail,index_117)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1719,f1764])).
% 2.91/1.42 fof(f1766,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q29,X0)=select(queue_131,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1765,f345])).
% 2.91/1.42 fof(f1767,plain,(
% 2.91/1.42 select(q29,tail)=index_117),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1765,f343])).
% 2.91/1.42 fof(f1768,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_137,X0)=select(q2,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f560,f345])).
% 2.91/1.42 fof(f1776,plain,(
% 2.91/1.42 q3=store(queue_137,tail,index_138)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f661,f561])).
% 2.91/1.42 fof(f1777,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q3,X0)=select(queue_137,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1776,f345])).
% 2.91/1.42 fof(f1778,plain,(
% 2.91/1.42 select(q3,tail)=index_138),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1776,f343])).
% 2.91/1.42 fof(f1779,plain,(
% 2.91/1.42 index_201=index_138),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f486,f1778])).
% 2.91/1.42 fof(f1781,plain,(
% 2.91/1.42 s(index_201)=p(index_135)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1779,f1135])).
% 2.91/1.42 fof(f1785,plain,(
% 2.91/1.42 index_201=s(index_135)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1779,f463])).
% 2.91/1.42 fof(f1786,plain,(
% 2.91/1.42 index_204=p(index_135)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f487,f1781])).
% 2.91/1.42 fof(f1791,plain,(
% 2.91/1.42 s(index_204)=index_135),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1786,f350])).
% 2.91/1.42 fof(f1810,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_143,X0)=select(q29,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f562,f345])).
% 2.91/1.42 fof(f1812,plain,(
% 2.91/1.42 q30=store(queue_143,tail,index_144)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f662,f563])).
% 2.91/1.42 fof(f1813,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q30,X0)=select(queue_143,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1812,f345])).
% 2.91/1.42 fof(f1814,plain,(
% 2.91/1.42 select(q30,tail)=index_144),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1812,f343])).
% 2.91/1.42 fof(f1815,plain,(
% 2.91/1.42 index_147=index_144),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f466,f1814])).
% 2.91/1.42 fof(f1817,plain,(
% 2.91/1.42 s(index_147)=p(index_141)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1815,f1134])).
% 2.91/1.42 fof(f1822,plain,(
% 2.91/1.42 index_150=p(index_141)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f468,f1817])).
% 2.91/1.42 fof(f1827,plain,(
% 2.91/1.42 s(index_150)=index_141),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1822,f350])).
% 2.91/1.42 fof(f1846,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_149,X0)=select(q30,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f564,f345])).
% 2.91/1.42 fof(f1848,plain,(
% 2.91/1.42 q31=store(queue_149,tail,index_150)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f663,f565])).
% 2.91/1.42 fof(f1849,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q31,X0)=select(queue_149,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1848,f345])).
% 2.91/1.42 fof(f1850,plain,(
% 2.91/1.42 select(q31,tail)=index_150),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1848,f343])).
% 2.91/1.42 fof(f1851,plain,(
% 2.91/1.42 index_153=index_150),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f469,f1850])).
% 2.91/1.42 fof(f1852,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_155,X0)=select(q31,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f566,f345])).
% 2.91/1.42 fof(f1855,plain,(
% 2.91/1.42 s(index_153)=index_141),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1851,f1827])).
% 2.91/1.42 fof(f1861,plain,(
% 2.91/1.42 index_156=index_141),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1855,f470])).
% 2.91/1.42 fof(f1878,plain,(
% 2.91/1.42 q32=store(queue_155,tail,index_156)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f664,f567])).
% 2.91/1.42 fof(f1879,plain,(
% 2.91/1.42 q32=store(queue_155,tail,index_141)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1861,f1878])).
% 2.91/1.42 fof(f1880,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q32,X0)=select(queue_155,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1879,f345])).
% 2.91/1.42 fof(f1881,plain,(
% 2.91/1.42 select(q32,tail)=index_141),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1879,f343])).
% 2.91/1.42 fof(f1892,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_161,X0)=select(q32,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f568,f345])).
% 2.91/1.42 fof(f1894,plain,(
% 2.91/1.42 q33=store(queue_161,tail,index_162)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f665,f569])).
% 2.91/1.42 fof(f1895,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q33,X0)=select(queue_161,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1894,f345])).
% 2.91/1.42 fof(f1896,plain,(
% 2.91/1.42 select(q33,tail)=index_162),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1894,f343])).
% 2.91/1.42 fof(f1897,plain,(
% 2.91/1.42 index_165=index_162),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f473,f1896])).
% 2.91/1.42 fof(f1899,plain,(
% 2.91/1.42 s(index_165)=p(index_159)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1897,f1131])).
% 2.91/1.42 fof(f1904,plain,(
% 2.91/1.42 index_168=p(index_159)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f474,f1899])).
% 2.91/1.42 fof(f1909,plain,(
% 2.91/1.42 s(index_168)=index_159),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1904,f350])).
% 2.91/1.42 fof(f1928,plain,(
% 2.91/1.42 index_117=index_99),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1514,f455])).
% 2.91/1.42 fof(f1949,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_167,X0)=select(q33,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f570,f345])).
% 2.91/1.42 fof(f1951,plain,(
% 2.91/1.42 q34=store(queue_167,tail,index_168)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f666,f571])).
% 2.91/1.42 fof(f1952,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q34,X0)=select(queue_167,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1951,f345])).
% 2.91/1.42 fof(f1953,plain,(
% 2.91/1.42 select(q34,tail)=index_168),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1951,f343])).
% 2.91/1.42 fof(f1954,plain,(
% 2.91/1.42 index_171=index_168),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f475,f1953])).
% 2.91/1.42 fof(f1955,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_17,X0)=select(q10,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f572,f345])).
% 2.91/1.42 fof(f1964,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_173,X0)=select(q34,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f573,f345])).
% 2.91/1.42 fof(f1967,plain,(
% 2.91/1.42 s(index_171)=index_159),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1954,f1909])).
% 2.91/1.42 fof(f1976,plain,(
% 2.91/1.42 index_174=index_159),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f1967,f476])).
% 2.91/1.42 fof(f2003,plain,(
% 2.91/1.42 q35=store(queue_173,tail,index_174)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f667,f574])).
% 2.91/1.42 fof(f2004,plain,(
% 2.91/1.42 q35=store(queue_173,tail,index_159)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1976,f2003])).
% 2.91/1.42 fof(f2005,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q35,X0)=select(queue_173,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2004,f345])).
% 2.91/1.42 fof(f2006,plain,(
% 2.91/1.42 select(q35,tail)=index_159),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2004,f343])).
% 2.91/1.42 fof(f2007,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_179,X0)=select(q35,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f575,f345])).
% 2.91/1.42 fof(f2009,plain,(
% 2.91/1.42 index_141=index_99),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2010,f464])).
% 2.91/1.42 fof(f2010,plain,(
% 2.91/1.42 select(q29,tail)=index_99),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1928,f1767])).
% 2.91/1.42 fof(f2038,plain,(
% 2.91/1.42 q36=store(queue_179,tail,index_180)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f668,f576])).
% 2.91/1.42 fof(f2039,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q36,X0)=select(queue_179,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2038,f345])).
% 2.91/1.42 fof(f2040,plain,(
% 2.91/1.42 select(q36,tail)=index_180),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2038,f343])).
% 2.91/1.42 fof(f2041,plain,(
% 2.91/1.42 index_183=index_180),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f480,f2040])).
% 2.91/1.42 fof(f2042,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_185,X0)=select(q36,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f577,f345])).
% 2.91/1.42 fof(f2044,plain,(
% 2.91/1.42 q37=store(queue_185,tail,index_186)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f669,f578])).
% 2.91/1.42 fof(f2045,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q37,X0)=select(queue_185,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2044,f345])).
% 2.91/1.42 fof(f2046,plain,(
% 2.91/1.42 select(q37,tail)=index_186),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2044,f343])).
% 2.91/1.42 fof(f2047,plain,(
% 2.91/1.42 index_189=index_186),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f482,f2046])).
% 2.91/1.42 fof(f2050,plain,(
% 2.91/1.42 p(index_183)=index_177),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2041,f770])).
% 2.91/1.42 fof(f2057,plain,(
% 2.91/1.42 s(index_189)=p(index_183)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2047,f1126])).
% 2.91/1.42 fof(f2062,plain,(
% 2.91/1.42 index_192=p(index_183)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f483,f2057])).
% 2.91/1.42 fof(f2065,plain,(
% 2.91/1.42 q11=store(queue_17,tail,index_18)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f641,f579])).
% 2.91/1.42 fof(f2066,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q11,X0)=select(queue_17,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2065,f345])).
% 2.91/1.42 fof(f2067,plain,(
% 2.91/1.42 select(q11,tail)=index_18),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2065,f343])).
% 2.91/1.42 fof(f2068,plain,(
% 2.91/1.42 index_21=index_18),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f489,f2067])).
% 2.91/1.42 fof(f2070,plain,(
% 2.91/1.42 s(index_21)=index_9),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2068,f1749])).
% 2.91/1.42 fof(f2071,plain,(
% 2.91/1.42 index_21=p(index_9)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2068,f1717])).
% 2.91/1.42 fof(f2075,plain,(
% 2.91/1.42 index_21=s(index_15)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2068,f478])).
% 2.91/1.42 fof(f2099,plain,(
% 2.91/1.42 index_192=index_177),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2050,f2062])).
% 2.91/1.42 fof(f2102,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_191,X0)=select(q37,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f580,f345])).
% 2.91/1.42 fof(f2104,plain,(
% 2.91/1.42 q38=store(queue_191,tail,index_192)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f670,f581])).
% 2.91/1.42 fof(f2105,plain,(
% 2.91/1.42 q38=store(queue_191,tail,index_177)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2099,f2104])).
% 2.91/1.42 fof(f2106,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q38,X0)=select(queue_191,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2105,f345])).
% 2.91/1.42 fof(f2107,plain,(
% 2.91/1.42 select(q38,tail)=index_177),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2105,f343])).
% 2.91/1.42 fof(f2117,plain,(
% 2.91/1.42 index_24=index_9),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2070,f500])).
% 2.91/1.42 fof(f2151,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_197,X0)=select(q38,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f582,f345])).
% 2.91/1.42 fof(f2153,plain,(
% 2.91/1.42 q39=store(queue_197,tail,index_198)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f671,f583])).
% 2.91/1.42 fof(f2154,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q39,X0)=select(queue_197,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2153,f345])).
% 2.91/1.42 fof(f2155,plain,(
% 2.91/1.42 select(q39,tail)=index_198),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2153,f343])).
% 2.91/1.42 fof(f2156,plain,(
% 2.91/1.42 index_207=index_198),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f488,f2155])).
% 2.91/1.42 fof(f2157,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_203,X0)=select(q3,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f584,f345])).
% 2.91/1.42 fof(f2160,plain,(
% 2.91/1.42 s(index_207)=p(index_195)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2156,f1124])).
% 2.91/1.42 fof(f2165,plain,(
% 2.91/1.42 index_210=p(index_195)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f490,f2160])).
% 2.91/1.42 fof(f2167,plain,(
% 2.91/1.42 q4=store(queue_203,tail,index_204)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f672,f585])).
% 2.91/1.42 fof(f2168,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q4,X0)=select(queue_203,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2167,f345])).
% 2.91/1.42 fof(f2169,plain,(
% 2.91/1.42 select(q4,tail)=index_204),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2167,f343])).
% 2.91/1.42 fof(f2170,plain,(
% 2.91/1.42 index_249=index_204),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f504,f2169])).
% 2.91/1.42 fof(f2172,plain,(
% 2.91/1.42 s(index_249)=index_135),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2170,f1791])).
% 2.91/1.42 fof(f2181,plain,(
% 2.91/1.42 s(index_210)=index_195),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2165,f350])).
% 2.91/1.42 fof(f2194,plain,(
% 2.91/1.42 index_252=index_135),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2172,f505])).
% 2.91/1.42 fof(f2205,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_209,X0)=select(q39,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f586,f345])).
% 2.91/1.42 fof(f2207,plain,(
% 2.91/1.42 q40=store(queue_209,tail,index_210)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f673,f587])).
% 2.91/1.42 fof(f2208,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q40,X0)=select(queue_209,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2207,f345])).
% 2.91/1.42 fof(f2209,plain,(
% 2.91/1.42 select(q40,tail)=index_210),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2207,f343])).
% 2.91/1.42 fof(f2210,plain,(
% 2.91/1.42 index_213=index_210),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f491,f2209])).
% 2.91/1.42 fof(f2237,plain,(
% 2.91/1.42 index_216=index_195),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2238,f492])).
% 2.91/1.42 fof(f2238,plain,(
% 2.91/1.42 s(index_213)=index_195),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2210,f2181])).
% 2.91/1.42 fof(f2257,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_215,X0)=select(q40,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f588,f345])).
% 2.91/1.42 fof(f2259,plain,(
% 2.91/1.42 q41=store(queue_215,tail,index_216)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f674,f589])).
% 2.91/1.42 fof(f2260,plain,(
% 2.91/1.42 q41=store(queue_215,tail,index_195)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2237,f2259])).
% 2.91/1.42 fof(f2261,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q41,X0)=select(queue_215,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2260,f345])).
% 2.91/1.42 fof(f2262,plain,(
% 2.91/1.42 select(q41,tail)=index_195),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2260,f343])).
% 2.91/1.42 fof(f2263,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_221,X0)=select(q41,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f590,f345])).
% 2.91/1.42 fof(f2275,plain,(
% 2.91/1.42 q42=store(queue_221,tail,index_222)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f675,f591])).
% 2.91/1.42 fof(f2276,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q42,X0)=select(queue_221,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2275,f345])).
% 2.91/1.42 fof(f2277,plain,(
% 2.91/1.42 select(q42,tail)=index_222),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2275,f343])).
% 2.91/1.42 fof(f2278,plain,(
% 2.91/1.42 index_225=index_222),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f495,f2277])).
% 2.91/1.42 fof(f2280,plain,(
% 2.91/1.42 s(index_225)=p(index_219)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2278,f1120])).
% 2.91/1.42 fof(f2285,plain,(
% 2.91/1.42 index_228=p(index_219)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f496,f2280])).
% 2.91/1.42 fof(f2290,plain,(
% 2.91/1.42 s(index_228)=index_219),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2285,f350])).
% 2.91/1.42 fof(f2304,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_227,X0)=select(q42,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f592,f345])).
% 2.91/1.42 fof(f2306,plain,(
% 2.91/1.42 q43=store(queue_227,tail,index_228)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f676,f593])).
% 2.91/1.42 fof(f2307,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q43,X0)=select(queue_227,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2306,f345])).
% 2.91/1.42 fof(f2308,plain,(
% 2.91/1.42 select(q43,tail)=index_228),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2306,f343])).
% 2.91/1.42 fof(f2309,plain,(
% 2.91/1.42 index_231=index_228),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f497,f2308])).
% 2.91/1.42 fof(f2318,plain,(
% 2.91/1.42 index_234=index_219),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2319,f498])).
% 2.91/1.42 fof(f2319,plain,(
% 2.91/1.42 s(index_231)=index_219),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2309,f2290])).
% 2.91/1.42 fof(f2348,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_23,X0)=select(q11,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f594,f345])).
% 2.91/1.42 fof(f2350,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_233,X0)=select(q43,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f595,f345])).
% 2.91/1.42 fof(f2352,plain,(
% 2.91/1.42 q44=store(queue_233,tail,index_234)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f677,f596])).
% 2.91/1.42 fof(f2353,plain,(
% 2.91/1.42 q44=store(queue_233,tail,index_219)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2318,f2352])).
% 2.91/1.42 fof(f2354,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q44,X0)=select(queue_233,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2353,f345])).
% 2.91/1.42 fof(f2355,plain,(
% 2.91/1.42 select(q44,tail)=index_219),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2353,f343])).
% 2.91/1.42 fof(f2356,plain,(
% 2.91/1.42 index_159=index_99),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2357,f471])).
% 2.91/1.42 fof(f2357,plain,(
% 2.91/1.42 select(q32,tail)=index_99),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2009,f1881])).
% 2.91/1.42 fof(f2378,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_239,X0)=select(q44,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f597,f345])).
% 2.91/1.42 fof(f2390,plain,(
% 2.91/1.42 q45=store(queue_239,tail,index_240)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f678,f598])).
% 2.91/1.42 fof(f2391,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q45,X0)=select(queue_239,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2390,f345])).
% 2.91/1.42 fof(f2392,plain,(
% 2.91/1.42 select(q45,tail)=index_240),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2390,f343])).
% 2.91/1.42 fof(f2393,plain,(
% 2.91/1.42 index_243=index_240),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f502,f2392])).
% 2.91/1.42 fof(f2394,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_245,X0)=select(q45,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f599,f345])).
% 2.91/1.42 fof(f2397,plain,(
% 2.91/1.42 s(index_243)=p(index_237)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2393,f1116])).
% 2.91/1.42 fof(f2402,plain,(
% 2.91/1.42 index_246=p(index_237)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f503,f2397])).
% 2.91/1.42 fof(f2426,plain,(
% 2.91/1.42 q46=store(queue_245,tail,index_246)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f679,f600])).
% 2.91/1.42 fof(f2427,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q46,X0)=select(queue_245,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2426,f345])).
% 2.91/1.42 fof(f2428,plain,(
% 2.91/1.42 select(q46,tail)=index_246),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2426,f343])).
% 2.91/1.42 fof(f2429,plain,(
% 2.91/1.42 q12=store(queue_23,tail,index_24)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f642,f601])).
% 2.91/1.42 fof(f2430,plain,(
% 2.91/1.42 q12=store(queue_23,tail,index_9)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2117,f2429])).
% 2.91/1.42 fof(f2431,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q12,X0)=select(queue_23,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2430,f345])).
% 2.91/1.42 fof(f2432,plain,(
% 2.91/1.42 select(q12,tail)=index_9),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2430,f343])).
% 2.91/1.42 fof(f2433,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_251,X0)=select(q4,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f602,f345])).
% 2.91/1.42 fof(f2435,plain,(
% 2.91/1.42 index_177=index_99),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2436,f477])).
% 2.91/1.42 fof(f2436,plain,(
% 2.91/1.42 select(q35,tail)=index_99),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2356,f2006])).
% 2.91/1.42 fof(f2461,plain,(
% 2.91/1.42 q5=store(queue_251,tail,index_252)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f680,f603])).
% 2.91/1.42 fof(f2462,plain,(
% 2.91/1.42 q5=store(queue_251,tail,index_135)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2194,f2461])).
% 2.91/1.42 fof(f2463,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q5,X0)=select(queue_251,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2462,f345])).
% 2.91/1.42 fof(f2464,plain,(
% 2.91/1.42 select(q5,tail)=index_135),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2462,f343])).
% 2.91/1.42 fof(f2471,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_257,X0)=select(q5,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f604,f345])).
% 2.91/1.42 fof(f2473,plain,(
% 2.91/1.42 q6=store(queue_257,tail,index_258)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f681,f605])).
% 2.91/1.42 fof(f2474,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q6,X0)=select(queue_257,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2473,f345])).
% 2.91/1.42 fof(f2475,plain,(
% 2.91/1.42 select(q6,tail)=index_258),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2473,f343])).
% 2.91/1.42 fof(f2476,plain,(
% 2.91/1.42 index_261=index_258),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f508,f2475])).
% 2.91/1.42 fof(f2478,plain,(
% 2.91/1.42 s(index_261)=p(index_255)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2476,f1113])).
% 2.91/1.42 fof(f2483,plain,(
% 2.91/1.42 index_264=p(index_255)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f509,f2478])).
% 2.91/1.42 fof(f2488,plain,(
% 2.91/1.42 s(index_264)=index_255),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2483,f350])).
% 2.91/1.42 fof(f2510,plain,(
% 2.91/1.42 index_195=index_99),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2511,f484])).
% 2.91/1.42 fof(f2511,plain,(
% 2.91/1.42 select(q38,tail)=index_99),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2435,f2107])).
% 2.91/1.42 fof(f2512,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_263,X0)=select(q6,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f606,f345])).
% 2.91/1.42 fof(f2514,plain,(
% 2.91/1.42 q7=store(queue_263,tail,index_264)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f682,f607])).
% 2.91/1.42 fof(f2515,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q7,X0)=select(queue_263,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2514,f345])).
% 2.91/1.42 fof(f2516,plain,(
% 2.91/1.42 select(q7,tail)=index_264),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2514,f343])).
% 2.91/1.42 fof(f2517,plain,(
% 2.91/1.42 index_267=index_264),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f510,f2516])).
% 2.91/1.42 fof(f2518,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_269,X0)=select(q7,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f608,f345])).
% 2.91/1.42 fof(f2533,plain,(
% 2.91/1.42 s(index_267)=index_255),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2517,f2488])).
% 2.91/1.42 fof(f2552,plain,(
% 2.91/1.42 q8=store(queue_269,tail,index_270)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f683,f609])).
% 2.91/1.42 fof(f2553,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q8,X0)=select(queue_269,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2552,f345])).
% 2.91/1.42 fof(f2554,plain,(
% 2.91/1.42 select(q8,tail)=index_270),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2552,f343])).
% 2.91/1.42 fof(f2555,plain,(
% 2.91/1.42 index_273=index_270),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f513,f2554])).
% 2.91/1.42 fof(f2559,plain,(
% 2.91/1.42 s(index_273)=p(index_267)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2555,f1111])).
% 2.91/1.42 fof(f2564,plain,(
% 2.91/1.42 index_276=p(index_267)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f514,f2559])).
% 2.91/1.42 fof(f2568,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_275,X0)=select(q8,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f610,f345])).
% 2.91/1.42 fof(f2570,plain,(
% 2.91/1.42 q9=store(queue_275,tail,index_276)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f684,f611])).
% 2.91/1.42 fof(f2571,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q9,X0)=select(queue_275,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2570,f345])).
% 2.91/1.42 fof(f2572,plain,(
% 2.91/1.42 select(q9,tail)=index_276),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2570,f343])).
% 2.91/1.42 fof(f2573,plain,(
% 2.91/1.42 index_9=index_276),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f540,f2572])).
% 2.91/1.42 fof(f2613,plain,(
% 2.91/1.42 index_9=p(index_267)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2573,f2564])).
% 2.91/1.42 fof(f2614,plain,(
% 2.91/1.42 s(index_267)=p(index_9)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2613,f1144])).
% 2.91/1.42 fof(f2618,plain,(
% 2.91/1.42 index_255=p(index_9)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2533,f2614])).
% 2.91/1.42 fof(f2619,plain,(
% 2.91/1.42 index_255=index_21),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2071,f2618])).
% 2.91/1.42 fof(f2638,plain,(
% 2.91/1.42 index_21=select(q5,tail)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2619,f506])).
% 2.91/1.42 fof(f2648,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_29,X0)=select(q12,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f612,f345])).
% 2.91/1.42 fof(f2650,plain,(
% 2.91/1.42 q13=store(queue_29,tail,index_30)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f643,f613])).
% 2.91/1.42 fof(f2651,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q13,X0)=select(queue_29,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2650,f345])).
% 2.91/1.42 fof(f2652,plain,(
% 2.91/1.42 select(q13,tail)=index_30),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2650,f343])).
% 2.91/1.42 fof(f2653,plain,(
% 2.91/1.42 index_33=index_30),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f520,f2652])).
% 2.91/1.42 fof(f2654,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_35,X0)=select(q13,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f614,f345])).
% 2.91/1.42 fof(f2659,plain,(
% 2.91/1.42 p(index_33)=index_27),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2653,f852])).
% 2.91/1.42 fof(f2662,plain,(
% 2.91/1.42 index_33=s(index_27)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2653,f519])).
% 2.91/1.42 fof(f2665,plain,(
% 2.91/1.42 q14=store(queue_35,tail,index_36)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f644,f615])).
% 2.91/1.42 fof(f2666,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q14,X0)=select(queue_35,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2665,f345])).
% 2.91/1.42 fof(f2667,plain,(
% 2.91/1.42 select(q14,tail)=index_36),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2665,f343])).
% 2.91/1.42 fof(f2668,plain,(
% 2.91/1.42 index_39=index_36),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f522,f2667])).
% 2.91/1.42 fof(f2671,plain,(
% 2.91/1.42 s(index_39)=p(index_33)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2668,f1107])).
% 2.91/1.42 fof(f2676,plain,(
% 2.91/1.42 index_42=p(index_33)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f523,f2671])).
% 2.91/1.42 fof(f2688,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_41,X0)=select(q14,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f616,f345])).
% 2.91/1.42 fof(f2690,plain,(
% 2.91/1.42 q15=store(queue_41,tail,index_42)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f645,f617])).
% 2.91/1.42 fof(f2691,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q15,X0)=select(queue_41,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2690,f345])).
% 2.91/1.42 fof(f2692,plain,(
% 2.91/1.42 select(q15,tail)=index_42),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2690,f343])).
% 2.91/1.42 fof(f2693,plain,(
% 2.91/1.42 index_45=index_42),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f524,f2692])).
% 2.91/1.42 fof(f2723,plain,(
% 2.91/1.42 index_45=p(index_33)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2693,f2676])).
% 2.91/1.42 fof(f2734,plain,(
% 2.91/1.42 index_48=s(index_27)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2735,f525])).
% 2.91/1.42 fof(f2735,plain,(
% 2.91/1.42 index_45=index_27),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2659,f2723])).
% 2.91/1.42 fof(f2737,plain,(
% 2.91/1.42 index_48=index_33),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2662,f2734])).
% 2.91/1.42 fof(f2750,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_47,X0)=select(q15,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f618,f345])).
% 2.91/1.42 fof(f2752,plain,(
% 2.91/1.42 q16=store(queue_47,tail,index_48)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f646,f619])).
% 2.91/1.42 fof(f2753,plain,(
% 2.91/1.42 q16=store(queue_47,tail,index_33)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2737,f2752])).
% 2.91/1.42 fof(f2754,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q16,X0)=select(queue_47,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2753,f345])).
% 2.91/1.42 fof(f2755,plain,(
% 2.91/1.42 select(q16,tail)=index_33),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2753,f343])).
% 2.91/1.42 fof(f2756,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_5,X0)=select(q0,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f620,f345])).
% 2.91/1.42 fof(f2766,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_53,X0)=select(q16,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f621,f345])).
% 2.91/1.42 fof(f2773,plain,(
% 2.91/1.42 q17=store(queue_53,tail,index_54)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f647,f622])).
% 2.91/1.42 fof(f2774,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q17,X0)=select(queue_53,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2773,f345])).
% 2.91/1.42 fof(f2775,plain,(
% 2.91/1.42 select(q17,tail)=index_54),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2773,f343])).
% 2.91/1.42 fof(f2776,plain,(
% 2.91/1.42 index_57=index_54),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f528,f2775])).
% 2.91/1.42 fof(f2777,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_59,X0)=select(q17,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f623,f345])).
% 2.91/1.42 fof(f2784,plain,(
% 2.91/1.42 index_57=s(index_51)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2776,f527])).
% 2.91/1.42 fof(f2809,plain,(
% 2.91/1.42 index_219=index_99),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2810,f493])).
% 2.91/1.42 fof(f2810,plain,(
% 2.91/1.42 select(q41,tail)=index_99),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2510,f2262])).
% 2.91/1.42 fof(f2836,plain,(
% 2.91/1.42 q18=store(queue_59,tail,index_60)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f648,f624])).
% 2.91/1.42 fof(f2837,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q18,X0)=select(queue_59,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2836,f345])).
% 2.91/1.42 fof(f2838,plain,(
% 2.91/1.42 select(q18,tail)=index_60),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2836,f343])).
% 2.91/1.42 fof(f2839,plain,(
% 2.91/1.42 index_63=index_60),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f531,f2838])).
% 2.91/1.42 fof(f2840,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_65,X0)=select(q18,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f625,f345])).
% 2.91/1.42 fof(f2842,plain,(
% 2.91/1.42 q19=store(queue_65,tail,index_66)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f649,f626])).
% 2.91/1.42 fof(f2843,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q19,X0)=select(queue_65,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2842,f345])).
% 2.91/1.42 fof(f2844,plain,(
% 2.91/1.42 select(q19,tail)=index_66),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2842,f343])).
% 2.91/1.42 fof(f2845,plain,(
% 2.91/1.42 index_75=index_66),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f535,f2844])).
% 2.91/1.42 fof(f2852,plain,(
% 2.91/1.42 p(index_63)=index_57),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2839,f878])).
% 2.91/1.42 fof(f2855,plain,(
% 2.91/1.42 q1=store(queue_5,tail,index_6)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f639,f627])).
% 2.91/1.42 fof(f2856,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q1,X0)=select(queue_5,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2855,f345])).
% 2.91/1.42 fof(f2857,plain,(
% 2.91/1.42 select(q1,tail)=index_6),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2855,f343])).
% 2.91/1.42 fof(f2858,plain,(
% 2.91/1.42 index_69=index_6),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f533,f2857])).
% 2.91/1.42 fof(f2860,plain,(
% 2.91/1.42 s(index_75)=p(index_63)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2845,f1101])).
% 2.91/1.42 fof(f2865,plain,(
% 2.91/1.42 index_78=p(index_63)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f536,f2860])).
% 2.91/1.42 fof(f2868,plain,(
% 2.91/1.42 s(index_69)=p(index_3)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2858,f1103])).
% 2.91/1.42 fof(f2873,plain,(
% 2.91/1.42 index_72=p(index_3)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f534,f2868])).
% 2.91/1.42 fof(f2882,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_71,X0)=select(q1,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f628,f345])).
% 2.91/1.42 fof(f2884,plain,(
% 2.91/1.42 q2=store(queue_71,tail,index_72)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f650,f629])).
% 2.91/1.42 fof(f2885,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q2,X0)=select(queue_71,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2884,f345])).
% 2.91/1.42 fof(f2886,plain,(
% 2.91/1.42 select(q2,tail)=index_72),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2884,f343])).
% 2.91/1.42 fof(f2887,plain,(
% 2.91/1.42 index_135=index_72),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f462,f2886])).
% 2.91/1.42 fof(f2927,plain,(
% 2.91/1.42 index_78=index_57),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2852,f2865])).
% 2.91/1.42 fof(f2939,plain,(
% 2.91/1.42 index_135=p(index_3)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2887,f2873])).
% 2.91/1.42 fof(f2943,plain,(
% 2.91/1.42 s(index_135)=index_3),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2939,f350])).
% 2.91/1.42 fof(f2945,plain,(
% 2.91/1.42 index_201=index_3),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1785,f2943])).
% 2.91/1.42 fof(f2951,plain,(
% 2.91/1.42 index_201=select(q0,tail)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2945,f518])).
% 2.91/1.42 fof(f2952,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_77,X0)=select(q19,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f630,f345])).
% 2.91/1.42 fof(f2954,plain,(
% 2.91/1.42 q20=store(queue_77,tail,index_78)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f651,f631])).
% 2.91/1.42 fof(f2955,plain,(
% 2.91/1.42 q20=store(queue_77,tail,index_57)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2927,f2954])).
% 2.91/1.42 fof(f2956,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q20,X0)=select(queue_77,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2955,f345])).
% 2.91/1.42 fof(f2957,plain,(
% 2.91/1.42 select(q20,tail)=index_57),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2955,f343])).
% 2.91/1.42 fof(f2958,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_83,X0)=select(q20,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f632,f345])).
% 2.91/1.42 fof(f2966,plain,(
% 2.91/1.42 q21=store(queue_83,tail,index_84)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f652,f633])).
% 2.91/1.42 fof(f2967,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q21,X0)=select(queue_83,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2966,f345])).
% 2.91/1.42 fof(f2968,plain,(
% 2.91/1.42 select(q21,tail)=index_84),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2966,f343])).
% 2.91/1.42 fof(f2969,plain,(
% 2.91/1.42 index_87=index_84),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f539,f2968])).
% 2.91/1.42 fof(f2971,plain,(
% 2.91/1.42 s(index_87)=p(index_81)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2969,f1098])).
% 2.91/1.42 fof(f2976,plain,(
% 2.91/1.42 index_90=p(index_81)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f541,f2971])).
% 2.91/1.42 fof(f2986,plain,(
% 2.91/1.42 s(index_90)=index_81),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2976,f350])).
% 2.91/1.42 fof(f2999,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_89,X0)=select(q21,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f634,f345])).
% 2.91/1.42 fof(f3001,plain,(
% 2.91/1.42 q22=store(queue_89,tail,index_90)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f653,f635])).
% 2.91/1.42 fof(f3002,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q22,X0)=select(queue_89,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f3001,f345])).
% 2.91/1.42 fof(f3003,plain,(
% 2.91/1.42 select(q22,tail)=index_90),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f3001,f343])).
% 2.91/1.42 fof(f3004,plain,(
% 2.91/1.42 index_93=index_90),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f542,f3003])).
% 2.91/1.42 fof(f3015,plain,(
% 2.91/1.42 index_96=index_81),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3016,f543])).
% 2.91/1.42 fof(f3016,plain,(
% 2.91/1.42 s(index_93)=index_81),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f3004,f2986])).
% 2.91/1.42 fof(f3045,plain,(
% 2.91/1.42 ![X0]: (seq=X0|select(queue_95,X0)=select(q22,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f636,f345])).
% 2.91/1.42 fof(f3047,plain,(
% 2.91/1.42 q23=store(queue_95,tail,index_96)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f654,f637])).
% 2.91/1.42 fof(f3048,plain,(
% 2.91/1.42 q23=store(queue_95,tail,index_81)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f3015,f3047])).
% 2.91/1.42 fof(f3049,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q23,X0)=select(queue_95,X0))),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f3048,f345])).
% 2.91/1.42 fof(f3050,plain,(
% 2.91/1.42 select(q23,tail)=index_81),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f3048,f343])).
% 2.91/1.42 fof(f3051,plain,(
% 2.91/1.42 index_99=index_81),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f544,f3050])).
% 2.91/1.42 fof(f3064,plain,(
% 2.91/1.42 index_99=select(q20,tail)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3051,f537])).
% 2.91/1.42 fof(f3095,plain,(
% 2.91/1.42 index_237=index_99),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3096,f499])).
% 2.91/1.42 fof(f3096,plain,(
% 2.91/1.42 select(q44,tail)=index_99),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2809,f2355])).
% 2.91/1.42 fof(f3100,plain,(
% 2.91/1.42 index_246=p(index_99)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3095,f2402])).
% 2.91/1.42 fof(f3106,plain,(
% 2.91/1.42 index_246=index_111),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1394,f3100])).
% 2.91/1.42 fof(f3129,plain,(
% 2.91/1.42 index_281=index_111),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3130,f516])).
% 2.91/1.42 fof(f3130,plain,(
% 2.91/1.42 select(q46,tail)=index_111),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f3106,f2428])).
% 2.91/1.42 fof(f3132,plain,(
% 2.91/1.42 p(index_111)=index_282),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3129,f848])).
% 2.91/1.42 fof(f3137,plain,(
% 2.91/1.42 index_105=index_282),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1389,f3132])).
% 2.91/1.42 fof(f3139,plain,(
% 2.91/1.42 elem_283=select(earray_278,index_105)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3137,f448])).
% 2.91/1.42 fof(f3147,plain,(
% 2.91/1.42 index_27=index_9),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f2432,f511])).
% 2.91/1.42 fof(f3151,plain,(
% 2.91/1.42 index_33=s(index_9)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3147,f2662])).
% 2.91/1.42 fof(f3158,plain,(
% 2.91/1.42 index_33=index_15),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1716,f3151])).
% 2.91/1.42 fof(f3202,plain,(
% 2.91/1.42 index_135=s(index_15)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3212,f2075])).
% 2.91/1.42 fof(f3205,plain,(
% 2.91/1.42 s(index_135)=index_9),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3212,f2070])).
% 2.91/1.42 fof(f3212,plain,(
% 2.91/1.42 index_21=index_135),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f2464,f2638])).
% 2.91/1.42 fof(f3217,plain,(
% 2.91/1.42 s(index_135)=p(index_15)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f3202,f694])).
% 2.91/1.42 fof(f3220,plain,(
% 2.91/1.42 index_201=p(index_15)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1785,f3217])).
% 2.91/1.42 fof(f3221,plain,(
% 2.91/1.42 index_201=index_9),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f1713,f3220])).
% 2.91/1.42 fof(f3277,plain,(
% 2.91/1.42 index_51=index_15),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3278,f526])).
% 2.91/1.42 fof(f3278,plain,(
% 2.91/1.42 select(q16,tail)=index_15),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f3158,f2755])).
% 2.91/1.42 fof(f3284,plain,(
% 2.91/1.42 index_57=s(index_15)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3277,f2784])).
% 2.91/1.42 fof(f3290,plain,(
% 2.91/1.42 index_57=index_135),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f3202,f3284])).
% 2.91/1.42 fof(f3334,plain,(
% 2.91/1.42 index_9=select(q0,tail)),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f3221,f2951])).
% 2.91/1.42 fof(f3335,plain,(
% 2.91/1.42 select(q20,tail)=index_135),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f3290,f2957])).
% 2.91/1.42 fof(f3336,plain,(
% 2.91/1.42 index_99=index_135),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3064,f3335])).
% 2.91/1.42 fof(f3341,plain,(
% 2.91/1.42 s(index_99)=index_9),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3336,f3205])).
% 2.91/1.42 fof(f3404,plain,(
% 2.91/1.42 index_105=index_9),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3341,f1373])).
% 2.91/1.42 fof(f3423,plain,(
% 2.91/1.42 elem_283=select(earray_278,index_9)),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f3404,f3139])).
% 2.91/1.42 fof(f4030,plain,(
% 2.91/1.42 head=tail|select(q0,tail)=index_0),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f449,f1269])).
% 2.91/1.42 fof(f4032,definition,(
% 2.91/1.42 sQ47_spl <=> (head=tail)),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f4033,plain,(
% 2.91/1.42 head=tail|~sQ47_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f4032])).
% 2.91/1.42 fof(f4035,definition,(
% 2.91/1.42 sQ48_spl <=> (select(q0,tail)=index_0)),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f4036,plain,(
% 2.91/1.42 select(q0,tail)=index_0|~sQ48_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f4035])).
% 2.91/1.42 fof(f4038,plain,(
% 2.91/1.42 sQ47_spl|sQ48_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f4030,f4032,f4035])).
% 2.91/1.42 fof(f4040,plain,(
% 2.91/1.42 $false|~sQ47_spl),
% 2.91/1.42 inference(forward_subsumption_resolution,[status(thm)],[f4033,f346])).
% 2.91/1.42 fof(f4041,plain,(
% 2.91/1.42 ~sQ47_spl),
% 2.91/1.42 inference(contradiction_clause,[status(thm)],[f4040])).
% 2.91/1.42 fof(f4042,plain,(
% 2.91/1.42 index_9=index_0|~sQ48_spl),
% 2.91/1.42 inference(forward_demodulation,[status(thm)],[f3334,f4036])).
% 2.91/1.42 fof(f4043,plain,(
% 2.91/1.42 select(q0,head)=index_9|~sQ48_spl),
% 2.91/1.42 inference(backward_demodulation,[status(thm)],[f4042,f1270])).
% 2.91/1.42 fof(f4066,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q23,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1361,f1364])).
% 2.91/1.42 fof(f4092,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q25,X0)=select(q24,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1367,f1384])).
% 2.91/1.42 fof(f4120,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q26,X0)=select(q25,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1425,f1513])).
% 2.91/1.42 fof(f4141,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q27,X0)=select(q26,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1515,f1518])).
% 2.91/1.42 fof(f4162,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q28,X0)=select(q27,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1541,f1697])).
% 2.91/1.42 fof(f4176,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q9,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1423,f1701])).
% 2.91/1.42 fof(f4192,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q29,X0)=select(q28,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1762,f1766])).
% 2.91/1.42 fof(f4218,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q3,X0)=select(q2,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1768,f1777])).
% 2.91/1.42 fof(f4239,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q30,X0)=select(q29,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1810,f1813])).
% 2.91/1.42 fof(f4260,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q31,X0)=select(q30,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1846,f1849])).
% 2.91/1.42 fof(f4281,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q32,X0)=select(q31,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1852,f1880])).
% 2.91/1.42 fof(f4302,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q33,X0)=select(q32,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1892,f1895])).
% 2.91/1.42 fof(f4323,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q34,X0)=select(q33,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1949,f1952])).
% 2.91/1.42 fof(f4351,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q35,X0)=select(q34,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1964,f2005])).
% 2.91/1.42 fof(f4372,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q36,X0)=select(q35,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2007,f2039])).
% 2.91/1.42 fof(f4393,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q37,X0)=select(q36,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2042,f2045])).
% 2.91/1.42 fof(f4402,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q11,X0)=select(q10,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f1955,f2066])).
% 2.91/1.42 fof(f4428,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q38,X0)=select(q37,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2102,f2106])).
% 2.91/1.42 fof(f4449,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q39,X0)=select(q38,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2151,f2154])).
% 2.91/1.42 fof(f4470,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q4,X0)=select(q3,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2157,f2168])).
% 2.91/1.42 fof(f4491,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q40,X0)=select(q39,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2205,f2208])).
% 2.91/1.42 fof(f4512,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q41,X0)=select(q40,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2257,f2261])).
% 2.91/1.42 fof(f4533,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q42,X0)=select(q41,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2263,f2276])).
% 2.91/1.42 fof(f4549,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q43,X0)=select(q42,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2304,f2307])).
% 2.91/1.42 fof(f4582,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q44,X0)=select(q43,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2350,f2354])).
% 2.91/1.42 fof(f4603,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q45,X0)=select(q44,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2378,f2391])).
% 2.91/1.42 fof(f4624,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q46,X0)=select(q45,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2394,f2427])).
% 2.91/1.42 fof(f4634,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q12,X0)=select(q11,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2348,f2431])).
% 2.91/1.42 fof(f4679,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q5,X0)=select(q4,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2433,f2463])).
% 2.91/1.42 fof(f4700,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q6,X0)=select(q5,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2471,f2474])).
% 2.91/1.42 fof(f4721,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q7,X0)=select(q6,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2512,f2515])).
% 2.91/1.42 fof(f4737,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q8,X0)=select(q7,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2518,f2553])).
% 2.91/1.42 fof(f4775,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q9,X0)=select(q8,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2568,f2571])).
% 2.91/1.42 fof(f4821,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q13,X0)=select(q12,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2648,f2651])).
% 2.91/1.42 fof(f4842,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q14,X0)=select(q13,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2654,f2666])).
% 2.91/1.42 fof(f4863,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q15,X0)=select(q14,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2688,f2691])).
% 2.91/1.42 fof(f4884,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q16,X0)=select(q15,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2750,f2754])).
% 2.91/1.42 fof(f4912,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q17,X0)=select(q16,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2766,f2774])).
% 2.91/1.42 fof(f4928,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q18,X0)=select(q17,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2777,f2837])).
% 2.91/1.42 fof(f4954,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q19,X0)=select(q18,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2840,f2843])).
% 2.91/1.42 fof(f4968,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q1,X0)=select(q0,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2756,f2856])).
% 2.91/1.42 fof(f4989,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q2,X0)=select(q1,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2882,f2885])).
% 2.91/1.42 fof(f5028,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q20,X0)=select(q19,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2952,f2956])).
% 2.91/1.42 fof(f5049,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q21,X0)=select(q20,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2958,f2967])).
% 2.91/1.42 fof(f5070,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q22,X0)=select(q21,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f2999,f3002])).
% 2.91/1.42 fof(f5091,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q23,X0)=select(q22,X0)|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f3045,f3049])).
% 2.91/1.42 fof(f6042,plain,(
% 2.91/1.42 tail=head|index_279=select(q45,head)|seq=head),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f515,f4624])).
% 2.91/1.42 fof(f6051,definition,(
% 2.91/1.42 sQ254_spl <=> (index_279=select(q45,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6052,plain,(
% 2.91/1.42 index_279=select(q45,head)|~sQ254_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6051])).
% 2.91/1.42 fof(f6054,definition,(
% 2.91/1.42 sQ255_spl <=> (seq=head)),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6055,plain,(
% 2.91/1.42 seq=head|~sQ255_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6054])).
% 2.91/1.42 fof(f6057,plain,(
% 2.91/1.42 sQ47_spl|sQ254_spl|sQ255_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6042,f4032,f6051,f6054])).
% 2.91/1.42 fof(f6062,plain,(
% 2.91/1.42 index_279=select(q44,head)|tail=head|seq=head|~sQ254_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4603,f6052])).
% 2.91/1.42 fof(f6064,definition,(
% 2.91/1.42 sQ256_spl <=> (index_279=select(q44,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6065,plain,(
% 2.91/1.42 index_279=select(q44,head)|~sQ256_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6064])).
% 2.91/1.42 fof(f6067,plain,(
% 2.91/1.42 sQ256_spl|sQ47_spl|sQ255_spl|~sQ254_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6062,f6064,f4032,f6054,f6051])).
% 2.91/1.42 fof(f6069,plain,(
% 2.91/1.42 $false|~sQ255_spl),
% 2.91/1.42 inference(forward_subsumption_resolution,[status(thm)],[f6055,f347])).
% 2.91/1.42 fof(f6070,plain,(
% 2.91/1.42 ~sQ255_spl),
% 2.91/1.42 inference(contradiction_clause,[status(thm)],[f6069])).
% 2.91/1.42 fof(f6071,plain,(
% 2.91/1.42 index_279=select(q43,head)|tail=head|seq=head|~sQ256_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4582,f6065])).
% 2.91/1.42 fof(f6073,definition,(
% 2.91/1.42 sQ257_spl <=> (index_279=select(q43,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6074,plain,(
% 2.91/1.42 index_279=select(q43,head)|~sQ257_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6073])).
% 2.91/1.42 fof(f6076,plain,(
% 2.91/1.42 sQ257_spl|sQ47_spl|sQ255_spl|~sQ256_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6071,f6073,f4032,f6054,f6064])).
% 2.91/1.42 fof(f6082,plain,(
% 2.91/1.42 index_279=select(q42,head)|tail=head|seq=head|~sQ257_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4549,f6074])).
% 2.91/1.42 fof(f6084,definition,(
% 2.91/1.42 sQ258_spl <=> (index_279=select(q42,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6085,plain,(
% 2.91/1.42 index_279=select(q42,head)|~sQ258_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6084])).
% 2.91/1.42 fof(f6087,plain,(
% 2.91/1.42 sQ258_spl|sQ47_spl|sQ255_spl|~sQ257_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6082,f6084,f4032,f6054,f6073])).
% 2.91/1.42 fof(f6089,plain,(
% 2.91/1.42 index_279=select(q41,head)|tail=head|seq=head|~sQ258_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4533,f6085])).
% 2.91/1.42 fof(f6091,definition,(
% 2.91/1.42 sQ259_spl <=> (index_279=select(q41,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6092,plain,(
% 2.91/1.42 index_279=select(q41,head)|~sQ259_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6091])).
% 2.91/1.42 fof(f6094,plain,(
% 2.91/1.42 sQ259_spl|sQ47_spl|sQ255_spl|~sQ258_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6089,f6091,f4032,f6054,f6084])).
% 2.91/1.42 fof(f6096,plain,(
% 2.91/1.42 index_279=select(q40,head)|tail=head|seq=head|~sQ259_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4512,f6092])).
% 2.91/1.42 fof(f6098,definition,(
% 2.91/1.42 sQ260_spl <=> (index_279=select(q40,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6099,plain,(
% 2.91/1.42 index_279=select(q40,head)|~sQ260_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6098])).
% 2.91/1.42 fof(f6101,plain,(
% 2.91/1.42 sQ260_spl|sQ47_spl|sQ255_spl|~sQ259_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6096,f6098,f4032,f6054,f6091])).
% 2.91/1.42 fof(f6103,plain,(
% 2.91/1.42 index_279=select(q39,head)|tail=head|seq=head|~sQ260_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4491,f6099])).
% 2.91/1.42 fof(f6105,definition,(
% 2.91/1.42 sQ261_spl <=> (index_279=select(q39,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ261_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6106,plain,(
% 2.91/1.42 index_279=select(q39,head)|~sQ261_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6105])).
% 2.91/1.42 fof(f6108,plain,(
% 2.91/1.42 sQ261_spl|sQ47_spl|sQ255_spl|~sQ260_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6103,f6105,f4032,f6054,f6098])).
% 2.91/1.42 fof(f6110,plain,(
% 2.91/1.42 index_279=select(q38,head)|tail=head|seq=head|~sQ261_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4449,f6106])).
% 2.91/1.42 fof(f6112,definition,(
% 2.91/1.42 sQ262_spl <=> (index_279=select(q38,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6113,plain,(
% 2.91/1.42 index_279=select(q38,head)|~sQ262_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6112])).
% 2.91/1.42 fof(f6115,plain,(
% 2.91/1.42 sQ262_spl|sQ47_spl|sQ255_spl|~sQ261_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6110,f6112,f4032,f6054,f6105])).
% 2.91/1.42 fof(f6117,plain,(
% 2.91/1.42 index_279=select(q37,head)|tail=head|seq=head|~sQ262_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4428,f6113])).
% 2.91/1.42 fof(f6119,definition,(
% 2.91/1.42 sQ263_spl <=> (index_279=select(q37,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6120,plain,(
% 2.91/1.42 index_279=select(q37,head)|~sQ263_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6119])).
% 2.91/1.42 fof(f6122,plain,(
% 2.91/1.42 sQ263_spl|sQ47_spl|sQ255_spl|~sQ262_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6117,f6119,f4032,f6054,f6112])).
% 2.91/1.42 fof(f6124,plain,(
% 2.91/1.42 index_279=select(q36,head)|tail=head|seq=head|~sQ263_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4393,f6120])).
% 2.91/1.42 fof(f6126,definition,(
% 2.91/1.42 sQ264_spl <=> (index_279=select(q36,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6127,plain,(
% 2.91/1.42 index_279=select(q36,head)|~sQ264_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6126])).
% 2.91/1.42 fof(f6129,plain,(
% 2.91/1.42 sQ264_spl|sQ47_spl|sQ255_spl|~sQ263_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6124,f6126,f4032,f6054,f6119])).
% 2.91/1.42 fof(f6131,plain,(
% 2.91/1.42 index_279=select(q35,head)|tail=head|seq=head|~sQ264_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4372,f6127])).
% 2.91/1.42 fof(f6133,definition,(
% 2.91/1.42 sQ265_spl <=> (index_279=select(q35,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6134,plain,(
% 2.91/1.42 index_279=select(q35,head)|~sQ265_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6133])).
% 2.91/1.42 fof(f6136,plain,(
% 2.91/1.42 sQ265_spl|sQ47_spl|sQ255_spl|~sQ264_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6131,f6133,f4032,f6054,f6126])).
% 2.91/1.42 fof(f6138,plain,(
% 2.91/1.42 index_279=select(q34,head)|tail=head|seq=head|~sQ265_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4351,f6134])).
% 2.91/1.42 fof(f6140,definition,(
% 2.91/1.42 sQ266_spl <=> (index_279=select(q34,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6141,plain,(
% 2.91/1.42 index_279=select(q34,head)|~sQ266_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6140])).
% 2.91/1.42 fof(f6143,plain,(
% 2.91/1.42 sQ266_spl|sQ47_spl|sQ255_spl|~sQ265_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6138,f6140,f4032,f6054,f6133])).
% 2.91/1.42 fof(f6145,plain,(
% 2.91/1.42 index_279=select(q33,head)|tail=head|seq=head|~sQ266_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4323,f6141])).
% 2.91/1.42 fof(f6147,definition,(
% 2.91/1.42 sQ267_spl <=> (index_279=select(q33,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6148,plain,(
% 2.91/1.42 index_279=select(q33,head)|~sQ267_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6147])).
% 2.91/1.42 fof(f6150,plain,(
% 2.91/1.42 sQ267_spl|sQ47_spl|sQ255_spl|~sQ266_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6145,f6147,f4032,f6054,f6140])).
% 2.91/1.42 fof(f6152,plain,(
% 2.91/1.42 index_279=select(q32,head)|tail=head|seq=head|~sQ267_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4302,f6148])).
% 2.91/1.42 fof(f6154,definition,(
% 2.91/1.42 sQ268_spl <=> (index_279=select(q32,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6155,plain,(
% 2.91/1.42 index_279=select(q32,head)|~sQ268_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6154])).
% 2.91/1.42 fof(f6157,plain,(
% 2.91/1.42 sQ268_spl|sQ47_spl|sQ255_spl|~sQ267_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6152,f6154,f4032,f6054,f6147])).
% 2.91/1.42 fof(f6159,plain,(
% 2.91/1.42 index_279=select(q31,head)|tail=head|seq=head|~sQ268_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4281,f6155])).
% 2.91/1.42 fof(f6161,definition,(
% 2.91/1.42 sQ269_spl <=> (index_279=select(q31,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6162,plain,(
% 2.91/1.42 index_279=select(q31,head)|~sQ269_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6161])).
% 2.91/1.42 fof(f6164,plain,(
% 2.91/1.42 sQ269_spl|sQ47_spl|sQ255_spl|~sQ268_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6159,f6161,f4032,f6054,f6154])).
% 2.91/1.42 fof(f6166,plain,(
% 2.91/1.42 index_279=select(q30,head)|tail=head|seq=head|~sQ269_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4260,f6162])).
% 2.91/1.42 fof(f6168,definition,(
% 2.91/1.42 sQ270_spl <=> (index_279=select(q30,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6169,plain,(
% 2.91/1.42 index_279=select(q30,head)|~sQ270_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6168])).
% 2.91/1.42 fof(f6171,plain,(
% 2.91/1.42 sQ270_spl|sQ47_spl|sQ255_spl|~sQ269_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6166,f6168,f4032,f6054,f6161])).
% 2.91/1.42 fof(f6184,plain,(
% 2.91/1.42 index_279=select(q29,head)|tail=head|seq=head|~sQ270_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4239,f6169])).
% 2.91/1.42 fof(f6186,definition,(
% 2.91/1.42 sQ272_spl <=> (index_279=select(q29,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6187,plain,(
% 2.91/1.42 index_279=select(q29,head)|~sQ272_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6186])).
% 2.91/1.42 fof(f6189,plain,(
% 2.91/1.42 sQ272_spl|sQ47_spl|sQ255_spl|~sQ270_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6184,f6186,f4032,f6054,f6168])).
% 2.91/1.42 fof(f6191,plain,(
% 2.91/1.42 index_279=select(q28,head)|tail=head|seq=head|~sQ272_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4192,f6187])).
% 2.91/1.42 fof(f6193,definition,(
% 2.91/1.42 sQ273_spl <=> (index_279=select(q28,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6194,plain,(
% 2.91/1.42 index_279=select(q28,head)|~sQ273_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6193])).
% 2.91/1.42 fof(f6196,plain,(
% 2.91/1.42 sQ273_spl|sQ47_spl|sQ255_spl|~sQ272_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6191,f6193,f4032,f6054,f6186])).
% 2.91/1.42 fof(f6198,plain,(
% 2.91/1.42 index_279=select(q27,head)|tail=head|seq=head|~sQ273_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4162,f6194])).
% 2.91/1.42 fof(f6200,definition,(
% 2.91/1.42 sQ274_spl <=> (index_279=select(q27,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6201,plain,(
% 2.91/1.42 index_279=select(q27,head)|~sQ274_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6200])).
% 2.91/1.42 fof(f6203,plain,(
% 2.91/1.42 sQ274_spl|sQ47_spl|sQ255_spl|~sQ273_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6198,f6200,f4032,f6054,f6193])).
% 2.91/1.42 fof(f6205,plain,(
% 2.91/1.42 index_279=select(q26,head)|tail=head|seq=head|~sQ274_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4141,f6201])).
% 2.91/1.42 fof(f6207,definition,(
% 2.91/1.42 sQ275_spl <=> (index_279=select(q26,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ275_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6208,plain,(
% 2.91/1.42 index_279=select(q26,head)|~sQ275_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6207])).
% 2.91/1.42 fof(f6210,plain,(
% 2.91/1.42 sQ275_spl|sQ47_spl|sQ255_spl|~sQ274_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6205,f6207,f4032,f6054,f6200])).
% 2.91/1.42 fof(f6212,plain,(
% 2.91/1.42 index_279=select(q25,head)|tail=head|seq=head|~sQ275_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4120,f6208])).
% 2.91/1.42 fof(f6214,definition,(
% 2.91/1.42 sQ276_spl <=> (index_279=select(q25,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6215,plain,(
% 2.91/1.42 index_279=select(q25,head)|~sQ276_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6214])).
% 2.91/1.42 fof(f6217,plain,(
% 2.91/1.42 sQ276_spl|sQ47_spl|sQ255_spl|~sQ275_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6212,f6214,f4032,f6054,f6207])).
% 2.91/1.42 fof(f6219,plain,(
% 2.91/1.42 index_279=select(q24,head)|tail=head|seq=head|~sQ276_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4092,f6215])).
% 2.91/1.42 fof(f6221,definition,(
% 2.91/1.42 sQ277_spl <=> (index_279=select(q24,head))),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6222,plain,(
% 2.91/1.42 index_279=select(q24,head)|~sQ277_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6221])).
% 2.91/1.42 fof(f6224,plain,(
% 2.91/1.42 sQ277_spl|sQ47_spl|sQ255_spl|~sQ276_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6219,f6221,f4032,f6054,f6214])).
% 2.91/1.42 fof(f6272,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q8,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4176,f4775])).
% 2.91/1.42 fof(f6281,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q8,X0)|seq=X0)),
% 2.91/1.42 inference(duplicate_literals_removal,[status(thm)],[f6272])).
% 2.91/1.42 fof(f6375,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q2,X0)=select(q0,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4968,f4989])).
% 2.91/1.42 fof(f6387,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q2,X0)=select(q0,X0)|seq=X0)),
% 2.91/1.42 inference(duplicate_literals_removal,[status(thm)],[f6375])).
% 2.91/1.42 fof(f6426,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q22,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4066,f5091])).
% 2.91/1.42 fof(f6435,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q22,X0)|seq=X0)),
% 2.91/1.42 inference(duplicate_literals_removal,[status(thm)],[f6426])).
% 2.91/1.42 fof(f6473,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q7,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4737,f6281])).
% 2.91/1.42 fof(f6482,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q7,X0)|seq=X0)),
% 2.91/1.42 inference(duplicate_literals_removal,[status(thm)],[f6473])).
% 2.91/1.42 fof(f6486,plain,(
% 2.91/1.42 tail=head|select(q2,head)=index_9|seq=head|~sQ48_spl),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4043,f6387])).
% 2.91/1.42 fof(f6492,definition,(
% 2.91/1.42 sQ302_spl <=> (select(q2,head)=index_9)),
% 2.91/1.42 introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition])).
% 2.91/1.42 fof(f6493,plain,(
% 2.91/1.42 select(q2,head)=index_9|~sQ302_spl),
% 2.91/1.42 inference(component_clause,[status(thm)],[f6492])).
% 2.91/1.42 fof(f6495,plain,(
% 2.91/1.42 sQ47_spl|sQ302_spl|sQ255_spl|~sQ48_spl),
% 2.91/1.42 inference(split_clause,[status(thm)],[f6486,f4032,f6492,f6054,f4035])).
% 2.91/1.42 fof(f6506,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q21,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f5070,f6435])).
% 2.91/1.42 fof(f6515,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q21,X0)|seq=X0)),
% 2.91/1.42 inference(duplicate_literals_removal,[status(thm)],[f6506])).
% 2.91/1.42 fof(f6521,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q6,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4721,f6482])).
% 2.91/1.42 fof(f6533,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q6,X0)|seq=X0)),
% 2.91/1.42 inference(duplicate_literals_removal,[status(thm)],[f6521])).
% 2.91/1.42 fof(f6561,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q20,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f5049,f6515])).
% 2.91/1.42 fof(f6573,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q20,X0)|seq=X0)),
% 2.91/1.42 inference(duplicate_literals_removal,[status(thm)],[f6561])).
% 2.91/1.42 fof(f6579,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q5,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f4700,f6533])).
% 2.91/1.42 fof(f6588,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q10,X0)=select(q5,X0)|seq=X0)),
% 2.91/1.42 inference(duplicate_literals_removal,[status(thm)],[f6579])).
% 2.91/1.42 fof(f6594,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q19,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.42 inference(paramodulation,[status(thm)],[f5028,f6573])).
% 2.91/1.42 fof(f6603,plain,(
% 2.91/1.42 ![X0]: (tail=X0|select(q24,X0)=select(q19,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6594])).
% 2.91/1.43 fof(f6609,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q10,X0)=select(q4,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4679,f6588])).
% 2.91/1.43 fof(f6618,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q10,X0)=select(q4,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6609])).
% 2.91/1.43 fof(f6624,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q18,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4954,f6603])).
% 2.91/1.43 fof(f6633,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q18,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6624])).
% 2.91/1.43 fof(f6639,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q10,X0)=select(q3,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4470,f6618])).
% 2.91/1.43 fof(f6648,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q10,X0)=select(q3,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6639])).
% 2.91/1.43 fof(f6654,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q17,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4928,f6633])).
% 2.91/1.43 fof(f6663,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q17,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6654])).
% 2.91/1.43 fof(f6669,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q10,X0)=select(q2,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4218,f6648])).
% 2.91/1.43 fof(f6678,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q10,X0)=select(q2,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6669])).
% 2.91/1.43 fof(f6684,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q16,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4912,f6663])).
% 2.91/1.43 fof(f6693,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q16,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6684])).
% 2.91/1.43 fof(f6721,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q15,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4884,f6693])).
% 2.91/1.43 fof(f6730,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q15,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6721])).
% 2.91/1.43 fof(f6736,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q14,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4863,f6730])).
% 2.91/1.43 fof(f6745,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q14,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6736])).
% 2.91/1.43 fof(f6751,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q13,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4842,f6745])).
% 2.91/1.43 fof(f6760,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q13,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6751])).
% 2.91/1.43 fof(f6766,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q12,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4821,f6760])).
% 2.91/1.43 fof(f6775,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q12,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6766])).
% 2.91/1.43 fof(f6781,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q11,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4634,f6775])).
% 2.91/1.43 fof(f6790,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q11,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6781])).
% 2.91/1.43 fof(f6796,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q10,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f4402,f6790])).
% 2.91/1.43 fof(f6805,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q10,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6796])).
% 2.91/1.43 fof(f6811,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q2,X0)|seq=X0|tail=X0|seq=X0)),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f6678,f6805])).
% 2.91/1.43 fof(f6820,plain,(
% 2.91/1.43 ![X0]: (tail=X0|select(q24,X0)=select(q2,X0)|seq=X0)),
% 2.91/1.43 inference(duplicate_literals_removal,[status(thm)],[f6811])).
% 2.91/1.43 fof(f6824,plain,(
% 2.91/1.43 tail=head|select(q24,head)=index_9|seq=head|~sQ302_spl),
% 2.91/1.43 inference(paramodulation,[status(thm)],[f6493,f6820])).
% 2.91/1.43 fof(f6830,definition,(
% 2.91/1.43 sQ328_spl <=> (select(q24,head)=index_9)),
% 2.91/1.43 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 2.91/1.43 fof(f6831,plain,(
% 2.91/1.43 select(q24,head)=index_9|~sQ328_spl),
% 2.91/1.43 inference(component_clause,[status(thm)],[f6830])).
% 2.91/1.43 fof(f6833,plain,(
% 2.91/1.43 sQ47_spl|sQ328_spl|sQ255_spl|~sQ302_spl),
% 2.91/1.43 inference(split_clause,[status(thm)],[f6824,f4032,f6830,f6054,f6492])).
% 2.91/1.43 fof(f6842,plain,(
% 2.91/1.43 index_279=index_9|~sQ328_spl|~sQ277_spl),
% 2.91/1.43 inference(backward_demodulation,[status(thm)],[f6831,f6222])).
% 2.91/1.43 fof(f6887,plain,(
% 2.91/1.43 elem_280=select(earray_278,index_9)|~sQ328_spl|~sQ277_spl),
% 2.91/1.43 inference(backward_demodulation,[status(thm)],[f6842,f447])).
% 2.91/1.43 fof(f6888,plain,(
% 2.91/1.43 elem_283=elem_280|~sQ328_spl|~sQ277_spl),
% 2.91/1.43 inference(backward_demodulation,[status(thm)],[f6887,f3423])).
% 2.91/1.43 fof(f6889,plain,(
% 2.91/1.43 $false|~sQ328_spl|~sQ277_spl),
% 2.91/1.43 inference(forward_subsumption_resolution,[status(thm)],[f6888,f685])).
% 2.91/1.43 fof(f6890,plain,(
% 2.91/1.43 ~sQ328_spl|~sQ277_spl),
% 2.91/1.43 inference(contradiction_clause,[status(thm)],[f6889])).
% 2.91/1.43 fof(f6891,plain,(
% 2.91/1.43 $false),
% 2.91/1.43 inference(sat_refutation,[status(thm)],[f4038,f4041,f6057,f6067,f6070,f6076,f6087,f6094,f6101,f6108,f6115,f6122,f6129,f6136,f6143,f6150,f6157,f6164,f6171,f6189,f6196,f6203,f6210,f6217,f6224,f6495,f6833,f6890])).
% 2.91/1.43 % SZS output end CNFRefutation for theBenchmark.p
% 2.91/1.43 % Elapsed time: 0.485090 seconds
% 2.91/1.43 % CPU time: 3.546430 seconds
% 2.91/1.43 % Total memory used: 158.018 MB
% 2.91/1.43 % Net memory used: 155.021 MB
%------------------------------------------------------------------------------