%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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 : Fri Sep 25 03:23:46 PM UTC 2026
% Result : Unsatisfiable 19.00s 13.35s
% Output : CNFRefutation 19.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 256
% Syntax : Number of formulae : 1026 ( 966 unt; 0 def)
% Number of atoms : 1175 (1174 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 230 ( 81 ~; 149 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 1 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 268 ( 268 usr; 259 con; 0-3 aty)
% Number of variables : 136 ( 0 sgn 136 !; 0 ?; 88 :)
% 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(f82,axiom,
earray_152 = rselect_seq(q2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
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(f120,axiom,
earray_8 = rselect_seq(q9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp55) ).
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(f321,plain,
earray_152 = rselect_seq(queue_82),
inference(definition_unfolding,[],[f82,f292]) ).
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(f340,plain,
earray_8 = rselect_seq(queue_211),
inference(definition_unfolding,[],[f120,f310]) ).
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]) ).
tcf(c_357,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_358,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X1 = X3 )
| ( select(store(X0,X1,X2),X3) = select(X0,X3) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_359,plain,
! [X0: $i,X1: $i] : rselect_seq(rstore_seq(X0,X1)) = X1,
inference(cnf_transformation,[],[f3]) ).
tcf(c_360,plain,
! [X0: $i,X1: $i] : rselect_head(rstore_head(X0,X1)) = X1,
inference(cnf_transformation,[],[f4]) ).
tcf(c_361,plain,
! [X0: $i,X1: $i] : rselect_tail(rstore_tail(X0,X1)) = X1,
inference(cnf_transformation,[],[f5]) ).
tcf(c_362,plain,
! [X0: $i,X1: $i] : rselect_seq(rstore_head(X0,X1)) = rselect_seq(X0),
inference(cnf_transformation,[],[f6]) ).
tcf(c_363,plain,
! [X0: $i,X1: $i] : rselect_seq(rstore_tail(X0,X1)) = rselect_seq(X0),
inference(cnf_transformation,[],[f8]) ).
tcf(c_364,plain,
! [X0: $i,X1: $i] : rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[],[f9]) ).
tcf(c_365,plain,
! [X0: $i,X1: $i] : rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[],[f11]) ).
tcf(c_367,plain,
! [X0: $i,X1: $i] : rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
inference(cnf_transformation,[],[f14]) ).
tcf(c_399,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))) != X0,
inference(cnf_transformation,[],[f46]) ).
tcf(c_400,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))) != X0,
inference(cnf_transformation,[],[f47]) ).
tcf(c_401,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))) != X0,
inference(cnf_transformation,[],[f48]) ).
tcf(c_402,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))) != X0,
inference(cnf_transformation,[],[f49]) ).
tcf(c_403,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
inference(cnf_transformation,[],[f50]) ).
tcf(c_404,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
inference(cnf_transformation,[],[f51]) ).
tcf(c_405,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
inference(cnf_transformation,[],[f52]) ).
tcf(c_406,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(cnf_transformation,[],[f53]) ).
tcf(c_407,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(cnf_transformation,[],[f54]) ).
tcf(c_408,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(cnf_transformation,[],[f55]) ).
tcf(c_409,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(cnf_transformation,[],[f56]) ).
tcf(c_410,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(cnf_transformation,[],[f57]) ).
tcf(c_411,plain,
! [X0: $i] : s(s(s(s(s(s(s(X0))))))) != X0,
inference(cnf_transformation,[],[f58]) ).
tcf(c_412,plain,
! [X0: $i] : s(s(s(s(s(s(X0)))))) != X0,
inference(cnf_transformation,[],[f59]) ).
tcf(c_413,plain,
! [X0: $i] : s(s(s(s(s(X0))))) != X0,
inference(cnf_transformation,[],[f60]) ).
tcf(c_414,plain,
! [X0: $i] : s(s(s(s(X0)))) != X0,
inference(cnf_transformation,[],[f61]) ).
tcf(c_415,plain,
! [X0: $i] : s(s(s(X0))) != X0,
inference(cnf_transformation,[],[f62]) ).
tcf(c_416,plain,
! [X0: $i] : s(s(X0)) != X0,
inference(cnf_transformation,[],[f63]) ).
tcf(c_417,plain,
! [X0: $i] : s(X0) != X0,
inference(cnf_transformation,[],[f64]) ).
tcf(c_419,plain,
store(earray_98,index_99,e21) = earray_100,
inference(cnf_transformation,[],[f66]) ).
tcf(c_420,plain,
rselect_seq(queue_103) = earray_104,
inference(cnf_transformation,[],[f313]) ).
tcf(c_421,plain,
store(earray_104,index_105,e22) = earray_106,
inference(cnf_transformation,[],[f68]) ).
tcf(c_422,plain,
rselect_seq(queue_109) = earray_110,
inference(cnf_transformation,[],[f314]) ).
tcf(c_423,plain,
store(earray_110,index_111,e23) = earray_112,
inference(cnf_transformation,[],[f70]) ).
tcf(c_424,plain,
rselect_seq(queue_118) = earray_119,
inference(cnf_transformation,[],[f315]) ).
tcf(c_425,plain,
store(earray_119,index_120,e24) = earray_121,
inference(cnf_transformation,[],[f72]) ).
tcf(c_426,plain,
rselect_seq(queue_124) = earray_125,
inference(cnf_transformation,[],[f316]) ).
tcf(c_427,plain,
store(earray_125,index_126,e25) = earray_127,
inference(cnf_transformation,[],[f74]) ).
tcf(c_428,plain,
rselect_seq(queue_130) = earray_131,
inference(cnf_transformation,[],[f317]) ).
tcf(c_429,plain,
store(earray_131,index_132,e26) = earray_133,
inference(cnf_transformation,[],[f76]) ).
tcf(c_431,plain,
rselect_seq(queue_139) = earray_140,
inference(cnf_transformation,[],[f319]) ).
tcf(c_432,plain,
store(earray_140,index_141,e27) = earray_142,
inference(cnf_transformation,[],[f79]) ).
tcf(c_433,plain,
rselect_seq(queue_145) = earray_146,
inference(cnf_transformation,[],[f320]) ).
tcf(c_434,plain,
store(earray_146,index_147,e28) = earray_148,
inference(cnf_transformation,[],[f81]) ).
tcf(c_435,plain,
rselect_seq(queue_82) = earray_152,
inference(cnf_transformation,[],[f321]) ).
tcf(c_437,plain,
store(earray_14,index_15,e10) = earray_16,
inference(cnf_transformation,[],[f84]) ).
tcf(c_438,plain,
rselect_seq(queue_151) = earray_161,
inference(cnf_transformation,[],[f322]) ).
tcf(c_439,plain,
store(earray_161,index_162,e29) = earray_163,
inference(cnf_transformation,[],[f86]) ).
tcf(c_451,plain,
rselect_seq(queue_19) = earray_20,
inference(cnf_transformation,[],[f329]) ).
tcf(c_454,plain,
rselect_seq(queue_169) = earray_212,
inference(cnf_transformation,[],[f331]) ).
tcf(c_455,plain,
store(earray_20,index_21,e11) = earray_22,
inference(cnf_transformation,[],[f102]) ).
tcf(c_456,plain,
rselect_seq(queue_28) = earray_29,
inference(cnf_transformation,[],[f332]) ).
tcf(c_457,plain,
store(earray_29,index_30,e12) = earray_31,
inference(cnf_transformation,[],[f104]) ).
tcf(c_458,plain,
rselect_seq(queue_34) = earray_35,
inference(cnf_transformation,[],[f333]) ).
tcf(c_459,plain,
store(earray_35,index_36,e13) = earray_37,
inference(cnf_transformation,[],[f106]) ).
tcf(c_461,plain,
rselect_seq(queue_40) = earray_41,
inference(cnf_transformation,[],[f334]) ).
tcf(c_462,plain,
store(earray_41,index_42,e14) = earray_43,
inference(cnf_transformation,[],[f109]) ).
tcf(c_463,plain,
rselect_seq(queue_49) = earray_50,
inference(cnf_transformation,[],[f335]) ).
tcf(c_464,plain,
store(earray_50,index_51,e15) = earray_52,
inference(cnf_transformation,[],[f111]) ).
tcf(c_465,plain,
rselect_seq(queue_55) = earray_56,
inference(cnf_transformation,[],[f336]) ).
tcf(c_466,plain,
store(earray_56,index_57,e16) = earray_58,
inference(cnf_transformation,[],[f113]) ).
tcf(c_467,plain,
rselect_seq(queue_61) = earray_62,
inference(cnf_transformation,[],[f337]) ).
tcf(c_468,plain,
store(earray_62,index_63,e17) = earray_64,
inference(cnf_transformation,[],[f115]) ).
tcf(c_469,plain,
rselect_seq(queue_70) = earray_71,
inference(cnf_transformation,[],[f338]) ).
tcf(c_470,plain,
store(earray_71,index_72,e18) = earray_73,
inference(cnf_transformation,[],[f117]) ).
tcf(c_473,plain,
rselect_seq(queue_211) = earray_8,
inference(cnf_transformation,[],[f340]) ).
tcf(c_474,plain,
rselect_seq(queue_76) = earray_83,
inference(cnf_transformation,[],[f341]) ).
tcf(c_475,plain,
store(earray_83,index_84,e19) = earray_85,
inference(cnf_transformation,[],[f122]) ).
tcf(c_476,plain,
rselect_seq(queue_88) = earray_89,
inference(cnf_transformation,[],[f342]) ).
tcf(c_477,plain,
store(earray_89,index_90,e20) = earray_91,
inference(cnf_transformation,[],[f124]) ).
tcf(c_478,plain,
rselect_seq(queue_97) = earray_98,
inference(cnf_transformation,[],[f343]) ).
tcf(c_479,plain,
select(earray_212,index_213) = elem_214,
inference(cnf_transformation,[],[f126]) ).
tcf(c_480,plain,
rselect_tail(q) = index_0,
inference(cnf_transformation,[],[f127]) ).
tcf(c_481,plain,
s(index_99) = index_102,
inference(cnf_transformation,[],[f128]) ).
tcf(c_482,plain,
rselect_tail(queue_103) = index_105,
inference(cnf_transformation,[],[f344]) ).
tcf(c_483,plain,
s(index_105) = index_108,
inference(cnf_transformation,[],[f130]) ).
tcf(c_484,plain,
rselect_tail(queue_109) = index_111,
inference(cnf_transformation,[],[f345]) ).
tcf(c_485,plain,
s(index_111) = index_114,
inference(cnf_transformation,[],[f132]) ).
tcf(c_486,plain,
rselect_head(queue_115) = index_116,
inference(cnf_transformation,[],[f133]) ).
tcf(c_487,plain,
s(index_116) = index_117,
inference(cnf_transformation,[],[f134]) ).
tcf(c_488,plain,
s(index_9) = index_12,
inference(cnf_transformation,[],[f135]) ).
tcf(c_489,plain,
rselect_tail(queue_118) = index_120,
inference(cnf_transformation,[],[f346]) ).
tcf(c_490,plain,
s(index_120) = index_123,
inference(cnf_transformation,[],[f137]) ).
tcf(c_491,plain,
rselect_tail(queue_124) = index_126,
inference(cnf_transformation,[],[f347]) ).
tcf(c_492,plain,
s(index_126) = index_129,
inference(cnf_transformation,[],[f139]) ).
tcf(c_493,plain,
rselect_tail(queue_130) = index_132,
inference(cnf_transformation,[],[f348]) ).
tcf(c_494,plain,
s(index_132) = index_135,
inference(cnf_transformation,[],[f141]) ).
tcf(c_495,plain,
rselect_head(queue_136) = index_137,
inference(cnf_transformation,[],[f142]) ).
tcf(c_496,plain,
s(index_137) = index_138,
inference(cnf_transformation,[],[f143]) ).
tcf(c_497,plain,
rselect_tail(queue_139) = index_141,
inference(cnf_transformation,[],[f349]) ).
tcf(c_498,plain,
s(index_141) = index_144,
inference(cnf_transformation,[],[f145]) ).
tcf(c_499,plain,
rselect_tail(queue_145) = index_147,
inference(cnf_transformation,[],[f350]) ).
tcf(c_500,plain,
rselect_tail(queue_13) = index_15,
inference(cnf_transformation,[],[f351]) ).
tcf(c_501,plain,
s(index_147) = index_150,
inference(cnf_transformation,[],[f148]) ).
tcf(c_502,plain,
rselect_tail(queue_82) = index_153,
inference(cnf_transformation,[],[f352]) ).
tcf(c_503,plain,
s(index_153) = index_156,
inference(cnf_transformation,[],[f150]) ).
tcf(c_504,plain,
rselect_head(queue_157) = index_158,
inference(cnf_transformation,[],[f151]) ).
tcf(c_505,plain,
s(index_158) = index_159,
inference(cnf_transformation,[],[f152]) ).
tcf(c_506,plain,
rselect_tail(queue_151) = index_162,
inference(cnf_transformation,[],[f353]) ).
tcf(c_508,plain,
rselect_head(queue_166) = index_167,
inference(cnf_transformation,[],[f155]) ).
tcf(c_509,plain,
s(index_167) = index_168,
inference(cnf_transformation,[],[f156]) ).
tcf(c_510,plain,
rselect_tail(queue_160) = index_171,
inference(cnf_transformation,[],[f354]) ).
tcf(c_511,plain,
s(index_171) = index_174,
inference(cnf_transformation,[],[f158]) ).
tcf(c_512,plain,
rselect_tail(queue_175) = index_177,
inference(cnf_transformation,[],[f355]) ).
tcf(c_513,plain,
s(index_15) = index_18,
inference(cnf_transformation,[],[f160]) ).
tcf(c_514,plain,
s(index_177) = index_180,
inference(cnf_transformation,[],[f161]) ).
tcf(c_515,plain,
rselect_tail(queue_181) = index_183,
inference(cnf_transformation,[],[f356]) ).
tcf(c_516,plain,
s(index_183) = index_186,
inference(cnf_transformation,[],[f163]) ).
tcf(c_517,plain,
rselect_head(queue_187) = index_188,
inference(cnf_transformation,[],[f164]) ).
tcf(c_518,plain,
s(index_188) = index_189,
inference(cnf_transformation,[],[f165]) ).
tcf(c_519,plain,
rselect_tail(queue_190) = index_192,
inference(cnf_transformation,[],[f357]) ).
tcf(c_520,plain,
s(index_192) = index_195,
inference(cnf_transformation,[],[f167]) ).
tcf(c_521,plain,
rselect_tail(queue_196) = index_198,
inference(cnf_transformation,[],[f358]) ).
tcf(c_522,plain,
s(index_198) = index_201,
inference(cnf_transformation,[],[f169]) ).
tcf(c_523,plain,
rselect_tail(queue_202) = index_204,
inference(cnf_transformation,[],[f359]) ).
tcf(c_524,plain,
s(index_204) = index_207,
inference(cnf_transformation,[],[f171]) ).
tcf(c_525,plain,
rselect_head(queue_208) = index_209,
inference(cnf_transformation,[],[f172]) ).
tcf(c_526,plain,
rselect_tail(queue_19) = index_21,
inference(cnf_transformation,[],[f360]) ).
tcf(c_527,plain,
s(index_209) = index_210,
inference(cnf_transformation,[],[f174]) ).
tcf(c_528,plain,
rselect_head(queue_169) = index_213,
inference(cnf_transformation,[],[f361]) ).
tcf(c_529,plain,
s(index_21) = index_24,
inference(cnf_transformation,[],[f176]) ).
tcf(c_530,plain,
rselect_head(queue_25) = index_26,
inference(cnf_transformation,[],[f177]) ).
tcf(c_531,plain,
s(index_26) = index_27,
inference(cnf_transformation,[],[f178]) ).
tcf(c_532,plain,
rselect_tail(queue_1) = index_3,
inference(cnf_transformation,[],[f362]) ).
tcf(c_533,plain,
rselect_tail(queue_28) = index_30,
inference(cnf_transformation,[],[f363]) ).
tcf(c_534,plain,
s(index_30) = index_33,
inference(cnf_transformation,[],[f181]) ).
tcf(c_535,plain,
rselect_tail(queue_34) = index_36,
inference(cnf_transformation,[],[f364]) ).
tcf(c_536,plain,
s(index_36) = index_39,
inference(cnf_transformation,[],[f183]) ).
tcf(c_537,plain,
rselect_tail(queue_40) = index_42,
inference(cnf_transformation,[],[f365]) ).
tcf(c_538,plain,
s(index_42) = index_45,
inference(cnf_transformation,[],[f185]) ).
tcf(c_539,plain,
rselect_head(queue_46) = index_47,
inference(cnf_transformation,[],[f186]) ).
tcf(c_540,plain,
s(index_47) = index_48,
inference(cnf_transformation,[],[f187]) ).
tcf(c_541,plain,
rselect_tail(queue_49) = index_51,
inference(cnf_transformation,[],[f366]) ).
tcf(c_542,plain,
s(index_51) = index_54,
inference(cnf_transformation,[],[f189]) ).
tcf(c_543,plain,
rselect_tail(queue_55) = index_57,
inference(cnf_transformation,[],[f367]) ).
tcf(c_544,plain,
s(index_3) = index_6,
inference(cnf_transformation,[],[f191]) ).
tcf(c_545,plain,
s(index_57) = index_60,
inference(cnf_transformation,[],[f192]) ).
tcf(c_546,plain,
rselect_tail(queue_61) = index_63,
inference(cnf_transformation,[],[f368]) ).
tcf(c_547,plain,
s(index_63) = index_66,
inference(cnf_transformation,[],[f194]) ).
tcf(c_548,plain,
rselect_head(queue_67) = index_68,
inference(cnf_transformation,[],[f195]) ).
tcf(c_549,plain,
s(index_68) = index_69,
inference(cnf_transformation,[],[f196]) ).
tcf(c_550,plain,
rselect_tail(queue_70) = index_72,
inference(cnf_transformation,[],[f369]) ).
tcf(c_551,plain,
s(index_72) = index_75,
inference(cnf_transformation,[],[f198]) ).
tcf(c_552,plain,
rselect_tail(queue_7) = index_78,
inference(cnf_transformation,[],[f370]) ).
tcf(c_553,plain,
s(index_78) = index_81,
inference(cnf_transformation,[],[f200]) ).
tcf(c_554,plain,
rselect_tail(queue_76) = index_84,
inference(cnf_transformation,[],[f371]) ).
tcf(c_555,plain,
s(index_84) = index_87,
inference(cnf_transformation,[],[f202]) ).
tcf(c_556,plain,
rselect_tail(queue_211) = index_9,
inference(cnf_transformation,[],[f372]) ).
tcf(c_557,plain,
rselect_tail(queue_88) = index_90,
inference(cnf_transformation,[],[f373]) ).
tcf(c_558,plain,
s(index_90) = index_93,
inference(cnf_transformation,[],[f205]) ).
tcf(c_559,plain,
rselect_head(queue_94) = index_95,
inference(cnf_transformation,[],[f206]) ).
tcf(c_560,plain,
s(index_95) = index_96,
inference(cnf_transformation,[],[f207]) ).
tcf(c_561,plain,
rselect_tail(queue_97) = index_99,
inference(cnf_transformation,[],[f374]) ).
tcf(c_562,plain,
rstore_head(q,index_0) = queue_1,
inference(cnf_transformation,[],[f209]) ).
tcf(c_563,plain,
rstore_seq(queue_97,earray_100) = queue_101,
inference(cnf_transformation,[],[f375]) ).
tcf(c_564,plain,
rstore_tail(queue_101,index_102) = queue_103,
inference(cnf_transformation,[],[f211]) ).
tcf(c_565,plain,
rstore_seq(queue_103,earray_106) = queue_107,
inference(cnf_transformation,[],[f376]) ).
tcf(c_566,plain,
rstore_tail(queue_107,index_108) = queue_109,
inference(cnf_transformation,[],[f213]) ).
tcf(c_567,plain,
rstore_seq(queue_211,earray_10) = queue_11,
inference(cnf_transformation,[],[f377]) ).
tcf(c_568,plain,
rstore_seq(queue_109,earray_112) = queue_113,
inference(cnf_transformation,[],[f378]) ).
tcf(c_569,plain,
rstore_tail(queue_113,index_114) = queue_115,
inference(cnf_transformation,[],[f216]) ).
tcf(c_570,plain,
rstore_head(queue_115,index_117) = queue_118,
inference(cnf_transformation,[],[f217]) ).
tcf(c_571,plain,
rstore_seq(queue_118,earray_121) = queue_122,
inference(cnf_transformation,[],[f379]) ).
tcf(c_572,plain,
rstore_tail(queue_122,index_123) = queue_124,
inference(cnf_transformation,[],[f219]) ).
tcf(c_573,plain,
rstore_seq(queue_124,earray_127) = queue_128,
inference(cnf_transformation,[],[f380]) ).
tcf(c_574,plain,
rstore_tail(queue_11,index_12) = queue_13,
inference(cnf_transformation,[],[f221]) ).
tcf(c_575,plain,
rstore_tail(queue_128,index_129) = queue_130,
inference(cnf_transformation,[],[f222]) ).
tcf(c_576,plain,
rstore_seq(queue_130,earray_133) = queue_134,
inference(cnf_transformation,[],[f381]) ).
tcf(c_577,plain,
rstore_tail(queue_134,index_135) = queue_136,
inference(cnf_transformation,[],[f224]) ).
tcf(c_578,plain,
rstore_head(queue_136,index_138) = queue_139,
inference(cnf_transformation,[],[f225]) ).
tcf(c_579,plain,
rstore_seq(queue_139,earray_142) = queue_143,
inference(cnf_transformation,[],[f382]) ).
tcf(c_580,plain,
rstore_tail(queue_143,index_144) = queue_145,
inference(cnf_transformation,[],[f227]) ).
tcf(c_581,plain,
rstore_seq(queue_145,earray_148) = queue_149,
inference(cnf_transformation,[],[f383]) ).
tcf(c_582,plain,
rstore_tail(queue_149,index_150) = queue_151,
inference(cnf_transformation,[],[f229]) ).
tcf(c_583,plain,
rstore_seq(queue_82,earray_154) = queue_155,
inference(cnf_transformation,[],[f384]) ).
tcf(c_584,plain,
rstore_tail(queue_155,index_156) = queue_157,
inference(cnf_transformation,[],[f231]) ).
tcf(c_585,plain,
rstore_head(queue_157,index_159) = queue_160,
inference(cnf_transformation,[],[f232]) ).
tcf(c_586,plain,
rstore_seq(queue_151,earray_163) = queue_164,
inference(cnf_transformation,[],[f385]) ).
tcf(c_587,plain,
rstore_tail(queue_164,index_165) = queue_166,
inference(cnf_transformation,[],[f234]) ).
tcf(c_588,plain,
rstore_head(queue_166,index_168) = queue_169,
inference(cnf_transformation,[],[f235]) ).
tcf(c_589,plain,
rstore_seq(queue_13,earray_16) = queue_17,
inference(cnf_transformation,[],[f386]) ).
tcf(c_590,plain,
rstore_seq(queue_160,earray_172) = queue_173,
inference(cnf_transformation,[],[f387]) ).
tcf(c_591,plain,
rstore_tail(queue_173,index_174) = queue_175,
inference(cnf_transformation,[],[f238]) ).
tcf(c_592,plain,
rstore_seq(queue_175,earray_178) = queue_179,
inference(cnf_transformation,[],[f388]) ).
tcf(c_593,plain,
rstore_tail(queue_179,index_180) = queue_181,
inference(cnf_transformation,[],[f240]) ).
tcf(c_594,plain,
rstore_seq(queue_181,earray_184) = queue_185,
inference(cnf_transformation,[],[f389]) ).
tcf(c_595,plain,
rstore_tail(queue_185,index_186) = queue_187,
inference(cnf_transformation,[],[f242]) ).
tcf(c_596,plain,
rstore_tail(queue_17,index_18) = queue_19,
inference(cnf_transformation,[],[f243]) ).
tcf(c_597,plain,
rstore_head(queue_187,index_189) = queue_190,
inference(cnf_transformation,[],[f244]) ).
tcf(c_598,plain,
rstore_seq(queue_190,earray_193) = queue_194,
inference(cnf_transformation,[],[f390]) ).
tcf(c_599,plain,
rstore_tail(queue_194,index_195) = queue_196,
inference(cnf_transformation,[],[f246]) ).
tcf(c_600,plain,
rstore_seq(queue_196,earray_199) = queue_200,
inference(cnf_transformation,[],[f391]) ).
tcf(c_601,plain,
rstore_tail(queue_200,index_201) = queue_202,
inference(cnf_transformation,[],[f248]) ).
tcf(c_602,plain,
rstore_seq(queue_202,earray_205) = queue_206,
inference(cnf_transformation,[],[f392]) ).
tcf(c_603,plain,
rstore_tail(queue_206,index_207) = queue_208,
inference(cnf_transformation,[],[f250]) ).
tcf(c_604,plain,
rstore_head(queue_208,index_210) = queue_211,
inference(cnf_transformation,[],[f251]) ).
tcf(c_605,plain,
rstore_seq(queue_19,earray_22) = queue_23,
inference(cnf_transformation,[],[f393]) ).
tcf(c_606,plain,
rstore_tail(queue_23,index_24) = queue_25,
inference(cnf_transformation,[],[f253]) ).
tcf(c_607,plain,
rstore_head(queue_25,index_27) = queue_28,
inference(cnf_transformation,[],[f254]) ).
tcf(c_608,plain,
rstore_seq(queue_28,earray_31) = queue_32,
inference(cnf_transformation,[],[f394]) ).
tcf(c_609,plain,
rstore_tail(queue_32,index_33) = queue_34,
inference(cnf_transformation,[],[f256]) ).
tcf(c_610,plain,
rstore_seq(queue_34,earray_37) = queue_38,
inference(cnf_transformation,[],[f395]) ).
tcf(c_611,plain,
rstore_tail(queue_38,index_39) = queue_40,
inference(cnf_transformation,[],[f258]) ).
tcf(c_612,plain,
rstore_seq(queue_40,earray_43) = queue_44,
inference(cnf_transformation,[],[f396]) ).
tcf(c_613,plain,
rstore_tail(queue_44,index_45) = queue_46,
inference(cnf_transformation,[],[f260]) ).
tcf(c_614,plain,
rstore_head(queue_46,index_48) = queue_49,
inference(cnf_transformation,[],[f261]) ).
tcf(c_615,plain,
rstore_seq(queue_1,earray_4) = queue_5,
inference(cnf_transformation,[],[f397]) ).
tcf(c_616,plain,
rstore_seq(queue_49,earray_52) = queue_53,
inference(cnf_transformation,[],[f398]) ).
tcf(c_617,plain,
rstore_tail(queue_53,index_54) = queue_55,
inference(cnf_transformation,[],[f264]) ).
tcf(c_618,plain,
rstore_seq(queue_55,earray_58) = queue_59,
inference(cnf_transformation,[],[f399]) ).
tcf(c_619,plain,
rstore_tail(queue_59,index_60) = queue_61,
inference(cnf_transformation,[],[f266]) ).
tcf(c_620,plain,
rstore_seq(queue_61,earray_64) = queue_65,
inference(cnf_transformation,[],[f400]) ).
tcf(c_621,plain,
rstore_tail(queue_65,index_66) = queue_67,
inference(cnf_transformation,[],[f268]) ).
tcf(c_622,plain,
rstore_tail(queue_5,index_6) = queue_7,
inference(cnf_transformation,[],[f269]) ).
tcf(c_623,plain,
rstore_head(queue_67,index_69) = queue_70,
inference(cnf_transformation,[],[f270]) ).
tcf(c_624,plain,
rstore_seq(queue_70,earray_73) = queue_74,
inference(cnf_transformation,[],[f401]) ).
tcf(c_625,plain,
rstore_tail(queue_74,index_75) = queue_76,
inference(cnf_transformation,[],[f272]) ).
tcf(c_626,plain,
rstore_seq(queue_7,earray_79) = queue_80,
inference(cnf_transformation,[],[f402]) ).
tcf(c_627,plain,
rstore_tail(queue_80,index_81) = queue_82,
inference(cnf_transformation,[],[f274]) ).
tcf(c_628,plain,
rstore_seq(queue_76,earray_85) = queue_86,
inference(cnf_transformation,[],[f403]) ).
tcf(c_629,plain,
rstore_tail(queue_86,index_87) = queue_88,
inference(cnf_transformation,[],[f276]) ).
tcf(c_630,plain,
rstore_seq(queue_88,earray_91) = queue_92,
inference(cnf_transformation,[],[f404]) ).
tcf(c_631,plain,
rstore_tail(queue_92,index_93) = queue_94,
inference(cnf_transformation,[],[f278]) ).
tcf(c_632,plain,
rstore_head(queue_94,index_96) = queue_97,
inference(cnf_transformation,[],[f279]) ).
tcf(c_633,negated_conjecture,
e10 != elem_214,
inference(cnf_transformation,[],[f312]) ).
tcf(c_1264,negated_conjecture,
e10 != elem_214,
inference(demodulation,[status(thm)],[c_633]) ).
tcf(c_1898,plain,
select(earray_16,index_15) = e10,
inference(superposition,[status(thm)],[c_437,c_357]) ).
tcf(c_1929,plain,
index_15 != index_18,
inference(superposition,[status(thm)],[c_513,c_417]) ).
tcf(c_1953,plain,
rselect_seq(queue_101) = earray_100,
inference(superposition,[status(thm)],[c_563,c_359]) ).
tcf(c_1954,plain,
rselect_seq(queue_107) = earray_106,
inference(superposition,[status(thm)],[c_565,c_359]) ).
tcf(c_1956,plain,
rselect_seq(queue_113) = earray_112,
inference(superposition,[status(thm)],[c_568,c_359]) ).
tcf(c_1957,plain,
rselect_seq(queue_122) = earray_121,
inference(superposition,[status(thm)],[c_571,c_359]) ).
tcf(c_1958,plain,
rselect_seq(queue_128) = earray_127,
inference(superposition,[status(thm)],[c_573,c_359]) ).
tcf(c_1959,plain,
rselect_seq(queue_134) = earray_133,
inference(superposition,[status(thm)],[c_576,c_359]) ).
tcf(c_1960,plain,
rselect_seq(queue_143) = earray_142,
inference(superposition,[status(thm)],[c_579,c_359]) ).
tcf(c_1961,plain,
rselect_seq(queue_149) = earray_148,
inference(superposition,[status(thm)],[c_581,c_359]) ).
tcf(c_1963,plain,
rselect_head(queue_1) = index_0,
inference(superposition,[status(thm)],[c_562,c_360]) ).
tcf(c_1964,plain,
rselect_head(queue_118) = index_117,
inference(superposition,[status(thm)],[c_570,c_360]) ).
tcf(c_1965,plain,
rselect_head(queue_139) = index_138,
inference(superposition,[status(thm)],[c_578,c_360]) ).
tcf(c_1966,plain,
rselect_head(queue_160) = index_159,
inference(superposition,[status(thm)],[c_585,c_360]) ).
tcf(c_1967,plain,
rselect_seq(queue_164) = earray_163,
inference(superposition,[status(thm)],[c_586,c_359]) ).
tcf(c_1968,plain,
rselect_head(queue_169) = index_168,
inference(superposition,[status(thm)],[c_588,c_360]) ).
tcf(c_1969,plain,
index_213 = index_168,
inference(light_normalisation,[status(thm)],[c_1968,c_528]) ).
tcf(c_1970,plain,
rstore_head(queue_166,index_213) = queue_169,
inference(demodulation,[status(thm)],[c_588,c_1969]) ).
tcf(c_1972,plain,
s(index_167) = index_213,
inference(demodulation,[status(thm)],[c_509,c_1969]) ).
tcf(c_1974,plain,
rselect_seq(queue_17) = earray_16,
inference(superposition,[status(thm)],[c_589,c_359]) ).
tcf(c_1979,plain,
rselect_head(queue_190) = index_189,
inference(superposition,[status(thm)],[c_597,c_360]) ).
tcf(c_1982,plain,
rselect_tail(queue_103) = index_102,
inference(superposition,[status(thm)],[c_564,c_361]) ).
tcf(c_1983,plain,
rselect_tail(queue_109) = index_108,
inference(superposition,[status(thm)],[c_566,c_361]) ).
tcf(c_1984,plain,
rselect_tail(queue_115) = index_114,
inference(superposition,[status(thm)],[c_569,c_361]) ).
tcf(c_1985,plain,
rselect_tail(queue_124) = index_123,
inference(superposition,[status(thm)],[c_572,c_361]) ).
tcf(c_1986,plain,
rselect_tail(queue_13) = index_12,
inference(superposition,[status(thm)],[c_574,c_361]) ).
tcf(c_1987,plain,
rselect_tail(queue_130) = index_129,
inference(superposition,[status(thm)],[c_575,c_361]) ).
tcf(c_1988,plain,
rselect_tail(queue_136) = index_135,
inference(superposition,[status(thm)],[c_577,c_361]) ).
tcf(c_1989,plain,
rselect_tail(queue_145) = index_144,
inference(superposition,[status(thm)],[c_580,c_361]) ).
tcf(c_1990,plain,
rselect_tail(queue_151) = index_150,
inference(superposition,[status(thm)],[c_582,c_361]) ).
tcf(c_1991,plain,
rselect_tail(queue_157) = index_156,
inference(superposition,[status(thm)],[c_584,c_361]) ).
tcf(c_1993,plain,
rselect_tail(queue_175) = index_174,
inference(superposition,[status(thm)],[c_591,c_361]) ).
tcf(c_1994,plain,
rselect_tail(queue_181) = index_180,
inference(superposition,[status(thm)],[c_593,c_361]) ).
tcf(c_1995,plain,
rselect_tail(queue_187) = index_186,
inference(superposition,[status(thm)],[c_595,c_361]) ).
tcf(c_1996,plain,
rselect_tail(queue_19) = index_18,
inference(superposition,[status(thm)],[c_596,c_361]) ).
tcf(c_1997,plain,
rselect_tail(queue_196) = index_195,
inference(superposition,[status(thm)],[c_599,c_361]) ).
tcf(c_1998,plain,
rselect_tail(queue_202) = index_201,
inference(superposition,[status(thm)],[c_601,c_361]) ).
tcf(c_1999,plain,
index_204 = index_201,
inference(light_normalisation,[status(thm)],[c_1998,c_523]) ).
tcf(c_2000,plain,
index_198 = index_195,
inference(light_normalisation,[status(thm)],[c_1997,c_521]) ).
tcf(c_2001,plain,
index_21 = index_18,
inference(light_normalisation,[status(thm)],[c_1996,c_526]) ).
tcf(c_2002,plain,
index_183 = index_180,
inference(light_normalisation,[status(thm)],[c_1994,c_515]) ).
tcf(c_2003,plain,
index_177 = index_174,
inference(light_normalisation,[status(thm)],[c_1993,c_512]) ).
tcf(c_2004,plain,
index_162 = index_150,
inference(light_normalisation,[status(thm)],[c_1990,c_506]) ).
tcf(c_2005,plain,
index_147 = index_144,
inference(light_normalisation,[status(thm)],[c_1989,c_499]) ).
tcf(c_2006,plain,
index_132 = index_129,
inference(light_normalisation,[status(thm)],[c_1987,c_493]) ).
tcf(c_2007,plain,
index_15 = index_12,
inference(light_normalisation,[status(thm)],[c_1986,c_500]) ).
tcf(c_2008,plain,
index_126 = index_123,
inference(light_normalisation,[status(thm)],[c_1985,c_491]) ).
tcf(c_2009,plain,
index_111 = index_108,
inference(light_normalisation,[status(thm)],[c_1983,c_484]) ).
tcf(c_2010,plain,
index_105 = index_102,
inference(light_normalisation,[status(thm)],[c_1982,c_482]) ).
tcf(c_2011,plain,
rstore_tail(queue_200,index_204) = queue_202,
inference(demodulation,[status(thm)],[c_601,c_1999]) ).
tcf(c_2013,plain,
s(index_198) = index_204,
inference(demodulation,[status(thm)],[c_522,c_1999]) ).
tcf(c_2014,plain,
rstore_tail(queue_194,index_198) = queue_196,
inference(demodulation,[status(thm)],[c_599,c_2000]) ).
tcf(c_2016,plain,
s(index_192) = index_198,
inference(demodulation,[status(thm)],[c_520,c_2000]) ).
tcf(c_2017,plain,
rstore_tail(queue_17,index_21) = queue_19,
inference(demodulation,[status(thm)],[c_596,c_2001]) ).
tcf(c_2018,plain,
index_15 != index_21,
inference(demodulation,[status(thm)],[c_1929,c_2001]) ).
tcf(c_2019,plain,
s(index_15) = index_21,
inference(demodulation,[status(thm)],[c_513,c_2001]) ).
tcf(c_2020,plain,
rstore_tail(queue_179,index_183) = queue_181,
inference(demodulation,[status(thm)],[c_593,c_2002]) ).
tcf(c_2022,plain,
s(index_177) = index_183,
inference(demodulation,[status(thm)],[c_514,c_2002]) ).
tcf(c_2023,plain,
rstore_tail(queue_173,index_177) = queue_175,
inference(demodulation,[status(thm)],[c_591,c_2003]) ).
tcf(c_2025,plain,
s(index_171) = index_177,
inference(demodulation,[status(thm)],[c_511,c_2003]) ).
tcf(c_2026,plain,
rstore_tail(queue_149,index_162) = queue_151,
inference(demodulation,[status(thm)],[c_582,c_2004]) ).
tcf(c_2028,plain,
s(index_147) = index_162,
inference(demodulation,[status(thm)],[c_501,c_2004]) ).
tcf(c_2029,plain,
rstore_tail(queue_143,index_147) = queue_145,
inference(demodulation,[status(thm)],[c_580,c_2005]) ).
tcf(c_2031,plain,
s(index_141) = index_147,
inference(demodulation,[status(thm)],[c_498,c_2005]) ).
tcf(c_2032,plain,
rstore_tail(queue_128,index_132) = queue_130,
inference(demodulation,[status(thm)],[c_575,c_2006]) ).
tcf(c_2034,plain,
s(index_126) = index_132,
inference(demodulation,[status(thm)],[c_492,c_2006]) ).
tcf(c_2035,plain,
rstore_tail(queue_11,index_15) = queue_13,
inference(demodulation,[status(thm)],[c_574,c_2007]) ).
tcf(c_2037,plain,
s(index_9) = index_15,
inference(demodulation,[status(thm)],[c_488,c_2007]) ).
tcf(c_2038,plain,
rstore_tail(queue_122,index_126) = queue_124,
inference(demodulation,[status(thm)],[c_572,c_2008]) ).
tcf(c_2040,plain,
s(index_120) = index_126,
inference(demodulation,[status(thm)],[c_490,c_2008]) ).
tcf(c_2041,plain,
rstore_tail(queue_107,index_111) = queue_109,
inference(demodulation,[status(thm)],[c_566,c_2009]) ).
tcf(c_2043,plain,
s(index_105) = index_111,
inference(demodulation,[status(thm)],[c_483,c_2009]) ).
tcf(c_2044,plain,
rstore_tail(queue_101,index_105) = queue_103,
inference(demodulation,[status(thm)],[c_564,c_2010]) ).
tcf(c_2046,plain,
s(index_99) = index_105,
inference(demodulation,[status(thm)],[c_481,c_2010]) ).
tcf(c_2047,plain,
rselect_seq(queue_206) = earray_205,
inference(superposition,[status(thm)],[c_602,c_359]) ).
tcf(c_2048,plain,
rselect_tail(queue_208) = index_207,
inference(superposition,[status(thm)],[c_603,c_361]) ).
tcf(c_2049,plain,
rselect_head(queue_211) = index_210,
inference(superposition,[status(thm)],[c_604,c_360]) ).
tcf(c_2050,plain,
rselect_seq(queue_23) = earray_22,
inference(superposition,[status(thm)],[c_605,c_359]) ).
tcf(c_2051,plain,
rselect_tail(queue_25) = index_24,
inference(superposition,[status(thm)],[c_606,c_361]) ).
tcf(c_2052,plain,
rselect_head(queue_28) = index_27,
inference(superposition,[status(thm)],[c_607,c_360]) ).
tcf(c_2053,plain,
rselect_seq(queue_32) = earray_31,
inference(superposition,[status(thm)],[c_608,c_359]) ).
tcf(c_2054,plain,
rselect_tail(queue_34) = index_33,
inference(superposition,[status(thm)],[c_609,c_361]) ).
tcf(c_2055,plain,
index_36 = index_33,
inference(light_normalisation,[status(thm)],[c_2054,c_535]) ).
tcf(c_2056,plain,
rstore_tail(queue_32,index_36) = queue_34,
inference(demodulation,[status(thm)],[c_609,c_2055]) ).
tcf(c_2058,plain,
s(index_30) = index_36,
inference(demodulation,[status(thm)],[c_534,c_2055]) ).
tcf(c_2063,plain,
rselect_seq(queue_38) = earray_37,
inference(superposition,[status(thm)],[c_610,c_359]) ).
tcf(c_2064,plain,
rselect_tail(queue_40) = index_39,
inference(superposition,[status(thm)],[c_611,c_361]) ).
tcf(c_2065,plain,
index_42 = index_39,
inference(light_normalisation,[status(thm)],[c_2064,c_537]) ).
tcf(c_2066,plain,
rstore_tail(queue_38,index_42) = queue_40,
inference(demodulation,[status(thm)],[c_611,c_2065]) ).
tcf(c_2068,plain,
s(index_36) = index_42,
inference(demodulation,[status(thm)],[c_536,c_2065]) ).
tcf(c_2069,plain,
rselect_seq(queue_44) = earray_43,
inference(superposition,[status(thm)],[c_612,c_359]) ).
tcf(c_2070,plain,
rselect_tail(queue_46) = index_45,
inference(superposition,[status(thm)],[c_613,c_361]) ).
tcf(c_2078,plain,
rselect_head(queue_49) = index_48,
inference(superposition,[status(thm)],[c_614,c_360]) ).
tcf(c_2080,plain,
rselect_seq(queue_53) = earray_52,
inference(superposition,[status(thm)],[c_616,c_359]) ).
tcf(c_2081,plain,
rselect_tail(queue_55) = index_54,
inference(superposition,[status(thm)],[c_617,c_361]) ).
tcf(c_2082,plain,
index_57 = index_54,
inference(light_normalisation,[status(thm)],[c_2081,c_543]) ).
tcf(c_2083,plain,
rstore_tail(queue_53,index_57) = queue_55,
inference(demodulation,[status(thm)],[c_617,c_2082]) ).
tcf(c_2085,plain,
s(index_51) = index_57,
inference(demodulation,[status(thm)],[c_542,c_2082]) ).
tcf(c_2090,plain,
rselect_seq(queue_59) = earray_58,
inference(superposition,[status(thm)],[c_618,c_359]) ).
tcf(c_2091,plain,
rselect_tail(queue_61) = index_60,
inference(superposition,[status(thm)],[c_619,c_361]) ).
tcf(c_2092,plain,
index_63 = index_60,
inference(light_normalisation,[status(thm)],[c_2091,c_546]) ).
tcf(c_2093,plain,
rstore_tail(queue_59,index_63) = queue_61,
inference(demodulation,[status(thm)],[c_619,c_2092]) ).
tcf(c_2095,plain,
s(index_57) = index_63,
inference(demodulation,[status(thm)],[c_545,c_2092]) ).
tcf(c_2096,plain,
rselect_seq(queue_65) = earray_64,
inference(superposition,[status(thm)],[c_620,c_359]) ).
tcf(c_2097,plain,
rselect_tail(queue_67) = index_66,
inference(superposition,[status(thm)],[c_621,c_361]) ).
tcf(c_2101,plain,
rselect_tail(queue_7) = index_6,
inference(superposition,[status(thm)],[c_622,c_361]) ).
tcf(c_2102,plain,
index_78 = index_6,
inference(light_normalisation,[status(thm)],[c_2101,c_552]) ).
tcf(c_2103,plain,
rstore_tail(queue_5,index_78) = queue_7,
inference(demodulation,[status(thm)],[c_622,c_2102]) ).
tcf(c_2105,plain,
s(index_3) = index_78,
inference(demodulation,[status(thm)],[c_544,c_2102]) ).
tcf(c_2106,plain,
rselect_head(queue_70) = index_69,
inference(superposition,[status(thm)],[c_623,c_360]) ).
tcf(c_2107,plain,
rselect_seq(queue_74) = earray_73,
inference(superposition,[status(thm)],[c_624,c_359]) ).
tcf(c_2108,plain,
rselect_tail(queue_76) = index_75,
inference(superposition,[status(thm)],[c_625,c_361]) ).
tcf(c_2109,plain,
index_84 = index_75,
inference(light_normalisation,[status(thm)],[c_2108,c_554]) ).
tcf(c_2110,plain,
rstore_tail(queue_74,index_84) = queue_76,
inference(demodulation,[status(thm)],[c_625,c_2109]) ).
tcf(c_2112,plain,
s(index_72) = index_84,
inference(demodulation,[status(thm)],[c_551,c_2109]) ).
tcf(c_2117,plain,
rselect_seq(queue_80) = earray_79,
inference(superposition,[status(thm)],[c_626,c_359]) ).
tcf(c_2118,plain,
rselect_tail(queue_82) = index_81,
inference(superposition,[status(thm)],[c_627,c_361]) ).
tcf(c_2119,plain,
index_153 = index_81,
inference(light_normalisation,[status(thm)],[c_2118,c_502]) ).
tcf(c_2120,plain,
rstore_tail(queue_80,index_153) = queue_82,
inference(demodulation,[status(thm)],[c_627,c_2119]) ).
tcf(c_2122,plain,
s(index_78) = index_153,
inference(demodulation,[status(thm)],[c_553,c_2119]) ).
tcf(c_2123,plain,
rselect_seq(queue_86) = earray_85,
inference(superposition,[status(thm)],[c_628,c_359]) ).
tcf(c_2124,plain,
rselect_tail(queue_88) = index_87,
inference(superposition,[status(thm)],[c_629,c_361]) ).
tcf(c_2125,plain,
index_90 = index_87,
inference(light_normalisation,[status(thm)],[c_2124,c_557]) ).
tcf(c_2126,plain,
rstore_tail(queue_86,index_90) = queue_88,
inference(demodulation,[status(thm)],[c_629,c_2125]) ).
tcf(c_2128,plain,
s(index_84) = index_90,
inference(demodulation,[status(thm)],[c_555,c_2125]) ).
tcf(c_2133,plain,
rselect_seq(queue_92) = earray_91,
inference(superposition,[status(thm)],[c_630,c_359]) ).
tcf(c_2134,plain,
rselect_tail(queue_94) = index_93,
inference(superposition,[status(thm)],[c_631,c_361]) ).
tcf(c_2135,plain,
rselect_head(queue_97) = index_96,
inference(superposition,[status(thm)],[c_632,c_360]) ).
tcf(c_2152,plain,
s(index_21) != index_15,
inference(superposition,[status(thm)],[c_2019,c_416]) ).
tcf(c_2187,plain,
index_15 != index_24,
inference(light_normalisation,[status(thm)],[c_2152,c_529]) ).
tcf(c_2202,plain,
! [X0: $i] :
( ( X0 = index_99 )
| ( select(earray_100,X0) = select(earray_98,X0) ) ),
inference(superposition,[status(thm)],[c_419,c_358]) ).
tcf(c_2207,plain,
! [X0: $i] :
( ( X0 = index_105 )
| ( select(earray_104,X0) = select(earray_106,X0) ) ),
inference(superposition,[status(thm)],[c_421,c_358]) ).
tcf(c_2211,plain,
! [X0: $i] :
( ( X0 = index_111 )
| ( select(earray_110,X0) = select(earray_112,X0) ) ),
inference(superposition,[status(thm)],[c_423,c_358]) ).
tcf(c_2218,plain,
! [X0: $i] :
( ( X0 = index_120 )
| ( select(earray_119,X0) = select(earray_121,X0) ) ),
inference(superposition,[status(thm)],[c_425,c_358]) ).
tcf(c_2223,plain,
! [X0: $i] :
( ( X0 = index_126 )
| ( select(earray_125,X0) = select(earray_127,X0) ) ),
inference(superposition,[status(thm)],[c_427,c_358]) ).
tcf(c_2228,plain,
! [X0: $i] :
( ( X0 = index_132 )
| ( select(earray_131,X0) = select(earray_133,X0) ) ),
inference(superposition,[status(thm)],[c_429,c_358]) ).
tcf(c_2233,plain,
! [X0: $i] :
( ( X0 = index_141 )
| ( select(earray_140,X0) = select(earray_142,X0) ) ),
inference(superposition,[status(thm)],[c_432,c_358]) ).
tcf(c_2249,plain,
! [X0: $i] :
( ( X0 = index_147 )
| ( select(earray_146,X0) = select(earray_148,X0) ) ),
inference(superposition,[status(thm)],[c_434,c_358]) ).
tcf(c_2259,plain,
! [X0: $i] :
( ( X0 = index_162 )
| ( select(earray_161,X0) = select(earray_163,X0) ) ),
inference(superposition,[status(thm)],[c_439,c_358]) ).
tcf(c_2298,plain,
! [X0: $i] :
( ( X0 = index_21 )
| ( select(earray_20,X0) = select(earray_22,X0) ) ),
inference(superposition,[status(thm)],[c_455,c_358]) ).
tcf(c_2303,plain,
! [X0: $i] :
( ( X0 = index_30 )
| ( select(earray_29,X0) = select(earray_31,X0) ) ),
inference(superposition,[status(thm)],[c_457,c_358]) ).
tcf(c_2308,plain,
! [X0: $i] :
( ( X0 = index_36 )
| ( select(earray_35,X0) = select(earray_37,X0) ) ),
inference(superposition,[status(thm)],[c_459,c_358]) ).
tcf(c_2322,plain,
! [X0: $i] :
( ( X0 = index_42 )
| ( select(earray_41,X0) = select(earray_43,X0) ) ),
inference(superposition,[status(thm)],[c_462,c_358]) ).
tcf(c_2327,plain,
! [X0: $i] :
( ( X0 = index_51 )
| ( select(earray_50,X0) = select(earray_52,X0) ) ),
inference(superposition,[status(thm)],[c_464,c_358]) ).
tcf(c_2332,plain,
! [X0: $i] :
( ( X0 = index_57 )
| ( select(earray_56,X0) = select(earray_58,X0) ) ),
inference(superposition,[status(thm)],[c_466,c_358]) ).
tcf(c_2337,plain,
! [X0: $i] :
( ( X0 = index_63 )
| ( select(earray_62,X0) = select(earray_64,X0) ) ),
inference(superposition,[status(thm)],[c_468,c_358]) ).
tcf(c_2342,plain,
! [X0: $i] :
( ( X0 = index_72 )
| ( select(earray_71,X0) = select(earray_73,X0) ) ),
inference(superposition,[status(thm)],[c_470,c_358]) ).
tcf(c_2352,plain,
! [X0: $i] :
( ( X0 = index_84 )
| ( select(earray_83,X0) = select(earray_85,X0) ) ),
inference(superposition,[status(thm)],[c_475,c_358]) ).
tcf(c_2363,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( select(earray_89,X0) = select(earray_91,X0) ) ),
inference(superposition,[status(thm)],[c_477,c_358]) ).
tcf(c_2369,plain,
rselect_seq(queue_115) = rselect_seq(queue_118),
inference(superposition,[status(thm)],[c_570,c_362]) ).
tcf(c_2370,plain,
rselect_seq(queue_136) = rselect_seq(queue_139),
inference(superposition,[status(thm)],[c_578,c_362]) ).
tcf(c_2373,plain,
rselect_seq(queue_208) = rselect_seq(queue_211),
inference(superposition,[status(thm)],[c_604,c_362]) ).
tcf(c_2374,plain,
rselect_seq(queue_25) = rselect_seq(queue_28),
inference(superposition,[status(thm)],[c_607,c_362]) ).
tcf(c_2375,plain,
rselect_seq(queue_46) = rselect_seq(queue_49),
inference(superposition,[status(thm)],[c_614,c_362]) ).
tcf(c_2376,plain,
rselect_seq(queue_67) = rselect_seq(queue_70),
inference(superposition,[status(thm)],[c_623,c_362]) ).
tcf(c_2377,plain,
rselect_seq(queue_94) = rselect_seq(queue_97),
inference(superposition,[status(thm)],[c_632,c_362]) ).
tcf(c_2378,plain,
rselect_seq(queue_166) = rselect_seq(queue_169),
inference(superposition,[status(thm)],[c_1970,c_362]) ).
tcf(c_2379,plain,
rselect_seq(queue_166) = earray_212,
inference(light_normalisation,[status(thm)],[c_2378,c_454]) ).
tcf(c_2380,plain,
rselect_seq(queue_94) = earray_98,
inference(light_normalisation,[status(thm)],[c_2377,c_478]) ).
tcf(c_2381,plain,
rselect_seq(queue_67) = earray_71,
inference(light_normalisation,[status(thm)],[c_2376,c_469]) ).
tcf(c_2382,plain,
rselect_seq(queue_46) = earray_50,
inference(light_normalisation,[status(thm)],[c_2375,c_463]) ).
tcf(c_2383,plain,
rselect_seq(queue_25) = earray_29,
inference(light_normalisation,[status(thm)],[c_2374,c_456]) ).
tcf(c_2384,plain,
rselect_seq(queue_208) = earray_8,
inference(light_normalisation,[status(thm)],[c_2373,c_473]) ).
tcf(c_2387,plain,
rselect_seq(queue_136) = earray_140,
inference(light_normalisation,[status(thm)],[c_2370,c_431]) ).
tcf(c_2388,plain,
rselect_seq(queue_115) = earray_119,
inference(light_normalisation,[status(thm)],[c_2369,c_424]) ).
tcf(c_2390,plain,
rselect_seq(queue_115) = rselect_seq(queue_113),
inference(superposition,[status(thm)],[c_569,c_363]) ).
tcf(c_2391,plain,
rselect_seq(queue_136) = rselect_seq(queue_134),
inference(superposition,[status(thm)],[c_577,c_363]) ).
tcf(c_2393,plain,
rselect_seq(queue_166) = rselect_seq(queue_164),
inference(superposition,[status(thm)],[c_587,c_363]) ).
tcf(c_2395,plain,
rselect_seq(queue_208) = rselect_seq(queue_206),
inference(superposition,[status(thm)],[c_603,c_363]) ).
tcf(c_2396,plain,
rselect_seq(queue_25) = rselect_seq(queue_23),
inference(superposition,[status(thm)],[c_606,c_363]) ).
tcf(c_2397,plain,
rselect_seq(queue_46) = rselect_seq(queue_44),
inference(superposition,[status(thm)],[c_613,c_363]) ).
tcf(c_2398,plain,
rselect_seq(queue_67) = rselect_seq(queue_65),
inference(superposition,[status(thm)],[c_621,c_363]) ).
tcf(c_2399,plain,
rselect_seq(queue_94) = rselect_seq(queue_92),
inference(superposition,[status(thm)],[c_631,c_363]) ).
tcf(c_2402,plain,
rselect_seq(queue_17) = rselect_seq(queue_19),
inference(superposition,[status(thm)],[c_2017,c_363]) ).
tcf(c_2405,plain,
rselect_seq(queue_149) = rselect_seq(queue_151),
inference(superposition,[status(thm)],[c_2026,c_363]) ).
tcf(c_2406,plain,
rselect_seq(queue_143) = rselect_seq(queue_145),
inference(superposition,[status(thm)],[c_2029,c_363]) ).
tcf(c_2407,plain,
rselect_seq(queue_128) = rselect_seq(queue_130),
inference(superposition,[status(thm)],[c_2032,c_363]) ).
tcf(c_2409,plain,
rselect_seq(queue_122) = rselect_seq(queue_124),
inference(superposition,[status(thm)],[c_2038,c_363]) ).
tcf(c_2410,plain,
rselect_seq(queue_107) = rselect_seq(queue_109),
inference(superposition,[status(thm)],[c_2041,c_363]) ).
tcf(c_2411,plain,
rselect_seq(queue_101) = rselect_seq(queue_103),
inference(superposition,[status(thm)],[c_2044,c_363]) ).
tcf(c_2412,plain,
rselect_seq(queue_32) = rselect_seq(queue_34),
inference(superposition,[status(thm)],[c_2056,c_363]) ).
tcf(c_2413,plain,
rselect_seq(queue_38) = rselect_seq(queue_40),
inference(superposition,[status(thm)],[c_2066,c_363]) ).
tcf(c_2414,plain,
rselect_seq(queue_53) = rselect_seq(queue_55),
inference(superposition,[status(thm)],[c_2083,c_363]) ).
tcf(c_2415,plain,
rselect_seq(queue_59) = rselect_seq(queue_61),
inference(superposition,[status(thm)],[c_2093,c_363]) ).
tcf(c_2417,plain,
rselect_seq(queue_74) = rselect_seq(queue_76),
inference(superposition,[status(thm)],[c_2110,c_363]) ).
tcf(c_2418,plain,
rselect_seq(queue_80) = rselect_seq(queue_82),
inference(superposition,[status(thm)],[c_2120,c_363]) ).
tcf(c_2419,plain,
rselect_seq(queue_86) = rselect_seq(queue_88),
inference(superposition,[status(thm)],[c_2126,c_363]) ).
tcf(c_2420,plain,
earray_85 = earray_89,
inference(light_normalisation,[status(thm)],[c_2419,c_476,c_2123]) ).
tcf(c_2421,plain,
earray_152 = earray_79,
inference(light_normalisation,[status(thm)],[c_2418,c_435,c_2117]) ).
tcf(c_2422,plain,
earray_73 = earray_83,
inference(light_normalisation,[status(thm)],[c_2417,c_474,c_2107]) ).
tcf(c_2424,plain,
earray_58 = earray_62,
inference(light_normalisation,[status(thm)],[c_2415,c_467,c_2090]) ).
tcf(c_2425,plain,
earray_52 = earray_56,
inference(light_normalisation,[status(thm)],[c_2414,c_465,c_2080]) ).
tcf(c_2426,plain,
earray_37 = earray_41,
inference(light_normalisation,[status(thm)],[c_2413,c_461,c_2063]) ).
tcf(c_2427,plain,
earray_31 = earray_35,
inference(light_normalisation,[status(thm)],[c_2412,c_458,c_2053]) ).
tcf(c_2428,plain,
earray_100 = earray_104,
inference(light_normalisation,[status(thm)],[c_2411,c_420,c_1953]) ).
tcf(c_2429,plain,
earray_106 = earray_110,
inference(light_normalisation,[status(thm)],[c_2410,c_422,c_1954]) ).
tcf(c_2430,plain,
earray_121 = earray_125,
inference(light_normalisation,[status(thm)],[c_2409,c_426,c_1957]) ).
tcf(c_2432,plain,
earray_127 = earray_131,
inference(light_normalisation,[status(thm)],[c_2407,c_428,c_1958]) ).
tcf(c_2433,plain,
earray_142 = earray_146,
inference(light_normalisation,[status(thm)],[c_2406,c_433,c_1960]) ).
tcf(c_2434,plain,
earray_148 = earray_161,
inference(light_normalisation,[status(thm)],[c_2405,c_438,c_1961]) ).
tcf(c_2437,plain,
earray_16 = earray_20,
inference(light_normalisation,[status(thm)],[c_2402,c_451,c_1974]) ).
tcf(c_2440,plain,
earray_98 = earray_91,
inference(light_normalisation,[status(thm)],[c_2399,c_2133,c_2380]) ).
tcf(c_2441,plain,
earray_64 = earray_71,
inference(light_normalisation,[status(thm)],[c_2398,c_2096,c_2381]) ).
tcf(c_2442,plain,
earray_43 = earray_50,
inference(light_normalisation,[status(thm)],[c_2397,c_2069,c_2382]) ).
tcf(c_2443,plain,
earray_22 = earray_29,
inference(light_normalisation,[status(thm)],[c_2396,c_2050,c_2383]) ).
tcf(c_2444,plain,
earray_8 = earray_205,
inference(light_normalisation,[status(thm)],[c_2395,c_2047,c_2384]) ).
tcf(c_2446,plain,
earray_163 = earray_212,
inference(light_normalisation,[status(thm)],[c_2393,c_1967,c_2379]) ).
tcf(c_2448,plain,
earray_133 = earray_140,
inference(light_normalisation,[status(thm)],[c_2391,c_1959,c_2387]) ).
tcf(c_2449,plain,
earray_112 = earray_119,
inference(light_normalisation,[status(thm)],[c_2390,c_1956,c_2388]) ).
tcf(c_2455,plain,
rstore_seq(queue_7,earray_152) = queue_80,
inference(demodulation,[status(thm)],[c_626,c_2421]) ).
tcf(c_2467,plain,
! [X0: $i] :
( ( X0 = index_105 )
| ( select(earray_100,X0) = select(earray_106,X0) ) ),
inference(demodulation,[status(thm)],[c_2207,c_2428]) ).
tcf(c_2498,plain,
rstore_seq(queue_88,earray_98) = queue_92,
inference(demodulation,[status(thm)],[c_630,c_2440]) ).
tcf(c_2507,plain,
rstore_seq(queue_202,earray_8) = queue_206,
inference(demodulation,[status(thm)],[c_602,c_2444]) ).
tcf(c_2510,plain,
select(earray_163,index_213) = elem_214,
inference(demodulation,[status(thm)],[c_479,c_2446]) ).
tcf(c_2621,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c_569,c_364]) ).
tcf(c_2622,plain,
rselect_head(queue_136) = rselect_head(queue_134),
inference(superposition,[status(thm)],[c_577,c_364]) ).
tcf(c_2623,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(superposition,[status(thm)],[c_584,c_364]) ).
tcf(c_2624,plain,
rselect_head(queue_166) = rselect_head(queue_164),
inference(superposition,[status(thm)],[c_587,c_364]) ).
tcf(c_2625,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(superposition,[status(thm)],[c_595,c_364]) ).
tcf(c_2626,plain,
rselect_head(queue_208) = rselect_head(queue_206),
inference(superposition,[status(thm)],[c_603,c_364]) ).
tcf(c_2627,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c_606,c_364]) ).
tcf(c_2628,plain,
rselect_head(queue_46) = rselect_head(queue_44),
inference(superposition,[status(thm)],[c_613,c_364]) ).
tcf(c_2629,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(superposition,[status(thm)],[c_621,c_364]) ).
tcf(c_2630,plain,
rselect_head(queue_94) = rselect_head(queue_92),
inference(superposition,[status(thm)],[c_631,c_364]) ).
tcf(c_2631,plain,
rselect_head(queue_200) = rselect_head(queue_202),
inference(superposition,[status(thm)],[c_2011,c_364]) ).
tcf(c_2632,plain,
rselect_head(queue_194) = rselect_head(queue_196),
inference(superposition,[status(thm)],[c_2014,c_364]) ).
tcf(c_2633,plain,
rselect_head(queue_17) = rselect_head(queue_19),
inference(superposition,[status(thm)],[c_2017,c_364]) ).
tcf(c_2634,plain,
rselect_head(queue_179) = rselect_head(queue_181),
inference(superposition,[status(thm)],[c_2020,c_364]) ).
tcf(c_2635,plain,
rselect_head(queue_173) = rselect_head(queue_175),
inference(superposition,[status(thm)],[c_2023,c_364]) ).
tcf(c_2636,plain,
rselect_head(queue_149) = rselect_head(queue_151),
inference(superposition,[status(thm)],[c_2026,c_364]) ).
tcf(c_2637,plain,
rselect_head(queue_143) = rselect_head(queue_145),
inference(superposition,[status(thm)],[c_2029,c_364]) ).
tcf(c_2638,plain,
rselect_head(queue_128) = rselect_head(queue_130),
inference(superposition,[status(thm)],[c_2032,c_364]) ).
tcf(c_2639,plain,
rselect_head(queue_11) = rselect_head(queue_13),
inference(superposition,[status(thm)],[c_2035,c_364]) ).
tcf(c_2640,plain,
rselect_head(queue_122) = rselect_head(queue_124),
inference(superposition,[status(thm)],[c_2038,c_364]) ).
tcf(c_2641,plain,
rselect_head(queue_107) = rselect_head(queue_109),
inference(superposition,[status(thm)],[c_2041,c_364]) ).
tcf(c_2642,plain,
rselect_head(queue_101) = rselect_head(queue_103),
inference(superposition,[status(thm)],[c_2044,c_364]) ).
tcf(c_2643,plain,
rselect_head(queue_32) = rselect_head(queue_34),
inference(superposition,[status(thm)],[c_2056,c_364]) ).
tcf(c_2644,plain,
rselect_head(queue_38) = rselect_head(queue_40),
inference(superposition,[status(thm)],[c_2066,c_364]) ).
tcf(c_2645,plain,
rselect_head(queue_53) = rselect_head(queue_55),
inference(superposition,[status(thm)],[c_2083,c_364]) ).
tcf(c_2646,plain,
rselect_head(queue_59) = rselect_head(queue_61),
inference(superposition,[status(thm)],[c_2093,c_364]) ).
tcf(c_2647,plain,
rselect_head(queue_5) = rselect_head(queue_7),
inference(superposition,[status(thm)],[c_2103,c_364]) ).
tcf(c_2648,plain,
rselect_head(queue_74) = rselect_head(queue_76),
inference(superposition,[status(thm)],[c_2110,c_364]) ).
tcf(c_2649,plain,
rselect_head(queue_80) = rselect_head(queue_82),
inference(superposition,[status(thm)],[c_2120,c_364]) ).
tcf(c_2650,plain,
rselect_head(queue_86) = rselect_head(queue_88),
inference(superposition,[status(thm)],[c_2126,c_364]) ).
tcf(c_2651,plain,
rselect_head(queue_92) = index_95,
inference(light_normalisation,[status(thm)],[c_2630,c_559]) ).
tcf(c_2652,plain,
rselect_head(queue_65) = index_68,
inference(light_normalisation,[status(thm)],[c_2629,c_548]) ).
tcf(c_2653,plain,
rselect_head(queue_44) = index_47,
inference(light_normalisation,[status(thm)],[c_2628,c_539]) ).
tcf(c_2654,plain,
rselect_head(queue_23) = index_26,
inference(light_normalisation,[status(thm)],[c_2627,c_530]) ).
tcf(c_2655,plain,
rselect_head(queue_206) = index_209,
inference(light_normalisation,[status(thm)],[c_2626,c_525]) ).
tcf(c_2656,plain,
rselect_head(queue_185) = index_188,
inference(light_normalisation,[status(thm)],[c_2625,c_517]) ).
tcf(c_2657,plain,
rselect_head(queue_164) = index_167,
inference(light_normalisation,[status(thm)],[c_2624,c_508]) ).
tcf(c_2658,plain,
rselect_head(queue_155) = index_158,
inference(light_normalisation,[status(thm)],[c_2623,c_504]) ).
tcf(c_2659,plain,
rselect_head(queue_134) = index_137,
inference(light_normalisation,[status(thm)],[c_2622,c_495]) ).
tcf(c_2660,plain,
rselect_head(queue_113) = index_116,
inference(light_normalisation,[status(thm)],[c_2621,c_486]) ).
tcf(c_2663,plain,
rselect_head(queue_101) = rselect_head(queue_97),
inference(superposition,[status(thm)],[c_563,c_365]) ).
tcf(c_2664,plain,
rselect_head(queue_103) = rselect_head(queue_107),
inference(superposition,[status(thm)],[c_565,c_365]) ).
tcf(c_2665,plain,
rselect_head(queue_11) = rselect_head(queue_211),
inference(superposition,[status(thm)],[c_567,c_365]) ).
tcf(c_2666,plain,
rselect_head(queue_109) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c_568,c_365]) ).
tcf(c_2667,plain,
rselect_head(queue_118) = rselect_head(queue_122),
inference(superposition,[status(thm)],[c_571,c_365]) ).
tcf(c_2668,plain,
rselect_head(queue_124) = rselect_head(queue_128),
inference(superposition,[status(thm)],[c_573,c_365]) ).
tcf(c_2669,plain,
rselect_head(queue_130) = rselect_head(queue_134),
inference(superposition,[status(thm)],[c_576,c_365]) ).
tcf(c_2670,plain,
rselect_head(queue_139) = rselect_head(queue_143),
inference(superposition,[status(thm)],[c_579,c_365]) ).
tcf(c_2671,plain,
rselect_head(queue_145) = rselect_head(queue_149),
inference(superposition,[status(thm)],[c_581,c_365]) ).
tcf(c_2672,plain,
rselect_head(queue_155) = rselect_head(queue_82),
inference(superposition,[status(thm)],[c_583,c_365]) ).
tcf(c_2673,plain,
rselect_head(queue_151) = rselect_head(queue_164),
inference(superposition,[status(thm)],[c_586,c_365]) ).
tcf(c_2674,plain,
rselect_head(queue_13) = rselect_head(queue_17),
inference(superposition,[status(thm)],[c_589,c_365]) ).
tcf(c_2675,plain,
rselect_head(queue_160) = rselect_head(queue_173),
inference(superposition,[status(thm)],[c_590,c_365]) ).
tcf(c_2676,plain,
rselect_head(queue_175) = rselect_head(queue_179),
inference(superposition,[status(thm)],[c_592,c_365]) ).
tcf(c_2677,plain,
rselect_head(queue_181) = rselect_head(queue_185),
inference(superposition,[status(thm)],[c_594,c_365]) ).
tcf(c_2678,plain,
rselect_head(queue_190) = rselect_head(queue_194),
inference(superposition,[status(thm)],[c_598,c_365]) ).
tcf(c_2679,plain,
rselect_head(queue_196) = rselect_head(queue_200),
inference(superposition,[status(thm)],[c_600,c_365]) ).
tcf(c_2680,plain,
rselect_head(queue_19) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c_605,c_365]) ).
tcf(c_2681,plain,
rselect_head(queue_28) = rselect_head(queue_32),
inference(superposition,[status(thm)],[c_608,c_365]) ).
tcf(c_2682,plain,
rselect_head(queue_34) = rselect_head(queue_38),
inference(superposition,[status(thm)],[c_610,c_365]) ).
tcf(c_2683,plain,
rselect_head(queue_40) = rselect_head(queue_44),
inference(superposition,[status(thm)],[c_612,c_365]) ).
tcf(c_2684,plain,
rselect_head(queue_1) = rselect_head(queue_5),
inference(superposition,[status(thm)],[c_615,c_365]) ).
tcf(c_2685,plain,
rselect_head(queue_49) = rselect_head(queue_53),
inference(superposition,[status(thm)],[c_616,c_365]) ).
tcf(c_2686,plain,
rselect_head(queue_55) = rselect_head(queue_59),
inference(superposition,[status(thm)],[c_618,c_365]) ).
tcf(c_2687,plain,
rselect_head(queue_61) = rselect_head(queue_65),
inference(superposition,[status(thm)],[c_620,c_365]) ).
tcf(c_2688,plain,
rselect_head(queue_70) = rselect_head(queue_74),
inference(superposition,[status(thm)],[c_624,c_365]) ).
tcf(c_2689,plain,
rselect_head(queue_76) = rselect_head(queue_86),
inference(superposition,[status(thm)],[c_628,c_365]) ).
tcf(c_2690,plain,
rselect_head(queue_74) = index_69,
inference(light_normalisation,[status(thm)],[c_2688,c_2106,c_2648]) ).
tcf(c_2691,plain,
rselect_head(queue_61) = index_68,
inference(light_normalisation,[status(thm)],[c_2687,c_2652]) ).
tcf(c_2692,plain,
rselect_head(queue_53) = index_48,
inference(light_normalisation,[status(thm)],[c_2685,c_2078,c_2645]) ).
tcf(c_2693,plain,
rselect_head(queue_5) = index_0,
inference(light_normalisation,[status(thm)],[c_2684,c_1963,c_2647]) ).
tcf(c_2694,plain,
rselect_head(queue_40) = index_47,
inference(light_normalisation,[status(thm)],[c_2683,c_2653]) ).
tcf(c_2695,plain,
rselect_head(queue_32) = index_27,
inference(light_normalisation,[status(thm)],[c_2681,c_2052,c_2643]) ).
tcf(c_2696,plain,
rselect_head(queue_19) = index_26,
inference(light_normalisation,[status(thm)],[c_2680,c_2654]) ).
tcf(c_2697,plain,
rselect_head(queue_194) = index_189,
inference(light_normalisation,[status(thm)],[c_2678,c_1979,c_2632]) ).
tcf(c_2698,plain,
rselect_head(queue_181) = index_188,
inference(light_normalisation,[status(thm)],[c_2677,c_2656]) ).
tcf(c_2699,plain,
rselect_head(queue_173) = index_159,
inference(light_normalisation,[status(thm)],[c_2675,c_1966,c_2635]) ).
tcf(c_2700,plain,
rselect_head(queue_151) = index_167,
inference(light_normalisation,[status(thm)],[c_2673,c_2657]) ).
tcf(c_2701,plain,
rselect_head(queue_82) = index_158,
inference(light_normalisation,[status(thm)],[c_2672,c_2658]) ).
tcf(c_2702,plain,
rselect_head(queue_143) = index_138,
inference(light_normalisation,[status(thm)],[c_2670,c_1965,c_2637]) ).
tcf(c_2703,plain,
rselect_head(queue_130) = index_137,
inference(light_normalisation,[status(thm)],[c_2669,c_2659]) ).
tcf(c_2704,plain,
rselect_head(queue_122) = index_117,
inference(light_normalisation,[status(thm)],[c_2667,c_1964,c_2640]) ).
tcf(c_2705,plain,
rselect_head(queue_109) = index_116,
inference(light_normalisation,[status(thm)],[c_2666,c_2660]) ).
tcf(c_2706,plain,
rselect_head(queue_13) = index_210,
inference(light_normalisation,[status(thm)],[c_2665,c_2049,c_2639]) ).
tcf(c_2707,plain,
rselect_head(queue_103) = index_96,
inference(light_normalisation,[status(thm)],[c_2663,c_2135,c_2642]) ).
tcf(c_2864,plain,
rselect_tail(q) = rselect_tail(queue_1),
inference(superposition,[status(thm)],[c_562,c_367]) ).
tcf(c_2865,plain,
rselect_tail(queue_115) = rselect_tail(queue_118),
inference(superposition,[status(thm)],[c_570,c_367]) ).
tcf(c_2866,plain,
rselect_tail(queue_136) = rselect_tail(queue_139),
inference(superposition,[status(thm)],[c_578,c_367]) ).
tcf(c_2867,plain,
rselect_tail(queue_157) = rselect_tail(queue_160),
inference(superposition,[status(thm)],[c_585,c_367]) ).
tcf(c_2868,plain,
rselect_tail(queue_187) = rselect_tail(queue_190),
inference(superposition,[status(thm)],[c_597,c_367]) ).
tcf(c_2869,plain,
rselect_tail(queue_208) = rselect_tail(queue_211),
inference(superposition,[status(thm)],[c_604,c_367]) ).
tcf(c_2870,plain,
rselect_tail(queue_25) = rselect_tail(queue_28),
inference(superposition,[status(thm)],[c_607,c_367]) ).
tcf(c_2871,plain,
rselect_tail(queue_46) = rselect_tail(queue_49),
inference(superposition,[status(thm)],[c_614,c_367]) ).
tcf(c_2872,plain,
rselect_tail(queue_67) = rselect_tail(queue_70),
inference(superposition,[status(thm)],[c_623,c_367]) ).
tcf(c_2873,plain,
rselect_tail(queue_94) = rselect_tail(queue_97),
inference(superposition,[status(thm)],[c_632,c_367]) ).
tcf(c_2876,plain,
index_99 = index_93,
inference(light_normalisation,[status(thm)],[c_2873,c_561,c_2134]) ).
tcf(c_2877,plain,
index_72 = index_66,
inference(light_normalisation,[status(thm)],[c_2872,c_550,c_2097]) ).
tcf(c_2878,plain,
index_51 = index_45,
inference(light_normalisation,[status(thm)],[c_2871,c_541,c_2070]) ).
tcf(c_2879,plain,
index_30 = index_24,
inference(light_normalisation,[status(thm)],[c_2870,c_533,c_2051]) ).
tcf(c_2880,plain,
index_9 = index_207,
inference(light_normalisation,[status(thm)],[c_2869,c_556,c_2048]) ).
tcf(c_2881,plain,
index_192 = index_186,
inference(light_normalisation,[status(thm)],[c_2868,c_519,c_1995]) ).
tcf(c_2882,plain,
index_171 = index_156,
inference(light_normalisation,[status(thm)],[c_2867,c_510,c_1991]) ).
tcf(c_2883,plain,
index_141 = index_135,
inference(light_normalisation,[status(thm)],[c_2866,c_497,c_1988]) ).
tcf(c_2884,plain,
index_120 = index_114,
inference(light_normalisation,[status(thm)],[c_2865,c_489,c_1984]) ).
tcf(c_2885,plain,
index_3 = index_0,
inference(light_normalisation,[status(thm)],[c_2864,c_480,c_532]) ).
tcf(c_2891,plain,
s(index_90) = index_99,
inference(demodulation,[status(thm)],[c_558,c_2876]) ).
tcf(c_2898,plain,
s(index_63) = index_72,
inference(demodulation,[status(thm)],[c_547,c_2877]) ).
tcf(c_2905,plain,
s(index_42) = index_51,
inference(demodulation,[status(thm)],[c_538,c_2878]) ).
tcf(c_2908,plain,
index_15 != index_30,
inference(demodulation,[status(thm)],[c_2187,c_2879]) ).
tcf(c_2912,plain,
s(index_21) = index_30,
inference(demodulation,[status(thm)],[c_529,c_2879]) ).
tcf(c_2919,plain,
s(index_204) = index_9,
inference(demodulation,[status(thm)],[c_524,c_2880]) ).
tcf(c_2926,plain,
s(index_183) = index_192,
inference(demodulation,[status(thm)],[c_516,c_2881]) ).
tcf(c_2933,plain,
s(index_153) = index_171,
inference(demodulation,[status(thm)],[c_503,c_2882]) ).
tcf(c_2940,plain,
s(index_132) = index_141,
inference(demodulation,[status(thm)],[c_494,c_2883]) ).
tcf(c_2947,plain,
s(index_111) = index_120,
inference(demodulation,[status(thm)],[c_485,c_2884]) ).
tcf(c_2965,plain,
s(s(index_21)) != index_15,
inference(superposition,[status(thm)],[c_2019,c_415]) ).
tcf(c_2994,plain,
index_15 != index_36,
inference(light_normalisation,[status(thm)],[c_2965,c_2058,c_2912]) ).
tcf(c_3021,plain,
s(s(s(index_21))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_414]) ).
tcf(c_3050,plain,
index_15 != index_42,
inference(light_normalisation,[status(thm)],[c_3021,c_2058,c_2068,c_2912]) ).
tcf(c_3099,plain,
s(s(s(s(index_21)))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_413]) ).
tcf(c_3128,plain,
index_15 != index_51,
inference(light_normalisation,[status(thm)],[c_3099,c_2058,c_2068,c_2905,c_2912]) ).
tcf(c_3215,plain,
s(s(s(s(s(index_21))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_412]) ).
tcf(c_3244,plain,
index_15 != index_57,
inference(light_normalisation,[status(thm)],[c_3215,c_2058,c_2068,c_2085,c_2905,c_2912]) ).
tcf(c_3266,plain,
s(s(s(s(s(s(index_21)))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_411]) ).
tcf(c_3295,plain,
index_15 != index_63,
inference(light_normalisation,[status(thm)],[c_3266,c_2058,c_2068,c_2085,c_2095,c_2905,c_2912]) ).
tcf(c_3325,plain,
! [X0: $i] :
( ( X0 = index_111 )
| ( select(earray_106,X0) = select(earray_112,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2211,c_2429]) ).
tcf(c_3347,plain,
s(s(s(s(s(s(s(index_21))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_410]) ).
tcf(c_3376,plain,
index_15 != index_72,
inference(light_normalisation,[status(thm)],[c_3347,c_2058,c_2068,c_2085,c_2095,c_2898,c_2905,c_2912]) ).
tcf(c_3468,plain,
s(s(s(s(s(s(s(s(index_21)))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_409]) ).
tcf(c_3497,plain,
index_15 != index_84,
inference(light_normalisation,[status(thm)],[c_3468,c_2058,c_2068,c_2085,c_2095,c_2112,c_2898,c_2905,c_2912]) ).
tcf(c_3589,plain,
s(s(s(s(s(s(s(s(s(index_21))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_408]) ).
tcf(c_3618,plain,
index_15 != index_90,
inference(light_normalisation,[status(thm)],[c_3589,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2898,c_2905,c_2912]) ).
tcf(c_3798,plain,
s(s(s(s(s(s(s(s(s(s(index_21)))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_407]) ).
tcf(c_3827,plain,
index_99 != index_15,
inference(light_normalisation,[status(thm)],[c_3798,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912]) ).
tcf(c_3984,plain,
! [X0: $i] :
( ( X0 = index_120 )
| ( select(earray_112,X0) = select(earray_121,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2218,c_2449]) ).
tcf(c_4006,plain,
s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_406]) ).
tcf(c_4035,plain,
index_105 != index_15,
inference(light_normalisation,[status(thm)],[c_4006,c_2046,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912]) ).
tcf(c_4057,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_405]) ).
tcf(c_4086,plain,
index_111 != index_15,
inference(light_normalisation,[status(thm)],[c_4057,c_2043,c_2046,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912]) ).
tcf(c_4155,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_404]) ).
tcf(c_4184,plain,
index_120 != index_15,
inference(light_normalisation,[status(thm)],[c_4155,c_2043,c_2046,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912,c_2947]) ).
tcf(c_4206,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_403]) ).
tcf(c_4235,plain,
index_126 != index_15,
inference(light_normalisation,[status(thm)],[c_4206,c_2040,c_2043,c_2046,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912,c_2947]) ).
tcf(c_4290,plain,
! [X0: $i] :
( ( X0 = index_126 )
| ( select(earray_121,X0) = select(earray_127,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2223,c_2430]) ).
tcf(c_4312,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_402]) ).
tcf(c_4341,plain,
index_132 != index_15,
inference(light_normalisation,[status(thm)],[c_4312,c_2034,c_2040,c_2043,c_2046,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912,c_2947]) ).
tcf(c_4403,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_401]) ).
tcf(c_4432,plain,
index_141 != index_15,
inference(light_normalisation,[status(thm)],[c_4403,c_2034,c_2040,c_2043,c_2046,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912,c_2940,c_2947]) ).
tcf(c_4494,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_400]) ).
tcf(c_4523,plain,
index_147 != index_15,
inference(light_normalisation,[status(thm)],[c_4494,c_2031,c_2034,c_2040,c_2043,c_2046,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912,c_2940,c_2947]) ).
tcf(c_5077,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2019,c_399]) ).
tcf(c_5106,plain,
index_15 != index_162,
inference(light_normalisation,[status(thm)],[c_5077,c_2028,c_2031,c_2034,c_2040,c_2043,c_2046,c_2058,c_2068,c_2085,c_2095,c_2112,c_2128,c_2891,c_2898,c_2905,c_2912,c_2940,c_2947]) ).
tcf(c_5169,plain,
! [X0: $i] :
( ( X0 = index_132 )
| ( select(earray_127,X0) = select(earray_133,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2228,c_2432]) ).
tcf(c_6339,plain,
! [X0: $i] :
( ( X0 = index_141 )
| ( select(earray_133,X0) = select(earray_142,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2233,c_2448]) ).
tcf(c_7143,plain,
rselect_head(queue_5) = index_3,
inference(light_normalisation,[status(thm)],[c_2693,c_2885]) ).
tcf(c_7144,plain,
! [X0: $i] :
( ( X0 = index_147 )
| ( select(earray_142,X0) = select(earray_148,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2249,c_2433]) ).
tcf(c_11073,plain,
! [X0: $i] :
( ( X0 = index_162 )
| ( select(earray_148,X0) = select(earray_163,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2259,c_2434]) ).
tcf(c_11083,plain,
( ( index_162 = index_213 )
| ( select(earray_148,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_11073,c_2510]) ).
tcf(c_11438,plain,
( ( index_162 = index_213 )
| ( index_147 = index_213 )
| ( select(earray_142,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_7144,c_11083]) ).
tcf(c_12044,plain,
( ( index_162 = index_213 )
| ( index_147 = index_213 )
| ( index_141 = index_213 )
| ( select(earray_133,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_6339,c_11438]) ).
tcf(c_13051,plain,
( ( index_162 = index_213 )
| ( index_147 = index_213 )
| ( index_141 = index_213 )
| ( index_132 = index_213 )
| ( select(earray_127,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_5169,c_12044]) ).
tcf(c_13782,plain,
( ( index_162 = index_213 )
| ( index_147 = index_213 )
| ( index_141 = index_213 )
| ( index_132 = index_213 )
| ( index_126 = index_213 )
| ( select(earray_121,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_4290,c_13051]) ).
tcf(c_14403,plain,
( ( index_162 = index_213 )
| ( index_147 = index_213 )
| ( index_141 = index_213 )
| ( index_132 = index_213 )
| ( index_126 = index_213 )
| ( index_120 = index_213 )
| ( select(earray_112,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_3984,c_13782]) ).
tcf(c_14426,plain,
( ( index_162 = index_213 )
| ( index_147 = index_213 )
| ( index_141 = index_213 )
| ( index_132 = index_213 )
| ( index_126 = index_213 )
| ( index_120 = index_213 )
| ( index_111 = index_213 )
| ( select(earray_106,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_3325,c_14403]) ).
tcf(c_14513,plain,
! [X0: $i] :
( ( X0 = index_21 )
| ( select(earray_16,X0) = select(earray_22,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2298,c_2437]) ).
tcf(c_14522,plain,
! [X0: $i] :
( ( X0 = index_30 )
| ( select(earray_22,X0) = select(earray_31,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2303,c_2443]) ).
tcf(c_14531,plain,
! [X0: $i] :
( ( X0 = index_36 )
| ( select(earray_31,X0) = select(earray_37,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2308,c_2427]) ).
tcf(c_14546,plain,
! [X0: $i] :
( ( X0 = index_42 )
| ( select(earray_37,X0) = select(earray_43,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2322,c_2426]) ).
tcf(c_14555,plain,
! [X0: $i] :
( ( X0 = index_51 )
| ( select(earray_43,X0) = select(earray_52,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2327,c_2442]) ).
tcf(c_14564,plain,
! [X0: $i] :
( ( X0 = index_57 )
| ( select(earray_52,X0) = select(earray_58,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2332,c_2425]) ).
tcf(c_14573,plain,
! [X0: $i] :
( ( X0 = index_63 )
| ( select(earray_58,X0) = select(earray_64,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2337,c_2424]) ).
tcf(c_14582,plain,
! [X0: $i] :
( ( X0 = index_72 )
| ( select(earray_64,X0) = select(earray_73,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2342,c_2441]) ).
tcf(c_14607,plain,
! [X0: $i] :
( ( X0 = index_84 )
| ( select(earray_73,X0) = select(earray_85,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2352,c_2422]) ).
tcf(c_14616,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( select(earray_98,X0) = select(earray_85,X0) ) ),
inference(light_normalisation,[status(thm)],[c_2363,c_2420,c_2440]) ).
tcf(c_14625,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( X0 = index_84 )
| ( select(earray_98,X0) = select(earray_73,X0) ) ),
inference(superposition,[status(thm)],[c_14616,c_14607]) ).
tcf(c_14667,plain,
rselect_head(queue_7) = rselect_head(queue_80),
inference(superposition,[status(thm)],[c_2455,c_365]) ).
tcf(c_14671,plain,
rselect_head(queue_88) = rselect_head(queue_92),
inference(superposition,[status(thm)],[c_2498,c_365]) ).
tcf(c_14673,plain,
rselect_head(queue_88) = index_95,
inference(light_normalisation,[status(thm)],[c_14671,c_2651]) ).
tcf(c_14679,plain,
rselect_head(queue_202) = rselect_head(queue_206),
inference(superposition,[status(thm)],[c_2507,c_365]) ).
tcf(c_14681,plain,
rselect_head(queue_202) = index_209,
inference(light_normalisation,[status(thm)],[c_14679,c_2655]) ).
tcf(c_14683,plain,
rselect_head(queue_196) = index_209,
inference(light_normalisation,[status(thm)],[c_2631,c_2679,c_14681]) ).
tcf(c_14684,plain,
index_189 = index_209,
inference(light_normalisation,[status(thm)],[c_2632,c_2697,c_14683]) ).
tcf(c_14690,plain,
s(index_189) = index_210,
inference(demodulation,[status(thm)],[c_527,c_14684]) ).
tcf(c_14793,plain,
index_210 = index_26,
inference(light_normalisation,[status(thm)],[c_2633,c_2674,c_2696,c_2706]) ).
tcf(c_14798,plain,
s(index_210) = index_27,
inference(demodulation,[status(thm)],[c_531,c_14793]) ).
tcf(c_14949,plain,
rselect_head(queue_175) = index_188,
inference(light_normalisation,[status(thm)],[c_2634,c_2676,c_2698]) ).
tcf(c_14950,plain,
index_159 = index_188,
inference(light_normalisation,[status(thm)],[c_2635,c_2699,c_14949]) ).
tcf(c_14956,plain,
s(index_159) = index_189,
inference(demodulation,[status(thm)],[c_518,c_14950]) ).
tcf(c_15466,plain,
rselect_head(queue_145) = index_167,
inference(light_normalisation,[status(thm)],[c_2636,c_2671,c_2700]) ).
tcf(c_15467,plain,
index_138 = index_167,
inference(light_normalisation,[status(thm)],[c_2637,c_2702,c_15466]) ).
tcf(c_15472,plain,
s(index_138) = index_213,
inference(demodulation,[status(thm)],[c_1972,c_15467]) ).
tcf(c_15528,plain,
rselect_head(queue_124) = index_137,
inference(light_normalisation,[status(thm)],[c_2638,c_2668,c_2703]) ).
tcf(c_15530,plain,
index_117 = index_137,
inference(light_normalisation,[status(thm)],[c_2640,c_2704,c_15528]) ).
tcf(c_15536,plain,
s(index_117) = index_138,
inference(demodulation,[status(thm)],[c_496,c_15530]) ).
tcf(c_15638,plain,
index_116 = index_96,
inference(light_normalisation,[status(thm)],[c_2641,c_2664,c_2705,c_2707]) ).
tcf(c_15644,plain,
s(index_95) = index_116,
inference(demodulation,[status(thm)],[c_560,c_15638]) ).
tcf(c_15798,plain,
rselect_head(queue_34) = index_27,
inference(light_normalisation,[status(thm)],[c_2643,c_2695]) ).
tcf(c_15799,plain,
index_27 = index_47,
inference(light_normalisation,[status(thm)],[c_2644,c_2682,c_2694,c_15798]) ).
tcf(c_15804,plain,
s(index_27) = index_48,
inference(demodulation,[status(thm)],[c_540,c_15799]) ).
tcf(c_15856,plain,
rselect_head(queue_55) = index_48,
inference(light_normalisation,[status(thm)],[c_2645,c_2692]) ).
tcf(c_15857,plain,
index_48 = index_68,
inference(light_normalisation,[status(thm)],[c_2646,c_2686,c_2691,c_15856]) ).
tcf(c_15862,plain,
s(index_48) = index_69,
inference(demodulation,[status(thm)],[c_549,c_15857]) ).
tcf(c_15967,plain,
rselect_head(queue_7) = index_3,
inference(light_normalisation,[status(thm)],[c_2647,c_7143]) ).
tcf(c_15968,plain,
rselect_head(queue_76) = index_69,
inference(light_normalisation,[status(thm)],[c_2648,c_2690]) ).
tcf(c_15969,plain,
index_3 = index_158,
inference(light_normalisation,[status(thm)],[c_2649,c_2701,c_14667,c_15967]) ).
tcf(c_15974,plain,
s(index_3) = index_159,
inference(demodulation,[status(thm)],[c_505,c_15969]) ).
tcf(c_15976,plain,
index_78 = index_159,
inference(light_normalisation,[status(thm)],[c_15974,c_2105]) ).
tcf(c_15979,plain,
s(index_78) = index_189,
inference(demodulation,[status(thm)],[c_14956,c_15976]) ).
tcf(c_15989,plain,
index_153 = index_189,
inference(light_normalisation,[status(thm)],[c_15979,c_2122]) ).
tcf(c_15991,plain,
s(index_153) = index_210,
inference(demodulation,[status(thm)],[c_14690,c_15989]) ).
tcf(c_16000,plain,
index_171 = index_210,
inference(light_normalisation,[status(thm)],[c_15991,c_2933]) ).
tcf(c_16003,plain,
s(index_171) = index_27,
inference(demodulation,[status(thm)],[c_14798,c_16000]) ).
tcf(c_16011,plain,
index_177 = index_27,
inference(light_normalisation,[status(thm)],[c_16003,c_2025]) ).
tcf(c_16013,plain,
s(index_177) = index_48,
inference(demodulation,[status(thm)],[c_15804,c_16011]) ).
tcf(c_16022,plain,
index_183 = index_48,
inference(light_normalisation,[status(thm)],[c_16013,c_2022]) ).
tcf(c_16024,plain,
s(index_183) = index_69,
inference(demodulation,[status(thm)],[c_15862,c_16022]) ).
tcf(c_16033,plain,
index_192 = index_69,
inference(light_normalisation,[status(thm)],[c_16024,c_2926]) ).
tcf(c_16034,plain,
rselect_head(queue_76) = index_192,
inference(demodulation,[status(thm)],[c_15968,c_16033]) ).
tcf(c_16045,plain,
( ( index_162 = index_213 )
| ( index_147 = index_213 )
| ( index_141 = index_213 )
| ( index_132 = index_213 )
| ( index_126 = index_213 )
| ( index_120 = index_213 )
| ( index_111 = index_213 )
| ( index_105 = index_213 )
| ( select(earray_100,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_2467,c_14426]) ).
tcf(c_16084,plain,
index_192 = index_95,
inference(light_normalisation,[status(thm)],[c_2650,c_2689,c_14673,c_16034]) ).
tcf(c_16088,plain,
s(index_192) = index_116,
inference(demodulation,[status(thm)],[c_15644,c_16084]) ).
tcf(c_16093,plain,
index_198 = index_116,
inference(light_normalisation,[status(thm)],[c_16088,c_2016]) ).
tcf(c_16102,plain,
s(index_198) = index_117,
inference(demodulation,[status(thm)],[c_487,c_16093]) ).
tcf(c_16104,plain,
index_204 = index_117,
inference(light_normalisation,[status(thm)],[c_16102,c_2013]) ).
tcf(c_16106,plain,
s(index_204) = index_138,
inference(demodulation,[status(thm)],[c_15536,c_16104]) ).
tcf(c_16116,plain,
index_9 = index_138,
inference(light_normalisation,[status(thm)],[c_16106,c_2919]) ).
tcf(c_16119,plain,
s(index_9) = index_213,
inference(demodulation,[status(thm)],[c_15472,c_16116]) ).
tcf(c_16127,plain,
index_15 = index_213,
inference(light_normalisation,[status(thm)],[c_16119,c_2037]) ).
tcf(c_16128,plain,
( ( index_15 = index_162 )
| ( index_147 = index_15 )
| ( index_141 = index_15 )
| ( index_132 = index_15 )
| ( index_126 = index_15 )
| ( index_120 = index_15 )
| ( index_111 = index_15 )
| ( index_105 = index_15 )
| ( select(earray_100,index_15) = elem_214 ) ),
inference(demodulation,[status(thm)],[c_16045,c_16127]) ).
tcf(c_16147,plain,
select(earray_100,index_15) = elem_214,
inference(forward_subsumption_resolution,[status(thm)],[c_16128,c_5106,c_4523,c_4432,c_4341,c_4235,c_4184,c_4086,c_4035]) ).
tcf(c_16510,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( X0 = index_84 )
| ( X0 = index_72 )
| ( select(earray_98,X0) = select(earray_64,X0) ) ),
inference(superposition,[status(thm)],[c_14625,c_14582]) ).
tcf(c_16630,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( X0 = index_84 )
| ( X0 = index_72 )
| ( X0 = index_63 )
| ( select(earray_98,X0) = select(earray_58,X0) ) ),
inference(superposition,[status(thm)],[c_16510,c_14573]) ).
tcf(c_16754,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( X0 = index_84 )
| ( X0 = index_72 )
| ( X0 = index_63 )
| ( X0 = index_57 )
| ( select(earray_98,X0) = select(earray_52,X0) ) ),
inference(superposition,[status(thm)],[c_16630,c_14564]) ).
tcf(c_16878,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( X0 = index_84 )
| ( X0 = index_72 )
| ( X0 = index_63 )
| ( X0 = index_57 )
| ( X0 = index_51 )
| ( select(earray_98,X0) = select(earray_43,X0) ) ),
inference(superposition,[status(thm)],[c_16754,c_14555]) ).
tcf(c_17010,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( X0 = index_84 )
| ( X0 = index_72 )
| ( X0 = index_63 )
| ( X0 = index_57 )
| ( X0 = index_51 )
| ( X0 = index_42 )
| ( select(earray_98,X0) = select(earray_37,X0) ) ),
inference(superposition,[status(thm)],[c_16878,c_14546]) ).
tcf(c_17198,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( X0 = index_84 )
| ( X0 = index_72 )
| ( X0 = index_63 )
| ( X0 = index_57 )
| ( X0 = index_51 )
| ( X0 = index_42 )
| ( X0 = index_36 )
| ( select(earray_98,X0) = select(earray_31,X0) ) ),
inference(superposition,[status(thm)],[c_17010,c_14531]) ).
tcf(c_17302,plain,
! [X0: $i] :
( ( 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 )
| ( select(earray_98,X0) = select(earray_22,X0) ) ),
inference(superposition,[status(thm)],[c_17198,c_14522]) ).
tcf(c_17413,plain,
! [X0: $i] :
( ( 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 )
| ( select(earray_98,X0) = select(earray_16,X0) ) ),
inference(superposition,[status(thm)],[c_17302,c_14513]) ).
tcf(c_17528,plain,
( ( 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 )
| ( select(earray_98,index_15) = e10 ) ),
inference(superposition,[status(thm)],[c_17413,c_1898]) ).
tcf(c_17530,plain,
select(earray_98,index_15) = e10,
inference(forward_subsumption_resolution,[status(thm)],[c_17528,c_3618,c_3497,c_3376,c_3295,c_3244,c_3128,c_3050,c_2994,c_2908,c_2018]) ).
tcf(c_17544,plain,
( ( index_99 = index_15 )
| ( select(earray_100,index_15) = e10 ) ),
inference(superposition,[status(thm)],[c_2202,c_17530]) ).
tcf(c_17546,plain,
( ( e10 = elem_214 )
| ( index_99 = index_15 ) ),
inference(light_normalisation,[status(thm)],[c_17544,c_16147]) ).
tcf(c_17547,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_17546,c_1264,c_3827]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/10.44 % Computer : n018.cluster.edu
% 0.15/10.44 % Model : x86_64 x86_64
% 0.15/10.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/10.44 % Memory : 8046.5625MB
% 0.15/10.44 % OS : Linux 6.8.0-71-generic
% 0.15/10.44 % CPULimit : 300
% 0.15/10.44 % WCLimit : 300
% 0.15/10.44 % DateTime : Thu Sep 24 20:37:59 UTC 2026
% 0.15/10.45 % CPUTime :
% 0.15/10.45 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/10.48 Running first-order theorem proving
% 0.15/10.48 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/10.49
% 0.15/10.49 % ======== iProver multi-core TPTP/SMT =========
% 0.15/10.49
% 0.15/10.49 % Detected problem language: tptp
% 0.21/10.50 % Proving...
% 19.00/13.35 % SZS status Started for theBenchmark.p
% 19.00/13.35 % SZS status Unsatisfiable for theBenchmark.p
% 19.00/13.35
% 19.00/13.35 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 19.00/13.35
% 19.00/13.35 % ------ iProver source info
% 19.00/13.35
% 19.00/13.35 % git: date: 2026-07-19 20:42:38 +0200
% 19.00/13.35 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 19.00/13.35 % git: non_committed_changes: false
% 19.00/13.35
% 19.00/13.35 % ------ Parsing...% successful
% 19.00/13.35
% 19.00/13.35
% 19.00/13.35 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 19.00/13.35
% 19.00/13.35 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 19.00/13.35
% 19.00/13.35 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 19.00/13.35
% 19.00/13.35 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 19.00/13.35 % ------ Proving...
% 19.00/13.35 % ------ Problem Properties
% 19.00/13.35
% 19.00/13.35 %
% 19.00/13.35 % clauses 277
% 19.00/13.35 % conjectures 1
% 19.00/13.35 % EPR 1
% 19.00/13.35 % Horn 276
% 19.00/13.35 % unary 276
% 19.00/13.35 % binary 1
% 19.00/13.35 % lits 278
% 19.00/13.35 % lits eq 278
% 19.00/13.35 % fd_pure 0
% 19.00/13.35 % fd_pseudo 0
% 19.00/13.35 % fd_cond 0
% 19.00/13.35 % fd_pseudo_cond 1
% 19.00/13.35 % AC symbols 0
% 19.00/13.35
% 19.00/13.35 % ------ Schedule dynamic 5 is on
% 19.00/13.35
% 19.00/13.35 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 19.00/13.35
% 19.00/13.35
% 19.00/13.35 % ------
% 19.00/13.35 % Current options:
% 19.00/13.35 % ------
% 19.00/13.35
% 19.00/13.35
% 19.00/13.35 %
% 19.00/13.35
% 19.00/13.35 % ------ Proving...
% 19.00/13.35 %
% 19.00/13.35
% 19.00/13.35 % SZS status Unsatisfiable for theBenchmark.p
% 19.00/13.35
% 19.00/13.35 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 19.00/13.36
% 19.00/13.36
%------------------------------------------------------------------------------