%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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:25:59 PM UTC 2026
% Result : Unsatisfiable 11.59s 2.51s
% Output : Refutation 11.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 256
% Syntax : Number of formulae : 1169 (1084 unt; 2 def)
% Number of atoms : 1351 (1316 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 608 ( 426 ~; 180 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 2 avg)
% Maximal term depth : 20 ( 3 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 266 ( 266 usr; 257 con; 0-3 aty)
% Number of variables : 95 ( 0 sgn 95 !; 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,
! [X0,X1] : rselect_seq(rstore_seq(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_seq) ).
fof(f4,axiom,
! [X0,X1] : rselect_head(rstore_head(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_head) ).
fof(f5,axiom,
! [X0,X1] : rselect_tail(rstore_tail(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_tail) ).
fof(f6,axiom,
! [X0,X1] : rselect_seq(rstore_head(X0,X1)) = rselect_seq(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_seq_head) ).
fof(f7,axiom,
! [X0,X1] : rselect_seq(rstore_tail(X0,X1)) = rselect_seq(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_seq_tail) ).
fof(f8,plain,
! [X0,X1] : rselect_seq(X0) = rselect_seq(rstore_tail(X0,X1)),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X0,X1] : rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_head_tail) ).
fof(f10,axiom,
! [X0,X1] : rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_head_seq) ).
fof(f11,plain,
! [X0,X1] : rselect_head(X0) = rselect_head(rstore_seq(X0,X1)),
inference(reorient_equations,[],[f10]) ).
fof(f13,axiom,
! [X0,X1] : rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_tail_head) ).
fof(f14,plain,
! [X0,X1] : rselect_tail(X0) = rselect_tail(rstore_head(X0,X1)),
inference(reorient_equations,[],[f13]) ).
fof(f46,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(f47,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(f48,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(f49,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(f50,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(f51,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(f52,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(f53,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(f54,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as11) ).
fof(f55,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as10) ).
fof(f56,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as9) ).
fof(f57,axiom,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as8) ).
fof(f58,axiom,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as7) ).
fof(f59,axiom,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as6) ).
fof(f60,axiom,
! [X0] : s(s(s(s(s(X0))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as5) ).
fof(f61,axiom,
! [X0] : s(s(s(s(X0)))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as4) ).
fof(f62,axiom,
! [X0] : s(s(s(X0))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as3) ).
fof(f63,axiom,
! [X0] : s(s(X0)) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as2) ).
fof(f64,axiom,
! [X0] : s(X0) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as1) ).
fof(f66,axiom,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f67,axiom,
earray_104 = rselect_seq(q22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f68,axiom,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f69,axiom,
earray_110 = rselect_seq(q23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f70,axiom,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f71,axiom,
earray_119 = rselect_seq(q24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f72,axiom,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f73,axiom,
earray_125 = rselect_seq(q25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f74,axiom,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f75,axiom,
earray_131 = rselect_seq(q26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f76,axiom,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f78,axiom,
earray_140 = rselect_seq(q27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f79,axiom,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f80,axiom,
earray_146 = rselect_seq(q28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f81,axiom,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f84,axiom,
earray_16 = store(earray_14,index_15,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f85,axiom,
earray_161 = rselect_seq(q29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f86,axiom,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f98,axiom,
earray_20 = rselect_seq(q11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
fof(f101,axiom,
earray_212 = rselect_seq(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f102,axiom,
earray_22 = store(earray_20,index_21,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f103,axiom,
earray_29 = rselect_seq(q12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f104,axiom,
earray_31 = store(earray_29,index_30,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f105,axiom,
earray_35 = rselect_seq(q13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f106,axiom,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f108,axiom,
earray_41 = rselect_seq(q14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
fof(f109,axiom,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp44) ).
fof(f110,axiom,
earray_50 = rselect_seq(q15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
fof(f111,axiom,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp46) ).
fof(f112,axiom,
earray_56 = rselect_seq(q16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
fof(f113,axiom,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp48) ).
fof(f114,axiom,
earray_62 = rselect_seq(q17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp49) ).
fof(f115,axiom,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp50) ).
fof(f116,axiom,
earray_71 = rselect_seq(q18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp51) ).
fof(f117,axiom,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp52) ).
fof(f121,axiom,
earray_83 = rselect_seq(q19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp56) ).
fof(f122,axiom,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp57) ).
fof(f123,axiom,
earray_89 = rselect_seq(q20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp58) ).
fof(f124,axiom,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp59) ).
fof(f125,axiom,
earray_98 = rselect_seq(q21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp60) ).
fof(f126,axiom,
elem_214 = select(earray_212,index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp61) ).
fof(f127,axiom,
index_0 = rselect_tail(q),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp62) ).
fof(f128,axiom,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp63) ).
fof(f129,axiom,
index_105 = rselect_tail(q22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp64) ).
fof(f130,axiom,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp65) ).
fof(f131,axiom,
index_111 = rselect_tail(q23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp66) ).
fof(f132,axiom,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp67) ).
fof(f133,axiom,
index_116 = rselect_head(queue_115),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp68) ).
fof(f134,axiom,
index_117 = s(index_116),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp69) ).
fof(f135,axiom,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp70) ).
fof(f136,axiom,
index_120 = rselect_tail(q24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp71) ).
fof(f137,axiom,
index_123 = s(index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp72) ).
fof(f138,axiom,
index_126 = rselect_tail(q25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp73) ).
fof(f139,axiom,
index_129 = s(index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp74) ).
fof(f140,axiom,
index_132 = rselect_tail(q26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp75) ).
fof(f141,axiom,
index_135 = s(index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp76) ).
fof(f142,axiom,
index_137 = rselect_head(queue_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp77) ).
fof(f143,axiom,
index_138 = s(index_137),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp78) ).
fof(f144,axiom,
index_141 = rselect_tail(q27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp79) ).
fof(f145,axiom,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp80) ).
fof(f146,axiom,
index_147 = rselect_tail(q28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp81) ).
fof(f147,axiom,
index_15 = rselect_tail(q10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp82) ).
fof(f148,axiom,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp83) ).
fof(f149,axiom,
index_153 = rselect_tail(q2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp84) ).
fof(f150,axiom,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp85) ).
fof(f151,axiom,
index_158 = rselect_head(queue_157),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp86) ).
fof(f152,axiom,
index_159 = s(index_158),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp87) ).
fof(f153,axiom,
index_162 = rselect_tail(q29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp88) ).
fof(f155,axiom,
index_167 = rselect_head(queue_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp90) ).
fof(f156,axiom,
index_168 = s(index_167),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp91) ).
fof(f157,axiom,
index_171 = rselect_tail(q3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp92) ).
fof(f158,axiom,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp93) ).
fof(f159,axiom,
index_177 = rselect_tail(q4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp94) ).
fof(f160,axiom,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp95) ).
fof(f161,axiom,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp96) ).
fof(f162,axiom,
index_183 = rselect_tail(q5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp97) ).
fof(f163,axiom,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp98) ).
fof(f164,axiom,
index_188 = rselect_head(queue_187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
fof(f165,axiom,
index_189 = s(index_188),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
fof(f166,axiom,
index_192 = rselect_tail(q6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f167,axiom,
index_195 = s(index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp102) ).
fof(f168,axiom,
index_198 = rselect_tail(q7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp103) ).
fof(f169,axiom,
index_201 = s(index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
fof(f170,axiom,
index_204 = rselect_tail(q8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp105) ).
fof(f171,axiom,
index_207 = s(index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp106) ).
fof(f172,axiom,
index_209 = rselect_head(queue_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
fof(f173,axiom,
index_21 = rselect_tail(q11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
fof(f174,axiom,
index_210 = s(index_209),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
fof(f175,axiom,
index_213 = rselect_head(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp110) ).
fof(f176,axiom,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp111) ).
fof(f177,axiom,
index_26 = rselect_head(queue_25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp112) ).
fof(f178,axiom,
index_27 = s(index_26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp113) ).
fof(f179,axiom,
index_3 = rselect_tail(q0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
fof(f180,axiom,
index_30 = rselect_tail(q12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp115) ).
fof(f181,axiom,
index_33 = s(index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp116) ).
fof(f182,axiom,
index_36 = rselect_tail(q13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp117) ).
fof(f183,axiom,
index_39 = s(index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp118) ).
fof(f184,axiom,
index_42 = rselect_tail(q14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp119) ).
fof(f185,axiom,
index_45 = s(index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp120) ).
fof(f186,axiom,
index_47 = rselect_head(queue_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp121) ).
fof(f187,axiom,
index_48 = s(index_47),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp122) ).
fof(f188,axiom,
index_51 = rselect_tail(q15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp123) ).
fof(f189,axiom,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp124) ).
fof(f190,axiom,
index_57 = rselect_tail(q16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp125) ).
fof(f191,axiom,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp126) ).
fof(f192,axiom,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp127) ).
fof(f193,axiom,
index_63 = rselect_tail(q17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp128) ).
fof(f194,axiom,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp129) ).
fof(f195,axiom,
index_68 = rselect_head(queue_67),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp130) ).
fof(f196,axiom,
index_69 = s(index_68),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp131) ).
fof(f197,axiom,
index_72 = rselect_tail(q18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp132) ).
fof(f198,axiom,
index_75 = s(index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp133) ).
fof(f199,axiom,
index_78 = rselect_tail(q1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp134) ).
fof(f200,axiom,
index_81 = s(index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp135) ).
fof(f201,axiom,
index_84 = rselect_tail(q19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp136) ).
fof(f202,axiom,
index_87 = s(index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp137) ).
fof(f203,axiom,
index_9 = rselect_tail(q9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
fof(f204,axiom,
index_90 = rselect_tail(q20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp139) ).
fof(f205,axiom,
index_93 = s(index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp140) ).
fof(f206,axiom,
index_95 = rselect_head(queue_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp141) ).
fof(f207,axiom,
index_96 = s(index_95),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp142) ).
fof(f208,axiom,
index_99 = rselect_tail(q21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp143) ).
fof(f209,axiom,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp144) ).
fof(f210,axiom,
queue_101 = rstore_seq(q21,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp145) ).
fof(f211,axiom,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp146) ).
fof(f212,axiom,
queue_107 = rstore_seq(q22,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp147) ).
fof(f213,axiom,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp148) ).
fof(f214,axiom,
queue_11 = rstore_seq(q9,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp149) ).
fof(f215,axiom,
queue_113 = rstore_seq(q23,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp150) ).
fof(f216,axiom,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp151) ).
fof(f217,axiom,
queue_118 = rstore_head(queue_115,index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
fof(f218,axiom,
queue_122 = rstore_seq(q24,earray_121),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp153) ).
fof(f219,axiom,
queue_124 = rstore_tail(queue_122,index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp154) ).
fof(f220,axiom,
queue_128 = rstore_seq(q25,earray_127),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp155) ).
fof(f221,axiom,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp156) ).
fof(f222,axiom,
queue_130 = rstore_tail(queue_128,index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp157) ).
fof(f223,axiom,
queue_134 = rstore_seq(q26,earray_133),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp158) ).
fof(f224,axiom,
queue_136 = rstore_tail(queue_134,index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp159) ).
fof(f225,axiom,
queue_139 = rstore_head(queue_136,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
fof(f226,axiom,
queue_143 = rstore_seq(q27,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp161) ).
fof(f227,axiom,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp162) ).
fof(f228,axiom,
queue_149 = rstore_seq(q28,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp163) ).
fof(f229,axiom,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp164) ).
fof(f230,axiom,
queue_155 = rstore_seq(q2,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp165) ).
fof(f231,axiom,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp166) ).
fof(f232,axiom,
queue_160 = rstore_head(queue_157,index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp167) ).
fof(f233,axiom,
queue_164 = rstore_seq(q29,earray_163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
fof(f234,axiom,
queue_166 = rstore_tail(queue_164,index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp169) ).
fof(f235,axiom,
queue_169 = rstore_head(queue_166,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp170) ).
fof(f236,axiom,
queue_17 = rstore_seq(q10,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp171) ).
fof(f237,axiom,
queue_173 = rstore_seq(q3,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
fof(f238,axiom,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp173) ).
fof(f239,axiom,
queue_179 = rstore_seq(q4,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp174) ).
fof(f240,axiom,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
fof(f241,axiom,
queue_185 = rstore_seq(q5,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp176) ).
fof(f242,axiom,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp177) ).
fof(f243,axiom,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp178) ).
fof(f244,axiom,
queue_190 = rstore_head(queue_187,index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp179) ).
fof(f245,axiom,
queue_194 = rstore_seq(q6,earray_193),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp180) ).
fof(f246,axiom,
queue_196 = rstore_tail(queue_194,index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp181) ).
fof(f247,axiom,
queue_200 = rstore_seq(q7,earray_199),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp182) ).
fof(f248,axiom,
queue_202 = rstore_tail(queue_200,index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp183) ).
fof(f249,axiom,
queue_206 = rstore_seq(q8,earray_205),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp184) ).
fof(f250,axiom,
queue_208 = rstore_tail(queue_206,index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp185) ).
fof(f251,axiom,
queue_211 = rstore_head(queue_208,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp186) ).
fof(f252,axiom,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f253,axiom,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp188) ).
fof(f254,axiom,
queue_28 = rstore_head(queue_25,index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp189) ).
fof(f255,axiom,
queue_32 = rstore_seq(q12,earray_31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp190) ).
fof(f256,axiom,
queue_34 = rstore_tail(queue_32,index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
fof(f257,axiom,
queue_38 = rstore_seq(q13,earray_37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp192) ).
fof(f258,axiom,
queue_40 = rstore_tail(queue_38,index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp193) ).
fof(f259,axiom,
queue_44 = rstore_seq(q14,earray_43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp194) ).
fof(f260,axiom,
queue_46 = rstore_tail(queue_44,index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
fof(f261,axiom,
queue_49 = rstore_head(queue_46,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp196) ).
fof(f262,axiom,
queue_5 = rstore_seq(q0,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp197) ).
fof(f263,axiom,
queue_53 = rstore_seq(q15,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
fof(f264,axiom,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
fof(f265,axiom,
queue_59 = rstore_seq(q16,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
fof(f266,axiom,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
fof(f267,axiom,
queue_65 = rstore_seq(q17,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
fof(f268,axiom,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f269,axiom,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp204) ).
fof(f270,axiom,
queue_70 = rstore_head(queue_67,index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f271,axiom,
queue_74 = rstore_seq(q18,earray_73),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp206) ).
fof(f272,axiom,
queue_76 = rstore_tail(queue_74,index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f273,axiom,
queue_80 = rstore_seq(q1,earray_79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
fof(f274,axiom,
queue_82 = rstore_tail(queue_80,index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f275,axiom,
queue_86 = rstore_seq(q19,earray_85),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
fof(f276,axiom,
queue_88 = rstore_tail(queue_86,index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
fof(f277,axiom,
queue_92 = rstore_seq(q20,earray_91),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f278,axiom,
queue_94 = rstore_tail(queue_92,index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f279,axiom,
queue_97 = rstore_head(queue_94,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
fof(f280,axiom,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f281,axiom,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
fof(f282,axiom,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f283,axiom,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp218) ).
fof(f284,axiom,
q12 = queue_28,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp219) ).
fof(f285,axiom,
q13 = queue_34,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f286,axiom,
q14 = queue_40,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f287,axiom,
q15 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
fof(f288,axiom,
q16 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
fof(f289,axiom,
q17 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f290,axiom,
q18 = queue_70,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f291,axiom,
q19 = queue_76,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
fof(f292,axiom,
q2 = queue_82,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f293,axiom,
q20 = queue_88,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
fof(f294,axiom,
q21 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f295,axiom,
q22 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
fof(f296,axiom,
q23 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
fof(f297,axiom,
q24 = queue_118,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f298,axiom,
q25 = queue_124,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f299,axiom,
q26 = queue_130,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
fof(f300,axiom,
q27 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
fof(f301,axiom,
q28 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f302,axiom,
q29 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f303,axiom,
q3 = queue_160,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
fof(f304,axiom,
q30 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f305,axiom,
q4 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
fof(f306,axiom,
q5 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f307,axiom,
q6 = queue_190,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
fof(f308,axiom,
q7 = queue_196,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
fof(f309,axiom,
q8 = queue_202,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f310,axiom,
q9 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f311,negated_conjecture,
elem_214 != e10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f312,plain,
e10 != elem_214,
inference(reorient_equations,[],[f311]) ).
fof(f313,plain,
earray_104 = rselect_seq(queue_103),
inference(definition_unfolding,[],[f67,f295]) ).
fof(f314,plain,
earray_110 = rselect_seq(queue_109),
inference(definition_unfolding,[],[f69,f296]) ).
fof(f315,plain,
earray_119 = rselect_seq(queue_118),
inference(definition_unfolding,[],[f71,f297]) ).
fof(f316,plain,
earray_125 = rselect_seq(queue_124),
inference(definition_unfolding,[],[f73,f298]) ).
fof(f317,plain,
earray_131 = rselect_seq(queue_130),
inference(definition_unfolding,[],[f75,f299]) ).
fof(f319,plain,
earray_140 = rselect_seq(queue_139),
inference(definition_unfolding,[],[f78,f300]) ).
fof(f320,plain,
earray_146 = rselect_seq(queue_145),
inference(definition_unfolding,[],[f80,f301]) ).
fof(f322,plain,
earray_161 = rselect_seq(queue_151),
inference(definition_unfolding,[],[f85,f302]) ).
fof(f329,plain,
earray_20 = rselect_seq(queue_19),
inference(definition_unfolding,[],[f98,f283]) ).
fof(f331,plain,
earray_212 = rselect_seq(queue_169),
inference(definition_unfolding,[],[f101,f304]) ).
fof(f332,plain,
earray_29 = rselect_seq(queue_28),
inference(definition_unfolding,[],[f103,f284]) ).
fof(f333,plain,
earray_35 = rselect_seq(queue_34),
inference(definition_unfolding,[],[f105,f285]) ).
fof(f334,plain,
earray_41 = rselect_seq(queue_40),
inference(definition_unfolding,[],[f108,f286]) ).
fof(f335,plain,
earray_50 = rselect_seq(queue_49),
inference(definition_unfolding,[],[f110,f287]) ).
fof(f336,plain,
earray_56 = rselect_seq(queue_55),
inference(definition_unfolding,[],[f112,f288]) ).
fof(f337,plain,
earray_62 = rselect_seq(queue_61),
inference(definition_unfolding,[],[f114,f289]) ).
fof(f338,plain,
earray_71 = rselect_seq(queue_70),
inference(definition_unfolding,[],[f116,f290]) ).
fof(f341,plain,
earray_83 = rselect_seq(queue_76),
inference(definition_unfolding,[],[f121,f291]) ).
fof(f342,plain,
earray_89 = rselect_seq(queue_88),
inference(definition_unfolding,[],[f123,f293]) ).
fof(f343,plain,
earray_98 = rselect_seq(queue_97),
inference(definition_unfolding,[],[f125,f294]) ).
fof(f344,plain,
index_105 = rselect_tail(queue_103),
inference(definition_unfolding,[],[f129,f295]) ).
fof(f345,plain,
index_111 = rselect_tail(queue_109),
inference(definition_unfolding,[],[f131,f296]) ).
fof(f346,plain,
index_120 = rselect_tail(queue_118),
inference(definition_unfolding,[],[f136,f297]) ).
fof(f347,plain,
index_126 = rselect_tail(queue_124),
inference(definition_unfolding,[],[f138,f298]) ).
fof(f348,plain,
index_132 = rselect_tail(queue_130),
inference(definition_unfolding,[],[f140,f299]) ).
fof(f349,plain,
index_141 = rselect_tail(queue_139),
inference(definition_unfolding,[],[f144,f300]) ).
fof(f350,plain,
index_147 = rselect_tail(queue_145),
inference(definition_unfolding,[],[f146,f301]) ).
fof(f351,plain,
index_15 = rselect_tail(queue_13),
inference(definition_unfolding,[],[f147,f282]) ).
fof(f352,plain,
index_153 = rselect_tail(queue_82),
inference(definition_unfolding,[],[f149,f292]) ).
fof(f353,plain,
index_162 = rselect_tail(queue_151),
inference(definition_unfolding,[],[f153,f302]) ).
fof(f354,plain,
index_171 = rselect_tail(queue_160),
inference(definition_unfolding,[],[f157,f303]) ).
fof(f355,plain,
index_177 = rselect_tail(queue_175),
inference(definition_unfolding,[],[f159,f305]) ).
fof(f356,plain,
index_183 = rselect_tail(queue_181),
inference(definition_unfolding,[],[f162,f306]) ).
fof(f357,plain,
index_192 = rselect_tail(queue_190),
inference(definition_unfolding,[],[f166,f307]) ).
fof(f358,plain,
index_198 = rselect_tail(queue_196),
inference(definition_unfolding,[],[f168,f308]) ).
fof(f359,plain,
index_204 = rselect_tail(queue_202),
inference(definition_unfolding,[],[f170,f309]) ).
fof(f360,plain,
index_21 = rselect_tail(queue_19),
inference(definition_unfolding,[],[f173,f283]) ).
fof(f361,plain,
index_213 = rselect_head(queue_169),
inference(definition_unfolding,[],[f175,f304]) ).
fof(f362,plain,
index_3 = rselect_tail(queue_1),
inference(definition_unfolding,[],[f179,f280]) ).
fof(f363,plain,
index_30 = rselect_tail(queue_28),
inference(definition_unfolding,[],[f180,f284]) ).
fof(f364,plain,
index_36 = rselect_tail(queue_34),
inference(definition_unfolding,[],[f182,f285]) ).
fof(f365,plain,
index_42 = rselect_tail(queue_40),
inference(definition_unfolding,[],[f184,f286]) ).
fof(f366,plain,
index_51 = rselect_tail(queue_49),
inference(definition_unfolding,[],[f188,f287]) ).
fof(f367,plain,
index_57 = rselect_tail(queue_55),
inference(definition_unfolding,[],[f190,f288]) ).
fof(f368,plain,
index_63 = rselect_tail(queue_61),
inference(definition_unfolding,[],[f193,f289]) ).
fof(f369,plain,
index_72 = rselect_tail(queue_70),
inference(definition_unfolding,[],[f197,f290]) ).
fof(f370,plain,
index_78 = rselect_tail(queue_7),
inference(definition_unfolding,[],[f199,f281]) ).
fof(f371,plain,
index_84 = rselect_tail(queue_76),
inference(definition_unfolding,[],[f201,f291]) ).
fof(f372,plain,
index_9 = rselect_tail(queue_211),
inference(definition_unfolding,[],[f203,f310]) ).
fof(f373,plain,
index_90 = rselect_tail(queue_88),
inference(definition_unfolding,[],[f204,f293]) ).
fof(f374,plain,
index_99 = rselect_tail(queue_97),
inference(definition_unfolding,[],[f208,f294]) ).
fof(f375,plain,
queue_101 = rstore_seq(queue_97,earray_100),
inference(definition_unfolding,[],[f210,f294]) ).
fof(f376,plain,
queue_107 = rstore_seq(queue_103,earray_106),
inference(definition_unfolding,[],[f212,f295]) ).
fof(f377,plain,
queue_11 = rstore_seq(queue_211,earray_10),
inference(definition_unfolding,[],[f214,f310]) ).
fof(f378,plain,
queue_113 = rstore_seq(queue_109,earray_112),
inference(definition_unfolding,[],[f215,f296]) ).
fof(f379,plain,
queue_122 = rstore_seq(queue_118,earray_121),
inference(definition_unfolding,[],[f218,f297]) ).
fof(f380,plain,
queue_128 = rstore_seq(queue_124,earray_127),
inference(definition_unfolding,[],[f220,f298]) ).
fof(f381,plain,
queue_134 = rstore_seq(queue_130,earray_133),
inference(definition_unfolding,[],[f223,f299]) ).
fof(f382,plain,
queue_143 = rstore_seq(queue_139,earray_142),
inference(definition_unfolding,[],[f226,f300]) ).
fof(f383,plain,
queue_149 = rstore_seq(queue_145,earray_148),
inference(definition_unfolding,[],[f228,f301]) ).
fof(f384,plain,
queue_155 = rstore_seq(queue_82,earray_154),
inference(definition_unfolding,[],[f230,f292]) ).
fof(f385,plain,
queue_164 = rstore_seq(queue_151,earray_163),
inference(definition_unfolding,[],[f233,f302]) ).
fof(f386,plain,
queue_17 = rstore_seq(queue_13,earray_16),
inference(definition_unfolding,[],[f236,f282]) ).
fof(f387,plain,
queue_173 = rstore_seq(queue_160,earray_172),
inference(definition_unfolding,[],[f237,f303]) ).
fof(f388,plain,
queue_179 = rstore_seq(queue_175,earray_178),
inference(definition_unfolding,[],[f239,f305]) ).
fof(f389,plain,
queue_185 = rstore_seq(queue_181,earray_184),
inference(definition_unfolding,[],[f241,f306]) ).
fof(f390,plain,
queue_194 = rstore_seq(queue_190,earray_193),
inference(definition_unfolding,[],[f245,f307]) ).
fof(f391,plain,
queue_200 = rstore_seq(queue_196,earray_199),
inference(definition_unfolding,[],[f247,f308]) ).
fof(f392,plain,
queue_206 = rstore_seq(queue_202,earray_205),
inference(definition_unfolding,[],[f249,f309]) ).
fof(f393,plain,
queue_23 = rstore_seq(queue_19,earray_22),
inference(definition_unfolding,[],[f252,f283]) ).
fof(f394,plain,
queue_32 = rstore_seq(queue_28,earray_31),
inference(definition_unfolding,[],[f255,f284]) ).
fof(f395,plain,
queue_38 = rstore_seq(queue_34,earray_37),
inference(definition_unfolding,[],[f257,f285]) ).
fof(f396,plain,
queue_44 = rstore_seq(queue_40,earray_43),
inference(definition_unfolding,[],[f259,f286]) ).
fof(f397,plain,
queue_5 = rstore_seq(queue_1,earray_4),
inference(definition_unfolding,[],[f262,f280]) ).
fof(f398,plain,
queue_53 = rstore_seq(queue_49,earray_52),
inference(definition_unfolding,[],[f263,f287]) ).
fof(f399,plain,
queue_59 = rstore_seq(queue_55,earray_58),
inference(definition_unfolding,[],[f265,f288]) ).
fof(f400,plain,
queue_65 = rstore_seq(queue_61,earray_64),
inference(definition_unfolding,[],[f267,f289]) ).
fof(f401,plain,
queue_74 = rstore_seq(queue_70,earray_73),
inference(definition_unfolding,[],[f271,f290]) ).
fof(f402,plain,
queue_80 = rstore_seq(queue_7,earray_79),
inference(definition_unfolding,[],[f273,f281]) ).
fof(f403,plain,
queue_86 = rstore_seq(queue_76,earray_85),
inference(definition_unfolding,[],[f275,f291]) ).
fof(f404,plain,
queue_92 = rstore_seq(queue_88,earray_91),
inference(definition_unfolding,[],[f277,f293]) ).
fof(f415,plain,
index_15 != index_18,
inference(superposition,[],[f64,f160]) ).
fof(f455,plain,
index_15 != s(index_18),
inference(superposition,[],[f63,f160]) ).
fof(f486,plain,
earray_106 = rselect_seq(queue_107),
inference(superposition,[],[f3,f376]) ).
fof(f487,plain,
earray_112 = rselect_seq(queue_113),
inference(superposition,[],[f3,f378]) ).
fof(f488,plain,
earray_121 = rselect_seq(queue_122),
inference(superposition,[],[f3,f379]) ).
fof(f489,plain,
earray_127 = rselect_seq(queue_128),
inference(superposition,[],[f3,f380]) ).
fof(f490,plain,
earray_16 = rselect_seq(queue_17),
inference(superposition,[],[f3,f386]) ).
fof(f491,plain,
earray_133 = rselect_seq(queue_134),
inference(superposition,[],[f3,f381]) ).
fof(f492,plain,
earray_142 = rselect_seq(queue_143),
inference(superposition,[],[f3,f382]) ).
fof(f493,plain,
earray_148 = rselect_seq(queue_149),
inference(superposition,[],[f3,f383]) ).
fof(f494,plain,
earray_163 = rselect_seq(queue_164),
inference(superposition,[],[f3,f385]) ).
fof(f498,plain,
earray_22 = rselect_seq(queue_23),
inference(superposition,[],[f3,f393]) ).
fof(f503,plain,
earray_31 = rselect_seq(queue_32),
inference(superposition,[],[f3,f394]) ).
fof(f504,plain,
earray_37 = rselect_seq(queue_38),
inference(superposition,[],[f3,f395]) ).
fof(f505,plain,
earray_43 = rselect_seq(queue_44),
inference(superposition,[],[f3,f396]) ).
fof(f506,plain,
earray_52 = rselect_seq(queue_53),
inference(superposition,[],[f3,f398]) ).
fof(f507,plain,
earray_58 = rselect_seq(queue_59),
inference(superposition,[],[f3,f399]) ).
fof(f508,plain,
earray_64 = rselect_seq(queue_65),
inference(superposition,[],[f3,f400]) ).
fof(f510,plain,
earray_73 = rselect_seq(queue_74),
inference(superposition,[],[f3,f401]) ).
fof(f511,plain,
earray_85 = rselect_seq(queue_86),
inference(superposition,[],[f3,f403]) ).
fof(f513,plain,
earray_91 = rselect_seq(queue_92),
inference(superposition,[],[f3,f404]) ).
fof(f514,plain,
earray_100 = rselect_seq(queue_101),
inference(superposition,[],[f3,f375]) ).
fof(f515,plain,
index_0 = rselect_head(queue_1),
inference(superposition,[],[f4,f209]) ).
fof(f516,plain,
index_117 = rselect_head(queue_118),
inference(superposition,[],[f4,f217]) ).
fof(f517,plain,
index_138 = rselect_head(queue_139),
inference(superposition,[],[f4,f225]) ).
fof(f518,plain,
index_159 = rselect_head(queue_160),
inference(superposition,[],[f4,f232]) ).
fof(f519,plain,
index_168 = rselect_head(queue_169),
inference(superposition,[],[f4,f235]) ).
fof(f520,plain,
index_189 = rselect_head(queue_190),
inference(superposition,[],[f4,f244]) ).
fof(f521,plain,
index_210 = rselect_head(queue_211),
inference(superposition,[],[f4,f251]) ).
fof(f522,plain,
index_27 = rselect_head(queue_28),
inference(superposition,[],[f4,f254]) ).
fof(f523,plain,
index_48 = rselect_head(queue_49),
inference(superposition,[],[f4,f261]) ).
fof(f524,plain,
index_69 = rselect_head(queue_70),
inference(superposition,[],[f4,f270]) ).
fof(f525,plain,
index_96 = rselect_head(queue_97),
inference(superposition,[],[f4,f279]) ).
fof(f526,plain,
index_213 = index_168,
inference(forward_demodulation,[],[f519,f361]) ).
fof(f529,plain,
index_102 = rselect_tail(queue_103),
inference(superposition,[],[f5,f211]) ).
fof(f530,plain,
index_108 = rselect_tail(queue_109),
inference(superposition,[],[f5,f213]) ).
fof(f531,plain,
index_12 = rselect_tail(queue_13),
inference(superposition,[],[f5,f221]) ).
fof(f532,plain,
index_114 = rselect_tail(queue_115),
inference(superposition,[],[f5,f216]) ).
fof(f533,plain,
index_123 = rselect_tail(queue_124),
inference(superposition,[],[f5,f219]) ).
fof(f534,plain,
index_129 = rselect_tail(queue_130),
inference(superposition,[],[f5,f222]) ).
fof(f535,plain,
index_135 = rselect_tail(queue_136),
inference(superposition,[],[f5,f224]) ).
fof(f536,plain,
index_144 = rselect_tail(queue_145),
inference(superposition,[],[f5,f227]) ).
fof(f537,plain,
index_150 = rselect_tail(queue_151),
inference(superposition,[],[f5,f229]) ).
fof(f538,plain,
index_156 = rselect_tail(queue_157),
inference(superposition,[],[f5,f231]) ).
fof(f540,plain,
index_18 = rselect_tail(queue_19),
inference(superposition,[],[f5,f243]) ).
fof(f541,plain,
index_174 = rselect_tail(queue_175),
inference(superposition,[],[f5,f238]) ).
fof(f542,plain,
index_180 = rselect_tail(queue_181),
inference(superposition,[],[f5,f240]) ).
fof(f543,plain,
index_186 = rselect_tail(queue_187),
inference(superposition,[],[f5,f242]) ).
fof(f544,plain,
index_195 = rselect_tail(queue_196),
inference(superposition,[],[f5,f246]) ).
fof(f545,plain,
index_201 = rselect_tail(queue_202),
inference(superposition,[],[f5,f248]) ).
fof(f546,plain,
index_207 = rselect_tail(queue_208),
inference(superposition,[],[f5,f250]) ).
fof(f547,plain,
index_24 = rselect_tail(queue_25),
inference(superposition,[],[f5,f253]) ).
fof(f548,plain,
index_33 = rselect_tail(queue_34),
inference(superposition,[],[f5,f256]) ).
fof(f549,plain,
index_39 = rselect_tail(queue_40),
inference(superposition,[],[f5,f258]) ).
fof(f550,plain,
index_45 = rselect_tail(queue_46),
inference(superposition,[],[f5,f260]) ).
fof(f551,plain,
index_6 = rselect_tail(queue_7),
inference(superposition,[],[f5,f269]) ).
fof(f552,plain,
index_54 = rselect_tail(queue_55),
inference(superposition,[],[f5,f264]) ).
fof(f553,plain,
index_60 = rselect_tail(queue_61),
inference(superposition,[],[f5,f266]) ).
fof(f554,plain,
index_66 = rselect_tail(queue_67),
inference(superposition,[],[f5,f268]) ).
fof(f555,plain,
index_75 = rselect_tail(queue_76),
inference(superposition,[],[f5,f272]) ).
fof(f556,plain,
index_81 = rselect_tail(queue_82),
inference(superposition,[],[f5,f274]) ).
fof(f557,plain,
index_87 = rselect_tail(queue_88),
inference(superposition,[],[f5,f276]) ).
fof(f558,plain,
index_93 = rselect_tail(queue_94),
inference(superposition,[],[f5,f278]) ).
fof(f559,plain,
index_90 = index_87,
inference(forward_demodulation,[],[f557,f373]) ).
fof(f560,plain,
index_153 = index_81,
inference(forward_demodulation,[],[f556,f352]) ).
fof(f561,plain,
index_84 = index_75,
inference(forward_demodulation,[],[f555,f371]) ).
fof(f562,plain,
index_63 = index_60,
inference(forward_demodulation,[],[f553,f368]) ).
fof(f563,plain,
index_57 = index_54,
inference(forward_demodulation,[],[f552,f367]) ).
fof(f564,plain,
index_78 = index_6,
inference(forward_demodulation,[],[f551,f370]) ).
fof(f565,plain,
index_42 = index_39,
inference(forward_demodulation,[],[f549,f365]) ).
fof(f566,plain,
index_36 = index_33,
inference(forward_demodulation,[],[f548,f364]) ).
fof(f567,plain,
index_204 = index_201,
inference(forward_demodulation,[],[f545,f359]) ).
fof(f568,plain,
index_198 = index_195,
inference(forward_demodulation,[],[f544,f358]) ).
fof(f569,plain,
index_183 = index_180,
inference(forward_demodulation,[],[f542,f356]) ).
fof(f570,plain,
index_177 = index_174,
inference(forward_demodulation,[],[f541,f355]) ).
fof(f571,plain,
index_21 = index_18,
inference(forward_demodulation,[],[f540,f360]) ).
fof(f572,plain,
index_162 = index_150,
inference(forward_demodulation,[],[f537,f353]) ).
fof(f573,plain,
index_147 = index_144,
inference(forward_demodulation,[],[f536,f350]) ).
fof(f574,plain,
index_132 = index_129,
inference(forward_demodulation,[],[f534,f348]) ).
fof(f575,plain,
index_126 = index_123,
inference(forward_demodulation,[],[f533,f347]) ).
fof(f576,plain,
index_15 = index_12,
inference(forward_demodulation,[],[f531,f351]) ).
fof(f577,plain,
index_111 = index_108,
inference(forward_demodulation,[],[f530,f345]) ).
fof(f578,plain,
index_105 = index_102,
inference(forward_demodulation,[],[f529,f344]) ).
fof(f591,plain,
index_15 != s(s(index_18)),
inference(superposition,[],[f62,f160]) ).
fof(f627,plain,
rselect_seq(queue_118) = rselect_seq(queue_115),
inference(superposition,[],[f6,f217]) ).
fof(f628,plain,
rselect_seq(queue_139) = rselect_seq(queue_136),
inference(superposition,[],[f6,f225]) ).
fof(f630,plain,
rselect_seq(queue_169) = rselect_seq(queue_166),
inference(superposition,[],[f6,f235]) ).
fof(f633,plain,
rselect_seq(queue_28) = rselect_seq(queue_25),
inference(superposition,[],[f6,f254]) ).
fof(f634,plain,
rselect_seq(queue_49) = rselect_seq(queue_46),
inference(superposition,[],[f6,f261]) ).
fof(f635,plain,
rselect_seq(queue_70) = rselect_seq(queue_67),
inference(superposition,[],[f6,f270]) ).
fof(f636,plain,
rselect_seq(queue_97) = rselect_seq(queue_94),
inference(superposition,[],[f6,f279]) ).
fof(f637,plain,
earray_98 = rselect_seq(queue_94),
inference(forward_demodulation,[],[f636,f343]) ).
fof(f638,plain,
earray_71 = rselect_seq(queue_67),
inference(forward_demodulation,[],[f635,f338]) ).
fof(f639,plain,
earray_50 = rselect_seq(queue_46),
inference(forward_demodulation,[],[f634,f335]) ).
fof(f640,plain,
earray_29 = rselect_seq(queue_25),
inference(forward_demodulation,[],[f633,f332]) ).
fof(f643,plain,
earray_212 = rselect_seq(queue_166),
inference(forward_demodulation,[],[f630,f331]) ).
fof(f645,plain,
earray_140 = rselect_seq(queue_136),
inference(forward_demodulation,[],[f628,f319]) ).
fof(f646,plain,
earray_119 = rselect_seq(queue_115),
inference(forward_demodulation,[],[f627,f315]) ).
fof(f648,plain,
rselect_seq(queue_103) = rselect_seq(queue_101),
inference(superposition,[],[f8,f211]) ).
fof(f649,plain,
rselect_seq(queue_109) = rselect_seq(queue_107),
inference(superposition,[],[f8,f213]) ).
fof(f651,plain,
rselect_seq(queue_113) = rselect_seq(queue_115),
inference(superposition,[],[f8,f216]) ).
fof(f652,plain,
rselect_seq(queue_124) = rselect_seq(queue_122),
inference(superposition,[],[f8,f219]) ).
fof(f653,plain,
rselect_seq(queue_130) = rselect_seq(queue_128),
inference(superposition,[],[f8,f222]) ).
fof(f654,plain,
rselect_seq(queue_134) = rselect_seq(queue_136),
inference(superposition,[],[f8,f224]) ).
fof(f655,plain,
rselect_seq(queue_145) = rselect_seq(queue_143),
inference(superposition,[],[f8,f227]) ).
fof(f656,plain,
rselect_seq(queue_151) = rselect_seq(queue_149),
inference(superposition,[],[f8,f229]) ).
fof(f658,plain,
rselect_seq(queue_164) = rselect_seq(queue_166),
inference(superposition,[],[f8,f234]) ).
fof(f659,plain,
rselect_seq(queue_19) = rselect_seq(queue_17),
inference(superposition,[],[f8,f243]) ).
fof(f666,plain,
rselect_seq(queue_23) = rselect_seq(queue_25),
inference(superposition,[],[f8,f253]) ).
fof(f667,plain,
rselect_seq(queue_34) = rselect_seq(queue_32),
inference(superposition,[],[f8,f256]) ).
fof(f668,plain,
rselect_seq(queue_40) = rselect_seq(queue_38),
inference(superposition,[],[f8,f258]) ).
fof(f669,plain,
rselect_seq(queue_44) = rselect_seq(queue_46),
inference(superposition,[],[f8,f260]) ).
fof(f671,plain,
rselect_seq(queue_55) = rselect_seq(queue_53),
inference(superposition,[],[f8,f264]) ).
fof(f672,plain,
rselect_seq(queue_61) = rselect_seq(queue_59),
inference(superposition,[],[f8,f266]) ).
fof(f673,plain,
rselect_seq(queue_65) = rselect_seq(queue_67),
inference(superposition,[],[f8,f268]) ).
fof(f674,plain,
rselect_seq(queue_76) = rselect_seq(queue_74),
inference(superposition,[],[f8,f272]) ).
fof(f676,plain,
rselect_seq(queue_88) = rselect_seq(queue_86),
inference(superposition,[],[f8,f276]) ).
fof(f677,plain,
rselect_seq(queue_92) = rselect_seq(queue_94),
inference(superposition,[],[f8,f278]) ).
fof(f678,plain,
earray_89 = rselect_seq(queue_86),
inference(forward_demodulation,[],[f676,f342]) ).
fof(f680,plain,
earray_83 = rselect_seq(queue_74),
inference(forward_demodulation,[],[f674,f341]) ).
fof(f681,plain,
earray_62 = rselect_seq(queue_59),
inference(forward_demodulation,[],[f672,f337]) ).
fof(f682,plain,
earray_56 = rselect_seq(queue_53),
inference(forward_demodulation,[],[f671,f336]) ).
fof(f684,plain,
earray_41 = rselect_seq(queue_38),
inference(forward_demodulation,[],[f668,f334]) ).
fof(f685,plain,
earray_35 = rselect_seq(queue_32),
inference(forward_demodulation,[],[f667,f333]) ).
fof(f690,plain,
earray_20 = rselect_seq(queue_17),
inference(forward_demodulation,[],[f659,f329]) ).
fof(f691,plain,
earray_161 = rselect_seq(queue_149),
inference(forward_demodulation,[],[f656,f322]) ).
fof(f692,plain,
earray_146 = rselect_seq(queue_143),
inference(forward_demodulation,[],[f655,f320]) ).
fof(f693,plain,
earray_131 = rselect_seq(queue_128),
inference(forward_demodulation,[],[f653,f317]) ).
fof(f694,plain,
earray_125 = rselect_seq(queue_122),
inference(forward_demodulation,[],[f652,f316]) ).
fof(f696,plain,
earray_110 = rselect_seq(queue_107),
inference(forward_demodulation,[],[f649,f314]) ).
fof(f697,plain,
earray_104 = rselect_seq(queue_101),
inference(forward_demodulation,[],[f648,f313]) ).
fof(f698,plain,
rselect_head(queue_101) = rselect_head(queue_103),
inference(superposition,[],[f9,f211]) ).
fof(f699,plain,
rselect_head(queue_107) = rselect_head(queue_109),
inference(superposition,[],[f9,f213]) ).
fof(f700,plain,
rselect_head(queue_11) = rselect_head(queue_13),
inference(superposition,[],[f9,f221]) ).
fof(f701,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(superposition,[],[f9,f216]) ).
fof(f702,plain,
rselect_head(queue_122) = rselect_head(queue_124),
inference(superposition,[],[f9,f219]) ).
fof(f703,plain,
rselect_head(queue_128) = rselect_head(queue_130),
inference(superposition,[],[f9,f222]) ).
fof(f704,plain,
rselect_head(queue_136) = rselect_head(queue_134),
inference(superposition,[],[f9,f224]) ).
fof(f705,plain,
rselect_head(queue_143) = rselect_head(queue_145),
inference(superposition,[],[f9,f227]) ).
fof(f706,plain,
rselect_head(queue_149) = rselect_head(queue_151),
inference(superposition,[],[f9,f229]) ).
fof(f707,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(superposition,[],[f9,f231]) ).
fof(f708,plain,
rselect_head(queue_166) = rselect_head(queue_164),
inference(superposition,[],[f9,f234]) ).
fof(f709,plain,
rselect_head(queue_17) = rselect_head(queue_19),
inference(superposition,[],[f9,f243]) ).
fof(f710,plain,
rselect_head(queue_173) = rselect_head(queue_175),
inference(superposition,[],[f9,f238]) ).
fof(f711,plain,
rselect_head(queue_179) = rselect_head(queue_181),
inference(superposition,[],[f9,f240]) ).
fof(f712,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(superposition,[],[f9,f242]) ).
fof(f713,plain,
rselect_head(queue_194) = rselect_head(queue_196),
inference(superposition,[],[f9,f246]) ).
fof(f714,plain,
rselect_head(queue_200) = rselect_head(queue_202),
inference(superposition,[],[f9,f248]) ).
fof(f715,plain,
rselect_head(queue_208) = rselect_head(queue_206),
inference(superposition,[],[f9,f250]) ).
fof(f716,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(superposition,[],[f9,f253]) ).
fof(f717,plain,
rselect_head(queue_32) = rselect_head(queue_34),
inference(superposition,[],[f9,f256]) ).
fof(f718,plain,
rselect_head(queue_38) = rselect_head(queue_40),
inference(superposition,[],[f9,f258]) ).
fof(f719,plain,
rselect_head(queue_46) = rselect_head(queue_44),
inference(superposition,[],[f9,f260]) ).
fof(f720,plain,
rselect_head(queue_5) = rselect_head(queue_7),
inference(superposition,[],[f9,f269]) ).
fof(f721,plain,
rselect_head(queue_53) = rselect_head(queue_55),
inference(superposition,[],[f9,f264]) ).
fof(f722,plain,
rselect_head(queue_59) = rselect_head(queue_61),
inference(superposition,[],[f9,f266]) ).
fof(f723,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(superposition,[],[f9,f268]) ).
fof(f724,plain,
rselect_head(queue_74) = rselect_head(queue_76),
inference(superposition,[],[f9,f272]) ).
fof(f725,plain,
rselect_head(queue_80) = rselect_head(queue_82),
inference(superposition,[],[f9,f274]) ).
fof(f726,plain,
rselect_head(queue_86) = rselect_head(queue_88),
inference(superposition,[],[f9,f276]) ).
fof(f727,plain,
rselect_head(queue_94) = rselect_head(queue_92),
inference(superposition,[],[f9,f278]) ).
fof(f728,plain,
index_95 = rselect_head(queue_92),
inference(forward_demodulation,[],[f727,f206]) ).
fof(f729,plain,
index_68 = rselect_head(queue_65),
inference(forward_demodulation,[],[f723,f195]) ).
fof(f730,plain,
index_47 = rselect_head(queue_44),
inference(forward_demodulation,[],[f719,f186]) ).
fof(f731,plain,
index_26 = rselect_head(queue_23),
inference(forward_demodulation,[],[f716,f177]) ).
fof(f732,plain,
index_209 = rselect_head(queue_206),
inference(forward_demodulation,[],[f715,f172]) ).
fof(f733,plain,
index_188 = rselect_head(queue_185),
inference(forward_demodulation,[],[f712,f164]) ).
fof(f734,plain,
index_167 = rselect_head(queue_164),
inference(forward_demodulation,[],[f708,f155]) ).
fof(f735,plain,
index_158 = rselect_head(queue_155),
inference(forward_demodulation,[],[f707,f151]) ).
fof(f736,plain,
index_137 = rselect_head(queue_134),
inference(forward_demodulation,[],[f704,f142]) ).
fof(f737,plain,
index_116 = rselect_head(queue_113),
inference(forward_demodulation,[],[f701,f133]) ).
fof(f738,plain,
rselect_head(queue_1) = rselect_head(queue_5),
inference(superposition,[],[f11,f397]) ).
fof(f739,plain,
rselect_head(queue_103) = rselect_head(queue_107),
inference(superposition,[],[f11,f376]) ).
fof(f740,plain,
rselect_head(queue_109) = rselect_head(queue_113),
inference(superposition,[],[f11,f378]) ).
fof(f741,plain,
rselect_head(queue_118) = rselect_head(queue_122),
inference(superposition,[],[f11,f379]) ).
fof(f742,plain,
rselect_head(queue_124) = rselect_head(queue_128),
inference(superposition,[],[f11,f380]) ).
fof(f743,plain,
rselect_head(queue_13) = rselect_head(queue_17),
inference(superposition,[],[f11,f386]) ).
fof(f744,plain,
rselect_head(queue_130) = rselect_head(queue_134),
inference(superposition,[],[f11,f381]) ).
fof(f745,plain,
rselect_head(queue_139) = rselect_head(queue_143),
inference(superposition,[],[f11,f382]) ).
fof(f746,plain,
rselect_head(queue_145) = rselect_head(queue_149),
inference(superposition,[],[f11,f383]) ).
fof(f747,plain,
rselect_head(queue_151) = rselect_head(queue_164),
inference(superposition,[],[f11,f385]) ).
fof(f748,plain,
rselect_head(queue_160) = rselect_head(queue_173),
inference(superposition,[],[f11,f387]) ).
fof(f749,plain,
rselect_head(queue_175) = rselect_head(queue_179),
inference(superposition,[],[f11,f388]) ).
fof(f750,plain,
rselect_head(queue_181) = rselect_head(queue_185),
inference(superposition,[],[f11,f389]) ).
fof(f751,plain,
rselect_head(queue_19) = rselect_head(queue_23),
inference(superposition,[],[f11,f393]) ).
fof(f752,plain,
rselect_head(queue_190) = rselect_head(queue_194),
inference(superposition,[],[f11,f390]) ).
fof(f753,plain,
rselect_head(queue_196) = rselect_head(queue_200),
inference(superposition,[],[f11,f391]) ).
fof(f754,plain,
rselect_head(queue_202) = rselect_head(queue_206),
inference(superposition,[],[f11,f392]) ).
fof(f755,plain,
rselect_head(queue_211) = rselect_head(queue_11),
inference(superposition,[],[f11,f377]) ).
fof(f756,plain,
rselect_head(queue_28) = rselect_head(queue_32),
inference(superposition,[],[f11,f394]) ).
fof(f757,plain,
rselect_head(queue_34) = rselect_head(queue_38),
inference(superposition,[],[f11,f395]) ).
fof(f758,plain,
rselect_head(queue_40) = rselect_head(queue_44),
inference(superposition,[],[f11,f396]) ).
fof(f759,plain,
rselect_head(queue_49) = rselect_head(queue_53),
inference(superposition,[],[f11,f398]) ).
fof(f760,plain,
rselect_head(queue_55) = rselect_head(queue_59),
inference(superposition,[],[f11,f399]) ).
fof(f761,plain,
rselect_head(queue_61) = rselect_head(queue_65),
inference(superposition,[],[f11,f400]) ).
fof(f762,plain,
rselect_head(queue_7) = rselect_head(queue_80),
inference(superposition,[],[f11,f402]) ).
fof(f763,plain,
rselect_head(queue_70) = rselect_head(queue_74),
inference(superposition,[],[f11,f401]) ).
fof(f764,plain,
rselect_head(queue_76) = rselect_head(queue_86),
inference(superposition,[],[f11,f403]) ).
fof(f765,plain,
rselect_head(queue_155) = rselect_head(queue_82),
inference(superposition,[],[f11,f384]) ).
fof(f766,plain,
rselect_head(queue_88) = rselect_head(queue_92),
inference(superposition,[],[f11,f404]) ).
fof(f767,plain,
rselect_head(queue_97) = rselect_head(queue_101),
inference(superposition,[],[f11,f375]) ).
fof(f828,plain,
rselect_tail(q) = rselect_tail(queue_1),
inference(superposition,[],[f14,f209]) ).
fof(f829,plain,
rselect_tail(queue_118) = rselect_tail(queue_115),
inference(superposition,[],[f14,f217]) ).
fof(f830,plain,
rselect_tail(queue_139) = rselect_tail(queue_136),
inference(superposition,[],[f14,f225]) ).
fof(f831,plain,
rselect_tail(queue_160) = rselect_tail(queue_157),
inference(superposition,[],[f14,f232]) ).
fof(f833,plain,
rselect_tail(queue_190) = rselect_tail(queue_187),
inference(superposition,[],[f14,f244]) ).
fof(f834,plain,
rselect_tail(queue_211) = rselect_tail(queue_208),
inference(superposition,[],[f14,f251]) ).
fof(f835,plain,
rselect_tail(queue_28) = rselect_tail(queue_25),
inference(superposition,[],[f14,f254]) ).
fof(f836,plain,
rselect_tail(queue_49) = rselect_tail(queue_46),
inference(superposition,[],[f14,f261]) ).
fof(f837,plain,
rselect_tail(queue_70) = rselect_tail(queue_67),
inference(superposition,[],[f14,f270]) ).
fof(f838,plain,
rselect_tail(queue_97) = rselect_tail(queue_94),
inference(superposition,[],[f14,f279]) ).
fof(f839,plain,
index_99 = rselect_tail(queue_94),
inference(forward_demodulation,[],[f838,f374]) ).
fof(f840,plain,
index_72 = rselect_tail(queue_67),
inference(forward_demodulation,[],[f837,f369]) ).
fof(f841,plain,
index_51 = rselect_tail(queue_46),
inference(forward_demodulation,[],[f836,f366]) ).
fof(f842,plain,
index_30 = rselect_tail(queue_25),
inference(forward_demodulation,[],[f835,f363]) ).
fof(f843,plain,
index_9 = rselect_tail(queue_208),
inference(forward_demodulation,[],[f834,f372]) ).
fof(f844,plain,
index_192 = rselect_tail(queue_187),
inference(forward_demodulation,[],[f833,f357]) ).
fof(f845,plain,
index_171 = rselect_tail(queue_157),
inference(forward_demodulation,[],[f831,f354]) ).
fof(f846,plain,
index_141 = rselect_tail(queue_136),
inference(forward_demodulation,[],[f830,f349]) ).
fof(f847,plain,
index_120 = rselect_tail(queue_115),
inference(forward_demodulation,[],[f829,f346]) ).
fof(f848,plain,
index_3 = rselect_tail(q),
inference(forward_demodulation,[],[f828,f362]) ).
fof(f859,plain,
index_15 != s(s(s(index_18))),
inference(superposition,[],[f61,f160]) ).
fof(f903,plain,
e10 = select(earray_16,index_15),
inference(superposition,[],[f1,f84]) ).
fof(f936,plain,
index_15 != s(s(s(s(index_18)))),
inference(superposition,[],[f60,f160]) ).
fof(f985,plain,
index_15 != s(s(s(s(s(index_18))))),
inference(superposition,[],[f59,f160]) ).
fof(f1034,plain,
index_15 != s(s(s(s(s(s(index_18)))))),
inference(superposition,[],[f58,f160]) ).
fof(f1083,plain,
index_15 != s(s(s(s(s(s(s(index_18))))))),
inference(superposition,[],[f57,f160]) ).
fof(f1138,plain,
index_15 != s(s(s(s(s(s(s(s(index_18)))))))),
inference(superposition,[],[f56,f160]) ).
fof(f1188,plain,
! [X0] :
( select(earray_98,X0) = select(earray_100,X0)
| index_99 = X0 ),
inference(superposition,[],[f2,f66]) ).
fof(f1189,plain,
! [X0] :
( select(earray_104,X0) = select(earray_106,X0)
| index_105 = X0 ),
inference(superposition,[],[f2,f68]) ).
fof(f1190,plain,
! [X0] :
( select(earray_110,X0) = select(earray_112,X0)
| index_111 = X0 ),
inference(superposition,[],[f2,f70]) ).
fof(f1191,plain,
! [X0] :
( select(earray_119,X0) = select(earray_121,X0)
| index_120 = X0 ),
inference(superposition,[],[f2,f72]) ).
fof(f1192,plain,
! [X0] :
( select(earray_125,X0) = select(earray_127,X0)
| index_126 = X0 ),
inference(superposition,[],[f2,f74]) ).
fof(f1193,plain,
! [X0] :
( select(earray_131,X0) = select(earray_133,X0)
| index_132 = X0 ),
inference(superposition,[],[f2,f76]) ).
fof(f1195,plain,
! [X0] :
( select(earray_140,X0) = select(earray_142,X0)
| index_141 = X0 ),
inference(superposition,[],[f2,f79]) ).
fof(f1196,plain,
! [X0] :
( select(earray_146,X0) = select(earray_148,X0)
| index_147 = X0 ),
inference(superposition,[],[f2,f81]) ).
fof(f1198,plain,
! [X0] :
( select(earray_161,X0) = select(earray_163,X0)
| index_162 = X0 ),
inference(superposition,[],[f2,f86]) ).
fof(f1205,plain,
! [X0] :
( select(earray_20,X0) = select(earray_22,X0)
| index_21 = X0 ),
inference(superposition,[],[f2,f102]) ).
fof(f1207,plain,
! [X0] :
( select(earray_29,X0) = select(earray_31,X0)
| index_30 = X0 ),
inference(superposition,[],[f2,f104]) ).
fof(f1208,plain,
! [X0] :
( select(earray_35,X0) = select(earray_37,X0)
| index_36 = X0 ),
inference(superposition,[],[f2,f106]) ).
fof(f1209,plain,
! [X0] :
( select(earray_41,X0) = select(earray_43,X0)
| index_42 = X0 ),
inference(superposition,[],[f2,f109]) ).
fof(f1210,plain,
! [X0] :
( select(earray_50,X0) = select(earray_52,X0)
| index_51 = X0 ),
inference(superposition,[],[f2,f111]) ).
fof(f1211,plain,
! [X0] :
( select(earray_56,X0) = select(earray_58,X0)
| index_57 = X0 ),
inference(superposition,[],[f2,f113]) ).
fof(f1212,plain,
! [X0] :
( select(earray_62,X0) = select(earray_64,X0)
| index_63 = X0 ),
inference(superposition,[],[f2,f115]) ).
fof(f1213,plain,
! [X0] :
( select(earray_71,X0) = select(earray_73,X0)
| index_72 = X0 ),
inference(superposition,[],[f2,f117]) ).
fof(f1215,plain,
! [X0] :
( select(earray_83,X0) = select(earray_85,X0)
| index_84 = X0 ),
inference(superposition,[],[f2,f122]) ).
fof(f1216,plain,
! [X0] :
( select(earray_89,X0) = select(earray_91,X0)
| index_90 = X0 ),
inference(superposition,[],[f2,f124]) ).
fof(f1229,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_18))))))))),
inference(superposition,[],[f55,f160]) ).
fof(f1294,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_18)))))))))),
inference(superposition,[],[f54,f160]) ).
fof(f1361,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))),
inference(superposition,[],[f53,f160]) ).
fof(f1428,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))),
inference(superposition,[],[f52,f160]) ).
fof(f1498,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))),
inference(superposition,[],[f51,f160]) ).
fof(f1569,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))),
inference(superposition,[],[f50,f160]) ).
fof(f1640,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))),
inference(superposition,[],[f49,f160]) ).
fof(f1707,plain,
index_15 != s(index_21),
inference(superposition,[],[f455,f571]) ).
fof(f1708,plain,
index_15 != index_21,
inference(superposition,[],[f415,f571]) ).
fof(f1720,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))),
inference(superposition,[],[f48,f160]) ).
fof(f1763,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))),
inference(forward_demodulation,[],[f1720,f571]) ).
fof(f1776,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))),
inference(forward_demodulation,[],[f1763,f176]) ).
fof(f1805,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))))),
inference(superposition,[],[f47,f160]) ).
fof(f1848,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))),
inference(forward_demodulation,[],[f1805,f571]) ).
fof(f1863,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))),
inference(forward_demodulation,[],[f1848,f176]) ).
fof(f1890,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))))),
inference(superposition,[],[f46,f160]) ).
fof(f1933,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))))),
inference(forward_demodulation,[],[f1890,f571]) ).
fof(f1948,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))))),
inference(forward_demodulation,[],[f1933,f176]) ).
fof(f5051,plain,
earray_85 = earray_89,
inference(forward_demodulation,[],[f678,f511]) ).
fof(f5055,plain,
earray_73 = earray_83,
inference(forward_demodulation,[],[f680,f510]) ).
fof(f5058,plain,
earray_58 = earray_62,
inference(forward_demodulation,[],[f681,f507]) ).
fof(f5060,plain,
earray_52 = earray_56,
inference(forward_demodulation,[],[f682,f506]) ).
fof(f5065,plain,
earray_37 = earray_41,
inference(forward_demodulation,[],[f684,f504]) ).
fof(f5067,plain,
earray_31 = earray_35,
inference(forward_demodulation,[],[f685,f503]) ).
fof(f5077,plain,
earray_16 = earray_20,
inference(forward_demodulation,[],[f690,f490]) ).
fof(f5079,plain,
earray_148 = earray_161,
inference(forward_demodulation,[],[f691,f493]) ).
fof(f5081,plain,
earray_142 = earray_146,
inference(forward_demodulation,[],[f692,f492]) ).
fof(f5083,plain,
earray_127 = earray_131,
inference(forward_demodulation,[],[f693,f489]) ).
fof(f5085,plain,
earray_121 = earray_125,
inference(forward_demodulation,[],[f694,f488]) ).
fof(f5089,plain,
earray_106 = earray_110,
inference(forward_demodulation,[],[f696,f486]) ).
fof(f5091,plain,
earray_100 = earray_104,
inference(forward_demodulation,[],[f697,f514]) ).
fof(f5093,plain,
index_99 = index_93,
inference(superposition,[],[f839,f558]) ).
fof(f5099,plain,
index_72 = index_66,
inference(superposition,[],[f840,f554]) ).
fof(f5101,plain,
index_51 = index_45,
inference(superposition,[],[f841,f550]) ).
fof(f5103,plain,
index_30 = index_24,
inference(superposition,[],[f842,f547]) ).
fof(f5105,plain,
index_9 = index_207,
inference(superposition,[],[f843,f546]) ).
fof(f5107,plain,
index_192 = index_186,
inference(superposition,[],[f844,f543]) ).
fof(f5109,plain,
index_171 = index_156,
inference(superposition,[],[f845,f538]) ).
fof(f5111,plain,
index_141 = index_135,
inference(superposition,[],[f846,f535]) ).
fof(f5116,plain,
index_120 = index_114,
inference(superposition,[],[f847,f532]) ).
fof(f5118,plain,
index_3 = index_0,
inference(superposition,[],[f848,f127]) ).
fof(f5186,plain,
index_15 != s(s(index_21)),
inference(forward_demodulation,[],[f591,f571]) ).
fof(f5187,plain,
index_15 != s(index_24),
inference(forward_demodulation,[],[f5186,f176]) ).
fof(f5188,plain,
index_15 != s(index_30),
inference(forward_demodulation,[],[f5187,f5103]) ).
fof(f5189,plain,
index_15 != index_33,
inference(superposition,[],[f5188,f181]) ).
fof(f5235,plain,
index_15 != index_36,
inference(superposition,[],[f5189,f566]) ).
fof(f5286,plain,
earray_119 = rselect_seq(queue_113),
inference(forward_demodulation,[],[f651,f646]) ).
fof(f5287,plain,
earray_112 = earray_119,
inference(forward_demodulation,[],[f5286,f487]) ).
fof(f5291,plain,
earray_140 = rselect_seq(queue_134),
inference(forward_demodulation,[],[f654,f645]) ).
fof(f5292,plain,
earray_133 = earray_140,
inference(forward_demodulation,[],[f5291,f491]) ).
fof(f5297,plain,
earray_212 = rselect_seq(queue_164),
inference(forward_demodulation,[],[f658,f643]) ).
fof(f5298,plain,
earray_163 = earray_212,
inference(forward_demodulation,[],[f5297,f494]) ).
fof(f5299,plain,
elem_214 = select(earray_163,index_213),
inference(superposition,[],[f126,f5298]) ).
fof(f5307,plain,
earray_29 = rselect_seq(queue_23),
inference(forward_demodulation,[],[f666,f640]) ).
fof(f5308,plain,
earray_22 = earray_29,
inference(forward_demodulation,[],[f5307,f498]) ).
fof(f5310,plain,
earray_50 = rselect_seq(queue_44),
inference(forward_demodulation,[],[f669,f639]) ).
fof(f5311,plain,
earray_43 = earray_50,
inference(forward_demodulation,[],[f5310,f505]) ).
fof(f5313,plain,
earray_71 = rselect_seq(queue_65),
inference(forward_demodulation,[],[f673,f638]) ).
fof(f5314,plain,
earray_64 = earray_71,
inference(forward_demodulation,[],[f5313,f508]) ).
fof(f5316,plain,
earray_98 = rselect_seq(queue_92),
inference(forward_demodulation,[],[f677,f637]) ).
fof(f5317,plain,
earray_98 = earray_91,
inference(superposition,[],[f5316,f513]) ).
fof(f5320,plain,
index_0 = rselect_head(queue_5),
inference(forward_demodulation,[],[f738,f515]) ).
fof(f5321,plain,
index_3 = rselect_head(queue_5),
inference(forward_demodulation,[],[f5320,f5118]) ).
fof(f5322,plain,
index_3 = rselect_head(queue_7),
inference(superposition,[],[f5321,f720]) ).
fof(f5324,plain,
rselect_head(queue_103) = rselect_head(queue_109),
inference(superposition,[],[f739,f699]) ).
fof(f5326,plain,
index_116 = rselect_head(queue_109),
inference(forward_demodulation,[],[f740,f737]) ).
fof(f5327,plain,
index_117 = rselect_head(queue_122),
inference(forward_demodulation,[],[f741,f516]) ).
fof(f5328,plain,
index_117 = rselect_head(queue_124),
inference(superposition,[],[f5327,f702]) ).
fof(f5330,plain,
rselect_head(queue_124) = rselect_head(queue_130),
inference(superposition,[],[f742,f703]) ).
fof(f5332,plain,
rselect_head(queue_13) = rselect_head(queue_19),
inference(superposition,[],[f743,f709]) ).
fof(f5334,plain,
index_137 = rselect_head(queue_130),
inference(forward_demodulation,[],[f744,f736]) ).
fof(f5335,plain,
index_138 = rselect_head(queue_143),
inference(forward_demodulation,[],[f745,f517]) ).
fof(f5336,plain,
index_138 = rselect_head(queue_145),
inference(superposition,[],[f5335,f705]) ).
fof(f5338,plain,
rselect_head(queue_145) = rselect_head(queue_151),
inference(superposition,[],[f746,f706]) ).
fof(f5340,plain,
index_167 = rselect_head(queue_151),
inference(forward_demodulation,[],[f747,f734]) ).
fof(f5341,plain,
index_159 = rselect_head(queue_173),
inference(forward_demodulation,[],[f748,f518]) ).
fof(f5342,plain,
index_159 = rselect_head(queue_175),
inference(superposition,[],[f5341,f710]) ).
fof(f5344,plain,
rselect_head(queue_175) = rselect_head(queue_181),
inference(superposition,[],[f749,f711]) ).
fof(f5346,plain,
index_188 = rselect_head(queue_181),
inference(forward_demodulation,[],[f750,f733]) ).
fof(f5347,plain,
index_26 = rselect_head(queue_19),
inference(forward_demodulation,[],[f751,f731]) ).
fof(f5348,plain,
index_189 = rselect_head(queue_194),
inference(forward_demodulation,[],[f752,f520]) ).
fof(f5349,plain,
index_189 = rselect_head(queue_196),
inference(superposition,[],[f5348,f713]) ).
fof(f5351,plain,
rselect_head(queue_196) = rselect_head(queue_202),
inference(superposition,[],[f753,f714]) ).
fof(f5354,plain,
index_209 = rselect_head(queue_202),
inference(forward_demodulation,[],[f754,f732]) ).
fof(f5356,plain,
rselect_head(queue_211) = rselect_head(queue_13),
inference(forward_demodulation,[],[f755,f700]) ).
fof(f5357,plain,
index_210 = rselect_head(queue_13),
inference(forward_demodulation,[],[f5356,f521]) ).
fof(f5358,plain,
index_27 = rselect_head(queue_32),
inference(forward_demodulation,[],[f756,f522]) ).
fof(f5359,plain,
index_27 = rselect_head(queue_34),
inference(superposition,[],[f5358,f717]) ).
fof(f5361,plain,
rselect_head(queue_34) = rselect_head(queue_40),
inference(superposition,[],[f757,f718]) ).
fof(f5363,plain,
index_47 = rselect_head(queue_40),
inference(forward_demodulation,[],[f758,f730]) ).
fof(f5364,plain,
index_48 = rselect_head(queue_53),
inference(forward_demodulation,[],[f759,f523]) ).
fof(f5365,plain,
index_48 = rselect_head(queue_55),
inference(superposition,[],[f5364,f721]) ).
fof(f5368,plain,
rselect_head(queue_55) = rselect_head(queue_61),
inference(superposition,[],[f760,f722]) ).
fof(f5370,plain,
index_68 = rselect_head(queue_61),
inference(forward_demodulation,[],[f761,f729]) ).
fof(f5371,plain,
rselect_head(queue_7) = rselect_head(queue_82),
inference(superposition,[],[f762,f725]) ).
fof(f5374,plain,
index_69 = rselect_head(queue_74),
inference(forward_demodulation,[],[f763,f524]) ).
fof(f5375,plain,
index_69 = rselect_head(queue_76),
inference(superposition,[],[f5374,f724]) ).
fof(f5377,plain,
rselect_head(queue_76) = rselect_head(queue_88),
inference(superposition,[],[f764,f726]) ).
fof(f5379,plain,
index_158 = rselect_head(queue_82),
inference(forward_demodulation,[],[f765,f735]) ).
fof(f5380,plain,
index_95 = rselect_head(queue_88),
inference(forward_demodulation,[],[f766,f728]) ).
fof(f5383,plain,
rselect_head(queue_97) = rselect_head(queue_103),
inference(forward_demodulation,[],[f767,f698]) ).
fof(f5384,plain,
index_96 = rselect_head(queue_103),
inference(forward_demodulation,[],[f5383,f525]) ).
fof(f5396,plain,
index_15 != index_24,
inference(superposition,[],[f1707,f176]) ).
fof(f5397,plain,
index_15 != index_30,
inference(superposition,[],[f5396,f5103]) ).
fof(f5480,plain,
index_15 != s(s(s(index_21))),
inference(forward_demodulation,[],[f859,f571]) ).
fof(f5481,plain,
index_15 != s(s(index_24)),
inference(forward_demodulation,[],[f5480,f176]) ).
fof(f5482,plain,
index_15 != s(s(index_30)),
inference(forward_demodulation,[],[f5481,f5103]) ).
fof(f5483,plain,
index_15 != s(index_33),
inference(forward_demodulation,[],[f5482,f181]) ).
fof(f5484,plain,
index_15 != s(index_36),
inference(forward_demodulation,[],[f5483,f566]) ).
fof(f5485,plain,
index_15 != index_39,
inference(superposition,[],[f5484,f183]) ).
fof(f5486,plain,
index_15 != index_42,
inference(superposition,[],[f5485,f565]) ).
fof(f5693,plain,
index_15 != s(s(s(s(index_21)))),
inference(forward_demodulation,[],[f936,f571]) ).
fof(f5694,plain,
index_15 != s(s(s(index_24))),
inference(forward_demodulation,[],[f5693,f176]) ).
fof(f5695,plain,
index_15 != s(s(s(index_30))),
inference(forward_demodulation,[],[f5694,f5103]) ).
fof(f5696,plain,
index_15 != s(s(index_33)),
inference(forward_demodulation,[],[f5695,f181]) ).
fof(f5697,plain,
index_15 != s(s(index_36)),
inference(forward_demodulation,[],[f5696,f566]) ).
fof(f5698,plain,
index_15 != s(index_39),
inference(forward_demodulation,[],[f5697,f183]) ).
fof(f5699,plain,
index_15 != s(index_42),
inference(forward_demodulation,[],[f5698,f565]) ).
fof(f5701,plain,
index_15 != index_45,
inference(superposition,[],[f5699,f185]) ).
fof(f5709,plain,
index_15 != index_51,
inference(superposition,[],[f5701,f5101]) ).
fof(f5949,plain,
index_15 != s(s(s(s(s(index_21))))),
inference(forward_demodulation,[],[f985,f571]) ).
fof(f5950,plain,
index_15 != s(s(s(s(index_24)))),
inference(forward_demodulation,[],[f5949,f176]) ).
fof(f5951,plain,
index_15 != s(s(s(s(index_30)))),
inference(forward_demodulation,[],[f5950,f5103]) ).
fof(f5952,plain,
index_15 != s(s(s(index_33))),
inference(forward_demodulation,[],[f5951,f181]) ).
fof(f5953,plain,
index_15 != s(s(s(index_36))),
inference(forward_demodulation,[],[f5952,f566]) ).
fof(f5954,plain,
index_15 != s(s(index_39)),
inference(forward_demodulation,[],[f5953,f183]) ).
fof(f5955,plain,
index_15 != s(s(index_42)),
inference(forward_demodulation,[],[f5954,f565]) ).
fof(f5956,plain,
index_15 != s(index_45),
inference(forward_demodulation,[],[f5955,f185]) ).
fof(f5957,plain,
index_15 != s(index_51),
inference(forward_demodulation,[],[f5956,f5101]) ).
fof(f5959,plain,
index_15 != index_54,
inference(superposition,[],[f5957,f189]) ).
fof(f5960,plain,
index_15 != index_57,
inference(superposition,[],[f5959,f563]) ).
fof(f6253,plain,
index_15 != s(s(s(s(s(s(index_21)))))),
inference(forward_demodulation,[],[f1034,f571]) ).
fof(f6254,plain,
index_15 != s(s(s(s(s(index_24))))),
inference(forward_demodulation,[],[f6253,f176]) ).
fof(f6255,plain,
index_15 != s(s(s(s(s(index_30))))),
inference(forward_demodulation,[],[f6254,f5103]) ).
fof(f6256,plain,
index_15 != s(s(s(s(index_33)))),
inference(forward_demodulation,[],[f6255,f181]) ).
fof(f6257,plain,
index_15 != s(s(s(s(index_36)))),
inference(forward_demodulation,[],[f6256,f566]) ).
fof(f6258,plain,
index_15 != s(s(s(index_39))),
inference(forward_demodulation,[],[f6257,f183]) ).
fof(f6259,plain,
index_15 != s(s(s(index_42))),
inference(forward_demodulation,[],[f6258,f565]) ).
fof(f6260,plain,
index_15 != s(s(index_45)),
inference(forward_demodulation,[],[f6259,f185]) ).
fof(f6261,plain,
index_15 != s(s(index_51)),
inference(forward_demodulation,[],[f6260,f5101]) ).
fof(f6262,plain,
index_15 != s(index_54),
inference(forward_demodulation,[],[f6261,f189]) ).
fof(f6263,plain,
index_15 != s(index_57),
inference(forward_demodulation,[],[f6262,f563]) ).
fof(f6264,plain,
index_15 != index_60,
inference(superposition,[],[f6263,f192]) ).
fof(f6265,plain,
index_15 != index_63,
inference(superposition,[],[f6264,f562]) ).
fof(f6626,plain,
index_15 != s(s(s(s(s(s(s(index_21))))))),
inference(forward_demodulation,[],[f1083,f571]) ).
fof(f6627,plain,
index_15 != s(s(s(s(s(s(index_24)))))),
inference(forward_demodulation,[],[f6626,f176]) ).
fof(f6628,plain,
index_15 != s(s(s(s(s(s(index_30)))))),
inference(forward_demodulation,[],[f6627,f5103]) ).
fof(f6629,plain,
index_15 != s(s(s(s(s(index_33))))),
inference(forward_demodulation,[],[f6628,f181]) ).
fof(f6630,plain,
index_15 != s(s(s(s(s(index_36))))),
inference(forward_demodulation,[],[f6629,f566]) ).
fof(f6631,plain,
index_15 != s(s(s(s(index_39)))),
inference(forward_demodulation,[],[f6630,f183]) ).
fof(f6632,plain,
index_15 != s(s(s(s(index_42)))),
inference(forward_demodulation,[],[f6631,f565]) ).
fof(f6633,plain,
index_15 != s(s(s(index_45))),
inference(forward_demodulation,[],[f6632,f185]) ).
fof(f6634,plain,
index_15 != s(s(s(index_51))),
inference(forward_demodulation,[],[f6633,f5101]) ).
fof(f6635,plain,
index_15 != s(s(index_54)),
inference(forward_demodulation,[],[f6634,f189]) ).
fof(f6636,plain,
index_15 != s(s(index_57)),
inference(forward_demodulation,[],[f6635,f563]) ).
fof(f6637,plain,
index_15 != s(index_60),
inference(forward_demodulation,[],[f6636,f192]) ).
fof(f6638,plain,
index_15 != s(index_63),
inference(forward_demodulation,[],[f6637,f562]) ).
fof(f6639,plain,
index_15 != index_66,
inference(superposition,[],[f6638,f194]) ).
fof(f6669,plain,
index_15 != index_72,
inference(superposition,[],[f6639,f5099]) ).
fof(f6920,plain,
! [X0] :
( select(earray_100,X0) = select(earray_106,X0)
| index_105 = X0 ),
inference(forward_demodulation,[],[f1189,f5091]) ).
fof(f6921,plain,
! [X0] :
( select(earray_106,X0) = select(earray_112,X0)
| index_111 = X0 ),
inference(forward_demodulation,[],[f1190,f5089]) ).
fof(f6922,plain,
! [X0] :
( select(earray_112,X0) = select(earray_121,X0)
| index_120 = X0 ),
inference(forward_demodulation,[],[f1191,f5287]) ).
fof(f6923,plain,
! [X0] :
( select(earray_121,X0) = select(earray_127,X0)
| index_126 = X0 ),
inference(forward_demodulation,[],[f1192,f5085]) ).
fof(f6924,plain,
! [X0] :
( select(earray_127,X0) = select(earray_133,X0)
| index_132 = X0 ),
inference(forward_demodulation,[],[f1193,f5083]) ).
fof(f6926,plain,
! [X0] :
( select(earray_133,X0) = select(earray_142,X0)
| index_141 = X0 ),
inference(forward_demodulation,[],[f1195,f5292]) ).
fof(f6927,plain,
! [X0] :
( select(earray_142,X0) = select(earray_148,X0)
| index_147 = X0 ),
inference(forward_demodulation,[],[f1196,f5081]) ).
fof(f6928,plain,
! [X0] :
( select(earray_148,X0) = select(earray_163,X0)
| index_162 = X0 ),
inference(forward_demodulation,[],[f1198,f5079]) ).
fof(f6934,plain,
! [X0] :
( select(earray_16,X0) = select(earray_22,X0)
| index_21 = X0 ),
inference(forward_demodulation,[],[f1205,f5077]) ).
fof(f6937,plain,
! [X0] :
( select(earray_22,X0) = select(earray_31,X0)
| index_30 = X0 ),
inference(forward_demodulation,[],[f1207,f5308]) ).
fof(f6938,plain,
! [X0] :
( select(earray_31,X0) = select(earray_37,X0)
| index_36 = X0 ),
inference(forward_demodulation,[],[f1208,f5067]) ).
fof(f6939,plain,
! [X0] :
( select(earray_37,X0) = select(earray_43,X0)
| index_42 = X0 ),
inference(forward_demodulation,[],[f1209,f5065]) ).
fof(f6940,plain,
! [X0] :
( select(earray_43,X0) = select(earray_52,X0)
| index_51 = X0 ),
inference(forward_demodulation,[],[f1210,f5311]) ).
fof(f6941,plain,
! [X0] :
( select(earray_52,X0) = select(earray_58,X0)
| index_57 = X0 ),
inference(forward_demodulation,[],[f1211,f5060]) ).
fof(f6942,plain,
! [X0] :
( select(earray_58,X0) = select(earray_64,X0)
| index_63 = X0 ),
inference(forward_demodulation,[],[f1212,f5058]) ).
fof(f6943,plain,
! [X0] :
( select(earray_64,X0) = select(earray_73,X0)
| index_72 = X0 ),
inference(forward_demodulation,[],[f1213,f5314]) ).
fof(f6946,plain,
! [X0] :
( select(earray_73,X0) = select(earray_85,X0)
| index_84 = X0 ),
inference(forward_demodulation,[],[f1215,f5055]) ).
fof(f6947,plain,
! [X0] :
( select(earray_98,X0) = select(earray_89,X0)
| index_90 = X0 ),
inference(forward_demodulation,[],[f1216,f5317]) ).
fof(f6948,plain,
! [X0] :
( select(earray_98,X0) = select(earray_85,X0)
| index_90 = X0 ),
inference(forward_demodulation,[],[f6947,f5051]) ).
fof(f7012,plain,
! [X0] :
( select(earray_98,X0) = select(earray_73,X0)
| index_90 = X0
| index_84 = X0 ),
inference(superposition,[],[f6948,f6946]) ).
fof(f7124,plain,
index_15 != s(s(s(s(s(s(s(s(index_21)))))))),
inference(forward_demodulation,[],[f1138,f571]) ).
fof(f7125,plain,
index_15 != s(s(s(s(s(s(s(index_24))))))),
inference(forward_demodulation,[],[f7124,f176]) ).
fof(f7126,plain,
index_15 != s(s(s(s(s(s(s(index_30))))))),
inference(forward_demodulation,[],[f7125,f5103]) ).
fof(f7127,plain,
index_15 != s(s(s(s(s(s(index_33)))))),
inference(forward_demodulation,[],[f7126,f181]) ).
fof(f7128,plain,
index_15 != s(s(s(s(s(s(index_36)))))),
inference(forward_demodulation,[],[f7127,f566]) ).
fof(f7129,plain,
index_15 != s(s(s(s(s(index_39))))),
inference(forward_demodulation,[],[f7128,f183]) ).
fof(f7130,plain,
index_15 != s(s(s(s(s(index_42))))),
inference(forward_demodulation,[],[f7129,f565]) ).
fof(f7131,plain,
index_15 != s(s(s(s(index_45)))),
inference(forward_demodulation,[],[f7130,f185]) ).
fof(f7132,plain,
index_15 != s(s(s(s(index_51)))),
inference(forward_demodulation,[],[f7131,f5101]) ).
fof(f7133,plain,
index_15 != s(s(s(index_54))),
inference(forward_demodulation,[],[f7132,f189]) ).
fof(f7134,plain,
index_15 != s(s(s(index_57))),
inference(forward_demodulation,[],[f7133,f563]) ).
fof(f7135,plain,
index_15 != s(s(index_60)),
inference(forward_demodulation,[],[f7134,f192]) ).
fof(f7136,plain,
index_15 != s(s(index_63)),
inference(forward_demodulation,[],[f7135,f562]) ).
fof(f7137,plain,
index_15 != s(index_66),
inference(forward_demodulation,[],[f7136,f194]) ).
fof(f7138,plain,
index_15 != s(index_72),
inference(forward_demodulation,[],[f7137,f5099]) ).
fof(f7139,plain,
index_15 != index_75,
inference(superposition,[],[f7138,f198]) ).
fof(f7156,plain,
index_15 != index_84,
inference(superposition,[],[f7139,f561]) ).
fof(f7590,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_21))))))))),
inference(forward_demodulation,[],[f1229,f571]) ).
fof(f7591,plain,
index_15 != s(s(s(s(s(s(s(s(index_24)))))))),
inference(forward_demodulation,[],[f7590,f176]) ).
fof(f7592,plain,
index_15 != s(s(s(s(s(s(s(s(index_30)))))))),
inference(forward_demodulation,[],[f7591,f5103]) ).
fof(f7593,plain,
index_15 != s(s(s(s(s(s(s(index_33))))))),
inference(forward_demodulation,[],[f7592,f181]) ).
fof(f7594,plain,
index_15 != s(s(s(s(s(s(s(index_36))))))),
inference(forward_demodulation,[],[f7593,f566]) ).
fof(f7595,plain,
index_15 != s(s(s(s(s(s(index_39)))))),
inference(forward_demodulation,[],[f7594,f183]) ).
fof(f7596,plain,
index_15 != s(s(s(s(s(s(index_42)))))),
inference(forward_demodulation,[],[f7595,f565]) ).
fof(f7597,plain,
index_15 != s(s(s(s(s(index_45))))),
inference(forward_demodulation,[],[f7596,f185]) ).
fof(f7598,plain,
index_15 != s(s(s(s(s(index_51))))),
inference(forward_demodulation,[],[f7597,f5101]) ).
fof(f7599,plain,
index_15 != s(s(s(s(index_54)))),
inference(forward_demodulation,[],[f7598,f189]) ).
fof(f7600,plain,
index_15 != s(s(s(s(index_57)))),
inference(forward_demodulation,[],[f7599,f563]) ).
fof(f7601,plain,
index_15 != s(s(s(index_60))),
inference(forward_demodulation,[],[f7600,f192]) ).
fof(f7602,plain,
index_15 != s(s(s(index_63))),
inference(forward_demodulation,[],[f7601,f562]) ).
fof(f7603,plain,
index_15 != s(s(index_66)),
inference(forward_demodulation,[],[f7602,f194]) ).
fof(f7604,plain,
index_15 != s(s(index_72)),
inference(forward_demodulation,[],[f7603,f5099]) ).
fof(f7605,plain,
index_15 != s(index_75),
inference(forward_demodulation,[],[f7604,f198]) ).
fof(f7606,plain,
index_15 != s(index_84),
inference(forward_demodulation,[],[f7605,f561]) ).
fof(f7607,plain,
index_15 != index_87,
inference(superposition,[],[f7606,f202]) ).
fof(f7662,plain,
index_15 != index_90,
inference(superposition,[],[f7607,f559]) ).
fof(f8108,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_21)))))))))),
inference(forward_demodulation,[],[f1294,f571]) ).
fof(f8109,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_24))))))))),
inference(forward_demodulation,[],[f8108,f176]) ).
fof(f8110,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_30))))))))),
inference(forward_demodulation,[],[f8109,f5103]) ).
fof(f8111,plain,
index_15 != s(s(s(s(s(s(s(s(index_33)))))))),
inference(forward_demodulation,[],[f8110,f181]) ).
fof(f8112,plain,
index_15 != s(s(s(s(s(s(s(s(index_36)))))))),
inference(forward_demodulation,[],[f8111,f566]) ).
fof(f8113,plain,
index_15 != s(s(s(s(s(s(s(index_39))))))),
inference(forward_demodulation,[],[f8112,f183]) ).
fof(f8114,plain,
index_15 != s(s(s(s(s(s(s(index_42))))))),
inference(forward_demodulation,[],[f8113,f565]) ).
fof(f8115,plain,
index_15 != s(s(s(s(s(s(index_45)))))),
inference(forward_demodulation,[],[f8114,f185]) ).
fof(f8116,plain,
index_15 != s(s(s(s(s(s(index_51)))))),
inference(forward_demodulation,[],[f8115,f5101]) ).
fof(f8117,plain,
index_15 != s(s(s(s(s(index_54))))),
inference(forward_demodulation,[],[f8116,f189]) ).
fof(f8118,plain,
index_15 != s(s(s(s(s(index_57))))),
inference(forward_demodulation,[],[f8117,f563]) ).
fof(f8119,plain,
index_15 != s(s(s(s(index_60)))),
inference(forward_demodulation,[],[f8118,f192]) ).
fof(f8120,plain,
index_15 != s(s(s(s(index_63)))),
inference(forward_demodulation,[],[f8119,f562]) ).
fof(f8121,plain,
index_15 != s(s(s(index_66))),
inference(forward_demodulation,[],[f8120,f194]) ).
fof(f8122,plain,
index_15 != s(s(s(index_72))),
inference(forward_demodulation,[],[f8121,f5099]) ).
fof(f8123,plain,
index_15 != s(s(index_75)),
inference(forward_demodulation,[],[f8122,f198]) ).
fof(f8124,plain,
index_15 != s(s(index_84)),
inference(forward_demodulation,[],[f8123,f561]) ).
fof(f8125,plain,
index_15 != s(index_87),
inference(forward_demodulation,[],[f8124,f202]) ).
fof(f8126,plain,
index_15 != s(index_90),
inference(forward_demodulation,[],[f8125,f559]) ).
fof(f8127,plain,
index_15 != index_93,
inference(superposition,[],[f8126,f205]) ).
fof(f8128,plain,
index_99 != index_15,
inference(forward_demodulation,[],[f8127,f5093]) ).
fof(f8622,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))),
inference(forward_demodulation,[],[f1361,f571]) ).
fof(f8623,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_24)))))))))),
inference(forward_demodulation,[],[f8622,f176]) ).
fof(f8624,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_30)))))))))),
inference(forward_demodulation,[],[f8623,f5103]) ).
fof(f8625,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_33))))))))),
inference(forward_demodulation,[],[f8624,f181]) ).
fof(f8626,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_36))))))))),
inference(forward_demodulation,[],[f8625,f566]) ).
fof(f8627,plain,
index_15 != s(s(s(s(s(s(s(s(index_39)))))))),
inference(forward_demodulation,[],[f8626,f183]) ).
fof(f8628,plain,
index_15 != s(s(s(s(s(s(s(s(index_42)))))))),
inference(forward_demodulation,[],[f8627,f565]) ).
fof(f8629,plain,
index_15 != s(s(s(s(s(s(s(index_45))))))),
inference(forward_demodulation,[],[f8628,f185]) ).
fof(f8630,plain,
index_15 != s(s(s(s(s(s(s(index_51))))))),
inference(forward_demodulation,[],[f8629,f5101]) ).
fof(f8631,plain,
index_15 != s(s(s(s(s(s(index_54)))))),
inference(forward_demodulation,[],[f8630,f189]) ).
fof(f8632,plain,
index_15 != s(s(s(s(s(s(index_57)))))),
inference(forward_demodulation,[],[f8631,f563]) ).
fof(f8633,plain,
index_15 != s(s(s(s(s(index_60))))),
inference(forward_demodulation,[],[f8632,f192]) ).
fof(f8634,plain,
index_15 != s(s(s(s(s(index_63))))),
inference(forward_demodulation,[],[f8633,f562]) ).
fof(f8635,plain,
index_15 != s(s(s(s(index_66)))),
inference(forward_demodulation,[],[f8634,f194]) ).
fof(f8636,plain,
index_15 != s(s(s(s(index_72)))),
inference(forward_demodulation,[],[f8635,f5099]) ).
fof(f8637,plain,
index_15 != s(s(s(index_75))),
inference(forward_demodulation,[],[f8636,f198]) ).
fof(f8638,plain,
index_15 != s(s(s(index_84))),
inference(forward_demodulation,[],[f8637,f561]) ).
fof(f8639,plain,
index_15 != s(s(index_87)),
inference(forward_demodulation,[],[f8638,f202]) ).
fof(f8640,plain,
index_15 != s(s(index_90)),
inference(forward_demodulation,[],[f8639,f559]) ).
fof(f8641,plain,
index_15 != s(index_93),
inference(forward_demodulation,[],[f8640,f205]) ).
fof(f8642,plain,
index_15 != s(index_99),
inference(forward_demodulation,[],[f8641,f5093]) ).
fof(f8643,plain,
index_15 != index_102,
inference(superposition,[],[f8642,f128]) ).
fof(f8644,plain,
index_105 != index_15,
inference(forward_demodulation,[],[f8643,f578]) ).
fof(f9190,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))),
inference(forward_demodulation,[],[f1428,f571]) ).
fof(f9191,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))),
inference(forward_demodulation,[],[f9190,f176]) ).
fof(f9192,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))),
inference(forward_demodulation,[],[f9191,f5103]) ).
fof(f9193,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_33)))))))))),
inference(forward_demodulation,[],[f9192,f181]) ).
fof(f9194,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_36)))))))))),
inference(forward_demodulation,[],[f9193,f566]) ).
fof(f9195,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_39))))))))),
inference(forward_demodulation,[],[f9194,f183]) ).
fof(f9196,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_42))))))))),
inference(forward_demodulation,[],[f9195,f565]) ).
fof(f9197,plain,
index_15 != s(s(s(s(s(s(s(s(index_45)))))))),
inference(forward_demodulation,[],[f9196,f185]) ).
fof(f9198,plain,
index_15 != s(s(s(s(s(s(s(s(index_51)))))))),
inference(forward_demodulation,[],[f9197,f5101]) ).
fof(f9199,plain,
index_15 != s(s(s(s(s(s(s(index_54))))))),
inference(forward_demodulation,[],[f9198,f189]) ).
fof(f9200,plain,
index_15 != s(s(s(s(s(s(s(index_57))))))),
inference(forward_demodulation,[],[f9199,f563]) ).
fof(f9201,plain,
index_15 != s(s(s(s(s(s(index_60)))))),
inference(forward_demodulation,[],[f9200,f192]) ).
fof(f9202,plain,
index_15 != s(s(s(s(s(s(index_63)))))),
inference(forward_demodulation,[],[f9201,f562]) ).
fof(f9203,plain,
index_15 != s(s(s(s(s(index_66))))),
inference(forward_demodulation,[],[f9202,f194]) ).
fof(f9204,plain,
index_15 != s(s(s(s(s(index_72))))),
inference(forward_demodulation,[],[f9203,f5099]) ).
fof(f9205,plain,
index_15 != s(s(s(s(index_75)))),
inference(forward_demodulation,[],[f9204,f198]) ).
fof(f9206,plain,
index_15 != s(s(s(s(index_84)))),
inference(forward_demodulation,[],[f9205,f561]) ).
fof(f9207,plain,
index_15 != s(s(s(index_87))),
inference(forward_demodulation,[],[f9206,f202]) ).
fof(f9208,plain,
index_15 != s(s(s(index_90))),
inference(forward_demodulation,[],[f9207,f559]) ).
fof(f9209,plain,
index_15 != s(s(index_93)),
inference(forward_demodulation,[],[f9208,f205]) ).
fof(f9210,plain,
index_15 != s(s(index_99)),
inference(forward_demodulation,[],[f9209,f5093]) ).
fof(f9211,plain,
index_15 != s(index_102),
inference(forward_demodulation,[],[f9210,f128]) ).
fof(f9212,plain,
index_15 != s(index_105),
inference(forward_demodulation,[],[f9211,f578]) ).
fof(f9213,plain,
index_15 != index_108,
inference(superposition,[],[f9212,f130]) ).
fof(f9214,plain,
index_111 != index_15,
inference(forward_demodulation,[],[f9213,f577]) ).
fof(f9796,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))),
inference(forward_demodulation,[],[f1498,f571]) ).
fof(f9797,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))),
inference(forward_demodulation,[],[f9796,f176]) ).
fof(f9798,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))),
inference(forward_demodulation,[],[f9797,f5103]) ).
fof(f9799,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_33))))))))))),
inference(forward_demodulation,[],[f9798,f181]) ).
fof(f9800,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))),
inference(forward_demodulation,[],[f9799,f566]) ).
fof(f9801,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_39)))))))))),
inference(forward_demodulation,[],[f9800,f183]) ).
fof(f9802,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_42)))))))))),
inference(forward_demodulation,[],[f9801,f565]) ).
fof(f9803,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_45))))))))),
inference(forward_demodulation,[],[f9802,f185]) ).
fof(f9804,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_51))))))))),
inference(forward_demodulation,[],[f9803,f5101]) ).
fof(f9805,plain,
index_15 != s(s(s(s(s(s(s(s(index_54)))))))),
inference(forward_demodulation,[],[f9804,f189]) ).
fof(f9806,plain,
index_15 != s(s(s(s(s(s(s(s(index_57)))))))),
inference(forward_demodulation,[],[f9805,f563]) ).
fof(f9807,plain,
index_15 != s(s(s(s(s(s(s(index_60))))))),
inference(forward_demodulation,[],[f9806,f192]) ).
fof(f9808,plain,
index_15 != s(s(s(s(s(s(s(index_63))))))),
inference(forward_demodulation,[],[f9807,f562]) ).
fof(f9809,plain,
index_15 != s(s(s(s(s(s(index_66)))))),
inference(forward_demodulation,[],[f9808,f194]) ).
fof(f9810,plain,
index_15 != s(s(s(s(s(s(index_72)))))),
inference(forward_demodulation,[],[f9809,f5099]) ).
fof(f9811,plain,
index_15 != s(s(s(s(s(index_75))))),
inference(forward_demodulation,[],[f9810,f198]) ).
fof(f9812,plain,
index_15 != s(s(s(s(s(index_84))))),
inference(forward_demodulation,[],[f9811,f561]) ).
fof(f9813,plain,
index_15 != s(s(s(s(index_87)))),
inference(forward_demodulation,[],[f9812,f202]) ).
fof(f9814,plain,
index_15 != s(s(s(s(index_90)))),
inference(forward_demodulation,[],[f9813,f559]) ).
fof(f9815,plain,
index_15 != s(s(s(index_93))),
inference(forward_demodulation,[],[f9814,f205]) ).
fof(f9816,plain,
index_15 != s(s(s(index_99))),
inference(forward_demodulation,[],[f9815,f5093]) ).
fof(f9817,plain,
index_15 != s(s(index_102)),
inference(forward_demodulation,[],[f9816,f128]) ).
fof(f9818,plain,
index_15 != s(s(index_105)),
inference(forward_demodulation,[],[f9817,f578]) ).
fof(f9819,plain,
index_15 != s(index_108),
inference(forward_demodulation,[],[f9818,f130]) ).
fof(f9820,plain,
index_15 != s(index_111),
inference(forward_demodulation,[],[f9819,f577]) ).
fof(f9821,plain,
index_15 != index_114,
inference(superposition,[],[f9820,f132]) ).
fof(f9822,plain,
index_120 != index_15,
inference(forward_demodulation,[],[f9821,f5116]) ).
fof(f10406,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))),
inference(forward_demodulation,[],[f1569,f571]) ).
fof(f10407,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))),
inference(forward_demodulation,[],[f10406,f176]) ).
fof(f10408,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))),
inference(forward_demodulation,[],[f10407,f5103]) ).
fof(f10409,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_33)))))))))))),
inference(forward_demodulation,[],[f10408,f181]) ).
fof(f10410,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))),
inference(forward_demodulation,[],[f10409,f566]) ).
fof(f10411,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))),
inference(forward_demodulation,[],[f10410,f183]) ).
fof(f10412,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))),
inference(forward_demodulation,[],[f10411,f565]) ).
fof(f10413,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_45)))))))))),
inference(forward_demodulation,[],[f10412,f185]) ).
fof(f10414,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_51)))))))))),
inference(forward_demodulation,[],[f10413,f5101]) ).
fof(f10415,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_54))))))))),
inference(forward_demodulation,[],[f10414,f189]) ).
fof(f10416,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_57))))))))),
inference(forward_demodulation,[],[f10415,f563]) ).
fof(f10417,plain,
index_15 != s(s(s(s(s(s(s(s(index_60)))))))),
inference(forward_demodulation,[],[f10416,f192]) ).
fof(f10418,plain,
index_15 != s(s(s(s(s(s(s(s(index_63)))))))),
inference(forward_demodulation,[],[f10417,f562]) ).
fof(f10419,plain,
index_15 != s(s(s(s(s(s(s(index_66))))))),
inference(forward_demodulation,[],[f10418,f194]) ).
fof(f10420,plain,
index_15 != s(s(s(s(s(s(s(index_72))))))),
inference(forward_demodulation,[],[f10419,f5099]) ).
fof(f10421,plain,
index_15 != s(s(s(s(s(s(index_75)))))),
inference(forward_demodulation,[],[f10420,f198]) ).
fof(f10422,plain,
index_15 != s(s(s(s(s(s(index_84)))))),
inference(forward_demodulation,[],[f10421,f561]) ).
fof(f10423,plain,
index_15 != s(s(s(s(s(index_87))))),
inference(forward_demodulation,[],[f10422,f202]) ).
fof(f10424,plain,
index_15 != s(s(s(s(s(index_90))))),
inference(forward_demodulation,[],[f10423,f559]) ).
fof(f10425,plain,
index_15 != s(s(s(s(index_93)))),
inference(forward_demodulation,[],[f10424,f205]) ).
fof(f10426,plain,
index_15 != s(s(s(s(index_99)))),
inference(forward_demodulation,[],[f10425,f5093]) ).
fof(f10427,plain,
index_15 != s(s(s(index_102))),
inference(forward_demodulation,[],[f10426,f128]) ).
fof(f10428,plain,
index_15 != s(s(s(index_105))),
inference(forward_demodulation,[],[f10427,f578]) ).
fof(f10429,plain,
index_15 != s(s(index_108)),
inference(forward_demodulation,[],[f10428,f130]) ).
fof(f10430,plain,
index_15 != s(s(index_111)),
inference(forward_demodulation,[],[f10429,f577]) ).
fof(f10431,plain,
index_15 != s(index_114),
inference(forward_demodulation,[],[f10430,f132]) ).
fof(f10432,plain,
index_15 != s(index_120),
inference(forward_demodulation,[],[f10431,f5116]) ).
fof(f10433,plain,
index_15 != index_123,
inference(superposition,[],[f10432,f137]) ).
fof(f10434,plain,
index_126 != index_15,
inference(forward_demodulation,[],[f10433,f575]) ).
fof(f11118,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))),
inference(forward_demodulation,[],[f1640,f571]) ).
fof(f11119,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))),
inference(forward_demodulation,[],[f11118,f176]) ).
fof(f11120,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))),
inference(forward_demodulation,[],[f11119,f5103]) ).
fof(f11121,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_33))))))))))))),
inference(forward_demodulation,[],[f11120,f181]) ).
fof(f11122,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))),
inference(forward_demodulation,[],[f11121,f566]) ).
fof(f11123,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))),
inference(forward_demodulation,[],[f11122,f183]) ).
fof(f11124,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))),
inference(forward_demodulation,[],[f11123,f565]) ).
fof(f11125,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))),
inference(forward_demodulation,[],[f11124,f185]) ).
fof(f11126,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))),
inference(forward_demodulation,[],[f11125,f5101]) ).
fof(f11127,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_54)))))))))),
inference(forward_demodulation,[],[f11126,f189]) ).
fof(f11128,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_57)))))))))),
inference(forward_demodulation,[],[f11127,f563]) ).
fof(f11129,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_60))))))))),
inference(forward_demodulation,[],[f11128,f192]) ).
fof(f11130,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_63))))))))),
inference(forward_demodulation,[],[f11129,f562]) ).
fof(f11131,plain,
index_15 != s(s(s(s(s(s(s(s(index_66)))))))),
inference(forward_demodulation,[],[f11130,f194]) ).
fof(f11132,plain,
index_15 != s(s(s(s(s(s(s(s(index_72)))))))),
inference(forward_demodulation,[],[f11131,f5099]) ).
fof(f11133,plain,
index_15 != s(s(s(s(s(s(s(index_75))))))),
inference(forward_demodulation,[],[f11132,f198]) ).
fof(f11134,plain,
index_15 != s(s(s(s(s(s(s(index_84))))))),
inference(forward_demodulation,[],[f11133,f561]) ).
fof(f11135,plain,
index_15 != s(s(s(s(s(s(index_87)))))),
inference(forward_demodulation,[],[f11134,f202]) ).
fof(f11136,plain,
index_15 != s(s(s(s(s(s(index_90)))))),
inference(forward_demodulation,[],[f11135,f559]) ).
fof(f11137,plain,
index_15 != s(s(s(s(s(index_93))))),
inference(forward_demodulation,[],[f11136,f205]) ).
fof(f11138,plain,
index_15 != s(s(s(s(s(index_99))))),
inference(forward_demodulation,[],[f11137,f5093]) ).
fof(f11139,plain,
index_15 != s(s(s(s(index_102)))),
inference(forward_demodulation,[],[f11138,f128]) ).
fof(f11140,plain,
index_15 != s(s(s(s(index_105)))),
inference(forward_demodulation,[],[f11139,f578]) ).
fof(f11141,plain,
index_15 != s(s(s(index_108))),
inference(forward_demodulation,[],[f11140,f130]) ).
fof(f11142,plain,
index_15 != s(s(s(index_111))),
inference(forward_demodulation,[],[f11141,f577]) ).
fof(f11143,plain,
index_15 != s(s(index_114)),
inference(forward_demodulation,[],[f11142,f132]) ).
fof(f11144,plain,
index_15 != s(s(index_120)),
inference(forward_demodulation,[],[f11143,f5116]) ).
fof(f11145,plain,
index_15 != s(index_123),
inference(forward_demodulation,[],[f11144,f137]) ).
fof(f11146,plain,
index_15 != s(index_126),
inference(forward_demodulation,[],[f11145,f575]) ).
fof(f11148,plain,
index_15 != index_129,
inference(superposition,[],[f11146,f139]) ).
fof(f11149,plain,
index_132 != index_15,
inference(forward_demodulation,[],[f11148,f574]) ).
fof(f11554,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))),
inference(forward_demodulation,[],[f1776,f5103]) ).
fof(f11555,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_33)))))))))))))),
inference(forward_demodulation,[],[f11554,f181]) ).
fof(f11556,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))),
inference(forward_demodulation,[],[f11555,f566]) ).
fof(f11557,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))),
inference(forward_demodulation,[],[f11556,f183]) ).
fof(f11558,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))),
inference(forward_demodulation,[],[f11557,f565]) ).
fof(f11559,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))),
inference(forward_demodulation,[],[f11558,f185]) ).
fof(f11560,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))),
inference(forward_demodulation,[],[f11559,f5101]) ).
fof(f11561,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))),
inference(forward_demodulation,[],[f11560,f189]) ).
fof(f11562,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))),
inference(forward_demodulation,[],[f11561,f563]) ).
fof(f11563,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_60)))))))))),
inference(forward_demodulation,[],[f11562,f192]) ).
fof(f11564,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_63)))))))))),
inference(forward_demodulation,[],[f11563,f562]) ).
fof(f11565,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_66))))))))),
inference(forward_demodulation,[],[f11564,f194]) ).
fof(f11566,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_72))))))))),
inference(forward_demodulation,[],[f11565,f5099]) ).
fof(f11567,plain,
index_15 != s(s(s(s(s(s(s(s(index_75)))))))),
inference(forward_demodulation,[],[f11566,f198]) ).
fof(f11568,plain,
index_15 != s(s(s(s(s(s(s(s(index_84)))))))),
inference(forward_demodulation,[],[f11567,f561]) ).
fof(f11569,plain,
index_15 != s(s(s(s(s(s(s(index_87))))))),
inference(forward_demodulation,[],[f11568,f202]) ).
fof(f11570,plain,
index_15 != s(s(s(s(s(s(s(index_90))))))),
inference(forward_demodulation,[],[f11569,f559]) ).
fof(f11571,plain,
index_15 != s(s(s(s(s(s(index_93)))))),
inference(forward_demodulation,[],[f11570,f205]) ).
fof(f11572,plain,
index_15 != s(s(s(s(s(s(index_99)))))),
inference(forward_demodulation,[],[f11571,f5093]) ).
fof(f11573,plain,
index_15 != s(s(s(s(s(index_102))))),
inference(forward_demodulation,[],[f11572,f128]) ).
fof(f11574,plain,
index_15 != s(s(s(s(s(index_105))))),
inference(forward_demodulation,[],[f11573,f578]) ).
fof(f11575,plain,
index_15 != s(s(s(s(index_108)))),
inference(forward_demodulation,[],[f11574,f130]) ).
fof(f11576,plain,
index_15 != s(s(s(s(index_111)))),
inference(forward_demodulation,[],[f11575,f577]) ).
fof(f11577,plain,
index_15 != s(s(s(index_114))),
inference(forward_demodulation,[],[f11576,f132]) ).
fof(f11578,plain,
index_15 != s(s(s(index_120))),
inference(forward_demodulation,[],[f11577,f5116]) ).
fof(f11579,plain,
index_15 != s(s(index_123)),
inference(forward_demodulation,[],[f11578,f137]) ).
fof(f11580,plain,
index_15 != s(s(index_126)),
inference(forward_demodulation,[],[f11579,f575]) ).
fof(f11581,plain,
index_15 != s(index_129),
inference(forward_demodulation,[],[f11580,f139]) ).
fof(f11582,plain,
index_15 != s(index_132),
inference(forward_demodulation,[],[f11581,f574]) ).
fof(f11583,plain,
index_15 != index_135,
inference(superposition,[],[f11582,f141]) ).
fof(f11584,plain,
index_141 != index_15,
inference(forward_demodulation,[],[f11583,f5111]) ).
fof(f12270,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))))),
inference(forward_demodulation,[],[f1863,f5103]) ).
fof(f12271,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_33))))))))))))))),
inference(forward_demodulation,[],[f12270,f181]) ).
fof(f12272,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))))),
inference(forward_demodulation,[],[f12271,f566]) ).
fof(f12273,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))),
inference(forward_demodulation,[],[f12272,f183]) ).
fof(f12274,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))),
inference(forward_demodulation,[],[f12273,f565]) ).
fof(f12275,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))),
inference(forward_demodulation,[],[f12274,f185]) ).
fof(f12276,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))),
inference(forward_demodulation,[],[f12275,f5101]) ).
fof(f12277,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))),
inference(forward_demodulation,[],[f12276,f189]) ).
fof(f12278,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_57)))))))))))),
inference(forward_demodulation,[],[f12277,f563]) ).
fof(f12279,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))),
inference(forward_demodulation,[],[f12278,f192]) ).
fof(f12280,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_63))))))))))),
inference(forward_demodulation,[],[f12279,f562]) ).
fof(f12281,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_66)))))))))),
inference(forward_demodulation,[],[f12280,f194]) ).
fof(f12282,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_72)))))))))),
inference(forward_demodulation,[],[f12281,f5099]) ).
fof(f12283,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_75))))))))),
inference(forward_demodulation,[],[f12282,f198]) ).
fof(f12284,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_84))))))))),
inference(forward_demodulation,[],[f12283,f561]) ).
fof(f12285,plain,
index_15 != s(s(s(s(s(s(s(s(index_87)))))))),
inference(forward_demodulation,[],[f12284,f202]) ).
fof(f12286,plain,
index_15 != s(s(s(s(s(s(s(s(index_90)))))))),
inference(forward_demodulation,[],[f12285,f559]) ).
fof(f12287,plain,
index_15 != s(s(s(s(s(s(s(index_93))))))),
inference(forward_demodulation,[],[f12286,f205]) ).
fof(f12288,plain,
index_15 != s(s(s(s(s(s(s(index_99))))))),
inference(forward_demodulation,[],[f12287,f5093]) ).
fof(f12289,plain,
index_15 != s(s(s(s(s(s(index_102)))))),
inference(forward_demodulation,[],[f12288,f128]) ).
fof(f12290,plain,
index_15 != s(s(s(s(s(s(index_105)))))),
inference(forward_demodulation,[],[f12289,f578]) ).
fof(f12291,plain,
index_15 != s(s(s(s(s(index_108))))),
inference(forward_demodulation,[],[f12290,f130]) ).
fof(f12292,plain,
index_15 != s(s(s(s(s(index_111))))),
inference(forward_demodulation,[],[f12291,f577]) ).
fof(f12293,plain,
index_15 != s(s(s(s(index_114)))),
inference(forward_demodulation,[],[f12292,f132]) ).
fof(f12294,plain,
index_15 != s(s(s(s(index_120)))),
inference(forward_demodulation,[],[f12293,f5116]) ).
fof(f12295,plain,
index_15 != s(s(s(index_123))),
inference(forward_demodulation,[],[f12294,f137]) ).
fof(f12296,plain,
index_15 != s(s(s(index_126))),
inference(forward_demodulation,[],[f12295,f575]) ).
fof(f12297,plain,
index_15 != s(s(index_129)),
inference(forward_demodulation,[],[f12296,f139]) ).
fof(f12298,plain,
index_15 != s(s(index_132)),
inference(forward_demodulation,[],[f12297,f574]) ).
fof(f12299,plain,
index_15 != s(index_135),
inference(forward_demodulation,[],[f12298,f141]) ).
fof(f12300,plain,
index_15 != s(index_141),
inference(forward_demodulation,[],[f12299,f5111]) ).
fof(f12301,plain,
index_15 != index_144,
inference(superposition,[],[f12300,f145]) ).
fof(f12302,plain,
index_147 != index_15,
inference(forward_demodulation,[],[f12301,f573]) ).
fof(f12813,plain,
( elem_214 = select(earray_148,index_213)
| index_162 = index_213 ),
inference(superposition,[],[f5299,f6928]) ).
fof(f12816,definition,
( spl0_1
<=> index_162 = index_213 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f12818,plain,
( index_162 = index_213
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f12816]) ).
fof(f12820,definition,
( spl0_2
<=> elem_214 = select(earray_148,index_213) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f12822,plain,
( elem_214 = select(earray_148,index_213)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f12820]) ).
fof(f12824,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f12813,f12820,f12816]) ).
fof(f12825,plain,
index_116 = rselect_head(queue_103),
inference(forward_demodulation,[],[f5324,f5326]) ).
fof(f12844,plain,
index_116 = index_96,
inference(superposition,[],[f12825,f5384]) ).
fof(f13041,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))))),
inference(forward_demodulation,[],[f1948,f5103]) ).
fof(f13042,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_33)))))))))))))))),
inference(forward_demodulation,[],[f13041,f181]) ).
fof(f13043,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))))),
inference(forward_demodulation,[],[f13042,f566]) ).
fof(f13044,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))),
inference(forward_demodulation,[],[f13043,f183]) ).
fof(f13045,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))),
inference(forward_demodulation,[],[f13044,f565]) ).
fof(f13046,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))),
inference(forward_demodulation,[],[f13045,f185]) ).
fof(f13047,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))),
inference(forward_demodulation,[],[f13046,f5101]) ).
fof(f13048,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))),
inference(forward_demodulation,[],[f13047,f189]) ).
fof(f13049,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))))),
inference(forward_demodulation,[],[f13048,f563]) ).
fof(f13050,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))),
inference(forward_demodulation,[],[f13049,f192]) ).
fof(f13051,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_63)))))))))))),
inference(forward_demodulation,[],[f13050,f562]) ).
fof(f13052,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))),
inference(forward_demodulation,[],[f13051,f194]) ).
fof(f13053,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_72))))))))))),
inference(forward_demodulation,[],[f13052,f5099]) ).
fof(f13054,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_75)))))))))),
inference(forward_demodulation,[],[f13053,f198]) ).
fof(f13055,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_84)))))))))),
inference(forward_demodulation,[],[f13054,f561]) ).
fof(f13056,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_87))))))))),
inference(forward_demodulation,[],[f13055,f202]) ).
fof(f13057,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_90))))))))),
inference(forward_demodulation,[],[f13056,f559]) ).
fof(f13058,plain,
index_15 != s(s(s(s(s(s(s(s(index_93)))))))),
inference(forward_demodulation,[],[f13057,f205]) ).
fof(f13059,plain,
index_15 != s(s(s(s(s(s(s(s(index_99)))))))),
inference(forward_demodulation,[],[f13058,f5093]) ).
fof(f13060,plain,
index_15 != s(s(s(s(s(s(s(index_102))))))),
inference(forward_demodulation,[],[f13059,f128]) ).
fof(f13061,plain,
index_15 != s(s(s(s(s(s(s(index_105))))))),
inference(forward_demodulation,[],[f13060,f578]) ).
fof(f13062,plain,
index_15 != s(s(s(s(s(s(index_108)))))),
inference(forward_demodulation,[],[f13061,f130]) ).
fof(f13063,plain,
index_15 != s(s(s(s(s(s(index_111)))))),
inference(forward_demodulation,[],[f13062,f577]) ).
fof(f13064,plain,
index_15 != s(s(s(s(s(index_114))))),
inference(forward_demodulation,[],[f13063,f132]) ).
fof(f13065,plain,
index_15 != s(s(s(s(s(index_120))))),
inference(forward_demodulation,[],[f13064,f5116]) ).
fof(f13066,plain,
index_15 != s(s(s(s(index_123)))),
inference(forward_demodulation,[],[f13065,f137]) ).
fof(f13067,plain,
index_15 != s(s(s(s(index_126)))),
inference(forward_demodulation,[],[f13066,f575]) ).
fof(f13068,plain,
index_15 != s(s(s(index_129))),
inference(forward_demodulation,[],[f13067,f139]) ).
fof(f13069,plain,
index_15 != s(s(s(index_132))),
inference(forward_demodulation,[],[f13068,f574]) ).
fof(f13070,plain,
index_15 != s(s(index_135)),
inference(forward_demodulation,[],[f13069,f141]) ).
fof(f13071,plain,
index_15 != s(s(index_141)),
inference(forward_demodulation,[],[f13070,f5111]) ).
fof(f13072,plain,
index_15 != s(index_144),
inference(forward_demodulation,[],[f13071,f145]) ).
fof(f13073,plain,
index_15 != s(index_147),
inference(forward_demodulation,[],[f13072,f573]) ).
fof(f13074,plain,
index_15 != index_150,
inference(superposition,[],[f13073,f148]) ).
fof(f13151,plain,
index_15 != index_162,
inference(superposition,[],[f13074,f572]) ).
fof(f13578,plain,
index_137 = rselect_head(queue_124),
inference(forward_demodulation,[],[f5330,f5334]) ).
fof(f13579,plain,
index_117 = index_137,
inference(forward_demodulation,[],[f13578,f5328]) ).
fof(f13580,plain,
index_138 = s(index_117),
inference(superposition,[],[f143,f13579]) ).
fof(f14152,plain,
index_26 = rselect_head(queue_13),
inference(forward_demodulation,[],[f5332,f5347]) ).
fof(f14153,plain,
index_210 = index_26,
inference(forward_demodulation,[],[f14152,f5357]) ).
fof(f14199,plain,
index_27 = s(index_210),
inference(superposition,[],[f178,f14153]) ).
fof(f14456,plain,
index_167 = rselect_head(queue_145),
inference(forward_demodulation,[],[f5338,f5340]) ).
fof(f14457,plain,
index_138 = index_167,
inference(forward_demodulation,[],[f14456,f5336]) ).
fof(f14460,plain,
index_168 = s(index_138),
inference(superposition,[],[f156,f14457]) ).
fof(f14461,plain,
index_213 = s(index_138),
inference(forward_demodulation,[],[f14460,f526]) ).
fof(f14787,plain,
index_188 = rselect_head(queue_175),
inference(forward_demodulation,[],[f5344,f5346]) ).
fof(f14788,plain,
index_159 = index_188,
inference(forward_demodulation,[],[f14787,f5342]) ).
fof(f14837,plain,
index_189 = s(index_159),
inference(superposition,[],[f165,f14788]) ).
fof(f15389,plain,
index_209 = rselect_head(queue_196),
inference(forward_demodulation,[],[f5351,f5354]) ).
fof(f15390,plain,
index_189 = index_209,
inference(forward_demodulation,[],[f15389,f5349]) ).
fof(f15391,plain,
index_210 = s(index_189),
inference(superposition,[],[f174,f15390]) ).
fof(f16037,plain,
index_47 = rselect_head(queue_34),
inference(forward_demodulation,[],[f5361,f5363]) ).
fof(f16038,plain,
index_27 = index_47,
inference(forward_demodulation,[],[f16037,f5359]) ).
fof(f16041,plain,
index_48 = s(index_27),
inference(superposition,[],[f187,f16038]) ).
fof(f16479,plain,
index_68 = rselect_head(queue_55),
inference(forward_demodulation,[],[f5368,f5370]) ).
fof(f16480,plain,
index_48 = index_68,
inference(forward_demodulation,[],[f16479,f5365]) ).
fof(f16481,plain,
index_69 = s(index_48),
inference(superposition,[],[f196,f16480]) ).
fof(f16597,plain,
index_158 = rselect_head(queue_7),
inference(forward_demodulation,[],[f5371,f5379]) ).
fof(f16598,plain,
index_3 = index_158,
inference(forward_demodulation,[],[f16597,f5322]) ).
fof(f16600,plain,
index_159 = s(index_3),
inference(superposition,[],[f152,f16598]) ).
fof(f16606,plain,
index_159 = index_6,
inference(superposition,[],[f191,f16600]) ).
fof(f16705,plain,
index_78 = index_159,
inference(forward_demodulation,[],[f16606,f564]) ).
fof(f16970,plain,
index_189 = s(index_78),
inference(superposition,[],[f14837,f16705]) ).
fof(f17524,plain,
index_189 = index_81,
inference(superposition,[],[f200,f16970]) ).
fof(f17623,plain,
index_153 = index_189,
inference(forward_demodulation,[],[f17524,f560]) ).
fof(f17830,plain,
s(index_153) = index_210,
inference(superposition,[],[f15391,f17623]) ).
fof(f17836,plain,
index_156 = index_210,
inference(forward_demodulation,[],[f17830,f150]) ).
fof(f17859,plain,
index_171 = index_210,
inference(forward_demodulation,[],[f17836,f5109]) ).
fof(f18443,plain,
s(index_171) = index_27,
inference(superposition,[],[f14199,f17859]) ).
fof(f18454,plain,
index_174 = index_27,
inference(forward_demodulation,[],[f18443,f158]) ).
fof(f18473,plain,
index_177 = index_27,
inference(forward_demodulation,[],[f18454,f570]) ).
fof(f19085,plain,
s(index_177) = index_48,
inference(superposition,[],[f16041,f18473]) ).
fof(f19088,plain,
index_180 = index_48,
inference(forward_demodulation,[],[f19085,f161]) ).
fof(f19116,plain,
index_183 = index_48,
inference(forward_demodulation,[],[f19088,f569]) ).
fof(f19666,plain,
s(index_183) = index_69,
inference(superposition,[],[f16481,f19116]) ).
fof(f19669,plain,
index_186 = index_69,
inference(forward_demodulation,[],[f19666,f163]) ).
fof(f19697,plain,
index_192 = index_69,
inference(forward_demodulation,[],[f19669,f5107]) ).
fof(f21397,plain,
index_95 = rselect_head(queue_76),
inference(forward_demodulation,[],[f5377,f5380]) ).
fof(f21398,plain,
index_69 = index_95,
inference(forward_demodulation,[],[f21397,f5375]) ).
fof(f21399,plain,
index_192 = index_95,
inference(forward_demodulation,[],[f21398,f19697]) ).
fof(f21475,plain,
s(index_192) = index_96,
inference(superposition,[],[f207,f21399]) ).
fof(f21476,plain,
index_116 = s(index_192),
inference(forward_demodulation,[],[f21475,f12844]) ).
fof(f21565,plain,
index_116 = index_195,
inference(superposition,[],[f167,f21476]) ).
fof(f21670,plain,
index_198 = index_116,
inference(forward_demodulation,[],[f21565,f568]) ).
fof(f21838,plain,
index_117 = s(index_198),
inference(superposition,[],[f134,f21670]) ).
fof(f22095,plain,
index_117 = index_201,
inference(superposition,[],[f169,f21838]) ).
fof(f22201,plain,
index_204 = index_117,
inference(forward_demodulation,[],[f22095,f567]) ).
fof(f22379,plain,
index_138 = s(index_204),
inference(superposition,[],[f13580,f22201]) ).
fof(f22958,plain,
index_138 = index_207,
inference(superposition,[],[f171,f22379]) ).
fof(f23065,plain,
index_9 = index_138,
inference(forward_demodulation,[],[f22958,f5105]) ).
fof(f23424,plain,
index_213 = s(index_9),
inference(superposition,[],[f14461,f23065]) ).
fof(f24157,plain,
index_213 = index_12,
inference(superposition,[],[f135,f23424]) ).
fof(f24217,plain,
index_15 = index_213,
inference(forward_demodulation,[],[f24157,f576]) ).
fof(f27491,plain,
( elem_214 = select(earray_148,index_15)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12822,f24217]) ).
fof(f27718,plain,
( elem_214 = select(earray_142,index_15)
| index_147 = index_15
| ~ spl0_2 ),
inference(superposition,[],[f6927,f27491]) ).
fof(f27719,plain,
( elem_214 = select(earray_142,index_15)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f27718,f12302]) ).
fof(f28664,plain,
( elem_214 = select(earray_133,index_15)
| index_141 = index_15
| ~ spl0_2 ),
inference(superposition,[],[f6926,f27719]) ).
fof(f28665,plain,
( elem_214 = select(earray_133,index_15)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f28664,f11584]) ).
fof(f29169,plain,
( elem_214 = select(earray_127,index_15)
| index_132 = index_15
| ~ spl0_2 ),
inference(superposition,[],[f6924,f28665]) ).
fof(f29170,plain,
( elem_214 = select(earray_127,index_15)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f29169,f11149]) ).
fof(f29221,plain,
( elem_214 = select(earray_121,index_15)
| index_126 = index_15
| ~ spl0_2 ),
inference(superposition,[],[f6923,f29170]) ).
fof(f29222,plain,
( elem_214 = select(earray_121,index_15)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f29221,f10434]) ).
fof(f29468,plain,
( elem_214 = select(earray_112,index_15)
| index_120 = index_15
| ~ spl0_2 ),
inference(superposition,[],[f6922,f29222]) ).
fof(f29469,plain,
( elem_214 = select(earray_112,index_15)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f29468,f9822]) ).
fof(f29769,plain,
( elem_214 = select(earray_106,index_15)
| index_111 = index_15
| ~ spl0_2 ),
inference(superposition,[],[f6921,f29469]) ).
fof(f29770,plain,
( elem_214 = select(earray_106,index_15)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f29769,f9214]) ).
fof(f30079,plain,
( elem_214 = select(earray_100,index_15)
| index_105 = index_15
| ~ spl0_2 ),
inference(superposition,[],[f6920,f29770]) ).
fof(f30080,plain,
( elem_214 = select(earray_100,index_15)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f30079,f8644]) ).
fof(f41051,plain,
! [X0] :
( select(earray_98,X0) = select(earray_64,X0)
| index_90 = X0
| index_84 = X0
| index_72 = X0 ),
inference(superposition,[],[f7012,f6943]) ).
fof(f46351,plain,
! [X0] :
( select(earray_98,X0) = select(earray_58,X0)
| index_90 = X0
| index_84 = X0
| index_72 = X0
| index_63 = X0 ),
inference(superposition,[],[f41051,f6942]) ).
fof(f52929,plain,
! [X0] :
( select(earray_98,X0) = select(earray_52,X0)
| index_90 = X0
| index_84 = X0
| index_72 = X0
| index_63 = X0
| index_57 = X0 ),
inference(superposition,[],[f46351,f6941]) ).
fof(f56981,plain,
! [X0] :
( select(earray_98,X0) = select(earray_43,X0)
| index_90 = X0
| index_84 = X0
| index_72 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0 ),
inference(superposition,[],[f52929,f6940]) ).
fof(f59351,plain,
! [X0] :
( select(earray_98,X0) = select(earray_37,X0)
| index_90 = X0
| index_84 = X0
| index_72 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0
| index_42 = X0 ),
inference(superposition,[],[f56981,f6939]) ).
fof(f63801,plain,
! [X0] :
( select(earray_98,X0) = select(earray_31,X0)
| index_90 = X0
| index_84 = X0
| index_72 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0
| index_42 = X0
| index_36 = X0 ),
inference(superposition,[],[f59351,f6938]) ).
fof(f67865,plain,
! [X0] :
( select(earray_98,X0) = select(earray_22,X0)
| index_90 = X0
| index_84 = X0
| index_72 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0
| index_42 = X0
| index_36 = X0
| index_30 = X0 ),
inference(superposition,[],[f63801,f6937]) ).
fof(f71127,plain,
! [X0] :
( select(earray_98,X0) = select(earray_16,X0)
| index_90 = X0
| index_84 = X0
| index_72 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0
| index_42 = X0
| index_36 = X0
| index_30 = X0
| index_21 = X0 ),
inference(superposition,[],[f67865,f6934]) ).
fof(f73950,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_90
| index_15 = index_84
| index_15 = index_72
| index_15 = index_63
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(superposition,[],[f903,f71127]) ).
fof(f73952,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_84
| index_15 = index_72
| index_15 = index_63
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73950,f7662]) ).
fof(f73954,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_72
| index_15 = index_63
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73952,f7156]) ).
fof(f73956,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_63
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73954,f6669]) ).
fof(f73958,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73956,f6265]) ).
fof(f73960,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73958,f5960]) ).
fof(f73962,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73960,f5709]) ).
fof(f73964,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73962,f5486]) ).
fof(f73966,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73964,f5235]) ).
fof(f73968,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f73966,f5397]) ).
fof(f73970,plain,
e10 = select(earray_98,index_15),
inference(forward_subsumption_resolution,[],[f73968,f1708]) ).
fof(f74160,plain,
( e10 = select(earray_100,index_15)
| index_99 = index_15 ),
inference(superposition,[],[f1188,f73970]) ).
fof(f74161,plain,
e10 = select(earray_100,index_15),
inference(forward_subsumption_resolution,[],[f74160,f8128]) ).
fof(f74256,plain,
( e10 = elem_214
| ~ spl0_2 ),
inference(superposition,[],[f74161,f30080]) ).
fof(f74260,plain,
( $false
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f74256,f312]) ).
fof(f74261,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f74260]) ).
fof(f74262,plain,
( index_15 = index_162
| ~ spl0_1 ),
inference(forward_demodulation,[],[f12818,f24217]) ).
fof(f74266,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f74262,f13151]) ).
fof(f74267,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f74266]) ).
cnf(s2,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f12824]) ).
cnf(s4,plain,
~ spl0_2,
inference(sat_conversion,[],[f74261]) ).
cnf(s5,plain,
~ spl0_1,
inference(sat_conversion,[],[f74267]) ).
cnf(s6,plain,
$false,
inference(rat,[],[s2,s4,s5]) ).
fof(f74268,plain,
$false,
inference(avatar_sat_refutation,[],[s6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n006.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:53:11 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.39/2.35 % (3913817)Will run a generic schedule for satisfiability detection.
% 14.39/2.35 % (3913826)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4183382091:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.39/2.35 % (3913823)% WARNING: option uhcvi not known.
% 14.39/2.35 % (3913824)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1734911739:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.39/2.35 % (3913822)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1997765938_2999 on theBenchmark for (2999ds/0Mi)
% 14.39/2.35 % (3913823)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=272494153:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.39/2.35 % (3913825)dis+10_1_sil=32000:sp=arity:random_seed=2073880882:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.39/2.35 % (3913827)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1728710250:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.39/2.35 % (3913828)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2333712836:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.39/2.35 % (3913826)Instruction limit reached!
% 14.39/2.35 % (3913826)------------------------------
% 14.39/2.35 % (3913826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.39/2.35 % (3913826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.39/2.35 % (3913826)CaDiCaL version: 2.1.3
% 14.39/2.35 % (3913826)Termination reason: Instruction limit
% 14.39/2.35 % (3913826)Termination phase: Saturation
% 14.39/2.35 % (3913826)Time elapsed: 0.029 s
% 14.39/2.35 % (3913826)Peak memory usage: 13 MB
% 14.39/2.35 % (3913826)Instructions burned: 117 (million)
% 14.39/2.35 % (3913836)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1253093670:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.39/2.35 % (3913825)Instruction limit reached!
% 14.39/2.35 % (3913825)------------------------------
% 14.39/2.35 % (3913825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.39/2.35 % (3913825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.39/2.35 % (3913825)CaDiCaL version: 2.1.3
% 14.39/2.35 % (3913825)Termination reason: Instruction limit
% 14.39/2.35 % (3913825)Termination phase: Saturation
% 14.39/2.35 % (3913825)Time elapsed: 0.048 s
% 14.39/2.35 % (3913825)Peak memory usage: 12 MB
% 14.39/2.35 % (3913825)Instructions burned: 104 (million)
% 14.39/2.35 % (3913827)Instruction limit reached!
% 14.39/2.35 % (3913827)------------------------------
% 14.39/2.35 % (3913827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.39/2.35 % (3913827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.39/2.35 % (3913827)CaDiCaL version: 2.1.3
% 14.39/2.35 % (3913827)Termination reason: Instruction limit
% 14.39/2.35 % (3913827)Termination phase: Saturation
% 14.39/2.35 % (3913827)Time elapsed: 0.062 s
% 14.39/2.35 % (3913827)Peak memory usage: 12 MB
% 14.39/2.35 % (3913827)Instructions burned: 139 (million)
% 14.39/2.35 % (3913838)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3624438873:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.39/2.35 % TRYING [1]
% 14.39/2.35 % TRYING [1]
% 14.39/2.35 % TRYING [2]
% 14.39/2.35 % TRYING [2]
% 14.39/2.35 % TRYING [3]
% 14.39/2.35 % (3913828)Instruction limit reached!
% 14.39/2.35 % (3913828)------------------------------
% 14.39/2.35 % (3913828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.39/2.35 % (3913828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.39/2.35 % (3913828)CaDiCaL version: 2.1.3
% 14.39/2.35 % (3913828)Termination reason: Instruction limit
% 14.39/2.35 % (3913828)Termination phase: Saturation
% 14.39/2.35 % (3913828)Time elapsed: 0.080 s
% 14.39/2.35 % (3913828)Peak memory usage: 13 MB
% 14.39/2.35 % (3913828)Instructions burned: 161 (million)
% 14.39/2.35 % (3913839)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1459117171:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.39/2.35 % TRYING [3]
% 14.39/2.35 % (3913841)ott-21_1_sil=16000:fs=off:random_seed=4134987107:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.39/2.35 % TRYING [4]
% 14.39/2.35 % (3913838)Instruction limit reached!
% 14.39/2.35 % (3913838)------------------------------
% 14.39/2.35 % (3913838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.39/2.35 % (3913838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913838)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913838)Termination reason: Instruction limit
% 11.59/2.51 % (3913838)Termination phase: Saturation
% 11.59/2.51 % (3913838)Time elapsed: 0.068 s
% 11.59/2.51 % (3913838)Peak memory usage: 13 MB
% 11.59/2.51 % (3913838)Instructions burned: 133 (million)
% 11.59/2.51 % TRYING [4]
% 11.59/2.51 % (3913844)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2738887375:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 11.59/2.51 % TRYING [5]
% 11.59/2.51 % (3913841)Instruction limit reached!
% 11.59/2.51 % (3913841)------------------------------
% 11.59/2.51 % (3913841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913841)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913841)Termination reason: Instruction limit
% 11.59/2.51 % (3913841)Termination phase: Saturation
% 11.59/2.51 % (3913841)Time elapsed: 0.076 s
% 11.59/2.51 % (3913841)Peak memory usage: 13 MB
% 11.59/2.51 % (3913841)Instructions burned: 182 (million)
% 11.59/2.51 % (3913836)Instruction limit reached!
% 11.59/2.51 % (3913836)------------------------------
% 11.59/2.51 % (3913836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913836)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913836)Termination reason: Instruction limit
% 11.59/2.51 % (3913836)Termination phase: Finite model building constraint generation
% 11.59/2.51 % (3913836)Time elapsed: 0.152 s
% 11.59/2.51 % (3913836)Peak memory usage: 33 MB
% 11.59/2.51 % (3913836)Instructions burned: 716 (million)
% 11.59/2.51 % (3913846)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2707163082:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 11.59/2.51 % (3913847)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1247114502:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 11.59/2.51 % TRYING [5]
% 11.59/2.51 % TRYING [1]
% 11.59/2.51 % TRYING [2]
% 11.59/2.51 % TRYING [3]
% 11.59/2.51 % (3913844)Instruction limit reached!
% 11.59/2.51 % (3913844)------------------------------
% 11.59/2.51 % (3913844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913844)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913844)Termination reason: Instruction limit
% 11.59/2.51 % (3913844)Termination phase: Saturation
% 11.59/2.51 % (3913844)Time elapsed: 0.211 s
% 11.59/2.51 % (3913844)Peak memory usage: 15 MB
% 11.59/2.51 % (3913844)Instructions burned: 478 (million)
% 11.59/2.51 % (3913839)Instruction limit reached!
% 11.59/2.51 % (3913839)------------------------------
% 11.59/2.51 % (3913839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913839)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913839)Termination reason: Instruction limit
% 11.59/2.51 % (3913839)Termination phase: Saturation
% 11.59/2.51 % (3913839)Time elapsed: 0.289 s
% 11.59/2.51 % (3913839)Peak memory usage: 18 MB
% 11.59/2.51 % (3913839)Instructions burned: 684 (million)
% 11.59/2.51 % (3913850)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3798592046:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 11.59/2.51 % (3913851)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3449962907:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 11.59/2.51 % (3913847)Instruction limit reached!
% 11.59/2.51 % (3913847)------------------------------
% 11.59/2.51 % (3913847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913847)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913847)Termination reason: Instruction limit
% 11.59/2.51 % (3913847)Termination phase: Saturation
% 11.59/2.51 % (3913847)Time elapsed: 0.252 s
% 11.59/2.51 % (3913847)Peak memory usage: 19 MB
% 11.59/2.51 % (3913847)Instructions burned: 1184 (million)
% 11.59/2.51 % TRYING [4]
% 11.59/2.51 % (3913854)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=283201070:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 11.59/2.51 % TRYING [6]
% 11.59/2.51 % (3913846)Instruction limit reached!
% 11.59/2.51 % (3913846)------------------------------
% 11.59/2.51 % (3913846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913846)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913846)Termination reason: Instruction limit
% 11.59/2.51 % (3913846)Termination phase: Finite model building SAT solving
% 11.59/2.51 % (3913846)Time elapsed: 0.362 s
% 11.59/2.51 % (3913846)Peak memory usage: 29 MB
% 11.59/2.51 % (3913846)Instructions burned: 866 (million)
% 11.59/2.51 % (3913856)fmb+10_1_sil=64000:random_seed=3599643619:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 11.59/2.51 % TRYING [14]
% 11.59/2.51 % TRYING [1]
% 11.59/2.51 % (3913854)Instruction limit reached!
% 11.59/2.51 % (3913854)------------------------------
% 11.59/2.51 % (3913854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913854)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913854)Termination reason: Instruction limit
% 11.59/2.51 % (3913854)Termination phase: Saturation
% 11.59/2.51 % (3913854)Time elapsed: 0.197 s
% 11.59/2.51 % (3913854)Peak memory usage: 16 MB
% 11.59/2.51 % (3913854)Instructions burned: 879 (million)
% 11.59/2.51 % TRYING [2]
% 11.59/2.51 % (3913858)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1651699865:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 11.59/2.51 % (3913851)Instruction limit reached!
% 11.59/2.51 % (3913851)------------------------------
% 11.59/2.51 % (3913851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913851)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913851)Termination reason: Instruction limit
% 11.59/2.51 % (3913851)Termination phase: Saturation
% 11.59/2.51 % (3913851)Time elapsed: 0.296 s
% 11.59/2.51 % (3913851)Peak memory usage: 17 MB
% 11.59/2.51 % (3913851)Instructions burned: 693 (million)
% 11.59/2.51 % TRYING [3]
% 11.59/2.51 % (3913860)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1572406816:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 11.59/2.51 % TRYING [20]
% 11.59/2.51 % (3913850)Instruction limit reached!
% 11.59/2.51 % (3913850)------------------------------
% 11.59/2.51 % (3913850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913850)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913850)Termination reason: Instruction limit
% 11.59/2.51 % (3913850)Termination phase: Finite model building constraint generation
% 11.59/2.51 % (3913850)Time elapsed: 0.363 s
% 11.59/2.51 % (3913850)Peak memory usage: 77 MB
% 11.59/2.51 % (3913850)Instructions burned: 891 (million)
% 11.59/2.51 % (3913862)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3282523879:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 11.59/2.51 % TRYING [8]
% 11.59/2.51 % TRYING [4]
% 11.59/2.51 % TRYING [7]
% 11.59/2.51 % (3913860)Instruction limit reached!
% 11.59/2.51 % (3913860)------------------------------
% 11.59/2.51 % (3913860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913860)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913860)Termination reason: Instruction limit
% 11.59/2.51 % (3913860)Termination phase: Finite model building constraint generation
% 11.59/2.51 % (3913860)Time elapsed: 0.375 s
% 11.59/2.51 % (3913860)Peak memory usage: 87 MB
% 11.59/2.51 % (3913860)Instructions burned: 921 (million)
% 11.59/2.51 % (3913864)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2481691625:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 11.59/2.51 % TRYING [5]
% 11.59/2.51 % (3913864)Instruction limit reached!
% 11.59/2.51 % (3913864)------------------------------
% 11.59/2.51 % (3913864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.51 % (3913864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.51 % (3913864)CaDiCaL version: 2.1.3
% 11.59/2.51 % (3913864)Termination reason: Instruction limit
% 11.59/2.51 % (3913864)Termination phase: Saturation
% 11.59/2.51 % (3913864)Time elapsed: 0.659 s
% 11.59/2.51 % (3913864)Peak memory usage: 28 MB
% 11.59/2.51 % (3913864)Instructions burned: 1473 (million)
% 11.59/2.51 % (3913866)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=712392869:i=6324_2981 on theBenchmark for (2981ds/6324Mi)
% 11.59/2.51 % TRYING [77]
% 11.59/2.51 % TRYING [8]
% 11.59/2.51 % (3913823) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3913817-3913823"...
% 11.59/2.51 % (3913862) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3913817-3913862"...
% 11.59/2.51 % (3913823)...printing done.
% 11.59/2.51 % (3913823)Refutation found. Thanks to Tanya!
% 11.59/2.51 % SZS status Unsatisfiable for theBenchmark
% 11.59/2.51 % SZS output start Proof for theBenchmark
% See solution above
% 11.59/2.53 % (3913823)------------------------------
% 11.59/2.53 % (3913823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.59/2.53 % (3913823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.59/2.53 % (3913823)CaDiCaL version: 2.1.3
% 11.59/2.53 % (3913823)Termination reason: Refutation
% 11.59/2.53 % (3913823)Time elapsed: 2.166 s
% 11.59/2.53 % (3913823)Peak memory usage: 32 MB
% 11.59/2.53 % (3913823)Instructions burned: 5280 (million)
% 11.59/2.53 % (3913817)Success in time 2.28 s
% 11.59/2.53 % Vampire exiting
%------------------------------------------------------------------------------