%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV569-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:23:47 PM UTC 2026
% Result : Unsatisfiable 26.47s 6.32s
% Output : CNFRefutation 26.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 249
% Syntax : Number of formulae : 1087 ( 815 unt; 0 def)
% Number of atoms : 1512 (1511 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 544 ( 119 ~; 425 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 2 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 : 263 ( 263 usr; 260 con; 0-3 aty)
% Number of variables : 216 ( 0 sgn 216 !; 0 ?; 190 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
head != tail,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_tail) ).
fof(f4,axiom,
head != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_seq) ).
fof(f5,axiom,
tail != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tail_distinct_from_seq) ).
fof(f37,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(f38,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(f39,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(f40,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(f41,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(f42,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(f43,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(f44,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(f45,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as11) ).
fof(f46,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as10) ).
fof(f47,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as9) ).
fof(f48,axiom,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as8) ).
fof(f49,axiom,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as7) ).
fof(f50,axiom,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as6) ).
fof(f51,axiom,
! [X0] : s(s(s(s(s(X0))))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as5) ).
fof(f52,axiom,
! [X0] : s(s(s(s(X0)))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as4) ).
fof(f53,axiom,
! [X0] : s(s(s(X0))) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as3) ).
fof(f54,axiom,
! [X0] : s(s(X0)) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as2) ).
fof(f55,axiom,
! [X0] : s(X0) != X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as1) ).
fof(f57,axiom,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f58,axiom,
earray_104 = select(q22,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f59,axiom,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f60,axiom,
earray_110 = select(q23,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f61,axiom,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f62,axiom,
earray_119 = select(q24,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f63,axiom,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f64,axiom,
earray_125 = select(q25,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f65,axiom,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f66,axiom,
earray_131 = select(q26,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f67,axiom,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f69,axiom,
earray_140 = select(q27,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f70,axiom,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f71,axiom,
earray_146 = select(q28,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f72,axiom,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f75,axiom,
earray_16 = store(earray_14,index_15,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f76,axiom,
earray_161 = select(q29,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f77,axiom,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f89,axiom,
earray_20 = select(q11,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
fof(f92,axiom,
earray_212 = select(q30,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f93,axiom,
earray_22 = store(earray_20,index_21,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f94,axiom,
earray_29 = select(q12,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f95,axiom,
earray_31 = store(earray_29,index_30,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f96,axiom,
earray_35 = select(q13,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f97,axiom,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f99,axiom,
earray_41 = select(q14,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
fof(f100,axiom,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp44) ).
fof(f101,axiom,
earray_50 = select(q15,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
fof(f102,axiom,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp46) ).
fof(f103,axiom,
earray_56 = select(q16,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
fof(f104,axiom,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp48) ).
fof(f105,axiom,
earray_62 = select(q17,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp49) ).
fof(f106,axiom,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp50) ).
fof(f107,axiom,
earray_71 = select(q18,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp51) ).
fof(f108,axiom,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp52) ).
fof(f112,axiom,
earray_83 = select(q19,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp56) ).
fof(f113,axiom,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp57) ).
fof(f114,axiom,
earray_89 = select(q20,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp58) ).
fof(f115,axiom,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp59) ).
fof(f116,axiom,
earray_98 = select(q21,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp60) ).
fof(f117,axiom,
elem_214 = select(earray_212,index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp61) ).
fof(f118,axiom,
index_0 = select(q,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp62) ).
fof(f119,axiom,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp63) ).
fof(f120,axiom,
index_105 = select(q22,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp64) ).
fof(f121,axiom,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp65) ).
fof(f122,axiom,
index_111 = select(q23,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp66) ).
fof(f123,axiom,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp67) ).
fof(f124,axiom,
index_116 = select(queue_115,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp68) ).
fof(f125,axiom,
index_117 = s(index_116),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp69) ).
fof(f126,axiom,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp70) ).
fof(f127,axiom,
index_120 = select(q24,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp71) ).
fof(f128,axiom,
index_123 = s(index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp72) ).
fof(f129,axiom,
index_126 = select(q25,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp73) ).
fof(f130,axiom,
index_129 = s(index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp74) ).
fof(f131,axiom,
index_132 = select(q26,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp75) ).
fof(f132,axiom,
index_135 = s(index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp76) ).
fof(f133,axiom,
index_137 = select(queue_136,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp77) ).
fof(f134,axiom,
index_138 = s(index_137),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp78) ).
fof(f135,axiom,
index_141 = select(q27,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp79) ).
fof(f136,axiom,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp80) ).
fof(f137,axiom,
index_147 = select(q28,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp81) ).
fof(f138,axiom,
index_15 = select(q10,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp82) ).
fof(f139,axiom,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp83) ).
fof(f140,axiom,
index_153 = select(q2,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp84) ).
fof(f141,axiom,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp85) ).
fof(f142,axiom,
index_158 = select(queue_157,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp86) ).
fof(f143,axiom,
index_159 = s(index_158),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp87) ).
fof(f144,axiom,
index_162 = select(q29,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp88) ).
fof(f146,axiom,
index_167 = select(queue_166,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp90) ).
fof(f147,axiom,
index_168 = s(index_167),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp91) ).
fof(f148,axiom,
index_171 = select(q3,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp92) ).
fof(f149,axiom,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp93) ).
fof(f150,axiom,
index_177 = select(q4,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp94) ).
fof(f151,axiom,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp95) ).
fof(f152,axiom,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp96) ).
fof(f153,axiom,
index_183 = select(q5,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp97) ).
fof(f154,axiom,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp98) ).
fof(f155,axiom,
index_188 = select(queue_187,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
fof(f156,axiom,
index_189 = s(index_188),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
fof(f157,axiom,
index_192 = select(q6,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f158,axiom,
index_195 = s(index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp102) ).
fof(f159,axiom,
index_198 = select(q7,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp103) ).
fof(f160,axiom,
index_201 = s(index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
fof(f161,axiom,
index_204 = select(q8,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp105) ).
fof(f162,axiom,
index_207 = s(index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp106) ).
fof(f163,axiom,
index_209 = select(queue_208,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
fof(f164,axiom,
index_21 = select(q11,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
fof(f165,axiom,
index_210 = s(index_209),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
fof(f166,axiom,
index_213 = select(q30,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp110) ).
fof(f167,axiom,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp111) ).
fof(f168,axiom,
index_26 = select(queue_25,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp112) ).
fof(f169,axiom,
index_27 = s(index_26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp113) ).
fof(f170,axiom,
index_3 = select(q0,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
fof(f171,axiom,
index_30 = select(q12,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp115) ).
fof(f172,axiom,
index_33 = s(index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp116) ).
fof(f173,axiom,
index_36 = select(q13,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp117) ).
fof(f174,axiom,
index_39 = s(index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp118) ).
fof(f175,axiom,
index_42 = select(q14,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp119) ).
fof(f176,axiom,
index_45 = s(index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp120) ).
fof(f177,axiom,
index_47 = select(queue_46,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp121) ).
fof(f178,axiom,
index_48 = s(index_47),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp122) ).
fof(f179,axiom,
index_51 = select(q15,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp123) ).
fof(f180,axiom,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp124) ).
fof(f181,axiom,
index_57 = select(q16,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp125) ).
fof(f182,axiom,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp126) ).
fof(f183,axiom,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp127) ).
fof(f184,axiom,
index_63 = select(q17,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp128) ).
fof(f185,axiom,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp129) ).
fof(f186,axiom,
index_68 = select(queue_67,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp130) ).
fof(f187,axiom,
index_69 = s(index_68),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp131) ).
fof(f188,axiom,
index_72 = select(q18,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp132) ).
fof(f189,axiom,
index_75 = s(index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp133) ).
fof(f190,axiom,
index_78 = select(q1,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp134) ).
fof(f191,axiom,
index_81 = s(index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp135) ).
fof(f192,axiom,
index_84 = select(q19,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp136) ).
fof(f193,axiom,
index_87 = s(index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp137) ).
fof(f194,axiom,
index_9 = select(q9,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
fof(f195,axiom,
index_90 = select(q20,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp139) ).
fof(f196,axiom,
index_93 = s(index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp140) ).
fof(f197,axiom,
index_95 = select(queue_94,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp141) ).
fof(f198,axiom,
index_96 = s(index_95),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp142) ).
fof(f199,axiom,
index_99 = select(q21,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp143) ).
fof(f200,axiom,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp144) ).
fof(f201,axiom,
queue_101 = store(q21,seq,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp145) ).
fof(f202,axiom,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp146) ).
fof(f203,axiom,
queue_107 = store(q22,seq,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp147) ).
fof(f204,axiom,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp148) ).
fof(f205,axiom,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp149) ).
fof(f206,axiom,
queue_113 = store(q23,seq,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp150) ).
fof(f207,axiom,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp151) ).
fof(f208,axiom,
queue_118 = store(queue_115,head,index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
fof(f209,axiom,
queue_122 = store(q24,seq,earray_121),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp153) ).
fof(f210,axiom,
queue_124 = store(queue_122,tail,index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp154) ).
fof(f211,axiom,
queue_128 = store(q25,seq,earray_127),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp155) ).
fof(f212,axiom,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp156) ).
fof(f213,axiom,
queue_130 = store(queue_128,tail,index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp157) ).
fof(f214,axiom,
queue_134 = store(q26,seq,earray_133),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp158) ).
fof(f215,axiom,
queue_136 = store(queue_134,tail,index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp159) ).
fof(f216,axiom,
queue_139 = store(queue_136,head,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
fof(f217,axiom,
queue_143 = store(q27,seq,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp161) ).
fof(f218,axiom,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp162) ).
fof(f219,axiom,
queue_149 = store(q28,seq,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp163) ).
fof(f220,axiom,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp164) ).
fof(f221,axiom,
queue_155 = store(q2,seq,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp165) ).
fof(f222,axiom,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp166) ).
fof(f223,axiom,
queue_160 = store(queue_157,head,index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp167) ).
fof(f224,axiom,
queue_164 = store(q29,seq,earray_163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
fof(f225,axiom,
queue_166 = store(queue_164,tail,index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp169) ).
fof(f226,axiom,
queue_169 = store(queue_166,head,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp170) ).
fof(f227,axiom,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp171) ).
fof(f228,axiom,
queue_173 = store(q3,seq,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
fof(f229,axiom,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp173) ).
fof(f230,axiom,
queue_179 = store(q4,seq,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp174) ).
fof(f231,axiom,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
fof(f232,axiom,
queue_185 = store(q5,seq,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp176) ).
fof(f233,axiom,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp177) ).
fof(f234,axiom,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp178) ).
fof(f235,axiom,
queue_190 = store(queue_187,head,index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp179) ).
fof(f236,axiom,
queue_194 = store(q6,seq,earray_193),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp180) ).
fof(f237,axiom,
queue_196 = store(queue_194,tail,index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp181) ).
fof(f238,axiom,
queue_200 = store(q7,seq,earray_199),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp182) ).
fof(f239,axiom,
queue_202 = store(queue_200,tail,index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp183) ).
fof(f240,axiom,
queue_206 = store(q8,seq,earray_205),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp184) ).
fof(f241,axiom,
queue_208 = store(queue_206,tail,index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp185) ).
fof(f242,axiom,
queue_211 = store(queue_208,head,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp186) ).
fof(f243,axiom,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f244,axiom,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp188) ).
fof(f245,axiom,
queue_28 = store(queue_25,head,index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp189) ).
fof(f246,axiom,
queue_32 = store(q12,seq,earray_31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp190) ).
fof(f247,axiom,
queue_34 = store(queue_32,tail,index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
fof(f248,axiom,
queue_38 = store(q13,seq,earray_37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp192) ).
fof(f249,axiom,
queue_40 = store(queue_38,tail,index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp193) ).
fof(f250,axiom,
queue_44 = store(q14,seq,earray_43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp194) ).
fof(f251,axiom,
queue_46 = store(queue_44,tail,index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
fof(f252,axiom,
queue_49 = store(queue_46,head,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp196) ).
fof(f253,axiom,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp197) ).
fof(f254,axiom,
queue_53 = store(q15,seq,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
fof(f255,axiom,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
fof(f256,axiom,
queue_59 = store(q16,seq,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
fof(f257,axiom,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
fof(f258,axiom,
queue_65 = store(q17,seq,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
fof(f259,axiom,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f260,axiom,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp204) ).
fof(f261,axiom,
queue_70 = store(queue_67,head,index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f262,axiom,
queue_74 = store(q18,seq,earray_73),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp206) ).
fof(f263,axiom,
queue_76 = store(queue_74,tail,index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f264,axiom,
queue_80 = store(q1,seq,earray_79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
fof(f265,axiom,
queue_82 = store(queue_80,tail,index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f266,axiom,
queue_86 = store(q19,seq,earray_85),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
fof(f267,axiom,
queue_88 = store(queue_86,tail,index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
fof(f268,axiom,
queue_92 = store(q20,seq,earray_91),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f269,axiom,
queue_94 = store(queue_92,tail,index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f270,axiom,
queue_97 = store(queue_94,head,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
fof(f271,axiom,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f272,axiom,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
fof(f273,axiom,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f274,axiom,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp218) ).
fof(f275,axiom,
q12 = queue_28,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp219) ).
fof(f276,axiom,
q13 = queue_34,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f277,axiom,
q14 = queue_40,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f278,axiom,
q15 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
fof(f279,axiom,
q16 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
fof(f280,axiom,
q17 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f281,axiom,
q18 = queue_70,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f282,axiom,
q19 = queue_76,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
fof(f283,axiom,
q2 = queue_82,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f284,axiom,
q20 = queue_88,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
fof(f285,axiom,
q21 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f286,axiom,
q22 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
fof(f287,axiom,
q23 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
fof(f288,axiom,
q24 = queue_118,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f289,axiom,
q25 = queue_124,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f290,axiom,
q26 = queue_130,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
fof(f291,axiom,
q27 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
fof(f292,axiom,
q28 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f293,axiom,
q29 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f294,axiom,
q3 = queue_160,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
fof(f295,axiom,
q30 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f296,axiom,
q4 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
fof(f297,axiom,
q5 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f298,axiom,
q6 = queue_190,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
fof(f299,axiom,
q7 = queue_196,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
fof(f300,axiom,
q8 = queue_202,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f301,axiom,
q9 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f302,negated_conjecture,
elem_214 != e10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f303,plain,
e10 != elem_214,
inference(reorient_equations,[],[f302]) ).
fof(f304,plain,
earray_104 = select(queue_103,seq),
inference(definition_unfolding,[],[f58,f286]) ).
fof(f305,plain,
earray_110 = select(queue_109,seq),
inference(definition_unfolding,[],[f60,f287]) ).
fof(f306,plain,
earray_119 = select(queue_118,seq),
inference(definition_unfolding,[],[f62,f288]) ).
fof(f307,plain,
earray_125 = select(queue_124,seq),
inference(definition_unfolding,[],[f64,f289]) ).
fof(f308,plain,
earray_131 = select(queue_130,seq),
inference(definition_unfolding,[],[f66,f290]) ).
fof(f310,plain,
earray_140 = select(queue_139,seq),
inference(definition_unfolding,[],[f69,f291]) ).
fof(f311,plain,
earray_146 = select(queue_145,seq),
inference(definition_unfolding,[],[f71,f292]) ).
fof(f313,plain,
earray_161 = select(queue_151,seq),
inference(definition_unfolding,[],[f76,f293]) ).
fof(f320,plain,
earray_20 = select(queue_19,seq),
inference(definition_unfolding,[],[f89,f274]) ).
fof(f322,plain,
earray_212 = select(queue_169,seq),
inference(definition_unfolding,[],[f92,f295]) ).
fof(f323,plain,
earray_29 = select(queue_28,seq),
inference(definition_unfolding,[],[f94,f275]) ).
fof(f324,plain,
earray_35 = select(queue_34,seq),
inference(definition_unfolding,[],[f96,f276]) ).
fof(f325,plain,
earray_41 = select(queue_40,seq),
inference(definition_unfolding,[],[f99,f277]) ).
fof(f326,plain,
earray_50 = select(queue_49,seq),
inference(definition_unfolding,[],[f101,f278]) ).
fof(f327,plain,
earray_56 = select(queue_55,seq),
inference(definition_unfolding,[],[f103,f279]) ).
fof(f328,plain,
earray_62 = select(queue_61,seq),
inference(definition_unfolding,[],[f105,f280]) ).
fof(f329,plain,
earray_71 = select(queue_70,seq),
inference(definition_unfolding,[],[f107,f281]) ).
fof(f332,plain,
earray_83 = select(queue_76,seq),
inference(definition_unfolding,[],[f112,f282]) ).
fof(f333,plain,
earray_89 = select(queue_88,seq),
inference(definition_unfolding,[],[f114,f284]) ).
fof(f334,plain,
earray_98 = select(queue_97,seq),
inference(definition_unfolding,[],[f116,f285]) ).
fof(f335,plain,
index_105 = select(queue_103,tail),
inference(definition_unfolding,[],[f120,f286]) ).
fof(f336,plain,
index_111 = select(queue_109,tail),
inference(definition_unfolding,[],[f122,f287]) ).
fof(f337,plain,
index_120 = select(queue_118,tail),
inference(definition_unfolding,[],[f127,f288]) ).
fof(f338,plain,
index_126 = select(queue_124,tail),
inference(definition_unfolding,[],[f129,f289]) ).
fof(f339,plain,
index_132 = select(queue_130,tail),
inference(definition_unfolding,[],[f131,f290]) ).
fof(f340,plain,
index_141 = select(queue_139,tail),
inference(definition_unfolding,[],[f135,f291]) ).
fof(f341,plain,
index_147 = select(queue_145,tail),
inference(definition_unfolding,[],[f137,f292]) ).
fof(f342,plain,
index_15 = select(queue_13,tail),
inference(definition_unfolding,[],[f138,f273]) ).
fof(f343,plain,
index_153 = select(queue_82,tail),
inference(definition_unfolding,[],[f140,f283]) ).
fof(f344,plain,
index_162 = select(queue_151,tail),
inference(definition_unfolding,[],[f144,f293]) ).
fof(f345,plain,
index_171 = select(queue_160,tail),
inference(definition_unfolding,[],[f148,f294]) ).
fof(f346,plain,
index_177 = select(queue_175,tail),
inference(definition_unfolding,[],[f150,f296]) ).
fof(f347,plain,
index_183 = select(queue_181,tail),
inference(definition_unfolding,[],[f153,f297]) ).
fof(f348,plain,
index_192 = select(queue_190,tail),
inference(definition_unfolding,[],[f157,f298]) ).
fof(f349,plain,
index_198 = select(queue_196,tail),
inference(definition_unfolding,[],[f159,f299]) ).
fof(f350,plain,
index_204 = select(queue_202,tail),
inference(definition_unfolding,[],[f161,f300]) ).
fof(f351,plain,
index_21 = select(queue_19,tail),
inference(definition_unfolding,[],[f164,f274]) ).
fof(f352,plain,
index_213 = select(queue_169,head),
inference(definition_unfolding,[],[f166,f295]) ).
fof(f353,plain,
index_3 = select(queue_1,tail),
inference(definition_unfolding,[],[f170,f271]) ).
fof(f354,plain,
index_30 = select(queue_28,tail),
inference(definition_unfolding,[],[f171,f275]) ).
fof(f355,plain,
index_36 = select(queue_34,tail),
inference(definition_unfolding,[],[f173,f276]) ).
fof(f356,plain,
index_42 = select(queue_40,tail),
inference(definition_unfolding,[],[f175,f277]) ).
fof(f357,plain,
index_51 = select(queue_49,tail),
inference(definition_unfolding,[],[f179,f278]) ).
fof(f358,plain,
index_57 = select(queue_55,tail),
inference(definition_unfolding,[],[f181,f279]) ).
fof(f359,plain,
index_63 = select(queue_61,tail),
inference(definition_unfolding,[],[f184,f280]) ).
fof(f360,plain,
index_72 = select(queue_70,tail),
inference(definition_unfolding,[],[f188,f281]) ).
fof(f361,plain,
index_78 = select(queue_7,tail),
inference(definition_unfolding,[],[f190,f272]) ).
fof(f362,plain,
index_84 = select(queue_76,tail),
inference(definition_unfolding,[],[f192,f282]) ).
fof(f363,plain,
index_9 = select(queue_211,tail),
inference(definition_unfolding,[],[f194,f301]) ).
fof(f364,plain,
index_90 = select(queue_88,tail),
inference(definition_unfolding,[],[f195,f284]) ).
fof(f365,plain,
index_99 = select(queue_97,tail),
inference(definition_unfolding,[],[f199,f285]) ).
fof(f366,plain,
queue_101 = store(queue_97,seq,earray_100),
inference(definition_unfolding,[],[f201,f285]) ).
fof(f367,plain,
queue_107 = store(queue_103,seq,earray_106),
inference(definition_unfolding,[],[f203,f286]) ).
fof(f368,plain,
queue_11 = store(queue_211,seq,earray_10),
inference(definition_unfolding,[],[f205,f301]) ).
fof(f369,plain,
queue_113 = store(queue_109,seq,earray_112),
inference(definition_unfolding,[],[f206,f287]) ).
fof(f370,plain,
queue_122 = store(queue_118,seq,earray_121),
inference(definition_unfolding,[],[f209,f288]) ).
fof(f371,plain,
queue_128 = store(queue_124,seq,earray_127),
inference(definition_unfolding,[],[f211,f289]) ).
fof(f372,plain,
queue_134 = store(queue_130,seq,earray_133),
inference(definition_unfolding,[],[f214,f290]) ).
fof(f373,plain,
queue_143 = store(queue_139,seq,earray_142),
inference(definition_unfolding,[],[f217,f291]) ).
fof(f374,plain,
queue_149 = store(queue_145,seq,earray_148),
inference(definition_unfolding,[],[f219,f292]) ).
fof(f375,plain,
queue_155 = store(queue_82,seq,earray_154),
inference(definition_unfolding,[],[f221,f283]) ).
fof(f376,plain,
queue_164 = store(queue_151,seq,earray_163),
inference(definition_unfolding,[],[f224,f293]) ).
fof(f377,plain,
queue_17 = store(queue_13,seq,earray_16),
inference(definition_unfolding,[],[f227,f273]) ).
fof(f378,plain,
queue_173 = store(queue_160,seq,earray_172),
inference(definition_unfolding,[],[f228,f294]) ).
fof(f379,plain,
queue_179 = store(queue_175,seq,earray_178),
inference(definition_unfolding,[],[f230,f296]) ).
fof(f380,plain,
queue_185 = store(queue_181,seq,earray_184),
inference(definition_unfolding,[],[f232,f297]) ).
fof(f381,plain,
queue_194 = store(queue_190,seq,earray_193),
inference(definition_unfolding,[],[f236,f298]) ).
fof(f382,plain,
queue_200 = store(queue_196,seq,earray_199),
inference(definition_unfolding,[],[f238,f299]) ).
fof(f383,plain,
queue_206 = store(queue_202,seq,earray_205),
inference(definition_unfolding,[],[f240,f300]) ).
fof(f384,plain,
queue_23 = store(queue_19,seq,earray_22),
inference(definition_unfolding,[],[f243,f274]) ).
fof(f385,plain,
queue_32 = store(queue_28,seq,earray_31),
inference(definition_unfolding,[],[f246,f275]) ).
fof(f386,plain,
queue_38 = store(queue_34,seq,earray_37),
inference(definition_unfolding,[],[f248,f276]) ).
fof(f387,plain,
queue_44 = store(queue_40,seq,earray_43),
inference(definition_unfolding,[],[f250,f277]) ).
fof(f388,plain,
queue_5 = store(queue_1,seq,earray_4),
inference(definition_unfolding,[],[f253,f271]) ).
fof(f389,plain,
queue_53 = store(queue_49,seq,earray_52),
inference(definition_unfolding,[],[f254,f278]) ).
fof(f390,plain,
queue_59 = store(queue_55,seq,earray_58),
inference(definition_unfolding,[],[f256,f279]) ).
fof(f391,plain,
queue_65 = store(queue_61,seq,earray_64),
inference(definition_unfolding,[],[f258,f280]) ).
fof(f392,plain,
queue_74 = store(queue_70,seq,earray_73),
inference(definition_unfolding,[],[f262,f281]) ).
fof(f393,plain,
queue_80 = store(queue_7,seq,earray_79),
inference(definition_unfolding,[],[f264,f272]) ).
fof(f394,plain,
queue_86 = store(queue_76,seq,earray_85),
inference(definition_unfolding,[],[f266,f282]) ).
fof(f395,plain,
queue_92 = store(queue_88,seq,earray_91),
inference(definition_unfolding,[],[f268,f284]) ).
tcf(c_351,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_352,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_353,plain,
head != tail,
inference(cnf_transformation,[],[f3]) ).
tcf(c_354,plain,
head != seq,
inference(cnf_transformation,[],[f4]) ).
tcf(c_355,plain,
tail != seq,
inference(cnf_transformation,[],[f5]) ).
tcf(c_387,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,[],[f37]) ).
tcf(c_388,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,[],[f38]) ).
tcf(c_389,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,[],[f39]) ).
tcf(c_390,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))) != X0,
inference(cnf_transformation,[],[f40]) ).
tcf(c_391,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
inference(cnf_transformation,[],[f41]) ).
tcf(c_392,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
inference(cnf_transformation,[],[f42]) ).
tcf(c_393,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
inference(cnf_transformation,[],[f43]) ).
tcf(c_394,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(cnf_transformation,[],[f44]) ).
tcf(c_395,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(cnf_transformation,[],[f45]) ).
tcf(c_396,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(cnf_transformation,[],[f46]) ).
tcf(c_397,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(cnf_transformation,[],[f47]) ).
tcf(c_398,plain,
! [X0: $i] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(cnf_transformation,[],[f48]) ).
tcf(c_399,plain,
! [X0: $i] : s(s(s(s(s(s(s(X0))))))) != X0,
inference(cnf_transformation,[],[f49]) ).
tcf(c_400,plain,
! [X0: $i] : s(s(s(s(s(s(X0)))))) != X0,
inference(cnf_transformation,[],[f50]) ).
tcf(c_401,plain,
! [X0: $i] : s(s(s(s(s(X0))))) != X0,
inference(cnf_transformation,[],[f51]) ).
tcf(c_402,plain,
! [X0: $i] : s(s(s(s(X0)))) != X0,
inference(cnf_transformation,[],[f52]) ).
tcf(c_403,plain,
! [X0: $i] : s(s(s(X0))) != X0,
inference(cnf_transformation,[],[f53]) ).
tcf(c_404,plain,
! [X0: $i] : s(s(X0)) != X0,
inference(cnf_transformation,[],[f54]) ).
tcf(c_405,plain,
! [X0: $i] : s(X0) != X0,
inference(cnf_transformation,[],[f55]) ).
tcf(c_407,plain,
store(earray_98,index_99,e21) = earray_100,
inference(cnf_transformation,[],[f57]) ).
tcf(c_408,plain,
select(queue_103,seq) = earray_104,
inference(cnf_transformation,[],[f304]) ).
tcf(c_409,plain,
store(earray_104,index_105,e22) = earray_106,
inference(cnf_transformation,[],[f59]) ).
tcf(c_410,plain,
select(queue_109,seq) = earray_110,
inference(cnf_transformation,[],[f305]) ).
tcf(c_411,plain,
store(earray_110,index_111,e23) = earray_112,
inference(cnf_transformation,[],[f61]) ).
tcf(c_412,plain,
select(queue_118,seq) = earray_119,
inference(cnf_transformation,[],[f306]) ).
tcf(c_413,plain,
store(earray_119,index_120,e24) = earray_121,
inference(cnf_transformation,[],[f63]) ).
tcf(c_414,plain,
select(queue_124,seq) = earray_125,
inference(cnf_transformation,[],[f307]) ).
tcf(c_415,plain,
store(earray_125,index_126,e25) = earray_127,
inference(cnf_transformation,[],[f65]) ).
tcf(c_416,plain,
select(queue_130,seq) = earray_131,
inference(cnf_transformation,[],[f308]) ).
tcf(c_417,plain,
store(earray_131,index_132,e26) = earray_133,
inference(cnf_transformation,[],[f67]) ).
tcf(c_419,plain,
select(queue_139,seq) = earray_140,
inference(cnf_transformation,[],[f310]) ).
tcf(c_420,plain,
store(earray_140,index_141,e27) = earray_142,
inference(cnf_transformation,[],[f70]) ).
tcf(c_421,plain,
select(queue_145,seq) = earray_146,
inference(cnf_transformation,[],[f311]) ).
tcf(c_422,plain,
store(earray_146,index_147,e28) = earray_148,
inference(cnf_transformation,[],[f72]) ).
tcf(c_425,plain,
store(earray_14,index_15,e10) = earray_16,
inference(cnf_transformation,[],[f75]) ).
tcf(c_426,plain,
select(queue_151,seq) = earray_161,
inference(cnf_transformation,[],[f313]) ).
tcf(c_427,plain,
store(earray_161,index_162,e29) = earray_163,
inference(cnf_transformation,[],[f77]) ).
tcf(c_439,plain,
select(queue_19,seq) = earray_20,
inference(cnf_transformation,[],[f320]) ).
tcf(c_442,plain,
select(queue_169,seq) = earray_212,
inference(cnf_transformation,[],[f322]) ).
tcf(c_443,plain,
store(earray_20,index_21,e11) = earray_22,
inference(cnf_transformation,[],[f93]) ).
tcf(c_444,plain,
select(queue_28,seq) = earray_29,
inference(cnf_transformation,[],[f323]) ).
tcf(c_445,plain,
store(earray_29,index_30,e12) = earray_31,
inference(cnf_transformation,[],[f95]) ).
tcf(c_446,plain,
select(queue_34,seq) = earray_35,
inference(cnf_transformation,[],[f324]) ).
tcf(c_447,plain,
store(earray_35,index_36,e13) = earray_37,
inference(cnf_transformation,[],[f97]) ).
tcf(c_449,plain,
select(queue_40,seq) = earray_41,
inference(cnf_transformation,[],[f325]) ).
tcf(c_450,plain,
store(earray_41,index_42,e14) = earray_43,
inference(cnf_transformation,[],[f100]) ).
tcf(c_451,plain,
select(queue_49,seq) = earray_50,
inference(cnf_transformation,[],[f326]) ).
tcf(c_452,plain,
store(earray_50,index_51,e15) = earray_52,
inference(cnf_transformation,[],[f102]) ).
tcf(c_453,plain,
select(queue_55,seq) = earray_56,
inference(cnf_transformation,[],[f327]) ).
tcf(c_454,plain,
store(earray_56,index_57,e16) = earray_58,
inference(cnf_transformation,[],[f104]) ).
tcf(c_455,plain,
select(queue_61,seq) = earray_62,
inference(cnf_transformation,[],[f328]) ).
tcf(c_456,plain,
store(earray_62,index_63,e17) = earray_64,
inference(cnf_transformation,[],[f106]) ).
tcf(c_457,plain,
select(queue_70,seq) = earray_71,
inference(cnf_transformation,[],[f329]) ).
tcf(c_458,plain,
store(earray_71,index_72,e18) = earray_73,
inference(cnf_transformation,[],[f108]) ).
tcf(c_462,plain,
select(queue_76,seq) = earray_83,
inference(cnf_transformation,[],[f332]) ).
tcf(c_463,plain,
store(earray_83,index_84,e19) = earray_85,
inference(cnf_transformation,[],[f113]) ).
tcf(c_464,plain,
select(queue_88,seq) = earray_89,
inference(cnf_transformation,[],[f333]) ).
tcf(c_465,plain,
store(earray_89,index_90,e20) = earray_91,
inference(cnf_transformation,[],[f115]) ).
tcf(c_466,plain,
select(queue_97,seq) = earray_98,
inference(cnf_transformation,[],[f334]) ).
tcf(c_467,plain,
select(earray_212,index_213) = elem_214,
inference(cnf_transformation,[],[f117]) ).
tcf(c_468,plain,
select(q,tail) = index_0,
inference(cnf_transformation,[],[f118]) ).
tcf(c_469,plain,
s(index_99) = index_102,
inference(cnf_transformation,[],[f119]) ).
tcf(c_470,plain,
select(queue_103,tail) = index_105,
inference(cnf_transformation,[],[f335]) ).
tcf(c_471,plain,
s(index_105) = index_108,
inference(cnf_transformation,[],[f121]) ).
tcf(c_472,plain,
select(queue_109,tail) = index_111,
inference(cnf_transformation,[],[f336]) ).
tcf(c_473,plain,
s(index_111) = index_114,
inference(cnf_transformation,[],[f123]) ).
tcf(c_474,plain,
select(queue_115,head) = index_116,
inference(cnf_transformation,[],[f124]) ).
tcf(c_475,plain,
s(index_116) = index_117,
inference(cnf_transformation,[],[f125]) ).
tcf(c_476,plain,
s(index_9) = index_12,
inference(cnf_transformation,[],[f126]) ).
tcf(c_477,plain,
select(queue_118,tail) = index_120,
inference(cnf_transformation,[],[f337]) ).
tcf(c_478,plain,
s(index_120) = index_123,
inference(cnf_transformation,[],[f128]) ).
tcf(c_479,plain,
select(queue_124,tail) = index_126,
inference(cnf_transformation,[],[f338]) ).
tcf(c_480,plain,
s(index_126) = index_129,
inference(cnf_transformation,[],[f130]) ).
tcf(c_481,plain,
select(queue_130,tail) = index_132,
inference(cnf_transformation,[],[f339]) ).
tcf(c_482,plain,
s(index_132) = index_135,
inference(cnf_transformation,[],[f132]) ).
tcf(c_483,plain,
select(queue_136,head) = index_137,
inference(cnf_transformation,[],[f133]) ).
tcf(c_484,plain,
s(index_137) = index_138,
inference(cnf_transformation,[],[f134]) ).
tcf(c_485,plain,
select(queue_139,tail) = index_141,
inference(cnf_transformation,[],[f340]) ).
tcf(c_486,plain,
s(index_141) = index_144,
inference(cnf_transformation,[],[f136]) ).
tcf(c_487,plain,
select(queue_145,tail) = index_147,
inference(cnf_transformation,[],[f341]) ).
tcf(c_488,plain,
select(queue_13,tail) = index_15,
inference(cnf_transformation,[],[f342]) ).
tcf(c_489,plain,
s(index_147) = index_150,
inference(cnf_transformation,[],[f139]) ).
tcf(c_490,plain,
select(queue_82,tail) = index_153,
inference(cnf_transformation,[],[f343]) ).
tcf(c_491,plain,
s(index_153) = index_156,
inference(cnf_transformation,[],[f141]) ).
tcf(c_492,plain,
select(queue_157,head) = index_158,
inference(cnf_transformation,[],[f142]) ).
tcf(c_493,plain,
s(index_158) = index_159,
inference(cnf_transformation,[],[f143]) ).
tcf(c_494,plain,
select(queue_151,tail) = index_162,
inference(cnf_transformation,[],[f344]) ).
tcf(c_496,plain,
select(queue_166,head) = index_167,
inference(cnf_transformation,[],[f146]) ).
tcf(c_497,plain,
s(index_167) = index_168,
inference(cnf_transformation,[],[f147]) ).
tcf(c_498,plain,
select(queue_160,tail) = index_171,
inference(cnf_transformation,[],[f345]) ).
tcf(c_499,plain,
s(index_171) = index_174,
inference(cnf_transformation,[],[f149]) ).
tcf(c_500,plain,
select(queue_175,tail) = index_177,
inference(cnf_transformation,[],[f346]) ).
tcf(c_501,plain,
s(index_15) = index_18,
inference(cnf_transformation,[],[f151]) ).
tcf(c_502,plain,
s(index_177) = index_180,
inference(cnf_transformation,[],[f152]) ).
tcf(c_503,plain,
select(queue_181,tail) = index_183,
inference(cnf_transformation,[],[f347]) ).
tcf(c_504,plain,
s(index_183) = index_186,
inference(cnf_transformation,[],[f154]) ).
tcf(c_505,plain,
select(queue_187,head) = index_188,
inference(cnf_transformation,[],[f155]) ).
tcf(c_506,plain,
s(index_188) = index_189,
inference(cnf_transformation,[],[f156]) ).
tcf(c_507,plain,
select(queue_190,tail) = index_192,
inference(cnf_transformation,[],[f348]) ).
tcf(c_508,plain,
s(index_192) = index_195,
inference(cnf_transformation,[],[f158]) ).
tcf(c_509,plain,
select(queue_196,tail) = index_198,
inference(cnf_transformation,[],[f349]) ).
tcf(c_510,plain,
s(index_198) = index_201,
inference(cnf_transformation,[],[f160]) ).
tcf(c_511,plain,
select(queue_202,tail) = index_204,
inference(cnf_transformation,[],[f350]) ).
tcf(c_512,plain,
s(index_204) = index_207,
inference(cnf_transformation,[],[f162]) ).
tcf(c_513,plain,
select(queue_208,head) = index_209,
inference(cnf_transformation,[],[f163]) ).
tcf(c_514,plain,
select(queue_19,tail) = index_21,
inference(cnf_transformation,[],[f351]) ).
tcf(c_515,plain,
s(index_209) = index_210,
inference(cnf_transformation,[],[f165]) ).
tcf(c_516,plain,
select(queue_169,head) = index_213,
inference(cnf_transformation,[],[f352]) ).
tcf(c_517,plain,
s(index_21) = index_24,
inference(cnf_transformation,[],[f167]) ).
tcf(c_518,plain,
select(queue_25,head) = index_26,
inference(cnf_transformation,[],[f168]) ).
tcf(c_519,plain,
s(index_26) = index_27,
inference(cnf_transformation,[],[f169]) ).
tcf(c_520,plain,
select(queue_1,tail) = index_3,
inference(cnf_transformation,[],[f353]) ).
tcf(c_521,plain,
select(queue_28,tail) = index_30,
inference(cnf_transformation,[],[f354]) ).
tcf(c_522,plain,
s(index_30) = index_33,
inference(cnf_transformation,[],[f172]) ).
tcf(c_523,plain,
select(queue_34,tail) = index_36,
inference(cnf_transformation,[],[f355]) ).
tcf(c_524,plain,
s(index_36) = index_39,
inference(cnf_transformation,[],[f174]) ).
tcf(c_525,plain,
select(queue_40,tail) = index_42,
inference(cnf_transformation,[],[f356]) ).
tcf(c_526,plain,
s(index_42) = index_45,
inference(cnf_transformation,[],[f176]) ).
tcf(c_527,plain,
select(queue_46,head) = index_47,
inference(cnf_transformation,[],[f177]) ).
tcf(c_528,plain,
s(index_47) = index_48,
inference(cnf_transformation,[],[f178]) ).
tcf(c_529,plain,
select(queue_49,tail) = index_51,
inference(cnf_transformation,[],[f357]) ).
tcf(c_530,plain,
s(index_51) = index_54,
inference(cnf_transformation,[],[f180]) ).
tcf(c_531,plain,
select(queue_55,tail) = index_57,
inference(cnf_transformation,[],[f358]) ).
tcf(c_532,plain,
s(index_3) = index_6,
inference(cnf_transformation,[],[f182]) ).
tcf(c_533,plain,
s(index_57) = index_60,
inference(cnf_transformation,[],[f183]) ).
tcf(c_534,plain,
select(queue_61,tail) = index_63,
inference(cnf_transformation,[],[f359]) ).
tcf(c_535,plain,
s(index_63) = index_66,
inference(cnf_transformation,[],[f185]) ).
tcf(c_536,plain,
select(queue_67,head) = index_68,
inference(cnf_transformation,[],[f186]) ).
tcf(c_537,plain,
s(index_68) = index_69,
inference(cnf_transformation,[],[f187]) ).
tcf(c_538,plain,
select(queue_70,tail) = index_72,
inference(cnf_transformation,[],[f360]) ).
tcf(c_539,plain,
s(index_72) = index_75,
inference(cnf_transformation,[],[f189]) ).
tcf(c_540,plain,
select(queue_7,tail) = index_78,
inference(cnf_transformation,[],[f361]) ).
tcf(c_541,plain,
s(index_78) = index_81,
inference(cnf_transformation,[],[f191]) ).
tcf(c_542,plain,
select(queue_76,tail) = index_84,
inference(cnf_transformation,[],[f362]) ).
tcf(c_543,plain,
s(index_84) = index_87,
inference(cnf_transformation,[],[f193]) ).
tcf(c_544,plain,
select(queue_211,tail) = index_9,
inference(cnf_transformation,[],[f363]) ).
tcf(c_545,plain,
select(queue_88,tail) = index_90,
inference(cnf_transformation,[],[f364]) ).
tcf(c_546,plain,
s(index_90) = index_93,
inference(cnf_transformation,[],[f196]) ).
tcf(c_547,plain,
select(queue_94,head) = index_95,
inference(cnf_transformation,[],[f197]) ).
tcf(c_548,plain,
s(index_95) = index_96,
inference(cnf_transformation,[],[f198]) ).
tcf(c_549,plain,
select(queue_97,tail) = index_99,
inference(cnf_transformation,[],[f365]) ).
tcf(c_550,plain,
store(q,head,index_0) = queue_1,
inference(cnf_transformation,[],[f200]) ).
tcf(c_551,plain,
store(queue_97,seq,earray_100) = queue_101,
inference(cnf_transformation,[],[f366]) ).
tcf(c_552,plain,
store(queue_101,tail,index_102) = queue_103,
inference(cnf_transformation,[],[f202]) ).
tcf(c_553,plain,
store(queue_103,seq,earray_106) = queue_107,
inference(cnf_transformation,[],[f367]) ).
tcf(c_554,plain,
store(queue_107,tail,index_108) = queue_109,
inference(cnf_transformation,[],[f204]) ).
tcf(c_555,plain,
store(queue_211,seq,earray_10) = queue_11,
inference(cnf_transformation,[],[f368]) ).
tcf(c_556,plain,
store(queue_109,seq,earray_112) = queue_113,
inference(cnf_transformation,[],[f369]) ).
tcf(c_557,plain,
store(queue_113,tail,index_114) = queue_115,
inference(cnf_transformation,[],[f207]) ).
tcf(c_558,plain,
store(queue_115,head,index_117) = queue_118,
inference(cnf_transformation,[],[f208]) ).
tcf(c_559,plain,
store(queue_118,seq,earray_121) = queue_122,
inference(cnf_transformation,[],[f370]) ).
tcf(c_560,plain,
store(queue_122,tail,index_123) = queue_124,
inference(cnf_transformation,[],[f210]) ).
tcf(c_561,plain,
store(queue_124,seq,earray_127) = queue_128,
inference(cnf_transformation,[],[f371]) ).
tcf(c_562,plain,
store(queue_11,tail,index_12) = queue_13,
inference(cnf_transformation,[],[f212]) ).
tcf(c_563,plain,
store(queue_128,tail,index_129) = queue_130,
inference(cnf_transformation,[],[f213]) ).
tcf(c_564,plain,
store(queue_130,seq,earray_133) = queue_134,
inference(cnf_transformation,[],[f372]) ).
tcf(c_565,plain,
store(queue_134,tail,index_135) = queue_136,
inference(cnf_transformation,[],[f215]) ).
tcf(c_566,plain,
store(queue_136,head,index_138) = queue_139,
inference(cnf_transformation,[],[f216]) ).
tcf(c_567,plain,
store(queue_139,seq,earray_142) = queue_143,
inference(cnf_transformation,[],[f373]) ).
tcf(c_568,plain,
store(queue_143,tail,index_144) = queue_145,
inference(cnf_transformation,[],[f218]) ).
tcf(c_569,plain,
store(queue_145,seq,earray_148) = queue_149,
inference(cnf_transformation,[],[f374]) ).
tcf(c_570,plain,
store(queue_149,tail,index_150) = queue_151,
inference(cnf_transformation,[],[f220]) ).
tcf(c_571,plain,
store(queue_82,seq,earray_154) = queue_155,
inference(cnf_transformation,[],[f375]) ).
tcf(c_572,plain,
store(queue_155,tail,index_156) = queue_157,
inference(cnf_transformation,[],[f222]) ).
tcf(c_573,plain,
store(queue_157,head,index_159) = queue_160,
inference(cnf_transformation,[],[f223]) ).
tcf(c_574,plain,
store(queue_151,seq,earray_163) = queue_164,
inference(cnf_transformation,[],[f376]) ).
tcf(c_575,plain,
store(queue_164,tail,index_165) = queue_166,
inference(cnf_transformation,[],[f225]) ).
tcf(c_576,plain,
store(queue_166,head,index_168) = queue_169,
inference(cnf_transformation,[],[f226]) ).
tcf(c_577,plain,
store(queue_13,seq,earray_16) = queue_17,
inference(cnf_transformation,[],[f377]) ).
tcf(c_578,plain,
store(queue_160,seq,earray_172) = queue_173,
inference(cnf_transformation,[],[f378]) ).
tcf(c_579,plain,
store(queue_173,tail,index_174) = queue_175,
inference(cnf_transformation,[],[f229]) ).
tcf(c_580,plain,
store(queue_175,seq,earray_178) = queue_179,
inference(cnf_transformation,[],[f379]) ).
tcf(c_581,plain,
store(queue_179,tail,index_180) = queue_181,
inference(cnf_transformation,[],[f231]) ).
tcf(c_582,plain,
store(queue_181,seq,earray_184) = queue_185,
inference(cnf_transformation,[],[f380]) ).
tcf(c_583,plain,
store(queue_185,tail,index_186) = queue_187,
inference(cnf_transformation,[],[f233]) ).
tcf(c_584,plain,
store(queue_17,tail,index_18) = queue_19,
inference(cnf_transformation,[],[f234]) ).
tcf(c_585,plain,
store(queue_187,head,index_189) = queue_190,
inference(cnf_transformation,[],[f235]) ).
tcf(c_586,plain,
store(queue_190,seq,earray_193) = queue_194,
inference(cnf_transformation,[],[f381]) ).
tcf(c_587,plain,
store(queue_194,tail,index_195) = queue_196,
inference(cnf_transformation,[],[f237]) ).
tcf(c_588,plain,
store(queue_196,seq,earray_199) = queue_200,
inference(cnf_transformation,[],[f382]) ).
tcf(c_589,plain,
store(queue_200,tail,index_201) = queue_202,
inference(cnf_transformation,[],[f239]) ).
tcf(c_590,plain,
store(queue_202,seq,earray_205) = queue_206,
inference(cnf_transformation,[],[f383]) ).
tcf(c_591,plain,
store(queue_206,tail,index_207) = queue_208,
inference(cnf_transformation,[],[f241]) ).
tcf(c_592,plain,
store(queue_208,head,index_210) = queue_211,
inference(cnf_transformation,[],[f242]) ).
tcf(c_593,plain,
store(queue_19,seq,earray_22) = queue_23,
inference(cnf_transformation,[],[f384]) ).
tcf(c_594,plain,
store(queue_23,tail,index_24) = queue_25,
inference(cnf_transformation,[],[f244]) ).
tcf(c_595,plain,
store(queue_25,head,index_27) = queue_28,
inference(cnf_transformation,[],[f245]) ).
tcf(c_596,plain,
store(queue_28,seq,earray_31) = queue_32,
inference(cnf_transformation,[],[f385]) ).
tcf(c_597,plain,
store(queue_32,tail,index_33) = queue_34,
inference(cnf_transformation,[],[f247]) ).
tcf(c_598,plain,
store(queue_34,seq,earray_37) = queue_38,
inference(cnf_transformation,[],[f386]) ).
tcf(c_599,plain,
store(queue_38,tail,index_39) = queue_40,
inference(cnf_transformation,[],[f249]) ).
tcf(c_600,plain,
store(queue_40,seq,earray_43) = queue_44,
inference(cnf_transformation,[],[f387]) ).
tcf(c_601,plain,
store(queue_44,tail,index_45) = queue_46,
inference(cnf_transformation,[],[f251]) ).
tcf(c_602,plain,
store(queue_46,head,index_48) = queue_49,
inference(cnf_transformation,[],[f252]) ).
tcf(c_603,plain,
store(queue_1,seq,earray_4) = queue_5,
inference(cnf_transformation,[],[f388]) ).
tcf(c_604,plain,
store(queue_49,seq,earray_52) = queue_53,
inference(cnf_transformation,[],[f389]) ).
tcf(c_605,plain,
store(queue_53,tail,index_54) = queue_55,
inference(cnf_transformation,[],[f255]) ).
tcf(c_606,plain,
store(queue_55,seq,earray_58) = queue_59,
inference(cnf_transformation,[],[f390]) ).
tcf(c_607,plain,
store(queue_59,tail,index_60) = queue_61,
inference(cnf_transformation,[],[f257]) ).
tcf(c_608,plain,
store(queue_61,seq,earray_64) = queue_65,
inference(cnf_transformation,[],[f391]) ).
tcf(c_609,plain,
store(queue_65,tail,index_66) = queue_67,
inference(cnf_transformation,[],[f259]) ).
tcf(c_610,plain,
store(queue_5,tail,index_6) = queue_7,
inference(cnf_transformation,[],[f260]) ).
tcf(c_611,plain,
store(queue_67,head,index_69) = queue_70,
inference(cnf_transformation,[],[f261]) ).
tcf(c_612,plain,
store(queue_70,seq,earray_73) = queue_74,
inference(cnf_transformation,[],[f392]) ).
tcf(c_613,plain,
store(queue_74,tail,index_75) = queue_76,
inference(cnf_transformation,[],[f263]) ).
tcf(c_614,plain,
store(queue_7,seq,earray_79) = queue_80,
inference(cnf_transformation,[],[f393]) ).
tcf(c_615,plain,
store(queue_80,tail,index_81) = queue_82,
inference(cnf_transformation,[],[f265]) ).
tcf(c_616,plain,
store(queue_76,seq,earray_85) = queue_86,
inference(cnf_transformation,[],[f394]) ).
tcf(c_617,plain,
store(queue_86,tail,index_87) = queue_88,
inference(cnf_transformation,[],[f267]) ).
tcf(c_618,plain,
store(queue_88,seq,earray_91) = queue_92,
inference(cnf_transformation,[],[f395]) ).
tcf(c_619,plain,
store(queue_92,tail,index_93) = queue_94,
inference(cnf_transformation,[],[f269]) ).
tcf(c_620,plain,
store(queue_94,head,index_96) = queue_97,
inference(cnf_transformation,[],[f270]) ).
tcf(c_621,negated_conjecture,
e10 != elem_214,
inference(cnf_transformation,[],[f303]) ).
tcf(c_1225,negated_conjecture,
e10 != elem_214,
inference(demodulation,[status(thm)],[c_621]) ).
tcf(c_1805,plain,
select(earray_16,index_15) = e10,
inference(superposition,[status(thm)],[c_425,c_351]) ).
tcf(c_1822,plain,
index_15 != index_18,
inference(superposition,[status(thm)],[c_501,c_405]) ).
tcf(c_1916,plain,
s(index_18) != index_15,
inference(superposition,[status(thm)],[c_501,c_404]) ).
tcf(c_1945,plain,
! [X0: $i] :
( ( X0 = index_99 )
| ( select(earray_100,X0) = select(earray_98,X0) ) ),
inference(superposition,[status(thm)],[c_407,c_352]) ).
tcf(c_1950,plain,
! [X0: $i] :
( ( X0 = index_105 )
| ( select(earray_104,X0) = select(earray_106,X0) ) ),
inference(superposition,[status(thm)],[c_409,c_352]) ).
tcf(c_1955,plain,
! [X0: $i] :
( ( X0 = index_111 )
| ( select(earray_110,X0) = select(earray_112,X0) ) ),
inference(superposition,[status(thm)],[c_411,c_352]) ).
tcf(c_1960,plain,
! [X0: $i] :
( ( X0 = index_120 )
| ( select(earray_119,X0) = select(earray_121,X0) ) ),
inference(superposition,[status(thm)],[c_413,c_352]) ).
tcf(c_1965,plain,
! [X0: $i] :
( ( X0 = index_126 )
| ( select(earray_125,X0) = select(earray_127,X0) ) ),
inference(superposition,[status(thm)],[c_415,c_352]) ).
tcf(c_1970,plain,
! [X0: $i] :
( ( X0 = index_132 )
| ( select(earray_131,X0) = select(earray_133,X0) ) ),
inference(superposition,[status(thm)],[c_417,c_352]) ).
tcf(c_1975,plain,
! [X0: $i] :
( ( X0 = index_141 )
| ( select(earray_140,X0) = select(earray_142,X0) ) ),
inference(superposition,[status(thm)],[c_420,c_352]) ).
tcf(c_1980,plain,
! [X0: $i] :
( ( X0 = index_147 )
| ( select(earray_146,X0) = select(earray_148,X0) ) ),
inference(superposition,[status(thm)],[c_422,c_352]) ).
tcf(c_1990,plain,
! [X0: $i] :
( ( X0 = index_162 )
| ( select(earray_161,X0) = select(earray_163,X0) ) ),
inference(superposition,[status(thm)],[c_427,c_352]) ).
tcf(c_2025,plain,
! [X0: $i] :
( ( X0 = index_21 )
| ( select(earray_20,X0) = select(earray_22,X0) ) ),
inference(superposition,[status(thm)],[c_443,c_352]) ).
tcf(c_2030,plain,
! [X0: $i] :
( ( X0 = index_30 )
| ( select(earray_29,X0) = select(earray_31,X0) ) ),
inference(superposition,[status(thm)],[c_445,c_352]) ).
tcf(c_2035,plain,
! [X0: $i] :
( ( X0 = index_36 )
| ( select(earray_35,X0) = select(earray_37,X0) ) ),
inference(superposition,[status(thm)],[c_447,c_352]) ).
tcf(c_2045,plain,
! [X0: $i] :
( ( X0 = index_42 )
| ( select(earray_41,X0) = select(earray_43,X0) ) ),
inference(superposition,[status(thm)],[c_450,c_352]) ).
tcf(c_2050,plain,
! [X0: $i] :
( ( X0 = index_51 )
| ( select(earray_50,X0) = select(earray_52,X0) ) ),
inference(superposition,[status(thm)],[c_452,c_352]) ).
tcf(c_2055,plain,
! [X0: $i] :
( ( X0 = index_57 )
| ( select(earray_56,X0) = select(earray_58,X0) ) ),
inference(superposition,[status(thm)],[c_454,c_352]) ).
tcf(c_2060,plain,
! [X0: $i] :
( ( X0 = index_63 )
| ( select(earray_62,X0) = select(earray_64,X0) ) ),
inference(superposition,[status(thm)],[c_456,c_352]) ).
tcf(c_2065,plain,
! [X0: $i] :
( ( X0 = index_72 )
| ( select(earray_71,X0) = select(earray_73,X0) ) ),
inference(superposition,[status(thm)],[c_458,c_352]) ).
tcf(c_2075,plain,
! [X0: $i] :
( ( X0 = index_84 )
| ( select(earray_83,X0) = select(earray_85,X0) ) ),
inference(superposition,[status(thm)],[c_463,c_352]) ).
tcf(c_2085,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(q,X0) = select(queue_1,X0) ) ),
inference(superposition,[status(thm)],[c_550,c_352]) ).
tcf(c_2086,plain,
select(queue_1,head) = index_0,
inference(superposition,[status(thm)],[c_550,c_351]) ).
tcf(c_2090,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_101,X0) = select(queue_97,X0) ) ),
inference(superposition,[status(thm)],[c_551,c_352]) ).
tcf(c_2091,plain,
select(queue_101,seq) = earray_100,
inference(superposition,[status(thm)],[c_551,c_351]) ).
tcf(c_2094,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_101,X0) = select(queue_103,X0) ) ),
inference(superposition,[status(thm)],[c_552,c_352]) ).
tcf(c_2095,plain,
select(queue_103,tail) = index_102,
inference(superposition,[status(thm)],[c_552,c_351]) ).
tcf(c_2096,plain,
index_105 = index_102,
inference(light_normalisation,[status(thm)],[c_2095,c_470]) ).
tcf(c_2103,plain,
s(index_99) = index_105,
inference(demodulation,[status(thm)],[c_469,c_2096]) ).
tcf(c_2110,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_103,X0) = select(queue_107,X0) ) ),
inference(superposition,[status(thm)],[c_553,c_352]) ).
tcf(c_2111,plain,
select(queue_107,seq) = earray_106,
inference(superposition,[status(thm)],[c_553,c_351]) ).
tcf(c_2114,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_107,X0) = select(queue_109,X0) ) ),
inference(superposition,[status(thm)],[c_554,c_352]) ).
tcf(c_2115,plain,
select(queue_109,tail) = index_108,
inference(superposition,[status(thm)],[c_554,c_351]) ).
tcf(c_2116,plain,
index_111 = index_108,
inference(light_normalisation,[status(thm)],[c_2115,c_472]) ).
tcf(c_2124,plain,
s(index_105) = index_111,
inference(demodulation,[status(thm)],[c_471,c_2116]) ).
tcf(c_2128,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_11,X0) = select(queue_211,X0) ) ),
inference(superposition,[status(thm)],[c_555,c_352]) ).
tcf(c_2132,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_109,X0) = select(queue_113,X0) ) ),
inference(superposition,[status(thm)],[c_556,c_352]) ).
tcf(c_2133,plain,
select(queue_113,seq) = earray_112,
inference(superposition,[status(thm)],[c_556,c_351]) ).
tcf(c_2139,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_115,X0) = select(queue_113,X0) ) ),
inference(superposition,[status(thm)],[c_557,c_352]) ).
tcf(c_2140,plain,
select(queue_115,tail) = index_114,
inference(superposition,[status(thm)],[c_557,c_351]) ).
tcf(c_2144,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_115,X0) = select(queue_118,X0) ) ),
inference(superposition,[status(thm)],[c_558,c_352]) ).
tcf(c_2145,plain,
select(queue_118,head) = index_117,
inference(superposition,[status(thm)],[c_558,c_351]) ).
tcf(c_2149,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_118,X0) = select(queue_122,X0) ) ),
inference(superposition,[status(thm)],[c_559,c_352]) ).
tcf(c_2150,plain,
select(queue_122,seq) = earray_121,
inference(superposition,[status(thm)],[c_559,c_351]) ).
tcf(c_2153,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_122,X0) = select(queue_124,X0) ) ),
inference(superposition,[status(thm)],[c_560,c_352]) ).
tcf(c_2154,plain,
select(queue_124,tail) = index_123,
inference(superposition,[status(thm)],[c_560,c_351]) ).
tcf(c_2155,plain,
index_126 = index_123,
inference(light_normalisation,[status(thm)],[c_2154,c_479]) ).
tcf(c_2162,plain,
s(index_120) = index_126,
inference(demodulation,[status(thm)],[c_478,c_2155]) ).
tcf(c_2166,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_124,X0) = select(queue_128,X0) ) ),
inference(superposition,[status(thm)],[c_561,c_352]) ).
tcf(c_2167,plain,
select(queue_128,seq) = earray_127,
inference(superposition,[status(thm)],[c_561,c_351]) ).
tcf(c_2170,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_11,X0) = select(queue_13,X0) ) ),
inference(superposition,[status(thm)],[c_562,c_352]) ).
tcf(c_2171,plain,
select(queue_13,tail) = index_12,
inference(superposition,[status(thm)],[c_562,c_351]) ).
tcf(c_2172,plain,
index_15 = index_12,
inference(light_normalisation,[status(thm)],[c_2171,c_488]) ).
tcf(c_2179,plain,
s(index_9) = index_15,
inference(demodulation,[status(thm)],[c_476,c_2172]) ).
tcf(c_2189,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_128,X0) = select(queue_130,X0) ) ),
inference(superposition,[status(thm)],[c_563,c_352]) ).
tcf(c_2190,plain,
select(queue_130,tail) = index_129,
inference(superposition,[status(thm)],[c_563,c_351]) ).
tcf(c_2191,plain,
index_132 = index_129,
inference(light_normalisation,[status(thm)],[c_2190,c_481]) ).
tcf(c_2199,plain,
s(index_126) = index_132,
inference(demodulation,[status(thm)],[c_480,c_2191]) ).
tcf(c_2203,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_130,X0) = select(queue_134,X0) ) ),
inference(superposition,[status(thm)],[c_564,c_352]) ).
tcf(c_2204,plain,
select(queue_134,seq) = earray_133,
inference(superposition,[status(thm)],[c_564,c_351]) ).
tcf(c_2207,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_136,X0) = select(queue_134,X0) ) ),
inference(superposition,[status(thm)],[c_565,c_352]) ).
tcf(c_2208,plain,
select(queue_136,tail) = index_135,
inference(superposition,[status(thm)],[c_565,c_351]) ).
tcf(c_2317,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_136,X0) = select(queue_139,X0) ) ),
inference(superposition,[status(thm)],[c_566,c_352]) ).
tcf(c_2318,plain,
select(queue_139,head) = index_138,
inference(superposition,[status(thm)],[c_566,c_351]) ).
tcf(c_2322,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_139,X0) = select(queue_143,X0) ) ),
inference(superposition,[status(thm)],[c_567,c_352]) ).
tcf(c_2323,plain,
select(queue_143,seq) = earray_142,
inference(superposition,[status(thm)],[c_567,c_351]) ).
tcf(c_2329,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_143,X0) = select(queue_145,X0) ) ),
inference(superposition,[status(thm)],[c_568,c_352]) ).
tcf(c_2330,plain,
select(queue_145,tail) = index_144,
inference(superposition,[status(thm)],[c_568,c_351]) ).
tcf(c_2331,plain,
index_147 = index_144,
inference(light_normalisation,[status(thm)],[c_2330,c_487]) ).
tcf(c_2338,plain,
s(index_141) = index_147,
inference(demodulation,[status(thm)],[c_486,c_2331]) ).
tcf(c_2345,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_145,X0) = select(queue_149,X0) ) ),
inference(superposition,[status(thm)],[c_569,c_352]) ).
tcf(c_2346,plain,
select(queue_149,seq) = earray_148,
inference(superposition,[status(thm)],[c_569,c_351]) ).
tcf(c_2349,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_149,X0) = select(queue_151,X0) ) ),
inference(superposition,[status(thm)],[c_570,c_352]) ).
tcf(c_2350,plain,
select(queue_151,tail) = index_150,
inference(superposition,[status(thm)],[c_570,c_351]) ).
tcf(c_2351,plain,
index_162 = index_150,
inference(light_normalisation,[status(thm)],[c_2350,c_494]) ).
tcf(c_2358,plain,
s(index_147) = index_162,
inference(demodulation,[status(thm)],[c_489,c_2351]) ).
tcf(c_2362,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_155,X0) = select(queue_82,X0) ) ),
inference(superposition,[status(thm)],[c_571,c_352]) ).
tcf(c_2366,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_157,X0) = select(queue_155,X0) ) ),
inference(superposition,[status(thm)],[c_572,c_352]) ).
tcf(c_2367,plain,
select(queue_157,tail) = index_156,
inference(superposition,[status(thm)],[c_572,c_351]) ).
tcf(c_2375,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_157,X0) = select(queue_160,X0) ) ),
inference(superposition,[status(thm)],[c_573,c_352]) ).
tcf(c_2376,plain,
select(queue_160,head) = index_159,
inference(superposition,[status(thm)],[c_573,c_351]) ).
tcf(c_2380,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_151,X0) = select(queue_164,X0) ) ),
inference(superposition,[status(thm)],[c_574,c_352]) ).
tcf(c_2381,plain,
select(queue_164,seq) = earray_163,
inference(superposition,[status(thm)],[c_574,c_351]) ).
tcf(c_2384,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_166,X0) = select(queue_164,X0) ) ),
inference(superposition,[status(thm)],[c_575,c_352]) ).
tcf(c_2389,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_166,X0) = select(queue_169,X0) ) ),
inference(superposition,[status(thm)],[c_576,c_352]) ).
tcf(c_2390,plain,
select(queue_169,head) = index_168,
inference(superposition,[status(thm)],[c_576,c_351]) ).
tcf(c_2391,plain,
index_213 = index_168,
inference(light_normalisation,[status(thm)],[c_2390,c_516]) ).
tcf(c_2397,plain,
s(index_167) = index_213,
inference(demodulation,[status(thm)],[c_497,c_2391]) ).
tcf(c_2399,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_13,X0) = select(queue_17,X0) ) ),
inference(superposition,[status(thm)],[c_577,c_352]) ).
tcf(c_2400,plain,
select(queue_17,seq) = earray_16,
inference(superposition,[status(thm)],[c_577,c_351]) ).
tcf(c_2403,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_160,X0) = select(queue_173,X0) ) ),
inference(superposition,[status(thm)],[c_578,c_352]) ).
tcf(c_2410,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_173,X0) = select(queue_175,X0) ) ),
inference(superposition,[status(thm)],[c_579,c_352]) ).
tcf(c_2411,plain,
select(queue_175,tail) = index_174,
inference(superposition,[status(thm)],[c_579,c_351]) ).
tcf(c_2412,plain,
index_177 = index_174,
inference(light_normalisation,[status(thm)],[c_2411,c_500]) ).
tcf(c_2418,plain,
s(index_171) = index_177,
inference(demodulation,[status(thm)],[c_499,c_2412]) ).
tcf(c_2425,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_175,X0) = select(queue_179,X0) ) ),
inference(superposition,[status(thm)],[c_580,c_352]) ).
tcf(c_2429,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_179,X0) = select(queue_181,X0) ) ),
inference(superposition,[status(thm)],[c_581,c_352]) ).
tcf(c_2430,plain,
select(queue_181,tail) = index_180,
inference(superposition,[status(thm)],[c_581,c_351]) ).
tcf(c_2431,plain,
index_183 = index_180,
inference(light_normalisation,[status(thm)],[c_2430,c_503]) ).
tcf(c_2438,plain,
s(index_177) = index_183,
inference(demodulation,[status(thm)],[c_502,c_2431]) ).
tcf(c_2441,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_181,X0) = select(queue_185,X0) ) ),
inference(superposition,[status(thm)],[c_582,c_352]) ).
tcf(c_2445,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_187,X0) = select(queue_185,X0) ) ),
inference(superposition,[status(thm)],[c_583,c_352]) ).
tcf(c_2446,plain,
select(queue_187,tail) = index_186,
inference(superposition,[status(thm)],[c_583,c_351]) ).
tcf(c_2454,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_17,X0) = select(queue_19,X0) ) ),
inference(superposition,[status(thm)],[c_584,c_352]) ).
tcf(c_2455,plain,
select(queue_19,tail) = index_18,
inference(superposition,[status(thm)],[c_584,c_351]) ).
tcf(c_2456,plain,
index_21 = index_18,
inference(light_normalisation,[status(thm)],[c_2455,c_514]) ).
tcf(c_2461,plain,
s(index_21) != index_15,
inference(demodulation,[status(thm)],[c_1916,c_2456]) ).
tcf(c_2462,plain,
index_15 != index_21,
inference(demodulation,[status(thm)],[c_1822,c_2456]) ).
tcf(c_2463,plain,
s(index_15) = index_21,
inference(demodulation,[status(thm)],[c_501,c_2456]) ).
tcf(c_2464,plain,
index_15 != index_24,
inference(light_normalisation,[status(thm)],[c_2461,c_517]) ).
tcf(c_2466,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_187,X0) = select(queue_190,X0) ) ),
inference(superposition,[status(thm)],[c_585,c_352]) ).
tcf(c_2467,plain,
select(queue_190,head) = index_189,
inference(superposition,[status(thm)],[c_585,c_351]) ).
tcf(c_2471,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_190,X0) = select(queue_194,X0) ) ),
inference(superposition,[status(thm)],[c_586,c_352]) ).
tcf(c_2475,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_194,X0) = select(queue_196,X0) ) ),
inference(superposition,[status(thm)],[c_587,c_352]) ).
tcf(c_2476,plain,
select(queue_196,tail) = index_195,
inference(superposition,[status(thm)],[c_587,c_351]) ).
tcf(c_2477,plain,
index_198 = index_195,
inference(light_normalisation,[status(thm)],[c_2476,c_509]) ).
tcf(c_2483,plain,
s(index_192) = index_198,
inference(demodulation,[status(thm)],[c_508,c_2477]) ).
tcf(c_2486,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_196,X0) = select(queue_200,X0) ) ),
inference(superposition,[status(thm)],[c_588,c_352]) ).
tcf(c_2498,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_200,X0) = select(queue_202,X0) ) ),
inference(superposition,[status(thm)],[c_589,c_352]) ).
tcf(c_2499,plain,
select(queue_202,tail) = index_201,
inference(superposition,[status(thm)],[c_589,c_351]) ).
tcf(c_2500,plain,
index_204 = index_201,
inference(light_normalisation,[status(thm)],[c_2499,c_511]) ).
tcf(c_2507,plain,
s(index_198) = index_204,
inference(demodulation,[status(thm)],[c_510,c_2500]) ).
tcf(c_2511,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_202,X0) = select(queue_206,X0) ) ),
inference(superposition,[status(thm)],[c_590,c_352]) ).
tcf(c_2515,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_208,X0) = select(queue_206,X0) ) ),
inference(superposition,[status(thm)],[c_591,c_352]) ).
tcf(c_2516,plain,
select(queue_208,tail) = index_207,
inference(superposition,[status(thm)],[c_591,c_351]) ).
tcf(c_2520,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_208,X0) = select(queue_211,X0) ) ),
inference(superposition,[status(thm)],[c_592,c_352]) ).
tcf(c_2521,plain,
select(queue_211,head) = index_210,
inference(superposition,[status(thm)],[c_592,c_351]) ).
tcf(c_2525,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_19,X0) = select(queue_23,X0) ) ),
inference(superposition,[status(thm)],[c_593,c_352]) ).
tcf(c_2526,plain,
select(queue_23,seq) = earray_22,
inference(superposition,[status(thm)],[c_593,c_351]) ).
tcf(c_2533,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_25,X0) = select(queue_23,X0) ) ),
inference(superposition,[status(thm)],[c_594,c_352]) ).
tcf(c_2534,plain,
select(queue_25,tail) = index_24,
inference(superposition,[status(thm)],[c_594,c_351]) ).
tcf(c_2538,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_25,X0) = select(queue_28,X0) ) ),
inference(superposition,[status(thm)],[c_595,c_352]) ).
tcf(c_2539,plain,
select(queue_28,head) = index_27,
inference(superposition,[status(thm)],[c_595,c_351]) ).
tcf(c_2543,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_28,X0) = select(queue_32,X0) ) ),
inference(superposition,[status(thm)],[c_596,c_352]) ).
tcf(c_2544,plain,
select(queue_32,seq) = earray_31,
inference(superposition,[status(thm)],[c_596,c_351]) ).
tcf(c_2548,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_32,X0) = select(queue_34,X0) ) ),
inference(superposition,[status(thm)],[c_597,c_352]) ).
tcf(c_2549,plain,
select(queue_34,tail) = index_33,
inference(superposition,[status(thm)],[c_597,c_351]) ).
tcf(c_2550,plain,
index_36 = index_33,
inference(light_normalisation,[status(thm)],[c_2549,c_523]) ).
tcf(c_2556,plain,
s(index_30) = index_36,
inference(demodulation,[status(thm)],[c_522,c_2550]) ).
tcf(c_2559,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_34,X0) = select(queue_38,X0) ) ),
inference(superposition,[status(thm)],[c_598,c_352]) ).
tcf(c_2560,plain,
select(queue_38,seq) = earray_37,
inference(superposition,[status(thm)],[c_598,c_351]) ).
tcf(c_2563,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_38,X0) = select(queue_40,X0) ) ),
inference(superposition,[status(thm)],[c_599,c_352]) ).
tcf(c_2564,plain,
select(queue_40,tail) = index_39,
inference(superposition,[status(thm)],[c_599,c_351]) ).
tcf(c_2565,plain,
index_42 = index_39,
inference(light_normalisation,[status(thm)],[c_2564,c_525]) ).
tcf(c_2571,plain,
s(index_36) = index_42,
inference(demodulation,[status(thm)],[c_524,c_2565]) ).
tcf(c_2574,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_40,X0) = select(queue_44,X0) ) ),
inference(superposition,[status(thm)],[c_600,c_352]) ).
tcf(c_2575,plain,
select(queue_44,seq) = earray_43,
inference(superposition,[status(thm)],[c_600,c_351]) ).
tcf(c_2587,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_46,X0) = select(queue_44,X0) ) ),
inference(superposition,[status(thm)],[c_601,c_352]) ).
tcf(c_2588,plain,
select(queue_46,tail) = index_45,
inference(superposition,[status(thm)],[c_601,c_351]) ).
tcf(c_2593,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_46,X0) = select(queue_49,X0) ) ),
inference(superposition,[status(thm)],[c_602,c_352]) ).
tcf(c_2594,plain,
select(queue_49,head) = index_48,
inference(superposition,[status(thm)],[c_602,c_351]) ).
tcf(c_2706,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_1,X0) = select(queue_5,X0) ) ),
inference(superposition,[status(thm)],[c_603,c_352]) ).
tcf(c_2710,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_49,X0) = select(queue_53,X0) ) ),
inference(superposition,[status(thm)],[c_604,c_352]) ).
tcf(c_2711,plain,
select(queue_53,seq) = earray_52,
inference(superposition,[status(thm)],[c_604,c_351]) ).
tcf(c_2714,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_53,X0) = select(queue_55,X0) ) ),
inference(superposition,[status(thm)],[c_605,c_352]) ).
tcf(c_2715,plain,
select(queue_55,tail) = index_54,
inference(superposition,[status(thm)],[c_605,c_351]) ).
tcf(c_2716,plain,
index_57 = index_54,
inference(light_normalisation,[status(thm)],[c_2715,c_531]) ).
tcf(c_2722,plain,
s(index_51) = index_57,
inference(demodulation,[status(thm)],[c_530,c_2716]) ).
tcf(c_2729,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_55,X0) = select(queue_59,X0) ) ),
inference(superposition,[status(thm)],[c_606,c_352]) ).
tcf(c_2730,plain,
select(queue_59,seq) = earray_58,
inference(superposition,[status(thm)],[c_606,c_351]) ).
tcf(c_2733,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_59,X0) = select(queue_61,X0) ) ),
inference(superposition,[status(thm)],[c_607,c_352]) ).
tcf(c_2734,plain,
select(queue_61,tail) = index_60,
inference(superposition,[status(thm)],[c_607,c_351]) ).
tcf(c_2735,plain,
index_63 = index_60,
inference(light_normalisation,[status(thm)],[c_2734,c_534]) ).
tcf(c_2742,plain,
s(index_57) = index_63,
inference(demodulation,[status(thm)],[c_533,c_2735]) ).
tcf(c_2746,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_61,X0) = select(queue_65,X0) ) ),
inference(superposition,[status(thm)],[c_608,c_352]) ).
tcf(c_2747,plain,
select(queue_65,seq) = earray_64,
inference(superposition,[status(thm)],[c_608,c_351]) ).
tcf(c_2750,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_67,X0) = select(queue_65,X0) ) ),
inference(superposition,[status(thm)],[c_609,c_352]) ).
tcf(c_2751,plain,
select(queue_67,tail) = index_66,
inference(superposition,[status(thm)],[c_609,c_351]) ).
tcf(c_2755,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_5,X0) = select(queue_7,X0) ) ),
inference(superposition,[status(thm)],[c_610,c_352]) ).
tcf(c_2756,plain,
select(queue_7,tail) = index_6,
inference(superposition,[status(thm)],[c_610,c_351]) ).
tcf(c_2757,plain,
index_78 = index_6,
inference(light_normalisation,[status(thm)],[c_2756,c_540]) ).
tcf(c_2763,plain,
s(index_3) = index_78,
inference(demodulation,[status(thm)],[c_532,c_2757]) ).
tcf(c_2766,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_67,X0) = select(queue_70,X0) ) ),
inference(superposition,[status(thm)],[c_611,c_352]) ).
tcf(c_2767,plain,
select(queue_70,head) = index_69,
inference(superposition,[status(thm)],[c_611,c_351]) ).
tcf(c_2779,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_70,X0) = select(queue_74,X0) ) ),
inference(superposition,[status(thm)],[c_612,c_352]) ).
tcf(c_2780,plain,
select(queue_74,seq) = earray_73,
inference(superposition,[status(thm)],[c_612,c_351]) ).
tcf(c_2783,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_74,X0) = select(queue_76,X0) ) ),
inference(superposition,[status(thm)],[c_613,c_352]) ).
tcf(c_2784,plain,
select(queue_76,tail) = index_75,
inference(superposition,[status(thm)],[c_613,c_351]) ).
tcf(c_2785,plain,
index_84 = index_75,
inference(light_normalisation,[status(thm)],[c_2784,c_542]) ).
tcf(c_2791,plain,
s(index_72) = index_84,
inference(demodulation,[status(thm)],[c_539,c_2785]) ).
tcf(c_2794,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_7,X0) = select(queue_80,X0) ) ),
inference(superposition,[status(thm)],[c_614,c_352]) ).
tcf(c_2798,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_80,X0) = select(queue_82,X0) ) ),
inference(superposition,[status(thm)],[c_615,c_352]) ).
tcf(c_2799,plain,
select(queue_82,tail) = index_81,
inference(superposition,[status(thm)],[c_615,c_351]) ).
tcf(c_2800,plain,
index_153 = index_81,
inference(light_normalisation,[status(thm)],[c_2799,c_490]) ).
tcf(c_2807,plain,
s(index_78) = index_153,
inference(demodulation,[status(thm)],[c_541,c_2800]) ).
tcf(c_2810,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_76,X0) = select(queue_86,X0) ) ),
inference(superposition,[status(thm)],[c_616,c_352]) ).
tcf(c_2811,plain,
select(queue_86,seq) = earray_85,
inference(superposition,[status(thm)],[c_616,c_351]) ).
tcf(c_2822,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_86,X0) = select(queue_88,X0) ) ),
inference(superposition,[status(thm)],[c_617,c_352]) ).
tcf(c_2823,plain,
select(queue_88,tail) = index_87,
inference(superposition,[status(thm)],[c_617,c_351]) ).
tcf(c_2824,plain,
index_90 = index_87,
inference(light_normalisation,[status(thm)],[c_2823,c_545]) ).
tcf(c_2831,plain,
s(index_84) = index_90,
inference(demodulation,[status(thm)],[c_543,c_2824]) ).
tcf(c_2834,plain,
! [X0: $i] :
( ( X0 = seq )
| ( select(queue_88,X0) = select(queue_92,X0) ) ),
inference(superposition,[status(thm)],[c_618,c_352]) ).
tcf(c_2835,plain,
select(queue_92,seq) = earray_91,
inference(superposition,[status(thm)],[c_618,c_351]) ).
tcf(c_2838,plain,
! [X0: $i] :
( ( X0 = tail )
| ( select(queue_94,X0) = select(queue_92,X0) ) ),
inference(superposition,[status(thm)],[c_619,c_352]) ).
tcf(c_2839,plain,
select(queue_94,tail) = index_93,
inference(superposition,[status(thm)],[c_619,c_351]) ).
tcf(c_2843,plain,
! [X0: $i] :
( ( X0 = head )
| ( select(queue_94,X0) = select(queue_97,X0) ) ),
inference(superposition,[status(thm)],[c_620,c_352]) ).
tcf(c_2844,plain,
select(queue_97,head) = index_96,
inference(superposition,[status(thm)],[c_620,c_351]) ).
tcf(c_2877,plain,
s(s(index_21)) != index_15,
inference(superposition,[status(thm)],[c_2463,c_403]) ).
tcf(c_2912,plain,
s(index_24) != index_15,
inference(light_normalisation,[status(thm)],[c_2877,c_517]) ).
tcf(c_2942,plain,
s(s(s(index_21))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_402]) ).
tcf(c_2977,plain,
s(s(index_24)) != index_15,
inference(light_normalisation,[status(thm)],[c_2942,c_517]) ).
tcf(c_3041,plain,
s(s(s(s(index_21)))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_401]) ).
tcf(c_3076,plain,
s(s(s(index_24))) != index_15,
inference(light_normalisation,[status(thm)],[c_3041,c_517]) ).
tcf(c_3137,plain,
s(s(s(s(s(index_21))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_400]) ).
tcf(c_3172,plain,
s(s(s(s(index_24)))) != index_15,
inference(light_normalisation,[status(thm)],[c_3137,c_517]) ).
tcf(c_3281,plain,
s(s(s(s(s(s(index_21)))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_399]) ).
tcf(c_3316,plain,
s(s(s(s(s(index_24))))) != index_15,
inference(light_normalisation,[status(thm)],[c_3281,c_517]) ).
tcf(c_3341,plain,
s(s(s(s(s(s(s(index_21))))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_398]) ).
tcf(c_3376,plain,
s(s(s(s(s(s(index_24)))))) != index_15,
inference(light_normalisation,[status(thm)],[c_3341,c_517]) ).
tcf(c_3436,plain,
s(s(s(s(s(s(s(s(index_21)))))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_397]) ).
tcf(c_3471,plain,
s(s(s(s(s(s(s(index_24))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_3436,c_517]) ).
tcf(c_3587,plain,
s(s(s(s(s(s(s(s(s(index_21))))))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_396]) ).
tcf(c_3622,plain,
s(s(s(s(s(s(s(s(index_24)))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_3587,c_517]) ).
tcf(c_3805,plain,
s(s(s(s(s(s(s(s(s(s(index_21)))))))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_395]) ).
tcf(c_3840,plain,
s(s(s(s(s(s(s(s(s(index_24))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_3805,c_517]) ).
tcf(c_4005,plain,
s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_394]) ).
tcf(c_4040,plain,
s(s(s(s(s(s(s(s(s(s(index_24)))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_4005,c_517]) ).
tcf(c_4190,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_393]) ).
tcf(c_4225,plain,
s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_4190,c_517]) ).
tcf(c_4282,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_392]) ).
tcf(c_4317,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_4282,c_517]) ).
tcf(c_4410,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))) != index_15,
inference(superposition,[status(thm)],[c_2463,c_391]) ).
tcf(c_4445,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_4410,c_517]) ).
tcf(c_4553,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_2463,c_390]) ).
tcf(c_4588,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_4553,c_517]) ).
tcf(c_5954,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_2463,c_389]) ).
tcf(c_5989,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_5954,c_517]) ).
tcf(c_6175,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_2463,c_388]) ).
tcf(c_6210,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_6175,c_517]) ).
tcf(c_6319,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_2463,c_387]) ).
tcf(c_6354,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))))) != index_15,
inference(light_normalisation,[status(thm)],[c_6319,c_517]) ).
tcf(c_14159,plain,
( ( head = tail )
| ( select(queue_1,tail) = index_0 ) ),
inference(superposition,[status(thm)],[c_468,c_2085]) ).
tcf(c_14161,plain,
( ( index_3 = index_0 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_14159,c_520]) ).
tcf(c_14162,plain,
index_3 = index_0,
inference(forward_subsumption_resolution,[status(thm)],[c_14161,c_353]) ).
tcf(c_14163,plain,
select(queue_1,head) = index_3,
inference(demodulation,[status(thm)],[c_2086,c_14162]) ).
tcf(c_14182,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_97,X0) ) ),
inference(superposition,[status(thm)],[c_2094,c_2090]) ).
tcf(c_14183,plain,
( ( tail = seq )
| ( select(queue_103,seq) = earray_100 ) ),
inference(superposition,[status(thm)],[c_2094,c_2091]) ).
tcf(c_14184,plain,
( ( earray_100 = earray_104 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_14183,c_408]) ).
tcf(c_14185,plain,
earray_100 = earray_104,
inference(forward_subsumption_resolution,[status(thm)],[c_14184,c_355]) ).
tcf(c_14189,plain,
! [X0: $i] :
( ( X0 = index_105 )
| ( select(earray_100,X0) = select(earray_106,X0) ) ),
inference(demodulation,[status(thm)],[c_1950,c_14185]) ).
tcf(c_14209,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_103,X0) = select(queue_109,X0) ) ),
inference(superposition,[status(thm)],[c_2114,c_2110]) ).
tcf(c_14210,plain,
( ( tail = seq )
| ( select(queue_109,seq) = earray_106 ) ),
inference(superposition,[status(thm)],[c_2114,c_2111]) ).
tcf(c_14211,plain,
( ( earray_106 = earray_110 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_14210,c_410]) ).
tcf(c_14212,plain,
earray_106 = earray_110,
inference(forward_subsumption_resolution,[status(thm)],[c_14211,c_355]) ).
tcf(c_14216,plain,
! [X0: $i] :
( ( X0 = index_111 )
| ( select(earray_106,X0) = select(earray_112,X0) ) ),
inference(demodulation,[status(thm)],[c_1955,c_14212]) ).
tcf(c_14277,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_115,X0) = select(queue_109,X0) ) ),
inference(superposition,[status(thm)],[c_2139,c_2132]) ).
tcf(c_14278,plain,
( ( tail = seq )
| ( select(queue_115,seq) = earray_112 ) ),
inference(superposition,[status(thm)],[c_2139,c_2133]) ).
tcf(c_14279,plain,
select(queue_115,seq) = earray_112,
inference(forward_subsumption_resolution,[status(thm)],[c_14278,c_355]) ).
tcf(c_14290,plain,
( ( head = seq )
| ( select(queue_115,seq) = earray_119 ) ),
inference(superposition,[status(thm)],[c_2144,c_412]) ).
tcf(c_14291,plain,
( ( head = tail )
| ( select(queue_115,tail) = index_120 ) ),
inference(superposition,[status(thm)],[c_2144,c_477]) ).
tcf(c_14293,plain,
( ( index_120 = index_114 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_14291,c_2140]) ).
tcf(c_14294,plain,
index_120 = index_114,
inference(forward_subsumption_resolution,[status(thm)],[c_14293,c_353]) ).
tcf(c_14295,plain,
( ( earray_112 = earray_119 )
| ( head = seq ) ),
inference(light_normalisation,[status(thm)],[c_14290,c_14279]) ).
tcf(c_14296,plain,
earray_112 = earray_119,
inference(forward_subsumption_resolution,[status(thm)],[c_14295,c_354]) ).
tcf(c_14322,plain,
s(index_111) = index_120,
inference(demodulation,[status(thm)],[c_473,c_14294]) ).
tcf(c_14343,plain,
! [X0: $i] :
( ( X0 = index_120 )
| ( select(earray_112,X0) = select(earray_121,X0) ) ),
inference(demodulation,[status(thm)],[c_1960,c_14296]) ).
tcf(c_14859,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_118,X0) = select(queue_124,X0) ) ),
inference(superposition,[status(thm)],[c_2153,c_2149]) ).
tcf(c_14860,plain,
( ( tail = seq )
| ( select(queue_124,seq) = earray_121 ) ),
inference(superposition,[status(thm)],[c_2153,c_2150]) ).
tcf(c_14861,plain,
( ( earray_121 = earray_125 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_14860,c_414]) ).
tcf(c_14862,plain,
earray_121 = earray_125,
inference(forward_subsumption_resolution,[status(thm)],[c_14861,c_355]) ).
tcf(c_14866,plain,
! [X0: $i] :
( ( X0 = index_126 )
| ( select(earray_121,X0) = select(earray_127,X0) ) ),
inference(demodulation,[status(thm)],[c_1965,c_14862]) ).
tcf(c_14886,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_211,X0) ) ),
inference(superposition,[status(thm)],[c_2170,c_2128]) ).
tcf(c_14907,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_124,X0) = select(queue_130,X0) ) ),
inference(superposition,[status(thm)],[c_2189,c_2166]) ).
tcf(c_14908,plain,
( ( tail = seq )
| ( select(queue_130,seq) = earray_127 ) ),
inference(superposition,[status(thm)],[c_2189,c_2167]) ).
tcf(c_14909,plain,
( ( earray_127 = earray_131 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_14908,c_416]) ).
tcf(c_14910,plain,
earray_127 = earray_131,
inference(forward_subsumption_resolution,[status(thm)],[c_14909,c_355]) ).
tcf(c_14914,plain,
! [X0: $i] :
( ( X0 = index_132 )
| ( select(earray_127,X0) = select(earray_133,X0) ) ),
inference(demodulation,[status(thm)],[c_1970,c_14910]) ).
tcf(c_14933,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_136,X0) = select(queue_130,X0) ) ),
inference(superposition,[status(thm)],[c_2207,c_2203]) ).
tcf(c_14934,plain,
( ( tail = seq )
| ( select(queue_136,seq) = earray_133 ) ),
inference(superposition,[status(thm)],[c_2207,c_2204]) ).
tcf(c_14935,plain,
select(queue_136,seq) = earray_133,
inference(forward_subsumption_resolution,[status(thm)],[c_14934,c_355]) ).
tcf(c_14946,plain,
( ( head = seq )
| ( select(queue_136,seq) = earray_140 ) ),
inference(superposition,[status(thm)],[c_2317,c_419]) ).
tcf(c_14947,plain,
( ( head = tail )
| ( select(queue_136,tail) = index_141 ) ),
inference(superposition,[status(thm)],[c_2317,c_485]) ).
tcf(c_14949,plain,
( ( index_141 = index_135 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_14947,c_2208]) ).
tcf(c_14950,plain,
index_141 = index_135,
inference(forward_subsumption_resolution,[status(thm)],[c_14949,c_353]) ).
tcf(c_14951,plain,
( ( earray_133 = earray_140 )
| ( head = seq ) ),
inference(light_normalisation,[status(thm)],[c_14946,c_14935]) ).
tcf(c_14952,plain,
earray_133 = earray_140,
inference(forward_subsumption_resolution,[status(thm)],[c_14951,c_354]) ).
tcf(c_14994,plain,
s(index_132) = index_141,
inference(demodulation,[status(thm)],[c_482,c_14950]) ).
tcf(c_15028,plain,
! [X0: $i] :
( ( X0 = index_141 )
| ( select(earray_133,X0) = select(earray_142,X0) ) ),
inference(demodulation,[status(thm)],[c_1975,c_14952]) ).
tcf(c_15600,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_139,X0) = select(queue_145,X0) ) ),
inference(superposition,[status(thm)],[c_2329,c_2322]) ).
tcf(c_15601,plain,
( ( tail = seq )
| ( select(queue_145,seq) = earray_142 ) ),
inference(superposition,[status(thm)],[c_2329,c_2323]) ).
tcf(c_15602,plain,
( ( earray_142 = earray_146 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_15601,c_421]) ).
tcf(c_15603,plain,
earray_142 = earray_146,
inference(forward_subsumption_resolution,[status(thm)],[c_15602,c_355]) ).
tcf(c_15607,plain,
! [X0: $i] :
( ( X0 = index_147 )
| ( select(earray_142,X0) = select(earray_148,X0) ) ),
inference(demodulation,[status(thm)],[c_1980,c_15603]) ).
tcf(c_15627,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_145,X0) = select(queue_151,X0) ) ),
inference(superposition,[status(thm)],[c_2349,c_2345]) ).
tcf(c_15628,plain,
( ( tail = seq )
| ( select(queue_151,seq) = earray_148 ) ),
inference(superposition,[status(thm)],[c_2349,c_2346]) ).
tcf(c_15629,plain,
( ( earray_148 = earray_161 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_15628,c_426]) ).
tcf(c_15630,plain,
earray_148 = earray_161,
inference(forward_subsumption_resolution,[status(thm)],[c_15629,c_355]) ).
tcf(c_15634,plain,
! [X0: $i] :
( ( X0 = index_162 )
| ( select(earray_148,X0) = select(earray_163,X0) ) ),
inference(demodulation,[status(thm)],[c_1990,c_15630]) ).
tcf(c_15654,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_157,X0) = select(queue_82,X0) ) ),
inference(superposition,[status(thm)],[c_2366,c_2362]) ).
tcf(c_15669,plain,
( ( head = tail )
| ( select(queue_157,tail) = index_171 ) ),
inference(superposition,[status(thm)],[c_2375,c_498]) ).
tcf(c_15671,plain,
( ( index_171 = index_156 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_15669,c_2367]) ).
tcf(c_15672,plain,
index_171 = index_156,
inference(forward_subsumption_resolution,[status(thm)],[c_15671,c_353]) ).
tcf(c_15700,plain,
s(index_153) = index_171,
inference(demodulation,[status(thm)],[c_491,c_15672]) ).
tcf(c_16199,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_166,X0) = select(queue_151,X0) ) ),
inference(superposition,[status(thm)],[c_2384,c_2380]) ).
tcf(c_16200,plain,
( ( tail = seq )
| ( select(queue_166,seq) = earray_163 ) ),
inference(superposition,[status(thm)],[c_2384,c_2381]) ).
tcf(c_16201,plain,
select(queue_166,seq) = earray_163,
inference(forward_subsumption_resolution,[status(thm)],[c_16200,c_355]) ).
tcf(c_16211,plain,
( ( head = seq )
| ( select(queue_166,seq) = earray_212 ) ),
inference(superposition,[status(thm)],[c_2389,c_442]) ).
tcf(c_16213,plain,
( ( earray_163 = earray_212 )
| ( head = seq ) ),
inference(light_normalisation,[status(thm)],[c_16211,c_16201]) ).
tcf(c_16214,plain,
earray_163 = earray_212,
inference(forward_subsumption_resolution,[status(thm)],[c_16213,c_354]) ).
tcf(c_16216,plain,
select(earray_163,index_213) = elem_214,
inference(demodulation,[status(thm)],[c_467,c_16214]) ).
tcf(c_16237,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_160,X0) = select(queue_175,X0) ) ),
inference(superposition,[status(thm)],[c_2410,c_2403]) ).
tcf(c_16264,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_175,X0) = select(queue_181,X0) ) ),
inference(superposition,[status(thm)],[c_2429,c_2425]) ).
tcf(c_16358,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_187,X0) = select(queue_181,X0) ) ),
inference(superposition,[status(thm)],[c_2445,c_2441]) ).
tcf(c_16370,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_13,X0) = select(queue_19,X0) ) ),
inference(superposition,[status(thm)],[c_2454,c_2399]) ).
tcf(c_16371,plain,
( ( tail = seq )
| ( select(queue_19,seq) = earray_16 ) ),
inference(superposition,[status(thm)],[c_2454,c_2400]) ).
tcf(c_16372,plain,
( ( earray_16 = earray_20 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_16371,c_439]) ).
tcf(c_16373,plain,
earray_16 = earray_20,
inference(forward_subsumption_resolution,[status(thm)],[c_16372,c_355]) ).
tcf(c_16377,plain,
! [X0: $i] :
( ( X0 = index_21 )
| ( select(earray_16,X0) = select(earray_22,X0) ) ),
inference(demodulation,[status(thm)],[c_2025,c_16373]) ).
tcf(c_16391,plain,
( ( head = tail )
| ( select(queue_187,tail) = index_192 ) ),
inference(superposition,[status(thm)],[c_2466,c_507]) ).
tcf(c_16393,plain,
( ( index_192 = index_186 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_16391,c_2446]) ).
tcf(c_16394,plain,
index_192 = index_186,
inference(forward_subsumption_resolution,[status(thm)],[c_16393,c_353]) ).
tcf(c_16437,plain,
s(index_183) = index_192,
inference(demodulation,[status(thm)],[c_504,c_16394]) ).
tcf(c_16754,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_190,X0) = select(queue_196,X0) ) ),
inference(superposition,[status(thm)],[c_2475,c_2471]) ).
tcf(c_16781,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_196,X0) = select(queue_202,X0) ) ),
inference(superposition,[status(thm)],[c_2498,c_2486]) ).
tcf(c_16808,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_208,X0) = select(queue_202,X0) ) ),
inference(superposition,[status(thm)],[c_2515,c_2511]) ).
tcf(c_16822,plain,
( ( head = tail )
| ( select(queue_208,tail) = index_9 ) ),
inference(superposition,[status(thm)],[c_2520,c_544]) ).
tcf(c_16824,plain,
( ( index_9 = index_207 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_16822,c_2516]) ).
tcf(c_16825,plain,
index_9 = index_207,
inference(forward_subsumption_resolution,[status(thm)],[c_16824,c_353]) ).
tcf(c_16875,plain,
s(index_204) = index_9,
inference(demodulation,[status(thm)],[c_512,c_16825]) ).
tcf(c_17153,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_25,X0) = select(queue_19,X0) ) ),
inference(superposition,[status(thm)],[c_2533,c_2525]) ).
tcf(c_17154,plain,
( ( tail = seq )
| ( select(queue_25,seq) = earray_22 ) ),
inference(superposition,[status(thm)],[c_2533,c_2526]) ).
tcf(c_17155,plain,
select(queue_25,seq) = earray_22,
inference(forward_subsumption_resolution,[status(thm)],[c_17154,c_355]) ).
tcf(c_17166,plain,
( ( head = seq )
| ( select(queue_25,seq) = earray_29 ) ),
inference(superposition,[status(thm)],[c_2538,c_444]) ).
tcf(c_17167,plain,
( ( head = tail )
| ( select(queue_25,tail) = index_30 ) ),
inference(superposition,[status(thm)],[c_2538,c_521]) ).
tcf(c_17169,plain,
( ( index_30 = index_24 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_17167,c_2534]) ).
tcf(c_17170,plain,
index_30 = index_24,
inference(forward_subsumption_resolution,[status(thm)],[c_17169,c_353]) ).
tcf(c_17171,plain,
( ( earray_22 = earray_29 )
| ( head = seq ) ),
inference(light_normalisation,[status(thm)],[c_17166,c_17155]) ).
tcf(c_17172,plain,
earray_22 = earray_29,
inference(forward_subsumption_resolution,[status(thm)],[c_17171,c_354]) ).
tcf(c_17199,plain,
s(s(s(s(s(s(index_30)))))) != index_15,
inference(demodulation,[status(thm)],[c_3376,c_17170]) ).
tcf(c_17202,plain,
s(s(s(s(s(index_30))))) != index_15,
inference(demodulation,[status(thm)],[c_3316,c_17170]) ).
tcf(c_17205,plain,
s(s(s(s(index_30)))) != index_15,
inference(demodulation,[status(thm)],[c_3172,c_17170]) ).
tcf(c_17208,plain,
s(s(s(index_30))) != index_15,
inference(demodulation,[status(thm)],[c_3076,c_17170]) ).
tcf(c_17211,plain,
s(s(index_30)) != index_15,
inference(demodulation,[status(thm)],[c_2977,c_17170]) ).
tcf(c_17215,plain,
s(index_30) != index_15,
inference(demodulation,[status(thm)],[c_2912,c_17170]) ).
tcf(c_17219,plain,
index_15 != index_30,
inference(demodulation,[status(thm)],[c_2464,c_17170]) ).
tcf(c_17224,plain,
index_15 != index_36,
inference(light_normalisation,[status(thm)],[c_17215,c_2556]) ).
tcf(c_17228,plain,
index_15 != index_42,
inference(light_normalisation,[status(thm)],[c_17211,c_2556,c_2571]) ).
tcf(c_17231,plain,
index_15 != index_45,
inference(light_normalisation,[status(thm)],[c_17208,c_526,c_2556,c_2571]) ).
tcf(c_17234,plain,
s(index_45) != index_15,
inference(light_normalisation,[status(thm)],[c_17205,c_526,c_2556,c_2571]) ).
tcf(c_17237,plain,
s(s(index_45)) != index_15,
inference(light_normalisation,[status(thm)],[c_17202,c_526,c_2556,c_2571]) ).
tcf(c_17240,plain,
s(s(s(index_45))) != index_15,
inference(light_normalisation,[status(thm)],[c_17199,c_526,c_2556,c_2571]) ).
tcf(c_17260,plain,
! [X0: $i] :
( ( X0 = index_30 )
| ( select(earray_22,X0) = select(earray_31,X0) ) ),
inference(demodulation,[status(thm)],[c_2030,c_17172]) ).
tcf(c_17532,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_28,X0) = select(queue_34,X0) ) ),
inference(superposition,[status(thm)],[c_2548,c_2543]) ).
tcf(c_17533,plain,
( ( tail = seq )
| ( select(queue_34,seq) = earray_31 ) ),
inference(superposition,[status(thm)],[c_2548,c_2544]) ).
tcf(c_17534,plain,
( ( earray_31 = earray_35 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_17533,c_446]) ).
tcf(c_17535,plain,
earray_31 = earray_35,
inference(forward_subsumption_resolution,[status(thm)],[c_17534,c_355]) ).
tcf(c_17539,plain,
! [X0: $i] :
( ( X0 = index_36 )
| ( select(earray_31,X0) = select(earray_37,X0) ) ),
inference(demodulation,[status(thm)],[c_2035,c_17535]) ).
tcf(c_17679,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_34,X0) = select(queue_40,X0) ) ),
inference(superposition,[status(thm)],[c_2563,c_2559]) ).
tcf(c_17680,plain,
( ( tail = seq )
| ( select(queue_40,seq) = earray_37 ) ),
inference(superposition,[status(thm)],[c_2563,c_2560]) ).
tcf(c_17681,plain,
( ( earray_37 = earray_41 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_17680,c_449]) ).
tcf(c_17682,plain,
earray_37 = earray_41,
inference(forward_subsumption_resolution,[status(thm)],[c_17681,c_355]) ).
tcf(c_17686,plain,
! [X0: $i] :
( ( X0 = index_42 )
| ( select(earray_37,X0) = select(earray_43,X0) ) ),
inference(demodulation,[status(thm)],[c_2045,c_17682]) ).
tcf(c_17706,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_46,X0) = select(queue_40,X0) ) ),
inference(superposition,[status(thm)],[c_2587,c_2574]) ).
tcf(c_17707,plain,
( ( tail = seq )
| ( select(queue_46,seq) = earray_43 ) ),
inference(superposition,[status(thm)],[c_2587,c_2575]) ).
tcf(c_17708,plain,
select(queue_46,seq) = earray_43,
inference(forward_subsumption_resolution,[status(thm)],[c_17707,c_355]) ).
tcf(c_17719,plain,
( ( head = seq )
| ( select(queue_46,seq) = earray_50 ) ),
inference(superposition,[status(thm)],[c_2593,c_451]) ).
tcf(c_17720,plain,
( ( head = tail )
| ( select(queue_46,tail) = index_51 ) ),
inference(superposition,[status(thm)],[c_2593,c_529]) ).
tcf(c_17722,plain,
( ( index_51 = index_45 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_17720,c_2588]) ).
tcf(c_17723,plain,
index_51 = index_45,
inference(forward_subsumption_resolution,[status(thm)],[c_17722,c_353]) ).
tcf(c_17724,plain,
( ( earray_43 = earray_50 )
| ( head = seq ) ),
inference(light_normalisation,[status(thm)],[c_17719,c_17708]) ).
tcf(c_17725,plain,
earray_43 = earray_50,
inference(forward_subsumption_resolution,[status(thm)],[c_17724,c_354]) ).
tcf(c_17731,plain,
s(s(s(index_51))) != index_15,
inference(demodulation,[status(thm)],[c_17240,c_17723]) ).
tcf(c_17735,plain,
s(s(index_51)) != index_15,
inference(demodulation,[status(thm)],[c_17237,c_17723]) ).
tcf(c_17739,plain,
s(index_51) != index_15,
inference(demodulation,[status(thm)],[c_17234,c_17723]) ).
tcf(c_17746,plain,
index_15 != index_51,
inference(demodulation,[status(thm)],[c_17231,c_17723]) ).
tcf(c_17772,plain,
s(index_42) = index_51,
inference(demodulation,[status(thm)],[c_526,c_17723]) ).
tcf(c_17793,plain,
index_15 != index_57,
inference(light_normalisation,[status(thm)],[c_17739,c_2722]) ).
tcf(c_17797,plain,
index_15 != index_63,
inference(light_normalisation,[status(thm)],[c_17735,c_2722,c_2742]) ).
tcf(c_17801,plain,
index_15 != index_66,
inference(light_normalisation,[status(thm)],[c_17731,c_535,c_2722,c_2742]) ).
tcf(c_17807,plain,
! [X0: $i] :
( ( X0 = index_51 )
| ( select(earray_43,X0) = select(earray_52,X0) ) ),
inference(demodulation,[status(thm)],[c_2050,c_17725]) ).
tcf(c_17985,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_49,X0) = select(queue_55,X0) ) ),
inference(superposition,[status(thm)],[c_2714,c_2710]) ).
tcf(c_17986,plain,
( ( tail = seq )
| ( select(queue_55,seq) = earray_52 ) ),
inference(superposition,[status(thm)],[c_2714,c_2711]) ).
tcf(c_17987,plain,
( ( earray_52 = earray_56 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_17986,c_453]) ).
tcf(c_17988,plain,
earray_52 = earray_56,
inference(forward_subsumption_resolution,[status(thm)],[c_17987,c_355]) ).
tcf(c_17992,plain,
! [X0: $i] :
( ( X0 = index_57 )
| ( select(earray_52,X0) = select(earray_58,X0) ) ),
inference(demodulation,[status(thm)],[c_2055,c_17988]) ).
tcf(c_18012,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_55,X0) = select(queue_61,X0) ) ),
inference(superposition,[status(thm)],[c_2733,c_2729]) ).
tcf(c_18013,plain,
( ( tail = seq )
| ( select(queue_61,seq) = earray_58 ) ),
inference(superposition,[status(thm)],[c_2733,c_2730]) ).
tcf(c_18014,plain,
( ( earray_58 = earray_62 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_18013,c_455]) ).
tcf(c_18015,plain,
earray_58 = earray_62,
inference(forward_subsumption_resolution,[status(thm)],[c_18014,c_355]) ).
tcf(c_18019,plain,
! [X0: $i] :
( ( X0 = index_63 )
| ( select(earray_58,X0) = select(earray_64,X0) ) ),
inference(demodulation,[status(thm)],[c_2060,c_18015]) ).
tcf(c_18039,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_67,X0) = select(queue_61,X0) ) ),
inference(superposition,[status(thm)],[c_2750,c_2746]) ).
tcf(c_18040,plain,
( ( tail = seq )
| ( select(queue_67,seq) = earray_64 ) ),
inference(superposition,[status(thm)],[c_2750,c_2747]) ).
tcf(c_18041,plain,
select(queue_67,seq) = earray_64,
inference(forward_subsumption_resolution,[status(thm)],[c_18040,c_355]) ).
tcf(c_18051,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_1,X0) = select(queue_7,X0) ) ),
inference(superposition,[status(thm)],[c_2755,c_2706]) ).
tcf(c_18126,plain,
( ( head = seq )
| ( select(queue_67,seq) = earray_71 ) ),
inference(superposition,[status(thm)],[c_2766,c_457]) ).
tcf(c_18127,plain,
( ( head = tail )
| ( select(queue_67,tail) = index_72 ) ),
inference(superposition,[status(thm)],[c_2766,c_538]) ).
tcf(c_18129,plain,
( ( index_72 = index_66 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_18127,c_2751]) ).
tcf(c_18130,plain,
index_72 = index_66,
inference(forward_subsumption_resolution,[status(thm)],[c_18129,c_353]) ).
tcf(c_18131,plain,
( ( earray_64 = earray_71 )
| ( head = seq ) ),
inference(light_normalisation,[status(thm)],[c_18126,c_18041]) ).
tcf(c_18132,plain,
earray_64 = earray_71,
inference(forward_subsumption_resolution,[status(thm)],[c_18131,c_354]) ).
tcf(c_18150,plain,
index_15 != index_72,
inference(demodulation,[status(thm)],[c_17801,c_18130]) ).
tcf(c_18182,plain,
s(index_63) = index_72,
inference(demodulation,[status(thm)],[c_535,c_18130]) ).
tcf(c_18220,plain,
! [X0: $i] :
( ( X0 = index_72 )
| ( select(earray_64,X0) = select(earray_73,X0) ) ),
inference(demodulation,[status(thm)],[c_2065,c_18132]) ).
tcf(c_18448,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_70,X0) = select(queue_76,X0) ) ),
inference(superposition,[status(thm)],[c_2783,c_2779]) ).
tcf(c_18449,plain,
( ( tail = seq )
| ( select(queue_76,seq) = earray_73 ) ),
inference(superposition,[status(thm)],[c_2783,c_2780]) ).
tcf(c_18450,plain,
( ( earray_73 = earray_83 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_18449,c_462]) ).
tcf(c_18451,plain,
earray_73 = earray_83,
inference(forward_subsumption_resolution,[status(thm)],[c_18450,c_355]) ).
tcf(c_18455,plain,
! [X0: $i] :
( ( X0 = index_84 )
| ( select(earray_73,X0) = select(earray_85,X0) ) ),
inference(demodulation,[status(thm)],[c_2075,c_18451]) ).
tcf(c_18475,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_7,X0) = select(queue_82,X0) ) ),
inference(superposition,[status(thm)],[c_2798,c_2794]) ).
tcf(c_18502,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_76,X0) = select(queue_88,X0) ) ),
inference(superposition,[status(thm)],[c_2822,c_2810]) ).
tcf(c_18503,plain,
( ( tail = seq )
| ( select(queue_88,seq) = earray_85 ) ),
inference(superposition,[status(thm)],[c_2822,c_2811]) ).
tcf(c_18504,plain,
( ( earray_85 = earray_89 )
| ( tail = seq ) ),
inference(light_normalisation,[status(thm)],[c_18503,c_464]) ).
tcf(c_18505,plain,
earray_85 = earray_89,
inference(forward_subsumption_resolution,[status(thm)],[c_18504,c_355]) ).
tcf(c_18510,plain,
store(earray_85,index_90,e20) = earray_91,
inference(demodulation,[status(thm)],[c_465,c_18505]) ).
tcf(c_18581,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_94,X0) = select(queue_88,X0) ) ),
inference(superposition,[status(thm)],[c_2838,c_2834]) ).
tcf(c_18582,plain,
( ( tail = seq )
| ( select(queue_94,seq) = earray_91 ) ),
inference(superposition,[status(thm)],[c_2838,c_2835]) ).
tcf(c_18583,plain,
select(queue_94,seq) = earray_91,
inference(forward_subsumption_resolution,[status(thm)],[c_18582,c_355]) ).
tcf(c_18594,plain,
( ( head = seq )
| ( select(queue_94,seq) = earray_98 ) ),
inference(superposition,[status(thm)],[c_2843,c_466]) ).
tcf(c_18595,plain,
( ( head = tail )
| ( select(queue_94,tail) = index_99 ) ),
inference(superposition,[status(thm)],[c_2843,c_549]) ).
tcf(c_18597,plain,
( ( index_99 = index_93 )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_18595,c_2839]) ).
tcf(c_18598,plain,
index_99 = index_93,
inference(forward_subsumption_resolution,[status(thm)],[c_18597,c_353]) ).
tcf(c_18599,plain,
( ( earray_98 = earray_91 )
| ( head = seq ) ),
inference(light_normalisation,[status(thm)],[c_18594,c_18583]) ).
tcf(c_18600,plain,
earray_98 = earray_91,
inference(forward_subsumption_resolution,[status(thm)],[c_18599,c_354]) ).
tcf(c_18650,plain,
s(index_90) = index_99,
inference(demodulation,[status(thm)],[c_546,c_18598]) ).
tcf(c_18912,plain,
store(earray_85,index_90,e20) = earray_98,
inference(light_normalisation,[status(thm)],[c_18510,c_18600]) ).
tcf(c_18913,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( select(earray_98,X0) = select(earray_85,X0) ) ),
inference(superposition,[status(thm)],[c_18912,c_352]) ).
tcf(c_18935,plain,
index_15 != index_84,
inference(light_normalisation,[status(thm)],[c_3471,c_2556,c_2571,c_2722,c_2742,c_2791,c_17170,c_17772,c_18182]) ).
tcf(c_19005,plain,
( ( index_162 = index_213 )
| ( select(earray_148,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_15634,c_16216]) ).
tcf(c_19012,plain,
( ( index_162 = index_213 )
| ( index_147 = index_213 )
| ( select(earray_142,index_213) = elem_214 ) ),
inference(superposition,[status(thm)],[c_15607,c_19005]) ).
tcf(c_19047,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_15028,c_19012]) ).
tcf(c_19134,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_14914,c_19047]) ).
tcf(c_19177,plain,
! [X0: $i] :
( ( X0 = index_90 )
| ( X0 = index_84 )
| ( select(earray_98,X0) = select(earray_73,X0) ) ),
inference(superposition,[status(thm)],[c_18455,c_18913]) ).
tcf(c_19196,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_14866,c_19134]) ).
tcf(c_19226,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_14343,c_19196]) ).
tcf(c_19237,plain,
index_15 != index_90,
inference(light_normalisation,[status(thm)],[c_3622,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_17170,c_17772,c_18182]) ).
tcf(c_19340,plain,
index_99 != index_15,
inference(light_normalisation,[status(thm)],[c_3840,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_19375,plain,
index_105 != index_15,
inference(light_normalisation,[status(thm)],[c_4040,c_2103,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_19409,plain,
index_111 != index_15,
inference(light_normalisation,[status(thm)],[c_4225,c_2103,c_2124,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_19434,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_103,head) = index_96 ) ),
inference(superposition,[status(thm)],[c_14182,c_2844]) ).
tcf(c_19435,plain,
select(queue_103,head) = index_96,
inference(forward_subsumption_resolution,[status(thm)],[c_19434,c_354,c_353]) ).
tcf(c_19464,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_115,X0) = select(queue_103,X0) ) ),
inference(superposition,[status(thm)],[c_14277,c_14209]) ).
tcf(c_19491,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_13,head) = index_210 ) ),
inference(superposition,[status(thm)],[c_14886,c_2521]) ).
tcf(c_19492,plain,
select(queue_13,head) = index_210,
inference(forward_subsumption_resolution,[status(thm)],[c_19491,c_354,c_353]) ).
tcf(c_19518,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_136,X0) = select(queue_124,X0) ) ),
inference(superposition,[status(thm)],[c_14933,c_14907]) ).
tcf(c_19563,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_166,X0) = select(queue_145,X0) ) ),
inference(superposition,[status(thm)],[c_16199,c_15627]) ).
tcf(c_19603,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_187,X0) = select(queue_175,X0) ) ),
inference(superposition,[status(thm)],[c_16358,c_16264]) ).
tcf(c_19648,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_208,X0) = select(queue_196,X0) ) ),
inference(superposition,[status(thm)],[c_16808,c_16781]) ).
tcf(c_19663,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_25,X0) = select(queue_13,X0) ) ),
inference(superposition,[status(thm)],[c_17153,c_16370]) ).
tcf(c_19698,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_46,X0) = select(queue_34,X0) ) ),
inference(superposition,[status(thm)],[c_17706,c_17679]) ).
tcf(c_19734,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_67,X0) = select(queue_55,X0) ) ),
inference(superposition,[status(thm)],[c_18039,c_18012]) ).
tcf(c_19769,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_157,X0) = select(queue_7,X0) ) ),
inference(superposition,[status(thm)],[c_18475,c_15654]) ).
tcf(c_19794,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_94,X0) = select(queue_76,X0) ) ),
inference(superposition,[status(thm)],[c_18581,c_18502]) ).
tcf(c_19831,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_19177,c_18220]) ).
tcf(c_19855,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_115,head) = index_96 ) ),
inference(superposition,[status(thm)],[c_19464,c_19435]) ).
tcf(c_19856,plain,
( ( index_116 = index_96 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_19855,c_474]) ).
tcf(c_19857,plain,
index_116 = index_96,
inference(forward_subsumption_resolution,[status(thm)],[c_19856,c_354,c_353]) ).
tcf(c_19874,plain,
s(index_95) = index_116,
inference(demodulation,[status(thm)],[c_548,c_19857]) ).
tcf(c_20103,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_136,X0) = select(queue_118,X0) ) ),
inference(superposition,[status(thm)],[c_19518,c_14859]) ).
tcf(c_20118,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_166,X0) = select(queue_139,X0) ) ),
inference(superposition,[status(thm)],[c_19563,c_15600]) ).
tcf(c_20133,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_187,X0) = select(queue_160,X0) ) ),
inference(superposition,[status(thm)],[c_19603,c_16237]) ).
tcf(c_20148,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_208,X0) = select(queue_190,X0) ) ),
inference(superposition,[status(thm)],[c_19648,c_16754]) ).
tcf(c_20163,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_25,head) = index_210 ) ),
inference(superposition,[status(thm)],[c_19663,c_19492]) ).
tcf(c_20164,plain,
( ( index_210 = index_26 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_20163,c_518]) ).
tcf(c_20165,plain,
index_210 = index_26,
inference(forward_subsumption_resolution,[status(thm)],[c_20164,c_354,c_353]) ).
tcf(c_20181,plain,
s(index_210) = index_27,
inference(demodulation,[status(thm)],[c_519,c_20165]) ).
tcf(c_20527,plain,
index_120 != index_15,
inference(light_normalisation,[status(thm)],[c_4317,c_2103,c_2124,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_14322,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_20540,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_46,X0) = select(queue_28,X0) ) ),
inference(superposition,[status(thm)],[c_19698,c_17532]) ).
tcf(c_20555,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_67,X0) = select(queue_49,X0) ) ),
inference(superposition,[status(thm)],[c_19734,c_17985]) ).
tcf(c_20570,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_157,X0) = select(queue_1,X0) ) ),
inference(superposition,[status(thm)],[c_19769,c_18051]) ).
tcf(c_20585,plain,
! [X0: $i] :
( ( X0 = seq )
| ( X0 = tail )
| ( select(queue_94,X0) = select(queue_70,X0) ) ),
inference(superposition,[status(thm)],[c_19794,c_18448]) ).
tcf(c_20602,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_136,head) = index_117 ) ),
inference(superposition,[status(thm)],[c_20103,c_2145]) ).
tcf(c_20603,plain,
( ( index_117 = index_137 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_20602,c_483]) ).
tcf(c_20604,plain,
index_117 = index_137,
inference(forward_subsumption_resolution,[status(thm)],[c_20603,c_354,c_353]) ).
tcf(c_20624,plain,
s(index_117) = index_138,
inference(demodulation,[status(thm)],[c_484,c_20604]) ).
tcf(c_20727,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_166,head) = index_138 ) ),
inference(superposition,[status(thm)],[c_20118,c_2318]) ).
tcf(c_20728,plain,
( ( index_138 = index_167 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_20727,c_496]) ).
tcf(c_20729,plain,
index_138 = index_167,
inference(forward_subsumption_resolution,[status(thm)],[c_20728,c_354,c_353]) ).
tcf(c_20747,plain,
s(index_138) = index_213,
inference(demodulation,[status(thm)],[c_2397,c_20729]) ).
tcf(c_20857,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_187,head) = index_159 ) ),
inference(superposition,[status(thm)],[c_20133,c_2376]) ).
tcf(c_20858,plain,
( ( index_159 = index_188 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_20857,c_505]) ).
tcf(c_20859,plain,
index_159 = index_188,
inference(forward_subsumption_resolution,[status(thm)],[c_20858,c_354,c_353]) ).
tcf(c_20880,plain,
s(index_159) = index_189,
inference(demodulation,[status(thm)],[c_506,c_20859]) ).
tcf(c_20967,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_208,head) = index_189 ) ),
inference(superposition,[status(thm)],[c_20148,c_2467]) ).
tcf(c_20968,plain,
( ( index_189 = index_209 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_20967,c_513]) ).
tcf(c_20969,plain,
index_189 = index_209,
inference(forward_subsumption_resolution,[status(thm)],[c_20968,c_354,c_353]) ).
tcf(c_20988,plain,
s(index_189) = index_210,
inference(demodulation,[status(thm)],[c_515,c_20969]) ).
tcf(c_21189,plain,
index_126 != index_15,
inference(light_normalisation,[status(thm)],[c_4445,c_2103,c_2124,c_2162,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_14322,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_21214,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_46,head) = index_27 ) ),
inference(superposition,[status(thm)],[c_20540,c_2539]) ).
tcf(c_21215,plain,
( ( index_27 = index_47 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_21214,c_527]) ).
tcf(c_21216,plain,
index_27 = index_47,
inference(forward_subsumption_resolution,[status(thm)],[c_21215,c_354,c_353]) ).
tcf(c_21237,plain,
s(index_27) = index_48,
inference(demodulation,[status(thm)],[c_528,c_21216]) ).
tcf(c_21354,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_67,head) = index_48 ) ),
inference(superposition,[status(thm)],[c_20555,c_2594]) ).
tcf(c_21355,plain,
( ( index_48 = index_68 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_21354,c_536]) ).
tcf(c_21356,plain,
index_48 = index_68,
inference(forward_subsumption_resolution,[status(thm)],[c_21355,c_354,c_353]) ).
tcf(c_21377,plain,
s(index_48) = index_69,
inference(demodulation,[status(thm)],[c_537,c_21356]) ).
tcf(c_21707,plain,
index_132 != index_15,
inference(light_normalisation,[status(thm)],[c_4588,c_2103,c_2124,c_2162,c_2199,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_14322,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_21723,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_157,head) = index_3 ) ),
inference(superposition,[status(thm)],[c_20570,c_14163]) ).
tcf(c_21724,plain,
( ( index_3 = index_158 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_21723,c_492]) ).
tcf(c_21725,plain,
index_3 = index_158,
inference(forward_subsumption_resolution,[status(thm)],[c_21724,c_354,c_353]) ).
tcf(c_21740,plain,
s(index_3) = index_159,
inference(demodulation,[status(thm)],[c_493,c_21725]) ).
tcf(c_21741,plain,
index_78 = index_159,
inference(light_normalisation,[status(thm)],[c_21740,c_2763]) ).
tcf(c_21754,plain,
s(index_78) = index_189,
inference(demodulation,[status(thm)],[c_20880,c_21741]) ).
tcf(c_21759,plain,
index_153 = index_189,
inference(light_normalisation,[status(thm)],[c_21754,c_2807]) ).
tcf(c_21772,plain,
s(index_153) = index_210,
inference(demodulation,[status(thm)],[c_20988,c_21759]) ).
tcf(c_21778,plain,
index_171 = index_210,
inference(light_normalisation,[status(thm)],[c_21772,c_15700]) ).
tcf(c_21792,plain,
s(index_171) = index_27,
inference(demodulation,[status(thm)],[c_20181,c_21778]) ).
tcf(c_21798,plain,
index_177 = index_27,
inference(light_normalisation,[status(thm)],[c_21792,c_2418]) ).
tcf(c_21811,plain,
s(index_177) = index_48,
inference(demodulation,[status(thm)],[c_21237,c_21798]) ).
tcf(c_21816,plain,
index_183 = index_48,
inference(light_normalisation,[status(thm)],[c_21811,c_2438]) ).
tcf(c_21828,plain,
s(index_183) = index_69,
inference(demodulation,[status(thm)],[c_21377,c_21816]) ).
tcf(c_21833,plain,
index_192 = index_69,
inference(light_normalisation,[status(thm)],[c_21828,c_16437]) ).
tcf(c_21834,plain,
select(queue_70,head) = index_192,
inference(demodulation,[status(thm)],[c_2767,c_21833]) ).
tcf(c_21996,plain,
( ( head = seq )
| ( head = tail )
| ( select(queue_94,head) = index_192 ) ),
inference(superposition,[status(thm)],[c_20585,c_21834]) ).
tcf(c_21997,plain,
( ( index_192 = index_95 )
| ( head = seq )
| ( head = tail ) ),
inference(light_normalisation,[status(thm)],[c_21996,c_547]) ).
tcf(c_21998,plain,
index_192 = index_95,
inference(forward_subsumption_resolution,[status(thm)],[c_21997,c_354,c_353]) ).
tcf(c_22018,plain,
s(index_192) = index_116,
inference(demodulation,[status(thm)],[c_19874,c_21998]) ).
tcf(c_22021,plain,
index_198 = index_116,
inference(light_normalisation,[status(thm)],[c_22018,c_2483]) ).
tcf(c_22041,plain,
s(index_198) = index_117,
inference(demodulation,[status(thm)],[c_475,c_22021]) ).
tcf(c_22042,plain,
index_204 = index_117,
inference(light_normalisation,[status(thm)],[c_22041,c_2507]) ).
tcf(c_22057,plain,
s(index_204) = index_138,
inference(demodulation,[status(thm)],[c_20624,c_22042]) ).
tcf(c_22062,plain,
index_9 = index_138,
inference(light_normalisation,[status(thm)],[c_22057,c_16875]) ).
tcf(c_22077,plain,
s(index_9) = index_213,
inference(demodulation,[status(thm)],[c_20747,c_22062]) ).
tcf(c_22081,plain,
index_15 = index_213,
inference(light_normalisation,[status(thm)],[c_22077,c_2179]) ).
tcf(c_22084,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 )
| ( select(earray_112,index_15) = elem_214 ) ),
inference(demodulation,[status(thm)],[c_19226,c_22081]) ).
tcf(c_22113,plain,
( ( index_15 = index_162 )
| ( index_147 = index_15 )
| ( index_141 = index_15 )
| ( select(earray_112,index_15) = elem_214 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_22084,c_21707,c_21189,c_20527]) ).
tcf(c_22159,plain,
index_141 != index_15,
inference(light_normalisation,[status(thm)],[c_5989,c_2103,c_2124,c_2162,c_2199,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_14322,c_14994,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_22260,plain,
( ( index_15 = index_162 )
| ( index_147 = index_15 )
| ( select(earray_112,index_15) = elem_214 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_22113,c_22159]) ).
tcf(c_22270,plain,
( ( index_15 = index_162 )
| ( index_147 = index_15 )
| ( index_111 = index_15 )
| ( select(earray_106,index_15) = elem_214 ) ),
inference(superposition,[status(thm)],[c_14216,c_22260]) ).
tcf(c_22272,plain,
( ( index_15 = index_162 )
| ( index_147 = index_15 )
| ( select(earray_106,index_15) = elem_214 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_22270,c_19409]) ).
tcf(c_22307,plain,
( ( index_15 = index_162 )
| ( index_147 = index_15 )
| ( index_105 = index_15 )
| ( select(earray_100,index_15) = elem_214 ) ),
inference(superposition,[status(thm)],[c_14189,c_22272]) ).
tcf(c_22309,plain,
( ( index_15 = index_162 )
| ( index_147 = index_15 )
| ( select(earray_100,index_15) = elem_214 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_22307,c_19375]) ).
tcf(c_22448,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_19831,c_18019]) ).
tcf(c_22725,plain,
index_147 != index_15,
inference(light_normalisation,[status(thm)],[c_6210,c_2103,c_2124,c_2162,c_2199,c_2338,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_14322,c_14994,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_22726,plain,
( ( index_15 = index_162 )
| ( select(earray_100,index_15) = elem_214 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_22309,c_22725]) ).
tcf(c_22845,plain,
index_15 != index_162,
inference(light_normalisation,[status(thm)],[c_6354,c_2103,c_2124,c_2162,c_2199,c_2338,c_2358,c_2556,c_2571,c_2722,c_2742,c_2791,c_2831,c_14322,c_14994,c_17170,c_17772,c_18182,c_18650]) ).
tcf(c_22852,plain,
select(earray_100,index_15) = elem_214,
inference(backward_subsumption_resolution,[status(thm)],[c_22726,c_22845]) ).
tcf(c_23107,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_22448,c_17992]) ).
tcf(c_23372,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_23107,c_17807]) ).
tcf(c_23643,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_23372,c_17686]) ).
tcf(c_23912,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_23643,c_17539]) ).
tcf(c_24152,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_23912,c_17260]) ).
tcf(c_24399,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_24152,c_16377]) ).
tcf(c_24657,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_24399,c_1805]) ).
tcf(c_24659,plain,
select(earray_98,index_15) = e10,
inference(forward_subsumption_resolution,[status(thm)],[c_24657,c_19237,c_18935,c_18150,c_17797,c_17793,c_17746,c_17228,c_17224,c_17219,c_2462]) ).
tcf(c_24673,plain,
( ( index_99 = index_15 )
| ( select(earray_100,index_15) = e10 ) ),
inference(superposition,[status(thm)],[c_1945,c_24659]) ).
tcf(c_24675,plain,
( ( e10 = elem_214 )
| ( index_99 = index_15 ) ),
inference(light_normalisation,[status(thm)],[c_24673,c_22852]) ).
tcf(c_24676,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_24675,c_1225,c_19340]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV569-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n002.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 20:38:49 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.44 % Detected problem language: tptp
% 0.10/0.45 % Proving...
% 26.47/6.32 % SZS status Started for theBenchmark.p
% 26.47/6.32 % SZS status Unsatisfiable for theBenchmark.p
% 26.47/6.32
% 26.47/6.32 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 26.47/6.32
% 26.47/6.32 % ------ iProver source info
% 26.47/6.32
% 26.47/6.32 % git: date: 2026-07-19 20:42:38 +0200
% 26.47/6.32 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 26.47/6.32 % git: non_committed_changes: false
% 26.47/6.32
% 26.47/6.32 % ------ Parsing...% successful
% 26.47/6.32
% 26.47/6.32
% 26.47/6.32 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 26.47/6.32
% 26.47/6.32 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 26.47/6.32
% 26.47/6.32 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 26.47/6.32
% 26.47/6.32 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 26.47/6.32 % ------ Proving...
% 26.47/6.32 % ------ Problem Properties
% 26.47/6.32
% 26.47/6.32 %
% 26.47/6.32 % clauses 271
% 26.47/6.32 % conjectures 1
% 26.47/6.32 % EPR 4
% 26.47/6.32 % Horn 270
% 26.47/6.32 % unary 270
% 26.47/6.32 % binary 1
% 26.47/6.32 % lits 272
% 26.47/6.32 % lits eq 272
% 26.47/6.32 % fd_pure 0
% 26.47/6.32 % fd_pseudo 0
% 26.47/6.32 % fd_cond 0
% 26.47/6.32 % fd_pseudo_cond 1
% 26.47/6.32 % AC symbols 0
% 26.47/6.32
% 26.47/6.32 % ------ Schedule dynamic 5 is on
% 26.47/6.32
% 26.47/6.32 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 26.47/6.32
% 26.47/6.32
% 26.47/6.32 % ------
% 26.47/6.32 % Current options:
% 26.47/6.32 % ------
% 26.47/6.32
% 26.47/6.32
% 26.47/6.32 %
% 26.47/6.32
% 26.47/6.32 % ------ Proving...
% 26.47/6.32 %
% 26.47/6.32
% 26.47/6.32 % SZS status Unsatisfiable for theBenchmark.p
% 26.47/6.32
% 26.47/6.32 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 26.47/6.34
% 26.47/6.34
%------------------------------------------------------------------------------