%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV568-1.040 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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:49:06 PM UTC 2026
% Result : Unsatisfiable 28.64s 14.10s
% Output : CNFRefutation 29.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 334
% Syntax : Number of formulae : 1770 (1655 unt; 0 def)
% Number of atoms : 1941 (1940 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 582 ( 411 ~; 171 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 1 avg)
% Maximal term depth : 27 ( 4 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 349 ( 349 usr; 340 con; 0-3 aty)
% Number of variables : 186 ( 186 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,E] : rselect_seq(rstore_seq(A,E)) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,E] : rselect_head(rstore_head(A,E)) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,E] : rselect_tail(rstore_tail(A,E)) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,E] : rselect_seq(rstore_head(A,E)) = rselect_seq(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,E] : rselect_seq(rstore_tail(A,E)) = rselect_seq(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,E] : rselect_head(rstore_tail(A,E)) = rselect_head(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,E] : rselect_head(rstore_seq(A,E)) = rselect_head(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,E] : rselect_tail(rstore_head(A,E)) = rselect_tail(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(X))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(X)))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [X] : s(s(s(s(s(s(s(s(s(X))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [X] : s(s(s(s(s(s(s(s(X)))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [X] : s(s(s(s(s(s(s(X))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [X] : s(s(s(s(s(s(X)))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [X] : s(s(s(s(s(X))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [X] : s(s(s(s(X)))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [X] : s(s(s(X))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [X] : s(s(X)) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [X] : s(X) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,hypothesis,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
earray_104 = rselect_seq(q22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,hypothesis,
earray_110 = rselect_seq(q23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,hypothesis,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,hypothesis,
earray_119 = rselect_seq(q24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,hypothesis,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,hypothesis,
earray_125 = rselect_seq(q25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,hypothesis,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,hypothesis,
earray_131 = rselect_seq(q26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,hypothesis,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,hypothesis,
earray_140 = rselect_seq(q27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,hypothesis,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,hypothesis,
earray_146 = rselect_seq(q28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,hypothesis,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,hypothesis,
earray_161 = rselect_seq(q29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,hypothesis,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,hypothesis,
earray_170 = rselect_seq(q30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,hypothesis,
earray_172 = store(earray_170,index_171,e30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,hypothesis,
earray_176 = rselect_seq(q31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,hypothesis,
earray_178 = store(earray_176,index_177,e31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,hypothesis,
earray_182 = rselect_seq(q32),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,hypothesis,
earray_184 = store(earray_182,index_183,e32),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,hypothesis,
earray_191 = rselect_seq(q33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
earray_193 = store(earray_191,index_192,e33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,hypothesis,
earray_197 = rselect_seq(q34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,hypothesis,
earray_199 = store(earray_197,index_198,e34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,hypothesis,
earray_203 = rselect_seq(q35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
earray_205 = store(earray_203,index_204,e35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
earray_212 = rselect_seq(q36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
earray_214 = store(earray_212,index_213,e36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,hypothesis,
earray_218 = rselect_seq(q37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
earray_220 = store(earray_218,index_219,e37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,hypothesis,
earray_224 = rselect_seq(q38),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,hypothesis,
earray_226 = store(earray_224,index_225,e38),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,hypothesis,
earray_239 = rselect_seq(q39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,hypothesis,
earray_241 = store(earray_239,index_240,e39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,hypothesis,
earray_281 = rselect_seq(q40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,hypothesis,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,hypothesis,
earray_41 = rselect_seq(q14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,hypothesis,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,hypothesis,
earray_50 = rselect_seq(q15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,hypothesis,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,hypothesis,
earray_56 = rselect_seq(q16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,hypothesis,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,hypothesis,
earray_62 = rselect_seq(q17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,hypothesis,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,hypothesis,
earray_71 = rselect_seq(q18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f150,hypothesis,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f154,hypothesis,
earray_83 = rselect_seq(q19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,hypothesis,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,hypothesis,
earray_89 = rselect_seq(q20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,hypothesis,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,hypothesis,
earray_98 = rselect_seq(q21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,hypothesis,
elem_283 = select(earray_281,index_282),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,hypothesis,
index_0 = rselect_tail(q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,hypothesis,
index_105 = rselect_tail(q22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,hypothesis,
index_111 = rselect_tail(q23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f165,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f166,hypothesis,
index_116 = rselect_head(queue_115),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f167,hypothesis,
index_117 = s(index_116),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,hypothesis,
index_120 = rselect_tail(q24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f170,hypothesis,
index_123 = s(index_120),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,hypothesis,
index_126 = rselect_tail(q25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,hypothesis,
index_129 = s(index_126),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,hypothesis,
index_132 = rselect_tail(q26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,hypothesis,
index_135 = s(index_132),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,hypothesis,
index_137 = rselect_head(queue_136),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f176,hypothesis,
index_138 = s(index_137),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f177,hypothesis,
index_141 = rselect_tail(q27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,hypothesis,
index_147 = rselect_tail(q28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f180,hypothesis,
index_15 = rselect_tail(q10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f181,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f182,hypothesis,
index_153 = rselect_tail(q2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f183,hypothesis,
index_156 = s(index_153),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f184,hypothesis,
index_158 = rselect_head(queue_157),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,hypothesis,
index_159 = s(index_158),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,hypothesis,
index_162 = rselect_tail(q29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,hypothesis,
index_165 = s(index_162),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,hypothesis,
index_167 = rselect_head(queue_166),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,hypothesis,
index_168 = s(index_167),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,hypothesis,
index_171 = rselect_tail(q30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,hypothesis,
index_177 = rselect_tail(q31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,hypothesis,
index_18 = s(index_15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,hypothesis,
index_180 = s(index_177),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,hypothesis,
index_183 = rselect_tail(q32),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,hypothesis,
index_188 = rselect_head(queue_187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,hypothesis,
index_189 = s(index_188),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,hypothesis,
index_192 = rselect_tail(q33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,hypothesis,
index_195 = s(index_192),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,hypothesis,
index_198 = rselect_tail(q34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,hypothesis,
index_201 = s(index_198),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f203,hypothesis,
index_204 = rselect_tail(q35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,hypothesis,
index_207 = s(index_204),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f205,hypothesis,
index_209 = rselect_head(queue_208),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f206,hypothesis,
index_21 = rselect_tail(q11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f207,hypothesis,
index_210 = s(index_209),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f208,hypothesis,
index_213 = rselect_tail(q36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f209,hypothesis,
index_216 = s(index_213),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f210,hypothesis,
index_219 = rselect_tail(q37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,hypothesis,
index_222 = s(index_219),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f212,hypothesis,
index_225 = rselect_tail(q38),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,hypothesis,
index_228 = s(index_225),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f214,hypothesis,
index_230 = rselect_head(queue_229),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f215,hypothesis,
index_231 = s(index_230),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f216,hypothesis,
index_234 = rselect_tail(q3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f217,hypothesis,
index_237 = s(index_234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f218,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f219,hypothesis,
index_240 = rselect_tail(q39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f221,hypothesis,
index_246 = rselect_tail(q4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f222,hypothesis,
index_249 = s(index_246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f223,hypothesis,
index_252 = rselect_tail(q5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f224,hypothesis,
index_255 = s(index_252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f225,hypothesis,
index_257 = rselect_head(queue_256),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f226,hypothesis,
index_258 = s(index_257),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f227,hypothesis,
index_26 = rselect_head(queue_25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f228,hypothesis,
index_261 = rselect_tail(q6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f229,hypothesis,
index_264 = s(index_261),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f230,hypothesis,
index_267 = rselect_tail(q7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f231,hypothesis,
index_27 = s(index_26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f232,hypothesis,
index_270 = s(index_267),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f233,hypothesis,
index_273 = rselect_tail(q8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f234,hypothesis,
index_276 = s(index_273),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f235,hypothesis,
index_278 = rselect_head(queue_277),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f236,hypothesis,
index_279 = s(index_278),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f237,hypothesis,
index_282 = rselect_head(q40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f238,hypothesis,
index_3 = rselect_tail(q0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f239,hypothesis,
index_30 = rselect_tail(q12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f240,hypothesis,
index_33 = s(index_30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f241,hypothesis,
index_36 = rselect_tail(q13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f242,hypothesis,
index_39 = s(index_36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f243,hypothesis,
index_42 = rselect_tail(q14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f244,hypothesis,
index_45 = s(index_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f245,hypothesis,
index_47 = rselect_head(queue_46),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f246,hypothesis,
index_48 = s(index_47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f247,hypothesis,
index_51 = rselect_tail(q15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f248,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f249,hypothesis,
index_57 = rselect_tail(q16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f250,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f251,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f252,hypothesis,
index_63 = rselect_tail(q17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f254,hypothesis,
index_68 = rselect_head(queue_67),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f255,hypothesis,
index_69 = s(index_68),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f256,hypothesis,
index_72 = rselect_tail(q18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f257,hypothesis,
index_75 = s(index_72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f258,hypothesis,
index_78 = rselect_tail(q1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f259,hypothesis,
index_81 = s(index_78),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f260,hypothesis,
index_84 = rselect_tail(q19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f261,hypothesis,
index_87 = s(index_84),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f262,hypothesis,
index_9 = rselect_tail(q9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f263,hypothesis,
index_90 = rselect_tail(q20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f264,hypothesis,
index_93 = s(index_90),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f265,hypothesis,
index_95 = rselect_head(queue_94),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f266,hypothesis,
index_96 = s(index_95),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f267,hypothesis,
index_99 = rselect_tail(q21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f268,hypothesis,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f269,hypothesis,
queue_101 = rstore_seq(q21,earray_100),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f270,hypothesis,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f271,hypothesis,
queue_107 = rstore_seq(q22,earray_106),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f272,hypothesis,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f273,hypothesis,
queue_11 = rstore_seq(q9,earray_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f274,hypothesis,
queue_113 = rstore_seq(q23,earray_112),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f275,hypothesis,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f276,hypothesis,
queue_118 = rstore_head(queue_115,index_117),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f277,hypothesis,
queue_122 = rstore_seq(q24,earray_121),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f278,hypothesis,
queue_124 = rstore_tail(queue_122,index_123),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f279,hypothesis,
queue_128 = rstore_seq(q25,earray_127),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,hypothesis,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f281,hypothesis,
queue_130 = rstore_tail(queue_128,index_129),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f282,hypothesis,
queue_134 = rstore_seq(q26,earray_133),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f283,hypothesis,
queue_136 = rstore_tail(queue_134,index_135),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f284,hypothesis,
queue_139 = rstore_head(queue_136,index_138),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f285,hypothesis,
queue_143 = rstore_seq(q27,earray_142),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f286,hypothesis,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f287,hypothesis,
queue_149 = rstore_seq(q28,earray_148),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f288,hypothesis,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,hypothesis,
queue_155 = rstore_seq(q2,earray_154),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f290,hypothesis,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f291,hypothesis,
queue_160 = rstore_head(queue_157,index_159),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f292,hypothesis,
queue_164 = rstore_seq(q29,earray_163),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f293,hypothesis,
queue_166 = rstore_tail(queue_164,index_165),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f294,hypothesis,
queue_169 = rstore_head(queue_166,index_168),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f295,hypothesis,
queue_17 = rstore_seq(q10,earray_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f296,hypothesis,
queue_173 = rstore_seq(q30,earray_172),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f297,hypothesis,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f298,hypothesis,
queue_179 = rstore_seq(q31,earray_178),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f299,hypothesis,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f300,hypothesis,
queue_185 = rstore_seq(q32,earray_184),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f301,hypothesis,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f302,hypothesis,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f303,hypothesis,
queue_190 = rstore_head(queue_187,index_189),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f304,hypothesis,
queue_194 = rstore_seq(q33,earray_193),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f305,hypothesis,
queue_196 = rstore_tail(queue_194,index_195),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f306,hypothesis,
queue_200 = rstore_seq(q34,earray_199),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f307,hypothesis,
queue_202 = rstore_tail(queue_200,index_201),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f308,hypothesis,
queue_206 = rstore_seq(q35,earray_205),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f309,hypothesis,
queue_208 = rstore_tail(queue_206,index_207),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f310,hypothesis,
queue_211 = rstore_head(queue_208,index_210),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f311,hypothesis,
queue_215 = rstore_seq(q36,earray_214),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f312,hypothesis,
queue_217 = rstore_tail(queue_215,index_216),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f313,hypothesis,
queue_221 = rstore_seq(q37,earray_220),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f314,hypothesis,
queue_223 = rstore_tail(queue_221,index_222),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f315,hypothesis,
queue_227 = rstore_seq(q38,earray_226),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f316,hypothesis,
queue_229 = rstore_tail(queue_227,index_228),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f317,hypothesis,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f318,hypothesis,
queue_232 = rstore_head(queue_229,index_231),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f319,hypothesis,
queue_236 = rstore_seq(q3,earray_235),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f320,hypothesis,
queue_238 = rstore_tail(queue_236,index_237),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f321,hypothesis,
queue_242 = rstore_seq(q39,earray_241),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f322,hypothesis,
queue_244 = rstore_tail(queue_242,index_243),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f323,hypothesis,
queue_248 = rstore_seq(q4,earray_247),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f324,hypothesis,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f325,hypothesis,
queue_250 = rstore_tail(queue_248,index_249),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f326,hypothesis,
queue_254 = rstore_seq(q5,earray_253),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f327,hypothesis,
queue_256 = rstore_tail(queue_254,index_255),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f328,hypothesis,
queue_259 = rstore_head(queue_256,index_258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f329,hypothesis,
queue_263 = rstore_seq(q6,earray_262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f330,hypothesis,
queue_265 = rstore_tail(queue_263,index_264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f331,hypothesis,
queue_269 = rstore_seq(q7,earray_268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f332,hypothesis,
queue_271 = rstore_tail(queue_269,index_270),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f333,hypothesis,
queue_275 = rstore_seq(q8,earray_274),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f334,hypothesis,
queue_277 = rstore_tail(queue_275,index_276),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f335,hypothesis,
queue_28 = rstore_head(queue_25,index_27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f336,hypothesis,
queue_280 = rstore_head(queue_277,index_279),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f337,hypothesis,
queue_32 = rstore_seq(q12,earray_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f338,hypothesis,
queue_34 = rstore_tail(queue_32,index_33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f339,hypothesis,
queue_38 = rstore_seq(q13,earray_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f340,hypothesis,
queue_40 = rstore_tail(queue_38,index_39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f341,hypothesis,
queue_44 = rstore_seq(q14,earray_43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f342,hypothesis,
queue_46 = rstore_tail(queue_44,index_45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f343,hypothesis,
queue_49 = rstore_head(queue_46,index_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f344,hypothesis,
queue_5 = rstore_seq(q0,earray_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f345,hypothesis,
queue_53 = rstore_seq(q15,earray_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f346,hypothesis,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f347,hypothesis,
queue_59 = rstore_seq(q16,earray_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f348,hypothesis,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f349,hypothesis,
queue_65 = rstore_seq(q17,earray_64),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f350,hypothesis,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f351,hypothesis,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f352,hypothesis,
queue_70 = rstore_head(queue_67,index_69),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f353,hypothesis,
queue_74 = rstore_seq(q18,earray_73),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f354,hypothesis,
queue_76 = rstore_tail(queue_74,index_75),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f355,hypothesis,
queue_80 = rstore_seq(q1,earray_79),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f356,hypothesis,
queue_82 = rstore_tail(queue_80,index_81),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f357,hypothesis,
queue_86 = rstore_seq(q19,earray_85),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f358,hypothesis,
queue_88 = rstore_tail(queue_86,index_87),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f359,hypothesis,
queue_92 = rstore_seq(q20,earray_91),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f360,hypothesis,
queue_94 = rstore_tail(queue_92,index_93),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f361,hypothesis,
queue_97 = rstore_head(queue_94,index_96),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f362,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f363,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f364,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f365,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f366,hypothesis,
q12 = queue_28,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f367,hypothesis,
q13 = queue_34,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f368,hypothesis,
q14 = queue_40,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f369,hypothesis,
q15 = queue_49,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f370,hypothesis,
q16 = queue_55,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f371,hypothesis,
q17 = queue_61,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f372,hypothesis,
q18 = queue_70,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f373,hypothesis,
q19 = queue_76,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f374,hypothesis,
q2 = queue_82,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f375,hypothesis,
q20 = queue_88,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f376,hypothesis,
q21 = queue_97,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f377,hypothesis,
q22 = queue_103,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f378,hypothesis,
q23 = queue_109,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f379,hypothesis,
q24 = queue_118,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f380,hypothesis,
q25 = queue_124,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f381,hypothesis,
q26 = queue_130,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f382,hypothesis,
q27 = queue_139,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f383,hypothesis,
q28 = queue_145,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f384,hypothesis,
q29 = queue_151,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f385,hypothesis,
q3 = queue_160,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f386,hypothesis,
q30 = queue_169,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f387,hypothesis,
q31 = queue_175,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f388,hypothesis,
q32 = queue_181,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f389,hypothesis,
q33 = queue_190,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f390,hypothesis,
q34 = queue_196,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f391,hypothesis,
q35 = queue_202,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f392,hypothesis,
q36 = queue_211,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f393,hypothesis,
q37 = queue_217,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f394,hypothesis,
q38 = queue_223,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f395,hypothesis,
q39 = queue_232,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f396,hypothesis,
q4 = queue_238,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f397,hypothesis,
q40 = queue_244,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f398,hypothesis,
q5 = queue_250,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f399,hypothesis,
q6 = queue_259,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f400,hypothesis,
q7 = queue_265,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f401,hypothesis,
q8 = queue_271,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f402,hypothesis,
q9 = queue_280,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f403,negated_conjecture,
elem_283 != e13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f404,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f405,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f406,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f405]) ).
fof(f407,plain,
! [X0,X1] : rselect_seq(rstore_seq(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f408,plain,
! [X0,X1] : rselect_head(rstore_head(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f409,plain,
! [X0,X1] : rselect_tail(rstore_tail(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f410,plain,
! [X0,X1] : rselect_seq(rstore_head(X0,X1)) = rselect_seq(X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f411,plain,
! [X0,X1] : rselect_seq(rstore_tail(X0,X1)) = rselect_seq(X0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f412,plain,
! [X0,X1] : rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f413,plain,
! [X0,X1] : rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f415,plain,
! [X0,X1] : rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f456,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f457,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f458,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f459,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f460,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f461,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f462,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f463,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f464,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f465,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f466,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f467,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f468,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f469,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f470,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f471,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f472,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f473,plain,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f474,plain,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f475,plain,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f476,plain,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f477,plain,
! [X0] : s(s(s(s(s(X0))))) != X0,
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f478,plain,
! [X0] : s(s(s(s(X0)))) != X0,
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f479,plain,
! [X0] : s(s(s(X0))) != X0,
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f480,plain,
! [X0] : s(s(X0)) != X0,
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f481,plain,
! [X0] : s(X0) != X0,
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f483,plain,
earray_100 = store(earray_98,index_99,e21),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f484,plain,
earray_104 = rselect_seq(q22),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f485,plain,
earray_106 = store(earray_104,index_105,e22),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f486,plain,
earray_110 = rselect_seq(q23),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f487,plain,
earray_112 = store(earray_110,index_111,e23),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f488,plain,
earray_119 = rselect_seq(q24),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f489,plain,
earray_121 = store(earray_119,index_120,e24),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f490,plain,
earray_125 = rselect_seq(q25),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f491,plain,
earray_127 = store(earray_125,index_126,e25),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f492,plain,
earray_131 = rselect_seq(q26),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f493,plain,
earray_133 = store(earray_131,index_132,e26),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f495,plain,
earray_140 = rselect_seq(q27),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f496,plain,
earray_142 = store(earray_140,index_141,e27),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f497,plain,
earray_146 = rselect_seq(q28),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f498,plain,
earray_148 = store(earray_146,index_147,e28),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f502,plain,
earray_161 = rselect_seq(q29),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f503,plain,
earray_163 = store(earray_161,index_162,e29),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f504,plain,
earray_170 = rselect_seq(q30),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f505,plain,
earray_172 = store(earray_170,index_171,e30),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f506,plain,
earray_176 = rselect_seq(q31),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f507,plain,
earray_178 = store(earray_176,index_177,e31),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f508,plain,
earray_182 = rselect_seq(q32),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f509,plain,
earray_184 = store(earray_182,index_183,e32),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f510,plain,
earray_191 = rselect_seq(q33),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f511,plain,
earray_193 = store(earray_191,index_192,e33),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f512,plain,
earray_197 = rselect_seq(q34),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f513,plain,
earray_199 = store(earray_197,index_198,e34),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f516,plain,
earray_203 = rselect_seq(q35),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f517,plain,
earray_205 = store(earray_203,index_204,e35),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f518,plain,
earray_212 = rselect_seq(q36),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f519,plain,
earray_214 = store(earray_212,index_213,e36),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f520,plain,
earray_218 = rselect_seq(q37),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f522,plain,
earray_220 = store(earray_218,index_219,e37),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f523,plain,
earray_224 = rselect_seq(q38),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f524,plain,
earray_226 = store(earray_224,index_225,e38),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f527,plain,
earray_239 = rselect_seq(q39),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f528,plain,
earray_241 = store(earray_239,index_240,e39),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f539,plain,
earray_281 = rselect_seq(q40),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f543,plain,
earray_37 = store(earray_35,index_36,e13),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f545,plain,
earray_41 = rselect_seq(q14),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f546,plain,
earray_43 = store(earray_41,index_42,e14),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f547,plain,
earray_50 = rselect_seq(q15),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f548,plain,
earray_52 = store(earray_50,index_51,e15),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f549,plain,
earray_56 = rselect_seq(q16),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f550,plain,
earray_58 = store(earray_56,index_57,e16),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f551,plain,
earray_62 = rselect_seq(q17),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f552,plain,
earray_64 = store(earray_62,index_63,e17),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f553,plain,
earray_71 = rselect_seq(q18),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f554,plain,
earray_73 = store(earray_71,index_72,e18),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f558,plain,
earray_83 = rselect_seq(q19),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f559,plain,
earray_85 = store(earray_83,index_84,e19),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f560,plain,
earray_89 = rselect_seq(q20),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f561,plain,
earray_91 = store(earray_89,index_90,e20),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f562,plain,
earray_98 = rselect_seq(q21),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f563,plain,
elem_283 = select(earray_281,index_282),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f564,plain,
index_0 = rselect_tail(q),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f565,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f566,plain,
index_105 = rselect_tail(q22),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f567,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f568,plain,
index_111 = rselect_tail(q23),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f569,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f570,plain,
index_116 = rselect_head(queue_115),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f571,plain,
index_117 = s(index_116),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f572,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f573,plain,
index_120 = rselect_tail(q24),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f574,plain,
index_123 = s(index_120),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f575,plain,
index_126 = rselect_tail(q25),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f576,plain,
index_129 = s(index_126),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f577,plain,
index_132 = rselect_tail(q26),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f578,plain,
index_135 = s(index_132),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f579,plain,
index_137 = rselect_head(queue_136),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f580,plain,
index_138 = s(index_137),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f581,plain,
index_141 = rselect_tail(q27),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f582,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f583,plain,
index_147 = rselect_tail(q28),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f584,plain,
index_15 = rselect_tail(q10),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f585,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f586,plain,
index_153 = rselect_tail(q2),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f587,plain,
index_156 = s(index_153),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f588,plain,
index_158 = rselect_head(queue_157),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f589,plain,
index_159 = s(index_158),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f590,plain,
index_162 = rselect_tail(q29),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f591,plain,
index_165 = s(index_162),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f592,plain,
index_167 = rselect_head(queue_166),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f593,plain,
index_168 = s(index_167),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f594,plain,
index_171 = rselect_tail(q30),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f595,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f596,plain,
index_177 = rselect_tail(q31),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f597,plain,
index_18 = s(index_15),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f598,plain,
index_180 = s(index_177),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f599,plain,
index_183 = rselect_tail(q32),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f600,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f601,plain,
index_188 = rselect_head(queue_187),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f602,plain,
index_189 = s(index_188),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f603,plain,
index_192 = rselect_tail(q33),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f604,plain,
index_195 = s(index_192),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f605,plain,
index_198 = rselect_tail(q34),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f606,plain,
index_201 = s(index_198),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f607,plain,
index_204 = rselect_tail(q35),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f608,plain,
index_207 = s(index_204),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f609,plain,
index_209 = rselect_head(queue_208),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f610,plain,
index_21 = rselect_tail(q11),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f611,plain,
index_210 = s(index_209),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f612,plain,
index_213 = rselect_tail(q36),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f613,plain,
index_216 = s(index_213),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f614,plain,
index_219 = rselect_tail(q37),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f615,plain,
index_222 = s(index_219),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f616,plain,
index_225 = rselect_tail(q38),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f617,plain,
index_228 = s(index_225),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f618,plain,
index_230 = rselect_head(queue_229),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f619,plain,
index_231 = s(index_230),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f620,plain,
index_234 = rselect_tail(q3),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f621,plain,
index_237 = s(index_234),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f622,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f623,plain,
index_240 = rselect_tail(q39),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f625,plain,
index_246 = rselect_tail(q4),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f626,plain,
index_249 = s(index_246),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f627,plain,
index_252 = rselect_tail(q5),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f628,plain,
index_255 = s(index_252),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f629,plain,
index_257 = rselect_head(queue_256),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f630,plain,
index_258 = s(index_257),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f631,plain,
index_26 = rselect_head(queue_25),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f632,plain,
index_261 = rselect_tail(q6),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f633,plain,
index_264 = s(index_261),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f634,plain,
index_267 = rselect_tail(q7),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f635,plain,
index_27 = s(index_26),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f636,plain,
index_270 = s(index_267),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f637,plain,
index_273 = rselect_tail(q8),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f638,plain,
index_276 = s(index_273),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f639,plain,
index_278 = rselect_head(queue_277),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f640,plain,
index_279 = s(index_278),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f641,plain,
index_282 = rselect_head(q40),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f642,plain,
index_3 = rselect_tail(q0),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f643,plain,
index_30 = rselect_tail(q12),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f644,plain,
index_33 = s(index_30),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f645,plain,
index_36 = rselect_tail(q13),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f646,plain,
index_39 = s(index_36),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f647,plain,
index_42 = rselect_tail(q14),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f648,plain,
index_45 = s(index_42),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f649,plain,
index_47 = rselect_head(queue_46),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f650,plain,
index_48 = s(index_47),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f651,plain,
index_51 = rselect_tail(q15),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f652,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f653,plain,
index_57 = rselect_tail(q16),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f654,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f655,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f656,plain,
index_63 = rselect_tail(q17),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f657,plain,
index_66 = s(index_63),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f658,plain,
index_68 = rselect_head(queue_67),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f659,plain,
index_69 = s(index_68),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f660,plain,
index_72 = rselect_tail(q18),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f661,plain,
index_75 = s(index_72),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f662,plain,
index_78 = rselect_tail(q1),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f663,plain,
index_81 = s(index_78),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f664,plain,
index_84 = rselect_tail(q19),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f665,plain,
index_87 = s(index_84),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f666,plain,
index_9 = rselect_tail(q9),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f667,plain,
index_90 = rselect_tail(q20),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f668,plain,
index_93 = s(index_90),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f669,plain,
index_95 = rselect_head(queue_94),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f670,plain,
index_96 = s(index_95),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f671,plain,
index_99 = rselect_tail(q21),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f672,plain,
queue_1 = rstore_head(q,index_0),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f673,plain,
queue_101 = rstore_seq(q21,earray_100),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f674,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f675,plain,
queue_107 = rstore_seq(q22,earray_106),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f676,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f677,plain,
queue_11 = rstore_seq(q9,earray_10),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f678,plain,
queue_113 = rstore_seq(q23,earray_112),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f679,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f680,plain,
queue_118 = rstore_head(queue_115,index_117),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f681,plain,
queue_122 = rstore_seq(q24,earray_121),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f682,plain,
queue_124 = rstore_tail(queue_122,index_123),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f683,plain,
queue_128 = rstore_seq(q25,earray_127),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f684,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f685,plain,
queue_130 = rstore_tail(queue_128,index_129),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f686,plain,
queue_134 = rstore_seq(q26,earray_133),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f687,plain,
queue_136 = rstore_tail(queue_134,index_135),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f688,plain,
queue_139 = rstore_head(queue_136,index_138),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f689,plain,
queue_143 = rstore_seq(q27,earray_142),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f690,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f691,plain,
queue_149 = rstore_seq(q28,earray_148),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f692,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f693,plain,
queue_155 = rstore_seq(q2,earray_154),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f694,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f695,plain,
queue_160 = rstore_head(queue_157,index_159),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f696,plain,
queue_164 = rstore_seq(q29,earray_163),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f697,plain,
queue_166 = rstore_tail(queue_164,index_165),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f698,plain,
queue_169 = rstore_head(queue_166,index_168),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f699,plain,
queue_17 = rstore_seq(q10,earray_16),
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f700,plain,
queue_173 = rstore_seq(q30,earray_172),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f701,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f702,plain,
queue_179 = rstore_seq(q31,earray_178),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f703,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f704,plain,
queue_185 = rstore_seq(q32,earray_184),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f705,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f706,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f707,plain,
queue_190 = rstore_head(queue_187,index_189),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f708,plain,
queue_194 = rstore_seq(q33,earray_193),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f709,plain,
queue_196 = rstore_tail(queue_194,index_195),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f710,plain,
queue_200 = rstore_seq(q34,earray_199),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f711,plain,
queue_202 = rstore_tail(queue_200,index_201),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f712,plain,
queue_206 = rstore_seq(q35,earray_205),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f713,plain,
queue_208 = rstore_tail(queue_206,index_207),
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f714,plain,
queue_211 = rstore_head(queue_208,index_210),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f715,plain,
queue_215 = rstore_seq(q36,earray_214),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f716,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f717,plain,
queue_221 = rstore_seq(q37,earray_220),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f718,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f719,plain,
queue_227 = rstore_seq(q38,earray_226),
inference(cnf_transformation,[status(thm)],[f315]) ).
fof(f720,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f721,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f722,plain,
queue_232 = rstore_head(queue_229,index_231),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f723,plain,
queue_236 = rstore_seq(q3,earray_235),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f724,plain,
queue_238 = rstore_tail(queue_236,index_237),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f725,plain,
queue_242 = rstore_seq(q39,earray_241),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f726,plain,
queue_244 = rstore_tail(queue_242,index_243),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f727,plain,
queue_248 = rstore_seq(q4,earray_247),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f728,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f729,plain,
queue_250 = rstore_tail(queue_248,index_249),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f730,plain,
queue_254 = rstore_seq(q5,earray_253),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f731,plain,
queue_256 = rstore_tail(queue_254,index_255),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f732,plain,
queue_259 = rstore_head(queue_256,index_258),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f733,plain,
queue_263 = rstore_seq(q6,earray_262),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f734,plain,
queue_265 = rstore_tail(queue_263,index_264),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f735,plain,
queue_269 = rstore_seq(q7,earray_268),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f736,plain,
queue_271 = rstore_tail(queue_269,index_270),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f737,plain,
queue_275 = rstore_seq(q8,earray_274),
inference(cnf_transformation,[status(thm)],[f333]) ).
fof(f738,plain,
queue_277 = rstore_tail(queue_275,index_276),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f739,plain,
queue_28 = rstore_head(queue_25,index_27),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f740,plain,
queue_280 = rstore_head(queue_277,index_279),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f741,plain,
queue_32 = rstore_seq(q12,earray_31),
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f742,plain,
queue_34 = rstore_tail(queue_32,index_33),
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f743,plain,
queue_38 = rstore_seq(q13,earray_37),
inference(cnf_transformation,[status(thm)],[f339]) ).
fof(f744,plain,
queue_40 = rstore_tail(queue_38,index_39),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f745,plain,
queue_44 = rstore_seq(q14,earray_43),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f746,plain,
queue_46 = rstore_tail(queue_44,index_45),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f747,plain,
queue_49 = rstore_head(queue_46,index_48),
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f748,plain,
queue_5 = rstore_seq(q0,earray_4),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f749,plain,
queue_53 = rstore_seq(q15,earray_52),
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f750,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(cnf_transformation,[status(thm)],[f346]) ).
fof(f751,plain,
queue_59 = rstore_seq(q16,earray_58),
inference(cnf_transformation,[status(thm)],[f347]) ).
fof(f752,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f753,plain,
queue_65 = rstore_seq(q17,earray_64),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f754,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f755,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(cnf_transformation,[status(thm)],[f351]) ).
fof(f756,plain,
queue_70 = rstore_head(queue_67,index_69),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f757,plain,
queue_74 = rstore_seq(q18,earray_73),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f758,plain,
queue_76 = rstore_tail(queue_74,index_75),
inference(cnf_transformation,[status(thm)],[f354]) ).
fof(f759,plain,
queue_80 = rstore_seq(q1,earray_79),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f760,plain,
queue_82 = rstore_tail(queue_80,index_81),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f761,plain,
queue_86 = rstore_seq(q19,earray_85),
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f762,plain,
queue_88 = rstore_tail(queue_86,index_87),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f763,plain,
queue_92 = rstore_seq(q20,earray_91),
inference(cnf_transformation,[status(thm)],[f359]) ).
fof(f764,plain,
queue_94 = rstore_tail(queue_92,index_93),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f765,plain,
queue_97 = rstore_head(queue_94,index_96),
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f766,plain,
q0 = queue_1,
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f767,plain,
q1 = queue_7,
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f768,plain,
q10 = queue_13,
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f769,plain,
q11 = queue_19,
inference(cnf_transformation,[status(thm)],[f365]) ).
fof(f770,plain,
q12 = queue_28,
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f771,plain,
q13 = queue_34,
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f772,plain,
q14 = queue_40,
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f773,plain,
q15 = queue_49,
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f774,plain,
q16 = queue_55,
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f775,plain,
q17 = queue_61,
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f776,plain,
q18 = queue_70,
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f777,plain,
q19 = queue_76,
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f778,plain,
q2 = queue_82,
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f779,plain,
q20 = queue_88,
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f780,plain,
q21 = queue_97,
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f781,plain,
q22 = queue_103,
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f782,plain,
q23 = queue_109,
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f783,plain,
q24 = queue_118,
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f784,plain,
q25 = queue_124,
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f785,plain,
q26 = queue_130,
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f786,plain,
q27 = queue_139,
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f787,plain,
q28 = queue_145,
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f788,plain,
q29 = queue_151,
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f789,plain,
q3 = queue_160,
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f790,plain,
q30 = queue_169,
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f791,plain,
q31 = queue_175,
inference(cnf_transformation,[status(thm)],[f387]) ).
fof(f792,plain,
q32 = queue_181,
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f793,plain,
q33 = queue_190,
inference(cnf_transformation,[status(thm)],[f389]) ).
fof(f794,plain,
q34 = queue_196,
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f795,plain,
q35 = queue_202,
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f796,plain,
q36 = queue_211,
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f797,plain,
q37 = queue_217,
inference(cnf_transformation,[status(thm)],[f393]) ).
fof(f798,plain,
q38 = queue_223,
inference(cnf_transformation,[status(thm)],[f394]) ).
fof(f799,plain,
q39 = queue_232,
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f800,plain,
q4 = queue_238,
inference(cnf_transformation,[status(thm)],[f396]) ).
fof(f801,plain,
q40 = queue_244,
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f802,plain,
q5 = queue_250,
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f803,plain,
q6 = queue_259,
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f804,plain,
q7 = queue_265,
inference(cnf_transformation,[status(thm)],[f400]) ).
fof(f805,plain,
q8 = queue_271,
inference(cnf_transformation,[status(thm)],[f401]) ).
fof(f806,plain,
q9 = queue_280,
inference(cnf_transformation,[status(thm)],[f402]) ).
fof(f807,plain,
elem_283 != e13,
inference(cnf_transformation,[status(thm)],[f403]) ).
fof(f808,plain,
select(earray_37,index_36) = e13,
inference(paramodulation,[status(thm)],[f543,f404]) ).
fof(f814,plain,
earray_104 = rselect_seq(queue_103),
inference(forward_demodulation,[status(thm)],[f781,f484]) ).
fof(f815,plain,
earray_110 = rselect_seq(queue_109),
inference(forward_demodulation,[status(thm)],[f782,f486]) ).
fof(f816,plain,
earray_119 = rselect_seq(queue_118),
inference(forward_demodulation,[status(thm)],[f783,f488]) ).
fof(f817,plain,
earray_125 = rselect_seq(queue_124),
inference(forward_demodulation,[status(thm)],[f784,f490]) ).
fof(f818,plain,
earray_131 = rselect_seq(queue_130),
inference(forward_demodulation,[status(thm)],[f785,f492]) ).
fof(f820,plain,
earray_140 = rselect_seq(queue_139),
inference(forward_demodulation,[status(thm)],[f786,f495]) ).
fof(f821,plain,
earray_146 = rselect_seq(queue_145),
inference(forward_demodulation,[status(thm)],[f787,f497]) ).
fof(f823,plain,
earray_161 = rselect_seq(queue_151),
inference(forward_demodulation,[status(thm)],[f788,f502]) ).
fof(f824,plain,
earray_170 = rselect_seq(queue_169),
inference(forward_demodulation,[status(thm)],[f790,f504]) ).
fof(f825,plain,
earray_176 = rselect_seq(queue_175),
inference(forward_demodulation,[status(thm)],[f791,f506]) ).
fof(f826,plain,
earray_182 = rselect_seq(queue_181),
inference(forward_demodulation,[status(thm)],[f792,f508]) ).
fof(f827,plain,
earray_191 = rselect_seq(queue_190),
inference(forward_demodulation,[status(thm)],[f793,f510]) ).
fof(f828,plain,
earray_197 = rselect_seq(queue_196),
inference(forward_demodulation,[status(thm)],[f794,f512]) ).
fof(f831,plain,
earray_203 = rselect_seq(queue_202),
inference(forward_demodulation,[status(thm)],[f795,f516]) ).
fof(f832,plain,
earray_212 = rselect_seq(queue_211),
inference(forward_demodulation,[status(thm)],[f796,f518]) ).
fof(f833,plain,
earray_218 = rselect_seq(queue_217),
inference(forward_demodulation,[status(thm)],[f797,f520]) ).
fof(f834,plain,
earray_224 = rselect_seq(queue_223),
inference(forward_demodulation,[status(thm)],[f798,f523]) ).
fof(f836,plain,
earray_239 = rselect_seq(queue_232),
inference(forward_demodulation,[status(thm)],[f799,f527]) ).
fof(f842,plain,
earray_281 = rselect_seq(queue_244),
inference(forward_demodulation,[status(thm)],[f801,f539]) ).
fof(f845,plain,
earray_41 = rselect_seq(queue_40),
inference(forward_demodulation,[status(thm)],[f772,f545]) ).
fof(f846,plain,
earray_50 = rselect_seq(queue_49),
inference(forward_demodulation,[status(thm)],[f773,f547]) ).
fof(f847,plain,
earray_56 = rselect_seq(queue_55),
inference(forward_demodulation,[status(thm)],[f774,f549]) ).
fof(f848,plain,
earray_62 = rselect_seq(queue_61),
inference(forward_demodulation,[status(thm)],[f775,f551]) ).
fof(f849,plain,
earray_71 = rselect_seq(queue_70),
inference(forward_demodulation,[status(thm)],[f776,f553]) ).
fof(f852,plain,
earray_83 = rselect_seq(queue_76),
inference(forward_demodulation,[status(thm)],[f777,f558]) ).
fof(f853,plain,
earray_89 = rselect_seq(queue_88),
inference(forward_demodulation,[status(thm)],[f779,f560]) ).
fof(f854,plain,
earray_98 = rselect_seq(queue_97),
inference(forward_demodulation,[status(thm)],[f780,f562]) ).
fof(f889,plain,
index_105 = rselect_tail(queue_103),
inference(forward_demodulation,[status(thm)],[f781,f566]) ).
fof(f924,plain,
index_111 = rselect_tail(queue_109),
inference(forward_demodulation,[status(thm)],[f782,f568]) ).
fof(f1047,plain,
index_120 = rselect_tail(queue_118),
inference(forward_demodulation,[status(thm)],[f783,f573]) ).
fof(f1098,plain,
index_126 = rselect_tail(queue_124),
inference(forward_demodulation,[status(thm)],[f784,f575]) ).
fof(f1139,plain,
index_132 = rselect_tail(queue_130),
inference(forward_demodulation,[status(thm)],[f785,f577]) ).
fof(f1256,plain,
index_141 = rselect_tail(queue_139),
inference(forward_demodulation,[status(thm)],[f786,f581]) ).
fof(f1321,plain,
index_147 = rselect_tail(queue_145),
inference(forward_demodulation,[status(thm)],[f787,f583]) ).
fof(f1322,plain,
index_15 = rselect_tail(queue_13),
inference(forward_demodulation,[status(thm)],[f768,f584]) ).
fof(f1402,plain,
index_153 = rselect_tail(queue_82),
inference(forward_demodulation,[status(thm)],[f778,f586]) ).
fof(f1540,plain,
index_162 = rselect_tail(queue_151),
inference(forward_demodulation,[status(thm)],[f788,f590]) ).
fof(f1690,plain,
index_171 = rselect_tail(queue_169),
inference(forward_demodulation,[status(thm)],[f790,f594]) ).
fof(f1762,plain,
index_177 = rselect_tail(queue_175),
inference(forward_demodulation,[status(thm)],[f791,f596]) ).
fof(f1911,plain,
index_183 = rselect_tail(queue_181),
inference(forward_demodulation,[status(thm)],[f792,f599]) ).
fof(f2108,plain,
index_192 = rselect_tail(queue_190),
inference(forward_demodulation,[status(thm)],[f793,f603]) ).
fof(f2171,plain,
index_198 = rselect_tail(queue_196),
inference(forward_demodulation,[status(thm)],[f794,f605]) ).
fof(f2278,plain,
index_204 = rselect_tail(queue_202),
inference(forward_demodulation,[status(thm)],[f795,f607]) ).
fof(f2391,plain,
index_21 = rselect_tail(queue_19),
inference(forward_demodulation,[status(thm)],[f769,f610]) ).
fof(f2458,plain,
! [X0] :
( select(earray_100,X0) = select(earray_98,X0)
| index_99 = X0 ),
inference(paramodulation,[status(thm)],[f483,f406]) ).
fof(f2460,plain,
index_213 = rselect_tail(queue_211),
inference(forward_demodulation,[status(thm)],[f796,f612]) ).
fof(f2527,plain,
! [X0] :
( select(earray_106,X0) = select(earray_104,X0)
| index_105 = X0 ),
inference(paramodulation,[status(thm)],[f485,f406]) ).
fof(f2529,plain,
! [X0] :
( select(earray_112,X0) = select(earray_110,X0)
| index_111 = X0 ),
inference(paramodulation,[status(thm)],[f487,f406]) ).
fof(f2531,plain,
index_219 = rselect_tail(queue_217),
inference(forward_demodulation,[status(thm)],[f797,f614]) ).
fof(f2598,plain,
index_225 = rselect_tail(queue_223),
inference(forward_demodulation,[status(thm)],[f798,f616]) ).
fof(f2665,plain,
! [X0] :
( select(earray_121,X0) = select(earray_119,X0)
| index_120 = X0 ),
inference(paramodulation,[status(thm)],[f489,f406]) ).
fof(f2667,plain,
! [X0] :
( select(earray_127,X0) = select(earray_125,X0)
| index_126 = X0 ),
inference(paramodulation,[status(thm)],[f491,f406]) ).
fof(f2669,plain,
! [X0] :
( select(earray_133,X0) = select(earray_131,X0)
| index_132 = X0 ),
inference(paramodulation,[status(thm)],[f493,f406]) ).
fof(f2737,plain,
! [X0] :
( select(earray_142,X0) = select(earray_140,X0)
| index_141 = X0 ),
inference(paramodulation,[status(thm)],[f496,f406]) ).
fof(f2739,plain,
index_234 = rselect_tail(queue_160),
inference(forward_demodulation,[status(thm)],[f789,f620]) ).
fof(f2806,plain,
! [X0] :
( select(earray_148,X0) = select(earray_146,X0)
| index_147 = X0 ),
inference(paramodulation,[status(thm)],[f498,f406]) ).
fof(f2876,plain,
index_240 = rselect_tail(queue_232),
inference(forward_demodulation,[status(thm)],[f799,f623]) ).
fof(f2943,plain,
index_246 = rselect_tail(queue_238),
inference(forward_demodulation,[status(thm)],[f800,f625]) ).
fof(f2946,plain,
! [X0] :
( select(earray_163,X0) = select(earray_161,X0)
| index_162 = X0 ),
inference(paramodulation,[status(thm)],[f503,f406]) ).
fof(f2948,plain,
! [X0] :
( select(earray_172,X0) = select(earray_170,X0)
| index_171 = X0 ),
inference(paramodulation,[status(thm)],[f505,f406]) ).
fof(f3016,plain,
! [X0] :
( select(earray_178,X0) = select(earray_176,X0)
| index_177 = X0 ),
inference(paramodulation,[status(thm)],[f507,f406]) ).
fof(f3018,plain,
index_252 = rselect_tail(queue_250),
inference(forward_demodulation,[status(thm)],[f802,f627]) ).
fof(f3085,plain,
! [X0] :
( select(earray_184,X0) = select(earray_182,X0)
| index_183 = X0 ),
inference(paramodulation,[status(thm)],[f509,f406]) ).
fof(f3087,plain,
! [X0] :
( select(earray_193,X0) = select(earray_191,X0)
| index_192 = X0 ),
inference(paramodulation,[status(thm)],[f511,f406]) ).
fof(f3155,plain,
index_261 = rselect_tail(queue_259),
inference(forward_demodulation,[status(thm)],[f803,f632]) ).
fof(f3222,plain,
! [X0] :
( select(earray_199,X0) = select(earray_197,X0)
| index_198 = X0 ),
inference(paramodulation,[status(thm)],[f513,f406]) ).
fof(f3224,plain,
! [X0] :
( select(earray_205,X0) = select(earray_203,X0)
| index_204 = X0 ),
inference(paramodulation,[status(thm)],[f517,f406]) ).
fof(f3226,plain,
! [X0] :
( select(earray_214,X0) = select(earray_212,X0)
| index_213 = X0 ),
inference(paramodulation,[status(thm)],[f519,f406]) ).
fof(f3228,plain,
index_267 = rselect_tail(queue_265),
inference(forward_demodulation,[status(thm)],[f804,f634]) ).
fof(f3363,plain,
index_273 = rselect_tail(queue_271),
inference(forward_demodulation,[status(thm)],[f805,f637]) ).
fof(f3364,plain,
! [X0] :
( select(earray_220,X0) = select(earray_218,X0)
| index_219 = X0 ),
inference(paramodulation,[status(thm)],[f522,f406]) ).
fof(f3366,plain,
! [X0] :
( select(earray_226,X0) = select(earray_224,X0)
| index_225 = X0 ),
inference(paramodulation,[status(thm)],[f524,f406]) ).
fof(f3500,plain,
index_282 = rselect_head(queue_244),
inference(forward_demodulation,[status(thm)],[f801,f641]) ).
fof(f3503,plain,
! [X0] :
( select(earray_241,X0) = select(earray_239,X0)
| index_240 = X0 ),
inference(paramodulation,[status(thm)],[f528,f406]) ).
fof(f3507,plain,
index_3 = rselect_tail(queue_1),
inference(forward_demodulation,[status(thm)],[f766,f642]) ).
fof(f3508,plain,
index_30 = rselect_tail(queue_28),
inference(forward_demodulation,[status(thm)],[f770,f643]) ).
fof(f3577,plain,
index_36 = rselect_tail(queue_34),
inference(forward_demodulation,[status(thm)],[f771,f645]) ).
fof(f3578,plain,
s(s(index_39)) != index_36,
inference(paramodulation,[status(thm)],[f646,f479]) ).
fof(f3634,plain,
s(index_39) != index_36,
inference(paramodulation,[status(thm)],[f646,f480]) ).
fof(f3643,plain,
index_39 != index_36,
inference(paramodulation,[status(thm)],[f646,f481]) ).
fof(f3648,plain,
index_42 = rselect_tail(queue_40),
inference(forward_demodulation,[status(thm)],[f772,f647]) ).
fof(f3787,plain,
index_51 = rselect_tail(queue_49),
inference(forward_demodulation,[status(thm)],[f773,f651]) ).
fof(f3788,plain,
! [X0] :
( select(earray_43,X0) = select(earray_41,X0)
| index_42 = X0 ),
inference(paramodulation,[status(thm)],[f546,f406]) ).
fof(f3856,plain,
index_57 = rselect_tail(queue_55),
inference(forward_demodulation,[status(thm)],[f774,f653]) ).
fof(f3923,plain,
! [X0] :
( select(earray_52,X0) = select(earray_50,X0)
| index_51 = X0 ),
inference(paramodulation,[status(thm)],[f548,f406]) ).
fof(f3925,plain,
! [X0] :
( select(earray_58,X0) = select(earray_56,X0)
| index_57 = X0 ),
inference(paramodulation,[status(thm)],[f550,f406]) ).
fof(f3993,plain,
index_63 = rselect_tail(queue_61),
inference(forward_demodulation,[status(thm)],[f775,f656]) ).
fof(f4060,plain,
! [X0] :
( select(earray_64,X0) = select(earray_62,X0)
| index_63 = X0 ),
inference(paramodulation,[status(thm)],[f552,f406]) ).
fof(f4062,plain,
! [X0] :
( select(earray_73,X0) = select(earray_71,X0)
| index_72 = X0 ),
inference(paramodulation,[status(thm)],[f554,f406]) ).
fof(f4132,plain,
! [X0] :
( select(earray_85,X0) = select(earray_83,X0)
| index_84 = X0 ),
inference(paramodulation,[status(thm)],[f559,f406]) ).
fof(f4134,plain,
index_72 = rselect_tail(queue_70),
inference(forward_demodulation,[status(thm)],[f776,f660]) ).
fof(f4201,plain,
! [X0] :
( select(earray_91,X0) = select(earray_89,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f561,f406]) ).
fof(f4203,plain,
index_78 = rselect_tail(queue_7),
inference(forward_demodulation,[status(thm)],[f767,f662]) ).
fof(f4270,plain,
index_84 = rselect_tail(queue_76),
inference(forward_demodulation,[status(thm)],[f777,f664]) ).
fof(f4337,plain,
index_9 = rselect_tail(queue_280),
inference(forward_demodulation,[status(thm)],[f806,f666]) ).
fof(f4338,plain,
index_90 = rselect_tail(queue_88),
inference(forward_demodulation,[status(thm)],[f779,f667]) ).
fof(f4471,plain,
index_99 = rselect_tail(queue_97),
inference(forward_demodulation,[status(thm)],[f780,f671]) ).
fof(f4472,plain,
rselect_tail(queue_1) = rselect_tail(q),
inference(paramodulation,[status(thm)],[f672,f415]) ).
fof(f4474,plain,
rselect_head(queue_1) = index_0,
inference(paramodulation,[status(thm)],[f672,f408]) ).
fof(f4475,plain,
index_3 = rselect_tail(q),
inference(forward_demodulation,[status(thm)],[f3507,f4472]) ).
fof(f4476,plain,
index_3 = index_0,
inference(forward_demodulation,[status(thm)],[f564,f4475]) ).
fof(f4478,plain,
queue_101 = rstore_seq(queue_97,earray_100),
inference(forward_demodulation,[status(thm)],[f780,f673]) ).
fof(f4480,plain,
rselect_head(queue_101) = rselect_head(queue_97),
inference(paramodulation,[status(thm)],[f4478,f413]) ).
fof(f4481,plain,
rselect_seq(queue_101) = earray_100,
inference(paramodulation,[status(thm)],[f4478,f407]) ).
fof(f4484,plain,
index_6 = s(index_0),
inference(backward_demodulation,[status(thm)],[f4476,f654]) ).
fof(f4487,plain,
rselect_head(queue_103) = rselect_head(queue_101),
inference(paramodulation,[status(thm)],[f674,f412]) ).
fof(f4488,plain,
rselect_seq(queue_103) = rselect_seq(queue_101),
inference(paramodulation,[status(thm)],[f674,f411]) ).
fof(f4489,plain,
rselect_tail(queue_103) = index_102,
inference(paramodulation,[status(thm)],[f674,f409]) ).
fof(f4490,plain,
earray_104 = rselect_seq(queue_101),
inference(forward_demodulation,[status(thm)],[f814,f4488]) ).
fof(f4491,plain,
index_105 = index_102,
inference(forward_demodulation,[status(thm)],[f889,f4489]) ).
fof(f4492,plain,
queue_107 = rstore_seq(queue_103,earray_106),
inference(forward_demodulation,[status(thm)],[f781,f675]) ).
fof(f4494,plain,
rselect_head(queue_107) = rselect_head(queue_103),
inference(paramodulation,[status(thm)],[f4492,f413]) ).
fof(f4495,plain,
rselect_seq(queue_107) = earray_106,
inference(paramodulation,[status(thm)],[f4492,f407]) ).
fof(f4497,plain,
rselect_head(queue_109) = rselect_head(queue_107),
inference(paramodulation,[status(thm)],[f676,f412]) ).
fof(f4498,plain,
rselect_seq(queue_109) = rselect_seq(queue_107),
inference(paramodulation,[status(thm)],[f676,f411]) ).
fof(f4499,plain,
rselect_tail(queue_109) = index_108,
inference(paramodulation,[status(thm)],[f676,f409]) ).
fof(f4500,plain,
earray_110 = rselect_seq(queue_107),
inference(forward_demodulation,[status(thm)],[f815,f4498]) ).
fof(f4501,plain,
index_111 = index_108,
inference(forward_demodulation,[status(thm)],[f924,f4499]) ).
fof(f4505,plain,
index_108 = s(index_102),
inference(backward_demodulation,[status(thm)],[f4491,f567]) ).
fof(f4510,plain,
index_114 = s(index_108),
inference(backward_demodulation,[status(thm)],[f4501,f569]) ).
fof(f4512,plain,
queue_11 = rstore_seq(queue_280,earray_10),
inference(forward_demodulation,[status(thm)],[f806,f677]) ).
fof(f4514,plain,
rselect_head(queue_11) = rselect_head(queue_280),
inference(paramodulation,[status(thm)],[f4512,f413]) ).
fof(f4517,plain,
queue_113 = rstore_seq(queue_109,earray_112),
inference(forward_demodulation,[status(thm)],[f782,f678]) ).
fof(f4519,plain,
rselect_head(queue_113) = rselect_head(queue_109),
inference(paramodulation,[status(thm)],[f4517,f413]) ).
fof(f4520,plain,
rselect_seq(queue_113) = earray_112,
inference(paramodulation,[status(thm)],[f4517,f407]) ).
fof(f4521,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(paramodulation,[status(thm)],[f679,f412]) ).
fof(f4522,plain,
rselect_seq(queue_115) = rselect_seq(queue_113),
inference(paramodulation,[status(thm)],[f679,f411]) ).
fof(f4523,plain,
rselect_tail(queue_115) = index_114,
inference(paramodulation,[status(thm)],[f679,f409]) ).
fof(f4524,plain,
index_116 = rselect_head(queue_113),
inference(forward_demodulation,[status(thm)],[f570,f4521]) ).
fof(f4525,plain,
rselect_tail(queue_118) = rselect_tail(queue_115),
inference(paramodulation,[status(thm)],[f680,f415]) ).
fof(f4526,plain,
rselect_seq(queue_118) = rselect_seq(queue_115),
inference(paramodulation,[status(thm)],[f680,f410]) ).
fof(f4527,plain,
rselect_head(queue_118) = index_117,
inference(paramodulation,[status(thm)],[f680,f408]) ).
fof(f4528,plain,
index_120 = rselect_tail(queue_115),
inference(forward_demodulation,[status(thm)],[f1047,f4525]) ).
fof(f4529,plain,
earray_119 = rselect_seq(queue_115),
inference(forward_demodulation,[status(thm)],[f816,f4526]) ).
fof(f4530,plain,
queue_122 = rstore_seq(queue_118,earray_121),
inference(forward_demodulation,[status(thm)],[f783,f681]) ).
fof(f4532,plain,
rselect_head(queue_122) = rselect_head(queue_118),
inference(paramodulation,[status(thm)],[f4530,f413]) ).
fof(f4533,plain,
rselect_seq(queue_122) = earray_121,
inference(paramodulation,[status(thm)],[f4530,f407]) ).
fof(f4535,plain,
rselect_head(queue_124) = rselect_head(queue_122),
inference(paramodulation,[status(thm)],[f682,f412]) ).
fof(f4536,plain,
rselect_seq(queue_124) = rselect_seq(queue_122),
inference(paramodulation,[status(thm)],[f682,f411]) ).
fof(f4537,plain,
rselect_tail(queue_124) = index_123,
inference(paramodulation,[status(thm)],[f682,f409]) ).
fof(f4538,plain,
earray_125 = rselect_seq(queue_122),
inference(forward_demodulation,[status(thm)],[f817,f4536]) ).
fof(f4539,plain,
index_126 = index_123,
inference(forward_demodulation,[status(thm)],[f1098,f4537]) ).
fof(f4543,plain,
index_129 = s(index_123),
inference(backward_demodulation,[status(thm)],[f4539,f576]) ).
fof(f4545,plain,
queue_128 = rstore_seq(queue_124,earray_127),
inference(forward_demodulation,[status(thm)],[f784,f683]) ).
fof(f4547,plain,
rselect_head(queue_128) = rselect_head(queue_124),
inference(paramodulation,[status(thm)],[f4545,f413]) ).
fof(f4548,plain,
rselect_seq(queue_128) = earray_127,
inference(paramodulation,[status(thm)],[f4545,f407]) ).
fof(f4549,plain,
rselect_head(queue_13) = rselect_head(queue_11),
inference(paramodulation,[status(thm)],[f684,f412]) ).
fof(f4551,plain,
rselect_tail(queue_13) = index_12,
inference(paramodulation,[status(thm)],[f684,f409]) ).
fof(f4553,plain,
index_15 = index_12,
inference(forward_demodulation,[status(thm)],[f1322,f4551]) ).
fof(f4554,plain,
rselect_head(queue_130) = rselect_head(queue_128),
inference(paramodulation,[status(thm)],[f685,f412]) ).
fof(f4555,plain,
rselect_seq(queue_130) = rselect_seq(queue_128),
inference(paramodulation,[status(thm)],[f685,f411]) ).
fof(f4556,plain,
rselect_tail(queue_130) = index_129,
inference(paramodulation,[status(thm)],[f685,f409]) ).
fof(f4557,plain,
earray_131 = rselect_seq(queue_128),
inference(forward_demodulation,[status(thm)],[f818,f4555]) ).
fof(f4558,plain,
index_132 = index_129,
inference(forward_demodulation,[status(thm)],[f1139,f4556]) ).
fof(f4562,plain,
index_18 = s(index_12),
inference(backward_demodulation,[status(thm)],[f4553,f597]) ).
fof(f4567,plain,
index_135 = s(index_129),
inference(backward_demodulation,[status(thm)],[f4558,f578]) ).
fof(f4569,plain,
queue_134 = rstore_seq(queue_130,earray_133),
inference(forward_demodulation,[status(thm)],[f785,f686]) ).
fof(f4571,plain,
rselect_head(queue_134) = rselect_head(queue_130),
inference(paramodulation,[status(thm)],[f4569,f413]) ).
fof(f4572,plain,
rselect_seq(queue_134) = earray_133,
inference(paramodulation,[status(thm)],[f4569,f407]) ).
fof(f4573,plain,
rselect_head(queue_136) = rselect_head(queue_134),
inference(paramodulation,[status(thm)],[f687,f412]) ).
fof(f4574,plain,
rselect_seq(queue_136) = rselect_seq(queue_134),
inference(paramodulation,[status(thm)],[f687,f411]) ).
fof(f4575,plain,
rselect_tail(queue_136) = index_135,
inference(paramodulation,[status(thm)],[f687,f409]) ).
fof(f4576,plain,
index_137 = rselect_head(queue_134),
inference(forward_demodulation,[status(thm)],[f579,f4573]) ).
fof(f4577,plain,
rselect_tail(queue_139) = rselect_tail(queue_136),
inference(paramodulation,[status(thm)],[f688,f415]) ).
fof(f4578,plain,
rselect_seq(queue_139) = rselect_seq(queue_136),
inference(paramodulation,[status(thm)],[f688,f410]) ).
fof(f4579,plain,
rselect_head(queue_139) = index_138,
inference(paramodulation,[status(thm)],[f688,f408]) ).
fof(f4580,plain,
index_141 = rselect_tail(queue_136),
inference(forward_demodulation,[status(thm)],[f1256,f4577]) ).
fof(f4581,plain,
earray_140 = rselect_seq(queue_136),
inference(forward_demodulation,[status(thm)],[f820,f4578]) ).
fof(f4582,plain,
queue_143 = rstore_seq(queue_139,earray_142),
inference(forward_demodulation,[status(thm)],[f786,f689]) ).
fof(f4584,plain,
rselect_head(queue_143) = rselect_head(queue_139),
inference(paramodulation,[status(thm)],[f4582,f413]) ).
fof(f4585,plain,
rselect_seq(queue_143) = earray_142,
inference(paramodulation,[status(thm)],[f4582,f407]) ).
fof(f4587,plain,
rselect_head(queue_145) = rselect_head(queue_143),
inference(paramodulation,[status(thm)],[f690,f412]) ).
fof(f4588,plain,
rselect_seq(queue_145) = rselect_seq(queue_143),
inference(paramodulation,[status(thm)],[f690,f411]) ).
fof(f4589,plain,
rselect_tail(queue_145) = index_144,
inference(paramodulation,[status(thm)],[f690,f409]) ).
fof(f4590,plain,
earray_146 = rselect_seq(queue_143),
inference(forward_demodulation,[status(thm)],[f821,f4588]) ).
fof(f4591,plain,
index_147 = index_144,
inference(forward_demodulation,[status(thm)],[f1321,f4589]) ).
fof(f4592,plain,
queue_149 = rstore_seq(queue_145,earray_148),
inference(forward_demodulation,[status(thm)],[f787,f691]) ).
fof(f4594,plain,
rselect_head(queue_149) = rselect_head(queue_145),
inference(paramodulation,[status(thm)],[f4592,f413]) ).
fof(f4595,plain,
rselect_seq(queue_149) = earray_148,
inference(paramodulation,[status(thm)],[f4592,f407]) ).
fof(f4600,plain,
index_150 = s(index_144),
inference(backward_demodulation,[status(thm)],[f4591,f585]) ).
fof(f4602,plain,
rselect_head(queue_151) = rselect_head(queue_149),
inference(paramodulation,[status(thm)],[f692,f412]) ).
fof(f4603,plain,
rselect_seq(queue_151) = rselect_seq(queue_149),
inference(paramodulation,[status(thm)],[f692,f411]) ).
fof(f4604,plain,
rselect_tail(queue_151) = index_150,
inference(paramodulation,[status(thm)],[f692,f409]) ).
fof(f4605,plain,
earray_161 = rselect_seq(queue_149),
inference(forward_demodulation,[status(thm)],[f823,f4603]) ).
fof(f4606,plain,
index_162 = index_150,
inference(forward_demodulation,[status(thm)],[f1540,f4604]) ).
fof(f4607,plain,
queue_155 = rstore_seq(queue_82,earray_154),
inference(forward_demodulation,[status(thm)],[f778,f693]) ).
fof(f4609,plain,
rselect_head(queue_155) = rselect_head(queue_82),
inference(paramodulation,[status(thm)],[f4607,f413]) ).
fof(f4612,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(paramodulation,[status(thm)],[f694,f412]) ).
fof(f4614,plain,
rselect_tail(queue_157) = index_156,
inference(paramodulation,[status(thm)],[f694,f409]) ).
fof(f4615,plain,
index_158 = rselect_head(queue_155),
inference(forward_demodulation,[status(thm)],[f588,f4612]) ).
fof(f4619,plain,
index_165 = s(index_150),
inference(backward_demodulation,[status(thm)],[f4606,f591]) ).
fof(f4621,plain,
rselect_tail(queue_160) = rselect_tail(queue_157),
inference(paramodulation,[status(thm)],[f695,f415]) ).
fof(f4623,plain,
rselect_head(queue_160) = index_159,
inference(paramodulation,[status(thm)],[f695,f408]) ).
fof(f4624,plain,
index_234 = rselect_tail(queue_157),
inference(forward_demodulation,[status(thm)],[f2739,f4621]) ).
fof(f4626,plain,
queue_164 = rstore_seq(queue_151,earray_163),
inference(forward_demodulation,[status(thm)],[f788,f696]) ).
fof(f4628,plain,
rselect_head(queue_164) = rselect_head(queue_151),
inference(paramodulation,[status(thm)],[f4626,f413]) ).
fof(f4629,plain,
rselect_seq(queue_164) = earray_163,
inference(paramodulation,[status(thm)],[f4626,f407]) ).
fof(f4630,plain,
rselect_head(queue_166) = rselect_head(queue_164),
inference(paramodulation,[status(thm)],[f697,f412]) ).
fof(f4631,plain,
rselect_seq(queue_166) = rselect_seq(queue_164),
inference(paramodulation,[status(thm)],[f697,f411]) ).
fof(f4632,plain,
rselect_tail(queue_166) = index_165,
inference(paramodulation,[status(thm)],[f697,f409]) ).
fof(f4633,plain,
index_167 = rselect_head(queue_164),
inference(forward_demodulation,[status(thm)],[f592,f4630]) ).
fof(f4634,plain,
rselect_tail(queue_169) = rselect_tail(queue_166),
inference(paramodulation,[status(thm)],[f698,f415]) ).
fof(f4635,plain,
rselect_seq(queue_169) = rselect_seq(queue_166),
inference(paramodulation,[status(thm)],[f698,f410]) ).
fof(f4636,plain,
rselect_head(queue_169) = index_168,
inference(paramodulation,[status(thm)],[f698,f408]) ).
fof(f4637,plain,
index_171 = rselect_tail(queue_166),
inference(forward_demodulation,[status(thm)],[f1690,f4634]) ).
fof(f4638,plain,
earray_170 = rselect_seq(queue_166),
inference(forward_demodulation,[status(thm)],[f824,f4635]) ).
fof(f4639,plain,
queue_17 = rstore_seq(queue_13,earray_16),
inference(forward_demodulation,[status(thm)],[f768,f699]) ).
fof(f4641,plain,
rselect_head(queue_17) = rselect_head(queue_13),
inference(paramodulation,[status(thm)],[f4639,f413]) ).
fof(f4643,plain,
queue_173 = rstore_seq(queue_169,earray_172),
inference(forward_demodulation,[status(thm)],[f790,f700]) ).
fof(f4645,plain,
rselect_head(queue_173) = rselect_head(queue_169),
inference(paramodulation,[status(thm)],[f4643,f413]) ).
fof(f4646,plain,
rselect_seq(queue_173) = earray_172,
inference(paramodulation,[status(thm)],[f4643,f407]) ).
fof(f4648,plain,
rselect_head(queue_175) = rselect_head(queue_173),
inference(paramodulation,[status(thm)],[f701,f412]) ).
fof(f4649,plain,
rselect_seq(queue_175) = rselect_seq(queue_173),
inference(paramodulation,[status(thm)],[f701,f411]) ).
fof(f4650,plain,
rselect_tail(queue_175) = index_174,
inference(paramodulation,[status(thm)],[f701,f409]) ).
fof(f4651,plain,
earray_176 = rselect_seq(queue_173),
inference(forward_demodulation,[status(thm)],[f825,f4649]) ).
fof(f4652,plain,
index_177 = index_174,
inference(forward_demodulation,[status(thm)],[f1762,f4650]) ).
fof(f4656,plain,
index_180 = s(index_174),
inference(backward_demodulation,[status(thm)],[f4652,f598]) ).
fof(f4659,plain,
queue_179 = rstore_seq(queue_175,earray_178),
inference(forward_demodulation,[status(thm)],[f791,f702]) ).
fof(f4661,plain,
rselect_head(queue_179) = rselect_head(queue_175),
inference(paramodulation,[status(thm)],[f4659,f413]) ).
fof(f4662,plain,
rselect_seq(queue_179) = earray_178,
inference(paramodulation,[status(thm)],[f4659,f407]) ).
fof(f4663,plain,
rselect_head(queue_181) = rselect_head(queue_179),
inference(paramodulation,[status(thm)],[f703,f412]) ).
fof(f4664,plain,
rselect_seq(queue_181) = rselect_seq(queue_179),
inference(paramodulation,[status(thm)],[f703,f411]) ).
fof(f4665,plain,
rselect_tail(queue_181) = index_180,
inference(paramodulation,[status(thm)],[f703,f409]) ).
fof(f4666,plain,
earray_182 = rselect_seq(queue_179),
inference(forward_demodulation,[status(thm)],[f826,f4664]) ).
fof(f4667,plain,
index_183 = index_180,
inference(forward_demodulation,[status(thm)],[f1911,f4665]) ).
fof(f4671,plain,
index_186 = s(index_180),
inference(backward_demodulation,[status(thm)],[f4667,f600]) ).
fof(f4673,plain,
queue_185 = rstore_seq(queue_181,earray_184),
inference(forward_demodulation,[status(thm)],[f792,f704]) ).
fof(f4675,plain,
rselect_head(queue_185) = rselect_head(queue_181),
inference(paramodulation,[status(thm)],[f4673,f413]) ).
fof(f4676,plain,
rselect_seq(queue_185) = earray_184,
inference(paramodulation,[status(thm)],[f4673,f407]) ).
fof(f4677,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(paramodulation,[status(thm)],[f705,f412]) ).
fof(f4678,plain,
rselect_seq(queue_187) = rselect_seq(queue_185),
inference(paramodulation,[status(thm)],[f705,f411]) ).
fof(f4679,plain,
rselect_tail(queue_187) = index_186,
inference(paramodulation,[status(thm)],[f705,f409]) ).
fof(f4680,plain,
index_188 = rselect_head(queue_185),
inference(forward_demodulation,[status(thm)],[f601,f4677]) ).
fof(f4681,plain,
rselect_head(queue_19) = rselect_head(queue_17),
inference(paramodulation,[status(thm)],[f706,f412]) ).
fof(f4683,plain,
rselect_tail(queue_19) = index_18,
inference(paramodulation,[status(thm)],[f706,f409]) ).
fof(f4685,plain,
index_21 = index_18,
inference(forward_demodulation,[status(thm)],[f2391,f4683]) ).
fof(f4689,plain,
index_24 = s(index_18),
inference(backward_demodulation,[status(thm)],[f4685,f622]) ).
fof(f4691,plain,
rselect_tail(queue_190) = rselect_tail(queue_187),
inference(paramodulation,[status(thm)],[f707,f415]) ).
fof(f4692,plain,
rselect_seq(queue_190) = rselect_seq(queue_187),
inference(paramodulation,[status(thm)],[f707,f410]) ).
fof(f4693,plain,
rselect_head(queue_190) = index_189,
inference(paramodulation,[status(thm)],[f707,f408]) ).
fof(f4694,plain,
index_192 = rselect_tail(queue_187),
inference(forward_demodulation,[status(thm)],[f2108,f4691]) ).
fof(f4695,plain,
earray_191 = rselect_seq(queue_187),
inference(forward_demodulation,[status(thm)],[f827,f4692]) ).
fof(f4696,plain,
queue_194 = rstore_seq(queue_190,earray_193),
inference(forward_demodulation,[status(thm)],[f793,f708]) ).
fof(f4698,plain,
rselect_head(queue_194) = rselect_head(queue_190),
inference(paramodulation,[status(thm)],[f4696,f413]) ).
fof(f4699,plain,
rselect_seq(queue_194) = earray_193,
inference(paramodulation,[status(thm)],[f4696,f407]) ).
fof(f4701,plain,
rselect_head(queue_196) = rselect_head(queue_194),
inference(paramodulation,[status(thm)],[f709,f412]) ).
fof(f4702,plain,
rselect_seq(queue_196) = rselect_seq(queue_194),
inference(paramodulation,[status(thm)],[f709,f411]) ).
fof(f4703,plain,
rselect_tail(queue_196) = index_195,
inference(paramodulation,[status(thm)],[f709,f409]) ).
fof(f4704,plain,
earray_197 = rselect_seq(queue_194),
inference(forward_demodulation,[status(thm)],[f828,f4702]) ).
fof(f4705,plain,
index_198 = index_195,
inference(forward_demodulation,[status(thm)],[f2171,f4703]) ).
fof(f4709,plain,
index_201 = s(index_195),
inference(backward_demodulation,[status(thm)],[f4705,f606]) ).
fof(f4711,plain,
queue_200 = rstore_seq(queue_196,earray_199),
inference(forward_demodulation,[status(thm)],[f794,f710]) ).
fof(f4713,plain,
rselect_head(queue_200) = rselect_head(queue_196),
inference(paramodulation,[status(thm)],[f4711,f413]) ).
fof(f4714,plain,
rselect_seq(queue_200) = earray_199,
inference(paramodulation,[status(thm)],[f4711,f407]) ).
fof(f4715,plain,
rselect_head(queue_202) = rselect_head(queue_200),
inference(paramodulation,[status(thm)],[f711,f412]) ).
fof(f4716,plain,
rselect_seq(queue_202) = rselect_seq(queue_200),
inference(paramodulation,[status(thm)],[f711,f411]) ).
fof(f4717,plain,
rselect_tail(queue_202) = index_201,
inference(paramodulation,[status(thm)],[f711,f409]) ).
fof(f4718,plain,
earray_203 = rselect_seq(queue_200),
inference(forward_demodulation,[status(thm)],[f831,f4716]) ).
fof(f4719,plain,
index_204 = index_201,
inference(forward_demodulation,[status(thm)],[f2278,f4717]) ).
fof(f4720,plain,
queue_206 = rstore_seq(queue_202,earray_205),
inference(forward_demodulation,[status(thm)],[f795,f712]) ).
fof(f4722,plain,
rselect_head(queue_206) = rselect_head(queue_202),
inference(paramodulation,[status(thm)],[f4720,f413]) ).
fof(f4723,plain,
rselect_seq(queue_206) = earray_205,
inference(paramodulation,[status(thm)],[f4720,f407]) ).
fof(f4728,plain,
index_207 = s(index_201),
inference(backward_demodulation,[status(thm)],[f4719,f608]) ).
fof(f4730,plain,
rselect_head(queue_208) = rselect_head(queue_206),
inference(paramodulation,[status(thm)],[f713,f412]) ).
fof(f4731,plain,
rselect_seq(queue_208) = rselect_seq(queue_206),
inference(paramodulation,[status(thm)],[f713,f411]) ).
fof(f4732,plain,
rselect_tail(queue_208) = index_207,
inference(paramodulation,[status(thm)],[f713,f409]) ).
fof(f4733,plain,
index_209 = rselect_head(queue_206),
inference(forward_demodulation,[status(thm)],[f609,f4730]) ).
fof(f4801,plain,
earray_104 = earray_100,
inference(forward_demodulation,[status(thm)],[f4481,f4490]) ).
fof(f4803,plain,
rselect_tail(queue_211) = rselect_tail(queue_208),
inference(paramodulation,[status(thm)],[f714,f415]) ).
fof(f4804,plain,
rselect_seq(queue_211) = rselect_seq(queue_208),
inference(paramodulation,[status(thm)],[f714,f410]) ).
fof(f4805,plain,
rselect_head(queue_211) = index_210,
inference(paramodulation,[status(thm)],[f714,f408]) ).
fof(f4806,plain,
index_213 = rselect_tail(queue_208),
inference(forward_demodulation,[status(thm)],[f2460,f4803]) ).
fof(f4807,plain,
earray_212 = rselect_seq(queue_208),
inference(forward_demodulation,[status(thm)],[f832,f4804]) ).
fof(f4808,plain,
queue_215 = rstore_seq(queue_211,earray_214),
inference(forward_demodulation,[status(thm)],[f796,f715]) ).
fof(f4810,plain,
rselect_head(queue_215) = rselect_head(queue_211),
inference(paramodulation,[status(thm)],[f4808,f413]) ).
fof(f4811,plain,
rselect_seq(queue_215) = earray_214,
inference(paramodulation,[status(thm)],[f4808,f407]) ).
fof(f4814,plain,
earray_110 = earray_106,
inference(forward_demodulation,[status(thm)],[f4495,f4500]) ).
fof(f4882,plain,
rselect_head(queue_217) = rselect_head(queue_215),
inference(paramodulation,[status(thm)],[f716,f412]) ).
fof(f4883,plain,
rselect_seq(queue_217) = rselect_seq(queue_215),
inference(paramodulation,[status(thm)],[f716,f411]) ).
fof(f4884,plain,
rselect_tail(queue_217) = index_216,
inference(paramodulation,[status(thm)],[f716,f409]) ).
fof(f4885,plain,
earray_218 = rselect_seq(queue_215),
inference(forward_demodulation,[status(thm)],[f833,f4883]) ).
fof(f4886,plain,
index_219 = index_216,
inference(forward_demodulation,[status(thm)],[f2531,f4884]) ).
fof(f4887,plain,
queue_221 = rstore_seq(queue_217,earray_220),
inference(forward_demodulation,[status(thm)],[f797,f717]) ).
fof(f4889,plain,
rselect_head(queue_221) = rselect_head(queue_217),
inference(paramodulation,[status(thm)],[f4887,f413]) ).
fof(f4890,plain,
rselect_seq(queue_221) = earray_220,
inference(paramodulation,[status(thm)],[f4887,f407]) ).
fof(f4892,plain,
rselect_head(queue_223) = rselect_head(queue_221),
inference(paramodulation,[status(thm)],[f718,f412]) ).
fof(f4893,plain,
rselect_seq(queue_223) = rselect_seq(queue_221),
inference(paramodulation,[status(thm)],[f718,f411]) ).
fof(f4894,plain,
rselect_tail(queue_223) = index_222,
inference(paramodulation,[status(thm)],[f718,f409]) ).
fof(f4895,plain,
earray_224 = rselect_seq(queue_221),
inference(forward_demodulation,[status(thm)],[f834,f4893]) ).
fof(f4896,plain,
index_225 = index_222,
inference(forward_demodulation,[status(thm)],[f2598,f4894]) ).
fof(f4900,plain,
index_222 = s(index_216),
inference(backward_demodulation,[status(thm)],[f4886,f615]) ).
fof(f4905,plain,
index_228 = s(index_222),
inference(backward_demodulation,[status(thm)],[f4896,f617]) ).
fof(f4907,plain,
queue_227 = rstore_seq(queue_223,earray_226),
inference(forward_demodulation,[status(thm)],[f798,f719]) ).
fof(f4909,plain,
rselect_head(queue_227) = rselect_head(queue_223),
inference(paramodulation,[status(thm)],[f4907,f413]) ).
fof(f4910,plain,
rselect_seq(queue_227) = earray_226,
inference(paramodulation,[status(thm)],[f4907,f407]) ).
fof(f4978,plain,
rselect_head(queue_229) = rselect_head(queue_227),
inference(paramodulation,[status(thm)],[f720,f412]) ).
fof(f4979,plain,
rselect_seq(queue_229) = rselect_seq(queue_227),
inference(paramodulation,[status(thm)],[f720,f411]) ).
fof(f4980,plain,
rselect_tail(queue_229) = index_228,
inference(paramodulation,[status(thm)],[f720,f409]) ).
fof(f4981,plain,
index_230 = rselect_head(queue_227),
inference(forward_demodulation,[status(thm)],[f618,f4978]) ).
fof(f4982,plain,
queue_23 = rstore_seq(queue_19,earray_22),
inference(forward_demodulation,[status(thm)],[f769,f721]) ).
fof(f4984,plain,
rselect_head(queue_23) = rselect_head(queue_19),
inference(paramodulation,[status(thm)],[f4982,f413]) ).
fof(f4986,plain,
rselect_tail(queue_232) = rselect_tail(queue_229),
inference(paramodulation,[status(thm)],[f722,f415]) ).
fof(f4987,plain,
rselect_seq(queue_232) = rselect_seq(queue_229),
inference(paramodulation,[status(thm)],[f722,f410]) ).
fof(f4988,plain,
rselect_head(queue_232) = index_231,
inference(paramodulation,[status(thm)],[f722,f408]) ).
fof(f4989,plain,
index_240 = rselect_tail(queue_229),
inference(forward_demodulation,[status(thm)],[f2876,f4986]) ).
fof(f4990,plain,
earray_239 = rselect_seq(queue_229),
inference(forward_demodulation,[status(thm)],[f836,f4987]) ).
fof(f4991,plain,
queue_236 = rstore_seq(queue_160,earray_235),
inference(forward_demodulation,[status(thm)],[f789,f723]) ).
fof(f4993,plain,
rselect_head(queue_236) = rselect_head(queue_160),
inference(paramodulation,[status(thm)],[f4991,f413]) ).
fof(f4996,plain,
rselect_head(queue_238) = rselect_head(queue_236),
inference(paramodulation,[status(thm)],[f724,f412]) ).
fof(f4998,plain,
rselect_tail(queue_238) = index_237,
inference(paramodulation,[status(thm)],[f724,f409]) ).
fof(f5000,plain,
index_246 = index_237,
inference(forward_demodulation,[status(thm)],[f2943,f4998]) ).
fof(f5004,plain,
index_249 = s(index_237),
inference(backward_demodulation,[status(thm)],[f5000,f626]) ).
fof(f5006,plain,
queue_242 = rstore_seq(queue_232,earray_241),
inference(forward_demodulation,[status(thm)],[f799,f725]) ).
fof(f5008,plain,
rselect_head(queue_242) = rselect_head(queue_232),
inference(paramodulation,[status(thm)],[f5006,f413]) ).
fof(f5009,plain,
rselect_seq(queue_242) = earray_241,
inference(paramodulation,[status(thm)],[f5006,f407]) ).
fof(f5014,plain,
index_123 = s(index_114),
inference(backward_demodulation,[status(thm)],[f5016,f574]) ).
fof(f5016,plain,
index_120 = index_114,
inference(forward_demodulation,[status(thm)],[f4523,f4528]) ).
fof(f5017,plain,
rselect_head(queue_244) = rselect_head(queue_242),
inference(paramodulation,[status(thm)],[f726,f412]) ).
fof(f5018,plain,
rselect_seq(queue_244) = rselect_seq(queue_242),
inference(paramodulation,[status(thm)],[f726,f411]) ).
fof(f5020,plain,
index_282 = rselect_head(queue_242),
inference(forward_demodulation,[status(thm)],[f3500,f5017]) ).
fof(f5021,plain,
earray_281 = rselect_seq(queue_242),
inference(forward_demodulation,[status(thm)],[f842,f5018]) ).
fof(f5022,plain,
queue_248 = rstore_seq(queue_238,earray_247),
inference(forward_demodulation,[status(thm)],[f800,f727]) ).
fof(f5024,plain,
rselect_head(queue_248) = rselect_head(queue_238),
inference(paramodulation,[status(thm)],[f5022,f413]) ).
fof(f5028,plain,
earray_125 = earray_121,
inference(forward_demodulation,[status(thm)],[f4533,f4538]) ).
fof(f5095,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(paramodulation,[status(thm)],[f728,f412]) ).
fof(f5097,plain,
rselect_tail(queue_25) = index_24,
inference(paramodulation,[status(thm)],[f728,f409]) ).
fof(f5098,plain,
index_26 = rselect_head(queue_23),
inference(forward_demodulation,[status(thm)],[f631,f5095]) ).
fof(f5099,plain,
rselect_head(queue_250) = rselect_head(queue_248),
inference(paramodulation,[status(thm)],[f729,f412]) ).
fof(f5101,plain,
rselect_tail(queue_250) = index_249,
inference(paramodulation,[status(thm)],[f729,f409]) ).
fof(f5103,plain,
index_252 = index_249,
inference(forward_demodulation,[status(thm)],[f3018,f5101]) ).
fof(f5104,plain,
queue_254 = rstore_seq(queue_250,earray_253),
inference(forward_demodulation,[status(thm)],[f802,f730]) ).
fof(f5106,plain,
rselect_head(queue_254) = rselect_head(queue_250),
inference(paramodulation,[status(thm)],[f5104,f413]) ).
fof(f5112,plain,
index_255 = s(index_249),
inference(backward_demodulation,[status(thm)],[f5103,f628]) ).
fof(f5114,plain,
rselect_head(queue_256) = rselect_head(queue_254),
inference(paramodulation,[status(thm)],[f731,f412]) ).
fof(f5116,plain,
rselect_tail(queue_256) = index_255,
inference(paramodulation,[status(thm)],[f731,f409]) ).
fof(f5117,plain,
index_257 = rselect_head(queue_254),
inference(forward_demodulation,[status(thm)],[f629,f5114]) ).
fof(f5121,plain,
earray_131 = earray_127,
inference(forward_demodulation,[status(thm)],[f4548,f4557]) ).
fof(f5122,plain,
rselect_tail(queue_259) = rselect_tail(queue_256),
inference(paramodulation,[status(thm)],[f732,f415]) ).
fof(f5124,plain,
rselect_head(queue_259) = index_258,
inference(paramodulation,[status(thm)],[f732,f408]) ).
fof(f5125,plain,
index_261 = rselect_tail(queue_256),
inference(forward_demodulation,[status(thm)],[f3155,f5122]) ).
fof(f5127,plain,
queue_263 = rstore_seq(queue_259,earray_262),
inference(forward_demodulation,[status(thm)],[f803,f733]) ).
fof(f5129,plain,
rselect_head(queue_263) = rselect_head(queue_259),
inference(paramodulation,[status(thm)],[f5127,f413]) ).
fof(f5266,plain,
rselect_head(queue_265) = rselect_head(queue_263),
inference(paramodulation,[status(thm)],[f734,f412]) ).
fof(f5268,plain,
rselect_tail(queue_265) = index_264,
inference(paramodulation,[status(thm)],[f734,f409]) ).
fof(f5270,plain,
index_267 = index_264,
inference(forward_demodulation,[status(thm)],[f3228,f5268]) ).
fof(f5271,plain,
queue_269 = rstore_seq(queue_265,earray_268),
inference(forward_demodulation,[status(thm)],[f804,f735]) ).
fof(f5273,plain,
rselect_head(queue_269) = rselect_head(queue_265),
inference(paramodulation,[status(thm)],[f5271,f413]) ).
fof(f5276,plain,
rselect_head(queue_271) = rselect_head(queue_269),
inference(paramodulation,[status(thm)],[f736,f412]) ).
fof(f5278,plain,
rselect_tail(queue_271) = index_270,
inference(paramodulation,[status(thm)],[f736,f409]) ).
fof(f5280,plain,
index_273 = index_270,
inference(forward_demodulation,[status(thm)],[f3363,f5278]) ).
fof(f5284,plain,
index_270 = s(index_264),
inference(backward_demodulation,[status(thm)],[f5270,f636]) ).
fof(f5286,plain,
queue_275 = rstore_seq(queue_271,earray_274),
inference(forward_demodulation,[status(thm)],[f805,f737]) ).
fof(f5288,plain,
rselect_head(queue_275) = rselect_head(queue_271),
inference(paramodulation,[status(thm)],[f5286,f413]) ).
fof(f5294,plain,
index_276 = s(index_270),
inference(backward_demodulation,[status(thm)],[f5280,f638]) ).
fof(f5296,plain,
rselect_head(queue_277) = rselect_head(queue_275),
inference(paramodulation,[status(thm)],[f738,f412]) ).
fof(f5298,plain,
rselect_tail(queue_277) = index_276,
inference(paramodulation,[status(thm)],[f738,f409]) ).
fof(f5299,plain,
index_278 = rselect_head(queue_275),
inference(forward_demodulation,[status(thm)],[f639,f5296]) ).
fof(f5300,plain,
rselect_tail(queue_28) = rselect_tail(queue_25),
inference(paramodulation,[status(thm)],[f739,f415]) ).
fof(f5302,plain,
rselect_head(queue_28) = index_27,
inference(paramodulation,[status(thm)],[f739,f408]) ).
fof(f5303,plain,
index_30 = rselect_tail(queue_25),
inference(forward_demodulation,[status(thm)],[f3508,f5300]) ).
fof(f5308,plain,
index_144 = s(index_135),
inference(backward_demodulation,[status(thm)],[f5310,f582]) ).
fof(f5310,plain,
index_141 = index_135,
inference(forward_demodulation,[status(thm)],[f4575,f4580]) ).
fof(f5311,plain,
rselect_tail(queue_280) = rselect_tail(queue_277),
inference(paramodulation,[status(thm)],[f740,f415]) ).
fof(f5313,plain,
rselect_head(queue_280) = index_279,
inference(paramodulation,[status(thm)],[f740,f408]) ).
fof(f5314,plain,
index_9 = rselect_tail(queue_277),
inference(forward_demodulation,[status(thm)],[f4337,f5311]) ).
fof(f5316,plain,
queue_32 = rstore_seq(queue_28,earray_31),
inference(forward_demodulation,[status(thm)],[f770,f741]) ).
fof(f5318,plain,
rselect_head(queue_32) = rselect_head(queue_28),
inference(paramodulation,[status(thm)],[f5316,f413]) ).
fof(f5321,plain,
rselect_head(queue_34) = rselect_head(queue_32),
inference(paramodulation,[status(thm)],[f742,f412]) ).
fof(f5323,plain,
rselect_tail(queue_34) = index_33,
inference(paramodulation,[status(thm)],[f742,f409]) ).
fof(f5325,plain,
index_36 = index_33,
inference(forward_demodulation,[status(thm)],[f3577,f5323]) ).
fof(f5326,plain,
s(index_39) != index_33,
inference(backward_demodulation,[status(thm)],[f5325,f3634]) ).
fof(f5327,plain,
index_39 != index_33,
inference(backward_demodulation,[status(thm)],[f5325,f3643]) ).
fof(f5328,plain,
index_39 = s(index_33),
inference(backward_demodulation,[status(thm)],[f5325,f646]) ).
fof(f5331,plain,
select(earray_37,index_33) = e13,
inference(backward_demodulation,[status(thm)],[f5325,f808]) ).
fof(f5337,plain,
queue_38 = rstore_seq(queue_34,earray_37),
inference(forward_demodulation,[status(thm)],[f771,f743]) ).
fof(f5339,plain,
rselect_head(queue_38) = rselect_head(queue_34),
inference(paramodulation,[status(thm)],[f5337,f413]) ).
fof(f5340,plain,
rselect_seq(queue_38) = earray_37,
inference(paramodulation,[status(thm)],[f5337,f407]) ).
fof(f5341,plain,
rselect_head(queue_40) = rselect_head(queue_38),
inference(paramodulation,[status(thm)],[f744,f412]) ).
fof(f5342,plain,
rselect_seq(queue_40) = rselect_seq(queue_38),
inference(paramodulation,[status(thm)],[f744,f411]) ).
fof(f5343,plain,
rselect_tail(queue_40) = index_39,
inference(paramodulation,[status(thm)],[f744,f409]) ).
fof(f5344,plain,
earray_41 = rselect_seq(queue_38),
inference(forward_demodulation,[status(thm)],[f845,f5342]) ).
fof(f5345,plain,
index_42 = index_39,
inference(forward_demodulation,[status(thm)],[f3648,f5343]) ).
fof(f5349,plain,
index_45 = s(index_39),
inference(backward_demodulation,[status(thm)],[f5345,f648]) ).
fof(f5353,plain,
earray_146 = earray_142,
inference(forward_demodulation,[status(thm)],[f4585,f4590]) ).
fof(f5355,plain,
queue_44 = rstore_seq(queue_40,earray_43),
inference(forward_demodulation,[status(thm)],[f772,f745]) ).
fof(f5357,plain,
rselect_head(queue_44) = rselect_head(queue_40),
inference(paramodulation,[status(thm)],[f5355,f413]) ).
fof(f5358,plain,
rselect_seq(queue_44) = earray_43,
inference(paramodulation,[status(thm)],[f5355,f407]) ).
fof(f5359,plain,
rselect_head(queue_46) = rselect_head(queue_44),
inference(paramodulation,[status(thm)],[f746,f412]) ).
fof(f5360,plain,
rselect_seq(queue_46) = rselect_seq(queue_44),
inference(paramodulation,[status(thm)],[f746,f411]) ).
fof(f5361,plain,
rselect_tail(queue_46) = index_45,
inference(paramodulation,[status(thm)],[f746,f409]) ).
fof(f5362,plain,
index_47 = rselect_head(queue_44),
inference(forward_demodulation,[status(thm)],[f649,f5359]) ).
fof(f5363,plain,
rselect_tail(queue_49) = rselect_tail(queue_46),
inference(paramodulation,[status(thm)],[f747,f415]) ).
fof(f5364,plain,
rselect_seq(queue_49) = rselect_seq(queue_46),
inference(paramodulation,[status(thm)],[f747,f410]) ).
fof(f5365,plain,
rselect_head(queue_49) = index_48,
inference(paramodulation,[status(thm)],[f747,f408]) ).
fof(f5366,plain,
index_51 = rselect_tail(queue_46),
inference(forward_demodulation,[status(thm)],[f3787,f5363]) ).
fof(f5367,plain,
earray_50 = rselect_seq(queue_46),
inference(forward_demodulation,[status(thm)],[f846,f5364]) ).
fof(f5368,plain,
queue_5 = rstore_seq(queue_1,earray_4),
inference(forward_demodulation,[status(thm)],[f766,f748]) ).
fof(f5370,plain,
rselect_head(queue_5) = rselect_head(queue_1),
inference(paramodulation,[status(thm)],[f5368,f413]) ).
fof(f5373,plain,
rselect_head(queue_5) = index_0,
inference(forward_demodulation,[status(thm)],[f4474,f5370]) ).
fof(f5441,plain,
earray_161 = earray_148,
inference(forward_demodulation,[status(thm)],[f4595,f4605]) ).
fof(f5442,plain,
queue_53 = rstore_seq(queue_49,earray_52),
inference(forward_demodulation,[status(thm)],[f773,f749]) ).
fof(f5444,plain,
rselect_head(queue_53) = rselect_head(queue_49),
inference(paramodulation,[status(thm)],[f5442,f413]) ).
fof(f5445,plain,
rselect_seq(queue_53) = earray_52,
inference(paramodulation,[status(thm)],[f5442,f407]) ).
fof(f5447,plain,
rselect_head(queue_55) = rselect_head(queue_53),
inference(paramodulation,[status(thm)],[f750,f412]) ).
fof(f5448,plain,
rselect_seq(queue_55) = rselect_seq(queue_53),
inference(paramodulation,[status(thm)],[f750,f411]) ).
fof(f5449,plain,
rselect_tail(queue_55) = index_54,
inference(paramodulation,[status(thm)],[f750,f409]) ).
fof(f5450,plain,
earray_56 = rselect_seq(queue_53),
inference(forward_demodulation,[status(thm)],[f847,f5448]) ).
fof(f5451,plain,
index_57 = index_54,
inference(forward_demodulation,[status(thm)],[f3856,f5449]) ).
fof(f5454,plain,
index_60 = s(index_54),
inference(backward_demodulation,[status(thm)],[f5451,f655]) ).
fof(f5457,plain,
queue_59 = rstore_seq(queue_55,earray_58),
inference(forward_demodulation,[status(thm)],[f774,f751]) ).
fof(f5459,plain,
rselect_head(queue_59) = rselect_head(queue_55),
inference(paramodulation,[status(thm)],[f5457,f413]) ).
fof(f5460,plain,
rselect_seq(queue_59) = earray_58,
inference(paramodulation,[status(thm)],[f5457,f407]) ).
fof(f5461,plain,
rselect_head(queue_61) = rselect_head(queue_59),
inference(paramodulation,[status(thm)],[f752,f412]) ).
fof(f5462,plain,
rselect_seq(queue_61) = rselect_seq(queue_59),
inference(paramodulation,[status(thm)],[f752,f411]) ).
fof(f5463,plain,
rselect_tail(queue_61) = index_60,
inference(paramodulation,[status(thm)],[f752,f409]) ).
fof(f5464,plain,
earray_62 = rselect_seq(queue_59),
inference(forward_demodulation,[status(thm)],[f848,f5462]) ).
fof(f5465,plain,
index_63 = index_60,
inference(forward_demodulation,[status(thm)],[f3993,f5463]) ).
fof(f5466,plain,
queue_65 = rstore_seq(queue_61,earray_64),
inference(forward_demodulation,[status(thm)],[f775,f753]) ).
fof(f5468,plain,
rselect_head(queue_65) = rselect_head(queue_61),
inference(paramodulation,[status(thm)],[f5466,f413]) ).
fof(f5469,plain,
rselect_seq(queue_65) = earray_64,
inference(paramodulation,[status(thm)],[f5466,f407]) ).
fof(f5474,plain,
index_66 = s(index_60),
inference(backward_demodulation,[status(thm)],[f5465,f657]) ).
fof(f5476,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(paramodulation,[status(thm)],[f754,f412]) ).
fof(f5477,plain,
rselect_seq(queue_67) = rselect_seq(queue_65),
inference(paramodulation,[status(thm)],[f754,f411]) ).
fof(f5478,plain,
rselect_tail(queue_67) = index_66,
inference(paramodulation,[status(thm)],[f754,f409]) ).
fof(f5479,plain,
index_68 = rselect_head(queue_65),
inference(forward_demodulation,[status(thm)],[f658,f5476]) ).
fof(f5550,plain,
index_237 = s(index_156),
inference(backward_demodulation,[status(thm)],[f5552,f621]) ).
fof(f5552,plain,
index_234 = index_156,
inference(forward_demodulation,[status(thm)],[f4614,f4624]) ).
fof(f5553,plain,
rselect_head(queue_7) = rselect_head(queue_5),
inference(paramodulation,[status(thm)],[f755,f412]) ).
fof(f5555,plain,
rselect_tail(queue_7) = index_6,
inference(paramodulation,[status(thm)],[f755,f409]) ).
fof(f5557,plain,
index_78 = index_6,
inference(forward_demodulation,[status(thm)],[f4203,f5555]) ).
fof(f5558,plain,
rselect_tail(queue_70) = rselect_tail(queue_67),
inference(paramodulation,[status(thm)],[f756,f415]) ).
fof(f5559,plain,
rselect_seq(queue_70) = rselect_seq(queue_67),
inference(paramodulation,[status(thm)],[f756,f410]) ).
fof(f5560,plain,
rselect_head(queue_70) = index_69,
inference(paramodulation,[status(thm)],[f756,f408]) ).
fof(f5561,plain,
index_72 = rselect_tail(queue_67),
inference(forward_demodulation,[status(thm)],[f4134,f5558]) ).
fof(f5562,plain,
earray_71 = rselect_seq(queue_67),
inference(forward_demodulation,[status(thm)],[f849,f5559]) ).
fof(f5565,plain,
index_81 = s(index_6),
inference(backward_demodulation,[status(thm)],[f5557,f663]) ).
fof(f5568,plain,
queue_74 = rstore_seq(queue_70,earray_73),
inference(forward_demodulation,[status(thm)],[f776,f757]) ).
fof(f5570,plain,
rselect_head(queue_74) = rselect_head(queue_70),
inference(paramodulation,[status(thm)],[f5568,f413]) ).
fof(f5571,plain,
rselect_seq(queue_74) = earray_73,
inference(paramodulation,[status(thm)],[f5568,f407]) ).
fof(f5573,plain,
rselect_head(queue_76) = rselect_head(queue_74),
inference(paramodulation,[status(thm)],[f758,f412]) ).
fof(f5574,plain,
rselect_seq(queue_76) = rselect_seq(queue_74),
inference(paramodulation,[status(thm)],[f758,f411]) ).
fof(f5575,plain,
rselect_tail(queue_76) = index_75,
inference(paramodulation,[status(thm)],[f758,f409]) ).
fof(f5576,plain,
earray_83 = rselect_seq(queue_74),
inference(forward_demodulation,[status(thm)],[f852,f5574]) ).
fof(f5577,plain,
index_84 = index_75,
inference(forward_demodulation,[status(thm)],[f4270,f5575]) ).
fof(f5578,plain,
queue_80 = rstore_seq(queue_7,earray_79),
inference(forward_demodulation,[status(thm)],[f767,f759]) ).
fof(f5580,plain,
rselect_head(queue_80) = rselect_head(queue_7),
inference(paramodulation,[status(thm)],[f5578,f413]) ).
fof(f5584,plain,
index_87 = s(index_75),
inference(backward_demodulation,[status(thm)],[f5577,f665]) ).
fof(f5587,plain,
rselect_head(queue_82) = rselect_head(queue_80),
inference(paramodulation,[status(thm)],[f760,f412]) ).
fof(f5589,plain,
rselect_tail(queue_82) = index_81,
inference(paramodulation,[status(thm)],[f760,f409]) ).
fof(f5591,plain,
index_153 = index_81,
inference(forward_demodulation,[status(thm)],[f1402,f5589]) ).
fof(f5596,plain,
index_156 = s(index_81),
inference(backward_demodulation,[status(thm)],[f5591,f587]) ).
fof(f5598,plain,
queue_86 = rstore_seq(queue_76,earray_85),
inference(forward_demodulation,[status(thm)],[f777,f761]) ).
fof(f5600,plain,
rselect_head(queue_86) = rselect_head(queue_76),
inference(paramodulation,[status(thm)],[f5598,f413]) ).
fof(f5601,plain,
rselect_seq(queue_86) = earray_85,
inference(paramodulation,[status(thm)],[f5598,f407]) ).
fof(f5602,plain,
rselect_head(queue_88) = rselect_head(queue_86),
inference(paramodulation,[status(thm)],[f762,f412]) ).
fof(f5603,plain,
rselect_seq(queue_88) = rselect_seq(queue_86),
inference(paramodulation,[status(thm)],[f762,f411]) ).
fof(f5604,plain,
rselect_tail(queue_88) = index_87,
inference(paramodulation,[status(thm)],[f762,f409]) ).
fof(f5605,plain,
earray_89 = rselect_seq(queue_86),
inference(forward_demodulation,[status(thm)],[f853,f5603]) ).
fof(f5606,plain,
index_90 = index_87,
inference(forward_demodulation,[status(thm)],[f4338,f5604]) ).
fof(f5609,plain,
index_93 = s(index_87),
inference(backward_demodulation,[status(thm)],[f5606,f668]) ).
fof(f5615,plain,
index_174 = s(index_165),
inference(backward_demodulation,[status(thm)],[f5617,f595]) ).
fof(f5617,plain,
index_171 = index_165,
inference(forward_demodulation,[status(thm)],[f4632,f4637]) ).
fof(f5618,plain,
queue_92 = rstore_seq(queue_88,earray_91),
inference(forward_demodulation,[status(thm)],[f779,f763]) ).
fof(f5620,plain,
rselect_head(queue_92) = rselect_head(queue_88),
inference(paramodulation,[status(thm)],[f5618,f413]) ).
fof(f5621,plain,
rselect_seq(queue_92) = earray_91,
inference(paramodulation,[status(thm)],[f5618,f407]) ).
fof(f5622,plain,
rselect_head(queue_94) = rselect_head(queue_92),
inference(paramodulation,[status(thm)],[f764,f412]) ).
fof(f5623,plain,
rselect_seq(queue_94) = rselect_seq(queue_92),
inference(paramodulation,[status(thm)],[f764,f411]) ).
fof(f5624,plain,
rselect_tail(queue_94) = index_93,
inference(paramodulation,[status(thm)],[f764,f409]) ).
fof(f5625,plain,
index_95 = rselect_head(queue_92),
inference(forward_demodulation,[status(thm)],[f669,f5622]) ).
fof(f5626,plain,
rselect_tail(queue_97) = rselect_tail(queue_94),
inference(paramodulation,[status(thm)],[f765,f415]) ).
fof(f5627,plain,
rselect_seq(queue_97) = rselect_seq(queue_94),
inference(paramodulation,[status(thm)],[f765,f410]) ).
fof(f5628,plain,
rselect_head(queue_97) = index_96,
inference(paramodulation,[status(thm)],[f765,f408]) ).
fof(f5629,plain,
index_99 = rselect_tail(queue_94),
inference(forward_demodulation,[status(thm)],[f4471,f5626]) ).
fof(f5630,plain,
earray_98 = rselect_seq(queue_94),
inference(forward_demodulation,[status(thm)],[f854,f5627]) ).
fof(f5635,plain,
earray_176 = earray_172,
inference(forward_demodulation,[status(thm)],[f4646,f4651]) ).
fof(f5709,plain,
earray_182 = earray_178,
inference(forward_demodulation,[status(thm)],[f4662,f4666]) ).
fof(f5867,plain,
index_195 = s(index_186),
inference(backward_demodulation,[status(thm)],[f5869,f604]) ).
fof(f5869,plain,
index_192 = index_186,
inference(forward_demodulation,[status(thm)],[f4679,f4694]) ).
fof(f5947,plain,
earray_197 = earray_193,
inference(forward_demodulation,[status(thm)],[f4699,f4704]) ).
fof(f6019,plain,
earray_203 = earray_199,
inference(forward_demodulation,[status(thm)],[f4714,f4718]) ).
fof(f6026,plain,
index_216 = s(index_207),
inference(backward_demodulation,[status(thm)],[f6028,f613]) ).
fof(f6028,plain,
index_213 = index_207,
inference(forward_demodulation,[status(thm)],[f4732,f4806]) ).
fof(f6098,plain,
earray_218 = earray_214,
inference(forward_demodulation,[status(thm)],[f4811,f4885]) ).
fof(f6101,plain,
earray_224 = earray_220,
inference(forward_demodulation,[status(thm)],[f4890,f4895]) ).
fof(f6245,plain,
index_240 = index_228,
inference(forward_demodulation,[status(thm)],[f4980,f4989]) ).
fof(f6520,plain,
elem_283 = select(earray_241,index_282),
inference(backward_demodulation,[status(thm)],[f6521,f563]) ).
fof(f6521,plain,
earray_281 = earray_241,
inference(forward_demodulation,[status(thm)],[f5009,f5021]) ).
fof(f6598,plain,
index_264 = s(index_255),
inference(backward_demodulation,[status(thm)],[f6600,f633]) ).
fof(f6600,plain,
index_261 = index_255,
inference(forward_demodulation,[status(thm)],[f5116,f5125]) ).
fof(f7015,plain,
index_33 = s(index_24),
inference(backward_demodulation,[status(thm)],[f7017,f644]) ).
fof(f7017,plain,
index_30 = index_24,
inference(forward_demodulation,[status(thm)],[f5097,f5303]) ).
fof(f7093,plain,
index_12 = s(index_276),
inference(backward_demodulation,[status(thm)],[f7094,f572]) ).
fof(f7094,plain,
index_9 = index_276,
inference(forward_demodulation,[status(thm)],[f5298,f5314]) ).
fof(f7168,plain,
index_45 != index_33,
inference(forward_demodulation,[status(thm)],[f5349,f5326]) ).
fof(f7372,plain,
earray_41 = earray_37,
inference(forward_demodulation,[status(thm)],[f5340,f5344]) ).
fof(f7443,plain,
index_54 = s(index_45),
inference(backward_demodulation,[status(thm)],[f7445,f652]) ).
fof(f7445,plain,
index_51 = index_45,
inference(forward_demodulation,[status(thm)],[f5361,f5366]) ).
fof(f7522,plain,
earray_56 = earray_52,
inference(forward_demodulation,[status(thm)],[f5445,f5450]) ).
fof(f7850,plain,
earray_62 = earray_58,
inference(forward_demodulation,[status(thm)],[f5460,f5464]) ).
fof(f8058,plain,
index_75 = s(index_66),
inference(backward_demodulation,[status(thm)],[f8061,f661]) ).
fof(f8061,plain,
index_72 = index_66,
inference(forward_demodulation,[status(thm)],[f5478,f5561]) ).
fof(f8068,plain,
earray_83 = earray_73,
inference(forward_demodulation,[status(thm)],[f5571,f5576]) ).
fof(f8276,plain,
earray_89 = earray_85,
inference(forward_demodulation,[status(thm)],[f5601,f5605]) ).
fof(f8483,plain,
index_102 = s(index_93),
inference(backward_demodulation,[status(thm)],[f8484,f565]) ).
fof(f8484,plain,
index_99 = index_93,
inference(forward_demodulation,[status(thm)],[f5624,f5629]) ).
fof(f11838,plain,
s(index_45) != index_36,
inference(forward_demodulation,[status(thm)],[f5349,f3578]) ).
fof(f11839,plain,
index_54 != index_36,
inference(forward_demodulation,[status(thm)],[f7443,f11838]) ).
fof(f11840,plain,
index_54 != index_33,
inference(forward_demodulation,[status(thm)],[f5325,f11839]) ).
fof(f12098,plain,
rselect_head(queue_101) = index_96,
inference(forward_demodulation,[status(thm)],[f5628,f4480]) ).
fof(f12135,plain,
rselect_head(queue_103) = index_96,
inference(forward_demodulation,[status(thm)],[f12098,f4487]) ).
fof(f12136,plain,
rselect_head(queue_107) = index_96,
inference(forward_demodulation,[status(thm)],[f12135,f4494]) ).
fof(f12137,plain,
rselect_head(queue_109) = index_96,
inference(forward_demodulation,[status(thm)],[f12136,f4497]) ).
fof(f12138,plain,
rselect_head(queue_11) = index_279,
inference(forward_demodulation,[status(thm)],[f5313,f4514]) ).
fof(f12140,plain,
index_116 = rselect_head(queue_109),
inference(forward_demodulation,[status(thm)],[f4524,f4519]) ).
fof(f12150,plain,
index_116 = s(index_95),
inference(backward_demodulation,[status(thm)],[f12151,f670]) ).
fof(f12151,plain,
index_116 = index_96,
inference(forward_demodulation,[status(thm)],[f12137,f12140]) ).
fof(f12413,plain,
earray_119 = rselect_seq(queue_113),
inference(forward_demodulation,[status(thm)],[f4529,f4522]) ).
fof(f12417,plain,
earray_119 = earray_112,
inference(forward_demodulation,[status(thm)],[f4520,f12413]) ).
fof(f12420,plain,
rselect_head(queue_122) = index_117,
inference(forward_demodulation,[status(thm)],[f4527,f4532]) ).
fof(f12421,plain,
rselect_head(queue_124) = index_117,
inference(forward_demodulation,[status(thm)],[f12420,f4535]) ).
fof(f12457,plain,
rselect_head(queue_128) = index_117,
inference(forward_demodulation,[status(thm)],[f12421,f4547]) ).
fof(f12458,plain,
rselect_head(queue_13) = index_279,
inference(forward_demodulation,[status(thm)],[f12138,f4549]) ).
fof(f12459,plain,
rselect_head(queue_130) = index_117,
inference(forward_demodulation,[status(thm)],[f12457,f4554]) ).
fof(f12461,plain,
index_137 = rselect_head(queue_130),
inference(forward_demodulation,[status(thm)],[f4576,f4571]) ).
fof(f12466,plain,
index_138 = s(index_117),
inference(backward_demodulation,[status(thm)],[f12468,f580]) ).
fof(f12468,plain,
index_137 = index_117,
inference(forward_demodulation,[status(thm)],[f12459,f12461]) ).
fof(f12606,plain,
earray_140 = rselect_seq(queue_134),
inference(forward_demodulation,[status(thm)],[f4581,f4574]) ).
fof(f12610,plain,
earray_140 = earray_133,
inference(forward_demodulation,[status(thm)],[f4572,f12606]) ).
fof(f12611,plain,
rselect_head(queue_143) = index_138,
inference(forward_demodulation,[status(thm)],[f4579,f4584]) ).
fof(f12612,plain,
rselect_head(queue_145) = index_138,
inference(forward_demodulation,[status(thm)],[f12611,f4587]) ).
fof(f12613,plain,
rselect_head(queue_149) = index_138,
inference(forward_demodulation,[status(thm)],[f12612,f4594]) ).
fof(f12650,plain,
rselect_head(queue_151) = index_138,
inference(forward_demodulation,[status(thm)],[f12613,f4602]) ).
fof(f12651,plain,
index_158 = rselect_head(queue_82),
inference(forward_demodulation,[status(thm)],[f4615,f4609]) ).
fof(f12694,plain,
index_167 = rselect_head(queue_151),
inference(forward_demodulation,[status(thm)],[f4633,f4628]) ).
fof(f12699,plain,
index_168 = s(index_138),
inference(backward_demodulation,[status(thm)],[f12701,f593]) ).
fof(f12701,plain,
index_167 = index_138,
inference(forward_demodulation,[status(thm)],[f12650,f12694]) ).
fof(f12804,plain,
earray_170 = rselect_seq(queue_164),
inference(forward_demodulation,[status(thm)],[f4638,f4631]) ).
fof(f12808,plain,
earray_170 = earray_163,
inference(forward_demodulation,[status(thm)],[f4629,f12804]) ).
fof(f12812,plain,
rselect_head(queue_17) = index_279,
inference(forward_demodulation,[status(thm)],[f12458,f4641]) ).
fof(f12847,plain,
rselect_head(queue_173) = index_168,
inference(forward_demodulation,[status(thm)],[f4636,f4645]) ).
fof(f12848,plain,
rselect_head(queue_175) = index_168,
inference(forward_demodulation,[status(thm)],[f12847,f4648]) ).
fof(f12850,plain,
rselect_head(queue_179) = index_168,
inference(forward_demodulation,[status(thm)],[f12848,f4661]) ).
fof(f12851,plain,
rselect_head(queue_181) = index_168,
inference(forward_demodulation,[status(thm)],[f12850,f4663]) ).
fof(f12904,plain,
index_188 = rselect_head(queue_181),
inference(forward_demodulation,[status(thm)],[f4680,f4675]) ).
fof(f12909,plain,
index_189 = s(index_168),
inference(backward_demodulation,[status(thm)],[f12911,f602]) ).
fof(f12911,plain,
index_188 = index_168,
inference(forward_demodulation,[status(thm)],[f12851,f12904]) ).
fof(f13013,plain,
earray_191 = rselect_seq(queue_185),
inference(forward_demodulation,[status(thm)],[f4695,f4678]) ).
fof(f13017,plain,
earray_191 = earray_184,
inference(forward_demodulation,[status(thm)],[f4676,f13013]) ).
fof(f13018,plain,
rselect_head(queue_19) = index_279,
inference(forward_demodulation,[status(thm)],[f12812,f4681]) ).
fof(f13019,plain,
rselect_head(queue_194) = index_189,
inference(forward_demodulation,[status(thm)],[f4693,f4698]) ).
fof(f13056,plain,
rselect_head(queue_196) = index_189,
inference(forward_demodulation,[status(thm)],[f13019,f4701]) ).
fof(f13075,plain,
rselect_head(queue_200) = index_189,
inference(forward_demodulation,[status(thm)],[f13056,f4713]) ).
fof(f13076,plain,
rselect_head(queue_202) = index_189,
inference(forward_demodulation,[status(thm)],[f13075,f4715]) ).
fof(f13077,plain,
index_209 = rselect_head(queue_202),
inference(forward_demodulation,[status(thm)],[f4733,f4722]) ).
fof(f13082,plain,
index_210 = s(index_189),
inference(backward_demodulation,[status(thm)],[f13084,f611]) ).
fof(f13084,plain,
index_209 = index_189,
inference(forward_demodulation,[status(thm)],[f13076,f13077]) ).
fof(f13152,plain,
earray_212 = rselect_seq(queue_206),
inference(forward_demodulation,[status(thm)],[f4807,f4731]) ).
fof(f13156,plain,
earray_212 = earray_205,
inference(forward_demodulation,[status(thm)],[f4723,f13152]) ).
fof(f13178,plain,
rselect_head(queue_215) = index_210,
inference(forward_demodulation,[status(thm)],[f4805,f4810]) ).
fof(f13198,plain,
rselect_head(queue_217) = index_210,
inference(forward_demodulation,[status(thm)],[f13178,f4882]) ).
fof(f13199,plain,
rselect_head(queue_221) = index_210,
inference(forward_demodulation,[status(thm)],[f13198,f4889]) ).
fof(f13200,plain,
rselect_head(queue_223) = index_210,
inference(forward_demodulation,[status(thm)],[f13199,f4892]) ).
fof(f13236,plain,
index_230 = rselect_head(queue_223),
inference(forward_demodulation,[status(thm)],[f4981,f4909]) ).
fof(f13241,plain,
index_231 = s(index_210),
inference(backward_demodulation,[status(thm)],[f13243,f619]) ).
fof(f13243,plain,
index_230 = index_210,
inference(forward_demodulation,[status(thm)],[f13200,f13236]) ).
fof(f13364,plain,
earray_239 = rselect_seq(queue_227),
inference(forward_demodulation,[status(thm)],[f4990,f4979]) ).
fof(f13368,plain,
earray_239 = earray_226,
inference(forward_demodulation,[status(thm)],[f4910,f13364]) ).
fof(f13389,plain,
index_26 = rselect_head(queue_19),
inference(forward_demodulation,[status(thm)],[f5098,f4984]) ).
fof(f13399,plain,
index_26 = s(index_278),
inference(backward_demodulation,[status(thm)],[f13400,f640]) ).
fof(f13400,plain,
index_26 = index_279,
inference(forward_demodulation,[status(thm)],[f13018,f13389]) ).
fof(f13576,plain,
rselect_head(queue_236) = index_159,
inference(forward_demodulation,[status(thm)],[f4623,f4993]) ).
fof(f13612,plain,
rselect_head(queue_238) = index_159,
inference(forward_demodulation,[status(thm)],[f13576,f4996]) ).
fof(f13613,plain,
index_282 = rselect_head(queue_232),
inference(forward_demodulation,[status(thm)],[f5020,f5008]) ).
fof(f13615,plain,
index_282 = s(index_210),
inference(backward_demodulation,[status(thm)],[f13620,f13241]) ).
fof(f13620,plain,
index_282 = index_231,
inference(forward_demodulation,[status(thm)],[f4988,f13613]) ).
fof(f13747,plain,
rselect_head(queue_248) = index_159,
inference(forward_demodulation,[status(thm)],[f13612,f5024]) ).
fof(f13779,plain,
rselect_head(queue_250) = index_159,
inference(forward_demodulation,[status(thm)],[f13747,f5099]) ).
fof(f13780,plain,
index_257 = rselect_head(queue_250),
inference(forward_demodulation,[status(thm)],[f5117,f5106]) ).
fof(f13785,plain,
index_258 = s(index_159),
inference(backward_demodulation,[status(thm)],[f13787,f630]) ).
fof(f13787,plain,
index_257 = index_159,
inference(forward_demodulation,[status(thm)],[f13779,f13780]) ).
fof(f13870,plain,
rselect_head(queue_263) = index_258,
inference(forward_demodulation,[status(thm)],[f5124,f5129]) ).
fof(f13875,plain,
rselect_head(queue_265) = index_258,
inference(forward_demodulation,[status(thm)],[f13870,f5266]) ).
fof(f13876,plain,
rselect_head(queue_269) = index_258,
inference(forward_demodulation,[status(thm)],[f13875,f5273]) ).
fof(f13892,plain,
rselect_head(queue_271) = index_258,
inference(forward_demodulation,[status(thm)],[f13876,f5276]) ).
fof(f13893,plain,
index_278 = rselect_head(queue_271),
inference(forward_demodulation,[status(thm)],[f5299,f5288]) ).
fof(f13895,plain,
index_26 = s(index_258),
inference(backward_demodulation,[status(thm)],[f13900,f13399]) ).
fof(f13900,plain,
index_278 = index_258,
inference(forward_demodulation,[status(thm)],[f13892,f13893]) ).
fof(f14062,plain,
rselect_head(queue_32) = index_27,
inference(forward_demodulation,[status(thm)],[f5302,f5318]) ).
fof(f14063,plain,
rselect_head(queue_34) = index_27,
inference(forward_demodulation,[status(thm)],[f14062,f5321]) ).
fof(f14065,plain,
rselect_head(queue_38) = index_27,
inference(forward_demodulation,[status(thm)],[f14063,f5339]) ).
fof(f14076,plain,
rselect_head(queue_40) = index_27,
inference(forward_demodulation,[status(thm)],[f14065,f5341]) ).
fof(f14078,plain,
index_47 = rselect_head(queue_40),
inference(forward_demodulation,[status(thm)],[f5362,f5357]) ).
fof(f14083,plain,
index_48 = s(index_27),
inference(backward_demodulation,[status(thm)],[f14085,f650]) ).
fof(f14085,plain,
index_47 = index_27,
inference(forward_demodulation,[status(thm)],[f14076,f14078]) ).
fof(f14165,plain,
earray_50 = rselect_seq(queue_44),
inference(forward_demodulation,[status(thm)],[f5367,f5360]) ).
fof(f14169,plain,
earray_50 = earray_43,
inference(forward_demodulation,[status(thm)],[f5358,f14165]) ).
fof(f14179,plain,
rselect_head(queue_53) = index_48,
inference(forward_demodulation,[status(thm)],[f5365,f5444]) ).
fof(f14180,plain,
rselect_head(queue_55) = index_48,
inference(forward_demodulation,[status(thm)],[f14179,f5447]) ).
fof(f14182,plain,
rselect_head(queue_59) = index_48,
inference(forward_demodulation,[status(thm)],[f14180,f5459]) ).
fof(f14183,plain,
rselect_head(queue_61) = index_48,
inference(forward_demodulation,[status(thm)],[f14182,f5461]) ).
fof(f14199,plain,
index_68 = rselect_head(queue_61),
inference(forward_demodulation,[status(thm)],[f5479,f5468]) ).
fof(f14204,plain,
index_69 = s(index_48),
inference(backward_demodulation,[status(thm)],[f14206,f659]) ).
fof(f14206,plain,
index_68 = index_48,
inference(forward_demodulation,[status(thm)],[f14183,f14199]) ).
fof(f14280,plain,
earray_71 = rselect_seq(queue_65),
inference(forward_demodulation,[status(thm)],[f5562,f5477]) ).
fof(f14284,plain,
earray_71 = earray_64,
inference(forward_demodulation,[status(thm)],[f5469,f14280]) ).
fof(f14287,plain,
rselect_head(queue_7) = index_0,
inference(forward_demodulation,[status(thm)],[f5373,f5553]) ).
fof(f14300,plain,
rselect_head(queue_74) = index_69,
inference(forward_demodulation,[status(thm)],[f5560,f5570]) ).
fof(f14301,plain,
rselect_head(queue_76) = index_69,
inference(forward_demodulation,[status(thm)],[f14300,f5573]) ).
fof(f14308,plain,
rselect_head(queue_80) = index_0,
inference(forward_demodulation,[status(thm)],[f14287,f5580]) ).
fof(f14309,plain,
index_158 = rselect_head(queue_80),
inference(forward_demodulation,[status(thm)],[f12651,f5587]) ).
fof(f14315,plain,
index_159 = s(index_0),
inference(backward_demodulation,[status(thm)],[f14317,f589]) ).
fof(f14317,plain,
index_158 = index_0,
inference(forward_demodulation,[status(thm)],[f14308,f14309]) ).
fof(f14318,plain,
index_159 = index_6,
inference(forward_demodulation,[status(thm)],[f4484,f14315]) ).
fof(f14325,plain,
index_81 = s(index_159),
inference(backward_demodulation,[status(thm)],[f14318,f5565]) ).
fof(f14331,plain,
index_81 = index_258,
inference(forward_demodulation,[status(thm)],[f13785,f14325]) ).
fof(f14339,plain,
index_156 = s(index_258),
inference(backward_demodulation,[status(thm)],[f14331,f5596]) ).
fof(f14345,plain,
index_156 = index_26,
inference(forward_demodulation,[status(thm)],[f13895,f14339]) ).
fof(f14750,plain,
index_27 = s(index_156),
inference(backward_demodulation,[status(thm)],[f14345,f635]) ).
fof(f14752,plain,
index_27 = index_237,
inference(forward_demodulation,[status(thm)],[f5550,f14750]) ).
fof(f16574,plain,
index_48 = s(index_237),
inference(backward_demodulation,[status(thm)],[f14752,f14083]) ).
fof(f16585,plain,
index_48 = index_249,
inference(forward_demodulation,[status(thm)],[f5004,f16574]) ).
fof(f16591,plain,
index_69 = s(index_249),
inference(backward_demodulation,[status(thm)],[f16585,f14204]) ).
fof(f16601,plain,
index_69 = index_255,
inference(forward_demodulation,[status(thm)],[f5112,f16591]) ).
fof(f16609,plain,
rselect_head(queue_76) = index_255,
inference(backward_demodulation,[status(thm)],[f16601,f14301]) ).
fof(f17106,plain,
rselect_head(queue_86) = index_255,
inference(forward_demodulation,[status(thm)],[f16609,f5600]) ).
fof(f17107,plain,
rselect_head(queue_88) = index_255,
inference(forward_demodulation,[status(thm)],[f17106,f5602]) ).
fof(f17109,plain,
index_95 = rselect_head(queue_88),
inference(forward_demodulation,[status(thm)],[f5625,f5620]) ).
fof(f17113,plain,
index_116 = s(index_255),
inference(backward_demodulation,[status(thm)],[f17116,f12150]) ).
fof(f17116,plain,
index_95 = index_255,
inference(forward_demodulation,[status(thm)],[f17107,f17109]) ).
fof(f17117,plain,
index_116 = index_264,
inference(forward_demodulation,[status(thm)],[f6598,f17113]) ).
fof(f17131,plain,
index_270 = s(index_116),
inference(backward_demodulation,[status(thm)],[f17117,f5284]) ).
fof(f17135,plain,
index_270 = index_117,
inference(forward_demodulation,[status(thm)],[f571,f17131]) ).
fof(f17587,plain,
index_276 = s(index_117),
inference(backward_demodulation,[status(thm)],[f17135,f5294]) ).
fof(f17591,plain,
index_276 = index_138,
inference(forward_demodulation,[status(thm)],[f12466,f17587]) ).
fof(f17619,plain,
index_12 = s(index_138),
inference(backward_demodulation,[status(thm)],[f17591,f7093]) ).
fof(f17629,plain,
index_12 = index_168,
inference(forward_demodulation,[status(thm)],[f12699,f17619]) ).
fof(f17639,plain,
index_189 = s(index_12),
inference(backward_demodulation,[status(thm)],[f17629,f12909]) ).
fof(f17652,plain,
index_189 = index_18,
inference(forward_demodulation,[status(thm)],[f4562,f17639]) ).
fof(f17665,plain,
index_210 = s(index_18),
inference(backward_demodulation,[status(thm)],[f17652,f13082]) ).
fof(f17675,plain,
index_210 = index_24,
inference(forward_demodulation,[status(thm)],[f4689,f17665]) ).
fof(f19270,plain,
index_33 = s(index_210),
inference(backward_demodulation,[status(thm)],[f17675,f7015]) ).
fof(f19280,plain,
index_33 = index_282,
inference(forward_demodulation,[status(thm)],[f13615,f19270]) ).
fof(f19292,plain,
index_54 != index_282,
inference(backward_demodulation,[status(thm)],[f19280,f11840]) ).
fof(f19297,plain,
index_45 != index_282,
inference(backward_demodulation,[status(thm)],[f19280,f7168]) ).
fof(f19299,plain,
index_39 = s(index_282),
inference(backward_demodulation,[status(thm)],[f19280,f5328]) ).
fof(f19300,plain,
index_39 != index_282,
inference(backward_demodulation,[status(thm)],[f19280,f5327]) ).
fof(f19301,plain,
select(earray_37,index_282) = e13,
inference(backward_demodulation,[status(thm)],[f19280,f5331]) ).
fof(f19482,plain,
s(s(s(index_39))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f478]) ).
fof(f19483,plain,
s(s(s(s(index_39)))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f477]) ).
fof(f19484,plain,
s(s(s(s(s(index_39))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f476]) ).
fof(f19485,plain,
s(s(s(s(s(s(index_39)))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f475]) ).
fof(f19486,plain,
s(s(s(s(s(s(s(index_39))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f474]) ).
fof(f19487,plain,
s(s(s(s(s(s(s(s(index_39)))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f473]) ).
fof(f19488,plain,
s(s(s(s(s(s(s(s(s(index_39))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f472]) ).
fof(f19489,plain,
s(s(s(s(s(s(s(s(s(s(index_39)))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f471]) ).
fof(f19490,plain,
s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f470]) ).
fof(f19491,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f469]) ).
fof(f19492,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f468]) ).
fof(f19493,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f467]) ).
fof(f19494,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f466]) ).
fof(f19495,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f465]) ).
fof(f19496,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f464]) ).
fof(f19497,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f463]) ).
fof(f19498,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f462]) ).
fof(f19499,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f461]) ).
fof(f19500,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f460]) ).
fof(f19501,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f459]) ).
fof(f19502,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f458]) ).
fof(f19503,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f457]) ).
fof(f19504,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))))))))) != index_282,
inference(paramodulation,[status(thm)],[f19299,f456]) ).
fof(f20482,plain,
s(s(index_45)) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19482]) ).
fof(f20483,plain,
s(index_54) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20482]) ).
fof(f20484,plain,
index_60 != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20483]) ).
fof(f20485,plain,
s(s(s(index_45))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19483]) ).
fof(f20486,plain,
s(s(index_54)) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20485]) ).
fof(f20487,plain,
s(index_60) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20486]) ).
fof(f20488,plain,
index_66 != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20487]) ).
fof(f20489,plain,
s(s(s(s(index_45)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19484]) ).
fof(f20490,plain,
s(s(s(index_54))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20489]) ).
fof(f20491,plain,
s(s(index_60)) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20490]) ).
fof(f20492,plain,
s(index_66) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20491]) ).
fof(f20493,plain,
index_75 != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20492]) ).
fof(f20494,plain,
s(s(s(s(s(index_45))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19485]) ).
fof(f20495,plain,
s(s(s(s(index_54)))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20494]) ).
fof(f20496,plain,
s(s(s(index_60))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20495]) ).
fof(f20497,plain,
s(s(index_66)) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20496]) ).
fof(f20498,plain,
s(index_75) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20497]) ).
fof(f20499,plain,
index_87 != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20498]) ).
fof(f20500,plain,
s(s(s(s(s(s(index_45)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19486]) ).
fof(f20501,plain,
s(s(s(s(s(index_54))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20500]) ).
fof(f20502,plain,
s(s(s(s(index_60)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20501]) ).
fof(f20503,plain,
s(s(s(index_66))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20502]) ).
fof(f20504,plain,
s(s(index_75)) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20503]) ).
fof(f20505,plain,
s(index_87) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20504]) ).
fof(f20506,plain,
index_93 != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20505]) ).
fof(f20507,plain,
s(s(s(s(s(s(s(index_45))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19487]) ).
fof(f20508,plain,
s(s(s(s(s(s(index_54)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20507]) ).
fof(f20509,plain,
s(s(s(s(s(index_60))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20508]) ).
fof(f20510,plain,
s(s(s(s(index_66)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20509]) ).
fof(f20511,plain,
s(s(s(index_75))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20510]) ).
fof(f20512,plain,
s(s(index_87)) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20511]) ).
fof(f20513,plain,
s(index_93) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20512]) ).
fof(f20514,plain,
index_102 != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20513]) ).
fof(f20515,plain,
s(s(s(s(s(s(s(s(index_45)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19488]) ).
fof(f20516,plain,
s(s(s(s(s(s(s(index_54))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20515]) ).
fof(f20517,plain,
s(s(s(s(s(s(index_60)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20516]) ).
fof(f20518,plain,
s(s(s(s(s(index_66))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20517]) ).
fof(f20519,plain,
s(s(s(s(index_75)))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20518]) ).
fof(f20520,plain,
s(s(s(index_87))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20519]) ).
fof(f20521,plain,
s(s(index_93)) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20520]) ).
fof(f20522,plain,
s(index_102) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20521]) ).
fof(f20523,plain,
index_108 != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20522]) ).
fof(f20524,plain,
s(s(s(s(s(s(s(s(s(index_45))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19489]) ).
fof(f20525,plain,
s(s(s(s(s(s(s(s(index_54)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20524]) ).
fof(f20526,plain,
s(s(s(s(s(s(s(index_60))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20525]) ).
fof(f20527,plain,
s(s(s(s(s(s(index_66)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20526]) ).
fof(f20528,plain,
s(s(s(s(s(index_75))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20527]) ).
fof(f20529,plain,
s(s(s(s(index_87)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20528]) ).
fof(f20530,plain,
s(s(s(index_93))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20529]) ).
fof(f20531,plain,
s(s(index_102)) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20530]) ).
fof(f20532,plain,
s(index_108) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20531]) ).
fof(f20533,plain,
index_114 != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20532]) ).
fof(f20534,plain,
s(s(s(s(s(s(s(s(s(s(index_45)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19490]) ).
fof(f20535,plain,
s(s(s(s(s(s(s(s(s(index_54))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20534]) ).
fof(f20536,plain,
s(s(s(s(s(s(s(s(index_60)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20535]) ).
fof(f20537,plain,
s(s(s(s(s(s(s(index_66))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20536]) ).
fof(f20538,plain,
s(s(s(s(s(s(index_75)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20537]) ).
fof(f20539,plain,
s(s(s(s(s(index_87))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20538]) ).
fof(f20540,plain,
s(s(s(s(index_93)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20539]) ).
fof(f20541,plain,
s(s(s(index_102))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20540]) ).
fof(f20542,plain,
s(s(index_108)) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20541]) ).
fof(f20543,plain,
s(index_114) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20542]) ).
fof(f20544,plain,
index_123 != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20543]) ).
fof(f20545,plain,
s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19491]) ).
fof(f20546,plain,
s(s(s(s(s(s(s(s(s(s(index_54)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20545]) ).
fof(f20547,plain,
s(s(s(s(s(s(s(s(s(index_60))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20546]) ).
fof(f20548,plain,
s(s(s(s(s(s(s(s(index_66)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20547]) ).
fof(f20549,plain,
s(s(s(s(s(s(s(index_75))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20548]) ).
fof(f20550,plain,
s(s(s(s(s(s(index_87)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20549]) ).
fof(f20551,plain,
s(s(s(s(s(index_93))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20550]) ).
fof(f20552,plain,
s(s(s(s(index_102)))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20551]) ).
fof(f20553,plain,
s(s(s(index_108))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20552]) ).
fof(f20554,plain,
s(s(index_114)) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20553]) ).
fof(f20555,plain,
s(index_123) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20554]) ).
fof(f20556,plain,
index_129 != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20555]) ).
fof(f20557,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19492]) ).
fof(f20558,plain,
s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20557]) ).
fof(f20559,plain,
s(s(s(s(s(s(s(s(s(s(index_60)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20558]) ).
fof(f20560,plain,
s(s(s(s(s(s(s(s(s(index_66))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20559]) ).
fof(f20561,plain,
s(s(s(s(s(s(s(s(index_75)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20560]) ).
fof(f20562,plain,
s(s(s(s(s(s(s(index_87))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20561]) ).
fof(f20563,plain,
s(s(s(s(s(s(index_93)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20562]) ).
fof(f20564,plain,
s(s(s(s(s(index_102))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20563]) ).
fof(f20565,plain,
s(s(s(s(index_108)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20564]) ).
fof(f20566,plain,
s(s(s(index_114))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20565]) ).
fof(f20567,plain,
s(s(index_123)) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20566]) ).
fof(f20568,plain,
s(index_129) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20567]) ).
fof(f20569,plain,
index_135 != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20568]) ).
fof(f20570,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19493]) ).
fof(f20571,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20570]) ).
fof(f20572,plain,
s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20571]) ).
fof(f20573,plain,
s(s(s(s(s(s(s(s(s(s(index_66)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20572]) ).
fof(f20574,plain,
s(s(s(s(s(s(s(s(s(index_75))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20573]) ).
fof(f20575,plain,
s(s(s(s(s(s(s(s(index_87)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20574]) ).
fof(f20576,plain,
s(s(s(s(s(s(s(index_93))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20575]) ).
fof(f20577,plain,
s(s(s(s(s(s(index_102)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20576]) ).
fof(f20578,plain,
s(s(s(s(s(index_108))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20577]) ).
fof(f20579,plain,
s(s(s(s(index_114)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20578]) ).
fof(f20580,plain,
s(s(s(index_123))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20579]) ).
fof(f20581,plain,
s(s(index_129)) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20580]) ).
fof(f20582,plain,
s(index_135) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20581]) ).
fof(f20583,plain,
index_144 != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20582]) ).
fof(f20584,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19494]) ).
fof(f20585,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20584]) ).
fof(f20586,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20585]) ).
fof(f20587,plain,
s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20586]) ).
fof(f20588,plain,
s(s(s(s(s(s(s(s(s(s(index_75)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20587]) ).
fof(f20589,plain,
s(s(s(s(s(s(s(s(s(index_87))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20588]) ).
fof(f20590,plain,
s(s(s(s(s(s(s(s(index_93)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20589]) ).
fof(f20591,plain,
s(s(s(s(s(s(s(index_102))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20590]) ).
fof(f20592,plain,
s(s(s(s(s(s(index_108)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20591]) ).
fof(f20593,plain,
s(s(s(s(s(index_114))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20592]) ).
fof(f20594,plain,
s(s(s(s(index_123)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20593]) ).
fof(f20595,plain,
s(s(s(index_129))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20594]) ).
fof(f20596,plain,
s(s(index_135)) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20595]) ).
fof(f20597,plain,
s(index_144) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20596]) ).
fof(f20598,plain,
index_150 != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20597]) ).
fof(f20599,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19495]) ).
fof(f20600,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20599]) ).
fof(f20601,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20600]) ).
fof(f20602,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20601]) ).
fof(f20603,plain,
s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20602]) ).
fof(f20604,plain,
s(s(s(s(s(s(s(s(s(s(index_87)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20603]) ).
fof(f20605,plain,
s(s(s(s(s(s(s(s(s(index_93))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20604]) ).
fof(f20606,plain,
s(s(s(s(s(s(s(s(index_102)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20605]) ).
fof(f20607,plain,
s(s(s(s(s(s(s(index_108))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20606]) ).
fof(f20608,plain,
s(s(s(s(s(s(index_114)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20607]) ).
fof(f20609,plain,
s(s(s(s(s(index_123))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20608]) ).
fof(f20610,plain,
s(s(s(s(index_129)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20609]) ).
fof(f20611,plain,
s(s(s(index_135))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20610]) ).
fof(f20612,plain,
s(s(index_144)) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20611]) ).
fof(f20613,plain,
s(index_150) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20612]) ).
fof(f20614,plain,
index_165 != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20613]) ).
fof(f20615,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19496]) ).
fof(f20616,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20615]) ).
fof(f20617,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20616]) ).
fof(f20618,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20617]) ).
fof(f20619,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20618]) ).
fof(f20620,plain,
s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20619]) ).
fof(f20621,plain,
s(s(s(s(s(s(s(s(s(s(index_93)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20620]) ).
fof(f20622,plain,
s(s(s(s(s(s(s(s(s(index_102))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20621]) ).
fof(f20623,plain,
s(s(s(s(s(s(s(s(index_108)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20622]) ).
fof(f20624,plain,
s(s(s(s(s(s(s(index_114))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20623]) ).
fof(f20625,plain,
s(s(s(s(s(s(index_123)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20624]) ).
fof(f20626,plain,
s(s(s(s(s(index_129))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20625]) ).
fof(f20627,plain,
s(s(s(s(index_135)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20626]) ).
fof(f20628,plain,
s(s(s(index_144))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20627]) ).
fof(f20629,plain,
s(s(index_150)) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20628]) ).
fof(f20630,plain,
s(index_165) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20629]) ).
fof(f20631,plain,
index_174 != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20630]) ).
fof(f20632,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19497]) ).
fof(f20633,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20632]) ).
fof(f20634,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20633]) ).
fof(f20635,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20634]) ).
fof(f20636,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20635]) ).
fof(f20637,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20636]) ).
fof(f20638,plain,
s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20637]) ).
fof(f20639,plain,
s(s(s(s(s(s(s(s(s(s(index_102)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20638]) ).
fof(f20640,plain,
s(s(s(s(s(s(s(s(s(index_108))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20639]) ).
fof(f20641,plain,
s(s(s(s(s(s(s(s(index_114)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20640]) ).
fof(f20642,plain,
s(s(s(s(s(s(s(index_123))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20641]) ).
fof(f20643,plain,
s(s(s(s(s(s(index_129)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20642]) ).
fof(f20644,plain,
s(s(s(s(s(index_135))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20643]) ).
fof(f20645,plain,
s(s(s(s(index_144)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20644]) ).
fof(f20646,plain,
s(s(s(index_150))) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20645]) ).
fof(f20647,plain,
s(s(index_165)) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20646]) ).
fof(f20648,plain,
s(index_174) != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20647]) ).
fof(f20649,plain,
index_180 != index_282,
inference(forward_demodulation,[status(thm)],[f4656,f20648]) ).
fof(f20650,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19498]) ).
fof(f20651,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20650]) ).
fof(f20652,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20651]) ).
fof(f20653,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20652]) ).
fof(f20654,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20653]) ).
fof(f20655,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20654]) ).
fof(f20656,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20655]) ).
fof(f20657,plain,
s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20656]) ).
fof(f20658,plain,
s(s(s(s(s(s(s(s(s(s(index_108)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20657]) ).
fof(f20659,plain,
s(s(s(s(s(s(s(s(s(index_114))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20658]) ).
fof(f20660,plain,
s(s(s(s(s(s(s(s(index_123)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20659]) ).
fof(f20661,plain,
s(s(s(s(s(s(s(index_129))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20660]) ).
fof(f20662,plain,
s(s(s(s(s(s(index_135)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20661]) ).
fof(f20663,plain,
s(s(s(s(s(index_144))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20662]) ).
fof(f20664,plain,
s(s(s(s(index_150)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20663]) ).
fof(f20665,plain,
s(s(s(index_165))) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20664]) ).
fof(f20666,plain,
s(s(index_174)) != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20665]) ).
fof(f20667,plain,
s(index_180) != index_282,
inference(forward_demodulation,[status(thm)],[f4656,f20666]) ).
fof(f20668,plain,
index_186 != index_282,
inference(forward_demodulation,[status(thm)],[f4671,f20667]) ).
fof(f20669,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19499]) ).
fof(f20670,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20669]) ).
fof(f20671,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20670]) ).
fof(f20672,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20671]) ).
fof(f20673,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20672]) ).
fof(f20674,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20673]) ).
fof(f20675,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20674]) ).
fof(f20676,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20675]) ).
fof(f20677,plain,
s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20676]) ).
fof(f20678,plain,
s(s(s(s(s(s(s(s(s(s(index_114)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20677]) ).
fof(f20679,plain,
s(s(s(s(s(s(s(s(s(index_123))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20678]) ).
fof(f20680,plain,
s(s(s(s(s(s(s(s(index_129)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20679]) ).
fof(f20681,plain,
s(s(s(s(s(s(s(index_135))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20680]) ).
fof(f20682,plain,
s(s(s(s(s(s(index_144)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20681]) ).
fof(f20683,plain,
s(s(s(s(s(index_150))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20682]) ).
fof(f20684,plain,
s(s(s(s(index_165)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20683]) ).
fof(f20685,plain,
s(s(s(index_174))) != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20684]) ).
fof(f20686,plain,
s(s(index_180)) != index_282,
inference(forward_demodulation,[status(thm)],[f4656,f20685]) ).
fof(f20687,plain,
s(index_186) != index_282,
inference(forward_demodulation,[status(thm)],[f4671,f20686]) ).
fof(f20688,plain,
index_195 != index_282,
inference(forward_demodulation,[status(thm)],[f5867,f20687]) ).
fof(f20689,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19500]) ).
fof(f20690,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20689]) ).
fof(f20691,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20690]) ).
fof(f20692,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20691]) ).
fof(f20693,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20692]) ).
fof(f20694,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20693]) ).
fof(f20695,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20694]) ).
fof(f20696,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20695]) ).
fof(f20697,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_108)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20696]) ).
fof(f20698,plain,
s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20697]) ).
fof(f20699,plain,
s(s(s(s(s(s(s(s(s(s(index_123)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20698]) ).
fof(f20700,plain,
s(s(s(s(s(s(s(s(s(index_129))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20699]) ).
fof(f20701,plain,
s(s(s(s(s(s(s(s(index_135)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20700]) ).
fof(f20702,plain,
s(s(s(s(s(s(s(index_144))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20701]) ).
fof(f20703,plain,
s(s(s(s(s(s(index_150)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20702]) ).
fof(f20704,plain,
s(s(s(s(s(index_165))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20703]) ).
fof(f20705,plain,
s(s(s(s(index_174)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20704]) ).
fof(f20706,plain,
s(s(s(index_180))) != index_282,
inference(forward_demodulation,[status(thm)],[f4656,f20705]) ).
fof(f20707,plain,
s(s(index_186)) != index_282,
inference(forward_demodulation,[status(thm)],[f4671,f20706]) ).
fof(f20708,plain,
s(index_195) != index_282,
inference(forward_demodulation,[status(thm)],[f5867,f20707]) ).
fof(f20709,plain,
index_201 != index_282,
inference(forward_demodulation,[status(thm)],[f4709,f20708]) ).
fof(f20710,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19501]) ).
fof(f20711,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20710]) ).
fof(f20712,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20711]) ).
fof(f20713,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20712]) ).
fof(f20714,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20713]) ).
fof(f20715,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20714]) ).
fof(f20716,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20715]) ).
fof(f20717,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20716]) ).
fof(f20718,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20717]) ).
fof(f20719,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20718]) ).
fof(f20720,plain,
s(s(s(s(s(s(s(s(s(s(s(index_123))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20719]) ).
fof(f20721,plain,
s(s(s(s(s(s(s(s(s(s(index_129)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20720]) ).
fof(f20722,plain,
s(s(s(s(s(s(s(s(s(index_135))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20721]) ).
fof(f20723,plain,
s(s(s(s(s(s(s(s(index_144)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20722]) ).
fof(f20724,plain,
s(s(s(s(s(s(s(index_150))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20723]) ).
fof(f20725,plain,
s(s(s(s(s(s(index_165)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20724]) ).
fof(f20726,plain,
s(s(s(s(s(index_174))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20725]) ).
fof(f20727,plain,
s(s(s(s(index_180)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4656,f20726]) ).
fof(f20728,plain,
s(s(s(index_186))) != index_282,
inference(forward_demodulation,[status(thm)],[f4671,f20727]) ).
fof(f20729,plain,
s(s(index_195)) != index_282,
inference(forward_demodulation,[status(thm)],[f5867,f20728]) ).
fof(f20730,plain,
s(index_201) != index_282,
inference(forward_demodulation,[status(thm)],[f4709,f20729]) ).
fof(f20731,plain,
index_207 != index_282,
inference(forward_demodulation,[status(thm)],[f4728,f20730]) ).
fof(f20732,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19502]) ).
fof(f20733,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20732]) ).
fof(f20734,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20733]) ).
fof(f20735,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20734]) ).
fof(f20736,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20735]) ).
fof(f20737,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20736]) ).
fof(f20738,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20737]) ).
fof(f20739,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20738]) ).
fof(f20740,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20739]) ).
fof(f20741,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20740]) ).
fof(f20742,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_123)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20741]) ).
fof(f20743,plain,
s(s(s(s(s(s(s(s(s(s(s(index_129))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20742]) ).
fof(f20744,plain,
s(s(s(s(s(s(s(s(s(s(index_135)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20743]) ).
fof(f20745,plain,
s(s(s(s(s(s(s(s(s(index_144))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20744]) ).
fof(f20746,plain,
s(s(s(s(s(s(s(s(index_150)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20745]) ).
fof(f20747,plain,
s(s(s(s(s(s(s(index_165))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20746]) ).
fof(f20748,plain,
s(s(s(s(s(s(index_174)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20747]) ).
fof(f20749,plain,
s(s(s(s(s(index_180))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4656,f20748]) ).
fof(f20750,plain,
s(s(s(s(index_186)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4671,f20749]) ).
fof(f20751,plain,
s(s(s(index_195))) != index_282,
inference(forward_demodulation,[status(thm)],[f5867,f20750]) ).
fof(f20752,plain,
s(s(index_201)) != index_282,
inference(forward_demodulation,[status(thm)],[f4709,f20751]) ).
fof(f20753,plain,
s(index_207) != index_282,
inference(forward_demodulation,[status(thm)],[f4728,f20752]) ).
fof(f20754,plain,
index_216 != index_282,
inference(forward_demodulation,[status(thm)],[f6026,f20753]) ).
fof(f20755,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19503]) ).
fof(f20756,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20755]) ).
fof(f20757,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20756]) ).
fof(f20758,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20757]) ).
fof(f20759,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20758]) ).
fof(f20760,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20759]) ).
fof(f20761,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20760]) ).
fof(f20762,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20761]) ).
fof(f20763,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20762]) ).
fof(f20764,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20763]) ).
fof(f20765,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_123))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20764]) ).
fof(f20766,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_129)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20765]) ).
fof(f20767,plain,
s(s(s(s(s(s(s(s(s(s(s(index_135))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20766]) ).
fof(f20768,plain,
s(s(s(s(s(s(s(s(s(s(index_144)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20767]) ).
fof(f20769,plain,
s(s(s(s(s(s(s(s(s(index_150))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20768]) ).
fof(f20770,plain,
s(s(s(s(s(s(s(s(index_165)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20769]) ).
fof(f20771,plain,
s(s(s(s(s(s(s(index_174))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20770]) ).
fof(f20772,plain,
s(s(s(s(s(s(index_180)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4656,f20771]) ).
fof(f20773,plain,
s(s(s(s(s(index_186))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4671,f20772]) ).
fof(f20774,plain,
s(s(s(s(index_195)))) != index_282,
inference(forward_demodulation,[status(thm)],[f5867,f20773]) ).
fof(f20775,plain,
s(s(s(index_201))) != index_282,
inference(forward_demodulation,[status(thm)],[f4709,f20774]) ).
fof(f20776,plain,
s(s(index_207)) != index_282,
inference(forward_demodulation,[status(thm)],[f4728,f20775]) ).
fof(f20777,plain,
s(index_216) != index_282,
inference(forward_demodulation,[status(thm)],[f6026,f20776]) ).
fof(f20778,plain,
index_222 != index_282,
inference(forward_demodulation,[status(thm)],[f4900,f20777]) ).
fof(f20779,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5349,f19504]) ).
fof(f20780,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f7443,f20779]) ).
fof(f20781,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5454,f20780]) ).
fof(f20782,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5474,f20781]) ).
fof(f20783,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8058,f20782]) ).
fof(f20784,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5584,f20783]) ).
fof(f20785,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5609,f20784]) ).
fof(f20786,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f8483,f20785]) ).
fof(f20787,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108)))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4505,f20786]) ).
fof(f20788,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4510,f20787]) ).
fof(f20789,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_123)))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5014,f20788]) ).
fof(f20790,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_129))))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4543,f20789]) ).
fof(f20791,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_135)))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4567,f20790]) ).
fof(f20792,plain,
s(s(s(s(s(s(s(s(s(s(s(index_144))))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5308,f20791]) ).
fof(f20793,plain,
s(s(s(s(s(s(s(s(s(s(index_150)))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4600,f20792]) ).
fof(f20794,plain,
s(s(s(s(s(s(s(s(s(index_165))))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4619,f20793]) ).
fof(f20795,plain,
s(s(s(s(s(s(s(s(index_174)))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5615,f20794]) ).
fof(f20796,plain,
s(s(s(s(s(s(s(index_180))))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4656,f20795]) ).
fof(f20797,plain,
s(s(s(s(s(s(index_186)))))) != index_282,
inference(forward_demodulation,[status(thm)],[f4671,f20796]) ).
fof(f20798,plain,
s(s(s(s(s(index_195))))) != index_282,
inference(forward_demodulation,[status(thm)],[f5867,f20797]) ).
fof(f20799,plain,
s(s(s(s(index_201)))) != index_282,
inference(forward_demodulation,[status(thm)],[f4709,f20798]) ).
fof(f20800,plain,
s(s(s(index_207))) != index_282,
inference(forward_demodulation,[status(thm)],[f4728,f20799]) ).
fof(f20801,plain,
s(s(index_216)) != index_282,
inference(forward_demodulation,[status(thm)],[f6026,f20800]) ).
fof(f20802,plain,
s(index_222) != index_282,
inference(forward_demodulation,[status(thm)],[f4900,f20801]) ).
fof(f20803,plain,
index_228 != index_282,
inference(forward_demodulation,[status(thm)],[f4905,f20802]) ).
fof(f23012,plain,
earray_98 = rselect_seq(queue_92),
inference(forward_demodulation,[status(thm)],[f5630,f5623]) ).
fof(f23017,plain,
earray_98 = earray_91,
inference(forward_demodulation,[status(thm)],[f5621,f23012]) ).
fof(f27557,plain,
! [X0] :
( select(earray_100,X0) = select(earray_98,X0)
| index_93 = X0 ),
inference(forward_demodulation,[status(thm)],[f8484,f2458]) ).
fof(f27600,plain,
! [X0] :
( select(earray_106,X0) = select(earray_104,X0)
| index_102 = X0 ),
inference(forward_demodulation,[status(thm)],[f4491,f2527]) ).
fof(f27601,plain,
! [X0] :
( select(earray_106,X0) = select(earray_100,X0)
| index_102 = X0 ),
inference(forward_demodulation,[status(thm)],[f4801,f27600]) ).
fof(f27604,plain,
! [X0] :
( select(earray_112,X0) = select(earray_110,X0)
| index_108 = X0 ),
inference(forward_demodulation,[status(thm)],[f4501,f2529]) ).
fof(f27605,plain,
! [X0] :
( select(earray_112,X0) = select(earray_106,X0)
| index_108 = X0 ),
inference(forward_demodulation,[status(thm)],[f4814,f27604]) ).
fof(f27608,plain,
! [X0] :
( select(earray_121,X0) = select(earray_119,X0)
| index_114 = X0 ),
inference(forward_demodulation,[status(thm)],[f5016,f2665]) ).
fof(f27609,plain,
! [X0] :
( select(earray_121,X0) = select(earray_112,X0)
| index_114 = X0 ),
inference(forward_demodulation,[status(thm)],[f12417,f27608]) ).
fof(f27612,plain,
! [X0] :
( select(earray_127,X0) = select(earray_125,X0)
| index_123 = X0 ),
inference(forward_demodulation,[status(thm)],[f4539,f2667]) ).
fof(f27613,plain,
! [X0] :
( select(earray_127,X0) = select(earray_121,X0)
| index_123 = X0 ),
inference(forward_demodulation,[status(thm)],[f5028,f27612]) ).
fof(f27671,plain,
! [X0] :
( select(earray_133,X0) = select(earray_131,X0)
| index_129 = X0 ),
inference(forward_demodulation,[status(thm)],[f4558,f2669]) ).
fof(f27672,plain,
! [X0] :
( select(earray_133,X0) = select(earray_127,X0)
| index_129 = X0 ),
inference(forward_demodulation,[status(thm)],[f5121,f27671]) ).
fof(f27675,plain,
! [X0] :
( select(earray_142,X0) = select(earray_140,X0)
| index_135 = X0 ),
inference(forward_demodulation,[status(thm)],[f5310,f2737]) ).
fof(f27676,plain,
! [X0] :
( select(earray_142,X0) = select(earray_133,X0)
| index_135 = X0 ),
inference(forward_demodulation,[status(thm)],[f12610,f27675]) ).
fof(f27702,plain,
! [X0] :
( select(earray_148,X0) = select(earray_146,X0)
| index_144 = X0 ),
inference(forward_demodulation,[status(thm)],[f4591,f2806]) ).
fof(f27703,plain,
! [X0] :
( select(earray_148,X0) = select(earray_142,X0)
| index_144 = X0 ),
inference(forward_demodulation,[status(thm)],[f5353,f27702]) ).
fof(f27713,plain,
! [X0] :
( select(earray_163,X0) = select(earray_161,X0)
| index_150 = X0 ),
inference(forward_demodulation,[status(thm)],[f4606,f2946]) ).
fof(f27714,plain,
! [X0] :
( select(earray_163,X0) = select(earray_148,X0)
| index_150 = X0 ),
inference(forward_demodulation,[status(thm)],[f5441,f27713]) ).
fof(f27752,plain,
! [X0] :
( select(earray_172,X0) = select(earray_170,X0)
| index_165 = X0 ),
inference(forward_demodulation,[status(thm)],[f5617,f2948]) ).
fof(f27753,plain,
! [X0] :
( select(earray_172,X0) = select(earray_163,X0)
| index_165 = X0 ),
inference(forward_demodulation,[status(thm)],[f12808,f27752]) ).
fof(f27756,plain,
! [X0] :
( select(earray_178,X0) = select(earray_176,X0)
| index_174 = X0 ),
inference(forward_demodulation,[status(thm)],[f4652,f3016]) ).
fof(f27757,plain,
! [X0] :
( select(earray_178,X0) = select(earray_172,X0)
| index_174 = X0 ),
inference(forward_demodulation,[status(thm)],[f5635,f27756]) ).
fof(f27760,plain,
! [X0] :
( select(earray_184,X0) = select(earray_182,X0)
| index_180 = X0 ),
inference(forward_demodulation,[status(thm)],[f4667,f3085]) ).
fof(f27761,plain,
! [X0] :
( select(earray_184,X0) = select(earray_178,X0)
| index_180 = X0 ),
inference(forward_demodulation,[status(thm)],[f5709,f27760]) ).
fof(f27764,plain,
! [X0] :
( select(earray_193,X0) = select(earray_191,X0)
| index_186 = X0 ),
inference(forward_demodulation,[status(thm)],[f5869,f3087]) ).
fof(f27765,plain,
! [X0] :
( select(earray_193,X0) = select(earray_184,X0)
| index_186 = X0 ),
inference(forward_demodulation,[status(thm)],[f13017,f27764]) ).
fof(f27768,plain,
! [X0] :
( select(earray_199,X0) = select(earray_197,X0)
| index_195 = X0 ),
inference(forward_demodulation,[status(thm)],[f4705,f3222]) ).
fof(f27769,plain,
! [X0] :
( select(earray_199,X0) = select(earray_193,X0)
| index_195 = X0 ),
inference(forward_demodulation,[status(thm)],[f5947,f27768]) ).
fof(f27772,plain,
! [X0] :
( select(earray_205,X0) = select(earray_203,X0)
| index_201 = X0 ),
inference(forward_demodulation,[status(thm)],[f4719,f3224]) ).
fof(f27773,plain,
! [X0] :
( select(earray_205,X0) = select(earray_199,X0)
| index_201 = X0 ),
inference(forward_demodulation,[status(thm)],[f6019,f27772]) ).
fof(f27832,plain,
! [X0] :
( select(earray_214,X0) = select(earray_212,X0)
| index_207 = X0 ),
inference(forward_demodulation,[status(thm)],[f6028,f3226]) ).
fof(f27833,plain,
! [X0] :
( select(earray_214,X0) = select(earray_205,X0)
| index_207 = X0 ),
inference(forward_demodulation,[status(thm)],[f13156,f27832]) ).
fof(f27855,plain,
! [X0] :
( select(earray_220,X0) = select(earray_218,X0)
| index_216 = X0 ),
inference(forward_demodulation,[status(thm)],[f4886,f3364]) ).
fof(f27856,plain,
! [X0] :
( select(earray_220,X0) = select(earray_214,X0)
| index_216 = X0 ),
inference(forward_demodulation,[status(thm)],[f6098,f27855]) ).
fof(f27859,plain,
! [X0] :
( select(earray_226,X0) = select(earray_224,X0)
| index_222 = X0 ),
inference(forward_demodulation,[status(thm)],[f4896,f3366]) ).
fof(f27860,plain,
! [X0] :
( select(earray_226,X0) = select(earray_220,X0)
| index_222 = X0 ),
inference(forward_demodulation,[status(thm)],[f6101,f27859]) ).
fof(f27867,plain,
! [X0] :
( select(earray_241,X0) = select(earray_239,X0)
| index_228 = X0 ),
inference(forward_demodulation,[status(thm)],[f6245,f3503]) ).
fof(f27868,plain,
! [X0] :
( select(earray_241,X0) = select(earray_226,X0)
| index_228 = X0 ),
inference(forward_demodulation,[status(thm)],[f13368,f27867]) ).
fof(f27870,plain,
( elem_283 = select(earray_226,index_282)
| index_228 = index_282 ),
inference(paramodulation,[status(thm)],[f6520,f27868]) ).
fof(f27873,plain,
elem_283 = select(earray_226,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27870,f20803]) ).
fof(f27875,plain,
( index_222 = index_282
| elem_283 = select(earray_220,index_282) ),
inference(paramodulation,[status(thm)],[f27860,f27873]) ).
fof(f27877,plain,
elem_283 = select(earray_220,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27875,f20778]) ).
fof(f27879,plain,
( index_216 = index_282
| elem_283 = select(earray_214,index_282) ),
inference(paramodulation,[status(thm)],[f27856,f27877]) ).
fof(f27881,plain,
elem_283 = select(earray_214,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27879,f20754]) ).
fof(f27883,plain,
( index_207 = index_282
| elem_283 = select(earray_205,index_282) ),
inference(paramodulation,[status(thm)],[f27833,f27881]) ).
fof(f27885,plain,
elem_283 = select(earray_205,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27883,f20731]) ).
fof(f27887,plain,
( index_201 = index_282
| elem_283 = select(earray_199,index_282) ),
inference(paramodulation,[status(thm)],[f27773,f27885]) ).
fof(f27889,plain,
elem_283 = select(earray_199,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27887,f20709]) ).
fof(f27952,plain,
( index_195 = index_282
| elem_283 = select(earray_193,index_282) ),
inference(paramodulation,[status(thm)],[f27769,f27889]) ).
fof(f27954,plain,
elem_283 = select(earray_193,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27952,f20688]) ).
fof(f27956,plain,
( index_186 = index_282
| elem_283 = select(earray_184,index_282) ),
inference(paramodulation,[status(thm)],[f27765,f27954]) ).
fof(f27958,plain,
elem_283 = select(earray_184,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27956,f20668]) ).
fof(f27960,plain,
( index_180 = index_282
| elem_283 = select(earray_178,index_282) ),
inference(paramodulation,[status(thm)],[f27761,f27958]) ).
fof(f27962,plain,
elem_283 = select(earray_178,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27960,f20649]) ).
fof(f27964,plain,
( index_174 = index_282
| elem_283 = select(earray_172,index_282) ),
inference(paramodulation,[status(thm)],[f27757,f27962]) ).
fof(f27966,plain,
elem_283 = select(earray_172,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27964,f20631]) ).
fof(f27968,plain,
( index_165 = index_282
| elem_283 = select(earray_163,index_282) ),
inference(paramodulation,[status(thm)],[f27753,f27966]) ).
fof(f27970,plain,
elem_283 = select(earray_163,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27968,f20614]) ).
fof(f27972,plain,
( index_150 = index_282
| elem_283 = select(earray_148,index_282) ),
inference(paramodulation,[status(thm)],[f27714,f27970]) ).
fof(f27974,plain,
elem_283 = select(earray_148,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27972,f20598]) ).
fof(f27976,plain,
( index_144 = index_282
| elem_283 = select(earray_142,index_282) ),
inference(paramodulation,[status(thm)],[f27703,f27974]) ).
fof(f27978,plain,
elem_283 = select(earray_142,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27976,f20583]) ).
fof(f27980,plain,
( index_135 = index_282
| elem_283 = select(earray_133,index_282) ),
inference(paramodulation,[status(thm)],[f27676,f27978]) ).
fof(f27982,plain,
elem_283 = select(earray_133,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f27980,f20569]) ).
fof(f28038,plain,
( index_129 = index_282
| elem_283 = select(earray_127,index_282) ),
inference(paramodulation,[status(thm)],[f27672,f27982]) ).
fof(f28040,plain,
elem_283 = select(earray_127,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f28038,f20556]) ).
fof(f28042,plain,
( index_123 = index_282
| elem_283 = select(earray_121,index_282) ),
inference(paramodulation,[status(thm)],[f27613,f28040]) ).
fof(f28044,plain,
elem_283 = select(earray_121,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f28042,f20544]) ).
fof(f28046,plain,
( index_114 = index_282
| elem_283 = select(earray_112,index_282) ),
inference(paramodulation,[status(thm)],[f27609,f28044]) ).
fof(f28048,plain,
elem_283 = select(earray_112,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f28046,f20533]) ).
fof(f28050,plain,
( index_108 = index_282
| elem_283 = select(earray_106,index_282) ),
inference(paramodulation,[status(thm)],[f27605,f28048]) ).
fof(f28052,plain,
elem_283 = select(earray_106,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f28050,f20523]) ).
fof(f28054,plain,
( index_102 = index_282
| elem_283 = select(earray_100,index_282) ),
inference(paramodulation,[status(thm)],[f27601,f28052]) ).
fof(f28056,plain,
elem_283 = select(earray_100,index_282),
inference(forward_subsumption_resolution,[status(thm)],[f28054,f20514]) ).
fof(f28172,plain,
! [X0] :
( select(earray_43,X0) = select(earray_41,X0)
| index_39 = X0 ),
inference(forward_demodulation,[status(thm)],[f5345,f3788]) ).
fof(f28173,plain,
! [X0] :
( select(earray_43,X0) = select(earray_37,X0)
| index_39 = X0 ),
inference(forward_demodulation,[status(thm)],[f7372,f28172]) ).
fof(f28176,plain,
! [X0] :
( select(earray_52,X0) = select(earray_50,X0)
| index_45 = X0 ),
inference(forward_demodulation,[status(thm)],[f7445,f3923]) ).
fof(f28177,plain,
! [X0] :
( select(earray_52,X0) = select(earray_43,X0)
| index_45 = X0 ),
inference(forward_demodulation,[status(thm)],[f14169,f28176]) ).
fof(f28180,plain,
! [X0] :
( select(earray_58,X0) = select(earray_56,X0)
| index_54 = X0 ),
inference(forward_demodulation,[status(thm)],[f5451,f3925]) ).
fof(f28181,plain,
! [X0] :
( select(earray_58,X0) = select(earray_52,X0)
| index_54 = X0 ),
inference(forward_demodulation,[status(thm)],[f7522,f28180]) ).
fof(f28223,plain,
! [X0] :
( select(earray_64,X0) = select(earray_62,X0)
| index_60 = X0 ),
inference(forward_demodulation,[status(thm)],[f5465,f4060]) ).
fof(f28224,plain,
! [X0] :
( select(earray_64,X0) = select(earray_58,X0)
| index_60 = X0 ),
inference(forward_demodulation,[status(thm)],[f7850,f28223]) ).
fof(f28227,plain,
! [X0] :
( select(earray_73,X0) = select(earray_71,X0)
| index_66 = X0 ),
inference(forward_demodulation,[status(thm)],[f8061,f4062]) ).
fof(f28228,plain,
! [X0] :
( select(earray_73,X0) = select(earray_64,X0)
| index_66 = X0 ),
inference(forward_demodulation,[status(thm)],[f14284,f28227]) ).
fof(f28253,plain,
! [X0] :
( select(earray_85,X0) = select(earray_83,X0)
| index_75 = X0 ),
inference(forward_demodulation,[status(thm)],[f5577,f4132]) ).
fof(f28254,plain,
! [X0] :
( select(earray_85,X0) = select(earray_73,X0)
| index_75 = X0 ),
inference(forward_demodulation,[status(thm)],[f8068,f28253]) ).
fof(f28283,plain,
! [X0] :
( select(earray_91,X0) = select(earray_89,X0)
| index_87 = X0 ),
inference(forward_demodulation,[status(thm)],[f5606,f4201]) ).
fof(f28284,plain,
! [X0] :
( select(earray_98,X0) = select(earray_89,X0)
| index_87 = X0 ),
inference(forward_demodulation,[status(thm)],[f23017,f28283]) ).
fof(f28285,plain,
! [X0] :
( select(earray_98,X0) = select(earray_85,X0)
| index_87 = X0 ),
inference(forward_demodulation,[status(thm)],[f8276,f28284]) ).
fof(f28287,plain,
! [X0] :
( index_75 = X0
| select(earray_98,X0) = select(earray_73,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f28254,f28285]) ).
fof(f32675,plain,
! [X0] :
( index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_64,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f28228,f28287]) ).
fof(f35445,plain,
! [X0] :
( index_60 = X0
| index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_58,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f28224,f32675]) ).
fof(f39576,plain,
! [X0] :
( index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_52,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f28181,f35445]) ).
fof(f41610,plain,
! [X0] :
( index_45 = X0
| index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_43,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f28177,f39576]) ).
fof(f45781,plain,
! [X0] :
( index_39 = X0
| index_45 = X0
| index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| select(earray_98,X0) = select(earray_37,X0)
| index_87 = X0 ),
inference(paramodulation,[status(thm)],[f28173,f41610]) ).
fof(f47371,plain,
( index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| index_75 = index_282
| select(earray_98,index_282) = e13
| index_87 = index_282 ),
inference(paramodulation,[status(thm)],[f19301,f45781]) ).
fof(f47375,plain,
( index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| index_75 = index_282
| select(earray_98,index_282) = e13 ),
inference(forward_subsumption_resolution,[status(thm)],[f47371,f20499]) ).
fof(f47404,plain,
( index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| select(earray_98,index_282) = e13 ),
inference(forward_subsumption_resolution,[status(thm)],[f47375,f20493]) ).
fof(f47405,plain,
( index_93 = index_282
| index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| select(earray_100,index_282) = e13 ),
inference(paramodulation,[status(thm)],[f27557,f47404]) ).
fof(f47407,plain,
( index_93 = index_282
| index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282
| elem_283 = e13 ),
inference(forward_demodulation,[status(thm)],[f28056,f47405]) ).
fof(f47408,plain,
( index_93 = index_282
| index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282
| index_66 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f47407,f807]) ).
fof(f47411,plain,
( index_93 = index_282
| index_39 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f47408,f20488]) ).
fof(f47412,plain,
( index_93 = index_282
| index_45 = index_282
| index_54 = index_282
| index_60 = index_282 ),
inference(resolution,[status(thm)],[f47411,f19300]) ).
fof(f47441,plain,
( index_93 = index_282
| index_45 = index_282
| index_54 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f47412,f20484]) ).
fof(f47454,plain,
( index_93 = index_282
| index_45 = index_282 ),
inference(forward_subsumption_resolution,[status(thm)],[f47441,f19292]) ).
fof(f47455,plain,
index_93 = index_282,
inference(resolution,[status(thm)],[f47454,f19297]) ).
fof(f47488,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f47455,f20506]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV568-1.040 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/10.36 % Computer : n002.cluster.edu
% 0.08/10.36 % Model : x86_64 x86_64
% 0.08/10.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.36 % Memory : 8046.5625MB
% 0.08/10.36 % OS : Linux 6.8.0-71-generic
% 0.08/10.36 % CPULimit : 300
% 0.08/10.36 % WCLimit : 300
% 0.08/10.36 % DateTime : Mon Sep 21 09:13:13 UTC 2026
% 0.08/10.36 % CPUTime :
% 0.08/10.37 % Drodi V4.1.1
% 28.64/14.10 % Refutation found
% 28.64/14.10 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 28.64/14.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 29.42/14.17 % Elapsed time: 3.799077 seconds
% 29.42/14.17 % CPU time: 29.896587 seconds
% 29.42/14.17 % Total memory used: 476.070 MB
% 29.42/14.17 % Net memory used: 473.276 MB
%------------------------------------------------------------------------------