%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV569-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 02:49:07 PM UTC 2026
% Result : Unsatisfiable 9.16s 1.56s
% Output : CNFRefutation 9.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 249
% Syntax : Number of formulae : 1276 ( 951 unt; 0 def)
% Number of atoms : 1899 (1898 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 882 ( 259 ~; 623 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 2 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 263 ( 263 usr; 260 con; 0-3 aty)
% Number of variables : 206 ( 206 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
head != tail,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
head != seq,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
tail != seq,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(X))))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(X)))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] : s(s(s(s(s(s(s(s(s(X))))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X] : s(s(s(s(s(s(s(s(X)))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] : s(s(s(s(s(s(s(X))))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [X] : s(s(s(s(s(s(X)))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [X] : s(s(s(s(s(X))))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X] : s(s(s(s(X)))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X] : s(s(s(X))) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] : s(s(X)) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] : s(X) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,hypothesis,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,hypothesis,
earray_104 = select(q22,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,hypothesis,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,hypothesis,
earray_110 = select(q23,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,hypothesis,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,hypothesis,
earray_119 = select(q24,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,hypothesis,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,hypothesis,
earray_125 = select(q25,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,hypothesis,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,hypothesis,
earray_131 = select(q26,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,hypothesis,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,hypothesis,
earray_140 = select(q27,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,hypothesis,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,hypothesis,
earray_146 = select(q28,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,hypothesis,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
earray_16 = store(earray_14,index_15,e10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
earray_161 = select(q29,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,hypothesis,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,hypothesis,
earray_20 = select(q11,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,hypothesis,
earray_212 = select(q30,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,hypothesis,
earray_22 = store(earray_20,index_21,e11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,hypothesis,
earray_29 = select(q12,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,hypothesis,
earray_31 = store(earray_29,index_30,e12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,hypothesis,
earray_35 = select(q13,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,hypothesis,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,hypothesis,
earray_41 = select(q14,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,hypothesis,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,hypothesis,
earray_50 = select(q15,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,hypothesis,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,hypothesis,
earray_56 = select(q16,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,hypothesis,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,hypothesis,
earray_62 = select(q17,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,hypothesis,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
earray_71 = select(q18,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,hypothesis,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,hypothesis,
earray_83 = select(q19,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
earray_89 = select(q20,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,hypothesis,
earray_98 = select(q21,seq),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,hypothesis,
elem_214 = select(earray_212,index_213),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
index_0 = select(q,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,hypothesis,
index_105 = select(q22,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,hypothesis,
index_111 = select(q23,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,hypothesis,
index_116 = select(queue_115,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,hypothesis,
index_117 = s(index_116),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,hypothesis,
index_120 = select(q24,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,hypothesis,
index_123 = s(index_120),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,hypothesis,
index_126 = select(q25,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f130,hypothesis,
index_129 = s(index_126),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f131,hypothesis,
index_132 = select(q26,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,hypothesis,
index_135 = s(index_132),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,hypothesis,
index_137 = select(queue_136,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,hypothesis,
index_138 = s(index_137),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,hypothesis,
index_141 = select(q27,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f136,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,hypothesis,
index_147 = select(q28,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,hypothesis,
index_15 = select(q10,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f140,hypothesis,
index_153 = select(q2,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,hypothesis,
index_156 = s(index_153),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,hypothesis,
index_158 = select(queue_157,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,hypothesis,
index_159 = s(index_158),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,hypothesis,
index_162 = select(q29,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,hypothesis,
index_167 = select(queue_166,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,hypothesis,
index_168 = s(index_167),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,hypothesis,
index_171 = select(q3,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f150,hypothesis,
index_177 = select(q4,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f151,hypothesis,
index_18 = s(index_15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,hypothesis,
index_180 = s(index_177),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,hypothesis,
index_183 = select(q5,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f154,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,hypothesis,
index_188 = select(queue_187,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,hypothesis,
index_189 = s(index_188),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,hypothesis,
index_192 = select(q6,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,hypothesis,
index_195 = s(index_192),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,hypothesis,
index_198 = select(q7,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,hypothesis,
index_201 = s(index_198),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,hypothesis,
index_204 = select(q8,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,hypothesis,
index_207 = s(index_204),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,hypothesis,
index_209 = select(queue_208,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,hypothesis,
index_21 = select(q11,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f165,hypothesis,
index_210 = s(index_209),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f166,hypothesis,
index_213 = select(q30,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f167,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,hypothesis,
index_26 = select(queue_25,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,hypothesis,
index_27 = s(index_26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f170,hypothesis,
index_3 = select(q0,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,hypothesis,
index_30 = select(q12,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,hypothesis,
index_33 = s(index_30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,hypothesis,
index_36 = select(q13,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,hypothesis,
index_39 = s(index_36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,hypothesis,
index_42 = select(q14,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f176,hypothesis,
index_45 = s(index_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f177,hypothesis,
index_47 = select(queue_46,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,hypothesis,
index_48 = s(index_47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,hypothesis,
index_51 = select(q15,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f180,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f181,hypothesis,
index_57 = select(q16,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f182,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f183,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f184,hypothesis,
index_63 = select(q17,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,hypothesis,
index_68 = select(queue_67,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,hypothesis,
index_69 = s(index_68),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,hypothesis,
index_72 = select(q18,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,hypothesis,
index_75 = s(index_72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,hypothesis,
index_78 = select(q1,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,hypothesis,
index_81 = s(index_78),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,hypothesis,
index_84 = select(q19,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,hypothesis,
index_87 = s(index_84),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,hypothesis,
index_9 = select(q9,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,hypothesis,
index_90 = select(q20,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,hypothesis,
index_93 = s(index_90),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,hypothesis,
index_95 = select(queue_94,head),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,hypothesis,
index_96 = s(index_95),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,hypothesis,
index_99 = select(q21,tail),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f200,hypothesis,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,hypothesis,
queue_101 = store(q21,seq,earray_100),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,hypothesis,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f203,hypothesis,
queue_107 = store(q22,seq,earray_106),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,hypothesis,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f205,hypothesis,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f206,hypothesis,
queue_113 = store(q23,seq,earray_112),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f207,hypothesis,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f208,hypothesis,
queue_118 = store(queue_115,head,index_117),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f209,hypothesis,
queue_122 = store(q24,seq,earray_121),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f210,hypothesis,
queue_124 = store(queue_122,tail,index_123),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,hypothesis,
queue_128 = store(q25,seq,earray_127),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f212,hypothesis,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,hypothesis,
queue_130 = store(queue_128,tail,index_129),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f214,hypothesis,
queue_134 = store(q26,seq,earray_133),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f215,hypothesis,
queue_136 = store(queue_134,tail,index_135),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f216,hypothesis,
queue_139 = store(queue_136,head,index_138),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f217,hypothesis,
queue_143 = store(q27,seq,earray_142),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f218,hypothesis,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f219,hypothesis,
queue_149 = store(q28,seq,earray_148),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f220,hypothesis,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f221,hypothesis,
queue_155 = store(q2,seq,earray_154),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f222,hypothesis,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f223,hypothesis,
queue_160 = store(queue_157,head,index_159),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f224,hypothesis,
queue_164 = store(q29,seq,earray_163),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f225,hypothesis,
queue_166 = store(queue_164,tail,index_165),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f226,hypothesis,
queue_169 = store(queue_166,head,index_168),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f227,hypothesis,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f228,hypothesis,
queue_173 = store(q3,seq,earray_172),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f229,hypothesis,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f230,hypothesis,
queue_179 = store(q4,seq,earray_178),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f231,hypothesis,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f232,hypothesis,
queue_185 = store(q5,seq,earray_184),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f233,hypothesis,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f234,hypothesis,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f235,hypothesis,
queue_190 = store(queue_187,head,index_189),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f236,hypothesis,
queue_194 = store(q6,seq,earray_193),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f237,hypothesis,
queue_196 = store(queue_194,tail,index_195),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f238,hypothesis,
queue_200 = store(q7,seq,earray_199),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f239,hypothesis,
queue_202 = store(queue_200,tail,index_201),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f240,hypothesis,
queue_206 = store(q8,seq,earray_205),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f241,hypothesis,
queue_208 = store(queue_206,tail,index_207),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f242,hypothesis,
queue_211 = store(queue_208,head,index_210),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f243,hypothesis,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f244,hypothesis,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f245,hypothesis,
queue_28 = store(queue_25,head,index_27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f246,hypothesis,
queue_32 = store(q12,seq,earray_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f247,hypothesis,
queue_34 = store(queue_32,tail,index_33),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f248,hypothesis,
queue_38 = store(q13,seq,earray_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f249,hypothesis,
queue_40 = store(queue_38,tail,index_39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f250,hypothesis,
queue_44 = store(q14,seq,earray_43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f251,hypothesis,
queue_46 = store(queue_44,tail,index_45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f252,hypothesis,
queue_49 = store(queue_46,head,index_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,hypothesis,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f254,hypothesis,
queue_53 = store(q15,seq,earray_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f255,hypothesis,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f256,hypothesis,
queue_59 = store(q16,seq,earray_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f257,hypothesis,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f258,hypothesis,
queue_65 = store(q17,seq,earray_64),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f259,hypothesis,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f260,hypothesis,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f261,hypothesis,
queue_70 = store(queue_67,head,index_69),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f262,hypothesis,
queue_74 = store(q18,seq,earray_73),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f263,hypothesis,
queue_76 = store(queue_74,tail,index_75),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f264,hypothesis,
queue_80 = store(q1,seq,earray_79),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f265,hypothesis,
queue_82 = store(queue_80,tail,index_81),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f266,hypothesis,
queue_86 = store(q19,seq,earray_85),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f267,hypothesis,
queue_88 = store(queue_86,tail,index_87),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f268,hypothesis,
queue_92 = store(q20,seq,earray_91),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f269,hypothesis,
queue_94 = store(queue_92,tail,index_93),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f270,hypothesis,
queue_97 = store(queue_94,head,index_96),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f271,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f272,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f273,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f274,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f275,hypothesis,
q12 = queue_28,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f276,hypothesis,
q13 = queue_34,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f277,hypothesis,
q14 = queue_40,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f278,hypothesis,
q15 = queue_49,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f279,hypothesis,
q16 = queue_55,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,hypothesis,
q17 = queue_61,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f281,hypothesis,
q18 = queue_70,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f282,hypothesis,
q19 = queue_76,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f283,hypothesis,
q2 = queue_82,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f284,hypothesis,
q20 = queue_88,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f285,hypothesis,
q21 = queue_97,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f286,hypothesis,
q22 = queue_103,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f287,hypothesis,
q23 = queue_109,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f288,hypothesis,
q24 = queue_118,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,hypothesis,
q25 = queue_124,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f290,hypothesis,
q26 = queue_130,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f291,hypothesis,
q27 = queue_139,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f292,hypothesis,
q28 = queue_145,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f293,hypothesis,
q29 = queue_151,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f294,hypothesis,
q3 = queue_160,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f295,hypothesis,
q30 = queue_169,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f296,hypothesis,
q4 = queue_175,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f297,hypothesis,
q5 = queue_181,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f298,hypothesis,
q6 = queue_190,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f299,hypothesis,
q7 = queue_196,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f300,hypothesis,
q8 = queue_202,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f301,hypothesis,
q9 = queue_211,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f302,negated_conjecture,
elem_214 != e10,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f303,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f304,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f305,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f306,plain,
head != tail,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f307,plain,
head != seq,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f308,plain,
tail != seq,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f340,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f341,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f342,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f343,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f344,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f345,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f346,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f347,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f348,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f349,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f350,plain,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f351,plain,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f352,plain,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f353,plain,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f354,plain,
! [X0] : s(s(s(s(s(X0))))) != X0,
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f355,plain,
! [X0] : s(s(s(s(X0)))) != X0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f356,plain,
! [X0] : s(s(s(X0))) != X0,
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f357,plain,
! [X0] : s(s(X0)) != X0,
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f358,plain,
! [X0] : s(X0) != X0,
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f360,plain,
earray_100 = store(earray_98,index_99,e21),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f361,plain,
earray_104 = select(q22,seq),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f362,plain,
earray_106 = store(earray_104,index_105,e22),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f363,plain,
earray_110 = select(q23,seq),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f364,plain,
earray_112 = store(earray_110,index_111,e23),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f365,plain,
earray_119 = select(q24,seq),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f366,plain,
earray_121 = store(earray_119,index_120,e24),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f367,plain,
earray_125 = select(q25,seq),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f368,plain,
earray_127 = store(earray_125,index_126,e25),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f369,plain,
earray_131 = select(q26,seq),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f370,plain,
earray_133 = store(earray_131,index_132,e26),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f372,plain,
earray_140 = select(q27,seq),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f373,plain,
earray_142 = store(earray_140,index_141,e27),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f374,plain,
earray_146 = select(q28,seq),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f375,plain,
earray_148 = store(earray_146,index_147,e28),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f378,plain,
earray_16 = store(earray_14,index_15,e10),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f379,plain,
earray_161 = select(q29,seq),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f380,plain,
earray_163 = store(earray_161,index_162,e29),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f392,plain,
earray_20 = select(q11,seq),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f395,plain,
earray_212 = select(q30,seq),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f396,plain,
earray_22 = store(earray_20,index_21,e11),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f397,plain,
earray_29 = select(q12,seq),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f398,plain,
earray_31 = store(earray_29,index_30,e12),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f399,plain,
earray_35 = select(q13,seq),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f400,plain,
earray_37 = store(earray_35,index_36,e13),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f402,plain,
earray_41 = select(q14,seq),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f403,plain,
earray_43 = store(earray_41,index_42,e14),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f404,plain,
earray_50 = select(q15,seq),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f405,plain,
earray_52 = store(earray_50,index_51,e15),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f406,plain,
earray_56 = select(q16,seq),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f407,plain,
earray_58 = store(earray_56,index_57,e16),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f408,plain,
earray_62 = select(q17,seq),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f409,plain,
earray_64 = store(earray_62,index_63,e17),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f410,plain,
earray_71 = select(q18,seq),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f411,plain,
earray_73 = store(earray_71,index_72,e18),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f415,plain,
earray_83 = select(q19,seq),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f416,plain,
earray_85 = store(earray_83,index_84,e19),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f417,plain,
earray_89 = select(q20,seq),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f418,plain,
earray_91 = store(earray_89,index_90,e20),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f419,plain,
earray_98 = select(q21,seq),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f420,plain,
elem_214 = select(earray_212,index_213),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f421,plain,
index_0 = select(q,tail),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f422,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f423,plain,
index_105 = select(q22,tail),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f424,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f425,plain,
index_111 = select(q23,tail),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f426,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f427,plain,
index_116 = select(queue_115,head),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f428,plain,
index_117 = s(index_116),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f429,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f430,plain,
index_120 = select(q24,tail),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f431,plain,
index_123 = s(index_120),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f432,plain,
index_126 = select(q25,tail),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f433,plain,
index_129 = s(index_126),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f434,plain,
index_132 = select(q26,tail),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f435,plain,
index_135 = s(index_132),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f436,plain,
index_137 = select(queue_136,head),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f437,plain,
index_138 = s(index_137),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f438,plain,
index_141 = select(q27,tail),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f439,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f440,plain,
index_147 = select(q28,tail),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f441,plain,
index_15 = select(q10,tail),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f442,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f443,plain,
index_153 = select(q2,tail),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f444,plain,
index_156 = s(index_153),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f445,plain,
index_158 = select(queue_157,head),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f446,plain,
index_159 = s(index_158),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f447,plain,
index_162 = select(q29,tail),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f449,plain,
index_167 = select(queue_166,head),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f450,plain,
index_168 = s(index_167),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f451,plain,
index_171 = select(q3,tail),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f452,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f453,plain,
index_177 = select(q4,tail),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f454,plain,
index_18 = s(index_15),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f455,plain,
index_180 = s(index_177),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f456,plain,
index_183 = select(q5,tail),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f457,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f458,plain,
index_188 = select(queue_187,head),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f459,plain,
index_189 = s(index_188),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f460,plain,
index_192 = select(q6,tail),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f461,plain,
index_195 = s(index_192),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f462,plain,
index_198 = select(q7,tail),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f463,plain,
index_201 = s(index_198),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f464,plain,
index_204 = select(q8,tail),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f465,plain,
index_207 = s(index_204),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f466,plain,
index_209 = select(queue_208,head),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f467,plain,
index_21 = select(q11,tail),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f468,plain,
index_210 = s(index_209),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f469,plain,
index_213 = select(q30,head),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f470,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f471,plain,
index_26 = select(queue_25,head),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f472,plain,
index_27 = s(index_26),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f473,plain,
index_3 = select(q0,tail),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f474,plain,
index_30 = select(q12,tail),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f475,plain,
index_33 = s(index_30),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f476,plain,
index_36 = select(q13,tail),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f477,plain,
index_39 = s(index_36),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f478,plain,
index_42 = select(q14,tail),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f479,plain,
index_45 = s(index_42),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f480,plain,
index_47 = select(queue_46,head),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f481,plain,
index_48 = s(index_47),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f482,plain,
index_51 = select(q15,tail),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f483,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f484,plain,
index_57 = select(q16,tail),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f485,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f486,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f487,plain,
index_63 = select(q17,tail),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f488,plain,
index_66 = s(index_63),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f489,plain,
index_68 = select(queue_67,head),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f490,plain,
index_69 = s(index_68),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f491,plain,
index_72 = select(q18,tail),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f492,plain,
index_75 = s(index_72),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f493,plain,
index_78 = select(q1,tail),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f494,plain,
index_81 = s(index_78),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f495,plain,
index_84 = select(q19,tail),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f496,plain,
index_87 = s(index_84),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f497,plain,
index_9 = select(q9,tail),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f498,plain,
index_90 = select(q20,tail),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f499,plain,
index_93 = s(index_90),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f500,plain,
index_95 = select(queue_94,head),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f501,plain,
index_96 = s(index_95),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f502,plain,
index_99 = select(q21,tail),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f503,plain,
queue_1 = store(q,head,index_0),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f504,plain,
queue_101 = store(q21,seq,earray_100),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f505,plain,
queue_103 = store(queue_101,tail,index_102),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f506,plain,
queue_107 = store(q22,seq,earray_106),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f507,plain,
queue_109 = store(queue_107,tail,index_108),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f508,plain,
queue_11 = store(q9,seq,earray_10),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f509,plain,
queue_113 = store(q23,seq,earray_112),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f510,plain,
queue_115 = store(queue_113,tail,index_114),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f511,plain,
queue_118 = store(queue_115,head,index_117),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f512,plain,
queue_122 = store(q24,seq,earray_121),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f513,plain,
queue_124 = store(queue_122,tail,index_123),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f514,plain,
queue_128 = store(q25,seq,earray_127),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f515,plain,
queue_13 = store(queue_11,tail,index_12),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f516,plain,
queue_130 = store(queue_128,tail,index_129),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f517,plain,
queue_134 = store(q26,seq,earray_133),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f518,plain,
queue_136 = store(queue_134,tail,index_135),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f519,plain,
queue_139 = store(queue_136,head,index_138),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f520,plain,
queue_143 = store(q27,seq,earray_142),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f521,plain,
queue_145 = store(queue_143,tail,index_144),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f522,plain,
queue_149 = store(q28,seq,earray_148),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f523,plain,
queue_151 = store(queue_149,tail,index_150),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f524,plain,
queue_155 = store(q2,seq,earray_154),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f525,plain,
queue_157 = store(queue_155,tail,index_156),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f526,plain,
queue_160 = store(queue_157,head,index_159),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f527,plain,
queue_164 = store(q29,seq,earray_163),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f528,plain,
queue_166 = store(queue_164,tail,index_165),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f529,plain,
queue_169 = store(queue_166,head,index_168),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f530,plain,
queue_17 = store(q10,seq,earray_16),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f531,plain,
queue_173 = store(q3,seq,earray_172),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f532,plain,
queue_175 = store(queue_173,tail,index_174),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f533,plain,
queue_179 = store(q4,seq,earray_178),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f534,plain,
queue_181 = store(queue_179,tail,index_180),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f535,plain,
queue_185 = store(q5,seq,earray_184),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f536,plain,
queue_187 = store(queue_185,tail,index_186),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f537,plain,
queue_19 = store(queue_17,tail,index_18),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f538,plain,
queue_190 = store(queue_187,head,index_189),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f539,plain,
queue_194 = store(q6,seq,earray_193),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f540,plain,
queue_196 = store(queue_194,tail,index_195),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f541,plain,
queue_200 = store(q7,seq,earray_199),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f542,plain,
queue_202 = store(queue_200,tail,index_201),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f543,plain,
queue_206 = store(q8,seq,earray_205),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f544,plain,
queue_208 = store(queue_206,tail,index_207),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f545,plain,
queue_211 = store(queue_208,head,index_210),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f546,plain,
queue_23 = store(q11,seq,earray_22),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f547,plain,
queue_25 = store(queue_23,tail,index_24),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f548,plain,
queue_28 = store(queue_25,head,index_27),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f549,plain,
queue_32 = store(q12,seq,earray_31),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f550,plain,
queue_34 = store(queue_32,tail,index_33),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f551,plain,
queue_38 = store(q13,seq,earray_37),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f552,plain,
queue_40 = store(queue_38,tail,index_39),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f553,plain,
queue_44 = store(q14,seq,earray_43),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f554,plain,
queue_46 = store(queue_44,tail,index_45),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f555,plain,
queue_49 = store(queue_46,head,index_48),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f556,plain,
queue_5 = store(q0,seq,earray_4),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f557,plain,
queue_53 = store(q15,seq,earray_52),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f558,plain,
queue_55 = store(queue_53,tail,index_54),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f559,plain,
queue_59 = store(q16,seq,earray_58),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f560,plain,
queue_61 = store(queue_59,tail,index_60),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f561,plain,
queue_65 = store(q17,seq,earray_64),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f562,plain,
queue_67 = store(queue_65,tail,index_66),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f563,plain,
queue_7 = store(queue_5,tail,index_6),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f564,plain,
queue_70 = store(queue_67,head,index_69),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f565,plain,
queue_74 = store(q18,seq,earray_73),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f566,plain,
queue_76 = store(queue_74,tail,index_75),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f567,plain,
queue_80 = store(q1,seq,earray_79),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f568,plain,
queue_82 = store(queue_80,tail,index_81),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f569,plain,
queue_86 = store(q19,seq,earray_85),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f570,plain,
queue_88 = store(queue_86,tail,index_87),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f571,plain,
queue_92 = store(q20,seq,earray_91),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f572,plain,
queue_94 = store(queue_92,tail,index_93),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f573,plain,
queue_97 = store(queue_94,head,index_96),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f574,plain,
q0 = queue_1,
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f575,plain,
q1 = queue_7,
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f576,plain,
q10 = queue_13,
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f577,plain,
q11 = queue_19,
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f578,plain,
q12 = queue_28,
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f579,plain,
q13 = queue_34,
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f580,plain,
q14 = queue_40,
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f581,plain,
q15 = queue_49,
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f582,plain,
q16 = queue_55,
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f583,plain,
q17 = queue_61,
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f584,plain,
q18 = queue_70,
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f585,plain,
q19 = queue_76,
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f586,plain,
q2 = queue_82,
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f587,plain,
q20 = queue_88,
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f588,plain,
q21 = queue_97,
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f589,plain,
q22 = queue_103,
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f590,plain,
q23 = queue_109,
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f591,plain,
q24 = queue_118,
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f592,plain,
q25 = queue_124,
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f593,plain,
q26 = queue_130,
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f594,plain,
q27 = queue_139,
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f595,plain,
q28 = queue_145,
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f596,plain,
q29 = queue_151,
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f597,plain,
q3 = queue_160,
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f598,plain,
q30 = queue_169,
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f599,plain,
q4 = queue_175,
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f600,plain,
q5 = queue_181,
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f601,plain,
q6 = queue_190,
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f602,plain,
q7 = queue_196,
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f603,plain,
q8 = queue_202,
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f604,plain,
q9 = queue_211,
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f605,plain,
elem_214 != e10,
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f606,plain,
select(earray_16,index_15) = e10,
inference(paramodulation,[status(thm)],[f378,f303]) ).
fof(f794,plain,
s(index_18) != index_15,
inference(paramodulation,[status(thm)],[f454,f357]) ).
fof(f798,plain,
index_18 != index_15,
inference(paramodulation,[status(thm)],[f454,f358]) ).
fof(f1595,plain,
s(s(index_18)) != index_15,
inference(paramodulation,[status(thm)],[f454,f356]) ).
fof(f2454,plain,
! [X0] :
( select(earray_100,X0) = select(earray_98,X0)
| index_99 = X0 ),
inference(paramodulation,[status(thm)],[f360,f305]) ).
fof(f2456,plain,
! [X0] :
( select(earray_106,X0) = select(earray_104,X0)
| index_105 = X0 ),
inference(paramodulation,[status(thm)],[f362,f305]) ).
fof(f2458,plain,
! [X0] :
( select(earray_112,X0) = select(earray_110,X0)
| index_111 = X0 ),
inference(paramodulation,[status(thm)],[f364,f305]) ).
fof(f2460,plain,
! [X0] :
( select(earray_121,X0) = select(earray_119,X0)
| index_120 = X0 ),
inference(paramodulation,[status(thm)],[f366,f305]) ).
fof(f2462,plain,
! [X0] :
( select(earray_127,X0) = select(earray_125,X0)
| index_126 = X0 ),
inference(paramodulation,[status(thm)],[f368,f305]) ).
fof(f2464,plain,
! [X0] :
( select(earray_133,X0) = select(earray_131,X0)
| index_132 = X0 ),
inference(paramodulation,[status(thm)],[f370,f305]) ).
fof(f2586,plain,
! [X0] :
( select(earray_142,X0) = select(earray_140,X0)
| index_141 = X0 ),
inference(paramodulation,[status(thm)],[f373,f305]) ).
fof(f2588,plain,
! [X0] :
( select(earray_148,X0) = select(earray_146,X0)
| index_147 = X0 ),
inference(paramodulation,[status(thm)],[f375,f305]) ).
fof(f2632,plain,
! [X0] :
( select(earray_163,X0) = select(earray_161,X0)
| index_162 = X0 ),
inference(paramodulation,[status(thm)],[f380,f305]) ).
fof(f2646,plain,
! [X0] :
( select(earray_22,X0) = select(earray_20,X0)
| index_21 = X0 ),
inference(paramodulation,[status(thm)],[f396,f305]) ).
fof(f2648,plain,
! [X0] :
( select(earray_31,X0) = select(earray_29,X0)
| index_30 = X0 ),
inference(paramodulation,[status(thm)],[f398,f305]) ).
fof(f2650,plain,
! [X0] :
( select(earray_37,X0) = select(earray_35,X0)
| index_36 = X0 ),
inference(paramodulation,[status(thm)],[f400,f305]) ).
fof(f2654,plain,
! [X0] :
( select(earray_43,X0) = select(earray_41,X0)
| index_42 = X0 ),
inference(paramodulation,[status(thm)],[f403,f305]) ).
fof(f2656,plain,
! [X0] :
( select(earray_52,X0) = select(earray_50,X0)
| index_51 = X0 ),
inference(paramodulation,[status(thm)],[f405,f305]) ).
fof(f2658,plain,
! [X0] :
( select(earray_58,X0) = select(earray_56,X0)
| index_57 = X0 ),
inference(paramodulation,[status(thm)],[f407,f305]) ).
fof(f2660,plain,
! [X0] :
( select(earray_64,X0) = select(earray_62,X0)
| index_63 = X0 ),
inference(paramodulation,[status(thm)],[f409,f305]) ).
fof(f2662,plain,
! [X0] :
( select(earray_73,X0) = select(earray_71,X0)
| index_72 = X0 ),
inference(paramodulation,[status(thm)],[f411,f305]) ).
fof(f2666,plain,
! [X0] :
( select(earray_85,X0) = select(earray_83,X0)
| index_84 = X0 ),
inference(paramodulation,[status(thm)],[f416,f305]) ).
fof(f2668,plain,
! [X0] :
( select(earray_91,X0) = select(earray_89,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f418,f305]) ).
fof(f2670,plain,
q0 = store(q,head,index_0),
inference(forward_demodulation,[status(thm)],[f574,f503]) ).
fof(f2671,plain,
! [X0] :
( select(q0,X0) = select(q,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f2670,f305]) ).
fof(f2672,plain,
select(q0,head) = index_0,
inference(paramodulation,[status(thm)],[f2670,f303]) ).
fof(f2673,plain,
! [X0] :
( select(queue_101,X0) = select(q21,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f504,f305]) ).
fof(f2674,plain,
select(queue_101,seq) = earray_100,
inference(paramodulation,[status(thm)],[f504,f303]) ).
fof(f2675,plain,
q22 = store(queue_101,tail,index_102),
inference(forward_demodulation,[status(thm)],[f589,f505]) ).
fof(f2676,plain,
! [X0] :
( select(q22,X0) = select(queue_101,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2675,f305]) ).
fof(f2677,plain,
select(q22,tail) = index_102,
inference(paramodulation,[status(thm)],[f2675,f303]) ).
fof(f2678,plain,
index_105 = index_102,
inference(forward_demodulation,[status(thm)],[f423,f2677]) ).
fof(f2683,plain,
index_105 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2678,f422]) ).
fof(f2785,plain,
! [X0] :
( select(queue_107,X0) = select(q22,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f506,f305]) ).
fof(f2786,plain,
select(queue_107,seq) = earray_106,
inference(paramodulation,[status(thm)],[f506,f303]) ).
fof(f2787,plain,
q23 = store(queue_107,tail,index_108),
inference(forward_demodulation,[status(thm)],[f590,f507]) ).
fof(f2788,plain,
! [X0] :
( select(q23,X0) = select(queue_107,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2787,f305]) ).
fof(f2789,plain,
select(q23,tail) = index_108,
inference(paramodulation,[status(thm)],[f2787,f303]) ).
fof(f2790,plain,
index_111 = index_108,
inference(forward_demodulation,[status(thm)],[f425,f2789]) ).
fof(f2798,plain,
index_111 = s(index_105),
inference(backward_demodulation,[status(thm)],[f2790,f424]) ).
fof(f2803,plain,
! [X0] :
( select(queue_11,X0) = select(q9,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f508,f305]) ).
fof(f2805,plain,
! [X0] :
( select(queue_113,X0) = select(q23,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f509,f305]) ).
fof(f2806,plain,
select(queue_113,seq) = earray_112,
inference(paramodulation,[status(thm)],[f509,f303]) ).
fof(f2906,plain,
! [X0] :
( select(queue_115,X0) = select(queue_113,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f510,f305]) ).
fof(f2907,plain,
select(queue_115,tail) = index_114,
inference(paramodulation,[status(thm)],[f510,f303]) ).
fof(f2908,plain,
q24 = store(queue_115,head,index_117),
inference(forward_demodulation,[status(thm)],[f591,f511]) ).
fof(f2909,plain,
! [X0] :
( select(q24,X0) = select(queue_115,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f2908,f305]) ).
fof(f2910,plain,
select(q24,head) = index_117,
inference(paramodulation,[status(thm)],[f2908,f303]) ).
fof(f2911,plain,
! [X0] :
( select(queue_122,X0) = select(q24,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f512,f305]) ).
fof(f2912,plain,
select(queue_122,seq) = earray_121,
inference(paramodulation,[status(thm)],[f512,f303]) ).
fof(f2913,plain,
q25 = store(queue_122,tail,index_123),
inference(forward_demodulation,[status(thm)],[f592,f513]) ).
fof(f2914,plain,
! [X0] :
( select(q25,X0) = select(queue_122,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2913,f305]) ).
fof(f2915,plain,
select(q25,tail) = index_123,
inference(paramodulation,[status(thm)],[f2913,f303]) ).
fof(f2916,plain,
index_126 = index_123,
inference(forward_demodulation,[status(thm)],[f432,f2915]) ).
fof(f2921,plain,
index_126 = s(index_120),
inference(backward_demodulation,[status(thm)],[f2916,f431]) ).
fof(f2924,plain,
! [X0] :
( select(queue_128,X0) = select(q25,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f514,f305]) ).
fof(f2925,plain,
select(queue_128,seq) = earray_127,
inference(paramodulation,[status(thm)],[f514,f303]) ).
fof(f2926,plain,
q10 = store(queue_11,tail,index_12),
inference(forward_demodulation,[status(thm)],[f576,f515]) ).
fof(f2927,plain,
! [X0] :
( select(q10,X0) = select(queue_11,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2926,f305]) ).
fof(f2928,plain,
select(q10,tail) = index_12,
inference(paramodulation,[status(thm)],[f2926,f303]) ).
fof(f2929,plain,
index_15 = index_12,
inference(forward_demodulation,[status(thm)],[f441,f2928]) ).
fof(f2930,plain,
q26 = store(queue_128,tail,index_129),
inference(forward_demodulation,[status(thm)],[f593,f516]) ).
fof(f2931,plain,
! [X0] :
( select(q26,X0) = select(queue_128,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2930,f305]) ).
fof(f2932,plain,
select(q26,tail) = index_129,
inference(paramodulation,[status(thm)],[f2930,f303]) ).
fof(f2933,plain,
index_132 = index_129,
inference(forward_demodulation,[status(thm)],[f434,f2932]) ).
fof(f2938,plain,
index_15 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2929,f429]) ).
fof(f2946,plain,
index_132 = s(index_126),
inference(backward_demodulation,[status(thm)],[f2933,f433]) ).
fof(f2949,plain,
! [X0] :
( select(queue_134,X0) = select(q26,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f517,f305]) ).
fof(f2950,plain,
select(queue_134,seq) = earray_133,
inference(paramodulation,[status(thm)],[f517,f303]) ).
fof(f3202,plain,
! [X0] :
( select(queue_136,X0) = select(queue_134,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f518,f305]) ).
fof(f3203,plain,
select(queue_136,tail) = index_135,
inference(paramodulation,[status(thm)],[f518,f303]) ).
fof(f3204,plain,
q27 = store(queue_136,head,index_138),
inference(forward_demodulation,[status(thm)],[f594,f519]) ).
fof(f3205,plain,
! [X0] :
( select(q27,X0) = select(queue_136,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f3204,f305]) ).
fof(f3206,plain,
select(q27,head) = index_138,
inference(paramodulation,[status(thm)],[f3204,f303]) ).
fof(f3209,plain,
! [X0] :
( select(queue_143,X0) = select(q27,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f520,f305]) ).
fof(f3210,plain,
select(queue_143,seq) = earray_142,
inference(paramodulation,[status(thm)],[f520,f303]) ).
fof(f3211,plain,
q28 = store(queue_143,tail,index_144),
inference(forward_demodulation,[status(thm)],[f595,f521]) ).
fof(f3212,plain,
! [X0] :
( select(q28,X0) = select(queue_143,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3211,f305]) ).
fof(f3213,plain,
select(q28,tail) = index_144,
inference(paramodulation,[status(thm)],[f3211,f303]) ).
fof(f3214,plain,
index_147 = index_144,
inference(forward_demodulation,[status(thm)],[f440,f3213]) ).
fof(f3219,plain,
index_147 = s(index_141),
inference(backward_demodulation,[status(thm)],[f3214,f439]) ).
fof(f3321,plain,
! [X0] :
( select(queue_149,X0) = select(q28,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f522,f305]) ).
fof(f3322,plain,
select(queue_149,seq) = earray_148,
inference(paramodulation,[status(thm)],[f522,f303]) ).
fof(f3323,plain,
q29 = store(queue_149,tail,index_150),
inference(forward_demodulation,[status(thm)],[f596,f523]) ).
fof(f3324,plain,
! [X0] :
( select(q29,X0) = select(queue_149,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3323,f305]) ).
fof(f3325,plain,
select(q29,tail) = index_150,
inference(paramodulation,[status(thm)],[f3323,f303]) ).
fof(f3326,plain,
index_162 = index_150,
inference(forward_demodulation,[status(thm)],[f447,f3325]) ).
fof(f3334,plain,
index_162 = s(index_147),
inference(backward_demodulation,[status(thm)],[f3326,f442]) ).
fof(f3339,plain,
! [X0] :
( select(queue_155,X0) = select(q2,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f524,f305]) ).
fof(f3341,plain,
! [X0] :
( select(queue_157,X0) = select(queue_155,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f525,f305]) ).
fof(f3342,plain,
select(queue_157,tail) = index_156,
inference(paramodulation,[status(thm)],[f525,f303]) ).
fof(f3343,plain,
q3 = store(queue_157,head,index_159),
inference(forward_demodulation,[status(thm)],[f597,f526]) ).
fof(f3344,plain,
! [X0] :
( select(q3,X0) = select(queue_157,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f3343,f305]) ).
fof(f3345,plain,
select(q3,head) = index_159,
inference(paramodulation,[status(thm)],[f3343,f303]) ).
fof(f3346,plain,
! [X0] :
( select(queue_164,X0) = select(q29,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f527,f305]) ).
fof(f3347,plain,
select(queue_164,seq) = earray_163,
inference(paramodulation,[status(thm)],[f527,f303]) ).
fof(f3447,plain,
! [X0] :
( select(queue_166,X0) = select(queue_164,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f528,f305]) ).
fof(f3449,plain,
q30 = store(queue_166,head,index_168),
inference(forward_demodulation,[status(thm)],[f598,f529]) ).
fof(f3450,plain,
! [X0] :
( select(q30,X0) = select(queue_166,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f3449,f305]) ).
fof(f3451,plain,
select(q30,head) = index_168,
inference(paramodulation,[status(thm)],[f3449,f303]) ).
fof(f3452,plain,
index_213 = index_168,
inference(forward_demodulation,[status(thm)],[f469,f3451]) ).
fof(f3457,plain,
index_213 = s(index_167),
inference(backward_demodulation,[status(thm)],[f3452,f450]) ).
fof(f3458,plain,
! [X0] :
( select(queue_17,X0) = select(q10,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f530,f305]) ).
fof(f3459,plain,
select(queue_17,seq) = earray_16,
inference(paramodulation,[status(thm)],[f530,f303]) ).
fof(f3460,plain,
! [X0] :
( select(queue_173,X0) = select(q3,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f531,f305]) ).
fof(f3512,plain,
q4 = store(queue_173,tail,index_174),
inference(forward_demodulation,[status(thm)],[f599,f532]) ).
fof(f3513,plain,
! [X0] :
( select(q4,X0) = select(queue_173,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3512,f305]) ).
fof(f3514,plain,
select(q4,tail) = index_174,
inference(paramodulation,[status(thm)],[f3512,f303]) ).
fof(f3515,plain,
index_177 = index_174,
inference(forward_demodulation,[status(thm)],[f453,f3514]) ).
fof(f3520,plain,
index_177 = s(index_171),
inference(backward_demodulation,[status(thm)],[f3515,f452]) ).
fof(f3622,plain,
! [X0] :
( select(queue_179,X0) = select(q4,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f533,f305]) ).
fof(f3624,plain,
q5 = store(queue_179,tail,index_180),
inference(forward_demodulation,[status(thm)],[f600,f534]) ).
fof(f3625,plain,
! [X0] :
( select(q5,X0) = select(queue_179,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3624,f305]) ).
fof(f3626,plain,
select(q5,tail) = index_180,
inference(paramodulation,[status(thm)],[f3624,f303]) ).
fof(f3627,plain,
index_183 = index_180,
inference(forward_demodulation,[status(thm)],[f456,f3626]) ).
fof(f3635,plain,
index_183 = s(index_177),
inference(backward_demodulation,[status(thm)],[f3627,f455]) ).
fof(f3640,plain,
! [X0] :
( select(queue_185,X0) = select(q5,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f535,f305]) ).
fof(f3642,plain,
! [X0] :
( select(queue_187,X0) = select(queue_185,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f536,f305]) ).
fof(f3643,plain,
select(queue_187,tail) = index_186,
inference(paramodulation,[status(thm)],[f536,f303]) ).
fof(f3644,plain,
q11 = store(queue_17,tail,index_18),
inference(forward_demodulation,[status(thm)],[f577,f537]) ).
fof(f3645,plain,
! [X0] :
( select(q11,X0) = select(queue_17,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3644,f305]) ).
fof(f3646,plain,
select(q11,tail) = index_18,
inference(paramodulation,[status(thm)],[f3644,f303]) ).
fof(f3647,plain,
index_21 = index_18,
inference(forward_demodulation,[status(thm)],[f467,f3646]) ).
fof(f3652,plain,
s(s(index_21)) != index_15,
inference(backward_demodulation,[status(thm)],[f3647,f1595]) ).
fof(f3653,plain,
s(index_21) != index_15,
inference(backward_demodulation,[status(thm)],[f3647,f794]) ).
fof(f3654,plain,
index_21 != index_15,
inference(backward_demodulation,[status(thm)],[f3647,f798]) ).
fof(f3655,plain,
index_21 = s(index_15),
inference(backward_demodulation,[status(thm)],[f3647,f454]) ).
fof(f3658,plain,
s(index_24) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3652]) ).
fof(f3659,plain,
index_24 != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3653]) ).
fof(f3660,plain,
q6 = store(queue_187,head,index_189),
inference(forward_demodulation,[status(thm)],[f601,f538]) ).
fof(f3661,plain,
! [X0] :
( select(q6,X0) = select(queue_187,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f3660,f305]) ).
fof(f3662,plain,
select(q6,head) = index_189,
inference(paramodulation,[status(thm)],[f3660,f303]) ).
fof(f3762,plain,
s(s(s(s(index_21)))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f354]) ).
fof(f3763,plain,
s(s(s(s(s(index_21))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f353]) ).
fof(f3764,plain,
s(s(s(s(s(s(index_21)))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f352]) ).
fof(f3765,plain,
s(s(s(s(s(s(s(index_21))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f351]) ).
fof(f3766,plain,
s(s(s(index_21))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f355]) ).
fof(f3767,plain,
s(s(s(s(s(s(s(s(index_21)))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f350]) ).
fof(f3768,plain,
s(s(s(s(s(s(s(s(s(index_21))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f349]) ).
fof(f3769,plain,
s(s(s(s(s(s(s(s(s(s(index_21)))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f348]) ).
fof(f3770,plain,
s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f347]) ).
fof(f3771,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f346]) ).
fof(f3772,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f345]) ).
fof(f3773,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f344]) ).
fof(f3774,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f343]) ).
fof(f3775,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f342]) ).
fof(f3776,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f341]) ).
fof(f3777,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f3655,f340]) ).
fof(f3812,plain,
s(s(s(index_24))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3762]) ).
fof(f3813,plain,
s(s(s(s(index_24)))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3763]) ).
fof(f3814,plain,
s(s(s(s(s(index_24))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3764]) ).
fof(f3815,plain,
s(s(s(s(s(s(index_24)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3765]) ).
fof(f3816,plain,
s(s(index_24)) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3766]) ).
fof(f3817,plain,
s(s(s(s(s(s(s(index_24))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3767]) ).
fof(f3818,plain,
s(s(s(s(s(s(s(s(index_24)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3768]) ).
fof(f3819,plain,
s(s(s(s(s(s(s(s(s(index_24))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3769]) ).
fof(f3820,plain,
s(s(s(s(s(s(s(s(s(s(index_24)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3770]) ).
fof(f3821,plain,
s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3771]) ).
fof(f3822,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3772]) ).
fof(f3823,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3773]) ).
fof(f3824,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3774]) ).
fof(f3825,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3775]) ).
fof(f3826,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3776]) ).
fof(f3827,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f470,f3777]) ).
fof(f3861,plain,
! [X0] :
( select(queue_194,X0) = select(q6,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f539,f305]) ).
fof(f3863,plain,
q7 = store(queue_194,tail,index_195),
inference(forward_demodulation,[status(thm)],[f602,f540]) ).
fof(f3864,plain,
! [X0] :
( select(q7,X0) = select(queue_194,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3863,f305]) ).
fof(f3865,plain,
select(q7,tail) = index_195,
inference(paramodulation,[status(thm)],[f3863,f303]) ).
fof(f3866,plain,
index_198 = index_195,
inference(forward_demodulation,[status(thm)],[f462,f3865]) ).
fof(f3871,plain,
index_198 = s(index_192),
inference(backward_demodulation,[status(thm)],[f3866,f461]) ).
fof(f3973,plain,
! [X0] :
( select(queue_200,X0) = select(q7,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f541,f305]) ).
fof(f3975,plain,
q8 = store(queue_200,tail,index_201),
inference(forward_demodulation,[status(thm)],[f603,f542]) ).
fof(f3976,plain,
! [X0] :
( select(q8,X0) = select(queue_200,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3975,f305]) ).
fof(f3977,plain,
select(q8,tail) = index_201,
inference(paramodulation,[status(thm)],[f3975,f303]) ).
fof(f3978,plain,
index_204 = index_201,
inference(forward_demodulation,[status(thm)],[f464,f3977]) ).
fof(f3986,plain,
index_204 = s(index_198),
inference(backward_demodulation,[status(thm)],[f3978,f463]) ).
fof(f4090,plain,
! [X0] :
( select(queue_206,X0) = select(q8,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f543,f305]) ).
fof(f4092,plain,
! [X0] :
( select(queue_208,X0) = select(queue_206,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f544,f305]) ).
fof(f4093,plain,
select(queue_208,tail) = index_207,
inference(paramodulation,[status(thm)],[f544,f303]) ).
fof(f4094,plain,
q9 = store(queue_208,head,index_210),
inference(forward_demodulation,[status(thm)],[f604,f545]) ).
fof(f4095,plain,
! [X0] :
( select(q9,X0) = select(queue_208,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f4094,f305]) ).
fof(f4096,plain,
select(q9,head) = index_210,
inference(paramodulation,[status(thm)],[f4094,f303]) ).
fof(f4097,plain,
! [X0] :
( select(queue_23,X0) = select(q11,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f546,f305]) ).
fof(f4098,plain,
select(queue_23,seq) = earray_22,
inference(paramodulation,[status(thm)],[f546,f303]) ).
fof(f4099,plain,
! [X0] :
( select(queue_25,X0) = select(queue_23,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f547,f305]) ).
fof(f4100,plain,
select(queue_25,tail) = index_24,
inference(paramodulation,[status(thm)],[f547,f303]) ).
fof(f4101,plain,
q12 = store(queue_25,head,index_27),
inference(forward_demodulation,[status(thm)],[f578,f548]) ).
fof(f4102,plain,
! [X0] :
( select(q12,X0) = select(queue_25,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f4101,f305]) ).
fof(f4103,plain,
select(q12,head) = index_27,
inference(paramodulation,[status(thm)],[f4101,f303]) ).
fof(f4104,plain,
! [X0] :
( select(queue_32,X0) = select(q12,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f549,f305]) ).
fof(f4105,plain,
select(queue_32,seq) = earray_31,
inference(paramodulation,[status(thm)],[f549,f303]) ).
fof(f4106,plain,
q13 = store(queue_32,tail,index_33),
inference(forward_demodulation,[status(thm)],[f579,f550]) ).
fof(f4107,plain,
! [X0] :
( select(q13,X0) = select(queue_32,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4106,f305]) ).
fof(f4108,plain,
select(q13,tail) = index_33,
inference(paramodulation,[status(thm)],[f4106,f303]) ).
fof(f4109,plain,
index_36 = index_33,
inference(forward_demodulation,[status(thm)],[f476,f4108]) ).
fof(f4114,plain,
index_36 = s(index_30),
inference(backward_demodulation,[status(thm)],[f4109,f475]) ).
fof(f4216,plain,
! [X0] :
( select(queue_38,X0) = select(q13,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f551,f305]) ).
fof(f4217,plain,
select(queue_38,seq) = earray_37,
inference(paramodulation,[status(thm)],[f551,f303]) ).
fof(f4218,plain,
q14 = store(queue_38,tail,index_39),
inference(forward_demodulation,[status(thm)],[f580,f552]) ).
fof(f4219,plain,
! [X0] :
( select(q14,X0) = select(queue_38,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4218,f305]) ).
fof(f4220,plain,
select(q14,tail) = index_39,
inference(paramodulation,[status(thm)],[f4218,f303]) ).
fof(f4221,plain,
index_42 = index_39,
inference(forward_demodulation,[status(thm)],[f478,f4220]) ).
fof(f4229,plain,
index_42 = s(index_36),
inference(backward_demodulation,[status(thm)],[f4221,f477]) ).
fof(f4333,plain,
! [X0] :
( select(queue_44,X0) = select(q14,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f553,f305]) ).
fof(f4334,plain,
select(queue_44,seq) = earray_43,
inference(paramodulation,[status(thm)],[f553,f303]) ).
fof(f4335,plain,
! [X0] :
( select(queue_46,X0) = select(queue_44,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f554,f305]) ).
fof(f4336,plain,
select(queue_46,tail) = index_45,
inference(paramodulation,[status(thm)],[f554,f303]) ).
fof(f4337,plain,
q15 = store(queue_46,head,index_48),
inference(forward_demodulation,[status(thm)],[f581,f555]) ).
fof(f4338,plain,
! [X0] :
( select(q15,X0) = select(queue_46,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f4337,f305]) ).
fof(f4339,plain,
select(q15,head) = index_48,
inference(paramodulation,[status(thm)],[f4337,f303]) ).
fof(f4340,plain,
! [X0] :
( select(queue_5,X0) = select(q0,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f556,f305]) ).
fof(f4342,plain,
! [X0] :
( select(queue_53,X0) = select(q15,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f557,f305]) ).
fof(f4343,plain,
select(queue_53,seq) = earray_52,
inference(paramodulation,[status(thm)],[f557,f303]) ).
fof(f4344,plain,
q16 = store(queue_53,tail,index_54),
inference(forward_demodulation,[status(thm)],[f582,f558]) ).
fof(f4345,plain,
! [X0] :
( select(q16,X0) = select(queue_53,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4344,f305]) ).
fof(f4346,plain,
select(q16,tail) = index_54,
inference(paramodulation,[status(thm)],[f4344,f303]) ).
fof(f4347,plain,
index_57 = index_54,
inference(forward_demodulation,[status(thm)],[f484,f4346]) ).
fof(f4348,plain,
! [X0] :
( select(queue_59,X0) = select(q16,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f559,f305]) ).
fof(f4349,plain,
select(queue_59,seq) = earray_58,
inference(paramodulation,[status(thm)],[f559,f303]) ).
fof(f4354,plain,
index_57 = s(index_51),
inference(backward_demodulation,[status(thm)],[f4347,f483]) ).
fof(f4456,plain,
q17 = store(queue_59,tail,index_60),
inference(forward_demodulation,[status(thm)],[f583,f560]) ).
fof(f4457,plain,
! [X0] :
( select(q17,X0) = select(queue_59,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4456,f305]) ).
fof(f4458,plain,
select(q17,tail) = index_60,
inference(paramodulation,[status(thm)],[f4456,f303]) ).
fof(f4459,plain,
index_63 = index_60,
inference(forward_demodulation,[status(thm)],[f487,f4458]) ).
fof(f4466,plain,
index_63 = s(index_57),
inference(backward_demodulation,[status(thm)],[f4459,f486]) ).
fof(f4571,plain,
! [X0] :
( select(queue_65,X0) = select(q17,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f561,f305]) ).
fof(f4572,plain,
select(queue_65,seq) = earray_64,
inference(paramodulation,[status(thm)],[f561,f303]) ).
fof(f4573,plain,
! [X0] :
( select(queue_67,X0) = select(queue_65,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f562,f305]) ).
fof(f4574,plain,
select(queue_67,tail) = index_66,
inference(paramodulation,[status(thm)],[f562,f303]) ).
fof(f4575,plain,
q1 = store(queue_5,tail,index_6),
inference(forward_demodulation,[status(thm)],[f575,f563]) ).
fof(f4576,plain,
! [X0] :
( select(q1,X0) = select(queue_5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4575,f305]) ).
fof(f4577,plain,
select(q1,tail) = index_6,
inference(paramodulation,[status(thm)],[f4575,f303]) ).
fof(f4578,plain,
index_78 = index_6,
inference(forward_demodulation,[status(thm)],[f493,f4577]) ).
fof(f4583,plain,
index_78 = s(index_3),
inference(backward_demodulation,[status(thm)],[f4578,f485]) ).
fof(f4685,plain,
q18 = store(queue_67,head,index_69),
inference(forward_demodulation,[status(thm)],[f584,f564]) ).
fof(f4686,plain,
! [X0] :
( select(q18,X0) = select(queue_67,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f4685,f305]) ).
fof(f4687,plain,
select(q18,head) = index_69,
inference(paramodulation,[status(thm)],[f4685,f303]) ).
fof(f4688,plain,
! [X0] :
( select(queue_74,X0) = select(q18,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f565,f305]) ).
fof(f4689,plain,
select(queue_74,seq) = earray_73,
inference(paramodulation,[status(thm)],[f565,f303]) ).
fof(f4690,plain,
q19 = store(queue_74,tail,index_75),
inference(forward_demodulation,[status(thm)],[f585,f566]) ).
fof(f4691,plain,
! [X0] :
( select(q19,X0) = select(queue_74,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4690,f305]) ).
fof(f4692,plain,
select(q19,tail) = index_75,
inference(paramodulation,[status(thm)],[f4690,f303]) ).
fof(f4693,plain,
index_84 = index_75,
inference(forward_demodulation,[status(thm)],[f495,f4692]) ).
fof(f4698,plain,
index_84 = s(index_72),
inference(backward_demodulation,[status(thm)],[f4693,f492]) ).
fof(f4800,plain,
! [X0] :
( select(queue_80,X0) = select(q1,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f567,f305]) ).
fof(f4802,plain,
q2 = store(queue_80,tail,index_81),
inference(forward_demodulation,[status(thm)],[f586,f568]) ).
fof(f4803,plain,
! [X0] :
( select(q2,X0) = select(queue_80,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4802,f305]) ).
fof(f4804,plain,
select(q2,tail) = index_81,
inference(paramodulation,[status(thm)],[f4802,f303]) ).
fof(f4805,plain,
index_153 = index_81,
inference(forward_demodulation,[status(thm)],[f443,f4804]) ).
fof(f4806,plain,
! [X0] :
( select(queue_86,X0) = select(q19,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f569,f305]) ).
fof(f4807,plain,
select(queue_86,seq) = earray_85,
inference(paramodulation,[status(thm)],[f569,f303]) ).
fof(f4815,plain,
index_153 = s(index_78),
inference(backward_demodulation,[status(thm)],[f4805,f494]) ).
fof(f4820,plain,
q20 = store(queue_86,tail,index_87),
inference(forward_demodulation,[status(thm)],[f587,f570]) ).
fof(f4821,plain,
! [X0] :
( select(q20,X0) = select(queue_86,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4820,f305]) ).
fof(f4822,plain,
select(q20,tail) = index_87,
inference(paramodulation,[status(thm)],[f4820,f303]) ).
fof(f4823,plain,
index_90 = index_87,
inference(forward_demodulation,[status(thm)],[f498,f4822]) ).
fof(f4831,plain,
index_90 = s(index_84),
inference(backward_demodulation,[status(thm)],[f4823,f496]) ).
fof(f5034,plain,
! [X0] :
( select(queue_92,X0) = select(q20,X0)
| seq = X0 ),
inference(paramodulation,[status(thm)],[f571,f305]) ).
fof(f5035,plain,
select(queue_92,seq) = earray_91,
inference(paramodulation,[status(thm)],[f571,f303]) ).
fof(f5036,plain,
! [X0] :
( select(queue_94,X0) = select(queue_92,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f572,f305]) ).
fof(f5037,plain,
select(queue_94,tail) = index_93,
inference(paramodulation,[status(thm)],[f572,f303]) ).
fof(f5038,plain,
q21 = store(queue_94,head,index_96),
inference(forward_demodulation,[status(thm)],[f588,f573]) ).
fof(f5039,plain,
! [X0] :
( select(q21,X0) = select(queue_94,X0)
| head = X0 ),
inference(paramodulation,[status(thm)],[f5038,f305]) ).
fof(f5040,plain,
select(q21,head) = index_96,
inference(paramodulation,[status(thm)],[f5038,f303]) ).
fof(f5299,plain,
( select(q0,tail) = index_0
| head = tail ),
inference(paramodulation,[status(thm)],[f421,f2671]) ).
fof(f5301,plain,
( index_3 = index_0
| head = tail ),
inference(forward_demodulation,[status(thm)],[f473,f5299]) ).
fof(f5302,plain,
index_3 = index_0,
inference(forward_subsumption_resolution,[status(thm)],[f5301,f306]) ).
fof(f5305,plain,
select(q0,head) = index_3,
inference(backward_demodulation,[status(thm)],[f5302,f2672]) ).
fof(f5314,plain,
( select(q22,seq) = earray_100
| tail = seq ),
inference(paramodulation,[status(thm)],[f2674,f2676]) ).
fof(f5315,plain,
! [X0] :
( seq = X0
| select(q22,X0) = select(q21,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2673,f2676]) ).
fof(f5318,plain,
( earray_104 = earray_100
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f361,f5314]) ).
fof(f5319,plain,
earray_104 = earray_100,
inference(forward_subsumption_resolution,[status(thm)],[f5318,f308]) ).
fof(f5322,plain,
! [X0] :
( select(earray_106,X0) = select(earray_100,X0)
| index_105 = X0 ),
inference(backward_demodulation,[status(thm)],[f5319,f2456]) ).
fof(f5329,plain,
( select(q23,seq) = earray_106
| tail = seq ),
inference(paramodulation,[status(thm)],[f2786,f2788]) ).
fof(f5330,plain,
! [X0] :
( seq = X0
| select(q23,X0) = select(q22,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2785,f2788]) ).
fof(f5333,plain,
( earray_110 = earray_106
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f363,f5329]) ).
fof(f5334,plain,
earray_110 = earray_106,
inference(forward_subsumption_resolution,[status(thm)],[f5333,f308]) ).
fof(f5340,plain,
! [X0] :
( select(earray_112,X0) = select(earray_106,X0)
| index_111 = X0 ),
inference(backward_demodulation,[status(thm)],[f5334,f2458]) ).
fof(f5349,plain,
( select(queue_115,seq) = earray_112
| tail = seq ),
inference(paramodulation,[status(thm)],[f2806,f2906]) ).
fof(f5350,plain,
! [X0] :
( seq = X0
| select(queue_115,X0) = select(q23,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2805,f2906]) ).
fof(f5353,plain,
select(queue_115,seq) = earray_112,
inference(forward_subsumption_resolution,[status(thm)],[f5349,f308]) ).
fof(f5355,plain,
( select(q24,seq) = earray_112
| head = seq ),
inference(paramodulation,[status(thm)],[f5353,f2909]) ).
fof(f5356,plain,
( select(q24,tail) = index_114
| head = tail ),
inference(paramodulation,[status(thm)],[f2907,f2909]) ).
fof(f5361,plain,
( earray_119 = earray_112
| head = seq ),
inference(forward_demodulation,[status(thm)],[f365,f5355]) ).
fof(f5362,plain,
earray_119 = earray_112,
inference(forward_subsumption_resolution,[status(thm)],[f5361,f307]) ).
fof(f5363,plain,
( index_120 = index_114
| head = tail ),
inference(forward_demodulation,[status(thm)],[f430,f5356]) ).
fof(f5364,plain,
index_120 = index_114,
inference(forward_subsumption_resolution,[status(thm)],[f5363,f306]) ).
fof(f5369,plain,
! [X0] :
( select(earray_121,X0) = select(earray_112,X0)
| index_120 = X0 ),
inference(backward_demodulation,[status(thm)],[f5362,f2460]) ).
fof(f5400,plain,
index_120 = s(index_111),
inference(backward_demodulation,[status(thm)],[f5364,f426]) ).
fof(f5669,plain,
( select(q25,seq) = earray_121
| tail = seq ),
inference(paramodulation,[status(thm)],[f2912,f2914]) ).
fof(f5670,plain,
! [X0] :
( seq = X0
| select(q25,X0) = select(q24,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2911,f2914]) ).
fof(f5673,plain,
( earray_125 = earray_121
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f367,f5669]) ).
fof(f5674,plain,
earray_125 = earray_121,
inference(forward_subsumption_resolution,[status(thm)],[f5673,f308]) ).
fof(f5677,plain,
! [X0] :
( select(earray_127,X0) = select(earray_121,X0)
| index_126 = X0 ),
inference(backward_demodulation,[status(thm)],[f5674,f2462]) ).
fof(f5685,plain,
! [X0] :
( seq = X0
| select(q10,X0) = select(q9,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2803,f2927]) ).
fof(f5697,plain,
( select(q26,seq) = earray_127
| tail = seq ),
inference(paramodulation,[status(thm)],[f2925,f2931]) ).
fof(f5698,plain,
! [X0] :
( seq = X0
| select(q26,X0) = select(q25,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2924,f2931]) ).
fof(f5701,plain,
( earray_131 = earray_127
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f369,f5697]) ).
fof(f5702,plain,
earray_131 = earray_127,
inference(forward_subsumption_resolution,[status(thm)],[f5701,f308]) ).
fof(f5705,plain,
! [X0] :
( select(earray_133,X0) = select(earray_127,X0)
| index_132 = X0 ),
inference(backward_demodulation,[status(thm)],[f5702,f2464]) ).
fof(f5723,plain,
( select(queue_136,seq) = earray_133
| tail = seq ),
inference(paramodulation,[status(thm)],[f2950,f3202]) ).
fof(f5724,plain,
! [X0] :
( seq = X0
| select(queue_136,X0) = select(q26,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f2949,f3202]) ).
fof(f5727,plain,
select(queue_136,seq) = earray_133,
inference(forward_subsumption_resolution,[status(thm)],[f5723,f308]) ).
fof(f5729,plain,
( select(q27,seq) = earray_133
| head = seq ),
inference(paramodulation,[status(thm)],[f5727,f3205]) ).
fof(f5730,plain,
( select(q27,tail) = index_135
| head = tail ),
inference(paramodulation,[status(thm)],[f3203,f3205]) ).
fof(f5735,plain,
( earray_140 = earray_133
| head = seq ),
inference(forward_demodulation,[status(thm)],[f372,f5729]) ).
fof(f5736,plain,
earray_140 = earray_133,
inference(forward_subsumption_resolution,[status(thm)],[f5735,f307]) ).
fof(f5737,plain,
( index_141 = index_135
| head = tail ),
inference(forward_demodulation,[status(thm)],[f438,f5730]) ).
fof(f5738,plain,
index_141 = index_135,
inference(forward_subsumption_resolution,[status(thm)],[f5737,f306]) ).
fof(f5746,plain,
! [X0] :
( select(earray_142,X0) = select(earray_133,X0)
| index_141 = X0 ),
inference(backward_demodulation,[status(thm)],[f5736,f2586]) ).
fof(f5775,plain,
index_141 = s(index_132),
inference(backward_demodulation,[status(thm)],[f5738,f435]) ).
fof(f6034,plain,
( select(q28,seq) = earray_142
| tail = seq ),
inference(paramodulation,[status(thm)],[f3210,f3212]) ).
fof(f6035,plain,
! [X0] :
( seq = X0
| select(q28,X0) = select(q27,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3209,f3212]) ).
fof(f6038,plain,
( earray_146 = earray_142
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f374,f6034]) ).
fof(f6039,plain,
earray_146 = earray_142,
inference(forward_subsumption_resolution,[status(thm)],[f6038,f308]) ).
fof(f6042,plain,
! [X0] :
( select(earray_148,X0) = select(earray_142,X0)
| index_147 = X0 ),
inference(backward_demodulation,[status(thm)],[f6039,f2588]) ).
fof(f6049,plain,
( select(q29,seq) = earray_148
| tail = seq ),
inference(paramodulation,[status(thm)],[f3322,f3324]) ).
fof(f6050,plain,
! [X0] :
( seq = X0
| select(q29,X0) = select(q28,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3321,f3324]) ).
fof(f6053,plain,
( earray_161 = earray_148
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f379,f6049]) ).
fof(f6054,plain,
earray_161 = earray_148,
inference(forward_subsumption_resolution,[status(thm)],[f6053,f308]) ).
fof(f6057,plain,
! [X0] :
( select(earray_163,X0) = select(earray_148,X0)
| index_162 = X0 ),
inference(backward_demodulation,[status(thm)],[f6054,f2632]) ).
fof(f6065,plain,
! [X0] :
( seq = X0
| select(queue_157,X0) = select(q2,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3339,f3341]) ).
fof(f6071,plain,
( select(q3,tail) = index_156
| head = tail ),
inference(paramodulation,[status(thm)],[f3342,f3344]) ).
fof(f6078,plain,
( index_171 = index_156
| head = tail ),
inference(forward_demodulation,[status(thm)],[f451,f6071]) ).
fof(f6079,plain,
index_171 = index_156,
inference(forward_subsumption_resolution,[status(thm)],[f6078,f306]) ).
fof(f6105,plain,
index_171 = s(index_153),
inference(backward_demodulation,[status(thm)],[f6079,f444]) ).
fof(f6345,plain,
( select(queue_166,seq) = earray_163
| tail = seq ),
inference(paramodulation,[status(thm)],[f3347,f3447]) ).
fof(f6346,plain,
! [X0] :
( seq = X0
| select(queue_166,X0) = select(q29,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3346,f3447]) ).
fof(f6349,plain,
select(queue_166,seq) = earray_163,
inference(forward_subsumption_resolution,[status(thm)],[f6345,f308]) ).
fof(f6351,plain,
( select(q30,seq) = earray_163
| head = seq ),
inference(paramodulation,[status(thm)],[f6349,f3450]) ).
fof(f6357,plain,
( earray_212 = earray_163
| head = seq ),
inference(forward_demodulation,[status(thm)],[f395,f6351]) ).
fof(f6358,plain,
earray_212 = earray_163,
inference(forward_subsumption_resolution,[status(thm)],[f6357,f307]) ).
fof(f6364,plain,
elem_214 = select(earray_163,index_213),
inference(backward_demodulation,[status(thm)],[f6358,f420]) ).
fof(f6379,plain,
! [X0] :
( seq = X0
| select(q4,X0) = select(q3,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3460,f3513]) ).
fof(f6394,plain,
! [X0] :
( seq = X0
| select(q5,X0) = select(q4,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3622,f3625]) ).
fof(f6409,plain,
! [X0] :
( seq = X0
| select(queue_187,X0) = select(q5,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3640,f3642]) ).
fof(f6414,plain,
( select(q11,seq) = earray_16
| tail = seq ),
inference(paramodulation,[status(thm)],[f3459,f3645]) ).
fof(f6415,plain,
! [X0] :
( seq = X0
| select(q11,X0) = select(q10,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3458,f3645]) ).
fof(f6418,plain,
( earray_20 = earray_16
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f392,f6414]) ).
fof(f6419,plain,
earray_20 = earray_16,
inference(forward_subsumption_resolution,[status(thm)],[f6418,f308]) ).
fof(f6422,plain,
! [X0] :
( select(earray_22,X0) = select(earray_16,X0)
| index_21 = X0 ),
inference(backward_demodulation,[status(thm)],[f6419,f2646]) ).
fof(f6428,plain,
( select(q6,tail) = index_186
| head = tail ),
inference(paramodulation,[status(thm)],[f3643,f3661]) ).
fof(f6435,plain,
( index_192 = index_186
| head = tail ),
inference(forward_demodulation,[status(thm)],[f460,f6428]) ).
fof(f6436,plain,
index_192 = index_186,
inference(forward_subsumption_resolution,[status(thm)],[f6435,f306]) ).
fof(f6468,plain,
index_192 = s(index_183),
inference(backward_demodulation,[status(thm)],[f6436,f457]) ).
fof(f6706,plain,
! [X0] :
( seq = X0
| select(q7,X0) = select(q6,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3861,f3864]) ).
fof(f6728,plain,
! [X0] :
( seq = X0
| select(q8,X0) = select(q7,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f3973,f3976]) ).
fof(f6743,plain,
! [X0] :
( seq = X0
| select(queue_208,X0) = select(q8,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4090,f4092]) ).
fof(f6749,plain,
( select(q9,tail) = index_207
| head = tail ),
inference(paramodulation,[status(thm)],[f4093,f4095]) ).
fof(f6756,plain,
( index_9 = index_207
| head = tail ),
inference(forward_demodulation,[status(thm)],[f497,f6749]) ).
fof(f6757,plain,
index_9 = index_207,
inference(forward_subsumption_resolution,[status(thm)],[f6756,f306]) ).
fof(f6793,plain,
index_9 = s(index_204),
inference(backward_demodulation,[status(thm)],[f6757,f465]) ).
fof(f7060,plain,
( select(queue_25,seq) = earray_22
| tail = seq ),
inference(paramodulation,[status(thm)],[f4098,f4099]) ).
fof(f7061,plain,
! [X0] :
( seq = X0
| select(queue_25,X0) = select(q11,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4097,f4099]) ).
fof(f7064,plain,
select(queue_25,seq) = earray_22,
inference(forward_subsumption_resolution,[status(thm)],[f7060,f308]) ).
fof(f7077,plain,
( select(q12,seq) = earray_22
| head = seq ),
inference(paramodulation,[status(thm)],[f7064,f4102]) ).
fof(f7078,plain,
( select(q12,tail) = index_24
| head = tail ),
inference(paramodulation,[status(thm)],[f4100,f4102]) ).
fof(f7083,plain,
( earray_29 = earray_22
| head = seq ),
inference(forward_demodulation,[status(thm)],[f397,f7077]) ).
fof(f7084,plain,
earray_29 = earray_22,
inference(forward_subsumption_resolution,[status(thm)],[f7083,f307]) ).
fof(f7085,plain,
( index_30 = index_24
| head = tail ),
inference(forward_demodulation,[status(thm)],[f474,f7078]) ).
fof(f7086,plain,
index_30 = index_24,
inference(forward_subsumption_resolution,[status(thm)],[f7085,f306]) ).
fof(f7091,plain,
! [X0] :
( select(earray_31,X0) = select(earray_22,X0)
| index_30 = X0 ),
inference(backward_demodulation,[status(thm)],[f7084,f2648]) ).
fof(f7109,plain,
s(s(s(s(index_30)))) != index_15,
inference(backward_demodulation,[status(thm)],[f7086,f3813]) ).
fof(f7112,plain,
s(s(s(index_30))) != index_15,
inference(backward_demodulation,[status(thm)],[f7086,f3812]) ).
fof(f7117,plain,
s(s(index_30)) != index_15,
inference(backward_demodulation,[status(thm)],[f7086,f3816]) ).
fof(f7118,plain,
s(index_30) != index_15,
inference(backward_demodulation,[status(thm)],[f7086,f3658]) ).
fof(f7120,plain,
index_30 != index_15,
inference(backward_demodulation,[status(thm)],[f7086,f3659]) ).
fof(f7152,plain,
s(s(s(index_36))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f7109]) ).
fof(f7153,plain,
s(s(index_42)) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f7152]) ).
fof(f7154,plain,
s(index_45) != index_15,
inference(forward_demodulation,[status(thm)],[f479,f7153]) ).
fof(f7161,plain,
s(s(index_36)) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f7112]) ).
fof(f7162,plain,
s(index_42) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f7161]) ).
fof(f7163,plain,
index_45 != index_15,
inference(forward_demodulation,[status(thm)],[f479,f7162]) ).
fof(f7169,plain,
s(index_36) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f7117]) ).
fof(f7170,plain,
index_42 != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f7169]) ).
fof(f7171,plain,
index_36 != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f7118]) ).
fof(f7384,plain,
( select(q13,seq) = earray_31
| tail = seq ),
inference(paramodulation,[status(thm)],[f4105,f4107]) ).
fof(f7385,plain,
! [X0] :
( seq = X0
| select(q13,X0) = select(q12,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4104,f4107]) ).
fof(f7388,plain,
( earray_35 = earray_31
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f399,f7384]) ).
fof(f7389,plain,
earray_35 = earray_31,
inference(forward_subsumption_resolution,[status(thm)],[f7388,f308]) ).
fof(f7392,plain,
! [X0] :
( select(earray_37,X0) = select(earray_31,X0)
| index_36 = X0 ),
inference(backward_demodulation,[status(thm)],[f7389,f2650]) ).
fof(f7399,plain,
( select(q14,seq) = earray_37
| tail = seq ),
inference(paramodulation,[status(thm)],[f4217,f4219]) ).
fof(f7400,plain,
! [X0] :
( seq = X0
| select(q14,X0) = select(q13,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4216,f4219]) ).
fof(f7403,plain,
( earray_41 = earray_37
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f402,f7399]) ).
fof(f7404,plain,
earray_41 = earray_37,
inference(forward_subsumption_resolution,[status(thm)],[f7403,f308]) ).
fof(f7407,plain,
! [X0] :
( select(earray_43,X0) = select(earray_37,X0)
| index_42 = X0 ),
inference(backward_demodulation,[status(thm)],[f7404,f2654]) ).
fof(f7414,plain,
( select(queue_46,seq) = earray_43
| tail = seq ),
inference(paramodulation,[status(thm)],[f4334,f4335]) ).
fof(f7415,plain,
! [X0] :
( seq = X0
| select(queue_46,X0) = select(q14,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4333,f4335]) ).
fof(f7418,plain,
select(queue_46,seq) = earray_43,
inference(forward_subsumption_resolution,[status(thm)],[f7414,f308]) ).
fof(f7444,plain,
( select(q15,seq) = earray_43
| head = seq ),
inference(paramodulation,[status(thm)],[f7418,f4338]) ).
fof(f7445,plain,
( select(q15,tail) = index_45
| head = tail ),
inference(paramodulation,[status(thm)],[f4336,f4338]) ).
fof(f7450,plain,
( earray_50 = earray_43
| head = seq ),
inference(forward_demodulation,[status(thm)],[f404,f7444]) ).
fof(f7451,plain,
earray_50 = earray_43,
inference(forward_subsumption_resolution,[status(thm)],[f7450,f307]) ).
fof(f7452,plain,
( index_51 = index_45
| head = tail ),
inference(forward_demodulation,[status(thm)],[f482,f7445]) ).
fof(f7453,plain,
index_51 = index_45,
inference(forward_subsumption_resolution,[status(thm)],[f7452,f306]) ).
fof(f7458,plain,
! [X0] :
( select(earray_52,X0) = select(earray_43,X0)
| index_51 = X0 ),
inference(backward_demodulation,[status(thm)],[f7451,f2656]) ).
fof(f7466,plain,
s(index_51) != index_15,
inference(backward_demodulation,[status(thm)],[f7453,f7154]) ).
fof(f7469,plain,
index_51 != index_15,
inference(backward_demodulation,[status(thm)],[f7453,f7163]) ).
fof(f7488,plain,
index_51 = s(index_42),
inference(backward_demodulation,[status(thm)],[f7453,f479]) ).
fof(f7501,plain,
index_57 != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f7466]) ).
fof(f7743,plain,
( select(q16,seq) = earray_52
| tail = seq ),
inference(paramodulation,[status(thm)],[f4343,f4345]) ).
fof(f7744,plain,
! [X0] :
( seq = X0
| select(q16,X0) = select(q15,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4342,f4345]) ).
fof(f7747,plain,
( earray_56 = earray_52
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f406,f7743]) ).
fof(f7748,plain,
earray_56 = earray_52,
inference(forward_subsumption_resolution,[status(thm)],[f7747,f308]) ).
fof(f7751,plain,
! [X0] :
( select(earray_58,X0) = select(earray_52,X0)
| index_57 = X0 ),
inference(backward_demodulation,[status(thm)],[f7748,f2658]) ).
fof(f7758,plain,
( select(q17,seq) = earray_58
| tail = seq ),
inference(paramodulation,[status(thm)],[f4349,f4457]) ).
fof(f7759,plain,
! [X0] :
( seq = X0
| select(q17,X0) = select(q16,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4348,f4457]) ).
fof(f7762,plain,
( earray_62 = earray_58
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f408,f7758]) ).
fof(f7763,plain,
earray_62 = earray_58,
inference(forward_subsumption_resolution,[status(thm)],[f7762,f308]) ).
fof(f7766,plain,
! [X0] :
( select(earray_64,X0) = select(earray_58,X0)
| index_63 = X0 ),
inference(backward_demodulation,[status(thm)],[f7763,f2660]) ).
fof(f7773,plain,
( select(queue_67,seq) = earray_64
| tail = seq ),
inference(paramodulation,[status(thm)],[f4572,f4573]) ).
fof(f7774,plain,
! [X0] :
( seq = X0
| select(queue_67,X0) = select(q17,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4571,f4573]) ).
fof(f7777,plain,
select(queue_67,seq) = earray_64,
inference(forward_subsumption_resolution,[status(thm)],[f7773,f308]) ).
fof(f7780,plain,
! [X0] :
( seq = X0
| select(q1,X0) = select(q0,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4340,f4576]) ).
fof(f7800,plain,
( select(q18,seq) = earray_64
| head = seq ),
inference(paramodulation,[status(thm)],[f7777,f4686]) ).
fof(f7801,plain,
( select(q18,tail) = index_66
| head = tail ),
inference(paramodulation,[status(thm)],[f4574,f4686]) ).
fof(f7806,plain,
( earray_71 = earray_64
| head = seq ),
inference(forward_demodulation,[status(thm)],[f410,f7800]) ).
fof(f7807,plain,
earray_71 = earray_64,
inference(forward_subsumption_resolution,[status(thm)],[f7806,f307]) ).
fof(f7808,plain,
( index_72 = index_66
| head = tail ),
inference(forward_demodulation,[status(thm)],[f491,f7801]) ).
fof(f7809,plain,
index_72 = index_66,
inference(forward_subsumption_resolution,[status(thm)],[f7808,f306]) ).
fof(f7814,plain,
! [X0] :
( select(earray_73,X0) = select(earray_64,X0)
| index_72 = X0 ),
inference(backward_demodulation,[status(thm)],[f7807,f2662]) ).
fof(f7843,plain,
index_72 = s(index_63),
inference(backward_demodulation,[status(thm)],[f7809,f488]) ).
fof(f8085,plain,
( select(q19,seq) = earray_73
| tail = seq ),
inference(paramodulation,[status(thm)],[f4689,f4691]) ).
fof(f8086,plain,
! [X0] :
( seq = X0
| select(q19,X0) = select(q18,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4688,f4691]) ).
fof(f8089,plain,
( earray_83 = earray_73
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f415,f8085]) ).
fof(f8090,plain,
earray_83 = earray_73,
inference(forward_subsumption_resolution,[status(thm)],[f8089,f308]) ).
fof(f8093,plain,
! [X0] :
( select(earray_85,X0) = select(earray_73,X0)
| index_84 = X0 ),
inference(backward_demodulation,[status(thm)],[f8090,f2666]) ).
fof(f8101,plain,
! [X0] :
( seq = X0
| select(q2,X0) = select(q1,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4800,f4803]) ).
fof(f8122,plain,
( select(q20,seq) = earray_85
| tail = seq ),
inference(paramodulation,[status(thm)],[f4807,f4821]) ).
fof(f8123,plain,
! [X0] :
( seq = X0
| select(q20,X0) = select(q19,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f4806,f4821]) ).
fof(f8126,plain,
( earray_89 = earray_85
| tail = seq ),
inference(forward_demodulation,[status(thm)],[f417,f8122]) ).
fof(f8127,plain,
earray_89 = earray_85,
inference(forward_subsumption_resolution,[status(thm)],[f8126,f308]) ).
fof(f8130,plain,
! [X0] :
( select(earray_91,X0) = select(earray_85,X0)
| index_90 = X0 ),
inference(backward_demodulation,[status(thm)],[f8127,f2668]) ).
fof(f8137,plain,
( select(queue_94,seq) = earray_91
| tail = seq ),
inference(paramodulation,[status(thm)],[f5035,f5036]) ).
fof(f8138,plain,
! [X0] :
( seq = X0
| select(queue_94,X0) = select(q20,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f5034,f5036]) ).
fof(f8141,plain,
select(queue_94,seq) = earray_91,
inference(forward_subsumption_resolution,[status(thm)],[f8137,f308]) ).
fof(f8143,plain,
( select(q21,seq) = earray_91
| head = seq ),
inference(paramodulation,[status(thm)],[f8141,f5039]) ).
fof(f8144,plain,
( select(q21,tail) = index_93
| head = tail ),
inference(paramodulation,[status(thm)],[f5037,f5039]) ).
fof(f8149,plain,
( earray_98 = earray_91
| head = seq ),
inference(forward_demodulation,[status(thm)],[f419,f8143]) ).
fof(f8150,plain,
earray_98 = earray_91,
inference(forward_subsumption_resolution,[status(thm)],[f8149,f307]) ).
fof(f8151,plain,
( index_99 = index_93
| head = tail ),
inference(forward_demodulation,[status(thm)],[f502,f8144]) ).
fof(f8152,plain,
index_99 = index_93,
inference(forward_subsumption_resolution,[status(thm)],[f8151,f306]) ).
fof(f8188,plain,
index_99 = s(index_90),
inference(backward_demodulation,[status(thm)],[f8152,f499]) ).
fof(f8734,plain,
( elem_214 = select(earray_148,index_213)
| index_162 = index_213 ),
inference(paramodulation,[status(thm)],[f6364,f6057]) ).
fof(f8738,plain,
( index_147 = index_213
| elem_214 = select(earray_142,index_213)
| index_162 = index_213 ),
inference(paramodulation,[status(thm)],[f6042,f8734]) ).
fof(f8756,plain,
( index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_133,index_213)
| index_162 = index_213 ),
inference(paramodulation,[status(thm)],[f5746,f8738]) ).
fof(f8758,plain,
( index_132 = index_213
| index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_127,index_213)
| index_162 = index_213 ),
inference(paramodulation,[status(thm)],[f5705,f8756]) ).
fof(f8760,plain,
( index_126 = index_213
| index_132 = index_213
| index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_121,index_213)
| index_162 = index_213 ),
inference(paramodulation,[status(thm)],[f5677,f8758]) ).
fof(f8762,plain,
( index_120 = index_213
| index_126 = index_213
| index_132 = index_213
| index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_112,index_213)
| index_162 = index_213 ),
inference(paramodulation,[status(thm)],[f5369,f8760]) ).
fof(f8764,plain,
( index_111 = index_213
| index_120 = index_213
| index_126 = index_213
| index_132 = index_213
| index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_106,index_213)
| index_162 = index_213 ),
inference(paramodulation,[status(thm)],[f5340,f8762]) ).
fof(f8766,plain,
( index_105 = index_213
| index_111 = index_213
| index_120 = index_213
| index_126 = index_213
| index_132 = index_213
| index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_100,index_213)
| index_162 = index_213 ),
inference(paramodulation,[status(thm)],[f5322,f8764]) ).
fof(f8922,plain,
! [X0] :
( select(earray_98,X0) = select(earray_85,X0)
| index_90 = X0 ),
inference(forward_demodulation,[status(thm)],[f8150,f8130]) ).
fof(f8924,plain,
! [X0] :
( index_84 = X0
| select(earray_98,X0) = select(earray_73,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f8093,f8922]) ).
fof(f9196,plain,
s(s(s(s(s(index_30))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3814]) ).
fof(f9197,plain,
s(s(s(s(index_36)))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f9196]) ).
fof(f9198,plain,
s(s(s(index_42))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f9197]) ).
fof(f9199,plain,
s(s(index_51)) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f9198]) ).
fof(f9200,plain,
s(index_57) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f9199]) ).
fof(f9201,plain,
index_63 != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f9200]) ).
fof(f9543,plain,
s(s(s(s(s(s(index_30)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3815]) ).
fof(f9544,plain,
s(s(s(s(s(index_36))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f9543]) ).
fof(f9545,plain,
s(s(s(s(index_42)))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f9544]) ).
fof(f9546,plain,
s(s(s(index_51))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f9545]) ).
fof(f9547,plain,
s(s(index_57)) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f9546]) ).
fof(f9548,plain,
s(index_63) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f9547]) ).
fof(f9549,plain,
index_72 != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f9548]) ).
fof(f9701,plain,
( seq = head
| select(q22,head) = index_96
| tail = head ),
inference(paramodulation,[status(thm)],[f5040,f5315]) ).
fof(f9707,plain,
( seq = head
| select(q22,head) = index_96 ),
inference(forward_subsumption_resolution,[status(thm)],[f9701,f306]) ).
fof(f9709,plain,
select(q22,head) = index_96,
inference(forward_subsumption_resolution,[status(thm)],[f9707,f307]) ).
fof(f9743,plain,
( seq = head
| index_116 = select(q23,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f427,f5350]) ).
fof(f9749,plain,
( seq = head
| index_116 = select(q23,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f9743,f306]) ).
fof(f9751,plain,
index_116 = select(q23,head),
inference(forward_subsumption_resolution,[status(thm)],[f9749,f307]) ).
fof(f9752,plain,
( seq = head
| tail = head
| index_116 = select(q22,head) ),
inference(paramodulation,[status(thm)],[f5330,f9751]) ).
fof(f9754,plain,
( seq = head
| tail = head
| index_116 = index_96 ),
inference(forward_demodulation,[status(thm)],[f9709,f9752]) ).
fof(f9755,plain,
( seq = head
| index_116 = index_96 ),
inference(forward_subsumption_resolution,[status(thm)],[f9754,f306]) ).
fof(f9768,plain,
index_116 = s(index_95),
inference(backward_demodulation,[status(thm)],[f9769,f501]) ).
fof(f9769,plain,
index_116 = index_96,
inference(forward_subsumption_resolution,[status(thm)],[f9755,f307]) ).
fof(f9914,plain,
( seq = head
| select(q10,head) = index_210
| tail = head ),
inference(paramodulation,[status(thm)],[f4096,f5685]) ).
fof(f9920,plain,
( seq = head
| select(q10,head) = index_210 ),
inference(forward_subsumption_resolution,[status(thm)],[f9914,f306]) ).
fof(f9922,plain,
select(q10,head) = index_210,
inference(forward_subsumption_resolution,[status(thm)],[f9920,f307]) ).
fof(f9984,plain,
( seq = head
| index_137 = select(q26,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f436,f5724]) ).
fof(f9990,plain,
( seq = head
| index_137 = select(q26,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f9984,f306]) ).
fof(f9992,plain,
index_137 = select(q26,head),
inference(forward_subsumption_resolution,[status(thm)],[f9990,f307]) ).
fof(f9993,plain,
( seq = head
| tail = head
| index_137 = select(q25,head) ),
inference(paramodulation,[status(thm)],[f5698,f9992]) ).
fof(f9995,plain,
( seq = head
| index_137 = select(q25,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f9993,f306]) ).
fof(f9997,plain,
index_137 = select(q25,head),
inference(forward_subsumption_resolution,[status(thm)],[f9995,f307]) ).
fof(f9998,plain,
( seq = head
| tail = head
| index_137 = select(q24,head) ),
inference(paramodulation,[status(thm)],[f5670,f9997]) ).
fof(f10000,plain,
( seq = head
| tail = head
| index_137 = index_117 ),
inference(forward_demodulation,[status(thm)],[f2910,f9998]) ).
fof(f10001,plain,
( seq = head
| index_137 = index_117 ),
inference(forward_subsumption_resolution,[status(thm)],[f10000,f306]) ).
fof(f10020,plain,
index_138 = s(index_117),
inference(backward_demodulation,[status(thm)],[f10021,f437]) ).
fof(f10021,plain,
index_137 = index_117,
inference(forward_subsumption_resolution,[status(thm)],[f10001,f307]) ).
fof(f10141,plain,
( seq = head
| index_158 = select(q2,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f445,f6065]) ).
fof(f10147,plain,
( seq = head
| index_158 = select(q2,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10141,f306]) ).
fof(f10149,plain,
index_158 = select(q2,head),
inference(forward_subsumption_resolution,[status(thm)],[f10147,f307]) ).
fof(f10160,plain,
( seq = head
| index_167 = select(q29,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f449,f6346]) ).
fof(f10166,plain,
( seq = head
| index_167 = select(q29,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10160,f306]) ).
fof(f10168,plain,
index_167 = select(q29,head),
inference(forward_subsumption_resolution,[status(thm)],[f10166,f307]) ).
fof(f10169,plain,
( seq = head
| tail = head
| index_167 = select(q28,head) ),
inference(paramodulation,[status(thm)],[f6050,f10168]) ).
fof(f10171,plain,
( seq = head
| index_167 = select(q28,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10169,f306]) ).
fof(f10173,plain,
index_167 = select(q28,head),
inference(forward_subsumption_resolution,[status(thm)],[f10171,f307]) ).
fof(f10174,plain,
( seq = head
| tail = head
| index_167 = select(q27,head) ),
inference(paramodulation,[status(thm)],[f6035,f10173]) ).
fof(f10176,plain,
( seq = head
| tail = head
| index_167 = index_138 ),
inference(forward_demodulation,[status(thm)],[f3206,f10174]) ).
fof(f10177,plain,
( seq = head
| index_167 = index_138 ),
inference(forward_subsumption_resolution,[status(thm)],[f10176,f306]) ).
fof(f10194,plain,
index_213 = s(index_138),
inference(backward_demodulation,[status(thm)],[f10198,f3457]) ).
fof(f10198,plain,
index_167 = index_138,
inference(forward_subsumption_resolution,[status(thm)],[f10177,f307]) ).
fof(f10323,plain,
( seq = head
| index_188 = select(q5,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f458,f6409]) ).
fof(f10329,plain,
( seq = head
| index_188 = select(q5,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10323,f306]) ).
fof(f10331,plain,
index_188 = select(q5,head),
inference(forward_subsumption_resolution,[status(thm)],[f10329,f307]) ).
fof(f10332,plain,
( seq = head
| tail = head
| index_188 = select(q4,head) ),
inference(paramodulation,[status(thm)],[f6394,f10331]) ).
fof(f10334,plain,
( seq = head
| index_188 = select(q4,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10332,f306]) ).
fof(f10336,plain,
index_188 = select(q4,head),
inference(forward_subsumption_resolution,[status(thm)],[f10334,f307]) ).
fof(f10337,plain,
( seq = head
| tail = head
| index_188 = select(q3,head) ),
inference(paramodulation,[status(thm)],[f6379,f10336]) ).
fof(f10339,plain,
( seq = head
| tail = head
| index_188 = index_159 ),
inference(forward_demodulation,[status(thm)],[f3345,f10337]) ).
fof(f10340,plain,
( seq = head
| index_188 = index_159 ),
inference(forward_subsumption_resolution,[status(thm)],[f10339,f306]) ).
fof(f10368,plain,
index_189 = s(index_159),
inference(backward_demodulation,[status(thm)],[f10369,f459]) ).
fof(f10369,plain,
index_188 = index_159,
inference(forward_subsumption_resolution,[status(thm)],[f10340,f307]) ).
fof(f10501,plain,
( seq = head
| index_209 = select(q8,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f466,f6743]) ).
fof(f10507,plain,
( seq = head
| index_209 = select(q8,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10501,f306]) ).
fof(f10509,plain,
index_209 = select(q8,head),
inference(forward_subsumption_resolution,[status(thm)],[f10507,f307]) ).
fof(f10510,plain,
( seq = head
| tail = head
| index_209 = select(q7,head) ),
inference(paramodulation,[status(thm)],[f6728,f10509]) ).
fof(f10512,plain,
( seq = head
| index_209 = select(q7,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10510,f306]) ).
fof(f10514,plain,
index_209 = select(q7,head),
inference(forward_subsumption_resolution,[status(thm)],[f10512,f307]) ).
fof(f10515,plain,
( seq = head
| tail = head
| index_209 = select(q6,head) ),
inference(paramodulation,[status(thm)],[f6706,f10514]) ).
fof(f10517,plain,
( seq = head
| tail = head
| index_209 = index_189 ),
inference(forward_demodulation,[status(thm)],[f3662,f10515]) ).
fof(f10518,plain,
( seq = head
| index_209 = index_189 ),
inference(forward_subsumption_resolution,[status(thm)],[f10517,f306]) ).
fof(f10531,plain,
index_210 = s(index_189),
inference(backward_demodulation,[status(thm)],[f10532,f468]) ).
fof(f10532,plain,
index_209 = index_189,
inference(forward_subsumption_resolution,[status(thm)],[f10518,f307]) ).
fof(f10648,plain,
( seq = head
| index_26 = select(q11,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f471,f7061]) ).
fof(f10654,plain,
( seq = head
| index_26 = select(q11,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10648,f306]) ).
fof(f10656,plain,
index_26 = select(q11,head),
inference(forward_subsumption_resolution,[status(thm)],[f10654,f307]) ).
fof(f10657,plain,
( seq = head
| tail = head
| index_26 = select(q10,head) ),
inference(paramodulation,[status(thm)],[f6415,f10656]) ).
fof(f10659,plain,
( seq = head
| tail = head
| index_26 = index_210 ),
inference(forward_demodulation,[status(thm)],[f9922,f10657]) ).
fof(f10660,plain,
( seq = head
| index_26 = index_210 ),
inference(forward_subsumption_resolution,[status(thm)],[f10659,f306]) ).
fof(f10672,plain,
index_27 = s(index_210),
inference(backward_demodulation,[status(thm)],[f10673,f472]) ).
fof(f10673,plain,
index_26 = index_210,
inference(forward_subsumption_resolution,[status(thm)],[f10660,f307]) ).
fof(f10802,plain,
( seq = head
| index_47 = select(q14,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f480,f7415]) ).
fof(f10808,plain,
( seq = head
| index_47 = select(q14,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10802,f306]) ).
fof(f10810,plain,
index_47 = select(q14,head),
inference(forward_subsumption_resolution,[status(thm)],[f10808,f307]) ).
fof(f10811,plain,
( seq = head
| tail = head
| index_47 = select(q13,head) ),
inference(paramodulation,[status(thm)],[f7400,f10810]) ).
fof(f10813,plain,
( seq = head
| index_47 = select(q13,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10811,f306]) ).
fof(f10815,plain,
index_47 = select(q13,head),
inference(forward_subsumption_resolution,[status(thm)],[f10813,f307]) ).
fof(f10816,plain,
( seq = head
| tail = head
| index_47 = select(q12,head) ),
inference(paramodulation,[status(thm)],[f7385,f10815]) ).
fof(f10818,plain,
( seq = head
| tail = head
| index_47 = index_27 ),
inference(forward_demodulation,[status(thm)],[f4103,f10816]) ).
fof(f10819,plain,
( seq = head
| index_47 = index_27 ),
inference(forward_subsumption_resolution,[status(thm)],[f10818,f306]) ).
fof(f10841,plain,
index_48 = s(index_27),
inference(backward_demodulation,[status(thm)],[f10842,f481]) ).
fof(f10842,plain,
index_47 = index_27,
inference(forward_subsumption_resolution,[status(thm)],[f10819,f307]) ).
fof(f10984,plain,
( seq = head
| index_68 = select(q17,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f489,f7774]) ).
fof(f10990,plain,
( seq = head
| index_68 = select(q17,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10984,f306]) ).
fof(f10992,plain,
index_68 = select(q17,head),
inference(forward_subsumption_resolution,[status(thm)],[f10990,f307]) ).
fof(f10993,plain,
( seq = head
| tail = head
| index_68 = select(q16,head) ),
inference(paramodulation,[status(thm)],[f7759,f10992]) ).
fof(f10995,plain,
( seq = head
| index_68 = select(q16,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f10993,f306]) ).
fof(f10997,plain,
index_68 = select(q16,head),
inference(forward_subsumption_resolution,[status(thm)],[f10995,f307]) ).
fof(f10998,plain,
( seq = head
| tail = head
| index_68 = select(q15,head) ),
inference(paramodulation,[status(thm)],[f7744,f10997]) ).
fof(f11000,plain,
( seq = head
| tail = head
| index_68 = index_48 ),
inference(forward_demodulation,[status(thm)],[f4339,f10998]) ).
fof(f11001,plain,
( seq = head
| index_68 = index_48 ),
inference(forward_subsumption_resolution,[status(thm)],[f11000,f306]) ).
fof(f11014,plain,
index_69 = s(index_48),
inference(backward_demodulation,[status(thm)],[f11015,f490]) ).
fof(f11015,plain,
index_68 = index_48,
inference(forward_subsumption_resolution,[status(thm)],[f11001,f307]) ).
fof(f11150,plain,
! [X0] :
( seq = X0
| tail = X0
| seq = X0
| select(q2,X0) = select(q0,X0)
| tail = X0 ),
inference(paramodulation,[status(thm)],[f7780,f8101]) ).
fof(f11154,plain,
! [X0] :
( seq = X0
| select(q2,X0) = select(q0,X0)
| tail = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f11150]) ).
fof(f11162,plain,
( seq = head
| index_95 = select(q20,head)
| tail = head ),
inference(paramodulation,[status(thm)],[f500,f8138]) ).
fof(f11168,plain,
( seq = head
| index_95 = select(q20,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f11162,f306]) ).
fof(f11170,plain,
index_95 = select(q20,head),
inference(forward_subsumption_resolution,[status(thm)],[f11168,f307]) ).
fof(f11171,plain,
( seq = head
| tail = head
| index_95 = select(q19,head) ),
inference(paramodulation,[status(thm)],[f8123,f11170]) ).
fof(f11173,plain,
( seq = head
| index_95 = select(q19,head) ),
inference(forward_subsumption_resolution,[status(thm)],[f11171,f306]) ).
fof(f11175,plain,
index_95 = select(q19,head),
inference(forward_subsumption_resolution,[status(thm)],[f11173,f307]) ).
fof(f11176,plain,
( seq = head
| tail = head
| index_95 = select(q18,head) ),
inference(paramodulation,[status(thm)],[f8086,f11175]) ).
fof(f11178,plain,
( seq = head
| tail = head
| index_95 = index_69 ),
inference(forward_demodulation,[status(thm)],[f4687,f11176]) ).
fof(f11179,plain,
( seq = head
| index_95 = index_69 ),
inference(forward_subsumption_resolution,[status(thm)],[f11178,f306]) ).
fof(f11221,plain,
index_116 = s(index_69),
inference(backward_demodulation,[status(thm)],[f11225,f9768]) ).
fof(f11225,plain,
index_95 = index_69,
inference(forward_subsumption_resolution,[status(thm)],[f11179,f307]) ).
fof(f11524,plain,
! [X0] :
( index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_64,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f7814,f8924]) ).
fof(f11633,plain,
( seq = head
| select(q2,head) = index_3
| tail = head ),
inference(paramodulation,[status(thm)],[f5305,f11154]) ).
fof(f11639,plain,
( seq = head
| index_158 = index_3
| tail = head ),
inference(forward_demodulation,[status(thm)],[f10149,f11633]) ).
fof(f11640,plain,
( seq = head
| index_158 = index_3 ),
inference(forward_subsumption_resolution,[status(thm)],[f11639,f306]) ).
fof(f11652,plain,
index_159 = s(index_3),
inference(backward_demodulation,[status(thm)],[f11653,f446]) ).
fof(f11653,plain,
index_158 = index_3,
inference(forward_subsumption_resolution,[status(thm)],[f11640,f307]) ).
fof(f11654,plain,
index_159 = index_78,
inference(forward_demodulation,[status(thm)],[f4583,f11652]) ).
fof(f11670,plain,
index_189 = s(index_78),
inference(backward_demodulation,[status(thm)],[f11654,f10368]) ).
fof(f11675,plain,
index_189 = index_153,
inference(forward_demodulation,[status(thm)],[f4815,f11670]) ).
fof(f11693,plain,
index_210 = s(index_153),
inference(backward_demodulation,[status(thm)],[f11675,f10531]) ).
fof(f11698,plain,
index_210 = index_171,
inference(forward_demodulation,[status(thm)],[f6105,f11693]) ).
fof(f11711,plain,
index_27 = s(index_171),
inference(backward_demodulation,[status(thm)],[f11698,f10672]) ).
fof(f11717,plain,
index_27 = index_177,
inference(forward_demodulation,[status(thm)],[f3520,f11711]) ).
fof(f11738,plain,
index_48 = s(index_177),
inference(backward_demodulation,[status(thm)],[f11717,f10841]) ).
fof(f11743,plain,
index_48 = index_183,
inference(forward_demodulation,[status(thm)],[f3635,f11738]) ).
fof(f11758,plain,
index_69 = s(index_183),
inference(backward_demodulation,[status(thm)],[f11743,f11014]) ).
fof(f11763,plain,
index_69 = index_192,
inference(forward_demodulation,[status(thm)],[f6468,f11758]) ).
fof(f11787,plain,
index_116 = s(index_192),
inference(backward_demodulation,[status(thm)],[f11763,f11221]) ).
fof(f11796,plain,
index_116 = index_198,
inference(forward_demodulation,[status(thm)],[f3871,f11787]) ).
fof(f11826,plain,
index_117 = s(index_198),
inference(backward_demodulation,[status(thm)],[f11796,f428]) ).
fof(f11827,plain,
index_117 = index_204,
inference(forward_demodulation,[status(thm)],[f3986,f11826]) ).
fof(f11847,plain,
index_138 = s(index_204),
inference(backward_demodulation,[status(thm)],[f11827,f10020]) ).
fof(f11852,plain,
index_138 = index_9,
inference(forward_demodulation,[status(thm)],[f6793,f11847]) ).
fof(f11878,plain,
index_213 = s(index_9),
inference(backward_demodulation,[status(thm)],[f11852,f10194]) ).
fof(f11883,plain,
index_213 = index_15,
inference(forward_demodulation,[status(thm)],[f2938,f11878]) ).
fof(f11891,plain,
( index_105 = index_15
| index_111 = index_213
| index_120 = index_213
| index_126 = index_213
| index_132 = index_213
| index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_100,index_213)
| index_162 = index_213 ),
inference(backward_demodulation,[status(thm)],[f11883,f8766]) ).
fof(f11903,plain,
( index_105 = index_15
| index_111 = index_213
| index_120 = index_213
| index_126 = index_213
| index_132 = index_213
| index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_100,index_213)
| index_162 = index_15 ),
inference(forward_demodulation,[status(thm)],[f11883,f11891]) ).
fof(f11904,plain,
( index_105 = index_15
| index_111 = index_213
| index_120 = index_213
| index_126 = index_213
| index_132 = index_213
| index_141 = index_213
| index_147 = index_213
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(forward_demodulation,[status(thm)],[f11883,f11903]) ).
fof(f11905,plain,
( index_105 = index_15
| index_111 = index_213
| index_120 = index_213
| index_126 = index_213
| index_132 = index_213
| index_141 = index_213
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(forward_demodulation,[status(thm)],[f11883,f11904]) ).
fof(f11906,plain,
( index_105 = index_15
| index_111 = index_213
| index_120 = index_213
| index_126 = index_213
| index_132 = index_213
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(forward_demodulation,[status(thm)],[f11883,f11905]) ).
fof(f11907,plain,
( index_105 = index_15
| index_111 = index_213
| index_120 = index_213
| index_126 = index_213
| index_132 = index_15
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(forward_demodulation,[status(thm)],[f11883,f11906]) ).
fof(f11908,plain,
( index_105 = index_15
| index_111 = index_213
| index_120 = index_213
| index_126 = index_15
| index_132 = index_15
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(forward_demodulation,[status(thm)],[f11883,f11907]) ).
fof(f11909,plain,
( index_105 = index_15
| index_111 = index_213
| index_120 = index_15
| index_126 = index_15
| index_132 = index_15
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(forward_demodulation,[status(thm)],[f11883,f11908]) ).
fof(f11910,plain,
( index_105 = index_15
| index_111 = index_15
| index_120 = index_15
| index_126 = index_15
| index_132 = index_15
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(forward_demodulation,[status(thm)],[f11883,f11909]) ).
fof(f12943,plain,
s(s(s(s(s(s(s(index_30))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3817]) ).
fof(f12944,plain,
s(s(s(s(s(s(index_36)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f12943]) ).
fof(f12945,plain,
s(s(s(s(s(index_42))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f12944]) ).
fof(f12946,plain,
s(s(s(s(index_51)))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f12945]) ).
fof(f12947,plain,
s(s(s(index_57))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f12946]) ).
fof(f12948,plain,
s(s(index_63)) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f12947]) ).
fof(f12949,plain,
s(index_72) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f12948]) ).
fof(f12950,plain,
index_84 != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f12949]) ).
fof(f13493,plain,
! [X0] :
( index_63 = X0
| index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_58,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f7766,f11524]) ).
fof(f14325,plain,
s(s(s(s(s(s(s(s(index_30)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3818]) ).
fof(f14326,plain,
s(s(s(s(s(s(s(index_36))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f14325]) ).
fof(f14327,plain,
s(s(s(s(s(s(index_42)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f14326]) ).
fof(f14328,plain,
s(s(s(s(s(index_51))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f14327]) ).
fof(f14329,plain,
s(s(s(s(index_57)))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f14328]) ).
fof(f14330,plain,
s(s(s(index_63))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f14329]) ).
fof(f14331,plain,
s(s(index_72)) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f14330]) ).
fof(f14332,plain,
s(index_84) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f14331]) ).
fof(f14333,plain,
index_90 != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f14332]) ).
fof(f15363,plain,
s(s(s(s(s(s(s(s(s(index_30))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3819]) ).
fof(f15364,plain,
s(s(s(s(s(s(s(s(index_36)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f15363]) ).
fof(f15365,plain,
s(s(s(s(s(s(s(index_42))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f15364]) ).
fof(f15366,plain,
s(s(s(s(s(s(index_51)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f15365]) ).
fof(f15367,plain,
s(s(s(s(s(index_57))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f15366]) ).
fof(f15368,plain,
s(s(s(s(index_63)))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f15367]) ).
fof(f15369,plain,
s(s(s(index_72))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f15368]) ).
fof(f15370,plain,
s(s(index_84)) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f15369]) ).
fof(f15371,plain,
s(index_90) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f15370]) ).
fof(f15372,plain,
index_99 != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f15371]) ).
fof(f15795,plain,
! [X0] :
( index_57 = X0
| index_63 = X0
| index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_52,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f7751,f13493]) ).
fof(f16458,plain,
s(s(s(s(s(s(s(s(s(s(index_30)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3820]) ).
fof(f16459,plain,
s(s(s(s(s(s(s(s(s(index_36))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f16458]) ).
fof(f16460,plain,
s(s(s(s(s(s(s(s(index_42)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f16459]) ).
fof(f16461,plain,
s(s(s(s(s(s(s(index_51))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f16460]) ).
fof(f16462,plain,
s(s(s(s(s(s(index_57)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f16461]) ).
fof(f16463,plain,
s(s(s(s(s(index_63))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f16462]) ).
fof(f16464,plain,
s(s(s(s(index_72)))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f16463]) ).
fof(f16465,plain,
s(s(s(index_84))) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f16464]) ).
fof(f16466,plain,
s(s(index_90)) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f16465]) ).
fof(f16467,plain,
s(index_99) != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f16466]) ).
fof(f16468,plain,
( index_111 = index_15
| index_120 = index_15
| index_126 = index_15
| index_132 = index_15
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(backward_subsumption_resolution,[status(thm)],[f11910,f16469]) ).
fof(f16469,plain,
index_105 != index_15,
inference(forward_demodulation,[status(thm)],[f2683,f16467]) ).
fof(f16905,plain,
! [X0] :
( index_51 = X0
| index_57 = X0
| index_63 = X0
| index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_43,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f7458,f15795]) ).
fof(f17672,plain,
s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3821]) ).
fof(f17673,plain,
s(s(s(s(s(s(s(s(s(s(index_36)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f17672]) ).
fof(f17674,plain,
s(s(s(s(s(s(s(s(s(index_42))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f17673]) ).
fof(f17675,plain,
s(s(s(s(s(s(s(s(index_51)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f17674]) ).
fof(f17676,plain,
s(s(s(s(s(s(s(index_57))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f17675]) ).
fof(f17677,plain,
s(s(s(s(s(s(index_63)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f17676]) ).
fof(f17678,plain,
s(s(s(s(s(index_72))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f17677]) ).
fof(f17679,plain,
s(s(s(s(index_84)))) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f17678]) ).
fof(f17680,plain,
s(s(s(index_90))) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f17679]) ).
fof(f17681,plain,
s(s(index_99)) != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f17680]) ).
fof(f17682,plain,
s(index_105) != index_15,
inference(forward_demodulation,[status(thm)],[f2683,f17681]) ).
fof(f17683,plain,
( index_120 = index_15
| index_126 = index_15
| index_132 = index_15
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(backward_subsumption_resolution,[status(thm)],[f16468,f17685]) ).
fof(f17685,plain,
index_111 != index_15,
inference(forward_demodulation,[status(thm)],[f2798,f17682]) ).
fof(f18842,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3822]) ).
fof(f18843,plain,
s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f18842]) ).
fof(f18844,plain,
s(s(s(s(s(s(s(s(s(s(index_42)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f18843]) ).
fof(f18845,plain,
s(s(s(s(s(s(s(s(s(index_51))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f18844]) ).
fof(f18846,plain,
s(s(s(s(s(s(s(s(index_57)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f18845]) ).
fof(f18847,plain,
s(s(s(s(s(s(s(index_63))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f18846]) ).
fof(f18848,plain,
s(s(s(s(s(s(index_72)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f18847]) ).
fof(f18849,plain,
s(s(s(s(s(index_84))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f18848]) ).
fof(f18850,plain,
s(s(s(s(index_90)))) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f18849]) ).
fof(f18851,plain,
s(s(s(index_99))) != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f18850]) ).
fof(f18852,plain,
s(s(index_105)) != index_15,
inference(forward_demodulation,[status(thm)],[f2683,f18851]) ).
fof(f18853,plain,
s(index_111) != index_15,
inference(forward_demodulation,[status(thm)],[f2798,f18852]) ).
fof(f18855,plain,
( index_126 = index_15
| index_132 = index_15
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(backward_subsumption_resolution,[status(thm)],[f17683,f18857]) ).
fof(f18857,plain,
index_120 != index_15,
inference(forward_demodulation,[status(thm)],[f5400,f18853]) ).
fof(f19337,plain,
! [X0] :
( index_42 = X0
| index_51 = X0
| index_57 = X0
| index_63 = X0
| index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_37,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f7407,f16905]) ).
fof(f20132,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3823]) ).
fof(f20133,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f20132]) ).
fof(f20134,plain,
s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f20133]) ).
fof(f20135,plain,
s(s(s(s(s(s(s(s(s(s(index_51)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f20134]) ).
fof(f20136,plain,
s(s(s(s(s(s(s(s(s(index_57))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f20135]) ).
fof(f20137,plain,
s(s(s(s(s(s(s(s(index_63)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f20136]) ).
fof(f20138,plain,
s(s(s(s(s(s(s(index_72))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f20137]) ).
fof(f20139,plain,
s(s(s(s(s(s(index_84)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f20138]) ).
fof(f20140,plain,
s(s(s(s(s(index_90))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f20139]) ).
fof(f20141,plain,
s(s(s(s(index_99)))) != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f20140]) ).
fof(f20142,plain,
s(s(s(index_105))) != index_15,
inference(forward_demodulation,[status(thm)],[f2683,f20141]) ).
fof(f20143,plain,
s(s(index_111)) != index_15,
inference(forward_demodulation,[status(thm)],[f2798,f20142]) ).
fof(f20144,plain,
s(index_120) != index_15,
inference(forward_demodulation,[status(thm)],[f5400,f20143]) ).
fof(f20146,plain,
( index_132 = index_15
| index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(backward_subsumption_resolution,[status(thm)],[f18855,f20149]) ).
fof(f20149,plain,
index_126 != index_15,
inference(forward_demodulation,[status(thm)],[f2921,f20144]) ).
fof(f20579,plain,
! [X0] :
( index_36 = X0
| index_42 = X0
| index_51 = X0
| index_57 = X0
| index_63 = X0
| index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_31,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f7392,f19337]) ).
fof(f21316,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3824]) ).
fof(f21317,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f21316]) ).
fof(f21318,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f21317]) ).
fof(f21319,plain,
s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f21318]) ).
fof(f21320,plain,
s(s(s(s(s(s(s(s(s(s(index_57)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f21319]) ).
fof(f21321,plain,
s(s(s(s(s(s(s(s(s(index_63))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f21320]) ).
fof(f21322,plain,
s(s(s(s(s(s(s(s(index_72)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f21321]) ).
fof(f21323,plain,
s(s(s(s(s(s(s(index_84))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f21322]) ).
fof(f21324,plain,
s(s(s(s(s(s(index_90)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f21323]) ).
fof(f21325,plain,
s(s(s(s(s(index_99))))) != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f21324]) ).
fof(f21326,plain,
s(s(s(s(index_105)))) != index_15,
inference(forward_demodulation,[status(thm)],[f2683,f21325]) ).
fof(f21327,plain,
s(s(s(index_111))) != index_15,
inference(forward_demodulation,[status(thm)],[f2798,f21326]) ).
fof(f21328,plain,
s(s(index_120)) != index_15,
inference(forward_demodulation,[status(thm)],[f5400,f21327]) ).
fof(f21329,plain,
s(index_126) != index_15,
inference(forward_demodulation,[status(thm)],[f2921,f21328]) ).
fof(f21332,plain,
( index_141 = index_15
| index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(backward_subsumption_resolution,[status(thm)],[f20146,f21335]) ).
fof(f21335,plain,
index_132 != index_15,
inference(forward_demodulation,[status(thm)],[f2946,f21329]) ).
fof(f22640,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3825]) ).
fof(f22641,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f22640]) ).
fof(f22642,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f22641]) ).
fof(f22643,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f22642]) ).
fof(f22644,plain,
s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f22643]) ).
fof(f22645,plain,
s(s(s(s(s(s(s(s(s(s(index_63)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f22644]) ).
fof(f22646,plain,
s(s(s(s(s(s(s(s(s(index_72))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f22645]) ).
fof(f22647,plain,
s(s(s(s(s(s(s(s(index_84)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f22646]) ).
fof(f22648,plain,
s(s(s(s(s(s(s(index_90))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f22647]) ).
fof(f22649,plain,
s(s(s(s(s(s(index_99)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f22648]) ).
fof(f22650,plain,
s(s(s(s(s(index_105))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2683,f22649]) ).
fof(f22651,plain,
s(s(s(s(index_111)))) != index_15,
inference(forward_demodulation,[status(thm)],[f2798,f22650]) ).
fof(f22652,plain,
s(s(s(index_120))) != index_15,
inference(forward_demodulation,[status(thm)],[f5400,f22651]) ).
fof(f22653,plain,
s(s(index_126)) != index_15,
inference(forward_demodulation,[status(thm)],[f2921,f22652]) ).
fof(f22654,plain,
s(index_132) != index_15,
inference(forward_demodulation,[status(thm)],[f2946,f22653]) ).
fof(f22657,plain,
( index_147 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(backward_subsumption_resolution,[status(thm)],[f21332,f22661]) ).
fof(f22661,plain,
index_141 != index_15,
inference(forward_demodulation,[status(thm)],[f5775,f22654]) ).
fof(f23164,plain,
! [X0] :
( index_30 = X0
| index_36 = X0
| index_42 = X0
| index_51 = X0
| index_57 = X0
| index_63 = X0
| index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_22,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f7091,f20579]) ).
fof(f23985,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3826]) ).
fof(f23986,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f23985]) ).
fof(f23987,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f23986]) ).
fof(f23988,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f23987]) ).
fof(f23989,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_57)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f23988]) ).
fof(f23990,plain,
s(s(s(s(s(s(s(s(s(s(s(index_63))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f23989]) ).
fof(f23991,plain,
s(s(s(s(s(s(s(s(s(s(index_72)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f23990]) ).
fof(f23992,plain,
s(s(s(s(s(s(s(s(s(index_84))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f23991]) ).
fof(f23993,plain,
s(s(s(s(s(s(s(s(index_90)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f23992]) ).
fof(f23994,plain,
s(s(s(s(s(s(s(index_99))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f23993]) ).
fof(f23995,plain,
s(s(s(s(s(s(index_105)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2683,f23994]) ).
fof(f23996,plain,
s(s(s(s(s(index_111))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2798,f23995]) ).
fof(f23997,plain,
s(s(s(s(index_120)))) != index_15,
inference(forward_demodulation,[status(thm)],[f5400,f23996]) ).
fof(f23998,plain,
s(s(s(index_126))) != index_15,
inference(forward_demodulation,[status(thm)],[f2921,f23997]) ).
fof(f23999,plain,
s(s(index_132)) != index_15,
inference(forward_demodulation,[status(thm)],[f2946,f23998]) ).
fof(f24000,plain,
s(index_141) != index_15,
inference(forward_demodulation,[status(thm)],[f5775,f23999]) ).
fof(f24002,plain,
( elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(backward_subsumption_resolution,[status(thm)],[f22657,f24008]) ).
fof(f24008,plain,
index_147 != index_15,
inference(forward_demodulation,[status(thm)],[f3219,f24000]) ).
fof(f24652,plain,
! [X0] :
( index_21 = X0
| index_30 = X0
| index_36 = X0
| index_42 = X0
| index_51 = X0
| index_57 = X0
| index_63 = X0
| index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_16,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f6422,f23164]) ).
fof(f25476,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7086,f3827]) ).
fof(f25477,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4114,f25476]) ).
fof(f25478,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4229,f25477]) ).
fof(f25479,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7488,f25478]) ).
fof(f25480,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4354,f25479]) ).
fof(f25481,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_63)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4466,f25480]) ).
fof(f25482,plain,
s(s(s(s(s(s(s(s(s(s(s(index_72))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f7843,f25481]) ).
fof(f25483,plain,
s(s(s(s(s(s(s(s(s(s(index_84)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4698,f25482]) ).
fof(f25484,plain,
s(s(s(s(s(s(s(s(s(index_90))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4831,f25483]) ).
fof(f25485,plain,
s(s(s(s(s(s(s(s(index_99)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f8188,f25484]) ).
fof(f25486,plain,
s(s(s(s(s(s(s(index_105))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2683,f25485]) ).
fof(f25487,plain,
s(s(s(s(s(s(index_111)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2798,f25486]) ).
fof(f25488,plain,
s(s(s(s(s(index_120))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5400,f25487]) ).
fof(f25489,plain,
s(s(s(s(index_126)))) != index_15,
inference(forward_demodulation,[status(thm)],[f2921,f25488]) ).
fof(f25490,plain,
s(s(s(index_132))) != index_15,
inference(forward_demodulation,[status(thm)],[f2946,f25489]) ).
fof(f25491,plain,
s(s(index_141)) != index_15,
inference(forward_demodulation,[status(thm)],[f5775,f25490]) ).
fof(f25492,plain,
s(index_147) != index_15,
inference(forward_demodulation,[status(thm)],[f3219,f25491]) ).
fof(f25498,plain,
elem_214 = select(earray_100,index_15),
inference(backward_subsumption_resolution,[status(thm)],[f24002,f25501]) ).
fof(f25501,plain,
index_162 != index_15,
inference(forward_demodulation,[status(thm)],[f3334,f25492]) ).
fof(f27459,plain,
( index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15
| index_57 = index_15
| index_63 = index_15
| index_72 = index_15
| index_84 = index_15
| select(earray_98,index_15) = e10
| index_90 = index_15 ),
inference(paramodulation,[status(thm)],[f606,f24652]) ).
fof(f27463,plain,
( index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15
| index_57 = index_15
| index_63 = index_15
| index_72 = index_15
| index_84 = index_15
| select(earray_98,index_15) = e10 ),
inference(forward_subsumption_resolution,[status(thm)],[f27459,f14333]) ).
fof(f27465,plain,
( index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15
| index_57 = index_15
| index_63 = index_15
| index_72 = index_15
| select(earray_98,index_15) = e10 ),
inference(forward_subsumption_resolution,[status(thm)],[f27463,f12950]) ).
fof(f27466,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15
| index_57 = index_15
| index_63 = index_15
| index_72 = index_15
| select(earray_100,index_15) = e10 ),
inference(paramodulation,[status(thm)],[f2454,f27465]) ).
fof(f27468,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15
| index_57 = index_15
| index_63 = index_15
| index_72 = index_15
| elem_214 = e10 ),
inference(forward_demodulation,[status(thm)],[f25498,f27466]) ).
fof(f27469,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15
| index_57 = index_15
| index_63 = index_15
| index_72 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f27468,f605]) ).
fof(f27472,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15
| index_57 = index_15
| index_63 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f27469,f9549]) ).
fof(f27473,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15
| index_57 = index_15 ),
inference(resolution,[status(thm)],[f27472,f9201]) ).
fof(f27505,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15
| index_51 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f27473,f7501]) ).
fof(f27516,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15
| index_42 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f27505,f7469]) ).
fof(f27517,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15 ),
inference(resolution,[status(thm)],[f27516,f7170]) ).
fof(f27547,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f27517,f7171]) ).
fof(f27560,plain,
( index_99 = index_15
| index_21 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f27547,f7120]) ).
fof(f27561,plain,
index_99 = index_15,
inference(resolution,[status(thm)],[f27560,f3654]) ).
fof(f27587,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f27561,f15372]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV569-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 09:10:09 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 9.16/1.56 % Refutation found
% 9.16/1.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.16/1.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 9.16/1.60 % Elapsed time: 1.299823 seconds
% 9.16/1.60 % CPU time: 10.031742 seconds
% 9.16/1.60 % Total memory used: 330.274 MB
% 9.16/1.60 % Net memory used: 326.888 MB
%------------------------------------------------------------------------------