%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV569-1.040 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:18:58 PM UTC 2026
% Result : Unsatisfiable 53.77s 8.27s
% Output : Refutation 54.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 334
% Syntax : Number of formulae : 1574 (1178 unt; 4 def)
% Number of atoms : 2086 (2015 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 979 ( 467 ~; 508 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 27 ( 4 avg)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 346 ( 346 usr; 343 con; 0-3 aty)
% Number of variables : 238 ( 0 sgn 238 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
head != tail,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_tail) ).
fof(f4,axiom,
head != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_seq) ).
fof(f5,axiom,
tail != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tail_distinct_from_seq) ).
fof(f46,axiom,
! [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,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as26) ).
fof(f47,axiom,
! [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,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as25) ).
fof(f48,axiom,
! [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,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as24) ).
fof(f49,axiom,
! [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,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as23) ).
fof(f50,axiom,
! [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,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as22) ).
fof(f51,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as21) ).
fof(f52,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as20) ).
fof(f53,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as19) ).
fof(f54,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as18) ).
fof(f55,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as17) ).
fof(f56,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as16) ).
fof(f57,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as15) ).
fof(f58,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as14) ).
fof(f59,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as13) ).
fof(f60,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as12) ).
fof(f61,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as11) ).
fof(f62,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as10) ).
fof(f63,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as9) ).
fof(f64,axiom,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as8) ).
fof(f65,axiom,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as7) ).
fof(f66,axiom,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as6) ).
fof(f67,axiom,
! [X0] : s(s(s(s(s(X0))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as5) ).
fof(f68,axiom,
! [X0] : s(s(s(s(X0)))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as4) ).
fof(f69,axiom,
! [X0] : s(s(s(X0))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as3) ).
fof(f70,axiom,
! [X0] : s(s(X0)) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as2) ).
fof(f71,axiom,
! [X0] : s(X0) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as1) ).
fof(f73,axiom,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f74,axiom,
earray_104 = select(q22,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f75,axiom,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f76,axiom,
earray_110 = select(q23,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f77,axiom,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f78,axiom,
earray_119 = select(q24,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f79,axiom,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f80,axiom,
earray_125 = select(q25,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f81,axiom,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f82,axiom,
earray_131 = select(q26,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f83,axiom,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f85,axiom,
earray_140 = select(q27,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f86,axiom,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f87,axiom,
earray_146 = select(q28,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f88,axiom,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f92,axiom,
earray_161 = select(q29,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f93,axiom,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f94,axiom,
earray_170 = select(q30,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f95,axiom,
earray_172 = store(earray_170,index_171,e30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f96,axiom,
earray_176 = select(q31,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f97,axiom,
earray_178 = store(earray_176,index_177,e31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f98,axiom,
earray_182 = select(q32,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp26) ).
fof(f99,axiom,
earray_184 = store(earray_182,index_183,e32),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp27) ).
fof(f100,axiom,
earray_191 = select(q33,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f101,axiom,
earray_193 = store(earray_191,index_192,e33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp29) ).
fof(f102,axiom,
earray_197 = select(q34,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp30) ).
fof(f103,axiom,
earray_199 = store(earray_197,index_198,e34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp31) ).
fof(f106,axiom,
earray_203 = select(q35,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp34) ).
fof(f107,axiom,
earray_205 = store(earray_203,index_204,e35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp35) ).
fof(f108,axiom,
earray_212 = select(q36,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f109,axiom,
earray_214 = store(earray_212,index_213,e36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f110,axiom,
earray_218 = select(q37,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f112,axiom,
earray_220 = store(earray_218,index_219,e37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f113,axiom,
earray_224 = select(q38,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f114,axiom,
earray_226 = store(earray_224,index_225,e38),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp42) ).
fof(f117,axiom,
earray_239 = select(q39,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
fof(f118,axiom,
earray_241 = store(earray_239,index_240,e39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp46) ).
fof(f129,axiom,
earray_281 = select(q40,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp57) ).
fof(f133,axiom,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp61) ).
fof(f135,axiom,
earray_41 = select(q14,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp63) ).
fof(f136,axiom,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp64) ).
fof(f137,axiom,
earray_50 = select(q15,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp65) ).
fof(f138,axiom,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp66) ).
fof(f139,axiom,
earray_56 = select(q16,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp67) ).
fof(f140,axiom,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp68) ).
fof(f141,axiom,
earray_62 = select(q17,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp69) ).
fof(f142,axiom,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp70) ).
fof(f143,axiom,
earray_71 = select(q18,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp71) ).
fof(f144,axiom,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp72) ).
fof(f148,axiom,
earray_83 = select(q19,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp76) ).
fof(f149,axiom,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp77) ).
fof(f150,axiom,
earray_89 = select(q20,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp78) ).
fof(f151,axiom,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp79) ).
fof(f152,axiom,
earray_98 = select(q21,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp80) ).
fof(f153,axiom,
elem_283 = select(earray_281,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp81) ).
fof(f154,axiom,
index_0 = select(q,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp82) ).
fof(f155,axiom,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp83) ).
fof(f156,axiom,
index_105 = select(q22,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp84) ).
fof(f157,axiom,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp85) ).
fof(f158,axiom,
index_111 = select(q23,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp86) ).
fof(f159,axiom,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp87) ).
fof(f160,axiom,
index_116 = select(queue_115,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp88) ).
fof(f161,axiom,
index_117 = s(index_116),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp89) ).
fof(f162,axiom,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp90) ).
fof(f163,axiom,
index_120 = select(q24,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp91) ).
fof(f164,axiom,
index_123 = s(index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp92) ).
fof(f165,axiom,
index_126 = select(q25,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp93) ).
fof(f166,axiom,
index_129 = s(index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp94) ).
fof(f167,axiom,
index_132 = select(q26,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp95) ).
fof(f168,axiom,
index_135 = s(index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp96) ).
fof(f169,axiom,
index_137 = select(queue_136,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp97) ).
fof(f170,axiom,
index_138 = s(index_137),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp98) ).
fof(f171,axiom,
index_141 = select(q27,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
fof(f172,axiom,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
fof(f173,axiom,
index_147 = select(q28,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f174,axiom,
index_15 = select(q10,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp102) ).
fof(f175,axiom,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp103) ).
fof(f176,axiom,
index_153 = select(q2,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
fof(f177,axiom,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp105) ).
fof(f178,axiom,
index_158 = select(queue_157,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp106) ).
fof(f179,axiom,
index_159 = s(index_158),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
fof(f180,axiom,
index_162 = select(q29,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
fof(f181,axiom,
index_165 = s(index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
fof(f182,axiom,
index_167 = select(queue_166,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp110) ).
fof(f183,axiom,
index_168 = s(index_167),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp111) ).
fof(f184,axiom,
index_171 = select(q30,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp112) ).
fof(f185,axiom,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp113) ).
fof(f186,axiom,
index_177 = select(q31,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
fof(f187,axiom,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp115) ).
fof(f188,axiom,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp116) ).
fof(f189,axiom,
index_183 = select(q32,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp117) ).
fof(f190,axiom,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp118) ).
fof(f191,axiom,
index_188 = select(queue_187,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp119) ).
fof(f192,axiom,
index_189 = s(index_188),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp120) ).
fof(f193,axiom,
index_192 = select(q33,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp121) ).
fof(f194,axiom,
index_195 = s(index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp122) ).
fof(f195,axiom,
index_198 = select(q34,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp123) ).
fof(f196,axiom,
index_201 = s(index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp124) ).
fof(f197,axiom,
index_204 = select(q35,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp125) ).
fof(f198,axiom,
index_207 = s(index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp126) ).
fof(f199,axiom,
index_209 = select(queue_208,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp127) ).
fof(f200,axiom,
index_21 = select(q11,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp128) ).
fof(f201,axiom,
index_210 = s(index_209),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp129) ).
fof(f202,axiom,
index_213 = select(q36,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp130) ).
fof(f203,axiom,
index_216 = s(index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp131) ).
fof(f204,axiom,
index_219 = select(q37,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp132) ).
fof(f205,axiom,
index_222 = s(index_219),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp133) ).
fof(f206,axiom,
index_225 = select(q38,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp134) ).
fof(f207,axiom,
index_228 = s(index_225),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp135) ).
fof(f208,axiom,
index_230 = select(queue_229,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp136) ).
fof(f209,axiom,
index_231 = s(index_230),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp137) ).
fof(f210,axiom,
index_234 = select(q3,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
fof(f211,axiom,
index_237 = s(index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp139) ).
fof(f212,axiom,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp140) ).
fof(f213,axiom,
index_240 = select(q39,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp141) ).
fof(f214,axiom,
index_243 = s(index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp142) ).
fof(f215,axiom,
index_246 = select(q4,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp143) ).
fof(f216,axiom,
index_249 = s(index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp144) ).
fof(f217,axiom,
index_252 = select(q5,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp145) ).
fof(f218,axiom,
index_255 = s(index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp146) ).
fof(f219,axiom,
index_257 = select(queue_256,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp147) ).
fof(f220,axiom,
index_258 = s(index_257),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp148) ).
fof(f221,axiom,
index_26 = select(queue_25,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp149) ).
fof(f222,axiom,
index_261 = select(q6,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp150) ).
fof(f223,axiom,
index_264 = s(index_261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp151) ).
fof(f224,axiom,
index_267 = select(q7,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
fof(f225,axiom,
index_27 = s(index_26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp153) ).
fof(f226,axiom,
index_270 = s(index_267),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp154) ).
fof(f227,axiom,
index_273 = select(q8,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp155) ).
fof(f228,axiom,
index_276 = s(index_273),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp156) ).
fof(f229,axiom,
index_278 = select(queue_277,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp157) ).
fof(f230,axiom,
index_279 = s(index_278),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp158) ).
fof(f231,axiom,
index_282 = select(q40,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp159) ).
fof(f232,axiom,
index_3 = select(q0,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
fof(f233,axiom,
index_30 = select(q12,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp161) ).
fof(f234,axiom,
index_33 = s(index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp162) ).
fof(f235,axiom,
index_36 = select(q13,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp163) ).
fof(f236,axiom,
index_39 = s(index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp164) ).
fof(f237,axiom,
index_42 = select(q14,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp165) ).
fof(f238,axiom,
index_45 = s(index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp166) ).
fof(f239,axiom,
index_47 = select(queue_46,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp167) ).
fof(f240,axiom,
index_48 = s(index_47),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
fof(f241,axiom,
index_51 = select(q15,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp169) ).
fof(f242,axiom,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp170) ).
fof(f243,axiom,
index_57 = select(q16,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp171) ).
fof(f244,axiom,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
fof(f245,axiom,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp173) ).
fof(f246,axiom,
index_63 = select(q17,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp174) ).
fof(f247,axiom,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
fof(f248,axiom,
index_68 = select(queue_67,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp176) ).
fof(f249,axiom,
index_69 = s(index_68),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp177) ).
fof(f250,axiom,
index_72 = select(q18,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp178) ).
fof(f251,axiom,
index_75 = s(index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp179) ).
fof(f252,axiom,
index_78 = select(q1,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp180) ).
fof(f253,axiom,
index_81 = s(index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp181) ).
fof(f254,axiom,
index_84 = select(q19,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp182) ).
fof(f255,axiom,
index_87 = s(index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp183) ).
fof(f256,axiom,
index_9 = select(q9,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp184) ).
fof(f257,axiom,
index_90 = select(q20,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp185) ).
fof(f258,axiom,
index_93 = s(index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp186) ).
fof(f259,axiom,
index_95 = select(queue_94,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f260,axiom,
index_96 = s(index_95),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp188) ).
fof(f261,axiom,
index_99 = select(q21,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp189) ).
fof(f262,axiom,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp190) ).
fof(f263,axiom,
queue_101 = store(q21,seq,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
fof(f264,axiom,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp192) ).
fof(f265,axiom,
queue_107 = store(q22,seq,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp193) ).
fof(f266,axiom,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp194) ).
fof(f267,axiom,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
fof(f268,axiom,
queue_113 = store(q23,seq,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp196) ).
fof(f269,axiom,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp197) ).
fof(f270,axiom,
queue_118 = store(queue_115,head,index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
fof(f271,axiom,
queue_122 = store(q24,seq,earray_121),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
fof(f272,axiom,
queue_124 = store(queue_122,tail,index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
fof(f273,axiom,
queue_128 = store(q25,seq,earray_127),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
fof(f274,axiom,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
fof(f275,axiom,
queue_130 = store(queue_128,tail,index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f276,axiom,
queue_134 = store(q26,seq,earray_133),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp204) ).
fof(f277,axiom,
queue_136 = store(queue_134,tail,index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f278,axiom,
queue_139 = store(queue_136,head,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp206) ).
fof(f279,axiom,
queue_143 = store(q27,seq,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f280,axiom,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
fof(f281,axiom,
queue_149 = store(q28,seq,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f282,axiom,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
fof(f283,axiom,
queue_155 = store(q2,seq,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
fof(f284,axiom,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f285,axiom,
queue_160 = store(queue_157,head,index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f286,axiom,
queue_164 = store(q29,seq,earray_163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
fof(f287,axiom,
queue_166 = store(queue_164,tail,index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f288,axiom,
queue_169 = store(queue_166,head,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
fof(f289,axiom,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f290,axiom,
queue_173 = store(q30,seq,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp218) ).
fof(f291,axiom,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp219) ).
fof(f292,axiom,
queue_179 = store(q31,seq,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f293,axiom,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f294,axiom,
queue_185 = store(q32,seq,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
fof(f295,axiom,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
fof(f296,axiom,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f297,axiom,
queue_190 = store(queue_187,head,index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f298,axiom,
queue_194 = store(q33,seq,earray_193),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
fof(f299,axiom,
queue_196 = store(queue_194,tail,index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f300,axiom,
queue_200 = store(q34,seq,earray_199),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
fof(f301,axiom,
queue_202 = store(queue_200,tail,index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f302,axiom,
queue_206 = store(q35,seq,earray_205),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
fof(f303,axiom,
queue_208 = store(queue_206,tail,index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
fof(f304,axiom,
queue_211 = store(queue_208,head,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f305,axiom,
queue_215 = store(q36,seq,earray_214),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f306,axiom,
queue_217 = store(queue_215,tail,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
fof(f307,axiom,
queue_221 = store(q37,seq,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
fof(f308,axiom,
queue_223 = store(queue_221,tail,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f309,axiom,
queue_227 = store(q38,seq,earray_226),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f310,axiom,
queue_229 = store(queue_227,tail,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
fof(f311,axiom,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f312,axiom,
queue_232 = store(queue_229,head,index_231),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
fof(f313,axiom,
queue_236 = store(q3,seq,earray_235),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f314,axiom,
queue_238 = store(queue_236,tail,index_237),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
fof(f315,axiom,
queue_242 = store(q39,seq,earray_241),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
fof(f316,axiom,
queue_244 = store(queue_242,tail,index_243),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f317,axiom,
queue_248 = store(q4,seq,earray_247),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f318,axiom,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp246) ).
fof(f319,axiom,
queue_250 = store(queue_248,tail,index_249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp247) ).
fof(f320,axiom,
queue_254 = store(q5,seq,earray_253),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp248) ).
fof(f321,axiom,
queue_256 = store(queue_254,tail,index_255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp249) ).
fof(f322,axiom,
queue_259 = store(queue_256,head,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp250) ).
fof(f323,axiom,
queue_263 = store(q6,seq,earray_262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp251) ).
fof(f324,axiom,
queue_265 = store(queue_263,tail,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp252) ).
fof(f325,axiom,
queue_269 = store(q7,seq,earray_268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp253) ).
fof(f326,axiom,
queue_271 = store(queue_269,tail,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp254) ).
fof(f327,axiom,
queue_275 = store(q8,seq,earray_274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp255) ).
fof(f328,axiom,
queue_277 = store(queue_275,tail,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp256) ).
fof(f329,axiom,
queue_28 = store(queue_25,head,index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp257) ).
fof(f330,axiom,
queue_280 = store(queue_277,head,index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp258) ).
fof(f331,axiom,
queue_32 = store(q12,seq,earray_31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp259) ).
fof(f332,axiom,
queue_34 = store(queue_32,tail,index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp260) ).
fof(f333,axiom,
queue_38 = store(q13,seq,earray_37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp261) ).
fof(f334,axiom,
queue_40 = store(queue_38,tail,index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp262) ).
fof(f335,axiom,
queue_44 = store(q14,seq,earray_43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp263) ).
fof(f336,axiom,
queue_46 = store(queue_44,tail,index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp264) ).
fof(f337,axiom,
queue_49 = store(queue_46,head,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp265) ).
fof(f338,axiom,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp266) ).
fof(f339,axiom,
queue_53 = store(q15,seq,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp267) ).
fof(f340,axiom,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp268) ).
fof(f341,axiom,
queue_59 = store(q16,seq,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp269) ).
fof(f342,axiom,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp270) ).
fof(f343,axiom,
queue_65 = store(q17,seq,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp271) ).
fof(f344,axiom,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp272) ).
fof(f345,axiom,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp273) ).
fof(f346,axiom,
queue_70 = store(queue_67,head,index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp274) ).
fof(f347,axiom,
queue_74 = store(q18,seq,earray_73),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp275) ).
fof(f348,axiom,
queue_76 = store(queue_74,tail,index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp276) ).
fof(f349,axiom,
queue_80 = store(q1,seq,earray_79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp277) ).
fof(f350,axiom,
queue_82 = store(queue_80,tail,index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp278) ).
fof(f351,axiom,
queue_86 = store(q19,seq,earray_85),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp279) ).
fof(f352,axiom,
queue_88 = store(queue_86,tail,index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp280) ).
fof(f353,axiom,
queue_92 = store(q20,seq,earray_91),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp281) ).
fof(f354,axiom,
queue_94 = store(queue_92,tail,index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp282) ).
fof(f355,axiom,
queue_97 = store(queue_94,head,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp283) ).
fof(f356,axiom,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp284) ).
fof(f357,axiom,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp285) ).
fof(f358,axiom,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp286) ).
fof(f359,axiom,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp287) ).
fof(f360,axiom,
q12 = queue_28,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp288) ).
fof(f361,axiom,
q13 = queue_34,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp289) ).
fof(f362,axiom,
q14 = queue_40,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp290) ).
fof(f363,axiom,
q15 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp291) ).
fof(f364,axiom,
q16 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp292) ).
fof(f365,axiom,
q17 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp293) ).
fof(f366,axiom,
q18 = queue_70,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp294) ).
fof(f367,axiom,
q19 = queue_76,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp295) ).
fof(f368,axiom,
q2 = queue_82,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp296) ).
fof(f369,axiom,
q20 = queue_88,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp297) ).
fof(f370,axiom,
q21 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp298) ).
fof(f371,axiom,
q22 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp299) ).
fof(f372,axiom,
q23 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp300) ).
fof(f373,axiom,
q24 = queue_118,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp301) ).
fof(f374,axiom,
q25 = queue_124,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp302) ).
fof(f375,axiom,
q26 = queue_130,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp303) ).
fof(f376,axiom,
q27 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp304) ).
fof(f377,axiom,
q28 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp305) ).
fof(f378,axiom,
q29 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp306) ).
fof(f379,axiom,
q3 = queue_160,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp307) ).
fof(f380,axiom,
q30 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp308) ).
fof(f381,axiom,
q31 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp309) ).
fof(f382,axiom,
q32 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp310) ).
fof(f383,axiom,
q33 = queue_190,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp311) ).
fof(f384,axiom,
q34 = queue_196,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp312) ).
fof(f385,axiom,
q35 = queue_202,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp313) ).
fof(f386,axiom,
q36 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp314) ).
fof(f387,axiom,
q37 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp315) ).
fof(f388,axiom,
q38 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp316) ).
fof(f389,axiom,
q39 = queue_232,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp317) ).
fof(f390,axiom,
q4 = queue_238,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp318) ).
fof(f391,axiom,
q40 = queue_244,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp319) ).
fof(f392,axiom,
q5 = queue_250,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp320) ).
fof(f393,axiom,
q6 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp321) ).
fof(f394,axiom,
q7 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp322) ).
fof(f395,axiom,
q8 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp323) ).
fof(f396,axiom,
q9 = queue_280,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp324) ).
fof(f397,negated_conjecture,
elem_283 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f398,plain,
e13 != elem_283,
inference(reorient_equations,[],[f397]) ).
fof(f399,plain,
earray_104 = select(queue_103,seq),
inference(definition_unfolding,[],[f74,f371]) ).
fof(f400,plain,
earray_110 = select(queue_109,seq),
inference(definition_unfolding,[],[f76,f372]) ).
fof(f401,plain,
earray_119 = select(queue_118,seq),
inference(definition_unfolding,[],[f78,f373]) ).
fof(f402,plain,
earray_125 = select(queue_124,seq),
inference(definition_unfolding,[],[f80,f374]) ).
fof(f403,plain,
earray_131 = select(queue_130,seq),
inference(definition_unfolding,[],[f82,f375]) ).
fof(f405,plain,
earray_140 = select(queue_139,seq),
inference(definition_unfolding,[],[f85,f376]) ).
fof(f406,plain,
earray_146 = select(queue_145,seq),
inference(definition_unfolding,[],[f87,f377]) ).
fof(f408,plain,
earray_161 = select(queue_151,seq),
inference(definition_unfolding,[],[f92,f378]) ).
fof(f409,plain,
earray_170 = select(queue_169,seq),
inference(definition_unfolding,[],[f94,f380]) ).
fof(f410,plain,
earray_176 = select(queue_175,seq),
inference(definition_unfolding,[],[f96,f381]) ).
fof(f411,plain,
earray_182 = select(queue_181,seq),
inference(definition_unfolding,[],[f98,f382]) ).
fof(f412,plain,
earray_191 = select(queue_190,seq),
inference(definition_unfolding,[],[f100,f383]) ).
fof(f413,plain,
earray_197 = select(queue_196,seq),
inference(definition_unfolding,[],[f102,f384]) ).
fof(f416,plain,
earray_203 = select(queue_202,seq),
inference(definition_unfolding,[],[f106,f385]) ).
fof(f417,plain,
earray_212 = select(queue_211,seq),
inference(definition_unfolding,[],[f108,f386]) ).
fof(f418,plain,
earray_218 = select(queue_217,seq),
inference(definition_unfolding,[],[f110,f387]) ).
fof(f419,plain,
earray_224 = select(queue_223,seq),
inference(definition_unfolding,[],[f113,f388]) ).
fof(f421,plain,
earray_239 = select(queue_232,seq),
inference(definition_unfolding,[],[f117,f389]) ).
fof(f427,plain,
earray_281 = select(queue_244,seq),
inference(definition_unfolding,[],[f129,f391]) ).
fof(f430,plain,
earray_41 = select(queue_40,seq),
inference(definition_unfolding,[],[f135,f362]) ).
fof(f431,plain,
earray_50 = select(queue_49,seq),
inference(definition_unfolding,[],[f137,f363]) ).
fof(f432,plain,
earray_56 = select(queue_55,seq),
inference(definition_unfolding,[],[f139,f364]) ).
fof(f433,plain,
earray_62 = select(queue_61,seq),
inference(definition_unfolding,[],[f141,f365]) ).
fof(f434,plain,
earray_71 = select(queue_70,seq),
inference(definition_unfolding,[],[f143,f366]) ).
fof(f437,plain,
earray_83 = select(queue_76,seq),
inference(definition_unfolding,[],[f148,f367]) ).
fof(f438,plain,
earray_89 = select(queue_88,seq),
inference(definition_unfolding,[],[f150,f369]) ).
fof(f439,plain,
earray_98 = select(queue_97,seq),
inference(definition_unfolding,[],[f152,f370]) ).
fof(f440,plain,
index_105 = select(queue_103,tail),
inference(definition_unfolding,[],[f156,f371]) ).
fof(f441,plain,
index_111 = select(queue_109,tail),
inference(definition_unfolding,[],[f158,f372]) ).
fof(f442,plain,
index_120 = select(queue_118,tail),
inference(definition_unfolding,[],[f163,f373]) ).
fof(f443,plain,
index_126 = select(queue_124,tail),
inference(definition_unfolding,[],[f165,f374]) ).
fof(f444,plain,
index_132 = select(queue_130,tail),
inference(definition_unfolding,[],[f167,f375]) ).
fof(f445,plain,
index_141 = select(queue_139,tail),
inference(definition_unfolding,[],[f171,f376]) ).
fof(f446,plain,
index_147 = select(queue_145,tail),
inference(definition_unfolding,[],[f173,f377]) ).
fof(f447,plain,
index_15 = select(queue_13,tail),
inference(definition_unfolding,[],[f174,f358]) ).
fof(f448,plain,
index_153 = select(queue_82,tail),
inference(definition_unfolding,[],[f176,f368]) ).
fof(f449,plain,
index_162 = select(queue_151,tail),
inference(definition_unfolding,[],[f180,f378]) ).
fof(f450,plain,
index_171 = select(queue_169,tail),
inference(definition_unfolding,[],[f184,f380]) ).
fof(f451,plain,
index_177 = select(queue_175,tail),
inference(definition_unfolding,[],[f186,f381]) ).
fof(f452,plain,
index_183 = select(queue_181,tail),
inference(definition_unfolding,[],[f189,f382]) ).
fof(f453,plain,
index_192 = select(queue_190,tail),
inference(definition_unfolding,[],[f193,f383]) ).
fof(f454,plain,
index_198 = select(queue_196,tail),
inference(definition_unfolding,[],[f195,f384]) ).
fof(f455,plain,
index_204 = select(queue_202,tail),
inference(definition_unfolding,[],[f197,f385]) ).
fof(f456,plain,
index_21 = select(queue_19,tail),
inference(definition_unfolding,[],[f200,f359]) ).
fof(f457,plain,
index_213 = select(queue_211,tail),
inference(definition_unfolding,[],[f202,f386]) ).
fof(f458,plain,
index_219 = select(queue_217,tail),
inference(definition_unfolding,[],[f204,f387]) ).
fof(f459,plain,
index_225 = select(queue_223,tail),
inference(definition_unfolding,[],[f206,f388]) ).
fof(f460,plain,
index_234 = select(queue_160,tail),
inference(definition_unfolding,[],[f210,f379]) ).
fof(f461,plain,
index_240 = select(queue_232,tail),
inference(definition_unfolding,[],[f213,f389]) ).
fof(f462,plain,
index_246 = select(queue_238,tail),
inference(definition_unfolding,[],[f215,f390]) ).
fof(f463,plain,
index_252 = select(queue_250,tail),
inference(definition_unfolding,[],[f217,f392]) ).
fof(f464,plain,
index_261 = select(queue_259,tail),
inference(definition_unfolding,[],[f222,f393]) ).
fof(f465,plain,
index_267 = select(queue_265,tail),
inference(definition_unfolding,[],[f224,f394]) ).
fof(f466,plain,
index_273 = select(queue_271,tail),
inference(definition_unfolding,[],[f227,f395]) ).
fof(f467,plain,
index_282 = select(queue_244,head),
inference(definition_unfolding,[],[f231,f391]) ).
fof(f468,plain,
index_3 = select(queue_1,tail),
inference(definition_unfolding,[],[f232,f356]) ).
fof(f469,plain,
index_30 = select(queue_28,tail),
inference(definition_unfolding,[],[f233,f360]) ).
fof(f470,plain,
index_36 = select(queue_34,tail),
inference(definition_unfolding,[],[f235,f361]) ).
fof(f471,plain,
index_42 = select(queue_40,tail),
inference(definition_unfolding,[],[f237,f362]) ).
fof(f472,plain,
index_51 = select(queue_49,tail),
inference(definition_unfolding,[],[f241,f363]) ).
fof(f473,plain,
index_57 = select(queue_55,tail),
inference(definition_unfolding,[],[f243,f364]) ).
fof(f474,plain,
index_63 = select(queue_61,tail),
inference(definition_unfolding,[],[f246,f365]) ).
fof(f475,plain,
index_72 = select(queue_70,tail),
inference(definition_unfolding,[],[f250,f366]) ).
fof(f476,plain,
index_78 = select(queue_7,tail),
inference(definition_unfolding,[],[f252,f357]) ).
fof(f477,plain,
index_84 = select(queue_76,tail),
inference(definition_unfolding,[],[f254,f367]) ).
fof(f478,plain,
index_9 = select(queue_280,tail),
inference(definition_unfolding,[],[f256,f396]) ).
fof(f479,plain,
index_90 = select(queue_88,tail),
inference(definition_unfolding,[],[f257,f369]) ).
fof(f480,plain,
index_99 = select(queue_97,tail),
inference(definition_unfolding,[],[f261,f370]) ).
fof(f481,plain,
queue_101 = store(queue_97,seq,earray_100),
inference(definition_unfolding,[],[f263,f370]) ).
fof(f482,plain,
queue_107 = store(queue_103,seq,earray_106),
inference(definition_unfolding,[],[f265,f371]) ).
fof(f483,plain,
queue_11 = store(queue_280,seq,earray_10),
inference(definition_unfolding,[],[f267,f396]) ).
fof(f484,plain,
queue_113 = store(queue_109,seq,earray_112),
inference(definition_unfolding,[],[f268,f372]) ).
fof(f485,plain,
queue_122 = store(queue_118,seq,earray_121),
inference(definition_unfolding,[],[f271,f373]) ).
fof(f486,plain,
queue_128 = store(queue_124,seq,earray_127),
inference(definition_unfolding,[],[f273,f374]) ).
fof(f487,plain,
queue_134 = store(queue_130,seq,earray_133),
inference(definition_unfolding,[],[f276,f375]) ).
fof(f488,plain,
queue_143 = store(queue_139,seq,earray_142),
inference(definition_unfolding,[],[f279,f376]) ).
fof(f489,plain,
queue_149 = store(queue_145,seq,earray_148),
inference(definition_unfolding,[],[f281,f377]) ).
fof(f490,plain,
queue_155 = store(queue_82,seq,earray_154),
inference(definition_unfolding,[],[f283,f368]) ).
fof(f491,plain,
queue_164 = store(queue_151,seq,earray_163),
inference(definition_unfolding,[],[f286,f378]) ).
fof(f492,plain,
queue_17 = store(queue_13,seq,earray_16),
inference(definition_unfolding,[],[f289,f358]) ).
fof(f493,plain,
queue_173 = store(queue_169,seq,earray_172),
inference(definition_unfolding,[],[f290,f380]) ).
fof(f494,plain,
queue_179 = store(queue_175,seq,earray_178),
inference(definition_unfolding,[],[f292,f381]) ).
fof(f495,plain,
queue_185 = store(queue_181,seq,earray_184),
inference(definition_unfolding,[],[f294,f382]) ).
fof(f496,plain,
queue_194 = store(queue_190,seq,earray_193),
inference(definition_unfolding,[],[f298,f383]) ).
fof(f497,plain,
queue_200 = store(queue_196,seq,earray_199),
inference(definition_unfolding,[],[f300,f384]) ).
fof(f498,plain,
queue_206 = store(queue_202,seq,earray_205),
inference(definition_unfolding,[],[f302,f385]) ).
fof(f499,plain,
queue_215 = store(queue_211,seq,earray_214),
inference(definition_unfolding,[],[f305,f386]) ).
fof(f500,plain,
queue_221 = store(queue_217,seq,earray_220),
inference(definition_unfolding,[],[f307,f387]) ).
fof(f501,plain,
queue_227 = store(queue_223,seq,earray_226),
inference(definition_unfolding,[],[f309,f388]) ).
fof(f502,plain,
queue_23 = store(queue_19,seq,earray_22),
inference(definition_unfolding,[],[f311,f359]) ).
fof(f503,plain,
queue_236 = store(queue_160,seq,earray_235),
inference(definition_unfolding,[],[f313,f379]) ).
fof(f504,plain,
queue_242 = store(queue_232,seq,earray_241),
inference(definition_unfolding,[],[f315,f389]) ).
fof(f505,plain,
queue_248 = store(queue_238,seq,earray_247),
inference(definition_unfolding,[],[f317,f390]) ).
fof(f506,plain,
queue_254 = store(queue_250,seq,earray_253),
inference(definition_unfolding,[],[f320,f392]) ).
fof(f507,plain,
queue_263 = store(queue_259,seq,earray_262),
inference(definition_unfolding,[],[f323,f393]) ).
fof(f508,plain,
queue_269 = store(queue_265,seq,earray_268),
inference(definition_unfolding,[],[f325,f394]) ).
fof(f509,plain,
queue_275 = store(queue_271,seq,earray_274),
inference(definition_unfolding,[],[f327,f395]) ).
fof(f510,plain,
queue_32 = store(queue_28,seq,earray_31),
inference(definition_unfolding,[],[f331,f360]) ).
fof(f511,plain,
queue_38 = store(queue_34,seq,earray_37),
inference(definition_unfolding,[],[f333,f361]) ).
fof(f512,plain,
queue_44 = store(queue_40,seq,earray_43),
inference(definition_unfolding,[],[f335,f362]) ).
fof(f513,plain,
queue_5 = store(queue_1,seq,earray_4),
inference(definition_unfolding,[],[f338,f356]) ).
fof(f514,plain,
queue_53 = store(queue_49,seq,earray_52),
inference(definition_unfolding,[],[f339,f363]) ).
fof(f515,plain,
queue_59 = store(queue_55,seq,earray_58),
inference(definition_unfolding,[],[f341,f364]) ).
fof(f516,plain,
queue_65 = store(queue_61,seq,earray_64),
inference(definition_unfolding,[],[f343,f365]) ).
fof(f517,plain,
queue_74 = store(queue_70,seq,earray_73),
inference(definition_unfolding,[],[f347,f366]) ).
fof(f518,plain,
queue_80 = store(queue_7,seq,earray_79),
inference(definition_unfolding,[],[f349,f357]) ).
fof(f519,plain,
queue_86 = store(queue_76,seq,earray_85),
inference(definition_unfolding,[],[f351,f367]) ).
fof(f520,plain,
queue_92 = store(queue_88,seq,earray_91),
inference(definition_unfolding,[],[f353,f369]) ).
fof(f521,plain,
e13 = select(earray_37,index_36),
inference(superposition,[],[f1,f133]) ).
fof(f522,plain,
earray_37 = select(queue_38,seq),
inference(superposition,[],[f1,f511]) ).
fof(f524,plain,
! [X0] :
( select(queue_34,X0) = select(queue_38,X0)
| seq = X0 ),
inference(superposition,[],[f2,f511]) ).
fof(f525,plain,
! [X0] :
( select(queue_40,X0) = select(queue_44,X0)
| seq = X0 ),
inference(superposition,[],[f2,f512]) ).
fof(f526,plain,
earray_43 = select(queue_44,seq),
inference(superposition,[],[f1,f512]) ).
fof(f527,plain,
! [X0] :
( select(queue_28,X0) = select(queue_32,X0)
| seq = X0 ),
inference(superposition,[],[f2,f510]) ).
fof(f529,plain,
! [X0] :
( select(queue_232,X0) = select(queue_242,X0)
| seq = X0 ),
inference(superposition,[],[f2,f504]) ).
fof(f530,plain,
earray_241 = select(queue_242,seq),
inference(superposition,[],[f1,f504]) ).
fof(f531,plain,
! [X0] :
( select(earray_41,X0) = select(earray_43,X0)
| index_42 = X0 ),
inference(superposition,[],[f2,f136]) ).
fof(f533,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))),
inference(superposition,[],[f57,f236]) ).
fof(f534,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))),
inference(superposition,[],[f58,f236]) ).
fof(f535,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))),
inference(superposition,[],[f59,f236]) ).
fof(f536,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))),
inference(superposition,[],[f60,f236]) ).
fof(f537,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(index_39)))))))))),
inference(superposition,[],[f61,f236]) ).
fof(f538,plain,
index_36 != s(s(s(s(s(s(s(s(s(index_39))))))))),
inference(superposition,[],[f62,f236]) ).
fof(f539,plain,
index_36 != s(s(s(s(s(s(s(s(index_39)))))))),
inference(superposition,[],[f63,f236]) ).
fof(f540,plain,
index_36 != s(s(s(s(s(s(s(index_39))))))),
inference(superposition,[],[f64,f236]) ).
fof(f541,plain,
index_36 != s(s(s(s(s(s(index_39)))))),
inference(superposition,[],[f65,f236]) ).
fof(f542,plain,
index_36 != s(s(s(s(index_39)))),
inference(superposition,[],[f67,f236]) ).
fof(f543,plain,
index_36 != index_39,
inference(superposition,[],[f71,f236]) ).
fof(f544,plain,
! [X0] :
( select(queue_49,X0) = select(queue_53,X0)
| seq = X0 ),
inference(superposition,[],[f2,f514]) ).
fof(f545,plain,
earray_52 = select(queue_53,seq),
inference(superposition,[],[f1,f514]) ).
fof(f548,plain,
! [X0] :
( select(earray_239,X0) = select(earray_241,X0)
| index_240 = X0 ),
inference(superposition,[],[f2,f118]) ).
fof(f550,plain,
index_36 != s(s(s(s(s(index_39))))),
inference(superposition,[],[f66,f236]) ).
fof(f551,plain,
! [X0] :
( select(queue_19,X0) = select(queue_23,X0)
| seq = X0 ),
inference(superposition,[],[f2,f502]) ).
fof(f553,plain,
! [X0] :
( select(queue_223,X0) = select(queue_227,X0)
| seq = X0 ),
inference(superposition,[],[f2,f501]) ).
fof(f554,plain,
earray_226 = select(queue_227,seq),
inference(superposition,[],[f1,f501]) ).
fof(f555,plain,
! [X0] :
( select(queue_13,X0) = select(queue_17,X0)
| seq = X0 ),
inference(superposition,[],[f2,f492]) ).
fof(f557,plain,
! [X0] :
( select(queue_55,X0) = select(queue_59,X0)
| seq = X0 ),
inference(superposition,[],[f2,f515]) ).
fof(f558,plain,
earray_58 = select(queue_59,seq),
inference(superposition,[],[f1,f515]) ).
fof(f559,plain,
! [X0] :
( select(queue_217,X0) = select(queue_221,X0)
| seq = X0 ),
inference(superposition,[],[f2,f500]) ).
fof(f560,plain,
earray_220 = select(queue_221,seq),
inference(superposition,[],[f1,f500]) ).
fof(f561,plain,
! [X0] :
( select(earray_50,X0) = select(earray_52,X0)
| index_51 = X0 ),
inference(superposition,[],[f2,f138]) ).
fof(f565,plain,
! [X0] :
( select(earray_224,X0) = select(earray_226,X0)
| index_225 = X0 ),
inference(superposition,[],[f2,f114]) ).
fof(f567,plain,
index_36 != s(s(s(index_39))),
inference(superposition,[],[f68,f236]) ).
fof(f568,plain,
! [X0] :
( select(queue_38,X0) = select(queue_40,X0)
| tail = X0 ),
inference(superposition,[],[f2,f334]) ).
fof(f569,plain,
index_39 = select(queue_40,tail),
inference(superposition,[],[f1,f334]) ).
fof(f570,plain,
index_42 = index_39,
inference(backward_demodulation,[],[f471,f569]) ).
fof(f571,plain,
! [X0] :
( select(earray_41,X0) = select(earray_43,X0)
| index_39 = X0 ),
inference(backward_demodulation,[],[f531,f570]) ).
fof(f574,plain,
index_45 = s(index_39),
inference(backward_demodulation,[],[f238,f570]) ).
fof(f575,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))),
inference(backward_demodulation,[],[f533,f574]) ).
fof(f576,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))),
inference(backward_demodulation,[],[f534,f574]) ).
fof(f577,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))),
inference(backward_demodulation,[],[f535,f574]) ).
fof(f578,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(index_45)))))))))),
inference(backward_demodulation,[],[f536,f574]) ).
fof(f579,plain,
index_36 != s(s(s(s(s(s(s(s(s(index_45))))))))),
inference(backward_demodulation,[],[f537,f574]) ).
fof(f580,plain,
index_36 != s(s(s(s(s(s(s(s(index_45)))))))),
inference(backward_demodulation,[],[f538,f574]) ).
fof(f581,plain,
index_36 != s(s(s(s(s(s(s(index_45))))))),
inference(backward_demodulation,[],[f539,f574]) ).
fof(f582,plain,
index_36 != s(s(s(s(s(s(index_45)))))),
inference(backward_demodulation,[],[f540,f574]) ).
fof(f583,plain,
index_36 != s(s(s(s(s(index_45))))),
inference(backward_demodulation,[],[f541,f574]) ).
fof(f584,plain,
index_36 != s(s(s(index_45))),
inference(backward_demodulation,[],[f542,f574]) ).
fof(f585,plain,
index_36 != s(s(s(s(index_45)))),
inference(backward_demodulation,[],[f550,f574]) ).
fof(f586,plain,
index_36 != s(s(index_45)),
inference(backward_demodulation,[],[f567,f574]) ).
fof(f587,plain,
! [X0] :
( select(queue_61,X0) = select(queue_65,X0)
| seq = X0 ),
inference(superposition,[],[f2,f516]) ).
fof(f588,plain,
earray_64 = select(queue_65,seq),
inference(superposition,[],[f1,f516]) ).
fof(f589,plain,
! [X0] :
( select(queue_211,X0) = select(queue_215,X0)
| seq = X0 ),
inference(superposition,[],[f2,f499]) ).
fof(f590,plain,
earray_214 = select(queue_215,seq),
inference(superposition,[],[f1,f499]) ).
fof(f591,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))),
inference(superposition,[],[f56,f236]) ).
fof(f592,plain,
index_36 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))),
inference(forward_demodulation,[],[f591,f574]) ).
fof(f593,plain,
! [X0] :
( select(earray_56,X0) = select(earray_58,X0)
| index_57 = X0 ),
inference(superposition,[],[f2,f140]) ).
fof(f595,plain,
! [X0] :
( select(earray_218,X0) = select(earray_220,X0)
| index_219 = X0 ),
inference(superposition,[],[f2,f112]) ).
fof(f601,plain,
! [X0] :
( select(queue_242,X0) = select(queue_244,X0)
| tail = X0 ),
inference(superposition,[],[f2,f316]) ).
fof(f603,plain,
! [X0] :
( select(queue_280,X0) = select(queue_11,X0)
| seq = X0 ),
inference(superposition,[],[f2,f483]) ).
fof(f605,plain,
! [X0] :
( select(queue_34,X0) = select(queue_32,X0)
| tail = X0 ),
inference(superposition,[],[f2,f332]) ).
fof(f606,plain,
index_33 = select(queue_34,tail),
inference(superposition,[],[f1,f332]) ).
fof(f607,plain,
index_36 = index_33,
inference(backward_demodulation,[],[f470,f606]) ).
fof(f609,plain,
index_39 = s(index_33),
inference(backward_demodulation,[],[f236,f607]) ).
fof(f610,plain,
e13 = select(earray_37,index_33),
inference(backward_demodulation,[],[f521,f607]) ).
fof(f612,plain,
index_33 != index_39,
inference(backward_demodulation,[],[f543,f607]) ).
fof(f613,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))),
inference(backward_demodulation,[],[f575,f607]) ).
fof(f614,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))),
inference(backward_demodulation,[],[f576,f607]) ).
fof(f615,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))),
inference(backward_demodulation,[],[f577,f607]) ).
fof(f616,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_45)))))))))),
inference(backward_demodulation,[],[f578,f607]) ).
fof(f617,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_45))))))))),
inference(backward_demodulation,[],[f579,f607]) ).
fof(f618,plain,
index_33 != s(s(s(s(s(s(s(s(index_45)))))))),
inference(backward_demodulation,[],[f580,f607]) ).
fof(f619,plain,
index_33 != s(s(s(s(s(s(s(index_45))))))),
inference(backward_demodulation,[],[f581,f607]) ).
fof(f620,plain,
index_33 != s(s(s(s(s(s(index_45)))))),
inference(backward_demodulation,[],[f582,f607]) ).
fof(f621,plain,
index_33 != s(s(s(s(s(index_45))))),
inference(backward_demodulation,[],[f583,f607]) ).
fof(f622,plain,
index_33 != s(s(s(index_45))),
inference(backward_demodulation,[],[f584,f607]) ).
fof(f623,plain,
index_33 != s(s(s(s(index_45)))),
inference(backward_demodulation,[],[f585,f607]) ).
fof(f624,plain,
index_33 != s(s(index_45)),
inference(backward_demodulation,[],[f586,f607]) ).
fof(f625,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))),
inference(backward_demodulation,[],[f592,f607]) ).
fof(f628,plain,
! [X0] :
( select(queue_49,X0) = select(queue_46,X0)
| head = X0 ),
inference(superposition,[],[f2,f337]) ).
fof(f629,plain,
index_48 = select(queue_49,head),
inference(superposition,[],[f1,f337]) ).
fof(f630,plain,
! [X0] :
( select(queue_28,X0) = select(queue_25,X0)
| head = X0 ),
inference(superposition,[],[f2,f329]) ).
fof(f631,plain,
index_27 = select(queue_28,head),
inference(superposition,[],[f1,f329]) ).
fof(f632,plain,
! [X0] :
( select(queue_232,X0) = select(queue_229,X0)
| head = X0 ),
inference(superposition,[],[f2,f312]) ).
fof(f633,plain,
index_231 = select(queue_232,head),
inference(superposition,[],[f1,f312]) ).
fof(f634,plain,
! [X0] :
( select(queue_44,X0) = select(queue_46,X0)
| tail = X0 ),
inference(superposition,[],[f2,f336]) ).
fof(f635,plain,
index_45 = select(queue_46,tail),
inference(superposition,[],[f1,f336]) ).
fof(f732,plain,
! [X0] :
( select(earray_62,X0) = select(earray_64,X0)
| index_63 = X0 ),
inference(superposition,[],[f2,f142]) ).
fof(f734,plain,
! [X0] :
( select(earray_212,X0) = select(earray_214,X0)
| index_213 = X0 ),
inference(superposition,[],[f2,f109]) ).
fof(f736,plain,
! [X0] :
( select(queue_70,X0) = select(queue_74,X0)
| seq = X0 ),
inference(superposition,[],[f2,f517]) ).
fof(f737,plain,
earray_73 = select(queue_74,seq),
inference(superposition,[],[f1,f517]) ).
fof(f752,plain,
! [X0] :
( select(queue_202,X0) = select(queue_206,X0)
| seq = X0 ),
inference(superposition,[],[f2,f498]) ).
fof(f753,plain,
earray_205 = select(queue_206,seq),
inference(superposition,[],[f1,f498]) ).
fof(f754,plain,
! [X0] :
( select(queue_227,X0) = select(queue_229,X0)
| tail = X0 ),
inference(superposition,[],[f2,f310]) ).
fof(f755,plain,
index_228 = select(queue_229,tail),
inference(superposition,[],[f1,f310]) ).
fof(f772,plain,
! [X0] :
( select(queue_23,X0) = select(queue_25,X0)
| tail = X0 ),
inference(superposition,[],[f2,f318]) ).
fof(f773,plain,
index_24 = select(queue_25,tail),
inference(superposition,[],[f1,f318]) ).
fof(f774,plain,
! [X0] :
( select(queue_271,X0) = select(queue_275,X0)
| seq = X0 ),
inference(superposition,[],[f2,f509]) ).
fof(f859,plain,
! [X0] :
( select(earray_71,X0) = select(earray_73,X0)
| index_72 = X0 ),
inference(superposition,[],[f2,f144]) ).
fof(f875,plain,
! [X0] :
( select(queue_53,X0) = select(queue_55,X0)
| tail = X0 ),
inference(superposition,[],[f2,f340]) ).
fof(f876,plain,
index_54 = select(queue_55,tail),
inference(superposition,[],[f1,f340]) ).
fof(f877,plain,
index_57 = index_54,
inference(backward_demodulation,[],[f473,f876]) ).
fof(f879,plain,
index_60 = s(index_54),
inference(backward_demodulation,[],[f245,f877]) ).
fof(f880,plain,
! [X0] :
( select(earray_56,X0) = select(earray_58,X0)
| index_54 = X0 ),
inference(backward_demodulation,[],[f593,f877]) ).
fof(f925,plain,
! [X0] :
( select(queue_196,X0) = select(queue_200,X0)
| seq = X0 ),
inference(superposition,[],[f2,f497]) ).
fof(f926,plain,
earray_199 = select(queue_200,seq),
inference(superposition,[],[f1,f497]) ).
fof(f929,plain,
! [X0] :
( select(earray_203,X0) = select(earray_205,X0)
| index_204 = X0 ),
inference(superposition,[],[f2,f107]) ).
fof(f931,plain,
! [X0] :
( select(queue_76,X0) = select(queue_86,X0)
| seq = X0 ),
inference(superposition,[],[f2,f519]) ).
fof(f932,plain,
earray_85 = select(queue_86,seq),
inference(superposition,[],[f1,f519]) ).
fof(f961,plain,
! [X0] :
( select(queue_265,X0) = select(queue_269,X0)
| seq = X0 ),
inference(superposition,[],[f2,f508]) ).
fof(f1003,plain,
index_33 != s(s(index_39)),
inference(superposition,[],[f69,f609]) ).
fof(f1008,plain,
index_33 != s(index_45),
inference(forward_demodulation,[],[f1003,f574]) ).
fof(f1012,plain,
! [X0] :
( select(queue_223,X0) = select(queue_221,X0)
| tail = X0 ),
inference(superposition,[],[f2,f308]) ).
fof(f1013,plain,
index_222 = select(queue_223,tail),
inference(superposition,[],[f1,f308]) ).
fof(f1014,plain,
index_225 = index_222,
inference(backward_demodulation,[],[f459,f1013]) ).
fof(f1016,plain,
index_228 = s(index_222),
inference(backward_demodulation,[],[f207,f1014]) ).
fof(f1017,plain,
! [X0] :
( select(earray_224,X0) = select(earray_226,X0)
| index_222 = X0 ),
inference(backward_demodulation,[],[f565,f1014]) ).
fof(f1080,plain,
! [X0] :
( select(queue_19,X0) = select(queue_17,X0)
| tail = X0 ),
inference(superposition,[],[f2,f296]) ).
fof(f1081,plain,
index_18 = select(queue_19,tail),
inference(superposition,[],[f1,f296]) ).
fof(f1082,plain,
index_21 = index_18,
inference(backward_demodulation,[],[f456,f1081]) ).
fof(f1084,plain,
index_24 = s(index_18),
inference(backward_demodulation,[],[f212,f1082]) ).
fof(f1151,plain,
( index_30 = select(queue_25,tail)
| head = tail ),
inference(superposition,[],[f469,f630]) ).
fof(f1152,plain,
index_30 = select(queue_25,tail),
inference(forward_subsumption_resolution,[],[f1151,f3]) ).
fof(f1156,plain,
index_30 = index_24,
inference(forward_demodulation,[],[f1152,f773]) ).
fof(f1159,plain,
index_33 = s(index_24),
inference(backward_demodulation,[],[f234,f1156]) ).
fof(f1307,plain,
( earray_50 = select(queue_46,seq)
| head = seq ),
inference(superposition,[],[f431,f628]) ).
fof(f1308,plain,
( index_51 = select(queue_46,tail)
| head = tail ),
inference(superposition,[],[f472,f628]) ).
fof(f1309,plain,
index_51 = select(queue_46,tail),
inference(forward_subsumption_resolution,[],[f1308,f3]) ).
fof(f1310,plain,
earray_50 = select(queue_46,seq),
inference(forward_subsumption_resolution,[],[f1307,f4]) ).
fof(f1313,plain,
index_51 = index_45,
inference(forward_demodulation,[],[f1309,f635]) ).
fof(f1316,plain,
index_54 = s(index_45),
inference(backward_demodulation,[],[f242,f1313]) ).
fof(f1318,plain,
! [X0] :
( select(earray_50,X0) = select(earray_52,X0)
| index_45 = X0 ),
inference(backward_demodulation,[],[f561,f1313]) ).
fof(f1335,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))),
inference(backward_demodulation,[],[f613,f1316]) ).
fof(f1336,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))),
inference(backward_demodulation,[],[f614,f1316]) ).
fof(f1337,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_54)))))))))),
inference(backward_demodulation,[],[f615,f1316]) ).
fof(f1338,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_54))))))))),
inference(backward_demodulation,[],[f616,f1316]) ).
fof(f1339,plain,
index_33 != s(s(s(s(s(s(s(s(index_54)))))))),
inference(backward_demodulation,[],[f617,f1316]) ).
fof(f1340,plain,
index_33 != s(s(s(s(s(s(s(index_54))))))),
inference(backward_demodulation,[],[f618,f1316]) ).
fof(f1341,plain,
index_33 != s(s(s(s(s(s(index_54)))))),
inference(backward_demodulation,[],[f619,f1316]) ).
fof(f1342,plain,
index_33 != s(s(s(s(s(index_54))))),
inference(backward_demodulation,[],[f620,f1316]) ).
fof(f1343,plain,
index_33 != s(s(s(s(index_54)))),
inference(backward_demodulation,[],[f621,f1316]) ).
fof(f1344,plain,
index_33 != s(s(index_54)),
inference(backward_demodulation,[],[f622,f1316]) ).
fof(f1345,plain,
index_33 != s(s(s(index_54))),
inference(backward_demodulation,[],[f623,f1316]) ).
fof(f1346,plain,
index_33 != s(index_54),
inference(backward_demodulation,[],[f624,f1316]) ).
fof(f1347,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))),
inference(backward_demodulation,[],[f625,f1316]) ).
fof(f1362,plain,
index_33 != index_54,
inference(backward_demodulation,[],[f1008,f1316]) ).
fof(f1446,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))),
inference(forward_demodulation,[],[f1347,f879]) ).
fof(f1447,plain,
index_33 != index_60,
inference(forward_demodulation,[],[f1346,f879]) ).
fof(f1448,plain,
index_33 != s(s(index_60)),
inference(forward_demodulation,[],[f1345,f879]) ).
fof(f1449,plain,
index_33 != s(index_60),
inference(forward_demodulation,[],[f1344,f879]) ).
fof(f1450,plain,
index_33 != s(s(s(index_60))),
inference(forward_demodulation,[],[f1343,f879]) ).
fof(f1451,plain,
index_33 != s(s(s(s(index_60)))),
inference(forward_demodulation,[],[f1342,f879]) ).
fof(f1452,plain,
index_33 != s(s(s(s(s(index_60))))),
inference(forward_demodulation,[],[f1341,f879]) ).
fof(f1453,plain,
index_33 != s(s(s(s(s(s(index_60)))))),
inference(forward_demodulation,[],[f1340,f879]) ).
fof(f1454,plain,
index_33 != s(s(s(s(s(s(s(index_60))))))),
inference(forward_demodulation,[],[f1339,f879]) ).
fof(f1455,plain,
index_33 != s(s(s(s(s(s(s(s(index_60)))))))),
inference(forward_demodulation,[],[f1338,f879]) ).
fof(f1456,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_60))))))))),
inference(forward_demodulation,[],[f1337,f879]) ).
fof(f1457,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_60)))))))))),
inference(forward_demodulation,[],[f1336,f879]) ).
fof(f1458,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))),
inference(forward_demodulation,[],[f1335,f879]) ).
fof(f1492,plain,
! [X0] :
( select(earray_83,X0) = select(earray_85,X0)
| index_84 = X0 ),
inference(superposition,[],[f2,f149]) ).
fof(f1496,plain,
( earray_239 = select(queue_229,seq)
| head = seq ),
inference(superposition,[],[f421,f632]) ).
fof(f1497,plain,
( index_240 = select(queue_229,tail)
| head = tail ),
inference(superposition,[],[f461,f632]) ).
fof(f1498,plain,
index_240 = select(queue_229,tail),
inference(forward_subsumption_resolution,[],[f1497,f3]) ).
fof(f1499,plain,
earray_239 = select(queue_229,seq),
inference(forward_subsumption_resolution,[],[f1496,f4]) ).
fof(f1502,plain,
index_240 = index_228,
inference(forward_demodulation,[],[f1498,f755]) ).
fof(f1505,plain,
index_243 = s(index_228),
inference(backward_demodulation,[],[f214,f1502]) ).
fof(f1507,plain,
! [X0] :
( select(earray_239,X0) = select(earray_241,X0)
| index_228 = X0 ),
inference(backward_demodulation,[],[f548,f1502]) ).
fof(f1571,plain,
! [X0] :
( select(queue_59,X0) = select(queue_61,X0)
| tail = X0 ),
inference(superposition,[],[f2,f342]) ).
fof(f1572,plain,
index_60 = select(queue_61,tail),
inference(superposition,[],[f1,f342]) ).
fof(f1573,plain,
index_63 = index_60,
inference(backward_demodulation,[],[f474,f1572]) ).
fof(f1575,plain,
index_66 = s(index_60),
inference(backward_demodulation,[],[f247,f1573]) ).
fof(f1576,plain,
! [X0] :
( select(earray_62,X0) = select(earray_64,X0)
| index_60 = X0 ),
inference(backward_demodulation,[],[f732,f1573]) ).
fof(f1664,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))),
inference(backward_demodulation,[],[f1446,f1575]) ).
fof(f1665,plain,
index_33 != s(index_66),
inference(backward_demodulation,[],[f1448,f1575]) ).
fof(f1666,plain,
index_33 != index_66,
inference(backward_demodulation,[],[f1449,f1575]) ).
fof(f1667,plain,
index_33 != s(s(index_66)),
inference(backward_demodulation,[],[f1450,f1575]) ).
fof(f1668,plain,
index_33 != s(s(s(index_66))),
inference(backward_demodulation,[],[f1451,f1575]) ).
fof(f1669,plain,
index_33 != s(s(s(s(index_66)))),
inference(backward_demodulation,[],[f1452,f1575]) ).
fof(f1670,plain,
index_33 != s(s(s(s(s(index_66))))),
inference(backward_demodulation,[],[f1453,f1575]) ).
fof(f1671,plain,
index_33 != s(s(s(s(s(s(index_66)))))),
inference(backward_demodulation,[],[f1454,f1575]) ).
fof(f1672,plain,
index_33 != s(s(s(s(s(s(s(index_66))))))),
inference(backward_demodulation,[],[f1455,f1575]) ).
fof(f1673,plain,
index_33 != s(s(s(s(s(s(s(s(index_66)))))))),
inference(backward_demodulation,[],[f1456,f1575]) ).
fof(f1674,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_66))))))))),
inference(backward_demodulation,[],[f1457,f1575]) ).
fof(f1675,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_66)))))))))),
inference(backward_demodulation,[],[f1458,f1575]) ).
fof(f1693,plain,
! [X0] :
( select(queue_190,X0) = select(queue_194,X0)
| seq = X0 ),
inference(superposition,[],[f2,f496]) ).
fof(f1694,plain,
earray_193 = select(queue_194,seq),
inference(superposition,[],[f1,f496]) ).
fof(f1740,plain,
! [X0] :
( select(earray_197,X0) = select(earray_199,X0)
| index_198 = X0 ),
inference(superposition,[],[f2,f103]) ).
fof(f1744,plain,
! [X0] :
( select(queue_259,X0) = select(queue_263,X0)
| seq = X0 ),
inference(superposition,[],[f2,f507]) ).
fof(f1761,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))),
inference(superposition,[],[f54,f609]) ).
fof(f1771,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))),
inference(forward_demodulation,[],[f1761,f574]) ).
fof(f1779,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))),
inference(forward_demodulation,[],[f1771,f1316]) ).
fof(f1785,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))),
inference(forward_demodulation,[],[f1779,f879]) ).
fof(f1789,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))),
inference(forward_demodulation,[],[f1785,f1575]) ).
fof(f1799,plain,
! [X0] :
( select(queue_280,X0) = select(queue_277,X0)
| head = X0 ),
inference(superposition,[],[f2,f330]) ).
fof(f1800,plain,
index_279 = select(queue_280,head),
inference(superposition,[],[f1,f330]) ).
fof(f1804,plain,
( index_9 = select(queue_277,tail)
| head = tail ),
inference(superposition,[],[f478,f1799]) ).
fof(f1805,plain,
index_9 = select(queue_277,tail),
inference(forward_subsumption_resolution,[],[f1804,f3]) ).
fof(f1809,plain,
! [X0] :
( select(queue_70,X0) = select(queue_67,X0)
| head = X0 ),
inference(superposition,[],[f2,f346]) ).
fof(f1810,plain,
index_69 = select(queue_70,head),
inference(superposition,[],[f1,f346]) ).
fof(f1813,plain,
( earray_71 = select(queue_67,seq)
| head = seq ),
inference(superposition,[],[f434,f1809]) ).
fof(f1814,plain,
( index_72 = select(queue_67,tail)
| head = tail ),
inference(superposition,[],[f475,f1809]) ).
fof(f1815,plain,
index_72 = select(queue_67,tail),
inference(forward_subsumption_resolution,[],[f1814,f3]) ).
fof(f1816,plain,
earray_71 = select(queue_67,seq),
inference(forward_subsumption_resolution,[],[f1813,f4]) ).
fof(f1819,plain,
! [X0] :
( select(queue_217,X0) = select(queue_215,X0)
| tail = X0 ),
inference(superposition,[],[f2,f306]) ).
fof(f1820,plain,
index_216 = select(queue_217,tail),
inference(superposition,[],[f1,f306]) ).
fof(f1821,plain,
index_219 = index_216,
inference(backward_demodulation,[],[f458,f1820]) ).
fof(f1823,plain,
index_222 = s(index_216),
inference(backward_demodulation,[],[f205,f1821]) ).
fof(f1824,plain,
! [X0] :
( select(earray_218,X0) = select(earray_220,X0)
| index_216 = X0 ),
inference(backward_demodulation,[],[f595,f1821]) ).
fof(f1934,plain,
! [X0] :
( select(queue_88,X0) = select(queue_92,X0)
| seq = X0 ),
inference(superposition,[],[f2,f520]) ).
fof(f1935,plain,
earray_91 = select(queue_92,seq),
inference(superposition,[],[f1,f520]) ).
fof(f1936,plain,
! [X0] :
( select(queue_211,X0) = select(queue_208,X0)
| head = X0 ),
inference(superposition,[],[f2,f304]) ).
fof(f1937,plain,
index_210 = select(queue_211,head),
inference(superposition,[],[f1,f304]) ).
fof(f1940,plain,
( earray_212 = select(queue_208,seq)
| head = seq ),
inference(superposition,[],[f417,f1936]) ).
fof(f1941,plain,
( index_213 = select(queue_208,tail)
| head = tail ),
inference(superposition,[],[f457,f1936]) ).
fof(f1942,plain,
index_213 = select(queue_208,tail),
inference(forward_subsumption_resolution,[],[f1941,f3]) ).
fof(f1943,plain,
earray_212 = select(queue_208,seq),
inference(forward_subsumption_resolution,[],[f1940,f4]) ).
fof(f1961,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))),
inference(superposition,[],[f53,f609]) ).
fof(f1971,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))),
inference(forward_demodulation,[],[f1961,f574]) ).
fof(f1980,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))),
inference(forward_demodulation,[],[f1971,f1316]) ).
fof(f1987,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))),
inference(forward_demodulation,[],[f1980,f879]) ).
fof(f1992,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))),
inference(forward_demodulation,[],[f1987,f1575]) ).
fof(f2002,plain,
! [X0] :
( select(queue_65,X0) = select(queue_67,X0)
| tail = X0 ),
inference(superposition,[],[f2,f344]) ).
fof(f2003,plain,
index_66 = select(queue_67,tail),
inference(superposition,[],[f1,f344]) ).
fof(f2004,plain,
index_72 = index_66,
inference(backward_demodulation,[],[f1815,f2003]) ).
fof(f2006,plain,
index_75 = s(index_66),
inference(backward_demodulation,[],[f251,f2004]) ).
fof(f2008,plain,
! [X0] :
( select(earray_71,X0) = select(earray_73,X0)
| index_66 = X0 ),
inference(backward_demodulation,[],[f859,f2004]) ).
fof(f2107,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_75)))))))))),
inference(backward_demodulation,[],[f1664,f2006]) ).
fof(f2108,plain,
index_33 != index_75,
inference(backward_demodulation,[],[f1665,f2006]) ).
fof(f2109,plain,
index_33 != s(index_75),
inference(backward_demodulation,[],[f1667,f2006]) ).
fof(f2110,plain,
index_33 != s(s(index_75)),
inference(backward_demodulation,[],[f1668,f2006]) ).
fof(f2111,plain,
index_33 != s(s(s(index_75))),
inference(backward_demodulation,[],[f1669,f2006]) ).
fof(f2112,plain,
index_33 != s(s(s(s(index_75)))),
inference(backward_demodulation,[],[f1670,f2006]) ).
fof(f2113,plain,
index_33 != s(s(s(s(s(index_75))))),
inference(backward_demodulation,[],[f1671,f2006]) ).
fof(f2114,plain,
index_33 != s(s(s(s(s(s(index_75)))))),
inference(backward_demodulation,[],[f1672,f2006]) ).
fof(f2115,plain,
index_33 != s(s(s(s(s(s(s(index_75))))))),
inference(backward_demodulation,[],[f1673,f2006]) ).
fof(f2116,plain,
index_33 != s(s(s(s(s(s(s(s(index_75)))))))),
inference(backward_demodulation,[],[f1674,f2006]) ).
fof(f2117,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_75))))))))),
inference(backward_demodulation,[],[f1675,f2006]) ).
fof(f2122,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))),
inference(backward_demodulation,[],[f1789,f2006]) ).
fof(f2130,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))),
inference(backward_demodulation,[],[f1992,f2006]) ).
fof(f2172,plain,
! [X0] :
( select(queue_13,X0) = select(queue_11,X0)
| tail = X0 ),
inference(superposition,[],[f2,f274]) ).
fof(f2173,plain,
index_12 = select(queue_13,tail),
inference(superposition,[],[f1,f274]) ).
fof(f2174,plain,
index_15 = index_12,
inference(backward_demodulation,[],[f447,f2173]) ).
fof(f2176,plain,
index_18 = s(index_12),
inference(backward_demodulation,[],[f187,f2174]) ).
fof(f2471,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))),
inference(superposition,[],[f55,f609]) ).
fof(f2483,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))),
inference(forward_demodulation,[],[f2471,f574]) ).
fof(f2494,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))),
inference(forward_demodulation,[],[f2483,f1316]) ).
fof(f2503,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))),
inference(forward_demodulation,[],[f2494,f879]) ).
fof(f2510,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))),
inference(forward_demodulation,[],[f2503,f1575]) ).
fof(f2515,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))),
inference(forward_demodulation,[],[f2510,f2006]) ).
fof(f2583,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))),
inference(superposition,[],[f52,f609]) ).
fof(f2596,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))),
inference(forward_demodulation,[],[f2583,f574]) ).
fof(f2607,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))),
inference(forward_demodulation,[],[f2596,f1316]) ).
fof(f2616,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))),
inference(forward_demodulation,[],[f2607,f879]) ).
fof(f2623,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))),
inference(forward_demodulation,[],[f2616,f1575]) ).
fof(f2628,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))),
inference(forward_demodulation,[],[f2623,f2006]) ).
fof(f2668,plain,
! [X0] :
( select(earray_191,X0) = select(earray_193,X0)
| index_192 = X0 ),
inference(superposition,[],[f2,f101]) ).
fof(f2728,plain,
! [X0] :
( select(earray_89,X0) = select(earray_91,X0)
| index_90 = X0 ),
inference(superposition,[],[f2,f151]) ).
fof(f2730,plain,
! [X0] :
( select(queue_97,X0) = select(queue_101,X0)
| seq = X0 ),
inference(superposition,[],[f2,f481]) ).
fof(f2731,plain,
earray_100 = select(queue_101,seq),
inference(superposition,[],[f1,f481]) ).
fof(f2796,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))))),
inference(superposition,[],[f51,f609]) ).
fof(f2809,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))),
inference(forward_demodulation,[],[f2796,f574]) ).
fof(f2820,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))),
inference(forward_demodulation,[],[f2809,f1316]) ).
fof(f2829,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))),
inference(forward_demodulation,[],[f2820,f879]) ).
fof(f2836,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))),
inference(forward_demodulation,[],[f2829,f1575]) ).
fof(f2841,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))),
inference(forward_demodulation,[],[f2836,f2006]) ).
fof(f2856,plain,
! [X0] :
( select(queue_206,X0) = select(queue_208,X0)
| tail = X0 ),
inference(superposition,[],[f2,f303]) ).
fof(f2857,plain,
index_207 = select(queue_208,tail),
inference(superposition,[],[f1,f303]) ).
fof(f2858,plain,
index_213 = index_207,
inference(backward_demodulation,[],[f1942,f2857]) ).
fof(f2860,plain,
index_216 = s(index_207),
inference(backward_demodulation,[],[f203,f2858]) ).
fof(f2862,plain,
! [X0] :
( select(earray_212,X0) = select(earray_214,X0)
| index_207 = X0 ),
inference(backward_demodulation,[],[f734,f2858]) ).
fof(f3042,plain,
( earray_281 = select(queue_242,seq)
| tail = seq ),
inference(superposition,[],[f427,f601]) ).
fof(f3043,plain,
( index_282 = select(queue_242,head)
| head = tail ),
inference(superposition,[],[f467,f601]) ).
fof(f3044,plain,
index_282 = select(queue_242,head),
inference(forward_subsumption_resolution,[],[f3043,f3]) ).
fof(f3045,plain,
earray_281 = select(queue_242,seq),
inference(forward_subsumption_resolution,[],[f3042,f5]) ).
fof(f3048,plain,
earray_241 = earray_281,
inference(forward_demodulation,[],[f3045,f530]) ).
fof(f3051,plain,
elem_283 = select(earray_241,index_282),
inference(backward_demodulation,[],[f153,f3048]) ).
fof(f3052,plain,
( elem_283 = select(earray_239,index_282)
| index_282 = index_228 ),
inference(superposition,[],[f3051,f1507]) ).
fof(f3055,definition,
( spl0_1
<=> index_282 = index_228 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f3057,plain,
( index_282 = index_228
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f3055]) ).
fof(f3059,definition,
( spl0_2
<=> elem_283 = select(earray_239,index_282) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f3061,plain,
( elem_283 = select(earray_239,index_282)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f3059]) ).
fof(f3063,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f3052,f3059,f3055]) ).
fof(f3066,plain,
! [X0] :
( select(queue_275,X0) = select(queue_277,X0)
| tail = X0 ),
inference(superposition,[],[f2,f328]) ).
fof(f3067,plain,
index_276 = select(queue_277,tail),
inference(superposition,[],[f1,f328]) ).
fof(f3068,plain,
index_9 = index_276,
inference(backward_demodulation,[],[f1805,f3067]) ).
fof(f3070,plain,
index_12 = s(index_276),
inference(backward_demodulation,[],[f162,f3068]) ).
fof(f3418,plain,
! [X0] :
( select(queue_181,X0) = select(queue_185,X0)
| seq = X0 ),
inference(superposition,[],[f2,f495]) ).
fof(f3419,plain,
earray_184 = select(queue_185,seq),
inference(superposition,[],[f1,f495]) ).
fof(f3444,plain,
index_33 != s(index_39),
inference(superposition,[],[f70,f609]) ).
fof(f3457,plain,
index_33 != index_45,
inference(forward_demodulation,[],[f3444,f574]) ).
fof(f3469,plain,
( earray_56 = select(queue_53,seq)
| tail = seq ),
inference(superposition,[],[f432,f875]) ).
fof(f3470,plain,
! [X0] :
( select(queue_53,X0) = select(queue_59,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f557,f875]) ).
fof(f3471,plain,
earray_56 = select(queue_53,seq),
inference(forward_subsumption_resolution,[],[f3469,f5]) ).
fof(f3473,plain,
earray_52 = earray_56,
inference(forward_demodulation,[],[f3471,f545]) ).
fof(f3476,plain,
! [X0] :
( select(earray_52,X0) = select(earray_58,X0)
| index_54 = X0 ),
inference(backward_demodulation,[],[f880,f3473]) ).
fof(f3484,plain,
( earray_41 = select(queue_38,seq)
| tail = seq ),
inference(superposition,[],[f430,f568]) ).
fof(f3485,plain,
! [X0] :
( select(queue_38,X0) = select(queue_44,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f525,f568]) ).
fof(f3486,plain,
earray_41 = select(queue_38,seq),
inference(forward_subsumption_resolution,[],[f3484,f5]) ).
fof(f3488,plain,
earray_37 = earray_41,
inference(forward_demodulation,[],[f3486,f522]) ).
fof(f3490,plain,
! [X0] :
( select(earray_37,X0) = select(earray_43,X0)
| index_39 = X0 ),
inference(backward_demodulation,[],[f571,f3488]) ).
fof(f3499,plain,
( earray_62 = select(queue_59,seq)
| tail = seq ),
inference(superposition,[],[f433,f1571]) ).
fof(f3500,plain,
! [X0] :
( select(queue_59,X0) = select(queue_65,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f587,f1571]) ).
fof(f3501,plain,
earray_62 = select(queue_59,seq),
inference(forward_subsumption_resolution,[],[f3499,f5]) ).
fof(f3503,plain,
earray_58 = earray_62,
inference(forward_demodulation,[],[f3501,f558]) ).
fof(f3506,plain,
! [X0] :
( select(earray_58,X0) = select(earray_64,X0)
| index_60 = X0 ),
inference(backward_demodulation,[],[f1576,f3503]) ).
fof(f3554,plain,
! [X0] :
( select(queue_250,X0) = select(queue_254,X0)
| seq = X0 ),
inference(superposition,[],[f2,f506]) ).
fof(f3557,plain,
( index_26 = select(queue_23,head)
| head = tail ),
inference(superposition,[],[f221,f772]) ).
fof(f3558,plain,
index_26 = select(queue_23,head),
inference(forward_subsumption_resolution,[],[f3557,f3]) ).
fof(f3561,plain,
( index_278 = select(queue_275,head)
| head = tail ),
inference(superposition,[],[f229,f3066]) ).
fof(f3562,plain,
index_278 = select(queue_275,head),
inference(forward_subsumption_resolution,[],[f3561,f3]) ).
fof(f3565,plain,
( index_47 = select(queue_44,head)
| head = tail ),
inference(superposition,[],[f239,f634]) ).
fof(f3566,plain,
index_47 = select(queue_44,head),
inference(forward_subsumption_resolution,[],[f3565,f3]) ).
fof(f3569,plain,
( index_68 = select(queue_65,head)
| head = tail ),
inference(superposition,[],[f248,f2002]) ).
fof(f3570,plain,
index_68 = select(queue_65,head),
inference(forward_subsumption_resolution,[],[f3569,f3]) ).
fof(f3573,plain,
( index_230 = select(queue_227,head)
| head = tail ),
inference(superposition,[],[f208,f754]) ).
fof(f3574,plain,
index_230 = select(queue_227,head),
inference(forward_subsumption_resolution,[],[f3573,f3]) ).
fof(f3581,plain,
( index_209 = select(queue_206,head)
| head = tail ),
inference(superposition,[],[f199,f2856]) ).
fof(f3582,plain,
index_209 = select(queue_206,head),
inference(forward_subsumption_resolution,[],[f3581,f3]) ).
fof(f3584,plain,
! [X0] :
( select(queue_103,X0) = select(queue_107,X0)
| seq = X0 ),
inference(superposition,[],[f2,f482]) ).
fof(f3585,plain,
earray_106 = select(queue_107,seq),
inference(superposition,[],[f1,f482]) ).
fof(f3612,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))))))))),
inference(superposition,[],[f50,f609]) ).
fof(f3625,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))),
inference(forward_demodulation,[],[f3612,f574]) ).
fof(f3638,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))))),
inference(forward_demodulation,[],[f3625,f1316]) ).
fof(f3649,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))))),
inference(forward_demodulation,[],[f3638,f879]) ).
fof(f3658,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))))),
inference(forward_demodulation,[],[f3649,f1575]) ).
fof(f3665,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))))),
inference(forward_demodulation,[],[f3658,f2006]) ).
fof(f3712,plain,
! [X0] :
( select(queue_74,X0) = select(queue_76,X0)
| tail = X0 ),
inference(superposition,[],[f2,f348]) ).
fof(f3713,plain,
index_75 = select(queue_76,tail),
inference(superposition,[],[f1,f348]) ).
fof(f3714,plain,
index_84 = index_75,
inference(backward_demodulation,[],[f477,f3713]) ).
fof(f3716,plain,
index_87 = s(index_75),
inference(backward_demodulation,[],[f255,f3714]) ).
fof(f3717,plain,
! [X0] :
( select(earray_83,X0) = select(earray_85,X0)
| index_75 = X0 ),
inference(backward_demodulation,[],[f1492,f3714]) ).
fof(f3825,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_87))))))))),
inference(backward_demodulation,[],[f2107,f3716]) ).
fof(f3826,plain,
index_33 != index_87,
inference(backward_demodulation,[],[f2109,f3716]) ).
fof(f3827,plain,
index_33 != s(index_87),
inference(backward_demodulation,[],[f2110,f3716]) ).
fof(f3828,plain,
index_33 != s(s(index_87)),
inference(backward_demodulation,[],[f2111,f3716]) ).
fof(f3829,plain,
index_33 != s(s(s(index_87))),
inference(backward_demodulation,[],[f2112,f3716]) ).
fof(f3830,plain,
index_33 != s(s(s(s(index_87)))),
inference(backward_demodulation,[],[f2113,f3716]) ).
fof(f3831,plain,
index_33 != s(s(s(s(s(index_87))))),
inference(backward_demodulation,[],[f2114,f3716]) ).
fof(f3832,plain,
index_33 != s(s(s(s(s(s(index_87)))))),
inference(backward_demodulation,[],[f2115,f3716]) ).
fof(f3833,plain,
index_33 != s(s(s(s(s(s(s(index_87))))))),
inference(backward_demodulation,[],[f2116,f3716]) ).
fof(f3834,plain,
index_33 != s(s(s(s(s(s(s(s(index_87)))))))),
inference(backward_demodulation,[],[f2117,f3716]) ).
fof(f3839,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))),
inference(backward_demodulation,[],[f2122,f3716]) ).
fof(f3846,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))),
inference(backward_demodulation,[],[f2130,f3716]) ).
fof(f3863,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_87)))))))))),
inference(backward_demodulation,[],[f2515,f3716]) ).
fof(f3872,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))),
inference(backward_demodulation,[],[f2628,f3716]) ).
fof(f3881,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))),
inference(backward_demodulation,[],[f2841,f3716]) ).
fof(f3912,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))))),
inference(backward_demodulation,[],[f3665,f3716]) ).
fof(f3944,plain,
( earray_83 = select(queue_74,seq)
| tail = seq ),
inference(superposition,[],[f437,f3712]) ).
fof(f3945,plain,
! [X0] :
( select(queue_74,X0) = select(queue_86,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f931,f3712]) ).
fof(f3946,plain,
earray_83 = select(queue_74,seq),
inference(forward_subsumption_resolution,[],[f3944,f5]) ).
fof(f3948,plain,
earray_73 = earray_83,
inference(forward_demodulation,[],[f3946,f737]) ).
fof(f3951,plain,
! [X0] :
( select(earray_73,X0) = select(earray_85,X0)
| index_75 = X0 ),
inference(backward_demodulation,[],[f3717,f3948]) ).
fof(f3979,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))))))))))),
inference(superposition,[],[f49,f609]) ).
fof(f3994,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))))),
inference(forward_demodulation,[],[f3979,f574]) ).
fof(f4008,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))))),
inference(forward_demodulation,[],[f3994,f1316]) ).
fof(f4020,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))))),
inference(forward_demodulation,[],[f4008,f879]) ).
fof(f4030,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))))),
inference(forward_demodulation,[],[f4020,f1575]) ).
fof(f4038,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))))),
inference(forward_demodulation,[],[f4030,f2006]) ).
fof(f4044,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))))),
inference(forward_demodulation,[],[f4038,f3716]) ).
fof(f4067,plain,
! [X0] :
( select(queue_175,X0) = select(queue_179,X0)
| seq = X0 ),
inference(superposition,[],[f2,f494]) ).
fof(f4068,plain,
earray_178 = select(queue_179,seq),
inference(superposition,[],[f1,f494]) ).
fof(f4069,plain,
! [X0] :
( select(earray_98,X0) = select(earray_100,X0)
| index_99 = X0 ),
inference(superposition,[],[f2,f73]) ).
fof(f4071,plain,
! [X0] :
( select(earray_182,X0) = select(earray_184,X0)
| index_183 = X0 ),
inference(superposition,[],[f2,f99]) ).
fof(f4099,plain,
! [X0] :
( select(queue_38,X0) = select(queue_32,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f524,f605]) ).
fof(f4113,plain,
( earray_224 = select(queue_221,seq)
| tail = seq ),
inference(superposition,[],[f419,f1012]) ).
fof(f4114,plain,
! [X0] :
( select(queue_227,X0) = select(queue_221,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f553,f1012]) ).
fof(f4115,plain,
earray_224 = select(queue_221,seq),
inference(forward_subsumption_resolution,[],[f4113,f5]) ).
fof(f4117,plain,
earray_220 = earray_224,
inference(forward_demodulation,[],[f4115,f560]) ).
fof(f4120,plain,
! [X0] :
( select(earray_226,X0) = select(earray_220,X0)
| index_222 = X0 ),
inference(backward_demodulation,[],[f1017,f4117]) ).
fof(f4128,plain,
( earray_218 = select(queue_215,seq)
| tail = seq ),
inference(superposition,[],[f418,f1819]) ).
fof(f4129,plain,
! [X0] :
( select(queue_221,X0) = select(queue_215,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f559,f1819]) ).
fof(f4130,plain,
earray_218 = select(queue_215,seq),
inference(forward_subsumption_resolution,[],[f4128,f5]) ).
fof(f4132,plain,
earray_214 = earray_218,
inference(forward_demodulation,[],[f4130,f590]) ).
fof(f4135,plain,
! [X0] :
( select(earray_220,X0) = select(earray_214,X0)
| index_216 = X0 ),
inference(backward_demodulation,[],[f1824,f4132]) ).
fof(f4148,plain,
! [X0] :
( select(queue_23,X0) = select(queue_17,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f551,f1080]) ).
fof(f4163,plain,
! [X0] :
( select(queue_17,X0) = select(queue_11,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f555,f2172]) ).
fof(f4175,plain,
! [X0] :
( select(queue_271,X0) = select(queue_269,X0)
| tail = X0 ),
inference(superposition,[],[f2,f326]) ).
fof(f4176,plain,
index_270 = select(queue_271,tail),
inference(superposition,[],[f1,f326]) ).
fof(f4177,plain,
index_273 = index_270,
inference(backward_demodulation,[],[f466,f4176]) ).
fof(f4179,plain,
index_276 = s(index_270),
inference(backward_demodulation,[],[f228,f4177]) ).
fof(f4619,plain,
! [X0] :
( select(queue_275,X0) = select(queue_269,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f774,f4175]) ).
fof(f4654,plain,
! [X0] :
( select(queue_202,X0) = select(queue_200,X0)
| tail = X0 ),
inference(superposition,[],[f2,f301]) ).
fof(f4655,plain,
index_201 = select(queue_202,tail),
inference(superposition,[],[f1,f301]) ).
fof(f4656,plain,
index_204 = index_201,
inference(backward_demodulation,[],[f455,f4655]) ).
fof(f4658,plain,
index_207 = s(index_201),
inference(backward_demodulation,[],[f198,f4656]) ).
fof(f4659,plain,
! [X0] :
( select(earray_203,X0) = select(earray_205,X0)
| index_201 = X0 ),
inference(backward_demodulation,[],[f929,f4656]) ).
fof(f4894,plain,
( earray_203 = select(queue_200,seq)
| tail = seq ),
inference(superposition,[],[f416,f4654]) ).
fof(f4895,plain,
! [X0] :
( select(queue_206,X0) = select(queue_200,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f752,f4654]) ).
fof(f4896,plain,
earray_203 = select(queue_200,seq),
inference(forward_subsumption_resolution,[],[f4894,f5]) ).
fof(f4898,plain,
earray_199 = earray_203,
inference(forward_demodulation,[],[f4896,f926]) ).
fof(f4901,plain,
! [X0] :
( select(earray_205,X0) = select(earray_199,X0)
| index_201 = X0 ),
inference(backward_demodulation,[],[f4659,f4898]) ).
fof(f4931,plain,
index_33 != 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))))))))))))))))))))))),
inference(superposition,[],[f48,f609]) ).
fof(f4946,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))))),
inference(forward_demodulation,[],[f4931,f574]) ).
fof(f4962,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))))))))))),
inference(forward_demodulation,[],[f4946,f1316]) ).
fof(f4976,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))))))))))),
inference(forward_demodulation,[],[f4962,f879]) ).
fof(f4988,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))))))))))),
inference(forward_demodulation,[],[f4976,f1575]) ).
fof(f4998,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75)))))))))))))))))),
inference(forward_demodulation,[],[f4988,f2006]) ).
fof(f5006,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87))))))))))))))))),
inference(forward_demodulation,[],[f4998,f3716]) ).
fof(f5034,plain,
! [X0] :
( select(queue_109,X0) = select(queue_113,X0)
| seq = X0 ),
inference(superposition,[],[f2,f484]) ).
fof(f5035,plain,
earray_112 = select(queue_113,seq),
inference(superposition,[],[f1,f484]) ).
fof(f5040,plain,
! [X0] :
( select(queue_238,X0) = select(queue_248,X0)
| seq = X0 ),
inference(superposition,[],[f2,f505]) ).
fof(f5094,plain,
! [X0] :
( select(queue_86,X0) = select(queue_88,X0)
| tail = X0 ),
inference(superposition,[],[f2,f352]) ).
fof(f5095,plain,
index_87 = select(queue_88,tail),
inference(superposition,[],[f1,f352]) ).
fof(f5096,plain,
index_90 = index_87,
inference(backward_demodulation,[],[f479,f5095]) ).
fof(f5098,plain,
index_93 = s(index_87),
inference(backward_demodulation,[],[f258,f5096]) ).
fof(f5119,plain,
! [X0] :
( select(earray_89,X0) = select(earray_91,X0)
| index_87 = X0 ),
inference(backward_demodulation,[],[f2728,f5096]) ).
fof(f5224,plain,
index_33 != s(s(s(s(s(s(s(s(index_93)))))))),
inference(backward_demodulation,[],[f3825,f5098]) ).
fof(f5225,plain,
index_33 != index_93,
inference(backward_demodulation,[],[f3827,f5098]) ).
fof(f5226,plain,
index_33 != s(index_93),
inference(backward_demodulation,[],[f3828,f5098]) ).
fof(f5227,plain,
index_33 != s(s(index_93)),
inference(backward_demodulation,[],[f3829,f5098]) ).
fof(f5228,plain,
index_33 != s(s(s(index_93))),
inference(backward_demodulation,[],[f3830,f5098]) ).
fof(f5229,plain,
index_33 != s(s(s(s(index_93)))),
inference(backward_demodulation,[],[f3831,f5098]) ).
fof(f5230,plain,
index_33 != s(s(s(s(s(index_93))))),
inference(backward_demodulation,[],[f3832,f5098]) ).
fof(f5231,plain,
index_33 != s(s(s(s(s(s(index_93)))))),
inference(backward_demodulation,[],[f3833,f5098]) ).
fof(f5232,plain,
index_33 != s(s(s(s(s(s(s(index_93))))))),
inference(backward_demodulation,[],[f3834,f5098]) ).
fof(f5237,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_93)))))))))),
inference(backward_demodulation,[],[f3839,f5098]) ).
fof(f5244,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))),
inference(backward_demodulation,[],[f3846,f5098]) ).
fof(f5260,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_93))))))))),
inference(backward_demodulation,[],[f3863,f5098]) ).
fof(f5269,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))),
inference(backward_demodulation,[],[f3872,f5098]) ).
fof(f5278,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))),
inference(backward_demodulation,[],[f3881,f5098]) ).
fof(f5297,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))))),
inference(backward_demodulation,[],[f3912,f5098]) ).
fof(f5308,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))))),
inference(backward_demodulation,[],[f4044,f5098]) ).
fof(f5340,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93)))))))))))))))),
inference(backward_demodulation,[],[f5006,f5098]) ).
fof(f5375,plain,
( earray_89 = select(queue_86,seq)
| tail = seq ),
inference(superposition,[],[f438,f5094]) ).
fof(f5376,plain,
! [X0] :
( select(queue_86,X0) = select(queue_92,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f1934,f5094]) ).
fof(f5377,plain,
earray_89 = select(queue_86,seq),
inference(forward_subsumption_resolution,[],[f5375,f5]) ).
fof(f5379,plain,
earray_85 = earray_89,
inference(forward_demodulation,[],[f5377,f932]) ).
fof(f5382,plain,
! [X0] :
( select(earray_85,X0) = select(earray_91,X0)
| index_87 = X0 ),
inference(backward_demodulation,[],[f5119,f5379]) ).
fof(f5390,plain,
! [X0] :
( select(queue_160,X0) = select(queue_236,X0)
| seq = X0 ),
inference(superposition,[],[f2,f503]) ).
fof(f5392,plain,
! [X0] :
( select(earray_176,X0) = select(earray_178,X0)
| index_177 = X0 ),
inference(superposition,[],[f2,f97]) ).
fof(f5394,plain,
! [X0] :
( select(earray_104,X0) = select(earray_106,X0)
| index_105 = X0 ),
inference(superposition,[],[f2,f75]) ).
fof(f5396,plain,
! [X0] :
( select(queue_169,X0) = select(queue_173,X0)
| seq = X0 ),
inference(superposition,[],[f2,f493]) ).
fof(f5397,plain,
earray_172 = select(queue_173,seq),
inference(superposition,[],[f1,f493]) ).
fof(f5423,plain,
index_33 != 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)))))))))))))))))))))))),
inference(superposition,[],[f47,f609]) ).
fof(f5440,plain,
index_33 != 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))))))))))))))))))))))),
inference(forward_demodulation,[],[f5423,f574]) ).
fof(f5457,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))))))))))))),
inference(forward_demodulation,[],[f5440,f1316]) ).
fof(f5472,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))))))),
inference(forward_demodulation,[],[f5457,f879]) ).
fof(f5485,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))))))),
inference(forward_demodulation,[],[f5472,f1575]) ).
fof(f5496,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))))))),
inference(forward_demodulation,[],[f5485,f2006]) ).
fof(f5505,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))))))),
inference(forward_demodulation,[],[f5496,f3716]) ).
fof(f5512,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))))))),
inference(forward_demodulation,[],[f5505,f5098]) ).
fof(f5540,plain,
! [X0] :
( select(queue_97,X0) = select(queue_94,X0)
| head = X0 ),
inference(superposition,[],[f2,f355]) ).
fof(f5541,plain,
index_96 = select(queue_97,head),
inference(superposition,[],[f1,f355]) ).
fof(f5545,plain,
( earray_98 = select(queue_94,seq)
| head = seq ),
inference(superposition,[],[f439,f5540]) ).
fof(f5547,plain,
( index_99 = select(queue_94,tail)
| head = tail ),
inference(superposition,[],[f480,f5540]) ).
fof(f5548,plain,
index_99 = select(queue_94,tail),
inference(forward_subsumption_resolution,[],[f5547,f3]) ).
fof(f5549,plain,
earray_98 = select(queue_94,seq),
inference(forward_subsumption_resolution,[],[f5545,f4]) ).
fof(f5585,plain,
! [X0] :
( select(queue_259,X0) = select(queue_256,X0)
| head = X0 ),
inference(superposition,[],[f2,f322]) ).
fof(f5586,plain,
index_258 = select(queue_259,head),
inference(superposition,[],[f1,f322]) ).
fof(f5591,plain,
( index_261 = select(queue_256,tail)
| head = tail ),
inference(superposition,[],[f464,f5585]) ).
fof(f5593,plain,
index_261 = select(queue_256,tail),
inference(forward_subsumption_resolution,[],[f5591,f3]) ).
fof(f5622,plain,
! [X0] :
( select(queue_265,X0) = select(queue_263,X0)
| tail = X0 ),
inference(superposition,[],[f2,f324]) ).
fof(f5623,plain,
index_264 = select(queue_265,tail),
inference(superposition,[],[f1,f324]) ).
fof(f5624,plain,
index_267 = index_264,
inference(backward_demodulation,[],[f465,f5623]) ).
fof(f5626,plain,
index_270 = s(index_264),
inference(backward_demodulation,[],[f226,f5624]) ).
fof(f6164,plain,
! [X0] :
( select(queue_269,X0) = select(queue_263,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f961,f5622]) ).
fof(f6251,plain,
! [X0] :
( select(queue_196,X0) = select(queue_194,X0)
| tail = X0 ),
inference(superposition,[],[f2,f299]) ).
fof(f6252,plain,
index_195 = select(queue_196,tail),
inference(superposition,[],[f1,f299]) ).
fof(f6253,plain,
index_198 = index_195,
inference(backward_demodulation,[],[f454,f6252]) ).
fof(f6255,plain,
index_201 = s(index_195),
inference(backward_demodulation,[],[f196,f6253]) ).
fof(f6256,plain,
! [X0] :
( select(earray_197,X0) = select(earray_199,X0)
| index_195 = X0 ),
inference(backward_demodulation,[],[f1740,f6253]) ).
fof(f6552,plain,
( earray_197 = select(queue_194,seq)
| tail = seq ),
inference(superposition,[],[f413,f6251]) ).
fof(f6553,plain,
! [X0] :
( select(queue_200,X0) = select(queue_194,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f925,f6251]) ).
fof(f6554,plain,
earray_197 = select(queue_194,seq),
inference(forward_subsumption_resolution,[],[f6552,f5]) ).
fof(f6556,plain,
earray_193 = earray_197,
inference(forward_demodulation,[],[f6554,f1694]) ).
fof(f6559,plain,
! [X0] :
( select(earray_199,X0) = select(earray_193,X0)
| index_195 = X0 ),
inference(backward_demodulation,[],[f6256,f6556]) ).
fof(f6565,plain,
! [X0] :
( select(queue_92,X0) = select(queue_94,X0)
| tail = X0 ),
inference(superposition,[],[f2,f354]) ).
fof(f6566,plain,
index_93 = select(queue_94,tail),
inference(superposition,[],[f1,f354]) ).
fof(f6567,plain,
index_99 = index_93,
inference(backward_demodulation,[],[f5548,f6566]) ).
fof(f6569,plain,
index_102 = s(index_93),
inference(backward_demodulation,[],[f155,f6567]) ).
fof(f6572,plain,
! [X0] :
( select(earray_98,X0) = select(earray_100,X0)
| index_93 = X0 ),
inference(backward_demodulation,[],[f4069,f6567]) ).
fof(f6712,plain,
index_33 != s(s(s(s(s(s(s(index_102))))))),
inference(backward_demodulation,[],[f5224,f6569]) ).
fof(f6713,plain,
index_102 != index_33,
inference(backward_demodulation,[],[f5226,f6569]) ).
fof(f6714,plain,
index_33 != s(index_102),
inference(backward_demodulation,[],[f5227,f6569]) ).
fof(f6715,plain,
index_33 != s(s(index_102)),
inference(backward_demodulation,[],[f5228,f6569]) ).
fof(f6716,plain,
index_33 != s(s(s(index_102))),
inference(backward_demodulation,[],[f5229,f6569]) ).
fof(f6717,plain,
index_33 != s(s(s(s(index_102)))),
inference(backward_demodulation,[],[f5230,f6569]) ).
fof(f6718,plain,
index_33 != s(s(s(s(s(index_102))))),
inference(backward_demodulation,[],[f5231,f6569]) ).
fof(f6719,plain,
index_33 != s(s(s(s(s(s(index_102)))))),
inference(backward_demodulation,[],[f5232,f6569]) ).
fof(f6724,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_102))))))))),
inference(backward_demodulation,[],[f5237,f6569]) ).
fof(f6731,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_102)))))))))),
inference(backward_demodulation,[],[f5244,f6569]) ).
fof(f6746,plain,
index_33 != s(s(s(s(s(s(s(s(index_102)))))))),
inference(backward_demodulation,[],[f5260,f6569]) ).
fof(f6755,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))),
inference(backward_demodulation,[],[f5269,f6569]) ).
fof(f6764,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))),
inference(backward_demodulation,[],[f5278,f6569]) ).
fof(f6782,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))))),
inference(backward_demodulation,[],[f5297,f6569]) ).
fof(f6793,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))))),
inference(backward_demodulation,[],[f5308,f6569]) ).
fof(f6814,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102))))))))))))))),
inference(backward_demodulation,[],[f5340,f6569]) ).
fof(f6827,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))))))),
inference(backward_demodulation,[],[f5512,f6569]) ).
fof(f6886,plain,
( index_95 = select(queue_92,head)
| head = tail ),
inference(superposition,[],[f259,f6565]) ).
fof(f6887,plain,
index_95 = select(queue_92,head),
inference(forward_subsumption_resolution,[],[f6886,f3]) ).
fof(f6889,plain,
! [X0] :
( select(queue_190,X0) = select(queue_187,X0)
| head = X0 ),
inference(superposition,[],[f2,f297]) ).
fof(f6890,plain,
index_189 = select(queue_190,head),
inference(superposition,[],[f1,f297]) ).
fof(f6894,plain,
( earray_191 = select(queue_187,seq)
| head = seq ),
inference(superposition,[],[f412,f6889]) ).
fof(f6895,plain,
( index_192 = select(queue_187,tail)
| head = tail ),
inference(superposition,[],[f453,f6889]) ).
fof(f6897,plain,
index_192 = select(queue_187,tail),
inference(forward_subsumption_resolution,[],[f6895,f3]) ).
fof(f6898,plain,
earray_191 = select(queue_187,seq),
inference(forward_subsumption_resolution,[],[f6894,f4]) ).
fof(f6957,plain,
index_39 != 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_45))))))))))))))))))))))))),
inference(superposition,[],[f46,f574]) ).
fof(f6974,plain,
index_39 != 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_54)))))))))))))))))))))))),
inference(forward_demodulation,[],[f6957,f1316]) ).
fof(f6994,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))))))))),
inference(forward_demodulation,[],[f6974,f879]) ).
fof(f7012,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))))))))),
inference(forward_demodulation,[],[f6994,f1575]) ).
fof(f7028,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_75))))))))))))))))))))),
inference(forward_demodulation,[],[f7012,f2006]) ).
fof(f7042,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_87)))))))))))))))))))),
inference(forward_demodulation,[],[f7028,f3716]) ).
fof(f7054,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))))))))))),
inference(forward_demodulation,[],[f7042,f5098]) ).
fof(f7064,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_102)))))))))))))))))),
inference(forward_demodulation,[],[f7054,f6569]) ).
fof(f7135,plain,
! [X0] :
( select(queue_118,X0) = select(queue_122,X0)
| seq = X0 ),
inference(superposition,[],[f2,f485]) ).
fof(f7136,plain,
earray_121 = select(queue_122,seq),
inference(superposition,[],[f1,f485]) ).
fof(f7143,plain,
! [X0] :
( select(earray_110,X0) = select(earray_112,X0)
| index_111 = X0 ),
inference(superposition,[],[f2,f77]) ).
fof(f7145,plain,
! [X0] :
( select(earray_170,X0) = select(earray_172,X0)
| index_171 = X0 ),
inference(superposition,[],[f2,f95]) ).
fof(f7385,plain,
! [X0] :
( select(queue_254,X0) = select(queue_256,X0)
| tail = X0 ),
inference(superposition,[],[f2,f321]) ).
fof(f7386,plain,
index_255 = select(queue_256,tail),
inference(superposition,[],[f1,f321]) ).
fof(f7387,plain,
index_261 = index_255,
inference(backward_demodulation,[],[f5593,f7386]) ).
fof(f7389,plain,
index_264 = s(index_255),
inference(backward_demodulation,[],[f223,f7387]) ).
fof(f8036,plain,
( index_257 = select(queue_254,head)
| head = tail ),
inference(superposition,[],[f219,f7385]) ).
fof(f8037,plain,
index_257 = select(queue_254,head),
inference(forward_subsumption_resolution,[],[f8036,f3]) ).
fof(f8039,plain,
! [X0] :
( select(queue_151,X0) = select(queue_164,X0)
| seq = X0 ),
inference(superposition,[],[f2,f491]) ).
fof(f8040,plain,
earray_163 = select(queue_164,seq),
inference(superposition,[],[f1,f491]) ).
fof(f8072,plain,
! [X0] :
( select(queue_185,X0) = select(queue_187,X0)
| tail = X0 ),
inference(superposition,[],[f2,f295]) ).
fof(f8073,plain,
index_186 = select(queue_187,tail),
inference(superposition,[],[f1,f295]) ).
fof(f8074,plain,
index_192 = index_186,
inference(backward_demodulation,[],[f6897,f8073]) ).
fof(f8076,plain,
index_195 = s(index_186),
inference(backward_demodulation,[],[f194,f8074]) ).
fof(f8078,plain,
! [X0] :
( select(earray_191,X0) = select(earray_193,X0)
| index_186 = X0 ),
inference(backward_demodulation,[],[f2668,f8074]) ).
fof(f8444,plain,
( index_188 = select(queue_185,head)
| head = tail ),
inference(superposition,[],[f191,f8072]) ).
fof(f8445,plain,
index_188 = select(queue_185,head),
inference(forward_subsumption_resolution,[],[f8444,f3]) ).
fof(f8474,plain,
! [X0] :
( select(q,X0) = select(queue_1,X0)
| head = X0 ),
inference(superposition,[],[f2,f262]) ).
fof(f8475,plain,
index_0 = select(queue_1,head),
inference(superposition,[],[f1,f262]) ).
fof(f8719,plain,
! [X0] :
( select(queue_82,X0) = select(queue_155,X0)
| seq = X0 ),
inference(superposition,[],[f2,f490]) ).
fof(f8721,plain,
! [X0] :
( select(queue_124,X0) = select(queue_128,X0)
| seq = X0 ),
inference(superposition,[],[f2,f486]) ).
fof(f8722,plain,
earray_127 = select(queue_128,seq),
inference(superposition,[],[f1,f486]) ).
fof(f8731,plain,
! [X0] :
( select(earray_119,X0) = select(earray_121,X0)
| index_120 = X0 ),
inference(superposition,[],[f2,f79]) ).
fof(f8789,plain,
! [X0] :
( select(earray_161,X0) = select(earray_163,X0)
| index_162 = X0 ),
inference(superposition,[],[f2,f93]) ).
fof(f8793,plain,
! [X0] :
( select(queue_145,X0) = select(queue_149,X0)
| seq = X0 ),
inference(superposition,[],[f2,f489]) ).
fof(f8794,plain,
earray_148 = select(queue_149,seq),
inference(superposition,[],[f1,f489]) ).
fof(f9042,plain,
! [X0] :
( select(queue_250,X0) = select(queue_248,X0)
| tail = X0 ),
inference(superposition,[],[f2,f319]) ).
fof(f9043,plain,
index_249 = select(queue_250,tail),
inference(superposition,[],[f1,f319]) ).
fof(f9044,plain,
index_252 = index_249,
inference(backward_demodulation,[],[f463,f9043]) ).
fof(f9046,plain,
index_255 = s(index_249),
inference(backward_demodulation,[],[f218,f9044]) ).
fof(f9781,plain,
! [X0] :
( select(queue_254,X0) = select(queue_248,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f3554,f9042]) ).
fof(f9822,plain,
! [X0] :
( select(queue_101,X0) = select(queue_103,X0)
| tail = X0 ),
inference(superposition,[],[f2,f264]) ).
fof(f9823,plain,
index_102 = select(queue_103,tail),
inference(superposition,[],[f1,f264]) ).
fof(f9824,plain,
index_105 = index_102,
inference(backward_demodulation,[],[f440,f9823]) ).
fof(f9826,plain,
index_108 = s(index_102),
inference(backward_demodulation,[],[f157,f9824]) ).
fof(f9828,plain,
! [X0] :
( select(earray_104,X0) = select(earray_106,X0)
| index_102 = X0 ),
inference(backward_demodulation,[],[f5394,f9824]) ).
fof(f9987,plain,
index_33 != s(s(s(s(s(s(index_108)))))),
inference(backward_demodulation,[],[f6712,f9826]) ).
fof(f9988,plain,
index_108 != index_33,
inference(backward_demodulation,[],[f6714,f9826]) ).
fof(f9989,plain,
index_33 != s(index_108),
inference(backward_demodulation,[],[f6715,f9826]) ).
fof(f9990,plain,
index_33 != s(s(index_108)),
inference(backward_demodulation,[],[f6716,f9826]) ).
fof(f9991,plain,
index_33 != s(s(s(index_108))),
inference(backward_demodulation,[],[f6717,f9826]) ).
fof(f9992,plain,
index_33 != s(s(s(s(index_108)))),
inference(backward_demodulation,[],[f6718,f9826]) ).
fof(f9993,plain,
index_33 != s(s(s(s(s(index_108))))),
inference(backward_demodulation,[],[f6719,f9826]) ).
fof(f9998,plain,
index_33 != s(s(s(s(s(s(s(s(index_108)))))))),
inference(backward_demodulation,[],[f6724,f9826]) ).
fof(f10005,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_108))))))))),
inference(backward_demodulation,[],[f6731,f9826]) ).
fof(f10019,plain,
index_33 != s(s(s(s(s(s(s(index_108))))))),
inference(backward_demodulation,[],[f6746,f9826]) ).
fof(f10028,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_108)))))))))),
inference(backward_demodulation,[],[f6755,f9826]) ).
fof(f10037,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))),
inference(backward_demodulation,[],[f6764,f9826]) ).
fof(f10054,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_108)))))))))))),
inference(backward_demodulation,[],[f6782,f9826]) ).
fof(f10065,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))))),
inference(backward_demodulation,[],[f6793,f9826]) ).
fof(f10085,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108)))))))))))))),
inference(backward_demodulation,[],[f6814,f9826]) ).
fof(f10098,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))))))),
inference(backward_demodulation,[],[f6827,f9826]) ).
fof(f10121,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_108))))))))))))))))),
inference(backward_demodulation,[],[f7064,f9826]) ).
fof(f10243,plain,
( earray_104 = select(queue_101,seq)
| tail = seq ),
inference(superposition,[],[f399,f9822]) ).
fof(f10244,plain,
! [X0] :
( select(queue_101,X0) = select(queue_107,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f3584,f9822]) ).
fof(f10245,plain,
earray_104 = select(queue_101,seq),
inference(forward_subsumption_resolution,[],[f10243,f5]) ).
fof(f10247,plain,
earray_100 = earray_104,
inference(forward_demodulation,[],[f10245,f2731]) ).
fof(f10250,plain,
! [X0] :
( select(earray_100,X0) = select(earray_106,X0)
| index_102 = X0 ),
inference(backward_demodulation,[],[f9828,f10247]) ).
fof(f10256,plain,
! [X0] :
( select(queue_181,X0) = select(queue_179,X0)
| tail = X0 ),
inference(superposition,[],[f2,f293]) ).
fof(f10257,plain,
index_180 = select(queue_181,tail),
inference(superposition,[],[f1,f293]) ).
fof(f10258,plain,
index_183 = index_180,
inference(backward_demodulation,[],[f452,f10257]) ).
fof(f10260,plain,
index_186 = s(index_180),
inference(backward_demodulation,[],[f190,f10258]) ).
fof(f10262,plain,
! [X0] :
( select(earray_182,X0) = select(earray_184,X0)
| index_180 = X0 ),
inference(backward_demodulation,[],[f4071,f10258]) ).
fof(f10697,plain,
( earray_182 = select(queue_179,seq)
| tail = seq ),
inference(superposition,[],[f411,f10256]) ).
fof(f10698,plain,
! [X0] :
( select(queue_185,X0) = select(queue_179,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f3418,f10256]) ).
fof(f10699,plain,
earray_182 = select(queue_179,seq),
inference(forward_subsumption_resolution,[],[f10697,f5]) ).
fof(f10701,plain,
earray_178 = earray_182,
inference(forward_demodulation,[],[f10699,f4068]) ).
fof(f10704,plain,
! [X0] :
( select(earray_184,X0) = select(earray_178,X0)
| index_180 = X0 ),
inference(backward_demodulation,[],[f10262,f10701]) ).
fof(f10739,plain,
! [X0] :
( select(queue_7,X0) = select(queue_80,X0)
| seq = X0 ),
inference(superposition,[],[f2,f518]) ).
fof(f10747,plain,
! [X0] :
( select(queue_130,X0) = select(queue_134,X0)
| seq = X0 ),
inference(superposition,[],[f2,f487]) ).
fof(f10748,plain,
earray_133 = select(queue_134,seq),
inference(superposition,[],[f1,f487]) ).
fof(f11014,plain,
( index_3 = select(q,tail)
| head = tail ),
inference(superposition,[],[f8474,f468]) ).
fof(f11015,plain,
index_3 = select(q,tail),
inference(forward_subsumption_resolution,[],[f11014,f3]) ).
fof(f11017,plain,
index_3 = index_0,
inference(forward_demodulation,[],[f11015,f154]) ).
fof(f11020,plain,
index_6 = s(index_0),
inference(backward_demodulation,[],[f244,f11017]) ).
fof(f11086,plain,
! [X0] :
( select(earray_125,X0) = select(earray_127,X0)
| index_126 = X0 ),
inference(superposition,[],[f2,f81]) ).
fof(f11088,plain,
! [X0] :
( select(queue_1,X0) = select(queue_5,X0)
| seq = X0 ),
inference(superposition,[],[f2,f513]) ).
fof(f11096,plain,
! [X0] :
( select(earray_146,X0) = select(earray_148,X0)
| index_147 = X0 ),
inference(superposition,[],[f2,f88]) ).
fof(f11098,plain,
! [X0] :
( select(queue_139,X0) = select(queue_143,X0)
| seq = X0 ),
inference(superposition,[],[f2,f488]) ).
fof(f11099,plain,
earray_142 = select(queue_143,seq),
inference(superposition,[],[f1,f488]) ).
fof(f11104,plain,
! [X0] :
( select(queue_107,X0) = select(queue_109,X0)
| tail = X0 ),
inference(superposition,[],[f2,f266]) ).
fof(f11105,plain,
index_108 = select(queue_109,tail),
inference(superposition,[],[f1,f266]) ).
fof(f11106,plain,
index_111 = index_108,
inference(backward_demodulation,[],[f441,f11105]) ).
fof(f11108,plain,
index_114 = s(index_108),
inference(backward_demodulation,[],[f159,f11106]) ).
fof(f11136,plain,
! [X0] :
( select(earray_110,X0) = select(earray_112,X0)
| index_108 = X0 ),
inference(backward_demodulation,[],[f7143,f11106]) ).
fof(f11288,plain,
index_33 != s(s(s(s(s(index_114))))),
inference(backward_demodulation,[],[f9987,f11108]) ).
fof(f11289,plain,
index_114 != index_33,
inference(backward_demodulation,[],[f9989,f11108]) ).
fof(f11290,plain,
index_33 != s(index_114),
inference(backward_demodulation,[],[f9990,f11108]) ).
fof(f11291,plain,
index_33 != s(s(index_114)),
inference(backward_demodulation,[],[f9991,f11108]) ).
fof(f11292,plain,
index_33 != s(s(s(index_114))),
inference(backward_demodulation,[],[f9992,f11108]) ).
fof(f11293,plain,
index_33 != s(s(s(s(index_114)))),
inference(backward_demodulation,[],[f9993,f11108]) ).
fof(f11298,plain,
index_33 != s(s(s(s(s(s(s(index_114))))))),
inference(backward_demodulation,[],[f9998,f11108]) ).
fof(f11305,plain,
index_33 != s(s(s(s(s(s(s(s(index_114)))))))),
inference(backward_demodulation,[],[f10005,f11108]) ).
fof(f11318,plain,
index_33 != s(s(s(s(s(s(index_114)))))),
inference(backward_demodulation,[],[f10019,f11108]) ).
fof(f11327,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_114))))))))),
inference(backward_demodulation,[],[f10028,f11108]) ).
fof(f11336,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_114)))))))))),
inference(backward_demodulation,[],[f10037,f11108]) ).
fof(f11352,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))),
inference(backward_demodulation,[],[f10054,f11108]) ).
fof(f11363,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))),
inference(backward_demodulation,[],[f10065,f11108]) ).
fof(f11382,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))))),
inference(backward_demodulation,[],[f10085,f11108]) ).
fof(f11395,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))))),
inference(backward_demodulation,[],[f10098,f11108]) ).
fof(f11417,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))))))),
inference(backward_demodulation,[],[f10121,f11108]) ).
fof(f11556,plain,
( earray_110 = select(queue_107,seq)
| tail = seq ),
inference(superposition,[],[f400,f11104]) ).
fof(f11557,plain,
! [X0] :
( select(queue_107,X0) = select(queue_113,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f5034,f11104]) ).
fof(f11558,plain,
earray_110 = select(queue_107,seq),
inference(forward_subsumption_resolution,[],[f11556,f5]) ).
fof(f11560,plain,
earray_106 = earray_110,
inference(forward_demodulation,[],[f11558,f3585]) ).
fof(f11563,plain,
! [X0] :
( select(earray_106,X0) = select(earray_112,X0)
| index_108 = X0 ),
inference(backward_demodulation,[],[f11136,f11560]) ).
fof(f11569,plain,
! [X0] :
( select(queue_238,X0) = select(queue_236,X0)
| tail = X0 ),
inference(superposition,[],[f2,f314]) ).
fof(f11570,plain,
index_237 = select(queue_238,tail),
inference(superposition,[],[f1,f314]) ).
fof(f11571,plain,
index_246 = index_237,
inference(backward_demodulation,[],[f462,f11570]) ).
fof(f11573,plain,
index_249 = s(index_237),
inference(backward_demodulation,[],[f216,f11571]) ).
fof(f12412,plain,
! [X0] :
( select(queue_248,X0) = select(queue_236,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f5040,f11569]) ).
fof(f12723,plain,
! [X0] :
( select(queue_175,X0) = select(queue_173,X0)
| tail = X0 ),
inference(superposition,[],[f2,f291]) ).
fof(f12724,plain,
index_174 = select(queue_175,tail),
inference(superposition,[],[f1,f291]) ).
fof(f12725,plain,
index_177 = index_174,
inference(backward_demodulation,[],[f451,f12724]) ).
fof(f12727,plain,
index_180 = s(index_174),
inference(backward_demodulation,[],[f188,f12725]) ).
fof(f12730,plain,
! [X0] :
( select(earray_176,X0) = select(earray_178,X0)
| index_174 = X0 ),
inference(backward_demodulation,[],[f5392,f12725]) ).
fof(f13243,plain,
( earray_176 = select(queue_173,seq)
| tail = seq ),
inference(superposition,[],[f410,f12723]) ).
fof(f13244,plain,
! [X0] :
( select(queue_179,X0) = select(queue_173,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f4067,f12723]) ).
fof(f13245,plain,
earray_176 = select(queue_173,seq),
inference(forward_subsumption_resolution,[],[f13243,f5]) ).
fof(f13247,plain,
earray_172 = earray_176,
inference(forward_demodulation,[],[f13245,f5397]) ).
fof(f13250,plain,
! [X0] :
( select(earray_178,X0) = select(earray_172,X0)
| index_174 = X0 ),
inference(backward_demodulation,[],[f12730,f13247]) ).
fof(f13257,plain,
( index_0 = select(queue_5,head)
| head = seq ),
inference(superposition,[],[f11088,f8475]) ).
fof(f13258,plain,
index_0 = select(queue_5,head),
inference(forward_subsumption_resolution,[],[f13257,f4]) ).
fof(f13262,plain,
! [X0] :
( select(queue_160,X0) = select(queue_157,X0)
| head = X0 ),
inference(superposition,[],[f2,f285]) ).
fof(f13263,plain,
index_159 = select(queue_160,head),
inference(superposition,[],[f1,f285]) ).
fof(f13269,plain,
( index_234 = select(queue_157,tail)
| head = tail ),
inference(superposition,[],[f460,f13262]) ).
fof(f13270,plain,
index_234 = select(queue_157,tail),
inference(forward_subsumption_resolution,[],[f13269,f3]) ).
fof(f13280,plain,
! [X0] :
( select(queue_169,X0) = select(queue_166,X0)
| head = X0 ),
inference(superposition,[],[f2,f288]) ).
fof(f13281,plain,
index_168 = select(queue_169,head),
inference(superposition,[],[f1,f288]) ).
fof(f13285,plain,
( earray_170 = select(queue_166,seq)
| head = seq ),
inference(superposition,[],[f409,f13280]) ).
fof(f13287,plain,
( index_171 = select(queue_166,tail)
| head = tail ),
inference(superposition,[],[f450,f13280]) ).
fof(f13288,plain,
index_171 = select(queue_166,tail),
inference(forward_subsumption_resolution,[],[f13287,f3]) ).
fof(f13289,plain,
earray_170 = select(queue_166,seq),
inference(forward_subsumption_resolution,[],[f13285,f4]) ).
fof(f13296,plain,
! [X0] :
( select(queue_118,X0) = select(queue_115,X0)
| head = X0 ),
inference(superposition,[],[f2,f270]) ).
fof(f13297,plain,
index_117 = select(queue_118,head),
inference(superposition,[],[f1,f270]) ).
fof(f13301,plain,
( earray_119 = select(queue_115,seq)
| head = seq ),
inference(superposition,[],[f401,f13296]) ).
fof(f13302,plain,
( index_120 = select(queue_115,tail)
| head = tail ),
inference(superposition,[],[f442,f13296]) ).
fof(f13304,plain,
index_120 = select(queue_115,tail),
inference(forward_subsumption_resolution,[],[f13302,f3]) ).
fof(f13305,plain,
earray_119 = select(queue_115,seq),
inference(forward_subsumption_resolution,[],[f13301,f4]) ).
fof(f13308,plain,
! [X0] :
( select(earray_140,X0) = select(earray_142,X0)
| index_141 = X0 ),
inference(superposition,[],[f2,f86]) ).
fof(f13310,plain,
! [X0] :
( select(earray_131,X0) = select(earray_133,X0)
| index_132 = X0 ),
inference(superposition,[],[f2,f83]) ).
fof(f13316,plain,
! [X0] :
( select(queue_113,X0) = select(queue_115,X0)
| tail = X0 ),
inference(superposition,[],[f2,f269]) ).
fof(f13317,plain,
index_114 = select(queue_115,tail),
inference(superposition,[],[f1,f269]) ).
fof(f13318,plain,
index_120 = index_114,
inference(backward_demodulation,[],[f13304,f13317]) ).
fof(f13320,plain,
index_123 = s(index_114),
inference(backward_demodulation,[],[f164,f13318]) ).
fof(f13351,plain,
! [X0] :
( select(earray_119,X0) = select(earray_121,X0)
| index_114 = X0 ),
inference(backward_demodulation,[],[f8731,f13318]) ).
fof(f13520,plain,
index_33 != s(s(s(s(index_123)))),
inference(backward_demodulation,[],[f11288,f13320]) ).
fof(f13521,plain,
index_123 != index_33,
inference(backward_demodulation,[],[f11290,f13320]) ).
fof(f13522,plain,
index_33 != s(index_123),
inference(backward_demodulation,[],[f11291,f13320]) ).
fof(f13523,plain,
index_33 != s(s(index_123)),
inference(backward_demodulation,[],[f11292,f13320]) ).
fof(f13524,plain,
index_33 != s(s(s(index_123))),
inference(backward_demodulation,[],[f11293,f13320]) ).
fof(f13529,plain,
index_33 != s(s(s(s(s(s(index_123)))))),
inference(backward_demodulation,[],[f11298,f13320]) ).
fof(f13536,plain,
index_33 != s(s(s(s(s(s(s(index_123))))))),
inference(backward_demodulation,[],[f11305,f13320]) ).
fof(f13548,plain,
index_33 != s(s(s(s(s(index_123))))),
inference(backward_demodulation,[],[f11318,f13320]) ).
fof(f13557,plain,
index_33 != s(s(s(s(s(s(s(s(index_123)))))))),
inference(backward_demodulation,[],[f11327,f13320]) ).
fof(f13566,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_123))))))))),
inference(backward_demodulation,[],[f11336,f13320]) ).
fof(f13581,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_123)))))))))),
inference(backward_demodulation,[],[f11352,f13320]) ).
fof(f13592,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_123))))))))))),
inference(backward_demodulation,[],[f11363,f13320]) ).
fof(f13610,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_123)))))))))))),
inference(backward_demodulation,[],[f11382,f13320]) ).
fof(f13623,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_123))))))))))))),
inference(backward_demodulation,[],[f11395,f13320]) ).
fof(f13644,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_123))))))))))))))),
inference(backward_demodulation,[],[f11417,f13320]) ).
fof(f13815,plain,
( index_116 = select(queue_113,head)
| head = tail ),
inference(superposition,[],[f160,f13316]) ).
fof(f13817,plain,
index_116 = select(queue_113,head),
inference(forward_subsumption_resolution,[],[f13815,f3]) ).
fof(f14150,plain,
! [X0] :
( select(queue_155,X0) = select(queue_157,X0)
| tail = X0 ),
inference(superposition,[],[f2,f284]) ).
fof(f14151,plain,
index_156 = select(queue_157,tail),
inference(superposition,[],[f1,f284]) ).
fof(f14152,plain,
index_234 = index_156,
inference(backward_demodulation,[],[f13270,f14151]) ).
fof(f14154,plain,
index_237 = s(index_156),
inference(backward_demodulation,[],[f211,f14152]) ).
fof(f15123,plain,
( index_158 = select(queue_155,head)
| head = tail ),
inference(superposition,[],[f178,f14150]) ).
fof(f15125,plain,
index_158 = select(queue_155,head),
inference(forward_subsumption_resolution,[],[f15123,f3]) ).
fof(f15127,plain,
! [X0] :
( select(queue_164,X0) = select(queue_166,X0)
| tail = X0 ),
inference(superposition,[],[f2,f287]) ).
fof(f15128,plain,
index_165 = select(queue_166,tail),
inference(superposition,[],[f1,f287]) ).
fof(f15129,plain,
index_171 = index_165,
inference(backward_demodulation,[],[f13288,f15128]) ).
fof(f15131,plain,
index_174 = s(index_165),
inference(backward_demodulation,[],[f185,f15129]) ).
fof(f15135,plain,
! [X0] :
( select(earray_170,X0) = select(earray_172,X0)
| index_165 = X0 ),
inference(backward_demodulation,[],[f7145,f15129]) ).
fof(f15716,plain,
( index_167 = select(queue_164,head)
| head = tail ),
inference(superposition,[],[f182,f15127]) ).
fof(f15718,plain,
index_167 = select(queue_164,head),
inference(forward_subsumption_resolution,[],[f15716,f3]) ).
fof(f17526,plain,
( index_48 = select(queue_53,head)
| head = seq ),
inference(superposition,[],[f544,f629]) ).
fof(f17527,plain,
index_48 = select(queue_53,head),
inference(forward_subsumption_resolution,[],[f17526,f4]) ).
fof(f17530,plain,
( index_69 = select(queue_74,head)
| head = seq ),
inference(superposition,[],[f736,f1810]) ).
fof(f17531,plain,
index_69 = select(queue_74,head),
inference(forward_subsumption_resolution,[],[f17530,f4]) ).
fof(f17534,plain,
( index_96 = select(queue_101,head)
| head = seq ),
inference(superposition,[],[f2730,f5541]) ).
fof(f17535,plain,
index_96 = select(queue_101,head),
inference(forward_subsumption_resolution,[],[f17534,f4]) ).
fof(f17537,plain,
! [X0] :
( select(queue_82,X0) = select(queue_80,X0)
| tail = X0 ),
inference(superposition,[],[f2,f350]) ).
fof(f17538,plain,
index_81 = select(queue_82,tail),
inference(superposition,[],[f1,f350]) ).
fof(f17539,plain,
index_153 = index_81,
inference(backward_demodulation,[],[f448,f17538]) ).
fof(f17541,plain,
index_156 = s(index_81),
inference(backward_demodulation,[],[f177,f17539]) ).
fof(f18760,plain,
! [X0] :
( select(queue_155,X0) = select(queue_80,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f8719,f17537]) ).
fof(f18773,plain,
( index_210 = select(queue_215,head)
| head = seq ),
inference(superposition,[],[f589,f1937]) ).
fof(f18774,plain,
index_210 = select(queue_215,head),
inference(forward_subsumption_resolution,[],[f18773,f4]) ).
fof(f18777,plain,
( index_258 = select(queue_263,head)
| head = seq ),
inference(superposition,[],[f1744,f5586]) ).
fof(f18778,plain,
index_258 = select(queue_263,head),
inference(forward_subsumption_resolution,[],[f18777,f4]) ).
fof(f18781,plain,
( index_159 = select(queue_236,head)
| head = seq ),
inference(superposition,[],[f5390,f13263]) ).
fof(f18782,plain,
index_159 = select(queue_236,head),
inference(forward_subsumption_resolution,[],[f18781,f4]) ).
fof(f18785,plain,
( index_27 = select(queue_32,head)
| head = seq ),
inference(superposition,[],[f527,f631]) ).
fof(f18786,plain,
index_27 = select(queue_32,head),
inference(forward_subsumption_resolution,[],[f18785,f4]) ).
fof(f18788,plain,
! [X0] :
( select(queue_122,X0) = select(queue_124,X0)
| tail = X0 ),
inference(superposition,[],[f2,f272]) ).
fof(f18789,plain,
index_123 = select(queue_124,tail),
inference(superposition,[],[f1,f272]) ).
fof(f18790,plain,
index_126 = index_123,
inference(backward_demodulation,[],[f443,f18789]) ).
fof(f18792,plain,
index_129 = s(index_123),
inference(backward_demodulation,[],[f166,f18790]) ).
fof(f18824,plain,
! [X0] :
( select(earray_125,X0) = select(earray_127,X0)
| index_123 = X0 ),
inference(backward_demodulation,[],[f11086,f18790]) ).
fof(f19015,plain,
index_33 != s(s(s(index_129))),
inference(backward_demodulation,[],[f13520,f18792]) ).
fof(f19016,plain,
index_129 != index_33,
inference(backward_demodulation,[],[f13522,f18792]) ).
fof(f19017,plain,
index_33 != s(index_129),
inference(backward_demodulation,[],[f13523,f18792]) ).
fof(f19018,plain,
index_33 != s(s(index_129)),
inference(backward_demodulation,[],[f13524,f18792]) ).
fof(f19023,plain,
index_33 != s(s(s(s(s(index_129))))),
inference(backward_demodulation,[],[f13529,f18792]) ).
fof(f19030,plain,
index_33 != s(s(s(s(s(s(index_129)))))),
inference(backward_demodulation,[],[f13536,f18792]) ).
fof(f19041,plain,
index_33 != s(s(s(s(index_129)))),
inference(backward_demodulation,[],[f13548,f18792]) ).
fof(f19050,plain,
index_33 != s(s(s(s(s(s(s(index_129))))))),
inference(backward_demodulation,[],[f13557,f18792]) ).
fof(f19059,plain,
index_33 != s(s(s(s(s(s(s(s(index_129)))))))),
inference(backward_demodulation,[],[f13566,f18792]) ).
fof(f19073,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_129))))))))),
inference(backward_demodulation,[],[f13581,f18792]) ).
fof(f19084,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_129)))))))))),
inference(backward_demodulation,[],[f13592,f18792]) ).
fof(f19101,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_129))))))))))),
inference(backward_demodulation,[],[f13610,f18792]) ).
fof(f19114,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(s(index_129)))))))))))),
inference(backward_demodulation,[],[f13623,f18792]) ).
fof(f19134,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_129)))))))))))))),
inference(backward_demodulation,[],[f13644,f18792]) ).
fof(f19462,plain,
( earray_125 = select(queue_122,seq)
| tail = seq ),
inference(superposition,[],[f402,f18788]) ).
fof(f19463,plain,
! [X0] :
( select(queue_122,X0) = select(queue_128,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f8721,f18788]) ).
fof(f19464,plain,
earray_125 = select(queue_122,seq),
inference(forward_subsumption_resolution,[],[f19462,f5]) ).
fof(f19466,plain,
earray_121 = earray_125,
inference(forward_demodulation,[],[f19464,f7136]) ).
fof(f19469,plain,
! [X0] :
( select(earray_121,X0) = select(earray_127,X0)
| index_123 = X0 ),
inference(backward_demodulation,[],[f18824,f19466]) ).
fof(f19476,plain,
( index_189 = select(queue_194,head)
| head = seq ),
inference(superposition,[],[f1693,f6890]) ).
fof(f19477,plain,
index_189 = select(queue_194,head),
inference(forward_subsumption_resolution,[],[f19476,f4]) ).
fof(f19480,plain,
( index_279 = select(queue_11,head)
| head = seq ),
inference(superposition,[],[f603,f1800]) ).
fof(f19481,plain,
index_279 = select(queue_11,head),
inference(forward_subsumption_resolution,[],[f19480,f4]) ).
fof(f19484,plain,
( index_168 = select(queue_173,head)
| head = seq ),
inference(superposition,[],[f5396,f13281]) ).
fof(f19485,plain,
index_168 = select(queue_173,head),
inference(forward_subsumption_resolution,[],[f19484,f4]) ).
fof(f19488,plain,
( index_231 = select(queue_242,head)
| head = seq ),
inference(superposition,[],[f529,f633]) ).
fof(f19489,plain,
index_231 = select(queue_242,head),
inference(forward_subsumption_resolution,[],[f19488,f4]) ).
fof(f19491,plain,
index_282 = index_231,
inference(forward_demodulation,[],[f19489,f3044]) ).
fof(f19493,plain,
index_282 = s(index_230),
inference(backward_demodulation,[],[f209,f19491]) ).
fof(f19570,plain,
! [X0] :
( select(queue_151,X0) = select(queue_149,X0)
| tail = X0 ),
inference(superposition,[],[f2,f282]) ).
fof(f19571,plain,
index_150 = select(queue_151,tail),
inference(superposition,[],[f1,f282]) ).
fof(f19572,plain,
index_162 = index_150,
inference(backward_demodulation,[],[f449,f19571]) ).
fof(f19574,plain,
index_165 = s(index_150),
inference(backward_demodulation,[],[f181,f19572]) ).
fof(f19577,plain,
! [X0] :
( select(earray_161,X0) = select(earray_163,X0)
| index_150 = X0 ),
inference(backward_demodulation,[],[f8789,f19572]) ).
fof(f20312,plain,
( earray_161 = select(queue_149,seq)
| tail = seq ),
inference(superposition,[],[f408,f19570]) ).
fof(f20313,plain,
! [X0] :
( select(queue_164,X0) = select(queue_149,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f8039,f19570]) ).
fof(f20314,plain,
earray_161 = select(queue_149,seq),
inference(forward_subsumption_resolution,[],[f20312,f5]) ).
fof(f20316,plain,
earray_148 = earray_161,
inference(forward_demodulation,[],[f20314,f8794]) ).
fof(f20319,plain,
! [X0] :
( select(earray_163,X0) = select(earray_148,X0)
| index_150 = X0 ),
inference(backward_demodulation,[],[f19577,f20316]) ).
fof(f20326,plain,
( index_117 = select(queue_122,head)
| head = seq ),
inference(superposition,[],[f7135,f13297]) ).
fof(f20327,plain,
index_117 = select(queue_122,head),
inference(forward_subsumption_resolution,[],[f20326,f4]) ).
fof(f20393,plain,
! [X0] :
( select(queue_128,X0) = select(queue_130,X0)
| tail = X0 ),
inference(superposition,[],[f2,f275]) ).
fof(f20394,plain,
index_129 = select(queue_130,tail),
inference(superposition,[],[f1,f275]) ).
fof(f20395,plain,
index_132 = index_129,
inference(backward_demodulation,[],[f444,f20394]) ).
fof(f20397,plain,
index_135 = s(index_129),
inference(backward_demodulation,[],[f168,f20395]) ).
fof(f20430,plain,
! [X0] :
( select(earray_131,X0) = select(earray_133,X0)
| index_129 = X0 ),
inference(backward_demodulation,[],[f13310,f20395]) ).
fof(f20643,plain,
index_33 != s(s(index_135)),
inference(backward_demodulation,[],[f19015,f20397]) ).
fof(f20644,plain,
index_135 != index_33,
inference(backward_demodulation,[],[f19017,f20397]) ).
fof(f20645,plain,
index_33 != s(index_135),
inference(backward_demodulation,[],[f19018,f20397]) ).
fof(f20650,plain,
index_33 != s(s(s(s(index_135)))),
inference(backward_demodulation,[],[f19023,f20397]) ).
fof(f20657,plain,
index_33 != s(s(s(s(s(index_135))))),
inference(backward_demodulation,[],[f19030,f20397]) ).
fof(f20667,plain,
index_33 != s(s(s(index_135))),
inference(backward_demodulation,[],[f19041,f20397]) ).
fof(f20676,plain,
index_33 != s(s(s(s(s(s(index_135)))))),
inference(backward_demodulation,[],[f19050,f20397]) ).
fof(f20685,plain,
index_33 != s(s(s(s(s(s(s(index_135))))))),
inference(backward_demodulation,[],[f19059,f20397]) ).
fof(f20698,plain,
index_33 != s(s(s(s(s(s(s(s(index_135)))))))),
inference(backward_demodulation,[],[f19073,f20397]) ).
fof(f20709,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_135))))))))),
inference(backward_demodulation,[],[f19084,f20397]) ).
fof(f20725,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_135)))))))))),
inference(backward_demodulation,[],[f19101,f20397]) ).
fof(f20738,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(s(index_135))))))))))),
inference(backward_demodulation,[],[f19114,f20397]) ).
fof(f20757,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_135))))))))))))),
inference(backward_demodulation,[],[f19134,f20397]) ).
fof(f21079,plain,
( earray_131 = select(queue_128,seq)
| tail = seq ),
inference(superposition,[],[f403,f20393]) ).
fof(f21080,plain,
! [X0] :
( select(queue_128,X0) = select(queue_134,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f10747,f20393]) ).
fof(f21081,plain,
earray_131 = select(queue_128,seq),
inference(forward_subsumption_resolution,[],[f21079,f5]) ).
fof(f21083,plain,
earray_127 = earray_131,
inference(forward_demodulation,[],[f21081,f8722]) ).
fof(f21086,plain,
! [X0] :
( select(earray_127,X0) = select(earray_133,X0)
| index_129 = X0 ),
inference(backward_demodulation,[],[f20430,f21083]) ).
fof(f21092,plain,
! [X0] :
( select(queue_7,X0) = select(queue_5,X0)
| tail = X0 ),
inference(superposition,[],[f2,f345]) ).
fof(f21093,plain,
index_6 = select(queue_7,tail),
inference(superposition,[],[f1,f345]) ).
fof(f21094,plain,
index_78 = index_6,
inference(backward_demodulation,[],[f476,f21093]) ).
fof(f21095,plain,
index_81 = s(index_6),
inference(backward_demodulation,[],[f253,f21094]) ).
fof(f22388,plain,
! [X0] :
( select(queue_80,X0) = select(queue_5,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f10739,f21092]) ).
fof(f22403,plain,
! [X0] :
( select(queue_155,X0) = select(queue_5,X0)
| seq = X0
| tail = X0
| seq = X0
| tail = X0 ),
inference(superposition,[],[f18760,f22388]) ).
fof(f22404,plain,
! [X0] :
( select(queue_155,X0) = select(queue_5,X0)
| seq = X0
| tail = X0 ),
inference(duplicate_literal_removal,[],[f22403]) ).
fof(f22410,plain,
! [X0] :
( select(queue_145,X0) = select(queue_143,X0)
| tail = X0 ),
inference(superposition,[],[f2,f280]) ).
fof(f22411,plain,
index_144 = select(queue_145,tail),
inference(superposition,[],[f1,f280]) ).
fof(f22412,plain,
index_147 = index_144,
inference(backward_demodulation,[],[f446,f22411]) ).
fof(f22414,plain,
index_150 = s(index_144),
inference(backward_demodulation,[],[f175,f22412]) ).
fof(f22417,plain,
! [X0] :
( select(earray_146,X0) = select(earray_148,X0)
| index_144 = X0 ),
inference(backward_demodulation,[],[f11096,f22412]) ).
fof(f23203,plain,
( earray_146 = select(queue_143,seq)
| tail = seq ),
inference(superposition,[],[f406,f22410]) ).
fof(f23204,plain,
! [X0] :
( select(queue_149,X0) = select(queue_143,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f8793,f22410]) ).
fof(f23205,plain,
earray_146 = select(queue_143,seq),
inference(forward_subsumption_resolution,[],[f23203,f5]) ).
fof(f23207,plain,
earray_142 = earray_146,
inference(forward_demodulation,[],[f23205,f11099]) ).
fof(f23210,plain,
! [X0] :
( select(earray_148,X0) = select(earray_142,X0)
| index_144 = X0 ),
inference(backward_demodulation,[],[f22417,f23207]) ).
fof(f23218,plain,
! [X0] :
( select(queue_139,X0) = select(queue_136,X0)
| head = X0 ),
inference(superposition,[],[f2,f278]) ).
fof(f23219,plain,
index_138 = select(queue_139,head),
inference(superposition,[],[f1,f278]) ).
fof(f23223,plain,
( earray_140 = select(queue_136,seq)
| head = seq ),
inference(superposition,[],[f405,f23218]) ).
fof(f23224,plain,
( index_141 = select(queue_136,tail)
| head = tail ),
inference(superposition,[],[f445,f23218]) ).
fof(f23226,plain,
index_141 = select(queue_136,tail),
inference(forward_subsumption_resolution,[],[f23224,f3]) ).
fof(f23227,plain,
earray_140 = select(queue_136,seq),
inference(forward_subsumption_resolution,[],[f23223,f4]) ).
fof(f23231,plain,
( index_138 = select(queue_143,head)
| head = seq ),
inference(superposition,[],[f11098,f23219]) ).
fof(f23232,plain,
index_138 = select(queue_143,head),
inference(forward_subsumption_resolution,[],[f23231,f4]) ).
fof(f23234,plain,
! [X0] :
( select(queue_134,X0) = select(queue_136,X0)
| tail = X0 ),
inference(superposition,[],[f2,f277]) ).
fof(f23235,plain,
index_135 = select(queue_136,tail),
inference(superposition,[],[f1,f277]) ).
fof(f23236,plain,
index_141 = index_135,
inference(backward_demodulation,[],[f23226,f23235]) ).
fof(f23238,plain,
index_144 = s(index_135),
inference(backward_demodulation,[],[f172,f23236]) ).
fof(f23242,plain,
! [X0] :
( select(earray_140,X0) = select(earray_142,X0)
| index_135 = X0 ),
inference(backward_demodulation,[],[f13308,f23236]) ).
fof(f23507,plain,
index_33 != s(index_144),
inference(backward_demodulation,[],[f20643,f23238]) ).
fof(f23508,plain,
index_144 != index_33,
inference(backward_demodulation,[],[f20645,f23238]) ).
fof(f23513,plain,
index_33 != s(s(s(index_144))),
inference(backward_demodulation,[],[f20650,f23238]) ).
fof(f23520,plain,
index_33 != s(s(s(s(index_144)))),
inference(backward_demodulation,[],[f20657,f23238]) ).
fof(f23530,plain,
index_33 != s(s(index_144)),
inference(backward_demodulation,[],[f20667,f23238]) ).
fof(f23538,plain,
index_33 != s(s(s(s(s(index_144))))),
inference(backward_demodulation,[],[f20676,f23238]) ).
fof(f23547,plain,
index_33 != s(s(s(s(s(s(index_144)))))),
inference(backward_demodulation,[],[f20685,f23238]) ).
fof(f23559,plain,
index_33 != s(s(s(s(s(s(s(index_144))))))),
inference(backward_demodulation,[],[f20698,f23238]) ).
fof(f23570,plain,
index_33 != s(s(s(s(s(s(s(s(index_144)))))))),
inference(backward_demodulation,[],[f20709,f23238]) ).
fof(f23585,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_144))))))))),
inference(backward_demodulation,[],[f20725,f23238]) ).
fof(f23598,plain,
index_33 != s(s(s(s(s(s(s(s(s(s(index_144)))))))))),
inference(backward_demodulation,[],[f20738,f23238]) ).
fof(f23616,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(s(index_144)))))))))))),
inference(backward_demodulation,[],[f20757,f23238]) ).
fof(f24178,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(s(index_150))))))))))),
inference(forward_demodulation,[],[f23616,f22414]) ).
fof(f24195,plain,
index_33 != s(s(s(s(s(s(s(s(s(index_150))))))))),
inference(forward_demodulation,[],[f23598,f22414]) ).
fof(f24208,plain,
index_33 != s(s(s(s(s(s(s(s(index_150)))))))),
inference(forward_demodulation,[],[f23585,f22414]) ).
fof(f24222,plain,
index_33 != s(s(s(s(s(s(s(index_150))))))),
inference(forward_demodulation,[],[f23570,f22414]) ).
fof(f24233,plain,
index_33 != s(s(s(s(s(s(index_150)))))),
inference(forward_demodulation,[],[f23559,f22414]) ).
fof(f24244,plain,
index_33 != s(s(s(s(s(index_150))))),
inference(forward_demodulation,[],[f23547,f22414]) ).
fof(f24253,plain,
index_33 != s(s(s(s(index_150)))),
inference(forward_demodulation,[],[f23538,f22414]) ).
fof(f24260,plain,
index_33 != s(index_150),
inference(forward_demodulation,[],[f23530,f22414]) ).
fof(f24269,plain,
index_33 != s(s(s(index_150))),
inference(forward_demodulation,[],[f23520,f22414]) ).
fof(f24276,plain,
index_33 != s(s(index_150)),
inference(forward_demodulation,[],[f23513,f22414]) ).
fof(f24281,plain,
index_150 != index_33,
inference(forward_demodulation,[],[f23507,f22414]) ).
fof(f24765,plain,
index_39 != s(s(s(s(s(s(s(s(s(s(index_165)))))))))),
inference(forward_demodulation,[],[f24178,f19574]) ).
fof(f24781,plain,
index_33 != s(s(s(s(s(s(s(s(index_165)))))))),
inference(forward_demodulation,[],[f24195,f19574]) ).
fof(f24794,plain,
index_33 != s(s(s(s(s(s(s(index_165))))))),
inference(forward_demodulation,[],[f24208,f19574]) ).
fof(f24807,plain,
index_33 != s(s(s(s(s(s(index_165)))))),
inference(forward_demodulation,[],[f24222,f19574]) ).
fof(f24818,plain,
index_33 != s(s(s(s(s(index_165))))),
inference(forward_demodulation,[],[f24233,f19574]) ).
fof(f24828,plain,
index_33 != s(s(s(s(index_165)))),
inference(forward_demodulation,[],[f24244,f19574]) ).
fof(f24837,plain,
index_33 != s(s(s(index_165))),
inference(forward_demodulation,[],[f24253,f19574]) ).
fof(f24843,plain,
index_165 != index_33,
inference(forward_demodulation,[],[f24260,f19574]) ).
fof(f24851,plain,
index_33 != s(s(index_165)),
inference(forward_demodulation,[],[f24269,f19574]) ).
fof(f24857,plain,
index_33 != s(index_165),
inference(forward_demodulation,[],[f24276,f19574]) ).
fof(f25325,plain,
index_39 != s(s(s(s(s(s(s(s(s(index_174))))))))),
inference(forward_demodulation,[],[f24765,f15131]) ).
fof(f25340,plain,
index_33 != s(s(s(s(s(s(s(index_174))))))),
inference(forward_demodulation,[],[f24781,f15131]) ).
fof(f25353,plain,
index_33 != s(s(s(s(s(s(index_174)))))),
inference(forward_demodulation,[],[f24794,f15131]) ).
fof(f25365,plain,
index_33 != s(s(s(s(s(index_174))))),
inference(forward_demodulation,[],[f24807,f15131]) ).
fof(f25376,plain,
index_33 != s(s(s(s(index_174)))),
inference(forward_demodulation,[],[f24818,f15131]) ).
fof(f25385,plain,
index_33 != s(s(s(index_174))),
inference(forward_demodulation,[],[f24828,f15131]) ).
fof(f25393,plain,
index_33 != s(s(index_174)),
inference(forward_demodulation,[],[f24837,f15131]) ).
fof(f25405,plain,
index_33 != s(index_174),
inference(forward_demodulation,[],[f24851,f15131]) ).
fof(f25410,plain,
index_174 != index_33,
inference(forward_demodulation,[],[f24857,f15131]) ).
fof(f25858,plain,
index_39 != s(s(s(s(s(s(s(s(index_180)))))))),
inference(forward_demodulation,[],[f25325,f12727]) ).
fof(f25872,plain,
index_33 != s(s(s(s(s(s(index_180)))))),
inference(forward_demodulation,[],[f25340,f12727]) ).
fof(f25885,plain,
index_33 != s(s(s(s(s(index_180))))),
inference(forward_demodulation,[],[f25353,f12727]) ).
fof(f25896,plain,
index_33 != s(s(s(s(index_180)))),
inference(forward_demodulation,[],[f25365,f12727]) ).
fof(f25906,plain,
index_33 != s(s(s(index_180))),
inference(forward_demodulation,[],[f25376,f12727]) ).
fof(f25914,plain,
index_33 != s(s(index_180)),
inference(forward_demodulation,[],[f25385,f12727]) ).
fof(f25921,plain,
index_33 != s(index_180),
inference(forward_demodulation,[],[f25393,f12727]) ).
fof(f25931,plain,
index_180 != index_33,
inference(forward_demodulation,[],[f25405,f12727]) ).
fof(f26364,plain,
index_39 != s(s(s(s(s(s(s(index_186))))))),
inference(forward_demodulation,[],[f25858,f10260]) ).
fof(f26377,plain,
index_33 != s(s(s(s(s(index_186))))),
inference(forward_demodulation,[],[f25872,f10260]) ).
fof(f26389,plain,
index_33 != s(s(s(s(index_186)))),
inference(forward_demodulation,[],[f25885,f10260]) ).
fof(f26399,plain,
index_33 != s(s(s(index_186))),
inference(forward_demodulation,[],[f25896,f10260]) ).
fof(f26408,plain,
index_33 != s(s(index_186)),
inference(forward_demodulation,[],[f25906,f10260]) ).
fof(f26415,plain,
index_33 != s(index_186),
inference(forward_demodulation,[],[f25914,f10260]) ).
fof(f26421,plain,
index_186 != index_33,
inference(forward_demodulation,[],[f25921,f10260]) ).
fof(f26842,plain,
index_39 != s(s(s(s(s(s(index_195)))))),
inference(forward_demodulation,[],[f26364,f8076]) ).
fof(f26854,plain,
index_33 != s(s(s(s(index_195)))),
inference(forward_demodulation,[],[f26377,f8076]) ).
fof(f26865,plain,
index_33 != s(s(s(index_195))),
inference(forward_demodulation,[],[f26389,f8076]) ).
fof(f26874,plain,
index_33 != s(s(index_195)),
inference(forward_demodulation,[],[f26399,f8076]) ).
fof(f26882,plain,
index_33 != s(index_195),
inference(forward_demodulation,[],[f26408,f8076]) ).
fof(f26888,plain,
index_195 != index_33,
inference(forward_demodulation,[],[f26415,f8076]) ).
fof(f27292,plain,
index_39 != s(s(s(s(s(index_201))))),
inference(forward_demodulation,[],[f26842,f6255]) ).
fof(f27303,plain,
index_33 != s(s(s(index_201))),
inference(forward_demodulation,[],[f26854,f6255]) ).
fof(f27313,plain,
index_33 != s(s(index_201)),
inference(forward_demodulation,[],[f26865,f6255]) ).
fof(f27321,plain,
index_33 != s(index_201),
inference(forward_demodulation,[],[f26874,f6255]) ).
fof(f27328,plain,
index_201 != index_33,
inference(forward_demodulation,[],[f26882,f6255]) ).
fof(f27714,plain,
index_39 != s(s(s(s(index_207)))),
inference(forward_demodulation,[],[f27292,f4658]) ).
fof(f27724,plain,
index_33 != s(s(index_207)),
inference(forward_demodulation,[],[f27303,f4658]) ).
fof(f27733,plain,
index_33 != s(index_207),
inference(forward_demodulation,[],[f27313,f4658]) ).
fof(f27740,plain,
index_207 != index_33,
inference(forward_demodulation,[],[f27321,f4658]) ).
fof(f28109,plain,
index_39 != s(s(s(index_216))),
inference(forward_demodulation,[],[f27714,f2860]) ).
fof(f28118,plain,
index_33 != s(index_216),
inference(forward_demodulation,[],[f27724,f2860]) ).
fof(f28126,plain,
index_216 != index_33,
inference(forward_demodulation,[],[f27733,f2860]) ).
fof(f28478,plain,
index_39 != s(s(index_222)),
inference(forward_demodulation,[],[f28109,f1823]) ).
fof(f28486,plain,
index_222 != index_33,
inference(forward_demodulation,[],[f28118,f1823]) ).
fof(f28822,plain,
index_39 != s(index_228),
inference(forward_demodulation,[],[f28478,f1016]) ).
fof(f29142,plain,
index_243 != index_39,
inference(forward_demodulation,[],[f28822,f1505]) ).
fof(f29678,plain,
( index_137 = select(queue_134,head)
| head = tail ),
inference(superposition,[],[f169,f23234]) ).
fof(f29680,plain,
index_137 = select(queue_134,head),
inference(forward_subsumption_resolution,[],[f29678,f3]) ).
fof(f40604,plain,
( earray_71 = select(queue_65,seq)
| tail = seq ),
inference(superposition,[],[f2002,f1816]) ).
fof(f40605,plain,
earray_71 = select(queue_65,seq),
inference(forward_subsumption_resolution,[],[f40604,f5]) ).
fof(f40607,plain,
earray_64 = earray_71,
inference(forward_demodulation,[],[f40605,f588]) ).
fof(f40610,plain,
! [X0] :
( select(earray_64,X0) = select(earray_73,X0)
| index_66 = X0 ),
inference(backward_demodulation,[],[f2008,f40607]) ).
fof(f40636,plain,
( earray_239 = select(queue_227,seq)
| tail = seq ),
inference(superposition,[],[f754,f1499]) ).
fof(f40637,plain,
earray_239 = select(queue_227,seq),
inference(forward_subsumption_resolution,[],[f40636,f5]) ).
fof(f40639,plain,
earray_226 = earray_239,
inference(forward_demodulation,[],[f40637,f554]) ).
fof(f40641,plain,
( elem_283 = select(earray_226,index_282)
| ~ spl0_2 ),
inference(backward_demodulation,[],[f3061,f40639]) ).
fof(f40652,plain,
( elem_283 = select(earray_220,index_282)
| index_282 = index_222
| ~ spl0_2 ),
inference(superposition,[],[f40641,f4120]) ).
fof(f40655,definition,
( spl0_3
<=> index_282 = index_222 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f40657,plain,
( index_282 = index_222
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f40655]) ).
fof(f40659,definition,
( spl0_4
<=> elem_283 = select(earray_220,index_282) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f40661,plain,
( elem_283 = select(earray_220,index_282)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f40659]) ).
fof(f40663,plain,
( spl0_3
| spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f40652,f3059,f40659,f40655]) ).
fof(f40730,plain,
( index_282 != index_33
| ~ spl0_3 ),
inference(backward_demodulation,[],[f28486,f40657]) ).
fof(f41984,plain,
( earray_50 = select(queue_44,seq)
| tail = seq ),
inference(superposition,[],[f634,f1310]) ).
fof(f41985,plain,
earray_50 = select(queue_44,seq),
inference(forward_subsumption_resolution,[],[f41984,f5]) ).
fof(f41987,plain,
earray_43 = earray_50,
inference(forward_demodulation,[],[f41985,f526]) ).
fof(f41990,plain,
! [X0] :
( select(earray_43,X0) = select(earray_52,X0)
| index_45 = X0 ),
inference(backward_demodulation,[],[f1318,f41987]) ).
fof(f42000,plain,
( earray_212 = select(queue_206,seq)
| tail = seq ),
inference(superposition,[],[f2856,f1943]) ).
fof(f42001,plain,
earray_212 = select(queue_206,seq),
inference(forward_subsumption_resolution,[],[f42000,f5]) ).
fof(f42003,plain,
earray_205 = earray_212,
inference(forward_demodulation,[],[f42001,f753]) ).
fof(f42006,plain,
! [X0] :
( select(earray_214,X0) = select(earray_205,X0)
| index_207 = X0 ),
inference(backward_demodulation,[],[f2862,f42003]) ).
fof(f42016,plain,
( index_0 = select(queue_155,head)
| head = seq
| head = tail ),
inference(superposition,[],[f22404,f13258]) ).
fof(f42017,plain,
( index_0 = select(queue_155,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f42016,f4]) ).
fof(f42019,plain,
index_0 = select(queue_155,head),
inference(forward_subsumption_resolution,[],[f42017,f3]) ).
fof(f42021,plain,
index_0 = index_158,
inference(backward_demodulation,[],[f15125,f42019]) ).
fof(f42023,plain,
index_159 = s(index_0),
inference(backward_demodulation,[],[f179,f42021]) ).
fof(f42075,plain,
index_159 = index_6,
inference(backward_demodulation,[],[f11020,f42023]) ).
fof(f42080,plain,
index_81 = s(index_159),
inference(backward_demodulation,[],[f21095,f42075]) ).
fof(f45865,plain,
( earray_191 = select(queue_185,seq)
| tail = seq ),
inference(superposition,[],[f8072,f6898]) ).
fof(f45866,plain,
earray_191 = select(queue_185,seq),
inference(forward_subsumption_resolution,[],[f45865,f5]) ).
fof(f45868,plain,
earray_184 = earray_191,
inference(forward_demodulation,[],[f45866,f3419]) ).
fof(f45871,plain,
! [X0] :
( select(earray_193,X0) = select(earray_184,X0)
| index_186 = X0 ),
inference(backward_demodulation,[],[f8078,f45868]) ).
fof(f45881,plain,
( earray_170 = select(queue_164,seq)
| tail = seq ),
inference(superposition,[],[f15127,f13289]) ).
fof(f45882,plain,
earray_170 = select(queue_164,seq),
inference(forward_subsumption_resolution,[],[f45881,f5]) ).
fof(f45884,plain,
earray_163 = earray_170,
inference(forward_demodulation,[],[f45882,f8040]) ).
fof(f45887,plain,
! [X0] :
( select(earray_172,X0) = select(earray_163,X0)
| index_165 = X0 ),
inference(backward_demodulation,[],[f15135,f45884]) ).
fof(f45897,plain,
( earray_140 = select(queue_134,seq)
| tail = seq ),
inference(superposition,[],[f23234,f23227]) ).
fof(f45898,plain,
earray_140 = select(queue_134,seq),
inference(forward_subsumption_resolution,[],[f45897,f5]) ).
fof(f45900,plain,
earray_133 = earray_140,
inference(forward_demodulation,[],[f45898,f10748]) ).
fof(f45903,plain,
! [X0] :
( select(earray_142,X0) = select(earray_133,X0)
| index_135 = X0 ),
inference(backward_demodulation,[],[f23242,f45900]) ).
fof(f45913,plain,
( earray_119 = select(queue_113,seq)
| tail = seq ),
inference(superposition,[],[f13316,f13305]) ).
fof(f45914,plain,
earray_119 = select(queue_113,seq),
inference(forward_subsumption_resolution,[],[f45913,f5]) ).
fof(f45916,plain,
earray_112 = earray_119,
inference(forward_demodulation,[],[f45914,f5035]) ).
fof(f45919,plain,
! [X0] :
( select(earray_112,X0) = select(earray_121,X0)
| index_114 = X0 ),
inference(backward_demodulation,[],[f13351,f45916]) ).
fof(f46906,plain,
( earray_98 = select(queue_92,seq)
| tail = seq ),
inference(superposition,[],[f6565,f5549]) ).
fof(f46907,plain,
earray_98 = select(queue_92,seq),
inference(forward_subsumption_resolution,[],[f46906,f5]) ).
fof(f46909,plain,
earray_98 = earray_91,
inference(backward_demodulation,[],[f1935,f46907]) ).
fof(f46911,plain,
! [X0] :
( select(earray_85,X0) = select(earray_98,X0)
| index_87 = X0 ),
inference(backward_demodulation,[],[f5382,f46909]) ).
fof(f46916,plain,
! [X0] :
( select(earray_73,X0) = select(earray_98,X0)
| index_75 = X0
| index_87 = X0 ),
inference(superposition,[],[f3951,f46911]) ).
fof(f46925,plain,
! [X0] :
( select(earray_64,X0) = select(earray_98,X0)
| index_66 = X0
| index_75 = X0
| index_87 = X0 ),
inference(superposition,[],[f40610,f46916]) ).
fof(f46932,plain,
! [X0] :
( select(earray_58,X0) = select(earray_98,X0)
| index_60 = X0
| index_66 = X0
| index_75 = X0
| index_87 = X0 ),
inference(superposition,[],[f3506,f46925]) ).
fof(f46942,plain,
! [X0] :
( select(earray_52,X0) = select(earray_98,X0)
| index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| index_87 = X0 ),
inference(superposition,[],[f3476,f46932]) ).
fof(f46955,plain,
! [X0] :
( select(earray_43,X0) = select(earray_98,X0)
| index_45 = X0
| index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| index_87 = X0 ),
inference(superposition,[],[f41990,f46942]) ).
fof(f46970,plain,
! [X0] :
( select(earray_37,X0) = select(earray_98,X0)
| index_39 = X0
| index_45 = X0
| index_54 = X0
| index_60 = X0
| index_66 = X0
| index_75 = X0
| index_87 = X0 ),
inference(superposition,[],[f3490,f46955]) ).
fof(f46986,plain,
( e13 = select(earray_98,index_33)
| index_33 = index_39
| index_33 = index_45
| index_33 = index_54
| index_33 = index_60
| index_33 = index_66
| index_33 = index_75
| index_33 = index_87 ),
inference(superposition,[],[f610,f46970]) ).
fof(f46988,plain,
( e13 = select(earray_98,index_33)
| index_33 = index_45
| index_33 = index_54
| index_33 = index_60
| index_33 = index_66
| index_33 = index_75
| index_33 = index_87 ),
inference(forward_subsumption_resolution,[],[f46986,f612]) ).
fof(f46990,plain,
( e13 = select(earray_98,index_33)
| index_33 = index_54
| index_33 = index_60
| index_33 = index_66
| index_33 = index_75
| index_33 = index_87 ),
inference(forward_subsumption_resolution,[],[f46988,f3457]) ).
fof(f46992,plain,
( e13 = select(earray_98,index_33)
| index_33 = index_60
| index_33 = index_66
| index_33 = index_75
| index_33 = index_87 ),
inference(forward_subsumption_resolution,[],[f46990,f1362]) ).
fof(f46994,plain,
( e13 = select(earray_98,index_33)
| index_33 = index_66
| index_33 = index_75
| index_33 = index_87 ),
inference(forward_subsumption_resolution,[],[f46992,f1447]) ).
fof(f46996,plain,
( e13 = select(earray_98,index_33)
| index_33 = index_75
| index_33 = index_87 ),
inference(forward_subsumption_resolution,[],[f46994,f1666]) ).
fof(f46998,plain,
( e13 = select(earray_98,index_33)
| index_33 = index_87 ),
inference(forward_subsumption_resolution,[],[f46996,f2108]) ).
fof(f47000,plain,
e13 = select(earray_98,index_33),
inference(forward_subsumption_resolution,[],[f46998,f3826]) ).
fof(f47075,plain,
( e13 = select(earray_100,index_33)
| index_33 = index_93 ),
inference(superposition,[],[f6572,f47000]) ).
fof(f47076,plain,
e13 = select(earray_100,index_33),
inference(forward_subsumption_resolution,[],[f47075,f5225]) ).
fof(f50441,plain,
( index_257 = select(queue_248,head)
| head = seq
| head = tail ),
inference(superposition,[],[f9781,f8037]) ).
fof(f50442,plain,
( index_257 = select(queue_248,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f50441,f4]) ).
fof(f50444,plain,
index_257 = select(queue_248,head),
inference(forward_subsumption_resolution,[],[f50442,f3]) ).
fof(f50447,plain,
( index_257 = select(queue_236,head)
| head = seq
| head = tail ),
inference(superposition,[],[f12412,f50444]) ).
fof(f50448,plain,
( index_257 = select(queue_236,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f50447,f4]) ).
fof(f50450,plain,
index_257 = select(queue_236,head),
inference(forward_subsumption_resolution,[],[f50448,f3]) ).
fof(f50452,plain,
index_159 = index_257,
inference(forward_demodulation,[],[f50450,f18782]) ).
fof(f50455,plain,
index_258 = s(index_159),
inference(backward_demodulation,[],[f220,f50452]) ).
fof(f50514,plain,
index_258 = index_81,
inference(backward_demodulation,[],[f42080,f50455]) ).
fof(f50519,plain,
index_156 = s(index_258),
inference(backward_demodulation,[],[f17541,f50514]) ).
fof(f54860,plain,
( index_68 = select(queue_59,head)
| head = seq
| head = tail ),
inference(superposition,[],[f3500,f3570]) ).
fof(f54861,plain,
( index_68 = select(queue_59,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f54860,f4]) ).
fof(f54863,plain,
index_68 = select(queue_59,head),
inference(forward_subsumption_resolution,[],[f54861,f3]) ).
fof(f54866,plain,
( index_68 = select(queue_53,head)
| head = seq
| head = tail ),
inference(superposition,[],[f3470,f54863]) ).
fof(f54867,plain,
( index_68 = select(queue_53,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f54866,f4]) ).
fof(f54869,plain,
index_68 = select(queue_53,head),
inference(forward_subsumption_resolution,[],[f54867,f3]) ).
fof(f54871,plain,
index_48 = index_68,
inference(forward_demodulation,[],[f54869,f17527]) ).
fof(f54874,plain,
index_69 = s(index_48),
inference(backward_demodulation,[],[f249,f54871]) ).
fof(f55051,plain,
( index_95 = select(queue_86,head)
| head = seq
| head = tail ),
inference(superposition,[],[f5376,f6887]) ).
fof(f55052,plain,
( index_95 = select(queue_86,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f55051,f4]) ).
fof(f55054,plain,
index_95 = select(queue_86,head),
inference(forward_subsumption_resolution,[],[f55052,f3]) ).
fof(f55057,plain,
( index_95 = select(queue_74,head)
| head = seq
| head = tail ),
inference(superposition,[],[f3945,f55054]) ).
fof(f55058,plain,
( index_95 = select(queue_74,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f55057,f4]) ).
fof(f55060,plain,
index_95 = select(queue_74,head),
inference(forward_subsumption_resolution,[],[f55058,f3]) ).
fof(f55062,plain,
index_69 = index_95,
inference(forward_demodulation,[],[f55060,f17531]) ).
fof(f55065,plain,
index_96 = s(index_69),
inference(backward_demodulation,[],[f260,f55062]) ).
fof(f55296,plain,
( index_26 = select(queue_17,head)
| head = seq
| head = tail ),
inference(superposition,[],[f4148,f3558]) ).
fof(f55297,plain,
( index_26 = select(queue_17,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f55296,f4]) ).
fof(f55299,plain,
index_26 = select(queue_17,head),
inference(forward_subsumption_resolution,[],[f55297,f3]) ).
fof(f55302,plain,
( index_26 = select(queue_11,head)
| head = seq
| head = tail ),
inference(superposition,[],[f4163,f55299]) ).
fof(f55303,plain,
( index_26 = select(queue_11,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f55302,f4]) ).
fof(f55305,plain,
index_26 = select(queue_11,head),
inference(forward_subsumption_resolution,[],[f55303,f3]) ).
fof(f55307,plain,
index_26 = index_279,
inference(backward_demodulation,[],[f19481,f55305]) ).
fof(f55308,plain,
index_26 = s(index_278),
inference(backward_demodulation,[],[f230,f55307]) ).
fof(f55538,plain,
( index_47 = select(queue_38,head)
| head = seq
| head = tail ),
inference(superposition,[],[f3485,f3566]) ).
fof(f55539,plain,
( index_47 = select(queue_38,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f55538,f4]) ).
fof(f55541,plain,
index_47 = select(queue_38,head),
inference(forward_subsumption_resolution,[],[f55539,f3]) ).
fof(f55544,plain,
( index_47 = select(queue_32,head)
| head = seq
| head = tail ),
inference(superposition,[],[f4099,f55541]) ).
fof(f55545,plain,
( index_47 = select(queue_32,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f55544,f4]) ).
fof(f55547,plain,
index_47 = select(queue_32,head),
inference(forward_subsumption_resolution,[],[f55545,f3]) ).
fof(f55549,plain,
index_27 = index_47,
inference(forward_demodulation,[],[f55547,f18786]) ).
fof(f55552,plain,
index_48 = s(index_27),
inference(backward_demodulation,[],[f240,f55549]) ).
fof(f56104,plain,
( index_278 = select(queue_269,head)
| head = seq
| head = tail ),
inference(superposition,[],[f4619,f3562]) ).
fof(f56105,plain,
( index_278 = select(queue_269,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f56104,f4]) ).
fof(f56107,plain,
index_278 = select(queue_269,head),
inference(forward_subsumption_resolution,[],[f56105,f3]) ).
fof(f56110,plain,
( index_278 = select(queue_263,head)
| head = seq
| head = tail ),
inference(superposition,[],[f6164,f56107]) ).
fof(f56111,plain,
( index_278 = select(queue_263,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f56110,f4]) ).
fof(f56113,plain,
index_278 = select(queue_263,head),
inference(forward_subsumption_resolution,[],[f56111,f3]) ).
fof(f56115,plain,
index_258 = index_278,
inference(forward_demodulation,[],[f56113,f18778]) ).
fof(f56119,plain,
index_26 = s(index_258),
inference(backward_demodulation,[],[f55308,f56115]) ).
fof(f56177,plain,
index_156 = index_26,
inference(forward_demodulation,[],[f56119,f50519]) ).
fof(f56179,plain,
index_27 = s(index_156),
inference(backward_demodulation,[],[f225,f56177]) ).
fof(f56243,plain,
index_237 = index_27,
inference(forward_demodulation,[],[f56179,f14154]) ).
fof(f56249,plain,
index_48 = s(index_237),
inference(backward_demodulation,[],[f55552,f56243]) ).
fof(f56310,plain,
index_249 = index_48,
inference(forward_demodulation,[],[f56249,f11573]) ).
fof(f56316,plain,
index_69 = s(index_249),
inference(backward_demodulation,[],[f54874,f56310]) ).
fof(f56378,plain,
index_255 = index_69,
inference(forward_demodulation,[],[f56316,f9046]) ).
fof(f56384,plain,
index_96 = s(index_255),
inference(backward_demodulation,[],[f55065,f56378]) ).
fof(f56447,plain,
index_264 = index_96,
inference(forward_demodulation,[],[f56384,f7389]) ).
fof(f56450,plain,
index_264 = select(queue_101,head),
inference(backward_demodulation,[],[f17535,f56447]) ).
fof(f62871,plain,
( index_230 = select(queue_221,head)
| head = seq
| head = tail ),
inference(superposition,[],[f4114,f3574]) ).
fof(f62872,plain,
( index_230 = select(queue_221,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f62871,f4]) ).
fof(f62874,plain,
index_230 = select(queue_221,head),
inference(forward_subsumption_resolution,[],[f62872,f3]) ).
fof(f62877,plain,
( index_230 = select(queue_215,head)
| head = seq
| head = tail ),
inference(superposition,[],[f4129,f62874]) ).
fof(f62878,plain,
( index_230 = select(queue_215,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f62877,f4]) ).
fof(f62880,plain,
index_230 = select(queue_215,head),
inference(forward_subsumption_resolution,[],[f62878,f3]) ).
fof(f62882,plain,
index_210 = index_230,
inference(forward_demodulation,[],[f62880,f18774]) ).
fof(f62886,plain,
index_282 = s(index_210),
inference(backward_demodulation,[],[f19493,f62882]) ).
fof(f63278,plain,
( index_188 = select(queue_179,head)
| head = seq
| head = tail ),
inference(superposition,[],[f10698,f8445]) ).
fof(f63279,plain,
( index_188 = select(queue_179,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f63278,f4]) ).
fof(f63281,plain,
index_188 = select(queue_179,head),
inference(forward_subsumption_resolution,[],[f63279,f3]) ).
fof(f63284,plain,
( index_188 = select(queue_173,head)
| head = seq
| head = tail ),
inference(superposition,[],[f13244,f63281]) ).
fof(f63285,plain,
( index_188 = select(queue_173,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f63284,f4]) ).
fof(f63287,plain,
index_188 = select(queue_173,head),
inference(forward_subsumption_resolution,[],[f63285,f3]) ).
fof(f63289,plain,
index_168 = index_188,
inference(forward_demodulation,[],[f63287,f19485]) ).
fof(f63292,plain,
index_189 = s(index_168),
inference(backward_demodulation,[],[f192,f63289]) ).
fof(f63469,plain,
( index_209 = select(queue_200,head)
| head = seq
| head = tail ),
inference(superposition,[],[f4895,f3582]) ).
fof(f63470,plain,
( index_209 = select(queue_200,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f63469,f4]) ).
fof(f63472,plain,
index_209 = select(queue_200,head),
inference(forward_subsumption_resolution,[],[f63470,f3]) ).
fof(f63475,plain,
( index_209 = select(queue_194,head)
| head = seq
| head = tail ),
inference(superposition,[],[f6553,f63472]) ).
fof(f63476,plain,
( index_209 = select(queue_194,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f63475,f4]) ).
fof(f63478,plain,
index_209 = select(queue_194,head),
inference(forward_subsumption_resolution,[],[f63476,f3]) ).
fof(f63480,plain,
index_189 = index_209,
inference(forward_demodulation,[],[f63478,f19477]) ).
fof(f63483,plain,
index_210 = s(index_189),
inference(backward_demodulation,[],[f201,f63480]) ).
fof(f64191,plain,
( index_116 = select(queue_107,head)
| head = seq
| head = tail ),
inference(superposition,[],[f11557,f13817]) ).
fof(f64192,plain,
( index_116 = select(queue_107,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f64191,f4]) ).
fof(f64194,plain,
index_116 = select(queue_107,head),
inference(forward_subsumption_resolution,[],[f64192,f3]) ).
fof(f64197,plain,
( index_116 = select(queue_101,head)
| head = seq
| head = tail ),
inference(superposition,[],[f10244,f64194]) ).
fof(f64198,plain,
( index_116 = select(queue_101,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f64197,f4]) ).
fof(f64200,plain,
index_116 = select(queue_101,head),
inference(forward_subsumption_resolution,[],[f64198,f3]) ).
fof(f64202,plain,
index_116 = index_264,
inference(backward_demodulation,[],[f56450,f64200]) ).
fof(f64206,plain,
s(index_116) = index_270,
inference(backward_demodulation,[],[f5626,f64202]) ).
fof(f64286,plain,
index_117 = index_270,
inference(forward_demodulation,[],[f64206,f161]) ).
fof(f64290,plain,
index_276 = s(index_117),
inference(backward_demodulation,[],[f4179,f64286]) ).
fof(f68316,plain,
( index_137 = select(queue_128,head)
| head = seq
| head = tail ),
inference(superposition,[],[f21080,f29680]) ).
fof(f68317,plain,
( index_137 = select(queue_128,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f68316,f4]) ).
fof(f68319,plain,
index_137 = select(queue_128,head),
inference(forward_subsumption_resolution,[],[f68317,f3]) ).
fof(f68322,plain,
( index_137 = select(queue_122,head)
| head = seq
| head = tail ),
inference(superposition,[],[f19463,f68319]) ).
fof(f68323,plain,
( index_137 = select(queue_122,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f68322,f4]) ).
fof(f68325,plain,
index_137 = select(queue_122,head),
inference(forward_subsumption_resolution,[],[f68323,f3]) ).
fof(f68327,plain,
index_117 = index_137,
inference(forward_demodulation,[],[f68325,f20327]) ).
fof(f68330,plain,
index_138 = s(index_117),
inference(backward_demodulation,[],[f170,f68327]) ).
fof(f68389,plain,
index_138 = index_276,
inference(backward_demodulation,[],[f64290,f68330]) ).
fof(f68394,plain,
index_12 = s(index_138),
inference(backward_demodulation,[],[f3070,f68389]) ).
fof(f72302,plain,
( index_167 = select(queue_149,head)
| head = seq
| head = tail ),
inference(superposition,[],[f20313,f15718]) ).
fof(f72303,plain,
( index_167 = select(queue_149,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f72302,f4]) ).
fof(f72305,plain,
index_167 = select(queue_149,head),
inference(forward_subsumption_resolution,[],[f72303,f3]) ).
fof(f72308,plain,
( index_167 = select(queue_143,head)
| head = seq
| head = tail ),
inference(superposition,[],[f23204,f72305]) ).
fof(f72309,plain,
( index_167 = select(queue_143,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f72308,f4]) ).
fof(f72311,plain,
index_167 = select(queue_143,head),
inference(forward_subsumption_resolution,[],[f72309,f3]) ).
fof(f72313,plain,
index_138 = index_167,
inference(forward_demodulation,[],[f72311,f23232]) ).
fof(f72316,plain,
index_168 = s(index_138),
inference(backward_demodulation,[],[f183,f72313]) ).
fof(f72375,plain,
index_12 = index_168,
inference(forward_demodulation,[],[f72316,f68394]) ).
fof(f72381,plain,
index_189 = s(index_12),
inference(backward_demodulation,[],[f63292,f72375]) ).
fof(f72441,plain,
index_18 = index_189,
inference(forward_demodulation,[],[f72381,f2176]) ).
fof(f72447,plain,
index_210 = s(index_18),
inference(backward_demodulation,[],[f63483,f72441]) ).
fof(f72508,plain,
index_210 = index_24,
inference(backward_demodulation,[],[f1084,f72447]) ).
fof(f72513,plain,
index_33 = s(index_210),
inference(backward_demodulation,[],[f1159,f72508]) ).
fof(f72591,plain,
index_282 = index_33,
inference(forward_demodulation,[],[f72513,f62886]) ).
fof(f72592,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f72591,f40730]) ).
fof(f72593,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f72592]) ).
fof(f73472,plain,
index_39 = s(index_282),
inference(backward_demodulation,[],[f609,f72591]) ).
fof(f73486,plain,
index_282 != index_102,
inference(backward_demodulation,[],[f6713,f72591]) ).
fof(f73489,plain,
index_282 != index_108,
inference(backward_demodulation,[],[f9988,f72591]) ).
fof(f73490,plain,
index_282 != index_114,
inference(backward_demodulation,[],[f11289,f72591]) ).
fof(f73492,plain,
index_282 != index_123,
inference(backward_demodulation,[],[f13521,f72591]) ).
fof(f73494,plain,
index_282 != index_129,
inference(backward_demodulation,[],[f19016,f72591]) ).
fof(f73495,plain,
index_282 != index_135,
inference(backward_demodulation,[],[f20644,f72591]) ).
fof(f73497,plain,
index_282 != index_144,
inference(backward_demodulation,[],[f23508,f72591]) ).
fof(f73498,plain,
index_282 != index_150,
inference(backward_demodulation,[],[f24281,f72591]) ).
fof(f73499,plain,
index_282 != index_165,
inference(backward_demodulation,[],[f24843,f72591]) ).
fof(f73500,plain,
index_282 != index_174,
inference(backward_demodulation,[],[f25410,f72591]) ).
fof(f73501,plain,
index_282 != index_180,
inference(backward_demodulation,[],[f25931,f72591]) ).
fof(f73502,plain,
index_282 != index_186,
inference(backward_demodulation,[],[f26421,f72591]) ).
fof(f73503,plain,
index_282 != index_195,
inference(backward_demodulation,[],[f26888,f72591]) ).
fof(f73504,plain,
index_282 != index_201,
inference(backward_demodulation,[],[f27328,f72591]) ).
fof(f73505,plain,
index_282 != index_207,
inference(backward_demodulation,[],[f27740,f72591]) ).
fof(f73506,plain,
index_282 != index_216,
inference(backward_demodulation,[],[f28126,f72591]) ).
fof(f73537,plain,
e13 = select(earray_100,index_282),
inference(backward_demodulation,[],[f47076,f72591]) ).
fof(f79398,plain,
( elem_283 = select(earray_214,index_282)
| index_282 = index_216
| ~ spl0_4 ),
inference(superposition,[],[f4135,f40661]) ).
fof(f79399,plain,
( elem_283 = select(earray_214,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f79398,f73506]) ).
fof(f81807,plain,
( elem_283 = select(earray_205,index_282)
| index_282 = index_207
| ~ spl0_4 ),
inference(superposition,[],[f42006,f79399]) ).
fof(f81808,plain,
( elem_283 = select(earray_205,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81807,f73505]) ).
fof(f81811,plain,
( elem_283 = select(earray_199,index_282)
| index_282 = index_201
| ~ spl0_4 ),
inference(superposition,[],[f4901,f81808]) ).
fof(f81812,plain,
( elem_283 = select(earray_199,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81811,f73504]) ).
fof(f81815,plain,
( elem_283 = select(earray_193,index_282)
| index_282 = index_195
| ~ spl0_4 ),
inference(superposition,[],[f6559,f81812]) ).
fof(f81816,plain,
( elem_283 = select(earray_193,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81815,f73503]) ).
fof(f81819,plain,
( elem_283 = select(earray_184,index_282)
| index_282 = index_186
| ~ spl0_4 ),
inference(superposition,[],[f45871,f81816]) ).
fof(f81820,plain,
( elem_283 = select(earray_184,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81819,f73502]) ).
fof(f81823,plain,
( elem_283 = select(earray_178,index_282)
| index_282 = index_180
| ~ spl0_4 ),
inference(superposition,[],[f10704,f81820]) ).
fof(f81824,plain,
( elem_283 = select(earray_178,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81823,f73501]) ).
fof(f81827,plain,
( elem_283 = select(earray_172,index_282)
| index_282 = index_174
| ~ spl0_4 ),
inference(superposition,[],[f13250,f81824]) ).
fof(f81828,plain,
( elem_283 = select(earray_172,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81827,f73500]) ).
fof(f81831,plain,
( elem_283 = select(earray_163,index_282)
| index_282 = index_165
| ~ spl0_4 ),
inference(superposition,[],[f45887,f81828]) ).
fof(f81832,plain,
( elem_283 = select(earray_163,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81831,f73499]) ).
fof(f81835,plain,
( elem_283 = select(earray_148,index_282)
| index_282 = index_150
| ~ spl0_4 ),
inference(superposition,[],[f20319,f81832]) ).
fof(f81836,plain,
( elem_283 = select(earray_148,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81835,f73498]) ).
fof(f81839,plain,
( elem_283 = select(earray_142,index_282)
| index_282 = index_144
| ~ spl0_4 ),
inference(superposition,[],[f23210,f81836]) ).
fof(f81840,plain,
( elem_283 = select(earray_142,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81839,f73497]) ).
fof(f81843,plain,
( elem_283 = select(earray_133,index_282)
| index_282 = index_135
| ~ spl0_4 ),
inference(superposition,[],[f45903,f81840]) ).
fof(f81844,plain,
( elem_283 = select(earray_133,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81843,f73495]) ).
fof(f81847,plain,
( elem_283 = select(earray_127,index_282)
| index_282 = index_129
| ~ spl0_4 ),
inference(superposition,[],[f21086,f81844]) ).
fof(f81848,plain,
( elem_283 = select(earray_127,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81847,f73494]) ).
fof(f81851,plain,
( elem_283 = select(earray_121,index_282)
| index_282 = index_123
| ~ spl0_4 ),
inference(superposition,[],[f19469,f81848]) ).
fof(f81852,plain,
( elem_283 = select(earray_121,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81851,f73492]) ).
fof(f81855,plain,
( elem_283 = select(earray_112,index_282)
| index_282 = index_114
| ~ spl0_4 ),
inference(superposition,[],[f45919,f81852]) ).
fof(f81856,plain,
( elem_283 = select(earray_112,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81855,f73490]) ).
fof(f81859,plain,
( elem_283 = select(earray_106,index_282)
| index_282 = index_108
| ~ spl0_4 ),
inference(superposition,[],[f11563,f81856]) ).
fof(f81860,plain,
( elem_283 = select(earray_106,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81859,f73489]) ).
fof(f81862,plain,
( elem_283 = select(earray_100,index_282)
| index_282 = index_102
| ~ spl0_4 ),
inference(superposition,[],[f81860,f10250]) ).
fof(f81865,plain,
( elem_283 = select(earray_100,index_282)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81862,f73486]) ).
fof(f81867,plain,
( e13 = elem_283
| ~ spl0_4 ),
inference(forward_demodulation,[],[f81865,f73537]) ).
fof(f81870,plain,
( $false
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f81867,f398]) ).
fof(f81871,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f81870]) ).
fof(f81877,plain,
( index_243 = s(index_282)
| ~ spl0_1 ),
inference(backward_demodulation,[],[f1505,f3057]) ).
fof(f81982,plain,
( index_243 = index_39
| ~ spl0_1 ),
inference(backward_demodulation,[],[f73472,f81877]) ).
fof(f81986,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f81982,f29142]) ).
fof(f81987,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f81986]) ).
cnf(s2,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f3063]) ).
cnf(s4,plain,
( ~ spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f40663]) ).
cnf(s6,plain,
~ spl0_3,
inference(sat_conversion,[],[f72593]) ).
cnf(s8,plain,
~ spl0_4,
inference(sat_conversion,[],[f81871]) ).
cnf(s11,plain,
~ spl0_1,
inference(sat_conversion,[],[f81987]) ).
cnf(s12,plain,
~ spl0_2,
inference(rat,[],[s4,s8,s6]) ).
cnf(s13,plain,
$false,
inference(rat,[],[s2,s12,s11]) ).
fof(f81988,plain,
$false,
inference(avatar_sat_refutation,[],[s13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV569-1.040 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n006.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 11:53:40 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.41/1.97 % (3914718)Input is clausal, will run a generic CNF schedule.
% 7.41/1.97 % (3914725)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=992660267:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.41/1.97 % (3914728)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2621188570:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.41/1.97 % (3914729)dis-21_1_sil=8000:lcm=predicate:random_seed=358737721:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.41/1.97 % (3914726)lrs+10_1_sil=8000:sp=occurrence:random_seed=2143940422:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.41/1.97 % (3914724)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=412555831:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.41/1.97 % (3914727)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2760428657:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.41/1.97 % (3914723)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4060833976:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.41/1.97 % (3914729)Refutation not found, incomplete strategy
% 7.41/1.97 % (3914729)------------------------------
% 7.41/1.97 % (3914729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.97 % (3914729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.97 % (3914729)CaDiCaL version: 2.1.3
% 7.41/1.97 % (3914729)Termination reason: Refutation not found, incomplete strategy
% 7.41/1.97 % (3914729)Time elapsed: 0.028 s
% 7.41/1.97 % (3914729)Peak memory usage: 88 MB
% 7.41/1.97 % (3914729)Instructions burned: 63 (million)
% 7.41/1.97 % (3914726)Instruction limit reached!
% 7.41/1.97 % (3914726)------------------------------
% 7.41/1.97 % (3914726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.97 % (3914726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.97 % (3914726)CaDiCaL version: 2.1.3
% 7.41/1.97 % (3914726)Termination reason: Instruction limit
% 7.41/1.97 % (3914726)Termination phase: Saturation
% 7.41/1.97 % (3914726)Time elapsed: 0.049 s
% 7.41/1.97 % (3914726)Peak memory usage: 89 MB
% 7.41/1.97 % (3914726)Instructions burned: 108 (million)
% 7.41/1.97 % (3914727)Instruction limit reached!
% 7.41/1.97 % (3914727)------------------------------
% 7.41/1.97 % (3914727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.97 % (3914727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.97 % (3914727)CaDiCaL version: 2.1.3
% 7.41/1.97 % (3914727)Termination reason: Instruction limit
% 7.41/1.97 % (3914727)Termination phase: Saturation
% 7.41/1.97 % (3914727)Time elapsed: 0.050 s
% 7.41/1.97 % (3914727)Peak memory usage: 89 MB
% 7.41/1.97 % (3914727)Instructions burned: 114 (million)
% 7.41/1.97 % (3914728)Instruction limit reached!
% 7.41/1.97 % (3914728)------------------------------
% 7.41/1.97 % (3914728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/1.97 % (3914728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/1.97 % (3914728)CaDiCaL version: 2.1.3
% 7.41/1.97 % (3914728)Termination reason: Instruction limit
% 7.41/1.97 % (3914728)Termination phase: Saturation
% 7.41/1.97 % (3914728)Time elapsed: 0.080 s
% 7.41/1.97 % (3914728)Peak memory usage: 89 MB
% 7.41/1.97 % (3914728)Instructions burned: 180 (million)
% 7.41/1.97 % (3914738)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4244191735:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 7.41/1.97 % (3914737)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1078920730:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.41/1.97 % (3914739)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2475407331:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.41/1.97 % (3914737)Instruction limit reached!
% 7.41/1.97 % (3914737)------------------------------
% 7.41/1.97 % (3914737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.09 % (3914737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.09 % (3914737)CaDiCaL version: 2.1.3
% 17.13/3.09 % (3914737)Termination reason: Instruction limit
% 17.13/3.09 % (3914737)Termination phase: Saturation
% 17.13/3.09 % (3914737)Time elapsed: 0.057 s
% 17.13/3.09 % (3914737)Peak memory usage: 88 MB
% 17.13/3.09 % (3914737)Instructions burned: 145 (million)
% 17.13/3.09 % (3914738)Instruction limit reached!
% 17.13/3.09 % (3914738)------------------------------
% 17.13/3.09 % (3914738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.09 % (3914738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.09 % (3914738)CaDiCaL version: 2.1.3
% 17.13/3.09 % (3914738)Termination reason: Instruction limit
% 17.13/3.09 % (3914738)Termination phase: Saturation
% 17.13/3.09 % (3914738)Time elapsed: 0.073 s
% 17.13/3.09 % (3914738)Peak memory usage: 89 MB
% 17.13/3.09 % (3914738)Instructions burned: 190 (million)
% 17.13/3.09 % (3914729)------------------------------
% 17.13/3.09 % (3914729)------------------------------
% 17.13/3.09 % (3914739)Instruction limit reached!
% 17.13/3.09 % (3914739)------------------------------
% 17.13/3.09 % (3914739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.09 % (3914739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.09 % (3914739)CaDiCaL version: 2.1.3
% 17.13/3.09 % (3914739)Termination reason: Instruction limit
% 17.13/3.09 % (3914739)Termination phase: Saturation
% 17.13/3.09 % (3914739)Time elapsed: 0.092 s
% 17.13/3.09 % (3914739)Peak memory usage: 89 MB
% 17.13/3.09 % (3914739)Instructions burned: 219 (million)
% 17.13/3.09 % (3914745)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1051091633:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 17.13/3.09 % (3914744)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2695153116:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 17.13/3.09 % (3914743)lrs+10_64_to=lpo:sil=8000:random_seed=3013302011:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 17.13/3.09 % (3914745)Instruction limit reached!
% 17.13/3.09 % (3914745)------------------------------
% 17.13/3.09 % (3914745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.09 % (3914745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.09 % (3914745)CaDiCaL version: 2.1.3
% 17.13/3.09 % (3914745)Termination reason: Instruction limit
% 17.13/3.09 % (3914745)Termination phase: Saturation
% 17.13/3.09 % (3914745)Time elapsed: 0.044 s
% 17.13/3.09 % (3914745)Peak memory usage: 93 MB
% 17.13/3.09 % (3914745)Instructions burned: 158 (million)
% 17.13/3.09 % (3914743)Instruction limit reached!
% 17.13/3.09 % (3914743)------------------------------
% 17.13/3.09 % (3914743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.09 % (3914743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.09 % (3914743)CaDiCaL version: 2.1.3
% 17.13/3.09 % (3914743)Termination reason: Instruction limit
% 17.13/3.09 % (3914743)Termination phase: Saturation
% 17.13/3.09 % (3914743)Time elapsed: 0.058 s
% 17.13/3.09 % (3914743)Peak memory usage: 88 MB
% 17.13/3.09 % (3914743)Instructions burned: 126 (million)
% 17.13/3.09 % (3914746)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2149740788:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 17.13/3.09 % (3914744)Instruction limit reached!
% 17.13/3.09 % (3914744)------------------------------
% 17.13/3.09 % (3914744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.09 % (3914744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.09 % (3914744)CaDiCaL version: 2.1.3
% 17.13/3.09 % (3914744)Termination reason: Instruction limit
% 17.13/3.09 % (3914744)Termination phase: Saturation
% 17.13/3.09 % (3914744)Time elapsed: 0.088 s
% 17.13/3.09 % (3914744)Peak memory usage: 90 MB
% 17.13/3.09 % (3914744)Instructions burned: 195 (million)
% 17.13/3.09 % (3914750)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3687198614:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 17.13/3.09 % (3914750)Instruction limit reached!
% 17.13/3.09 % (3914750)------------------------------
% 17.13/3.09 % (3914750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.09 % (3914750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.32/5.05 % (3914750)CaDiCaL version: 2.1.3
% 31.32/5.05 % (3914750)Termination reason: Instruction limit
% 31.32/5.05 % (3914750)Termination phase: Saturation
% 31.32/5.05 % (3914750)Time elapsed: 0.024 s
% 31.32/5.05 % (3914750)Peak memory usage: 89 MB
% 31.32/5.05 % (3914750)Instructions burned: 108 (million)
% 31.32/5.05 % (3914751)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2237299430:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 31.32/5.05 % (3914753)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=577436990:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 31.32/5.05 % (3914751)Instruction limit reached!
% 31.32/5.05 % (3914751)------------------------------
% 31.32/5.05 % (3914751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.32/5.05 % (3914751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.32/5.05 % (3914751)CaDiCaL version: 2.1.3
% 31.32/5.05 % (3914751)Termination reason: Instruction limit
% 31.32/5.05 % (3914751)Termination phase: Saturation
% 31.32/5.05 % (3914751)Time elapsed: 0.042 s
% 31.32/5.05 % (3914751)Peak memory usage: 88 MB
% 31.32/5.05 % (3914751)Instructions burned: 109 (million)
% 31.32/5.05 % (3914755)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1241564400:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 31.32/5.05 % (3914753)Instruction limit reached!
% 31.32/5.05 % (3914753)------------------------------
% 31.32/5.05 % (3914753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.32/5.05 % (3914753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.32/5.05 % (3914753)CaDiCaL version: 2.1.3
% 31.32/5.05 % (3914753)Termination reason: Instruction limit
% 31.32/5.05 % (3914753)Termination phase: Saturation
% 31.32/5.05 % (3914753)Time elapsed: 0.111 s
% 31.32/5.05 % (3914753)Peak memory usage: 90 MB
% 31.32/5.05 % (3914753)Instructions burned: 242 (million)
% 31.32/5.05 % (3914758)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2825941572:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 31.32/5.05 % (3914758)Instruction limit reached!
% 31.32/5.05 % (3914758)------------------------------
% 31.32/5.05 % (3914758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.32/5.05 % (3914758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.32/5.05 % (3914758)CaDiCaL version: 2.1.3
% 31.32/5.05 % (3914758)Termination reason: Instruction limit
% 31.32/5.05 % (3914758)Termination phase: Saturation
% 31.32/5.05 % (3914758)Time elapsed: 0.062 s
% 31.32/5.05 % (3914758)Peak memory usage: 89 MB
% 31.32/5.05 % (3914758)Instructions burned: 134 (million)
% 31.32/5.05 % (3914760)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3552402994:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 31.32/5.05 % (3914762)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2580667379:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 31.32/5.05 % (3914762)Instruction limit reached!
% 31.32/5.05 % (3914762)------------------------------
% 31.32/5.05 % (3914762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.32/5.05 % (3914762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.32/5.05 % (3914762)CaDiCaL version: 2.1.3
% 31.32/5.05 % (3914762)Termination reason: Instruction limit
% 31.32/5.05 % (3914762)Termination phase: Saturation
% 31.32/5.05 % (3914762)Time elapsed: 0.087 s
% 31.32/5.05 % (3914762)Peak memory usage: 90 MB
% 31.32/5.05 % (3914762)Instructions burned: 192 (million)
% 31.32/5.05 % (3914760)Instruction limit reached!
% 31.32/5.05 % (3914760)------------------------------
% 31.32/5.05 % (3914760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.32/5.05 % (3914760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.32/5.05 % (3914760)CaDiCaL version: 2.1.3
% 31.32/5.05 % (3914760)Termination reason: Instruction limit
% 31.32/5.05 % (3914760)Termination phase: Saturation
% 31.32/5.05 % (3914760)Time elapsed: 0.243 s
% 31.32/5.05 % (3914760)Peak memory usage: 93 MB
% 31.32/5.05 % (3914760)Instructions burned: 501 (million)
% 31.32/5.05 % (3914765)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2935665685:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 42.81/6.70 % (3914766)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1252697747:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 42.81/6.70 % (3914766)Instruction limit reached!
% 42.81/6.70 % (3914766)------------------------------
% 42.81/6.70 % (3914766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/6.70 % (3914765)Instruction limit reached!
% 42.81/6.70 % (3914765)------------------------------
% 42.81/6.70 % (3914765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/6.70 % (3914765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/6.70 % (3914766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/6.70 % (3914765)CaDiCaL version: 2.1.3
% 42.81/6.70 % (3914766)CaDiCaL version: 2.1.3
% 42.81/6.70 % (3914765)Termination reason: Instruction limit
% 42.81/6.70 % (3914765)Termination phase: Saturation
% 42.81/6.70 % (3914766)Termination reason: Instruction limit
% 42.81/6.70 % (3914766)Termination phase: Saturation
% 42.81/6.70 % (3914765)Time elapsed: 0.129 s
% 42.81/6.70 % (3914766)Time elapsed: 0.075 s
% 42.81/6.70 % (3914765)Peak memory usage: 92 MB
% 42.81/6.70 % (3914766)Peak memory usage: 90 MB
% 42.81/6.70 % (3914766)Instructions burned: 159 (million)
% 42.81/6.70 % (3914765)Instructions burned: 265 (million)
% 42.81/6.70 % (3914769)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3470674609:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 42.81/6.70 % (3914770)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3827793296:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 42.81/6.70 % (3914770)Instruction limit reached!
% 42.81/6.70 % (3914770)------------------------------
% 42.81/6.70 % (3914770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/6.70 % (3914770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/6.70 % (3914770)CaDiCaL version: 2.1.3
% 42.81/6.70 % (3914770)Termination reason: Instruction limit
% 42.81/6.70 % (3914770)Termination phase: Saturation
% 42.81/6.70 % (3914770)Time elapsed: 0.267 s
% 42.81/6.70 % (3914770)Peak memory usage: 93 MB
% 42.81/6.70 % (3914770)Instructions burned: 538 (million)
% 42.81/6.70 % (3914746)Instruction limit reached!
% 42.81/6.70 % (3914746)------------------------------
% 42.81/6.70 % (3914746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/6.70 % (3914746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/6.70 % (3914746)CaDiCaL version: 2.1.3
% 42.81/6.70 % (3914746)Termination reason: Instruction limit
% 42.81/6.70 % (3914746)Termination phase: Saturation
% 42.81/6.70 % (3914746)Time elapsed: 1.312 s
% 42.81/6.70 % (3914746)Peak memory usage: 151 MB
% 42.81/6.70 % (3914746)Instructions burned: 3396 (million)
% 42.81/6.70 % (3914773)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=174274388:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 42.81/6.70 % (3914774)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2615093490:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi)
% 42.81/6.70 % (3914773)Instruction limit reached!
% 42.81/6.70 % (3914773)------------------------------
% 42.81/6.70 % (3914773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/6.70 % (3914773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/6.70 % (3914773)CaDiCaL version: 2.1.3
% 42.81/6.70 % (3914773)Termination reason: Instruction limit
% 42.81/6.70 % (3914773)Termination phase: Saturation
% 42.81/6.70 % (3914773)Time elapsed: 0.088 s
% 42.81/6.70 % (3914773)Peak memory usage: 89 MB
% 42.81/6.70 % (3914773)Instructions burned: 180 (million)
% 42.81/6.70 % (3914777)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=4004223713:i=412:gtgl=4:gtg=exists_all_2979 on theBenchmark for (2979ds/412Mi)
% 42.81/6.70 % (3914777)Instruction limit reached!
% 42.81/6.70 % (3914777)------------------------------
% 42.81/6.70 % (3914777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.81/6.70 % (3914777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.81/6.70 % (3914777)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914777)Termination reason: Instruction limit
% 53.77/8.27 % (3914777)Termination phase: Saturation
% 53.77/8.27 % (3914777)Time elapsed: 0.241 s
% 53.77/8.27 % (3914777)Peak memory usage: 96 MB
% 53.77/8.27 % (3914777)Instructions burned: 413 (million)
% 53.77/8.27 % (3914779)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2125871302:s2pl=no:i=8478:s2at=4:nm=6_2975 on theBenchmark for (2975ds/8478Mi)
% 53.77/8.27 % (3914755)Instruction limit reached!
% 53.77/8.27 % (3914755)------------------------------
% 53.77/8.27 % (3914755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914755)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914755)Termination reason: Instruction limit
% 53.77/8.27 % (3914755)Termination phase: Saturation
% 53.77/8.27 % (3914755)Time elapsed: 2.594 s
% 53.77/8.27 % (3914755)Peak memory usage: 160 MB
% 53.77/8.27 % (3914755)Instructions burned: 5210 (million)
% 53.77/8.27 % (3914769)Instruction limit reached!
% 53.77/8.27 % (3914769)------------------------------
% 53.77/8.27 % (3914769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914769)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914769)Termination reason: Instruction limit
% 53.77/8.27 % (3914769)Termination phase: Saturation
% 53.77/8.27 % (3914769)Time elapsed: 1.840 s
% 53.77/8.27 % (3914769)Peak memory usage: 148 MB
% 53.77/8.27 % (3914769)Instructions burned: 3256 (million)
% 53.77/8.27 % (3914781)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=1003369127:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2966 on theBenchmark for (2966ds/303Mi)
% 53.77/8.27 % (3914782)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3940650790:st=4:i=720:sd=3:fsr=off:ss=axioms_2965 on theBenchmark for (2965ds/720Mi)
% 53.77/8.27 % (3914781)Refutation not found, incomplete strategy
% 53.77/8.27 % (3914781)------------------------------
% 53.77/8.27 % (3914781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914781)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914781)Termination reason: Refutation not found, incomplete strategy
% 53.77/8.27 % (3914781)Time elapsed: 0.094 s
% 53.77/8.27 % (3914781)Peak memory usage: 90 MB
% 53.77/8.27 % (3914781)Instructions burned: 241 (million)
% 53.77/8.27 % (3914781)------------------------------
% 53.77/8.27 % (3914781)------------------------------
% 53.77/8.27 % (3914782)Instruction limit reached!
% 53.77/8.27 % (3914782)------------------------------
% 53.77/8.27 % (3914782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914782)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914782)Termination reason: Instruction limit
% 53.77/8.27 % (3914782)Termination phase: Saturation
% 53.77/8.27 % (3914782)Time elapsed: 0.323 s
% 53.77/8.27 % (3914782)Peak memory usage: 94 MB
% 53.77/8.27 % (3914782)Instructions burned: 722 (million)
% 53.77/8.27 % (3914785)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3897806122:i=598:bs=on:bd=preordered:av=off:ss=axioms_2961 on theBenchmark for (2961ds/598Mi)
% 53.77/8.27 % (3914786)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3423935714:i=2989:sd=3:ss=axioms:sgt=60_2961 on theBenchmark for (2961ds/2989Mi)
% 53.77/8.27 % (3914785)Instruction limit reached!
% 53.77/8.27 % (3914785)------------------------------
% 53.77/8.27 % (3914785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914785)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914785)Termination reason: Instruction limit
% 53.77/8.27 % (3914785)Termination phase: Saturation
% 53.77/8.27 % (3914785)Time elapsed: 0.265 s
% 53.77/8.27 % (3914785)Peak memory usage: 92 MB
% 53.77/8.27 % (3914785)Instructions burned: 599 (million)
% 53.77/8.27 % (3914789)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=384172487:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2957 on theBenchmark for (2957ds/1997Mi)
% 53.77/8.27 % (3914774)Instruction limit reached!
% 53.77/8.27 % (3914774)------------------------------
% 53.77/8.27 % (3914774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914774)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914774)Termination reason: Instruction limit
% 53.77/8.27 % (3914774)Termination phase: Saturation
% 53.77/8.27 % (3914774)Time elapsed: 2.768 s
% 53.77/8.27 % (3914774)Peak memory usage: 183 MB
% 53.77/8.27 % (3914774)Instructions burned: 10310 (million)
% 53.77/8.27 % (3914791)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2888794196:i=2088:bd=preordered:av=off_2952 on theBenchmark for (2952ds/2088Mi)
% 53.77/8.27 % (3914791)Instruction limit reached!
% 53.77/8.27 % (3914791)------------------------------
% 53.77/8.27 % (3914791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914791)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914791)Termination reason: Instruction limit
% 53.77/8.27 % (3914791)Termination phase: Saturation
% 53.77/8.27 % (3914791)Time elapsed: 0.735 s
% 53.77/8.27 % (3914791)Peak memory usage: 139 MB
% 53.77/8.27 % (3914791)Instructions burned: 2091 (million)
% 53.77/8.27 % (3914789)Instruction limit reached!
% 53.77/8.27 % (3914789)------------------------------
% 53.77/8.27 % (3914789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914789)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914789)Termination reason: Instruction limit
% 53.77/8.27 % (3914789)Termination phase: Saturation
% 53.77/8.27 % (3914789)Time elapsed: 1.207 s
% 53.77/8.27 % (3914789)Peak memory usage: 138 MB
% 53.77/8.27 % (3914789)Instructions burned: 1999 (million)
% 53.77/8.27 % (3914793)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2462470916:i=1098:nicw=on_2943 on theBenchmark for (2943ds/1098Mi)
% 53.77/8.27 % (3914794)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=120310914:i=433:bd=preordered_2943 on theBenchmark for (2943ds/433Mi)
% 53.77/8.27 % (3914786)Instruction limit reached!
% 53.77/8.27 % (3914786)------------------------------
% 53.77/8.27 % (3914786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914786)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914786)Termination reason: Instruction limit
% 53.77/8.27 % (3914786)Termination phase: Saturation
% 53.77/8.27 % (3914786)Time elapsed: 1.834 s
% 53.77/8.27 % (3914786)Peak memory usage: 146 MB
% 53.77/8.27 % (3914786)Instructions burned: 2989 (million)
% 53.77/8.27 % (3914793)Instruction limit reached!
% 53.77/8.27 % (3914793)------------------------------
% 53.77/8.27 % (3914793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914793)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914793)Termination reason: Instruction limit
% 53.77/8.27 % (3914793)Termination phase: Saturation
% 53.77/8.27 % (3914793)Time elapsed: 0.264 s
% 53.77/8.27 % (3914793)Peak memory usage: 95 MB
% 53.77/8.27 % (3914793)Instructions burned: 1099 (million)
% 53.77/8.27 % (3914794)Instruction limit reached!
% 53.77/8.27 % (3914794)------------------------------
% 53.77/8.27 % (3914794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914794)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914794)Termination reason: Instruction limit
% 53.77/8.27 % (3914794)Termination phase: Saturation
% 53.77/8.27 % (3914794)Time elapsed: 0.225 s
% 53.77/8.27 % (3914794)Peak memory usage: 93 MB
% 53.77/8.27 % (3914794)Instructions burned: 434 (million)
% 53.77/8.27 % (3914797)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1898931869:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2941 on theBenchmark for (2941ds/2942Mi)
% 53.77/8.27 % (3914799)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3284289188:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2940 on theBenchmark for (2940ds/596Mi)
% 53.77/8.27 % (3914799)Refutation not found, incomplete strategy
% 53.77/8.27 % (3914799)------------------------------
% 53.77/8.27 % (3914799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914799)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914799)Termination reason: Refutation not found, incomplete strategy
% 53.77/8.27 % (3914799)Time elapsed: 0.024 s
% 53.77/8.27 % (3914799)Peak memory usage: 89 MB
% 53.77/8.27 % (3914799)Instructions burned: 98 (million)
% 53.77/8.27 % (3914798)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1395374775:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2940 on theBenchmark for (2940ds/6922Mi)
% 53.77/8.27 % (3914799)------------------------------
% 53.77/8.27 % (3914799)------------------------------
% 53.77/8.27 % (3914803)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2918010174:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2937 on theBenchmark for (2937ds/4123Mi)
% 53.77/8.27 % (3914779)Instruction limit reached!
% 53.77/8.27 % (3914779)------------------------------
% 53.77/8.27 % (3914779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.77/8.27 % (3914779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/8.27 % (3914779)CaDiCaL version: 2.1.3
% 53.77/8.27 % (3914779)Termination reason: Instruction limit
% 53.77/8.27 % (3914779)Termination phase: Saturation
% 53.77/8.27 % (3914779)Time elapsed: 4.561 s
% 53.77/8.27 % (3914779)Peak memory usage: 188 MB
% 53.77/8.27 % (3914779)Instructions burned: 8479 (million)
% 53.77/8.27 % (3914805)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1184319219:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2928 on theBenchmark for (2928ds/16411Mi)
% 53.77/8.27 % (3914725)First to succeed.
% 53.77/8.27 % (3914725)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3914718"
% 53.77/8.27 % (3914725)Refutation found. Thanks to Tanya!
% 53.77/8.27 % SZS status Unsatisfiable for theBenchmark
% 53.77/8.27 % SZS output start Proof for theBenchmark
% See solution above
% 54.25/8.36 % (3914725)------------------------------
% 54.25/8.36 % (3914725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.25/8.36 % (3914725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.25/8.36 % (3914725)CaDiCaL version: 2.1.3
% 54.25/8.36 % (3914725)Termination reason: Refutation
% 54.25/8.36 % (3914725)Time elapsed: 7.209 s
% 54.25/8.36 % (3914725)Peak memory usage: 201 MB
% 54.25/8.36 % (3914725)Instructions burned: 15989 (million)
% 54.25/8.36 % (3914725)------------------------------
% 54.25/8.36 % (3914725)------------------------------
% 54.25/8.36 % (3914718)Success in time 7.603 s
% 54.25/8.36 % Vampire exiting
%------------------------------------------------------------------------------