%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV571-1.043 : 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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:52:50 PM UTC 2026
% Result : Unsatisfiable 0.22s 1.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV571-1.043 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.47 % Computer : n002.cluster.edu
% 0.17/0.47 % Model : x86_64 x86_64
% 0.17/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.47 % Memory : 8046.5625MB
% 0.17/0.47 % OS : Linux 6.8.0-71-generic
% 0.17/0.47 % CPULimit : 300
% 0.17/0.47 % WCLimit : 300
% 0.17/0.47 % DateTime : Mon Sep 21 09:13:47 UTC 2026
% 0.17/0.47 % CPUTime :
% 0.17/0.50 % Drodi V4.1.1
% 0.22/1.14 % Refutation found
% 0.22/1.14 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.22/1.14 % SZS output start CNFRefutation for theBenchmark
% 0.22/1.14 fof(f1,axiom,(
% 0.22/1.14 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f2,axiom,(
% 0.22/1.14 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f3,axiom,(
% 0.22/1.14 head != tail ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f4,axiom,(
% 0.22/1.14 head != seq ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f5,axiom,(
% 0.22/1.14 tail != seq ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f6,axiom,(
% 0.22/1.14 (![X]: (p(s(X)) = X ))),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f7,axiom,(
% 0.22/1.14 (![X]: (s(p(X)) = X ))),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f10,axiom,(
% 0.22/1.14 (![X]: (s(s(s(X))) = X ))),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f59,hypothesis,(
% 0.22/1.14 earray_226 = store(earray_224,index_225,e42) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f71,hypothesis,(
% 0.22/1.14 earray_260 = select(q43,seq) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f98,hypothesis,(
% 0.22/1.14 elem_262 = select(earray_260,index_261) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f99,hypothesis,(
% 0.22/1.14 elem_265 = select(earray_260,index_264) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f100,hypothesis,(
% 0.22/1.14 index_0 = select(q,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f101,hypothesis,(
% 0.22/1.14 index_102 = s(index_99) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f102,hypothesis,(
% 0.22/1.14 index_105 = select(q24,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f103,hypothesis,(
% 0.22/1.14 index_108 = s(index_105) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f104,hypothesis,(
% 0.22/1.14 index_111 = select(q25,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f105,hypothesis,(
% 0.22/1.14 index_114 = s(index_111) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f106,hypothesis,(
% 0.22/1.14 index_117 = select(q26,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f107,hypothesis,(
% 0.22/1.14 index_12 = s(index_9) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f108,hypothesis,(
% 0.22/1.14 index_120 = s(index_117) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f109,hypothesis,(
% 0.22/1.14 index_123 = select(q27,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f110,hypothesis,(
% 0.22/1.14 index_126 = s(index_123) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f111,hypothesis,(
% 0.22/1.14 index_129 = select(q28,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f112,hypothesis,(
% 0.22/1.14 index_132 = s(index_129) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f113,hypothesis,(
% 0.22/1.14 index_135 = select(q2,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f114,hypothesis,(
% 0.22/1.14 index_138 = s(index_135) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f115,hypothesis,(
% 0.22/1.14 index_141 = select(q29,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f116,hypothesis,(
% 0.22/1.14 index_144 = s(index_141) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f117,hypothesis,(
% 0.22/1.14 index_147 = select(q30,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f118,hypothesis,(
% 0.22/1.14 index_15 = select(q10,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f119,hypothesis,(
% 0.22/1.14 index_150 = s(index_147) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f120,hypothesis,(
% 0.22/1.14 index_153 = select(q31,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f121,hypothesis,(
% 0.22/1.14 index_156 = s(index_153) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f122,hypothesis,(
% 0.22/1.14 index_159 = select(q32,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f123,hypothesis,(
% 0.22/1.14 index_162 = s(index_159) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f124,hypothesis,(
% 0.22/1.14 index_165 = select(q33,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f125,hypothesis,(
% 0.22/1.14 index_168 = s(index_165) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f126,hypothesis,(
% 0.22/1.14 index_171 = select(q34,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f127,hypothesis,(
% 0.22/1.14 index_174 = s(index_171) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f128,hypothesis,(
% 0.22/1.14 index_177 = select(q35,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f129,hypothesis,(
% 0.22/1.14 index_18 = s(index_15) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f130,hypothesis,(
% 0.22/1.14 index_180 = s(index_177) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f131,hypothesis,(
% 0.22/1.14 index_183 = select(q36,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f132,hypothesis,(
% 0.22/1.14 index_186 = s(index_183) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f133,hypothesis,(
% 0.22/1.14 index_189 = select(q37,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f134,hypothesis,(
% 0.22/1.14 index_192 = s(index_189) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f135,hypothesis,(
% 0.22/1.14 index_195 = select(q38,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f136,hypothesis,(
% 0.22/1.14 index_198 = s(index_195) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f137,hypothesis,(
% 0.22/1.14 index_201 = select(q3,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f138,hypothesis,(
% 0.22/1.14 index_204 = s(index_201) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f139,hypothesis,(
% 0.22/1.14 index_207 = select(q39,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f140,hypothesis,(
% 0.22/1.14 index_21 = select(q11,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f141,hypothesis,(
% 0.22/1.14 index_210 = s(index_207) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f142,hypothesis,(
% 0.22/1.14 index_213 = select(q40,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f143,hypothesis,(
% 0.22/1.14 index_216 = s(index_213) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f144,hypothesis,(
% 0.22/1.14 index_219 = select(q41,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f145,hypothesis,(
% 0.22/1.14 index_222 = s(index_219) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f146,hypothesis,(
% 0.22/1.14 index_225 = select(q42,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f147,hypothesis,(
% 0.22/1.14 index_228 = s(index_225) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f148,hypothesis,(
% 0.22/1.14 index_231 = select(q4,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f149,hypothesis,(
% 0.22/1.14 index_234 = s(index_231) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f150,hypothesis,(
% 0.22/1.14 index_237 = select(q5,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f151,hypothesis,(
% 0.22/1.14 index_24 = s(index_21) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f152,hypothesis,(
% 0.22/1.14 index_240 = s(index_237) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f153,hypothesis,(
% 0.22/1.14 index_243 = select(q6,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f154,hypothesis,(
% 0.22/1.14 index_246 = s(index_243) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f155,hypothesis,(
% 0.22/1.14 index_249 = select(q7,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f156,hypothesis,(
% 0.22/1.14 index_252 = s(index_249) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f157,hypothesis,(
% 0.22/1.14 index_255 = select(q8,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f158,hypothesis,(
% 0.22/1.14 index_258 = s(index_255) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f159,hypothesis,(
% 0.22/1.14 index_261 = select(q43,head) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f160,hypothesis,(
% 0.22/1.14 index_263 = select(q43,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f161,hypothesis,(
% 0.22/1.14 s(index_264) = index_263 ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f162,hypothesis,(
% 0.22/1.14 index_27 = select(q12,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f163,hypothesis,(
% 0.22/1.14 index_3 = select(q0,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f164,hypothesis,(
% 0.22/1.14 index_30 = s(index_27) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f165,hypothesis,(
% 0.22/1.14 index_33 = select(q13,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f166,hypothesis,(
% 0.22/1.14 index_36 = s(index_33) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f167,hypothesis,(
% 0.22/1.14 index_39 = select(q14,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f168,hypothesis,(
% 0.22/1.14 index_42 = s(index_39) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f169,hypothesis,(
% 0.22/1.14 index_45 = select(q15,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f170,hypothesis,(
% 0.22/1.14 index_48 = s(index_45) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f171,hypothesis,(
% 0.22/1.14 index_51 = select(q16,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f172,hypothesis,(
% 0.22/1.14 index_54 = s(index_51) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f173,hypothesis,(
% 0.22/1.14 index_57 = select(q17,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f174,hypothesis,(
% 0.22/1.14 index_6 = s(index_3) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f175,hypothesis,(
% 0.22/1.14 index_60 = s(index_57) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f176,hypothesis,(
% 0.22/1.14 index_63 = select(q18,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f177,hypothesis,(
% 0.22/1.14 index_66 = s(index_63) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f178,hypothesis,(
% 0.22/1.14 index_69 = select(q1,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f179,hypothesis,(
% 0.22/1.14 index_72 = s(index_69) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f180,hypothesis,(
% 0.22/1.14 index_75 = select(q19,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f181,hypothesis,(
% 0.22/1.14 index_78 = s(index_75) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f182,hypothesis,(
% 0.22/1.14 index_81 = select(q20,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f183,hypothesis,(
% 0.22/1.14 index_84 = s(index_81) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f184,hypothesis,(
% 0.22/1.14 index_87 = select(q21,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f185,hypothesis,(
% 0.22/1.14 index_9 = select(q9,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f186,hypothesis,(
% 0.22/1.14 index_90 = s(index_87) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f187,hypothesis,(
% 0.22/1.14 index_93 = select(q22,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f188,hypothesis,(
% 0.22/1.14 index_96 = s(index_93) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f189,hypothesis,(
% 0.22/1.14 index_99 = select(q23,tail) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f190,hypothesis,(
% 0.22/1.14 queue_1 = store(q,head,index_0) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f191,hypothesis,(
% 0.22/1.14 queue_101 = store(q23,seq,earray_100) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f192,hypothesis,(
% 0.22/1.14 queue_103 = store(queue_101,tail,index_102) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f193,hypothesis,(
% 0.22/1.14 queue_107 = store(q24,seq,earray_106) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f194,hypothesis,(
% 0.22/1.14 queue_109 = store(queue_107,tail,index_108) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f195,hypothesis,(
% 0.22/1.14 queue_11 = store(q9,seq,earray_10) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f196,hypothesis,(
% 0.22/1.14 queue_113 = store(q25,seq,earray_112) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f197,hypothesis,(
% 0.22/1.14 queue_115 = store(queue_113,tail,index_114) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f198,hypothesis,(
% 0.22/1.14 queue_119 = store(q26,seq,earray_118) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f199,hypothesis,(
% 0.22/1.14 queue_121 = store(queue_119,tail,index_120) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f200,hypothesis,(
% 0.22/1.14 queue_125 = store(q27,seq,earray_124) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f201,hypothesis,(
% 0.22/1.14 queue_127 = store(queue_125,tail,index_126) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f202,hypothesis,(
% 0.22/1.14 queue_13 = store(queue_11,tail,index_12) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f203,hypothesis,(
% 0.22/1.14 queue_131 = store(q28,seq,earray_130) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f204,hypothesis,(
% 0.22/1.14 queue_133 = store(queue_131,tail,index_132) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f205,hypothesis,(
% 0.22/1.14 queue_137 = store(q2,seq,earray_136) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f206,hypothesis,(
% 0.22/1.14 queue_139 = store(queue_137,tail,index_138) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f207,hypothesis,(
% 0.22/1.14 queue_143 = store(q29,seq,earray_142) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f208,hypothesis,(
% 0.22/1.14 queue_145 = store(queue_143,tail,index_144) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f209,hypothesis,(
% 0.22/1.14 queue_149 = store(q30,seq,earray_148) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f210,hypothesis,(
% 0.22/1.14 queue_151 = store(queue_149,tail,index_150) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f211,hypothesis,(
% 0.22/1.14 queue_155 = store(q31,seq,earray_154) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f212,hypothesis,(
% 0.22/1.14 queue_157 = store(queue_155,tail,index_156) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f213,hypothesis,(
% 0.22/1.14 queue_161 = store(q32,seq,earray_160) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f214,hypothesis,(
% 0.22/1.14 queue_163 = store(queue_161,tail,index_162) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f215,hypothesis,(
% 0.22/1.14 queue_167 = store(q33,seq,earray_166) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f216,hypothesis,(
% 0.22/1.14 queue_169 = store(queue_167,tail,index_168) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f217,hypothesis,(
% 0.22/1.14 queue_17 = store(q10,seq,earray_16) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f218,hypothesis,(
% 0.22/1.14 queue_173 = store(q34,seq,earray_172) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f219,hypothesis,(
% 0.22/1.14 queue_175 = store(queue_173,tail,index_174) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f220,hypothesis,(
% 0.22/1.14 queue_179 = store(q35,seq,earray_178) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f221,hypothesis,(
% 0.22/1.14 queue_181 = store(queue_179,tail,index_180) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f222,hypothesis,(
% 0.22/1.14 queue_185 = store(q36,seq,earray_184) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f223,hypothesis,(
% 0.22/1.14 queue_187 = store(queue_185,tail,index_186) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f224,hypothesis,(
% 0.22/1.14 queue_19 = store(queue_17,tail,index_18) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f225,hypothesis,(
% 0.22/1.14 queue_191 = store(q37,seq,earray_190) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f226,hypothesis,(
% 0.22/1.14 queue_193 = store(queue_191,tail,index_192) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f227,hypothesis,(
% 0.22/1.14 queue_197 = store(q38,seq,earray_196) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f228,hypothesis,(
% 0.22/1.14 queue_199 = store(queue_197,tail,index_198) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f229,hypothesis,(
% 0.22/1.14 queue_203 = store(q3,seq,earray_202) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f230,hypothesis,(
% 0.22/1.14 queue_205 = store(queue_203,tail,index_204) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f231,hypothesis,(
% 0.22/1.14 queue_209 = store(q39,seq,earray_208) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f232,hypothesis,(
% 0.22/1.14 queue_211 = store(queue_209,tail,index_210) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f233,hypothesis,(
% 0.22/1.14 queue_215 = store(q40,seq,earray_214) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f234,hypothesis,(
% 0.22/1.14 queue_217 = store(queue_215,tail,index_216) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f235,hypothesis,(
% 0.22/1.14 queue_221 = store(q41,seq,earray_220) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f236,hypothesis,(
% 0.22/1.14 queue_223 = store(queue_221,tail,index_222) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f237,hypothesis,(
% 0.22/1.14 queue_227 = store(q42,seq,earray_226) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f238,hypothesis,(
% 0.22/1.14 queue_229 = store(queue_227,tail,index_228) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f239,hypothesis,(
% 0.22/1.14 queue_23 = store(q11,seq,earray_22) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f240,hypothesis,(
% 0.22/1.14 queue_233 = store(q4,seq,earray_232) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f241,hypothesis,(
% 0.22/1.14 queue_235 = store(queue_233,tail,index_234) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f242,hypothesis,(
% 0.22/1.14 queue_239 = store(q5,seq,earray_238) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f243,hypothesis,(
% 0.22/1.14 queue_241 = store(queue_239,tail,index_240) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f244,hypothesis,(
% 0.22/1.14 queue_245 = store(q6,seq,earray_244) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f245,hypothesis,(
% 0.22/1.14 queue_247 = store(queue_245,tail,index_246) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f246,hypothesis,(
% 0.22/1.14 queue_25 = store(queue_23,tail,index_24) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f247,hypothesis,(
% 0.22/1.14 queue_251 = store(q7,seq,earray_250) ),
% 0.22/1.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.14 fof(f248,hypothesis,(
% 0.22/1.14 queue_253 = store(queue_251,tail,index_252) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f249,hypothesis,(
% 0.22/1.15 queue_257 = store(q8,seq,earray_256) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f250,hypothesis,(
% 0.22/1.15 queue_259 = store(queue_257,tail,index_258) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f251,hypothesis,(
% 0.22/1.15 queue_29 = store(q12,seq,earray_28) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f252,hypothesis,(
% 0.22/1.15 queue_31 = store(queue_29,tail,index_30) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f253,hypothesis,(
% 0.22/1.15 queue_35 = store(q13,seq,earray_34) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f254,hypothesis,(
% 0.22/1.15 queue_37 = store(queue_35,tail,index_36) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f255,hypothesis,(
% 0.22/1.15 queue_41 = store(q14,seq,earray_40) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f256,hypothesis,(
% 0.22/1.15 queue_43 = store(queue_41,tail,index_42) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f257,hypothesis,(
% 0.22/1.15 queue_47 = store(q15,seq,earray_46) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f258,hypothesis,(
% 0.22/1.15 queue_49 = store(queue_47,tail,index_48) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f259,hypothesis,(
% 0.22/1.15 queue_5 = store(q0,seq,earray_4) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f260,hypothesis,(
% 0.22/1.15 queue_53 = store(q16,seq,earray_52) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f261,hypothesis,(
% 0.22/1.15 queue_55 = store(queue_53,tail,index_54) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f262,hypothesis,(
% 0.22/1.15 queue_59 = store(q17,seq,earray_58) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f263,hypothesis,(
% 0.22/1.15 queue_61 = store(queue_59,tail,index_60) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f264,hypothesis,(
% 0.22/1.15 queue_65 = store(q18,seq,earray_64) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f265,hypothesis,(
% 0.22/1.15 queue_67 = store(queue_65,tail,index_66) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f266,hypothesis,(
% 0.22/1.15 queue_7 = store(queue_5,tail,index_6) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f267,hypothesis,(
% 0.22/1.15 queue_71 = store(q1,seq,earray_70) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f268,hypothesis,(
% 0.22/1.15 queue_73 = store(queue_71,tail,index_72) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f269,hypothesis,(
% 0.22/1.15 queue_77 = store(q19,seq,earray_76) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f270,hypothesis,(
% 0.22/1.15 queue_79 = store(queue_77,tail,index_78) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f271,hypothesis,(
% 0.22/1.15 queue_83 = store(q20,seq,earray_82) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f272,hypothesis,(
% 0.22/1.15 queue_85 = store(queue_83,tail,index_84) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f273,hypothesis,(
% 0.22/1.15 queue_89 = store(q21,seq,earray_88) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f274,hypothesis,(
% 0.22/1.15 queue_91 = store(queue_89,tail,index_90) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f275,hypothesis,(
% 0.22/1.15 queue_95 = store(q22,seq,earray_94) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f276,hypothesis,(
% 0.22/1.15 queue_97 = store(queue_95,tail,index_96) ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f277,hypothesis,(
% 0.22/1.15 q0 = queue_1 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f278,hypothesis,(
% 0.22/1.15 q1 = queue_7 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f279,hypothesis,(
% 0.22/1.15 q10 = queue_13 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f280,hypothesis,(
% 0.22/1.15 q11 = queue_19 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f281,hypothesis,(
% 0.22/1.15 q12 = queue_25 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f282,hypothesis,(
% 0.22/1.15 q13 = queue_31 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f283,hypothesis,(
% 0.22/1.15 q14 = queue_37 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f284,hypothesis,(
% 0.22/1.15 q15 = queue_43 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f285,hypothesis,(
% 0.22/1.15 q16 = queue_49 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f286,hypothesis,(
% 0.22/1.15 q17 = queue_55 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f287,hypothesis,(
% 0.22/1.15 q18 = queue_61 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f288,hypothesis,(
% 0.22/1.15 q19 = queue_67 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f289,hypothesis,(
% 0.22/1.15 q2 = queue_73 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f290,hypothesis,(
% 0.22/1.15 q20 = queue_79 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f291,hypothesis,(
% 0.22/1.15 q21 = queue_85 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f292,hypothesis,(
% 0.22/1.15 q22 = queue_91 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f293,hypothesis,(
% 0.22/1.15 q23 = queue_97 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f294,hypothesis,(
% 0.22/1.15 q24 = queue_103 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f295,hypothesis,(
% 0.22/1.15 q25 = queue_109 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f296,hypothesis,(
% 0.22/1.15 q26 = queue_115 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f297,hypothesis,(
% 0.22/1.15 q27 = queue_121 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f298,hypothesis,(
% 0.22/1.15 q28 = queue_127 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f299,hypothesis,(
% 0.22/1.15 q29 = queue_133 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f300,hypothesis,(
% 0.22/1.15 q3 = queue_139 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f301,hypothesis,(
% 0.22/1.15 q30 = queue_145 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f302,hypothesis,(
% 0.22/1.15 q31 = queue_151 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f303,hypothesis,(
% 0.22/1.15 q32 = queue_157 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f304,hypothesis,(
% 0.22/1.15 q33 = queue_163 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f305,hypothesis,(
% 0.22/1.15 q34 = queue_169 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f306,hypothesis,(
% 0.22/1.15 q35 = queue_175 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f307,hypothesis,(
% 0.22/1.15 q36 = queue_181 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f308,hypothesis,(
% 0.22/1.15 q37 = queue_187 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f309,hypothesis,(
% 0.22/1.15 q38 = queue_193 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f310,hypothesis,(
% 0.22/1.15 q39 = queue_199 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f311,hypothesis,(
% 0.22/1.15 q4 = queue_205 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f312,hypothesis,(
% 0.22/1.15 q40 = queue_211 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f313,hypothesis,(
% 0.22/1.15 q41 = queue_217 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f314,hypothesis,(
% 0.22/1.15 q42 = queue_223 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f315,hypothesis,(
% 0.22/1.15 q43 = queue_229 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f316,hypothesis,(
% 0.22/1.15 q5 = queue_235 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f317,hypothesis,(
% 0.22/1.15 q6 = queue_241 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f318,hypothesis,(
% 0.22/1.15 q7 = queue_247 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f319,hypothesis,(
% 0.22/1.15 q8 = queue_253 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f320,hypothesis,(
% 0.22/1.15 q9 = queue_259 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f321,negated_conjecture,(
% 0.22/1.15 elem_262 != elem_265 ),
% 0.22/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/1.15 fof(f322,plain,(
% 0.22/1.15 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f1])).
% 0.22/1.15 fof(f323,plain,(
% 0.22/1.15 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 0.22/1.15 inference(miniscoping,[status(thm)],[f2])).
% 0.22/1.15 fof(f324,plain,(
% 0.22/1.15 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f323])).
% 0.22/1.15 fof(f325,plain,(
% 0.22/1.15 ~head=tail),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f3])).
% 0.22/1.15 fof(f326,plain,(
% 0.22/1.15 ~head=seq),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f4])).
% 0.22/1.15 fof(f327,plain,(
% 0.22/1.15 ~tail=seq),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f5])).
% 0.22/1.15 fof(f328,plain,(
% 0.22/1.15 ![X0]: (p(s(X0))=X0)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f6])).
% 0.22/1.15 fof(f329,plain,(
% 0.22/1.15 ![X0]: (s(p(X0))=X0)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f7])).
% 0.22/1.15 fof(f332,plain,(
% 0.22/1.15 ![X0]: (s(s(s(X0)))=X0)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f10])).
% 0.22/1.15 fof(f381,plain,(
% 0.22/1.15 earray_226=store(earray_224,index_225,e42)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f59])).
% 0.22/1.15 fof(f393,plain,(
% 0.22/1.15 earray_260=select(q43,seq)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f71])).
% 0.22/1.15 fof(f420,plain,(
% 0.22/1.15 elem_262=select(earray_260,index_261)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f98])).
% 0.22/1.15 fof(f421,plain,(
% 0.22/1.15 elem_265=select(earray_260,index_264)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f99])).
% 0.22/1.15 fof(f422,plain,(
% 0.22/1.15 index_0=select(q,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f100])).
% 0.22/1.15 fof(f423,plain,(
% 0.22/1.15 index_102=s(index_99)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f101])).
% 0.22/1.15 fof(f424,plain,(
% 0.22/1.15 index_105=select(q24,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f102])).
% 0.22/1.15 fof(f425,plain,(
% 0.22/1.15 index_108=s(index_105)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f103])).
% 0.22/1.15 fof(f426,plain,(
% 0.22/1.15 index_111=select(q25,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f104])).
% 0.22/1.15 fof(f427,plain,(
% 0.22/1.15 index_114=s(index_111)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f105])).
% 0.22/1.15 fof(f428,plain,(
% 0.22/1.15 index_117=select(q26,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f106])).
% 0.22/1.15 fof(f429,plain,(
% 0.22/1.15 index_12=s(index_9)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f107])).
% 0.22/1.15 fof(f430,plain,(
% 0.22/1.15 index_120=s(index_117)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f108])).
% 0.22/1.15 fof(f431,plain,(
% 0.22/1.15 index_123=select(q27,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f109])).
% 0.22/1.15 fof(f432,plain,(
% 0.22/1.15 index_126=s(index_123)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f110])).
% 0.22/1.15 fof(f433,plain,(
% 0.22/1.15 index_129=select(q28,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f111])).
% 0.22/1.15 fof(f434,plain,(
% 0.22/1.15 index_132=s(index_129)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f112])).
% 0.22/1.15 fof(f435,plain,(
% 0.22/1.15 index_135=select(q2,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f113])).
% 0.22/1.15 fof(f436,plain,(
% 0.22/1.15 index_138=s(index_135)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f114])).
% 0.22/1.15 fof(f437,plain,(
% 0.22/1.15 index_141=select(q29,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f115])).
% 0.22/1.15 fof(f438,plain,(
% 0.22/1.15 index_144=s(index_141)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f116])).
% 0.22/1.15 fof(f439,plain,(
% 0.22/1.15 index_147=select(q30,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f117])).
% 0.22/1.15 fof(f440,plain,(
% 0.22/1.15 index_15=select(q10,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f118])).
% 0.22/1.15 fof(f441,plain,(
% 0.22/1.15 index_150=s(index_147)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f119])).
% 0.22/1.15 fof(f442,plain,(
% 0.22/1.15 index_153=select(q31,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f120])).
% 0.22/1.15 fof(f443,plain,(
% 0.22/1.15 index_156=s(index_153)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f121])).
% 0.22/1.15 fof(f444,plain,(
% 0.22/1.15 index_159=select(q32,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f122])).
% 0.22/1.15 fof(f445,plain,(
% 0.22/1.15 index_162=s(index_159)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f123])).
% 0.22/1.15 fof(f446,plain,(
% 0.22/1.15 index_165=select(q33,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f124])).
% 0.22/1.15 fof(f447,plain,(
% 0.22/1.15 index_168=s(index_165)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f125])).
% 0.22/1.15 fof(f448,plain,(
% 0.22/1.15 index_171=select(q34,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f126])).
% 0.22/1.15 fof(f449,plain,(
% 0.22/1.15 index_174=s(index_171)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f127])).
% 0.22/1.15 fof(f450,plain,(
% 0.22/1.15 index_177=select(q35,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f128])).
% 0.22/1.15 fof(f451,plain,(
% 0.22/1.15 index_18=s(index_15)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f129])).
% 0.22/1.15 fof(f452,plain,(
% 0.22/1.15 index_180=s(index_177)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f130])).
% 0.22/1.15 fof(f453,plain,(
% 0.22/1.15 index_183=select(q36,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f131])).
% 0.22/1.15 fof(f454,plain,(
% 0.22/1.15 index_186=s(index_183)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f132])).
% 0.22/1.15 fof(f455,plain,(
% 0.22/1.15 index_189=select(q37,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f133])).
% 0.22/1.15 fof(f456,plain,(
% 0.22/1.15 index_192=s(index_189)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f134])).
% 0.22/1.15 fof(f457,plain,(
% 0.22/1.15 index_195=select(q38,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f135])).
% 0.22/1.15 fof(f458,plain,(
% 0.22/1.15 index_198=s(index_195)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f136])).
% 0.22/1.15 fof(f459,plain,(
% 0.22/1.15 index_201=select(q3,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f137])).
% 0.22/1.15 fof(f460,plain,(
% 0.22/1.15 index_204=s(index_201)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f138])).
% 0.22/1.15 fof(f461,plain,(
% 0.22/1.15 index_207=select(q39,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f139])).
% 0.22/1.15 fof(f462,plain,(
% 0.22/1.15 index_21=select(q11,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f140])).
% 0.22/1.15 fof(f463,plain,(
% 0.22/1.15 index_210=s(index_207)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f141])).
% 0.22/1.15 fof(f464,plain,(
% 0.22/1.15 index_213=select(q40,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f142])).
% 0.22/1.15 fof(f465,plain,(
% 0.22/1.15 index_216=s(index_213)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f143])).
% 0.22/1.15 fof(f466,plain,(
% 0.22/1.15 index_219=select(q41,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f144])).
% 0.22/1.15 fof(f467,plain,(
% 0.22/1.15 index_222=s(index_219)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f145])).
% 0.22/1.15 fof(f468,plain,(
% 0.22/1.15 index_225=select(q42,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f146])).
% 0.22/1.15 fof(f469,plain,(
% 0.22/1.15 index_228=s(index_225)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f147])).
% 0.22/1.15 fof(f470,plain,(
% 0.22/1.15 index_231=select(q4,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f148])).
% 0.22/1.15 fof(f471,plain,(
% 0.22/1.15 index_234=s(index_231)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f149])).
% 0.22/1.15 fof(f472,plain,(
% 0.22/1.15 index_237=select(q5,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f150])).
% 0.22/1.15 fof(f473,plain,(
% 0.22/1.15 index_24=s(index_21)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f151])).
% 0.22/1.15 fof(f474,plain,(
% 0.22/1.15 index_240=s(index_237)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f152])).
% 0.22/1.15 fof(f475,plain,(
% 0.22/1.15 index_243=select(q6,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f153])).
% 0.22/1.15 fof(f476,plain,(
% 0.22/1.15 index_246=s(index_243)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f154])).
% 0.22/1.15 fof(f477,plain,(
% 0.22/1.15 index_249=select(q7,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f155])).
% 0.22/1.15 fof(f478,plain,(
% 0.22/1.15 index_252=s(index_249)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f156])).
% 0.22/1.15 fof(f479,plain,(
% 0.22/1.15 index_255=select(q8,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f157])).
% 0.22/1.15 fof(f480,plain,(
% 0.22/1.15 index_258=s(index_255)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f158])).
% 0.22/1.15 fof(f481,plain,(
% 0.22/1.15 index_261=select(q43,head)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f159])).
% 0.22/1.15 fof(f482,plain,(
% 0.22/1.15 index_263=select(q43,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f160])).
% 0.22/1.15 fof(f483,plain,(
% 0.22/1.15 s(index_264)=index_263),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f161])).
% 0.22/1.15 fof(f484,plain,(
% 0.22/1.15 index_27=select(q12,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f162])).
% 0.22/1.15 fof(f485,plain,(
% 0.22/1.15 index_3=select(q0,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f163])).
% 0.22/1.15 fof(f486,plain,(
% 0.22/1.15 index_30=s(index_27)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f164])).
% 0.22/1.15 fof(f487,plain,(
% 0.22/1.15 index_33=select(q13,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f165])).
% 0.22/1.15 fof(f488,plain,(
% 0.22/1.15 index_36=s(index_33)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f166])).
% 0.22/1.15 fof(f489,plain,(
% 0.22/1.15 index_39=select(q14,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f167])).
% 0.22/1.15 fof(f490,plain,(
% 0.22/1.15 index_42=s(index_39)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f168])).
% 0.22/1.15 fof(f491,plain,(
% 0.22/1.15 index_45=select(q15,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f169])).
% 0.22/1.15 fof(f492,plain,(
% 0.22/1.15 index_48=s(index_45)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f170])).
% 0.22/1.15 fof(f493,plain,(
% 0.22/1.15 index_51=select(q16,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f171])).
% 0.22/1.15 fof(f494,plain,(
% 0.22/1.15 index_54=s(index_51)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f172])).
% 0.22/1.15 fof(f495,plain,(
% 0.22/1.15 index_57=select(q17,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f173])).
% 0.22/1.15 fof(f496,plain,(
% 0.22/1.15 index_6=s(index_3)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f174])).
% 0.22/1.15 fof(f497,plain,(
% 0.22/1.15 index_60=s(index_57)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f175])).
% 0.22/1.15 fof(f498,plain,(
% 0.22/1.15 index_63=select(q18,tail)),
% 0.22/1.15 inference(cnf_transformation,[status(thm)],[f176])).
% 0.22/1.16 fof(f499,plain,(
% 0.22/1.16 index_66=s(index_63)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f177])).
% 0.22/1.16 fof(f500,plain,(
% 0.22/1.16 index_69=select(q1,tail)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f178])).
% 0.22/1.16 fof(f501,plain,(
% 0.22/1.16 index_72=s(index_69)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f179])).
% 0.22/1.16 fof(f502,plain,(
% 0.22/1.16 index_75=select(q19,tail)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f180])).
% 0.22/1.16 fof(f503,plain,(
% 0.22/1.16 index_78=s(index_75)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f181])).
% 0.22/1.16 fof(f504,plain,(
% 0.22/1.16 index_81=select(q20,tail)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f182])).
% 0.22/1.16 fof(f505,plain,(
% 0.22/1.16 index_84=s(index_81)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f183])).
% 0.22/1.16 fof(f506,plain,(
% 0.22/1.16 index_87=select(q21,tail)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f184])).
% 0.22/1.16 fof(f507,plain,(
% 0.22/1.16 index_9=select(q9,tail)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f185])).
% 0.22/1.16 fof(f508,plain,(
% 0.22/1.16 index_90=s(index_87)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f186])).
% 0.22/1.16 fof(f509,plain,(
% 0.22/1.16 index_93=select(q22,tail)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f187])).
% 0.22/1.16 fof(f510,plain,(
% 0.22/1.16 index_96=s(index_93)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f188])).
% 0.22/1.16 fof(f511,plain,(
% 0.22/1.16 index_99=select(q23,tail)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f189])).
% 0.22/1.16 fof(f512,plain,(
% 0.22/1.16 queue_1=store(q,head,index_0)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f190])).
% 0.22/1.16 fof(f513,plain,(
% 0.22/1.16 queue_101=store(q23,seq,earray_100)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f191])).
% 0.22/1.16 fof(f514,plain,(
% 0.22/1.16 queue_103=store(queue_101,tail,index_102)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f192])).
% 0.22/1.16 fof(f515,plain,(
% 0.22/1.16 queue_107=store(q24,seq,earray_106)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f193])).
% 0.22/1.16 fof(f516,plain,(
% 0.22/1.16 queue_109=store(queue_107,tail,index_108)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f194])).
% 0.22/1.16 fof(f517,plain,(
% 0.22/1.16 queue_11=store(q9,seq,earray_10)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f195])).
% 0.22/1.16 fof(f518,plain,(
% 0.22/1.16 queue_113=store(q25,seq,earray_112)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f196])).
% 0.22/1.16 fof(f519,plain,(
% 0.22/1.16 queue_115=store(queue_113,tail,index_114)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f197])).
% 0.22/1.16 fof(f520,plain,(
% 0.22/1.16 queue_119=store(q26,seq,earray_118)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f198])).
% 0.22/1.16 fof(f521,plain,(
% 0.22/1.16 queue_121=store(queue_119,tail,index_120)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f199])).
% 0.22/1.16 fof(f522,plain,(
% 0.22/1.16 queue_125=store(q27,seq,earray_124)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f200])).
% 0.22/1.16 fof(f523,plain,(
% 0.22/1.16 queue_127=store(queue_125,tail,index_126)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f201])).
% 0.22/1.16 fof(f524,plain,(
% 0.22/1.16 queue_13=store(queue_11,tail,index_12)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f202])).
% 0.22/1.16 fof(f525,plain,(
% 0.22/1.16 queue_131=store(q28,seq,earray_130)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f203])).
% 0.22/1.16 fof(f526,plain,(
% 0.22/1.16 queue_133=store(queue_131,tail,index_132)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f204])).
% 0.22/1.16 fof(f527,plain,(
% 0.22/1.16 queue_137=store(q2,seq,earray_136)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f205])).
% 0.22/1.16 fof(f528,plain,(
% 0.22/1.16 queue_139=store(queue_137,tail,index_138)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f206])).
% 0.22/1.16 fof(f529,plain,(
% 0.22/1.16 queue_143=store(q29,seq,earray_142)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f207])).
% 0.22/1.16 fof(f530,plain,(
% 0.22/1.16 queue_145=store(queue_143,tail,index_144)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f208])).
% 0.22/1.16 fof(f531,plain,(
% 0.22/1.16 queue_149=store(q30,seq,earray_148)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f209])).
% 0.22/1.16 fof(f532,plain,(
% 0.22/1.16 queue_151=store(queue_149,tail,index_150)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f210])).
% 0.22/1.16 fof(f533,plain,(
% 0.22/1.16 queue_155=store(q31,seq,earray_154)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f211])).
% 0.22/1.16 fof(f534,plain,(
% 0.22/1.16 queue_157=store(queue_155,tail,index_156)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f212])).
% 0.22/1.16 fof(f535,plain,(
% 0.22/1.16 queue_161=store(q32,seq,earray_160)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f213])).
% 0.22/1.16 fof(f536,plain,(
% 0.22/1.16 queue_163=store(queue_161,tail,index_162)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 0.22/1.16 fof(f537,plain,(
% 0.22/1.16 queue_167=store(q33,seq,earray_166)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f215])).
% 0.22/1.16 fof(f538,plain,(
% 0.22/1.16 queue_169=store(queue_167,tail,index_168)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f216])).
% 0.22/1.16 fof(f539,plain,(
% 0.22/1.16 queue_17=store(q10,seq,earray_16)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f217])).
% 0.22/1.16 fof(f540,plain,(
% 0.22/1.16 queue_173=store(q34,seq,earray_172)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f218])).
% 0.22/1.16 fof(f541,plain,(
% 0.22/1.16 queue_175=store(queue_173,tail,index_174)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f219])).
% 0.22/1.16 fof(f542,plain,(
% 0.22/1.16 queue_179=store(q35,seq,earray_178)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f220])).
% 0.22/1.16 fof(f543,plain,(
% 0.22/1.16 queue_181=store(queue_179,tail,index_180)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f221])).
% 0.22/1.16 fof(f544,plain,(
% 0.22/1.16 queue_185=store(q36,seq,earray_184)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f222])).
% 0.22/1.16 fof(f545,plain,(
% 0.22/1.16 queue_187=store(queue_185,tail,index_186)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f223])).
% 0.22/1.16 fof(f546,plain,(
% 0.22/1.16 queue_19=store(queue_17,tail,index_18)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f224])).
% 0.22/1.16 fof(f547,plain,(
% 0.22/1.16 queue_191=store(q37,seq,earray_190)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f225])).
% 0.22/1.16 fof(f548,plain,(
% 0.22/1.16 queue_193=store(queue_191,tail,index_192)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f226])).
% 0.22/1.16 fof(f549,plain,(
% 0.22/1.16 queue_197=store(q38,seq,earray_196)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f227])).
% 0.22/1.16 fof(f550,plain,(
% 0.22/1.16 queue_199=store(queue_197,tail,index_198)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f228])).
% 0.22/1.16 fof(f551,plain,(
% 0.22/1.16 queue_203=store(q3,seq,earray_202)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f229])).
% 0.22/1.16 fof(f552,plain,(
% 0.22/1.16 queue_205=store(queue_203,tail,index_204)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f230])).
% 0.22/1.16 fof(f553,plain,(
% 0.22/1.16 queue_209=store(q39,seq,earray_208)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f231])).
% 0.22/1.16 fof(f554,plain,(
% 0.22/1.16 queue_211=store(queue_209,tail,index_210)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f232])).
% 0.22/1.16 fof(f555,plain,(
% 0.22/1.16 queue_215=store(q40,seq,earray_214)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f233])).
% 0.22/1.16 fof(f556,plain,(
% 0.22/1.16 queue_217=store(queue_215,tail,index_216)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f234])).
% 0.22/1.16 fof(f557,plain,(
% 0.22/1.16 queue_221=store(q41,seq,earray_220)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f235])).
% 0.22/1.16 fof(f558,plain,(
% 0.22/1.16 queue_223=store(queue_221,tail,index_222)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f236])).
% 0.22/1.16 fof(f559,plain,(
% 0.22/1.16 queue_227=store(q42,seq,earray_226)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f237])).
% 0.22/1.16 fof(f560,plain,(
% 0.22/1.16 queue_229=store(queue_227,tail,index_228)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f238])).
% 0.22/1.16 fof(f561,plain,(
% 0.22/1.16 queue_23=store(q11,seq,earray_22)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f239])).
% 0.22/1.16 fof(f562,plain,(
% 0.22/1.16 queue_233=store(q4,seq,earray_232)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f240])).
% 0.22/1.16 fof(f563,plain,(
% 0.22/1.16 queue_235=store(queue_233,tail,index_234)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f241])).
% 0.22/1.16 fof(f564,plain,(
% 0.22/1.16 queue_239=store(q5,seq,earray_238)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f242])).
% 0.22/1.16 fof(f565,plain,(
% 0.22/1.16 queue_241=store(queue_239,tail,index_240)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f243])).
% 0.22/1.16 fof(f566,plain,(
% 0.22/1.16 queue_245=store(q6,seq,earray_244)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f244])).
% 0.22/1.16 fof(f567,plain,(
% 0.22/1.16 queue_247=store(queue_245,tail,index_246)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f245])).
% 0.22/1.16 fof(f568,plain,(
% 0.22/1.16 queue_25=store(queue_23,tail,index_24)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f246])).
% 0.22/1.16 fof(f569,plain,(
% 0.22/1.16 queue_251=store(q7,seq,earray_250)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f247])).
% 0.22/1.16 fof(f570,plain,(
% 0.22/1.16 queue_253=store(queue_251,tail,index_252)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f248])).
% 0.22/1.16 fof(f571,plain,(
% 0.22/1.16 queue_257=store(q8,seq,earray_256)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f249])).
% 0.22/1.16 fof(f572,plain,(
% 0.22/1.16 queue_259=store(queue_257,tail,index_258)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f250])).
% 0.22/1.16 fof(f573,plain,(
% 0.22/1.16 queue_29=store(q12,seq,earray_28)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f251])).
% 0.22/1.16 fof(f574,plain,(
% 0.22/1.16 queue_31=store(queue_29,tail,index_30)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f252])).
% 0.22/1.16 fof(f575,plain,(
% 0.22/1.16 queue_35=store(q13,seq,earray_34)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f253])).
% 0.22/1.16 fof(f576,plain,(
% 0.22/1.16 queue_37=store(queue_35,tail,index_36)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f254])).
% 0.22/1.16 fof(f577,plain,(
% 0.22/1.16 queue_41=store(q14,seq,earray_40)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f255])).
% 0.22/1.16 fof(f578,plain,(
% 0.22/1.16 queue_43=store(queue_41,tail,index_42)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f256])).
% 0.22/1.16 fof(f579,plain,(
% 0.22/1.16 queue_47=store(q15,seq,earray_46)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f257])).
% 0.22/1.16 fof(f580,plain,(
% 0.22/1.16 queue_49=store(queue_47,tail,index_48)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f258])).
% 0.22/1.16 fof(f581,plain,(
% 0.22/1.16 queue_5=store(q0,seq,earray_4)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f259])).
% 0.22/1.16 fof(f582,plain,(
% 0.22/1.16 queue_53=store(q16,seq,earray_52)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f260])).
% 0.22/1.16 fof(f583,plain,(
% 0.22/1.16 queue_55=store(queue_53,tail,index_54)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f261])).
% 0.22/1.16 fof(f584,plain,(
% 0.22/1.16 queue_59=store(q17,seq,earray_58)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f262])).
% 0.22/1.16 fof(f585,plain,(
% 0.22/1.16 queue_61=store(queue_59,tail,index_60)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f263])).
% 0.22/1.16 fof(f586,plain,(
% 0.22/1.16 queue_65=store(q18,seq,earray_64)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f264])).
% 0.22/1.16 fof(f587,plain,(
% 0.22/1.16 queue_67=store(queue_65,tail,index_66)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f265])).
% 0.22/1.16 fof(f588,plain,(
% 0.22/1.16 queue_7=store(queue_5,tail,index_6)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f266])).
% 0.22/1.16 fof(f589,plain,(
% 0.22/1.16 queue_71=store(q1,seq,earray_70)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f267])).
% 0.22/1.16 fof(f590,plain,(
% 0.22/1.16 queue_73=store(queue_71,tail,index_72)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f268])).
% 0.22/1.16 fof(f591,plain,(
% 0.22/1.16 queue_77=store(q19,seq,earray_76)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f269])).
% 0.22/1.16 fof(f592,plain,(
% 0.22/1.16 queue_79=store(queue_77,tail,index_78)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f270])).
% 0.22/1.16 fof(f593,plain,(
% 0.22/1.16 queue_83=store(q20,seq,earray_82)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f271])).
% 0.22/1.16 fof(f594,plain,(
% 0.22/1.16 queue_85=store(queue_83,tail,index_84)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f272])).
% 0.22/1.16 fof(f595,plain,(
% 0.22/1.16 queue_89=store(q21,seq,earray_88)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f273])).
% 0.22/1.16 fof(f596,plain,(
% 0.22/1.16 queue_91=store(queue_89,tail,index_90)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f274])).
% 0.22/1.16 fof(f597,plain,(
% 0.22/1.16 queue_95=store(q22,seq,earray_94)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f275])).
% 0.22/1.16 fof(f598,plain,(
% 0.22/1.16 queue_97=store(queue_95,tail,index_96)),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f276])).
% 0.22/1.16 fof(f599,plain,(
% 0.22/1.16 q0=queue_1),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f277])).
% 0.22/1.16 fof(f600,plain,(
% 0.22/1.16 q1=queue_7),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f278])).
% 0.22/1.16 fof(f601,plain,(
% 0.22/1.16 q10=queue_13),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f279])).
% 0.22/1.16 fof(f602,plain,(
% 0.22/1.16 q11=queue_19),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f280])).
% 0.22/1.16 fof(f603,plain,(
% 0.22/1.16 q12=queue_25),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f281])).
% 0.22/1.16 fof(f604,plain,(
% 0.22/1.16 q13=queue_31),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f282])).
% 0.22/1.16 fof(f605,plain,(
% 0.22/1.16 q14=queue_37),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f283])).
% 0.22/1.16 fof(f606,plain,(
% 0.22/1.16 q15=queue_43),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f284])).
% 0.22/1.16 fof(f607,plain,(
% 0.22/1.16 q16=queue_49),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f285])).
% 0.22/1.16 fof(f608,plain,(
% 0.22/1.16 q17=queue_55),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f286])).
% 0.22/1.16 fof(f609,plain,(
% 0.22/1.16 q18=queue_61),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f287])).
% 0.22/1.16 fof(f610,plain,(
% 0.22/1.16 q19=queue_67),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f288])).
% 0.22/1.16 fof(f611,plain,(
% 0.22/1.16 q2=queue_73),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f289])).
% 0.22/1.16 fof(f612,plain,(
% 0.22/1.16 q20=queue_79),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f290])).
% 0.22/1.16 fof(f613,plain,(
% 0.22/1.16 q21=queue_85),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f291])).
% 0.22/1.16 fof(f614,plain,(
% 0.22/1.16 q22=queue_91),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f292])).
% 0.22/1.16 fof(f615,plain,(
% 0.22/1.16 q23=queue_97),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f293])).
% 0.22/1.16 fof(f616,plain,(
% 0.22/1.16 q24=queue_103),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f294])).
% 0.22/1.16 fof(f617,plain,(
% 0.22/1.16 q25=queue_109),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f295])).
% 0.22/1.16 fof(f618,plain,(
% 0.22/1.16 q26=queue_115),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f296])).
% 0.22/1.16 fof(f619,plain,(
% 0.22/1.16 q27=queue_121),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f297])).
% 0.22/1.16 fof(f620,plain,(
% 0.22/1.16 q28=queue_127),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f298])).
% 0.22/1.16 fof(f621,plain,(
% 0.22/1.16 q29=queue_133),
% 0.22/1.16 inference(cnf_transformation,[status(thm)],[f299])).
% 0.22/1.16 fof(f622,plain,(
% 0.22/1.16 q3=queue_139),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f300])).
% 0.22/1.17 fof(f623,plain,(
% 0.22/1.17 q30=queue_145),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f301])).
% 0.22/1.17 fof(f624,plain,(
% 0.22/1.17 q31=queue_151),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f302])).
% 0.22/1.17 fof(f625,plain,(
% 0.22/1.17 q32=queue_157),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f303])).
% 0.22/1.17 fof(f626,plain,(
% 0.22/1.17 q33=queue_163),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f304])).
% 0.22/1.17 fof(f627,plain,(
% 0.22/1.17 q34=queue_169),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f305])).
% 0.22/1.17 fof(f628,plain,(
% 0.22/1.17 q35=queue_175),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f306])).
% 0.22/1.17 fof(f629,plain,(
% 0.22/1.17 q36=queue_181),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f307])).
% 0.22/1.17 fof(f630,plain,(
% 0.22/1.17 q37=queue_187),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f308])).
% 0.22/1.17 fof(f631,plain,(
% 0.22/1.17 q38=queue_193),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f309])).
% 0.22/1.17 fof(f632,plain,(
% 0.22/1.17 q39=queue_199),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f310])).
% 0.22/1.17 fof(f633,plain,(
% 0.22/1.17 q4=queue_205),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f311])).
% 0.22/1.17 fof(f634,plain,(
% 0.22/1.17 q40=queue_211),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f312])).
% 0.22/1.17 fof(f635,plain,(
% 0.22/1.17 q41=queue_217),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f313])).
% 0.22/1.17 fof(f636,plain,(
% 0.22/1.17 q42=queue_223),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f314])).
% 0.22/1.17 fof(f637,plain,(
% 0.22/1.17 q43=queue_229),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f315])).
% 0.22/1.17 fof(f638,plain,(
% 0.22/1.17 q5=queue_235),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f316])).
% 0.22/1.17 fof(f639,plain,(
% 0.22/1.17 q6=queue_241),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f317])).
% 0.22/1.17 fof(f640,plain,(
% 0.22/1.17 q7=queue_247),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f318])).
% 0.22/1.17 fof(f641,plain,(
% 0.22/1.17 q8=queue_253),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f319])).
% 0.22/1.17 fof(f642,plain,(
% 0.22/1.17 q9=queue_259),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f320])).
% 0.22/1.17 fof(f643,plain,(
% 0.22/1.17 ~elem_262=elem_265),
% 0.22/1.17 inference(cnf_transformation,[status(thm)],[f321])).
% 0.22/1.17 fof(f652,plain,(
% 0.22/1.17 ![X0]: (s(s(X0))=p(X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f329,f332])).
% 0.22/1.17 fof(f668,plain,(
% 0.22/1.17 p(index_108)=index_105),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f425,f328])).
% 0.22/1.17 fof(f676,plain,(
% 0.22/1.17 p(index_12)=index_9),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f429,f328])).
% 0.22/1.17 fof(f684,plain,(
% 0.22/1.17 p(index_126)=index_123),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f432,f328])).
% 0.22/1.17 fof(f720,plain,(
% 0.22/1.17 p(index_174)=index_171),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f449,f328])).
% 0.22/1.17 fof(f754,plain,(
% 0.22/1.17 p(index_216)=index_213),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f465,f328])).
% 0.22/1.17 fof(f774,plain,(
% 0.22/1.17 p(index_240)=index_237),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f474,f328])).
% 0.22/1.17 fof(f790,plain,(
% 0.22/1.17 p(index_258)=index_255),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f480,f328])).
% 0.22/1.17 fof(f794,plain,(
% 0.22/1.17 p(index_263)=index_264),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f483,f328])).
% 0.22/1.17 fof(f814,plain,(
% 0.22/1.17 p(index_54)=index_51),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f494,f328])).
% 0.22/1.17 fof(f836,plain,(
% 0.22/1.17 p(index_78)=index_75),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f503,f328])).
% 0.22/1.17 fof(f848,plain,(
% 0.22/1.17 p(index_96)=index_93),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f510,f328])).
% 0.22/1.17 fof(f1016,plain,(
% 0.22/1.17 select(earray_226,index_225)=e42),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f381,f322])).
% 0.22/1.17 fof(f1027,plain,(
% 0.22/1.17 s(index_84)=p(index_81)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f505,f652])).
% 0.22/1.17 fof(f1031,plain,(
% 0.22/1.17 s(index_60)=p(index_57)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f497,f652])).
% 0.22/1.17 fof(f1032,plain,(
% 0.22/1.17 s(index_6)=p(index_3)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f496,f652])).
% 0.22/1.17 fof(f1037,plain,(
% 0.22/1.17 s(index_30)=p(index_27)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f486,f652])).
% 0.22/1.17 fof(f1041,plain,(
% 0.22/1.17 s(index_246)=p(index_243)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f476,f652])).
% 0.22/1.17 fof(f1046,plain,(
% 0.22/1.17 s(index_222)=p(index_219)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f467,f652])).
% 0.22/1.17 fof(f1047,plain,(
% 0.22/1.17 s(index_216)=p(index_213)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f465,f652])).
% 0.22/1.17 fof(f1051,plain,(
% 0.22/1.17 s(index_192)=p(index_189)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f456,f652])).
% 0.22/1.17 fof(f1053,plain,(
% 0.22/1.17 s(index_180)=p(index_177)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f452,f652])).
% 0.22/1.17 fof(f1059,plain,(
% 0.22/1.17 s(index_150)=p(index_147)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f441,f652])).
% 0.22/1.17 fof(f1061,plain,(
% 0.22/1.17 s(index_138)=p(index_135)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f436,f652])).
% 0.22/1.17 fof(f1062,plain,(
% 0.22/1.17 s(index_132)=p(index_129)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f434,f652])).
% 0.22/1.17 fof(f1065,plain,(
% 0.22/1.17 s(index_12)=p(index_9)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f429,f652])).
% 0.22/1.17 fof(f1238,plain,(
% 0.22/1.17 q0=store(q,head,index_0)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f599,f512])).
% 0.22/1.17 fof(f1239,plain,(
% 0.22/1.17 ![X0]: (head=X0|select(q0,X0)=select(q,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1238,f324])).
% 0.22/1.17 fof(f1240,plain,(
% 0.22/1.17 select(q0,head)=index_0),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1238,f322])).
% 0.22/1.17 fof(f1241,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_101,X0)=select(q23,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f513,f324])).
% 0.22/1.17 fof(f1273,plain,(
% 0.22/1.17 q24=store(queue_101,tail,index_102)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f616,f514])).
% 0.22/1.17 fof(f1274,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q24,X0)=select(queue_101,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1273,f324])).
% 0.22/1.17 fof(f1275,plain,(
% 0.22/1.17 select(q24,tail)=index_102),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1273,f322])).
% 0.22/1.17 fof(f1276,plain,(
% 0.22/1.17 index_105=index_102),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f424,f1275])).
% 0.22/1.17 fof(f1281,plain,(
% 0.22/1.17 index_105=s(index_99)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1276,f423])).
% 0.22/1.17 fof(f1287,plain,(
% 0.22/1.17 s(index_105)=p(index_99)),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1281,f652])).
% 0.22/1.17 fof(f1290,plain,(
% 0.22/1.17 index_108=p(index_99)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f425,f1287])).
% 0.22/1.17 fof(f1293,plain,(
% 0.22/1.17 s(index_108)=index_99),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1290,f329])).
% 0.22/1.17 fof(f1320,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_107,X0)=select(q24,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f515,f324])).
% 0.22/1.17 fof(f1322,plain,(
% 0.22/1.17 q25=store(queue_107,tail,index_108)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f617,f516])).
% 0.22/1.17 fof(f1323,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q25,X0)=select(queue_107,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1322,f324])).
% 0.22/1.17 fof(f1324,plain,(
% 0.22/1.17 select(q25,tail)=index_108),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1322,f322])).
% 0.22/1.17 fof(f1325,plain,(
% 0.22/1.17 index_111=index_108),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f426,f1324])).
% 0.22/1.17 fof(f1327,plain,(
% 0.22/1.17 s(index_111)=index_99),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1325,f1293])).
% 0.22/1.17 fof(f1328,plain,(
% 0.22/1.17 index_111=p(index_99)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1325,f1290])).
% 0.22/1.17 fof(f1330,plain,(
% 0.22/1.17 p(index_111)=index_105),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1325,f668])).
% 0.22/1.17 fof(f1332,plain,(
% 0.22/1.17 index_111=s(index_105)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1325,f425])).
% 0.22/1.17 fof(f1333,plain,(
% 0.22/1.17 index_114=index_99),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1327,f427])).
% 0.22/1.17 fof(f1384,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_11,X0)=select(q9,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f517,f324])).
% 0.22/1.17 fof(f1386,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_113,X0)=select(q25,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f518,f324])).
% 0.22/1.17 fof(f1388,plain,(
% 0.22/1.17 q26=store(queue_113,tail,index_114)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f618,f519])).
% 0.22/1.17 fof(f1389,plain,(
% 0.22/1.17 q26=store(queue_113,tail,index_99)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f1333,f1388])).
% 0.22/1.17 fof(f1390,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q26,X0)=select(queue_113,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1389,f324])).
% 0.22/1.17 fof(f1391,plain,(
% 0.22/1.17 select(q26,tail)=index_99),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1389,f322])).
% 0.22/1.17 fof(f1422,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_119,X0)=select(q26,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f520,f324])).
% 0.22/1.17 fof(f1571,plain,(
% 0.22/1.17 q27=store(queue_119,tail,index_120)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f619,f521])).
% 0.22/1.17 fof(f1572,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q27,X0)=select(queue_119,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1571,f324])).
% 0.22/1.17 fof(f1573,plain,(
% 0.22/1.17 select(q27,tail)=index_120),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1571,f322])).
% 0.22/1.17 fof(f1574,plain,(
% 0.22/1.17 index_123=index_120),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f431,f1573])).
% 0.22/1.17 fof(f1575,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_125,X0)=select(q27,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f522,f324])).
% 0.22/1.17 fof(f1582,plain,(
% 0.22/1.17 index_123=s(index_117)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1574,f430])).
% 0.22/1.17 fof(f1607,plain,(
% 0.22/1.17 q28=store(queue_125,tail,index_126)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f620,f523])).
% 0.22/1.17 fof(f1608,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q28,X0)=select(queue_125,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1607,f324])).
% 0.22/1.17 fof(f1609,plain,(
% 0.22/1.17 select(q28,tail)=index_126),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1607,f322])).
% 0.22/1.17 fof(f1610,plain,(
% 0.22/1.17 index_129=index_126),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f433,f1609])).
% 0.22/1.17 fof(f1611,plain,(
% 0.22/1.17 q10=store(queue_11,tail,index_12)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f601,f524])).
% 0.22/1.17 fof(f1612,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q10,X0)=select(queue_11,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1611,f324])).
% 0.22/1.17 fof(f1613,plain,(
% 0.22/1.17 select(q10,tail)=index_12),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1611,f322])).
% 0.22/1.17 fof(f1614,plain,(
% 0.22/1.17 index_15=index_12),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f440,f1613])).
% 0.22/1.17 fof(f1615,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_131,X0)=select(q28,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f525,f324])).
% 0.22/1.17 fof(f1621,plain,(
% 0.22/1.17 p(index_129)=index_123),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1610,f684])).
% 0.22/1.17 fof(f1625,plain,(
% 0.22/1.17 s(index_15)=p(index_9)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1614,f1065])).
% 0.22/1.17 fof(f1626,plain,(
% 0.22/1.17 p(index_15)=index_9),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1614,f676])).
% 0.22/1.17 fof(f1629,plain,(
% 0.22/1.17 index_15=s(index_9)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1614,f429])).
% 0.22/1.17 fof(f1630,plain,(
% 0.22/1.17 index_18=p(index_9)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f451,f1625])).
% 0.22/1.17 fof(f1632,plain,(
% 0.22/1.17 q29=store(queue_131,tail,index_132)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f621,f526])).
% 0.22/1.17 fof(f1633,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q29,X0)=select(queue_131,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1632,f324])).
% 0.22/1.17 fof(f1634,plain,(
% 0.22/1.17 select(q29,tail)=index_132),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1632,f322])).
% 0.22/1.17 fof(f1635,plain,(
% 0.22/1.17 index_141=index_132),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f437,f1634])).
% 0.22/1.17 fof(f1637,plain,(
% 0.22/1.17 s(index_141)=p(index_129)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1635,f1062])).
% 0.22/1.17 fof(f1642,plain,(
% 0.22/1.17 index_144=p(index_129)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f438,f1637])).
% 0.22/1.17 fof(f1667,plain,(
% 0.22/1.17 s(index_18)=index_9),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1630,f329])).
% 0.22/1.17 fof(f1686,plain,(
% 0.22/1.17 index_144=index_123),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f1621,f1642])).
% 0.22/1.17 fof(f1695,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_137,X0)=select(q2,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f527,f324])).
% 0.22/1.17 fof(f1697,plain,(
% 0.22/1.17 q3=store(queue_137,tail,index_138)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f622,f528])).
% 0.22/1.17 fof(f1698,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q3,X0)=select(queue_137,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1697,f324])).
% 0.22/1.17 fof(f1699,plain,(
% 0.22/1.17 select(q3,tail)=index_138),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1697,f322])).
% 0.22/1.17 fof(f1700,plain,(
% 0.22/1.17 index_201=index_138),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f459,f1699])).
% 0.22/1.17 fof(f1703,plain,(
% 0.22/1.17 s(index_201)=p(index_135)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1700,f1061])).
% 0.22/1.17 fof(f1707,plain,(
% 0.22/1.17 index_201=s(index_135)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1700,f436])).
% 0.22/1.17 fof(f1708,plain,(
% 0.22/1.17 index_204=p(index_135)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f460,f1703])).
% 0.22/1.17 fof(f1720,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_143,X0)=select(q29,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f529,f324])).
% 0.22/1.17 fof(f1722,plain,(
% 0.22/1.17 q30=store(queue_143,tail,index_144)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f623,f530])).
% 0.22/1.17 fof(f1723,plain,(
% 0.22/1.17 q30=store(queue_143,tail,index_123)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f1686,f1722])).
% 0.22/1.17 fof(f1724,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q30,X0)=select(queue_143,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1723,f324])).
% 0.22/1.17 fof(f1725,plain,(
% 0.22/1.17 select(q30,tail)=index_123),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1723,f322])).
% 0.22/1.17 fof(f1726,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_149,X0)=select(q30,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f531,f324])).
% 0.22/1.17 fof(f1731,plain,(
% 0.22/1.17 s(index_204)=index_135),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1708,f329])).
% 0.22/1.17 fof(f1750,plain,(
% 0.22/1.17 q31=store(queue_149,tail,index_150)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f624,f532])).
% 0.22/1.17 fof(f1751,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q31,X0)=select(queue_149,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1750,f324])).
% 0.22/1.17 fof(f1752,plain,(
% 0.22/1.17 select(q31,tail)=index_150),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1750,f322])).
% 0.22/1.17 fof(f1753,plain,(
% 0.22/1.17 index_153=index_150),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f442,f1752])).
% 0.22/1.17 fof(f1755,plain,(
% 0.22/1.17 s(index_153)=p(index_147)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1753,f1059])).
% 0.22/1.17 fof(f1760,plain,(
% 0.22/1.17 index_156=p(index_147)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f443,f1755])).
% 0.22/1.17 fof(f1765,plain,(
% 0.22/1.17 s(index_156)=index_147),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1760,f329])).
% 0.22/1.17 fof(f1784,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_155,X0)=select(q31,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f533,f324])).
% 0.22/1.17 fof(f1786,plain,(
% 0.22/1.17 q32=store(queue_155,tail,index_156)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f625,f534])).
% 0.22/1.17 fof(f1787,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q32,X0)=select(queue_155,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1786,f324])).
% 0.22/1.17 fof(f1788,plain,(
% 0.22/1.17 select(q32,tail)=index_156),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1786,f322])).
% 0.22/1.17 fof(f1789,plain,(
% 0.22/1.17 index_159=index_156),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f444,f1788])).
% 0.22/1.17 fof(f1791,plain,(
% 0.22/1.17 s(index_159)=index_147),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1789,f1765])).
% 0.22/1.17 fof(f1797,plain,(
% 0.22/1.17 index_162=index_147),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1791,f445])).
% 0.22/1.17 fof(f1824,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_161,X0)=select(q32,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f535,f324])).
% 0.22/1.17 fof(f1826,plain,(
% 0.22/1.17 q33=store(queue_161,tail,index_162)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f626,f536])).
% 0.22/1.17 fof(f1827,plain,(
% 0.22/1.17 q33=store(queue_161,tail,index_147)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f1797,f1826])).
% 0.22/1.17 fof(f1828,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q33,X0)=select(queue_161,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1827,f324])).
% 0.22/1.17 fof(f1829,plain,(
% 0.22/1.17 select(q33,tail)=index_147),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1827,f322])).
% 0.22/1.17 fof(f1830,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_167,X0)=select(q33,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f537,f324])).
% 0.22/1.17 fof(f1832,plain,(
% 0.22/1.17 index_117=index_99),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1391,f428])).
% 0.22/1.17 fof(f1838,plain,(
% 0.22/1.17 index_123=s(index_99)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1832,f1582])).
% 0.22/1.17 fof(f1844,plain,(
% 0.22/1.17 index_123=index_105),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f1281,f1838])).
% 0.22/1.17 fof(f1845,plain,(
% 0.22/1.17 q34=store(queue_167,tail,index_168)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f627,f538])).
% 0.22/1.17 fof(f1846,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q34,X0)=select(queue_167,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1845,f324])).
% 0.22/1.17 fof(f1847,plain,(
% 0.22/1.17 select(q34,tail)=index_168),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1845,f322])).
% 0.22/1.17 fof(f1848,plain,(
% 0.22/1.17 index_171=index_168),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f448,f1847])).
% 0.22/1.17 fof(f1870,plain,(
% 0.22/1.17 index_171=s(index_165)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1848,f447])).
% 0.22/1.17 fof(f1874,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_17,X0)=select(q10,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f539,f324])).
% 0.22/1.17 fof(f1876,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_173,X0)=select(q34,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f540,f324])).
% 0.22/1.17 fof(f1905,plain,(
% 0.22/1.17 q35=store(queue_173,tail,index_174)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f628,f541])).
% 0.22/1.17 fof(f1906,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q35,X0)=select(queue_173,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1905,f324])).
% 0.22/1.17 fof(f1907,plain,(
% 0.22/1.17 select(q35,tail)=index_174),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1905,f322])).
% 0.22/1.17 fof(f1908,plain,(
% 0.22/1.17 index_177=index_174),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f450,f1907])).
% 0.22/1.17 fof(f1909,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_179,X0)=select(q35,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f542,f324])).
% 0.22/1.17 fof(f1911,plain,(
% 0.22/1.17 q36=store(queue_179,tail,index_180)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f629,f543])).
% 0.22/1.17 fof(f1912,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q36,X0)=select(queue_179,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1911,f324])).
% 0.22/1.17 fof(f1913,plain,(
% 0.22/1.17 select(q36,tail)=index_180),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1911,f322])).
% 0.22/1.17 fof(f1914,plain,(
% 0.22/1.17 index_183=index_180),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f453,f1913])).
% 0.22/1.17 fof(f1919,plain,(
% 0.22/1.17 p(index_177)=index_171),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1908,f720])).
% 0.22/1.17 fof(f1923,plain,(
% 0.22/1.17 s(index_183)=p(index_177)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1914,f1053])).
% 0.22/1.17 fof(f1928,plain,(
% 0.22/1.17 index_186=p(index_177)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f454,f1923])).
% 0.22/1.17 fof(f1930,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_185,X0)=select(q36,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f544,f324])).
% 0.22/1.17 fof(f1958,plain,(
% 0.22/1.17 index_186=index_171),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f1919,f1928])).
% 0.22/1.17 fof(f1970,plain,(
% 0.22/1.17 q37=store(queue_185,tail,index_186)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f630,f545])).
% 0.22/1.17 fof(f1971,plain,(
% 0.22/1.17 q37=store(queue_185,tail,index_171)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f1958,f1970])).
% 0.22/1.17 fof(f1972,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q37,X0)=select(queue_185,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1971,f324])).
% 0.22/1.17 fof(f1973,plain,(
% 0.22/1.17 select(q37,tail)=index_171),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1971,f322])).
% 0.22/1.17 fof(f1974,plain,(
% 0.22/1.17 q11=store(queue_17,tail,index_18)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f602,f546])).
% 0.22/1.17 fof(f1975,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q11,X0)=select(queue_17,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1974,f324])).
% 0.22/1.17 fof(f1976,plain,(
% 0.22/1.17 select(q11,tail)=index_18),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f1974,f322])).
% 0.22/1.17 fof(f1977,plain,(
% 0.22/1.17 index_21=index_18),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f462,f1976])).
% 0.22/1.17 fof(f1979,plain,(
% 0.22/1.17 s(index_21)=index_9),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1977,f1667])).
% 0.22/1.17 fof(f1980,plain,(
% 0.22/1.17 index_21=p(index_9)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1977,f1630])).
% 0.22/1.17 fof(f1984,plain,(
% 0.22/1.17 index_21=s(index_15)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1977,f451])).
% 0.22/1.17 fof(f1987,plain,(
% 0.22/1.17 index_24=index_9),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f1979,f473])).
% 0.22/1.17 fof(f2014,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_191,X0)=select(q37,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f547,f324])).
% 0.22/1.17 fof(f2016,plain,(
% 0.22/1.17 q38=store(queue_191,tail,index_192)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f631,f548])).
% 0.22/1.17 fof(f2017,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q38,X0)=select(queue_191,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f2016,f324])).
% 0.22/1.17 fof(f2018,plain,(
% 0.22/1.17 select(q38,tail)=index_192),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f2016,f322])).
% 0.22/1.17 fof(f2019,plain,(
% 0.22/1.17 index_195=index_192),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f457,f2018])).
% 0.22/1.17 fof(f2020,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_197,X0)=select(q38,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f549,f324])).
% 0.22/1.17 fof(f2023,plain,(
% 0.22/1.17 s(index_195)=p(index_189)),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f2019,f1051])).
% 0.22/1.17 fof(f2028,plain,(
% 0.22/1.17 index_198=p(index_189)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f458,f2023])).
% 0.22/1.17 fof(f2033,plain,(
% 0.22/1.17 s(index_198)=index_189),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f2028,f329])).
% 0.22/1.17 fof(f2046,plain,(
% 0.22/1.17 q39=store(queue_197,tail,index_198)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f632,f550])).
% 0.22/1.17 fof(f2047,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q39,X0)=select(queue_197,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f2046,f324])).
% 0.22/1.17 fof(f2048,plain,(
% 0.22/1.17 select(q39,tail)=index_198),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f2046,f322])).
% 0.22/1.17 fof(f2049,plain,(
% 0.22/1.17 index_207=index_198),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f461,f2048])).
% 0.22/1.17 fof(f2060,plain,(
% 0.22/1.17 index_210=index_189),
% 0.22/1.17 inference(backward_demodulation,[status(thm)],[f2061,f463])).
% 0.22/1.17 fof(f2061,plain,(
% 0.22/1.17 s(index_207)=index_189),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f2049,f2033])).
% 0.22/1.17 fof(f2086,plain,(
% 0.22/1.17 ![X0]: (seq=X0|select(queue_203,X0)=select(q3,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f551,f324])).
% 0.22/1.17 fof(f2088,plain,(
% 0.22/1.17 q4=store(queue_203,tail,index_204)),
% 0.22/1.17 inference(forward_demodulation,[status(thm)],[f633,f552])).
% 0.22/1.17 fof(f2089,plain,(
% 0.22/1.17 ![X0]: (tail=X0|select(q4,X0)=select(queue_203,X0))),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f2088,f324])).
% 0.22/1.17 fof(f2090,plain,(
% 0.22/1.17 select(q4,tail)=index_204),
% 0.22/1.17 inference(paramodulation,[status(thm)],[f2088,f322])).
% 4.26/1.17 fof(f2091,plain,(
% 4.26/1.17 index_231=index_204),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f470,f2090])).
% 4.26/1.17 fof(f2093,plain,(
% 4.26/1.17 s(index_231)=index_135),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2091,f1731])).
% 4.26/1.17 fof(f2103,plain,(
% 4.26/1.17 index_234=index_135),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2093,f471])).
% 4.26/1.17 fof(f2130,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_209,X0)=select(q39,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f553,f324])).
% 4.26/1.17 fof(f2132,plain,(
% 4.26/1.17 q40=store(queue_209,tail,index_210)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f634,f554])).
% 4.26/1.17 fof(f2133,plain,(
% 4.26/1.17 q40=store(queue_209,tail,index_189)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2060,f2132])).
% 4.26/1.17 fof(f2134,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q40,X0)=select(queue_209,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2133,f324])).
% 4.26/1.17 fof(f2135,plain,(
% 4.26/1.17 select(q40,tail)=index_189),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2133,f322])).
% 4.26/1.17 fof(f2136,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_215,X0)=select(q40,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f555,f324])).
% 4.26/1.17 fof(f2138,plain,(
% 4.26/1.17 index_147=index_105),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2139,f439])).
% 4.26/1.17 fof(f2139,plain,(
% 4.26/1.17 select(q30,tail)=index_105),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f1844,f1725])).
% 4.26/1.17 fof(f2140,plain,(
% 4.26/1.17 q41=store(queue_215,tail,index_216)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f635,f556])).
% 4.26/1.17 fof(f2141,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q41,X0)=select(queue_215,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2140,f324])).
% 4.26/1.17 fof(f2142,plain,(
% 4.26/1.17 select(q41,tail)=index_216),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2140,f322])).
% 4.26/1.17 fof(f2143,plain,(
% 4.26/1.17 index_219=index_216),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f466,f2142])).
% 4.26/1.17 fof(f2157,plain,(
% 4.26/1.17 s(index_219)=p(index_213)),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2143,f1047])).
% 4.26/1.17 fof(f2158,plain,(
% 4.26/1.17 p(index_219)=index_213),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2143,f754])).
% 4.26/1.17 fof(f2162,plain,(
% 4.26/1.17 index_222=p(index_213)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f467,f2157])).
% 4.26/1.17 fof(f2179,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_221,X0)=select(q41,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f557,f324])).
% 4.26/1.17 fof(f2181,plain,(
% 4.26/1.17 q42=store(queue_221,tail,index_222)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f636,f558])).
% 4.26/1.17 fof(f2182,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q42,X0)=select(queue_221,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2181,f324])).
% 4.26/1.17 fof(f2183,plain,(
% 4.26/1.17 select(q42,tail)=index_222),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2181,f322])).
% 4.26/1.17 fof(f2184,plain,(
% 4.26/1.17 index_225=index_222),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f468,f2183])).
% 4.26/1.17 fof(f2187,plain,(
% 4.26/1.17 s(index_225)=p(index_219)),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2184,f1046])).
% 4.26/1.17 fof(f2192,plain,(
% 4.26/1.17 index_228=p(index_219)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f469,f2187])).
% 4.26/1.17 fof(f2196,plain,(
% 4.26/1.17 index_225=p(index_213)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2184,f2162])).
% 4.26/1.17 fof(f2217,plain,(
% 4.26/1.17 index_228=index_213),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2158,f2192])).
% 4.26/1.17 fof(f2235,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_227,X0)=select(q42,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f559,f324])).
% 4.26/1.17 fof(f2236,plain,(
% 4.26/1.17 select(queue_227,seq)=earray_226),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f559,f322])).
% 4.26/1.17 fof(f2237,plain,(
% 4.26/1.17 q43=store(queue_227,tail,index_228)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f637,f560])).
% 4.26/1.17 fof(f2238,plain,(
% 4.26/1.17 q43=store(queue_227,tail,index_213)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2217,f2237])).
% 4.26/1.17 fof(f2239,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q43,X0)=select(queue_227,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2238,f324])).
% 4.26/1.17 fof(f2240,plain,(
% 4.26/1.17 select(q43,tail)=index_213),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2238,f322])).
% 4.26/1.17 fof(f2241,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_23,X0)=select(q11,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f561,f324])).
% 4.26/1.17 fof(f2244,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_233,X0)=select(q4,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f562,f324])).
% 4.26/1.17 fof(f2246,plain,(
% 4.26/1.17 index_165=index_105),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2247,f446])).
% 4.26/1.17 fof(f2247,plain,(
% 4.26/1.17 select(q33,tail)=index_105),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2138,f1829])).
% 4.26/1.17 fof(f2253,plain,(
% 4.26/1.17 index_171=s(index_105)),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2246,f1870])).
% 4.26/1.17 fof(f2259,plain,(
% 4.26/1.17 index_171=index_111),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f1332,f2253])).
% 4.26/1.17 fof(f2275,plain,(
% 4.26/1.17 q5=store(queue_233,tail,index_234)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f638,f563])).
% 4.26/1.17 fof(f2276,plain,(
% 4.26/1.17 q5=store(queue_233,tail,index_135)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2103,f2275])).
% 4.26/1.17 fof(f2277,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q5,X0)=select(queue_233,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2276,f324])).
% 4.26/1.17 fof(f2278,plain,(
% 4.26/1.17 select(q5,tail)=index_135),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2276,f322])).
% 4.26/1.17 fof(f2279,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_239,X0)=select(q5,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f564,f324])).
% 4.26/1.17 fof(f2286,plain,(
% 4.26/1.17 q6=store(queue_239,tail,index_240)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f639,f565])).
% 4.26/1.17 fof(f2287,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q6,X0)=select(queue_239,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2286,f324])).
% 4.26/1.17 fof(f2288,plain,(
% 4.26/1.17 select(q6,tail)=index_240),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2286,f322])).
% 4.26/1.17 fof(f2289,plain,(
% 4.26/1.17 index_243=index_240),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f475,f2288])).
% 4.26/1.17 fof(f2290,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_245,X0)=select(q6,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f566,f324])).
% 4.26/1.17 fof(f2292,plain,(
% 4.26/1.17 q7=store(queue_245,tail,index_246)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f640,f567])).
% 4.26/1.17 fof(f2293,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q7,X0)=select(queue_245,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2292,f324])).
% 4.26/1.17 fof(f2294,plain,(
% 4.26/1.17 select(q7,tail)=index_246),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2292,f322])).
% 4.26/1.17 fof(f2295,plain,(
% 4.26/1.17 index_249=index_246),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f477,f2294])).
% 4.26/1.17 fof(f2298,plain,(
% 4.26/1.17 p(index_243)=index_237),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2289,f774])).
% 4.26/1.17 fof(f2305,plain,(
% 4.26/1.17 s(index_249)=p(index_243)),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2295,f1041])).
% 4.26/1.17 fof(f2310,plain,(
% 4.26/1.17 index_252=p(index_243)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f478,f2305])).
% 4.26/1.17 fof(f2313,plain,(
% 4.26/1.17 q12=store(queue_23,tail,index_24)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f603,f568])).
% 4.26/1.17 fof(f2314,plain,(
% 4.26/1.17 q12=store(queue_23,tail,index_9)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f1987,f2313])).
% 4.26/1.17 fof(f2315,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q12,X0)=select(queue_23,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2314,f324])).
% 4.26/1.17 fof(f2316,plain,(
% 4.26/1.17 select(q12,tail)=index_9),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2314,f322])).
% 4.26/1.17 fof(f2337,plain,(
% 4.26/1.17 index_252=index_237),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2298,f2310])).
% 4.26/1.17 fof(f2355,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_251,X0)=select(q7,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f569,f324])).
% 4.26/1.17 fof(f2357,plain,(
% 4.26/1.17 q8=store(queue_251,tail,index_252)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f641,f570])).
% 4.26/1.17 fof(f2358,plain,(
% 4.26/1.17 q8=store(queue_251,tail,index_237)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2337,f2357])).
% 4.26/1.17 fof(f2359,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q8,X0)=select(queue_251,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2358,f324])).
% 4.26/1.17 fof(f2360,plain,(
% 4.26/1.17 select(q8,tail)=index_237),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2358,f322])).
% 4.26/1.17 fof(f2364,plain,(
% 4.26/1.17 index_189=index_111),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2365,f455])).
% 4.26/1.17 fof(f2365,plain,(
% 4.26/1.17 select(q37,tail)=index_111),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f2259,f1973])).
% 4.26/1.17 fof(f2393,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_257,X0)=select(q8,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f571,f324])).
% 4.26/1.17 fof(f2395,plain,(
% 4.26/1.17 q9=store(queue_257,tail,index_258)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f642,f572])).
% 4.26/1.17 fof(f2396,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q9,X0)=select(queue_257,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2395,f324])).
% 4.26/1.17 fof(f2397,plain,(
% 4.26/1.17 select(q9,tail)=index_258),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2395,f322])).
% 4.26/1.17 fof(f2398,plain,(
% 4.26/1.17 index_9=index_258),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f507,f2397])).
% 4.26/1.17 fof(f2399,plain,(
% 4.26/1.17 ![X0]: (seq=X0|select(queue_29,X0)=select(q12,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f573,f324])).
% 4.26/1.17 fof(f2403,plain,(
% 4.26/1.17 p(index_9)=index_255),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2398,f790])).
% 4.26/1.17 fof(f2408,plain,(
% 4.26/1.17 index_21=index_255),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f1980,f2403])).
% 4.26/1.17 fof(f2412,plain,(
% 4.26/1.17 index_21=select(q8,tail)),
% 4.26/1.17 inference(backward_demodulation,[status(thm)],[f2408,f479])).
% 4.26/1.17 fof(f2415,plain,(
% 4.26/1.17 q13=store(queue_29,tail,index_30)),
% 4.26/1.17 inference(forward_demodulation,[status(thm)],[f604,f574])).
% 4.26/1.17 fof(f2416,plain,(
% 4.26/1.17 ![X0]: (tail=X0|select(q13,X0)=select(queue_29,X0))),
% 4.26/1.17 inference(paramodulation,[status(thm)],[f2415,f324])).
% 4.26/1.18 fof(f2417,plain,(
% 4.26/1.18 select(q13,tail)=index_30),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2415,f322])).
% 4.26/1.18 fof(f2418,plain,(
% 4.26/1.18 index_33=index_30),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f487,f2417])).
% 4.26/1.18 fof(f2420,plain,(
% 4.26/1.18 s(index_33)=p(index_27)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2418,f1037])).
% 4.26/1.18 fof(f2425,plain,(
% 4.26/1.18 index_36=p(index_27)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f488,f2420])).
% 4.26/1.18 fof(f2435,plain,(
% 4.26/1.18 s(index_36)=index_27),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2425,f329])).
% 4.26/1.18 fof(f2448,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_35,X0)=select(q13,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f575,f324])).
% 4.26/1.18 fof(f2450,plain,(
% 4.26/1.18 q14=store(queue_35,tail,index_36)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f605,f576])).
% 4.26/1.18 fof(f2451,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q14,X0)=select(queue_35,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2450,f324])).
% 4.26/1.18 fof(f2452,plain,(
% 4.26/1.18 select(q14,tail)=index_36),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2450,f322])).
% 4.26/1.18 fof(f2453,plain,(
% 4.26/1.18 index_39=index_36),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f489,f2452])).
% 4.26/1.18 fof(f2464,plain,(
% 4.26/1.18 index_42=index_27),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2465,f490])).
% 4.26/1.18 fof(f2465,plain,(
% 4.26/1.18 s(index_39)=index_27),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2453,f2435])).
% 4.26/1.18 fof(f2494,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_41,X0)=select(q14,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f577,f324])).
% 4.26/1.18 fof(f2496,plain,(
% 4.26/1.18 q15=store(queue_41,tail,index_42)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f606,f578])).
% 4.26/1.18 fof(f2497,plain,(
% 4.26/1.18 q15=store(queue_41,tail,index_27)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2464,f2496])).
% 4.26/1.18 fof(f2498,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q15,X0)=select(queue_41,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2497,f324])).
% 4.26/1.18 fof(f2499,plain,(
% 4.26/1.18 select(q15,tail)=index_27),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2497,f322])).
% 4.26/1.18 fof(f2500,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_47,X0)=select(q15,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f579,f324])).
% 4.26/1.18 fof(f2502,plain,(
% 4.26/1.18 index_213=index_111),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2503,f464])).
% 4.26/1.18 fof(f2503,plain,(
% 4.26/1.18 select(q40,tail)=index_111),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2364,f2135])).
% 4.26/1.18 fof(f2509,plain,(
% 4.26/1.18 index_225=p(index_111)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2502,f2196])).
% 4.26/1.18 fof(f2515,plain,(
% 4.26/1.18 index_225=index_105),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f1330,f2509])).
% 4.26/1.18 fof(f2516,plain,(
% 4.26/1.18 q16=store(queue_47,tail,index_48)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f607,f580])).
% 4.26/1.18 fof(f2517,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q16,X0)=select(queue_47,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2516,f324])).
% 4.26/1.18 fof(f2518,plain,(
% 4.26/1.18 select(q16,tail)=index_48),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2516,f322])).
% 4.26/1.18 fof(f2519,plain,(
% 4.26/1.18 index_51=index_48),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f493,f2518])).
% 4.26/1.18 fof(f2529,plain,(
% 4.26/1.18 select(earray_226,index_105)=e42),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2515,f1016])).
% 4.26/1.18 fof(f2539,plain,(
% 4.26/1.18 index_51=s(index_45)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2519,f492])).
% 4.26/1.18 fof(f2543,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_5,X0)=select(q0,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f581,f324])).
% 4.26/1.18 fof(f2545,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_53,X0)=select(q16,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f582,f324])).
% 4.26/1.18 fof(f2572,plain,(
% 4.26/1.18 q17=store(queue_53,tail,index_54)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f608,f583])).
% 4.26/1.18 fof(f2573,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q17,X0)=select(queue_53,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2572,f324])).
% 4.26/1.18 fof(f2574,plain,(
% 4.26/1.18 select(q17,tail)=index_54),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2572,f322])).
% 4.26/1.18 fof(f2575,plain,(
% 4.26/1.18 index_57=index_54),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f495,f2574])).
% 4.26/1.18 fof(f2576,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_59,X0)=select(q17,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f584,f324])).
% 4.26/1.18 fof(f2578,plain,(
% 4.26/1.18 q18=store(queue_59,tail,index_60)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f609,f585])).
% 4.26/1.18 fof(f2579,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q18,X0)=select(queue_59,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2578,f324])).
% 4.26/1.18 fof(f2580,plain,(
% 4.26/1.18 select(q18,tail)=index_60),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2578,f322])).
% 4.26/1.18 fof(f2581,plain,(
% 4.26/1.18 index_63=index_60),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f498,f2580])).
% 4.26/1.18 fof(f2586,plain,(
% 4.26/1.18 p(index_57)=index_51),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2575,f814])).
% 4.26/1.18 fof(f2590,plain,(
% 4.26/1.18 s(index_63)=p(index_57)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2581,f1031])).
% 4.26/1.18 fof(f2595,plain,(
% 4.26/1.18 index_66=p(index_57)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f499,f2590])).
% 4.26/1.18 fof(f2597,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_65,X0)=select(q18,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f586,f324])).
% 4.26/1.18 fof(f2625,plain,(
% 4.26/1.18 index_66=index_51),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2586,f2595])).
% 4.26/1.18 fof(f2637,plain,(
% 4.26/1.18 q19=store(queue_65,tail,index_66)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f610,f587])).
% 4.26/1.18 fof(f2638,plain,(
% 4.26/1.18 q19=store(queue_65,tail,index_51)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2625,f2637])).
% 4.26/1.18 fof(f2639,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q19,X0)=select(queue_65,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2638,f324])).
% 4.26/1.18 fof(f2640,plain,(
% 4.26/1.18 select(q19,tail)=index_51),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2638,f322])).
% 4.26/1.18 fof(f2641,plain,(
% 4.26/1.18 q1=store(queue_5,tail,index_6)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f600,f588])).
% 4.26/1.18 fof(f2642,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q1,X0)=select(queue_5,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2641,f324])).
% 4.26/1.18 fof(f2643,plain,(
% 4.26/1.18 select(q1,tail)=index_6),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2641,f322])).
% 4.26/1.18 fof(f2644,plain,(
% 4.26/1.18 index_69=index_6),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f500,f2643])).
% 4.26/1.18 fof(f2646,plain,(
% 4.26/1.18 s(index_69)=p(index_3)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2644,f1032])).
% 4.26/1.18 fof(f2651,plain,(
% 4.26/1.18 index_72=p(index_3)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f501,f2646])).
% 4.26/1.18 fof(f2658,plain,(
% 4.26/1.18 s(index_72)=index_3),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2651,f329])).
% 4.26/1.18 fof(f2680,plain,(
% 4.26/1.18 index_263=index_111),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2681,f482])).
% 4.26/1.18 fof(f2681,plain,(
% 4.26/1.18 select(q43,tail)=index_111),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2502,f2240])).
% 4.26/1.18 fof(f2682,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_71,X0)=select(q1,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f589,f324])).
% 4.26/1.18 fof(f2684,plain,(
% 4.26/1.18 q2=store(queue_71,tail,index_72)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f611,f590])).
% 4.26/1.18 fof(f2685,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q2,X0)=select(queue_71,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2684,f324])).
% 4.26/1.18 fof(f2686,plain,(
% 4.26/1.18 select(q2,tail)=index_72),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2684,f322])).
% 4.26/1.18 fof(f2687,plain,(
% 4.26/1.18 index_135=index_72),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f435,f2686])).
% 4.26/1.18 fof(f2688,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_77,X0)=select(q19,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f591,f324])).
% 4.26/1.18 fof(f2691,plain,(
% 4.26/1.18 p(index_111)=index_264),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2680,f794])).
% 4.26/1.18 fof(f2696,plain,(
% 4.26/1.18 index_105=index_264),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f1330,f2691])).
% 4.26/1.18 fof(f2699,plain,(
% 4.26/1.18 s(index_135)=index_3),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2687,f2658])).
% 4.26/1.18 fof(f2705,plain,(
% 4.26/1.18 index_201=index_3),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f1707,f2699])).
% 4.26/1.18 fof(f2707,plain,(
% 4.26/1.18 elem_265=select(earray_260,index_105)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2696,f421])).
% 4.26/1.18 fof(f2710,plain,(
% 4.26/1.18 q20=store(queue_77,tail,index_78)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f612,f592])).
% 4.26/1.18 fof(f2711,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q20,X0)=select(queue_77,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2710,f324])).
% 4.26/1.18 fof(f2712,plain,(
% 4.26/1.18 select(q20,tail)=index_78),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2710,f322])).
% 4.26/1.18 fof(f2713,plain,(
% 4.26/1.18 index_81=index_78),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f504,f2712])).
% 4.26/1.18 fof(f2719,plain,(
% 4.26/1.18 index_201=select(q0,tail)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2705,f485])).
% 4.26/1.18 fof(f2729,plain,(
% 4.26/1.18 p(index_81)=index_75),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2713,f836])).
% 4.26/1.18 fof(f2738,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_83,X0)=select(q20,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f593,f324])).
% 4.26/1.18 fof(f2740,plain,(
% 4.26/1.18 q21=store(queue_83,tail,index_84)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f613,f594])).
% 4.26/1.18 fof(f2741,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q21,X0)=select(queue_83,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2740,f324])).
% 4.26/1.18 fof(f2742,plain,(
% 4.26/1.18 select(q21,tail)=index_84),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2740,f322])).
% 4.26/1.18 fof(f2743,plain,(
% 4.26/1.18 index_87=index_84),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f506,f2742])).
% 4.26/1.18 fof(f2746,plain,(
% 4.26/1.18 s(index_87)=p(index_81)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2743,f1027])).
% 4.26/1.18 fof(f2751,plain,(
% 4.26/1.18 index_90=p(index_81)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f508,f2746])).
% 4.26/1.18 fof(f2776,plain,(
% 4.26/1.18 index_90=index_75),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2729,f2751])).
% 4.26/1.18 fof(f2794,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_89,X0)=select(q21,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f595,f324])).
% 4.26/1.18 fof(f2796,plain,(
% 4.26/1.18 q22=store(queue_89,tail,index_90)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f614,f596])).
% 4.26/1.18 fof(f2797,plain,(
% 4.26/1.18 q22=store(queue_89,tail,index_75)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2776,f2796])).
% 4.26/1.18 fof(f2798,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q22,X0)=select(queue_89,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2797,f324])).
% 4.26/1.18 fof(f2799,plain,(
% 4.26/1.18 select(q22,tail)=index_75),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2797,f322])).
% 4.26/1.18 fof(f2800,plain,(
% 4.26/1.18 ![X0]: (seq=X0|select(queue_95,X0)=select(q22,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f597,f324])).
% 4.26/1.18 fof(f2803,plain,(
% 4.26/1.18 q23=store(queue_95,tail,index_96)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f615,f598])).
% 4.26/1.18 fof(f2804,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q23,X0)=select(queue_95,X0))),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2803,f324])).
% 4.26/1.18 fof(f2805,plain,(
% 4.26/1.18 select(q23,tail)=index_96),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2803,f322])).
% 4.26/1.18 fof(f2806,plain,(
% 4.26/1.18 index_99=index_96),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f511,f2805])).
% 4.26/1.18 fof(f2809,plain,(
% 4.26/1.18 p(index_99)=index_93),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2806,f848])).
% 4.26/1.18 fof(f2814,plain,(
% 4.26/1.18 index_111=index_93),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f1328,f2809])).
% 4.26/1.18 fof(f2818,plain,(
% 4.26/1.18 index_111=select(q22,tail)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2814,f509])).
% 4.26/1.18 fof(f2827,plain,(
% 4.26/1.18 index_237=index_135),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2278,f472])).
% 4.26/1.18 fof(f2866,plain,(
% 4.26/1.18 index_27=index_9),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2316,f484])).
% 4.26/1.18 fof(f2903,plain,(
% 4.26/1.18 select(q8,tail)=index_135),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2827,f2360])).
% 4.26/1.18 fof(f2913,plain,(
% 4.26/1.18 index_135=s(index_15)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2923,f1984])).
% 4.26/1.18 fof(f2923,plain,(
% 4.26/1.18 index_21=index_135),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2903,f2412])).
% 4.26/1.18 fof(f2924,plain,(
% 4.26/1.18 s(index_135)=p(index_15)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2913,f652])).
% 4.26/1.18 fof(f2927,plain,(
% 4.26/1.18 index_201=p(index_15)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f1707,f2924])).
% 4.26/1.18 fof(f2928,plain,(
% 4.26/1.18 index_201=index_9),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f1626,f2927])).
% 4.26/1.18 fof(f2987,plain,(
% 4.26/1.18 index_45=index_9),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2988,f491])).
% 4.26/1.18 fof(f2988,plain,(
% 4.26/1.18 select(q15,tail)=index_9),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2866,f2499])).
% 4.26/1.18 fof(f2994,plain,(
% 4.26/1.18 index_51=s(index_9)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2987,f2539])).
% 4.26/1.18 fof(f3000,plain,(
% 4.26/1.18 index_51=index_15),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f1629,f2994])).
% 4.26/1.18 fof(f3035,plain,(
% 4.26/1.18 index_75=index_15),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3036,f502])).
% 4.26/1.18 fof(f3036,plain,(
% 4.26/1.18 select(q19,tail)=index_15),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f3000,f2640])).
% 4.26/1.18 fof(f3074,plain,(
% 4.26/1.18 index_9=select(q0,tail)),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f2928,f2719])).
% 4.26/1.18 fof(f3088,plain,(
% 4.26/1.18 select(q22,tail)=index_15),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f3035,f2799])).
% 4.26/1.18 fof(f3089,plain,(
% 4.26/1.18 index_111=index_15),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f2818,f3088])).
% 4.26/1.18 fof(f3112,plain,(
% 4.26/1.18 p(index_111)=index_9),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3089,f1626])).
% 4.26/1.18 fof(f3162,plain,(
% 4.26/1.18 index_9=index_105),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3112,f1330])).
% 4.26/1.18 fof(f3175,plain,(
% 4.26/1.18 select(earray_226,index_9)=e42),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3162,f2529])).
% 4.26/1.18 fof(f3185,plain,(
% 4.26/1.18 elem_265=select(earray_260,index_9)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3162,f2707])).
% 4.26/1.18 fof(f3535,plain,(
% 4.26/1.18 head=tail|select(q0,tail)=index_0),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f422,f1239])).
% 4.26/1.18 fof(f3537,plain,(
% 4.26/1.18 head=tail|index_9=index_0),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f3074,f3535])).
% 4.26/1.18 fof(f3538,plain,(
% 4.26/1.18 index_9=index_0),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f3537,f325])).
% 4.26/1.18 fof(f3541,plain,(
% 4.26/1.18 select(q0,head)=index_9),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3538,f1240])).
% 4.26/1.18 fof(f3551,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q24,X0)=select(q23,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1241,f1274])).
% 4.26/1.18 fof(f3566,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q25,X0)=select(q24,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1320,f1323])).
% 4.26/1.18 fof(f3583,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q26,X0)=select(q25,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1386,f1390])).
% 4.26/1.18 fof(f3598,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q27,X0)=select(q26,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1422,f1572])).
% 4.26/1.18 fof(f3613,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q28,X0)=select(q27,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1575,f1608])).
% 4.26/1.18 fof(f3626,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q10,X0)=select(q9,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1384,f1612])).
% 4.26/1.18 fof(f3636,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q29,X0)=select(q28,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1615,f1633])).
% 4.26/1.18 fof(f3656,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q3,X0)=select(q2,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1695,f1698])).
% 4.26/1.18 fof(f3671,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q30,X0)=select(q29,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1720,f1724])).
% 4.26/1.18 fof(f3686,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q31,X0)=select(q30,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1726,f1751])).
% 4.26/1.18 fof(f3701,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q32,X0)=select(q31,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1784,f1787])).
% 4.26/1.18 fof(f3716,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q33,X0)=select(q32,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1824,f1828])).
% 4.26/1.18 fof(f3731,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q34,X0)=select(q33,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1830,f1846])).
% 4.26/1.18 fof(f3748,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q35,X0)=select(q34,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1876,f1906])).
% 4.26/1.18 fof(f3763,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q36,X0)=select(q35,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1909,f1912])).
% 4.26/1.18 fof(f3778,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q37,X0)=select(q36,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1930,f1972])).
% 4.26/1.18 fof(f3791,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q11,X0)=select(q10,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f1874,f1975])).
% 4.26/1.18 fof(f3806,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q38,X0)=select(q37,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2014,f2017])).
% 4.26/1.18 fof(f3821,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q39,X0)=select(q38,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2020,f2047])).
% 4.26/1.18 fof(f3836,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q4,X0)=select(q3,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2086,f2089])).
% 4.26/1.18 fof(f3846,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q40,X0)=select(q39,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2130,f2134])).
% 4.26/1.18 fof(f3866,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q41,X0)=select(q40,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2136,f2141])).
% 4.26/1.18 fof(f3881,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q42,X0)=select(q41,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2179,f2182])).
% 4.26/1.18 fof(f3895,plain,(
% 4.26/1.18 tail=seq|select(q43,seq)=earray_226),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2236,f2239])).
% 4.26/1.18 fof(f3896,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q43,X0)=select(q42,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2235,f2239])).
% 4.26/1.18 fof(f3899,plain,(
% 4.26/1.18 tail=seq|earray_260=earray_226),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f393,f3895])).
% 4.26/1.18 fof(f3900,plain,(
% 4.26/1.18 earray_260=earray_226),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f3899,f327])).
% 4.26/1.18 fof(f3903,plain,(
% 4.26/1.18 elem_265=select(earray_226,index_9)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3900,f3185])).
% 4.26/1.18 fof(f3905,plain,(
% 4.26/1.18 elem_262=select(earray_226,index_261)),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3900,f420])).
% 4.26/1.18 fof(f3906,plain,(
% 4.26/1.18 elem_265=e42),
% 4.26/1.18 inference(forward_demodulation,[status(thm)],[f3175,f3903])).
% 4.26/1.18 fof(f3907,plain,(
% 4.26/1.18 ~elem_262=e42),
% 4.26/1.18 inference(backward_demodulation,[status(thm)],[f3906,f643])).
% 4.26/1.18 fof(f3913,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q5,X0)=select(q4,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2244,f2277])).
% 4.26/1.18 fof(f3928,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q6,X0)=select(q5,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2279,f2287])).
% 4.26/1.18 fof(f3943,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q7,X0)=select(q6,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2290,f2293])).
% 4.26/1.18 fof(f3956,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q12,X0)=select(q11,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2241,f2315])).
% 4.26/1.18 fof(f3971,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q8,X0)=select(q7,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2355,f2359])).
% 4.26/1.18 fof(f3986,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q9,X0)=select(q8,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2393,f2396])).
% 4.26/1.18 fof(f3996,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q13,X0)=select(q12,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2399,f2416])).
% 4.26/1.18 fof(f4027,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q14,X0)=select(q13,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2448,f2451])).
% 4.26/1.18 fof(f4042,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q15,X0)=select(q14,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2494,f2498])).
% 4.26/1.18 fof(f4052,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q16,X0)=select(q15,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2500,f2517])).
% 4.26/1.18 fof(f4074,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q17,X0)=select(q16,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2545,f2573])).
% 4.26/1.18 fof(f4089,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q18,X0)=select(q17,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2576,f2579])).
% 4.26/1.18 fof(f4104,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q19,X0)=select(q18,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2597,f2639])).
% 4.26/1.18 fof(f4117,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q1,X0)=select(q0,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2543,f2642])).
% 4.26/1.18 fof(f4132,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q2,X0)=select(q1,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2682,f2685])).
% 4.26/1.18 fof(f4154,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q20,X0)=select(q19,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2688,f2711])).
% 4.26/1.18 fof(f4169,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q21,X0)=select(q20,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2738,f2741])).
% 4.26/1.18 fof(f4184,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q22,X0)=select(q21,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2794,f2798])).
% 4.26/1.18 fof(f4199,plain,(
% 4.26/1.18 ![X0]: (tail=X0|select(q23,X0)=select(q22,X0)|seq=X0)),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f2800,f2804])).
% 4.26/1.18 fof(f4539,plain,(
% 4.26/1.18 tail=head|index_261=select(q42,head)|seq=head),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f481,f3896])).
% 4.26/1.18 fof(f4543,plain,(
% 4.26/1.18 index_261=select(q42,head)|seq=head),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f4539,f325])).
% 4.26/1.18 fof(f4545,plain,(
% 4.26/1.18 index_261=select(q42,head)),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f4543,f326])).
% 4.26/1.18 fof(f4546,plain,(
% 4.26/1.18 index_261=select(q41,head)|tail=head|seq=head),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f3881,f4545])).
% 4.26/1.18 fof(f4548,plain,(
% 4.26/1.18 index_261=select(q41,head)|seq=head),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f4546,f325])).
% 4.26/1.18 fof(f4550,plain,(
% 4.26/1.18 index_261=select(q41,head)),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f4548,f326])).
% 4.26/1.18 fof(f4551,plain,(
% 4.26/1.18 index_261=select(q40,head)|tail=head|seq=head),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f3866,f4550])).
% 4.26/1.18 fof(f4553,plain,(
% 4.26/1.18 index_261=select(q40,head)|seq=head),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f4551,f325])).
% 4.26/1.18 fof(f4555,plain,(
% 4.26/1.18 index_261=select(q40,head)),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f4553,f326])).
% 4.26/1.18 fof(f4556,plain,(
% 4.26/1.18 index_261=select(q39,head)|tail=head|seq=head),
% 4.26/1.18 inference(paramodulation,[status(thm)],[f3846,f4555])).
% 4.26/1.18 fof(f4558,plain,(
% 4.26/1.18 index_261=select(q39,head)|seq=head),
% 4.26/1.18 inference(forward_subsumption_resolution,[status(thm)],[f4556,f325])).
% 4.26/1.19 fof(f4560,plain,(
% 4.26/1.19 index_261=select(q39,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4558,f326])).
% 4.26/1.19 fof(f4561,plain,(
% 4.26/1.19 index_261=select(q38,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3821,f4560])).
% 4.26/1.19 fof(f4563,plain,(
% 4.26/1.19 index_261=select(q38,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4561,f325])).
% 4.26/1.19 fof(f4565,plain,(
% 4.26/1.19 index_261=select(q38,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4563,f326])).
% 4.26/1.19 fof(f4566,plain,(
% 4.26/1.19 index_261=select(q37,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3806,f4565])).
% 4.26/1.19 fof(f4568,plain,(
% 4.26/1.19 index_261=select(q37,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4566,f325])).
% 4.26/1.19 fof(f4570,plain,(
% 4.26/1.19 index_261=select(q37,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4568,f326])).
% 4.26/1.19 fof(f4571,plain,(
% 4.26/1.19 index_261=select(q36,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3778,f4570])).
% 4.26/1.19 fof(f4573,plain,(
% 4.26/1.19 index_261=select(q36,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4571,f325])).
% 4.26/1.19 fof(f4575,plain,(
% 4.26/1.19 index_261=select(q36,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4573,f326])).
% 4.26/1.19 fof(f4576,plain,(
% 4.26/1.19 index_261=select(q35,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3763,f4575])).
% 4.26/1.19 fof(f4578,plain,(
% 4.26/1.19 index_261=select(q35,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4576,f325])).
% 4.26/1.19 fof(f4584,plain,(
% 4.26/1.19 index_261=select(q35,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4578,f326])).
% 4.26/1.19 fof(f4585,plain,(
% 4.26/1.19 index_261=select(q34,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3748,f4584])).
% 4.26/1.19 fof(f4587,plain,(
% 4.26/1.19 index_261=select(q34,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4585,f325])).
% 4.26/1.19 fof(f4589,plain,(
% 4.26/1.19 index_261=select(q34,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4587,f326])).
% 4.26/1.19 fof(f4590,plain,(
% 4.26/1.19 index_261=select(q33,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3731,f4589])).
% 4.26/1.19 fof(f4592,plain,(
% 4.26/1.19 index_261=select(q33,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4590,f325])).
% 4.26/1.19 fof(f4594,plain,(
% 4.26/1.19 index_261=select(q33,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4592,f326])).
% 4.26/1.19 fof(f4595,plain,(
% 4.26/1.19 index_261=select(q32,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3716,f4594])).
% 4.26/1.19 fof(f4597,plain,(
% 4.26/1.19 index_261=select(q32,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4595,f325])).
% 4.26/1.19 fof(f4603,plain,(
% 4.26/1.19 index_261=select(q32,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4597,f326])).
% 4.26/1.19 fof(f4604,plain,(
% 4.26/1.19 index_261=select(q31,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3701,f4603])).
% 4.26/1.19 fof(f4606,plain,(
% 4.26/1.19 index_261=select(q31,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4604,f325])).
% 4.26/1.19 fof(f4608,plain,(
% 4.26/1.19 index_261=select(q31,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4606,f326])).
% 4.26/1.19 fof(f4609,plain,(
% 4.26/1.19 index_261=select(q30,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3686,f4608])).
% 4.26/1.19 fof(f4611,plain,(
% 4.26/1.19 index_261=select(q30,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4609,f325])).
% 4.26/1.19 fof(f4613,plain,(
% 4.26/1.19 index_261=select(q30,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4611,f326])).
% 4.26/1.19 fof(f4614,plain,(
% 4.26/1.19 index_261=select(q29,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3671,f4613])).
% 4.26/1.19 fof(f4616,plain,(
% 4.26/1.19 index_261=select(q29,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4614,f325])).
% 4.26/1.19 fof(f4618,plain,(
% 4.26/1.19 index_261=select(q29,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4616,f326])).
% 4.26/1.19 fof(f4619,plain,(
% 4.26/1.19 index_261=select(q28,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3636,f4618])).
% 4.26/1.19 fof(f4621,plain,(
% 4.26/1.19 index_261=select(q28,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4619,f325])).
% 4.26/1.19 fof(f4623,plain,(
% 4.26/1.19 index_261=select(q28,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4621,f326])).
% 4.26/1.19 fof(f4624,plain,(
% 4.26/1.19 index_261=select(q27,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3613,f4623])).
% 4.26/1.19 fof(f4626,plain,(
% 4.26/1.19 index_261=select(q27,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4624,f325])).
% 4.26/1.19 fof(f4628,plain,(
% 4.26/1.19 index_261=select(q27,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4626,f326])).
% 4.26/1.19 fof(f4629,plain,(
% 4.26/1.19 index_261=select(q26,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3598,f4628])).
% 4.26/1.19 fof(f4631,plain,(
% 4.26/1.19 index_261=select(q26,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4629,f325])).
% 4.26/1.19 fof(f4637,plain,(
% 4.26/1.19 index_261=select(q26,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4631,f326])).
% 4.26/1.19 fof(f4638,plain,(
% 4.26/1.19 index_261=select(q25,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3583,f4637])).
% 4.26/1.19 fof(f4640,plain,(
% 4.26/1.19 index_261=select(q25,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4638,f325])).
% 4.26/1.19 fof(f4642,plain,(
% 4.26/1.19 index_261=select(q25,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4640,f326])).
% 4.26/1.19 fof(f4643,plain,(
% 4.26/1.19 index_261=select(q24,head)|tail=head|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3566,f4642])).
% 4.26/1.19 fof(f4645,plain,(
% 4.26/1.19 index_261=select(q24,head)|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4643,f325])).
% 4.26/1.19 fof(f4647,plain,(
% 4.26/1.19 index_261=select(q24,head)),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4645,f326])).
% 4.26/1.19 fof(f4658,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q8,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3626,f3986])).
% 4.26/1.19 fof(f4662,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q8,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4658])).
% 4.26/1.19 fof(f4698,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q2,X0)=select(q0,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4117,f4132])).
% 4.26/1.19 fof(f4702,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q2,X0)=select(q0,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4698])).
% 4.26/1.19 fof(f4718,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q22,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3551,f4199])).
% 4.26/1.19 fof(f4722,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q22,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4718])).
% 4.26/1.19 fof(f4744,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q7,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3971,f4662])).
% 4.26/1.19 fof(f4748,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q7,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4744])).
% 4.26/1.19 fof(f4750,plain,(
% 4.26/1.19 tail=head|select(q2,head)=index_9|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3541,f4702])).
% 4.26/1.19 fof(f4756,plain,(
% 4.26/1.19 select(q2,head)=index_9|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4750,f325])).
% 4.26/1.19 fof(f4758,plain,(
% 4.26/1.19 select(q2,head)=index_9),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4756,f326])).
% 4.26/1.19 fof(f4761,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q21,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4184,f4722])).
% 4.26/1.19 fof(f4765,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q21,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4761])).
% 4.26/1.19 fof(f4769,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q6,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3943,f4748])).
% 4.26/1.19 fof(f4773,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q6,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4769])).
% 4.26/1.19 fof(f4777,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q20,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4169,f4765])).
% 4.26/1.19 fof(f4781,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q20,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4777])).
% 4.26/1.19 fof(f4797,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q5,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3928,f4773])).
% 4.26/1.19 fof(f4801,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q5,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4797])).
% 4.26/1.19 fof(f4805,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q19,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4154,f4781])).
% 4.26/1.19 fof(f4809,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q19,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4805])).
% 4.26/1.19 fof(f4813,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q4,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3913,f4801])).
% 4.26/1.19 fof(f4817,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q4,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4813])).
% 4.26/1.19 fof(f4821,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q18,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4104,f4809])).
% 4.26/1.19 fof(f4825,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q18,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4821])).
% 4.26/1.19 fof(f4829,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q3,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3836,f4817])).
% 4.26/1.19 fof(f4833,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q3,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4829])).
% 4.26/1.19 fof(f4837,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q17,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4089,f4825])).
% 4.26/1.19 fof(f4841,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q17,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4837])).
% 4.26/1.19 fof(f4845,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q2,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3656,f4833])).
% 4.26/1.19 fof(f4849,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q10,X0)=select(q2,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4845])).
% 4.26/1.19 fof(f4853,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q16,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4074,f4841])).
% 4.26/1.19 fof(f4857,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q16,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4853])).
% 4.26/1.19 fof(f4871,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q15,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4052,f4857])).
% 4.26/1.19 fof(f4875,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q15,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4871])).
% 4.26/1.19 fof(f4879,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q14,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4042,f4875])).
% 4.26/1.19 fof(f4883,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q14,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4879])).
% 4.26/1.19 fof(f4887,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q13,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4027,f4883])).
% 4.26/1.19 fof(f4891,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q13,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4887])).
% 4.26/1.19 fof(f4895,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q12,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3996,f4891])).
% 4.26/1.19 fof(f4899,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q12,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4895])).
% 4.26/1.19 fof(f4903,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q11,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3956,f4899])).
% 4.26/1.19 fof(f4907,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q11,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4903])).
% 4.26/1.19 fof(f4911,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q10,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f3791,f4907])).
% 4.26/1.19 fof(f4915,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q10,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4911])).
% 4.26/1.19 fof(f4919,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q2,X0)|seq=X0|tail=X0|seq=X0)),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4849,f4915])).
% 4.26/1.19 fof(f4923,plain,(
% 4.26/1.19 ![X0]: (tail=X0|select(q24,X0)=select(q2,X0)|seq=X0)),
% 4.26/1.19 inference(duplicate_literals_removal,[status(thm)],[f4919])).
% 4.26/1.19 fof(f4925,plain,(
% 4.26/1.19 tail=head|select(q24,head)=index_9|seq=head),
% 4.26/1.19 inference(paramodulation,[status(thm)],[f4758,f4923])).
% 4.26/1.19 fof(f4931,plain,(
% 4.26/1.19 tail=head|index_261=index_9|seq=head),
% 4.26/1.19 inference(forward_demodulation,[status(thm)],[f4647,f4925])).
% 4.26/1.19 fof(f4932,plain,(
% 4.26/1.19 index_261=index_9|seq=head),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4931,f325])).
% 4.26/1.19 fof(f4973,plain,(
% 4.26/1.19 elem_262=select(earray_226,index_9)),
% 4.26/1.19 inference(backward_demodulation,[status(thm)],[f4975,f3905])).
% 4.26/1.19 fof(f4975,plain,(
% 4.26/1.19 index_261=index_9),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4932,f326])).
% 4.26/1.19 fof(f4982,plain,(
% 4.26/1.19 elem_262=e42),
% 4.26/1.19 inference(forward_demodulation,[status(thm)],[f3175,f4973])).
% 4.26/1.19 fof(f4983,plain,(
% 4.26/1.19 $false),
% 4.26/1.19 inference(forward_subsumption_resolution,[status(thm)],[f4982,f3907])).
% 4.26/1.19 % SZS output end CNFRefutation for theBenchmark.p
% 4.26/1.20 % Elapsed time: 0.705155 seconds
% 4.26/1.20 % CPU time: 4.978467 seconds
% 4.26/1.20 % Total memory used: 153.204 MB
% 4.26/1.20 % Net memory used: 150.565 MB
%------------------------------------------------------------------------------