%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV569-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:26:00 PM UTC 2026
% Result : Unsatisfiable 19.80s 3.12s
% Output : Refutation 19.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 252
% Syntax : Number of formulae : 1243 ( 964 unt; 3 def)
% Number of atoms : 1698 (1633 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 894 ( 439 ~; 452 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 2 avg)
% Maximal term depth : 20 ( 3 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 263 ( 263 usr; 260 con; 0-3 aty)
% Number of variables : 159 ( 0 sgn 159 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
head != tail,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',head_distinct_from_tail) ).
fof(f4,axiom,
head != seq,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',head_distinct_from_seq) ).
fof(f5,axiom,
tail != seq,
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',as12) ).
fof(f45,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as11) ).
fof(f46,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as10) ).
fof(f47,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as9) ).
fof(f48,axiom,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as8) ).
fof(f49,axiom,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as7) ).
fof(f50,axiom,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as6) ).
fof(f51,axiom,
! [X0] : s(s(s(s(s(X0))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as5) ).
fof(f52,axiom,
! [X0] : s(s(s(s(X0)))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as4) ).
fof(f53,axiom,
! [X0] : s(s(s(X0))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as3) ).
fof(f54,axiom,
! [X0] : s(s(X0)) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as2) ).
fof(f55,axiom,
! [X0] : s(X0) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as1) ).
fof(f57,axiom,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
fof(f58,axiom,
earray_104 = select(q22,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f59,axiom,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f60,axiom,
earray_110 = select(q23,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f61,axiom,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f62,axiom,
earray_119 = select(q24,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f63,axiom,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f64,axiom,
earray_125 = select(q25,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f65,axiom,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f66,axiom,
earray_131 = select(q26,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f67,axiom,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f69,axiom,
earray_140 = select(q27,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f70,axiom,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f71,axiom,
earray_146 = select(q28,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f72,axiom,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f75,axiom,
earray_16 = store(earray_14,index_15,e10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f76,axiom,
earray_161 = select(q29,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f77,axiom,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f89,axiom,
earray_20 = select(q11,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f92,axiom,
earray_212 = select(q30,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f93,axiom,
earray_22 = store(earray_20,index_21,e11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f94,axiom,
earray_29 = select(q12,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f95,axiom,
earray_31 = store(earray_29,index_30,e12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f96,axiom,
earray_35 = select(q13,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f97,axiom,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f99,axiom,
earray_41 = select(q14,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f100,axiom,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f101,axiom,
earray_50 = select(q15,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f102,axiom,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f103,axiom,
earray_56 = select(q16,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f104,axiom,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp48) ).
fof(f105,axiom,
earray_62 = select(q17,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
fof(f106,axiom,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp50) ).
fof(f107,axiom,
earray_71 = select(q18,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp51) ).
fof(f108,axiom,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp52) ).
fof(f112,axiom,
earray_83 = select(q19,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp56) ).
fof(f113,axiom,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp57) ).
fof(f114,axiom,
earray_89 = select(q20,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp58) ).
fof(f115,axiom,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp59) ).
fof(f116,axiom,
earray_98 = select(q21,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp60) ).
fof(f117,axiom,
elem_214 = select(earray_212,index_213),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp61) ).
fof(f118,axiom,
index_0 = select(q,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp62) ).
fof(f119,axiom,
index_102 = s(index_99),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp63) ).
fof(f120,axiom,
index_105 = select(q22,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp64) ).
fof(f121,axiom,
index_108 = s(index_105),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp65) ).
fof(f122,axiom,
index_111 = select(q23,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp66) ).
fof(f123,axiom,
index_114 = s(index_111),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp67) ).
fof(f124,axiom,
index_116 = select(queue_115,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp68) ).
fof(f125,axiom,
index_117 = s(index_116),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp69) ).
fof(f126,axiom,
index_12 = s(index_9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp70) ).
fof(f127,axiom,
index_120 = select(q24,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp71) ).
fof(f128,axiom,
index_123 = s(index_120),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp72) ).
fof(f129,axiom,
index_126 = select(q25,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp73) ).
fof(f130,axiom,
index_129 = s(index_126),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp74) ).
fof(f131,axiom,
index_132 = select(q26,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp75) ).
fof(f132,axiom,
index_135 = s(index_132),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp76) ).
fof(f133,axiom,
index_137 = select(queue_136,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp77) ).
fof(f134,axiom,
index_138 = s(index_137),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp78) ).
fof(f135,axiom,
index_141 = select(q27,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp79) ).
fof(f136,axiom,
index_144 = s(index_141),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp80) ).
fof(f137,axiom,
index_147 = select(q28,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp81) ).
fof(f138,axiom,
index_15 = select(q10,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp82) ).
fof(f139,axiom,
index_150 = s(index_147),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp83) ).
fof(f140,axiom,
index_153 = select(q2,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp84) ).
fof(f141,axiom,
index_156 = s(index_153),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp85) ).
fof(f142,axiom,
index_158 = select(queue_157,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp86) ).
fof(f143,axiom,
index_159 = s(index_158),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp87) ).
fof(f144,axiom,
index_162 = select(q29,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp88) ).
fof(f146,axiom,
index_167 = select(queue_166,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp90) ).
fof(f147,axiom,
index_168 = s(index_167),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp91) ).
fof(f148,axiom,
index_171 = select(q3,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp92) ).
fof(f149,axiom,
index_174 = s(index_171),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp93) ).
fof(f150,axiom,
index_177 = select(q4,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp94) ).
fof(f151,axiom,
index_18 = s(index_15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp95) ).
fof(f152,axiom,
index_180 = s(index_177),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp96) ).
fof(f153,axiom,
index_183 = select(q5,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp97) ).
fof(f154,axiom,
index_186 = s(index_183),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp98) ).
fof(f155,axiom,
index_188 = select(queue_187,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp99) ).
fof(f156,axiom,
index_189 = s(index_188),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp100) ).
fof(f157,axiom,
index_192 = select(q6,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp101) ).
fof(f158,axiom,
index_195 = s(index_192),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp102) ).
fof(f159,axiom,
index_198 = select(q7,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp103) ).
fof(f160,axiom,
index_201 = s(index_198),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp104) ).
fof(f161,axiom,
index_204 = select(q8,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp105) ).
fof(f162,axiom,
index_207 = s(index_204),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp106) ).
fof(f163,axiom,
index_209 = select(queue_208,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp107) ).
fof(f164,axiom,
index_21 = select(q11,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp108) ).
fof(f165,axiom,
index_210 = s(index_209),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp109) ).
fof(f166,axiom,
index_213 = select(q30,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp110) ).
fof(f167,axiom,
index_24 = s(index_21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp111) ).
fof(f168,axiom,
index_26 = select(queue_25,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp112) ).
fof(f169,axiom,
index_27 = s(index_26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp113) ).
fof(f170,axiom,
index_3 = select(q0,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp114) ).
fof(f171,axiom,
index_30 = select(q12,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp115) ).
fof(f172,axiom,
index_33 = s(index_30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp116) ).
fof(f173,axiom,
index_36 = select(q13,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp117) ).
fof(f174,axiom,
index_39 = s(index_36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp118) ).
fof(f175,axiom,
index_42 = select(q14,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp119) ).
fof(f176,axiom,
index_45 = s(index_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp120) ).
fof(f177,axiom,
index_47 = select(queue_46,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp121) ).
fof(f178,axiom,
index_48 = s(index_47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp122) ).
fof(f179,axiom,
index_51 = select(q15,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp123) ).
fof(f180,axiom,
index_54 = s(index_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp124) ).
fof(f181,axiom,
index_57 = select(q16,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp125) ).
fof(f182,axiom,
index_6 = s(index_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp126) ).
fof(f183,axiom,
index_60 = s(index_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp127) ).
fof(f184,axiom,
index_63 = select(q17,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp128) ).
fof(f185,axiom,
index_66 = s(index_63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp129) ).
fof(f186,axiom,
index_68 = select(queue_67,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp130) ).
fof(f187,axiom,
index_69 = s(index_68),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp131) ).
fof(f188,axiom,
index_72 = select(q18,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp132) ).
fof(f189,axiom,
index_75 = s(index_72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp133) ).
fof(f190,axiom,
index_78 = select(q1,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp134) ).
fof(f191,axiom,
index_81 = s(index_78),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp135) ).
fof(f192,axiom,
index_84 = select(q19,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp136) ).
fof(f193,axiom,
index_87 = s(index_84),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp137) ).
fof(f194,axiom,
index_9 = select(q9,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp138) ).
fof(f195,axiom,
index_90 = select(q20,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp139) ).
fof(f196,axiom,
index_93 = s(index_90),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp140) ).
fof(f197,axiom,
index_95 = select(queue_94,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp141) ).
fof(f198,axiom,
index_96 = s(index_95),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp142) ).
fof(f199,axiom,
index_99 = select(q21,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp143) ).
fof(f200,axiom,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp144) ).
fof(f201,axiom,
queue_101 = store(q21,seq,earray_100),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp145) ).
fof(f202,axiom,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp146) ).
fof(f203,axiom,
queue_107 = store(q22,seq,earray_106),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp147) ).
fof(f204,axiom,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp148) ).
fof(f205,axiom,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp149) ).
fof(f206,axiom,
queue_113 = store(q23,seq,earray_112),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp150) ).
fof(f207,axiom,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp151) ).
fof(f208,axiom,
queue_118 = store(queue_115,head,index_117),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp152) ).
fof(f209,axiom,
queue_122 = store(q24,seq,earray_121),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp153) ).
fof(f210,axiom,
queue_124 = store(queue_122,tail,index_123),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp154) ).
fof(f211,axiom,
queue_128 = store(q25,seq,earray_127),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp155) ).
fof(f212,axiom,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp156) ).
fof(f213,axiom,
queue_130 = store(queue_128,tail,index_129),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp157) ).
fof(f214,axiom,
queue_134 = store(q26,seq,earray_133),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp158) ).
fof(f215,axiom,
queue_136 = store(queue_134,tail,index_135),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp159) ).
fof(f216,axiom,
queue_139 = store(queue_136,head,index_138),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp160) ).
fof(f217,axiom,
queue_143 = store(q27,seq,earray_142),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp161) ).
fof(f218,axiom,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp162) ).
fof(f219,axiom,
queue_149 = store(q28,seq,earray_148),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp163) ).
fof(f220,axiom,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp164) ).
fof(f221,axiom,
queue_155 = store(q2,seq,earray_154),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp165) ).
fof(f222,axiom,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp166) ).
fof(f223,axiom,
queue_160 = store(queue_157,head,index_159),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp167) ).
fof(f224,axiom,
queue_164 = store(q29,seq,earray_163),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp168) ).
fof(f225,axiom,
queue_166 = store(queue_164,tail,index_165),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp169) ).
fof(f226,axiom,
queue_169 = store(queue_166,head,index_168),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp170) ).
fof(f227,axiom,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp171) ).
fof(f228,axiom,
queue_173 = store(q3,seq,earray_172),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp172) ).
fof(f229,axiom,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp173) ).
fof(f230,axiom,
queue_179 = store(q4,seq,earray_178),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp174) ).
fof(f231,axiom,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp175) ).
fof(f232,axiom,
queue_185 = store(q5,seq,earray_184),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp176) ).
fof(f233,axiom,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp177) ).
fof(f234,axiom,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp178) ).
fof(f235,axiom,
queue_190 = store(queue_187,head,index_189),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp179) ).
fof(f236,axiom,
queue_194 = store(q6,seq,earray_193),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp180) ).
fof(f237,axiom,
queue_196 = store(queue_194,tail,index_195),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp181) ).
fof(f238,axiom,
queue_200 = store(q7,seq,earray_199),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp182) ).
fof(f239,axiom,
queue_202 = store(queue_200,tail,index_201),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp183) ).
fof(f240,axiom,
queue_206 = store(q8,seq,earray_205),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp184) ).
fof(f241,axiom,
queue_208 = store(queue_206,tail,index_207),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp185) ).
fof(f242,axiom,
queue_211 = store(queue_208,head,index_210),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp186) ).
fof(f243,axiom,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp187) ).
fof(f244,axiom,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp188) ).
fof(f245,axiom,
queue_28 = store(queue_25,head,index_27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp189) ).
fof(f246,axiom,
queue_32 = store(q12,seq,earray_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp190) ).
fof(f247,axiom,
queue_34 = store(queue_32,tail,index_33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp191) ).
fof(f248,axiom,
queue_38 = store(q13,seq,earray_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp192) ).
fof(f249,axiom,
queue_40 = store(queue_38,tail,index_39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp193) ).
fof(f250,axiom,
queue_44 = store(q14,seq,earray_43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp194) ).
fof(f251,axiom,
queue_46 = store(queue_44,tail,index_45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp195) ).
fof(f252,axiom,
queue_49 = store(queue_46,head,index_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp196) ).
fof(f253,axiom,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp197) ).
fof(f254,axiom,
queue_53 = store(q15,seq,earray_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp198) ).
fof(f255,axiom,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp199) ).
fof(f256,axiom,
queue_59 = store(q16,seq,earray_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp200) ).
fof(f257,axiom,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp201) ).
fof(f258,axiom,
queue_65 = store(q17,seq,earray_64),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp202) ).
fof(f259,axiom,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp203) ).
fof(f260,axiom,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp204) ).
fof(f261,axiom,
queue_70 = store(queue_67,head,index_69),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp205) ).
fof(f262,axiom,
queue_74 = store(q18,seq,earray_73),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp206) ).
fof(f263,axiom,
queue_76 = store(queue_74,tail,index_75),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp207) ).
fof(f264,axiom,
queue_80 = store(q1,seq,earray_79),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp208) ).
fof(f265,axiom,
queue_82 = store(queue_80,tail,index_81),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp209) ).
fof(f266,axiom,
queue_86 = store(q19,seq,earray_85),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp210) ).
fof(f267,axiom,
queue_88 = store(queue_86,tail,index_87),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp211) ).
fof(f268,axiom,
queue_92 = store(q20,seq,earray_91),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp212) ).
fof(f269,axiom,
queue_94 = store(queue_92,tail,index_93),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp213) ).
fof(f270,axiom,
queue_97 = store(queue_94,head,index_96),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp214) ).
fof(f271,axiom,
q0 = queue_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp215) ).
fof(f272,axiom,
q1 = queue_7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp216) ).
fof(f273,axiom,
q10 = queue_13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp217) ).
fof(f274,axiom,
q11 = queue_19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp218) ).
fof(f275,axiom,
q12 = queue_28,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp219) ).
fof(f276,axiom,
q13 = queue_34,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp220) ).
fof(f277,axiom,
q14 = queue_40,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp221) ).
fof(f278,axiom,
q15 = queue_49,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp222) ).
fof(f279,axiom,
q16 = queue_55,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp223) ).
fof(f280,axiom,
q17 = queue_61,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp224) ).
fof(f281,axiom,
q18 = queue_70,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp225) ).
fof(f282,axiom,
q19 = queue_76,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp226) ).
fof(f283,axiom,
q2 = queue_82,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp227) ).
fof(f284,axiom,
q20 = queue_88,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp228) ).
fof(f285,axiom,
q21 = queue_97,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp229) ).
fof(f286,axiom,
q22 = queue_103,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp230) ).
fof(f287,axiom,
q23 = queue_109,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp231) ).
fof(f288,axiom,
q24 = queue_118,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp232) ).
fof(f289,axiom,
q25 = queue_124,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp233) ).
fof(f290,axiom,
q26 = queue_130,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp234) ).
fof(f291,axiom,
q27 = queue_139,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp235) ).
fof(f292,axiom,
q28 = queue_145,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp236) ).
fof(f293,axiom,
q29 = queue_151,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp237) ).
fof(f294,axiom,
q3 = queue_160,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp238) ).
fof(f295,axiom,
q30 = queue_169,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp239) ).
fof(f296,axiom,
q4 = queue_175,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp240) ).
fof(f297,axiom,
q5 = queue_181,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp241) ).
fof(f298,axiom,
q6 = queue_190,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp242) ).
fof(f299,axiom,
q7 = queue_196,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp243) ).
fof(f300,axiom,
q8 = queue_202,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp244) ).
fof(f301,axiom,
q9 = queue_211,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp245) ).
fof(f302,negated_conjecture,
elem_214 != e10,
file('/export/starexec/sandbox/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]) ).
fof(f406,plain,
index_15 != index_18,
inference(superposition,[],[f55,f151]) ).
fof(f446,plain,
index_15 != s(index_18),
inference(superposition,[],[f54,f151]) ).
fof(f486,plain,
index_15 != s(s(index_18)),
inference(superposition,[],[f53,f151]) ).
fof(f526,plain,
index_15 != s(s(s(index_18))),
inference(superposition,[],[f52,f151]) ).
fof(f563,plain,
e10 = select(earray_16,index_15),
inference(superposition,[],[f1,f75]) ).
fof(f586,plain,
index_0 = select(queue_1,head),
inference(superposition,[],[f1,f200]) ).
fof(f587,plain,
index_117 = select(queue_118,head),
inference(superposition,[],[f1,f208]) ).
fof(f588,plain,
index_138 = select(queue_139,head),
inference(superposition,[],[f1,f216]) ).
fof(f589,plain,
index_159 = select(queue_160,head),
inference(superposition,[],[f1,f223]) ).
fof(f590,plain,
index_168 = select(queue_169,head),
inference(superposition,[],[f1,f226]) ).
fof(f591,plain,
index_189 = select(queue_190,head),
inference(superposition,[],[f1,f235]) ).
fof(f592,plain,
index_210 = select(queue_211,head),
inference(superposition,[],[f1,f242]) ).
fof(f593,plain,
index_27 = select(queue_28,head),
inference(superposition,[],[f1,f245]) ).
fof(f594,plain,
index_48 = select(queue_49,head),
inference(superposition,[],[f1,f252]) ).
fof(f595,plain,
index_69 = select(queue_70,head),
inference(superposition,[],[f1,f261]) ).
fof(f596,plain,
index_96 = select(queue_97,head),
inference(superposition,[],[f1,f270]) ).
fof(f598,plain,
index_102 = select(queue_103,tail),
inference(superposition,[],[f1,f202]) ).
fof(f599,plain,
earray_106 = select(queue_107,seq),
inference(superposition,[],[f1,f367]) ).
fof(f600,plain,
index_108 = select(queue_109,tail),
inference(superposition,[],[f1,f204]) ).
fof(f601,plain,
earray_112 = select(queue_113,seq),
inference(superposition,[],[f1,f369]) ).
fof(f602,plain,
index_12 = select(queue_13,tail),
inference(superposition,[],[f1,f212]) ).
fof(f603,plain,
index_114 = select(queue_115,tail),
inference(superposition,[],[f1,f207]) ).
fof(f604,plain,
earray_121 = select(queue_122,seq),
inference(superposition,[],[f1,f370]) ).
fof(f605,plain,
index_123 = select(queue_124,tail),
inference(superposition,[],[f1,f210]) ).
fof(f606,plain,
earray_127 = select(queue_128,seq),
inference(superposition,[],[f1,f371]) ).
fof(f607,plain,
index_129 = select(queue_130,tail),
inference(superposition,[],[f1,f213]) ).
fof(f608,plain,
earray_16 = select(queue_17,seq),
inference(superposition,[],[f1,f377]) ).
fof(f609,plain,
earray_133 = select(queue_134,seq),
inference(superposition,[],[f1,f372]) ).
fof(f610,plain,
index_135 = select(queue_136,tail),
inference(superposition,[],[f1,f215]) ).
fof(f611,plain,
earray_142 = select(queue_143,seq),
inference(superposition,[],[f1,f373]) ).
fof(f612,plain,
index_144 = select(queue_145,tail),
inference(superposition,[],[f1,f218]) ).
fof(f613,plain,
earray_148 = select(queue_149,seq),
inference(superposition,[],[f1,f374]) ).
fof(f614,plain,
index_150 = select(queue_151,tail),
inference(superposition,[],[f1,f220]) ).
fof(f615,plain,
earray_163 = select(queue_164,seq),
inference(superposition,[],[f1,f376]) ).
fof(f616,plain,
index_156 = select(queue_157,tail),
inference(superposition,[],[f1,f222]) ).
fof(f619,plain,
index_18 = select(queue_19,tail),
inference(superposition,[],[f1,f234]) ).
fof(f620,plain,
index_174 = select(queue_175,tail),
inference(superposition,[],[f1,f229]) ).
fof(f622,plain,
index_180 = select(queue_181,tail),
inference(superposition,[],[f1,f231]) ).
fof(f624,plain,
index_186 = select(queue_187,tail),
inference(superposition,[],[f1,f233]) ).
fof(f625,plain,
earray_22 = select(queue_23,seq),
inference(superposition,[],[f1,f384]) ).
fof(f627,plain,
index_195 = select(queue_196,tail),
inference(superposition,[],[f1,f237]) ).
fof(f629,plain,
index_201 = select(queue_202,tail),
inference(superposition,[],[f1,f239]) ).
fof(f631,plain,
index_207 = select(queue_208,tail),
inference(superposition,[],[f1,f241]) ).
fof(f633,plain,
index_24 = select(queue_25,tail),
inference(superposition,[],[f1,f244]) ).
fof(f634,plain,
earray_31 = select(queue_32,seq),
inference(superposition,[],[f1,f385]) ).
fof(f635,plain,
index_33 = select(queue_34,tail),
inference(superposition,[],[f1,f247]) ).
fof(f636,plain,
earray_37 = select(queue_38,seq),
inference(superposition,[],[f1,f386]) ).
fof(f637,plain,
index_39 = select(queue_40,tail),
inference(superposition,[],[f1,f249]) ).
fof(f638,plain,
earray_43 = select(queue_44,seq),
inference(superposition,[],[f1,f387]) ).
fof(f639,plain,
index_45 = select(queue_46,tail),
inference(superposition,[],[f1,f251]) ).
fof(f640,plain,
earray_52 = select(queue_53,seq),
inference(superposition,[],[f1,f389]) ).
fof(f641,plain,
index_6 = select(queue_7,tail),
inference(superposition,[],[f1,f260]) ).
fof(f642,plain,
index_54 = select(queue_55,tail),
inference(superposition,[],[f1,f255]) ).
fof(f643,plain,
earray_58 = select(queue_59,seq),
inference(superposition,[],[f1,f390]) ).
fof(f644,plain,
index_60 = select(queue_61,tail),
inference(superposition,[],[f1,f257]) ).
fof(f645,plain,
earray_64 = select(queue_65,seq),
inference(superposition,[],[f1,f391]) ).
fof(f646,plain,
index_66 = select(queue_67,tail),
inference(superposition,[],[f1,f259]) ).
fof(f648,plain,
earray_73 = select(queue_74,seq),
inference(superposition,[],[f1,f392]) ).
fof(f649,plain,
index_75 = select(queue_76,tail),
inference(superposition,[],[f1,f263]) ).
fof(f650,plain,
earray_85 = select(queue_86,seq),
inference(superposition,[],[f1,f394]) ).
fof(f651,plain,
index_81 = select(queue_82,tail),
inference(superposition,[],[f1,f265]) ).
fof(f653,plain,
index_87 = select(queue_88,tail),
inference(superposition,[],[f1,f267]) ).
fof(f654,plain,
earray_91 = select(queue_92,seq),
inference(superposition,[],[f1,f395]) ).
fof(f655,plain,
index_93 = select(queue_94,tail),
inference(superposition,[],[f1,f269]) ).
fof(f656,plain,
earray_100 = select(queue_101,seq),
inference(superposition,[],[f1,f366]) ).
fof(f657,plain,
index_90 = index_87,
inference(forward_demodulation,[],[f653,f364]) ).
fof(f658,plain,
index_153 = index_81,
inference(forward_demodulation,[],[f651,f343]) ).
fof(f659,plain,
index_84 = index_75,
inference(forward_demodulation,[],[f649,f362]) ).
fof(f660,plain,
index_63 = index_60,
inference(forward_demodulation,[],[f644,f359]) ).
fof(f661,plain,
index_57 = index_54,
inference(forward_demodulation,[],[f642,f358]) ).
fof(f662,plain,
index_78 = index_6,
inference(forward_demodulation,[],[f641,f361]) ).
fof(f663,plain,
index_42 = index_39,
inference(forward_demodulation,[],[f637,f356]) ).
fof(f664,plain,
index_36 = index_33,
inference(forward_demodulation,[],[f635,f355]) ).
fof(f665,plain,
index_204 = index_201,
inference(forward_demodulation,[],[f629,f350]) ).
fof(f666,plain,
index_198 = index_195,
inference(forward_demodulation,[],[f627,f349]) ).
fof(f667,plain,
index_183 = index_180,
inference(forward_demodulation,[],[f622,f347]) ).
fof(f668,plain,
index_177 = index_174,
inference(forward_demodulation,[],[f620,f346]) ).
fof(f669,plain,
index_21 = index_18,
inference(forward_demodulation,[],[f619,f351]) ).
fof(f670,plain,
index_162 = index_150,
inference(forward_demodulation,[],[f614,f344]) ).
fof(f671,plain,
index_147 = index_144,
inference(forward_demodulation,[],[f612,f341]) ).
fof(f672,plain,
index_132 = index_129,
inference(forward_demodulation,[],[f607,f339]) ).
fof(f673,plain,
index_126 = index_123,
inference(forward_demodulation,[],[f605,f338]) ).
fof(f674,plain,
index_15 = index_12,
inference(forward_demodulation,[],[f602,f342]) ).
fof(f675,plain,
index_111 = index_108,
inference(forward_demodulation,[],[f600,f336]) ).
fof(f676,plain,
index_105 = index_102,
inference(forward_demodulation,[],[f598,f335]) ).
fof(f677,plain,
index_213 = index_168,
inference(forward_demodulation,[],[f590,f352]) ).
fof(f691,plain,
index_15 != s(s(s(s(index_18)))),
inference(superposition,[],[f51,f151]) ).
fof(f733,plain,
index_15 != s(s(s(s(s(index_18))))),
inference(superposition,[],[f50,f151]) ).
fof(f787,plain,
index_15 != s(s(s(s(s(s(index_18)))))),
inference(superposition,[],[f49,f151]) ).
fof(f841,plain,
index_15 != s(s(s(s(s(s(s(index_18))))))),
inference(superposition,[],[f48,f151]) ).
fof(f895,plain,
index_15 != s(s(s(s(s(s(s(s(index_18)))))))),
inference(superposition,[],[f47,f151]) ).
fof(f940,plain,
! [X0] :
( select(earray_98,X0) = select(earray_100,X0)
| index_99 = X0 ),
inference(superposition,[],[f2,f57]) ).
fof(f950,plain,
! [X0] :
( select(earray_161,X0) = select(earray_163,X0)
| index_162 = X0 ),
inference(superposition,[],[f2,f77]) ).
fof(f965,plain,
! [X0] :
( select(earray_71,X0) = select(earray_73,X0)
| index_72 = X0 ),
inference(superposition,[],[f2,f108]) ).
fof(f967,plain,
! [X0] :
( select(earray_83,X0) = select(earray_85,X0)
| index_84 = X0 ),
inference(superposition,[],[f2,f113]) ).
fof(f968,plain,
! [X0] :
( select(earray_89,X0) = select(earray_91,X0)
| index_90 = X0 ),
inference(superposition,[],[f2,f115]) ).
fof(f969,plain,
! [X0] :
( select(q,X0) = select(queue_1,X0)
| head = X0 ),
inference(superposition,[],[f2,f200]) ).
fof(f970,plain,
! [X0] :
( select(queue_115,X0) = select(queue_118,X0)
| head = X0 ),
inference(superposition,[],[f2,f208]) ).
fof(f971,plain,
! [X0] :
( select(queue_136,X0) = select(queue_139,X0)
| head = X0 ),
inference(superposition,[],[f2,f216]) ).
fof(f972,plain,
! [X0] :
( select(queue_157,X0) = select(queue_160,X0)
| head = X0 ),
inference(superposition,[],[f2,f223]) ).
fof(f973,plain,
! [X0] :
( select(queue_166,X0) = select(queue_169,X0)
| head = X0 ),
inference(superposition,[],[f2,f226]) ).
fof(f974,plain,
! [X0] :
( select(queue_187,X0) = select(queue_190,X0)
| head = X0 ),
inference(superposition,[],[f2,f235]) ).
fof(f975,plain,
! [X0] :
( select(queue_208,X0) = select(queue_211,X0)
| head = X0 ),
inference(superposition,[],[f2,f242]) ).
fof(f976,plain,
! [X0] :
( select(queue_25,X0) = select(queue_28,X0)
| head = X0 ),
inference(superposition,[],[f2,f245]) ).
fof(f977,plain,
! [X0] :
( select(queue_46,X0) = select(queue_49,X0)
| head = X0 ),
inference(superposition,[],[f2,f252]) ).
fof(f978,plain,
! [X0] :
( select(queue_67,X0) = select(queue_70,X0)
| head = X0 ),
inference(superposition,[],[f2,f261]) ).
fof(f979,plain,
! [X0] :
( select(queue_94,X0) = select(queue_97,X0)
| head = X0 ),
inference(superposition,[],[f2,f270]) ).
fof(f980,plain,
! [X0] :
( select(queue_1,X0) = select(queue_5,X0)
| seq = X0 ),
inference(superposition,[],[f2,f388]) ).
fof(f981,plain,
! [X0] :
( select(queue_101,X0) = select(queue_103,X0)
| tail = X0 ),
inference(superposition,[],[f2,f202]) ).
fof(f982,plain,
! [X0] :
( select(queue_103,X0) = select(queue_107,X0)
| seq = X0 ),
inference(superposition,[],[f2,f367]) ).
fof(f983,plain,
! [X0] :
( select(queue_107,X0) = select(queue_109,X0)
| tail = X0 ),
inference(superposition,[],[f2,f204]) ).
fof(f984,plain,
! [X0] :
( select(queue_109,X0) = select(queue_113,X0)
| seq = X0 ),
inference(superposition,[],[f2,f369]) ).
fof(f985,plain,
! [X0] :
( select(queue_11,X0) = select(queue_13,X0)
| tail = X0 ),
inference(superposition,[],[f2,f212]) ).
fof(f986,plain,
! [X0] :
( select(queue_115,X0) = select(queue_113,X0)
| tail = X0 ),
inference(superposition,[],[f2,f207]) ).
fof(f987,plain,
! [X0] :
( select(queue_118,X0) = select(queue_122,X0)
| seq = X0 ),
inference(superposition,[],[f2,f370]) ).
fof(f988,plain,
! [X0] :
( select(queue_122,X0) = select(queue_124,X0)
| tail = X0 ),
inference(superposition,[],[f2,f210]) ).
fof(f989,plain,
! [X0] :
( select(queue_124,X0) = select(queue_128,X0)
| seq = X0 ),
inference(superposition,[],[f2,f371]) ).
fof(f990,plain,
! [X0] :
( select(queue_128,X0) = select(queue_130,X0)
| tail = X0 ),
inference(superposition,[],[f2,f213]) ).
fof(f991,plain,
! [X0] :
( select(queue_13,X0) = select(queue_17,X0)
| seq = X0 ),
inference(superposition,[],[f2,f377]) ).
fof(f992,plain,
! [X0] :
( select(queue_130,X0) = select(queue_134,X0)
| seq = X0 ),
inference(superposition,[],[f2,f372]) ).
fof(f993,plain,
! [X0] :
( select(queue_136,X0) = select(queue_134,X0)
| tail = X0 ),
inference(superposition,[],[f2,f215]) ).
fof(f994,plain,
! [X0] :
( select(queue_139,X0) = select(queue_143,X0)
| seq = X0 ),
inference(superposition,[],[f2,f373]) ).
fof(f995,plain,
! [X0] :
( select(queue_143,X0) = select(queue_145,X0)
| tail = X0 ),
inference(superposition,[],[f2,f218]) ).
fof(f996,plain,
! [X0] :
( select(queue_145,X0) = select(queue_149,X0)
| seq = X0 ),
inference(superposition,[],[f2,f374]) ).
fof(f997,plain,
! [X0] :
( select(queue_149,X0) = select(queue_151,X0)
| tail = X0 ),
inference(superposition,[],[f2,f220]) ).
fof(f998,plain,
! [X0] :
( select(queue_151,X0) = select(queue_164,X0)
| seq = X0 ),
inference(superposition,[],[f2,f376]) ).
fof(f999,plain,
! [X0] :
( select(queue_157,X0) = select(queue_155,X0)
| tail = X0 ),
inference(superposition,[],[f2,f222]) ).
fof(f1000,plain,
! [X0] :
( select(queue_160,X0) = select(queue_173,X0)
| seq = X0 ),
inference(superposition,[],[f2,f378]) ).
fof(f1001,plain,
! [X0] :
( select(queue_166,X0) = select(queue_164,X0)
| tail = X0 ),
inference(superposition,[],[f2,f225]) ).
fof(f1002,plain,
! [X0] :
( select(queue_17,X0) = select(queue_19,X0)
| tail = X0 ),
inference(superposition,[],[f2,f234]) ).
fof(f1003,plain,
! [X0] :
( select(queue_173,X0) = select(queue_175,X0)
| tail = X0 ),
inference(superposition,[],[f2,f229]) ).
fof(f1004,plain,
! [X0] :
( select(queue_175,X0) = select(queue_179,X0)
| seq = X0 ),
inference(superposition,[],[f2,f379]) ).
fof(f1005,plain,
! [X0] :
( select(queue_179,X0) = select(queue_181,X0)
| tail = X0 ),
inference(superposition,[],[f2,f231]) ).
fof(f1006,plain,
! [X0] :
( select(queue_181,X0) = select(queue_185,X0)
| seq = X0 ),
inference(superposition,[],[f2,f380]) ).
fof(f1007,plain,
! [X0] :
( select(queue_187,X0) = select(queue_185,X0)
| tail = X0 ),
inference(superposition,[],[f2,f233]) ).
fof(f1008,plain,
! [X0] :
( select(queue_19,X0) = select(queue_23,X0)
| seq = X0 ),
inference(superposition,[],[f2,f384]) ).
fof(f1009,plain,
! [X0] :
( select(queue_190,X0) = select(queue_194,X0)
| seq = X0 ),
inference(superposition,[],[f2,f381]) ).
fof(f1010,plain,
! [X0] :
( select(queue_194,X0) = select(queue_196,X0)
| tail = X0 ),
inference(superposition,[],[f2,f237]) ).
fof(f1011,plain,
! [X0] :
( select(queue_196,X0) = select(queue_200,X0)
| seq = X0 ),
inference(superposition,[],[f2,f382]) ).
fof(f1012,plain,
! [X0] :
( select(queue_200,X0) = select(queue_202,X0)
| tail = X0 ),
inference(superposition,[],[f2,f239]) ).
fof(f1013,plain,
! [X0] :
( select(queue_202,X0) = select(queue_206,X0)
| seq = X0 ),
inference(superposition,[],[f2,f383]) ).
fof(f1014,plain,
! [X0] :
( select(queue_208,X0) = select(queue_206,X0)
| tail = X0 ),
inference(superposition,[],[f2,f241]) ).
fof(f1015,plain,
! [X0] :
( select(queue_211,X0) = select(queue_11,X0)
| seq = X0 ),
inference(superposition,[],[f2,f368]) ).
fof(f1016,plain,
! [X0] :
( select(queue_25,X0) = select(queue_23,X0)
| tail = X0 ),
inference(superposition,[],[f2,f244]) ).
fof(f1017,plain,
! [X0] :
( select(queue_28,X0) = select(queue_32,X0)
| seq = X0 ),
inference(superposition,[],[f2,f385]) ).
fof(f1018,plain,
! [X0] :
( select(queue_32,X0) = select(queue_34,X0)
| tail = X0 ),
inference(superposition,[],[f2,f247]) ).
fof(f1019,plain,
! [X0] :
( select(queue_34,X0) = select(queue_38,X0)
| seq = X0 ),
inference(superposition,[],[f2,f386]) ).
fof(f1020,plain,
! [X0] :
( select(queue_38,X0) = select(queue_40,X0)
| tail = X0 ),
inference(superposition,[],[f2,f249]) ).
fof(f1021,plain,
! [X0] :
( select(queue_40,X0) = select(queue_44,X0)
| seq = X0 ),
inference(superposition,[],[f2,f387]) ).
fof(f1022,plain,
! [X0] :
( select(queue_46,X0) = select(queue_44,X0)
| tail = X0 ),
inference(superposition,[],[f2,f251]) ).
fof(f1023,plain,
! [X0] :
( select(queue_49,X0) = select(queue_53,X0)
| seq = X0 ),
inference(superposition,[],[f2,f389]) ).
fof(f1024,plain,
! [X0] :
( select(queue_5,X0) = select(queue_7,X0)
| tail = X0 ),
inference(superposition,[],[f2,f260]) ).
fof(f1025,plain,
! [X0] :
( select(queue_53,X0) = select(queue_55,X0)
| tail = X0 ),
inference(superposition,[],[f2,f255]) ).
fof(f1026,plain,
! [X0] :
( select(queue_55,X0) = select(queue_59,X0)
| seq = X0 ),
inference(superposition,[],[f2,f390]) ).
fof(f1027,plain,
! [X0] :
( select(queue_59,X0) = select(queue_61,X0)
| tail = X0 ),
inference(superposition,[],[f2,f257]) ).
fof(f1028,plain,
! [X0] :
( select(queue_61,X0) = select(queue_65,X0)
| seq = X0 ),
inference(superposition,[],[f2,f391]) ).
fof(f1029,plain,
! [X0] :
( select(queue_67,X0) = select(queue_65,X0)
| tail = X0 ),
inference(superposition,[],[f2,f259]) ).
fof(f1030,plain,
! [X0] :
( select(queue_7,X0) = select(queue_80,X0)
| seq = X0 ),
inference(superposition,[],[f2,f393]) ).
fof(f1031,plain,
! [X0] :
( select(queue_70,X0) = select(queue_74,X0)
| seq = X0 ),
inference(superposition,[],[f2,f392]) ).
fof(f1032,plain,
! [X0] :
( select(queue_74,X0) = select(queue_76,X0)
| tail = X0 ),
inference(superposition,[],[f2,f263]) ).
fof(f1033,plain,
! [X0] :
( select(queue_76,X0) = select(queue_86,X0)
| seq = X0 ),
inference(superposition,[],[f2,f394]) ).
fof(f1034,plain,
! [X0] :
( select(queue_80,X0) = select(queue_82,X0)
| tail = X0 ),
inference(superposition,[],[f2,f265]) ).
fof(f1035,plain,
! [X0] :
( select(queue_155,X0) = select(queue_82,X0)
| seq = X0 ),
inference(superposition,[],[f2,f375]) ).
fof(f1036,plain,
! [X0] :
( select(queue_86,X0) = select(queue_88,X0)
| tail = X0 ),
inference(superposition,[],[f2,f267]) ).
fof(f1037,plain,
! [X0] :
( select(queue_88,X0) = select(queue_92,X0)
| seq = X0 ),
inference(superposition,[],[f2,f395]) ).
fof(f1038,plain,
! [X0] :
( select(queue_94,X0) = select(queue_92,X0)
| tail = X0 ),
inference(superposition,[],[f2,f269]) ).
fof(f1039,plain,
! [X0] :
( select(queue_97,X0) = select(queue_101,X0)
| seq = X0 ),
inference(superposition,[],[f2,f366]) ).
fof(f1053,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_18))))))))),
inference(superposition,[],[f46,f151]) ).
fof(f1111,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_18)))))))))),
inference(superposition,[],[f45,f151]) ).
fof(f1169,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))),
inference(superposition,[],[f44,f151]) ).
fof(f1227,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))),
inference(superposition,[],[f43,f151]) ).
fof(f1285,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))),
inference(superposition,[],[f42,f151]) ).
fof(f1343,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))),
inference(superposition,[],[f41,f151]) ).
fof(f1401,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))),
inference(superposition,[],[f40,f151]) ).
fof(f1459,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))),
inference(superposition,[],[f39,f151]) ).
fof(f1517,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))))),
inference(superposition,[],[f38,f151]) ).
fof(f1581,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))))),
inference(superposition,[],[f37,f151]) ).
fof(f2982,plain,
index_15 != s(index_21),
inference(superposition,[],[f446,f669]) ).
fof(f2983,plain,
index_15 != index_21,
inference(superposition,[],[f406,f669]) ).
fof(f3950,plain,
index_15 != s(s(index_21)),
inference(forward_demodulation,[],[f486,f669]) ).
fof(f3951,plain,
index_15 != s(index_24),
inference(forward_demodulation,[],[f3950,f167]) ).
fof(f4007,plain,
index_15 != index_24,
inference(superposition,[],[f2982,f167]) ).
fof(f4043,plain,
index_15 != s(s(s(index_21))),
inference(forward_demodulation,[],[f526,f669]) ).
fof(f4044,plain,
index_15 != s(s(index_24)),
inference(forward_demodulation,[],[f4043,f167]) ).
fof(f4116,plain,
index_15 != s(s(s(s(index_21)))),
inference(forward_demodulation,[],[f691,f669]) ).
fof(f4117,plain,
index_15 != s(s(s(index_24))),
inference(forward_demodulation,[],[f4116,f167]) ).
fof(f4205,plain,
index_15 != s(s(s(s(s(index_21))))),
inference(forward_demodulation,[],[f733,f669]) ).
fof(f4206,plain,
index_15 != s(s(s(s(index_24)))),
inference(forward_demodulation,[],[f4205,f167]) ).
fof(f4264,plain,
index_15 != s(s(s(s(s(s(index_21)))))),
inference(forward_demodulation,[],[f787,f669]) ).
fof(f4265,plain,
index_15 != s(s(s(s(s(index_24))))),
inference(forward_demodulation,[],[f4264,f167]) ).
fof(f4311,plain,
index_15 != s(s(s(s(s(s(s(index_21))))))),
inference(forward_demodulation,[],[f841,f669]) ).
fof(f4312,plain,
index_15 != s(s(s(s(s(s(index_24)))))),
inference(forward_demodulation,[],[f4311,f167]) ).
fof(f4337,plain,
( index_0 = select(queue_1,tail)
| head = tail ),
inference(superposition,[],[f118,f969]) ).
fof(f4338,plain,
index_0 = select(queue_1,tail),
inference(forward_subsumption_resolution,[],[f4337,f3]) ).
fof(f4340,plain,
index_3 = index_0,
inference(forward_demodulation,[],[f4338,f353]) ).
fof(f4343,plain,
( index_114 = select(queue_118,tail)
| head = tail ),
inference(superposition,[],[f603,f970]) ).
fof(f4344,plain,
index_114 = select(queue_118,tail),
inference(forward_subsumption_resolution,[],[f4343,f3]) ).
fof(f4346,plain,
index_120 = index_114,
inference(forward_demodulation,[],[f4344,f337]) ).
fof(f4349,plain,
( index_135 = select(queue_139,tail)
| head = tail ),
inference(superposition,[],[f610,f971]) ).
fof(f4350,plain,
index_135 = select(queue_139,tail),
inference(forward_subsumption_resolution,[],[f4349,f3]) ).
fof(f4352,plain,
index_141 = index_135,
inference(forward_demodulation,[],[f4350,f340]) ).
fof(f4356,plain,
( index_156 = select(queue_160,tail)
| head = tail ),
inference(superposition,[],[f616,f972]) ).
fof(f4357,plain,
index_156 = select(queue_160,tail),
inference(forward_subsumption_resolution,[],[f4356,f3]) ).
fof(f4359,plain,
index_171 = index_156,
inference(forward_demodulation,[],[f4357,f345]) ).
fof(f4362,plain,
( earray_212 = select(queue_166,seq)
| head = seq ),
inference(superposition,[],[f322,f973]) ).
fof(f4363,plain,
earray_212 = select(queue_166,seq),
inference(forward_subsumption_resolution,[],[f4362,f4]) ).
fof(f4366,plain,
( index_186 = select(queue_190,tail)
| head = tail ),
inference(superposition,[],[f624,f974]) ).
fof(f4367,plain,
index_186 = select(queue_190,tail),
inference(forward_subsumption_resolution,[],[f4366,f3]) ).
fof(f4369,plain,
index_192 = index_186,
inference(forward_demodulation,[],[f4367,f348]) ).
fof(f4542,plain,
( index_207 = select(queue_211,tail)
| head = tail ),
inference(superposition,[],[f631,f975]) ).
fof(f4543,plain,
index_207 = select(queue_211,tail),
inference(forward_subsumption_resolution,[],[f4542,f3]) ).
fof(f4545,plain,
index_9 = index_207,
inference(forward_demodulation,[],[f4543,f363]) ).
fof(f4548,plain,
( index_24 = select(queue_28,tail)
| head = tail ),
inference(superposition,[],[f633,f976]) ).
fof(f4549,plain,
index_24 = select(queue_28,tail),
inference(forward_subsumption_resolution,[],[f4548,f3]) ).
fof(f4551,plain,
index_30 = index_24,
inference(forward_demodulation,[],[f4549,f354]) ).
fof(f4554,plain,
( index_45 = select(queue_49,tail)
| head = tail ),
inference(superposition,[],[f639,f977]) ).
fof(f4555,plain,
index_45 = select(queue_49,tail),
inference(forward_subsumption_resolution,[],[f4554,f3]) ).
fof(f4557,plain,
index_51 = index_45,
inference(forward_demodulation,[],[f4555,f357]) ).
fof(f4560,plain,
( index_66 = select(queue_70,tail)
| head = tail ),
inference(superposition,[],[f646,f978]) ).
fof(f4561,plain,
index_66 = select(queue_70,tail),
inference(forward_subsumption_resolution,[],[f4560,f3]) ).
fof(f4563,plain,
index_72 = index_66,
inference(forward_demodulation,[],[f4561,f360]) ).
fof(f4566,plain,
( index_93 = select(queue_97,tail)
| head = tail ),
inference(superposition,[],[f655,f979]) ).
fof(f4567,plain,
index_93 = select(queue_97,tail),
inference(forward_subsumption_resolution,[],[f4566,f3]) ).
fof(f4569,plain,
index_99 = index_93,
inference(forward_demodulation,[],[f4567,f365]) ).
fof(f4663,plain,
( earray_100 = select(queue_103,seq)
| tail = seq ),
inference(superposition,[],[f656,f981]) ).
fof(f4664,plain,
earray_100 = select(queue_103,seq),
inference(forward_subsumption_resolution,[],[f4663,f5]) ).
fof(f4752,plain,
! [X0] :
( select(queue_103,X0) = select(queue_109,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f983,f982]) ).
fof(f4753,plain,
( earray_106 = select(queue_109,seq)
| tail = seq ),
inference(superposition,[],[f599,f983]) ).
fof(f4755,plain,
earray_106 = select(queue_109,seq),
inference(forward_subsumption_resolution,[],[f4753,f5]) ).
fof(f4855,plain,
index_15 != s(index_30),
inference(superposition,[],[f3951,f4551]) ).
fof(f4856,plain,
index_15 != index_30,
inference(superposition,[],[f4007,f4551]) ).
fof(f4859,plain,
index_15 != s(s(index_30)),
inference(superposition,[],[f4044,f4551]) ).
fof(f4861,plain,
index_15 != s(s(s(index_30))),
inference(superposition,[],[f4117,f4551]) ).
fof(f4863,plain,
index_15 != s(s(s(s(index_30)))),
inference(superposition,[],[f4206,f4551]) ).
fof(f4865,plain,
index_15 != s(s(s(s(s(index_30))))),
inference(superposition,[],[f4265,f4551]) ).
fof(f4867,plain,
index_15 != s(s(s(s(s(s(index_30)))))),
inference(superposition,[],[f4312,f4551]) ).
fof(f4868,plain,
index_15 != s(s(s(s(s(index_33))))),
inference(forward_demodulation,[],[f4867,f172]) ).
fof(f4870,plain,
index_15 != s(s(s(s(index_33)))),
inference(forward_demodulation,[],[f4865,f172]) ).
fof(f4872,plain,
index_15 != s(s(s(index_33))),
inference(forward_demodulation,[],[f4863,f172]) ).
fof(f4874,plain,
index_15 != s(s(index_33)),
inference(forward_demodulation,[],[f4861,f172]) ).
fof(f4876,plain,
index_15 != s(index_33),
inference(forward_demodulation,[],[f4859,f172]) ).
fof(f4883,plain,
index_15 != s(s(s(s(s(index_36))))),
inference(forward_demodulation,[],[f4868,f664]) ).
fof(f4885,plain,
index_15 != s(s(s(s(index_36)))),
inference(forward_demodulation,[],[f4870,f664]) ).
fof(f4887,plain,
index_15 != s(s(s(index_36))),
inference(forward_demodulation,[],[f4872,f664]) ).
fof(f4889,plain,
index_15 != s(s(index_36)),
inference(forward_demodulation,[],[f4874,f664]) ).
fof(f4891,plain,
index_15 != s(index_36),
inference(forward_demodulation,[],[f4876,f664]) ).
fof(f4898,plain,
index_15 != s(s(s(s(index_39)))),
inference(forward_demodulation,[],[f4883,f174]) ).
fof(f4900,plain,
index_15 != s(s(s(index_39))),
inference(forward_demodulation,[],[f4885,f174]) ).
fof(f4902,plain,
index_15 != s(s(index_39)),
inference(forward_demodulation,[],[f4887,f174]) ).
fof(f4904,plain,
index_15 != s(index_39),
inference(forward_demodulation,[],[f4889,f174]) ).
fof(f4910,plain,
index_15 != s(s(s(s(index_42)))),
inference(forward_demodulation,[],[f4898,f663]) ).
fof(f4912,plain,
index_15 != s(s(s(index_42))),
inference(forward_demodulation,[],[f4900,f663]) ).
fof(f4914,plain,
index_15 != s(s(index_42)),
inference(forward_demodulation,[],[f4902,f663]) ).
fof(f4916,plain,
index_15 != s(index_42),
inference(forward_demodulation,[],[f4904,f663]) ).
fof(f4922,plain,
index_15 != s(s(s(index_45))),
inference(forward_demodulation,[],[f4910,f176]) ).
fof(f4924,plain,
index_15 != s(s(index_45)),
inference(forward_demodulation,[],[f4912,f176]) ).
fof(f4926,plain,
index_15 != s(index_45),
inference(forward_demodulation,[],[f4914,f176]) ).
fof(f5017,plain,
! [X0] :
( select(queue_115,X0) = select(queue_109,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f986,f984]) ).
fof(f5018,plain,
( earray_112 = select(queue_115,seq)
| tail = seq ),
inference(superposition,[],[f601,f986]) ).
fof(f5020,plain,
earray_112 = select(queue_115,seq),
inference(forward_subsumption_resolution,[],[f5018,f5]) ).
fof(f5120,plain,
! [X0] :
( select(queue_118,X0) = select(queue_124,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f988,f987]) ).
fof(f5121,plain,
( earray_121 = select(queue_124,seq)
| tail = seq ),
inference(superposition,[],[f604,f988]) ).
fof(f5123,plain,
earray_121 = select(queue_124,seq),
inference(forward_subsumption_resolution,[],[f5121,f5]) ).
fof(f5126,plain,
! [X0] :
( select(queue_124,X0) = select(queue_130,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f990,f989]) ).
fof(f5127,plain,
( earray_127 = select(queue_130,seq)
| tail = seq ),
inference(superposition,[],[f606,f990]) ).
fof(f5129,plain,
earray_127 = select(queue_130,seq),
inference(forward_subsumption_resolution,[],[f5127,f5]) ).
fof(f5132,plain,
! [X0] :
( select(queue_136,X0) = select(queue_130,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f993,f992]) ).
fof(f5133,plain,
( earray_133 = select(queue_136,seq)
| tail = seq ),
inference(superposition,[],[f609,f993]) ).
fof(f5135,plain,
earray_133 = select(queue_136,seq),
inference(forward_subsumption_resolution,[],[f5133,f5]) ).
fof(f5276,plain,
! [X0] :
( select(queue_139,X0) = select(queue_145,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f995,f994]) ).
fof(f5277,plain,
( earray_142 = select(queue_145,seq)
| tail = seq ),
inference(superposition,[],[f611,f995]) ).
fof(f5279,plain,
earray_142 = select(queue_145,seq),
inference(forward_subsumption_resolution,[],[f5277,f5]) ).
fof(f5282,plain,
! [X0] :
( select(queue_145,X0) = select(queue_151,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f997,f996]) ).
fof(f5283,plain,
( earray_148 = select(queue_151,seq)
| tail = seq ),
inference(superposition,[],[f613,f997]) ).
fof(f5285,plain,
earray_148 = select(queue_151,seq),
inference(forward_subsumption_resolution,[],[f5283,f5]) ).
fof(f5292,plain,
! [X0] :
( select(queue_166,X0) = select(queue_151,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1001,f998]) ).
fof(f5293,plain,
( earray_163 = select(queue_166,seq)
| tail = seq ),
inference(superposition,[],[f615,f1001]) ).
fof(f5295,plain,
earray_163 = select(queue_166,seq),
inference(forward_subsumption_resolution,[],[f5293,f5]) ).
fof(f5298,plain,
! [X0] :
( select(queue_13,X0) = select(queue_19,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1002,f991]) ).
fof(f5299,plain,
( earray_16 = select(queue_19,seq)
| tail = seq ),
inference(superposition,[],[f608,f1002]) ).
fof(f5301,plain,
earray_16 = select(queue_19,seq),
inference(forward_subsumption_resolution,[],[f5299,f5]) ).
fof(f5304,plain,
! [X0] :
( select(queue_160,X0) = select(queue_175,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1003,f1000]) ).
fof(f5310,plain,
! [X0] :
( select(queue_175,X0) = select(queue_181,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1005,f1004]) ).
fof(f5316,plain,
! [X0] :
( select(queue_187,X0) = select(queue_181,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1007,f1006]) ).
fof(f5322,plain,
! [X0] :
( select(queue_190,X0) = select(queue_196,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1010,f1009]) ).
fof(f5328,plain,
! [X0] :
( select(queue_196,X0) = select(queue_202,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1012,f1011]) ).
fof(f5334,plain,
! [X0] :
( select(queue_208,X0) = select(queue_202,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1014,f1013]) ).
fof(f5339,plain,
! [X0] :
( select(queue_211,X0) = select(queue_13,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f1015,f985]) ).
fof(f5342,plain,
! [X0] :
( select(queue_25,X0) = select(queue_19,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1016,f1008]) ).
fof(f5343,plain,
( earray_22 = select(queue_25,seq)
| tail = seq ),
inference(superposition,[],[f625,f1016]) ).
fof(f5345,plain,
earray_22 = select(queue_25,seq),
inference(forward_subsumption_resolution,[],[f5343,f5]) ).
fof(f5348,plain,
! [X0] :
( select(queue_28,X0) = select(queue_34,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1018,f1017]) ).
fof(f5349,plain,
( earray_31 = select(queue_34,seq)
| tail = seq ),
inference(superposition,[],[f634,f1018]) ).
fof(f5351,plain,
earray_31 = select(queue_34,seq),
inference(forward_subsumption_resolution,[],[f5349,f5]) ).
fof(f5354,plain,
! [X0] :
( select(queue_34,X0) = select(queue_40,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1020,f1019]) ).
fof(f5355,plain,
( earray_37 = select(queue_40,seq)
| tail = seq ),
inference(superposition,[],[f636,f1020]) ).
fof(f5357,plain,
earray_37 = select(queue_40,seq),
inference(forward_subsumption_resolution,[],[f5355,f5]) ).
fof(f5360,plain,
! [X0] :
( select(queue_46,X0) = select(queue_40,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1022,f1021]) ).
fof(f5361,plain,
( earray_43 = select(queue_46,seq)
| tail = seq ),
inference(superposition,[],[f638,f1022]) ).
fof(f5363,plain,
earray_43 = select(queue_46,seq),
inference(forward_subsumption_resolution,[],[f5361,f5]) ).
fof(f5366,plain,
! [X0] :
( select(queue_1,X0) = select(queue_7,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1024,f980]) ).
fof(f5372,plain,
! [X0] :
( select(queue_49,X0) = select(queue_55,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1025,f1023]) ).
fof(f5373,plain,
( earray_52 = select(queue_55,seq)
| tail = seq ),
inference(superposition,[],[f640,f1025]) ).
fof(f5375,plain,
earray_52 = select(queue_55,seq),
inference(forward_subsumption_resolution,[],[f5373,f5]) ).
fof(f5378,plain,
! [X0] :
( select(queue_55,X0) = select(queue_61,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1027,f1026]) ).
fof(f5379,plain,
( earray_58 = select(queue_61,seq)
| tail = seq ),
inference(superposition,[],[f643,f1027]) ).
fof(f5381,plain,
earray_58 = select(queue_61,seq),
inference(forward_subsumption_resolution,[],[f5379,f5]) ).
fof(f5384,plain,
! [X0] :
( select(queue_67,X0) = select(queue_61,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1029,f1028]) ).
fof(f5385,plain,
( earray_64 = select(queue_67,seq)
| tail = seq ),
inference(superposition,[],[f645,f1029]) ).
fof(f5387,plain,
earray_64 = select(queue_67,seq),
inference(forward_subsumption_resolution,[],[f5385,f5]) ).
fof(f5390,plain,
! [X0] :
( select(queue_70,X0) = select(queue_76,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1032,f1031]) ).
fof(f5391,plain,
( earray_73 = select(queue_76,seq)
| tail = seq ),
inference(superposition,[],[f648,f1032]) ).
fof(f5393,plain,
earray_73 = select(queue_76,seq),
inference(forward_subsumption_resolution,[],[f5391,f5]) ).
fof(f5396,plain,
! [X0] :
( select(queue_7,X0) = select(queue_82,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1034,f1030]) ).
fof(f5403,plain,
! [X0] :
( select(queue_157,X0) = select(queue_82,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f1035,f999]) ).
fof(f5406,plain,
! [X0] :
( select(queue_76,X0) = select(queue_88,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1036,f1033]) ).
fof(f5407,plain,
( earray_85 = select(queue_88,seq)
| tail = seq ),
inference(superposition,[],[f650,f1036]) ).
fof(f5409,plain,
earray_85 = select(queue_88,seq),
inference(forward_subsumption_resolution,[],[f5407,f5]) ).
fof(f5415,plain,
! [X0] :
( select(queue_94,X0) = select(queue_88,X0)
| tail = X0
| seq = X0 ),
inference(superposition,[],[f1038,f1037]) ).
fof(f5416,plain,
( earray_91 = select(queue_94,seq)
| tail = seq ),
inference(superposition,[],[f654,f1038]) ).
fof(f5418,plain,
earray_91 = select(queue_94,seq),
inference(forward_subsumption_resolution,[],[f5416,f5]) ).
fof(f5420,plain,
! [X0] :
( select(queue_97,X0) = select(queue_103,X0)
| seq = X0
| tail = X0 ),
inference(superposition,[],[f1039,f981]) ).
fof(f5573,plain,
index_15 != s(s(s(s(s(s(s(s(index_21)))))))),
inference(forward_demodulation,[],[f895,f669]) ).
fof(f5574,plain,
index_15 != s(s(s(s(s(s(s(index_24))))))),
inference(forward_demodulation,[],[f5573,f167]) ).
fof(f5575,plain,
index_15 != s(s(s(s(s(s(s(index_30))))))),
inference(forward_demodulation,[],[f5574,f4551]) ).
fof(f5576,plain,
index_15 != s(s(s(s(s(s(index_33)))))),
inference(forward_demodulation,[],[f5575,f172]) ).
fof(f5577,plain,
index_15 != s(s(s(s(s(s(index_36)))))),
inference(forward_demodulation,[],[f5576,f664]) ).
fof(f5578,plain,
index_15 != s(s(s(s(s(index_39))))),
inference(forward_demodulation,[],[f5577,f174]) ).
fof(f5579,plain,
index_15 != s(s(s(s(s(index_42))))),
inference(forward_demodulation,[],[f5578,f663]) ).
fof(f5580,plain,
index_15 != s(s(s(s(index_45)))),
inference(forward_demodulation,[],[f5579,f176]) ).
fof(f5581,plain,
index_15 != s(s(s(s(index_51)))),
inference(forward_demodulation,[],[f5580,f4557]) ).
fof(f5582,plain,
index_15 != s(s(s(index_54))),
inference(forward_demodulation,[],[f5581,f180]) ).
fof(f5583,plain,
index_15 != s(s(s(index_57))),
inference(forward_demodulation,[],[f5582,f661]) ).
fof(f5584,plain,
index_15 != s(s(index_60)),
inference(forward_demodulation,[],[f5583,f183]) ).
fof(f5585,plain,
index_15 != s(s(index_63)),
inference(forward_demodulation,[],[f5584,f660]) ).
fof(f5586,plain,
index_15 != s(index_66),
inference(forward_demodulation,[],[f5585,f185]) ).
fof(f5587,plain,
index_15 != s(index_72),
inference(forward_demodulation,[],[f5586,f4563]) ).
fof(f5588,plain,
index_15 != index_75,
inference(superposition,[],[f5587,f189]) ).
fof(f5589,plain,
index_15 != index_84,
inference(superposition,[],[f5588,f659]) ).
fof(f6029,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_21))))))))),
inference(forward_demodulation,[],[f1053,f669]) ).
fof(f6030,plain,
index_15 != s(s(s(s(s(s(s(s(index_24)))))))),
inference(forward_demodulation,[],[f6029,f167]) ).
fof(f6031,plain,
index_15 != s(s(s(s(s(s(s(s(index_30)))))))),
inference(forward_demodulation,[],[f6030,f4551]) ).
fof(f6032,plain,
index_15 != s(s(s(s(s(s(s(index_33))))))),
inference(forward_demodulation,[],[f6031,f172]) ).
fof(f6033,plain,
index_15 != s(s(s(s(s(s(s(index_36))))))),
inference(forward_demodulation,[],[f6032,f664]) ).
fof(f6034,plain,
index_15 != s(s(s(s(s(s(index_39)))))),
inference(forward_demodulation,[],[f6033,f174]) ).
fof(f6035,plain,
index_15 != s(s(s(s(s(s(index_42)))))),
inference(forward_demodulation,[],[f6034,f663]) ).
fof(f6036,plain,
index_15 != s(s(s(s(s(index_45))))),
inference(forward_demodulation,[],[f6035,f176]) ).
fof(f6037,plain,
index_15 != s(s(s(s(s(index_51))))),
inference(forward_demodulation,[],[f6036,f4557]) ).
fof(f6038,plain,
index_15 != s(s(s(s(index_54)))),
inference(forward_demodulation,[],[f6037,f180]) ).
fof(f6039,plain,
index_15 != s(s(s(s(index_57)))),
inference(forward_demodulation,[],[f6038,f661]) ).
fof(f6040,plain,
index_15 != s(s(s(index_60))),
inference(forward_demodulation,[],[f6039,f183]) ).
fof(f6041,plain,
index_15 != s(s(s(index_63))),
inference(forward_demodulation,[],[f6040,f660]) ).
fof(f6042,plain,
index_15 != s(s(index_66)),
inference(forward_demodulation,[],[f6041,f185]) ).
fof(f6043,plain,
index_15 != s(s(index_72)),
inference(forward_demodulation,[],[f6042,f4563]) ).
fof(f6044,plain,
index_15 != s(index_75),
inference(forward_demodulation,[],[f6043,f189]) ).
fof(f6045,plain,
index_15 != s(index_84),
inference(forward_demodulation,[],[f6044,f659]) ).
fof(f6047,plain,
index_15 != index_87,
inference(superposition,[],[f6045,f193]) ).
fof(f6048,plain,
index_15 != index_90,
inference(superposition,[],[f6047,f657]) ).
fof(f6503,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_21)))))))))),
inference(forward_demodulation,[],[f1111,f669]) ).
fof(f6504,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_24))))))))),
inference(forward_demodulation,[],[f6503,f167]) ).
fof(f6505,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_30))))))))),
inference(forward_demodulation,[],[f6504,f4551]) ).
fof(f6506,plain,
index_15 != s(s(s(s(s(s(s(s(index_33)))))))),
inference(forward_demodulation,[],[f6505,f172]) ).
fof(f6507,plain,
index_15 != s(s(s(s(s(s(s(s(index_36)))))))),
inference(forward_demodulation,[],[f6506,f664]) ).
fof(f6508,plain,
index_15 != s(s(s(s(s(s(s(index_39))))))),
inference(forward_demodulation,[],[f6507,f174]) ).
fof(f6509,plain,
index_15 != s(s(s(s(s(s(s(index_42))))))),
inference(forward_demodulation,[],[f6508,f663]) ).
fof(f6510,plain,
index_15 != s(s(s(s(s(s(index_45)))))),
inference(forward_demodulation,[],[f6509,f176]) ).
fof(f6511,plain,
index_15 != s(s(s(s(s(s(index_51)))))),
inference(forward_demodulation,[],[f6510,f4557]) ).
fof(f6512,plain,
index_15 != s(s(s(s(s(index_54))))),
inference(forward_demodulation,[],[f6511,f180]) ).
fof(f6513,plain,
index_15 != s(s(s(s(s(index_57))))),
inference(forward_demodulation,[],[f6512,f661]) ).
fof(f6514,plain,
index_15 != s(s(s(s(index_60)))),
inference(forward_demodulation,[],[f6513,f183]) ).
fof(f6515,plain,
index_15 != s(s(s(s(index_63)))),
inference(forward_demodulation,[],[f6514,f660]) ).
fof(f6516,plain,
index_15 != s(s(s(index_66))),
inference(forward_demodulation,[],[f6515,f185]) ).
fof(f6517,plain,
index_15 != s(s(s(index_72))),
inference(forward_demodulation,[],[f6516,f4563]) ).
fof(f6518,plain,
index_15 != s(s(index_75)),
inference(forward_demodulation,[],[f6517,f189]) ).
fof(f6519,plain,
index_15 != s(s(index_84)),
inference(forward_demodulation,[],[f6518,f659]) ).
fof(f6520,plain,
index_15 != s(index_87),
inference(forward_demodulation,[],[f6519,f193]) ).
fof(f6521,plain,
index_15 != s(index_90),
inference(forward_demodulation,[],[f6520,f657]) ).
fof(f6522,plain,
index_15 != index_93,
inference(superposition,[],[f6521,f196]) ).
fof(f6523,plain,
index_99 != index_15,
inference(forward_demodulation,[],[f6522,f4569]) ).
fof(f7012,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))),
inference(forward_demodulation,[],[f1169,f669]) ).
fof(f7013,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_24)))))))))),
inference(forward_demodulation,[],[f7012,f167]) ).
fof(f7014,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_30)))))))))),
inference(forward_demodulation,[],[f7013,f4551]) ).
fof(f7015,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_33))))))))),
inference(forward_demodulation,[],[f7014,f172]) ).
fof(f7016,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_36))))))))),
inference(forward_demodulation,[],[f7015,f664]) ).
fof(f7017,plain,
index_15 != s(s(s(s(s(s(s(s(index_39)))))))),
inference(forward_demodulation,[],[f7016,f174]) ).
fof(f7018,plain,
index_15 != s(s(s(s(s(s(s(s(index_42)))))))),
inference(forward_demodulation,[],[f7017,f663]) ).
fof(f7019,plain,
index_15 != s(s(s(s(s(s(s(index_45))))))),
inference(forward_demodulation,[],[f7018,f176]) ).
fof(f7020,plain,
index_15 != s(s(s(s(s(s(s(index_51))))))),
inference(forward_demodulation,[],[f7019,f4557]) ).
fof(f7021,plain,
index_15 != s(s(s(s(s(s(index_54)))))),
inference(forward_demodulation,[],[f7020,f180]) ).
fof(f7022,plain,
index_15 != s(s(s(s(s(s(index_57)))))),
inference(forward_demodulation,[],[f7021,f661]) ).
fof(f7023,plain,
index_15 != s(s(s(s(s(index_60))))),
inference(forward_demodulation,[],[f7022,f183]) ).
fof(f7024,plain,
index_15 != s(s(s(s(s(index_63))))),
inference(forward_demodulation,[],[f7023,f660]) ).
fof(f7025,plain,
index_15 != s(s(s(s(index_66)))),
inference(forward_demodulation,[],[f7024,f185]) ).
fof(f7026,plain,
index_15 != s(s(s(s(index_72)))),
inference(forward_demodulation,[],[f7025,f4563]) ).
fof(f7027,plain,
index_15 != s(s(s(index_75))),
inference(forward_demodulation,[],[f7026,f189]) ).
fof(f7028,plain,
index_15 != s(s(s(index_84))),
inference(forward_demodulation,[],[f7027,f659]) ).
fof(f7029,plain,
index_15 != s(s(index_87)),
inference(forward_demodulation,[],[f7028,f193]) ).
fof(f7030,plain,
index_15 != s(s(index_90)),
inference(forward_demodulation,[],[f7029,f657]) ).
fof(f7031,plain,
index_15 != s(index_93),
inference(forward_demodulation,[],[f7030,f196]) ).
fof(f7032,plain,
index_15 != s(index_99),
inference(forward_demodulation,[],[f7031,f4569]) ).
fof(f7033,plain,
index_15 != index_102,
inference(superposition,[],[f7032,f119]) ).
fof(f7034,plain,
index_105 != index_15,
inference(forward_demodulation,[],[f7033,f676]) ).
fof(f7559,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))),
inference(forward_demodulation,[],[f1227,f669]) ).
fof(f7560,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))),
inference(forward_demodulation,[],[f7559,f167]) ).
fof(f7561,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))),
inference(forward_demodulation,[],[f7560,f4551]) ).
fof(f7562,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_33)))))))))),
inference(forward_demodulation,[],[f7561,f172]) ).
fof(f7563,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_36)))))))))),
inference(forward_demodulation,[],[f7562,f664]) ).
fof(f7564,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_39))))))))),
inference(forward_demodulation,[],[f7563,f174]) ).
fof(f7565,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_42))))))))),
inference(forward_demodulation,[],[f7564,f663]) ).
fof(f7566,plain,
index_15 != s(s(s(s(s(s(s(s(index_45)))))))),
inference(forward_demodulation,[],[f7565,f176]) ).
fof(f7567,plain,
index_15 != s(s(s(s(s(s(s(s(index_51)))))))),
inference(forward_demodulation,[],[f7566,f4557]) ).
fof(f7568,plain,
index_15 != s(s(s(s(s(s(s(index_54))))))),
inference(forward_demodulation,[],[f7567,f180]) ).
fof(f7569,plain,
index_15 != s(s(s(s(s(s(s(index_57))))))),
inference(forward_demodulation,[],[f7568,f661]) ).
fof(f7570,plain,
index_15 != s(s(s(s(s(s(index_60)))))),
inference(forward_demodulation,[],[f7569,f183]) ).
fof(f7571,plain,
index_15 != s(s(s(s(s(s(index_63)))))),
inference(forward_demodulation,[],[f7570,f660]) ).
fof(f7572,plain,
index_15 != s(s(s(s(s(index_66))))),
inference(forward_demodulation,[],[f7571,f185]) ).
fof(f7573,plain,
index_15 != s(s(s(s(s(index_72))))),
inference(forward_demodulation,[],[f7572,f4563]) ).
fof(f7574,plain,
index_15 != s(s(s(s(index_75)))),
inference(forward_demodulation,[],[f7573,f189]) ).
fof(f7575,plain,
index_15 != s(s(s(s(index_84)))),
inference(forward_demodulation,[],[f7574,f659]) ).
fof(f7576,plain,
index_15 != s(s(s(index_87))),
inference(forward_demodulation,[],[f7575,f193]) ).
fof(f7577,plain,
index_15 != s(s(s(index_90))),
inference(forward_demodulation,[],[f7576,f657]) ).
fof(f7578,plain,
index_15 != s(s(index_93)),
inference(forward_demodulation,[],[f7577,f196]) ).
fof(f7579,plain,
index_15 != s(s(index_99)),
inference(forward_demodulation,[],[f7578,f4569]) ).
fof(f7580,plain,
index_15 != s(index_102),
inference(forward_demodulation,[],[f7579,f119]) ).
fof(f7581,plain,
index_15 != s(index_105),
inference(forward_demodulation,[],[f7580,f676]) ).
fof(f7582,plain,
index_15 != index_108,
inference(superposition,[],[f7581,f121]) ).
fof(f7583,plain,
index_111 != index_15,
inference(forward_demodulation,[],[f7582,f675]) ).
fof(f8145,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))),
inference(forward_demodulation,[],[f1285,f669]) ).
fof(f8146,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))),
inference(forward_demodulation,[],[f8145,f167]) ).
fof(f8147,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))),
inference(forward_demodulation,[],[f8146,f4551]) ).
fof(f8148,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_33))))))))))),
inference(forward_demodulation,[],[f8147,f172]) ).
fof(f8149,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))),
inference(forward_demodulation,[],[f8148,f664]) ).
fof(f8150,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_39)))))))))),
inference(forward_demodulation,[],[f8149,f174]) ).
fof(f8151,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_42)))))))))),
inference(forward_demodulation,[],[f8150,f663]) ).
fof(f8152,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_45))))))))),
inference(forward_demodulation,[],[f8151,f176]) ).
fof(f8153,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_51))))))))),
inference(forward_demodulation,[],[f8152,f4557]) ).
fof(f8154,plain,
index_15 != s(s(s(s(s(s(s(s(index_54)))))))),
inference(forward_demodulation,[],[f8153,f180]) ).
fof(f8155,plain,
index_15 != s(s(s(s(s(s(s(s(index_57)))))))),
inference(forward_demodulation,[],[f8154,f661]) ).
fof(f8156,plain,
index_15 != s(s(s(s(s(s(s(index_60))))))),
inference(forward_demodulation,[],[f8155,f183]) ).
fof(f8157,plain,
index_15 != s(s(s(s(s(s(s(index_63))))))),
inference(forward_demodulation,[],[f8156,f660]) ).
fof(f8158,plain,
index_15 != s(s(s(s(s(s(index_66)))))),
inference(forward_demodulation,[],[f8157,f185]) ).
fof(f8159,plain,
index_15 != s(s(s(s(s(s(index_72)))))),
inference(forward_demodulation,[],[f8158,f4563]) ).
fof(f8160,plain,
index_15 != s(s(s(s(s(index_75))))),
inference(forward_demodulation,[],[f8159,f189]) ).
fof(f8161,plain,
index_15 != s(s(s(s(s(index_84))))),
inference(forward_demodulation,[],[f8160,f659]) ).
fof(f8162,plain,
index_15 != s(s(s(s(index_87)))),
inference(forward_demodulation,[],[f8161,f193]) ).
fof(f8163,plain,
index_15 != s(s(s(s(index_90)))),
inference(forward_demodulation,[],[f8162,f657]) ).
fof(f8164,plain,
index_15 != s(s(s(index_93))),
inference(forward_demodulation,[],[f8163,f196]) ).
fof(f8165,plain,
index_15 != s(s(s(index_99))),
inference(forward_demodulation,[],[f8164,f4569]) ).
fof(f8166,plain,
index_15 != s(s(index_102)),
inference(forward_demodulation,[],[f8165,f119]) ).
fof(f8167,plain,
index_15 != s(s(index_105)),
inference(forward_demodulation,[],[f8166,f676]) ).
fof(f8168,plain,
index_15 != s(index_108),
inference(forward_demodulation,[],[f8167,f121]) ).
fof(f8169,plain,
index_15 != s(index_111),
inference(forward_demodulation,[],[f8168,f675]) ).
fof(f8170,plain,
index_15 != index_114,
inference(superposition,[],[f8169,f123]) ).
fof(f8171,plain,
index_120 != index_15,
inference(forward_demodulation,[],[f8170,f4346]) ).
fof(f8761,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))),
inference(forward_demodulation,[],[f1343,f669]) ).
fof(f8762,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))),
inference(forward_demodulation,[],[f8761,f167]) ).
fof(f8763,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))),
inference(forward_demodulation,[],[f8762,f4551]) ).
fof(f8764,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_33)))))))))))),
inference(forward_demodulation,[],[f8763,f172]) ).
fof(f8765,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))),
inference(forward_demodulation,[],[f8764,f664]) ).
fof(f8766,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))),
inference(forward_demodulation,[],[f8765,f174]) ).
fof(f8767,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))),
inference(forward_demodulation,[],[f8766,f663]) ).
fof(f8768,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_45)))))))))),
inference(forward_demodulation,[],[f8767,f176]) ).
fof(f8769,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_51)))))))))),
inference(forward_demodulation,[],[f8768,f4557]) ).
fof(f8770,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_54))))))))),
inference(forward_demodulation,[],[f8769,f180]) ).
fof(f8771,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_57))))))))),
inference(forward_demodulation,[],[f8770,f661]) ).
fof(f8772,plain,
index_15 != s(s(s(s(s(s(s(s(index_60)))))))),
inference(forward_demodulation,[],[f8771,f183]) ).
fof(f8773,plain,
index_15 != s(s(s(s(s(s(s(s(index_63)))))))),
inference(forward_demodulation,[],[f8772,f660]) ).
fof(f8774,plain,
index_15 != s(s(s(s(s(s(s(index_66))))))),
inference(forward_demodulation,[],[f8773,f185]) ).
fof(f8775,plain,
index_15 != s(s(s(s(s(s(s(index_72))))))),
inference(forward_demodulation,[],[f8774,f4563]) ).
fof(f8776,plain,
index_15 != s(s(s(s(s(s(index_75)))))),
inference(forward_demodulation,[],[f8775,f189]) ).
fof(f8777,plain,
index_15 != s(s(s(s(s(s(index_84)))))),
inference(forward_demodulation,[],[f8776,f659]) ).
fof(f8778,plain,
index_15 != s(s(s(s(s(index_87))))),
inference(forward_demodulation,[],[f8777,f193]) ).
fof(f8779,plain,
index_15 != s(s(s(s(s(index_90))))),
inference(forward_demodulation,[],[f8778,f657]) ).
fof(f8780,plain,
index_15 != s(s(s(s(index_93)))),
inference(forward_demodulation,[],[f8779,f196]) ).
fof(f8781,plain,
index_15 != s(s(s(s(index_99)))),
inference(forward_demodulation,[],[f8780,f4569]) ).
fof(f8782,plain,
index_15 != s(s(s(index_102))),
inference(forward_demodulation,[],[f8781,f119]) ).
fof(f8783,plain,
index_15 != s(s(s(index_105))),
inference(forward_demodulation,[],[f8782,f676]) ).
fof(f8784,plain,
index_15 != s(s(index_108)),
inference(forward_demodulation,[],[f8783,f121]) ).
fof(f8785,plain,
index_15 != s(s(index_111)),
inference(forward_demodulation,[],[f8784,f675]) ).
fof(f8786,plain,
index_15 != s(index_114),
inference(forward_demodulation,[],[f8785,f123]) ).
fof(f8787,plain,
index_15 != s(index_120),
inference(forward_demodulation,[],[f8786,f4346]) ).
fof(f8788,plain,
index_15 != index_123,
inference(superposition,[],[f8787,f128]) ).
fof(f8789,plain,
index_126 != index_15,
inference(forward_demodulation,[],[f8788,f673]) ).
fof(f9403,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))),
inference(forward_demodulation,[],[f1401,f669]) ).
fof(f9404,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))),
inference(forward_demodulation,[],[f9403,f167]) ).
fof(f9405,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))),
inference(forward_demodulation,[],[f9404,f4551]) ).
fof(f9406,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_33))))))))))))),
inference(forward_demodulation,[],[f9405,f172]) ).
fof(f9407,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))),
inference(forward_demodulation,[],[f9406,f664]) ).
fof(f9408,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))),
inference(forward_demodulation,[],[f9407,f174]) ).
fof(f9409,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))),
inference(forward_demodulation,[],[f9408,f663]) ).
fof(f9410,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))),
inference(forward_demodulation,[],[f9409,f176]) ).
fof(f9411,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))),
inference(forward_demodulation,[],[f9410,f4557]) ).
fof(f9412,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_54)))))))))),
inference(forward_demodulation,[],[f9411,f180]) ).
fof(f9413,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_57)))))))))),
inference(forward_demodulation,[],[f9412,f661]) ).
fof(f9414,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_60))))))))),
inference(forward_demodulation,[],[f9413,f183]) ).
fof(f9415,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_63))))))))),
inference(forward_demodulation,[],[f9414,f660]) ).
fof(f9416,plain,
index_15 != s(s(s(s(s(s(s(s(index_66)))))))),
inference(forward_demodulation,[],[f9415,f185]) ).
fof(f9417,plain,
index_15 != s(s(s(s(s(s(s(s(index_72)))))))),
inference(forward_demodulation,[],[f9416,f4563]) ).
fof(f9418,plain,
index_15 != s(s(s(s(s(s(s(index_75))))))),
inference(forward_demodulation,[],[f9417,f189]) ).
fof(f9419,plain,
index_15 != s(s(s(s(s(s(s(index_84))))))),
inference(forward_demodulation,[],[f9418,f659]) ).
fof(f9420,plain,
index_15 != s(s(s(s(s(s(index_87)))))),
inference(forward_demodulation,[],[f9419,f193]) ).
fof(f9421,plain,
index_15 != s(s(s(s(s(s(index_90)))))),
inference(forward_demodulation,[],[f9420,f657]) ).
fof(f9422,plain,
index_15 != s(s(s(s(s(index_93))))),
inference(forward_demodulation,[],[f9421,f196]) ).
fof(f9423,plain,
index_15 != s(s(s(s(s(index_99))))),
inference(forward_demodulation,[],[f9422,f4569]) ).
fof(f9424,plain,
index_15 != s(s(s(s(index_102)))),
inference(forward_demodulation,[],[f9423,f119]) ).
fof(f9425,plain,
index_15 != s(s(s(s(index_105)))),
inference(forward_demodulation,[],[f9424,f676]) ).
fof(f9426,plain,
index_15 != s(s(s(index_108))),
inference(forward_demodulation,[],[f9425,f121]) ).
fof(f9427,plain,
index_15 != s(s(s(index_111))),
inference(forward_demodulation,[],[f9426,f675]) ).
fof(f9428,plain,
index_15 != s(s(index_114)),
inference(forward_demodulation,[],[f9427,f123]) ).
fof(f9429,plain,
index_15 != s(s(index_120)),
inference(forward_demodulation,[],[f9428,f4346]) ).
fof(f9430,plain,
index_15 != s(index_123),
inference(forward_demodulation,[],[f9429,f128]) ).
fof(f9431,plain,
index_15 != s(index_126),
inference(forward_demodulation,[],[f9430,f673]) ).
fof(f9432,plain,
index_15 != index_129,
inference(superposition,[],[f9431,f130]) ).
fof(f9433,plain,
index_132 != index_15,
inference(forward_demodulation,[],[f9432,f672]) ).
fof(f10083,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))),
inference(forward_demodulation,[],[f1459,f669]) ).
fof(f10084,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))),
inference(forward_demodulation,[],[f10083,f167]) ).
fof(f10085,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))),
inference(forward_demodulation,[],[f10084,f4551]) ).
fof(f10086,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_33)))))))))))))),
inference(forward_demodulation,[],[f10085,f172]) ).
fof(f10087,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))),
inference(forward_demodulation,[],[f10086,f664]) ).
fof(f10088,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))),
inference(forward_demodulation,[],[f10087,f174]) ).
fof(f10089,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))),
inference(forward_demodulation,[],[f10088,f663]) ).
fof(f10090,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))),
inference(forward_demodulation,[],[f10089,f176]) ).
fof(f10091,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))),
inference(forward_demodulation,[],[f10090,f4557]) ).
fof(f10092,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))),
inference(forward_demodulation,[],[f10091,f180]) ).
fof(f10093,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))),
inference(forward_demodulation,[],[f10092,f661]) ).
fof(f10094,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_60)))))))))),
inference(forward_demodulation,[],[f10093,f183]) ).
fof(f10095,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_63)))))))))),
inference(forward_demodulation,[],[f10094,f660]) ).
fof(f10096,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_66))))))))),
inference(forward_demodulation,[],[f10095,f185]) ).
fof(f10097,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_72))))))))),
inference(forward_demodulation,[],[f10096,f4563]) ).
fof(f10098,plain,
index_15 != s(s(s(s(s(s(s(s(index_75)))))))),
inference(forward_demodulation,[],[f10097,f189]) ).
fof(f10099,plain,
index_15 != s(s(s(s(s(s(s(s(index_84)))))))),
inference(forward_demodulation,[],[f10098,f659]) ).
fof(f10100,plain,
index_15 != s(s(s(s(s(s(s(index_87))))))),
inference(forward_demodulation,[],[f10099,f193]) ).
fof(f10101,plain,
index_15 != s(s(s(s(s(s(s(index_90))))))),
inference(forward_demodulation,[],[f10100,f657]) ).
fof(f10102,plain,
index_15 != s(s(s(s(s(s(index_93)))))),
inference(forward_demodulation,[],[f10101,f196]) ).
fof(f10103,plain,
index_15 != s(s(s(s(s(s(index_99)))))),
inference(forward_demodulation,[],[f10102,f4569]) ).
fof(f10104,plain,
index_15 != s(s(s(s(s(index_102))))),
inference(forward_demodulation,[],[f10103,f119]) ).
fof(f10105,plain,
index_15 != s(s(s(s(s(index_105))))),
inference(forward_demodulation,[],[f10104,f676]) ).
fof(f10106,plain,
index_15 != s(s(s(s(index_108)))),
inference(forward_demodulation,[],[f10105,f121]) ).
fof(f10107,plain,
index_15 != s(s(s(s(index_111)))),
inference(forward_demodulation,[],[f10106,f675]) ).
fof(f10108,plain,
index_15 != s(s(s(index_114))),
inference(forward_demodulation,[],[f10107,f123]) ).
fof(f10109,plain,
index_15 != s(s(s(index_120))),
inference(forward_demodulation,[],[f10108,f4346]) ).
fof(f10110,plain,
index_15 != s(s(index_123)),
inference(forward_demodulation,[],[f10109,f128]) ).
fof(f10111,plain,
index_15 != s(s(index_126)),
inference(forward_demodulation,[],[f10110,f673]) ).
fof(f10112,plain,
index_15 != s(index_129),
inference(forward_demodulation,[],[f10111,f130]) ).
fof(f10113,plain,
index_15 != s(index_132),
inference(forward_demodulation,[],[f10112,f672]) ).
fof(f10115,plain,
index_15 != index_135,
inference(superposition,[],[f10113,f132]) ).
fof(f10116,plain,
index_141 != index_15,
inference(forward_demodulation,[],[f10115,f4352]) ).
fof(f10818,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))),
inference(forward_demodulation,[],[f1517,f669]) ).
fof(f10819,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))),
inference(forward_demodulation,[],[f10818,f167]) ).
fof(f10820,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))))),
inference(forward_demodulation,[],[f10819,f4551]) ).
fof(f10821,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_33))))))))))))))),
inference(forward_demodulation,[],[f10820,f172]) ).
fof(f10822,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))))),
inference(forward_demodulation,[],[f10821,f664]) ).
fof(f10823,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39)))))))))))))),
inference(forward_demodulation,[],[f10822,f174]) ).
fof(f10824,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))),
inference(forward_demodulation,[],[f10823,f663]) ).
fof(f10825,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))),
inference(forward_demodulation,[],[f10824,f176]) ).
fof(f10826,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))),
inference(forward_demodulation,[],[f10825,f4557]) ).
fof(f10827,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_54)))))))))))),
inference(forward_demodulation,[],[f10826,f180]) ).
fof(f10828,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_57)))))))))))),
inference(forward_demodulation,[],[f10827,f661]) ).
fof(f10829,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))),
inference(forward_demodulation,[],[f10828,f183]) ).
fof(f10830,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_63))))))))))),
inference(forward_demodulation,[],[f10829,f660]) ).
fof(f10831,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_66)))))))))),
inference(forward_demodulation,[],[f10830,f185]) ).
fof(f10832,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_72)))))))))),
inference(forward_demodulation,[],[f10831,f4563]) ).
fof(f10833,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_75))))))))),
inference(forward_demodulation,[],[f10832,f189]) ).
fof(f10834,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_84))))))))),
inference(forward_demodulation,[],[f10833,f659]) ).
fof(f10835,plain,
index_15 != s(s(s(s(s(s(s(s(index_87)))))))),
inference(forward_demodulation,[],[f10834,f193]) ).
fof(f10836,plain,
index_15 != s(s(s(s(s(s(s(s(index_90)))))))),
inference(forward_demodulation,[],[f10835,f657]) ).
fof(f10837,plain,
index_15 != s(s(s(s(s(s(s(index_93))))))),
inference(forward_demodulation,[],[f10836,f196]) ).
fof(f10838,plain,
index_15 != s(s(s(s(s(s(s(index_99))))))),
inference(forward_demodulation,[],[f10837,f4569]) ).
fof(f10839,plain,
index_15 != s(s(s(s(s(s(index_102)))))),
inference(forward_demodulation,[],[f10838,f119]) ).
fof(f10840,plain,
index_15 != s(s(s(s(s(s(index_105)))))),
inference(forward_demodulation,[],[f10839,f676]) ).
fof(f10841,plain,
index_15 != s(s(s(s(s(index_108))))),
inference(forward_demodulation,[],[f10840,f121]) ).
fof(f10842,plain,
index_15 != s(s(s(s(s(index_111))))),
inference(forward_demodulation,[],[f10841,f675]) ).
fof(f10843,plain,
index_15 != s(s(s(s(index_114)))),
inference(forward_demodulation,[],[f10842,f123]) ).
fof(f10844,plain,
index_15 != s(s(s(s(index_120)))),
inference(forward_demodulation,[],[f10843,f4346]) ).
fof(f10845,plain,
index_15 != s(s(s(index_123))),
inference(forward_demodulation,[],[f10844,f128]) ).
fof(f10846,plain,
index_15 != s(s(s(index_126))),
inference(forward_demodulation,[],[f10845,f673]) ).
fof(f10847,plain,
index_15 != s(s(index_129)),
inference(forward_demodulation,[],[f10846,f130]) ).
fof(f10848,plain,
index_15 != s(s(index_132)),
inference(forward_demodulation,[],[f10847,f672]) ).
fof(f10849,plain,
index_15 != s(index_135),
inference(forward_demodulation,[],[f10848,f132]) ).
fof(f10850,plain,
index_15 != s(index_141),
inference(forward_demodulation,[],[f10849,f4352]) ).
fof(f10851,plain,
index_15 != index_144,
inference(superposition,[],[f10850,f136]) ).
fof(f10852,plain,
index_147 != index_15,
inference(forward_demodulation,[],[f10851,f671]) ).
fof(f11606,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))))),
inference(forward_demodulation,[],[f1581,f669]) ).
fof(f11607,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))))),
inference(forward_demodulation,[],[f11606,f167]) ).
fof(f11608,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))))),
inference(forward_demodulation,[],[f11607,f4551]) ).
fof(f11609,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_33)))))))))))))))),
inference(forward_demodulation,[],[f11608,f172]) ).
fof(f11610,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))))),
inference(forward_demodulation,[],[f11609,f664]) ).
fof(f11611,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_39))))))))))))))),
inference(forward_demodulation,[],[f11610,f174]) ).
fof(f11612,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))),
inference(forward_demodulation,[],[f11611,f663]) ).
fof(f11613,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))),
inference(forward_demodulation,[],[f11612,f176]) ).
fof(f11614,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))),
inference(forward_demodulation,[],[f11613,f4557]) ).
fof(f11615,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_54))))))))))))),
inference(forward_demodulation,[],[f11614,f180]) ).
fof(f11616,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))))),
inference(forward_demodulation,[],[f11615,f661]) ).
fof(f11617,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_60)))))))))))),
inference(forward_demodulation,[],[f11616,f183]) ).
fof(f11618,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(s(index_63)))))))))))),
inference(forward_demodulation,[],[f11617,f660]) ).
fof(f11619,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))),
inference(forward_demodulation,[],[f11618,f185]) ).
fof(f11620,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(s(index_72))))))))))),
inference(forward_demodulation,[],[f11619,f4563]) ).
fof(f11621,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_75)))))))))),
inference(forward_demodulation,[],[f11620,f189]) ).
fof(f11622,plain,
index_15 != s(s(s(s(s(s(s(s(s(s(index_84)))))))))),
inference(forward_demodulation,[],[f11621,f659]) ).
fof(f11623,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_87))))))))),
inference(forward_demodulation,[],[f11622,f193]) ).
fof(f11624,plain,
index_15 != s(s(s(s(s(s(s(s(s(index_90))))))))),
inference(forward_demodulation,[],[f11623,f657]) ).
fof(f11625,plain,
index_15 != s(s(s(s(s(s(s(s(index_93)))))))),
inference(forward_demodulation,[],[f11624,f196]) ).
fof(f11626,plain,
index_15 != s(s(s(s(s(s(s(s(index_99)))))))),
inference(forward_demodulation,[],[f11625,f4569]) ).
fof(f11627,plain,
index_15 != s(s(s(s(s(s(s(index_102))))))),
inference(forward_demodulation,[],[f11626,f119]) ).
fof(f11628,plain,
index_15 != s(s(s(s(s(s(s(index_105))))))),
inference(forward_demodulation,[],[f11627,f676]) ).
fof(f11629,plain,
index_15 != s(s(s(s(s(s(index_108)))))),
inference(forward_demodulation,[],[f11628,f121]) ).
fof(f11630,plain,
index_15 != s(s(s(s(s(s(index_111)))))),
inference(forward_demodulation,[],[f11629,f675]) ).
fof(f11631,plain,
index_15 != s(s(s(s(s(index_114))))),
inference(forward_demodulation,[],[f11630,f123]) ).
fof(f11632,plain,
index_15 != s(s(s(s(s(index_120))))),
inference(forward_demodulation,[],[f11631,f4346]) ).
fof(f11633,plain,
index_15 != s(s(s(s(index_123)))),
inference(forward_demodulation,[],[f11632,f128]) ).
fof(f11634,plain,
index_15 != s(s(s(s(index_126)))),
inference(forward_demodulation,[],[f11633,f673]) ).
fof(f11635,plain,
index_15 != s(s(s(index_129))),
inference(forward_demodulation,[],[f11634,f130]) ).
fof(f11636,plain,
index_15 != s(s(s(index_132))),
inference(forward_demodulation,[],[f11635,f672]) ).
fof(f11637,plain,
index_15 != s(s(index_135)),
inference(forward_demodulation,[],[f11636,f132]) ).
fof(f11638,plain,
index_15 != s(s(index_141)),
inference(forward_demodulation,[],[f11637,f4352]) ).
fof(f11639,plain,
index_15 != s(index_144),
inference(forward_demodulation,[],[f11638,f136]) ).
fof(f11640,plain,
index_15 != s(index_147),
inference(forward_demodulation,[],[f11639,f671]) ).
fof(f11641,plain,
index_15 != index_150,
inference(superposition,[],[f11640,f139]) ).
fof(f11642,plain,
index_15 != index_162,
inference(superposition,[],[f11641,f670]) ).
fof(f13531,plain,
index_15 != index_33,
inference(superposition,[],[f4855,f172]) ).
fof(f13532,plain,
index_15 != index_36,
inference(superposition,[],[f13531,f664]) ).
fof(f13692,plain,
index_15 != index_39,
inference(superposition,[],[f4891,f174]) ).
fof(f13804,plain,
index_15 != index_42,
inference(superposition,[],[f13692,f663]) ).
fof(f14328,plain,
index_15 != index_45,
inference(superposition,[],[f4916,f176]) ).
fof(f14329,plain,
index_15 != index_51,
inference(superposition,[],[f14328,f4557]) ).
fof(f14333,plain,
index_15 != s(index_51),
inference(forward_demodulation,[],[f4926,f4557]) ).
fof(f17712,plain,
index_15 != index_54,
inference(superposition,[],[f14333,f180]) ).
fof(f17713,plain,
index_15 != index_57,
inference(superposition,[],[f17712,f661]) ).
fof(f18178,plain,
earray_100 = earray_104,
inference(superposition,[],[f4664,f304]) ).
fof(f18231,plain,
earray_106 = store(earray_100,index_105,e22),
inference(superposition,[],[f59,f18178]) ).
fof(f18377,plain,
earray_106 = earray_110,
inference(superposition,[],[f4755,f305]) ).
fof(f18465,plain,
earray_112 = store(earray_106,index_111,e23),
inference(superposition,[],[f61,f18377]) ).
fof(f18578,plain,
( earray_112 = select(queue_118,seq)
| head = seq ),
inference(superposition,[],[f970,f5020]) ).
fof(f18579,plain,
earray_112 = select(queue_118,seq),
inference(forward_subsumption_resolution,[],[f18578,f4]) ).
fof(f18582,plain,
earray_121 = earray_125,
inference(superposition,[],[f5123,f307]) ).
fof(f18584,plain,
earray_127 = store(earray_121,index_126,e25),
inference(superposition,[],[f65,f18582]) ).
fof(f18728,plain,
earray_127 = earray_131,
inference(superposition,[],[f5129,f308]) ).
fof(f18754,plain,
earray_133 = store(earray_127,index_132,e26),
inference(superposition,[],[f67,f18728]) ).
fof(f18879,plain,
( earray_133 = select(queue_139,seq)
| head = seq ),
inference(superposition,[],[f971,f5135]) ).
fof(f18880,plain,
earray_133 = select(queue_139,seq),
inference(forward_subsumption_resolution,[],[f18879,f4]) ).
fof(f18898,plain,
earray_142 = earray_146,
inference(superposition,[],[f5279,f311]) ).
fof(f18926,plain,
earray_148 = store(earray_142,index_147,e28),
inference(superposition,[],[f72,f18898]) ).
fof(f18945,plain,
earray_148 = earray_161,
inference(superposition,[],[f5285,f313]) ).
fof(f18958,plain,
earray_163 = earray_212,
inference(superposition,[],[f5295,f4363]) ).
fof(f18960,plain,
elem_214 = select(earray_163,index_213),
inference(superposition,[],[f117,f18958]) ).
fof(f19209,plain,
earray_16 = earray_20,
inference(superposition,[],[f5301,f320]) ).
fof(f19379,plain,
earray_22 = store(earray_16,index_21,e11),
inference(superposition,[],[f93,f19209]) ).
fof(f19838,plain,
( earray_22 = select(queue_28,seq)
| head = seq ),
inference(superposition,[],[f976,f5345]) ).
fof(f19839,plain,
earray_22 = select(queue_28,seq),
inference(forward_subsumption_resolution,[],[f19838,f4]) ).
fof(f19845,plain,
earray_31 = earray_35,
inference(superposition,[],[f5351,f324]) ).
fof(f19847,plain,
earray_37 = store(earray_31,index_36,e13),
inference(superposition,[],[f97,f19845]) ).
fof(f20044,plain,
earray_37 = earray_41,
inference(superposition,[],[f5357,f325]) ).
fof(f20046,plain,
earray_43 = store(earray_37,index_42,e14),
inference(superposition,[],[f100,f20044]) ).
fof(f20228,plain,
( earray_43 = select(queue_49,seq)
| head = seq ),
inference(superposition,[],[f977,f5363]) ).
fof(f20229,plain,
earray_43 = select(queue_49,seq),
inference(forward_subsumption_resolution,[],[f20228,f4]) ).
fof(f20344,plain,
earray_52 = earray_56,
inference(superposition,[],[f5375,f327]) ).
fof(f20364,plain,
earray_58 = store(earray_52,index_57,e16),
inference(superposition,[],[f104,f20344]) ).
fof(f20599,plain,
earray_58 = earray_62,
inference(superposition,[],[f5381,f328]) ).
fof(f20641,plain,
earray_64 = store(earray_58,index_63,e17),
inference(superposition,[],[f106,f20599]) ).
fof(f20685,plain,
( earray_64 = select(queue_70,seq)
| head = seq ),
inference(superposition,[],[f978,f5387]) ).
fof(f20686,plain,
earray_64 = select(queue_70,seq),
inference(forward_subsumption_resolution,[],[f20685,f4]) ).
fof(f20706,plain,
earray_73 = earray_83,
inference(superposition,[],[f5393,f332]) ).
fof(f20719,plain,
earray_85 = earray_89,
inference(superposition,[],[f5409,f333]) ).
fof(f20817,plain,
( earray_91 = select(queue_97,seq)
| head = seq ),
inference(superposition,[],[f979,f5418]) ).
fof(f20818,plain,
earray_91 = select(queue_97,seq),
inference(forward_subsumption_resolution,[],[f20817,f4]) ).
fof(f20820,plain,
earray_98 = earray_91,
inference(forward_demodulation,[],[f20818,f334]) ).
fof(f20874,plain,
! [X0] :
( select(earray_98,X0) = select(earray_89,X0)
| index_90 = X0 ),
inference(superposition,[],[f968,f20820]) ).
fof(f20877,plain,
! [X0] :
( select(earray_98,X0) = select(earray_85,X0)
| index_90 = X0 ),
inference(forward_demodulation,[],[f20874,f20719]) ).
fof(f22381,plain,
index_15 != s(s(index_51)),
inference(forward_demodulation,[],[f4924,f4557]) ).
fof(f22382,plain,
index_15 != s(index_54),
inference(forward_demodulation,[],[f22381,f180]) ).
fof(f22383,plain,
index_15 != s(index_57),
inference(forward_demodulation,[],[f22382,f661]) ).
fof(f22424,plain,
index_15 != index_60,
inference(superposition,[],[f22383,f183]) ).
fof(f22455,plain,
index_15 != index_63,
inference(superposition,[],[f22424,f660]) ).
fof(f22997,plain,
earray_112 = earray_119,
inference(superposition,[],[f18579,f306]) ).
fof(f23018,plain,
earray_121 = store(earray_112,index_120,e24),
inference(superposition,[],[f63,f22997]) ).
fof(f23115,plain,
earray_133 = earray_140,
inference(superposition,[],[f18880,f310]) ).
fof(f23147,plain,
earray_142 = store(earray_133,index_141,e27),
inference(superposition,[],[f70,f23115]) ).
fof(f23380,plain,
earray_22 = earray_29,
inference(superposition,[],[f19839,f323]) ).
fof(f23382,plain,
earray_31 = store(earray_22,index_30,e12),
inference(superposition,[],[f95,f23380]) ).
fof(f23395,plain,
earray_43 = earray_50,
inference(superposition,[],[f20229,f326]) ).
fof(f23451,plain,
earray_52 = store(earray_43,index_51,e15),
inference(superposition,[],[f102,f23395]) ).
fof(f23490,plain,
earray_64 = earray_71,
inference(superposition,[],[f20686,f329]) ).
fof(f23545,plain,
( elem_214 = select(earray_161,index_213)
| index_162 = index_213 ),
inference(superposition,[],[f18960,f950]) ).
fof(f23548,plain,
( elem_214 = select(earray_148,index_213)
| index_162 = index_213 ),
inference(forward_demodulation,[],[f23545,f18945]) ).
fof(f23550,definition,
( spl0_1
<=> index_162 = index_213 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f23552,plain,
( index_162 = index_213
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f23550]) ).
fof(f23554,definition,
( spl0_2
<=> elem_214 = select(earray_148,index_213) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f23556,plain,
( elem_214 = select(earray_148,index_213)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f23554]) ).
fof(f23558,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f23548,f23554,f23550]) ).
fof(f23670,definition,
( spl0_3
<=> index_147 = index_213 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f23671,plain,
( index_147 != index_213
| spl0_3 ),
inference(avatar_component_clause,[],[f23670]) ).
fof(f23672,plain,
( index_147 = index_213
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f23670]) ).
fof(f25637,plain,
index_15 != s(s(s(index_51))),
inference(forward_demodulation,[],[f4922,f4557]) ).
fof(f25638,plain,
index_15 != s(s(index_54)),
inference(forward_demodulation,[],[f25637,f180]) ).
fof(f25639,plain,
index_15 != s(s(index_57)),
inference(forward_demodulation,[],[f25638,f661]) ).
fof(f25640,plain,
index_15 != s(index_60),
inference(forward_demodulation,[],[f25639,f183]) ).
fof(f25641,plain,
index_15 != s(index_63),
inference(forward_demodulation,[],[f25640,f660]) ).
fof(f25642,plain,
index_15 != index_66,
inference(superposition,[],[f25641,f185]) ).
fof(f25793,plain,
index_15 != index_72,
inference(superposition,[],[f25642,f4563]) ).
fof(f26487,plain,
! [X0] :
( select(earray_100,X0) = select(earray_106,X0)
| index_105 = X0 ),
inference(superposition,[],[f2,f18231]) ).
fof(f26505,plain,
! [X0] :
( select(earray_106,X0) = select(earray_112,X0)
| index_111 = X0 ),
inference(superposition,[],[f2,f18465]) ).
fof(f26509,plain,
! [X0] :
( select(earray_121,X0) = select(earray_127,X0)
| index_126 = X0 ),
inference(superposition,[],[f2,f18584]) ).
fof(f26537,plain,
! [X0] :
( select(earray_127,X0) = select(earray_133,X0)
| index_132 = X0 ),
inference(superposition,[],[f2,f18754]) ).
fof(f26572,plain,
! [X0] :
( select(earray_16,X0) = select(earray_22,X0)
| index_21 = X0 ),
inference(superposition,[],[f2,f19379]) ).
fof(f26888,plain,
! [X0] :
( select(earray_31,X0) = select(earray_37,X0)
| index_36 = X0 ),
inference(superposition,[],[f2,f19847]) ).
fof(f26890,plain,
! [X0] :
( select(earray_37,X0) = select(earray_43,X0)
| index_42 = X0 ),
inference(superposition,[],[f2,f20046]) ).
fof(f26894,plain,
! [X0] :
( select(earray_52,X0) = select(earray_58,X0)
| index_57 = X0 ),
inference(superposition,[],[f2,f20364]) ).
fof(f26896,plain,
! [X0] :
( select(earray_58,X0) = select(earray_64,X0)
| index_63 = X0 ),
inference(superposition,[],[f2,f20641]) ).
fof(f27303,plain,
! [X0] :
( select(earray_112,X0) = select(earray_121,X0)
| index_120 = X0 ),
inference(superposition,[],[f2,f23018]) ).
fof(f27305,plain,
! [X0] :
( select(earray_133,X0) = select(earray_142,X0)
| index_141 = X0 ),
inference(superposition,[],[f2,f23147]) ).
fof(f27399,plain,
! [X0] :
( select(earray_22,X0) = select(earray_31,X0)
| index_30 = X0 ),
inference(superposition,[],[f2,f23382]) ).
fof(f27443,plain,
! [X0] :
( select(earray_43,X0) = select(earray_52,X0)
| index_51 = X0 ),
inference(superposition,[],[f2,f23451]) ).
fof(f28811,plain,
! [X0] :
( select(earray_98,X0) = select(earray_83,X0)
| index_84 = X0
| index_90 = X0 ),
inference(superposition,[],[f967,f20877]) ).
fof(f28812,plain,
! [X0] :
( select(earray_98,X0) = select(earray_73,X0)
| index_84 = X0
| index_90 = X0 ),
inference(forward_demodulation,[],[f28811,f20706]) ).
fof(f29740,plain,
( index_116 = select(queue_109,head)
| head = tail
| head = seq ),
inference(superposition,[],[f124,f5017]) ).
fof(f29741,plain,
( index_116 = select(queue_109,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f29740,f3]) ).
fof(f29743,plain,
index_116 = select(queue_109,head),
inference(forward_subsumption_resolution,[],[f29741,f4]) ).
fof(f29800,plain,
( index_116 = select(queue_103,head)
| head = tail
| head = seq ),
inference(superposition,[],[f4752,f29743]) ).
fof(f29801,plain,
( index_116 = select(queue_103,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f29800,f3]) ).
fof(f29803,plain,
index_116 = select(queue_103,head),
inference(forward_subsumption_resolution,[],[f29801,f4]) ).
fof(f30206,plain,
( index_137 = select(queue_130,head)
| head = tail
| head = seq ),
inference(superposition,[],[f133,f5132]) ).
fof(f30207,plain,
( index_137 = select(queue_130,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f30206,f3]) ).
fof(f30209,plain,
index_137 = select(queue_130,head),
inference(forward_subsumption_resolution,[],[f30207,f4]) ).
fof(f30226,plain,
( index_137 = select(queue_124,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5126,f30209]) ).
fof(f30227,plain,
( index_137 = select(queue_124,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f30226,f3]) ).
fof(f30229,plain,
index_137 = select(queue_124,head),
inference(forward_subsumption_resolution,[],[f30227,f4]) ).
fof(f30268,plain,
( index_137 = select(queue_118,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5120,f30229]) ).
fof(f30269,plain,
( index_137 = select(queue_118,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f30268,f3]) ).
fof(f30271,plain,
index_137 = select(queue_118,head),
inference(forward_subsumption_resolution,[],[f30269,f4]) ).
fof(f30273,plain,
index_117 = index_137,
inference(forward_demodulation,[],[f30271,f587]) ).
fof(f30275,plain,
index_138 = s(index_117),
inference(superposition,[],[f134,f30273]) ).
fof(f30924,plain,
( index_167 = select(queue_151,head)
| head = tail
| head = seq ),
inference(superposition,[],[f146,f5292]) ).
fof(f30925,plain,
( index_167 = select(queue_151,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f30924,f3]) ).
fof(f30927,plain,
index_167 = select(queue_151,head),
inference(forward_subsumption_resolution,[],[f30925,f4]) ).
fof(f30930,plain,
( index_167 = select(queue_145,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5282,f30927]) ).
fof(f30931,plain,
( index_167 = select(queue_145,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f30930,f3]) ).
fof(f30933,plain,
index_167 = select(queue_145,head),
inference(forward_subsumption_resolution,[],[f30931,f4]) ).
fof(f30990,plain,
( index_167 = select(queue_139,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5276,f30933]) ).
fof(f30991,plain,
( index_167 = select(queue_139,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f30990,f3]) ).
fof(f30993,plain,
index_167 = select(queue_139,head),
inference(forward_subsumption_resolution,[],[f30991,f4]) ).
fof(f30995,plain,
index_138 = index_167,
inference(forward_demodulation,[],[f30993,f588]) ).
fof(f31072,plain,
index_168 = s(index_138),
inference(superposition,[],[f147,f30995]) ).
fof(f31073,plain,
index_213 = s(index_138),
inference(forward_demodulation,[],[f31072,f677]) ).
fof(f31075,plain,
( index_147 = s(index_138)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f31073,f23672]) ).
fof(f32790,plain,
( index_188 = select(queue_181,head)
| head = tail
| head = seq ),
inference(superposition,[],[f155,f5316]) ).
fof(f32791,plain,
( index_188 = select(queue_181,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f32790,f3]) ).
fof(f32793,plain,
index_188 = select(queue_181,head),
inference(forward_subsumption_resolution,[],[f32791,f4]) ).
fof(f32801,plain,
( index_188 = select(queue_175,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5310,f32793]) ).
fof(f32802,plain,
( index_188 = select(queue_175,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f32801,f3]) ).
fof(f32804,plain,
index_188 = select(queue_175,head),
inference(forward_subsumption_resolution,[],[f32802,f4]) ).
fof(f32807,plain,
( index_188 = select(queue_160,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5304,f32804]) ).
fof(f32808,plain,
( index_188 = select(queue_160,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f32807,f3]) ).
fof(f32810,plain,
index_188 = select(queue_160,head),
inference(forward_subsumption_resolution,[],[f32808,f4]) ).
fof(f32812,plain,
index_159 = index_188,
inference(forward_demodulation,[],[f32810,f589]) ).
fof(f32819,plain,
index_189 = s(index_159),
inference(superposition,[],[f156,f32812]) ).
fof(f33867,plain,
( index_209 = select(queue_202,head)
| head = tail
| head = seq ),
inference(superposition,[],[f163,f5334]) ).
fof(f33868,plain,
( index_209 = select(queue_202,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f33867,f3]) ).
fof(f33870,plain,
index_209 = select(queue_202,head),
inference(forward_subsumption_resolution,[],[f33868,f4]) ).
fof(f33873,plain,
( index_209 = select(queue_196,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5328,f33870]) ).
fof(f33874,plain,
( index_209 = select(queue_196,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f33873,f3]) ).
fof(f33876,plain,
index_209 = select(queue_196,head),
inference(forward_subsumption_resolution,[],[f33874,f4]) ).
fof(f33909,plain,
( index_209 = select(queue_190,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5322,f33876]) ).
fof(f33910,plain,
( index_209 = select(queue_190,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f33909,f3]) ).
fof(f33912,plain,
index_209 = select(queue_190,head),
inference(forward_subsumption_resolution,[],[f33910,f4]) ).
fof(f33914,plain,
index_189 = index_209,
inference(forward_demodulation,[],[f33912,f591]) ).
fof(f34042,plain,
index_210 = s(index_189),
inference(superposition,[],[f165,f33914]) ).
fof(f35142,plain,
( index_210 = select(queue_13,head)
| head = seq
| head = tail ),
inference(superposition,[],[f592,f5339]) ).
fof(f35143,plain,
( index_210 = select(queue_13,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f35142,f4]) ).
fof(f35145,plain,
index_210 = select(queue_13,head),
inference(forward_subsumption_resolution,[],[f35143,f3]) ).
fof(f35180,plain,
( index_26 = select(queue_19,head)
| head = tail
| head = seq ),
inference(superposition,[],[f168,f5342]) ).
fof(f35181,plain,
( index_26 = select(queue_19,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f35180,f3]) ).
fof(f35183,plain,
index_26 = select(queue_19,head),
inference(forward_subsumption_resolution,[],[f35181,f4]) ).
fof(f35186,plain,
( index_26 = select(queue_13,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5298,f35183]) ).
fof(f35187,plain,
( index_26 = select(queue_13,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f35186,f3]) ).
fof(f35189,plain,
index_26 = select(queue_13,head),
inference(forward_subsumption_resolution,[],[f35187,f4]) ).
fof(f35191,plain,
index_210 = index_26,
inference(forward_demodulation,[],[f35189,f35145]) ).
fof(f35283,plain,
index_27 = s(index_210),
inference(superposition,[],[f169,f35191]) ).
fof(f36945,plain,
( index_47 = select(queue_40,head)
| head = tail
| head = seq ),
inference(superposition,[],[f177,f5360]) ).
fof(f36946,plain,
( index_47 = select(queue_40,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f36945,f3]) ).
fof(f36948,plain,
index_47 = select(queue_40,head),
inference(forward_subsumption_resolution,[],[f36946,f4]) ).
fof(f36999,plain,
( index_47 = select(queue_34,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5354,f36948]) ).
fof(f37000,plain,
( index_47 = select(queue_34,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f36999,f3]) ).
fof(f37002,plain,
index_47 = select(queue_34,head),
inference(forward_subsumption_resolution,[],[f37000,f4]) ).
fof(f37131,plain,
( index_47 = select(queue_28,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5348,f37002]) ).
fof(f37132,plain,
( index_47 = select(queue_28,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f37131,f3]) ).
fof(f37134,plain,
index_47 = select(queue_28,head),
inference(forward_subsumption_resolution,[],[f37132,f4]) ).
fof(f37136,plain,
index_27 = index_47,
inference(forward_demodulation,[],[f37134,f593]) ).
fof(f37186,plain,
index_48 = s(index_27),
inference(superposition,[],[f178,f37136]) ).
fof(f38590,plain,
( index_68 = select(queue_61,head)
| head = tail
| head = seq ),
inference(superposition,[],[f186,f5384]) ).
fof(f38591,plain,
( index_68 = select(queue_61,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f38590,f3]) ).
fof(f38593,plain,
index_68 = select(queue_61,head),
inference(forward_subsumption_resolution,[],[f38591,f4]) ).
fof(f38596,plain,
( index_68 = select(queue_55,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5378,f38593]) ).
fof(f38597,plain,
( index_68 = select(queue_55,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f38596,f3]) ).
fof(f38599,plain,
index_68 = select(queue_55,head),
inference(forward_subsumption_resolution,[],[f38597,f4]) ).
fof(f38604,plain,
( index_68 = select(queue_49,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5372,f38599]) ).
fof(f38605,plain,
( index_68 = select(queue_49,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f38604,f3]) ).
fof(f38607,plain,
index_68 = select(queue_49,head),
inference(forward_subsumption_resolution,[],[f38605,f4]) ).
fof(f38609,plain,
index_48 = index_68,
inference(forward_demodulation,[],[f38607,f594]) ).
fof(f38612,plain,
index_69 = s(index_48),
inference(superposition,[],[f187,f38609]) ).
fof(f40291,plain,
( index_158 = select(queue_82,head)
| head = seq
| head = tail ),
inference(superposition,[],[f142,f5403]) ).
fof(f40292,plain,
( index_158 = select(queue_82,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f40291,f4]) ).
fof(f40294,plain,
index_158 = select(queue_82,head),
inference(forward_subsumption_resolution,[],[f40292,f3]) ).
fof(f40297,plain,
( index_158 = select(queue_7,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5396,f40294]) ).
fof(f40298,plain,
( index_158 = select(queue_7,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f40297,f3]) ).
fof(f40300,plain,
index_158 = select(queue_7,head),
inference(forward_subsumption_resolution,[],[f40298,f4]) ).
fof(f40304,plain,
( index_158 = select(queue_1,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5366,f40300]) ).
fof(f40305,plain,
( index_158 = select(queue_1,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f40304,f3]) ).
fof(f40307,plain,
index_158 = select(queue_1,head),
inference(forward_subsumption_resolution,[],[f40305,f4]) ).
fof(f40309,plain,
index_0 = index_158,
inference(forward_demodulation,[],[f40307,f586]) ).
fof(f40311,plain,
index_3 = index_158,
inference(forward_demodulation,[],[f40309,f4340]) ).
fof(f40313,plain,
index_159 = s(index_3),
inference(superposition,[],[f143,f40311]) ).
fof(f40317,plain,
( index_95 = select(queue_88,head)
| head = tail
| head = seq ),
inference(superposition,[],[f197,f5415]) ).
fof(f40318,plain,
( index_95 = select(queue_88,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f40317,f3]) ).
fof(f40320,plain,
index_95 = select(queue_88,head),
inference(forward_subsumption_resolution,[],[f40318,f4]) ).
fof(f40323,plain,
( index_96 = select(queue_103,head)
| head = seq
| head = tail ),
inference(superposition,[],[f596,f5420]) ).
fof(f40324,plain,
( index_96 = select(queue_103,head)
| head = tail ),
inference(forward_subsumption_resolution,[],[f40323,f4]) ).
fof(f40326,plain,
index_96 = select(queue_103,head),
inference(forward_subsumption_resolution,[],[f40324,f3]) ).
fof(f40328,plain,
index_116 = index_96,
inference(forward_demodulation,[],[f40326,f29803]) ).
fof(f40663,plain,
( index_95 = select(queue_76,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5406,f40320]) ).
fof(f40664,plain,
( index_95 = select(queue_76,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f40663,f3]) ).
fof(f40666,plain,
index_95 = select(queue_76,head),
inference(forward_subsumption_resolution,[],[f40664,f4]) ).
fof(f40681,plain,
index_159 = index_6,
inference(superposition,[],[f182,f40313]) ).
fof(f40780,plain,
index_78 = index_159,
inference(forward_demodulation,[],[f40681,f662]) ).
fof(f40965,plain,
( index_95 = select(queue_70,head)
| head = tail
| head = seq ),
inference(superposition,[],[f5390,f40666]) ).
fof(f40966,plain,
( index_95 = select(queue_70,head)
| head = seq ),
inference(forward_subsumption_resolution,[],[f40965,f3]) ).
fof(f40968,plain,
index_95 = select(queue_70,head),
inference(forward_subsumption_resolution,[],[f40966,f4]) ).
fof(f40970,plain,
index_69 = index_95,
inference(forward_demodulation,[],[f40968,f595]) ).
fof(f40974,plain,
index_96 = s(index_69),
inference(superposition,[],[f198,f40970]) ).
fof(f40981,plain,
index_116 = s(index_69),
inference(forward_demodulation,[],[f40974,f40328]) ).
fof(f41029,plain,
index_189 = s(index_78),
inference(superposition,[],[f32819,f40780]) ).
fof(f43625,plain,
! [X0] :
( select(earray_98,X0) = select(earray_71,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0 ),
inference(superposition,[],[f965,f28812]) ).
fof(f43626,plain,
! [X0] :
( select(earray_98,X0) = select(earray_64,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0 ),
inference(forward_demodulation,[],[f43625,f23490]) ).
fof(f43643,plain,
index_189 = index_81,
inference(superposition,[],[f191,f41029]) ).
fof(f43742,plain,
index_153 = index_189,
inference(forward_demodulation,[],[f43643,f658]) ).
fof(f44244,plain,
s(index_153) = index_210,
inference(superposition,[],[f34042,f43742]) ).
fof(f44254,plain,
index_156 = index_210,
inference(forward_demodulation,[],[f44244,f141]) ).
fof(f44315,plain,
index_171 = index_210,
inference(forward_demodulation,[],[f44254,f4359]) ).
fof(f46164,plain,
s(index_171) = index_27,
inference(superposition,[],[f35283,f44315]) ).
fof(f46173,plain,
index_174 = index_27,
inference(forward_demodulation,[],[f46164,f149]) ).
fof(f46247,plain,
index_177 = index_27,
inference(forward_demodulation,[],[f46173,f668]) ).
fof(f48225,plain,
! [X0] :
( select(earray_98,X0) = select(earray_58,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0
| index_63 = X0 ),
inference(superposition,[],[f43626,f26896]) ).
fof(f48360,plain,
s(index_177) = index_48,
inference(superposition,[],[f37186,f46247]) ).
fof(f48369,plain,
index_180 = index_48,
inference(forward_demodulation,[],[f48360,f152]) ).
fof(f48456,plain,
index_183 = index_48,
inference(forward_demodulation,[],[f48369,f667]) ).
fof(f50879,plain,
s(index_183) = index_69,
inference(superposition,[],[f38612,f48456]) ).
fof(f50888,plain,
index_186 = index_69,
inference(forward_demodulation,[],[f50879,f154]) ).
fof(f50985,plain,
index_192 = index_69,
inference(forward_demodulation,[],[f50888,f4369]) ).
fof(f53507,plain,
index_116 = s(index_192),
inference(superposition,[],[f40981,f50985]) ).
fof(f56524,plain,
index_116 = index_195,
inference(superposition,[],[f158,f53507]) ).
fof(f56629,plain,
index_198 = index_116,
inference(forward_demodulation,[],[f56524,f666]) ).
fof(f56949,plain,
index_117 = s(index_198),
inference(superposition,[],[f125,f56629]) ).
fof(f57004,plain,
index_117 = index_201,
inference(superposition,[],[f160,f56949]) ).
fof(f57110,plain,
index_204 = index_117,
inference(forward_demodulation,[],[f57004,f665]) ).
fof(f57345,plain,
index_138 = s(index_204),
inference(superposition,[],[f30275,f57110]) ).
fof(f58541,plain,
index_138 = index_207,
inference(superposition,[],[f162,f57345]) ).
fof(f58649,plain,
index_9 = index_138,
inference(forward_demodulation,[],[f58541,f4545]) ).
fof(f58858,plain,
( index_147 = s(index_9)
| ~ spl0_3 ),
inference(superposition,[],[f31075,f58649]) ).
fof(f60305,plain,
( index_147 = index_12
| ~ spl0_3 ),
inference(superposition,[],[f58858,f126]) ).
fof(f60509,plain,
( index_147 = index_15
| ~ spl0_3 ),
inference(superposition,[],[f60305,f674]) ).
fof(f60519,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f60509,f10852]) ).
fof(f60520,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f60519]) ).
fof(f60531,plain,
index_213 = s(index_9),
inference(forward_demodulation,[],[f31073,f58649]) ).
fof(f75434,plain,
index_213 = index_12,
inference(superposition,[],[f126,f60531]) ).
fof(f75494,plain,
index_15 = index_213,
inference(forward_demodulation,[],[f75434,f674]) ).
fof(f77134,plain,
! [X0] :
( select(earray_142,X0) = select(earray_148,X0)
| index_147 = X0 ),
inference(superposition,[],[f2,f18926]) ).
fof(f77139,plain,
( elem_214 = select(earray_142,index_213)
| index_147 = index_213
| ~ spl0_2 ),
inference(superposition,[],[f23556,f77134]) ).
fof(f77142,plain,
( elem_214 = select(earray_142,index_213)
| ~ spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f77139,f23671]) ).
fof(f77144,plain,
( elem_214 = select(earray_142,index_15)
| ~ spl0_2
| spl0_3 ),
inference(forward_demodulation,[],[f77142,f75494]) ).
fof(f77149,plain,
( elem_214 = select(earray_133,index_15)
| index_141 = index_15
| ~ spl0_2
| spl0_3 ),
inference(superposition,[],[f27305,f77144]) ).
fof(f77152,plain,
( elem_214 = select(earray_133,index_15)
| ~ spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f77149,f10116]) ).
fof(f77163,plain,
( elem_214 = select(earray_127,index_15)
| index_132 = index_15
| ~ spl0_2
| spl0_3 ),
inference(superposition,[],[f26537,f77152]) ).
fof(f77166,plain,
( elem_214 = select(earray_127,index_15)
| ~ spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f77163,f9433]) ).
fof(f77309,plain,
( elem_214 = select(earray_121,index_15)
| index_126 = index_15
| ~ spl0_2
| spl0_3 ),
inference(superposition,[],[f26509,f77166]) ).
fof(f77312,plain,
( elem_214 = select(earray_121,index_15)
| ~ spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f77309,f8789]) ).
fof(f77478,plain,
( elem_214 = select(earray_112,index_15)
| index_120 = index_15
| ~ spl0_2
| spl0_3 ),
inference(superposition,[],[f27303,f77312]) ).
fof(f77481,plain,
( elem_214 = select(earray_112,index_15)
| ~ spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f77478,f8171]) ).
fof(f77578,plain,
( elem_214 = select(earray_106,index_15)
| index_111 = index_15
| ~ spl0_2
| spl0_3 ),
inference(superposition,[],[f26505,f77481]) ).
fof(f77581,plain,
( elem_214 = select(earray_106,index_15)
| ~ spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f77578,f7583]) ).
fof(f77675,plain,
( elem_214 = select(earray_100,index_15)
| index_105 = index_15
| ~ spl0_2
| spl0_3 ),
inference(superposition,[],[f26487,f77581]) ).
fof(f77678,plain,
( elem_214 = select(earray_100,index_15)
| ~ spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f77675,f7034]) ).
fof(f80971,plain,
! [X0] :
( select(earray_98,X0) = select(earray_52,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0
| index_63 = X0
| index_57 = X0 ),
inference(superposition,[],[f48225,f26894]) ).
fof(f83060,plain,
! [X0] :
( select(earray_98,X0) = select(earray_43,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0 ),
inference(superposition,[],[f80971,f27443]) ).
fof(f85020,plain,
! [X0] :
( select(earray_98,X0) = select(earray_37,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0
| index_42 = X0 ),
inference(superposition,[],[f83060,f26890]) ).
fof(f86028,plain,
! [X0] :
( select(earray_98,X0) = select(earray_31,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0
| index_42 = X0
| index_36 = X0 ),
inference(superposition,[],[f85020,f26888]) ).
fof(f87441,plain,
! [X0] :
( select(earray_98,X0) = select(earray_22,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0
| index_42 = X0
| index_36 = X0
| index_30 = X0 ),
inference(superposition,[],[f86028,f27399]) ).
fof(f88619,plain,
! [X0] :
( select(earray_98,X0) = select(earray_16,X0)
| index_72 = X0
| index_84 = X0
| index_90 = X0
| index_63 = X0
| index_57 = X0
| index_51 = X0
| index_42 = X0
| index_36 = X0
| index_30 = X0
| index_21 = X0 ),
inference(superposition,[],[f87441,f26572]) ).
fof(f90196,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_72
| index_15 = index_84
| index_15 = index_90
| index_15 = index_63
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(superposition,[],[f563,f88619]) ).
fof(f90200,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_84
| index_15 = index_90
| index_15 = index_63
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90196,f25793]) ).
fof(f90203,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_90
| index_15 = index_63
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90200,f5589]) ).
fof(f90205,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_63
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90203,f6048]) ).
fof(f90207,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_57
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90205,f22455]) ).
fof(f90209,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_51
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90207,f17713]) ).
fof(f90211,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_42
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90209,f14329]) ).
fof(f90213,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_36
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90211,f13804]) ).
fof(f90215,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_30
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90213,f13532]) ).
fof(f90217,plain,
( e10 = select(earray_98,index_15)
| index_15 = index_21 ),
inference(forward_subsumption_resolution,[],[f90215,f4856]) ).
fof(f90219,plain,
e10 = select(earray_98,index_15),
inference(forward_subsumption_resolution,[],[f90217,f2983]) ).
fof(f90265,plain,
( e10 = select(earray_100,index_15)
| index_99 = index_15 ),
inference(superposition,[],[f940,f90219]) ).
fof(f90266,plain,
e10 = select(earray_100,index_15),
inference(forward_subsumption_resolution,[],[f90265,f6523]) ).
fof(f90509,plain,
( e10 = elem_214
| ~ spl0_2
| spl0_3 ),
inference(superposition,[],[f90266,f77678]) ).
fof(f90513,plain,
( $false
| ~ spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f90509,f303]) ).
fof(f90514,plain,
( ~ spl0_2
| spl0_3 ),
inference(avatar_contradiction_clause,[],[f90513]) ).
fof(f90515,plain,
( index_15 = index_162
| ~ spl0_1 ),
inference(forward_demodulation,[],[f23552,f75494]) ).
fof(f90519,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f90515,f11642]) ).
fof(f90520,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f90519]) ).
cnf(s2,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f23558]) ).
cnf(s6,plain,
~ spl0_3,
inference(sat_conversion,[],[f60520]) ).
cnf(s8,plain,
( ~ spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f90514]) ).
cnf(s9,plain,
~ spl0_1,
inference(sat_conversion,[],[f90520]) ).
cnf(s10,plain,
~ spl0_2,
inference(rat,[],[s8,s6]) ).
cnf(s11,plain,
$false,
inference(rat,[],[s2,s10,s9]) ).
fof(f90525,plain,
$false,
inference(avatar_sat_refutation,[],[s11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV569-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n016.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 11:59:03 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.35/1.98 % (3580485)Will run a generic schedule for satisfiability detection.
% 10.35/1.98 % (3580512)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3938865933:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 10.35/1.98 % (3580509)% WARNING: option uhcvi not known.
% 10.35/1.98 % (3580507)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3015614091_2999 on theBenchmark for (2999ds/0Mi)
% 10.35/1.98 % (3580511)dis+10_1_sil=32000:sp=arity:random_seed=3732613848:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 10.35/1.98 % (3580509)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2863314373:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 10.35/1.98 % (3580510)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2145967903:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 10.35/1.98 % (3580513)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3734727445:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 10.35/1.98 % (3580514)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1025888764:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 10.35/1.98 % (3580512)Instruction limit reached!
% 10.35/1.98 % (3580512)------------------------------
% 10.35/1.98 % (3580512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.35/1.98 % (3580512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.35/1.98 % (3580512)CaDiCaL version: 2.1.3
% 10.35/1.98 % (3580512)Termination reason: Instruction limit
% 10.35/1.98 % (3580512)Termination phase: Saturation
% 10.35/1.98 % (3580512)Time elapsed: 0.030 s
% 10.35/1.98 % (3580512)Peak memory usage: 12 MB
% 10.35/1.98 % (3580512)Instructions burned: 116 (million)
% 10.35/1.98 % (3580531)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=992553665:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 10.35/1.98 % (3580511)Instruction limit reached!
% 10.35/1.98 % (3580511)------------------------------
% 10.35/1.98 % (3580511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.35/1.98 % (3580511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.35/1.98 % (3580511)CaDiCaL version: 2.1.3
% 10.35/1.98 % (3580511)Termination reason: Instruction limit
% 10.35/1.98 % (3580511)Termination phase: Saturation
% 10.35/1.98 % (3580511)Time elapsed: 0.049 s
% 10.35/1.98 % (3580511)Peak memory usage: 12 MB
% 10.35/1.98 % (3580511)Instructions burned: 104 (million)
% 10.35/1.98 % (3580513)Instruction limit reached!
% 10.35/1.98 % (3580513)------------------------------
% 10.35/1.98 % (3580513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.35/1.98 % (3580513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.35/1.98 % (3580513)CaDiCaL version: 2.1.3
% 10.35/1.98 % (3580513)Termination reason: Instruction limit
% 10.35/1.98 % (3580513)Termination phase: Saturation
% 10.35/1.98 % (3580513)Time elapsed: 0.061 s
% 10.35/1.98 % (3580513)Peak memory usage: 12 MB
% 10.35/1.98 % (3580513)Instructions burned: 133 (million)
% 10.35/1.98 % (3580533)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1004481427:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 10.35/1.98 % Detected minimum model sizes of [3]
% 10.35/1.98 % Detected maximum model sizes of [max]
% 10.35/1.98 % TRYING [3]
% 10.35/1.98 % Detected minimum model sizes of [3]
% 10.35/1.98 % Detected maximum model sizes of [max]
% 10.35/1.98 % TRYING [3]
% 10.35/1.98 % (3580514)Instruction limit reached!
% 10.35/1.98 % (3580514)------------------------------
% 10.35/1.98 % (3580514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.35/1.98 % (3580514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.35/1.98 % (3580514)CaDiCaL version: 2.1.3
% 10.35/1.98 % (3580514)Termination reason: Instruction limit
% 10.35/1.98 % (3580514)Termination phase: Saturation
% 10.35/1.98 % (3580514)Time elapsed: 0.079 s
% 10.35/1.98 % (3580514)Peak memory usage: 13 MB
% 10.35/1.98 % (3580514)Instructions burned: 160 (million)
% 10.35/1.98 % (3580534)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3852470968:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 10.35/1.98 % TRYING [4]
% 10.35/1.98 % (3580536)ott-21_1_sil=16000:fs=off:random_seed=1007388510:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 10.35/1.98 % (3580533)Instruction limit reached!
% 10.35/1.98 % (3580533)------------------------------
% 10.35/1.98 % (3580533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580533)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580533)Termination reason: Instruction limit
% 19.80/3.12 % (3580533)Termination phase: Saturation
% 19.80/3.12 % (3580533)Time elapsed: 0.064 s
% 19.80/3.12 % (3580533)Peak memory usage: 13 MB
% 19.80/3.12 % (3580533)Instructions burned: 132 (million)
% 19.80/3.12 % TRYING [4]
% 19.80/3.12 % (3580539)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=260289752:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 19.80/3.12 % TRYING [5]
% 19.80/3.12 % (3580536)Instruction limit reached!
% 19.80/3.12 % (3580536)------------------------------
% 19.80/3.12 % (3580536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580536)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580536)Termination reason: Instruction limit
% 19.80/3.12 % (3580536)Termination phase: Saturation
% 19.80/3.12 % (3580536)Time elapsed: 0.076 s
% 19.80/3.12 % (3580536)Peak memory usage: 12 MB
% 19.80/3.12 % (3580536)Instructions burned: 180 (million)
% 19.80/3.12 % (3580531)Instruction limit reached!
% 19.80/3.12 % (3580531)------------------------------
% 19.80/3.12 % (3580531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580531)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580531)Termination reason: Instruction limit
% 19.80/3.12 % (3580531)Termination phase: Finite model building constraint generation
% 19.80/3.12 % (3580531)Time elapsed: 0.145 s
% 19.80/3.12 % (3580531)Peak memory usage: 32 MB
% 19.80/3.12 % (3580531)Instructions burned: 715 (million)
% 19.80/3.12 % (3580542)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3321824682:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 19.80/3.12 % (3580541)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2289937694:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 19.80/3.12 % TRYING [5]
% 19.80/3.12 % Detected minimum model sizes of [3]
% 19.80/3.12 % Detected maximum model sizes of [max]
% 19.80/3.12 % TRYING [3]
% 19.80/3.12 % (3580539)Instruction limit reached!
% 19.80/3.12 % (3580539)------------------------------
% 19.80/3.12 % (3580539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580539)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580539)Termination reason: Instruction limit
% 19.80/3.12 % (3580539)Termination phase: Saturation
% 19.80/3.12 % (3580539)Time elapsed: 0.209 s
% 19.80/3.12 % (3580539)Peak memory usage: 15 MB
% 19.80/3.12 % (3580539)Instructions burned: 477 (million)
% 19.80/3.12 % (3580534)Instruction limit reached!
% 19.80/3.12 % (3580534)------------------------------
% 19.80/3.12 % (3580534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580534)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580534)Termination reason: Instruction limit
% 19.80/3.12 % (3580534)Termination phase: Saturation
% 19.80/3.12 % (3580534)Time elapsed: 0.291 s
% 19.80/3.12 % (3580534)Peak memory usage: 16 MB
% 19.80/3.12 % (3580534)Instructions burned: 684 (million)
% 19.80/3.12 % (3580545)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3531980454:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 19.80/3.12 % (3580546)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2675410825:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 19.80/3.12 % TRYING [4]
% 19.80/3.12 % (3580542)Instruction limit reached!
% 19.80/3.12 % (3580542)------------------------------
% 19.80/3.12 % (3580542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580542)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580542)Termination reason: Instruction limit
% 19.80/3.12 % (3580542)Termination phase: Saturation
% 19.80/3.12 % (3580542)Time elapsed: 0.273 s
% 19.80/3.12 % (3580542)Peak memory usage: 19 MB
% 19.80/3.12 % (3580542)Instructions burned: 1180 (million)
% 19.80/3.12 % (3580549)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1800188173:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 19.80/3.12 % (3580541)Instruction limit reached!
% 19.80/3.12 % (3580541)------------------------------
% 19.80/3.12 % (3580541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580541)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580541)Termination reason: Instruction limit
% 19.80/3.12 % (3580541)Termination phase: Finite model building SAT solving
% 19.80/3.12 % (3580541)Time elapsed: 0.363 s
% 19.80/3.12 % (3580541)Peak memory usage: 30 MB
% 19.80/3.12 % (3580541)Instructions burned: 865 (million)
% 19.80/3.12 % TRYING [6]
% 19.80/3.12 % (3580551)fmb+10_1_sil=64000:random_seed=98157743:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 19.80/3.12 % TRYING [14]
% 19.80/3.12 % Detected minimum model sizes of [3]
% 19.80/3.12 % Detected maximum model sizes of [max]
% 19.80/3.12 % TRYING [3]
% 19.80/3.12 % (3580549)Instruction limit reached!
% 19.80/3.12 % (3580549)------------------------------
% 19.80/3.12 % (3580549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580549)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580549)Termination reason: Instruction limit
% 19.80/3.12 % (3580549)Termination phase: Saturation
% 19.80/3.12 % (3580549)Time elapsed: 0.200 s
% 19.80/3.12 % (3580549)Peak memory usage: 16 MB
% 19.80/3.12 % (3580549)Instructions burned: 879 (million)
% 19.80/3.12 % (3580553)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3064885738:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 19.80/3.12 % (3580546)Instruction limit reached!
% 19.80/3.12 % (3580546)------------------------------
% 19.80/3.12 % (3580546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580546)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580546)Termination reason: Instruction limit
% 19.80/3.12 % (3580546)Termination phase: Saturation
% 19.80/3.12 % (3580546)Time elapsed: 0.312 s
% 19.80/3.12 % (3580546)Peak memory usage: 16 MB
% 19.80/3.12 % (3580546)Instructions burned: 694 (million)
% 19.80/3.12 % (3580555)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=452329386:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 19.80/3.12 % Detected minimum model sizes of [3]
% 19.80/3.12 % Detected maximum model sizes of [max]
% 19.80/3.12 % TRYING [20]
% 19.80/3.12 % (3580545)Instruction limit reached!
% 19.80/3.12 % (3580545)------------------------------
% 19.80/3.12 % (3580545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580545)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580545)Termination reason: Instruction limit
% 19.80/3.12 % (3580545)Termination phase: Finite model building constraint generation
% 19.80/3.12 % (3580545)Time elapsed: 0.357 s
% 19.80/3.12 % (3580545)Peak memory usage: 72 MB
% 19.80/3.12 % (3580545)Instructions burned: 890 (million)
% 19.80/3.12 % (3580557)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1861135910:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 19.80/3.12 % Detected minimum model sizes of [3]
% 19.80/3.12 % Detected maximum model sizes of [max]
% 19.80/3.12 % TRYING [8]
% 19.80/3.12 % TRYING [4]
% 19.80/3.12 % (3580555)Instruction limit reached!
% 19.80/3.12 % (3580555)------------------------------
% 19.80/3.12 % (3580555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580555)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580555)Termination reason: Instruction limit
% 19.80/3.12 % (3580555)Termination phase: Finite model building constraint generation
% 19.80/3.12 % (3580555)Time elapsed: 0.340 s
% 19.80/3.12 % (3580555)Peak memory usage: 65 MB
% 19.80/3.12 % (3580555)Instructions burned: 922 (million)
% 19.80/3.12 % (3580559)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1927227542:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 19.80/3.12 % TRYING [7]
% 19.80/3.12 % TRYING [5]
% 19.80/3.12 % (3580559)Instruction limit reached!
% 19.80/3.12 % (3580559)------------------------------
% 19.80/3.12 % (3580559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580559)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580559)Termination reason: Instruction limit
% 19.80/3.12 % (3580559)Termination phase: Saturation
% 19.80/3.12 % (3580559)Time elapsed: 0.610 s
% 19.80/3.12 % (3580559)Peak memory usage: 22 MB
% 19.80/3.12 % (3580559)Instructions burned: 1472 (million)
% 19.80/3.12 % (3580561)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1255147156:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 19.80/3.12 % Detected minimum model sizes of [3]
% 19.80/3.12 % Detected maximum model sizes of [max]
% 19.80/3.12 % TRYING [77]
% 19.80/3.12 % TRYING [6]
% 19.80/3.12 % TRYING [8]
% 19.80/3.12 % (3580553)Instruction limit reached!
% 19.80/3.12 % (3580553)------------------------------
% 19.80/3.12 % (3580553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.12 % (3580553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.12 % (3580553)CaDiCaL version: 2.1.3
% 19.80/3.12 % (3580553)Termination reason: Instruction limit
% 19.80/3.12 % (3580553)Termination phase: Finite model building constraint generation
% 19.80/3.12 % (3580553)Time elapsed: 1.891 s
% 19.80/3.12 % (3580553)Peak memory usage: 570 MB
% 19.80/3.12 % (3580553)Instructions burned: 9520 (million)
% 19.80/3.12 % (3580563)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=217463249:fmbsr=2.30978:i=2174_2973 on theBenchmark for (2973ds/2174Mi)
% 19.80/3.12 % Detected minimum model sizes of [3]
% 19.80/3.12 % Detected maximum model sizes of [max]
% 19.80/3.12 % TRYING [16]
% 19.80/3.12 % (3580509) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3580485-3580509"...
% 19.80/3.12 % (3580509)...printing done.
% 19.80/3.12 % (3580509)Refutation found. Thanks to Tanya!
% 19.80/3.12 % SZS status Unsatisfiable for theBenchmark
% 19.80/3.12 % SZS output start Proof for theBenchmark
% See solution above
% 19.80/3.13 % (3580509)------------------------------
% 19.80/3.13 % (3580509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.13 % (3580509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.13 % (3580509)CaDiCaL version: 2.1.3
% 19.80/3.13 % (3580509)Termination reason: Refutation
% 19.80/3.13 % (3580509)Time elapsed: 2.815 s
% 19.80/3.13 % (3580509)Peak memory usage: 35 MB
% 19.80/3.13 % (3580509)Instructions burned: 6845 (million)
% 19.80/3.13 % (3580485)Success in time 2.894 s
% 19.80/3.13 % Vampire exiting
%------------------------------------------------------------------------------