%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV569-1.040 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 21:44:22 EDT 2022
% Result : Unsatisfiable 35.80s 36.21s
% Output : Refutation 36.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 329
% Syntax : Number of clauses : 1174 ( 811 unt; 363 nHn;1174 RR)
% Number of literals : 1660 ( 0 equ; 166 neg)
% Maximal clause size : 8 ( 1 avg)
% Maximal term depth : 27 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 350 ( 350 usr; 347 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(select(store(u,v,w),v),w),
file('SWV569-1.040.p',unknown),
[] ).
cnf(2,axiom,
( equal(u,v)
| equal(select(store(w,u,x),v),select(w,v)) ),
file('SWV569-1.040.p',unknown),
[] ).
cnf(3,axiom,
~ equal(tail,head),
file('SWV569-1.040.p',unknown),
[] ).
cnf(4,axiom,
~ equal(seq,head),
file('SWV569-1.040.p',unknown),
[] ).
cnf(5,axiom,
~ equal(seq,tail),
file('SWV569-1.040.p',unknown),
[] ).
cnf(46,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(47,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(48,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(49,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(50,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(51,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(52,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(53,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(54,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(55,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(56,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(57,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(58,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(59,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(60,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(61,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(u))))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(62,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(u)))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(63,axiom,
~ equal(s(s(s(s(s(s(s(s(s(u))))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(64,axiom,
~ equal(s(s(s(s(s(s(s(s(u)))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(65,axiom,
~ equal(s(s(s(s(s(s(s(u))))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(66,axiom,
~ equal(s(s(s(s(s(s(u)))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(67,axiom,
~ equal(s(s(s(s(s(u))))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(68,axiom,
~ equal(s(s(s(s(u)))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(69,axiom,
~ equal(s(s(s(u))),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(70,axiom,
~ equal(s(s(u)),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(71,axiom,
~ equal(s(u),u),
file('SWV569-1.040.p',unknown),
[] ).
cnf(73,axiom,
equal(store(earray_98,index_99,e21),earray_100),
file('SWV569-1.040.p',unknown),
[] ).
cnf(74,axiom,
equal(select(q22,seq),earray_104),
file('SWV569-1.040.p',unknown),
[] ).
cnf(75,axiom,
equal(store(earray_104,index_105,e22),earray_106),
file('SWV569-1.040.p',unknown),
[] ).
cnf(76,axiom,
equal(select(q23,seq),earray_110),
file('SWV569-1.040.p',unknown),
[] ).
cnf(77,axiom,
equal(store(earray_110,index_111,e23),earray_112),
file('SWV569-1.040.p',unknown),
[] ).
cnf(78,axiom,
equal(select(q24,seq),earray_119),
file('SWV569-1.040.p',unknown),
[] ).
cnf(79,axiom,
equal(store(earray_119,index_120,e24),earray_121),
file('SWV569-1.040.p',unknown),
[] ).
cnf(80,axiom,
equal(select(q25,seq),earray_125),
file('SWV569-1.040.p',unknown),
[] ).
cnf(81,axiom,
equal(store(earray_125,index_126,e25),earray_127),
file('SWV569-1.040.p',unknown),
[] ).
cnf(82,axiom,
equal(select(q26,seq),earray_131),
file('SWV569-1.040.p',unknown),
[] ).
cnf(83,axiom,
equal(store(earray_131,index_132,e26),earray_133),
file('SWV569-1.040.p',unknown),
[] ).
cnf(85,axiom,
equal(select(q27,seq),earray_140),
file('SWV569-1.040.p',unknown),
[] ).
cnf(86,axiom,
equal(store(earray_140,index_141,e27),earray_142),
file('SWV569-1.040.p',unknown),
[] ).
cnf(87,axiom,
equal(select(q28,seq),earray_146),
file('SWV569-1.040.p',unknown),
[] ).
cnf(88,axiom,
equal(store(earray_146,index_147,e28),earray_148),
file('SWV569-1.040.p',unknown),
[] ).
cnf(92,axiom,
equal(select(q29,seq),earray_161),
file('SWV569-1.040.p',unknown),
[] ).
cnf(93,axiom,
equal(store(earray_161,index_162,e29),earray_163),
file('SWV569-1.040.p',unknown),
[] ).
cnf(94,axiom,
equal(select(q30,seq),earray_170),
file('SWV569-1.040.p',unknown),
[] ).
cnf(95,axiom,
equal(store(earray_170,index_171,e30),earray_172),
file('SWV569-1.040.p',unknown),
[] ).
cnf(96,axiom,
equal(select(q31,seq),earray_176),
file('SWV569-1.040.p',unknown),
[] ).
cnf(97,axiom,
equal(store(earray_176,index_177,e31),earray_178),
file('SWV569-1.040.p',unknown),
[] ).
cnf(98,axiom,
equal(select(q32,seq),earray_182),
file('SWV569-1.040.p',unknown),
[] ).
cnf(99,axiom,
equal(store(earray_182,index_183,e32),earray_184),
file('SWV569-1.040.p',unknown),
[] ).
cnf(100,axiom,
equal(select(q33,seq),earray_191),
file('SWV569-1.040.p',unknown),
[] ).
cnf(101,axiom,
equal(store(earray_191,index_192,e33),earray_193),
file('SWV569-1.040.p',unknown),
[] ).
cnf(102,axiom,
equal(select(q34,seq),earray_197),
file('SWV569-1.040.p',unknown),
[] ).
cnf(103,axiom,
equal(store(earray_197,index_198,e34),earray_199),
file('SWV569-1.040.p',unknown),
[] ).
cnf(106,axiom,
equal(select(q35,seq),earray_203),
file('SWV569-1.040.p',unknown),
[] ).
cnf(107,axiom,
equal(store(earray_203,index_204,e35),earray_205),
file('SWV569-1.040.p',unknown),
[] ).
cnf(108,axiom,
equal(select(q36,seq),earray_212),
file('SWV569-1.040.p',unknown),
[] ).
cnf(109,axiom,
equal(store(earray_212,index_213,e36),earray_214),
file('SWV569-1.040.p',unknown),
[] ).
cnf(110,axiom,
equal(select(q37,seq),earray_218),
file('SWV569-1.040.p',unknown),
[] ).
cnf(112,axiom,
equal(store(earray_218,index_219,e37),earray_220),
file('SWV569-1.040.p',unknown),
[] ).
cnf(113,axiom,
equal(select(q38,seq),earray_224),
file('SWV569-1.040.p',unknown),
[] ).
cnf(114,axiom,
equal(store(earray_224,index_225,e38),earray_226),
file('SWV569-1.040.p',unknown),
[] ).
cnf(117,axiom,
equal(select(q39,seq),earray_239),
file('SWV569-1.040.p',unknown),
[] ).
cnf(118,axiom,
equal(store(earray_239,index_240,e39),earray_241),
file('SWV569-1.040.p',unknown),
[] ).
cnf(129,axiom,
equal(select(q40,seq),earray_281),
file('SWV569-1.040.p',unknown),
[] ).
cnf(133,axiom,
equal(store(earray_35,index_36,e13),earray_37),
file('SWV569-1.040.p',unknown),
[] ).
cnf(135,axiom,
equal(select(q14,seq),earray_41),
file('SWV569-1.040.p',unknown),
[] ).
cnf(136,axiom,
equal(store(earray_41,index_42,e14),earray_43),
file('SWV569-1.040.p',unknown),
[] ).
cnf(137,axiom,
equal(select(q15,seq),earray_50),
file('SWV569-1.040.p',unknown),
[] ).
cnf(138,axiom,
equal(store(earray_50,index_51,e15),earray_52),
file('SWV569-1.040.p',unknown),
[] ).
cnf(139,axiom,
equal(select(q16,seq),earray_56),
file('SWV569-1.040.p',unknown),
[] ).
cnf(140,axiom,
equal(store(earray_56,index_57,e16),earray_58),
file('SWV569-1.040.p',unknown),
[] ).
cnf(141,axiom,
equal(select(q17,seq),earray_62),
file('SWV569-1.040.p',unknown),
[] ).
cnf(142,axiom,
equal(store(earray_62,index_63,e17),earray_64),
file('SWV569-1.040.p',unknown),
[] ).
cnf(143,axiom,
equal(select(q18,seq),earray_71),
file('SWV569-1.040.p',unknown),
[] ).
cnf(144,axiom,
equal(store(earray_71,index_72,e18),earray_73),
file('SWV569-1.040.p',unknown),
[] ).
cnf(148,axiom,
equal(select(q19,seq),earray_83),
file('SWV569-1.040.p',unknown),
[] ).
cnf(149,axiom,
equal(store(earray_83,index_84,e19),earray_85),
file('SWV569-1.040.p',unknown),
[] ).
cnf(150,axiom,
equal(select(q20,seq),earray_89),
file('SWV569-1.040.p',unknown),
[] ).
cnf(151,axiom,
equal(store(earray_89,index_90,e20),earray_91),
file('SWV569-1.040.p',unknown),
[] ).
cnf(152,axiom,
equal(select(q21,seq),earray_98),
file('SWV569-1.040.p',unknown),
[] ).
cnf(153,axiom,
equal(select(earray_281,index_282),elem_283),
file('SWV569-1.040.p',unknown),
[] ).
cnf(154,axiom,
equal(select(q,tail),index_0),
file('SWV569-1.040.p',unknown),
[] ).
cnf(155,axiom,
equal(s(index_99),index_102),
file('SWV569-1.040.p',unknown),
[] ).
cnf(156,axiom,
equal(select(q22,tail),index_105),
file('SWV569-1.040.p',unknown),
[] ).
cnf(157,axiom,
equal(s(index_105),index_108),
file('SWV569-1.040.p',unknown),
[] ).
cnf(158,axiom,
equal(select(q23,tail),index_111),
file('SWV569-1.040.p',unknown),
[] ).
cnf(159,axiom,
equal(s(index_111),index_114),
file('SWV569-1.040.p',unknown),
[] ).
cnf(160,axiom,
equal(select(queue_115,head),index_116),
file('SWV569-1.040.p',unknown),
[] ).
cnf(161,axiom,
equal(s(index_116),index_117),
file('SWV569-1.040.p',unknown),
[] ).
cnf(162,axiom,
equal(s(index_9),index_12),
file('SWV569-1.040.p',unknown),
[] ).
cnf(163,axiom,
equal(select(q24,tail),index_120),
file('SWV569-1.040.p',unknown),
[] ).
cnf(164,axiom,
equal(s(index_120),index_123),
file('SWV569-1.040.p',unknown),
[] ).
cnf(165,axiom,
equal(select(q25,tail),index_126),
file('SWV569-1.040.p',unknown),
[] ).
cnf(166,axiom,
equal(s(index_126),index_129),
file('SWV569-1.040.p',unknown),
[] ).
cnf(167,axiom,
equal(select(q26,tail),index_132),
file('SWV569-1.040.p',unknown),
[] ).
cnf(168,axiom,
equal(s(index_132),index_135),
file('SWV569-1.040.p',unknown),
[] ).
cnf(169,axiom,
equal(select(queue_136,head),index_137),
file('SWV569-1.040.p',unknown),
[] ).
cnf(170,axiom,
equal(s(index_137),index_138),
file('SWV569-1.040.p',unknown),
[] ).
cnf(171,axiom,
equal(select(q27,tail),index_141),
file('SWV569-1.040.p',unknown),
[] ).
cnf(172,axiom,
equal(s(index_141),index_144),
file('SWV569-1.040.p',unknown),
[] ).
cnf(173,axiom,
equal(select(q28,tail),index_147),
file('SWV569-1.040.p',unknown),
[] ).
cnf(174,axiom,
equal(select(q10,tail),index_15),
file('SWV569-1.040.p',unknown),
[] ).
cnf(175,axiom,
equal(s(index_147),index_150),
file('SWV569-1.040.p',unknown),
[] ).
cnf(176,axiom,
equal(select(q2,tail),index_153),
file('SWV569-1.040.p',unknown),
[] ).
cnf(177,axiom,
equal(s(index_153),index_156),
file('SWV569-1.040.p',unknown),
[] ).
cnf(178,axiom,
equal(select(queue_157,head),index_158),
file('SWV569-1.040.p',unknown),
[] ).
cnf(179,axiom,
equal(s(index_158),index_159),
file('SWV569-1.040.p',unknown),
[] ).
cnf(180,axiom,
equal(select(q29,tail),index_162),
file('SWV569-1.040.p',unknown),
[] ).
cnf(181,axiom,
equal(s(index_162),index_165),
file('SWV569-1.040.p',unknown),
[] ).
cnf(182,axiom,
equal(select(queue_166,head),index_167),
file('SWV569-1.040.p',unknown),
[] ).
cnf(183,axiom,
equal(s(index_167),index_168),
file('SWV569-1.040.p',unknown),
[] ).
cnf(184,axiom,
equal(select(q30,tail),index_171),
file('SWV569-1.040.p',unknown),
[] ).
cnf(185,axiom,
equal(s(index_171),index_174),
file('SWV569-1.040.p',unknown),
[] ).
cnf(186,axiom,
equal(select(q31,tail),index_177),
file('SWV569-1.040.p',unknown),
[] ).
cnf(187,axiom,
equal(s(index_15),index_18),
file('SWV569-1.040.p',unknown),
[] ).
cnf(188,axiom,
equal(s(index_177),index_180),
file('SWV569-1.040.p',unknown),
[] ).
cnf(189,axiom,
equal(select(q32,tail),index_183),
file('SWV569-1.040.p',unknown),
[] ).
cnf(190,axiom,
equal(s(index_183),index_186),
file('SWV569-1.040.p',unknown),
[] ).
cnf(191,axiom,
equal(select(queue_187,head),index_188),
file('SWV569-1.040.p',unknown),
[] ).
cnf(192,axiom,
equal(s(index_188),index_189),
file('SWV569-1.040.p',unknown),
[] ).
cnf(193,axiom,
equal(select(q33,tail),index_192),
file('SWV569-1.040.p',unknown),
[] ).
cnf(194,axiom,
equal(s(index_192),index_195),
file('SWV569-1.040.p',unknown),
[] ).
cnf(195,axiom,
equal(select(q34,tail),index_198),
file('SWV569-1.040.p',unknown),
[] ).
cnf(196,axiom,
equal(s(index_198),index_201),
file('SWV569-1.040.p',unknown),
[] ).
cnf(197,axiom,
equal(select(q35,tail),index_204),
file('SWV569-1.040.p',unknown),
[] ).
cnf(198,axiom,
equal(s(index_204),index_207),
file('SWV569-1.040.p',unknown),
[] ).
cnf(199,axiom,
equal(select(queue_208,head),index_209),
file('SWV569-1.040.p',unknown),
[] ).
cnf(200,axiom,
equal(select(q11,tail),index_21),
file('SWV569-1.040.p',unknown),
[] ).
cnf(201,axiom,
equal(s(index_209),index_210),
file('SWV569-1.040.p',unknown),
[] ).
cnf(202,axiom,
equal(select(q36,tail),index_213),
file('SWV569-1.040.p',unknown),
[] ).
cnf(203,axiom,
equal(s(index_213),index_216),
file('SWV569-1.040.p',unknown),
[] ).
cnf(204,axiom,
equal(select(q37,tail),index_219),
file('SWV569-1.040.p',unknown),
[] ).
cnf(205,axiom,
equal(s(index_219),index_222),
file('SWV569-1.040.p',unknown),
[] ).
cnf(206,axiom,
equal(select(q38,tail),index_225),
file('SWV569-1.040.p',unknown),
[] ).
cnf(207,axiom,
equal(s(index_225),index_228),
file('SWV569-1.040.p',unknown),
[] ).
cnf(208,axiom,
equal(select(queue_229,head),index_230),
file('SWV569-1.040.p',unknown),
[] ).
cnf(209,axiom,
equal(s(index_230),index_231),
file('SWV569-1.040.p',unknown),
[] ).
cnf(210,axiom,
equal(select(q3,tail),index_234),
file('SWV569-1.040.p',unknown),
[] ).
cnf(211,axiom,
equal(s(index_234),index_237),
file('SWV569-1.040.p',unknown),
[] ).
cnf(212,axiom,
equal(s(index_21),index_24),
file('SWV569-1.040.p',unknown),
[] ).
cnf(213,axiom,
equal(select(q39,tail),index_240),
file('SWV569-1.040.p',unknown),
[] ).
cnf(215,axiom,
equal(select(q4,tail),index_246),
file('SWV569-1.040.p',unknown),
[] ).
cnf(216,axiom,
equal(s(index_246),index_249),
file('SWV569-1.040.p',unknown),
[] ).
cnf(217,axiom,
equal(select(q5,tail),index_252),
file('SWV569-1.040.p',unknown),
[] ).
cnf(218,axiom,
equal(s(index_252),index_255),
file('SWV569-1.040.p',unknown),
[] ).
cnf(219,axiom,
equal(select(queue_256,head),index_257),
file('SWV569-1.040.p',unknown),
[] ).
cnf(220,axiom,
equal(s(index_257),index_258),
file('SWV569-1.040.p',unknown),
[] ).
cnf(221,axiom,
equal(select(queue_25,head),index_26),
file('SWV569-1.040.p',unknown),
[] ).
cnf(222,axiom,
equal(select(q6,tail),index_261),
file('SWV569-1.040.p',unknown),
[] ).
cnf(223,axiom,
equal(s(index_261),index_264),
file('SWV569-1.040.p',unknown),
[] ).
cnf(224,axiom,
equal(select(q7,tail),index_267),
file('SWV569-1.040.p',unknown),
[] ).
cnf(225,axiom,
equal(s(index_26),index_27),
file('SWV569-1.040.p',unknown),
[] ).
cnf(226,axiom,
equal(s(index_267),index_270),
file('SWV569-1.040.p',unknown),
[] ).
cnf(227,axiom,
equal(select(q8,tail),index_273),
file('SWV569-1.040.p',unknown),
[] ).
cnf(228,axiom,
equal(s(index_273),index_276),
file('SWV569-1.040.p',unknown),
[] ).
cnf(229,axiom,
equal(select(queue_277,head),index_278),
file('SWV569-1.040.p',unknown),
[] ).
cnf(230,axiom,
equal(s(index_278),index_279),
file('SWV569-1.040.p',unknown),
[] ).
cnf(231,axiom,
equal(select(q40,head),index_282),
file('SWV569-1.040.p',unknown),
[] ).
cnf(232,axiom,
equal(select(q0,tail),index_3),
file('SWV569-1.040.p',unknown),
[] ).
cnf(233,axiom,
equal(select(q12,tail),index_30),
file('SWV569-1.040.p',unknown),
[] ).
cnf(234,axiom,
equal(s(index_30),index_33),
file('SWV569-1.040.p',unknown),
[] ).
cnf(235,axiom,
equal(select(q13,tail),index_36),
file('SWV569-1.040.p',unknown),
[] ).
cnf(236,axiom,
equal(s(index_36),index_39),
file('SWV569-1.040.p',unknown),
[] ).
cnf(237,axiom,
equal(select(q14,tail),index_42),
file('SWV569-1.040.p',unknown),
[] ).
cnf(238,axiom,
equal(s(index_42),index_45),
file('SWV569-1.040.p',unknown),
[] ).
cnf(239,axiom,
equal(select(queue_46,head),index_47),
file('SWV569-1.040.p',unknown),
[] ).
cnf(240,axiom,
equal(s(index_47),index_48),
file('SWV569-1.040.p',unknown),
[] ).
cnf(241,axiom,
equal(select(q15,tail),index_51),
file('SWV569-1.040.p',unknown),
[] ).
cnf(242,axiom,
equal(s(index_51),index_54),
file('SWV569-1.040.p',unknown),
[] ).
cnf(243,axiom,
equal(select(q16,tail),index_57),
file('SWV569-1.040.p',unknown),
[] ).
cnf(244,axiom,
equal(s(index_3),index_6),
file('SWV569-1.040.p',unknown),
[] ).
cnf(245,axiom,
equal(s(index_57),index_60),
file('SWV569-1.040.p',unknown),
[] ).
cnf(246,axiom,
equal(select(q17,tail),index_63),
file('SWV569-1.040.p',unknown),
[] ).
cnf(247,axiom,
equal(s(index_63),index_66),
file('SWV569-1.040.p',unknown),
[] ).
cnf(248,axiom,
equal(select(queue_67,head),index_68),
file('SWV569-1.040.p',unknown),
[] ).
cnf(249,axiom,
equal(s(index_68),index_69),
file('SWV569-1.040.p',unknown),
[] ).
cnf(250,axiom,
equal(select(q18,tail),index_72),
file('SWV569-1.040.p',unknown),
[] ).
cnf(251,axiom,
equal(s(index_72),index_75),
file('SWV569-1.040.p',unknown),
[] ).
cnf(252,axiom,
equal(select(q1,tail),index_78),
file('SWV569-1.040.p',unknown),
[] ).
cnf(253,axiom,
equal(s(index_78),index_81),
file('SWV569-1.040.p',unknown),
[] ).
cnf(254,axiom,
equal(select(q19,tail),index_84),
file('SWV569-1.040.p',unknown),
[] ).
cnf(255,axiom,
equal(s(index_84),index_87),
file('SWV569-1.040.p',unknown),
[] ).
cnf(256,axiom,
equal(select(q9,tail),index_9),
file('SWV569-1.040.p',unknown),
[] ).
cnf(257,axiom,
equal(select(q20,tail),index_90),
file('SWV569-1.040.p',unknown),
[] ).
cnf(258,axiom,
equal(s(index_90),index_93),
file('SWV569-1.040.p',unknown),
[] ).
cnf(259,axiom,
equal(select(queue_94,head),index_95),
file('SWV569-1.040.p',unknown),
[] ).
cnf(260,axiom,
equal(s(index_95),index_96),
file('SWV569-1.040.p',unknown),
[] ).
cnf(261,axiom,
equal(select(q21,tail),index_99),
file('SWV569-1.040.p',unknown),
[] ).
cnf(262,axiom,
equal(store(q,head,index_0),queue_1),
file('SWV569-1.040.p',unknown),
[] ).
cnf(263,axiom,
equal(store(q21,seq,earray_100),queue_101),
file('SWV569-1.040.p',unknown),
[] ).
cnf(264,axiom,
equal(store(queue_101,tail,index_102),queue_103),
file('SWV569-1.040.p',unknown),
[] ).
cnf(265,axiom,
equal(store(q22,seq,earray_106),queue_107),
file('SWV569-1.040.p',unknown),
[] ).
cnf(266,axiom,
equal(store(queue_107,tail,index_108),queue_109),
file('SWV569-1.040.p',unknown),
[] ).
cnf(267,axiom,
equal(store(q9,seq,earray_10),queue_11),
file('SWV569-1.040.p',unknown),
[] ).
cnf(268,axiom,
equal(store(q23,seq,earray_112),queue_113),
file('SWV569-1.040.p',unknown),
[] ).
cnf(269,axiom,
equal(store(queue_113,tail,index_114),queue_115),
file('SWV569-1.040.p',unknown),
[] ).
cnf(270,axiom,
equal(store(queue_115,head,index_117),queue_118),
file('SWV569-1.040.p',unknown),
[] ).
cnf(271,axiom,
equal(store(q24,seq,earray_121),queue_122),
file('SWV569-1.040.p',unknown),
[] ).
cnf(272,axiom,
equal(store(queue_122,tail,index_123),queue_124),
file('SWV569-1.040.p',unknown),
[] ).
cnf(273,axiom,
equal(store(q25,seq,earray_127),queue_128),
file('SWV569-1.040.p',unknown),
[] ).
cnf(274,axiom,
equal(store(queue_11,tail,index_12),queue_13),
file('SWV569-1.040.p',unknown),
[] ).
cnf(275,axiom,
equal(store(queue_128,tail,index_129),queue_130),
file('SWV569-1.040.p',unknown),
[] ).
cnf(276,axiom,
equal(store(q26,seq,earray_133),queue_134),
file('SWV569-1.040.p',unknown),
[] ).
cnf(277,axiom,
equal(store(queue_134,tail,index_135),queue_136),
file('SWV569-1.040.p',unknown),
[] ).
cnf(278,axiom,
equal(store(queue_136,head,index_138),queue_139),
file('SWV569-1.040.p',unknown),
[] ).
cnf(279,axiom,
equal(store(q27,seq,earray_142),queue_143),
file('SWV569-1.040.p',unknown),
[] ).
cnf(280,axiom,
equal(store(queue_143,tail,index_144),queue_145),
file('SWV569-1.040.p',unknown),
[] ).
cnf(281,axiom,
equal(store(q28,seq,earray_148),queue_149),
file('SWV569-1.040.p',unknown),
[] ).
cnf(282,axiom,
equal(store(queue_149,tail,index_150),queue_151),
file('SWV569-1.040.p',unknown),
[] ).
cnf(283,axiom,
equal(store(q2,seq,earray_154),queue_155),
file('SWV569-1.040.p',unknown),
[] ).
cnf(284,axiom,
equal(store(queue_155,tail,index_156),queue_157),
file('SWV569-1.040.p',unknown),
[] ).
cnf(285,axiom,
equal(store(queue_157,head,index_159),queue_160),
file('SWV569-1.040.p',unknown),
[] ).
cnf(286,axiom,
equal(store(q29,seq,earray_163),queue_164),
file('SWV569-1.040.p',unknown),
[] ).
cnf(287,axiom,
equal(store(queue_164,tail,index_165),queue_166),
file('SWV569-1.040.p',unknown),
[] ).
cnf(288,axiom,
equal(store(queue_166,head,index_168),queue_169),
file('SWV569-1.040.p',unknown),
[] ).
cnf(289,axiom,
equal(store(q10,seq,earray_16),queue_17),
file('SWV569-1.040.p',unknown),
[] ).
cnf(290,axiom,
equal(store(q30,seq,earray_172),queue_173),
file('SWV569-1.040.p',unknown),
[] ).
cnf(291,axiom,
equal(store(queue_173,tail,index_174),queue_175),
file('SWV569-1.040.p',unknown),
[] ).
cnf(292,axiom,
equal(store(q31,seq,earray_178),queue_179),
file('SWV569-1.040.p',unknown),
[] ).
cnf(293,axiom,
equal(store(queue_179,tail,index_180),queue_181),
file('SWV569-1.040.p',unknown),
[] ).
cnf(294,axiom,
equal(store(q32,seq,earray_184),queue_185),
file('SWV569-1.040.p',unknown),
[] ).
cnf(295,axiom,
equal(store(queue_185,tail,index_186),queue_187),
file('SWV569-1.040.p',unknown),
[] ).
cnf(296,axiom,
equal(store(queue_17,tail,index_18),queue_19),
file('SWV569-1.040.p',unknown),
[] ).
cnf(297,axiom,
equal(store(queue_187,head,index_189),queue_190),
file('SWV569-1.040.p',unknown),
[] ).
cnf(298,axiom,
equal(store(q33,seq,earray_193),queue_194),
file('SWV569-1.040.p',unknown),
[] ).
cnf(299,axiom,
equal(store(queue_194,tail,index_195),queue_196),
file('SWV569-1.040.p',unknown),
[] ).
cnf(300,axiom,
equal(store(q34,seq,earray_199),queue_200),
file('SWV569-1.040.p',unknown),
[] ).
cnf(301,axiom,
equal(store(queue_200,tail,index_201),queue_202),
file('SWV569-1.040.p',unknown),
[] ).
cnf(302,axiom,
equal(store(q35,seq,earray_205),queue_206),
file('SWV569-1.040.p',unknown),
[] ).
cnf(303,axiom,
equal(store(queue_206,tail,index_207),queue_208),
file('SWV569-1.040.p',unknown),
[] ).
cnf(304,axiom,
equal(store(queue_208,head,index_210),queue_211),
file('SWV569-1.040.p',unknown),
[] ).
cnf(305,axiom,
equal(store(q36,seq,earray_214),queue_215),
file('SWV569-1.040.p',unknown),
[] ).
cnf(306,axiom,
equal(store(queue_215,tail,index_216),queue_217),
file('SWV569-1.040.p',unknown),
[] ).
cnf(307,axiom,
equal(store(q37,seq,earray_220),queue_221),
file('SWV569-1.040.p',unknown),
[] ).
cnf(308,axiom,
equal(store(queue_221,tail,index_222),queue_223),
file('SWV569-1.040.p',unknown),
[] ).
cnf(309,axiom,
equal(store(q38,seq,earray_226),queue_227),
file('SWV569-1.040.p',unknown),
[] ).
cnf(310,axiom,
equal(store(queue_227,tail,index_228),queue_229),
file('SWV569-1.040.p',unknown),
[] ).
cnf(311,axiom,
equal(store(q11,seq,earray_22),queue_23),
file('SWV569-1.040.p',unknown),
[] ).
cnf(312,axiom,
equal(store(queue_229,head,index_231),queue_232),
file('SWV569-1.040.p',unknown),
[] ).
cnf(313,axiom,
equal(store(q3,seq,earray_235),queue_236),
file('SWV569-1.040.p',unknown),
[] ).
cnf(314,axiom,
equal(store(queue_236,tail,index_237),queue_238),
file('SWV569-1.040.p',unknown),
[] ).
cnf(315,axiom,
equal(store(q39,seq,earray_241),queue_242),
file('SWV569-1.040.p',unknown),
[] ).
cnf(316,axiom,
equal(store(queue_242,tail,index_243),queue_244),
file('SWV569-1.040.p',unknown),
[] ).
cnf(317,axiom,
equal(store(q4,seq,earray_247),queue_248),
file('SWV569-1.040.p',unknown),
[] ).
cnf(318,axiom,
equal(store(queue_23,tail,index_24),queue_25),
file('SWV569-1.040.p',unknown),
[] ).
cnf(319,axiom,
equal(store(queue_248,tail,index_249),queue_250),
file('SWV569-1.040.p',unknown),
[] ).
cnf(320,axiom,
equal(store(q5,seq,earray_253),queue_254),
file('SWV569-1.040.p',unknown),
[] ).
cnf(321,axiom,
equal(store(queue_254,tail,index_255),queue_256),
file('SWV569-1.040.p',unknown),
[] ).
cnf(322,axiom,
equal(store(queue_256,head,index_258),queue_259),
file('SWV569-1.040.p',unknown),
[] ).
cnf(323,axiom,
equal(store(q6,seq,earray_262),queue_263),
file('SWV569-1.040.p',unknown),
[] ).
cnf(324,axiom,
equal(store(queue_263,tail,index_264),queue_265),
file('SWV569-1.040.p',unknown),
[] ).
cnf(325,axiom,
equal(store(q7,seq,earray_268),queue_269),
file('SWV569-1.040.p',unknown),
[] ).
cnf(326,axiom,
equal(store(queue_269,tail,index_270),queue_271),
file('SWV569-1.040.p',unknown),
[] ).
cnf(327,axiom,
equal(store(q8,seq,earray_274),queue_275),
file('SWV569-1.040.p',unknown),
[] ).
cnf(328,axiom,
equal(store(queue_275,tail,index_276),queue_277),
file('SWV569-1.040.p',unknown),
[] ).
cnf(329,axiom,
equal(store(queue_25,head,index_27),queue_28),
file('SWV569-1.040.p',unknown),
[] ).
cnf(330,axiom,
equal(store(queue_277,head,index_279),queue_280),
file('SWV569-1.040.p',unknown),
[] ).
cnf(331,axiom,
equal(store(q12,seq,earray_31),queue_32),
file('SWV569-1.040.p',unknown),
[] ).
cnf(332,axiom,
equal(store(queue_32,tail,index_33),queue_34),
file('SWV569-1.040.p',unknown),
[] ).
cnf(333,axiom,
equal(store(q13,seq,earray_37),queue_38),
file('SWV569-1.040.p',unknown),
[] ).
cnf(334,axiom,
equal(store(queue_38,tail,index_39),queue_40),
file('SWV569-1.040.p',unknown),
[] ).
cnf(335,axiom,
equal(store(q14,seq,earray_43),queue_44),
file('SWV569-1.040.p',unknown),
[] ).
cnf(336,axiom,
equal(store(queue_44,tail,index_45),queue_46),
file('SWV569-1.040.p',unknown),
[] ).
cnf(337,axiom,
equal(store(queue_46,head,index_48),queue_49),
file('SWV569-1.040.p',unknown),
[] ).
cnf(338,axiom,
equal(store(q0,seq,earray_4),queue_5),
file('SWV569-1.040.p',unknown),
[] ).
cnf(339,axiom,
equal(store(q15,seq,earray_52),queue_53),
file('SWV569-1.040.p',unknown),
[] ).
cnf(340,axiom,
equal(store(queue_53,tail,index_54),queue_55),
file('SWV569-1.040.p',unknown),
[] ).
cnf(341,axiom,
equal(store(q16,seq,earray_58),queue_59),
file('SWV569-1.040.p',unknown),
[] ).
cnf(342,axiom,
equal(store(queue_59,tail,index_60),queue_61),
file('SWV569-1.040.p',unknown),
[] ).
cnf(343,axiom,
equal(store(q17,seq,earray_64),queue_65),
file('SWV569-1.040.p',unknown),
[] ).
cnf(344,axiom,
equal(store(queue_65,tail,index_66),queue_67),
file('SWV569-1.040.p',unknown),
[] ).
cnf(345,axiom,
equal(store(queue_5,tail,index_6),queue_7),
file('SWV569-1.040.p',unknown),
[] ).
cnf(346,axiom,
equal(store(queue_67,head,index_69),queue_70),
file('SWV569-1.040.p',unknown),
[] ).
cnf(347,axiom,
equal(store(q18,seq,earray_73),queue_74),
file('SWV569-1.040.p',unknown),
[] ).
cnf(348,axiom,
equal(store(queue_74,tail,index_75),queue_76),
file('SWV569-1.040.p',unknown),
[] ).
cnf(349,axiom,
equal(store(q1,seq,earray_79),queue_80),
file('SWV569-1.040.p',unknown),
[] ).
cnf(350,axiom,
equal(store(queue_80,tail,index_81),queue_82),
file('SWV569-1.040.p',unknown),
[] ).
cnf(351,axiom,
equal(store(q19,seq,earray_85),queue_86),
file('SWV569-1.040.p',unknown),
[] ).
cnf(352,axiom,
equal(store(queue_86,tail,index_87),queue_88),
file('SWV569-1.040.p',unknown),
[] ).
cnf(353,axiom,
equal(store(q20,seq,earray_91),queue_92),
file('SWV569-1.040.p',unknown),
[] ).
cnf(354,axiom,
equal(store(queue_92,tail,index_93),queue_94),
file('SWV569-1.040.p',unknown),
[] ).
cnf(355,axiom,
equal(store(queue_94,head,index_96),queue_97),
file('SWV569-1.040.p',unknown),
[] ).
cnf(356,axiom,
equal(queue_1,q0),
file('SWV569-1.040.p',unknown),
[] ).
cnf(357,axiom,
equal(queue_7,q1),
file('SWV569-1.040.p',unknown),
[] ).
cnf(358,axiom,
equal(queue_13,q10),
file('SWV569-1.040.p',unknown),
[] ).
cnf(359,axiom,
equal(queue_19,q11),
file('SWV569-1.040.p',unknown),
[] ).
cnf(360,axiom,
equal(queue_28,q12),
file('SWV569-1.040.p',unknown),
[] ).
cnf(361,axiom,
equal(queue_34,q13),
file('SWV569-1.040.p',unknown),
[] ).
cnf(362,axiom,
equal(queue_40,q14),
file('SWV569-1.040.p',unknown),
[] ).
cnf(363,axiom,
equal(queue_49,q15),
file('SWV569-1.040.p',unknown),
[] ).
cnf(364,axiom,
equal(queue_55,q16),
file('SWV569-1.040.p',unknown),
[] ).
cnf(365,axiom,
equal(queue_61,q17),
file('SWV569-1.040.p',unknown),
[] ).
cnf(366,axiom,
equal(queue_70,q18),
file('SWV569-1.040.p',unknown),
[] ).
cnf(367,axiom,
equal(queue_76,q19),
file('SWV569-1.040.p',unknown),
[] ).
cnf(368,axiom,
equal(queue_82,q2),
file('SWV569-1.040.p',unknown),
[] ).
cnf(369,axiom,
equal(queue_88,q20),
file('SWV569-1.040.p',unknown),
[] ).
cnf(370,axiom,
equal(queue_97,q21),
file('SWV569-1.040.p',unknown),
[] ).
cnf(371,axiom,
equal(queue_103,q22),
file('SWV569-1.040.p',unknown),
[] ).
cnf(372,axiom,
equal(queue_109,q23),
file('SWV569-1.040.p',unknown),
[] ).
cnf(373,axiom,
equal(queue_118,q24),
file('SWV569-1.040.p',unknown),
[] ).
cnf(374,axiom,
equal(queue_124,q25),
file('SWV569-1.040.p',unknown),
[] ).
cnf(375,axiom,
equal(queue_130,q26),
file('SWV569-1.040.p',unknown),
[] ).
cnf(376,axiom,
equal(queue_139,q27),
file('SWV569-1.040.p',unknown),
[] ).
cnf(377,axiom,
equal(queue_145,q28),
file('SWV569-1.040.p',unknown),
[] ).
cnf(378,axiom,
equal(queue_151,q29),
file('SWV569-1.040.p',unknown),
[] ).
cnf(379,axiom,
equal(queue_160,q3),
file('SWV569-1.040.p',unknown),
[] ).
cnf(380,axiom,
equal(queue_169,q30),
file('SWV569-1.040.p',unknown),
[] ).
cnf(381,axiom,
equal(queue_175,q31),
file('SWV569-1.040.p',unknown),
[] ).
cnf(382,axiom,
equal(queue_181,q32),
file('SWV569-1.040.p',unknown),
[] ).
cnf(383,axiom,
equal(queue_190,q33),
file('SWV569-1.040.p',unknown),
[] ).
cnf(384,axiom,
equal(queue_196,q34),
file('SWV569-1.040.p',unknown),
[] ).
cnf(385,axiom,
equal(queue_202,q35),
file('SWV569-1.040.p',unknown),
[] ).
cnf(386,axiom,
equal(queue_211,q36),
file('SWV569-1.040.p',unknown),
[] ).
cnf(387,axiom,
equal(queue_217,q37),
file('SWV569-1.040.p',unknown),
[] ).
cnf(388,axiom,
equal(queue_223,q38),
file('SWV569-1.040.p',unknown),
[] ).
cnf(389,axiom,
equal(queue_232,q39),
file('SWV569-1.040.p',unknown),
[] ).
cnf(390,axiom,
equal(queue_238,q4),
file('SWV569-1.040.p',unknown),
[] ).
cnf(391,axiom,
equal(queue_244,q40),
file('SWV569-1.040.p',unknown),
[] ).
cnf(392,axiom,
equal(queue_250,q5),
file('SWV569-1.040.p',unknown),
[] ).
cnf(393,axiom,
equal(queue_259,q6),
file('SWV569-1.040.p',unknown),
[] ).
cnf(394,axiom,
equal(queue_265,q7),
file('SWV569-1.040.p',unknown),
[] ).
cnf(395,axiom,
equal(queue_271,q8),
file('SWV569-1.040.p',unknown),
[] ).
cnf(396,axiom,
equal(queue_280,q9),
file('SWV569-1.040.p',unknown),
[] ).
cnf(397,axiom,
~ equal(elem_283,e13),
file('SWV569-1.040.p',unknown),
[] ).
cnf(398,plain,
equal(store(queue_94,head,index_96),q21),
inference(rew,[status(thm),theory(equality)],[370,355]),
[iquote('0:Rew:370.0,355.0')] ).
cnf(399,plain,
equal(store(queue_86,tail,index_87),q20),
inference(rew,[status(thm),theory(equality)],[369,352]),
[iquote('0:Rew:369.0,352.0')] ).
cnf(400,plain,
equal(store(queue_80,tail,index_81),q2),
inference(rew,[status(thm),theory(equality)],[368,350]),
[iquote('0:Rew:368.0,350.0')] ).
cnf(401,plain,
equal(store(queue_74,tail,index_75),q19),
inference(rew,[status(thm),theory(equality)],[367,348]),
[iquote('0:Rew:367.0,348.0')] ).
cnf(402,plain,
equal(store(queue_67,head,index_69),q18),
inference(rew,[status(thm),theory(equality)],[366,346]),
[iquote('0:Rew:366.0,346.0')] ).
cnf(403,plain,
equal(store(queue_5,tail,index_6),q1),
inference(rew,[status(thm),theory(equality)],[357,345]),
[iquote('0:Rew:357.0,345.0')] ).
cnf(404,plain,
equal(store(queue_59,tail,index_60),q17),
inference(rew,[status(thm),theory(equality)],[365,342]),
[iquote('0:Rew:365.0,342.0')] ).
cnf(405,plain,
equal(store(queue_53,tail,index_54),q16),
inference(rew,[status(thm),theory(equality)],[364,340]),
[iquote('0:Rew:364.0,340.0')] ).
cnf(406,plain,
equal(store(queue_46,head,index_48),q15),
inference(rew,[status(thm),theory(equality)],[363,337]),
[iquote('0:Rew:363.0,337.0')] ).
cnf(407,plain,
equal(store(queue_38,tail,index_39),q14),
inference(rew,[status(thm),theory(equality)],[362,334]),
[iquote('0:Rew:362.0,334.0')] ).
cnf(408,plain,
equal(store(queue_32,tail,index_33),q13),
inference(rew,[status(thm),theory(equality)],[361,332]),
[iquote('0:Rew:361.0,332.0')] ).
cnf(409,plain,
equal(store(queue_277,head,index_279),q9),
inference(rew,[status(thm),theory(equality)],[396,330]),
[iquote('0:Rew:396.0,330.0')] ).
cnf(410,plain,
equal(store(queue_25,head,index_27),q12),
inference(rew,[status(thm),theory(equality)],[360,329]),
[iquote('0:Rew:360.0,329.0')] ).
cnf(411,plain,
equal(store(queue_269,tail,index_270),q8),
inference(rew,[status(thm),theory(equality)],[395,326]),
[iquote('0:Rew:395.0,326.0')] ).
cnf(412,plain,
equal(store(queue_263,tail,index_264),q7),
inference(rew,[status(thm),theory(equality)],[394,324]),
[iquote('0:Rew:394.0,324.0')] ).
cnf(413,plain,
equal(store(queue_256,head,index_258),q6),
inference(rew,[status(thm),theory(equality)],[393,322]),
[iquote('0:Rew:393.0,322.0')] ).
cnf(414,plain,
equal(store(queue_248,tail,index_249),q5),
inference(rew,[status(thm),theory(equality)],[392,319]),
[iquote('0:Rew:392.0,319.0')] ).
cnf(415,plain,
equal(store(queue_242,tail,index_243),q40),
inference(rew,[status(thm),theory(equality)],[391,316]),
[iquote('0:Rew:391.0,316.0')] ).
cnf(416,plain,
equal(store(queue_236,tail,index_237),q4),
inference(rew,[status(thm),theory(equality)],[390,314]),
[iquote('0:Rew:390.0,314.0')] ).
cnf(417,plain,
equal(store(queue_229,head,index_231),q39),
inference(rew,[status(thm),theory(equality)],[389,312]),
[iquote('0:Rew:389.0,312.0')] ).
cnf(418,plain,
equal(store(queue_221,tail,index_222),q38),
inference(rew,[status(thm),theory(equality)],[388,308]),
[iquote('0:Rew:388.0,308.0')] ).
cnf(419,plain,
equal(store(queue_215,tail,index_216),q37),
inference(rew,[status(thm),theory(equality)],[387,306]),
[iquote('0:Rew:387.0,306.0')] ).
cnf(420,plain,
equal(store(queue_208,head,index_210),q36),
inference(rew,[status(thm),theory(equality)],[386,304]),
[iquote('0:Rew:386.0,304.0')] ).
cnf(421,plain,
equal(store(queue_200,tail,index_201),q35),
inference(rew,[status(thm),theory(equality)],[385,301]),
[iquote('0:Rew:385.0,301.0')] ).
cnf(422,plain,
equal(store(queue_194,tail,index_195),q34),
inference(rew,[status(thm),theory(equality)],[384,299]),
[iquote('0:Rew:384.0,299.0')] ).
cnf(423,plain,
equal(store(queue_187,head,index_189),q33),
inference(rew,[status(thm),theory(equality)],[383,297]),
[iquote('0:Rew:383.0,297.0')] ).
cnf(424,plain,
equal(store(queue_17,tail,index_18),q11),
inference(rew,[status(thm),theory(equality)],[359,296]),
[iquote('0:Rew:359.0,296.0')] ).
cnf(425,plain,
equal(store(queue_179,tail,index_180),q32),
inference(rew,[status(thm),theory(equality)],[382,293]),
[iquote('0:Rew:382.0,293.0')] ).
cnf(426,plain,
equal(store(queue_173,tail,index_174),q31),
inference(rew,[status(thm),theory(equality)],[381,291]),
[iquote('0:Rew:381.0,291.0')] ).
cnf(427,plain,
equal(store(queue_166,head,index_168),q30),
inference(rew,[status(thm),theory(equality)],[380,288]),
[iquote('0:Rew:380.0,288.0')] ).
cnf(428,plain,
equal(store(queue_157,head,index_159),q3),
inference(rew,[status(thm),theory(equality)],[379,285]),
[iquote('0:Rew:379.0,285.0')] ).
cnf(429,plain,
equal(store(queue_149,tail,index_150),q29),
inference(rew,[status(thm),theory(equality)],[378,282]),
[iquote('0:Rew:378.0,282.0')] ).
cnf(430,plain,
equal(store(queue_143,tail,index_144),q28),
inference(rew,[status(thm),theory(equality)],[377,280]),
[iquote('0:Rew:377.0,280.0')] ).
cnf(431,plain,
equal(store(queue_136,head,index_138),q27),
inference(rew,[status(thm),theory(equality)],[376,278]),
[iquote('0:Rew:376.0,278.0')] ).
cnf(432,plain,
equal(store(queue_128,tail,index_129),q26),
inference(rew,[status(thm),theory(equality)],[375,275]),
[iquote('0:Rew:375.0,275.0')] ).
cnf(433,plain,
equal(store(queue_11,tail,index_12),q10),
inference(rew,[status(thm),theory(equality)],[358,274]),
[iquote('0:Rew:358.0,274.0')] ).
cnf(434,plain,
equal(store(queue_122,tail,index_123),q25),
inference(rew,[status(thm),theory(equality)],[374,272]),
[iquote('0:Rew:374.0,272.0')] ).
cnf(435,plain,
equal(store(queue_115,head,index_117),q24),
inference(rew,[status(thm),theory(equality)],[373,270]),
[iquote('0:Rew:373.0,270.0')] ).
cnf(436,plain,
equal(store(queue_107,tail,index_108),q23),
inference(rew,[status(thm),theory(equality)],[372,266]),
[iquote('0:Rew:372.0,266.0')] ).
cnf(437,plain,
equal(store(queue_101,tail,index_102),q22),
inference(rew,[status(thm),theory(equality)],[371,264]),
[iquote('0:Rew:371.0,264.0')] ).
cnf(438,plain,
equal(store(q,head,index_0),q0),
inference(rew,[status(thm),theory(equality)],[356,262]),
[iquote('0:Rew:356.0,262.0')] ).
cnf(644,plain,
~ equal(index_39,index_36),
inference(spl,[status(thm),theory(equality)],[236,71]),
[iquote('0:SpL:236.0,71.0')] ).
cnf(831,plain,
~ equal(s(index_39),index_36),
inference(spl,[status(thm),theory(equality)],[236,70]),
[iquote('0:SpL:236.0,70.0')] ).
cnf(884,plain,
~ equal(s(s(index_39)),index_36),
inference(spl,[status(thm),theory(equality)],[236,69]),
[iquote('0:SpL:236.0,69.0')] ).
cnf(937,plain,
~ equal(s(s(s(index_39))),index_36),
inference(spl,[status(thm),theory(equality)],[236,68]),
[iquote('0:SpL:236.0,68.0')] ).
cnf(979,plain,
equal(select(q21,head),index_96),
inference(spr,[status(thm),theory(equality)],[398,1]),
[iquote('0:SpR:398.0,1.0')] ).
cnf(980,plain,
equal(select(q18,head),index_69),
inference(spr,[status(thm),theory(equality)],[402,1]),
[iquote('0:SpR:402.0,1.0')] ).
cnf(981,plain,
equal(select(q15,head),index_48),
inference(spr,[status(thm),theory(equality)],[406,1]),
[iquote('0:SpR:406.0,1.0')] ).
cnf(982,plain,
equal(select(q9,head),index_279),
inference(spr,[status(thm),theory(equality)],[409,1]),
[iquote('0:SpR:409.0,1.0')] ).
cnf(983,plain,
equal(select(q12,head),index_27),
inference(spr,[status(thm),theory(equality)],[410,1]),
[iquote('0:SpR:410.0,1.0')] ).
cnf(984,plain,
equal(select(q6,head),index_258),
inference(spr,[status(thm),theory(equality)],[413,1]),
[iquote('0:SpR:413.0,1.0')] ).
cnf(985,plain,
equal(select(q39,head),index_231),
inference(spr,[status(thm),theory(equality)],[417,1]),
[iquote('0:SpR:417.0,1.0')] ).
cnf(986,plain,
equal(select(q36,head),index_210),
inference(spr,[status(thm),theory(equality)],[420,1]),
[iquote('0:SpR:420.0,1.0')] ).
cnf(987,plain,
equal(select(q33,head),index_189),
inference(spr,[status(thm),theory(equality)],[423,1]),
[iquote('0:SpR:423.0,1.0')] ).
cnf(988,plain,
equal(select(q30,head),index_168),
inference(spr,[status(thm),theory(equality)],[427,1]),
[iquote('0:SpR:427.0,1.0')] ).
cnf(989,plain,
equal(select(q3,head),index_159),
inference(spr,[status(thm),theory(equality)],[428,1]),
[iquote('0:SpR:428.0,1.0')] ).
cnf(990,plain,
equal(select(q27,head),index_138),
inference(spr,[status(thm),theory(equality)],[431,1]),
[iquote('0:SpR:431.0,1.0')] ).
cnf(991,plain,
equal(select(q24,head),index_117),
inference(spr,[status(thm),theory(equality)],[435,1]),
[iquote('0:SpR:435.0,1.0')] ).
cnf(992,plain,
equal(select(q0,head),index_0),
inference(spr,[status(thm),theory(equality)],[438,1]),
[iquote('0:SpR:438.0,1.0')] ).
cnf(993,plain,
equal(select(queue_94,tail),index_93),
inference(spr,[status(thm),theory(equality)],[354,1]),
[iquote('0:SpR:354.0,1.0')] ).
cnf(994,plain,
equal(select(q20,tail),index_87),
inference(spr,[status(thm),theory(equality)],[399,1]),
[iquote('0:SpR:399.0,1.0')] ).
cnf(995,plain,
equal(select(q2,tail),index_81),
inference(spr,[status(thm),theory(equality)],[400,1]),
[iquote('0:SpR:400.0,1.0')] ).
cnf(996,plain,
equal(select(q19,tail),index_75),
inference(spr,[status(thm),theory(equality)],[401,1]),
[iquote('0:SpR:401.0,1.0')] ).
cnf(997,plain,
equal(select(q1,tail),index_6),
inference(spr,[status(thm),theory(equality)],[403,1]),
[iquote('0:SpR:403.0,1.0')] ).
cnf(998,plain,
equal(select(queue_67,tail),index_66),
inference(spr,[status(thm),theory(equality)],[344,1]),
[iquote('0:SpR:344.0,1.0')] ).
cnf(999,plain,
equal(select(q17,tail),index_60),
inference(spr,[status(thm),theory(equality)],[404,1]),
[iquote('0:SpR:404.0,1.0')] ).
cnf(1000,plain,
equal(select(q16,tail),index_54),
inference(spr,[status(thm),theory(equality)],[405,1]),
[iquote('0:SpR:405.0,1.0')] ).
cnf(1001,plain,
equal(select(queue_46,tail),index_45),
inference(spr,[status(thm),theory(equality)],[336,1]),
[iquote('0:SpR:336.0,1.0')] ).
cnf(1002,plain,
equal(select(q14,tail),index_39),
inference(spr,[status(thm),theory(equality)],[407,1]),
[iquote('0:SpR:407.0,1.0')] ).
cnf(1003,plain,
equal(select(q13,tail),index_33),
inference(spr,[status(thm),theory(equality)],[408,1]),
[iquote('0:SpR:408.0,1.0')] ).
cnf(1004,plain,
equal(select(queue_277,tail),index_276),
inference(spr,[status(thm),theory(equality)],[328,1]),
[iquote('0:SpR:328.0,1.0')] ).
cnf(1005,plain,
equal(select(q8,tail),index_270),
inference(spr,[status(thm),theory(equality)],[411,1]),
[iquote('0:SpR:411.0,1.0')] ).
cnf(1006,plain,
equal(select(q7,tail),index_264),
inference(spr,[status(thm),theory(equality)],[412,1]),
[iquote('0:SpR:412.0,1.0')] ).
cnf(1007,plain,
equal(select(queue_256,tail),index_255),
inference(spr,[status(thm),theory(equality)],[321,1]),
[iquote('0:SpR:321.0,1.0')] ).
cnf(1008,plain,
equal(select(q5,tail),index_249),
inference(spr,[status(thm),theory(equality)],[414,1]),
[iquote('0:SpR:414.0,1.0')] ).
cnf(1009,plain,
equal(select(queue_25,tail),index_24),
inference(spr,[status(thm),theory(equality)],[318,1]),
[iquote('0:SpR:318.0,1.0')] ).
cnf(1011,plain,
equal(select(q4,tail),index_237),
inference(spr,[status(thm),theory(equality)],[416,1]),
[iquote('0:SpR:416.0,1.0')] ).
cnf(1012,plain,
equal(select(queue_229,tail),index_228),
inference(spr,[status(thm),theory(equality)],[310,1]),
[iquote('0:SpR:310.0,1.0')] ).
cnf(1013,plain,
equal(select(q38,tail),index_222),
inference(spr,[status(thm),theory(equality)],[418,1]),
[iquote('0:SpR:418.0,1.0')] ).
cnf(1014,plain,
equal(select(q37,tail),index_216),
inference(spr,[status(thm),theory(equality)],[419,1]),
[iquote('0:SpR:419.0,1.0')] ).
cnf(1015,plain,
equal(select(queue_208,tail),index_207),
inference(spr,[status(thm),theory(equality)],[303,1]),
[iquote('0:SpR:303.0,1.0')] ).
cnf(1016,plain,
equal(select(q35,tail),index_201),
inference(spr,[status(thm),theory(equality)],[421,1]),
[iquote('0:SpR:421.0,1.0')] ).
cnf(1017,plain,
equal(select(q34,tail),index_195),
inference(spr,[status(thm),theory(equality)],[422,1]),
[iquote('0:SpR:422.0,1.0')] ).
cnf(1018,plain,
equal(select(q11,tail),index_18),
inference(spr,[status(thm),theory(equality)],[424,1]),
[iquote('0:SpR:424.0,1.0')] ).
cnf(1019,plain,
equal(select(queue_187,tail),index_186),
inference(spr,[status(thm),theory(equality)],[295,1]),
[iquote('0:SpR:295.0,1.0')] ).
cnf(1020,plain,
equal(select(q32,tail),index_180),
inference(spr,[status(thm),theory(equality)],[425,1]),
[iquote('0:SpR:425.0,1.0')] ).
cnf(1021,plain,
equal(select(q31,tail),index_174),
inference(spr,[status(thm),theory(equality)],[426,1]),
[iquote('0:SpR:426.0,1.0')] ).
cnf(1022,plain,
equal(select(queue_166,tail),index_165),
inference(spr,[status(thm),theory(equality)],[287,1]),
[iquote('0:SpR:287.0,1.0')] ).
cnf(1023,plain,
equal(select(queue_157,tail),index_156),
inference(spr,[status(thm),theory(equality)],[284,1]),
[iquote('0:SpR:284.0,1.0')] ).
cnf(1024,plain,
equal(select(q29,tail),index_150),
inference(spr,[status(thm),theory(equality)],[429,1]),
[iquote('0:SpR:429.0,1.0')] ).
cnf(1025,plain,
equal(select(q28,tail),index_144),
inference(spr,[status(thm),theory(equality)],[430,1]),
[iquote('0:SpR:430.0,1.0')] ).
cnf(1026,plain,
equal(select(queue_136,tail),index_135),
inference(spr,[status(thm),theory(equality)],[277,1]),
[iquote('0:SpR:277.0,1.0')] ).
cnf(1027,plain,
equal(select(q26,tail),index_129),
inference(spr,[status(thm),theory(equality)],[432,1]),
[iquote('0:SpR:432.0,1.0')] ).
cnf(1028,plain,
equal(select(q10,tail),index_12),
inference(spr,[status(thm),theory(equality)],[433,1]),
[iquote('0:SpR:433.0,1.0')] ).
cnf(1029,plain,
equal(select(q25,tail),index_123),
inference(spr,[status(thm),theory(equality)],[434,1]),
[iquote('0:SpR:434.0,1.0')] ).
cnf(1030,plain,
equal(select(queue_115,tail),index_114),
inference(spr,[status(thm),theory(equality)],[269,1]),
[iquote('0:SpR:269.0,1.0')] ).
cnf(1031,plain,
equal(select(q23,tail),index_108),
inference(spr,[status(thm),theory(equality)],[436,1]),
[iquote('0:SpR:436.0,1.0')] ).
cnf(1032,plain,
equal(select(q22,tail),index_102),
inference(spr,[status(thm),theory(equality)],[437,1]),
[iquote('0:SpR:437.0,1.0')] ).
cnf(1033,plain,
equal(select(queue_92,seq),earray_91),
inference(spr,[status(thm),theory(equality)],[353,1]),
[iquote('0:SpR:353.0,1.0')] ).
cnf(1034,plain,
equal(select(queue_86,seq),earray_85),
inference(spr,[status(thm),theory(equality)],[351,1]),
[iquote('0:SpR:351.0,1.0')] ).
cnf(1036,plain,
equal(select(queue_74,seq),earray_73),
inference(spr,[status(thm),theory(equality)],[347,1]),
[iquote('0:SpR:347.0,1.0')] ).
cnf(1037,plain,
equal(select(queue_65,seq),earray_64),
inference(spr,[status(thm),theory(equality)],[343,1]),
[iquote('0:SpR:343.0,1.0')] ).
cnf(1038,plain,
equal(select(queue_59,seq),earray_58),
inference(spr,[status(thm),theory(equality)],[341,1]),
[iquote('0:SpR:341.0,1.0')] ).
cnf(1039,plain,
equal(select(queue_53,seq),earray_52),
inference(spr,[status(thm),theory(equality)],[339,1]),
[iquote('0:SpR:339.0,1.0')] ).
cnf(1041,plain,
equal(select(queue_44,seq),earray_43),
inference(spr,[status(thm),theory(equality)],[335,1]),
[iquote('0:SpR:335.0,1.0')] ).
cnf(1042,plain,
equal(select(queue_38,seq),earray_37),
inference(spr,[status(thm),theory(equality)],[333,1]),
[iquote('0:SpR:333.0,1.0')] ).
cnf(1049,plain,
equal(select(queue_242,seq),earray_241),
inference(spr,[status(thm),theory(equality)],[315,1]),
[iquote('0:SpR:315.0,1.0')] ).
cnf(1052,plain,
equal(select(queue_227,seq),earray_226),
inference(spr,[status(thm),theory(equality)],[309,1]),
[iquote('0:SpR:309.0,1.0')] ).
cnf(1053,plain,
equal(select(queue_221,seq),earray_220),
inference(spr,[status(thm),theory(equality)],[307,1]),
[iquote('0:SpR:307.0,1.0')] ).
cnf(1054,plain,
equal(select(queue_215,seq),earray_214),
inference(spr,[status(thm),theory(equality)],[305,1]),
[iquote('0:SpR:305.0,1.0')] ).
cnf(1055,plain,
equal(select(queue_206,seq),earray_205),
inference(spr,[status(thm),theory(equality)],[302,1]),
[iquote('0:SpR:302.0,1.0')] ).
cnf(1056,plain,
equal(select(queue_200,seq),earray_199),
inference(spr,[status(thm),theory(equality)],[300,1]),
[iquote('0:SpR:300.0,1.0')] ).
cnf(1057,plain,
equal(select(queue_194,seq),earray_193),
inference(spr,[status(thm),theory(equality)],[298,1]),
[iquote('0:SpR:298.0,1.0')] ).
cnf(1058,plain,
equal(select(queue_185,seq),earray_184),
inference(spr,[status(thm),theory(equality)],[294,1]),
[iquote('0:SpR:294.0,1.0')] ).
cnf(1059,plain,
equal(select(queue_179,seq),earray_178),
inference(spr,[status(thm),theory(equality)],[292,1]),
[iquote('0:SpR:292.0,1.0')] ).
cnf(1060,plain,
equal(select(queue_173,seq),earray_172),
inference(spr,[status(thm),theory(equality)],[290,1]),
[iquote('0:SpR:290.0,1.0')] ).
cnf(1062,plain,
equal(select(queue_164,seq),earray_163),
inference(spr,[status(thm),theory(equality)],[286,1]),
[iquote('0:SpR:286.0,1.0')] ).
cnf(1064,plain,
equal(select(queue_149,seq),earray_148),
inference(spr,[status(thm),theory(equality)],[281,1]),
[iquote('0:SpR:281.0,1.0')] ).
cnf(1065,plain,
equal(select(queue_143,seq),earray_142),
inference(spr,[status(thm),theory(equality)],[279,1]),
[iquote('0:SpR:279.0,1.0')] ).
cnf(1066,plain,
equal(select(queue_134,seq),earray_133),
inference(spr,[status(thm),theory(equality)],[276,1]),
[iquote('0:SpR:276.0,1.0')] ).
cnf(1067,plain,
equal(select(queue_128,seq),earray_127),
inference(spr,[status(thm),theory(equality)],[273,1]),
[iquote('0:SpR:273.0,1.0')] ).
cnf(1068,plain,
equal(select(queue_122,seq),earray_121),
inference(spr,[status(thm),theory(equality)],[271,1]),
[iquote('0:SpR:271.0,1.0')] ).
cnf(1069,plain,
equal(select(queue_113,seq),earray_112),
inference(spr,[status(thm),theory(equality)],[268,1]),
[iquote('0:SpR:268.0,1.0')] ).
cnf(1071,plain,
equal(select(queue_107,seq),earray_106),
inference(spr,[status(thm),theory(equality)],[265,1]),
[iquote('0:SpR:265.0,1.0')] ).
cnf(1072,plain,
equal(select(queue_101,seq),earray_100),
inference(spr,[status(thm),theory(equality)],[263,1]),
[iquote('0:SpR:263.0,1.0')] ).
cnf(1082,plain,
equal(select(earray_37,index_36),e13),
inference(spr,[status(thm),theory(equality)],[133,1]),
[iquote('0:SpR:133.0,1.0')] ).
cnf(1113,plain,
equal(index_87,index_90),
inference(rew,[status(thm),theory(equality)],[257,994]),
[iquote('0:Rew:257.0,994.0')] ).
cnf(1114,plain,
equal(s(index_84),index_90),
inference(rew,[status(thm),theory(equality)],[1113,255]),
[iquote('0:Rew:1113.0,255.0')] ).
cnf(1116,plain,
equal(store(queue_86,tail,index_90),q20),
inference(rew,[status(thm),theory(equality)],[1113,399]),
[iquote('0:Rew:1113.0,399.0')] ).
cnf(1120,plain,
equal(index_81,index_153),
inference(rew,[status(thm),theory(equality)],[176,995]),
[iquote('0:Rew:176.0,995.0')] ).
cnf(1121,plain,
equal(s(index_78),index_153),
inference(rew,[status(thm),theory(equality)],[1120,253]),
[iquote('0:Rew:1120.0,253.0')] ).
cnf(1123,plain,
equal(store(queue_80,tail,index_153),q2),
inference(rew,[status(thm),theory(equality)],[1120,400]),
[iquote('0:Rew:1120.0,400.0')] ).
cnf(1127,plain,
equal(index_75,index_84),
inference(rew,[status(thm),theory(equality)],[254,996]),
[iquote('0:Rew:254.0,996.0')] ).
cnf(1128,plain,
equal(s(index_72),index_84),
inference(rew,[status(thm),theory(equality)],[1127,251]),
[iquote('0:Rew:1127.0,251.0')] ).
cnf(1130,plain,
equal(store(queue_74,tail,index_84),q19),
inference(rew,[status(thm),theory(equality)],[1127,401]),
[iquote('0:Rew:1127.0,401.0')] ).
cnf(1134,plain,
equal(index_6,index_78),
inference(rew,[status(thm),theory(equality)],[252,997]),
[iquote('0:Rew:252.0,997.0')] ).
cnf(1135,plain,
equal(s(index_3),index_78),
inference(rew,[status(thm),theory(equality)],[1134,244]),
[iquote('0:Rew:1134.0,244.0')] ).
cnf(1137,plain,
equal(store(queue_5,tail,index_78),q1),
inference(rew,[status(thm),theory(equality)],[1134,403]),
[iquote('0:Rew:1134.0,403.0')] ).
cnf(1141,plain,
equal(index_60,index_63),
inference(rew,[status(thm),theory(equality)],[246,999]),
[iquote('0:Rew:246.0,999.0')] ).
cnf(1142,plain,
equal(s(index_57),index_63),
inference(rew,[status(thm),theory(equality)],[1141,245]),
[iquote('0:Rew:1141.0,245.0')] ).
cnf(1144,plain,
equal(store(queue_59,tail,index_63),q17),
inference(rew,[status(thm),theory(equality)],[1141,404]),
[iquote('0:Rew:1141.0,404.0')] ).
cnf(1148,plain,
equal(index_54,index_57),
inference(rew,[status(thm),theory(equality)],[243,1000]),
[iquote('0:Rew:243.0,1000.0')] ).
cnf(1149,plain,
equal(s(index_51),index_57),
inference(rew,[status(thm),theory(equality)],[1148,242]),
[iquote('0:Rew:1148.0,242.0')] ).
cnf(1151,plain,
equal(store(queue_53,tail,index_57),q16),
inference(rew,[status(thm),theory(equality)],[1148,405]),
[iquote('0:Rew:1148.0,405.0')] ).
cnf(1155,plain,
equal(index_39,index_42),
inference(rew,[status(thm),theory(equality)],[237,1002]),
[iquote('0:Rew:237.0,1002.0')] ).
cnf(1156,plain,
equal(s(index_36),index_42),
inference(rew,[status(thm),theory(equality)],[1155,236]),
[iquote('0:Rew:1155.0,236.0')] ).
cnf(1157,plain,
~ equal(index_42,index_36),
inference(rew,[status(thm),theory(equality)],[1155,644]),
[iquote('0:Rew:1155.0,644.0')] ).
cnf(1158,plain,
equal(store(queue_38,tail,index_42),q14),
inference(rew,[status(thm),theory(equality)],[1155,407]),
[iquote('0:Rew:1155.0,407.0')] ).
cnf(1159,plain,
~ equal(s(index_42),index_36),
inference(rew,[status(thm),theory(equality)],[1155,831]),
[iquote('0:Rew:1155.0,831.0')] ).
cnf(1160,plain,
~ equal(s(s(index_42)),index_36),
inference(rew,[status(thm),theory(equality)],[1155,884]),
[iquote('0:Rew:1155.0,884.0')] ).
cnf(1161,plain,
~ equal(s(s(s(index_42))),index_36),
inference(rew,[status(thm),theory(equality)],[1155,937]),
[iquote('0:Rew:1155.0,937.0')] ).
cnf(1162,plain,
equal(index_33,index_36),
inference(rew,[status(thm),theory(equality)],[235,1003]),
[iquote('0:Rew:235.0,1003.0')] ).
cnf(1163,plain,
equal(s(index_30),index_36),
inference(rew,[status(thm),theory(equality)],[1162,234]),
[iquote('0:Rew:1162.0,234.0')] ).
cnf(1165,plain,
equal(store(queue_32,tail,index_36),q13),
inference(rew,[status(thm),theory(equality)],[1162,408]),
[iquote('0:Rew:1162.0,408.0')] ).
cnf(1169,plain,
equal(index_270,index_273),
inference(rew,[status(thm),theory(equality)],[227,1005]),
[iquote('0:Rew:227.0,1005.0')] ).
cnf(1170,plain,
equal(s(index_267),index_273),
inference(rew,[status(thm),theory(equality)],[1169,226]),
[iquote('0:Rew:1169.0,226.0')] ).
cnf(1172,plain,
equal(store(queue_269,tail,index_273),q8),
inference(rew,[status(thm),theory(equality)],[1169,411]),
[iquote('0:Rew:1169.0,411.0')] ).
cnf(1176,plain,
equal(index_264,index_267),
inference(rew,[status(thm),theory(equality)],[224,1006]),
[iquote('0:Rew:224.0,1006.0')] ).
cnf(1177,plain,
equal(s(index_261),index_267),
inference(rew,[status(thm),theory(equality)],[1176,223]),
[iquote('0:Rew:1176.0,223.0')] ).
cnf(1179,plain,
equal(store(queue_263,tail,index_267),q7),
inference(rew,[status(thm),theory(equality)],[1176,412]),
[iquote('0:Rew:1176.0,412.0')] ).
cnf(1183,plain,
equal(index_249,index_252),
inference(rew,[status(thm),theory(equality)],[217,1008]),
[iquote('0:Rew:217.0,1008.0')] ).
cnf(1184,plain,
equal(s(index_246),index_252),
inference(rew,[status(thm),theory(equality)],[1183,216]),
[iquote('0:Rew:1183.0,216.0')] ).
cnf(1186,plain,
equal(store(queue_248,tail,index_252),q5),
inference(rew,[status(thm),theory(equality)],[1183,414]),
[iquote('0:Rew:1183.0,414.0')] ).
cnf(1190,plain,
equal(index_237,index_246),
inference(rew,[status(thm),theory(equality)],[215,1011]),
[iquote('0:Rew:215.0,1011.0')] ).
cnf(1191,plain,
equal(s(index_234),index_246),
inference(rew,[status(thm),theory(equality)],[1190,211]),
[iquote('0:Rew:1190.0,211.0')] ).
cnf(1193,plain,
equal(store(queue_236,tail,index_246),q4),
inference(rew,[status(thm),theory(equality)],[1190,416]),
[iquote('0:Rew:1190.0,416.0')] ).
cnf(1197,plain,
equal(index_222,index_225),
inference(rew,[status(thm),theory(equality)],[206,1013]),
[iquote('0:Rew:206.0,1013.0')] ).
cnf(1198,plain,
equal(s(index_219),index_225),
inference(rew,[status(thm),theory(equality)],[1197,205]),
[iquote('0:Rew:1197.0,205.0')] ).
cnf(1200,plain,
equal(store(queue_221,tail,index_225),q38),
inference(rew,[status(thm),theory(equality)],[1197,418]),
[iquote('0:Rew:1197.0,418.0')] ).
cnf(1204,plain,
equal(index_216,index_219),
inference(rew,[status(thm),theory(equality)],[204,1014]),
[iquote('0:Rew:204.0,1014.0')] ).
cnf(1205,plain,
equal(s(index_213),index_219),
inference(rew,[status(thm),theory(equality)],[1204,203]),
[iquote('0:Rew:1204.0,203.0')] ).
cnf(1207,plain,
equal(store(queue_215,tail,index_219),q37),
inference(rew,[status(thm),theory(equality)],[1204,419]),
[iquote('0:Rew:1204.0,419.0')] ).
cnf(1211,plain,
equal(index_201,index_204),
inference(rew,[status(thm),theory(equality)],[197,1016]),
[iquote('0:Rew:197.0,1016.0')] ).
cnf(1212,plain,
equal(s(index_198),index_204),
inference(rew,[status(thm),theory(equality)],[1211,196]),
[iquote('0:Rew:1211.0,196.0')] ).
cnf(1214,plain,
equal(store(queue_200,tail,index_204),q35),
inference(rew,[status(thm),theory(equality)],[1211,421]),
[iquote('0:Rew:1211.0,421.0')] ).
cnf(1218,plain,
equal(index_195,index_198),
inference(rew,[status(thm),theory(equality)],[195,1017]),
[iquote('0:Rew:195.0,1017.0')] ).
cnf(1219,plain,
equal(s(index_192),index_198),
inference(rew,[status(thm),theory(equality)],[1218,194]),
[iquote('0:Rew:1218.0,194.0')] ).
cnf(1221,plain,
equal(store(queue_194,tail,index_198),q34),
inference(rew,[status(thm),theory(equality)],[1218,422]),
[iquote('0:Rew:1218.0,422.0')] ).
cnf(1225,plain,
equal(index_18,index_21),
inference(rew,[status(thm),theory(equality)],[200,1018]),
[iquote('0:Rew:200.0,1018.0')] ).
cnf(1226,plain,
equal(s(index_15),index_21),
inference(rew,[status(thm),theory(equality)],[1225,187]),
[iquote('0:Rew:1225.0,187.0')] ).
cnf(1228,plain,
equal(store(queue_17,tail,index_21),q11),
inference(rew,[status(thm),theory(equality)],[1225,424]),
[iquote('0:Rew:1225.0,424.0')] ).
cnf(1232,plain,
equal(index_180,index_183),
inference(rew,[status(thm),theory(equality)],[189,1020]),
[iquote('0:Rew:189.0,1020.0')] ).
cnf(1233,plain,
equal(s(index_177),index_183),
inference(rew,[status(thm),theory(equality)],[1232,188]),
[iquote('0:Rew:1232.0,188.0')] ).
cnf(1235,plain,
equal(store(queue_179,tail,index_183),q32),
inference(rew,[status(thm),theory(equality)],[1232,425]),
[iquote('0:Rew:1232.0,425.0')] ).
cnf(1239,plain,
equal(index_174,index_177),
inference(rew,[status(thm),theory(equality)],[186,1021]),
[iquote('0:Rew:186.0,1021.0')] ).
cnf(1240,plain,
equal(s(index_171),index_177),
inference(rew,[status(thm),theory(equality)],[1239,185]),
[iquote('0:Rew:1239.0,185.0')] ).
cnf(1242,plain,
equal(store(queue_173,tail,index_177),q31),
inference(rew,[status(thm),theory(equality)],[1239,426]),
[iquote('0:Rew:1239.0,426.0')] ).
cnf(1246,plain,
equal(index_150,index_162),
inference(rew,[status(thm),theory(equality)],[180,1024]),
[iquote('0:Rew:180.0,1024.0')] ).
cnf(1247,plain,
equal(s(index_147),index_162),
inference(rew,[status(thm),theory(equality)],[1246,175]),
[iquote('0:Rew:1246.0,175.0')] ).
cnf(1249,plain,
equal(store(queue_149,tail,index_162),q29),
inference(rew,[status(thm),theory(equality)],[1246,429]),
[iquote('0:Rew:1246.0,429.0')] ).
cnf(1253,plain,
equal(index_144,index_147),
inference(rew,[status(thm),theory(equality)],[173,1025]),
[iquote('0:Rew:173.0,1025.0')] ).
cnf(1254,plain,
equal(s(index_141),index_147),
inference(rew,[status(thm),theory(equality)],[1253,172]),
[iquote('0:Rew:1253.0,172.0')] ).
cnf(1256,plain,
equal(store(queue_143,tail,index_147),q28),
inference(rew,[status(thm),theory(equality)],[1253,430]),
[iquote('0:Rew:1253.0,430.0')] ).
cnf(1260,plain,
equal(index_129,index_132),
inference(rew,[status(thm),theory(equality)],[167,1027]),
[iquote('0:Rew:167.0,1027.0')] ).
cnf(1261,plain,
equal(s(index_126),index_132),
inference(rew,[status(thm),theory(equality)],[1260,166]),
[iquote('0:Rew:1260.0,166.0')] ).
cnf(1263,plain,
equal(store(queue_128,tail,index_132),q26),
inference(rew,[status(thm),theory(equality)],[1260,432]),
[iquote('0:Rew:1260.0,432.0')] ).
cnf(1267,plain,
equal(index_12,index_15),
inference(rew,[status(thm),theory(equality)],[174,1028]),
[iquote('0:Rew:174.0,1028.0')] ).
cnf(1268,plain,
equal(s(index_9),index_15),
inference(rew,[status(thm),theory(equality)],[1267,162]),
[iquote('0:Rew:1267.0,162.0')] ).
cnf(1270,plain,
equal(store(queue_11,tail,index_15),q10),
inference(rew,[status(thm),theory(equality)],[1267,433]),
[iquote('0:Rew:1267.0,433.0')] ).
cnf(1274,plain,
equal(index_123,index_126),
inference(rew,[status(thm),theory(equality)],[165,1029]),
[iquote('0:Rew:165.0,1029.0')] ).
cnf(1275,plain,
equal(s(index_120),index_126),
inference(rew,[status(thm),theory(equality)],[1274,164]),
[iquote('0:Rew:1274.0,164.0')] ).
cnf(1277,plain,
equal(store(queue_122,tail,index_126),q25),
inference(rew,[status(thm),theory(equality)],[1274,434]),
[iquote('0:Rew:1274.0,434.0')] ).
cnf(1281,plain,
equal(index_108,index_111),
inference(rew,[status(thm),theory(equality)],[158,1031]),
[iquote('0:Rew:158.0,1031.0')] ).
cnf(1282,plain,
equal(s(index_105),index_111),
inference(rew,[status(thm),theory(equality)],[1281,157]),
[iquote('0:Rew:1281.0,157.0')] ).
cnf(1284,plain,
equal(store(queue_107,tail,index_111),q23),
inference(rew,[status(thm),theory(equality)],[1281,436]),
[iquote('0:Rew:1281.0,436.0')] ).
cnf(1288,plain,
equal(index_102,index_105),
inference(rew,[status(thm),theory(equality)],[156,1032]),
[iquote('0:Rew:156.0,1032.0')] ).
cnf(1289,plain,
equal(s(index_99),index_105),
inference(rew,[status(thm),theory(equality)],[1288,155]),
[iquote('0:Rew:1288.0,155.0')] ).
cnf(1291,plain,
equal(store(queue_101,tail,index_105),q22),
inference(rew,[status(thm),theory(equality)],[1288,437]),
[iquote('0:Rew:1288.0,437.0')] ).
cnf(1301,plain,
~ equal(index_45,index_36),
inference(rew,[status(thm),theory(equality)],[238,1159]),
[iquote('0:Rew:238.0,1159.0')] ).
cnf(1330,plain,
~ equal(s(index_45),index_36),
inference(rew,[status(thm),theory(equality)],[238,1160]),
[iquote('0:Rew:238.0,1160.0')] ).
cnf(1369,plain,
~ equal(s(s(index_45)),index_36),
inference(rew,[status(thm),theory(equality)],[238,1161]),
[iquote('0:Rew:238.0,1161.0')] ).
cnf(1761,plain,
~ equal(s(s(s(s(index_42)))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,67]),
[iquote('0:SpL:1156.0,67.0')] ).
cnf(1787,plain,
~ equal(s(s(s(index_45))),index_36),
inference(rew,[status(thm),theory(equality)],[238,1761]),
[iquote('0:Rew:238.0,1761.0')] ).
cnf(1844,plain,
~ equal(s(s(s(s(s(index_42))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,66]),
[iquote('0:SpL:1156.0,66.0')] ).
cnf(1870,plain,
~ equal(s(s(s(s(index_45)))),index_36),
inference(rew,[status(thm),theory(equality)],[238,1844]),
[iquote('0:Rew:238.0,1844.0')] ).
cnf(1927,plain,
~ equal(s(s(s(s(s(s(index_42)))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,65]),
[iquote('0:SpL:1156.0,65.0')] ).
cnf(1953,plain,
~ equal(s(s(s(s(s(index_45))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,1927]),
[iquote('0:Rew:238.0,1927.0')] ).
cnf(2010,plain,
~ equal(s(s(s(s(s(s(s(index_42))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,64]),
[iquote('0:SpL:1156.0,64.0')] ).
cnf(2036,plain,
~ equal(s(s(s(s(s(s(index_45)))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2010]),
[iquote('0:Rew:238.0,2010.0')] ).
cnf(2093,plain,
~ equal(s(s(s(s(s(s(s(s(index_42)))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,63]),
[iquote('0:SpL:1156.0,63.0')] ).
cnf(2119,plain,
~ equal(s(s(s(s(s(s(s(index_45))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2093]),
[iquote('0:Rew:238.0,2093.0')] ).
cnf(2145,plain,
( equal(head,u)
| equal(select(queue_94,u),select(q21,u)) ),
inference(spr,[status(thm),theory(equality)],[398,2]),
[iquote('0:SpR:398.0,2.1')] ).
cnf(2146,plain,
( equal(head,u)
| equal(select(queue_67,u),select(q18,u)) ),
inference(spr,[status(thm),theory(equality)],[402,2]),
[iquote('0:SpR:402.0,2.1')] ).
cnf(2147,plain,
( equal(head,u)
| equal(select(queue_46,u),select(q15,u)) ),
inference(spr,[status(thm),theory(equality)],[406,2]),
[iquote('0:SpR:406.0,2.1')] ).
cnf(2148,plain,
( equal(head,u)
| equal(select(queue_277,u),select(q9,u)) ),
inference(spr,[status(thm),theory(equality)],[409,2]),
[iquote('0:SpR:409.0,2.1')] ).
cnf(2149,plain,
( equal(head,u)
| equal(select(queue_25,u),select(q12,u)) ),
inference(spr,[status(thm),theory(equality)],[410,2]),
[iquote('0:SpR:410.0,2.1')] ).
cnf(2150,plain,
( equal(head,u)
| equal(select(queue_256,u),select(q6,u)) ),
inference(spr,[status(thm),theory(equality)],[413,2]),
[iquote('0:SpR:413.0,2.1')] ).
cnf(2151,plain,
( equal(head,u)
| equal(select(queue_229,u),select(q39,u)) ),
inference(spr,[status(thm),theory(equality)],[417,2]),
[iquote('0:SpR:417.0,2.1')] ).
cnf(2152,plain,
( equal(head,u)
| equal(select(queue_208,u),select(q36,u)) ),
inference(spr,[status(thm),theory(equality)],[420,2]),
[iquote('0:SpR:420.0,2.1')] ).
cnf(2153,plain,
( equal(head,u)
| equal(select(queue_187,u),select(q33,u)) ),
inference(spr,[status(thm),theory(equality)],[423,2]),
[iquote('0:SpR:423.0,2.1')] ).
cnf(2154,plain,
( equal(head,u)
| equal(select(queue_166,u),select(q30,u)) ),
inference(spr,[status(thm),theory(equality)],[427,2]),
[iquote('0:SpR:427.0,2.1')] ).
cnf(2155,plain,
( equal(head,u)
| equal(select(queue_157,u),select(q3,u)) ),
inference(spr,[status(thm),theory(equality)],[428,2]),
[iquote('0:SpR:428.0,2.1')] ).
cnf(2156,plain,
( equal(head,u)
| equal(select(queue_136,u),select(q27,u)) ),
inference(spr,[status(thm),theory(equality)],[431,2]),
[iquote('0:SpR:431.0,2.1')] ).
cnf(2157,plain,
( equal(head,u)
| equal(select(queue_115,u),select(q24,u)) ),
inference(spr,[status(thm),theory(equality)],[435,2]),
[iquote('0:SpR:435.0,2.1')] ).
cnf(2158,plain,
( equal(head,u)
| equal(select(q,u),select(q0,u)) ),
inference(spr,[status(thm),theory(equality)],[438,2]),
[iquote('0:SpR:438.0,2.1')] ).
cnf(2159,plain,
( equal(tail,u)
| equal(select(queue_92,u),select(queue_94,u)) ),
inference(spr,[status(thm),theory(equality)],[354,2]),
[iquote('0:SpR:354.0,2.1')] ).
cnf(2160,plain,
( equal(tail,u)
| equal(select(queue_65,u),select(queue_67,u)) ),
inference(spr,[status(thm),theory(equality)],[344,2]),
[iquote('0:SpR:344.0,2.1')] ).
cnf(2161,plain,
( equal(tail,u)
| equal(select(queue_44,u),select(queue_46,u)) ),
inference(spr,[status(thm),theory(equality)],[336,2]),
[iquote('0:SpR:336.0,2.1')] ).
cnf(2162,plain,
( equal(tail,u)
| equal(select(queue_275,u),select(queue_277,u)) ),
inference(spr,[status(thm),theory(equality)],[328,2]),
[iquote('0:SpR:328.0,2.1')] ).
cnf(2163,plain,
( equal(tail,u)
| equal(select(queue_254,u),select(queue_256,u)) ),
inference(spr,[status(thm),theory(equality)],[321,2]),
[iquote('0:SpR:321.0,2.1')] ).
cnf(2164,plain,
( equal(tail,u)
| equal(select(queue_23,u),select(queue_25,u)) ),
inference(spr,[status(thm),theory(equality)],[318,2]),
[iquote('0:SpR:318.0,2.1')] ).
cnf(2165,plain,
( equal(tail,u)
| equal(select(queue_242,u),select(q40,u)) ),
inference(spr,[status(thm),theory(equality)],[415,2]),
[iquote('0:SpR:415.0,2.1')] ).
cnf(2166,plain,
( equal(tail,u)
| equal(select(queue_227,u),select(queue_229,u)) ),
inference(spr,[status(thm),theory(equality)],[310,2]),
[iquote('0:SpR:310.0,2.1')] ).
cnf(2167,plain,
( equal(tail,u)
| equal(select(queue_206,u),select(queue_208,u)) ),
inference(spr,[status(thm),theory(equality)],[303,2]),
[iquote('0:SpR:303.0,2.1')] ).
cnf(2168,plain,
( equal(tail,u)
| equal(select(queue_185,u),select(queue_187,u)) ),
inference(spr,[status(thm),theory(equality)],[295,2]),
[iquote('0:SpR:295.0,2.1')] ).
cnf(2169,plain,
( equal(tail,u)
| equal(select(queue_164,u),select(queue_166,u)) ),
inference(spr,[status(thm),theory(equality)],[287,2]),
[iquote('0:SpR:287.0,2.1')] ).
cnf(2170,plain,
( equal(tail,u)
| equal(select(queue_155,u),select(queue_157,u)) ),
inference(spr,[status(thm),theory(equality)],[284,2]),
[iquote('0:SpR:284.0,2.1')] ).
cnf(2171,plain,
( equal(tail,u)
| equal(select(queue_134,u),select(queue_136,u)) ),
inference(spr,[status(thm),theory(equality)],[277,2]),
[iquote('0:SpR:277.0,2.1')] ).
cnf(2172,plain,
( equal(tail,u)
| equal(select(queue_113,u),select(queue_115,u)) ),
inference(spr,[status(thm),theory(equality)],[269,2]),
[iquote('0:SpR:269.0,2.1')] ).
cnf(2173,plain,
( equal(tail,u)
| equal(select(queue_86,u),select(q20,u)) ),
inference(spr,[status(thm),theory(equality)],[1116,2]),
[iquote('0:SpR:1116.0,2.1')] ).
cnf(2174,plain,
( equal(tail,u)
| equal(select(queue_80,u),select(q2,u)) ),
inference(spr,[status(thm),theory(equality)],[1123,2]),
[iquote('0:SpR:1123.0,2.1')] ).
cnf(2175,plain,
( equal(tail,u)
| equal(select(queue_74,u),select(q19,u)) ),
inference(spr,[status(thm),theory(equality)],[1130,2]),
[iquote('0:SpR:1130.0,2.1')] ).
cnf(2176,plain,
( equal(tail,u)
| equal(select(queue_5,u),select(q1,u)) ),
inference(spr,[status(thm),theory(equality)],[1137,2]),
[iquote('0:SpR:1137.0,2.1')] ).
cnf(2177,plain,
( equal(tail,u)
| equal(select(queue_59,u),select(q17,u)) ),
inference(spr,[status(thm),theory(equality)],[1144,2]),
[iquote('0:SpR:1144.0,2.1')] ).
cnf(2178,plain,
( equal(tail,u)
| equal(select(queue_53,u),select(q16,u)) ),
inference(spr,[status(thm),theory(equality)],[1151,2]),
[iquote('0:SpR:1151.0,2.1')] ).
cnf(2179,plain,
( equal(tail,u)
| equal(select(queue_38,u),select(q14,u)) ),
inference(spr,[status(thm),theory(equality)],[1158,2]),
[iquote('0:SpR:1158.0,2.1')] ).
cnf(2180,plain,
( equal(tail,u)
| equal(select(queue_32,u),select(q13,u)) ),
inference(spr,[status(thm),theory(equality)],[1165,2]),
[iquote('0:SpR:1165.0,2.1')] ).
cnf(2181,plain,
( equal(tail,u)
| equal(select(queue_269,u),select(q8,u)) ),
inference(spr,[status(thm),theory(equality)],[1172,2]),
[iquote('0:SpR:1172.0,2.1')] ).
cnf(2182,plain,
( equal(tail,u)
| equal(select(queue_263,u),select(q7,u)) ),
inference(spr,[status(thm),theory(equality)],[1179,2]),
[iquote('0:SpR:1179.0,2.1')] ).
cnf(2183,plain,
( equal(tail,u)
| equal(select(queue_248,u),select(q5,u)) ),
inference(spr,[status(thm),theory(equality)],[1186,2]),
[iquote('0:SpR:1186.0,2.1')] ).
cnf(2184,plain,
( equal(tail,u)
| equal(select(queue_236,u),select(q4,u)) ),
inference(spr,[status(thm),theory(equality)],[1193,2]),
[iquote('0:SpR:1193.0,2.1')] ).
cnf(2185,plain,
( equal(tail,u)
| equal(select(queue_221,u),select(q38,u)) ),
inference(spr,[status(thm),theory(equality)],[1200,2]),
[iquote('0:SpR:1200.0,2.1')] ).
cnf(2186,plain,
( equal(tail,u)
| equal(select(queue_215,u),select(q37,u)) ),
inference(spr,[status(thm),theory(equality)],[1207,2]),
[iquote('0:SpR:1207.0,2.1')] ).
cnf(2187,plain,
( equal(tail,u)
| equal(select(queue_200,u),select(q35,u)) ),
inference(spr,[status(thm),theory(equality)],[1214,2]),
[iquote('0:SpR:1214.0,2.1')] ).
cnf(2188,plain,
( equal(tail,u)
| equal(select(queue_194,u),select(q34,u)) ),
inference(spr,[status(thm),theory(equality)],[1221,2]),
[iquote('0:SpR:1221.0,2.1')] ).
cnf(2189,plain,
( equal(tail,u)
| equal(select(queue_17,u),select(q11,u)) ),
inference(spr,[status(thm),theory(equality)],[1228,2]),
[iquote('0:SpR:1228.0,2.1')] ).
cnf(2190,plain,
( equal(tail,u)
| equal(select(queue_179,u),select(q32,u)) ),
inference(spr,[status(thm),theory(equality)],[1235,2]),
[iquote('0:SpR:1235.0,2.1')] ).
cnf(2191,plain,
( equal(tail,u)
| equal(select(queue_173,u),select(q31,u)) ),
inference(spr,[status(thm),theory(equality)],[1242,2]),
[iquote('0:SpR:1242.0,2.1')] ).
cnf(2192,plain,
( equal(tail,u)
| equal(select(queue_149,u),select(q29,u)) ),
inference(spr,[status(thm),theory(equality)],[1249,2]),
[iquote('0:SpR:1249.0,2.1')] ).
cnf(2193,plain,
( equal(tail,u)
| equal(select(queue_143,u),select(q28,u)) ),
inference(spr,[status(thm),theory(equality)],[1256,2]),
[iquote('0:SpR:1256.0,2.1')] ).
cnf(2194,plain,
( equal(tail,u)
| equal(select(queue_128,u),select(q26,u)) ),
inference(spr,[status(thm),theory(equality)],[1263,2]),
[iquote('0:SpR:1263.0,2.1')] ).
cnf(2195,plain,
( equal(tail,u)
| equal(select(queue_11,u),select(q10,u)) ),
inference(spr,[status(thm),theory(equality)],[1270,2]),
[iquote('0:SpR:1270.0,2.1')] ).
cnf(2196,plain,
( equal(tail,u)
| equal(select(queue_122,u),select(q25,u)) ),
inference(spr,[status(thm),theory(equality)],[1277,2]),
[iquote('0:SpR:1277.0,2.1')] ).
cnf(2197,plain,
( equal(tail,u)
| equal(select(queue_107,u),select(q23,u)) ),
inference(spr,[status(thm),theory(equality)],[1284,2]),
[iquote('0:SpR:1284.0,2.1')] ).
cnf(2198,plain,
( equal(tail,u)
| equal(select(queue_101,u),select(q22,u)) ),
inference(spr,[status(thm),theory(equality)],[1291,2]),
[iquote('0:SpR:1291.0,2.1')] ).
cnf(2199,plain,
( equal(seq,u)
| equal(select(queue_92,u),select(q20,u)) ),
inference(spr,[status(thm),theory(equality)],[353,2]),
[iquote('0:SpR:353.0,2.1')] ).
cnf(2200,plain,
( equal(seq,u)
| equal(select(queue_86,u),select(q19,u)) ),
inference(spr,[status(thm),theory(equality)],[351,2]),
[iquote('0:SpR:351.0,2.1')] ).
cnf(2201,plain,
( equal(seq,u)
| equal(select(queue_80,u),select(q1,u)) ),
inference(spr,[status(thm),theory(equality)],[349,2]),
[iquote('0:SpR:349.0,2.1')] ).
cnf(2202,plain,
( equal(seq,u)
| equal(select(queue_74,u),select(q18,u)) ),
inference(spr,[status(thm),theory(equality)],[347,2]),
[iquote('0:SpR:347.0,2.1')] ).
cnf(2203,plain,
( equal(seq,u)
| equal(select(queue_65,u),select(q17,u)) ),
inference(spr,[status(thm),theory(equality)],[343,2]),
[iquote('0:SpR:343.0,2.1')] ).
cnf(2204,plain,
( equal(seq,u)
| equal(select(queue_59,u),select(q16,u)) ),
inference(spr,[status(thm),theory(equality)],[341,2]),
[iquote('0:SpR:341.0,2.1')] ).
cnf(2205,plain,
( equal(seq,u)
| equal(select(queue_53,u),select(q15,u)) ),
inference(spr,[status(thm),theory(equality)],[339,2]),
[iquote('0:SpR:339.0,2.1')] ).
cnf(2206,plain,
( equal(seq,u)
| equal(select(queue_5,u),select(q0,u)) ),
inference(spr,[status(thm),theory(equality)],[338,2]),
[iquote('0:SpR:338.0,2.1')] ).
cnf(2207,plain,
( equal(seq,u)
| equal(select(queue_44,u),select(q14,u)) ),
inference(spr,[status(thm),theory(equality)],[335,2]),
[iquote('0:SpR:335.0,2.1')] ).
cnf(2208,plain,
( equal(seq,u)
| equal(select(queue_38,u),select(q13,u)) ),
inference(spr,[status(thm),theory(equality)],[333,2]),
[iquote('0:SpR:333.0,2.1')] ).
cnf(2209,plain,
( equal(seq,u)
| equal(select(queue_32,u),select(q12,u)) ),
inference(spr,[status(thm),theory(equality)],[331,2]),
[iquote('0:SpR:331.0,2.1')] ).
cnf(2210,plain,
( equal(seq,u)
| equal(select(queue_275,u),select(q8,u)) ),
inference(spr,[status(thm),theory(equality)],[327,2]),
[iquote('0:SpR:327.0,2.1')] ).
cnf(2211,plain,
( equal(seq,u)
| equal(select(queue_269,u),select(q7,u)) ),
inference(spr,[status(thm),theory(equality)],[325,2]),
[iquote('0:SpR:325.0,2.1')] ).
cnf(2212,plain,
( equal(seq,u)
| equal(select(queue_263,u),select(q6,u)) ),
inference(spr,[status(thm),theory(equality)],[323,2]),
[iquote('0:SpR:323.0,2.1')] ).
cnf(2213,plain,
( equal(seq,u)
| equal(select(queue_254,u),select(q5,u)) ),
inference(spr,[status(thm),theory(equality)],[320,2]),
[iquote('0:SpR:320.0,2.1')] ).
cnf(2214,plain,
( equal(seq,u)
| equal(select(queue_248,u),select(q4,u)) ),
inference(spr,[status(thm),theory(equality)],[317,2]),
[iquote('0:SpR:317.0,2.1')] ).
cnf(2215,plain,
( equal(seq,u)
| equal(select(queue_242,u),select(q39,u)) ),
inference(spr,[status(thm),theory(equality)],[315,2]),
[iquote('0:SpR:315.0,2.1')] ).
cnf(2216,plain,
( equal(seq,u)
| equal(select(queue_236,u),select(q3,u)) ),
inference(spr,[status(thm),theory(equality)],[313,2]),
[iquote('0:SpR:313.0,2.1')] ).
cnf(2217,plain,
( equal(seq,u)
| equal(select(queue_23,u),select(q11,u)) ),
inference(spr,[status(thm),theory(equality)],[311,2]),
[iquote('0:SpR:311.0,2.1')] ).
cnf(2218,plain,
( equal(seq,u)
| equal(select(queue_227,u),select(q38,u)) ),
inference(spr,[status(thm),theory(equality)],[309,2]),
[iquote('0:SpR:309.0,2.1')] ).
cnf(2219,plain,
( equal(seq,u)
| equal(select(queue_221,u),select(q37,u)) ),
inference(spr,[status(thm),theory(equality)],[307,2]),
[iquote('0:SpR:307.0,2.1')] ).
cnf(2220,plain,
( equal(seq,u)
| equal(select(queue_215,u),select(q36,u)) ),
inference(spr,[status(thm),theory(equality)],[305,2]),
[iquote('0:SpR:305.0,2.1')] ).
cnf(2221,plain,
( equal(seq,u)
| equal(select(queue_206,u),select(q35,u)) ),
inference(spr,[status(thm),theory(equality)],[302,2]),
[iquote('0:SpR:302.0,2.1')] ).
cnf(2222,plain,
( equal(seq,u)
| equal(select(queue_200,u),select(q34,u)) ),
inference(spr,[status(thm),theory(equality)],[300,2]),
[iquote('0:SpR:300.0,2.1')] ).
cnf(2223,plain,
( equal(seq,u)
| equal(select(queue_194,u),select(q33,u)) ),
inference(spr,[status(thm),theory(equality)],[298,2]),
[iquote('0:SpR:298.0,2.1')] ).
cnf(2224,plain,
( equal(seq,u)
| equal(select(queue_185,u),select(q32,u)) ),
inference(spr,[status(thm),theory(equality)],[294,2]),
[iquote('0:SpR:294.0,2.1')] ).
cnf(2225,plain,
( equal(seq,u)
| equal(select(queue_179,u),select(q31,u)) ),
inference(spr,[status(thm),theory(equality)],[292,2]),
[iquote('0:SpR:292.0,2.1')] ).
cnf(2226,plain,
( equal(seq,u)
| equal(select(queue_173,u),select(q30,u)) ),
inference(spr,[status(thm),theory(equality)],[290,2]),
[iquote('0:SpR:290.0,2.1')] ).
cnf(2227,plain,
( equal(seq,u)
| equal(select(queue_17,u),select(q10,u)) ),
inference(spr,[status(thm),theory(equality)],[289,2]),
[iquote('0:SpR:289.0,2.1')] ).
cnf(2228,plain,
( equal(seq,u)
| equal(select(queue_164,u),select(q29,u)) ),
inference(spr,[status(thm),theory(equality)],[286,2]),
[iquote('0:SpR:286.0,2.1')] ).
cnf(2229,plain,
( equal(seq,u)
| equal(select(queue_155,u),select(q2,u)) ),
inference(spr,[status(thm),theory(equality)],[283,2]),
[iquote('0:SpR:283.0,2.1')] ).
cnf(2230,plain,
( equal(seq,u)
| equal(select(queue_149,u),select(q28,u)) ),
inference(spr,[status(thm),theory(equality)],[281,2]),
[iquote('0:SpR:281.0,2.1')] ).
cnf(2231,plain,
( equal(seq,u)
| equal(select(queue_143,u),select(q27,u)) ),
inference(spr,[status(thm),theory(equality)],[279,2]),
[iquote('0:SpR:279.0,2.1')] ).
cnf(2232,plain,
( equal(seq,u)
| equal(select(queue_134,u),select(q26,u)) ),
inference(spr,[status(thm),theory(equality)],[276,2]),
[iquote('0:SpR:276.0,2.1')] ).
cnf(2233,plain,
( equal(seq,u)
| equal(select(queue_128,u),select(q25,u)) ),
inference(spr,[status(thm),theory(equality)],[273,2]),
[iquote('0:SpR:273.0,2.1')] ).
cnf(2234,plain,
( equal(seq,u)
| equal(select(queue_122,u),select(q24,u)) ),
inference(spr,[status(thm),theory(equality)],[271,2]),
[iquote('0:SpR:271.0,2.1')] ).
cnf(2235,plain,
( equal(seq,u)
| equal(select(queue_113,u),select(q23,u)) ),
inference(spr,[status(thm),theory(equality)],[268,2]),
[iquote('0:SpR:268.0,2.1')] ).
cnf(2236,plain,
( equal(seq,u)
| equal(select(queue_11,u),select(q9,u)) ),
inference(spr,[status(thm),theory(equality)],[267,2]),
[iquote('0:SpR:267.0,2.1')] ).
cnf(2237,plain,
( equal(seq,u)
| equal(select(queue_107,u),select(q22,u)) ),
inference(spr,[status(thm),theory(equality)],[265,2]),
[iquote('0:SpR:265.0,2.1')] ).
cnf(2238,plain,
( equal(seq,u)
| equal(select(queue_101,u),select(q21,u)) ),
inference(spr,[status(thm),theory(equality)],[263,2]),
[iquote('0:SpR:263.0,2.1')] ).
cnf(2239,plain,
( equal(index_90,u)
| equal(select(earray_91,u),select(earray_89,u)) ),
inference(spr,[status(thm),theory(equality)],[151,2]),
[iquote('0:SpR:151.0,2.1')] ).
cnf(2240,plain,
( equal(index_84,u)
| equal(select(earray_85,u),select(earray_83,u)) ),
inference(spr,[status(thm),theory(equality)],[149,2]),
[iquote('0:SpR:149.0,2.1')] ).
cnf(2242,plain,
( equal(index_72,u)
| equal(select(earray_73,u),select(earray_71,u)) ),
inference(spr,[status(thm),theory(equality)],[144,2]),
[iquote('0:SpR:144.0,2.1')] ).
cnf(2243,plain,
( equal(index_63,u)
| equal(select(earray_64,u),select(earray_62,u)) ),
inference(spr,[status(thm),theory(equality)],[142,2]),
[iquote('0:SpR:142.0,2.1')] ).
cnf(2244,plain,
( equal(index_57,u)
| equal(select(earray_58,u),select(earray_56,u)) ),
inference(spr,[status(thm),theory(equality)],[140,2]),
[iquote('0:SpR:140.0,2.1')] ).
cnf(2245,plain,
( equal(index_51,u)
| equal(select(earray_52,u),select(earray_50,u)) ),
inference(spr,[status(thm),theory(equality)],[138,2]),
[iquote('0:SpR:138.0,2.1')] ).
cnf(2246,plain,
( equal(index_42,u)
| equal(select(earray_43,u),select(earray_41,u)) ),
inference(spr,[status(thm),theory(equality)],[136,2]),
[iquote('0:SpR:136.0,2.1')] ).
cnf(2255,plain,
( equal(index_240,u)
| equal(select(earray_241,u),select(earray_239,u)) ),
inference(spr,[status(thm),theory(equality)],[118,2]),
[iquote('0:SpR:118.0,2.1')] ).
cnf(2257,plain,
( equal(index_225,u)
| equal(select(earray_226,u),select(earray_224,u)) ),
inference(spr,[status(thm),theory(equality)],[114,2]),
[iquote('0:SpR:114.0,2.1')] ).
cnf(2258,plain,
( equal(index_219,u)
| equal(select(earray_220,u),select(earray_218,u)) ),
inference(spr,[status(thm),theory(equality)],[112,2]),
[iquote('0:SpR:112.0,2.1')] ).
cnf(2260,plain,
( equal(index_213,u)
| equal(select(earray_214,u),select(earray_212,u)) ),
inference(spr,[status(thm),theory(equality)],[109,2]),
[iquote('0:SpR:109.0,2.1')] ).
cnf(2261,plain,
( equal(index_204,u)
| equal(select(earray_205,u),select(earray_203,u)) ),
inference(spr,[status(thm),theory(equality)],[107,2]),
[iquote('0:SpR:107.0,2.1')] ).
cnf(2262,plain,
( equal(index_198,u)
| equal(select(earray_199,u),select(earray_197,u)) ),
inference(spr,[status(thm),theory(equality)],[103,2]),
[iquote('0:SpR:103.0,2.1')] ).
cnf(2263,plain,
( equal(index_192,u)
| equal(select(earray_193,u),select(earray_191,u)) ),
inference(spr,[status(thm),theory(equality)],[101,2]),
[iquote('0:SpR:101.0,2.1')] ).
cnf(2264,plain,
( equal(index_183,u)
| equal(select(earray_184,u),select(earray_182,u)) ),
inference(spr,[status(thm),theory(equality)],[99,2]),
[iquote('0:SpR:99.0,2.1')] ).
cnf(2265,plain,
( equal(index_177,u)
| equal(select(earray_178,u),select(earray_176,u)) ),
inference(spr,[status(thm),theory(equality)],[97,2]),
[iquote('0:SpR:97.0,2.1')] ).
cnf(2266,plain,
( equal(index_171,u)
| equal(select(earray_172,u),select(earray_170,u)) ),
inference(spr,[status(thm),theory(equality)],[95,2]),
[iquote('0:SpR:95.0,2.1')] ).
cnf(2267,plain,
( equal(index_162,u)
| equal(select(earray_163,u),select(earray_161,u)) ),
inference(spr,[status(thm),theory(equality)],[93,2]),
[iquote('0:SpR:93.0,2.1')] ).
cnf(2270,plain,
( equal(index_147,u)
| equal(select(earray_148,u),select(earray_146,u)) ),
inference(spr,[status(thm),theory(equality)],[88,2]),
[iquote('0:SpR:88.0,2.1')] ).
cnf(2271,plain,
( equal(index_141,u)
| equal(select(earray_142,u),select(earray_140,u)) ),
inference(spr,[status(thm),theory(equality)],[86,2]),
[iquote('0:SpR:86.0,2.1')] ).
cnf(2272,plain,
( equal(index_132,u)
| equal(select(earray_133,u),select(earray_131,u)) ),
inference(spr,[status(thm),theory(equality)],[83,2]),
[iquote('0:SpR:83.0,2.1')] ).
cnf(2273,plain,
( equal(index_126,u)
| equal(select(earray_127,u),select(earray_125,u)) ),
inference(spr,[status(thm),theory(equality)],[81,2]),
[iquote('0:SpR:81.0,2.1')] ).
cnf(2274,plain,
( equal(index_120,u)
| equal(select(earray_121,u),select(earray_119,u)) ),
inference(spr,[status(thm),theory(equality)],[79,2]),
[iquote('0:SpR:79.0,2.1')] ).
cnf(2275,plain,
( equal(index_111,u)
| equal(select(earray_112,u),select(earray_110,u)) ),
inference(spr,[status(thm),theory(equality)],[77,2]),
[iquote('0:SpR:77.0,2.1')] ).
cnf(2276,plain,
( equal(index_105,u)
| equal(select(earray_106,u),select(earray_104,u)) ),
inference(spr,[status(thm),theory(equality)],[75,2]),
[iquote('0:SpR:75.0,2.1')] ).
cnf(2277,plain,
( equal(index_99,u)
| equal(select(earray_98,u),select(earray_100,u)) ),
inference(spr,[status(thm),theory(equality)],[73,2]),
[iquote('0:SpR:73.0,2.1')] ).
cnf(2316,plain,
~ equal(s(s(s(s(s(s(s(s(s(index_42))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,62]),
[iquote('0:SpL:1156.0,62.0')] ).
cnf(2342,plain,
~ equal(s(s(s(s(s(s(s(s(index_45)))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2316]),
[iquote('0:Rew:238.0,2316.0')] ).
cnf(2399,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(index_42)))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,61]),
[iquote('0:SpL:1156.0,61.0')] ).
cnf(2425,plain,
~ equal(s(s(s(s(s(s(s(s(s(index_45))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2399]),
[iquote('0:Rew:238.0,2399.0')] ).
cnf(2482,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,60]),
[iquote('0:SpL:1156.0,60.0')] ).
cnf(2508,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(index_45)))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2482]),
[iquote('0:Rew:238.0,2482.0')] ).
cnf(2565,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,59]),
[iquote('0:SpL:1156.0,59.0')] ).
cnf(2591,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2565]),
[iquote('0:Rew:238.0,2565.0')] ).
cnf(2648,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,58]),
[iquote('0:SpL:1156.0,58.0')] ).
cnf(2674,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2648]),
[iquote('0:Rew:238.0,2648.0')] ).
cnf(2731,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,57]),
[iquote('0:SpL:1156.0,57.0')] ).
cnf(2757,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2731]),
[iquote('0:Rew:238.0,2731.0')] ).
cnf(2814,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,56]),
[iquote('0:SpL:1156.0,56.0')] ).
cnf(2840,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2814]),
[iquote('0:Rew:238.0,2814.0')] ).
cnf(2897,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,55]),
[iquote('0:SpL:1156.0,55.0')] ).
cnf(2936,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2897]),
[iquote('0:Rew:238.0,2897.0')] ).
cnf(2980,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,54]),
[iquote('0:SpL:1156.0,54.0')] ).
cnf(3019,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,2980]),
[iquote('0:Rew:238.0,2980.0')] ).
cnf(3063,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,53]),
[iquote('0:SpL:1156.0,53.0')] ).
cnf(3102,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,3063]),
[iquote('0:Rew:238.0,3063.0')] ).
cnf(3146,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,52]),
[iquote('0:SpL:1156.0,52.0')] ).
cnf(3185,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,3146]),
[iquote('0:Rew:238.0,3146.0')] ).
cnf(3226,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,51]),
[iquote('0:SpL:1156.0,51.0')] ).
cnf(3265,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,3226]),
[iquote('0:Rew:238.0,3226.0')] ).
cnf(3305,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,50]),
[iquote('0:SpL:1156.0,50.0')] ).
cnf(3344,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,3305]),
[iquote('0:Rew:238.0,3305.0')] ).
cnf(3384,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,49]),
[iquote('0:SpL:1156.0,49.0')] ).
cnf(3423,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,3384]),
[iquote('0:Rew:238.0,3384.0')] ).
cnf(3463,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,48]),
[iquote('0:SpL:1156.0,48.0')] ).
cnf(3502,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,3463]),
[iquote('0:Rew:238.0,3463.0')] ).
cnf(3542,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,47]),
[iquote('0:SpL:1156.0,47.0')] ).
cnf(3581,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,3542]),
[iquote('0:Rew:238.0,3542.0')] ).
cnf(3621,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))))))))))))),index_36),
inference(spl,[status(thm),theory(equality)],[1156,46]),
[iquote('0:SpL:1156.0,46.0')] ).
cnf(3660,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[238,3621]),
[iquote('0:Rew:238.0,3621.0')] ).
cnf(6831,plain,
( equal(tail,head)
| equal(select(q21,tail),index_93) ),
inference(spr,[status(thm),theory(equality)],[2145,993]),
[iquote('0:SpR:2145.1,993.0')] ).
cnf(6834,plain,
( equal(tail,head)
| equal(index_93,index_99) ),
inference(rew,[status(thm),theory(equality)],[261,6831]),
[iquote('0:Rew:261.0,6831.1')] ).
cnf(6835,plain,
equal(index_93,index_99),
inference(mrr,[status(thm)],[6834,3]),
[iquote('0:MRR:6834.0,3.0')] ).
cnf(6836,plain,
equal(s(index_90),index_99),
inference(rew,[status(thm),theory(equality)],[6835,258]),
[iquote('0:Rew:6835.0,258.0')] ).
cnf(7364,plain,
( equal(tail,head)
| equal(select(q18,tail),index_66) ),
inference(spr,[status(thm),theory(equality)],[2146,998]),
[iquote('0:SpR:2146.1,998.0')] ).
cnf(7367,plain,
( equal(tail,head)
| equal(index_66,index_72) ),
inference(rew,[status(thm),theory(equality)],[250,7364]),
[iquote('0:Rew:250.0,7364.1')] ).
cnf(7368,plain,
equal(index_66,index_72),
inference(mrr,[status(thm)],[7367,3]),
[iquote('0:MRR:7367.0,3.0')] ).
cnf(7369,plain,
equal(s(index_63),index_72),
inference(rew,[status(thm),theory(equality)],[7368,247]),
[iquote('0:Rew:7368.0,247.0')] ).
cnf(7897,plain,
( equal(tail,head)
| equal(select(q15,tail),index_45) ),
inference(spr,[status(thm),theory(equality)],[2147,1001]),
[iquote('0:SpR:2147.1,1001.0')] ).
cnf(7900,plain,
( equal(tail,head)
| equal(index_45,index_51) ),
inference(rew,[status(thm),theory(equality)],[241,7897]),
[iquote('0:Rew:241.0,7897.1')] ).
cnf(7901,plain,
equal(index_45,index_51),
inference(mrr,[status(thm)],[7900,3]),
[iquote('0:MRR:7900.0,3.0')] ).
cnf(7905,plain,
~ equal(index_51,index_36),
inference(rew,[status(thm),theory(equality)],[7901,1301]),
[iquote('0:Rew:7901.0,1301.0')] ).
cnf(7908,plain,
~ equal(s(index_51),index_36),
inference(rew,[status(thm),theory(equality)],[7901,1330]),
[iquote('0:Rew:7901.0,1330.0')] ).
cnf(7911,plain,
~ equal(s(s(index_51)),index_36),
inference(rew,[status(thm),theory(equality)],[7901,1369]),
[iquote('0:Rew:7901.0,1369.0')] ).
cnf(7914,plain,
~ equal(s(s(s(index_51))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,1787]),
[iquote('0:Rew:7901.0,1787.0')] ).
cnf(7917,plain,
~ equal(s(s(s(s(index_51)))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,1870]),
[iquote('0:Rew:7901.0,1870.0')] ).
cnf(7920,plain,
~ equal(s(s(s(s(s(index_51))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,1953]),
[iquote('0:Rew:7901.0,1953.0')] ).
cnf(7923,plain,
~ equal(s(s(s(s(s(s(index_51)))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2036]),
[iquote('0:Rew:7901.0,2036.0')] ).
cnf(7935,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2936]),
[iquote('0:Rew:7901.0,2936.0')] ).
cnf(7937,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3019]),
[iquote('0:Rew:7901.0,3019.0')] ).
cnf(7939,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3102]),
[iquote('0:Rew:7901.0,3102.0')] ).
cnf(7941,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3185]),
[iquote('0:Rew:7901.0,3185.0')] ).
cnf(7943,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3265]),
[iquote('0:Rew:7901.0,3265.0')] ).
cnf(7945,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3344]),
[iquote('0:Rew:7901.0,3344.0')] ).
cnf(7947,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3423]),
[iquote('0:Rew:7901.0,3423.0')] ).
cnf(7949,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3502]),
[iquote('0:Rew:7901.0,3502.0')] ).
cnf(7951,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3581]),
[iquote('0:Rew:7901.0,3581.0')] ).
cnf(7953,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,3660]),
[iquote('0:Rew:7901.0,3660.0')] ).
cnf(8084,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2840]),
[iquote('0:Rew:7901.0,2840.0')] ).
cnf(8086,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2757]),
[iquote('0:Rew:7901.0,2757.0')] ).
cnf(8088,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2674]),
[iquote('0:Rew:7901.0,2674.0')] ).
cnf(8090,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2591]),
[iquote('0:Rew:7901.0,2591.0')] ).
cnf(8092,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(index_51)))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2508]),
[iquote('0:Rew:7901.0,2508.0')] ).
cnf(8094,plain,
~ equal(s(s(s(s(s(s(s(s(s(index_51))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2425]),
[iquote('0:Rew:7901.0,2425.0')] ).
cnf(8096,plain,
~ equal(s(s(s(s(s(s(s(s(index_51)))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2342]),
[iquote('0:Rew:7901.0,2342.0')] ).
cnf(8098,plain,
~ equal(s(s(s(s(s(s(s(index_51))))))),index_36),
inference(rew,[status(thm),theory(equality)],[7901,2119]),
[iquote('0:Rew:7901.0,2119.0')] ).
cnf(8101,plain,
~ equal(index_57,index_36),
inference(rew,[status(thm),theory(equality)],[1149,7908]),
[iquote('0:Rew:1149.0,7908.0')] ).
cnf(8104,plain,
~ equal(index_63,index_36),
inference(rew,[status(thm),theory(equality)],[1142,7911,1149]),
[iquote('0:Rew:1142.0,7911.0,1149.0,7911.0')] ).
cnf(8107,plain,
~ equal(index_72,index_36),
inference(rew,[status(thm),theory(equality)],[7369,7914,1142,1149]),
[iquote('0:Rew:7369.0,7914.0,1142.0,7914.0,1149.0,7914.0')] ).
cnf(8110,plain,
~ equal(index_84,index_36),
inference(rew,[status(thm),theory(equality)],[1128,7917,7369,1142,1149]),
[iquote('0:Rew:1128.0,7917.0,7369.0,7917.0,1142.0,7917.0,1149.0,7917.0')] ).
cnf(8113,plain,
~ equal(index_90,index_36),
inference(rew,[status(thm),theory(equality)],[1114,7920,1128,7369,1142,1149]),
[iquote('0:Rew:1114.0,7920.0,1128.0,7920.0,7369.0,7920.0,1142.0,7920.0,1149.0,7920.0')] ).
cnf(8116,plain,
~ equal(index_36,index_99),
inference(rew,[status(thm),theory(equality)],[6836,7923,1114,1128,7369,1142,1149]),
[iquote('0:Rew:6836.0,7923.0,1114.0,7923.0,1128.0,7923.0,7369.0,7923.0,1142.0,7923.0,1149.0,7923.0')] ).
cnf(8119,plain,
~ equal(index_36,index_105),
inference(rew,[status(thm),theory(equality)],[1289,8098,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:1289.0,8098.0,6836.0,8098.0,1114.0,8098.0,1128.0,8098.0,7369.0,8098.0,1142.0,8098.0,1149.0,8098.0')] ).
cnf(8122,plain,
~ equal(index_36,index_111),
inference(rew,[status(thm),theory(equality)],[1282,8096,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:1282.0,8096.0,1289.0,8096.0,6836.0,8096.0,1114.0,8096.0,1128.0,8096.0,7369.0,8096.0,1142.0,8096.0,1149.0,8096.0')] ).
cnf(8125,plain,
~ equal(index_114,index_36),
inference(rew,[status(thm),theory(equality)],[159,8094,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,8094.0,1282.0,8094.0,1289.0,8094.0,6836.0,8094.0,1114.0,8094.0,1128.0,8094.0,7369.0,8094.0,1142.0,8094.0,1149.0,8094.0')] ).
cnf(8128,plain,
~ equal(s(index_114),index_36),
inference(rew,[status(thm),theory(equality)],[159,8092,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,8092.0,1282.0,8092.0,1289.0,8092.0,6836.0,8092.0,1114.0,8092.0,1128.0,8092.0,7369.0,8092.0,1142.0,8092.0,1149.0,8092.0')] ).
cnf(8131,plain,
~ equal(s(s(index_114)),index_36),
inference(rew,[status(thm),theory(equality)],[159,8090,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,8090.0,1282.0,8090.0,1289.0,8090.0,6836.0,8090.0,1114.0,8090.0,1128.0,8090.0,7369.0,8090.0,1142.0,8090.0,1149.0,8090.0')] ).
cnf(8134,plain,
~ equal(s(s(s(index_114))),index_36),
inference(rew,[status(thm),theory(equality)],[159,8088,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,8088.0,1282.0,8088.0,1289.0,8088.0,6836.0,8088.0,1114.0,8088.0,1128.0,8088.0,7369.0,8088.0,1142.0,8088.0,1149.0,8088.0')] ).
cnf(8137,plain,
~ equal(s(s(s(s(index_114)))),index_36),
inference(rew,[status(thm),theory(equality)],[159,8086,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,8086.0,1282.0,8086.0,1289.0,8086.0,6836.0,8086.0,1114.0,8086.0,1128.0,8086.0,7369.0,8086.0,1142.0,8086.0,1149.0,8086.0')] ).
cnf(8140,plain,
~ equal(s(s(s(s(s(index_114))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,8084,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,8084.0,1282.0,8084.0,1289.0,8084.0,6836.0,8084.0,1114.0,8084.0,1128.0,8084.0,7369.0,8084.0,1142.0,8084.0,1149.0,8084.0')] ).
cnf(8143,plain,
~ equal(s(s(s(s(s(s(index_114)))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7935,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7935.0,1282.0,7935.0,1289.0,7935.0,6836.0,7935.0,1114.0,7935.0,1128.0,7935.0,7369.0,7935.0,1142.0,7935.0,1149.0,7935.0')] ).
cnf(8146,plain,
~ equal(s(s(s(s(s(s(s(index_114))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7937,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7937.0,1282.0,7937.0,1289.0,7937.0,6836.0,7937.0,1114.0,7937.0,1128.0,7937.0,7369.0,7937.0,1142.0,7937.0,1149.0,7937.0')] ).
cnf(8149,plain,
~ equal(s(s(s(s(s(s(s(s(index_114)))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7939,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7939.0,1282.0,7939.0,1289.0,7939.0,6836.0,7939.0,1114.0,7939.0,1128.0,7939.0,7369.0,7939.0,1142.0,7939.0,1149.0,7939.0')] ).
cnf(8152,plain,
~ equal(s(s(s(s(s(s(s(s(s(index_114))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7941,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7941.0,1282.0,7941.0,1289.0,7941.0,6836.0,7941.0,1114.0,7941.0,1128.0,7941.0,7369.0,7941.0,1142.0,7941.0,1149.0,7941.0')] ).
cnf(8155,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(index_114)))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7943,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7943.0,1282.0,7943.0,1289.0,7943.0,6836.0,7943.0,1114.0,7943.0,1128.0,7943.0,7369.0,7943.0,1142.0,7943.0,1149.0,7943.0')] ).
cnf(8158,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7945,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7945.0,1282.0,7945.0,1289.0,7945.0,6836.0,7945.0,1114.0,7945.0,1128.0,7945.0,7369.0,7945.0,1142.0,7945.0,1149.0,7945.0')] ).
cnf(8161,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7947,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7947.0,1282.0,7947.0,1289.0,7947.0,6836.0,7947.0,1114.0,7947.0,1128.0,7947.0,7369.0,7947.0,1142.0,7947.0,1149.0,7947.0')] ).
cnf(8164,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7949,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7949.0,1282.0,7949.0,1289.0,7949.0,6836.0,7949.0,1114.0,7949.0,1128.0,7949.0,7369.0,7949.0,1142.0,7949.0,1149.0,7949.0')] ).
cnf(8167,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114)))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7951,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7951.0,1282.0,7951.0,1289.0,7951.0,6836.0,7951.0,1114.0,7951.0,1128.0,7951.0,7369.0,7951.0,1142.0,7951.0,1149.0,7951.0')] ).
cnf(8170,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_114))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[159,7953,1282,1289,6836,1114,1128,7369,1142,1149]),
[iquote('0:Rew:159.0,7953.0,1282.0,7953.0,1289.0,7953.0,6836.0,7953.0,1114.0,7953.0,1128.0,7953.0,7369.0,7953.0,1142.0,7953.0,1149.0,7953.0')] ).
cnf(8430,plain,
( equal(tail,head)
| equal(select(q9,tail),index_276) ),
inference(spr,[status(thm),theory(equality)],[2148,1004]),
[iquote('0:SpR:2148.1,1004.0')] ).
cnf(8433,plain,
( equal(tail,head)
| equal(index_276,index_9) ),
inference(rew,[status(thm),theory(equality)],[256,8430]),
[iquote('0:Rew:256.0,8430.1')] ).
cnf(8434,plain,
equal(index_276,index_9),
inference(mrr,[status(thm)],[8433,3]),
[iquote('0:MRR:8433.0,3.0')] ).
cnf(8435,plain,
equal(s(index_273),index_9),
inference(rew,[status(thm),theory(equality)],[8434,228]),
[iquote('0:Rew:8434.0,228.0')] ).
cnf(8963,plain,
( equal(tail,head)
| equal(select(q12,tail),index_24) ),
inference(spr,[status(thm),theory(equality)],[2149,1009]),
[iquote('0:SpR:2149.1,1009.0')] ).
cnf(8966,plain,
( equal(tail,head)
| equal(index_24,index_30) ),
inference(rew,[status(thm),theory(equality)],[233,8963]),
[iquote('0:Rew:233.0,8963.1')] ).
cnf(8967,plain,
equal(index_24,index_30),
inference(mrr,[status(thm)],[8966,3]),
[iquote('0:MRR:8966.0,3.0')] ).
cnf(8968,plain,
equal(s(index_21),index_30),
inference(rew,[status(thm),theory(equality)],[8967,212]),
[iquote('0:Rew:8967.0,212.0')] ).
cnf(9865,plain,
( equal(tail,head)
| equal(select(q6,tail),index_255) ),
inference(spr,[status(thm),theory(equality)],[2150,1007]),
[iquote('0:SpR:2150.1,1007.0')] ).
cnf(9868,plain,
( equal(tail,head)
| equal(index_255,index_261) ),
inference(rew,[status(thm),theory(equality)],[222,9865]),
[iquote('0:Rew:222.0,9865.1')] ).
cnf(9869,plain,
equal(index_255,index_261),
inference(mrr,[status(thm)],[9868,3]),
[iquote('0:MRR:9868.0,3.0')] ).
cnf(9870,plain,
equal(s(index_252),index_261),
inference(rew,[status(thm),theory(equality)],[9869,218]),
[iquote('0:Rew:9869.0,218.0')] ).
cnf(10398,plain,
( equal(tail,head)
| equal(select(q39,tail),index_228) ),
inference(spr,[status(thm),theory(equality)],[2151,1012]),
[iquote('0:SpR:2151.1,1012.0')] ).
cnf(10401,plain,
( equal(tail,head)
| equal(index_228,index_240) ),
inference(rew,[status(thm),theory(equality)],[213,10398]),
[iquote('0:Rew:213.0,10398.1')] ).
cnf(10402,plain,
equal(index_228,index_240),
inference(mrr,[status(thm)],[10401,3]),
[iquote('0:MRR:10401.0,3.0')] ).
cnf(10403,plain,
equal(s(index_225),index_240),
inference(rew,[status(thm),theory(equality)],[10402,207]),
[iquote('0:Rew:10402.0,207.0')] ).
cnf(10931,plain,
( equal(tail,head)
| equal(select(q36,tail),index_207) ),
inference(spr,[status(thm),theory(equality)],[2152,1015]),
[iquote('0:SpR:2152.1,1015.0')] ).
cnf(10934,plain,
( equal(tail,head)
| equal(index_207,index_213) ),
inference(rew,[status(thm),theory(equality)],[202,10931]),
[iquote('0:Rew:202.0,10931.1')] ).
cnf(10935,plain,
equal(index_207,index_213),
inference(mrr,[status(thm)],[10934,3]),
[iquote('0:MRR:10934.0,3.0')] ).
cnf(10936,plain,
equal(s(index_204),index_213),
inference(rew,[status(thm),theory(equality)],[10935,198]),
[iquote('0:Rew:10935.0,198.0')] ).
cnf(11464,plain,
( equal(tail,head)
| equal(select(q33,tail),index_186) ),
inference(spr,[status(thm),theory(equality)],[2153,1019]),
[iquote('0:SpR:2153.1,1019.0')] ).
cnf(11467,plain,
( equal(tail,head)
| equal(index_186,index_192) ),
inference(rew,[status(thm),theory(equality)],[193,11464]),
[iquote('0:Rew:193.0,11464.1')] ).
cnf(11468,plain,
equal(index_186,index_192),
inference(mrr,[status(thm)],[11467,3]),
[iquote('0:MRR:11467.0,3.0')] ).
cnf(11469,plain,
equal(s(index_183),index_192),
inference(rew,[status(thm),theory(equality)],[11468,190]),
[iquote('0:Rew:11468.0,190.0')] ).
cnf(11997,plain,
( equal(tail,head)
| equal(select(q30,tail),index_165) ),
inference(spr,[status(thm),theory(equality)],[2154,1022]),
[iquote('0:SpR:2154.1,1022.0')] ).
cnf(12000,plain,
( equal(tail,head)
| equal(index_165,index_171) ),
inference(rew,[status(thm),theory(equality)],[184,11997]),
[iquote('0:Rew:184.0,11997.1')] ).
cnf(12001,plain,
equal(index_165,index_171),
inference(mrr,[status(thm)],[12000,3]),
[iquote('0:MRR:12000.0,3.0')] ).
cnf(12002,plain,
equal(s(index_162),index_171),
inference(rew,[status(thm),theory(equality)],[12001,181]),
[iquote('0:Rew:12001.0,181.0')] ).
cnf(12530,plain,
( equal(tail,head)
| equal(select(q3,tail),index_156) ),
inference(spr,[status(thm),theory(equality)],[2155,1023]),
[iquote('0:SpR:2155.1,1023.0')] ).
cnf(12533,plain,
( equal(tail,head)
| equal(index_156,index_234) ),
inference(rew,[status(thm),theory(equality)],[210,12530]),
[iquote('0:Rew:210.0,12530.1')] ).
cnf(12534,plain,
equal(index_156,index_234),
inference(mrr,[status(thm)],[12533,3]),
[iquote('0:MRR:12533.0,3.0')] ).
cnf(12535,plain,
equal(s(index_153),index_234),
inference(rew,[status(thm),theory(equality)],[12534,177]),
[iquote('0:Rew:12534.0,177.0')] ).
cnf(13063,plain,
( equal(tail,head)
| equal(select(q27,tail),index_135) ),
inference(spr,[status(thm),theory(equality)],[2156,1026]),
[iquote('0:SpR:2156.1,1026.0')] ).
cnf(13066,plain,
( equal(tail,head)
| equal(index_135,index_141) ),
inference(rew,[status(thm),theory(equality)],[171,13063]),
[iquote('0:Rew:171.0,13063.1')] ).
cnf(13067,plain,
equal(index_135,index_141),
inference(mrr,[status(thm)],[13066,3]),
[iquote('0:MRR:13066.0,3.0')] ).
cnf(13068,plain,
equal(s(index_132),index_141),
inference(rew,[status(thm),theory(equality)],[13067,168]),
[iquote('0:Rew:13067.0,168.0')] ).
cnf(13596,plain,
( equal(tail,head)
| equal(select(q24,tail),index_114) ),
inference(spr,[status(thm),theory(equality)],[2157,1030]),
[iquote('0:SpR:2157.1,1030.0')] ).
cnf(13599,plain,
( equal(tail,head)
| equal(index_114,index_120) ),
inference(rew,[status(thm),theory(equality)],[163,13596]),
[iquote('0:Rew:163.0,13596.1')] ).
cnf(13600,plain,
equal(index_114,index_120),
inference(mrr,[status(thm)],[13599,3]),
[iquote('0:MRR:13599.0,3.0')] ).
cnf(13631,plain,
~ equal(s(s(s(s(s(s(index_120)))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8143]),
[iquote('0:Rew:13600.0,8143.0')] ).
cnf(13652,plain,
~ equal(s(s(s(s(s(index_120))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8140]),
[iquote('0:Rew:13600.0,8140.0')] ).
cnf(13673,plain,
~ equal(s(s(s(s(index_120)))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8137]),
[iquote('0:Rew:13600.0,8137.0')] ).
cnf(13694,plain,
~ equal(s(s(s(index_120))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8134]),
[iquote('0:Rew:13600.0,8134.0')] ).
cnf(13715,plain,
~ equal(s(s(index_120)),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8131]),
[iquote('0:Rew:13600.0,8131.0')] ).
cnf(13736,plain,
~ equal(s(index_120),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8128]),
[iquote('0:Rew:13600.0,8128.0')] ).
cnf(13758,plain,
~ equal(index_36,index_120),
inference(rew,[status(thm),theory(equality)],[13600,8125]),
[iquote('0:Rew:13600.0,8125.0')] ).
cnf(14714,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_120))))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8170]),
[iquote('0:Rew:13600.0,8170.0')] ).
cnf(14737,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_120)))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8167]),
[iquote('0:Rew:13600.0,8167.0')] ).
cnf(14760,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(index_120))))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8164]),
[iquote('0:Rew:13600.0,8164.0')] ).
cnf(14783,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(index_120)))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8161]),
[iquote('0:Rew:13600.0,8161.0')] ).
cnf(14806,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(index_120))))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8158]),
[iquote('0:Rew:13600.0,8158.0')] ).
cnf(14829,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(index_120)))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8155]),
[iquote('0:Rew:13600.0,8155.0')] ).
cnf(14852,plain,
~ equal(s(s(s(s(s(s(s(s(s(index_120))))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8152]),
[iquote('0:Rew:13600.0,8152.0')] ).
cnf(14875,plain,
~ equal(s(s(s(s(s(s(s(s(index_120)))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8149]),
[iquote('0:Rew:13600.0,8149.0')] ).
cnf(14898,plain,
~ equal(s(s(s(s(s(s(s(index_120))))))),index_36),
inference(rew,[status(thm),theory(equality)],[13600,8146]),
[iquote('0:Rew:13600.0,8146.0')] ).
cnf(14922,plain,
~ equal(index_36,index_126),
inference(rew,[status(thm),theory(equality)],[1275,13736]),
[iquote('0:Rew:1275.0,13736.0')] ).
cnf(14946,plain,
~ equal(index_36,index_132),
inference(rew,[status(thm),theory(equality)],[1261,13715,1275]),
[iquote('0:Rew:1261.0,13715.0,1275.0,13715.0')] ).
cnf(14970,plain,
~ equal(index_36,index_141),
inference(rew,[status(thm),theory(equality)],[13068,13694,1261,1275]),
[iquote('0:Rew:13068.0,13694.0,1261.0,13694.0,1275.0,13694.0')] ).
cnf(14994,plain,
~ equal(index_36,index_147),
inference(rew,[status(thm),theory(equality)],[1254,13673,13068,1261,1275]),
[iquote('0:Rew:1254.0,13673.0,13068.0,13673.0,1261.0,13673.0,1275.0,13673.0')] ).
cnf(15018,plain,
~ equal(index_36,index_162),
inference(rew,[status(thm),theory(equality)],[1247,13652,1254,13068,1261,1275]),
[iquote('0:Rew:1247.0,13652.0,1254.0,13652.0,13068.0,13652.0,1261.0,13652.0,1275.0,13652.0')] ).
cnf(15042,plain,
~ equal(index_36,index_171),
inference(rew,[status(thm),theory(equality)],[12002,13631,1247,1254,13068,1261,1275]),
[iquote('0:Rew:12002.0,13631.0,1247.0,13631.0,1254.0,13631.0,13068.0,13631.0,1261.0,13631.0,1275.0,13631.0')] ).
cnf(15066,plain,
~ equal(index_36,index_177),
inference(rew,[status(thm),theory(equality)],[1240,14898,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:1240.0,14898.0,12002.0,14898.0,1247.0,14898.0,1254.0,14898.0,13068.0,14898.0,1261.0,14898.0,1275.0,14898.0')] ).
cnf(15090,plain,
~ equal(index_36,index_183),
inference(rew,[status(thm),theory(equality)],[1233,14875,1240,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:1233.0,14875.0,1240.0,14875.0,12002.0,14875.0,1247.0,14875.0,1254.0,14875.0,13068.0,14875.0,1261.0,14875.0,1275.0,14875.0')] ).
cnf(15114,plain,
~ equal(index_36,index_192),
inference(rew,[status(thm),theory(equality)],[11469,14852,1233,1240,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:11469.0,14852.0,1233.0,14852.0,1240.0,14852.0,12002.0,14852.0,1247.0,14852.0,1254.0,14852.0,13068.0,14852.0,1261.0,14852.0,1275.0,14852.0')] ).
cnf(15138,plain,
~ equal(index_36,index_198),
inference(rew,[status(thm),theory(equality)],[1219,14829,11469,1233,1240,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:1219.0,14829.0,11469.0,14829.0,1233.0,14829.0,1240.0,14829.0,12002.0,14829.0,1247.0,14829.0,1254.0,14829.0,13068.0,14829.0,1261.0,14829.0,1275.0,14829.0')] ).
cnf(15162,plain,
~ equal(index_36,index_204),
inference(rew,[status(thm),theory(equality)],[1212,14806,1219,11469,1233,1240,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:1212.0,14806.0,1219.0,14806.0,11469.0,14806.0,1233.0,14806.0,1240.0,14806.0,12002.0,14806.0,1247.0,14806.0,1254.0,14806.0,13068.0,14806.0,1261.0,14806.0,1275.0,14806.0')] ).
cnf(15186,plain,
~ equal(index_36,index_213),
inference(rew,[status(thm),theory(equality)],[10936,14783,1212,1219,11469,1233,1240,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:10936.0,14783.0,1212.0,14783.0,1219.0,14783.0,11469.0,14783.0,1233.0,14783.0,1240.0,14783.0,12002.0,14783.0,1247.0,14783.0,1254.0,14783.0,13068.0,14783.0,1261.0,14783.0,1275.0,14783.0')] ).
cnf(15210,plain,
~ equal(index_36,index_219),
inference(rew,[status(thm),theory(equality)],[1205,14760,10936,1212,1219,11469,1233,1240,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:1205.0,14760.0,10936.0,14760.0,1212.0,14760.0,1219.0,14760.0,11469.0,14760.0,1233.0,14760.0,1240.0,14760.0,12002.0,14760.0,1247.0,14760.0,1254.0,14760.0,13068.0,14760.0,1261.0,14760.0,1275.0,14760.0')] ).
cnf(15234,plain,
~ equal(index_36,index_225),
inference(rew,[status(thm),theory(equality)],[1198,14737,1205,10936,1212,1219,11469,1233,1240,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:1198.0,14737.0,1205.0,14737.0,10936.0,14737.0,1212.0,14737.0,1219.0,14737.0,11469.0,14737.0,1233.0,14737.0,1240.0,14737.0,12002.0,14737.0,1247.0,14737.0,1254.0,14737.0,13068.0,14737.0,1261.0,14737.0,1275.0,14737.0')] ).
cnf(15258,plain,
~ equal(index_36,index_240),
inference(rew,[status(thm),theory(equality)],[10403,14714,1198,1205,10936,1212,1219,11469,1233,1240,12002,1247,1254,13068,1261,1275]),
[iquote('0:Rew:10403.0,14714.0,1198.0,14714.0,1205.0,14714.0,10936.0,14714.0,1212.0,14714.0,1219.0,14714.0,11469.0,14714.0,1233.0,14714.0,1240.0,14714.0,12002.0,14714.0,1247.0,14714.0,1254.0,14714.0,13068.0,14714.0,1261.0,14714.0,1275.0,14714.0')] ).
cnf(16334,plain,
( equal(tail,head)
| equal(select(q0,tail),index_0) ),
inference(spr,[status(thm),theory(equality)],[2158,154]),
[iquote('0:SpR:2158.1,154.0')] ).
cnf(16336,plain,
( equal(tail,head)
| equal(index_0,index_3) ),
inference(rew,[status(thm),theory(equality)],[232,16334]),
[iquote('0:Rew:232.0,16334.1')] ).
cnf(16337,plain,
equal(index_0,index_3),
inference(mrr,[status(thm)],[16336,3]),
[iquote('0:MRR:16336.0,3.0')] ).
cnf(16340,plain,
equal(select(q0,head),index_3),
inference(rew,[status(thm),theory(equality)],[16337,992]),
[iquote('0:Rew:16337.0,992.0')] ).
cnf(16348,plain,
( equal(seq,tail)
| equal(select(queue_94,seq),earray_91) ),
inference(spr,[status(thm),theory(equality)],[2159,1033]),
[iquote('0:SpR:2159.1,1033.0')] ).
cnf(16350,plain,
equal(select(queue_94,seq),earray_91),
inference(mrr,[status(thm)],[16348,5]),
[iquote('0:MRR:16348.0,5.0')] ).
cnf(16352,plain,
( equal(seq,head)
| equal(select(q21,seq),earray_91) ),
inference(spr,[status(thm),theory(equality)],[16350,2145]),
[iquote('0:SpR:16350.0,2145.1')] ).
cnf(16353,plain,
( equal(seq,head)
| equal(earray_91,earray_98) ),
inference(rew,[status(thm),theory(equality)],[152,16352]),
[iquote('0:Rew:152.0,16352.1')] ).
cnf(16354,plain,
equal(earray_91,earray_98),
inference(mrr,[status(thm)],[16353,4]),
[iquote('0:MRR:16353.0,4.0')] ).
cnf(16360,plain,
( equal(index_90,u)
| equal(select(earray_89,u),select(earray_98,u)) ),
inference(rew,[status(thm),theory(equality)],[16354,2239]),
[iquote('0:Rew:16354.0,2239.1')] ).
cnf(16373,plain,
( equal(seq,tail)
| equal(select(queue_67,seq),earray_64) ),
inference(spr,[status(thm),theory(equality)],[2160,1037]),
[iquote('0:SpR:2160.1,1037.0')] ).
cnf(16375,plain,
equal(select(queue_67,seq),earray_64),
inference(mrr,[status(thm)],[16373,5]),
[iquote('0:MRR:16373.0,5.0')] ).
cnf(16377,plain,
( equal(seq,head)
| equal(select(q18,seq),earray_64) ),
inference(spr,[status(thm),theory(equality)],[16375,2146]),
[iquote('0:SpR:16375.0,2146.1')] ).
cnf(16378,plain,
( equal(seq,head)
| equal(earray_71,earray_64) ),
inference(rew,[status(thm),theory(equality)],[143,16377]),
[iquote('0:Rew:143.0,16377.1')] ).
cnf(16379,plain,
equal(earray_71,earray_64),
inference(mrr,[status(thm)],[16378,4]),
[iquote('0:MRR:16378.0,4.0')] ).
cnf(16382,plain,
( equal(index_72,u)
| equal(select(earray_73,u),select(earray_64,u)) ),
inference(rew,[status(thm),theory(equality)],[16379,2242]),
[iquote('0:Rew:16379.0,2242.1')] ).
cnf(16388,plain,
( equal(seq,tail)
| equal(select(queue_46,seq),earray_43) ),
inference(spr,[status(thm),theory(equality)],[2161,1041]),
[iquote('0:SpR:2161.1,1041.0')] ).
cnf(16390,plain,
equal(select(queue_46,seq),earray_43),
inference(mrr,[status(thm)],[16388,5]),
[iquote('0:MRR:16388.0,5.0')] ).
cnf(16392,plain,
( equal(seq,head)
| equal(select(q15,seq),earray_43) ),
inference(spr,[status(thm),theory(equality)],[16390,2147]),
[iquote('0:SpR:16390.0,2147.1')] ).
cnf(16393,plain,
( equal(seq,head)
| equal(earray_50,earray_43) ),
inference(rew,[status(thm),theory(equality)],[137,16392]),
[iquote('0:Rew:137.0,16392.1')] ).
cnf(16394,plain,
equal(earray_50,earray_43),
inference(mrr,[status(thm)],[16393,4]),
[iquote('0:MRR:16393.0,4.0')] ).
cnf(16397,plain,
( equal(index_51,u)
| equal(select(earray_52,u),select(earray_43,u)) ),
inference(rew,[status(thm),theory(equality)],[16394,2245]),
[iquote('0:Rew:16394.0,2245.1')] ).
cnf(16458,plain,
( equal(seq,tail)
| equal(select(q40,seq),earray_241) ),
inference(spr,[status(thm),theory(equality)],[2165,1049]),
[iquote('0:SpR:2165.1,1049.0')] ).
cnf(16460,plain,
( equal(seq,tail)
| equal(earray_281,earray_241) ),
inference(rew,[status(thm),theory(equality)],[129,16458]),
[iquote('0:Rew:129.0,16458.1')] ).
cnf(16461,plain,
equal(earray_281,earray_241),
inference(mrr,[status(thm)],[16460,5]),
[iquote('0:MRR:16460.0,5.0')] ).
cnf(16462,plain,
equal(select(earray_241,index_282),elem_283),
inference(rew,[status(thm),theory(equality)],[16461,153]),
[iquote('0:Rew:16461.0,153.0')] ).
cnf(16467,plain,
( equal(seq,tail)
| equal(select(queue_229,seq),earray_226) ),
inference(spr,[status(thm),theory(equality)],[2166,1052]),
[iquote('0:SpR:2166.1,1052.0')] ).
cnf(16469,plain,
equal(select(queue_229,seq),earray_226),
inference(mrr,[status(thm)],[16467,5]),
[iquote('0:MRR:16467.0,5.0')] ).
cnf(16471,plain,
( equal(seq,head)
| equal(select(q39,seq),earray_226) ),
inference(spr,[status(thm),theory(equality)],[16469,2151]),
[iquote('0:SpR:16469.0,2151.1')] ).
cnf(16472,plain,
( equal(seq,head)
| equal(earray_239,earray_226) ),
inference(rew,[status(thm),theory(equality)],[117,16471]),
[iquote('0:Rew:117.0,16471.1')] ).
cnf(16473,plain,
equal(earray_239,earray_226),
inference(mrr,[status(thm)],[16472,4]),
[iquote('0:MRR:16472.0,4.0')] ).
cnf(16476,plain,
( equal(index_240,u)
| equal(select(earray_241,u),select(earray_226,u)) ),
inference(rew,[status(thm),theory(equality)],[16473,2255]),
[iquote('0:Rew:16473.0,2255.1')] ).
cnf(16482,plain,
( equal(seq,tail)
| equal(select(queue_208,seq),earray_205) ),
inference(spr,[status(thm),theory(equality)],[2167,1055]),
[iquote('0:SpR:2167.1,1055.0')] ).
cnf(16484,plain,
equal(select(queue_208,seq),earray_205),
inference(mrr,[status(thm)],[16482,5]),
[iquote('0:MRR:16482.0,5.0')] ).
cnf(16486,plain,
( equal(seq,head)
| equal(select(q36,seq),earray_205) ),
inference(spr,[status(thm),theory(equality)],[16484,2152]),
[iquote('0:SpR:16484.0,2152.1')] ).
cnf(16487,plain,
( equal(seq,head)
| equal(earray_212,earray_205) ),
inference(rew,[status(thm),theory(equality)],[108,16486]),
[iquote('0:Rew:108.0,16486.1')] ).
cnf(16488,plain,
equal(earray_212,earray_205),
inference(mrr,[status(thm)],[16487,4]),
[iquote('0:MRR:16487.0,4.0')] ).
cnf(16491,plain,
( equal(index_213,u)
| equal(select(earray_214,u),select(earray_205,u)) ),
inference(rew,[status(thm),theory(equality)],[16488,2260]),
[iquote('0:Rew:16488.0,2260.1')] ).
cnf(16497,plain,
( equal(seq,tail)
| equal(select(queue_187,seq),earray_184) ),
inference(spr,[status(thm),theory(equality)],[2168,1058]),
[iquote('0:SpR:2168.1,1058.0')] ).
cnf(16499,plain,
equal(select(queue_187,seq),earray_184),
inference(mrr,[status(thm)],[16497,5]),
[iquote('0:MRR:16497.0,5.0')] ).
cnf(16501,plain,
( equal(seq,head)
| equal(select(q33,seq),earray_184) ),
inference(spr,[status(thm),theory(equality)],[16499,2153]),
[iquote('0:SpR:16499.0,2153.1')] ).
cnf(16502,plain,
( equal(seq,head)
| equal(earray_191,earray_184) ),
inference(rew,[status(thm),theory(equality)],[100,16501]),
[iquote('0:Rew:100.0,16501.1')] ).
cnf(16503,plain,
equal(earray_191,earray_184),
inference(mrr,[status(thm)],[16502,4]),
[iquote('0:MRR:16502.0,4.0')] ).
cnf(16506,plain,
( equal(index_192,u)
| equal(select(earray_193,u),select(earray_184,u)) ),
inference(rew,[status(thm),theory(equality)],[16503,2263]),
[iquote('0:Rew:16503.0,2263.1')] ).
cnf(16512,plain,
( equal(seq,tail)
| equal(select(queue_166,seq),earray_163) ),
inference(spr,[status(thm),theory(equality)],[2169,1062]),
[iquote('0:SpR:2169.1,1062.0')] ).
cnf(16514,plain,
equal(select(queue_166,seq),earray_163),
inference(mrr,[status(thm)],[16512,5]),
[iquote('0:MRR:16512.0,5.0')] ).
cnf(16516,plain,
( equal(seq,head)
| equal(select(q30,seq),earray_163) ),
inference(spr,[status(thm),theory(equality)],[16514,2154]),
[iquote('0:SpR:16514.0,2154.1')] ).
cnf(16517,plain,
( equal(seq,head)
| equal(earray_170,earray_163) ),
inference(rew,[status(thm),theory(equality)],[94,16516]),
[iquote('0:Rew:94.0,16516.1')] ).
cnf(16518,plain,
equal(earray_170,earray_163),
inference(mrr,[status(thm)],[16517,4]),
[iquote('0:MRR:16517.0,4.0')] ).
cnf(16521,plain,
( equal(index_171,u)
| equal(select(earray_172,u),select(earray_163,u)) ),
inference(rew,[status(thm),theory(equality)],[16518,2266]),
[iquote('0:Rew:16518.0,2266.1')] ).
cnf(16542,plain,
( equal(seq,tail)
| equal(select(queue_136,seq),earray_133) ),
inference(spr,[status(thm),theory(equality)],[2171,1066]),
[iquote('0:SpR:2171.1,1066.0')] ).
cnf(16544,plain,
equal(select(queue_136,seq),earray_133),
inference(mrr,[status(thm)],[16542,5]),
[iquote('0:MRR:16542.0,5.0')] ).
cnf(16546,plain,
( equal(seq,head)
| equal(select(q27,seq),earray_133) ),
inference(spr,[status(thm),theory(equality)],[16544,2156]),
[iquote('0:SpR:16544.0,2156.1')] ).
cnf(16547,plain,
( equal(seq,head)
| equal(earray_140,earray_133) ),
inference(rew,[status(thm),theory(equality)],[85,16546]),
[iquote('0:Rew:85.0,16546.1')] ).
cnf(16548,plain,
equal(earray_140,earray_133),
inference(mrr,[status(thm)],[16547,4]),
[iquote('0:MRR:16547.0,4.0')] ).
cnf(16551,plain,
( equal(index_141,u)
| equal(select(earray_142,u),select(earray_133,u)) ),
inference(rew,[status(thm),theory(equality)],[16548,2271]),
[iquote('0:Rew:16548.0,2271.1')] ).
cnf(16557,plain,
( equal(seq,tail)
| equal(select(queue_115,seq),earray_112) ),
inference(spr,[status(thm),theory(equality)],[2172,1069]),
[iquote('0:SpR:2172.1,1069.0')] ).
cnf(16559,plain,
equal(select(queue_115,seq),earray_112),
inference(mrr,[status(thm)],[16557,5]),
[iquote('0:MRR:16557.0,5.0')] ).
cnf(16561,plain,
( equal(seq,head)
| equal(select(q24,seq),earray_112) ),
inference(spr,[status(thm),theory(equality)],[16559,2157]),
[iquote('0:SpR:16559.0,2157.1')] ).
cnf(16562,plain,
( equal(seq,head)
| equal(earray_119,earray_112) ),
inference(rew,[status(thm),theory(equality)],[78,16561]),
[iquote('0:Rew:78.0,16561.1')] ).
cnf(16563,plain,
equal(earray_119,earray_112),
inference(mrr,[status(thm)],[16562,4]),
[iquote('0:MRR:16562.0,4.0')] ).
cnf(16566,plain,
( equal(index_120,u)
| equal(select(earray_121,u),select(earray_112,u)) ),
inference(rew,[status(thm),theory(equality)],[16563,2274]),
[iquote('0:Rew:16563.0,2274.1')] ).
cnf(16572,plain,
( equal(seq,tail)
| equal(select(q20,seq),earray_85) ),
inference(spr,[status(thm),theory(equality)],[2173,1034]),
[iquote('0:SpR:2173.1,1034.0')] ).
cnf(16574,plain,
( equal(seq,tail)
| equal(earray_89,earray_85) ),
inference(rew,[status(thm),theory(equality)],[150,16572]),
[iquote('0:Rew:150.0,16572.1')] ).
cnf(16575,plain,
equal(earray_89,earray_85),
inference(mrr,[status(thm)],[16574,5]),
[iquote('0:MRR:16574.0,5.0')] ).
cnf(16578,plain,
( equal(index_90,u)
| equal(select(earray_85,u),select(earray_98,u)) ),
inference(rew,[status(thm),theory(equality)],[16575,16360]),
[iquote('0:Rew:16575.0,16360.1')] ).
cnf(16603,plain,
( equal(seq,tail)
| equal(select(q19,seq),earray_73) ),
inference(spr,[status(thm),theory(equality)],[2175,1036]),
[iquote('0:SpR:2175.1,1036.0')] ).
cnf(16605,plain,
( equal(seq,tail)
| equal(earray_83,earray_73) ),
inference(rew,[status(thm),theory(equality)],[148,16603]),
[iquote('0:Rew:148.0,16603.1')] ).
cnf(16606,plain,
equal(earray_83,earray_73),
inference(mrr,[status(thm)],[16605,5]),
[iquote('0:MRR:16605.0,5.0')] ).
cnf(16609,plain,
( equal(index_84,u)
| equal(select(earray_85,u),select(earray_73,u)) ),
inference(rew,[status(thm),theory(equality)],[16606,2240]),
[iquote('0:Rew:16606.0,2240.1')] ).
cnf(16627,plain,
( equal(seq,tail)
| equal(select(q17,seq),earray_58) ),
inference(spr,[status(thm),theory(equality)],[2177,1038]),
[iquote('0:SpR:2177.1,1038.0')] ).
cnf(16629,plain,
( equal(seq,tail)
| equal(earray_62,earray_58) ),
inference(rew,[status(thm),theory(equality)],[141,16627]),
[iquote('0:Rew:141.0,16627.1')] ).
cnf(16630,plain,
equal(earray_62,earray_58),
inference(mrr,[status(thm)],[16629,5]),
[iquote('0:MRR:16629.0,5.0')] ).
cnf(16633,plain,
( equal(index_63,u)
| equal(select(earray_64,u),select(earray_58,u)) ),
inference(rew,[status(thm),theory(equality)],[16630,2243]),
[iquote('0:Rew:16630.0,2243.1')] ).
cnf(16639,plain,
( equal(seq,tail)
| equal(select(q16,seq),earray_52) ),
inference(spr,[status(thm),theory(equality)],[2178,1039]),
[iquote('0:SpR:2178.1,1039.0')] ).
cnf(16641,plain,
( equal(seq,tail)
| equal(earray_56,earray_52) ),
inference(rew,[status(thm),theory(equality)],[139,16639]),
[iquote('0:Rew:139.0,16639.1')] ).
cnf(16642,plain,
equal(earray_56,earray_52),
inference(mrr,[status(thm)],[16641,5]),
[iquote('0:MRR:16641.0,5.0')] ).
cnf(16645,plain,
( equal(index_57,u)
| equal(select(earray_58,u),select(earray_52,u)) ),
inference(rew,[status(thm),theory(equality)],[16642,2244]),
[iquote('0:Rew:16642.0,2244.1')] ).
cnf(16651,plain,
( equal(seq,tail)
| equal(select(q14,seq),earray_37) ),
inference(spr,[status(thm),theory(equality)],[2179,1042]),
[iquote('0:SpR:2179.1,1042.0')] ).
cnf(16653,plain,
( equal(seq,tail)
| equal(earray_41,earray_37) ),
inference(rew,[status(thm),theory(equality)],[135,16651]),
[iquote('0:Rew:135.0,16651.1')] ).
cnf(16654,plain,
equal(earray_41,earray_37),
inference(mrr,[status(thm)],[16653,5]),
[iquote('0:MRR:16653.0,5.0')] ).
cnf(16657,plain,
( equal(index_42,u)
| equal(select(earray_43,u),select(earray_37,u)) ),
inference(rew,[status(thm),theory(equality)],[16654,2246]),
[iquote('0:Rew:16654.0,2246.1')] ).
cnf(16723,plain,
( equal(seq,tail)
| equal(select(q38,seq),earray_220) ),
inference(spr,[status(thm),theory(equality)],[2185,1053]),
[iquote('0:SpR:2185.1,1053.0')] ).
cnf(16725,plain,
( equal(seq,tail)
| equal(earray_224,earray_220) ),
inference(rew,[status(thm),theory(equality)],[113,16723]),
[iquote('0:Rew:113.0,16723.1')] ).
cnf(16726,plain,
equal(earray_224,earray_220),
inference(mrr,[status(thm)],[16725,5]),
[iquote('0:MRR:16725.0,5.0')] ).
cnf(16729,plain,
( equal(index_225,u)
| equal(select(earray_226,u),select(earray_220,u)) ),
inference(rew,[status(thm),theory(equality)],[16726,2257]),
[iquote('0:Rew:16726.0,2257.1')] ).
cnf(16735,plain,
( equal(seq,tail)
| equal(select(q37,seq),earray_214) ),
inference(spr,[status(thm),theory(equality)],[2186,1054]),
[iquote('0:SpR:2186.1,1054.0')] ).
cnf(16737,plain,
( equal(seq,tail)
| equal(earray_218,earray_214) ),
inference(rew,[status(thm),theory(equality)],[110,16735]),
[iquote('0:Rew:110.0,16735.1')] ).
cnf(16738,plain,
equal(earray_218,earray_214),
inference(mrr,[status(thm)],[16737,5]),
[iquote('0:MRR:16737.0,5.0')] ).
cnf(16741,plain,
( equal(index_219,u)
| equal(select(earray_220,u),select(earray_214,u)) ),
inference(rew,[status(thm),theory(equality)],[16738,2258]),
[iquote('0:Rew:16738.0,2258.1')] ).
cnf(16747,plain,
( equal(seq,tail)
| equal(select(q35,seq),earray_199) ),
inference(spr,[status(thm),theory(equality)],[2187,1056]),
[iquote('0:SpR:2187.1,1056.0')] ).
cnf(16749,plain,
( equal(seq,tail)
| equal(earray_203,earray_199) ),
inference(rew,[status(thm),theory(equality)],[106,16747]),
[iquote('0:Rew:106.0,16747.1')] ).
cnf(16750,plain,
equal(earray_203,earray_199),
inference(mrr,[status(thm)],[16749,5]),
[iquote('0:MRR:16749.0,5.0')] ).
cnf(16753,plain,
( equal(index_204,u)
| equal(select(earray_205,u),select(earray_199,u)) ),
inference(rew,[status(thm),theory(equality)],[16750,2261]),
[iquote('0:Rew:16750.0,2261.1')] ).
cnf(16759,plain,
( equal(seq,tail)
| equal(select(q34,seq),earray_193) ),
inference(spr,[status(thm),theory(equality)],[2188,1057]),
[iquote('0:SpR:2188.1,1057.0')] ).
cnf(16761,plain,
( equal(seq,tail)
| equal(earray_197,earray_193) ),
inference(rew,[status(thm),theory(equality)],[102,16759]),
[iquote('0:Rew:102.0,16759.1')] ).
cnf(16762,plain,
equal(earray_197,earray_193),
inference(mrr,[status(thm)],[16761,5]),
[iquote('0:MRR:16761.0,5.0')] ).
cnf(16765,plain,
( equal(index_198,u)
| equal(select(earray_199,u),select(earray_193,u)) ),
inference(rew,[status(thm),theory(equality)],[16762,2262]),
[iquote('0:Rew:16762.0,2262.1')] ).
cnf(16783,plain,
( equal(seq,tail)
| equal(select(q32,seq),earray_178) ),
inference(spr,[status(thm),theory(equality)],[2190,1059]),
[iquote('0:SpR:2190.1,1059.0')] ).
cnf(16785,plain,
( equal(seq,tail)
| equal(earray_182,earray_178) ),
inference(rew,[status(thm),theory(equality)],[98,16783]),
[iquote('0:Rew:98.0,16783.1')] ).
cnf(16786,plain,
equal(earray_182,earray_178),
inference(mrr,[status(thm)],[16785,5]),
[iquote('0:MRR:16785.0,5.0')] ).
cnf(16789,plain,
( equal(index_183,u)
| equal(select(earray_184,u),select(earray_178,u)) ),
inference(rew,[status(thm),theory(equality)],[16786,2264]),
[iquote('0:Rew:16786.0,2264.1')] ).
cnf(16795,plain,
( equal(seq,tail)
| equal(select(q31,seq),earray_172) ),
inference(spr,[status(thm),theory(equality)],[2191,1060]),
[iquote('0:SpR:2191.1,1060.0')] ).
cnf(16797,plain,
( equal(seq,tail)
| equal(earray_176,earray_172) ),
inference(rew,[status(thm),theory(equality)],[96,16795]),
[iquote('0:Rew:96.0,16795.1')] ).
cnf(16798,plain,
equal(earray_176,earray_172),
inference(mrr,[status(thm)],[16797,5]),
[iquote('0:MRR:16797.0,5.0')] ).
cnf(16801,plain,
( equal(index_177,u)
| equal(select(earray_178,u),select(earray_172,u)) ),
inference(rew,[status(thm),theory(equality)],[16798,2265]),
[iquote('0:Rew:16798.0,2265.1')] ).
cnf(16807,plain,
( equal(seq,tail)
| equal(select(q29,seq),earray_148) ),
inference(spr,[status(thm),theory(equality)],[2192,1064]),
[iquote('0:SpR:2192.1,1064.0')] ).
cnf(16809,plain,
( equal(seq,tail)
| equal(earray_161,earray_148) ),
inference(rew,[status(thm),theory(equality)],[92,16807]),
[iquote('0:Rew:92.0,16807.1')] ).
cnf(16810,plain,
equal(earray_161,earray_148),
inference(mrr,[status(thm)],[16809,5]),
[iquote('0:MRR:16809.0,5.0')] ).
cnf(16813,plain,
( equal(index_162,u)
| equal(select(earray_163,u),select(earray_148,u)) ),
inference(rew,[status(thm),theory(equality)],[16810,2267]),
[iquote('0:Rew:16810.0,2267.1')] ).
cnf(16819,plain,
( equal(seq,tail)
| equal(select(q28,seq),earray_142) ),
inference(spr,[status(thm),theory(equality)],[2193,1065]),
[iquote('0:SpR:2193.1,1065.0')] ).
cnf(16821,plain,
( equal(seq,tail)
| equal(earray_146,earray_142) ),
inference(rew,[status(thm),theory(equality)],[87,16819]),
[iquote('0:Rew:87.0,16819.1')] ).
cnf(16822,plain,
equal(earray_146,earray_142),
inference(mrr,[status(thm)],[16821,5]),
[iquote('0:MRR:16821.0,5.0')] ).
cnf(16825,plain,
( equal(index_147,u)
| equal(select(earray_148,u),select(earray_142,u)) ),
inference(rew,[status(thm),theory(equality)],[16822,2270]),
[iquote('0:Rew:16822.0,2270.1')] ).
cnf(16831,plain,
( equal(seq,tail)
| equal(select(q26,seq),earray_127) ),
inference(spr,[status(thm),theory(equality)],[2194,1067]),
[iquote('0:SpR:2194.1,1067.0')] ).
cnf(16833,plain,
( equal(seq,tail)
| equal(earray_131,earray_127) ),
inference(rew,[status(thm),theory(equality)],[82,16831]),
[iquote('0:Rew:82.0,16831.1')] ).
cnf(16834,plain,
equal(earray_131,earray_127),
inference(mrr,[status(thm)],[16833,5]),
[iquote('0:MRR:16833.0,5.0')] ).
cnf(16837,plain,
( equal(index_132,u)
| equal(select(earray_133,u),select(earray_127,u)) ),
inference(rew,[status(thm),theory(equality)],[16834,2272]),
[iquote('0:Rew:16834.0,2272.1')] ).
cnf(16855,plain,
( equal(seq,tail)
| equal(select(q25,seq),earray_121) ),
inference(spr,[status(thm),theory(equality)],[2196,1068]),
[iquote('0:SpR:2196.1,1068.0')] ).
cnf(16857,plain,
( equal(seq,tail)
| equal(earray_125,earray_121) ),
inference(rew,[status(thm),theory(equality)],[80,16855]),
[iquote('0:Rew:80.0,16855.1')] ).
cnf(16858,plain,
equal(earray_125,earray_121),
inference(mrr,[status(thm)],[16857,5]),
[iquote('0:MRR:16857.0,5.0')] ).
cnf(16861,plain,
( equal(index_126,u)
| equal(select(earray_127,u),select(earray_121,u)) ),
inference(rew,[status(thm),theory(equality)],[16858,2273]),
[iquote('0:Rew:16858.0,2273.1')] ).
cnf(16867,plain,
( equal(seq,tail)
| equal(select(q23,seq),earray_106) ),
inference(spr,[status(thm),theory(equality)],[2197,1071]),
[iquote('0:SpR:2197.1,1071.0')] ).
cnf(16869,plain,
( equal(seq,tail)
| equal(earray_110,earray_106) ),
inference(rew,[status(thm),theory(equality)],[76,16867]),
[iquote('0:Rew:76.0,16867.1')] ).
cnf(16870,plain,
equal(earray_110,earray_106),
inference(mrr,[status(thm)],[16869,5]),
[iquote('0:MRR:16869.0,5.0')] ).
cnf(16873,plain,
( equal(index_111,u)
| equal(select(earray_112,u),select(earray_106,u)) ),
inference(rew,[status(thm),theory(equality)],[16870,2275]),
[iquote('0:Rew:16870.0,2275.1')] ).
cnf(16879,plain,
( equal(seq,tail)
| equal(select(q22,seq),earray_100) ),
inference(spr,[status(thm),theory(equality)],[2198,1072]),
[iquote('0:SpR:2198.1,1072.0')] ).
cnf(16881,plain,
( equal(seq,tail)
| equal(earray_104,earray_100) ),
inference(rew,[status(thm),theory(equality)],[74,16879]),
[iquote('0:Rew:74.0,16879.1')] ).
cnf(16882,plain,
equal(earray_104,earray_100),
inference(mrr,[status(thm)],[16881,5]),
[iquote('0:MRR:16881.0,5.0')] ).
cnf(16885,plain,
( equal(index_105,u)
| equal(select(earray_106,u),select(earray_100,u)) ),
inference(rew,[status(thm),theory(equality)],[16882,2276]),
[iquote('0:Rew:16882.0,2276.1')] ).
cnf(16892,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_94,u),select(q20,u)) ),
inference(spr,[status(thm),theory(equality)],[2199,2159]),
[iquote('0:SpR:2199.1,2159.1')] ).
cnf(16895,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q20,u),select(q19,u)) ),
inference(spr,[status(thm),theory(equality)],[2200,2173]),
[iquote('0:SpR:2200.1,2173.1')] ).
cnf(16897,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_94,u),select(q19,u)) ),
inference(rew,[status(thm),theory(equality)],[16895,16892]),
[iquote('0:Rew:16895.2,16892.2')] ).
cnf(16899,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q1,u),select(q2,u)) ),
inference(spr,[status(thm),theory(equality)],[2201,2174]),
[iquote('0:SpR:2201.1,2174.1')] ).
cnf(16902,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q19,u),select(q18,u)) ),
inference(spr,[status(thm),theory(equality)],[2202,2175]),
[iquote('0:SpR:2202.1,2175.1')] ).
cnf(16905,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_94,u),select(q18,u)) ),
inference(rew,[status(thm),theory(equality)],[16902,16897]),
[iquote('0:Rew:16902.2,16897.2')] ).
cnf(16907,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_67,u),select(q17,u)) ),
inference(spr,[status(thm),theory(equality)],[2203,2160]),
[iquote('0:SpR:2203.1,2160.1')] ).
cnf(16910,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q17,u),select(q16,u)) ),
inference(spr,[status(thm),theory(equality)],[2204,2177]),
[iquote('0:SpR:2204.1,2177.1')] ).
cnf(16912,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_67,u),select(q16,u)) ),
inference(rew,[status(thm),theory(equality)],[16910,16907]),
[iquote('0:Rew:16910.2,16907.2')] ).
cnf(16914,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q16,u),select(q15,u)) ),
inference(spr,[status(thm),theory(equality)],[2205,2178]),
[iquote('0:SpR:2205.1,2178.1')] ).
cnf(16917,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_67,u),select(q15,u)) ),
inference(rew,[status(thm),theory(equality)],[16914,16912]),
[iquote('0:Rew:16914.2,16912.2')] ).
cnf(16919,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q1,u),select(q0,u)) ),
inference(spr,[status(thm),theory(equality)],[2206,2176]),
[iquote('0:SpR:2206.1,2176.1')] ).
cnf(16921,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q0,u),select(q2,u)) ),
inference(rew,[status(thm),theory(equality)],[16899,16919]),
[iquote('0:Rew:16899.2,16919.2')] ).
cnf(16923,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_46,u),select(q14,u)) ),
inference(spr,[status(thm),theory(equality)],[2207,2161]),
[iquote('0:SpR:2207.1,2161.1')] ).
cnf(16926,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q14,u),select(q13,u)) ),
inference(spr,[status(thm),theory(equality)],[2208,2179]),
[iquote('0:SpR:2208.1,2179.1')] ).
cnf(16928,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_46,u),select(q13,u)) ),
inference(rew,[status(thm),theory(equality)],[16926,16923]),
[iquote('0:Rew:16926.2,16923.2')] ).
cnf(16930,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q13,u),select(q12,u)) ),
inference(spr,[status(thm),theory(equality)],[2209,2180]),
[iquote('0:SpR:2209.1,2180.1')] ).
cnf(16933,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_46,u),select(q12,u)) ),
inference(rew,[status(thm),theory(equality)],[16930,16928]),
[iquote('0:Rew:16930.2,16928.2')] ).
cnf(16935,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_277,u),select(q8,u)) ),
inference(spr,[status(thm),theory(equality)],[2210,2162]),
[iquote('0:SpR:2210.1,2162.1')] ).
cnf(16938,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q8,u),select(q7,u)) ),
inference(spr,[status(thm),theory(equality)],[2211,2181]),
[iquote('0:SpR:2211.1,2181.1')] ).
cnf(16940,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_277,u),select(q7,u)) ),
inference(rew,[status(thm),theory(equality)],[16938,16935]),
[iquote('0:Rew:16938.2,16935.2')] ).
cnf(16942,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q7,u),select(q6,u)) ),
inference(spr,[status(thm),theory(equality)],[2212,2182]),
[iquote('0:SpR:2212.1,2182.1')] ).
cnf(16945,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_277,u),select(q6,u)) ),
inference(rew,[status(thm),theory(equality)],[16942,16940]),
[iquote('0:Rew:16942.2,16940.2')] ).
cnf(16947,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_256,u),select(q5,u)) ),
inference(spr,[status(thm),theory(equality)],[2213,2163]),
[iquote('0:SpR:2213.1,2163.1')] ).
cnf(16950,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q5,u),select(q4,u)) ),
inference(spr,[status(thm),theory(equality)],[2214,2183]),
[iquote('0:SpR:2214.1,2183.1')] ).
cnf(16952,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_256,u),select(q4,u)) ),
inference(rew,[status(thm),theory(equality)],[16950,16947]),
[iquote('0:Rew:16950.2,16947.2')] ).
cnf(16954,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q40,u),select(q39,u)) ),
inference(spr,[status(thm),theory(equality)],[2215,2165]),
[iquote('0:SpR:2215.1,2165.1')] ).
cnf(16957,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q4,u),select(q3,u)) ),
inference(spr,[status(thm),theory(equality)],[2216,2184]),
[iquote('0:SpR:2216.1,2184.1')] ).
cnf(16960,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_256,u),select(q3,u)) ),
inference(rew,[status(thm),theory(equality)],[16957,16952]),
[iquote('0:Rew:16957.2,16952.2')] ).
cnf(16962,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_25,u),select(q11,u)) ),
inference(spr,[status(thm),theory(equality)],[2217,2164]),
[iquote('0:SpR:2217.1,2164.1')] ).
cnf(16965,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_229,u),select(q38,u)) ),
inference(spr,[status(thm),theory(equality)],[2218,2166]),
[iquote('0:SpR:2218.1,2166.1')] ).
cnf(16968,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q38,u),select(q37,u)) ),
inference(spr,[status(thm),theory(equality)],[2219,2185]),
[iquote('0:SpR:2219.1,2185.1')] ).
cnf(16970,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_229,u),select(q37,u)) ),
inference(rew,[status(thm),theory(equality)],[16968,16965]),
[iquote('0:Rew:16968.2,16965.2')] ).
cnf(16972,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q37,u),select(q36,u)) ),
inference(spr,[status(thm),theory(equality)],[2220,2186]),
[iquote('0:SpR:2220.1,2186.1')] ).
cnf(16975,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_229,u),select(q36,u)) ),
inference(rew,[status(thm),theory(equality)],[16972,16970]),
[iquote('0:Rew:16972.2,16970.2')] ).
cnf(16977,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_208,u),select(q35,u)) ),
inference(spr,[status(thm),theory(equality)],[2221,2167]),
[iquote('0:SpR:2221.1,2167.1')] ).
cnf(16980,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q35,u),select(q34,u)) ),
inference(spr,[status(thm),theory(equality)],[2222,2187]),
[iquote('0:SpR:2222.1,2187.1')] ).
cnf(16982,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_208,u),select(q34,u)) ),
inference(rew,[status(thm),theory(equality)],[16980,16977]),
[iquote('0:Rew:16980.2,16977.2')] ).
cnf(16984,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q34,u),select(q33,u)) ),
inference(spr,[status(thm),theory(equality)],[2223,2188]),
[iquote('0:SpR:2223.1,2188.1')] ).
cnf(16987,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_208,u),select(q33,u)) ),
inference(rew,[status(thm),theory(equality)],[16984,16982]),
[iquote('0:Rew:16984.2,16982.2')] ).
cnf(16989,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_187,u),select(q32,u)) ),
inference(spr,[status(thm),theory(equality)],[2224,2168]),
[iquote('0:SpR:2224.1,2168.1')] ).
cnf(16992,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q32,u),select(q31,u)) ),
inference(spr,[status(thm),theory(equality)],[2225,2190]),
[iquote('0:SpR:2225.1,2190.1')] ).
cnf(16994,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_187,u),select(q31,u)) ),
inference(rew,[status(thm),theory(equality)],[16992,16989]),
[iquote('0:Rew:16992.2,16989.2')] ).
cnf(16996,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q31,u),select(q30,u)) ),
inference(spr,[status(thm),theory(equality)],[2226,2191]),
[iquote('0:SpR:2226.1,2191.1')] ).
cnf(16999,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_187,u),select(q30,u)) ),
inference(rew,[status(thm),theory(equality)],[16996,16994]),
[iquote('0:Rew:16996.2,16994.2')] ).
cnf(17001,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q11,u),select(q10,u)) ),
inference(spr,[status(thm),theory(equality)],[2227,2189]),
[iquote('0:SpR:2227.1,2189.1')] ).
cnf(17003,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_25,u),select(q10,u)) ),
inference(rew,[status(thm),theory(equality)],[17001,16962]),
[iquote('0:Rew:17001.2,16962.2')] ).
cnf(17005,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_166,u),select(q29,u)) ),
inference(spr,[status(thm),theory(equality)],[2228,2169]),
[iquote('0:SpR:2228.1,2169.1')] ).
cnf(17008,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_157,u),select(q2,u)) ),
inference(spr,[status(thm),theory(equality)],[2229,2170]),
[iquote('0:SpR:2229.1,2170.1')] ).
cnf(17011,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q29,u),select(q28,u)) ),
inference(spr,[status(thm),theory(equality)],[2230,2192]),
[iquote('0:SpR:2230.1,2192.1')] ).
cnf(17013,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_166,u),select(q28,u)) ),
inference(rew,[status(thm),theory(equality)],[17011,17005]),
[iquote('0:Rew:17011.2,17005.2')] ).
cnf(17015,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q28,u),select(q27,u)) ),
inference(spr,[status(thm),theory(equality)],[2231,2193]),
[iquote('0:SpR:2231.1,2193.1')] ).
cnf(17018,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_166,u),select(q27,u)) ),
inference(rew,[status(thm),theory(equality)],[17015,17013]),
[iquote('0:Rew:17015.2,17013.2')] ).
cnf(17020,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_136,u),select(q26,u)) ),
inference(spr,[status(thm),theory(equality)],[2232,2171]),
[iquote('0:SpR:2232.1,2171.1')] ).
cnf(17023,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q26,u),select(q25,u)) ),
inference(spr,[status(thm),theory(equality)],[2233,2194]),
[iquote('0:SpR:2233.1,2194.1')] ).
cnf(17025,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_136,u),select(q25,u)) ),
inference(rew,[status(thm),theory(equality)],[17023,17020]),
[iquote('0:Rew:17023.2,17020.2')] ).
cnf(17027,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q25,u),select(q24,u)) ),
inference(spr,[status(thm),theory(equality)],[2234,2196]),
[iquote('0:SpR:2234.1,2196.1')] ).
cnf(17030,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_136,u),select(q24,u)) ),
inference(rew,[status(thm),theory(equality)],[17027,17025]),
[iquote('0:Rew:17027.2,17025.2')] ).
cnf(17032,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_115,u),select(q23,u)) ),
inference(spr,[status(thm),theory(equality)],[2235,2172]),
[iquote('0:SpR:2235.1,2172.1')] ).
cnf(17035,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q9,u),select(q10,u)) ),
inference(spr,[status(thm),theory(equality)],[2236,2195]),
[iquote('0:SpR:2236.1,2195.1')] ).
cnf(17038,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q23,u),select(q22,u)) ),
inference(spr,[status(thm),theory(equality)],[2237,2197]),
[iquote('0:SpR:2237.1,2197.1')] ).
cnf(17040,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_115,u),select(q22,u)) ),
inference(rew,[status(thm),theory(equality)],[17038,17032]),
[iquote('0:Rew:17038.2,17032.2')] ).
cnf(17042,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q21,u),select(q22,u)) ),
inference(spr,[status(thm),theory(equality)],[2238,2198]),
[iquote('0:SpR:2238.1,2198.1')] ).
cnf(17065,plain,
( equal(index_282,index_240)
| equal(select(earray_226,index_282),elem_283) ),
inference(spr,[status(thm),theory(equality)],[16476,16462]),
[iquote('0:SpR:16476.1,16462.0')] ).
cnf(17069,plain,
equal(index_282,index_240),
inference(spt,[spt(split,[position(s1)])],[17065]),
[iquote('1:Spt:17065.0')] ).
cnf(17070,plain,
equal(select(q40,head),index_240),
inference(rew,[status(thm),theory(equality)],[17069,231]),
[iquote('1:Rew:17069.0,231.0')] ).
cnf(17097,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(select(earray_73,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[16609,16578]),
[iquote('0:SpR:16609.1,16578.1')] ).
cnf(17168,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q18,head),index_95) ),
inference(spr,[status(thm),theory(equality)],[16905,259]),
[iquote('0:SpR:16905.2,259.0')] ).
cnf(17172,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_95,index_69) ),
inference(rew,[status(thm),theory(equality)],[980,17168]),
[iquote('0:Rew:980.0,17168.2')] ).
cnf(17173,plain,
equal(index_95,index_69),
inference(mrr,[status(thm)],[17172,4,3]),
[iquote('0:MRR:17172.0,17172.1,4.0,3.0')] ).
cnf(17174,plain,
equal(s(index_69),index_96),
inference(rew,[status(thm),theory(equality)],[17173,260]),
[iquote('0:Rew:17173.0,260.0')] ).
cnf(17386,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q15,head),index_68) ),
inference(spr,[status(thm),theory(equality)],[16917,248]),
[iquote('0:SpR:16917.2,248.0')] ).
cnf(17390,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_68,index_48) ),
inference(rew,[status(thm),theory(equality)],[981,17386]),
[iquote('0:Rew:981.0,17386.2')] ).
cnf(17391,plain,
equal(index_68,index_48),
inference(mrr,[status(thm)],[17390,4,3]),
[iquote('0:MRR:17390.0,17390.1,4.0,3.0')] ).
cnf(17392,plain,
equal(s(index_48),index_69),
inference(rew,[status(thm),theory(equality)],[17391,249]),
[iquote('0:Rew:17391.0,249.0')] ).
cnf(17727,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q2,head),index_3) ),
inference(spr,[status(thm),theory(equality)],[16921,16340]),
[iquote('0:SpR:16921.2,16340.0')] ).
cnf(17730,plain,
equal(select(q2,head),index_3),
inference(mrr,[status(thm)],[17727,4,3]),
[iquote('0:MRR:17727.0,17727.1,4.0,3.0')] ).
cnf(17739,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q12,head),index_47) ),
inference(spr,[status(thm),theory(equality)],[16933,239]),
[iquote('0:SpR:16933.2,239.0')] ).
cnf(17743,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_47,index_27) ),
inference(rew,[status(thm),theory(equality)],[983,17739]),
[iquote('0:Rew:983.0,17739.2')] ).
cnf(17744,plain,
equal(index_47,index_27),
inference(mrr,[status(thm)],[17743,4,3]),
[iquote('0:MRR:17743.0,17743.1,4.0,3.0')] ).
cnf(17745,plain,
equal(s(index_27),index_48),
inference(rew,[status(thm),theory(equality)],[17744,240]),
[iquote('0:Rew:17744.0,240.0')] ).
cnf(18086,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q6,head),index_278) ),
inference(spr,[status(thm),theory(equality)],[16945,229]),
[iquote('0:SpR:16945.2,229.0')] ).
cnf(18090,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_278,index_258) ),
inference(rew,[status(thm),theory(equality)],[984,18086]),
[iquote('0:Rew:984.0,18086.2')] ).
cnf(18091,plain,
equal(index_278,index_258),
inference(mrr,[status(thm)],[18090,4,3]),
[iquote('0:MRR:18090.0,18090.1,4.0,3.0')] ).
cnf(18092,plain,
equal(s(index_258),index_279),
inference(rew,[status(thm),theory(equality)],[18091,230]),
[iquote('0:Rew:18091.0,230.0')] ).
cnf(18298,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q39,head),index_240) ),
inference(spr,[status(thm),theory(equality)],[16954,17070]),
[iquote('1:SpR:16954.2,17070.0')] ).
cnf(18301,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_231,index_240) ),
inference(rew,[status(thm),theory(equality)],[985,18298]),
[iquote('1:Rew:985.0,18298.2')] ).
cnf(18302,plain,
equal(index_231,index_240),
inference(mrr,[status(thm)],[18301,4,3]),
[iquote('1:MRR:18301.0,18301.1,4.0,3.0')] ).
cnf(18303,plain,
equal(s(index_230),index_240),
inference(rew,[status(thm),theory(equality)],[18302,209]),
[iquote('1:Rew:18302.0,209.0')] ).
cnf(18581,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q3,head),index_257) ),
inference(spr,[status(thm),theory(equality)],[16960,219]),
[iquote('0:SpR:16960.2,219.0')] ).
cnf(18585,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_257,index_159) ),
inference(rew,[status(thm),theory(equality)],[989,18581]),
[iquote('0:Rew:989.0,18581.2')] ).
cnf(18586,plain,
equal(index_257,index_159),
inference(mrr,[status(thm)],[18585,4,3]),
[iquote('0:MRR:18585.0,18585.1,4.0,3.0')] ).
cnf(18587,plain,
equal(s(index_159),index_258),
inference(rew,[status(thm),theory(equality)],[18586,220]),
[iquote('0:Rew:18586.0,220.0')] ).
cnf(18928,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q36,head),index_230) ),
inference(spr,[status(thm),theory(equality)],[16975,208]),
[iquote('0:SpR:16975.2,208.0')] ).
cnf(18932,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_230,index_210) ),
inference(rew,[status(thm),theory(equality)],[986,18928]),
[iquote('0:Rew:986.0,18928.2')] ).
cnf(18933,plain,
equal(index_230,index_210),
inference(mrr,[status(thm)],[18932,4,3]),
[iquote('0:MRR:18932.0,18932.1,4.0,3.0')] ).
cnf(18935,plain,
equal(s(index_210),index_240),
inference(rew,[status(thm),theory(equality)],[18933,18303]),
[iquote('1:Rew:18933.0,18303.0')] ).
cnf(19274,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q33,head),index_209) ),
inference(spr,[status(thm),theory(equality)],[16987,199]),
[iquote('0:SpR:16987.2,199.0')] ).
cnf(19278,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_209,index_189) ),
inference(rew,[status(thm),theory(equality)],[987,19274]),
[iquote('0:Rew:987.0,19274.2')] ).
cnf(19279,plain,
equal(index_209,index_189),
inference(mrr,[status(thm)],[19278,4,3]),
[iquote('0:MRR:19278.0,19278.1,4.0,3.0')] ).
cnf(19280,plain,
equal(s(index_189),index_210),
inference(rew,[status(thm),theory(equality)],[19279,201]),
[iquote('0:Rew:19279.0,201.0')] ).
cnf(19621,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q30,head),index_188) ),
inference(spr,[status(thm),theory(equality)],[16999,191]),
[iquote('0:SpR:16999.2,191.0')] ).
cnf(19625,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_188,index_168) ),
inference(rew,[status(thm),theory(equality)],[988,19621]),
[iquote('0:Rew:988.0,19621.2')] ).
cnf(19626,plain,
equal(index_188,index_168),
inference(mrr,[status(thm)],[19625,4,3]),
[iquote('0:MRR:19625.0,19625.1,4.0,3.0')] ).
cnf(19627,plain,
equal(s(index_168),index_189),
inference(rew,[status(thm),theory(equality)],[19626,192]),
[iquote('0:Rew:19626.0,192.0')] ).
cnf(19966,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q10,head),index_26) ),
inference(spr,[status(thm),theory(equality)],[17003,221]),
[iquote('0:SpR:17003.2,221.0')] ).
cnf(19970,plain,
equal(select(q10,head),index_26),
inference(mrr,[status(thm)],[19966,4,3]),
[iquote('0:MRR:19966.0,19966.1,4.0,3.0')] ).
cnf(19976,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q2,head),index_158) ),
inference(spr,[status(thm),theory(equality)],[17008,178]),
[iquote('0:SpR:17008.2,178.0')] ).
cnf(19980,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_158,index_3) ),
inference(rew,[status(thm),theory(equality)],[17730,19976]),
[iquote('0:Rew:17730.0,19976.2')] ).
cnf(19981,plain,
equal(index_158,index_3),
inference(mrr,[status(thm)],[19980,4,3]),
[iquote('0:MRR:19980.0,19980.1,4.0,3.0')] ).
cnf(19982,plain,
equal(s(index_3),index_159),
inference(rew,[status(thm),theory(equality)],[19981,179]),
[iquote('0:Rew:19981.0,179.0')] ).
cnf(20050,plain,
equal(index_159,index_78),
inference(rew,[status(thm),theory(equality)],[1135,19982]),
[iquote('0:Rew:1135.0,19982.0')] ).
cnf(20054,plain,
equal(s(index_78),index_258),
inference(rew,[status(thm),theory(equality)],[20050,18587]),
[iquote('0:Rew:20050.0,18587.0')] ).
cnf(20123,plain,
equal(index_258,index_153),
inference(rew,[status(thm),theory(equality)],[1121,20054]),
[iquote('0:Rew:1121.0,20054.0')] ).
cnf(20127,plain,
equal(s(index_153),index_279),
inference(rew,[status(thm),theory(equality)],[20123,18092]),
[iquote('0:Rew:20123.0,18092.0')] ).
cnf(20197,plain,
equal(index_279,index_234),
inference(rew,[status(thm),theory(equality)],[12535,20127]),
[iquote('0:Rew:12535.0,20127.0')] ).
cnf(20199,plain,
equal(select(q9,head),index_234),
inference(rew,[status(thm),theory(equality)],[20197,982]),
[iquote('0:Rew:20197.0,982.0')] ).
cnf(20622,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q27,head),index_167) ),
inference(spr,[status(thm),theory(equality)],[17018,182]),
[iquote('0:SpR:17018.2,182.0')] ).
cnf(20626,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_167,index_138) ),
inference(rew,[status(thm),theory(equality)],[990,20622]),
[iquote('0:Rew:990.0,20622.2')] ).
cnf(20627,plain,
equal(index_167,index_138),
inference(mrr,[status(thm)],[20626,4,3]),
[iquote('0:MRR:20626.0,20626.1,4.0,3.0')] ).
cnf(20628,plain,
equal(s(index_138),index_168),
inference(rew,[status(thm),theory(equality)],[20627,183]),
[iquote('0:Rew:20627.0,183.0')] ).
cnf(20971,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q24,head),index_137) ),
inference(spr,[status(thm),theory(equality)],[17030,169]),
[iquote('0:SpR:17030.2,169.0')] ).
cnf(20975,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_137,index_117) ),
inference(rew,[status(thm),theory(equality)],[991,20971]),
[iquote('0:Rew:991.0,20971.2')] ).
cnf(20976,plain,
equal(index_137,index_117),
inference(mrr,[status(thm)],[20975,4,3]),
[iquote('0:MRR:20975.0,20975.1,4.0,3.0')] ).
cnf(20977,plain,
equal(s(index_117),index_138),
inference(rew,[status(thm),theory(equality)],[20976,170]),
[iquote('0:Rew:20976.0,170.0')] ).
cnf(21315,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q10,head),index_234) ),
inference(spr,[status(thm),theory(equality)],[17035,20199]),
[iquote('0:SpR:17035.2,20199.0')] ).
cnf(21318,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_26,index_234) ),
inference(rew,[status(thm),theory(equality)],[19970,21315]),
[iquote('0:Rew:19970.0,21315.2')] ).
cnf(21319,plain,
equal(index_26,index_234),
inference(mrr,[status(thm)],[21318,4,3]),
[iquote('0:MRR:21318.0,21318.1,4.0,3.0')] ).
cnf(21320,plain,
equal(s(index_234),index_27),
inference(rew,[status(thm),theory(equality)],[21319,225]),
[iquote('0:Rew:21319.0,225.0')] ).
cnf(21389,plain,
equal(index_27,index_246),
inference(rew,[status(thm),theory(equality)],[1191,21320]),
[iquote('0:Rew:1191.0,21320.0')] ).
cnf(21393,plain,
equal(s(index_246),index_48),
inference(rew,[status(thm),theory(equality)],[21389,17745]),
[iquote('0:Rew:21389.0,17745.0')] ).
cnf(21462,plain,
equal(index_48,index_252),
inference(rew,[status(thm),theory(equality)],[1184,21393]),
[iquote('0:Rew:1184.0,21393.0')] ).
cnf(21466,plain,
equal(s(index_252),index_69),
inference(rew,[status(thm),theory(equality)],[21462,17392]),
[iquote('0:Rew:21462.0,17392.0')] ).
cnf(21536,plain,
equal(index_69,index_261),
inference(rew,[status(thm),theory(equality)],[9870,21466]),
[iquote('0:Rew:9870.0,21466.0')] ).
cnf(21539,plain,
equal(s(index_261),index_96),
inference(rew,[status(thm),theory(equality)],[21536,17174]),
[iquote('0:Rew:21536.0,17174.0')] ).
cnf(21611,plain,
equal(index_96,index_267),
inference(rew,[status(thm),theory(equality)],[1177,21539]),
[iquote('0:Rew:1177.0,21539.0')] ).
cnf(21613,plain,
equal(select(q21,head),index_267),
inference(rew,[status(thm),theory(equality)],[21611,979]),
[iquote('0:Rew:21611.0,979.0')] ).
cnf(22167,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q22,head),index_116) ),
inference(spr,[status(thm),theory(equality)],[17040,160]),
[iquote('0:SpR:17040.2,160.0')] ).
cnf(22171,plain,
equal(select(q22,head),index_116),
inference(mrr,[status(thm)],[22167,4,3]),
[iquote('0:MRR:22167.0,22167.1,4.0,3.0')] ).
cnf(22179,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q22,head),index_267) ),
inference(spr,[status(thm),theory(equality)],[17042,21613]),
[iquote('0:SpR:17042.2,21613.0')] ).
cnf(22182,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_116,index_267) ),
inference(rew,[status(thm),theory(equality)],[22171,22179]),
[iquote('0:Rew:22171.0,22179.2')] ).
cnf(22183,plain,
equal(index_116,index_267),
inference(mrr,[status(thm)],[22182,4,3]),
[iquote('0:MRR:22182.0,22182.1,4.0,3.0')] ).
cnf(22184,plain,
equal(s(index_267),index_117),
inference(rew,[status(thm),theory(equality)],[22183,161]),
[iquote('0:Rew:22183.0,161.0')] ).
cnf(22253,plain,
equal(index_117,index_273),
inference(rew,[status(thm),theory(equality)],[1170,22184]),
[iquote('0:Rew:1170.0,22184.0')] ).
cnf(22257,plain,
equal(s(index_273),index_138),
inference(rew,[status(thm),theory(equality)],[22253,20977]),
[iquote('0:Rew:22253.0,20977.0')] ).
cnf(22326,plain,
equal(index_138,index_9),
inference(rew,[status(thm),theory(equality)],[8435,22257]),
[iquote('0:Rew:8435.0,22257.0')] ).
cnf(22330,plain,
equal(s(index_9),index_168),
inference(rew,[status(thm),theory(equality)],[22326,20628]),
[iquote('0:Rew:22326.0,20628.0')] ).
cnf(22400,plain,
equal(index_168,index_15),
inference(rew,[status(thm),theory(equality)],[1268,22330]),
[iquote('0:Rew:1268.0,22330.0')] ).
cnf(22404,plain,
equal(s(index_15),index_189),
inference(rew,[status(thm),theory(equality)],[22400,19627]),
[iquote('0:Rew:22400.0,19627.0')] ).
cnf(22475,plain,
equal(index_189,index_21),
inference(rew,[status(thm),theory(equality)],[1226,22404]),
[iquote('0:Rew:1226.0,22404.0')] ).
cnf(22479,plain,
equal(s(index_21),index_210),
inference(rew,[status(thm),theory(equality)],[22475,19280]),
[iquote('0:Rew:22475.0,19280.0')] ).
cnf(22551,plain,
equal(index_210,index_30),
inference(rew,[status(thm),theory(equality)],[8968,22479]),
[iquote('0:Rew:8968.0,22479.0')] ).
cnf(22554,plain,
equal(s(index_30),index_240),
inference(rew,[status(thm),theory(equality)],[22551,18935]),
[iquote('1:Rew:22551.0,18935.0')] ).
cnf(22555,plain,
equal(index_230,index_30),
inference(rew,[status(thm),theory(equality)],[22551,18933]),
[iquote('0:Rew:22551.0,18933.0')] ).
cnf(22628,plain,
equal(index_36,index_240),
inference(rew,[status(thm),theory(equality)],[1163,22554]),
[iquote('1:Rew:1163.0,22554.0')] ).
cnf(22629,plain,
$false,
inference(mrr,[status(thm)],[22628,15258]),
[iquote('1:MRR:22628.0,15258.0')] ).
cnf(22630,plain,
~ equal(index_282,index_240),
inference(spt,[spt(split,[position(sa)])],[22629,17069]),
[iquote('1:Spt:22629.0,17065.0,17069.0')] ).
cnf(22631,plain,
equal(select(earray_226,index_282),elem_283),
inference(spt,[spt(split,[position(s2)])],[17065]),
[iquote('1:Spt:22629.0,17065.1')] ).
cnf(22633,plain,
equal(s(index_30),index_231),
inference(rew,[status(thm),theory(equality)],[22555,209]),
[iquote('0:Rew:22555.0,209.0')] ).
cnf(22634,plain,
equal(index_231,index_36),
inference(rew,[status(thm),theory(equality)],[1163,22633]),
[iquote('0:Rew:1163.0,22633.0')] ).
cnf(22636,plain,
equal(select(q39,head),index_36),
inference(rew,[status(thm),theory(equality)],[22634,985]),
[iquote('0:Rew:22634.0,985.0')] ).
cnf(23907,plain,
( equal(index_282,index_225)
| equal(select(earray_220,index_282),elem_283) ),
inference(spr,[status(thm),theory(equality)],[22631,16729]),
[iquote('1:SpR:22631.0,16729.1')] ).
cnf(23947,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q39,head),index_282) ),
inference(spr,[status(thm),theory(equality)],[231,16954]),
[iquote('0:SpR:231.0,16954.2')] ).
cnf(23948,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_282,index_36) ),
inference(rew,[status(thm),theory(equality)],[22636,23947]),
[iquote('0:Rew:22636.0,23947.2')] ).
cnf(23949,plain,
equal(index_282,index_36),
inference(mrr,[status(thm)],[23948,4,3]),
[iquote('0:MRR:23948.0,23948.1,4.0,3.0')] ).
cnf(23954,plain,
( equal(index_36,index_225)
| equal(select(earray_220,index_282),elem_283) ),
inference(rew,[status(thm),theory(equality)],[23949,23907]),
[iquote('1:Rew:23949.0,23907.0')] ).
cnf(23955,plain,
( equal(index_36,index_225)
| equal(select(earray_220,index_36),elem_283) ),
inference(rew,[status(thm),theory(equality)],[23949,23954]),
[iquote('1:Rew:23949.0,23954.1')] ).
cnf(23956,plain,
equal(select(earray_220,index_36),elem_283),
inference(mrr,[status(thm)],[23955,15234]),
[iquote('1:MRR:23955.0,15234.0')] ).
cnf(23966,plain,
( equal(index_36,index_219)
| equal(select(earray_214,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23956,16741]),
[iquote('1:SpR:23956.0,16741.1')] ).
cnf(23967,plain,
equal(select(earray_214,index_36),elem_283),
inference(mrr,[status(thm)],[23966,15210]),
[iquote('1:MRR:23966.0,15210.0')] ).
cnf(23969,plain,
( equal(index_36,index_213)
| equal(select(earray_205,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23967,16491]),
[iquote('1:SpR:23967.0,16491.1')] ).
cnf(23970,plain,
equal(select(earray_205,index_36),elem_283),
inference(mrr,[status(thm)],[23969,15186]),
[iquote('1:MRR:23969.0,15186.0')] ).
cnf(23972,plain,
( equal(index_36,index_204)
| equal(select(earray_199,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23970,16753]),
[iquote('1:SpR:23970.0,16753.1')] ).
cnf(23973,plain,
equal(select(earray_199,index_36),elem_283),
inference(mrr,[status(thm)],[23972,15162]),
[iquote('1:MRR:23972.0,15162.0')] ).
cnf(23975,plain,
( equal(index_36,index_198)
| equal(select(earray_193,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23973,16765]),
[iquote('1:SpR:23973.0,16765.1')] ).
cnf(23976,plain,
equal(select(earray_193,index_36),elem_283),
inference(mrr,[status(thm)],[23975,15138]),
[iquote('1:MRR:23975.0,15138.0')] ).
cnf(23981,plain,
( equal(index_36,index_192)
| equal(select(earray_184,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23976,16506]),
[iquote('1:SpR:23976.0,16506.1')] ).
cnf(23982,plain,
equal(select(earray_184,index_36),elem_283),
inference(mrr,[status(thm)],[23981,15114]),
[iquote('1:MRR:23981.0,15114.0')] ).
cnf(23984,plain,
( equal(index_36,index_183)
| equal(select(earray_178,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23982,16789]),
[iquote('1:SpR:23982.0,16789.1')] ).
cnf(23985,plain,
equal(select(earray_178,index_36),elem_283),
inference(mrr,[status(thm)],[23984,15090]),
[iquote('1:MRR:23984.0,15090.0')] ).
cnf(23987,plain,
( equal(index_36,index_177)
| equal(select(earray_172,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23985,16801]),
[iquote('1:SpR:23985.0,16801.1')] ).
cnf(23988,plain,
equal(select(earray_172,index_36),elem_283),
inference(mrr,[status(thm)],[23987,15066]),
[iquote('1:MRR:23987.0,15066.0')] ).
cnf(23990,plain,
( equal(index_36,index_171)
| equal(select(earray_163,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23988,16521]),
[iquote('1:SpR:23988.0,16521.1')] ).
cnf(23991,plain,
equal(select(earray_163,index_36),elem_283),
inference(mrr,[status(thm)],[23990,15042]),
[iquote('1:MRR:23990.0,15042.0')] ).
cnf(23996,plain,
( equal(index_36,index_162)
| equal(select(earray_148,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23991,16813]),
[iquote('1:SpR:23991.0,16813.1')] ).
cnf(23997,plain,
equal(select(earray_148,index_36),elem_283),
inference(mrr,[status(thm)],[23996,15018]),
[iquote('1:MRR:23996.0,15018.0')] ).
cnf(23999,plain,
( equal(index_36,index_147)
| equal(select(earray_142,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[23997,16825]),
[iquote('1:SpR:23997.0,16825.1')] ).
cnf(24000,plain,
equal(select(earray_142,index_36),elem_283),
inference(mrr,[status(thm)],[23999,14994]),
[iquote('1:MRR:23999.0,14994.0')] ).
cnf(24002,plain,
( equal(index_36,index_141)
| equal(select(earray_133,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[24000,16551]),
[iquote('1:SpR:24000.0,16551.1')] ).
cnf(24003,plain,
equal(select(earray_133,index_36),elem_283),
inference(mrr,[status(thm)],[24002,14970]),
[iquote('1:MRR:24002.0,14970.0')] ).
cnf(24005,plain,
( equal(index_36,index_132)
| equal(select(earray_127,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[24003,16837]),
[iquote('1:SpR:24003.0,16837.1')] ).
cnf(24006,plain,
equal(select(earray_127,index_36),elem_283),
inference(mrr,[status(thm)],[24005,14946]),
[iquote('1:MRR:24005.0,14946.0')] ).
cnf(24011,plain,
( equal(index_36,index_126)
| equal(select(earray_121,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[24006,16861]),
[iquote('1:SpR:24006.0,16861.1')] ).
cnf(24012,plain,
equal(select(earray_121,index_36),elem_283),
inference(mrr,[status(thm)],[24011,14922]),
[iquote('1:MRR:24011.0,14922.0')] ).
cnf(24014,plain,
( equal(index_36,index_120)
| equal(select(earray_112,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[24012,16566]),
[iquote('1:SpR:24012.0,16566.1')] ).
cnf(24015,plain,
equal(select(earray_112,index_36),elem_283),
inference(mrr,[status(thm)],[24014,13758]),
[iquote('1:MRR:24014.0,13758.0')] ).
cnf(24017,plain,
( equal(index_36,index_111)
| equal(select(earray_106,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[24015,16873]),
[iquote('1:SpR:24015.0,16873.1')] ).
cnf(24018,plain,
equal(select(earray_106,index_36),elem_283),
inference(mrr,[status(thm)],[24017,8122]),
[iquote('1:MRR:24017.0,8122.0')] ).
cnf(24020,plain,
( equal(index_36,index_105)
| equal(select(earray_100,index_36),elem_283) ),
inference(spr,[status(thm),theory(equality)],[24018,16885]),
[iquote('1:SpR:24018.0,16885.1')] ).
cnf(24021,plain,
equal(select(earray_100,index_36),elem_283),
inference(mrr,[status(thm)],[24020,8119]),
[iquote('1:MRR:24020.0,8119.0')] ).
cnf(24037,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(select(earray_64,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[17097,16382]),
[iquote('0:SpR:17097.2,16382.1')] ).
cnf(24106,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(select(earray_58,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[24037,16633]),
[iquote('0:SpR:24037.3,16633.1')] ).
cnf(24122,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(select(earray_52,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[24106,16645]),
[iquote('0:SpR:24106.4,16645.1')] ).
cnf(24138,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(index_51,u)
| equal(select(earray_43,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[24122,16397]),
[iquote('0:SpR:24122.5,16397.1')] ).
cnf(24154,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(index_51,u)
| equal(index_42,u)
| equal(select(earray_37,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[24138,16657]),
[iquote('0:SpR:24138.6,16657.1')] ).
cnf(24169,plain,
( equal(index_84,index_36)
| equal(index_90,index_36)
| equal(index_72,index_36)
| equal(index_63,index_36)
| equal(index_57,index_36)
| equal(index_51,index_36)
| equal(index_42,index_36)
| equal(select(earray_98,index_36),e13) ),
inference(spr,[status(thm),theory(equality)],[24154,1082]),
[iquote('0:SpR:24154.7,1082.0')] ).
cnf(24172,plain,
equal(select(earray_98,index_36),e13),
inference(mrr,[status(thm)],[24169,8110,8113,8107,8104,8101,7905,1157]),
[iquote('0:MRR:24169.0,24169.1,24169.2,24169.3,24169.4,24169.5,24169.6,8110.0,8113.0,8107.0,8104.0,8101.0,7905.0,1157.0')] ).
cnf(24174,plain,
( equal(index_36,index_99)
| equal(select(earray_100,index_36),e13) ),
inference(spr,[status(thm),theory(equality)],[24172,2277]),
[iquote('0:SpR:24172.0,2277.1')] ).
cnf(24175,plain,
( equal(index_36,index_99)
| equal(elem_283,e13) ),
inference(rew,[status(thm),theory(equality)],[24021,24174]),
[iquote('1:Rew:24021.0,24174.1')] ).
cnf(24176,plain,
$false,
inference(mrr,[status(thm)],[24175,8116,397]),
[iquote('1:MRR:24175.0,24175.1,8116.0,397.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.21 % Problem : SWV569-1.040 : TPTP v8.1.0. Released v4.0.0.
% 0.09/0.21 % Command : run_spass %d %s
% 0.10/0.46 % Computer : n008.cluster.edu
% 0.10/0.46 % Model : x86_64 x86_64
% 0.10/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.46 % Memory : 8042.1875MB
% 0.10/0.46 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.46 % CPULimit : 300
% 0.10/0.46 % WCLimit : 600
% 0.10/0.46 % DateTime : Wed Jun 15 12:50:22 EDT 2022
% 0.10/0.46 % CPUTime :
% 35.80/36.21
% 35.80/36.21 SPASS V 3.9
% 35.80/36.21 SPASS beiseite: Proof found.
% 35.80/36.21 % SZS status Theorem
% 35.80/36.21 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.80/36.21 SPASS derived 13736 clauses, backtracked 645 clauses, performed 1 splits and kept 10229 clauses.
% 35.80/36.21 SPASS allocated 82777 KBytes.
% 35.80/36.21 SPASS spent 0:0:35.71 on the problem.
% 35.80/36.21 0:00:00.04 for the input.
% 35.80/36.21 0:00:00.00 for the FLOTTER CNF translation.
% 35.80/36.21 0:00:01.04 for inferences.
% 35.80/36.21 0:00:00.02 for the backtracking.
% 35.80/36.21 0:0:34.01 for the reduction.
% 35.80/36.21
% 35.80/36.21
% 35.80/36.21 Here is a proof with depth 20, length 1174 :
% 35.80/36.21 % SZS output start Refutation
% See solution above
% 36.70/37.15 Formulae used in the proof : a1 a2 head_distinct_from_tail head_distinct_from_seq tail_distinct_from_seq as26 as25 as24 as23 as22 as21 as20 as19 as18 as17 as16 as15 as14 as13 as12 as11 as10 as9 as8 as7 as6 as5 as4 as3 as2 as1 hyp1 hyp2 hyp3 hyp4 hyp5 hyp6 hyp7 hyp8 hyp9 hyp10 hyp11 hyp13 hyp14 hyp15 hyp16 hyp20 hyp21 hyp22 hyp23 hyp24 hyp25 hyp26 hyp27 hyp28 hyp29 hyp30 hyp31 hyp34 hyp35 hyp36 hyp37 hyp38 hyp40 hyp41 hyp42 hyp45 hyp46 hyp57 hyp61 hyp63 hyp64 hyp65 hyp66 hyp67 hyp68 hyp69 hyp70 hyp71 hyp72 hyp76 hyp77 hyp78 hyp79 hyp80 hyp81 hyp82 hyp83 hyp84 hyp85 hyp86 hyp87 hyp88 hyp89 hyp90 hyp91 hyp92 hyp93 hyp94 hyp95 hyp96 hyp97 hyp98 hyp99 hyp100 hyp101 hyp102 hyp103 hyp104 hyp105 hyp106 hyp107 hyp108 hyp109 hyp110 hyp111 hyp112 hyp113 hyp114 hyp115 hyp116 hyp117 hyp118 hyp119 hyp120 hyp121 hyp122 hyp123 hyp124 hyp125 hyp126 hyp127 hyp128 hyp129 hyp130 hyp131 hyp132 hyp133 hyp134 hyp135 hyp136 hyp137 hyp138 hyp139 hyp140 hyp141 hyp143 hyp144 hyp145 hyp146 hyp147 hyp148 hyp149 hyp150 hyp151 hyp152 hyp153 hyp154 hyp155 hyp156 hyp157 hyp158 hyp159 hyp160 hyp161 hyp162 hyp163 hyp164 hyp165 hyp166 hyp167 hyp168 hyp169 hyp170 hyp171 hyp172 hyp173 hyp174 hyp175 hyp176 hyp177 hyp178 hyp179 hyp180 hyp181 hyp182 hyp183 hyp184 hyp185 hyp186 hyp187 hyp188 hyp189 hyp190 hyp191 hyp192 hyp193 hyp194 hyp195 hyp196 hyp197 hyp198 hyp199 hyp200 hyp201 hyp202 hyp203 hyp204 hyp205 hyp206 hyp207 hyp208 hyp209 hyp210 hyp211 hyp212 hyp213 hyp214 hyp215 hyp216 hyp217 hyp218 hyp219 hyp220 hyp221 hyp222 hyp223 hyp224 hyp225 hyp226 hyp227 hyp228 hyp229 hyp230 hyp231 hyp232 hyp233 hyp234 hyp235 hyp236 hyp237 hyp238 hyp239 hyp240 hyp241 hyp242 hyp243 hyp244 hyp245 hyp246 hyp247 hyp248 hyp249 hyp250 hyp251 hyp252 hyp253 hyp254 hyp255 hyp256 hyp257 hyp258 hyp259 hyp260 hyp261 hyp262 hyp263 hyp264 hyp265 hyp266 hyp267 hyp268 hyp269 hyp270 hyp271 hyp272 hyp273 hyp274 hyp275 hyp276 hyp277 hyp278 hyp279 hyp280 hyp281 hyp282 hyp283 hyp284 hyp285 hyp286 hyp287 hyp288 hyp289 hyp290 hyp291 hyp292 hyp293 hyp294 hyp295 hyp296 hyp297 hyp298 hyp299 hyp300 hyp301 hyp302 hyp303 hyp304 hyp305 hyp306 hyp307 hyp308 hyp309 hyp310 hyp311 hyp312 hyp313 hyp314 hyp315 hyp316 hyp317 hyp318 hyp319 hyp320 hyp321 hyp322 hyp323 hyp324 goal
% 36.70/37.15
%------------------------------------------------------------------------------