%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV571-1.049 : 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 : n003.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:51 PM UTC 2026
% Result : Unsatisfiable 0.29s 1.07s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV571-1.049 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n003.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 09:12:46 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.46 % Drodi V4.1.1
% 0.29/1.07 % Refutation found
% 0.29/1.07 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.29/1.07 % SZS output start CNFRefutation for theBenchmark
% 0.29/1.07 fof(f1,axiom,(
% 0.29/1.07 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f2,axiom,(
% 0.29/1.07 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f3,axiom,(
% 0.29/1.07 head != tail ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f4,axiom,(
% 0.29/1.07 head != seq ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f6,axiom,(
% 0.29/1.07 (![X]: (p(s(X)) = X ))),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f7,axiom,(
% 0.29/1.07 (![X]: (s(p(X)) = X ))),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f10,axiom,(
% 0.29/1.07 (![X]: (s(s(s(X))) = X ))),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f110,hypothesis,(
% 0.29/1.07 elem_298 = select(earray_296,index_297) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f111,hypothesis,(
% 0.29/1.07 elem_301 = select(earray_296,index_300) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f112,hypothesis,(
% 0.29/1.07 index_0 = select(q,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f113,hypothesis,(
% 0.29/1.07 index_102 = s(index_99) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f114,hypothesis,(
% 0.29/1.07 index_105 = select(q24,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f115,hypothesis,(
% 0.29/1.07 index_108 = s(index_105) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f116,hypothesis,(
% 0.29/1.07 index_111 = select(q25,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f117,hypothesis,(
% 0.29/1.07 index_114 = s(index_111) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f118,hypothesis,(
% 0.29/1.07 index_117 = select(q26,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f119,hypothesis,(
% 0.29/1.07 index_12 = s(index_9) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f120,hypothesis,(
% 0.29/1.07 index_120 = s(index_117) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f121,hypothesis,(
% 0.29/1.07 index_123 = select(q27,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f122,hypothesis,(
% 0.29/1.07 index_126 = s(index_123) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f123,hypothesis,(
% 0.29/1.07 index_129 = select(q28,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f124,hypothesis,(
% 0.29/1.07 index_132 = s(index_129) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f125,hypothesis,(
% 0.29/1.07 index_135 = select(q2,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f126,hypothesis,(
% 0.29/1.07 index_138 = s(index_135) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f127,hypothesis,(
% 0.29/1.07 index_141 = select(q29,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f128,hypothesis,(
% 0.29/1.07 index_144 = s(index_141) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f129,hypothesis,(
% 0.29/1.07 index_147 = select(q30,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f130,hypothesis,(
% 0.29/1.07 index_15 = select(q10,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f131,hypothesis,(
% 0.29/1.07 index_150 = s(index_147) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f132,hypothesis,(
% 0.29/1.07 index_153 = select(q31,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f133,hypothesis,(
% 0.29/1.07 index_156 = s(index_153) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f134,hypothesis,(
% 0.29/1.07 index_159 = select(q32,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f135,hypothesis,(
% 0.29/1.07 index_162 = s(index_159) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f136,hypothesis,(
% 0.29/1.07 index_165 = select(q33,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f137,hypothesis,(
% 0.29/1.07 index_168 = s(index_165) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f138,hypothesis,(
% 0.29/1.07 index_171 = select(q34,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f139,hypothesis,(
% 0.29/1.07 index_174 = s(index_171) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f140,hypothesis,(
% 0.29/1.07 index_177 = select(q35,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f141,hypothesis,(
% 0.29/1.07 index_18 = s(index_15) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f142,hypothesis,(
% 0.29/1.07 index_180 = s(index_177) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f143,hypothesis,(
% 0.29/1.07 index_183 = select(q36,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f144,hypothesis,(
% 0.29/1.07 index_186 = s(index_183) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f145,hypothesis,(
% 0.29/1.07 index_189 = select(q37,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f146,hypothesis,(
% 0.29/1.07 index_192 = s(index_189) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f147,hypothesis,(
% 0.29/1.07 index_195 = select(q38,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f148,hypothesis,(
% 0.29/1.07 index_198 = s(index_195) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f149,hypothesis,(
% 0.29/1.07 index_201 = select(q3,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f150,hypothesis,(
% 0.29/1.07 index_204 = s(index_201) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f151,hypothesis,(
% 0.29/1.07 index_207 = select(q39,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f152,hypothesis,(
% 0.29/1.07 index_21 = select(q11,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f153,hypothesis,(
% 0.29/1.07 index_210 = s(index_207) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f154,hypothesis,(
% 0.29/1.07 index_213 = select(q40,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f155,hypothesis,(
% 0.29/1.07 index_216 = s(index_213) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f156,hypothesis,(
% 0.29/1.07 index_219 = select(q41,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f157,hypothesis,(
% 0.29/1.07 index_222 = s(index_219) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f158,hypothesis,(
% 0.29/1.07 index_225 = select(q42,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f159,hypothesis,(
% 0.29/1.07 index_228 = s(index_225) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f160,hypothesis,(
% 0.29/1.07 index_231 = select(q43,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f161,hypothesis,(
% 0.29/1.07 index_234 = s(index_231) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f162,hypothesis,(
% 0.29/1.07 index_237 = select(q44,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f163,hypothesis,(
% 0.29/1.07 index_24 = s(index_21) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f164,hypothesis,(
% 0.29/1.07 index_240 = s(index_237) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f165,hypothesis,(
% 0.29/1.07 index_243 = select(q45,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f166,hypothesis,(
% 0.29/1.07 index_246 = s(index_243) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f167,hypothesis,(
% 0.29/1.07 index_249 = select(q46,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f168,hypothesis,(
% 0.29/1.07 index_252 = s(index_249) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f169,hypothesis,(
% 0.29/1.07 index_255 = select(q47,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f170,hypothesis,(
% 0.29/1.07 index_258 = s(index_255) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f171,hypothesis,(
% 0.29/1.07 index_261 = select(q48,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f172,hypothesis,(
% 0.29/1.07 index_264 = s(index_261) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f173,hypothesis,(
% 0.29/1.07 index_267 = select(q4,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f174,hypothesis,(
% 0.29/1.07 index_27 = select(q12,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f175,hypothesis,(
% 0.29/1.07 index_270 = s(index_267) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f176,hypothesis,(
% 0.29/1.07 index_273 = select(q5,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f177,hypothesis,(
% 0.29/1.07 index_276 = s(index_273) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f178,hypothesis,(
% 0.29/1.07 index_279 = select(q6,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f179,hypothesis,(
% 0.29/1.07 index_282 = s(index_279) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f180,hypothesis,(
% 0.29/1.07 index_285 = select(q7,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f181,hypothesis,(
% 0.29/1.07 index_288 = s(index_285) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f182,hypothesis,(
% 0.29/1.07 index_291 = select(q8,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f183,hypothesis,(
% 0.29/1.07 index_294 = s(index_291) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f184,hypothesis,(
% 0.29/1.07 index_297 = select(q49,head) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f185,hypothesis,(
% 0.29/1.07 index_299 = select(q49,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f186,hypothesis,(
% 0.29/1.07 index_3 = select(q0,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f187,hypothesis,(
% 0.29/1.07 index_30 = s(index_27) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f188,hypothesis,(
% 0.29/1.07 s(index_300) = index_299 ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f189,hypothesis,(
% 0.29/1.07 index_33 = select(q13,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f190,hypothesis,(
% 0.29/1.07 index_36 = s(index_33) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f191,hypothesis,(
% 0.29/1.07 index_39 = select(q14,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f192,hypothesis,(
% 0.29/1.07 index_42 = s(index_39) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f193,hypothesis,(
% 0.29/1.07 index_45 = select(q15,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f194,hypothesis,(
% 0.29/1.07 index_48 = s(index_45) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f195,hypothesis,(
% 0.29/1.07 index_51 = select(q16,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f196,hypothesis,(
% 0.29/1.07 index_54 = s(index_51) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f197,hypothesis,(
% 0.29/1.07 index_57 = select(q17,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f198,hypothesis,(
% 0.29/1.07 index_6 = s(index_3) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f199,hypothesis,(
% 0.29/1.07 index_60 = s(index_57) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f200,hypothesis,(
% 0.29/1.07 index_63 = select(q18,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f201,hypothesis,(
% 0.29/1.07 index_66 = s(index_63) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f202,hypothesis,(
% 0.29/1.07 index_69 = select(q1,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f203,hypothesis,(
% 0.29/1.07 index_72 = s(index_69) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f204,hypothesis,(
% 0.29/1.07 index_75 = select(q19,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f205,hypothesis,(
% 0.29/1.07 index_78 = s(index_75) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f206,hypothesis,(
% 0.29/1.07 index_81 = select(q20,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f207,hypothesis,(
% 0.29/1.07 index_84 = s(index_81) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f208,hypothesis,(
% 0.29/1.07 index_87 = select(q21,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f209,hypothesis,(
% 0.29/1.07 index_9 = select(q9,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f210,hypothesis,(
% 0.29/1.07 index_90 = s(index_87) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f211,hypothesis,(
% 0.29/1.07 index_93 = select(q22,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f212,hypothesis,(
% 0.29/1.07 index_96 = s(index_93) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f213,hypothesis,(
% 0.29/1.07 index_99 = select(q23,tail) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f214,hypothesis,(
% 0.29/1.07 queue_1 = store(q,head,index_0) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f215,hypothesis,(
% 0.29/1.07 queue_101 = store(q23,seq,earray_100) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f216,hypothesis,(
% 0.29/1.07 queue_103 = store(queue_101,tail,index_102) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f217,hypothesis,(
% 0.29/1.07 queue_107 = store(q24,seq,earray_106) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f218,hypothesis,(
% 0.29/1.07 queue_109 = store(queue_107,tail,index_108) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f219,hypothesis,(
% 0.29/1.07 queue_11 = store(q9,seq,earray_10) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f220,hypothesis,(
% 0.29/1.07 queue_113 = store(q25,seq,earray_112) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f221,hypothesis,(
% 0.29/1.07 queue_115 = store(queue_113,tail,index_114) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f222,hypothesis,(
% 0.29/1.07 queue_119 = store(q26,seq,earray_118) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f223,hypothesis,(
% 0.29/1.07 queue_121 = store(queue_119,tail,index_120) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f224,hypothesis,(
% 0.29/1.07 queue_125 = store(q27,seq,earray_124) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f225,hypothesis,(
% 0.29/1.07 queue_127 = store(queue_125,tail,index_126) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f226,hypothesis,(
% 0.29/1.07 queue_13 = store(queue_11,tail,index_12) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f227,hypothesis,(
% 0.29/1.07 queue_131 = store(q28,seq,earray_130) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f228,hypothesis,(
% 0.29/1.07 queue_133 = store(queue_131,tail,index_132) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f229,hypothesis,(
% 0.29/1.07 queue_137 = store(q2,seq,earray_136) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f230,hypothesis,(
% 0.29/1.07 queue_139 = store(queue_137,tail,index_138) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f231,hypothesis,(
% 0.29/1.07 queue_143 = store(q29,seq,earray_142) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f232,hypothesis,(
% 0.29/1.07 queue_145 = store(queue_143,tail,index_144) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f233,hypothesis,(
% 0.29/1.07 queue_149 = store(q30,seq,earray_148) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f234,hypothesis,(
% 0.29/1.07 queue_151 = store(queue_149,tail,index_150) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f235,hypothesis,(
% 0.29/1.07 queue_155 = store(q31,seq,earray_154) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f236,hypothesis,(
% 0.29/1.07 queue_157 = store(queue_155,tail,index_156) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f237,hypothesis,(
% 0.29/1.07 queue_161 = store(q32,seq,earray_160) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f238,hypothesis,(
% 0.29/1.07 queue_163 = store(queue_161,tail,index_162) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f239,hypothesis,(
% 0.29/1.07 queue_167 = store(q33,seq,earray_166) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f240,hypothesis,(
% 0.29/1.07 queue_169 = store(queue_167,tail,index_168) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f241,hypothesis,(
% 0.29/1.07 queue_17 = store(q10,seq,earray_16) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f242,hypothesis,(
% 0.29/1.07 queue_173 = store(q34,seq,earray_172) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f243,hypothesis,(
% 0.29/1.07 queue_175 = store(queue_173,tail,index_174) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f244,hypothesis,(
% 0.29/1.07 queue_179 = store(q35,seq,earray_178) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f245,hypothesis,(
% 0.29/1.07 queue_181 = store(queue_179,tail,index_180) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f246,hypothesis,(
% 0.29/1.07 queue_185 = store(q36,seq,earray_184) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f247,hypothesis,(
% 0.29/1.07 queue_187 = store(queue_185,tail,index_186) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f248,hypothesis,(
% 0.29/1.07 queue_19 = store(queue_17,tail,index_18) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f249,hypothesis,(
% 0.29/1.07 queue_191 = store(q37,seq,earray_190) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f250,hypothesis,(
% 0.29/1.07 queue_193 = store(queue_191,tail,index_192) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f251,hypothesis,(
% 0.29/1.07 queue_197 = store(q38,seq,earray_196) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f252,hypothesis,(
% 0.29/1.07 queue_199 = store(queue_197,tail,index_198) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f253,hypothesis,(
% 0.29/1.07 queue_203 = store(q3,seq,earray_202) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f254,hypothesis,(
% 0.29/1.07 queue_205 = store(queue_203,tail,index_204) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f255,hypothesis,(
% 0.29/1.07 queue_209 = store(q39,seq,earray_208) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f256,hypothesis,(
% 0.29/1.07 queue_211 = store(queue_209,tail,index_210) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f257,hypothesis,(
% 0.29/1.07 queue_215 = store(q40,seq,earray_214) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f258,hypothesis,(
% 0.29/1.07 queue_217 = store(queue_215,tail,index_216) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f259,hypothesis,(
% 0.29/1.07 queue_221 = store(q41,seq,earray_220) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f260,hypothesis,(
% 0.29/1.07 queue_223 = store(queue_221,tail,index_222) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f261,hypothesis,(
% 0.29/1.07 queue_227 = store(q42,seq,earray_226) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f262,hypothesis,(
% 0.29/1.07 queue_229 = store(queue_227,tail,index_228) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f263,hypothesis,(
% 0.29/1.07 queue_23 = store(q11,seq,earray_22) ),
% 0.29/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.07 fof(f264,hypothesis,(
% 0.29/1.07 queue_233 = store(q43,seq,earray_232) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f265,hypothesis,(
% 0.29/1.08 queue_235 = store(queue_233,tail,index_234) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f266,hypothesis,(
% 0.29/1.08 queue_239 = store(q44,seq,earray_238) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f267,hypothesis,(
% 0.29/1.08 queue_241 = store(queue_239,tail,index_240) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f268,hypothesis,(
% 0.29/1.08 queue_245 = store(q45,seq,earray_244) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f269,hypothesis,(
% 0.29/1.08 queue_247 = store(queue_245,tail,index_246) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f270,hypothesis,(
% 0.29/1.08 queue_25 = store(queue_23,tail,index_24) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f271,hypothesis,(
% 0.29/1.08 queue_251 = store(q46,seq,earray_250) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f272,hypothesis,(
% 0.29/1.08 queue_253 = store(queue_251,tail,index_252) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f273,hypothesis,(
% 0.29/1.08 queue_257 = store(q47,seq,earray_256) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f274,hypothesis,(
% 0.29/1.08 queue_259 = store(queue_257,tail,index_258) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f275,hypothesis,(
% 0.29/1.08 queue_263 = store(q48,seq,earray_262) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f276,hypothesis,(
% 0.29/1.08 queue_265 = store(queue_263,tail,index_264) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f277,hypothesis,(
% 0.29/1.08 queue_269 = store(q4,seq,earray_268) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f278,hypothesis,(
% 0.29/1.08 queue_271 = store(queue_269,tail,index_270) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f279,hypothesis,(
% 0.29/1.08 queue_275 = store(q5,seq,earray_274) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f280,hypothesis,(
% 0.29/1.08 queue_277 = store(queue_275,tail,index_276) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f281,hypothesis,(
% 0.29/1.08 queue_281 = store(q6,seq,earray_280) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f282,hypothesis,(
% 0.29/1.08 queue_283 = store(queue_281,tail,index_282) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f283,hypothesis,(
% 0.29/1.08 queue_287 = store(q7,seq,earray_286) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f284,hypothesis,(
% 0.29/1.08 queue_289 = store(queue_287,tail,index_288) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f285,hypothesis,(
% 0.29/1.08 queue_29 = store(q12,seq,earray_28) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f286,hypothesis,(
% 0.29/1.08 queue_293 = store(q8,seq,earray_292) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f287,hypothesis,(
% 0.29/1.08 queue_295 = store(queue_293,tail,index_294) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f288,hypothesis,(
% 0.29/1.08 queue_31 = store(queue_29,tail,index_30) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f289,hypothesis,(
% 0.29/1.08 queue_35 = store(q13,seq,earray_34) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f290,hypothesis,(
% 0.29/1.08 queue_37 = store(queue_35,tail,index_36) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f291,hypothesis,(
% 0.29/1.08 queue_41 = store(q14,seq,earray_40) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f292,hypothesis,(
% 0.29/1.08 queue_43 = store(queue_41,tail,index_42) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f293,hypothesis,(
% 0.29/1.08 queue_47 = store(q15,seq,earray_46) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f294,hypothesis,(
% 0.29/1.08 queue_49 = store(queue_47,tail,index_48) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f295,hypothesis,(
% 0.29/1.08 queue_5 = store(q0,seq,earray_4) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f296,hypothesis,(
% 0.29/1.08 queue_53 = store(q16,seq,earray_52) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f297,hypothesis,(
% 0.29/1.08 queue_55 = store(queue_53,tail,index_54) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f298,hypothesis,(
% 0.29/1.08 queue_59 = store(q17,seq,earray_58) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f299,hypothesis,(
% 0.29/1.08 queue_61 = store(queue_59,tail,index_60) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f300,hypothesis,(
% 0.29/1.08 queue_65 = store(q18,seq,earray_64) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f301,hypothesis,(
% 0.29/1.08 queue_67 = store(queue_65,tail,index_66) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f302,hypothesis,(
% 0.29/1.08 queue_7 = store(queue_5,tail,index_6) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f303,hypothesis,(
% 0.29/1.08 queue_71 = store(q1,seq,earray_70) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f304,hypothesis,(
% 0.29/1.08 queue_73 = store(queue_71,tail,index_72) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f305,hypothesis,(
% 0.29/1.08 queue_77 = store(q19,seq,earray_76) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f306,hypothesis,(
% 0.29/1.08 queue_79 = store(queue_77,tail,index_78) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f307,hypothesis,(
% 0.29/1.08 queue_83 = store(q20,seq,earray_82) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f308,hypothesis,(
% 0.29/1.08 queue_85 = store(queue_83,tail,index_84) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f309,hypothesis,(
% 0.29/1.08 queue_89 = store(q21,seq,earray_88) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f310,hypothesis,(
% 0.29/1.08 queue_91 = store(queue_89,tail,index_90) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f311,hypothesis,(
% 0.29/1.08 queue_95 = store(q22,seq,earray_94) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f312,hypothesis,(
% 0.29/1.08 queue_97 = store(queue_95,tail,index_96) ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f313,hypothesis,(
% 0.29/1.08 q0 = queue_1 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f314,hypothesis,(
% 0.29/1.08 q1 = queue_7 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f315,hypothesis,(
% 0.29/1.08 q10 = queue_13 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f316,hypothesis,(
% 0.29/1.08 q11 = queue_19 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f317,hypothesis,(
% 0.29/1.08 q12 = queue_25 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f318,hypothesis,(
% 0.29/1.08 q13 = queue_31 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f319,hypothesis,(
% 0.29/1.08 q14 = queue_37 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f320,hypothesis,(
% 0.29/1.08 q15 = queue_43 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f321,hypothesis,(
% 0.29/1.08 q16 = queue_49 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f322,hypothesis,(
% 0.29/1.08 q17 = queue_55 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f323,hypothesis,(
% 0.29/1.08 q18 = queue_61 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f324,hypothesis,(
% 0.29/1.08 q19 = queue_67 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f325,hypothesis,(
% 0.29/1.08 q2 = queue_73 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f326,hypothesis,(
% 0.29/1.08 q20 = queue_79 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f327,hypothesis,(
% 0.29/1.08 q21 = queue_85 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f328,hypothesis,(
% 0.29/1.08 q22 = queue_91 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f329,hypothesis,(
% 0.29/1.08 q23 = queue_97 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f330,hypothesis,(
% 0.29/1.08 q24 = queue_103 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f331,hypothesis,(
% 0.29/1.08 q25 = queue_109 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f332,hypothesis,(
% 0.29/1.08 q26 = queue_115 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f333,hypothesis,(
% 0.29/1.08 q27 = queue_121 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f334,hypothesis,(
% 0.29/1.08 q28 = queue_127 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f335,hypothesis,(
% 0.29/1.08 q29 = queue_133 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f336,hypothesis,(
% 0.29/1.08 q3 = queue_139 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f337,hypothesis,(
% 0.29/1.08 q30 = queue_145 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f338,hypothesis,(
% 0.29/1.08 q31 = queue_151 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f339,hypothesis,(
% 0.29/1.08 q32 = queue_157 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f340,hypothesis,(
% 0.29/1.08 q33 = queue_163 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f341,hypothesis,(
% 0.29/1.08 q34 = queue_169 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f342,hypothesis,(
% 0.29/1.08 q35 = queue_175 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f343,hypothesis,(
% 0.29/1.08 q36 = queue_181 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f344,hypothesis,(
% 0.29/1.08 q37 = queue_187 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f345,hypothesis,(
% 0.29/1.08 q38 = queue_193 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f346,hypothesis,(
% 0.29/1.08 q39 = queue_199 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f347,hypothesis,(
% 0.29/1.08 q4 = queue_205 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f348,hypothesis,(
% 0.29/1.08 q40 = queue_211 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f349,hypothesis,(
% 0.29/1.08 q41 = queue_217 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f350,hypothesis,(
% 0.29/1.08 q42 = queue_223 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f351,hypothesis,(
% 0.29/1.08 q43 = queue_229 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f352,hypothesis,(
% 0.29/1.08 q44 = queue_235 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f353,hypothesis,(
% 0.29/1.08 q45 = queue_241 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f354,hypothesis,(
% 0.29/1.08 q46 = queue_247 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f355,hypothesis,(
% 0.29/1.08 q47 = queue_253 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f356,hypothesis,(
% 0.29/1.08 q48 = queue_259 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f357,hypothesis,(
% 0.29/1.08 q49 = queue_265 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f358,hypothesis,(
% 0.29/1.08 q5 = queue_271 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f359,hypothesis,(
% 0.29/1.08 q6 = queue_277 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f360,hypothesis,(
% 0.29/1.08 q7 = queue_283 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f361,hypothesis,(
% 0.29/1.08 q8 = queue_289 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f362,hypothesis,(
% 0.29/1.08 q9 = queue_295 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f363,negated_conjecture,(
% 0.29/1.08 elem_298 != elem_301 ),
% 0.29/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/1.08 fof(f364,plain,(
% 0.29/1.08 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f1])).
% 0.29/1.08 fof(f365,plain,(
% 0.29/1.08 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 0.29/1.08 inference(miniscoping,[status(thm)],[f2])).
% 0.29/1.08 fof(f366,plain,(
% 0.29/1.08 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f365])).
% 0.29/1.08 fof(f367,plain,(
% 0.29/1.08 ~head=tail),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f3])).
% 0.29/1.08 fof(f368,plain,(
% 0.29/1.08 ~head=seq),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f4])).
% 0.29/1.08 fof(f370,plain,(
% 0.29/1.08 ![X0]: (p(s(X0))=X0)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f6])).
% 0.29/1.08 fof(f371,plain,(
% 0.29/1.08 ![X0]: (s(p(X0))=X0)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f7])).
% 0.29/1.08 fof(f374,plain,(
% 0.29/1.08 ![X0]: (s(s(s(X0)))=X0)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f10])).
% 0.29/1.08 fof(f474,plain,(
% 0.29/1.08 elem_298=select(earray_296,index_297)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f110])).
% 0.29/1.08 fof(f475,plain,(
% 0.29/1.08 elem_301=select(earray_296,index_300)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f111])).
% 0.29/1.08 fof(f476,plain,(
% 0.29/1.08 index_0=select(q,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f112])).
% 0.29/1.08 fof(f477,plain,(
% 0.29/1.08 index_102=s(index_99)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f113])).
% 0.29/1.08 fof(f478,plain,(
% 0.29/1.08 index_105=select(q24,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f114])).
% 0.29/1.08 fof(f479,plain,(
% 0.29/1.08 index_108=s(index_105)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f115])).
% 0.29/1.08 fof(f480,plain,(
% 0.29/1.08 index_111=select(q25,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f116])).
% 0.29/1.08 fof(f481,plain,(
% 0.29/1.08 index_114=s(index_111)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f117])).
% 0.29/1.08 fof(f482,plain,(
% 0.29/1.08 index_117=select(q26,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f118])).
% 0.29/1.08 fof(f483,plain,(
% 0.29/1.08 index_12=s(index_9)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f119])).
% 0.29/1.08 fof(f484,plain,(
% 0.29/1.08 index_120=s(index_117)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f120])).
% 0.29/1.08 fof(f485,plain,(
% 0.29/1.08 index_123=select(q27,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f121])).
% 0.29/1.08 fof(f486,plain,(
% 0.29/1.08 index_126=s(index_123)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f122])).
% 0.29/1.08 fof(f487,plain,(
% 0.29/1.08 index_129=select(q28,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f123])).
% 0.29/1.08 fof(f488,plain,(
% 0.29/1.08 index_132=s(index_129)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f124])).
% 0.29/1.08 fof(f489,plain,(
% 0.29/1.08 index_135=select(q2,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f125])).
% 0.29/1.08 fof(f490,plain,(
% 0.29/1.08 index_138=s(index_135)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f126])).
% 0.29/1.08 fof(f491,plain,(
% 0.29/1.08 index_141=select(q29,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f127])).
% 0.29/1.08 fof(f492,plain,(
% 0.29/1.08 index_144=s(index_141)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f128])).
% 0.29/1.08 fof(f493,plain,(
% 0.29/1.08 index_147=select(q30,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f129])).
% 0.29/1.08 fof(f494,plain,(
% 0.29/1.08 index_15=select(q10,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f130])).
% 0.29/1.08 fof(f495,plain,(
% 0.29/1.08 index_150=s(index_147)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f131])).
% 0.29/1.08 fof(f496,plain,(
% 0.29/1.08 index_153=select(q31,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f132])).
% 0.29/1.08 fof(f497,plain,(
% 0.29/1.08 index_156=s(index_153)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f133])).
% 0.29/1.08 fof(f498,plain,(
% 0.29/1.08 index_159=select(q32,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f134])).
% 0.29/1.08 fof(f499,plain,(
% 0.29/1.08 index_162=s(index_159)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f135])).
% 0.29/1.08 fof(f500,plain,(
% 0.29/1.08 index_165=select(q33,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f136])).
% 0.29/1.08 fof(f501,plain,(
% 0.29/1.08 index_168=s(index_165)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f137])).
% 0.29/1.08 fof(f502,plain,(
% 0.29/1.08 index_171=select(q34,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f138])).
% 0.29/1.08 fof(f503,plain,(
% 0.29/1.08 index_174=s(index_171)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f139])).
% 0.29/1.08 fof(f504,plain,(
% 0.29/1.08 index_177=select(q35,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f140])).
% 0.29/1.08 fof(f505,plain,(
% 0.29/1.08 index_18=s(index_15)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f141])).
% 0.29/1.08 fof(f506,plain,(
% 0.29/1.08 index_180=s(index_177)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f142])).
% 0.29/1.08 fof(f507,plain,(
% 0.29/1.08 index_183=select(q36,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f143])).
% 0.29/1.08 fof(f508,plain,(
% 0.29/1.08 index_186=s(index_183)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f144])).
% 0.29/1.08 fof(f509,plain,(
% 0.29/1.08 index_189=select(q37,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f145])).
% 0.29/1.08 fof(f510,plain,(
% 0.29/1.08 index_192=s(index_189)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f146])).
% 0.29/1.08 fof(f511,plain,(
% 0.29/1.08 index_195=select(q38,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f147])).
% 0.29/1.08 fof(f512,plain,(
% 0.29/1.08 index_198=s(index_195)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f148])).
% 0.29/1.08 fof(f513,plain,(
% 0.29/1.08 index_201=select(q3,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f149])).
% 0.29/1.08 fof(f514,plain,(
% 0.29/1.08 index_204=s(index_201)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f150])).
% 0.29/1.08 fof(f515,plain,(
% 0.29/1.08 index_207=select(q39,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f151])).
% 0.29/1.08 fof(f516,plain,(
% 0.29/1.08 index_21=select(q11,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f152])).
% 0.29/1.08 fof(f517,plain,(
% 0.29/1.08 index_210=s(index_207)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f153])).
% 0.29/1.08 fof(f518,plain,(
% 0.29/1.08 index_213=select(q40,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f154])).
% 0.29/1.08 fof(f519,plain,(
% 0.29/1.08 index_216=s(index_213)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f155])).
% 0.29/1.08 fof(f520,plain,(
% 0.29/1.08 index_219=select(q41,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f156])).
% 0.29/1.08 fof(f521,plain,(
% 0.29/1.08 index_222=s(index_219)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f157])).
% 0.29/1.08 fof(f522,plain,(
% 0.29/1.08 index_225=select(q42,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f158])).
% 0.29/1.08 fof(f523,plain,(
% 0.29/1.08 index_228=s(index_225)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f159])).
% 0.29/1.08 fof(f524,plain,(
% 0.29/1.08 index_231=select(q43,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f160])).
% 0.29/1.08 fof(f525,plain,(
% 0.29/1.08 index_234=s(index_231)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f161])).
% 0.29/1.08 fof(f526,plain,(
% 0.29/1.08 index_237=select(q44,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f162])).
% 0.29/1.08 fof(f527,plain,(
% 0.29/1.08 index_24=s(index_21)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f163])).
% 0.29/1.08 fof(f528,plain,(
% 0.29/1.08 index_240=s(index_237)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f164])).
% 0.29/1.08 fof(f529,plain,(
% 0.29/1.08 index_243=select(q45,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f165])).
% 0.29/1.08 fof(f530,plain,(
% 0.29/1.08 index_246=s(index_243)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f166])).
% 0.29/1.08 fof(f531,plain,(
% 0.29/1.08 index_249=select(q46,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f167])).
% 0.29/1.08 fof(f532,plain,(
% 0.29/1.08 index_252=s(index_249)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f168])).
% 0.29/1.08 fof(f533,plain,(
% 0.29/1.08 index_255=select(q47,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f169])).
% 0.29/1.08 fof(f534,plain,(
% 0.29/1.08 index_258=s(index_255)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f170])).
% 0.29/1.08 fof(f535,plain,(
% 0.29/1.08 index_261=select(q48,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f171])).
% 0.29/1.08 fof(f536,plain,(
% 0.29/1.08 index_264=s(index_261)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f172])).
% 0.29/1.08 fof(f537,plain,(
% 0.29/1.08 index_267=select(q4,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f173])).
% 0.29/1.08 fof(f538,plain,(
% 0.29/1.08 index_27=select(q12,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f174])).
% 0.29/1.08 fof(f539,plain,(
% 0.29/1.08 index_270=s(index_267)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f175])).
% 0.29/1.08 fof(f540,plain,(
% 0.29/1.08 index_273=select(q5,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f176])).
% 0.29/1.08 fof(f541,plain,(
% 0.29/1.08 index_276=s(index_273)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f177])).
% 0.29/1.08 fof(f542,plain,(
% 0.29/1.08 index_279=select(q6,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f178])).
% 0.29/1.08 fof(f543,plain,(
% 0.29/1.08 index_282=s(index_279)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f179])).
% 0.29/1.08 fof(f544,plain,(
% 0.29/1.08 index_285=select(q7,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f180])).
% 0.29/1.08 fof(f545,plain,(
% 0.29/1.08 index_288=s(index_285)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f181])).
% 0.29/1.08 fof(f546,plain,(
% 0.29/1.08 index_291=select(q8,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f182])).
% 0.29/1.08 fof(f547,plain,(
% 0.29/1.08 index_294=s(index_291)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f183])).
% 0.29/1.08 fof(f548,plain,(
% 0.29/1.08 index_297=select(q49,head)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f184])).
% 0.29/1.08 fof(f549,plain,(
% 0.29/1.08 index_299=select(q49,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f185])).
% 0.29/1.08 fof(f550,plain,(
% 0.29/1.08 index_3=select(q0,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f186])).
% 0.29/1.08 fof(f551,plain,(
% 0.29/1.08 index_30=s(index_27)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f187])).
% 0.29/1.08 fof(f552,plain,(
% 0.29/1.08 s(index_300)=index_299),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f188])).
% 0.29/1.08 fof(f553,plain,(
% 0.29/1.08 index_33=select(q13,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f189])).
% 0.29/1.08 fof(f554,plain,(
% 0.29/1.08 index_36=s(index_33)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f190])).
% 0.29/1.08 fof(f555,plain,(
% 0.29/1.08 index_39=select(q14,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f191])).
% 0.29/1.08 fof(f556,plain,(
% 0.29/1.08 index_42=s(index_39)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f192])).
% 0.29/1.08 fof(f557,plain,(
% 0.29/1.08 index_45=select(q15,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f193])).
% 0.29/1.08 fof(f558,plain,(
% 0.29/1.08 index_48=s(index_45)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f194])).
% 0.29/1.08 fof(f559,plain,(
% 0.29/1.08 index_51=select(q16,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f195])).
% 0.29/1.08 fof(f560,plain,(
% 0.29/1.08 index_54=s(index_51)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f196])).
% 0.29/1.08 fof(f561,plain,(
% 0.29/1.08 index_57=select(q17,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f197])).
% 0.29/1.08 fof(f562,plain,(
% 0.29/1.08 index_6=s(index_3)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f198])).
% 0.29/1.08 fof(f563,plain,(
% 0.29/1.08 index_60=s(index_57)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f199])).
% 0.29/1.08 fof(f564,plain,(
% 0.29/1.08 index_63=select(q18,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f200])).
% 0.29/1.08 fof(f565,plain,(
% 0.29/1.08 index_66=s(index_63)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f201])).
% 0.29/1.08 fof(f566,plain,(
% 0.29/1.08 index_69=select(q1,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f202])).
% 0.29/1.08 fof(f567,plain,(
% 0.29/1.08 index_72=s(index_69)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f203])).
% 0.29/1.08 fof(f568,plain,(
% 0.29/1.08 index_75=select(q19,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f204])).
% 0.29/1.08 fof(f569,plain,(
% 0.29/1.08 index_78=s(index_75)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f205])).
% 0.29/1.08 fof(f570,plain,(
% 0.29/1.08 index_81=select(q20,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f206])).
% 0.29/1.08 fof(f571,plain,(
% 0.29/1.08 index_84=s(index_81)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f207])).
% 0.29/1.08 fof(f572,plain,(
% 0.29/1.08 index_87=select(q21,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f208])).
% 0.29/1.08 fof(f573,plain,(
% 0.29/1.08 index_9=select(q9,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f209])).
% 0.29/1.08 fof(f574,plain,(
% 0.29/1.08 index_90=s(index_87)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f210])).
% 0.29/1.08 fof(f575,plain,(
% 0.29/1.08 index_93=select(q22,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f211])).
% 0.29/1.08 fof(f576,plain,(
% 0.29/1.08 index_96=s(index_93)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f212])).
% 0.29/1.08 fof(f577,plain,(
% 0.29/1.08 index_99=select(q23,tail)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f213])).
% 0.29/1.08 fof(f578,plain,(
% 0.29/1.08 queue_1=store(q,head,index_0)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f214])).
% 0.29/1.08 fof(f579,plain,(
% 0.29/1.08 queue_101=store(q23,seq,earray_100)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f215])).
% 0.29/1.08 fof(f580,plain,(
% 0.29/1.08 queue_103=store(queue_101,tail,index_102)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f216])).
% 0.29/1.08 fof(f581,plain,(
% 0.29/1.08 queue_107=store(q24,seq,earray_106)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f217])).
% 0.29/1.08 fof(f582,plain,(
% 0.29/1.08 queue_109=store(queue_107,tail,index_108)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f218])).
% 0.29/1.08 fof(f583,plain,(
% 0.29/1.08 queue_11=store(q9,seq,earray_10)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f219])).
% 0.29/1.08 fof(f584,plain,(
% 0.29/1.08 queue_113=store(q25,seq,earray_112)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f220])).
% 0.29/1.08 fof(f585,plain,(
% 0.29/1.08 queue_115=store(queue_113,tail,index_114)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f221])).
% 0.29/1.08 fof(f586,plain,(
% 0.29/1.08 queue_119=store(q26,seq,earray_118)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f222])).
% 0.29/1.08 fof(f587,plain,(
% 0.29/1.08 queue_121=store(queue_119,tail,index_120)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f223])).
% 0.29/1.08 fof(f588,plain,(
% 0.29/1.08 queue_125=store(q27,seq,earray_124)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f224])).
% 0.29/1.08 fof(f589,plain,(
% 0.29/1.08 queue_127=store(queue_125,tail,index_126)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f225])).
% 0.29/1.08 fof(f590,plain,(
% 0.29/1.08 queue_13=store(queue_11,tail,index_12)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f226])).
% 0.29/1.08 fof(f591,plain,(
% 0.29/1.08 queue_131=store(q28,seq,earray_130)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f227])).
% 0.29/1.08 fof(f592,plain,(
% 0.29/1.08 queue_133=store(queue_131,tail,index_132)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f228])).
% 0.29/1.08 fof(f593,plain,(
% 0.29/1.08 queue_137=store(q2,seq,earray_136)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f229])).
% 0.29/1.08 fof(f594,plain,(
% 0.29/1.08 queue_139=store(queue_137,tail,index_138)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f230])).
% 0.29/1.08 fof(f595,plain,(
% 0.29/1.08 queue_143=store(q29,seq,earray_142)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f231])).
% 0.29/1.08 fof(f596,plain,(
% 0.29/1.08 queue_145=store(queue_143,tail,index_144)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f232])).
% 0.29/1.08 fof(f597,plain,(
% 0.29/1.08 queue_149=store(q30,seq,earray_148)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f233])).
% 0.29/1.08 fof(f598,plain,(
% 0.29/1.08 queue_151=store(queue_149,tail,index_150)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f234])).
% 0.29/1.08 fof(f599,plain,(
% 0.29/1.08 queue_155=store(q31,seq,earray_154)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f235])).
% 0.29/1.08 fof(f600,plain,(
% 0.29/1.08 queue_157=store(queue_155,tail,index_156)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f236])).
% 0.29/1.08 fof(f601,plain,(
% 0.29/1.08 queue_161=store(q32,seq,earray_160)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f237])).
% 0.29/1.08 fof(f602,plain,(
% 0.29/1.08 queue_163=store(queue_161,tail,index_162)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f238])).
% 0.29/1.08 fof(f603,plain,(
% 0.29/1.08 queue_167=store(q33,seq,earray_166)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f239])).
% 0.29/1.08 fof(f604,plain,(
% 0.29/1.08 queue_169=store(queue_167,tail,index_168)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f240])).
% 0.29/1.08 fof(f605,plain,(
% 0.29/1.08 queue_17=store(q10,seq,earray_16)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f241])).
% 0.29/1.08 fof(f606,plain,(
% 0.29/1.08 queue_173=store(q34,seq,earray_172)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f242])).
% 0.29/1.08 fof(f607,plain,(
% 0.29/1.08 queue_175=store(queue_173,tail,index_174)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f243])).
% 0.29/1.08 fof(f608,plain,(
% 0.29/1.08 queue_179=store(q35,seq,earray_178)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f244])).
% 0.29/1.08 fof(f609,plain,(
% 0.29/1.08 queue_181=store(queue_179,tail,index_180)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f245])).
% 0.29/1.08 fof(f610,plain,(
% 0.29/1.08 queue_185=store(q36,seq,earray_184)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f246])).
% 0.29/1.08 fof(f611,plain,(
% 0.29/1.08 queue_187=store(queue_185,tail,index_186)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f247])).
% 0.29/1.08 fof(f612,plain,(
% 0.29/1.08 queue_19=store(queue_17,tail,index_18)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f248])).
% 0.29/1.08 fof(f613,plain,(
% 0.29/1.08 queue_191=store(q37,seq,earray_190)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f249])).
% 0.29/1.08 fof(f614,plain,(
% 0.29/1.08 queue_193=store(queue_191,tail,index_192)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f250])).
% 0.29/1.08 fof(f615,plain,(
% 0.29/1.08 queue_197=store(q38,seq,earray_196)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f251])).
% 0.29/1.08 fof(f616,plain,(
% 0.29/1.08 queue_199=store(queue_197,tail,index_198)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f252])).
% 0.29/1.08 fof(f617,plain,(
% 0.29/1.08 queue_203=store(q3,seq,earray_202)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f253])).
% 0.29/1.08 fof(f618,plain,(
% 0.29/1.08 queue_205=store(queue_203,tail,index_204)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f254])).
% 0.29/1.08 fof(f619,plain,(
% 0.29/1.08 queue_209=store(q39,seq,earray_208)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f255])).
% 0.29/1.08 fof(f620,plain,(
% 0.29/1.08 queue_211=store(queue_209,tail,index_210)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f256])).
% 0.29/1.08 fof(f621,plain,(
% 0.29/1.08 queue_215=store(q40,seq,earray_214)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f257])).
% 0.29/1.08 fof(f622,plain,(
% 0.29/1.08 queue_217=store(queue_215,tail,index_216)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f258])).
% 0.29/1.08 fof(f623,plain,(
% 0.29/1.08 queue_221=store(q41,seq,earray_220)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f259])).
% 0.29/1.08 fof(f624,plain,(
% 0.29/1.08 queue_223=store(queue_221,tail,index_222)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f260])).
% 0.29/1.08 fof(f625,plain,(
% 0.29/1.08 queue_227=store(q42,seq,earray_226)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f261])).
% 0.29/1.08 fof(f626,plain,(
% 0.29/1.08 queue_229=store(queue_227,tail,index_228)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f262])).
% 0.29/1.08 fof(f627,plain,(
% 0.29/1.08 queue_23=store(q11,seq,earray_22)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f263])).
% 0.29/1.08 fof(f628,plain,(
% 0.29/1.08 queue_233=store(q43,seq,earray_232)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f264])).
% 0.29/1.08 fof(f629,plain,(
% 0.29/1.08 queue_235=store(queue_233,tail,index_234)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f265])).
% 0.29/1.08 fof(f630,plain,(
% 0.29/1.08 queue_239=store(q44,seq,earray_238)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f266])).
% 0.29/1.08 fof(f631,plain,(
% 0.29/1.08 queue_241=store(queue_239,tail,index_240)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f267])).
% 0.29/1.08 fof(f632,plain,(
% 0.29/1.08 queue_245=store(q45,seq,earray_244)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f268])).
% 0.29/1.08 fof(f633,plain,(
% 0.29/1.08 queue_247=store(queue_245,tail,index_246)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f269])).
% 0.29/1.08 fof(f634,plain,(
% 0.29/1.08 queue_25=store(queue_23,tail,index_24)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f270])).
% 0.29/1.08 fof(f635,plain,(
% 0.29/1.08 queue_251=store(q46,seq,earray_250)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f271])).
% 0.29/1.08 fof(f636,plain,(
% 0.29/1.08 queue_253=store(queue_251,tail,index_252)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f272])).
% 0.29/1.08 fof(f637,plain,(
% 0.29/1.08 queue_257=store(q47,seq,earray_256)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f273])).
% 0.29/1.08 fof(f638,plain,(
% 0.29/1.08 queue_259=store(queue_257,tail,index_258)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f274])).
% 0.29/1.08 fof(f639,plain,(
% 0.29/1.08 queue_263=store(q48,seq,earray_262)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f275])).
% 0.29/1.08 fof(f640,plain,(
% 0.29/1.08 queue_265=store(queue_263,tail,index_264)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f276])).
% 0.29/1.08 fof(f641,plain,(
% 0.29/1.08 queue_269=store(q4,seq,earray_268)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f277])).
% 0.29/1.08 fof(f642,plain,(
% 0.29/1.08 queue_271=store(queue_269,tail,index_270)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f278])).
% 0.29/1.08 fof(f643,plain,(
% 0.29/1.08 queue_275=store(q5,seq,earray_274)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f279])).
% 0.29/1.08 fof(f644,plain,(
% 0.29/1.08 queue_277=store(queue_275,tail,index_276)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f280])).
% 0.29/1.08 fof(f645,plain,(
% 0.29/1.08 queue_281=store(q6,seq,earray_280)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f281])).
% 0.29/1.08 fof(f646,plain,(
% 0.29/1.08 queue_283=store(queue_281,tail,index_282)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f282])).
% 0.29/1.08 fof(f647,plain,(
% 0.29/1.08 queue_287=store(q7,seq,earray_286)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f283])).
% 0.29/1.08 fof(f648,plain,(
% 0.29/1.08 queue_289=store(queue_287,tail,index_288)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f284])).
% 0.29/1.08 fof(f649,plain,(
% 0.29/1.08 queue_29=store(q12,seq,earray_28)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f285])).
% 0.29/1.08 fof(f650,plain,(
% 0.29/1.08 queue_293=store(q8,seq,earray_292)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f286])).
% 0.29/1.08 fof(f651,plain,(
% 0.29/1.08 queue_295=store(queue_293,tail,index_294)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f287])).
% 0.29/1.08 fof(f652,plain,(
% 0.29/1.08 queue_31=store(queue_29,tail,index_30)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f288])).
% 0.29/1.08 fof(f653,plain,(
% 0.29/1.08 queue_35=store(q13,seq,earray_34)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f289])).
% 0.29/1.08 fof(f654,plain,(
% 0.29/1.08 queue_37=store(queue_35,tail,index_36)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f290])).
% 0.29/1.08 fof(f655,plain,(
% 0.29/1.08 queue_41=store(q14,seq,earray_40)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f291])).
% 0.29/1.08 fof(f656,plain,(
% 0.29/1.08 queue_43=store(queue_41,tail,index_42)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f292])).
% 0.29/1.08 fof(f657,plain,(
% 0.29/1.08 queue_47=store(q15,seq,earray_46)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f293])).
% 0.29/1.08 fof(f658,plain,(
% 0.29/1.08 queue_49=store(queue_47,tail,index_48)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f294])).
% 0.29/1.08 fof(f659,plain,(
% 0.29/1.08 queue_5=store(q0,seq,earray_4)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f295])).
% 0.29/1.08 fof(f660,plain,(
% 0.29/1.08 queue_53=store(q16,seq,earray_52)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f296])).
% 0.29/1.08 fof(f661,plain,(
% 0.29/1.08 queue_55=store(queue_53,tail,index_54)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f297])).
% 0.29/1.08 fof(f662,plain,(
% 0.29/1.08 queue_59=store(q17,seq,earray_58)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f298])).
% 0.29/1.08 fof(f663,plain,(
% 0.29/1.08 queue_61=store(queue_59,tail,index_60)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f299])).
% 0.29/1.08 fof(f664,plain,(
% 0.29/1.08 queue_65=store(q18,seq,earray_64)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f300])).
% 0.29/1.08 fof(f665,plain,(
% 0.29/1.08 queue_67=store(queue_65,tail,index_66)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f301])).
% 0.29/1.08 fof(f666,plain,(
% 0.29/1.08 queue_7=store(queue_5,tail,index_6)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f302])).
% 0.29/1.08 fof(f667,plain,(
% 0.29/1.08 queue_71=store(q1,seq,earray_70)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f303])).
% 0.29/1.08 fof(f668,plain,(
% 0.29/1.08 queue_73=store(queue_71,tail,index_72)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f304])).
% 0.29/1.08 fof(f669,plain,(
% 0.29/1.08 queue_77=store(q19,seq,earray_76)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f305])).
% 0.29/1.08 fof(f670,plain,(
% 0.29/1.08 queue_79=store(queue_77,tail,index_78)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f306])).
% 0.29/1.08 fof(f671,plain,(
% 0.29/1.08 queue_83=store(q20,seq,earray_82)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f307])).
% 0.29/1.08 fof(f672,plain,(
% 0.29/1.08 queue_85=store(queue_83,tail,index_84)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f308])).
% 0.29/1.08 fof(f673,plain,(
% 0.29/1.08 queue_89=store(q21,seq,earray_88)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f309])).
% 0.29/1.08 fof(f674,plain,(
% 0.29/1.08 queue_91=store(queue_89,tail,index_90)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f310])).
% 0.29/1.08 fof(f675,plain,(
% 0.29/1.08 queue_95=store(q22,seq,earray_94)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f311])).
% 0.29/1.08 fof(f676,plain,(
% 0.29/1.08 queue_97=store(queue_95,tail,index_96)),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f312])).
% 0.29/1.08 fof(f677,plain,(
% 0.29/1.08 q0=queue_1),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f313])).
% 0.29/1.08 fof(f678,plain,(
% 0.29/1.08 q1=queue_7),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f314])).
% 0.29/1.08 fof(f679,plain,(
% 0.29/1.08 q10=queue_13),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f315])).
% 0.29/1.08 fof(f680,plain,(
% 0.29/1.08 q11=queue_19),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f316])).
% 0.29/1.08 fof(f681,plain,(
% 0.29/1.08 q12=queue_25),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f317])).
% 0.29/1.08 fof(f682,plain,(
% 0.29/1.08 q13=queue_31),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f318])).
% 0.29/1.08 fof(f683,plain,(
% 0.29/1.08 q14=queue_37),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f319])).
% 0.29/1.08 fof(f684,plain,(
% 0.29/1.08 q15=queue_43),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f320])).
% 0.29/1.08 fof(f685,plain,(
% 0.29/1.08 q16=queue_49),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f321])).
% 0.29/1.08 fof(f686,plain,(
% 0.29/1.08 q17=queue_55),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f322])).
% 0.29/1.08 fof(f687,plain,(
% 0.29/1.08 q18=queue_61),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f323])).
% 0.29/1.08 fof(f688,plain,(
% 0.29/1.08 q19=queue_67),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f324])).
% 0.29/1.08 fof(f689,plain,(
% 0.29/1.08 q2=queue_73),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f325])).
% 0.29/1.08 fof(f690,plain,(
% 0.29/1.08 q20=queue_79),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f326])).
% 0.29/1.08 fof(f691,plain,(
% 0.29/1.08 q21=queue_85),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f327])).
% 0.29/1.08 fof(f692,plain,(
% 0.29/1.08 q22=queue_91),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f328])).
% 0.29/1.08 fof(f693,plain,(
% 0.29/1.08 q23=queue_97),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f329])).
% 0.29/1.08 fof(f694,plain,(
% 0.29/1.08 q24=queue_103),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f330])).
% 0.29/1.08 fof(f695,plain,(
% 0.29/1.08 q25=queue_109),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f331])).
% 0.29/1.08 fof(f696,plain,(
% 0.29/1.08 q26=queue_115),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f332])).
% 0.29/1.08 fof(f697,plain,(
% 0.29/1.08 q27=queue_121),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f333])).
% 0.29/1.08 fof(f698,plain,(
% 0.29/1.08 q28=queue_127),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f334])).
% 0.29/1.08 fof(f699,plain,(
% 0.29/1.08 q29=queue_133),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f335])).
% 0.29/1.08 fof(f700,plain,(
% 0.29/1.08 q3=queue_139),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f336])).
% 0.29/1.08 fof(f701,plain,(
% 0.29/1.08 q30=queue_145),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f337])).
% 0.29/1.08 fof(f702,plain,(
% 0.29/1.08 q31=queue_151),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f338])).
% 0.29/1.08 fof(f703,plain,(
% 0.29/1.08 q32=queue_157),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f339])).
% 0.29/1.08 fof(f704,plain,(
% 0.29/1.08 q33=queue_163),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f340])).
% 0.29/1.08 fof(f705,plain,(
% 0.29/1.08 q34=queue_169),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f341])).
% 0.29/1.08 fof(f706,plain,(
% 0.29/1.08 q35=queue_175),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f342])).
% 0.29/1.08 fof(f707,plain,(
% 0.29/1.08 q36=queue_181),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f343])).
% 0.29/1.08 fof(f708,plain,(
% 0.29/1.08 q37=queue_187),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f344])).
% 0.29/1.08 fof(f709,plain,(
% 0.29/1.08 q38=queue_193),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f345])).
% 0.29/1.08 fof(f710,plain,(
% 0.29/1.08 q39=queue_199),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f346])).
% 0.29/1.08 fof(f711,plain,(
% 0.29/1.08 q4=queue_205),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f347])).
% 0.29/1.08 fof(f712,plain,(
% 0.29/1.08 q40=queue_211),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f348])).
% 0.29/1.08 fof(f713,plain,(
% 0.29/1.08 q41=queue_217),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f349])).
% 0.29/1.08 fof(f714,plain,(
% 0.29/1.08 q42=queue_223),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f350])).
% 0.29/1.08 fof(f715,plain,(
% 0.29/1.08 q43=queue_229),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f351])).
% 0.29/1.08 fof(f716,plain,(
% 0.29/1.08 q44=queue_235),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f352])).
% 0.29/1.08 fof(f717,plain,(
% 0.29/1.08 q45=queue_241),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f353])).
% 0.29/1.08 fof(f718,plain,(
% 0.29/1.08 q46=queue_247),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f354])).
% 0.29/1.08 fof(f719,plain,(
% 0.29/1.08 q47=queue_253),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f355])).
% 0.29/1.08 fof(f720,plain,(
% 0.29/1.08 q48=queue_259),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f356])).
% 0.29/1.08 fof(f721,plain,(
% 0.29/1.08 q49=queue_265),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f357])).
% 0.29/1.08 fof(f722,plain,(
% 0.29/1.08 q5=queue_271),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f358])).
% 0.29/1.08 fof(f723,plain,(
% 0.29/1.08 q6=queue_277),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f359])).
% 0.29/1.08 fof(f724,plain,(
% 0.29/1.08 q7=queue_283),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f360])).
% 0.29/1.08 fof(f725,plain,(
% 0.29/1.08 q8=queue_289),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f361])).
% 0.29/1.08 fof(f726,plain,(
% 0.29/1.08 q9=queue_295),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f362])).
% 0.29/1.08 fof(f727,plain,(
% 0.29/1.08 ~elem_298=elem_301),
% 0.29/1.08 inference(cnf_transformation,[status(thm)],[f363])).
% 0.29/1.08 fof(f736,plain,(
% 0.29/1.08 ![X0]: (s(s(X0))=p(X0))),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f371,f374])).
% 0.29/1.08 fof(f755,plain,(
% 0.29/1.08 p(index_102)=index_99),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f477,f370])).
% 0.29/1.08 fof(f770,plain,(
% 0.29/1.08 p(index_12)=index_9),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f483,f370])).
% 0.29/1.08 fof(f774,plain,(
% 0.29/1.08 p(index_120)=index_117),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f484,f370])).
% 0.29/1.08 fof(f791,plain,(
% 0.29/1.08 p(index_138)=index_135),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f490,f370])).
% 0.29/1.08 fof(f795,plain,(
% 0.29/1.08 p(index_144)=index_141),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f492,f370])).
% 0.29/1.08 fof(f808,plain,(
% 0.29/1.08 p(index_162)=index_159),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f499,f370])).
% 0.29/1.08 fof(f827,plain,(
% 0.29/1.08 p(index_180)=index_177),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f506,f370])).
% 0.29/1.08 fof(f839,plain,(
% 0.29/1.08 p(index_198)=index_195),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f512,f370])).
% 0.29/1.08 fof(f861,plain,(
% 0.29/1.08 p(index_222)=index_219),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f521,f370])).
% 0.29/1.08 fof(f876,plain,(
% 0.29/1.08 p(index_24)=index_21),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f527,f370])).
% 0.29/1.08 fof(f880,plain,(
% 0.29/1.08 p(index_240)=index_237),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f528,f370])).
% 0.29/1.08 fof(f896,plain,(
% 0.29/1.08 p(index_264)=index_261),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f536,f370])).
% 0.29/1.08 fof(f909,plain,(
% 0.29/1.08 p(index_276)=index_273),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f541,f370])).
% 0.29/1.08 fof(f922,plain,(
% 0.29/1.08 p(index_294)=index_291),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f547,f370])).
% 0.29/1.08 fof(f933,plain,(
% 0.29/1.08 p(index_299)=index_300),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f552,f370])).
% 0.29/1.08 fof(f941,plain,(
% 0.29/1.08 p(index_42)=index_39),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f556,f370])).
% 0.29/1.08 fof(f953,plain,(
% 0.29/1.08 p(index_6)=index_3),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f562,f370])).
% 0.29/1.08 fof(f962,plain,(
% 0.29/1.08 p(index_60)=index_57),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f563,f370])).
% 0.29/1.08 fof(f979,plain,(
% 0.29/1.08 p(index_84)=index_81),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f571,f370])).
% 0.29/1.08 fof(f983,plain,(
% 0.29/1.08 p(index_90)=index_87),
% 0.29/1.08 inference(paramodulation,[status(thm)],[f574,f370])).
% 0.29/1.08 fof(f1276,plain,(
% 0.29/1.08 index_105=select(queue_103,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f694,f478])).
% 0.29/1.08 fof(f1277,plain,(
% 0.29/1.08 index_111=select(queue_109,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f695,f480])).
% 0.29/1.08 fof(f1278,plain,(
% 0.29/1.08 index_117=select(queue_115,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f696,f482])).
% 0.29/1.08 fof(f1279,plain,(
% 0.29/1.08 index_123=select(queue_121,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f697,f485])).
% 0.29/1.08 fof(f1280,plain,(
% 0.29/1.08 index_129=select(queue_127,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f698,f487])).
% 0.29/1.08 fof(f1281,plain,(
% 0.29/1.08 index_135=select(queue_73,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f689,f489])).
% 0.29/1.08 fof(f1282,plain,(
% 0.29/1.08 index_141=select(queue_133,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f699,f491])).
% 0.29/1.08 fof(f1283,plain,(
% 0.29/1.08 index_147=select(queue_145,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f701,f493])).
% 0.29/1.08 fof(f1284,plain,(
% 0.29/1.08 index_15=select(queue_13,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f679,f494])).
% 0.29/1.08 fof(f1285,plain,(
% 0.29/1.08 index_153=select(queue_151,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f702,f496])).
% 0.29/1.08 fof(f1292,plain,(
% 0.29/1.08 index_159=select(queue_157,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f703,f498])).
% 0.29/1.08 fof(f1293,plain,(
% 0.29/1.08 index_165=select(queue_163,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f704,f500])).
% 0.29/1.08 fof(f1294,plain,(
% 0.29/1.08 index_171=select(queue_169,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f705,f502])).
% 0.29/1.08 fof(f1295,plain,(
% 0.29/1.08 index_177=select(queue_175,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f706,f504])).
% 0.29/1.08 fof(f1298,plain,(
% 0.29/1.08 index_183=select(queue_181,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f707,f507])).
% 0.29/1.08 fof(f1299,plain,(
% 0.29/1.08 index_189=select(queue_187,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f708,f509])).
% 0.29/1.08 fof(f1300,plain,(
% 0.29/1.08 index_195=select(queue_193,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f709,f511])).
% 0.29/1.08 fof(f1301,plain,(
% 0.29/1.08 index_201=select(queue_139,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f700,f513])).
% 0.29/1.08 fof(f1302,plain,(
% 0.29/1.08 index_207=select(queue_199,tail)),
% 0.29/1.08 inference(forward_demodulation,[status(thm)],[f710,f515])).
% 0.29/1.09 fof(f1303,plain,(
% 0.29/1.09 index_21=select(queue_19,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f680,f516])).
% 0.29/1.09 fof(f1304,plain,(
% 0.29/1.09 index_213=select(queue_211,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f712,f518])).
% 0.29/1.09 fof(f1305,plain,(
% 0.29/1.09 index_219=select(queue_217,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f713,f520])).
% 0.29/1.09 fof(f1310,plain,(
% 0.29/1.09 index_225=select(queue_223,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f714,f522])).
% 0.29/1.09 fof(f1311,plain,(
% 0.29/1.09 index_231=select(queue_229,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f715,f524])).
% 0.29/1.09 fof(f1312,plain,(
% 0.29/1.09 index_237=select(queue_235,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f716,f526])).
% 0.29/1.09 fof(f1313,plain,(
% 0.29/1.09 index_243=select(queue_241,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f717,f529])).
% 0.29/1.09 fof(f1314,plain,(
% 0.29/1.09 index_249=select(queue_247,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f718,f531])).
% 0.29/1.09 fof(f1315,plain,(
% 0.29/1.09 index_255=select(queue_253,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f719,f533])).
% 0.29/1.09 fof(f1316,plain,(
% 0.29/1.09 index_261=select(queue_259,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f720,f535])).
% 0.29/1.09 fof(f1317,plain,(
% 0.29/1.09 index_267=select(queue_205,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f711,f537])).
% 0.29/1.09 fof(f1318,plain,(
% 0.29/1.09 index_27=select(queue_25,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f681,f538])).
% 0.29/1.09 fof(f1319,plain,(
% 0.29/1.09 index_273=select(queue_271,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f722,f540])).
% 0.29/1.09 fof(f1320,plain,(
% 0.29/1.09 index_279=select(queue_277,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f723,f542])).
% 0.29/1.09 fof(f1321,plain,(
% 0.29/1.09 index_285=select(queue_283,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f724,f544])).
% 0.29/1.09 fof(f1328,plain,(
% 0.29/1.09 index_291=select(queue_289,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f725,f546])).
% 0.29/1.09 fof(f1329,plain,(
% 0.29/1.09 index_297=select(queue_265,head)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f721,f548])).
% 0.29/1.09 fof(f1330,plain,(
% 0.29/1.09 index_299=select(queue_265,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f721,f549])).
% 0.29/1.09 fof(f1331,plain,(
% 0.29/1.09 index_3=select(queue_1,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f677,f550])).
% 0.29/1.09 fof(f1332,plain,(
% 0.29/1.09 index_33=select(queue_31,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f682,f553])).
% 0.29/1.09 fof(f1333,plain,(
% 0.29/1.09 index_39=select(queue_37,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f683,f555])).
% 0.29/1.09 fof(f1334,plain,(
% 0.29/1.09 index_45=select(queue_43,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f684,f557])).
% 0.29/1.09 fof(f1335,plain,(
% 0.29/1.09 index_51=select(queue_49,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f685,f559])).
% 0.29/1.09 fof(f1336,plain,(
% 0.29/1.09 index_57=select(queue_55,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f686,f561])).
% 0.29/1.09 fof(f1337,plain,(
% 0.29/1.09 index_63=select(queue_61,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f687,f564])).
% 0.29/1.09 fof(f1338,plain,(
% 0.29/1.09 index_69=select(queue_7,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f678,f566])).
% 0.29/1.09 fof(f1339,plain,(
% 0.29/1.09 index_75=select(queue_67,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f688,f568])).
% 0.29/1.09 fof(f1340,plain,(
% 0.29/1.09 index_81=select(queue_79,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f690,f570])).
% 0.29/1.09 fof(f1341,plain,(
% 0.29/1.09 index_87=select(queue_85,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f691,f572])).
% 0.29/1.09 fof(f1342,plain,(
% 0.29/1.09 index_9=select(queue_295,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f726,f573])).
% 0.29/1.09 fof(f1343,plain,(
% 0.29/1.09 index_93=select(queue_91,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f692,f575])).
% 0.29/1.09 fof(f1344,plain,(
% 0.29/1.09 index_99=select(queue_97,tail)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f693,f577])).
% 0.29/1.09 fof(f1347,plain,(
% 0.29/1.09 s(index_96)=p(index_93)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f576,f736])).
% 0.29/1.09 fof(f1348,plain,(
% 0.29/1.09 s(index_90)=p(index_87)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f574,f736])).
% 0.29/1.09 fof(f1351,plain,(
% 0.29/1.09 s(index_72)=p(index_69)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f567,f736])).
% 0.29/1.09 fof(f1352,plain,(
% 0.29/1.09 s(index_66)=p(index_63)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f565,f736])).
% 0.29/1.09 fof(f1356,plain,(
% 0.29/1.09 s(index_48)=p(index_45)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f558,f736])).
% 0.29/1.09 fof(f1360,plain,(
% 0.29/1.09 s(index_30)=p(index_27)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f551,f736])).
% 0.29/1.09 fof(f1363,plain,(
% 0.29/1.09 s(index_282)=p(index_279)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f543,f736])).
% 0.29/1.09 fof(f1369,plain,(
% 0.29/1.09 s(index_246)=p(index_243)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f530,f736])).
% 0.29/1.09 fof(f1373,plain,(
% 0.29/1.09 s(index_228)=p(index_225)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f523,f736])).
% 0.29/1.09 fof(f1376,plain,(
% 0.29/1.09 s(index_210)=p(index_207)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f517,f736])).
% 0.29/1.09 fof(f1377,plain,(
% 0.29/1.09 s(index_204)=p(index_201)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f514,f736])).
% 0.29/1.09 fof(f1380,plain,(
% 0.29/1.09 s(index_186)=p(index_183)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f508,f736])).
% 0.29/1.09 fof(f1382,plain,(
% 0.29/1.09 s(index_18)=p(index_15)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f505,f736])).
% 0.29/1.09 fof(f1384,plain,(
% 0.29/1.09 s(index_168)=p(index_165)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f501,f736])).
% 0.29/1.09 fof(f1387,plain,(
% 0.29/1.09 s(index_150)=p(index_147)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f495,f736])).
% 0.29/1.09 fof(f1391,plain,(
% 0.29/1.09 s(index_126)=p(index_123)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f486,f736])).
% 0.29/1.09 fof(f1395,plain,(
% 0.29/1.09 s(index_108)=p(index_105)),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f479,f736])).
% 0.29/1.09 fof(f1407,plain,(
% 0.29/1.09 ![X0]: (head=X0|select(queue_1,X0)=select(q,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f578,f366])).
% 0.29/1.09 fof(f1408,plain,(
% 0.29/1.09 select(queue_1,head)=index_0),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f578,f364])).
% 0.29/1.09 fof(f1409,plain,(
% 0.29/1.09 queue_101=store(queue_97,seq,earray_100)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f693,f579])).
% 0.29/1.09 fof(f1410,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_101,X0)=select(queue_97,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1409,f366])).
% 0.29/1.09 fof(f1412,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_103,X0)=select(queue_101,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f580,f366])).
% 0.29/1.09 fof(f1413,plain,(
% 0.29/1.09 select(queue_103,tail)=index_102),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f580,f364])).
% 0.29/1.09 fof(f1418,plain,(
% 0.29/1.09 queue_107=store(queue_103,seq,earray_106)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f694,f581])).
% 0.29/1.09 fof(f1419,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_107,X0)=select(queue_103,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1418,f366])).
% 0.29/1.09 fof(f1427,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_109,X0)=select(queue_107,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f582,f366])).
% 0.29/1.09 fof(f1428,plain,(
% 0.29/1.09 select(queue_109,tail)=index_108),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f582,f364])).
% 0.29/1.09 fof(f1429,plain,(
% 0.29/1.09 queue_11=store(queue_295,seq,earray_10)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f726,f583])).
% 0.29/1.09 fof(f1430,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_11,X0)=select(queue_295,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1429,f366])).
% 0.29/1.09 fof(f1441,plain,(
% 0.29/1.09 queue_113=store(queue_109,seq,earray_112)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f695,f584])).
% 0.29/1.09 fof(f1442,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_113,X0)=select(queue_109,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1441,f366])).
% 0.29/1.09 fof(f1444,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_115,X0)=select(queue_113,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f585,f366])).
% 0.29/1.09 fof(f1445,plain,(
% 0.29/1.09 select(queue_115,tail)=index_114),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f585,f364])).
% 0.29/1.09 fof(f1446,plain,(
% 0.29/1.09 queue_119=store(queue_115,seq,earray_118)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f696,f586])).
% 0.29/1.09 fof(f1447,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_119,X0)=select(queue_115,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1446,f366])).
% 0.29/1.09 fof(f1452,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_121,X0)=select(queue_119,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f587,f366])).
% 0.29/1.09 fof(f1453,plain,(
% 0.29/1.09 select(queue_121,tail)=index_120),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f587,f364])).
% 0.29/1.09 fof(f1460,plain,(
% 0.29/1.09 queue_125=store(queue_121,seq,earray_124)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f697,f588])).
% 0.29/1.09 fof(f1461,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_125,X0)=select(queue_121,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1460,f366])).
% 0.29/1.09 fof(f1463,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_127,X0)=select(queue_125,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f589,f366])).
% 0.29/1.09 fof(f1464,plain,(
% 0.29/1.09 select(queue_127,tail)=index_126),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f589,f364])).
% 0.29/1.09 fof(f1476,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_13,X0)=select(queue_11,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f590,f366])).
% 0.29/1.09 fof(f1477,plain,(
% 0.29/1.09 select(queue_13,tail)=index_12),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f590,f364])).
% 0.29/1.09 fof(f1478,plain,(
% 0.29/1.09 queue_131=store(queue_127,seq,earray_130)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f698,f591])).
% 0.29/1.09 fof(f1479,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_131,X0)=select(queue_127,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1478,f366])).
% 0.29/1.09 fof(f1481,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_133,X0)=select(queue_131,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f592,f366])).
% 0.29/1.09 fof(f1482,plain,(
% 0.29/1.09 select(queue_133,tail)=index_132),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f592,f364])).
% 0.29/1.09 fof(f1485,plain,(
% 0.29/1.09 queue_137=store(queue_73,seq,earray_136)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f689,f593])).
% 0.29/1.09 fof(f1486,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_137,X0)=select(queue_73,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1485,f366])).
% 0.29/1.09 fof(f1494,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_139,X0)=select(queue_137,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f594,f366])).
% 0.29/1.09 fof(f1495,plain,(
% 0.29/1.09 select(queue_139,tail)=index_138),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f594,f364])).
% 0.29/1.09 fof(f1496,plain,(
% 0.29/1.09 queue_143=store(queue_133,seq,earray_142)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f699,f595])).
% 0.29/1.09 fof(f1497,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_143,X0)=select(queue_133,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1496,f366])).
% 0.29/1.09 fof(f1499,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_145,X0)=select(queue_143,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f596,f366])).
% 0.29/1.09 fof(f1500,plain,(
% 0.29/1.09 select(queue_145,tail)=index_144),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f596,f364])).
% 0.29/1.09 fof(f1501,plain,(
% 0.29/1.09 queue_149=store(queue_145,seq,earray_148)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f701,f597])).
% 0.29/1.09 fof(f1502,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_149,X0)=select(queue_145,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1501,f366])).
% 0.29/1.09 fof(f1504,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_151,X0)=select(queue_149,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f598,f366])).
% 0.29/1.09 fof(f1505,plain,(
% 0.29/1.09 select(queue_151,tail)=index_150),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f598,f364])).
% 0.29/1.09 fof(f1506,plain,(
% 0.29/1.09 queue_155=store(queue_151,seq,earray_154)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f702,f599])).
% 0.29/1.09 fof(f1507,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_155,X0)=select(queue_151,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1506,f366])).
% 0.29/1.09 fof(f1509,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_157,X0)=select(queue_155,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f600,f366])).
% 0.29/1.09 fof(f1510,plain,(
% 0.29/1.09 select(queue_157,tail)=index_156),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f600,f364])).
% 0.29/1.09 fof(f1511,plain,(
% 0.29/1.09 queue_161=store(queue_157,seq,earray_160)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f703,f601])).
% 0.29/1.09 fof(f1512,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_161,X0)=select(queue_157,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1511,f366])).
% 0.29/1.09 fof(f1549,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_163,X0)=select(queue_161,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f602,f366])).
% 0.29/1.09 fof(f1550,plain,(
% 0.29/1.09 select(queue_163,tail)=index_162),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f602,f364])).
% 0.29/1.09 fof(f1551,plain,(
% 0.29/1.09 queue_167=store(queue_163,seq,earray_166)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f704,f603])).
% 0.29/1.09 fof(f1552,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_167,X0)=select(queue_163,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1551,f366])).
% 0.29/1.09 fof(f1554,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_169,X0)=select(queue_167,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f604,f366])).
% 0.29/1.09 fof(f1555,plain,(
% 0.29/1.09 select(queue_169,tail)=index_168),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f604,f364])).
% 0.29/1.09 fof(f1584,plain,(
% 0.29/1.09 queue_17=store(queue_13,seq,earray_16)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f679,f605])).
% 0.29/1.09 fof(f1585,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_17,X0)=select(queue_13,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1584,f366])).
% 0.29/1.09 fof(f1643,plain,(
% 0.29/1.09 queue_173=store(queue_169,seq,earray_172)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f705,f606])).
% 0.29/1.09 fof(f1644,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_173,X0)=select(queue_169,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1643,f366])).
% 0.29/1.09 fof(f1646,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_175,X0)=select(queue_173,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f607,f366])).
% 0.29/1.09 fof(f1647,plain,(
% 0.29/1.09 select(queue_175,tail)=index_174),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f607,f364])).
% 0.29/1.09 fof(f1732,plain,(
% 0.29/1.09 queue_179=store(queue_175,seq,earray_178)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f706,f608])).
% 0.29/1.09 fof(f1733,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_179,X0)=select(queue_175,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1732,f366])).
% 0.29/1.09 fof(f1735,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_181,X0)=select(queue_179,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f609,f366])).
% 0.29/1.09 fof(f1736,plain,(
% 0.29/1.09 select(queue_181,tail)=index_180),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f609,f364])).
% 0.29/1.09 fof(f1737,plain,(
% 0.29/1.09 queue_185=store(queue_181,seq,earray_184)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f707,f610])).
% 0.29/1.09 fof(f1738,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_185,X0)=select(queue_181,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1737,f366])).
% 0.29/1.09 fof(f1768,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_187,X0)=select(queue_185,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f611,f366])).
% 0.29/1.09 fof(f1769,plain,(
% 0.29/1.09 select(queue_187,tail)=index_186),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f611,f364])).
% 0.29/1.09 fof(f1826,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_19,X0)=select(queue_17,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f612,f366])).
% 0.29/1.09 fof(f1827,plain,(
% 0.29/1.09 select(queue_19,tail)=index_18),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f612,f364])).
% 0.29/1.09 fof(f1828,plain,(
% 0.29/1.09 queue_191=store(queue_187,seq,earray_190)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f708,f613])).
% 0.29/1.09 fof(f1829,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_191,X0)=select(queue_187,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1828,f366])).
% 0.29/1.09 fof(f1950,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_193,X0)=select(queue_191,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f614,f366])).
% 0.29/1.09 fof(f1951,plain,(
% 0.29/1.09 select(queue_193,tail)=index_192),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f614,f364])).
% 0.29/1.09 fof(f1952,plain,(
% 0.29/1.09 queue_197=store(queue_193,seq,earray_196)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f709,f615])).
% 0.29/1.09 fof(f1953,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_197,X0)=select(queue_193,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1952,f366])).
% 0.29/1.09 fof(f1955,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_199,X0)=select(queue_197,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f616,f366])).
% 0.29/1.09 fof(f1956,plain,(
% 0.29/1.09 select(queue_199,tail)=index_198),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f616,f364])).
% 0.29/1.09 fof(f1957,plain,(
% 0.29/1.09 index_105=index_102),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1413,f1276])).
% 0.29/1.09 fof(f1958,plain,(
% 0.29/1.09 s(index_108)=p(index_102)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1957,f1395])).
% 0.29/1.09 fof(f1965,plain,(
% 0.29/1.09 s(index_108)=index_99),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f755,f1958])).
% 0.29/1.09 fof(f1967,plain,(
% 0.29/1.09 queue_203=store(queue_139,seq,earray_202)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f700,f617])).
% 0.29/1.09 fof(f1968,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_203,X0)=select(queue_139,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1967,f366])).
% 0.29/1.09 fof(f1992,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_205,X0)=select(queue_203,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f618,f366])).
% 0.29/1.09 fof(f1993,plain,(
% 0.29/1.09 select(queue_205,tail)=index_204),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f618,f364])).
% 0.29/1.09 fof(f1994,plain,(
% 0.29/1.09 queue_209=store(queue_199,seq,earray_208)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f710,f619])).
% 0.29/1.09 fof(f1995,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_209,X0)=select(queue_199,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f1994,f366])).
% 0.29/1.09 fof(f1997,plain,(
% 0.29/1.09 index_111=index_108),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1428,f1277])).
% 0.29/1.09 fof(f2003,plain,(
% 0.29/1.09 index_114=s(index_108)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1997,f481])).
% 0.29/1.09 fof(f2016,plain,(
% 0.29/1.09 index_114=index_99),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2003,f1965])).
% 0.29/1.09 fof(f2026,plain,(
% 0.29/1.09 index_114=select(queue_97,tail)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2016,f1344])).
% 0.29/1.09 fof(f2032,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_211,X0)=select(queue_209,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f620,f366])).
% 0.29/1.09 fof(f2033,plain,(
% 0.29/1.09 select(queue_211,tail)=index_210),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f620,f364])).
% 0.29/1.09 fof(f2034,plain,(
% 0.29/1.09 queue_215=store(queue_211,seq,earray_214)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f712,f621])).
% 0.29/1.09 fof(f2035,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_215,X0)=select(queue_211,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2034,f366])).
% 0.29/1.09 fof(f2037,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_217,X0)=select(queue_215,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f622,f366])).
% 0.29/1.09 fof(f2038,plain,(
% 0.29/1.09 select(queue_217,tail)=index_216),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f622,f364])).
% 0.29/1.09 fof(f2043,plain,(
% 0.29/1.09 queue_221=store(queue_217,seq,earray_220)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f713,f623])).
% 0.29/1.09 fof(f2044,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_221,X0)=select(queue_217,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2043,f366])).
% 0.29/1.09 fof(f2046,plain,(
% 0.29/1.09 index_117=index_114),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1445,f1278])).
% 0.29/1.09 fof(f2050,plain,(
% 0.29/1.09 p(index_120)=index_114),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2046,f774])).
% 0.29/1.09 fof(f2072,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_223,X0)=select(queue_221,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f624,f366])).
% 0.29/1.09 fof(f2073,plain,(
% 0.29/1.09 select(queue_223,tail)=index_222),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f624,f364])).
% 0.29/1.09 fof(f2074,plain,(
% 0.29/1.09 queue_227=store(queue_223,seq,earray_226)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f714,f625])).
% 0.29/1.09 fof(f2075,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_227,X0)=select(queue_223,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2074,f366])).
% 0.29/1.09 fof(f2090,plain,(
% 0.29/1.09 index_123=index_120),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1453,f1279])).
% 0.29/1.09 fof(f2091,plain,(
% 0.29/1.09 s(index_126)=p(index_120)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2090,f1391])).
% 0.29/1.09 fof(f2098,plain,(
% 0.29/1.09 s(index_126)=index_114),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f2050,f2091])).
% 0.29/1.09 fof(f2100,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_229,X0)=select(queue_227,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f626,f366])).
% 0.29/1.09 fof(f2101,plain,(
% 0.29/1.09 select(queue_229,tail)=index_228),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f626,f364])).
% 0.29/1.09 fof(f2102,plain,(
% 0.29/1.09 queue_23=store(queue_19,seq,earray_22)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f680,f627])).
% 0.29/1.09 fof(f2103,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_23,X0)=select(queue_19,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2102,f366])).
% 0.29/1.09 fof(f2105,plain,(
% 0.29/1.09 queue_233=store(queue_229,seq,earray_232)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f715,f628])).
% 0.29/1.09 fof(f2106,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_233,X0)=select(queue_229,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2105,f366])).
% 0.29/1.09 fof(f2132,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_235,X0)=select(queue_233,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f629,f366])).
% 0.29/1.09 fof(f2133,plain,(
% 0.29/1.09 select(queue_235,tail)=index_234),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f629,f364])).
% 0.29/1.09 fof(f2139,plain,(
% 0.29/1.09 index_129=index_126),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1464,f1280])).
% 0.29/1.09 fof(f2140,plain,(
% 0.29/1.09 queue_239=store(queue_235,seq,earray_238)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f716,f630])).
% 0.29/1.09 fof(f2141,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_239,X0)=select(queue_235,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2140,f366])).
% 0.29/1.09 fof(f2143,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_241,X0)=select(queue_239,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f631,f366])).
% 0.29/1.09 fof(f2144,plain,(
% 0.29/1.09 select(queue_241,tail)=index_240),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f631,f364])).
% 0.29/1.09 fof(f2151,plain,(
% 0.29/1.09 index_132=s(index_126)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2139,f488])).
% 0.29/1.09 fof(f2163,plain,(
% 0.29/1.09 index_132=index_114),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2151,f2098])).
% 0.29/1.09 fof(f2184,plain,(
% 0.29/1.09 queue_245=store(queue_241,seq,earray_244)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f717,f632])).
% 0.29/1.09 fof(f2185,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_245,X0)=select(queue_241,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2184,f366])).
% 0.29/1.09 fof(f2187,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_247,X0)=select(queue_245,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f633,f366])).
% 0.29/1.09 fof(f2188,plain,(
% 0.29/1.09 select(queue_247,tail)=index_246),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f633,f364])).
% 0.29/1.09 fof(f2189,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_25,X0)=select(queue_23,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f634,f366])).
% 0.29/1.09 fof(f2190,plain,(
% 0.29/1.09 select(queue_25,tail)=index_24),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f634,f364])).
% 0.29/1.09 fof(f2191,plain,(
% 0.29/1.09 index_15=index_12),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1477,f1284])).
% 0.29/1.09 fof(f2192,plain,(
% 0.29/1.09 s(index_18)=p(index_12)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2191,f1382])).
% 0.29/1.09 fof(f2199,plain,(
% 0.29/1.09 s(index_18)=index_9),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f770,f2192])).
% 0.29/1.09 fof(f2201,plain,(
% 0.29/1.09 queue_251=store(queue_247,seq,earray_250)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f718,f635])).
% 0.29/1.09 fof(f2202,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_251,X0)=select(queue_247,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2201,f366])).
% 0.29/1.09 fof(f2226,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_253,X0)=select(queue_251,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f636,f366])).
% 0.29/1.09 fof(f2227,plain,(
% 0.29/1.09 select(queue_253,tail)=index_252),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f636,f364])).
% 0.29/1.09 fof(f2228,plain,(
% 0.29/1.09 queue_257=store(queue_253,seq,earray_256)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f719,f637])).
% 0.29/1.09 fof(f2229,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_257,X0)=select(queue_253,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2228,f366])).
% 0.29/1.09 fof(f2231,plain,(
% 0.29/1.09 index_141=index_132),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1482,f1282])).
% 0.29/1.09 fof(f2235,plain,(
% 0.29/1.09 p(index_144)=index_132),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2231,f795])).
% 0.29/1.09 fof(f2267,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_259,X0)=select(queue_257,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f638,f366])).
% 0.29/1.09 fof(f2268,plain,(
% 0.29/1.09 select(queue_259,tail)=index_258),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f638,f364])).
% 0.29/1.09 fof(f2269,plain,(
% 0.29/1.09 queue_263=store(queue_259,seq,earray_262)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f720,f639])).
% 0.29/1.09 fof(f2270,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_263,X0)=select(queue_259,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2269,f366])).
% 0.29/1.09 fof(f2272,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_265,X0)=select(queue_263,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f640,f366])).
% 0.29/1.09 fof(f2273,plain,(
% 0.29/1.09 select(queue_265,tail)=index_264),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f640,f364])).
% 0.29/1.09 fof(f2274,plain,(
% 0.29/1.09 index_299=index_264),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f1330,f2273])).
% 0.29/1.09 fof(f2278,plain,(
% 0.29/1.09 p(index_299)=index_261),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2274,f896])).
% 0.29/1.09 fof(f2282,plain,(
% 0.29/1.09 index_300=index_261),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f933,f2278])).
% 0.29/1.09 fof(f2284,plain,(
% 0.29/1.09 index_300=select(queue_259,tail)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2282,f1316])).
% 0.29/1.09 fof(f2286,plain,(
% 0.29/1.09 queue_269=store(queue_205,seq,earray_268)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f711,f641])).
% 0.29/1.09 fof(f2287,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_269,X0)=select(queue_205,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2286,f366])).
% 0.29/1.09 fof(f2297,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_271,X0)=select(queue_269,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f642,f366])).
% 0.29/1.09 fof(f2298,plain,(
% 0.29/1.09 select(queue_271,tail)=index_270),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f642,f364])).
% 0.29/1.09 fof(f2299,plain,(
% 0.29/1.09 queue_275=store(queue_271,seq,earray_274)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f722,f643])).
% 0.29/1.09 fof(f2300,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_275,X0)=select(queue_271,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2299,f366])).
% 0.29/1.09 fof(f2302,plain,(
% 0.29/1.09 index_201=index_138),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1495,f1301])).
% 0.29/1.09 fof(f2303,plain,(
% 0.29/1.09 s(index_204)=p(index_138)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2302,f1377])).
% 0.29/1.09 fof(f2310,plain,(
% 0.29/1.09 s(index_204)=index_135),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f791,f2303])).
% 0.29/1.09 fof(f2334,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_277,X0)=select(queue_275,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f644,f366])).
% 0.29/1.09 fof(f2335,plain,(
% 0.29/1.09 select(queue_277,tail)=index_276),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f644,f364])).
% 0.29/1.09 fof(f2336,plain,(
% 0.29/1.09 queue_281=store(queue_277,seq,earray_280)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f723,f645])).
% 0.29/1.09 fof(f2337,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_281,X0)=select(queue_277,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2336,f366])).
% 0.29/1.09 fof(f2339,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_283,X0)=select(queue_281,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f646,f366])).
% 0.29/1.09 fof(f2340,plain,(
% 0.29/1.09 select(queue_283,tail)=index_282),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f646,f364])).
% 0.29/1.09 fof(f2341,plain,(
% 0.29/1.09 index_147=index_144),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1500,f1283])).
% 0.29/1.09 fof(f2342,plain,(
% 0.29/1.09 s(index_150)=p(index_144)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2341,f1387])).
% 0.29/1.09 fof(f2349,plain,(
% 0.29/1.09 s(index_150)=index_132),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f2235,f2342])).
% 0.29/1.09 fof(f2351,plain,(
% 0.29/1.09 queue_287=store(queue_283,seq,earray_286)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f724,f647])).
% 0.29/1.09 fof(f2352,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_287,X0)=select(queue_283,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2351,f366])).
% 0.29/1.09 fof(f2380,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_289,X0)=select(queue_287,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f648,f366])).
% 0.29/1.09 fof(f2381,plain,(
% 0.29/1.09 select(queue_289,tail)=index_288),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f648,f364])).
% 0.29/1.09 fof(f2382,plain,(
% 0.29/1.09 queue_29=store(queue_25,seq,earray_28)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f681,f649])).
% 0.29/1.09 fof(f2383,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_29,X0)=select(queue_25,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2382,f366])).
% 0.29/1.09 fof(f2390,plain,(
% 0.29/1.09 index_153=index_150),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1505,f1285])).
% 0.29/1.09 fof(f2397,plain,(
% 0.29/1.09 index_156=s(index_150)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2390,f497])).
% 0.29/1.09 fof(f2405,plain,(
% 0.29/1.09 queue_293=store(queue_289,seq,earray_292)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f725,f650])).
% 0.29/1.09 fof(f2406,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_293,X0)=select(queue_289,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2405,f366])).
% 0.29/1.09 fof(f2408,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_295,X0)=select(queue_293,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f651,f366])).
% 0.29/1.09 fof(f2409,plain,(
% 0.29/1.09 select(queue_295,tail)=index_294),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f651,f364])).
% 0.29/1.09 fof(f2410,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_31,X0)=select(queue_29,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f652,f366])).
% 0.29/1.09 fof(f2411,plain,(
% 0.29/1.09 select(queue_31,tail)=index_30),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f652,f364])).
% 0.29/1.09 fof(f2416,plain,(
% 0.29/1.09 index_156=index_132),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2397,f2349])).
% 0.29/1.09 fof(f2432,plain,(
% 0.29/1.09 index_156=index_114),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2416,f2163])).
% 0.29/1.09 fof(f2434,plain,(
% 0.29/1.09 queue_35=store(queue_31,seq,earray_34)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f682,f653])).
% 0.29/1.09 fof(f2435,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_35,X0)=select(queue_31,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2434,f366])).
% 0.29/1.09 fof(f2442,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_37,X0)=select(queue_35,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f654,f366])).
% 0.29/1.09 fof(f2443,plain,(
% 0.29/1.09 select(queue_37,tail)=index_36),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f654,f364])).
% 0.29/1.09 fof(f2444,plain,(
% 0.29/1.09 queue_41=store(queue_37,seq,earray_40)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f683,f655])).
% 0.29/1.09 fof(f2445,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_41,X0)=select(queue_37,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2444,f366])).
% 0.29/1.09 fof(f2447,plain,(
% 0.29/1.09 index_159=index_156),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1510,f1292])).
% 0.29/1.09 fof(f2451,plain,(
% 0.29/1.09 p(index_162)=index_156),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2447,f808])).
% 0.29/1.09 fof(f2485,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_43,X0)=select(queue_41,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f656,f366])).
% 0.29/1.09 fof(f2486,plain,(
% 0.29/1.09 select(queue_43,tail)=index_42),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f656,f364])).
% 0.29/1.09 fof(f2487,plain,(
% 0.29/1.09 queue_47=store(queue_43,seq,earray_46)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f684,f657])).
% 0.29/1.09 fof(f2488,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_47,X0)=select(queue_43,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2487,f366])).
% 0.29/1.09 fof(f2490,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_49,X0)=select(queue_47,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f658,f366])).
% 0.29/1.09 fof(f2491,plain,(
% 0.29/1.09 select(queue_49,tail)=index_48),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f658,f364])).
% 0.29/1.09 fof(f2493,plain,(
% 0.29/1.09 queue_5=store(queue_1,seq,earray_4)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f677,f659])).
% 0.29/1.09 fof(f2494,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_5,X0)=select(queue_1,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2493,f366])).
% 0.29/1.09 fof(f2504,plain,(
% 0.29/1.09 queue_53=store(queue_49,seq,earray_52)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f685,f660])).
% 0.29/1.09 fof(f2505,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_53,X0)=select(queue_49,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2504,f366])).
% 0.29/1.09 fof(f2507,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_55,X0)=select(queue_53,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f661,f366])).
% 0.29/1.09 fof(f2508,plain,(
% 0.29/1.09 select(queue_55,tail)=index_54),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f661,f364])).
% 0.29/1.09 fof(f2510,plain,(
% 0.29/1.09 index_165=index_162),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1550,f1293])).
% 0.29/1.09 fof(f2511,plain,(
% 0.29/1.09 s(index_168)=p(index_162)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2510,f1384])).
% 0.29/1.09 fof(f2518,plain,(
% 0.29/1.09 s(index_168)=index_156),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f2451,f2511])).
% 0.29/1.09 fof(f2548,plain,(
% 0.29/1.09 queue_59=store(queue_55,seq,earray_58)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f686,f662])).
% 0.29/1.09 fof(f2549,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_59,X0)=select(queue_55,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2548,f366])).
% 0.29/1.09 fof(f2551,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_61,X0)=select(queue_59,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f663,f366])).
% 0.29/1.09 fof(f2552,plain,(
% 0.29/1.09 select(queue_61,tail)=index_60),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f663,f364])).
% 0.29/1.09 fof(f2553,plain,(
% 0.29/1.09 queue_65=store(queue_61,seq,earray_64)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f687,f664])).
% 0.29/1.09 fof(f2554,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_65,X0)=select(queue_61,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2553,f366])).
% 0.29/1.09 fof(f2557,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_67,X0)=select(queue_65,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f665,f366])).
% 0.29/1.09 fof(f2558,plain,(
% 0.29/1.09 select(queue_67,tail)=index_66),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f665,f364])).
% 0.29/1.09 fof(f2563,plain,(
% 0.29/1.09 index_171=index_168),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1555,f1294])).
% 0.29/1.09 fof(f2570,plain,(
% 0.29/1.09 index_174=s(index_168)),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2563,f503])).
% 0.29/1.09 fof(f2573,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_7,X0)=select(queue_5,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f666,f366])).
% 0.29/1.09 fof(f2574,plain,(
% 0.29/1.09 select(queue_7,tail)=index_6),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f666,f364])).
% 0.29/1.09 fof(f2575,plain,(
% 0.29/1.09 queue_71=store(queue_7,seq,earray_70)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f678,f667])).
% 0.29/1.09 fof(f2576,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_71,X0)=select(queue_7,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2575,f366])).
% 0.29/1.09 fof(f2587,plain,(
% 0.29/1.09 index_174=index_156),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2570,f2518])).
% 0.29/1.09 fof(f2601,plain,(
% 0.29/1.09 index_174=index_114),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2587,f2432])).
% 0.29/1.09 fof(f2608,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_73,X0)=select(queue_71,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f668,f366])).
% 0.29/1.09 fof(f2609,plain,(
% 0.29/1.09 select(queue_73,tail)=index_72),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f668,f364])).
% 0.29/1.09 fof(f2610,plain,(
% 0.29/1.09 queue_77=store(queue_67,seq,earray_76)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f688,f669])).
% 0.29/1.09 fof(f2611,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_77,X0)=select(queue_67,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2610,f366])).
% 0.29/1.09 fof(f2613,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_79,X0)=select(queue_77,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f670,f366])).
% 0.29/1.09 fof(f2614,plain,(
% 0.29/1.09 select(queue_79,tail)=index_78),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f670,f364])).
% 0.29/1.09 fof(f2620,plain,(
% 0.29/1.09 queue_83=store(queue_79,seq,earray_82)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f690,f671])).
% 0.29/1.09 fof(f2621,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_83,X0)=select(queue_79,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2620,f366])).
% 0.29/1.09 fof(f2630,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_85,X0)=select(queue_83,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f672,f366])).
% 0.29/1.09 fof(f2631,plain,(
% 0.29/1.09 select(queue_85,tail)=index_84),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f672,f364])).
% 0.29/1.09 fof(f2632,plain,(
% 0.29/1.09 queue_89=store(queue_85,seq,earray_88)),
% 0.29/1.09 inference(forward_demodulation,[status(thm)],[f691,f673])).
% 0.29/1.09 fof(f2633,plain,(
% 0.29/1.09 ![X0]: (seq=X0|select(queue_89,X0)=select(queue_85,X0))),
% 0.29/1.09 inference(paramodulation,[status(thm)],[f2632,f366])).
% 0.29/1.09 fof(f2639,plain,(
% 0.29/1.09 index_177=index_174),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f1647,f1295])).
% 0.29/1.09 fof(f2643,plain,(
% 0.29/1.09 p(index_180)=index_174),
% 0.29/1.09 inference(backward_demodulation,[status(thm)],[f2639,f827])).
% 0.29/1.09 fof(f2665,plain,(
% 0.29/1.09 ![X0]: (tail=X0|select(queue_91,X0)=select(queue_89,X0))),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f674,f366])).
% 0.29/1.10 fof(f2666,plain,(
% 0.29/1.10 select(queue_91,tail)=index_90),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f674,f364])).
% 0.29/1.10 fof(f2667,plain,(
% 0.29/1.10 queue_95=store(queue_91,seq,earray_94)),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f692,f675])).
% 0.29/1.10 fof(f2668,plain,(
% 0.29/1.10 ![X0]: (seq=X0|select(queue_95,X0)=select(queue_91,X0))),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2667,f366])).
% 0.29/1.10 fof(f2670,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_97,X0)=select(queue_95,X0))),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f676,f366])).
% 0.29/1.10 fof(f2671,plain,(
% 0.29/1.10 select(queue_97,tail)=index_96),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f676,f364])).
% 0.29/1.10 fof(f2697,plain,(
% 0.29/1.10 index_174=select(queue_97,tail)),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f2601,f2026])).
% 0.29/1.10 fof(f2721,plain,(
% 0.29/1.10 index_183=index_180),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f1736,f1298])).
% 0.29/1.10 fof(f2722,plain,(
% 0.29/1.10 s(index_186)=p(index_180)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2721,f1380])).
% 0.29/1.10 fof(f2729,plain,(
% 0.29/1.10 s(index_186)=index_174),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f2643,f2722])).
% 0.29/1.10 fof(f2789,plain,(
% 0.29/1.10 index_189=index_186),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f1769,f1299])).
% 0.29/1.10 fof(f2799,plain,(
% 0.29/1.10 index_192=s(index_186)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2789,f510])).
% 0.29/1.10 fof(f2811,plain,(
% 0.29/1.10 index_192=index_174),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2799,f2729])).
% 0.29/1.10 fof(f2824,plain,(
% 0.29/1.10 index_192=select(queue_97,tail)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2811,f2697])).
% 0.29/1.10 fof(f2876,plain,(
% 0.29/1.10 index_21=index_18),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f1827,f1303])).
% 0.29/1.10 fof(f2881,plain,(
% 0.29/1.10 p(index_24)=index_18),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2876,f876])).
% 0.29/1.10 fof(f2883,plain,(
% 0.29/1.10 index_24=s(index_18)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2876,f527])).
% 0.29/1.10 fof(f2901,plain,(
% 0.29/1.10 index_24=index_9),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2883,f2199])).
% 0.29/1.10 fof(f2911,plain,(
% 0.29/1.10 index_24=select(queue_295,tail)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2901,f1342])).
% 0.29/1.10 fof(f2957,plain,(
% 0.29/1.10 index_195=index_192),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f1951,f1300])).
% 0.29/1.10 fof(f2961,plain,(
% 0.29/1.10 p(index_198)=index_192),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2957,f839])).
% 0.29/1.10 fof(f3028,plain,(
% 0.29/1.10 index_207=index_198),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f1956,f1302])).
% 0.29/1.10 fof(f3029,plain,(
% 0.29/1.10 s(index_210)=p(index_198)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3028,f1376])).
% 0.29/1.10 fof(f3036,plain,(
% 0.29/1.10 s(index_210)=index_192),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f2961,f3029])).
% 0.29/1.10 fof(f3097,plain,(
% 0.29/1.10 index_267=index_204),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f1993,f1317])).
% 0.29/1.10 fof(f3104,plain,(
% 0.29/1.10 index_270=s(index_204)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3097,f539])).
% 0.29/1.10 fof(f3118,plain,(
% 0.29/1.10 index_270=index_135),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3104,f2310])).
% 0.29/1.10 fof(f3128,plain,(
% 0.29/1.10 index_270=select(queue_73,tail)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3118,f1281])).
% 0.29/1.10 fof(f3140,plain,(
% 0.29/1.10 index_213=index_210),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2033,f1304])).
% 0.29/1.10 fof(f3147,plain,(
% 0.29/1.10 index_216=s(index_210)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3140,f519])).
% 0.29/1.10 fof(f3165,plain,(
% 0.29/1.10 index_216=index_192),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3147,f3036])).
% 0.29/1.10 fof(f3174,plain,(
% 0.29/1.10 index_216=select(queue_97,tail)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3165,f2824])).
% 0.29/1.10 fof(f3210,plain,(
% 0.29/1.10 index_219=index_216),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2038,f1305])).
% 0.29/1.10 fof(f3215,plain,(
% 0.29/1.10 p(index_222)=index_216),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3210,f861])).
% 0.29/1.10 fof(f3290,plain,(
% 0.29/1.10 index_225=index_222),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2073,f1310])).
% 0.29/1.10 fof(f3291,plain,(
% 0.29/1.10 s(index_228)=p(index_222)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3290,f1373])).
% 0.29/1.10 fof(f3298,plain,(
% 0.29/1.10 s(index_228)=index_216),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f3215,f3291])).
% 0.29/1.10 fof(f3363,plain,(
% 0.29/1.10 index_231=index_228),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2101,f1311])).
% 0.29/1.10 fof(f3373,plain,(
% 0.29/1.10 index_234=s(index_228)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3363,f525])).
% 0.29/1.10 fof(f3385,plain,(
% 0.29/1.10 index_234=index_216),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3373,f3298])).
% 0.29/1.10 fof(f3428,plain,(
% 0.29/1.10 index_234=select(queue_97,tail)),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f3385,f3174])).
% 0.29/1.10 fof(f3430,plain,(
% 0.29/1.10 index_237=index_234),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2133,f1312])).
% 0.29/1.10 fof(f3435,plain,(
% 0.29/1.10 p(index_240)=index_234),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3430,f880])).
% 0.29/1.10 fof(f3504,plain,(
% 0.29/1.10 index_243=index_240),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2144,f1313])).
% 0.29/1.10 fof(f3505,plain,(
% 0.29/1.10 s(index_246)=p(index_240)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3504,f1369])).
% 0.29/1.10 fof(f3512,plain,(
% 0.29/1.10 s(index_246)=index_234),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f3435,f3505])).
% 0.29/1.10 fof(f3589,plain,(
% 0.29/1.10 index_249=index_246),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2188,f1314])).
% 0.29/1.10 fof(f3596,plain,(
% 0.29/1.10 index_252=s(index_246)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3589,f532])).
% 0.29/1.10 fof(f3608,plain,(
% 0.29/1.10 index_252=index_234),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3596,f3512])).
% 0.29/1.10 fof(f3633,plain,(
% 0.29/1.10 index_252=select(queue_97,tail)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3608,f3428])).
% 0.29/1.10 fof(f3672,plain,(
% 0.29/1.10 index_27=index_24),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2190,f1318])).
% 0.29/1.10 fof(f3673,plain,(
% 0.29/1.10 s(index_30)=p(index_24)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3672,f1360])).
% 0.29/1.10 fof(f3680,plain,(
% 0.29/1.10 s(index_30)=index_18),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f2881,f3673])).
% 0.29/1.10 fof(f3725,plain,(
% 0.29/1.10 index_255=index_252),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2227,f1315])).
% 0.29/1.10 fof(f3732,plain,(
% 0.29/1.10 index_258=s(index_252)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3725,f534])).
% 0.29/1.10 fof(f3814,plain,(
% 0.29/1.10 index_300=index_258),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2268,f2284])).
% 0.29/1.10 fof(f3822,plain,(
% 0.29/1.10 elem_301=select(earray_296,index_258)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3814,f475])).
% 0.29/1.10 fof(f3906,plain,(
% 0.29/1.10 index_273=index_270),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2298,f1319])).
% 0.29/1.10 fof(f3914,plain,(
% 0.29/1.10 p(index_276)=index_270),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3906,f909])).
% 0.29/1.10 fof(f3955,plain,(
% 0.29/1.10 index_279=index_276),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2335,f1320])).
% 0.29/1.10 fof(f3956,plain,(
% 0.29/1.10 s(index_282)=p(index_276)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f3955,f1363])).
% 0.29/1.10 fof(f3963,plain,(
% 0.29/1.10 s(index_282)=index_270),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f3914,f3956])).
% 0.29/1.10 fof(f4003,plain,(
% 0.29/1.10 index_285=index_282),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2340,f1321])).
% 0.29/1.10 fof(f4010,plain,(
% 0.29/1.10 index_288=s(index_282)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4003,f545])).
% 0.29/1.10 fof(f4026,plain,(
% 0.29/1.10 index_288=index_270),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4010,f3963])).
% 0.29/1.10 fof(f4041,plain,(
% 0.29/1.10 index_288=select(queue_73,tail)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4026,f3128])).
% 0.29/1.10 fof(f4057,plain,(
% 0.29/1.10 index_291=index_288),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2381,f1328])).
% 0.29/1.10 fof(f4062,plain,(
% 0.29/1.10 p(index_294)=index_288),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4057,f922])).
% 0.29/1.10 fof(f4104,plain,(
% 0.29/1.10 index_24=index_294),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2409,f2911])).
% 0.29/1.10 fof(f4120,plain,(
% 0.29/1.10 p(index_294)=index_18),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4104,f2881])).
% 0.29/1.10 fof(f4123,plain,(
% 0.29/1.10 index_288=index_18),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4062,f4120])).
% 0.29/1.10 fof(f4127,plain,(
% 0.29/1.10 s(index_30)=index_288),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4123,f3680])).
% 0.29/1.10 fof(f4176,plain,(
% 0.29/1.10 index_33=index_30),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2411,f1332])).
% 0.29/1.10 fof(f4183,plain,(
% 0.29/1.10 index_36=s(index_30)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4176,f554])).
% 0.29/1.10 fof(f4197,plain,(
% 0.29/1.10 index_36=index_288),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4183,f4127])).
% 0.29/1.10 fof(f4227,plain,(
% 0.29/1.10 index_39=index_36),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2443,f1333])).
% 0.29/1.10 fof(f4232,plain,(
% 0.29/1.10 p(index_42)=index_36),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4227,f941])).
% 0.29/1.10 fof(f4286,plain,(
% 0.29/1.10 index_45=index_42),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2486,f1334])).
% 0.29/1.10 fof(f4287,plain,(
% 0.29/1.10 s(index_48)=p(index_42)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4286,f1356])).
% 0.29/1.10 fof(f4294,plain,(
% 0.29/1.10 s(index_48)=index_36),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4232,f4287])).
% 0.29/1.10 fof(f4346,plain,(
% 0.29/1.10 index_51=index_48),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2491,f1335])).
% 0.29/1.10 fof(f4353,plain,(
% 0.29/1.10 index_54=s(index_48)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4346,f560])).
% 0.29/1.10 fof(f4365,plain,(
% 0.29/1.10 index_54=index_36),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4353,f4294])).
% 0.29/1.10 fof(f4395,plain,(
% 0.29/1.10 index_54=index_288),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4365,f4197])).
% 0.29/1.10 fof(f4411,plain,(
% 0.29/1.10 index_57=index_54),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2508,f1336])).
% 0.29/1.10 fof(f4416,plain,(
% 0.29/1.10 p(index_60)=index_54),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4411,f962])).
% 0.29/1.10 fof(f4462,plain,(
% 0.29/1.10 index_54=select(queue_73,tail)),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4395,f4041])).
% 0.29/1.10 fof(f4479,plain,(
% 0.29/1.10 index_63=index_60),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2552,f1337])).
% 0.29/1.10 fof(f4480,plain,(
% 0.29/1.10 s(index_66)=p(index_60)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4479,f1352])).
% 0.29/1.10 fof(f4487,plain,(
% 0.29/1.10 s(index_66)=index_54),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4416,f4480])).
% 0.29/1.10 fof(f4547,plain,(
% 0.29/1.10 index_75=index_66),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2558,f1339])).
% 0.29/1.10 fof(f4554,plain,(
% 0.29/1.10 index_78=s(index_66)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4547,f569])).
% 0.29/1.10 fof(f4566,plain,(
% 0.29/1.10 index_78=index_54),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4554,f4487])).
% 0.29/1.10 fof(f4579,plain,(
% 0.29/1.10 index_78=select(queue_73,tail)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4566,f4462])).
% 0.29/1.10 fof(f4620,plain,(
% 0.29/1.10 index_69=index_6),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2574,f1338])).
% 0.29/1.10 fof(f4621,plain,(
% 0.29/1.10 s(index_72)=p(index_6)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4620,f1351])).
% 0.29/1.10 fof(f4628,plain,(
% 0.29/1.10 s(index_72)=index_3),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f953,f4621])).
% 0.29/1.10 fof(f4665,plain,(
% 0.29/1.10 index_81=index_78),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2614,f1340])).
% 0.29/1.10 fof(f4670,plain,(
% 0.29/1.10 p(index_84)=index_78),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4665,f979])).
% 0.29/1.10 fof(f4738,plain,(
% 0.29/1.10 index_87=index_84),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2631,f1341])).
% 0.29/1.10 fof(f4739,plain,(
% 0.29/1.10 s(index_90)=p(index_84)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4738,f1348])).
% 0.29/1.10 fof(f4743,plain,(
% 0.29/1.10 p(index_90)=index_84),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4738,f983])).
% 0.29/1.10 fof(f4746,plain,(
% 0.29/1.10 s(index_90)=index_78),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4670,f4739])).
% 0.29/1.10 fof(f4812,plain,(
% 0.29/1.10 index_93=index_90),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2666,f1343])).
% 0.29/1.10 fof(f4817,plain,(
% 0.29/1.10 s(index_96)=p(index_90)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4812,f1347])).
% 0.29/1.10 fof(f4823,plain,(
% 0.29/1.10 index_96=s(index_90)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4812,f576])).
% 0.29/1.10 fof(f4824,plain,(
% 0.29/1.10 s(index_96)=index_84),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4743,f4817])).
% 0.29/1.10 fof(f4835,plain,(
% 0.29/1.10 index_96=index_78),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4823,f4746])).
% 0.29/1.10 fof(f4872,plain,(
% 0.29/1.10 index_96=index_72),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4873,f2609])).
% 0.29/1.10 fof(f4873,plain,(
% 0.29/1.10 index_96=select(queue_73,tail)),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4835,f4579])).
% 0.29/1.10 fof(f4880,plain,(
% 0.29/1.10 s(index_96)=index_3),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4872,f4628])).
% 0.29/1.10 fof(f4885,plain,(
% 0.29/1.10 index_84=index_3),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4824,f4880])).
% 0.29/1.10 fof(f4894,plain,(
% 0.29/1.10 index_84=select(queue_1,tail)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4885,f1331])).
% 0.29/1.10 fof(f4922,plain,(
% 0.29/1.10 index_252=index_96),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f2671,f3633])).
% 0.29/1.10 fof(f4947,plain,(
% 0.29/1.10 index_258=s(index_96)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4922,f3732])).
% 0.29/1.10 fof(f4969,plain,(
% 0.29/1.10 index_258=index_84),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4824,f4947])).
% 0.29/1.10 fof(f5032,plain,(
% 0.29/1.10 elem_301=select(earray_296,index_84)),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f4969,f3822])).
% 0.29/1.10 fof(f5506,plain,(
% 0.29/1.10 head=tail|select(queue_1,tail)=index_0),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f476,f1407])).
% 0.29/1.10 fof(f5508,plain,(
% 0.29/1.10 head=tail|index_84=index_0),
% 0.29/1.10 inference(forward_demodulation,[status(thm)],[f4894,f5506])).
% 0.29/1.10 fof(f5509,plain,(
% 0.29/1.10 index_84=index_0),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f5508,f367])).
% 0.29/1.10 fof(f5512,plain,(
% 0.29/1.10 select(queue_1,head)=index_84),
% 0.29/1.10 inference(backward_demodulation,[status(thm)],[f5509,f1408])).
% 0.29/1.10 fof(f5522,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_103,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1410,f1412])).
% 0.29/1.10 fof(f5672,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_13,X0)=select(queue_295,X0)|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1430,f1476])).
% 0.29/1.10 fof(f5738,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_139,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1486,f1494])).
% 0.29/1.10 fof(f6875,plain,(
% 0.29/1.10 seq=head|select(queue_5,head)=index_84),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f5512,f2494])).
% 0.29/1.10 fof(f6881,plain,(
% 0.29/1.10 select(queue_5,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f6875,f368])).
% 0.29/1.10 fof(f6999,plain,(
% 0.29/1.10 tail=head|select(queue_7,head)=index_84),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f6881,f2573])).
% 0.29/1.10 fof(f7004,plain,(
% 0.29/1.10 select(queue_7,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f6999,f367])).
% 0.29/1.10 fof(f7025,plain,(
% 0.29/1.10 seq=head|select(queue_71,head)=index_84),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f7004,f2576])).
% 0.29/1.10 fof(f7031,plain,(
% 0.29/1.10 select(queue_71,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f7025,f368])).
% 0.29/1.10 fof(f7035,plain,(
% 0.29/1.10 tail=head|select(queue_73,head)=index_84),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f7031,f2608])).
% 0.29/1.10 fof(f7039,plain,(
% 0.29/1.10 select(queue_73,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f7035,f367])).
% 0.29/1.10 fof(f7695,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_107,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1419,f5522])).
% 0.29/1.10 fof(f7699,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_107,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7695])).
% 0.29/1.10 fof(f7703,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_17,X0)=select(queue_295,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1585,f5672])).
% 0.29/1.10 fof(f7707,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_17,X0)=select(queue_295,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7703])).
% 0.29/1.10 fof(f7711,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_203,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1968,f5738])).
% 0.29/1.10 fof(f7715,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_203,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7711])).
% 0.29/1.10 fof(f7737,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_109,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1427,f7699])).
% 0.29/1.10 fof(f7741,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_109,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7737])).
% 0.29/1.10 fof(f7745,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_19,X0)=select(queue_295,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1826,f7707])).
% 0.29/1.10 fof(f7749,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_19,X0)=select(queue_295,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7745])).
% 0.29/1.10 fof(f7753,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_205,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1992,f7715])).
% 0.29/1.10 fof(f7757,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_205,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7753])).
% 0.29/1.10 fof(f7761,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_113,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1442,f7741])).
% 0.29/1.10 fof(f7765,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_113,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7761])).
% 0.29/1.10 fof(f7789,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_23,X0)=select(queue_295,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2103,f7749])).
% 0.29/1.10 fof(f7793,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_23,X0)=select(queue_295,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7789])).
% 0.29/1.10 fof(f7797,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_269,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2287,f7757])).
% 0.29/1.10 fof(f7801,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_269,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7797])).
% 0.29/1.10 fof(f7805,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_115,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1444,f7765])).
% 0.29/1.10 fof(f7809,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_115,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7805])).
% 0.29/1.10 fof(f7813,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_25,X0)=select(queue_295,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2189,f7793])).
% 0.29/1.10 fof(f7817,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_25,X0)=select(queue_295,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7813])).
% 0.29/1.10 fof(f7821,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_271,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2297,f7801])).
% 0.29/1.10 fof(f7825,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_271,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7821])).
% 0.29/1.10 fof(f7829,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_119,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1447,f7809])).
% 0.29/1.10 fof(f7833,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_119,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7829])).
% 0.29/1.10 fof(f7847,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_29,X0)=select(queue_295,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2383,f7817])).
% 0.29/1.10 fof(f7851,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_29,X0)=select(queue_295,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7847])).
% 0.29/1.10 fof(f7855,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_275,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2300,f7825])).
% 0.29/1.10 fof(f7859,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_275,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7855])).
% 0.29/1.10 fof(f7863,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_121,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1452,f7833])).
% 0.29/1.10 fof(f7867,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_121,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7863])).
% 0.29/1.10 fof(f7871,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_31,X0)=select(queue_295,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2410,f7851])).
% 0.29/1.10 fof(f7875,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_31,X0)=select(queue_295,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7871])).
% 0.29/1.10 fof(f7879,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_277,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2334,f7859])).
% 0.29/1.10 fof(f7883,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_277,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7879])).
% 0.29/1.10 fof(f7887,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_125,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1461,f7867])).
% 0.29/1.10 fof(f7891,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_125,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7887])).
% 0.29/1.10 fof(f7915,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_281,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2337,f7883])).
% 0.29/1.10 fof(f7919,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_281,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7915])).
% 0.29/1.10 fof(f7923,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_127,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1463,f7891])).
% 0.29/1.10 fof(f7927,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_127,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7923])).
% 0.29/1.10 fof(f7931,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_283,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2339,f7919])).
% 0.29/1.10 fof(f7935,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_283,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7931])).
% 0.29/1.10 fof(f7939,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_131,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1479,f7927])).
% 0.29/1.10 fof(f7943,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_131,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7939])).
% 0.29/1.10 fof(f7947,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_287,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2352,f7935])).
% 0.29/1.10 fof(f7951,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_287,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7947])).
% 0.29/1.10 fof(f7965,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_133,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1481,f7943])).
% 0.29/1.10 fof(f7969,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_133,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7965])).
% 0.29/1.10 fof(f7973,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_289,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2380,f7951])).
% 0.29/1.10 fof(f7977,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_289,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7973])).
% 0.29/1.10 fof(f7981,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_143,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1497,f7969])).
% 0.29/1.10 fof(f7985,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_143,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7981])).
% 0.29/1.10 fof(f7989,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_293,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2406,f7977])).
% 0.29/1.10 fof(f7993,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_293,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7989])).
% 0.29/1.10 fof(f7997,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_145,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1499,f7985])).
% 0.29/1.10 fof(f8001,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_145,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f7997])).
% 0.29/1.10 fof(f8005,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_295,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2408,f7993])).
% 0.29/1.10 fof(f8009,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_295,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8005])).
% 0.29/1.10 fof(f8033,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_149,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1502,f8001])).
% 0.29/1.10 fof(f8037,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_149,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8033])).
% 0.29/1.10 fof(f8041,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_31,X0)=select(queue_73,X0)|seq=X0|tail=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f7875,f8009])).
% 0.29/1.10 fof(f8045,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_31,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8041])).
% 0.29/1.10 fof(f8049,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_151,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1504,f8037])).
% 0.29/1.10 fof(f8053,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_151,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8049])).
% 0.29/1.10 fof(f8057,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_35,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2435,f8045])).
% 0.29/1.10 fof(f8061,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_35,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8057])).
% 0.29/1.10 fof(f8065,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_155,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1507,f8053])).
% 0.29/1.10 fof(f8069,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_155,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8065])).
% 0.29/1.10 fof(f8073,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_37,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2442,f8061])).
% 0.29/1.10 fof(f8077,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_37,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8073])).
% 0.29/1.10 fof(f8091,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_157,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1509,f8069])).
% 0.29/1.10 fof(f8095,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_157,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8091])).
% 0.29/1.10 fof(f8099,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_41,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2445,f8077])).
% 0.29/1.10 fof(f8103,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_41,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8099])).
% 0.29/1.10 fof(f8107,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_161,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1512,f8095])).
% 0.29/1.10 fof(f8111,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_161,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8107])).
% 0.29/1.10 fof(f8115,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_43,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2485,f8103])).
% 0.29/1.10 fof(f8119,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_43,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8115])).
% 0.29/1.10 fof(f8123,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_163,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1549,f8111])).
% 0.29/1.10 fof(f8127,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_163,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8123])).
% 0.29/1.10 fof(f8131,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_47,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2488,f8119])).
% 0.29/1.10 fof(f8135,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_47,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8131])).
% 0.29/1.10 fof(f8159,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_167,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1552,f8127])).
% 0.29/1.10 fof(f8163,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_167,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8159])).
% 0.29/1.10 fof(f8167,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_49,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2490,f8135])).
% 0.29/1.10 fof(f8171,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_49,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8167])).
% 0.29/1.10 fof(f8175,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_169,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1554,f8163])).
% 0.29/1.10 fof(f8179,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_169,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8175])).
% 0.29/1.10 fof(f8183,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_53,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2505,f8171])).
% 0.29/1.10 fof(f8187,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_53,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8183])).
% 0.29/1.10 fof(f8191,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_173,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1644,f8179])).
% 0.29/1.10 fof(f8195,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_173,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8191])).
% 0.29/1.10 fof(f8199,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_55,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2507,f8187])).
% 0.29/1.10 fof(f8203,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_55,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8199])).
% 0.29/1.10 fof(f8217,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_175,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1646,f8195])).
% 0.29/1.10 fof(f8221,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_175,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8217])).
% 0.29/1.10 fof(f8225,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_59,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2549,f8203])).
% 0.29/1.10 fof(f8229,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_59,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8225])).
% 0.29/1.10 fof(f8233,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_179,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1733,f8221])).
% 0.29/1.10 fof(f8237,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_179,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8233])).
% 0.29/1.10 fof(f8241,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_61,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2551,f8229])).
% 0.29/1.10 fof(f8245,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_61,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8241])).
% 0.29/1.10 fof(f8249,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_181,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1735,f8237])).
% 0.29/1.10 fof(f8253,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_181,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8249])).
% 0.29/1.10 fof(f8257,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_65,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2554,f8245])).
% 0.29/1.10 fof(f8261,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_65,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8257])).
% 0.29/1.10 fof(f8285,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_185,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1738,f8253])).
% 0.29/1.10 fof(f8289,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_185,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8285])).
% 0.29/1.10 fof(f8293,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_67,X0)=select(queue_73,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2557,f8261])).
% 0.29/1.10 fof(f8297,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_67,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8293])).
% 0.29/1.10 fof(f8301,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_187,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1768,f8289])).
% 0.29/1.10 fof(f8305,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_187,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8301])).
% 0.29/1.10 fof(f8309,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_77,X0)=select(queue_73,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2611,f8297])).
% 0.29/1.10 fof(f8313,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_77,X0)=select(queue_73,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8309])).
% 0.29/1.10 fof(f8317,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_191,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1829,f8305])).
% 0.29/1.10 fof(f8321,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_191,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8317])).
% 0.29/1.10 fof(f8324,plain,(
% 0.29/1.10 tail=head|select(queue_77,head)=index_84|seq=head),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f7039,f8313])).
% 0.29/1.10 fof(f8329,plain,(
% 0.29/1.10 select(queue_77,head)=index_84|seq=head),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8324,f367])).
% 0.29/1.10 fof(f8341,plain,(
% 0.29/1.10 select(queue_77,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8329,f368])).
% 0.29/1.10 fof(f8342,plain,(
% 0.29/1.10 select(queue_79,head)=index_84|tail=head),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2613,f8341])).
% 0.29/1.10 fof(f8344,plain,(
% 0.29/1.10 select(queue_79,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8342,f367])).
% 0.29/1.10 fof(f8346,plain,(
% 0.29/1.10 select(queue_83,head)=index_84|seq=head),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2621,f8344])).
% 0.29/1.10 fof(f8348,plain,(
% 0.29/1.10 select(queue_83,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8346,f368])).
% 0.29/1.10 fof(f8350,plain,(
% 0.29/1.10 select(queue_85,head)=index_84|tail=head),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2630,f8348])).
% 0.29/1.10 fof(f8352,plain,(
% 0.29/1.10 select(queue_85,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8350,f367])).
% 0.29/1.10 fof(f8354,plain,(
% 0.29/1.10 select(queue_89,head)=index_84|seq=head),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2633,f8352])).
% 0.29/1.10 fof(f8356,plain,(
% 0.29/1.10 select(queue_89,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8354,f368])).
% 0.29/1.10 fof(f8358,plain,(
% 0.29/1.10 select(queue_91,head)=index_84|tail=head),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2665,f8356])).
% 0.29/1.10 fof(f8360,plain,(
% 0.29/1.10 select(queue_91,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8358,f367])).
% 0.29/1.10 fof(f8362,plain,(
% 0.29/1.10 select(queue_95,head)=index_84|seq=head),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2668,f8360])).
% 0.29/1.10 fof(f8364,plain,(
% 0.29/1.10 select(queue_95,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8362,f368])).
% 0.29/1.10 fof(f8366,plain,(
% 0.29/1.10 select(queue_97,head)=index_84|tail=head),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2670,f8364])).
% 0.29/1.10 fof(f8368,plain,(
% 0.29/1.10 select(queue_97,head)=index_84),
% 0.29/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8366,f367])).
% 0.29/1.10 fof(f8392,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_193,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1950,f8321])).
% 0.29/1.10 fof(f8396,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_193,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8392])).
% 0.29/1.10 fof(f8400,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_197,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1953,f8396])).
% 0.29/1.10 fof(f8404,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_197,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8400])).
% 0.29/1.10 fof(f8408,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_199,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1955,f8404])).
% 0.29/1.10 fof(f8412,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_199,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8408])).
% 0.29/1.10 fof(f8416,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_209,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f1995,f8412])).
% 0.29/1.10 fof(f8420,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_209,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8416])).
% 0.29/1.10 fof(f8434,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_211,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2032,f8420])).
% 0.29/1.10 fof(f8438,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_211,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8434])).
% 0.29/1.10 fof(f8442,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_215,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2035,f8438])).
% 0.29/1.10 fof(f8446,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_215,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8442])).
% 0.29/1.10 fof(f8450,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_217,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.10 inference(paramodulation,[status(thm)],[f2037,f8446])).
% 0.29/1.10 fof(f8454,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_217,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.10 inference(duplicate_literals_removal,[status(thm)],[f8450])).
% 0.29/1.10 fof(f8458,plain,(
% 0.29/1.10 ![X0]: (tail=X0|select(queue_221,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.11 inference(paramodulation,[status(thm)],[f2044,f8454])).
% 0.29/1.11 fof(f8462,plain,(
% 0.29/1.11 ![X0]: (tail=X0|select(queue_221,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.11 inference(duplicate_literals_removal,[status(thm)],[f8458])).
% 0.29/1.11 fof(f8466,plain,(
% 0.29/1.11 ![X0]: (tail=X0|select(queue_223,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.11 inference(paramodulation,[status(thm)],[f2072,f8462])).
% 0.29/1.11 fof(f8470,plain,(
% 0.29/1.11 ![X0]: (tail=X0|select(queue_223,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.11 inference(duplicate_literals_removal,[status(thm)],[f8466])).
% 0.29/1.11 fof(f8474,plain,(
% 0.29/1.11 ![X0]: (tail=X0|select(queue_227,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 0.29/1.11 inference(paramodulation,[status(thm)],[f2075,f8470])).
% 0.29/1.11 fof(f8478,plain,(
% 0.29/1.11 ![X0]: (tail=X0|select(queue_227,X0)=select(queue_97,X0)|seq=X0)),
% 0.29/1.11 inference(duplicate_literals_removal,[status(thm)],[f8474])).
% 0.29/1.11 fof(f8502,plain,(
% 0.29/1.11 ![X0]: (tail=X0|select(queue_229,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 0.29/1.11 inference(paramodulation,[status(thm)],[f2100,f8478])).
% 0.29/1.11 fof(f8506,plain,(
% 0.29/1.11 ![X0]: (tail=X0|select(queue_229,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8502])).
% 2.73/1.11 fof(f8510,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_233,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2106,f8506])).
% 2.73/1.11 fof(f8514,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_233,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8510])).
% 2.73/1.11 fof(f8518,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_235,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2132,f8514])).
% 2.73/1.11 fof(f8522,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_235,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8518])).
% 2.73/1.11 fof(f8526,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_239,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2141,f8522])).
% 2.73/1.11 fof(f8530,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_239,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8526])).
% 2.73/1.11 fof(f8534,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_241,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2143,f8530])).
% 2.73/1.11 fof(f8538,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_241,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8534])).
% 2.73/1.11 fof(f8542,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_245,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2185,f8538])).
% 2.73/1.11 fof(f8546,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_245,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8542])).
% 2.73/1.11 fof(f8560,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_247,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2187,f8546])).
% 2.73/1.11 fof(f8564,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_247,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8560])).
% 2.73/1.11 fof(f8568,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_251,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2202,f8564])).
% 2.73/1.11 fof(f8572,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_251,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8568])).
% 2.73/1.11 fof(f8576,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_253,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2226,f8572])).
% 2.73/1.11 fof(f8580,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_253,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8576])).
% 2.73/1.11 fof(f8584,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_257,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2229,f8580])).
% 2.73/1.11 fof(f8588,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_257,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8584])).
% 2.73/1.11 fof(f8592,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_259,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2267,f8588])).
% 2.73/1.11 fof(f8596,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_259,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8592])).
% 2.73/1.11 fof(f8600,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_263,X0)=select(queue_97,X0)|seq=X0|seq=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2270,f8596])).
% 2.73/1.11 fof(f8604,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_263,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8600])).
% 2.73/1.11 fof(f8628,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_265,X0)=select(queue_97,X0)|seq=X0|tail=X0)),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f2272,f8604])).
% 2.73/1.11 fof(f8632,plain,(
% 2.73/1.11 ![X0]: (tail=X0|select(queue_265,X0)=select(queue_97,X0)|seq=X0)),
% 2.73/1.11 inference(duplicate_literals_removal,[status(thm)],[f8628])).
% 2.73/1.11 fof(f8635,plain,(
% 2.73/1.11 tail=head|index_297=select(queue_97,head)|seq=head),
% 2.73/1.11 inference(paramodulation,[status(thm)],[f1329,f8632])).
% 2.73/1.11 fof(f8640,plain,(
% 2.73/1.11 tail=head|index_297=index_84|seq=head),
% 2.73/1.11 inference(forward_demodulation,[status(thm)],[f8368,f8635])).
% 2.73/1.11 fof(f8641,plain,(
% 2.73/1.11 index_297=index_84|seq=head),
% 2.73/1.11 inference(forward_subsumption_resolution,[status(thm)],[f8640,f367])).
% 2.73/1.11 fof(f8645,plain,(
% 2.73/1.11 elem_298=select(earray_296,index_84)),
% 2.73/1.11 inference(backward_demodulation,[status(thm)],[f8646,f474])).
% 2.73/1.11 fof(f8646,plain,(
% 2.73/1.11 index_297=index_84),
% 2.73/1.11 inference(forward_subsumption_resolution,[status(thm)],[f8641,f368])).
% 2.73/1.11 fof(f8647,plain,(
% 2.73/1.11 elem_298=elem_301),
% 2.73/1.11 inference(forward_demodulation,[status(thm)],[f5032,f8645])).
% 2.73/1.11 fof(f8648,plain,(
% 2.73/1.11 $false),
% 2.73/1.11 inference(forward_subsumption_resolution,[status(thm)],[f8647,f727])).
% 2.73/1.11 % SZS output end CNFRefutation for theBenchmark.p
% 2.40/1.13 % Elapsed time: 0.677418 seconds
% 2.40/1.13 % CPU time: 4.739340 seconds
% 2.40/1.13 % Total memory used: 157.833 MB
% 2.40/1.13 % Net memory used: 155.516 MB
%------------------------------------------------------------------------------