%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:06 PM UTC 2026
% Result : Unsatisfiable 9.34s 6.65s
% Output : CNFRefutation 9.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 255
% Syntax : Number of formulae : 1224 (1146 unt; 0 def)
% Number of atoms : 1422 (1421 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 448 ( 250 ~; 198 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 1 avg)
% Maximal term depth : 20 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 267 ( 267 usr; 258 con; 0-3 aty)
% Number of variables : 135 ( 135 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,E] : rselect_seq(rstore_seq(A,E)) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,E] : rselect_head(rstore_head(A,E)) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,E] : rselect_tail(rstore_tail(A,E)) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,E] : rselect_seq(rstore_head(A,E)) = rselect_seq(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,E] : rselect_seq(rstore_tail(A,E)) = rselect_seq(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,E] : rselect_head(rstore_tail(A,E)) = rselect_head(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,E] : rselect_head(rstore_seq(A,E)) = rselect_head(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,E] : rselect_tail(rstore_head(A,E)) = rselect_tail(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(s(X))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X] : s(s(s(s(s(s(s(s(s(s(X)))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X] : s(s(s(s(s(s(s(s(s(X))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [X] : s(s(s(s(s(s(s(s(X)))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] : s(s(s(s(s(s(s(X))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [X] : s(s(s(s(s(s(X)))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [X] : s(s(s(s(s(X))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [X] : s(s(s(s(X)))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [X] : s(s(s(X))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [X] : s(s(X)) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [X] : s(X) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,hypothesis,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,hypothesis,
earray_104 = rselect_seq(q22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,hypothesis,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,hypothesis,
earray_110 = rselect_seq(q23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,hypothesis,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,hypothesis,
earray_119 = rselect_seq(q24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,hypothesis,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f70,hypothesis,
earray_125 = rselect_seq(q25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,hypothesis,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,hypothesis,
earray_131 = rselect_seq(q26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
earray_140 = rselect_seq(q27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,hypothesis,
earray_146 = rselect_seq(q28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
earray_16 = store(earray_14,index_15,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,hypothesis,
earray_161 = rselect_seq(q29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,hypothesis,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,hypothesis,
earray_20 = rselect_seq(q11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,hypothesis,
earray_212 = rselect_seq(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,hypothesis,
earray_22 = store(earray_20,index_21,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,hypothesis,
earray_29 = rselect_seq(q12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,hypothesis,
earray_31 = store(earray_29,index_30,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,hypothesis,
earray_35 = rselect_seq(q13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f103,hypothesis,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,hypothesis,
earray_41 = rselect_seq(q14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,hypothesis,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
earray_50 = rselect_seq(q15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,hypothesis,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,hypothesis,
earray_56 = rselect_seq(q16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,hypothesis,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
earray_62 = rselect_seq(q17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,hypothesis,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
earray_71 = rselect_seq(q18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f117,hypothesis,
earray_8 = rselect_seq(q9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
earray_83 = rselect_seq(q19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,hypothesis,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,hypothesis,
earray_89 = rselect_seq(q20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f121,hypothesis,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,hypothesis,
earray_98 = rselect_seq(q21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,hypothesis,
elem_214 = select(earray_212,index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,hypothesis,
index_0 = rselect_tail(q),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,hypothesis,
index_105 = rselect_tail(q22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,hypothesis,
index_111 = rselect_tail(q23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,hypothesis,
index_116 = rselect_head(queue_115),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,hypothesis,
index_117 = s(index_116),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,hypothesis,
index_120 = rselect_tail(q24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,hypothesis,
index_123 = s(index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f135,hypothesis,
index_126 = rselect_tail(q25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,hypothesis,
index_129 = s(index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,hypothesis,
index_132 = rselect_tail(q26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,hypothesis,
index_135 = s(index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,hypothesis,
index_137 = rselect_head(queue_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,hypothesis,
index_138 = s(index_137),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,hypothesis,
index_141 = rselect_tail(q27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f143,hypothesis,
index_147 = rselect_tail(q28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,hypothesis,
index_15 = rselect_tail(q10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f146,hypothesis,
index_153 = rselect_tail(q2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f147,hypothesis,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f148,hypothesis,
index_158 = rselect_head(queue_157),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,hypothesis,
index_159 = s(index_158),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,hypothesis,
index_162 = rselect_tail(q29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,hypothesis,
index_167 = rselect_head(queue_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,hypothesis,
index_168 = s(index_167),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,hypothesis,
index_171 = rselect_tail(q3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f155,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,hypothesis,
index_177 = rselect_tail(q4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f157,hypothesis,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,hypothesis,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f159,hypothesis,
index_183 = rselect_tail(q5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f160,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,hypothesis,
index_188 = rselect_head(queue_187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,hypothesis,
index_189 = s(index_188),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f163,hypothesis,
index_192 = rselect_tail(q6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,hypothesis,
index_195 = s(index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f165,hypothesis,
index_198 = rselect_tail(q7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f166,hypothesis,
index_201 = s(index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,hypothesis,
index_204 = rselect_tail(q8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,hypothesis,
index_207 = s(index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,hypothesis,
index_209 = rselect_head(queue_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,hypothesis,
index_21 = rselect_tail(q11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,hypothesis,
index_210 = s(index_209),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,hypothesis,
index_213 = rselect_head(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,hypothesis,
index_26 = rselect_head(queue_25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,hypothesis,
index_27 = s(index_26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f176,hypothesis,
index_3 = rselect_tail(q0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f177,hypothesis,
index_30 = rselect_tail(q12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,hypothesis,
index_33 = s(index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f179,hypothesis,
index_36 = rselect_tail(q13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,hypothesis,
index_39 = s(index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,hypothesis,
index_42 = rselect_tail(q14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,hypothesis,
index_45 = s(index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f183,hypothesis,
index_47 = rselect_head(queue_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f184,hypothesis,
index_48 = s(index_47),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f185,hypothesis,
index_51 = rselect_tail(q15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,hypothesis,
index_57 = rselect_tail(q16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f190,hypothesis,
index_63 = rselect_tail(q17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f191,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,hypothesis,
index_68 = rselect_head(queue_67),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,hypothesis,
index_69 = s(index_68),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,hypothesis,
index_72 = rselect_tail(q18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,hypothesis,
index_75 = s(index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f196,hypothesis,
index_78 = rselect_tail(q1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,hypothesis,
index_81 = s(index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f198,hypothesis,
index_84 = rselect_tail(q19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,hypothesis,
index_87 = s(index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,hypothesis,
index_9 = rselect_tail(q9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f201,hypothesis,
index_90 = rselect_tail(q20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f202,hypothesis,
index_93 = s(index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f203,hypothesis,
index_95 = rselect_head(queue_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f204,hypothesis,
index_96 = s(index_95),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,hypothesis,
index_99 = rselect_tail(q21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,hypothesis,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f207,hypothesis,
queue_101 = rstore_seq(q21,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f208,hypothesis,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f209,hypothesis,
queue_107 = rstore_seq(q22,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,hypothesis,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f211,hypothesis,
queue_11 = rstore_seq(q9,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f212,hypothesis,
queue_113 = rstore_seq(q23,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f213,hypothesis,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f214,hypothesis,
queue_118 = rstore_head(queue_115,index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f215,hypothesis,
queue_122 = rstore_seq(q24,earray_121),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f216,hypothesis,
queue_124 = rstore_tail(queue_122,index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f217,hypothesis,
queue_128 = rstore_seq(q25,earray_127),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f218,hypothesis,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f219,hypothesis,
queue_130 = rstore_tail(queue_128,index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,hypothesis,
queue_134 = rstore_seq(q26,earray_133),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f221,hypothesis,
queue_136 = rstore_tail(queue_134,index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f222,hypothesis,
queue_139 = rstore_head(queue_136,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f223,hypothesis,
queue_143 = rstore_seq(q27,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f224,hypothesis,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f225,hypothesis,
queue_149 = rstore_seq(q28,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f226,hypothesis,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f227,hypothesis,
queue_155 = rstore_seq(q2,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f228,hypothesis,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f229,hypothesis,
queue_160 = rstore_head(queue_157,index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f230,hypothesis,
queue_164 = rstore_seq(q29,earray_163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f231,hypothesis,
queue_166 = rstore_tail(queue_164,index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f232,hypothesis,
queue_169 = rstore_head(queue_166,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f233,hypothesis,
queue_17 = rstore_seq(q10,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f234,hypothesis,
queue_173 = rstore_seq(q3,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f235,hypothesis,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f236,hypothesis,
queue_179 = rstore_seq(q4,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f237,hypothesis,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f238,hypothesis,
queue_185 = rstore_seq(q5,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f239,hypothesis,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f240,hypothesis,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f241,hypothesis,
queue_190 = rstore_head(queue_187,index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f242,hypothesis,
queue_194 = rstore_seq(q6,earray_193),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f243,hypothesis,
queue_196 = rstore_tail(queue_194,index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f244,hypothesis,
queue_200 = rstore_seq(q7,earray_199),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f245,hypothesis,
queue_202 = rstore_tail(queue_200,index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f246,hypothesis,
queue_206 = rstore_seq(q8,earray_205),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f247,hypothesis,
queue_208 = rstore_tail(queue_206,index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f248,hypothesis,
queue_211 = rstore_head(queue_208,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f249,hypothesis,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f250,hypothesis,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f251,hypothesis,
queue_28 = rstore_head(queue_25,index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f252,hypothesis,
queue_32 = rstore_seq(q12,earray_31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f253,hypothesis,
queue_34 = rstore_tail(queue_32,index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f254,hypothesis,
queue_38 = rstore_seq(q13,earray_37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f255,hypothesis,
queue_40 = rstore_tail(queue_38,index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f256,hypothesis,
queue_44 = rstore_seq(q14,earray_43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f257,hypothesis,
queue_46 = rstore_tail(queue_44,index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f258,hypothesis,
queue_49 = rstore_head(queue_46,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f259,hypothesis,
queue_5 = rstore_seq(q0,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f260,hypothesis,
queue_53 = rstore_seq(q15,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f261,hypothesis,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f262,hypothesis,
queue_59 = rstore_seq(q16,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f263,hypothesis,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f264,hypothesis,
queue_65 = rstore_seq(q17,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f265,hypothesis,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f266,hypothesis,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f267,hypothesis,
queue_70 = rstore_head(queue_67,index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f268,hypothesis,
queue_74 = rstore_seq(q18,earray_73),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f269,hypothesis,
queue_76 = rstore_tail(queue_74,index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f270,hypothesis,
queue_80 = rstore_seq(q1,earray_79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f271,hypothesis,
queue_82 = rstore_tail(queue_80,index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f272,hypothesis,
queue_86 = rstore_seq(q19,earray_85),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f273,hypothesis,
queue_88 = rstore_tail(queue_86,index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f274,hypothesis,
queue_92 = rstore_seq(q20,earray_91),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f275,hypothesis,
queue_94 = rstore_tail(queue_92,index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f276,hypothesis,
queue_97 = rstore_head(queue_94,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f277,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f278,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f279,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f280,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f281,hypothesis,
q12 = queue_28,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f282,hypothesis,
q13 = queue_34,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f283,hypothesis,
q14 = queue_40,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f284,hypothesis,
q15 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f285,hypothesis,
q16 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f286,hypothesis,
q17 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f287,hypothesis,
q18 = queue_70,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f288,hypothesis,
q19 = queue_76,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f289,hypothesis,
q2 = queue_82,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f290,hypothesis,
q20 = queue_88,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f291,hypothesis,
q21 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f292,hypothesis,
q22 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f293,hypothesis,
q23 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f294,hypothesis,
q24 = queue_118,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f295,hypothesis,
q25 = queue_124,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f296,hypothesis,
q26 = queue_130,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f297,hypothesis,
q27 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f298,hypothesis,
q28 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f299,hypothesis,
q29 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f300,hypothesis,
q3 = queue_160,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f301,hypothesis,
q30 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f302,hypothesis,
q4 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f303,hypothesis,
q5 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f304,hypothesis,
q6 = queue_190,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f305,hypothesis,
q7 = queue_196,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f306,hypothesis,
q8 = queue_202,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f307,hypothesis,
q9 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f308,negated_conjecture,
elem_214 != e10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f309,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f310,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f311,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f312,plain,
! [X0,X1] : rselect_seq(rstore_seq(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f313,plain,
! [X0,X1] : rselect_head(rstore_head(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f314,plain,
! [X0,X1] : rselect_tail(rstore_tail(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f315,plain,
! [X0,X1] : rselect_seq(rstore_head(X0,X1)) = rselect_seq(X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f316,plain,
! [X0,X1] : rselect_seq(rstore_tail(X0,X1)) = rselect_seq(X0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f317,plain,
! [X0,X1] : rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f318,plain,
! [X0,X1] : rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f320,plain,
! [X0,X1] : rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f352,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)],[f43]) ).
fof(f353,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)],[f44]) ).
fof(f354,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)],[f45]) ).
fof(f355,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)],[f46]) ).
fof(f356,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f357,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f358,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f359,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f360,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f361,plain,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f362,plain,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f363,plain,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f364,plain,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f365,plain,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f366,plain,
! [X0] : s(s(s(s(s(X0))))) != X0,
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f367,plain,
! [X0] : s(s(s(s(X0)))) != X0,
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f368,plain,
! [X0] : s(s(s(X0))) != X0,
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f369,plain,
! [X0] : s(s(X0)) != X0,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f370,plain,
! [X0] : s(X0) != X0,
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f372,plain,
earray_100 = store(earray_98,index_99,e21),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f373,plain,
earray_104 = rselect_seq(q22),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f374,plain,
earray_106 = store(earray_104,index_105,e22),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f375,plain,
earray_110 = rselect_seq(q23),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f376,plain,
earray_112 = store(earray_110,index_111,e23),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f377,plain,
earray_119 = rselect_seq(q24),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f378,plain,
earray_121 = store(earray_119,index_120,e24),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f379,plain,
earray_125 = rselect_seq(q25),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f380,plain,
earray_127 = store(earray_125,index_126,e25),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f381,plain,
earray_131 = rselect_seq(q26),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f382,plain,
earray_133 = store(earray_131,index_132,e26),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f384,plain,
earray_140 = rselect_seq(q27),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f385,plain,
earray_142 = store(earray_140,index_141,e27),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f386,plain,
earray_146 = rselect_seq(q28),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f387,plain,
earray_148 = store(earray_146,index_147,e28),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f390,plain,
earray_16 = store(earray_14,index_15,e10),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f391,plain,
earray_161 = rselect_seq(q29),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f392,plain,
earray_163 = store(earray_161,index_162,e29),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f404,plain,
earray_20 = rselect_seq(q11),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f407,plain,
earray_212 = rselect_seq(q30),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f408,plain,
earray_22 = store(earray_20,index_21,e11),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f409,plain,
earray_29 = rselect_seq(q12),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f410,plain,
earray_31 = store(earray_29,index_30,e12),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f411,plain,
earray_35 = rselect_seq(q13),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f412,plain,
earray_37 = store(earray_35,index_36,e13),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f414,plain,
earray_41 = rselect_seq(q14),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f415,plain,
earray_43 = store(earray_41,index_42,e14),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f416,plain,
earray_50 = rselect_seq(q15),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f417,plain,
earray_52 = store(earray_50,index_51,e15),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f418,plain,
earray_56 = rselect_seq(q16),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f419,plain,
earray_58 = store(earray_56,index_57,e16),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f420,plain,
earray_62 = rselect_seq(q17),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f421,plain,
earray_64 = store(earray_62,index_63,e17),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f422,plain,
earray_71 = rselect_seq(q18),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f423,plain,
earray_73 = store(earray_71,index_72,e18),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f426,plain,
earray_8 = rselect_seq(q9),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f427,plain,
earray_83 = rselect_seq(q19),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f428,plain,
earray_85 = store(earray_83,index_84,e19),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f429,plain,
earray_89 = rselect_seq(q20),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f430,plain,
earray_91 = store(earray_89,index_90,e20),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f431,plain,
earray_98 = rselect_seq(q21),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f432,plain,
elem_214 = select(earray_212,index_213),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f433,plain,
index_0 = rselect_tail(q),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f434,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f435,plain,
index_105 = rselect_tail(q22),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f436,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f437,plain,
index_111 = rselect_tail(q23),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f438,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f439,plain,
index_116 = rselect_head(queue_115),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f440,plain,
index_117 = s(index_116),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f441,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f442,plain,
index_120 = rselect_tail(q24),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f443,plain,
index_123 = s(index_120),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f444,plain,
index_126 = rselect_tail(q25),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f445,plain,
index_129 = s(index_126),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f446,plain,
index_132 = rselect_tail(q26),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f447,plain,
index_135 = s(index_132),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f448,plain,
index_137 = rselect_head(queue_136),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f449,plain,
index_138 = s(index_137),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f450,plain,
index_141 = rselect_tail(q27),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f451,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f452,plain,
index_147 = rselect_tail(q28),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f453,plain,
index_15 = rselect_tail(q10),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f454,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f455,plain,
index_153 = rselect_tail(q2),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f456,plain,
index_156 = s(index_153),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f457,plain,
index_158 = rselect_head(queue_157),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f458,plain,
index_159 = s(index_158),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f459,plain,
index_162 = rselect_tail(q29),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f461,plain,
index_167 = rselect_head(queue_166),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f462,plain,
index_168 = s(index_167),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f463,plain,
index_171 = rselect_tail(q3),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f464,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f465,plain,
index_177 = rselect_tail(q4),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f466,plain,
index_18 = s(index_15),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f467,plain,
index_180 = s(index_177),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f468,plain,
index_183 = rselect_tail(q5),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f469,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f470,plain,
index_188 = rselect_head(queue_187),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f471,plain,
index_189 = s(index_188),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f472,plain,
index_192 = rselect_tail(q6),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f473,plain,
index_195 = s(index_192),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f474,plain,
index_198 = rselect_tail(q7),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f475,plain,
index_201 = s(index_198),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f476,plain,
index_204 = rselect_tail(q8),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f477,plain,
index_207 = s(index_204),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f478,plain,
index_209 = rselect_head(queue_208),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f479,plain,
index_21 = rselect_tail(q11),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f480,plain,
index_210 = s(index_209),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f481,plain,
index_213 = rselect_head(q30),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f482,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f483,plain,
index_26 = rselect_head(queue_25),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f484,plain,
index_27 = s(index_26),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f485,plain,
index_3 = rselect_tail(q0),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f486,plain,
index_30 = rselect_tail(q12),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f487,plain,
index_33 = s(index_30),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f488,plain,
index_36 = rselect_tail(q13),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f489,plain,
index_39 = s(index_36),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f490,plain,
index_42 = rselect_tail(q14),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f491,plain,
index_45 = s(index_42),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f492,plain,
index_47 = rselect_head(queue_46),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f493,plain,
index_48 = s(index_47),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f494,plain,
index_51 = rselect_tail(q15),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f495,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f496,plain,
index_57 = rselect_tail(q16),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f497,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f498,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f499,plain,
index_63 = rselect_tail(q17),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f500,plain,
index_66 = s(index_63),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f501,plain,
index_68 = rselect_head(queue_67),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f502,plain,
index_69 = s(index_68),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f503,plain,
index_72 = rselect_tail(q18),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f504,plain,
index_75 = s(index_72),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f505,plain,
index_78 = rselect_tail(q1),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f506,plain,
index_81 = s(index_78),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f507,plain,
index_84 = rselect_tail(q19),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f508,plain,
index_87 = s(index_84),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f509,plain,
index_9 = rselect_tail(q9),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f510,plain,
index_90 = rselect_tail(q20),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f511,plain,
index_93 = s(index_90),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f512,plain,
index_95 = rselect_head(queue_94),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f513,plain,
index_96 = s(index_95),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f514,plain,
index_99 = rselect_tail(q21),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f515,plain,
queue_1 = rstore_head(q,index_0),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f516,plain,
queue_101 = rstore_seq(q21,earray_100),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f517,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f518,plain,
queue_107 = rstore_seq(q22,earray_106),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f519,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(cnf_transformation,[status(thm)],[f210]) ).
fof(f520,plain,
queue_11 = rstore_seq(q9,earray_10),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f521,plain,
queue_113 = rstore_seq(q23,earray_112),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f522,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f523,plain,
queue_118 = rstore_head(queue_115,index_117),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f524,plain,
queue_122 = rstore_seq(q24,earray_121),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f525,plain,
queue_124 = rstore_tail(queue_122,index_123),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f526,plain,
queue_128 = rstore_seq(q25,earray_127),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f527,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f528,plain,
queue_130 = rstore_tail(queue_128,index_129),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f529,plain,
queue_134 = rstore_seq(q26,earray_133),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f530,plain,
queue_136 = rstore_tail(queue_134,index_135),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f531,plain,
queue_139 = rstore_head(queue_136,index_138),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f532,plain,
queue_143 = rstore_seq(q27,earray_142),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f533,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f534,plain,
queue_149 = rstore_seq(q28,earray_148),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f535,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f536,plain,
queue_155 = rstore_seq(q2,earray_154),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f537,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f538,plain,
queue_160 = rstore_head(queue_157,index_159),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f539,plain,
queue_164 = rstore_seq(q29,earray_163),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f540,plain,
queue_166 = rstore_tail(queue_164,index_165),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f541,plain,
queue_169 = rstore_head(queue_166,index_168),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f542,plain,
queue_17 = rstore_seq(q10,earray_16),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f543,plain,
queue_173 = rstore_seq(q3,earray_172),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f544,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f545,plain,
queue_179 = rstore_seq(q4,earray_178),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f546,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f547,plain,
queue_185 = rstore_seq(q5,earray_184),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f548,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f549,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f550,plain,
queue_190 = rstore_head(queue_187,index_189),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f551,plain,
queue_194 = rstore_seq(q6,earray_193),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f552,plain,
queue_196 = rstore_tail(queue_194,index_195),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f553,plain,
queue_200 = rstore_seq(q7,earray_199),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f554,plain,
queue_202 = rstore_tail(queue_200,index_201),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f555,plain,
queue_206 = rstore_seq(q8,earray_205),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f556,plain,
queue_208 = rstore_tail(queue_206,index_207),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f557,plain,
queue_211 = rstore_head(queue_208,index_210),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f558,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f559,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f560,plain,
queue_28 = rstore_head(queue_25,index_27),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f561,plain,
queue_32 = rstore_seq(q12,earray_31),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f562,plain,
queue_34 = rstore_tail(queue_32,index_33),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f563,plain,
queue_38 = rstore_seq(q13,earray_37),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f564,plain,
queue_40 = rstore_tail(queue_38,index_39),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f565,plain,
queue_44 = rstore_seq(q14,earray_43),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f566,plain,
queue_46 = rstore_tail(queue_44,index_45),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f567,plain,
queue_49 = rstore_head(queue_46,index_48),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f568,plain,
queue_5 = rstore_seq(q0,earray_4),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f569,plain,
queue_53 = rstore_seq(q15,earray_52),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f570,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f571,plain,
queue_59 = rstore_seq(q16,earray_58),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f572,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f573,plain,
queue_65 = rstore_seq(q17,earray_64),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f574,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f575,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f576,plain,
queue_70 = rstore_head(queue_67,index_69),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f577,plain,
queue_74 = rstore_seq(q18,earray_73),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f578,plain,
queue_76 = rstore_tail(queue_74,index_75),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f579,plain,
queue_80 = rstore_seq(q1,earray_79),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f580,plain,
queue_82 = rstore_tail(queue_80,index_81),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f581,plain,
queue_86 = rstore_seq(q19,earray_85),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f582,plain,
queue_88 = rstore_tail(queue_86,index_87),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f583,plain,
queue_92 = rstore_seq(q20,earray_91),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f584,plain,
queue_94 = rstore_tail(queue_92,index_93),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f585,plain,
queue_97 = rstore_head(queue_94,index_96),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f586,plain,
q0 = queue_1,
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f587,plain,
q1 = queue_7,
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f588,plain,
q10 = queue_13,
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f589,plain,
q11 = queue_19,
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f590,plain,
q12 = queue_28,
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f591,plain,
q13 = queue_34,
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f592,plain,
q14 = queue_40,
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f593,plain,
q15 = queue_49,
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f594,plain,
q16 = queue_55,
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f595,plain,
q17 = queue_61,
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f596,plain,
q18 = queue_70,
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f597,plain,
q19 = queue_76,
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f598,plain,
q2 = queue_82,
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f599,plain,
q20 = queue_88,
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f600,plain,
q21 = queue_97,
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f601,plain,
q22 = queue_103,
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f602,plain,
q23 = queue_109,
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f603,plain,
q24 = queue_118,
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f604,plain,
q25 = queue_124,
inference(cnf_transformation,[status(thm)],[f295]) ).
fof(f605,plain,
q26 = queue_130,
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f606,plain,
q27 = queue_139,
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f607,plain,
q28 = queue_145,
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f608,plain,
q29 = queue_151,
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f609,plain,
q3 = queue_160,
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f610,plain,
q30 = queue_169,
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f611,plain,
q4 = queue_175,
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f612,plain,
q5 = queue_181,
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f613,plain,
q6 = queue_190,
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f614,plain,
q7 = queue_196,
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f615,plain,
q8 = queue_202,
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f616,plain,
q9 = queue_211,
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f617,plain,
elem_214 != e10,
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f618,plain,
select(earray_16,index_15) = e10,
inference(paramodulation,[status(thm)],[f390,f309]) ).
fof(f1368,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f466,f356]) ).
fof(f1369,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f466,f355]) ).
fof(f1370,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f466,f354]) ).
fof(f1371,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f466,f353]) ).
fof(f1372,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f466,f352]) ).
fof(f1402,plain,
s(index_18) != index_15,
inference(paramodulation,[status(thm)],[f466,f369]) ).
fof(f1405,plain,
index_18 != index_15,
inference(paramodulation,[status(thm)],[f466,f370]) ).
fof(f1626,plain,
! [X0] :
( select(earray_100,X0) = select(earray_98,X0)
| index_99 = X0 ),
inference(paramodulation,[status(thm)],[f372,f311]) ).
fof(f1728,plain,
! [X0] :
( select(earray_106,X0) = select(earray_104,X0)
| index_105 = X0 ),
inference(paramodulation,[status(thm)],[f374,f311]) ).
fof(f1730,plain,
! [X0] :
( select(earray_112,X0) = select(earray_110,X0)
| index_111 = X0 ),
inference(paramodulation,[status(thm)],[f376,f311]) ).
fof(f1732,plain,
! [X0] :
( select(earray_121,X0) = select(earray_119,X0)
| index_120 = X0 ),
inference(paramodulation,[status(thm)],[f378,f311]) ).
fof(f1784,plain,
! [X0] :
( select(earray_127,X0) = select(earray_125,X0)
| index_126 = X0 ),
inference(paramodulation,[status(thm)],[f380,f311]) ).
fof(f1836,plain,
! [X0] :
( select(earray_133,X0) = select(earray_131,X0)
| index_132 = X0 ),
inference(paramodulation,[status(thm)],[f382,f311]) ).
fof(f1838,plain,
! [X0] :
( select(earray_142,X0) = select(earray_140,X0)
| index_141 = X0 ),
inference(paramodulation,[status(thm)],[f385,f311]) ).
fof(f1940,plain,
! [X0] :
( select(earray_148,X0) = select(earray_146,X0)
| index_147 = X0 ),
inference(paramodulation,[status(thm)],[f387,f311]) ).
fof(f1944,plain,
! [X0] :
( select(earray_163,X0) = select(earray_161,X0)
| index_162 = X0 ),
inference(paramodulation,[status(thm)],[f392,f311]) ).
fof(f2158,plain,
! [X0] :
( select(earray_22,X0) = select(earray_20,X0)
| index_21 = X0 ),
inference(paramodulation,[status(thm)],[f408,f311]) ).
fof(f2210,plain,
! [X0] :
( select(earray_31,X0) = select(earray_29,X0)
| index_30 = X0 ),
inference(paramodulation,[status(thm)],[f410,f311]) ).
fof(f2212,plain,
! [X0] :
( select(earray_37,X0) = select(earray_35,X0)
| index_36 = X0 ),
inference(paramodulation,[status(thm)],[f412,f311]) ).
fof(f2366,plain,
! [X0] :
( select(earray_43,X0) = select(earray_41,X0)
| index_42 = X0 ),
inference(paramodulation,[status(thm)],[f415,f311]) ).
fof(f2368,plain,
! [X0] :
( select(earray_52,X0) = select(earray_50,X0)
| index_51 = X0 ),
inference(paramodulation,[status(thm)],[f417,f311]) ).
fof(f2370,plain,
! [X0] :
( select(earray_58,X0) = select(earray_56,X0)
| index_57 = X0 ),
inference(paramodulation,[status(thm)],[f419,f311]) ).
fof(f2472,plain,
! [X0] :
( select(earray_64,X0) = select(earray_62,X0)
| index_63 = X0 ),
inference(paramodulation,[status(thm)],[f421,f311]) ).
fof(f2474,plain,
! [X0] :
( select(earray_73,X0) = select(earray_71,X0)
| index_72 = X0 ),
inference(paramodulation,[status(thm)],[f423,f311]) ).
fof(f2578,plain,
! [X0] :
( select(earray_85,X0) = select(earray_83,X0)
| index_84 = X0 ),
inference(paramodulation,[status(thm)],[f428,f311]) ).
fof(f2580,plain,
! [X0] :
( select(earray_91,X0) = select(earray_89,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f430,f311]) ).
fof(f2682,plain,
q0 = rstore_head(q,index_0),
inference(forward_demodulation,[status(thm)],[f586,f515]) ).
fof(f2683,plain,
rselect_tail(q0) = rselect_tail(q),
inference(paramodulation,[status(thm)],[f2682,f320]) ).
fof(f2685,plain,
rselect_head(q0) = index_0,
inference(paramodulation,[status(thm)],[f2682,f313]) ).
fof(f2686,plain,
index_3 = rselect_tail(q),
inference(forward_demodulation,[status(thm)],[f485,f2683]) ).
fof(f2689,plain,
rselect_head(queue_101) = rselect_head(q21),
inference(paramodulation,[status(thm)],[f516,f318]) ).
fof(f2690,plain,
rselect_seq(queue_101) = earray_100,
inference(paramodulation,[status(thm)],[f516,f312]) ).
fof(f2692,plain,
q22 = rstore_tail(queue_101,index_102),
inference(forward_demodulation,[status(thm)],[f601,f517]) ).
fof(f2693,plain,
rselect_head(q22) = rselect_head(queue_101),
inference(paramodulation,[status(thm)],[f2692,f317]) ).
fof(f2694,plain,
rselect_seq(q22) = rselect_seq(queue_101),
inference(paramodulation,[status(thm)],[f2692,f316]) ).
fof(f2695,plain,
rselect_tail(q22) = index_102,
inference(paramodulation,[status(thm)],[f2692,f314]) ).
fof(f2696,plain,
earray_104 = rselect_seq(queue_101),
inference(forward_demodulation,[status(thm)],[f373,f2694]) ).
fof(f2697,plain,
index_105 = index_102,
inference(forward_demodulation,[status(thm)],[f435,f2695]) ).
fof(f2699,plain,
rselect_head(queue_107) = rselect_head(q22),
inference(paramodulation,[status(thm)],[f518,f318]) ).
fof(f2700,plain,
rselect_seq(queue_107) = earray_106,
inference(paramodulation,[status(thm)],[f518,f312]) ).
fof(f2705,plain,
index_105 = s(index_99),
inference(backward_demodulation,[status(thm)],[f2697,f434]) ).
fof(f2707,plain,
q23 = rstore_tail(queue_107,index_108),
inference(forward_demodulation,[status(thm)],[f602,f519]) ).
fof(f2708,plain,
rselect_head(q23) = rselect_head(queue_107),
inference(paramodulation,[status(thm)],[f2707,f317]) ).
fof(f2709,plain,
rselect_seq(q23) = rselect_seq(queue_107),
inference(paramodulation,[status(thm)],[f2707,f316]) ).
fof(f2710,plain,
rselect_tail(q23) = index_108,
inference(paramodulation,[status(thm)],[f2707,f314]) ).
fof(f2711,plain,
earray_110 = rselect_seq(queue_107),
inference(forward_demodulation,[status(thm)],[f375,f2709]) ).
fof(f2712,plain,
index_111 = index_108,
inference(forward_demodulation,[status(thm)],[f437,f2710]) ).
fof(f2717,plain,
index_111 = s(index_105),
inference(backward_demodulation,[status(thm)],[f2712,f436]) ).
fof(f2720,plain,
rselect_head(queue_11) = rselect_head(q9),
inference(paramodulation,[status(thm)],[f520,f318]) ).
fof(f2724,plain,
rselect_head(queue_113) = rselect_head(q23),
inference(paramodulation,[status(thm)],[f521,f318]) ).
fof(f2725,plain,
rselect_seq(queue_113) = earray_112,
inference(paramodulation,[status(thm)],[f521,f312]) ).
fof(f2727,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(paramodulation,[status(thm)],[f522,f317]) ).
fof(f2729,plain,
rselect_tail(queue_115) = index_114,
inference(paramodulation,[status(thm)],[f522,f314]) ).
fof(f2730,plain,
index_116 = rselect_head(queue_113),
inference(forward_demodulation,[status(thm)],[f439,f2727]) ).
fof(f2731,plain,
q24 = rstore_head(queue_115,index_117),
inference(forward_demodulation,[status(thm)],[f603,f523]) ).
fof(f2732,plain,
rselect_tail(q24) = rselect_tail(queue_115),
inference(paramodulation,[status(thm)],[f2731,f320]) ).
fof(f2733,plain,
rselect_seq(q24) = rselect_seq(queue_115),
inference(paramodulation,[status(thm)],[f2731,f315]) ).
fof(f2734,plain,
rselect_head(q24) = index_117,
inference(paramodulation,[status(thm)],[f2731,f313]) ).
fof(f2735,plain,
index_120 = rselect_tail(queue_115),
inference(forward_demodulation,[status(thm)],[f442,f2732]) ).
fof(f2736,plain,
earray_119 = rselect_seq(queue_115),
inference(forward_demodulation,[status(thm)],[f377,f2733]) ).
fof(f2738,plain,
rselect_head(queue_122) = rselect_head(q24),
inference(paramodulation,[status(thm)],[f524,f318]) ).
fof(f2739,plain,
rselect_seq(queue_122) = earray_121,
inference(paramodulation,[status(thm)],[f524,f312]) ).
fof(f2741,plain,
q25 = rstore_tail(queue_122,index_123),
inference(forward_demodulation,[status(thm)],[f604,f525]) ).
fof(f2742,plain,
rselect_head(q25) = rselect_head(queue_122),
inference(paramodulation,[status(thm)],[f2741,f317]) ).
fof(f2743,plain,
rselect_seq(q25) = rselect_seq(queue_122),
inference(paramodulation,[status(thm)],[f2741,f316]) ).
fof(f2744,plain,
rselect_tail(q25) = index_123,
inference(paramodulation,[status(thm)],[f2741,f314]) ).
fof(f2745,plain,
earray_125 = rselect_seq(queue_122),
inference(forward_demodulation,[status(thm)],[f379,f2743]) ).
fof(f2746,plain,
index_126 = index_123,
inference(forward_demodulation,[status(thm)],[f444,f2744]) ).
fof(f2750,plain,
index_126 = s(index_120),
inference(backward_demodulation,[status(thm)],[f2746,f443]) ).
fof(f2753,plain,
rselect_head(queue_128) = rselect_head(q25),
inference(paramodulation,[status(thm)],[f526,f318]) ).
fof(f2754,plain,
rselect_seq(queue_128) = earray_127,
inference(paramodulation,[status(thm)],[f526,f312]) ).
fof(f2756,plain,
q10 = rstore_tail(queue_11,index_12),
inference(forward_demodulation,[status(thm)],[f588,f527]) ).
fof(f2757,plain,
rselect_head(q10) = rselect_head(queue_11),
inference(paramodulation,[status(thm)],[f2756,f317]) ).
fof(f2759,plain,
rselect_tail(q10) = index_12,
inference(paramodulation,[status(thm)],[f2756,f314]) ).
fof(f2761,plain,
index_15 = index_12,
inference(forward_demodulation,[status(thm)],[f453,f2759]) ).
fof(f2765,plain,
index_15 = s(index_9),
inference(backward_demodulation,[status(thm)],[f2761,f441]) ).
fof(f2767,plain,
q26 = rstore_tail(queue_128,index_129),
inference(forward_demodulation,[status(thm)],[f605,f528]) ).
fof(f2768,plain,
rselect_head(q26) = rselect_head(queue_128),
inference(paramodulation,[status(thm)],[f2767,f317]) ).
fof(f2769,plain,
rselect_seq(q26) = rselect_seq(queue_128),
inference(paramodulation,[status(thm)],[f2767,f316]) ).
fof(f2770,plain,
rselect_tail(q26) = index_129,
inference(paramodulation,[status(thm)],[f2767,f314]) ).
fof(f2771,plain,
earray_131 = rselect_seq(queue_128),
inference(forward_demodulation,[status(thm)],[f381,f2769]) ).
fof(f2772,plain,
index_132 = index_129,
inference(forward_demodulation,[status(thm)],[f446,f2770]) ).
fof(f2774,plain,
rselect_head(queue_134) = rselect_head(q26),
inference(paramodulation,[status(thm)],[f529,f318]) ).
fof(f2775,plain,
rselect_seq(queue_134) = earray_133,
inference(paramodulation,[status(thm)],[f529,f312]) ).
fof(f2777,plain,
rselect_head(queue_136) = rselect_head(queue_134),
inference(paramodulation,[status(thm)],[f530,f317]) ).
fof(f2779,plain,
rselect_tail(queue_136) = index_135,
inference(paramodulation,[status(thm)],[f530,f314]) ).
fof(f2780,plain,
index_137 = rselect_head(queue_134),
inference(forward_demodulation,[status(thm)],[f448,f2777]) ).
fof(f2785,plain,
index_132 = s(index_126),
inference(backward_demodulation,[status(thm)],[f2772,f445]) ).
fof(f2787,plain,
q27 = rstore_head(queue_136,index_138),
inference(forward_demodulation,[status(thm)],[f606,f531]) ).
fof(f2788,plain,
rselect_tail(q27) = rselect_tail(queue_136),
inference(paramodulation,[status(thm)],[f2787,f320]) ).
fof(f2789,plain,
rselect_seq(q27) = rselect_seq(queue_136),
inference(paramodulation,[status(thm)],[f2787,f315]) ).
fof(f2790,plain,
rselect_head(q27) = index_138,
inference(paramodulation,[status(thm)],[f2787,f313]) ).
fof(f2791,plain,
index_141 = rselect_tail(queue_136),
inference(forward_demodulation,[status(thm)],[f450,f2788]) ).
fof(f2792,plain,
earray_140 = rselect_seq(queue_136),
inference(forward_demodulation,[status(thm)],[f384,f2789]) ).
fof(f2794,plain,
rselect_head(queue_143) = rselect_head(q27),
inference(paramodulation,[status(thm)],[f532,f318]) ).
fof(f2795,plain,
rselect_seq(queue_143) = earray_142,
inference(paramodulation,[status(thm)],[f532,f312]) ).
fof(f2797,plain,
q28 = rstore_tail(queue_143,index_144),
inference(forward_demodulation,[status(thm)],[f607,f533]) ).
fof(f2798,plain,
rselect_head(q28) = rselect_head(queue_143),
inference(paramodulation,[status(thm)],[f2797,f317]) ).
fof(f2799,plain,
rselect_seq(q28) = rselect_seq(queue_143),
inference(paramodulation,[status(thm)],[f2797,f316]) ).
fof(f2800,plain,
rselect_tail(q28) = index_144,
inference(paramodulation,[status(thm)],[f2797,f314]) ).
fof(f2801,plain,
earray_146 = rselect_seq(queue_143),
inference(forward_demodulation,[status(thm)],[f386,f2799]) ).
fof(f2802,plain,
index_147 = index_144,
inference(forward_demodulation,[status(thm)],[f452,f2800]) ).
fof(f2806,plain,
index_147 = s(index_141),
inference(backward_demodulation,[status(thm)],[f2802,f451]) ).
fof(f2809,plain,
rselect_head(queue_149) = rselect_head(q28),
inference(paramodulation,[status(thm)],[f534,f318]) ).
fof(f2810,plain,
rselect_seq(queue_149) = earray_148,
inference(paramodulation,[status(thm)],[f534,f312]) ).
fof(f2812,plain,
q29 = rstore_tail(queue_149,index_150),
inference(forward_demodulation,[status(thm)],[f608,f535]) ).
fof(f2813,plain,
rselect_head(q29) = rselect_head(queue_149),
inference(paramodulation,[status(thm)],[f2812,f317]) ).
fof(f2815,plain,
rselect_tail(q29) = index_150,
inference(paramodulation,[status(thm)],[f2812,f314]) ).
fof(f2817,plain,
index_162 = index_150,
inference(forward_demodulation,[status(thm)],[f459,f2815]) ).
fof(f2819,plain,
rselect_head(queue_155) = rselect_head(q2),
inference(paramodulation,[status(thm)],[f536,f318]) ).
fof(f2822,plain,
q29 = rstore_tail(queue_149,index_162),
inference(backward_demodulation,[status(thm)],[f2817,f2812]) ).
fof(f2826,plain,
index_162 = s(index_147),
inference(backward_demodulation,[status(thm)],[f2817,f454]) ).
fof(f2828,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(paramodulation,[status(thm)],[f537,f317]) ).
fof(f2830,plain,
rselect_tail(queue_157) = index_156,
inference(paramodulation,[status(thm)],[f537,f314]) ).
fof(f2831,plain,
index_158 = rselect_head(queue_155),
inference(forward_demodulation,[status(thm)],[f457,f2828]) ).
fof(f2832,plain,
q3 = rstore_head(queue_157,index_159),
inference(forward_demodulation,[status(thm)],[f609,f538]) ).
fof(f2833,plain,
rselect_tail(q3) = rselect_tail(queue_157),
inference(paramodulation,[status(thm)],[f2832,f320]) ).
fof(f2835,plain,
rselect_head(q3) = index_159,
inference(paramodulation,[status(thm)],[f2832,f313]) ).
fof(f2836,plain,
index_171 = rselect_tail(queue_157),
inference(forward_demodulation,[status(thm)],[f463,f2833]) ).
fof(f2839,plain,
rselect_head(queue_164) = rselect_head(q29),
inference(paramodulation,[status(thm)],[f539,f318]) ).
fof(f2840,plain,
rselect_seq(queue_164) = earray_163,
inference(paramodulation,[status(thm)],[f539,f312]) ).
fof(f2842,plain,
rselect_head(queue_166) = rselect_head(queue_164),
inference(paramodulation,[status(thm)],[f540,f317]) ).
fof(f2843,plain,
rselect_seq(queue_166) = rselect_seq(queue_164),
inference(paramodulation,[status(thm)],[f540,f316]) ).
fof(f2845,plain,
index_167 = rselect_head(queue_164),
inference(forward_demodulation,[status(thm)],[f461,f2842]) ).
fof(f2846,plain,
q30 = rstore_head(queue_166,index_168),
inference(forward_demodulation,[status(thm)],[f610,f541]) ).
fof(f2848,plain,
rselect_seq(q30) = rselect_seq(queue_166),
inference(paramodulation,[status(thm)],[f2846,f315]) ).
fof(f2849,plain,
rselect_head(q30) = index_168,
inference(paramodulation,[status(thm)],[f2846,f313]) ).
fof(f2850,plain,
earray_212 = rselect_seq(queue_166),
inference(forward_demodulation,[status(thm)],[f407,f2848]) ).
fof(f2851,plain,
index_213 = index_168,
inference(forward_demodulation,[status(thm)],[f481,f2849]) ).
fof(f2853,plain,
rselect_head(queue_17) = rselect_head(q10),
inference(paramodulation,[status(thm)],[f542,f318]) ).
fof(f2854,plain,
rselect_seq(queue_17) = earray_16,
inference(paramodulation,[status(thm)],[f542,f312]) ).
fof(f2859,plain,
index_213 = s(index_167),
inference(backward_demodulation,[status(thm)],[f2851,f462]) ).
fof(f2861,plain,
rselect_head(queue_173) = rselect_head(q3),
inference(paramodulation,[status(thm)],[f543,f318]) ).
fof(f2864,plain,
q4 = rstore_tail(queue_173,index_174),
inference(forward_demodulation,[status(thm)],[f611,f544]) ).
fof(f2865,plain,
rselect_head(q4) = rselect_head(queue_173),
inference(paramodulation,[status(thm)],[f2864,f317]) ).
fof(f2867,plain,
rselect_tail(q4) = index_174,
inference(paramodulation,[status(thm)],[f2864,f314]) ).
fof(f2869,plain,
index_177 = index_174,
inference(forward_demodulation,[status(thm)],[f465,f2867]) ).
fof(f2871,plain,
rselect_head(queue_179) = rselect_head(q4),
inference(paramodulation,[status(thm)],[f545,f318]) ).
fof(f2877,plain,
index_177 = s(index_171),
inference(backward_demodulation,[status(thm)],[f2869,f464]) ).
fof(f2879,plain,
q5 = rstore_tail(queue_179,index_180),
inference(forward_demodulation,[status(thm)],[f612,f546]) ).
fof(f2880,plain,
rselect_head(q5) = rselect_head(queue_179),
inference(paramodulation,[status(thm)],[f2879,f317]) ).
fof(f2882,plain,
rselect_tail(q5) = index_180,
inference(paramodulation,[status(thm)],[f2879,f314]) ).
fof(f2884,plain,
index_183 = index_180,
inference(forward_demodulation,[status(thm)],[f468,f2882]) ).
fof(f2886,plain,
rselect_head(queue_185) = rselect_head(q5),
inference(paramodulation,[status(thm)],[f547,f318]) ).
fof(f2889,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(paramodulation,[status(thm)],[f548,f317]) ).
fof(f2891,plain,
rselect_tail(queue_187) = index_186,
inference(paramodulation,[status(thm)],[f548,f314]) ).
fof(f2892,plain,
index_188 = rselect_head(queue_185),
inference(forward_demodulation,[status(thm)],[f470,f2889]) ).
fof(f2897,plain,
index_183 = s(index_177),
inference(backward_demodulation,[status(thm)],[f2884,f467]) ).
fof(f2899,plain,
q11 = rstore_tail(queue_17,index_18),
inference(forward_demodulation,[status(thm)],[f589,f549]) ).
fof(f2900,plain,
rselect_head(q11) = rselect_head(queue_17),
inference(paramodulation,[status(thm)],[f2899,f317]) ).
fof(f2901,plain,
rselect_seq(q11) = rselect_seq(queue_17),
inference(paramodulation,[status(thm)],[f2899,f316]) ).
fof(f2902,plain,
rselect_tail(q11) = index_18,
inference(paramodulation,[status(thm)],[f2899,f314]) ).
fof(f2903,plain,
earray_20 = rselect_seq(queue_17),
inference(forward_demodulation,[status(thm)],[f404,f2901]) ).
fof(f2904,plain,
index_21 = index_18,
inference(forward_demodulation,[status(thm)],[f479,f2902]) ).
fof(f2906,plain,
s(index_21) != index_15,
inference(backward_demodulation,[status(thm)],[f2904,f1402]) ).
fof(f2908,plain,
index_21 != index_15,
inference(backward_demodulation,[status(thm)],[f2904,f1405]) ).
fof(f2909,plain,
index_21 = s(index_15),
inference(backward_demodulation,[status(thm)],[f2904,f466]) ).
fof(f2910,plain,
index_24 != index_15,
inference(forward_demodulation,[status(thm)],[f482,f2906]) ).
fof(f2911,plain,
q6 = rstore_head(queue_187,index_189),
inference(forward_demodulation,[status(thm)],[f613,f550]) ).
fof(f2912,plain,
rselect_tail(q6) = rselect_tail(queue_187),
inference(paramodulation,[status(thm)],[f2911,f320]) ).
fof(f2914,plain,
rselect_head(q6) = index_189,
inference(paramodulation,[status(thm)],[f2911,f313]) ).
fof(f2915,plain,
index_192 = rselect_tail(queue_187),
inference(forward_demodulation,[status(thm)],[f472,f2912]) ).
fof(f2918,plain,
rselect_head(queue_194) = rselect_head(q6),
inference(paramodulation,[status(thm)],[f551,f318]) ).
fof(f2921,plain,
q7 = rstore_tail(queue_194,index_195),
inference(forward_demodulation,[status(thm)],[f614,f552]) ).
fof(f2922,plain,
rselect_head(q7) = rselect_head(queue_194),
inference(paramodulation,[status(thm)],[f2921,f317]) ).
fof(f2924,plain,
rselect_tail(q7) = index_195,
inference(paramodulation,[status(thm)],[f2921,f314]) ).
fof(f2926,plain,
index_198 = index_195,
inference(forward_demodulation,[status(thm)],[f474,f2924]) ).
fof(f2928,plain,
rselect_head(queue_200) = rselect_head(q7),
inference(paramodulation,[status(thm)],[f553,f318]) ).
fof(f2931,plain,
q8 = rstore_tail(queue_200,index_201),
inference(forward_demodulation,[status(thm)],[f615,f554]) ).
fof(f2932,plain,
rselect_head(q8) = rselect_head(queue_200),
inference(paramodulation,[status(thm)],[f2931,f317]) ).
fof(f2934,plain,
rselect_tail(q8) = index_201,
inference(paramodulation,[status(thm)],[f2931,f314]) ).
fof(f2936,plain,
index_204 = index_201,
inference(forward_demodulation,[status(thm)],[f476,f2934]) ).
fof(f2940,plain,
index_198 = s(index_192),
inference(backward_demodulation,[status(thm)],[f2926,f473]) ).
fof(f2945,plain,
index_204 = s(index_198),
inference(backward_demodulation,[status(thm)],[f2936,f475]) ).
fof(f2949,plain,
rselect_seq(queue_206) = earray_205,
inference(paramodulation,[status(thm)],[f555,f312]) ).
fof(f2952,plain,
rselect_head(queue_208) = rselect_head(queue_206),
inference(paramodulation,[status(thm)],[f556,f317]) ).
fof(f2954,plain,
rselect_tail(queue_208) = index_207,
inference(paramodulation,[status(thm)],[f556,f314]) ).
fof(f2955,plain,
index_209 = rselect_head(queue_206),
inference(forward_demodulation,[status(thm)],[f478,f2952]) ).
fof(f2956,plain,
q9 = rstore_head(queue_208,index_210),
inference(forward_demodulation,[status(thm)],[f616,f557]) ).
fof(f2957,plain,
rselect_tail(q9) = rselect_tail(queue_208),
inference(paramodulation,[status(thm)],[f2956,f320]) ).
fof(f2958,plain,
rselect_seq(q9) = rselect_seq(queue_208),
inference(paramodulation,[status(thm)],[f2956,f315]) ).
fof(f2959,plain,
rselect_head(q9) = index_210,
inference(paramodulation,[status(thm)],[f2956,f313]) ).
fof(f2960,plain,
index_9 = rselect_tail(queue_208),
inference(forward_demodulation,[status(thm)],[f509,f2957]) ).
fof(f2961,plain,
earray_8 = rselect_seq(queue_208),
inference(forward_demodulation,[status(thm)],[f426,f2958]) ).
fof(f2962,plain,
index_0 = index_3,
inference(backward_demodulation,[status(thm)],[f2686,f433]) ).
fof(f2964,plain,
rselect_head(q0) = index_3,
inference(forward_demodulation,[status(thm)],[f2962,f2685]) ).
fof(f2966,plain,
rselect_head(queue_23) = rselect_head(q11),
inference(paramodulation,[status(thm)],[f558,f318]) ).
fof(f2967,plain,
rselect_seq(queue_23) = earray_22,
inference(paramodulation,[status(thm)],[f558,f312]) ).
fof(f2969,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(paramodulation,[status(thm)],[f559,f317]) ).
fof(f2971,plain,
rselect_tail(queue_25) = index_24,
inference(paramodulation,[status(thm)],[f559,f314]) ).
fof(f2972,plain,
index_26 = rselect_head(queue_23),
inference(forward_demodulation,[status(thm)],[f483,f2969]) ).
fof(f2973,plain,
q12 = rstore_head(queue_25,index_27),
inference(forward_demodulation,[status(thm)],[f590,f560]) ).
fof(f2974,plain,
rselect_tail(q12) = rselect_tail(queue_25),
inference(paramodulation,[status(thm)],[f2973,f320]) ).
fof(f2975,plain,
rselect_seq(q12) = rselect_seq(queue_25),
inference(paramodulation,[status(thm)],[f2973,f315]) ).
fof(f2976,plain,
rselect_head(q12) = index_27,
inference(paramodulation,[status(thm)],[f2973,f313]) ).
fof(f2977,plain,
index_30 = rselect_tail(queue_25),
inference(forward_demodulation,[status(thm)],[f486,f2974]) ).
fof(f2978,plain,
earray_29 = rselect_seq(queue_25),
inference(forward_demodulation,[status(thm)],[f409,f2975]) ).
fof(f2981,plain,
earray_104 = earray_100,
inference(forward_demodulation,[status(thm)],[f2690,f2696]) ).
fof(f2983,plain,
rselect_head(queue_32) = rselect_head(q12),
inference(paramodulation,[status(thm)],[f561,f318]) ).
fof(f2984,plain,
rselect_seq(queue_32) = earray_31,
inference(paramodulation,[status(thm)],[f561,f312]) ).
fof(f3038,plain,
earray_110 = earray_106,
inference(forward_demodulation,[status(thm)],[f2700,f2711]) ).
fof(f3138,plain,
q13 = rstore_tail(queue_32,index_33),
inference(forward_demodulation,[status(thm)],[f591,f562]) ).
fof(f3139,plain,
rselect_head(q13) = rselect_head(queue_32),
inference(paramodulation,[status(thm)],[f3138,f317]) ).
fof(f3140,plain,
rselect_seq(q13) = rselect_seq(queue_32),
inference(paramodulation,[status(thm)],[f3138,f316]) ).
fof(f3141,plain,
rselect_tail(q13) = index_33,
inference(paramodulation,[status(thm)],[f3138,f314]) ).
fof(f3142,plain,
earray_35 = rselect_seq(queue_32),
inference(forward_demodulation,[status(thm)],[f411,f3140]) ).
fof(f3143,plain,
index_36 = index_33,
inference(forward_demodulation,[status(thm)],[f488,f3141]) ).
fof(f3145,plain,
rselect_head(queue_38) = rselect_head(q13),
inference(paramodulation,[status(thm)],[f563,f318]) ).
fof(f3146,plain,
rselect_seq(queue_38) = earray_37,
inference(paramodulation,[status(thm)],[f563,f312]) ).
fof(f3151,plain,
index_36 = s(index_30),
inference(backward_demodulation,[status(thm)],[f3143,f487]) ).
fof(f3153,plain,
q14 = rstore_tail(queue_38,index_39),
inference(forward_demodulation,[status(thm)],[f592,f564]) ).
fof(f3154,plain,
rselect_head(q14) = rselect_head(queue_38),
inference(paramodulation,[status(thm)],[f3153,f317]) ).
fof(f3155,plain,
rselect_seq(q14) = rselect_seq(queue_38),
inference(paramodulation,[status(thm)],[f3153,f316]) ).
fof(f3156,plain,
rselect_tail(q14) = index_39,
inference(paramodulation,[status(thm)],[f3153,f314]) ).
fof(f3157,plain,
earray_41 = rselect_seq(queue_38),
inference(forward_demodulation,[status(thm)],[f414,f3155]) ).
fof(f3158,plain,
index_42 = index_39,
inference(forward_demodulation,[status(thm)],[f490,f3156]) ).
fof(f3160,plain,
rselect_head(queue_44) = rselect_head(q14),
inference(paramodulation,[status(thm)],[f565,f318]) ).
fof(f3161,plain,
rselect_seq(queue_44) = earray_43,
inference(paramodulation,[status(thm)],[f565,f312]) ).
fof(f3163,plain,
rselect_head(queue_46) = rselect_head(queue_44),
inference(paramodulation,[status(thm)],[f566,f317]) ).
fof(f3165,plain,
rselect_tail(queue_46) = index_45,
inference(paramodulation,[status(thm)],[f566,f314]) ).
fof(f3166,plain,
index_47 = rselect_head(queue_44),
inference(forward_demodulation,[status(thm)],[f492,f3163]) ).
fof(f3171,plain,
index_42 = s(index_36),
inference(backward_demodulation,[status(thm)],[f3158,f489]) ).
fof(f3173,plain,
q15 = rstore_head(queue_46,index_48),
inference(forward_demodulation,[status(thm)],[f593,f567]) ).
fof(f3174,plain,
rselect_tail(q15) = rselect_tail(queue_46),
inference(paramodulation,[status(thm)],[f3173,f320]) ).
fof(f3175,plain,
rselect_seq(q15) = rselect_seq(queue_46),
inference(paramodulation,[status(thm)],[f3173,f315]) ).
fof(f3176,plain,
rselect_head(q15) = index_48,
inference(paramodulation,[status(thm)],[f3173,f313]) ).
fof(f3177,plain,
index_51 = rselect_tail(queue_46),
inference(forward_demodulation,[status(thm)],[f494,f3174]) ).
fof(f3178,plain,
earray_50 = rselect_seq(queue_46),
inference(forward_demodulation,[status(thm)],[f416,f3175]) ).
fof(f3180,plain,
rselect_head(queue_5) = rselect_head(q0),
inference(paramodulation,[status(thm)],[f568,f318]) ).
fof(f3183,plain,
rselect_head(queue_5) = index_3,
inference(forward_demodulation,[status(thm)],[f2964,f3180]) ).
fof(f3185,plain,
rselect_head(queue_53) = rselect_head(q15),
inference(paramodulation,[status(thm)],[f569,f318]) ).
fof(f3186,plain,
rselect_seq(queue_53) = earray_52,
inference(paramodulation,[status(thm)],[f569,f312]) ).
fof(f3188,plain,
index_120 = index_114,
inference(backward_demodulation,[status(thm)],[f2735,f2729]) ).
fof(f3189,plain,
queue_115 = rstore_tail(queue_113,index_120),
inference(backward_demodulation,[status(thm)],[f3188,f522]) ).
fof(f3193,plain,
index_120 = s(index_111),
inference(backward_demodulation,[status(thm)],[f3188,f438]) ).
fof(f3194,plain,
q16 = rstore_tail(queue_53,index_54),
inference(forward_demodulation,[status(thm)],[f594,f570]) ).
fof(f3195,plain,
rselect_head(q16) = rselect_head(queue_53),
inference(paramodulation,[status(thm)],[f3194,f317]) ).
fof(f3196,plain,
rselect_seq(q16) = rselect_seq(queue_53),
inference(paramodulation,[status(thm)],[f3194,f316]) ).
fof(f3197,plain,
rselect_tail(q16) = index_54,
inference(paramodulation,[status(thm)],[f3194,f314]) ).
fof(f3198,plain,
earray_56 = rselect_seq(queue_53),
inference(forward_demodulation,[status(thm)],[f418,f3196]) ).
fof(f3199,plain,
index_57 = index_54,
inference(forward_demodulation,[status(thm)],[f496,f3197]) ).
fof(f3201,plain,
rselect_head(queue_59) = rselect_head(q16),
inference(paramodulation,[status(thm)],[f571,f318]) ).
fof(f3202,plain,
rselect_seq(queue_59) = earray_58,
inference(paramodulation,[status(thm)],[f571,f312]) ).
fof(f3204,plain,
q17 = rstore_tail(queue_59,index_60),
inference(forward_demodulation,[status(thm)],[f595,f572]) ).
fof(f3205,plain,
rselect_head(q17) = rselect_head(queue_59),
inference(paramodulation,[status(thm)],[f3204,f317]) ).
fof(f3206,plain,
rselect_seq(q17) = rselect_seq(queue_59),
inference(paramodulation,[status(thm)],[f3204,f316]) ).
fof(f3207,plain,
rselect_tail(q17) = index_60,
inference(paramodulation,[status(thm)],[f3204,f314]) ).
fof(f3208,plain,
earray_62 = rselect_seq(queue_59),
inference(forward_demodulation,[status(thm)],[f420,f3206]) ).
fof(f3209,plain,
index_63 = index_60,
inference(forward_demodulation,[status(thm)],[f499,f3207]) ).
fof(f3213,plain,
index_57 = s(index_51),
inference(backward_demodulation,[status(thm)],[f3199,f495]) ).
fof(f3218,plain,
index_63 = s(index_57),
inference(backward_demodulation,[status(thm)],[f3209,f498]) ).
fof(f3221,plain,
rselect_head(queue_65) = rselect_head(q17),
inference(paramodulation,[status(thm)],[f573,f318]) ).
fof(f3222,plain,
rselect_seq(queue_65) = earray_64,
inference(paramodulation,[status(thm)],[f573,f312]) ).
fof(f3225,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(paramodulation,[status(thm)],[f574,f317]) ).
fof(f3227,plain,
rselect_tail(queue_67) = index_66,
inference(paramodulation,[status(thm)],[f574,f314]) ).
fof(f3228,plain,
index_68 = rselect_head(queue_65),
inference(forward_demodulation,[status(thm)],[f501,f3225]) ).
fof(f3229,plain,
q1 = rstore_tail(queue_5,index_6),
inference(forward_demodulation,[status(thm)],[f587,f575]) ).
fof(f3230,plain,
rselect_head(q1) = rselect_head(queue_5),
inference(paramodulation,[status(thm)],[f3229,f317]) ).
fof(f3232,plain,
rselect_tail(q1) = index_6,
inference(paramodulation,[status(thm)],[f3229,f314]) ).
fof(f3234,plain,
index_78 = index_6,
inference(forward_demodulation,[status(thm)],[f505,f3232]) ).
fof(f3238,plain,
index_78 = s(index_3),
inference(backward_demodulation,[status(thm)],[f3234,f497]) ).
fof(f3240,plain,
q18 = rstore_head(queue_67,index_69),
inference(forward_demodulation,[status(thm)],[f596,f576]) ).
fof(f3241,plain,
rselect_tail(q18) = rselect_tail(queue_67),
inference(paramodulation,[status(thm)],[f3240,f320]) ).
fof(f3242,plain,
rselect_seq(q18) = rselect_seq(queue_67),
inference(paramodulation,[status(thm)],[f3240,f315]) ).
fof(f3243,plain,
rselect_head(q18) = index_69,
inference(paramodulation,[status(thm)],[f3240,f313]) ).
fof(f3244,plain,
index_72 = rselect_tail(queue_67),
inference(forward_demodulation,[status(thm)],[f503,f3241]) ).
fof(f3245,plain,
earray_71 = rselect_seq(queue_67),
inference(forward_demodulation,[status(thm)],[f422,f3242]) ).
fof(f3247,plain,
rselect_head(queue_74) = rselect_head(q18),
inference(paramodulation,[status(thm)],[f577,f318]) ).
fof(f3248,plain,
rselect_seq(queue_74) = earray_73,
inference(paramodulation,[status(thm)],[f577,f312]) ).
fof(f3250,plain,
q19 = rstore_tail(queue_74,index_75),
inference(forward_demodulation,[status(thm)],[f597,f578]) ).
fof(f3251,plain,
rselect_head(q19) = rselect_head(queue_74),
inference(paramodulation,[status(thm)],[f3250,f317]) ).
fof(f3252,plain,
rselect_seq(q19) = rselect_seq(queue_74),
inference(paramodulation,[status(thm)],[f3250,f316]) ).
fof(f3253,plain,
rselect_tail(q19) = index_75,
inference(paramodulation,[status(thm)],[f3250,f314]) ).
fof(f3254,plain,
earray_83 = rselect_seq(queue_74),
inference(forward_demodulation,[status(thm)],[f427,f3252]) ).
fof(f3255,plain,
index_84 = index_75,
inference(forward_demodulation,[status(thm)],[f507,f3253]) ).
fof(f3259,plain,
index_84 = s(index_72),
inference(backward_demodulation,[status(thm)],[f3255,f504]) ).
fof(f3262,plain,
rselect_head(queue_80) = rselect_head(q1),
inference(paramodulation,[status(thm)],[f579,f318]) ).
fof(f3267,plain,
earray_125 = earray_121,
inference(forward_demodulation,[status(thm)],[f2739,f2745]) ).
fof(f3318,plain,
q2 = rstore_tail(queue_80,index_81),
inference(forward_demodulation,[status(thm)],[f598,f580]) ).
fof(f3319,plain,
rselect_head(q2) = rselect_head(queue_80),
inference(paramodulation,[status(thm)],[f3318,f317]) ).
fof(f3321,plain,
rselect_tail(q2) = index_81,
inference(paramodulation,[status(thm)],[f3318,f314]) ).
fof(f3323,plain,
index_153 = index_81,
inference(forward_demodulation,[status(thm)],[f455,f3321]) ).
fof(f3325,plain,
rselect_head(queue_86) = rselect_head(q19),
inference(paramodulation,[status(thm)],[f581,f318]) ).
fof(f3326,plain,
rselect_seq(queue_86) = earray_85,
inference(paramodulation,[status(thm)],[f581,f312]) ).
fof(f3332,plain,
index_153 = s(index_78),
inference(backward_demodulation,[status(thm)],[f3323,f506]) ).
fof(f3338,plain,
q20 = rstore_tail(queue_86,index_87),
inference(forward_demodulation,[status(thm)],[f599,f582]) ).
fof(f3339,plain,
rselect_head(q20) = rselect_head(queue_86),
inference(paramodulation,[status(thm)],[f3338,f317]) ).
fof(f3340,plain,
rselect_seq(q20) = rselect_seq(queue_86),
inference(paramodulation,[status(thm)],[f3338,f316]) ).
fof(f3341,plain,
rselect_tail(q20) = index_87,
inference(paramodulation,[status(thm)],[f3338,f314]) ).
fof(f3342,plain,
earray_89 = rselect_seq(queue_86),
inference(forward_demodulation,[status(thm)],[f429,f3340]) ).
fof(f3343,plain,
index_90 = index_87,
inference(forward_demodulation,[status(thm)],[f510,f3341]) ).
fof(f3346,plain,
rselect_seq(queue_92) = earray_91,
inference(paramodulation,[status(thm)],[f583,f312]) ).
fof(f3348,plain,
rselect_head(queue_94) = rselect_head(queue_92),
inference(paramodulation,[status(thm)],[f584,f317]) ).
fof(f3350,plain,
rselect_tail(queue_94) = index_93,
inference(paramodulation,[status(thm)],[f584,f314]) ).
fof(f3351,plain,
index_95 = rselect_head(queue_92),
inference(forward_demodulation,[status(thm)],[f512,f3348]) ).
fof(f3360,plain,
index_90 = s(index_84),
inference(backward_demodulation,[status(thm)],[f3343,f508]) ).
fof(f3362,plain,
q21 = rstore_head(queue_94,index_96),
inference(forward_demodulation,[status(thm)],[f600,f585]) ).
fof(f3363,plain,
rselect_tail(q21) = rselect_tail(queue_94),
inference(paramodulation,[status(thm)],[f3362,f320]) ).
fof(f3364,plain,
rselect_seq(q21) = rselect_seq(queue_94),
inference(paramodulation,[status(thm)],[f3362,f315]) ).
fof(f3365,plain,
rselect_head(q21) = index_96,
inference(paramodulation,[status(thm)],[f3362,f313]) ).
fof(f3366,plain,
index_99 = rselect_tail(queue_94),
inference(forward_demodulation,[status(thm)],[f514,f3363]) ).
fof(f3367,plain,
earray_98 = rselect_seq(queue_94),
inference(forward_demodulation,[status(thm)],[f431,f3364]) ).
fof(f3424,plain,
earray_131 = earray_127,
inference(forward_demodulation,[status(thm)],[f2754,f2771]) ).
fof(f3536,plain,
index_141 = index_135,
inference(backward_demodulation,[status(thm)],[f2791,f2779]) ).
fof(f3542,plain,
queue_136 = rstore_tail(queue_134,index_141),
inference(backward_demodulation,[status(thm)],[f3536,f530]) ).
fof(f3545,plain,
index_141 = s(index_132),
inference(backward_demodulation,[status(thm)],[f3536,f447]) ).
fof(f3602,plain,
earray_146 = earray_142,
inference(forward_demodulation,[status(thm)],[f2795,f2801]) ).
fof(f3604,plain,
rselect_seq(q29) = rselect_seq(queue_149),
inference(paramodulation,[status(thm)],[f2822,f316]) ).
fof(f3606,plain,
earray_161 = rselect_seq(queue_149),
inference(forward_demodulation,[status(thm)],[f391,f3604]) ).
fof(f3607,plain,
earray_161 = earray_148,
inference(forward_demodulation,[status(thm)],[f2810,f3606]) ).
fof(f3818,plain,
index_171 = index_156,
inference(backward_demodulation,[status(thm)],[f2836,f2830]) ).
fof(f3823,plain,
index_171 = s(index_153),
inference(backward_demodulation,[status(thm)],[f3818,f456]) ).
fof(f3932,plain,
s(s(index_21)) != index_15,
inference(paramodulation,[status(thm)],[f2909,f368]) ).
fof(f3933,plain,
s(s(s(index_21))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f367]) ).
fof(f3934,plain,
s(s(s(s(index_21)))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f366]) ).
fof(f3935,plain,
s(s(s(s(s(index_21))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f365]) ).
fof(f3936,plain,
s(s(s(s(s(s(index_21)))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f364]) ).
fof(f3937,plain,
s(s(s(s(s(s(s(index_21))))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f363]) ).
fof(f3938,plain,
s(s(s(s(s(s(s(s(index_21)))))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f362]) ).
fof(f3939,plain,
s(s(s(s(s(s(s(s(s(index_21))))))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f361]) ).
fof(f3940,plain,
s(s(s(s(s(s(s(s(s(s(index_21)))))))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f360]) ).
fof(f3941,plain,
s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f359]) ).
fof(f3942,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f358]) ).
fof(f3943,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))) != index_15,
inference(paramodulation,[status(thm)],[f2909,f357]) ).
fof(f3982,plain,
s(index_24) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3932]) ).
fof(f3983,plain,
s(s(index_24)) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3933]) ).
fof(f3984,plain,
s(s(s(index_24))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3934]) ).
fof(f3985,plain,
s(s(s(s(index_24)))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3935]) ).
fof(f3986,plain,
s(s(s(s(s(index_24))))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3936]) ).
fof(f3987,plain,
s(s(s(s(s(s(index_24)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3937]) ).
fof(f3988,plain,
s(s(s(s(s(s(s(index_24))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3938]) ).
fof(f3989,plain,
s(s(s(s(s(s(s(s(index_24)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3939]) ).
fof(f3990,plain,
s(s(s(s(s(s(s(s(s(index_24))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3940]) ).
fof(f3991,plain,
s(s(s(s(s(s(s(s(s(s(index_24)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3941]) ).
fof(f3992,plain,
s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3942]) ).
fof(f3993,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f482,f3943]) ).
fof(f4205,plain,
earray_20 = earray_16,
inference(forward_demodulation,[status(thm)],[f2854,f2903]) ).
fof(f4206,plain,
index_192 = index_186,
inference(backward_demodulation,[status(thm)],[f2915,f2891]) ).
fof(f4211,plain,
index_192 = s(index_183),
inference(backward_demodulation,[status(thm)],[f4206,f469]) ).
fof(f4374,plain,
rselect_seq(queue_115) = rselect_seq(queue_113),
inference(paramodulation,[status(thm)],[f3189,f316]) ).
fof(f4377,plain,
earray_119 = rselect_seq(queue_113),
inference(forward_demodulation,[status(thm)],[f2736,f4374]) ).
fof(f4378,plain,
earray_119 = earray_112,
inference(forward_demodulation,[status(thm)],[f2725,f4377]) ).
fof(f4590,plain,
index_9 = index_207,
inference(backward_demodulation,[status(thm)],[f2960,f2954]) ).
fof(f4591,plain,
queue_208 = rstore_tail(queue_206,index_9),
inference(backward_demodulation,[status(thm)],[f4590,f556]) ).
fof(f4595,plain,
index_9 = s(index_204),
inference(backward_demodulation,[status(thm)],[f4590,f477]) ).
fof(f4806,plain,
index_30 = index_24,
inference(backward_demodulation,[status(thm)],[f2977,f2971]) ).
fof(f4807,plain,
queue_25 = rstore_tail(queue_23,index_30),
inference(backward_demodulation,[status(thm)],[f4806,f559]) ).
fof(f4808,plain,
index_30 != index_15,
inference(backward_demodulation,[status(thm)],[f4806,f2910]) ).
fof(f4811,plain,
index_30 = s(index_21),
inference(backward_demodulation,[status(thm)],[f4806,f482]) ).
fof(f4975,plain,
earray_35 = earray_31,
inference(forward_demodulation,[status(thm)],[f2984,f3142]) ).
fof(f4978,plain,
earray_41 = earray_37,
inference(forward_demodulation,[status(thm)],[f3146,f3157]) ).
fof(f4981,plain,
index_51 = index_45,
inference(backward_demodulation,[status(thm)],[f3177,f3165]) ).
fof(f4983,plain,
queue_46 = rstore_tail(queue_44,index_51),
inference(backward_demodulation,[status(thm)],[f4981,f566]) ).
fof(f4986,plain,
index_51 = s(index_42),
inference(backward_demodulation,[status(thm)],[f4981,f491]) ).
fof(f4989,plain,
rselect_seq(queue_136) = rselect_seq(queue_134),
inference(paramodulation,[status(thm)],[f3542,f316]) ).
fof(f4992,plain,
earray_140 = rselect_seq(queue_134),
inference(forward_demodulation,[status(thm)],[f2792,f4989]) ).
fof(f4993,plain,
earray_140 = earray_133,
inference(forward_demodulation,[status(thm)],[f2775,f4992]) ).
fof(f5356,plain,
earray_56 = earray_52,
inference(forward_demodulation,[status(thm)],[f3186,f3198]) ).
fof(f5361,plain,
earray_62 = earray_58,
inference(forward_demodulation,[status(thm)],[f3202,f3208]) ).
fof(f5523,plain,
index_72 = index_66,
inference(backward_demodulation,[status(thm)],[f3244,f3227]) ).
fof(f5524,plain,
queue_67 = rstore_tail(queue_65,index_72),
inference(backward_demodulation,[status(thm)],[f5523,f574]) ).
fof(f5528,plain,
index_72 = s(index_63),
inference(backward_demodulation,[status(thm)],[f5523,f500]) ).
fof(f5538,plain,
earray_83 = earray_73,
inference(forward_demodulation,[status(thm)],[f3248,f3254]) ).
fof(f5542,plain,
rselect_seq(queue_208) = rselect_seq(queue_206),
inference(paramodulation,[status(thm)],[f4591,f316]) ).
fof(f5545,plain,
earray_8 = rselect_seq(queue_206),
inference(forward_demodulation,[status(thm)],[f2961,f5542]) ).
fof(f5696,plain,
earray_89 = earray_85,
inference(forward_demodulation,[status(thm)],[f3326,f3342]) ).
fof(f5698,plain,
rselect_seq(queue_25) = rselect_seq(queue_23),
inference(paramodulation,[status(thm)],[f4807,f316]) ).
fof(f5701,plain,
earray_29 = rselect_seq(queue_23),
inference(forward_demodulation,[status(thm)],[f2978,f5698]) ).
fof(f5702,plain,
earray_29 = earray_22,
inference(forward_demodulation,[status(thm)],[f2967,f5701]) ).
fof(f5855,plain,
index_99 = index_93,
inference(backward_demodulation,[status(thm)],[f3366,f3350]) ).
fof(f5859,plain,
queue_94 = rstore_tail(queue_92,index_99),
inference(backward_demodulation,[status(thm)],[f5855,f584]) ).
fof(f5862,plain,
index_99 = s(index_90),
inference(backward_demodulation,[status(thm)],[f5855,f511]) ).
fof(f5865,plain,
rselect_seq(queue_46) = rselect_seq(queue_44),
inference(paramodulation,[status(thm)],[f4983,f316]) ).
fof(f5868,plain,
earray_50 = rselect_seq(queue_44),
inference(forward_demodulation,[status(thm)],[f3178,f5865]) ).
fof(f5869,plain,
earray_50 = earray_43,
inference(forward_demodulation,[status(thm)],[f3161,f5868]) ).
fof(f6042,plain,
s(index_30) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3982]) ).
fof(f6043,plain,
index_36 != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f6042]) ).
fof(f6051,plain,
rselect_seq(queue_67) = rselect_seq(queue_65),
inference(paramodulation,[status(thm)],[f5524,f316]) ).
fof(f6054,plain,
earray_71 = rselect_seq(queue_65),
inference(forward_demodulation,[status(thm)],[f3245,f6051]) ).
fof(f6055,plain,
earray_71 = earray_64,
inference(forward_demodulation,[status(thm)],[f3222,f6054]) ).
fof(f6234,plain,
rselect_seq(queue_94) = rselect_seq(queue_92),
inference(paramodulation,[status(thm)],[f5859,f316]) ).
fof(f6237,plain,
earray_98 = rselect_seq(queue_92),
inference(forward_demodulation,[status(thm)],[f3367,f6234]) ).
fof(f6712,plain,
earray_8 = earray_205,
inference(backward_demodulation,[status(thm)],[f5545,f2949]) ).
fof(f6741,plain,
queue_206 = rstore_seq(q8,earray_8),
inference(backward_demodulation,[status(thm)],[f6712,f555]) ).
fof(f6748,plain,
rselect_head(queue_206) = rselect_head(q8),
inference(paramodulation,[status(thm)],[f6741,f318]) ).
fof(f6751,plain,
index_209 = rselect_head(q8),
inference(forward_demodulation,[status(thm)],[f2955,f6748]) ).
fof(f6762,plain,
earray_98 = earray_91,
inference(backward_demodulation,[status(thm)],[f6237,f3346]) ).
fof(f6764,plain,
queue_92 = rstore_seq(q20,earray_98),
inference(backward_demodulation,[status(thm)],[f6762,f583]) ).
fof(f6768,plain,
rselect_head(queue_92) = rselect_head(q20),
inference(paramodulation,[status(thm)],[f6764,f318]) ).
fof(f6771,plain,
index_95 = rselect_head(q20),
inference(forward_demodulation,[status(thm)],[f3351,f6768]) ).
fof(f7149,plain,
rselect_head(queue_101) = index_96,
inference(forward_demodulation,[status(thm)],[f3365,f2689]) ).
fof(f7150,plain,
rselect_head(q22) = index_96,
inference(forward_demodulation,[status(thm)],[f7149,f2693]) ).
fof(f7176,plain,
rselect_head(queue_107) = index_96,
inference(forward_demodulation,[status(thm)],[f7150,f2699]) ).
fof(f7177,plain,
rselect_head(q23) = index_96,
inference(forward_demodulation,[status(thm)],[f7176,f2708]) ).
fof(f7186,plain,
rselect_head(queue_11) = index_210,
inference(forward_demodulation,[status(thm)],[f2959,f2720]) ).
fof(f7187,plain,
index_116 = index_96,
inference(backward_demodulation,[status(thm)],[f7188,f7177]) ).
fof(f7188,plain,
index_116 = rselect_head(q23),
inference(forward_demodulation,[status(thm)],[f2730,f2724]) ).
fof(f7197,plain,
index_116 = s(index_95),
inference(backward_demodulation,[status(thm)],[f7187,f513]) ).
fof(f7339,plain,
rselect_head(queue_122) = index_117,
inference(forward_demodulation,[status(thm)],[f2734,f2738]) ).
fof(f7340,plain,
rselect_head(q25) = index_117,
inference(forward_demodulation,[status(thm)],[f7339,f2742]) ).
fof(f7357,plain,
rselect_head(queue_128) = index_117,
inference(forward_demodulation,[status(thm)],[f7340,f2753]) ).
fof(f7358,plain,
rselect_head(q10) = index_210,
inference(forward_demodulation,[status(thm)],[f7186,f2757]) ).
fof(f7359,plain,
rselect_head(q26) = index_117,
inference(forward_demodulation,[status(thm)],[f7357,f2768]) ).
fof(f7360,plain,
index_137 = rselect_head(q26),
inference(forward_demodulation,[status(thm)],[f2780,f2774]) ).
fof(f7365,plain,
index_138 = s(index_117),
inference(backward_demodulation,[status(thm)],[f7367,f449]) ).
fof(f7367,plain,
index_137 = index_117,
inference(forward_demodulation,[status(thm)],[f7359,f7360]) ).
fof(f7450,plain,
rselect_head(queue_143) = index_138,
inference(forward_demodulation,[status(thm)],[f2790,f2794]) ).
fof(f7451,plain,
rselect_head(q28) = index_138,
inference(forward_demodulation,[status(thm)],[f7450,f2798]) ).
fof(f7452,plain,
rselect_head(queue_149) = index_138,
inference(forward_demodulation,[status(thm)],[f7451,f2809]) ).
fof(f7453,plain,
rselect_head(q29) = index_138,
inference(forward_demodulation,[status(thm)],[f7452,f2813]) ).
fof(f7454,plain,
index_158 = rselect_head(q2),
inference(forward_demodulation,[status(thm)],[f2831,f2819]) ).
fof(f7477,plain,
index_167 = rselect_head(q29),
inference(forward_demodulation,[status(thm)],[f2845,f2839]) ).
fof(f7481,plain,
index_213 = s(index_138),
inference(backward_demodulation,[status(thm)],[f7484,f2859]) ).
fof(f7484,plain,
index_167 = index_138,
inference(forward_demodulation,[status(thm)],[f7453,f7477]) ).
fof(f7544,plain,
earray_212 = rselect_seq(queue_164),
inference(forward_demodulation,[status(thm)],[f2850,f2843]) ).
fof(f7547,plain,
elem_214 = select(earray_163,index_213),
inference(backward_demodulation,[status(thm)],[f7548,f432]) ).
fof(f7548,plain,
earray_212 = earray_163,
inference(forward_demodulation,[status(thm)],[f2840,f7544]) ).
fof(f7550,plain,
rselect_head(queue_17) = index_210,
inference(forward_demodulation,[status(thm)],[f7358,f2853]) ).
fof(f7565,plain,
rselect_head(queue_173) = index_159,
inference(forward_demodulation,[status(thm)],[f2835,f2861]) ).
fof(f7566,plain,
rselect_head(q4) = index_159,
inference(forward_demodulation,[status(thm)],[f7565,f2865]) ).
fof(f7574,plain,
rselect_head(queue_179) = index_159,
inference(forward_demodulation,[status(thm)],[f7566,f2871]) ).
fof(f7575,plain,
rselect_head(q5) = index_159,
inference(forward_demodulation,[status(thm)],[f7574,f2880]) ).
fof(f7576,plain,
index_188 = rselect_head(q5),
inference(forward_demodulation,[status(thm)],[f2892,f2886]) ).
fof(f7581,plain,
index_189 = s(index_159),
inference(backward_demodulation,[status(thm)],[f7583,f471]) ).
fof(f7583,plain,
index_188 = index_159,
inference(forward_demodulation,[status(thm)],[f7575,f7576]) ).
fof(f7658,plain,
rselect_head(q11) = index_210,
inference(forward_demodulation,[status(thm)],[f7550,f2900]) ).
fof(f7659,plain,
rselect_head(queue_194) = index_189,
inference(forward_demodulation,[status(thm)],[f2914,f2918]) ).
fof(f7667,plain,
rselect_head(q7) = index_189,
inference(forward_demodulation,[status(thm)],[f7659,f2922]) ).
fof(f7668,plain,
rselect_head(queue_200) = index_189,
inference(forward_demodulation,[status(thm)],[f7667,f2928]) ).
fof(f7669,plain,
index_209 = rselect_head(queue_200),
inference(forward_demodulation,[status(thm)],[f6751,f2932]) ).
fof(f7675,plain,
index_210 = s(index_189),
inference(backward_demodulation,[status(thm)],[f7677,f480]) ).
fof(f7677,plain,
index_209 = index_189,
inference(forward_demodulation,[status(thm)],[f7668,f7669]) ).
fof(f7760,plain,
index_26 = rselect_head(q11),
inference(forward_demodulation,[status(thm)],[f2972,f2966]) ).
fof(f7765,plain,
index_27 = s(index_210),
inference(backward_demodulation,[status(thm)],[f7767,f484]) ).
fof(f7767,plain,
index_26 = index_210,
inference(forward_demodulation,[status(thm)],[f7658,f7760]) ).
fof(f7820,plain,
rselect_head(queue_32) = index_27,
inference(forward_demodulation,[status(thm)],[f2976,f2983]) ).
fof(f7826,plain,
rselect_head(q13) = index_27,
inference(forward_demodulation,[status(thm)],[f7820,f3139]) ).
fof(f7848,plain,
rselect_head(queue_38) = index_27,
inference(forward_demodulation,[status(thm)],[f7826,f3145]) ).
fof(f7849,plain,
rselect_head(q14) = index_27,
inference(forward_demodulation,[status(thm)],[f7848,f3154]) ).
fof(f7857,plain,
index_47 = rselect_head(q14),
inference(forward_demodulation,[status(thm)],[f3166,f3160]) ).
fof(f7862,plain,
index_48 = s(index_27),
inference(backward_demodulation,[status(thm)],[f7864,f493]) ).
fof(f7864,plain,
index_47 = index_27,
inference(forward_demodulation,[status(thm)],[f7849,f7857]) ).
fof(f7917,plain,
rselect_head(queue_53) = index_48,
inference(forward_demodulation,[status(thm)],[f3176,f3185]) ).
fof(f7918,plain,
rselect_head(q16) = index_48,
inference(forward_demodulation,[status(thm)],[f7917,f3195]) ).
fof(f7919,plain,
rselect_head(queue_59) = index_48,
inference(forward_demodulation,[status(thm)],[f7918,f3201]) ).
fof(f7920,plain,
rselect_head(q17) = index_48,
inference(forward_demodulation,[status(thm)],[f7919,f3205]) ).
fof(f7927,plain,
index_68 = rselect_head(q17),
inference(forward_demodulation,[status(thm)],[f3228,f3221]) ).
fof(f7932,plain,
index_69 = s(index_48),
inference(backward_demodulation,[status(thm)],[f7934,f502]) ).
fof(f7934,plain,
index_68 = index_48,
inference(forward_demodulation,[status(thm)],[f7920,f7927]) ).
fof(f7991,plain,
rselect_head(q1) = index_3,
inference(forward_demodulation,[status(thm)],[f3183,f3230]) ).
fof(f7992,plain,
rselect_head(queue_74) = index_69,
inference(forward_demodulation,[status(thm)],[f3243,f3247]) ).
fof(f7993,plain,
rselect_head(q19) = index_69,
inference(forward_demodulation,[status(thm)],[f7992,f3251]) ).
fof(f7994,plain,
rselect_head(queue_80) = index_3,
inference(forward_demodulation,[status(thm)],[f7991,f3262]) ).
fof(f8003,plain,
index_158 = rselect_head(queue_80),
inference(forward_demodulation,[status(thm)],[f7454,f3319]) ).
fof(f8009,plain,
index_159 = s(index_3),
inference(backward_demodulation,[status(thm)],[f8011,f458]) ).
fof(f8011,plain,
index_158 = index_3,
inference(forward_demodulation,[status(thm)],[f7994,f8003]) ).
fof(f8012,plain,
index_159 = index_78,
inference(forward_demodulation,[status(thm)],[f3238,f8009]) ).
fof(f8016,plain,
index_189 = s(index_78),
inference(backward_demodulation,[status(thm)],[f8012,f7581]) ).
fof(f8025,plain,
index_189 = index_153,
inference(forward_demodulation,[status(thm)],[f3332,f8016]) ).
fof(f8032,plain,
index_210 = s(index_153),
inference(backward_demodulation,[status(thm)],[f8025,f7675]) ).
fof(f8040,plain,
index_210 = index_171,
inference(forward_demodulation,[status(thm)],[f3823,f8032]) ).
fof(f8046,plain,
index_27 = s(index_171),
inference(backward_demodulation,[status(thm)],[f8040,f7765]) ).
fof(f8056,plain,
index_27 = index_177,
inference(forward_demodulation,[status(thm)],[f2877,f8046]) ).
fof(f8071,plain,
index_48 = s(index_177),
inference(backward_demodulation,[status(thm)],[f8056,f7862]) ).
fof(f8081,plain,
index_48 = index_183,
inference(forward_demodulation,[status(thm)],[f2897,f8071]) ).
fof(f8092,plain,
index_69 = s(index_183),
inference(backward_demodulation,[status(thm)],[f8081,f7932]) ).
fof(f8101,plain,
index_69 = index_192,
inference(forward_demodulation,[status(thm)],[f4211,f8092]) ).
fof(f8104,plain,
rselect_head(q19) = index_192,
inference(backward_demodulation,[status(thm)],[f8101,f7993]) ).
fof(f8184,plain,
rselect_head(queue_86) = index_192,
inference(forward_demodulation,[status(thm)],[f8104,f3325]) ).
fof(f8185,plain,
index_95 = rselect_head(queue_86),
inference(forward_demodulation,[status(thm)],[f6771,f3339]) ).
fof(f8188,plain,
index_116 = s(index_192),
inference(backward_demodulation,[status(thm)],[f8193,f7197]) ).
fof(f8193,plain,
index_95 = index_192,
inference(forward_demodulation,[status(thm)],[f8184,f8185]) ).
fof(f8194,plain,
index_116 = index_198,
inference(forward_demodulation,[status(thm)],[f2940,f8188]) ).
fof(f8232,plain,
index_117 = s(index_198),
inference(backward_demodulation,[status(thm)],[f8194,f440]) ).
fof(f8234,plain,
index_117 = index_204,
inference(forward_demodulation,[status(thm)],[f2945,f8232]) ).
fof(f8243,plain,
index_138 = s(index_204),
inference(backward_demodulation,[status(thm)],[f8234,f7365]) ).
fof(f8253,plain,
index_138 = index_9,
inference(forward_demodulation,[status(thm)],[f4595,f8243]) ).
fof(f8260,plain,
index_213 = s(index_9),
inference(backward_demodulation,[status(thm)],[f8253,f7481]) ).
fof(f8269,plain,
index_213 = index_15,
inference(forward_demodulation,[status(thm)],[f2765,f8260]) ).
fof(f8278,plain,
elem_214 = select(earray_163,index_15),
inference(backward_demodulation,[status(thm)],[f8269,f7547]) ).
fof(f8687,plain,
s(s(index_30)) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3983]) ).
fof(f8688,plain,
s(index_36) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f8687]) ).
fof(f8689,plain,
index_42 != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f8688]) ).
fof(f9646,plain,
s(s(s(index_30))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3984]) ).
fof(f9647,plain,
s(s(index_36)) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f9646]) ).
fof(f9648,plain,
s(index_42) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f9647]) ).
fof(f9649,plain,
index_51 != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f9648]) ).
fof(f10209,plain,
s(s(s(s(index_30)))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3985]) ).
fof(f10210,plain,
s(s(s(index_36))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f10209]) ).
fof(f10211,plain,
s(s(index_42)) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f10210]) ).
fof(f10212,plain,
s(index_51) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f10211]) ).
fof(f10213,plain,
index_57 != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f10212]) ).
fof(f10406,plain,
! [X0] :
( select(earray_106,X0) = select(earray_100,X0)
| index_105 = X0 ),
inference(forward_demodulation,[status(thm)],[f2981,f1728]) ).
fof(f10409,plain,
! [X0] :
( select(earray_112,X0) = select(earray_106,X0)
| index_111 = X0 ),
inference(forward_demodulation,[status(thm)],[f3038,f1730]) ).
fof(f10420,plain,
! [X0] :
( select(earray_121,X0) = select(earray_112,X0)
| index_120 = X0 ),
inference(forward_demodulation,[status(thm)],[f4378,f1732]) ).
fof(f10423,plain,
! [X0] :
( select(earray_127,X0) = select(earray_121,X0)
| index_126 = X0 ),
inference(forward_demodulation,[status(thm)],[f3267,f1784]) ).
fof(f10426,plain,
! [X0] :
( select(earray_133,X0) = select(earray_127,X0)
| index_132 = X0 ),
inference(forward_demodulation,[status(thm)],[f3424,f1836]) ).
fof(f10429,plain,
! [X0] :
( select(earray_142,X0) = select(earray_133,X0)
| index_141 = X0 ),
inference(forward_demodulation,[status(thm)],[f4993,f1838]) ).
fof(f10432,plain,
! [X0] :
( select(earray_148,X0) = select(earray_142,X0)
| index_147 = X0 ),
inference(forward_demodulation,[status(thm)],[f3602,f1940]) ).
fof(f10450,plain,
! [X0] :
( select(earray_163,X0) = select(earray_148,X0)
| index_162 = X0 ),
inference(forward_demodulation,[status(thm)],[f3607,f1944]) ).
fof(f10451,plain,
( elem_214 = select(earray_148,index_15)
| index_162 = index_15 ),
inference(paramodulation,[status(thm)],[f8278,f10450]) ).
fof(f10455,plain,
( index_147 = index_15
| elem_214 = select(earray_142,index_15)
| index_162 = index_15 ),
inference(paramodulation,[status(thm)],[f10432,f10451]) ).
fof(f10550,plain,
! [X0] :
( select(earray_22,X0) = select(earray_16,X0)
| index_21 = X0 ),
inference(forward_demodulation,[status(thm)],[f4205,f2158]) ).
fof(f10553,plain,
! [X0] :
( select(earray_31,X0) = select(earray_22,X0)
| index_30 = X0 ),
inference(forward_demodulation,[status(thm)],[f5702,f2210]) ).
fof(f10577,plain,
! [X0] :
( select(earray_37,X0) = select(earray_31,X0)
| index_36 = X0 ),
inference(forward_demodulation,[status(thm)],[f4975,f2212]) ).
fof(f10587,plain,
! [X0] :
( select(earray_43,X0) = select(earray_37,X0)
| index_42 = X0 ),
inference(forward_demodulation,[status(thm)],[f4978,f2366]) ).
fof(f10590,plain,
! [X0] :
( select(earray_52,X0) = select(earray_43,X0)
| index_51 = X0 ),
inference(forward_demodulation,[status(thm)],[f5869,f2368]) ).
fof(f10593,plain,
! [X0] :
( select(earray_58,X0) = select(earray_52,X0)
| index_57 = X0 ),
inference(forward_demodulation,[status(thm)],[f5356,f2370]) ).
fof(f10596,plain,
! [X0] :
( select(earray_64,X0) = select(earray_58,X0)
| index_63 = X0 ),
inference(forward_demodulation,[status(thm)],[f5361,f2472]) ).
fof(f10624,plain,
! [X0] :
( select(earray_73,X0) = select(earray_64,X0)
| index_72 = X0 ),
inference(forward_demodulation,[status(thm)],[f6055,f2474]) ).
fof(f10635,plain,
! [X0] :
( select(earray_85,X0) = select(earray_73,X0)
| index_84 = X0 ),
inference(forward_demodulation,[status(thm)],[f5538,f2578]) ).
fof(f10638,plain,
! [X0] :
( select(earray_98,X0) = select(earray_89,X0)
| index_90 = X0 ),
inference(forward_demodulation,[status(thm)],[f6762,f2580]) ).
fof(f10639,plain,
! [X0] :
( select(earray_98,X0) = select(earray_85,X0)
| index_90 = X0 ),
inference(forward_demodulation,[status(thm)],[f5696,f10638]) ).
fof(f10641,plain,
! [X0] :
( index_84 = X0
| select(earray_98,X0) = select(earray_73,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f10635,f10639]) ).
fof(f11723,plain,
s(s(s(s(s(index_30))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3986]) ).
fof(f11724,plain,
s(s(s(s(index_36)))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f11723]) ).
fof(f11725,plain,
s(s(s(index_42))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f11724]) ).
fof(f11726,plain,
s(s(index_51)) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f11725]) ).
fof(f11727,plain,
s(index_57) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f11726]) ).
fof(f11728,plain,
index_63 != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f11727]) ).
fof(f12398,plain,
s(s(s(s(s(s(index_30)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3987]) ).
fof(f12399,plain,
s(s(s(s(s(index_36))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f12398]) ).
fof(f12400,plain,
s(s(s(s(index_42)))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f12399]) ).
fof(f12401,plain,
s(s(s(index_51))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f12400]) ).
fof(f12402,plain,
s(s(index_57)) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f12401]) ).
fof(f12403,plain,
s(index_63) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f12402]) ).
fof(f12404,plain,
index_72 != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f12403]) ).
fof(f12761,plain,
! [X0] :
( index_72 = X0
| index_84 = X0
| select(earray_98,X0) = select(earray_64,X0)
| index_90 = X0 ),
inference(paramodulation,[status(thm)],[f10624,f10641]) ).
fof(f13234,plain,
s(s(s(s(s(s(s(index_30))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3988]) ).
fof(f13235,plain,
s(s(s(s(s(s(index_36)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f13234]) ).
fof(f13236,plain,
s(s(s(s(s(index_42))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f13235]) ).
fof(f13237,plain,
s(s(s(s(index_51)))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f13236]) ).
fof(f13238,plain,
s(s(s(index_57))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f13237]) ).
fof(f13239,plain,
s(s(index_63)) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f13238]) ).
fof(f13240,plain,
s(index_72) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f13239]) ).
fof(f13241,plain,
index_84 != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f13240]) ).
fof(f13483,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)],[f10596,f12761]) ).
fof(f14581,plain,
s(s(s(s(s(s(s(s(index_30)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3989]) ).
fof(f14582,plain,
s(s(s(s(s(s(s(index_36))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f14581]) ).
fof(f14583,plain,
s(s(s(s(s(s(index_42)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f14582]) ).
fof(f14584,plain,
s(s(s(s(s(index_51))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f14583]) ).
fof(f14585,plain,
s(s(s(s(index_57)))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f14584]) ).
fof(f14586,plain,
s(s(s(index_63))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f14585]) ).
fof(f14587,plain,
s(s(index_72)) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f14586]) ).
fof(f14588,plain,
s(index_84) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f14587]) ).
fof(f14589,plain,
index_90 != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f14588]) ).
fof(f15758,plain,
s(s(s(s(s(s(s(s(s(index_30))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3990]) ).
fof(f15759,plain,
s(s(s(s(s(s(s(s(index_36)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f15758]) ).
fof(f15760,plain,
s(s(s(s(s(s(s(index_42))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f15759]) ).
fof(f15761,plain,
s(s(s(s(s(s(index_51)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f15760]) ).
fof(f15762,plain,
s(s(s(s(s(index_57))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f15761]) ).
fof(f15763,plain,
s(s(s(s(index_63)))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f15762]) ).
fof(f15764,plain,
s(s(s(index_72))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f15763]) ).
fof(f15765,plain,
s(s(index_84)) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f15764]) ).
fof(f15766,plain,
s(index_90) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f15765]) ).
fof(f15767,plain,
index_99 != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f15766]) ).
fof(f16516,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)],[f10593,f13483]) ).
fof(f17427,plain,
s(s(s(s(s(s(s(s(s(s(index_30)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3991]) ).
fof(f17428,plain,
s(s(s(s(s(s(s(s(s(index_36))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f17427]) ).
fof(f17429,plain,
s(s(s(s(s(s(s(s(index_42)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f17428]) ).
fof(f17430,plain,
s(s(s(s(s(s(s(index_51))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f17429]) ).
fof(f17431,plain,
s(s(s(s(s(s(index_57)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f17430]) ).
fof(f17432,plain,
s(s(s(s(s(index_63))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f17431]) ).
fof(f17433,plain,
s(s(s(s(index_72)))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f17432]) ).
fof(f17434,plain,
s(s(s(index_84))) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f17433]) ).
fof(f17435,plain,
s(s(index_90)) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f17434]) ).
fof(f17436,plain,
s(index_99) != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f17435]) ).
fof(f17438,plain,
index_105 != index_15,
inference(forward_demodulation,[status(thm)],[f2705,f17436]) ).
fof(f17718,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)],[f10590,f16516]) ).
fof(f18588,plain,
s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3992]) ).
fof(f18589,plain,
s(s(s(s(s(s(s(s(s(s(index_36)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f18588]) ).
fof(f18590,plain,
s(s(s(s(s(s(s(s(s(index_42))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f18589]) ).
fof(f18591,plain,
s(s(s(s(s(s(s(s(index_51)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f18590]) ).
fof(f18592,plain,
s(s(s(s(s(s(s(index_57))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f18591]) ).
fof(f18593,plain,
s(s(s(s(s(s(index_63)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f18592]) ).
fof(f18594,plain,
s(s(s(s(s(index_72))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f18593]) ).
fof(f18595,plain,
s(s(s(s(index_84)))) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f18594]) ).
fof(f18596,plain,
s(s(s(index_90))) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f18595]) ).
fof(f18597,plain,
s(s(index_99)) != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f18596]) ).
fof(f18598,plain,
s(index_105) != index_15,
inference(forward_demodulation,[status(thm)],[f2705,f18597]) ).
fof(f18601,plain,
index_111 != index_15,
inference(forward_demodulation,[status(thm)],[f2717,f18598]) ).
fof(f20018,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4806,f3993]) ).
fof(f20019,plain,
s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f20018]) ).
fof(f20020,plain,
s(s(s(s(s(s(s(s(s(s(index_42)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f20019]) ).
fof(f20021,plain,
s(s(s(s(s(s(s(s(s(index_51))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f20020]) ).
fof(f20022,plain,
s(s(s(s(s(s(s(s(index_57)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f20021]) ).
fof(f20023,plain,
s(s(s(s(s(s(s(index_63))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f20022]) ).
fof(f20024,plain,
s(s(s(s(s(s(index_72)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f20023]) ).
fof(f20025,plain,
s(s(s(s(s(index_84))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f20024]) ).
fof(f20026,plain,
s(s(s(s(index_90)))) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f20025]) ).
fof(f20027,plain,
s(s(s(index_99))) != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f20026]) ).
fof(f20028,plain,
s(s(index_105)) != index_15,
inference(forward_demodulation,[status(thm)],[f2705,f20027]) ).
fof(f20029,plain,
s(index_111) != index_15,
inference(forward_demodulation,[status(thm)],[f2717,f20028]) ).
fof(f20033,plain,
index_120 != index_15,
inference(forward_demodulation,[status(thm)],[f3193,f20029]) ).
fof(f20758,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)],[f10587,f17718]) ).
fof(f21111,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2904,f1368]) ).
fof(f21112,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4811,f21111]) ).
fof(f21113,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f21112]) ).
fof(f21114,plain,
s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f21113]) ).
fof(f21115,plain,
s(s(s(s(s(s(s(s(s(s(index_51)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f21114]) ).
fof(f21116,plain,
s(s(s(s(s(s(s(s(s(index_57))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f21115]) ).
fof(f21117,plain,
s(s(s(s(s(s(s(s(index_63)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f21116]) ).
fof(f21118,plain,
s(s(s(s(s(s(s(index_72))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f21117]) ).
fof(f21119,plain,
s(s(s(s(s(s(index_84)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f21118]) ).
fof(f21120,plain,
s(s(s(s(s(index_90))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f21119]) ).
fof(f21121,plain,
s(s(s(s(index_99)))) != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f21120]) ).
fof(f21122,plain,
s(s(s(index_105))) != index_15,
inference(forward_demodulation,[status(thm)],[f2705,f21121]) ).
fof(f21123,plain,
s(s(index_111)) != index_15,
inference(forward_demodulation,[status(thm)],[f2717,f21122]) ).
fof(f21124,plain,
s(index_120) != index_15,
inference(forward_demodulation,[status(thm)],[f3193,f21123]) ).
fof(f21129,plain,
index_126 != index_15,
inference(forward_demodulation,[status(thm)],[f2750,f21124]) ).
fof(f21138,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2904,f1369]) ).
fof(f21139,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4811,f21138]) ).
fof(f21140,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f21139]) ).
fof(f21141,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f21140]) ).
fof(f21142,plain,
s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f21141]) ).
fof(f21143,plain,
s(s(s(s(s(s(s(s(s(s(index_57)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f21142]) ).
fof(f21144,plain,
s(s(s(s(s(s(s(s(s(index_63))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f21143]) ).
fof(f21145,plain,
s(s(s(s(s(s(s(s(index_72)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f21144]) ).
fof(f21146,plain,
s(s(s(s(s(s(s(index_84))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f21145]) ).
fof(f21147,plain,
s(s(s(s(s(s(index_90)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f21146]) ).
fof(f21148,plain,
s(s(s(s(s(index_99))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f21147]) ).
fof(f21149,plain,
s(s(s(s(index_105)))) != index_15,
inference(forward_demodulation,[status(thm)],[f2705,f21148]) ).
fof(f21150,plain,
s(s(s(index_111))) != index_15,
inference(forward_demodulation,[status(thm)],[f2717,f21149]) ).
fof(f21151,plain,
s(s(index_120)) != index_15,
inference(forward_demodulation,[status(thm)],[f3193,f21150]) ).
fof(f21152,plain,
s(index_126) != index_15,
inference(forward_demodulation,[status(thm)],[f2750,f21151]) ).
fof(f21158,plain,
index_132 != index_15,
inference(forward_demodulation,[status(thm)],[f2785,f21152]) ).
fof(f21159,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2904,f1370]) ).
fof(f21160,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)],[f4811,f21159]) ).
fof(f21161,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3151,f21160]) ).
fof(f21162,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f21161]) ).
fof(f21163,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f21162]) ).
fof(f21164,plain,
s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f21163]) ).
fof(f21165,plain,
s(s(s(s(s(s(s(s(s(s(index_63)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f21164]) ).
fof(f21166,plain,
s(s(s(s(s(s(s(s(s(index_72))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f21165]) ).
fof(f21167,plain,
s(s(s(s(s(s(s(s(index_84)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f21166]) ).
fof(f21168,plain,
s(s(s(s(s(s(s(index_90))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f21167]) ).
fof(f21169,plain,
s(s(s(s(s(s(index_99)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f21168]) ).
fof(f21170,plain,
s(s(s(s(s(index_105))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2705,f21169]) ).
fof(f21171,plain,
s(s(s(s(index_111)))) != index_15,
inference(forward_demodulation,[status(thm)],[f2717,f21170]) ).
fof(f21172,plain,
s(s(s(index_120))) != index_15,
inference(forward_demodulation,[status(thm)],[f3193,f21171]) ).
fof(f21173,plain,
s(s(index_126)) != index_15,
inference(forward_demodulation,[status(thm)],[f2750,f21172]) ).
fof(f21174,plain,
s(index_132) != index_15,
inference(forward_demodulation,[status(thm)],[f2785,f21173]) ).
fof(f21176,plain,
index_141 != index_15,
inference(forward_demodulation,[status(thm)],[f3545,f21174]) ).
fof(f21177,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2904,f1371]) ).
fof(f21178,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)],[f4811,f21177]) ).
fof(f21179,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)],[f3151,f21178]) ).
fof(f21180,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3171,f21179]) ).
fof(f21181,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f21180]) ).
fof(f21182,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_57)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f21181]) ).
fof(f21183,plain,
s(s(s(s(s(s(s(s(s(s(s(index_63))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f21182]) ).
fof(f21184,plain,
s(s(s(s(s(s(s(s(s(s(index_72)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f21183]) ).
fof(f21185,plain,
s(s(s(s(s(s(s(s(s(index_84))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f21184]) ).
fof(f21186,plain,
s(s(s(s(s(s(s(s(index_90)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f21185]) ).
fof(f21187,plain,
s(s(s(s(s(s(s(index_99))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f21186]) ).
fof(f21188,plain,
s(s(s(s(s(s(index_105)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2705,f21187]) ).
fof(f21189,plain,
s(s(s(s(s(index_111))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2717,f21188]) ).
fof(f21190,plain,
s(s(s(s(index_120)))) != index_15,
inference(forward_demodulation,[status(thm)],[f3193,f21189]) ).
fof(f21191,plain,
s(s(s(index_126))) != index_15,
inference(forward_demodulation,[status(thm)],[f2750,f21190]) ).
fof(f21192,plain,
s(s(index_132)) != index_15,
inference(forward_demodulation,[status(thm)],[f2785,f21191]) ).
fof(f21193,plain,
s(index_141) != index_15,
inference(forward_demodulation,[status(thm)],[f3545,f21192]) ).
fof(f21194,plain,
( elem_214 = select(earray_142,index_15)
| index_162 = index_15 ),
inference(backward_subsumption_resolution,[status(thm)],[f10455,f21195]) ).
fof(f21195,plain,
index_147 != index_15,
inference(forward_demodulation,[status(thm)],[f2806,f21193]) ).
fof(f21196,plain,
( index_141 = index_15
| elem_214 = select(earray_133,index_15)
| index_162 = index_15 ),
inference(paramodulation,[status(thm)],[f10429,f21194]) ).
fof(f21198,plain,
( elem_214 = select(earray_133,index_15)
| index_162 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f21196,f21176]) ).
fof(f21200,plain,
( index_132 = index_15
| elem_214 = select(earray_127,index_15)
| index_162 = index_15 ),
inference(paramodulation,[status(thm)],[f10426,f21198]) ).
fof(f21202,plain,
( elem_214 = select(earray_127,index_15)
| index_162 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f21200,f21158]) ).
fof(f21204,plain,
( index_126 = index_15
| elem_214 = select(earray_121,index_15)
| index_162 = index_15 ),
inference(paramodulation,[status(thm)],[f10423,f21202]) ).
fof(f21206,plain,
( elem_214 = select(earray_121,index_15)
| index_162 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f21204,f21129]) ).
fof(f21208,plain,
( index_120 = index_15
| elem_214 = select(earray_112,index_15)
| index_162 = index_15 ),
inference(paramodulation,[status(thm)],[f10420,f21206]) ).
fof(f21210,plain,
( elem_214 = select(earray_112,index_15)
| index_162 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f21208,f20033]) ).
fof(f21212,plain,
( index_111 = index_15
| elem_214 = select(earray_106,index_15)
| index_162 = index_15 ),
inference(paramodulation,[status(thm)],[f10409,f21210]) ).
fof(f21214,plain,
( elem_214 = select(earray_106,index_15)
| index_162 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f21212,f18601]) ).
fof(f21216,plain,
( index_105 = index_15
| elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(paramodulation,[status(thm)],[f10406,f21214]) ).
fof(f21218,plain,
( elem_214 = select(earray_100,index_15)
| index_162 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f21216,f17438]) ).
fof(f21220,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2904,f1372]) ).
fof(f21221,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)],[f4811,f21220]) ).
fof(f21222,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)],[f3151,f21221]) ).
fof(f21223,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)],[f3171,f21222]) ).
fof(f21224,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f4986,f21223]) ).
fof(f21225,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3213,f21224]) ).
fof(f21226,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_63)))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3218,f21225]) ).
fof(f21227,plain,
s(s(s(s(s(s(s(s(s(s(s(index_72))))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5528,f21226]) ).
fof(f21228,plain,
s(s(s(s(s(s(s(s(s(s(index_84)))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3259,f21227]) ).
fof(f21229,plain,
s(s(s(s(s(s(s(s(s(index_90))))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3360,f21228]) ).
fof(f21230,plain,
s(s(s(s(s(s(s(s(index_99)))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f5862,f21229]) ).
fof(f21231,plain,
s(s(s(s(s(s(s(index_105))))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2705,f21230]) ).
fof(f21232,plain,
s(s(s(s(s(s(index_111)))))) != index_15,
inference(forward_demodulation,[status(thm)],[f2717,f21231]) ).
fof(f21233,plain,
s(s(s(s(s(index_120))))) != index_15,
inference(forward_demodulation,[status(thm)],[f3193,f21232]) ).
fof(f21234,plain,
s(s(s(s(index_126)))) != index_15,
inference(forward_demodulation,[status(thm)],[f2750,f21233]) ).
fof(f21235,plain,
s(s(s(index_132))) != index_15,
inference(forward_demodulation,[status(thm)],[f2785,f21234]) ).
fof(f21236,plain,
s(s(index_141)) != index_15,
inference(forward_demodulation,[status(thm)],[f3545,f21235]) ).
fof(f21237,plain,
s(index_147) != index_15,
inference(forward_demodulation,[status(thm)],[f2806,f21236]) ).
fof(f21238,plain,
elem_214 = select(earray_100,index_15),
inference(backward_subsumption_resolution,[status(thm)],[f21218,f21246]) ).
fof(f21246,plain,
index_162 != index_15,
inference(forward_demodulation,[status(thm)],[f2826,f21237]) ).
fof(f22546,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)],[f10577,f20758]) ).
fof(f25719,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)],[f10553,f22546]) ).
fof(f27463,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)],[f10550,f25719]) ).
fof(f30588,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)],[f618,f27463]) ).
fof(f30592,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)],[f30588,f14589]) ).
fof(f30594,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)],[f30592,f13241]) ).
fof(f30595,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)],[f1626,f30594]) ).
fof(f30597,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)],[f21238,f30595]) ).
fof(f30598,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)],[f30597,f617]) ).
fof(f30601,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)],[f30598,f12404]) ).
fof(f30602,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)],[f30601,f11728]) ).
fof(f30634,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)],[f30602,f10213]) ).
fof(f30645,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)],[f30634,f9649]) ).
fof(f30646,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15
| index_36 = index_15 ),
inference(resolution,[status(thm)],[f30645,f8689]) ).
fof(f30676,plain,
( index_99 = index_15
| index_21 = index_15
| index_30 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f30646,f6043]) ).
fof(f30689,plain,
( index_99 = index_15
| index_21 = index_15 ),
inference(forward_subsumption_resolution,[status(thm)],[f30676,f4808]) ).
fof(f30690,plain,
index_99 = index_15,
inference(resolution,[status(thm)],[f30689,f2908]) ).
fof(f30716,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f30690,f15767]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n026.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 09:13:28 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.15/5.41 % Drodi V4.1.1
% 9.34/6.65 % Refutation found
% 9.34/6.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.34/6.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 9.34/6.69 % Elapsed time: 1.300792 seconds
% 9.34/6.69 % CPU time: 9.904724 seconds
% 9.34/6.69 % Total memory used: 266.285 MB
% 9.34/6.69 % Net memory used: 264.348 MB
%------------------------------------------------------------------------------