%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV570-1.043 : TPTP v8.1.0. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.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:23 EDT 2022
% Result : Unsatisfiable 0.54s 0.75s
% Output : Refutation 0.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 231
% Syntax : Number of clauses : 794 ( 794 unt; 0 nHn; 794 RR)
% Number of literals : 794 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 278 ( 278 usr; 270 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
equal(rselect_head(rstore_head(u,v)),v),
file('SWV570-1.043.p',unknown),
[] ).
cnf(5,axiom,
equal(rselect_tail(rstore_tail(u,v)),v),
file('SWV570-1.043.p',unknown),
[] ).
cnf(8,axiom,
equal(rselect_head(rstore_tail(u,v)),rselect_head(u)),
file('SWV570-1.043.p',unknown),
[] ).
cnf(9,axiom,
equal(rselect_head(rstore_seq(u,v)),rselect_head(u)),
file('SWV570-1.043.p',unknown),
[] ).
cnf(11,axiom,
equal(rselect_tail(rstore_head(u,v)),rselect_tail(u)),
file('SWV570-1.043.p',unknown),
[] ).
cnf(12,axiom,
equal(p(s(u)),u),
file('SWV570-1.043.p',unknown),
[] ).
cnf(16,axiom,
equal(s(s(s(u))),u),
file('SWV570-1.043.p',unknown),
[] ).
cnf(104,axiom,
equal(select(earray_260,index_261),elem_262),
file('SWV570-1.043.p',unknown),
[] ).
cnf(105,axiom,
equal(select(earray_260,index_264),elem_265),
file('SWV570-1.043.p',unknown),
[] ).
cnf(106,axiom,
equal(rselect_tail(q),index_0),
file('SWV570-1.043.p',unknown),
[] ).
cnf(107,axiom,
equal(s(index_99),index_102),
file('SWV570-1.043.p',unknown),
[] ).
cnf(108,axiom,
equal(rselect_tail(q24),index_105),
file('SWV570-1.043.p',unknown),
[] ).
cnf(109,axiom,
equal(s(index_105),index_108),
file('SWV570-1.043.p',unknown),
[] ).
cnf(110,axiom,
equal(rselect_tail(q25),index_111),
file('SWV570-1.043.p',unknown),
[] ).
cnf(111,axiom,
equal(s(index_111),index_114),
file('SWV570-1.043.p',unknown),
[] ).
cnf(112,axiom,
equal(rselect_tail(q26),index_117),
file('SWV570-1.043.p',unknown),
[] ).
cnf(113,axiom,
equal(s(index_9),index_12),
file('SWV570-1.043.p',unknown),
[] ).
cnf(114,axiom,
equal(s(index_117),index_120),
file('SWV570-1.043.p',unknown),
[] ).
cnf(115,axiom,
equal(rselect_tail(q27),index_123),
file('SWV570-1.043.p',unknown),
[] ).
cnf(116,axiom,
equal(s(index_123),index_126),
file('SWV570-1.043.p',unknown),
[] ).
cnf(117,axiom,
equal(rselect_tail(q28),index_129),
file('SWV570-1.043.p',unknown),
[] ).
cnf(118,axiom,
equal(s(index_129),index_132),
file('SWV570-1.043.p',unknown),
[] ).
cnf(119,axiom,
equal(rselect_tail(q2),index_135),
file('SWV570-1.043.p',unknown),
[] ).
cnf(120,axiom,
equal(s(index_135),index_138),
file('SWV570-1.043.p',unknown),
[] ).
cnf(121,axiom,
equal(rselect_tail(q29),index_141),
file('SWV570-1.043.p',unknown),
[] ).
cnf(122,axiom,
equal(s(index_141),index_144),
file('SWV570-1.043.p',unknown),
[] ).
cnf(123,axiom,
equal(rselect_tail(q30),index_147),
file('SWV570-1.043.p',unknown),
[] ).
cnf(124,axiom,
equal(rselect_tail(q10),index_15),
file('SWV570-1.043.p',unknown),
[] ).
cnf(125,axiom,
equal(s(index_147),index_150),
file('SWV570-1.043.p',unknown),
[] ).
cnf(126,axiom,
equal(rselect_tail(q31),index_153),
file('SWV570-1.043.p',unknown),
[] ).
cnf(127,axiom,
equal(s(index_153),index_156),
file('SWV570-1.043.p',unknown),
[] ).
cnf(128,axiom,
equal(rselect_tail(q32),index_159),
file('SWV570-1.043.p',unknown),
[] ).
cnf(129,axiom,
equal(s(index_159),index_162),
file('SWV570-1.043.p',unknown),
[] ).
cnf(130,axiom,
equal(rselect_tail(q33),index_165),
file('SWV570-1.043.p',unknown),
[] ).
cnf(131,axiom,
equal(s(index_165),index_168),
file('SWV570-1.043.p',unknown),
[] ).
cnf(132,axiom,
equal(rselect_tail(q34),index_171),
file('SWV570-1.043.p',unknown),
[] ).
cnf(133,axiom,
equal(s(index_171),index_174),
file('SWV570-1.043.p',unknown),
[] ).
cnf(134,axiom,
equal(rselect_tail(q35),index_177),
file('SWV570-1.043.p',unknown),
[] ).
cnf(135,axiom,
equal(s(index_15),index_18),
file('SWV570-1.043.p',unknown),
[] ).
cnf(136,axiom,
equal(s(index_177),index_180),
file('SWV570-1.043.p',unknown),
[] ).
cnf(137,axiom,
equal(rselect_tail(q36),index_183),
file('SWV570-1.043.p',unknown),
[] ).
cnf(138,axiom,
equal(s(index_183),index_186),
file('SWV570-1.043.p',unknown),
[] ).
cnf(139,axiom,
equal(rselect_tail(q37),index_189),
file('SWV570-1.043.p',unknown),
[] ).
cnf(140,axiom,
equal(s(index_189),index_192),
file('SWV570-1.043.p',unknown),
[] ).
cnf(141,axiom,
equal(rselect_tail(q38),index_195),
file('SWV570-1.043.p',unknown),
[] ).
cnf(142,axiom,
equal(s(index_195),index_198),
file('SWV570-1.043.p',unknown),
[] ).
cnf(143,axiom,
equal(rselect_tail(q3),index_201),
file('SWV570-1.043.p',unknown),
[] ).
cnf(144,axiom,
equal(s(index_201),index_204),
file('SWV570-1.043.p',unknown),
[] ).
cnf(145,axiom,
equal(rselect_tail(q39),index_207),
file('SWV570-1.043.p',unknown),
[] ).
cnf(146,axiom,
equal(rselect_tail(q11),index_21),
file('SWV570-1.043.p',unknown),
[] ).
cnf(147,axiom,
equal(s(index_207),index_210),
file('SWV570-1.043.p',unknown),
[] ).
cnf(148,axiom,
equal(rselect_tail(q40),index_213),
file('SWV570-1.043.p',unknown),
[] ).
cnf(149,axiom,
equal(s(index_213),index_216),
file('SWV570-1.043.p',unknown),
[] ).
cnf(150,axiom,
equal(rselect_tail(q41),index_219),
file('SWV570-1.043.p',unknown),
[] ).
cnf(151,axiom,
equal(s(index_219),index_222),
file('SWV570-1.043.p',unknown),
[] ).
cnf(152,axiom,
equal(rselect_tail(q42),index_225),
file('SWV570-1.043.p',unknown),
[] ).
cnf(153,axiom,
equal(s(index_225),index_228),
file('SWV570-1.043.p',unknown),
[] ).
cnf(154,axiom,
equal(rselect_tail(q4),index_231),
file('SWV570-1.043.p',unknown),
[] ).
cnf(155,axiom,
equal(s(index_231),index_234),
file('SWV570-1.043.p',unknown),
[] ).
cnf(156,axiom,
equal(rselect_tail(q5),index_237),
file('SWV570-1.043.p',unknown),
[] ).
cnf(157,axiom,
equal(s(index_21),index_24),
file('SWV570-1.043.p',unknown),
[] ).
cnf(158,axiom,
equal(s(index_237),index_240),
file('SWV570-1.043.p',unknown),
[] ).
cnf(159,axiom,
equal(rselect_tail(q6),index_243),
file('SWV570-1.043.p',unknown),
[] ).
cnf(160,axiom,
equal(s(index_243),index_246),
file('SWV570-1.043.p',unknown),
[] ).
cnf(161,axiom,
equal(rselect_tail(q7),index_249),
file('SWV570-1.043.p',unknown),
[] ).
cnf(162,axiom,
equal(s(index_249),index_252),
file('SWV570-1.043.p',unknown),
[] ).
cnf(163,axiom,
equal(rselect_tail(q8),index_255),
file('SWV570-1.043.p',unknown),
[] ).
cnf(164,axiom,
equal(s(index_255),index_258),
file('SWV570-1.043.p',unknown),
[] ).
cnf(165,axiom,
equal(rselect_head(q43),index_261),
file('SWV570-1.043.p',unknown),
[] ).
cnf(166,axiom,
equal(rselect_tail(q43),index_263),
file('SWV570-1.043.p',unknown),
[] ).
cnf(167,axiom,
equal(s(index_264),index_263),
file('SWV570-1.043.p',unknown),
[] ).
cnf(168,axiom,
equal(rselect_tail(q12),index_27),
file('SWV570-1.043.p',unknown),
[] ).
cnf(169,axiom,
equal(rselect_tail(q0),index_3),
file('SWV570-1.043.p',unknown),
[] ).
cnf(170,axiom,
equal(s(index_27),index_30),
file('SWV570-1.043.p',unknown),
[] ).
cnf(171,axiom,
equal(rselect_tail(q13),index_33),
file('SWV570-1.043.p',unknown),
[] ).
cnf(172,axiom,
equal(s(index_33),index_36),
file('SWV570-1.043.p',unknown),
[] ).
cnf(173,axiom,
equal(rselect_tail(q14),index_39),
file('SWV570-1.043.p',unknown),
[] ).
cnf(174,axiom,
equal(s(index_39),index_42),
file('SWV570-1.043.p',unknown),
[] ).
cnf(175,axiom,
equal(rselect_tail(q15),index_45),
file('SWV570-1.043.p',unknown),
[] ).
cnf(176,axiom,
equal(s(index_45),index_48),
file('SWV570-1.043.p',unknown),
[] ).
cnf(177,axiom,
equal(rselect_tail(q16),index_51),
file('SWV570-1.043.p',unknown),
[] ).
cnf(178,axiom,
equal(s(index_51),index_54),
file('SWV570-1.043.p',unknown),
[] ).
cnf(179,axiom,
equal(rselect_tail(q17),index_57),
file('SWV570-1.043.p',unknown),
[] ).
cnf(180,axiom,
equal(s(index_3),index_6),
file('SWV570-1.043.p',unknown),
[] ).
cnf(181,axiom,
equal(s(index_57),index_60),
file('SWV570-1.043.p',unknown),
[] ).
cnf(182,axiom,
equal(rselect_tail(q18),index_63),
file('SWV570-1.043.p',unknown),
[] ).
cnf(183,axiom,
equal(s(index_63),index_66),
file('SWV570-1.043.p',unknown),
[] ).
cnf(184,axiom,
equal(rselect_tail(q1),index_69),
file('SWV570-1.043.p',unknown),
[] ).
cnf(185,axiom,
equal(s(index_69),index_72),
file('SWV570-1.043.p',unknown),
[] ).
cnf(186,axiom,
equal(rselect_tail(q19),index_75),
file('SWV570-1.043.p',unknown),
[] ).
cnf(187,axiom,
equal(s(index_75),index_78),
file('SWV570-1.043.p',unknown),
[] ).
cnf(188,axiom,
equal(rselect_tail(q20),index_81),
file('SWV570-1.043.p',unknown),
[] ).
cnf(189,axiom,
equal(s(index_81),index_84),
file('SWV570-1.043.p',unknown),
[] ).
cnf(190,axiom,
equal(rselect_tail(q21),index_87),
file('SWV570-1.043.p',unknown),
[] ).
cnf(191,axiom,
equal(rselect_tail(q9),index_9),
file('SWV570-1.043.p',unknown),
[] ).
cnf(192,axiom,
equal(s(index_87),index_90),
file('SWV570-1.043.p',unknown),
[] ).
cnf(193,axiom,
equal(rselect_tail(q22),index_93),
file('SWV570-1.043.p',unknown),
[] ).
cnf(194,axiom,
equal(s(index_93),index_96),
file('SWV570-1.043.p',unknown),
[] ).
cnf(195,axiom,
equal(rselect_tail(q23),index_99),
file('SWV570-1.043.p',unknown),
[] ).
cnf(196,axiom,
equal(rstore_head(q,index_0),queue_1),
file('SWV570-1.043.p',unknown),
[] ).
cnf(197,axiom,
equal(rstore_seq(q23,earray_100),queue_101),
file('SWV570-1.043.p',unknown),
[] ).
cnf(198,axiom,
equal(rstore_tail(queue_101,index_102),queue_103),
file('SWV570-1.043.p',unknown),
[] ).
cnf(199,axiom,
equal(rstore_seq(q24,earray_106),queue_107),
file('SWV570-1.043.p',unknown),
[] ).
cnf(200,axiom,
equal(rstore_tail(queue_107,index_108),queue_109),
file('SWV570-1.043.p',unknown),
[] ).
cnf(201,axiom,
equal(rstore_seq(q9,earray_10),queue_11),
file('SWV570-1.043.p',unknown),
[] ).
cnf(202,axiom,
equal(rstore_seq(q25,earray_112),queue_113),
file('SWV570-1.043.p',unknown),
[] ).
cnf(203,axiom,
equal(rstore_tail(queue_113,index_114),queue_115),
file('SWV570-1.043.p',unknown),
[] ).
cnf(204,axiom,
equal(rstore_seq(q26,earray_118),queue_119),
file('SWV570-1.043.p',unknown),
[] ).
cnf(205,axiom,
equal(rstore_tail(queue_119,index_120),queue_121),
file('SWV570-1.043.p',unknown),
[] ).
cnf(206,axiom,
equal(rstore_seq(q27,earray_124),queue_125),
file('SWV570-1.043.p',unknown),
[] ).
cnf(207,axiom,
equal(rstore_tail(queue_125,index_126),queue_127),
file('SWV570-1.043.p',unknown),
[] ).
cnf(208,axiom,
equal(rstore_tail(queue_11,index_12),queue_13),
file('SWV570-1.043.p',unknown),
[] ).
cnf(209,axiom,
equal(rstore_seq(q28,earray_130),queue_131),
file('SWV570-1.043.p',unknown),
[] ).
cnf(210,axiom,
equal(rstore_tail(queue_131,index_132),queue_133),
file('SWV570-1.043.p',unknown),
[] ).
cnf(211,axiom,
equal(rstore_seq(q2,earray_136),queue_137),
file('SWV570-1.043.p',unknown),
[] ).
cnf(212,axiom,
equal(rstore_tail(queue_137,index_138),queue_139),
file('SWV570-1.043.p',unknown),
[] ).
cnf(213,axiom,
equal(rstore_seq(q29,earray_142),queue_143),
file('SWV570-1.043.p',unknown),
[] ).
cnf(214,axiom,
equal(rstore_tail(queue_143,index_144),queue_145),
file('SWV570-1.043.p',unknown),
[] ).
cnf(215,axiom,
equal(rstore_seq(q30,earray_148),queue_149),
file('SWV570-1.043.p',unknown),
[] ).
cnf(216,axiom,
equal(rstore_tail(queue_149,index_150),queue_151),
file('SWV570-1.043.p',unknown),
[] ).
cnf(217,axiom,
equal(rstore_seq(q31,earray_154),queue_155),
file('SWV570-1.043.p',unknown),
[] ).
cnf(218,axiom,
equal(rstore_tail(queue_155,index_156),queue_157),
file('SWV570-1.043.p',unknown),
[] ).
cnf(219,axiom,
equal(rstore_seq(q32,earray_160),queue_161),
file('SWV570-1.043.p',unknown),
[] ).
cnf(220,axiom,
equal(rstore_tail(queue_161,index_162),queue_163),
file('SWV570-1.043.p',unknown),
[] ).
cnf(221,axiom,
equal(rstore_seq(q33,earray_166),queue_167),
file('SWV570-1.043.p',unknown),
[] ).
cnf(222,axiom,
equal(rstore_tail(queue_167,index_168),queue_169),
file('SWV570-1.043.p',unknown),
[] ).
cnf(223,axiom,
equal(rstore_seq(q10,earray_16),queue_17),
file('SWV570-1.043.p',unknown),
[] ).
cnf(224,axiom,
equal(rstore_seq(q34,earray_172),queue_173),
file('SWV570-1.043.p',unknown),
[] ).
cnf(225,axiom,
equal(rstore_tail(queue_173,index_174),queue_175),
file('SWV570-1.043.p',unknown),
[] ).
cnf(226,axiom,
equal(rstore_seq(q35,earray_178),queue_179),
file('SWV570-1.043.p',unknown),
[] ).
cnf(227,axiom,
equal(rstore_tail(queue_179,index_180),queue_181),
file('SWV570-1.043.p',unknown),
[] ).
cnf(228,axiom,
equal(rstore_seq(q36,earray_184),queue_185),
file('SWV570-1.043.p',unknown),
[] ).
cnf(229,axiom,
equal(rstore_tail(queue_185,index_186),queue_187),
file('SWV570-1.043.p',unknown),
[] ).
cnf(230,axiom,
equal(rstore_tail(queue_17,index_18),queue_19),
file('SWV570-1.043.p',unknown),
[] ).
cnf(231,axiom,
equal(rstore_seq(q37,earray_190),queue_191),
file('SWV570-1.043.p',unknown),
[] ).
cnf(232,axiom,
equal(rstore_tail(queue_191,index_192),queue_193),
file('SWV570-1.043.p',unknown),
[] ).
cnf(233,axiom,
equal(rstore_seq(q38,earray_196),queue_197),
file('SWV570-1.043.p',unknown),
[] ).
cnf(234,axiom,
equal(rstore_tail(queue_197,index_198),queue_199),
file('SWV570-1.043.p',unknown),
[] ).
cnf(235,axiom,
equal(rstore_seq(q3,earray_202),queue_203),
file('SWV570-1.043.p',unknown),
[] ).
cnf(236,axiom,
equal(rstore_tail(queue_203,index_204),queue_205),
file('SWV570-1.043.p',unknown),
[] ).
cnf(237,axiom,
equal(rstore_seq(q39,earray_208),queue_209),
file('SWV570-1.043.p',unknown),
[] ).
cnf(238,axiom,
equal(rstore_tail(queue_209,index_210),queue_211),
file('SWV570-1.043.p',unknown),
[] ).
cnf(239,axiom,
equal(rstore_seq(q40,earray_214),queue_215),
file('SWV570-1.043.p',unknown),
[] ).
cnf(240,axiom,
equal(rstore_tail(queue_215,index_216),queue_217),
file('SWV570-1.043.p',unknown),
[] ).
cnf(241,axiom,
equal(rstore_seq(q41,earray_220),queue_221),
file('SWV570-1.043.p',unknown),
[] ).
cnf(242,axiom,
equal(rstore_tail(queue_221,index_222),queue_223),
file('SWV570-1.043.p',unknown),
[] ).
cnf(243,axiom,
equal(rstore_seq(q42,earray_226),queue_227),
file('SWV570-1.043.p',unknown),
[] ).
cnf(244,axiom,
equal(rstore_tail(queue_227,index_228),queue_229),
file('SWV570-1.043.p',unknown),
[] ).
cnf(245,axiom,
equal(rstore_seq(q11,earray_22),queue_23),
file('SWV570-1.043.p',unknown),
[] ).
cnf(246,axiom,
equal(rstore_seq(q4,earray_232),queue_233),
file('SWV570-1.043.p',unknown),
[] ).
cnf(247,axiom,
equal(rstore_tail(queue_233,index_234),queue_235),
file('SWV570-1.043.p',unknown),
[] ).
cnf(248,axiom,
equal(rstore_seq(q5,earray_238),queue_239),
file('SWV570-1.043.p',unknown),
[] ).
cnf(249,axiom,
equal(rstore_tail(queue_239,index_240),queue_241),
file('SWV570-1.043.p',unknown),
[] ).
cnf(250,axiom,
equal(rstore_seq(q6,earray_244),queue_245),
file('SWV570-1.043.p',unknown),
[] ).
cnf(251,axiom,
equal(rstore_tail(queue_245,index_246),queue_247),
file('SWV570-1.043.p',unknown),
[] ).
cnf(252,axiom,
equal(rstore_tail(queue_23,index_24),queue_25),
file('SWV570-1.043.p',unknown),
[] ).
cnf(253,axiom,
equal(rstore_seq(q7,earray_250),queue_251),
file('SWV570-1.043.p',unknown),
[] ).
cnf(254,axiom,
equal(rstore_tail(queue_251,index_252),queue_253),
file('SWV570-1.043.p',unknown),
[] ).
cnf(255,axiom,
equal(rstore_seq(q8,earray_256),queue_257),
file('SWV570-1.043.p',unknown),
[] ).
cnf(256,axiom,
equal(rstore_tail(queue_257,index_258),queue_259),
file('SWV570-1.043.p',unknown),
[] ).
cnf(257,axiom,
equal(rstore_seq(q12,earray_28),queue_29),
file('SWV570-1.043.p',unknown),
[] ).
cnf(258,axiom,
equal(rstore_tail(queue_29,index_30),queue_31),
file('SWV570-1.043.p',unknown),
[] ).
cnf(259,axiom,
equal(rstore_seq(q13,earray_34),queue_35),
file('SWV570-1.043.p',unknown),
[] ).
cnf(260,axiom,
equal(rstore_tail(queue_35,index_36),queue_37),
file('SWV570-1.043.p',unknown),
[] ).
cnf(261,axiom,
equal(rstore_seq(q14,earray_40),queue_41),
file('SWV570-1.043.p',unknown),
[] ).
cnf(262,axiom,
equal(rstore_tail(queue_41,index_42),queue_43),
file('SWV570-1.043.p',unknown),
[] ).
cnf(263,axiom,
equal(rstore_seq(q15,earray_46),queue_47),
file('SWV570-1.043.p',unknown),
[] ).
cnf(264,axiom,
equal(rstore_tail(queue_47,index_48),queue_49),
file('SWV570-1.043.p',unknown),
[] ).
cnf(265,axiom,
equal(rstore_seq(q0,earray_4),queue_5),
file('SWV570-1.043.p',unknown),
[] ).
cnf(266,axiom,
equal(rstore_seq(q16,earray_52),queue_53),
file('SWV570-1.043.p',unknown),
[] ).
cnf(267,axiom,
equal(rstore_tail(queue_53,index_54),queue_55),
file('SWV570-1.043.p',unknown),
[] ).
cnf(268,axiom,
equal(rstore_seq(q17,earray_58),queue_59),
file('SWV570-1.043.p',unknown),
[] ).
cnf(269,axiom,
equal(rstore_tail(queue_59,index_60),queue_61),
file('SWV570-1.043.p',unknown),
[] ).
cnf(270,axiom,
equal(rstore_seq(q18,earray_64),queue_65),
file('SWV570-1.043.p',unknown),
[] ).
cnf(271,axiom,
equal(rstore_tail(queue_65,index_66),queue_67),
file('SWV570-1.043.p',unknown),
[] ).
cnf(272,axiom,
equal(rstore_tail(queue_5,index_6),queue_7),
file('SWV570-1.043.p',unknown),
[] ).
cnf(273,axiom,
equal(rstore_seq(q1,earray_70),queue_71),
file('SWV570-1.043.p',unknown),
[] ).
cnf(274,axiom,
equal(rstore_tail(queue_71,index_72),queue_73),
file('SWV570-1.043.p',unknown),
[] ).
cnf(275,axiom,
equal(rstore_seq(q19,earray_76),queue_77),
file('SWV570-1.043.p',unknown),
[] ).
cnf(276,axiom,
equal(rstore_tail(queue_77,index_78),queue_79),
file('SWV570-1.043.p',unknown),
[] ).
cnf(277,axiom,
equal(rstore_seq(q20,earray_82),queue_83),
file('SWV570-1.043.p',unknown),
[] ).
cnf(278,axiom,
equal(rstore_tail(queue_83,index_84),queue_85),
file('SWV570-1.043.p',unknown),
[] ).
cnf(279,axiom,
equal(rstore_seq(q21,earray_88),queue_89),
file('SWV570-1.043.p',unknown),
[] ).
cnf(280,axiom,
equal(rstore_tail(queue_89,index_90),queue_91),
file('SWV570-1.043.p',unknown),
[] ).
cnf(281,axiom,
equal(rstore_seq(q22,earray_94),queue_95),
file('SWV570-1.043.p',unknown),
[] ).
cnf(282,axiom,
equal(rstore_tail(queue_95,index_96),queue_97),
file('SWV570-1.043.p',unknown),
[] ).
cnf(283,axiom,
equal(queue_1,q0),
file('SWV570-1.043.p',unknown),
[] ).
cnf(284,axiom,
equal(queue_7,q1),
file('SWV570-1.043.p',unknown),
[] ).
cnf(285,axiom,
equal(queue_13,q10),
file('SWV570-1.043.p',unknown),
[] ).
cnf(286,axiom,
equal(queue_19,q11),
file('SWV570-1.043.p',unknown),
[] ).
cnf(287,axiom,
equal(queue_25,q12),
file('SWV570-1.043.p',unknown),
[] ).
cnf(288,axiom,
equal(queue_31,q13),
file('SWV570-1.043.p',unknown),
[] ).
cnf(289,axiom,
equal(queue_37,q14),
file('SWV570-1.043.p',unknown),
[] ).
cnf(290,axiom,
equal(queue_43,q15),
file('SWV570-1.043.p',unknown),
[] ).
cnf(291,axiom,
equal(queue_49,q16),
file('SWV570-1.043.p',unknown),
[] ).
cnf(292,axiom,
equal(queue_55,q17),
file('SWV570-1.043.p',unknown),
[] ).
cnf(293,axiom,
equal(queue_61,q18),
file('SWV570-1.043.p',unknown),
[] ).
cnf(294,axiom,
equal(queue_67,q19),
file('SWV570-1.043.p',unknown),
[] ).
cnf(295,axiom,
equal(queue_73,q2),
file('SWV570-1.043.p',unknown),
[] ).
cnf(296,axiom,
equal(queue_79,q20),
file('SWV570-1.043.p',unknown),
[] ).
cnf(297,axiom,
equal(queue_85,q21),
file('SWV570-1.043.p',unknown),
[] ).
cnf(298,axiom,
equal(queue_91,q22),
file('SWV570-1.043.p',unknown),
[] ).
cnf(299,axiom,
equal(queue_97,q23),
file('SWV570-1.043.p',unknown),
[] ).
cnf(300,axiom,
equal(queue_103,q24),
file('SWV570-1.043.p',unknown),
[] ).
cnf(301,axiom,
equal(queue_109,q25),
file('SWV570-1.043.p',unknown),
[] ).
cnf(302,axiom,
equal(queue_115,q26),
file('SWV570-1.043.p',unknown),
[] ).
cnf(303,axiom,
equal(queue_121,q27),
file('SWV570-1.043.p',unknown),
[] ).
cnf(304,axiom,
equal(queue_127,q28),
file('SWV570-1.043.p',unknown),
[] ).
cnf(305,axiom,
equal(queue_133,q29),
file('SWV570-1.043.p',unknown),
[] ).
cnf(306,axiom,
equal(queue_139,q3),
file('SWV570-1.043.p',unknown),
[] ).
cnf(307,axiom,
equal(queue_145,q30),
file('SWV570-1.043.p',unknown),
[] ).
cnf(308,axiom,
equal(queue_151,q31),
file('SWV570-1.043.p',unknown),
[] ).
cnf(309,axiom,
equal(queue_157,q32),
file('SWV570-1.043.p',unknown),
[] ).
cnf(310,axiom,
equal(queue_163,q33),
file('SWV570-1.043.p',unknown),
[] ).
cnf(311,axiom,
equal(queue_169,q34),
file('SWV570-1.043.p',unknown),
[] ).
cnf(312,axiom,
equal(queue_175,q35),
file('SWV570-1.043.p',unknown),
[] ).
cnf(313,axiom,
equal(queue_181,q36),
file('SWV570-1.043.p',unknown),
[] ).
cnf(314,axiom,
equal(queue_187,q37),
file('SWV570-1.043.p',unknown),
[] ).
cnf(315,axiom,
equal(queue_193,q38),
file('SWV570-1.043.p',unknown),
[] ).
cnf(316,axiom,
equal(queue_199,q39),
file('SWV570-1.043.p',unknown),
[] ).
cnf(317,axiom,
equal(queue_205,q4),
file('SWV570-1.043.p',unknown),
[] ).
cnf(318,axiom,
equal(queue_211,q40),
file('SWV570-1.043.p',unknown),
[] ).
cnf(319,axiom,
equal(queue_217,q41),
file('SWV570-1.043.p',unknown),
[] ).
cnf(320,axiom,
equal(queue_223,q42),
file('SWV570-1.043.p',unknown),
[] ).
cnf(321,axiom,
equal(queue_229,q43),
file('SWV570-1.043.p',unknown),
[] ).
cnf(322,axiom,
equal(queue_235,q5),
file('SWV570-1.043.p',unknown),
[] ).
cnf(323,axiom,
equal(queue_241,q6),
file('SWV570-1.043.p',unknown),
[] ).
cnf(324,axiom,
equal(queue_247,q7),
file('SWV570-1.043.p',unknown),
[] ).
cnf(325,axiom,
equal(queue_253,q8),
file('SWV570-1.043.p',unknown),
[] ).
cnf(326,axiom,
equal(queue_259,q9),
file('SWV570-1.043.p',unknown),
[] ).
cnf(327,axiom,
~ equal(elem_265,elem_262),
file('SWV570-1.043.p',unknown),
[] ).
cnf(328,plain,
equal(rstore_tail(queue_95,index_96),q23),
inference(rew,[status(thm),theory(equality)],[299,282]),
[iquote('0:Rew:299.0,282.0')] ).
cnf(329,plain,
equal(rstore_tail(queue_89,index_90),q22),
inference(rew,[status(thm),theory(equality)],[298,280]),
[iquote('0:Rew:298.0,280.0')] ).
cnf(330,plain,
equal(rstore_tail(queue_83,index_84),q21),
inference(rew,[status(thm),theory(equality)],[297,278]),
[iquote('0:Rew:297.0,278.0')] ).
cnf(331,plain,
equal(rstore_tail(queue_77,index_78),q20),
inference(rew,[status(thm),theory(equality)],[296,276]),
[iquote('0:Rew:296.0,276.0')] ).
cnf(332,plain,
equal(rstore_tail(queue_71,index_72),q2),
inference(rew,[status(thm),theory(equality)],[295,274]),
[iquote('0:Rew:295.0,274.0')] ).
cnf(333,plain,
equal(rstore_tail(queue_5,index_6),q1),
inference(rew,[status(thm),theory(equality)],[284,272]),
[iquote('0:Rew:284.0,272.0')] ).
cnf(334,plain,
equal(rstore_tail(queue_65,index_66),q19),
inference(rew,[status(thm),theory(equality)],[294,271]),
[iquote('0:Rew:294.0,271.0')] ).
cnf(335,plain,
equal(rstore_tail(queue_59,index_60),q18),
inference(rew,[status(thm),theory(equality)],[293,269]),
[iquote('0:Rew:293.0,269.0')] ).
cnf(336,plain,
equal(rstore_tail(queue_53,index_54),q17),
inference(rew,[status(thm),theory(equality)],[292,267]),
[iquote('0:Rew:292.0,267.0')] ).
cnf(337,plain,
equal(rstore_tail(queue_47,index_48),q16),
inference(rew,[status(thm),theory(equality)],[291,264]),
[iquote('0:Rew:291.0,264.0')] ).
cnf(338,plain,
equal(rstore_tail(queue_41,index_42),q15),
inference(rew,[status(thm),theory(equality)],[290,262]),
[iquote('0:Rew:290.0,262.0')] ).
cnf(339,plain,
equal(rstore_tail(queue_35,index_36),q14),
inference(rew,[status(thm),theory(equality)],[289,260]),
[iquote('0:Rew:289.0,260.0')] ).
cnf(340,plain,
equal(rstore_tail(queue_29,index_30),q13),
inference(rew,[status(thm),theory(equality)],[288,258]),
[iquote('0:Rew:288.0,258.0')] ).
cnf(341,plain,
equal(rstore_tail(queue_257,index_258),q9),
inference(rew,[status(thm),theory(equality)],[326,256]),
[iquote('0:Rew:326.0,256.0')] ).
cnf(342,plain,
equal(rstore_tail(queue_251,index_252),q8),
inference(rew,[status(thm),theory(equality)],[325,254]),
[iquote('0:Rew:325.0,254.0')] ).
cnf(343,plain,
equal(rstore_tail(queue_23,index_24),q12),
inference(rew,[status(thm),theory(equality)],[287,252]),
[iquote('0:Rew:287.0,252.0')] ).
cnf(344,plain,
equal(rstore_tail(queue_245,index_246),q7),
inference(rew,[status(thm),theory(equality)],[324,251]),
[iquote('0:Rew:324.0,251.0')] ).
cnf(345,plain,
equal(rstore_tail(queue_239,index_240),q6),
inference(rew,[status(thm),theory(equality)],[323,249]),
[iquote('0:Rew:323.0,249.0')] ).
cnf(346,plain,
equal(rstore_tail(queue_233,index_234),q5),
inference(rew,[status(thm),theory(equality)],[322,247]),
[iquote('0:Rew:322.0,247.0')] ).
cnf(347,plain,
equal(rstore_tail(queue_227,index_228),q43),
inference(rew,[status(thm),theory(equality)],[321,244]),
[iquote('0:Rew:321.0,244.0')] ).
cnf(348,plain,
equal(rstore_tail(queue_221,index_222),q42),
inference(rew,[status(thm),theory(equality)],[320,242]),
[iquote('0:Rew:320.0,242.0')] ).
cnf(349,plain,
equal(rstore_tail(queue_215,index_216),q41),
inference(rew,[status(thm),theory(equality)],[319,240]),
[iquote('0:Rew:319.0,240.0')] ).
cnf(350,plain,
equal(rstore_tail(queue_209,index_210),q40),
inference(rew,[status(thm),theory(equality)],[318,238]),
[iquote('0:Rew:318.0,238.0')] ).
cnf(351,plain,
equal(rstore_tail(queue_203,index_204),q4),
inference(rew,[status(thm),theory(equality)],[317,236]),
[iquote('0:Rew:317.0,236.0')] ).
cnf(352,plain,
equal(rstore_tail(queue_197,index_198),q39),
inference(rew,[status(thm),theory(equality)],[316,234]),
[iquote('0:Rew:316.0,234.0')] ).
cnf(353,plain,
equal(rstore_tail(queue_191,index_192),q38),
inference(rew,[status(thm),theory(equality)],[315,232]),
[iquote('0:Rew:315.0,232.0')] ).
cnf(354,plain,
equal(rstore_tail(queue_17,index_18),q11),
inference(rew,[status(thm),theory(equality)],[286,230]),
[iquote('0:Rew:286.0,230.0')] ).
cnf(355,plain,
equal(rstore_tail(queue_185,index_186),q37),
inference(rew,[status(thm),theory(equality)],[314,229]),
[iquote('0:Rew:314.0,229.0')] ).
cnf(356,plain,
equal(rstore_tail(queue_179,index_180),q36),
inference(rew,[status(thm),theory(equality)],[313,227]),
[iquote('0:Rew:313.0,227.0')] ).
cnf(357,plain,
equal(rstore_tail(queue_173,index_174),q35),
inference(rew,[status(thm),theory(equality)],[312,225]),
[iquote('0:Rew:312.0,225.0')] ).
cnf(358,plain,
equal(rstore_tail(queue_167,index_168),q34),
inference(rew,[status(thm),theory(equality)],[311,222]),
[iquote('0:Rew:311.0,222.0')] ).
cnf(359,plain,
equal(rstore_tail(queue_161,index_162),q33),
inference(rew,[status(thm),theory(equality)],[310,220]),
[iquote('0:Rew:310.0,220.0')] ).
cnf(360,plain,
equal(rstore_tail(queue_155,index_156),q32),
inference(rew,[status(thm),theory(equality)],[309,218]),
[iquote('0:Rew:309.0,218.0')] ).
cnf(361,plain,
equal(rstore_tail(queue_149,index_150),q31),
inference(rew,[status(thm),theory(equality)],[308,216]),
[iquote('0:Rew:308.0,216.0')] ).
cnf(362,plain,
equal(rstore_tail(queue_143,index_144),q30),
inference(rew,[status(thm),theory(equality)],[307,214]),
[iquote('0:Rew:307.0,214.0')] ).
cnf(363,plain,
equal(rstore_tail(queue_137,index_138),q3),
inference(rew,[status(thm),theory(equality)],[306,212]),
[iquote('0:Rew:306.0,212.0')] ).
cnf(364,plain,
equal(rstore_tail(queue_131,index_132),q29),
inference(rew,[status(thm),theory(equality)],[305,210]),
[iquote('0:Rew:305.0,210.0')] ).
cnf(365,plain,
equal(rstore_tail(queue_11,index_12),q10),
inference(rew,[status(thm),theory(equality)],[285,208]),
[iquote('0:Rew:285.0,208.0')] ).
cnf(366,plain,
equal(rstore_tail(queue_125,index_126),q28),
inference(rew,[status(thm),theory(equality)],[304,207]),
[iquote('0:Rew:304.0,207.0')] ).
cnf(367,plain,
equal(rstore_tail(queue_119,index_120),q27),
inference(rew,[status(thm),theory(equality)],[303,205]),
[iquote('0:Rew:303.0,205.0')] ).
cnf(368,plain,
equal(rstore_tail(queue_113,index_114),q26),
inference(rew,[status(thm),theory(equality)],[302,203]),
[iquote('0:Rew:302.0,203.0')] ).
cnf(369,plain,
equal(rstore_tail(queue_107,index_108),q25),
inference(rew,[status(thm),theory(equality)],[301,200]),
[iquote('0:Rew:301.0,200.0')] ).
cnf(370,plain,
equal(rstore_tail(queue_101,index_102),q24),
inference(rew,[status(thm),theory(equality)],[300,198]),
[iquote('0:Rew:300.0,198.0')] ).
cnf(371,plain,
equal(rstore_head(q,index_0),q0),
inference(rew,[status(thm),theory(equality)],[283,196]),
[iquote('0:Rew:283.0,196.0')] ).
cnf(644,plain,
equal(p(index_96),index_93),
inference(spr,[status(thm),theory(equality)],[194,12]),
[iquote('0:SpR:194.0,12.0')] ).
cnf(645,plain,
equal(p(index_90),index_87),
inference(spr,[status(thm),theory(equality)],[192,12]),
[iquote('0:SpR:192.0,12.0')] ).
cnf(646,plain,
equal(p(index_84),index_81),
inference(spr,[status(thm),theory(equality)],[189,12]),
[iquote('0:SpR:189.0,12.0')] ).
cnf(647,plain,
equal(p(index_78),index_75),
inference(spr,[status(thm),theory(equality)],[187,12]),
[iquote('0:SpR:187.0,12.0')] ).
cnf(648,plain,
equal(p(index_72),index_69),
inference(spr,[status(thm),theory(equality)],[185,12]),
[iquote('0:SpR:185.0,12.0')] ).
cnf(649,plain,
equal(p(index_66),index_63),
inference(spr,[status(thm),theory(equality)],[183,12]),
[iquote('0:SpR:183.0,12.0')] ).
cnf(650,plain,
equal(p(index_60),index_57),
inference(spr,[status(thm),theory(equality)],[181,12]),
[iquote('0:SpR:181.0,12.0')] ).
cnf(651,plain,
equal(p(index_6),index_3),
inference(spr,[status(thm),theory(equality)],[180,12]),
[iquote('0:SpR:180.0,12.0')] ).
cnf(652,plain,
equal(p(index_54),index_51),
inference(spr,[status(thm),theory(equality)],[178,12]),
[iquote('0:SpR:178.0,12.0')] ).
cnf(653,plain,
equal(p(index_48),index_45),
inference(spr,[status(thm),theory(equality)],[176,12]),
[iquote('0:SpR:176.0,12.0')] ).
cnf(654,plain,
equal(p(index_42),index_39),
inference(spr,[status(thm),theory(equality)],[174,12]),
[iquote('0:SpR:174.0,12.0')] ).
cnf(655,plain,
equal(p(index_36),index_33),
inference(spr,[status(thm),theory(equality)],[172,12]),
[iquote('0:SpR:172.0,12.0')] ).
cnf(656,plain,
equal(p(index_30),index_27),
inference(spr,[status(thm),theory(equality)],[170,12]),
[iquote('0:SpR:170.0,12.0')] ).
cnf(657,plain,
equal(p(index_263),index_264),
inference(spr,[status(thm),theory(equality)],[167,12]),
[iquote('0:SpR:167.0,12.0')] ).
cnf(658,plain,
equal(p(index_258),index_255),
inference(spr,[status(thm),theory(equality)],[164,12]),
[iquote('0:SpR:164.0,12.0')] ).
cnf(659,plain,
equal(p(index_252),index_249),
inference(spr,[status(thm),theory(equality)],[162,12]),
[iquote('0:SpR:162.0,12.0')] ).
cnf(660,plain,
equal(p(index_246),index_243),
inference(spr,[status(thm),theory(equality)],[160,12]),
[iquote('0:SpR:160.0,12.0')] ).
cnf(661,plain,
equal(p(index_240),index_237),
inference(spr,[status(thm),theory(equality)],[158,12]),
[iquote('0:SpR:158.0,12.0')] ).
cnf(662,plain,
equal(p(index_24),index_21),
inference(spr,[status(thm),theory(equality)],[157,12]),
[iquote('0:SpR:157.0,12.0')] ).
cnf(663,plain,
equal(p(index_234),index_231),
inference(spr,[status(thm),theory(equality)],[155,12]),
[iquote('0:SpR:155.0,12.0')] ).
cnf(664,plain,
equal(p(index_228),index_225),
inference(spr,[status(thm),theory(equality)],[153,12]),
[iquote('0:SpR:153.0,12.0')] ).
cnf(668,plain,
equal(p(index_204),index_201),
inference(spr,[status(thm),theory(equality)],[144,12]),
[iquote('0:SpR:144.0,12.0')] ).
cnf(671,plain,
equal(p(index_186),index_183),
inference(spr,[status(thm),theory(equality)],[138,12]),
[iquote('0:SpR:138.0,12.0')] ).
cnf(673,plain,
equal(p(index_18),index_15),
inference(spr,[status(thm),theory(equality)],[135,12]),
[iquote('0:SpR:135.0,12.0')] ).
cnf(680,plain,
equal(p(index_138),index_135),
inference(spr,[status(thm),theory(equality)],[120,12]),
[iquote('0:SpR:120.0,12.0')] ).
cnf(684,plain,
equal(p(index_12),index_9),
inference(spr,[status(thm),theory(equality)],[113,12]),
[iquote('0:SpR:113.0,12.0')] ).
cnf(686,plain,
equal(p(index_108),index_105),
inference(spr,[status(thm),theory(equality)],[109,12]),
[iquote('0:SpR:109.0,12.0')] ).
cnf(687,plain,
equal(p(index_102),index_99),
inference(spr,[status(thm),theory(equality)],[107,12]),
[iquote('0:SpR:107.0,12.0')] ).
cnf(910,plain,
equal(s(s(u)),p(u)),
inference(spr,[status(thm),theory(equality)],[16,12]),
[iquote('0:SpR:16.0,12.0')] ).
cnf(1008,plain,
equal(rselect_tail(q23),index_96),
inference(spr,[status(thm),theory(equality)],[328,5]),
[iquote('0:SpR:328.0,5.0')] ).
cnf(1009,plain,
equal(rselect_tail(q22),index_90),
inference(spr,[status(thm),theory(equality)],[329,5]),
[iquote('0:SpR:329.0,5.0')] ).
cnf(1010,plain,
equal(rselect_tail(q21),index_84),
inference(spr,[status(thm),theory(equality)],[330,5]),
[iquote('0:SpR:330.0,5.0')] ).
cnf(1011,plain,
equal(rselect_tail(q20),index_78),
inference(spr,[status(thm),theory(equality)],[331,5]),
[iquote('0:SpR:331.0,5.0')] ).
cnf(1012,plain,
equal(rselect_tail(q2),index_72),
inference(spr,[status(thm),theory(equality)],[332,5]),
[iquote('0:SpR:332.0,5.0')] ).
cnf(1013,plain,
equal(rselect_tail(q1),index_6),
inference(spr,[status(thm),theory(equality)],[333,5]),
[iquote('0:SpR:333.0,5.0')] ).
cnf(1014,plain,
equal(rselect_tail(q19),index_66),
inference(spr,[status(thm),theory(equality)],[334,5]),
[iquote('0:SpR:334.0,5.0')] ).
cnf(1015,plain,
equal(rselect_tail(q18),index_60),
inference(spr,[status(thm),theory(equality)],[335,5]),
[iquote('0:SpR:335.0,5.0')] ).
cnf(1016,plain,
equal(rselect_tail(q17),index_54),
inference(spr,[status(thm),theory(equality)],[336,5]),
[iquote('0:SpR:336.0,5.0')] ).
cnf(1017,plain,
equal(rselect_tail(q16),index_48),
inference(spr,[status(thm),theory(equality)],[337,5]),
[iquote('0:SpR:337.0,5.0')] ).
cnf(1018,plain,
equal(rselect_tail(q15),index_42),
inference(spr,[status(thm),theory(equality)],[338,5]),
[iquote('0:SpR:338.0,5.0')] ).
cnf(1019,plain,
equal(rselect_tail(q14),index_36),
inference(spr,[status(thm),theory(equality)],[339,5]),
[iquote('0:SpR:339.0,5.0')] ).
cnf(1020,plain,
equal(rselect_tail(q13),index_30),
inference(spr,[status(thm),theory(equality)],[340,5]),
[iquote('0:SpR:340.0,5.0')] ).
cnf(1021,plain,
equal(rselect_tail(q9),index_258),
inference(spr,[status(thm),theory(equality)],[341,5]),
[iquote('0:SpR:341.0,5.0')] ).
cnf(1022,plain,
equal(rselect_tail(q8),index_252),
inference(spr,[status(thm),theory(equality)],[342,5]),
[iquote('0:SpR:342.0,5.0')] ).
cnf(1023,plain,
equal(rselect_tail(q12),index_24),
inference(spr,[status(thm),theory(equality)],[343,5]),
[iquote('0:SpR:343.0,5.0')] ).
cnf(1024,plain,
equal(rselect_tail(q7),index_246),
inference(spr,[status(thm),theory(equality)],[344,5]),
[iquote('0:SpR:344.0,5.0')] ).
cnf(1025,plain,
equal(rselect_tail(q6),index_240),
inference(spr,[status(thm),theory(equality)],[345,5]),
[iquote('0:SpR:345.0,5.0')] ).
cnf(1026,plain,
equal(rselect_tail(q5),index_234),
inference(spr,[status(thm),theory(equality)],[346,5]),
[iquote('0:SpR:346.0,5.0')] ).
cnf(1027,plain,
equal(rselect_tail(q43),index_228),
inference(spr,[status(thm),theory(equality)],[347,5]),
[iquote('0:SpR:347.0,5.0')] ).
cnf(1028,plain,
equal(rselect_tail(q42),index_222),
inference(spr,[status(thm),theory(equality)],[348,5]),
[iquote('0:SpR:348.0,5.0')] ).
cnf(1029,plain,
equal(rselect_tail(q41),index_216),
inference(spr,[status(thm),theory(equality)],[349,5]),
[iquote('0:SpR:349.0,5.0')] ).
cnf(1030,plain,
equal(rselect_tail(q40),index_210),
inference(spr,[status(thm),theory(equality)],[350,5]),
[iquote('0:SpR:350.0,5.0')] ).
cnf(1031,plain,
equal(rselect_tail(q4),index_204),
inference(spr,[status(thm),theory(equality)],[351,5]),
[iquote('0:SpR:351.0,5.0')] ).
cnf(1032,plain,
equal(rselect_tail(q39),index_198),
inference(spr,[status(thm),theory(equality)],[352,5]),
[iquote('0:SpR:352.0,5.0')] ).
cnf(1033,plain,
equal(rselect_tail(q38),index_192),
inference(spr,[status(thm),theory(equality)],[353,5]),
[iquote('0:SpR:353.0,5.0')] ).
cnf(1034,plain,
equal(rselect_tail(q11),index_18),
inference(spr,[status(thm),theory(equality)],[354,5]),
[iquote('0:SpR:354.0,5.0')] ).
cnf(1035,plain,
equal(rselect_tail(q37),index_186),
inference(spr,[status(thm),theory(equality)],[355,5]),
[iquote('0:SpR:355.0,5.0')] ).
cnf(1036,plain,
equal(rselect_tail(q36),index_180),
inference(spr,[status(thm),theory(equality)],[356,5]),
[iquote('0:SpR:356.0,5.0')] ).
cnf(1037,plain,
equal(rselect_tail(q35),index_174),
inference(spr,[status(thm),theory(equality)],[357,5]),
[iquote('0:SpR:357.0,5.0')] ).
cnf(1038,plain,
equal(rselect_tail(q34),index_168),
inference(spr,[status(thm),theory(equality)],[358,5]),
[iquote('0:SpR:358.0,5.0')] ).
cnf(1039,plain,
equal(rselect_tail(q33),index_162),
inference(spr,[status(thm),theory(equality)],[359,5]),
[iquote('0:SpR:359.0,5.0')] ).
cnf(1040,plain,
equal(rselect_tail(q32),index_156),
inference(spr,[status(thm),theory(equality)],[360,5]),
[iquote('0:SpR:360.0,5.0')] ).
cnf(1041,plain,
equal(rselect_tail(q31),index_150),
inference(spr,[status(thm),theory(equality)],[361,5]),
[iquote('0:SpR:361.0,5.0')] ).
cnf(1042,plain,
equal(rselect_tail(q30),index_144),
inference(spr,[status(thm),theory(equality)],[362,5]),
[iquote('0:SpR:362.0,5.0')] ).
cnf(1043,plain,
equal(rselect_tail(q3),index_138),
inference(spr,[status(thm),theory(equality)],[363,5]),
[iquote('0:SpR:363.0,5.0')] ).
cnf(1044,plain,
equal(rselect_tail(q29),index_132),
inference(spr,[status(thm),theory(equality)],[364,5]),
[iquote('0:SpR:364.0,5.0')] ).
cnf(1045,plain,
equal(rselect_tail(q10),index_12),
inference(spr,[status(thm),theory(equality)],[365,5]),
[iquote('0:SpR:365.0,5.0')] ).
cnf(1046,plain,
equal(rselect_tail(q28),index_126),
inference(spr,[status(thm),theory(equality)],[366,5]),
[iquote('0:SpR:366.0,5.0')] ).
cnf(1047,plain,
equal(rselect_tail(q27),index_120),
inference(spr,[status(thm),theory(equality)],[367,5]),
[iquote('0:SpR:367.0,5.0')] ).
cnf(1048,plain,
equal(rselect_tail(q26),index_114),
inference(spr,[status(thm),theory(equality)],[368,5]),
[iquote('0:SpR:368.0,5.0')] ).
cnf(1049,plain,
equal(rselect_tail(q25),index_108),
inference(spr,[status(thm),theory(equality)],[369,5]),
[iquote('0:SpR:369.0,5.0')] ).
cnf(1050,plain,
equal(rselect_tail(q24),index_102),
inference(spr,[status(thm),theory(equality)],[370,5]),
[iquote('0:SpR:370.0,5.0')] ).
cnf(1051,plain,
equal(index_96,index_99),
inference(rew,[status(thm),theory(equality)],[195,1008]),
[iquote('0:Rew:195.0,1008.0')] ).
cnf(1052,plain,
equal(s(index_93),index_99),
inference(rew,[status(thm),theory(equality)],[1051,194]),
[iquote('0:Rew:1051.0,194.0')] ).
cnf(1053,plain,
equal(rstore_tail(queue_95,index_99),q23),
inference(rew,[status(thm),theory(equality)],[1051,328]),
[iquote('0:Rew:1051.0,328.0')] ).
cnf(1054,plain,
equal(p(index_99),index_93),
inference(rew,[status(thm),theory(equality)],[1051,644]),
[iquote('0:Rew:1051.0,644.0')] ).
cnf(1056,plain,
equal(index_90,index_93),
inference(rew,[status(thm),theory(equality)],[193,1009]),
[iquote('0:Rew:193.0,1009.0')] ).
cnf(1057,plain,
equal(s(index_87),index_93),
inference(rew,[status(thm),theory(equality)],[1056,192]),
[iquote('0:Rew:1056.0,192.0')] ).
cnf(1058,plain,
equal(rstore_tail(queue_89,index_93),q22),
inference(rew,[status(thm),theory(equality)],[1056,329]),
[iquote('0:Rew:1056.0,329.0')] ).
cnf(1059,plain,
equal(p(index_93),index_87),
inference(rew,[status(thm),theory(equality)],[1056,645]),
[iquote('0:Rew:1056.0,645.0')] ).
cnf(1061,plain,
equal(index_84,index_87),
inference(rew,[status(thm),theory(equality)],[190,1010]),
[iquote('0:Rew:190.0,1010.0')] ).
cnf(1063,plain,
equal(rstore_tail(queue_83,index_87),q21),
inference(rew,[status(thm),theory(equality)],[1061,330]),
[iquote('0:Rew:1061.0,330.0')] ).
cnf(1064,plain,
equal(p(index_87),index_81),
inference(rew,[status(thm),theory(equality)],[1061,646]),
[iquote('0:Rew:1061.0,646.0')] ).
cnf(1066,plain,
equal(index_78,index_81),
inference(rew,[status(thm),theory(equality)],[188,1011]),
[iquote('0:Rew:188.0,1011.0')] ).
cnf(1068,plain,
equal(rstore_tail(queue_77,index_81),q20),
inference(rew,[status(thm),theory(equality)],[1066,331]),
[iquote('0:Rew:1066.0,331.0')] ).
cnf(1069,plain,
equal(p(index_81),index_75),
inference(rew,[status(thm),theory(equality)],[1066,647]),
[iquote('0:Rew:1066.0,647.0')] ).
cnf(1071,plain,
equal(index_72,index_135),
inference(rew,[status(thm),theory(equality)],[119,1012]),
[iquote('0:Rew:119.0,1012.0')] ).
cnf(1073,plain,
equal(rstore_tail(queue_71,index_135),q2),
inference(rew,[status(thm),theory(equality)],[1071,332]),
[iquote('0:Rew:1071.0,332.0')] ).
cnf(1074,plain,
equal(p(index_135),index_69),
inference(rew,[status(thm),theory(equality)],[1071,648]),
[iquote('0:Rew:1071.0,648.0')] ).
cnf(1076,plain,
equal(index_6,index_69),
inference(rew,[status(thm),theory(equality)],[184,1013]),
[iquote('0:Rew:184.0,1013.0')] ).
cnf(1078,plain,
equal(rstore_tail(queue_5,index_69),q1),
inference(rew,[status(thm),theory(equality)],[1076,333]),
[iquote('0:Rew:1076.0,333.0')] ).
cnf(1079,plain,
equal(p(index_69),index_3),
inference(rew,[status(thm),theory(equality)],[1076,651]),
[iquote('0:Rew:1076.0,651.0')] ).
cnf(1081,plain,
equal(index_66,index_75),
inference(rew,[status(thm),theory(equality)],[186,1014]),
[iquote('0:Rew:186.0,1014.0')] ).
cnf(1083,plain,
equal(rstore_tail(queue_65,index_75),q19),
inference(rew,[status(thm),theory(equality)],[1081,334]),
[iquote('0:Rew:1081.0,334.0')] ).
cnf(1084,plain,
equal(p(index_75),index_63),
inference(rew,[status(thm),theory(equality)],[1081,649]),
[iquote('0:Rew:1081.0,649.0')] ).
cnf(1086,plain,
equal(index_60,index_63),
inference(rew,[status(thm),theory(equality)],[182,1015]),
[iquote('0:Rew:182.0,1015.0')] ).
cnf(1088,plain,
equal(rstore_tail(queue_59,index_63),q18),
inference(rew,[status(thm),theory(equality)],[1086,335]),
[iquote('0:Rew:1086.0,335.0')] ).
cnf(1089,plain,
equal(p(index_63),index_57),
inference(rew,[status(thm),theory(equality)],[1086,650]),
[iquote('0:Rew:1086.0,650.0')] ).
cnf(1091,plain,
equal(index_54,index_57),
inference(rew,[status(thm),theory(equality)],[179,1016]),
[iquote('0:Rew:179.0,1016.0')] ).
cnf(1093,plain,
equal(rstore_tail(queue_53,index_57),q17),
inference(rew,[status(thm),theory(equality)],[1091,336]),
[iquote('0:Rew:1091.0,336.0')] ).
cnf(1094,plain,
equal(p(index_57),index_51),
inference(rew,[status(thm),theory(equality)],[1091,652]),
[iquote('0:Rew:1091.0,652.0')] ).
cnf(1096,plain,
equal(index_48,index_51),
inference(rew,[status(thm),theory(equality)],[177,1017]),
[iquote('0:Rew:177.0,1017.0')] ).
cnf(1098,plain,
equal(rstore_tail(queue_47,index_51),q16),
inference(rew,[status(thm),theory(equality)],[1096,337]),
[iquote('0:Rew:1096.0,337.0')] ).
cnf(1099,plain,
equal(p(index_51),index_45),
inference(rew,[status(thm),theory(equality)],[1096,653]),
[iquote('0:Rew:1096.0,653.0')] ).
cnf(1101,plain,
equal(index_42,index_45),
inference(rew,[status(thm),theory(equality)],[175,1018]),
[iquote('0:Rew:175.0,1018.0')] ).
cnf(1103,plain,
equal(rstore_tail(queue_41,index_45),q15),
inference(rew,[status(thm),theory(equality)],[1101,338]),
[iquote('0:Rew:1101.0,338.0')] ).
cnf(1104,plain,
equal(p(index_45),index_39),
inference(rew,[status(thm),theory(equality)],[1101,654]),
[iquote('0:Rew:1101.0,654.0')] ).
cnf(1106,plain,
equal(index_36,index_39),
inference(rew,[status(thm),theory(equality)],[173,1019]),
[iquote('0:Rew:173.0,1019.0')] ).
cnf(1108,plain,
equal(rstore_tail(queue_35,index_39),q14),
inference(rew,[status(thm),theory(equality)],[1106,339]),
[iquote('0:Rew:1106.0,339.0')] ).
cnf(1109,plain,
equal(p(index_39),index_33),
inference(rew,[status(thm),theory(equality)],[1106,655]),
[iquote('0:Rew:1106.0,655.0')] ).
cnf(1111,plain,
equal(index_30,index_33),
inference(rew,[status(thm),theory(equality)],[171,1020]),
[iquote('0:Rew:171.0,1020.0')] ).
cnf(1113,plain,
equal(rstore_tail(queue_29,index_33),q13),
inference(rew,[status(thm),theory(equality)],[1111,340]),
[iquote('0:Rew:1111.0,340.0')] ).
cnf(1114,plain,
equal(p(index_33),index_27),
inference(rew,[status(thm),theory(equality)],[1111,656]),
[iquote('0:Rew:1111.0,656.0')] ).
cnf(1116,plain,
equal(index_258,index_9),
inference(rew,[status(thm),theory(equality)],[191,1021]),
[iquote('0:Rew:191.0,1021.0')] ).
cnf(1118,plain,
equal(rstore_tail(queue_257,index_9),q9),
inference(rew,[status(thm),theory(equality)],[1116,341]),
[iquote('0:Rew:1116.0,341.0')] ).
cnf(1119,plain,
equal(p(index_9),index_255),
inference(rew,[status(thm),theory(equality)],[1116,658]),
[iquote('0:Rew:1116.0,658.0')] ).
cnf(1121,plain,
equal(index_252,index_255),
inference(rew,[status(thm),theory(equality)],[163,1022]),
[iquote('0:Rew:163.0,1022.0')] ).
cnf(1123,plain,
equal(rstore_tail(queue_251,index_255),q8),
inference(rew,[status(thm),theory(equality)],[1121,342]),
[iquote('0:Rew:1121.0,342.0')] ).
cnf(1124,plain,
equal(p(index_255),index_249),
inference(rew,[status(thm),theory(equality)],[1121,659]),
[iquote('0:Rew:1121.0,659.0')] ).
cnf(1126,plain,
equal(index_24,index_27),
inference(rew,[status(thm),theory(equality)],[168,1023]),
[iquote('0:Rew:168.0,1023.0')] ).
cnf(1128,plain,
equal(rstore_tail(queue_23,index_27),q12),
inference(rew,[status(thm),theory(equality)],[1126,343]),
[iquote('0:Rew:1126.0,343.0')] ).
cnf(1129,plain,
equal(p(index_27),index_21),
inference(rew,[status(thm),theory(equality)],[1126,662]),
[iquote('0:Rew:1126.0,662.0')] ).
cnf(1131,plain,
equal(index_246,index_249),
inference(rew,[status(thm),theory(equality)],[161,1024]),
[iquote('0:Rew:161.0,1024.0')] ).
cnf(1133,plain,
equal(rstore_tail(queue_245,index_249),q7),
inference(rew,[status(thm),theory(equality)],[1131,344]),
[iquote('0:Rew:1131.0,344.0')] ).
cnf(1134,plain,
equal(p(index_249),index_243),
inference(rew,[status(thm),theory(equality)],[1131,660]),
[iquote('0:Rew:1131.0,660.0')] ).
cnf(1136,plain,
equal(index_240,index_243),
inference(rew,[status(thm),theory(equality)],[159,1025]),
[iquote('0:Rew:159.0,1025.0')] ).
cnf(1138,plain,
equal(rstore_tail(queue_239,index_243),q6),
inference(rew,[status(thm),theory(equality)],[1136,345]),
[iquote('0:Rew:1136.0,345.0')] ).
cnf(1139,plain,
equal(p(index_243),index_237),
inference(rew,[status(thm),theory(equality)],[1136,661]),
[iquote('0:Rew:1136.0,661.0')] ).
cnf(1141,plain,
equal(index_234,index_237),
inference(rew,[status(thm),theory(equality)],[156,1026]),
[iquote('0:Rew:156.0,1026.0')] ).
cnf(1143,plain,
equal(rstore_tail(queue_233,index_237),q5),
inference(rew,[status(thm),theory(equality)],[1141,346]),
[iquote('0:Rew:1141.0,346.0')] ).
cnf(1144,plain,
equal(p(index_237),index_231),
inference(rew,[status(thm),theory(equality)],[1141,663]),
[iquote('0:Rew:1141.0,663.0')] ).
cnf(1146,plain,
equal(index_263,index_228),
inference(rew,[status(thm),theory(equality)],[166,1027]),
[iquote('0:Rew:166.0,1027.0')] ).
cnf(1149,plain,
equal(p(index_228),index_264),
inference(rew,[status(thm),theory(equality)],[1146,657]),
[iquote('0:Rew:1146.0,657.0')] ).
cnf(1151,plain,
equal(index_222,index_225),
inference(rew,[status(thm),theory(equality)],[152,1028]),
[iquote('0:Rew:152.0,1028.0')] ).
cnf(1152,plain,
equal(s(index_219),index_225),
inference(rew,[status(thm),theory(equality)],[1151,151]),
[iquote('0:Rew:1151.0,151.0')] ).
cnf(1153,plain,
equal(rstore_tail(queue_221,index_225),q42),
inference(rew,[status(thm),theory(equality)],[1151,348]),
[iquote('0:Rew:1151.0,348.0')] ).
cnf(1156,plain,
equal(index_216,index_219),
inference(rew,[status(thm),theory(equality)],[150,1029]),
[iquote('0:Rew:150.0,1029.0')] ).
cnf(1157,plain,
equal(s(index_213),index_219),
inference(rew,[status(thm),theory(equality)],[1156,149]),
[iquote('0:Rew:1156.0,149.0')] ).
cnf(1158,plain,
equal(rstore_tail(queue_215,index_219),q41),
inference(rew,[status(thm),theory(equality)],[1156,349]),
[iquote('0:Rew:1156.0,349.0')] ).
cnf(1161,plain,
equal(index_210,index_213),
inference(rew,[status(thm),theory(equality)],[148,1030]),
[iquote('0:Rew:148.0,1030.0')] ).
cnf(1162,plain,
equal(s(index_207),index_213),
inference(rew,[status(thm),theory(equality)],[1161,147]),
[iquote('0:Rew:1161.0,147.0')] ).
cnf(1163,plain,
equal(rstore_tail(queue_209,index_213),q40),
inference(rew,[status(thm),theory(equality)],[1161,350]),
[iquote('0:Rew:1161.0,350.0')] ).
cnf(1166,plain,
equal(index_204,index_231),
inference(rew,[status(thm),theory(equality)],[154,1031]),
[iquote('0:Rew:154.0,1031.0')] ).
cnf(1168,plain,
equal(rstore_tail(queue_203,index_231),q4),
inference(rew,[status(thm),theory(equality)],[1166,351]),
[iquote('0:Rew:1166.0,351.0')] ).
cnf(1169,plain,
equal(p(index_231),index_201),
inference(rew,[status(thm),theory(equality)],[1166,668]),
[iquote('0:Rew:1166.0,668.0')] ).
cnf(1171,plain,
equal(index_198,index_207),
inference(rew,[status(thm),theory(equality)],[145,1032]),
[iquote('0:Rew:145.0,1032.0')] ).
cnf(1172,plain,
equal(s(index_195),index_207),
inference(rew,[status(thm),theory(equality)],[1171,142]),
[iquote('0:Rew:1171.0,142.0')] ).
cnf(1173,plain,
equal(rstore_tail(queue_197,index_207),q39),
inference(rew,[status(thm),theory(equality)],[1171,352]),
[iquote('0:Rew:1171.0,352.0')] ).
cnf(1176,plain,
equal(index_192,index_195),
inference(rew,[status(thm),theory(equality)],[141,1033]),
[iquote('0:Rew:141.0,1033.0')] ).
cnf(1177,plain,
equal(s(index_189),index_195),
inference(rew,[status(thm),theory(equality)],[1176,140]),
[iquote('0:Rew:1176.0,140.0')] ).
cnf(1178,plain,
equal(rstore_tail(queue_191,index_195),q38),
inference(rew,[status(thm),theory(equality)],[1176,353]),
[iquote('0:Rew:1176.0,353.0')] ).
cnf(1181,plain,
equal(index_18,index_21),
inference(rew,[status(thm),theory(equality)],[146,1034]),
[iquote('0:Rew:146.0,1034.0')] ).
cnf(1183,plain,
equal(rstore_tail(queue_17,index_21),q11),
inference(rew,[status(thm),theory(equality)],[1181,354]),
[iquote('0:Rew:1181.0,354.0')] ).
cnf(1184,plain,
equal(p(index_21),index_15),
inference(rew,[status(thm),theory(equality)],[1181,673]),
[iquote('0:Rew:1181.0,673.0')] ).
cnf(1186,plain,
equal(index_186,index_189),
inference(rew,[status(thm),theory(equality)],[139,1035]),
[iquote('0:Rew:139.0,1035.0')] ).
cnf(1187,plain,
equal(s(index_183),index_189),
inference(rew,[status(thm),theory(equality)],[1186,138]),
[iquote('0:Rew:1186.0,138.0')] ).
cnf(1188,plain,
equal(rstore_tail(queue_185,index_189),q37),
inference(rew,[status(thm),theory(equality)],[1186,355]),
[iquote('0:Rew:1186.0,355.0')] ).
cnf(1189,plain,
equal(p(index_189),index_183),
inference(rew,[status(thm),theory(equality)],[1186,671]),
[iquote('0:Rew:1186.0,671.0')] ).
cnf(1191,plain,
equal(index_180,index_183),
inference(rew,[status(thm),theory(equality)],[137,1036]),
[iquote('0:Rew:137.0,1036.0')] ).
cnf(1192,plain,
equal(s(index_177),index_183),
inference(rew,[status(thm),theory(equality)],[1191,136]),
[iquote('0:Rew:1191.0,136.0')] ).
cnf(1193,plain,
equal(rstore_tail(queue_179,index_183),q36),
inference(rew,[status(thm),theory(equality)],[1191,356]),
[iquote('0:Rew:1191.0,356.0')] ).
cnf(1196,plain,
equal(index_174,index_177),
inference(rew,[status(thm),theory(equality)],[134,1037]),
[iquote('0:Rew:134.0,1037.0')] ).
cnf(1197,plain,
equal(s(index_171),index_177),
inference(rew,[status(thm),theory(equality)],[1196,133]),
[iquote('0:Rew:1196.0,133.0')] ).
cnf(1198,plain,
equal(rstore_tail(queue_173,index_177),q35),
inference(rew,[status(thm),theory(equality)],[1196,357]),
[iquote('0:Rew:1196.0,357.0')] ).
cnf(1201,plain,
equal(index_168,index_171),
inference(rew,[status(thm),theory(equality)],[132,1038]),
[iquote('0:Rew:132.0,1038.0')] ).
cnf(1202,plain,
equal(s(index_165),index_171),
inference(rew,[status(thm),theory(equality)],[1201,131]),
[iquote('0:Rew:1201.0,131.0')] ).
cnf(1203,plain,
equal(rstore_tail(queue_167,index_171),q34),
inference(rew,[status(thm),theory(equality)],[1201,358]),
[iquote('0:Rew:1201.0,358.0')] ).
cnf(1206,plain,
equal(index_162,index_165),
inference(rew,[status(thm),theory(equality)],[130,1039]),
[iquote('0:Rew:130.0,1039.0')] ).
cnf(1207,plain,
equal(s(index_159),index_165),
inference(rew,[status(thm),theory(equality)],[1206,129]),
[iquote('0:Rew:1206.0,129.0')] ).
cnf(1208,plain,
equal(rstore_tail(queue_161,index_165),q33),
inference(rew,[status(thm),theory(equality)],[1206,359]),
[iquote('0:Rew:1206.0,359.0')] ).
cnf(1211,plain,
equal(index_156,index_159),
inference(rew,[status(thm),theory(equality)],[128,1040]),
[iquote('0:Rew:128.0,1040.0')] ).
cnf(1212,plain,
equal(s(index_153),index_159),
inference(rew,[status(thm),theory(equality)],[1211,127]),
[iquote('0:Rew:1211.0,127.0')] ).
cnf(1213,plain,
equal(rstore_tail(queue_155,index_159),q32),
inference(rew,[status(thm),theory(equality)],[1211,360]),
[iquote('0:Rew:1211.0,360.0')] ).
cnf(1216,plain,
equal(index_150,index_153),
inference(rew,[status(thm),theory(equality)],[126,1041]),
[iquote('0:Rew:126.0,1041.0')] ).
cnf(1217,plain,
equal(s(index_147),index_153),
inference(rew,[status(thm),theory(equality)],[1216,125]),
[iquote('0:Rew:1216.0,125.0')] ).
cnf(1218,plain,
equal(rstore_tail(queue_149,index_153),q31),
inference(rew,[status(thm),theory(equality)],[1216,361]),
[iquote('0:Rew:1216.0,361.0')] ).
cnf(1221,plain,
equal(index_144,index_147),
inference(rew,[status(thm),theory(equality)],[123,1042]),
[iquote('0:Rew:123.0,1042.0')] ).
cnf(1222,plain,
equal(s(index_141),index_147),
inference(rew,[status(thm),theory(equality)],[1221,122]),
[iquote('0:Rew:1221.0,122.0')] ).
cnf(1223,plain,
equal(rstore_tail(queue_143,index_147),q30),
inference(rew,[status(thm),theory(equality)],[1221,362]),
[iquote('0:Rew:1221.0,362.0')] ).
cnf(1226,plain,
equal(index_138,index_201),
inference(rew,[status(thm),theory(equality)],[143,1043]),
[iquote('0:Rew:143.0,1043.0')] ).
cnf(1228,plain,
equal(rstore_tail(queue_137,index_201),q3),
inference(rew,[status(thm),theory(equality)],[1226,363]),
[iquote('0:Rew:1226.0,363.0')] ).
cnf(1229,plain,
equal(p(index_201),index_135),
inference(rew,[status(thm),theory(equality)],[1226,680]),
[iquote('0:Rew:1226.0,680.0')] ).
cnf(1231,plain,
equal(index_132,index_141),
inference(rew,[status(thm),theory(equality)],[121,1044]),
[iquote('0:Rew:121.0,1044.0')] ).
cnf(1232,plain,
equal(s(index_129),index_141),
inference(rew,[status(thm),theory(equality)],[1231,118]),
[iquote('0:Rew:1231.0,118.0')] ).
cnf(1233,plain,
equal(rstore_tail(queue_131,index_141),q29),
inference(rew,[status(thm),theory(equality)],[1231,364]),
[iquote('0:Rew:1231.0,364.0')] ).
cnf(1236,plain,
equal(index_12,index_15),
inference(rew,[status(thm),theory(equality)],[124,1045]),
[iquote('0:Rew:124.0,1045.0')] ).
cnf(1237,plain,
equal(s(index_9),index_15),
inference(rew,[status(thm),theory(equality)],[1236,113]),
[iquote('0:Rew:1236.0,113.0')] ).
cnf(1238,plain,
equal(rstore_tail(queue_11,index_15),q10),
inference(rew,[status(thm),theory(equality)],[1236,365]),
[iquote('0:Rew:1236.0,365.0')] ).
cnf(1239,plain,
equal(p(index_15),index_9),
inference(rew,[status(thm),theory(equality)],[1236,684]),
[iquote('0:Rew:1236.0,684.0')] ).
cnf(1241,plain,
equal(index_126,index_129),
inference(rew,[status(thm),theory(equality)],[117,1046]),
[iquote('0:Rew:117.0,1046.0')] ).
cnf(1242,plain,
equal(s(index_123),index_129),
inference(rew,[status(thm),theory(equality)],[1241,116]),
[iquote('0:Rew:1241.0,116.0')] ).
cnf(1243,plain,
equal(rstore_tail(queue_125,index_129),q28),
inference(rew,[status(thm),theory(equality)],[1241,366]),
[iquote('0:Rew:1241.0,366.0')] ).
cnf(1246,plain,
equal(index_120,index_123),
inference(rew,[status(thm),theory(equality)],[115,1047]),
[iquote('0:Rew:115.0,1047.0')] ).
cnf(1247,plain,
equal(s(index_117),index_123),
inference(rew,[status(thm),theory(equality)],[1246,114]),
[iquote('0:Rew:1246.0,114.0')] ).
cnf(1248,plain,
equal(rstore_tail(queue_119,index_123),q27),
inference(rew,[status(thm),theory(equality)],[1246,367]),
[iquote('0:Rew:1246.0,367.0')] ).
cnf(1251,plain,
equal(index_114,index_117),
inference(rew,[status(thm),theory(equality)],[112,1048]),
[iquote('0:Rew:112.0,1048.0')] ).
cnf(1252,plain,
equal(s(index_111),index_117),
inference(rew,[status(thm),theory(equality)],[1251,111]),
[iquote('0:Rew:1251.0,111.0')] ).
cnf(1253,plain,
equal(rstore_tail(queue_113,index_117),q26),
inference(rew,[status(thm),theory(equality)],[1251,368]),
[iquote('0:Rew:1251.0,368.0')] ).
cnf(1256,plain,
equal(index_108,index_111),
inference(rew,[status(thm),theory(equality)],[110,1049]),
[iquote('0:Rew:110.0,1049.0')] ).
cnf(1257,plain,
equal(s(index_105),index_111),
inference(rew,[status(thm),theory(equality)],[1256,109]),
[iquote('0:Rew:1256.0,109.0')] ).
cnf(1258,plain,
equal(rstore_tail(queue_107,index_111),q25),
inference(rew,[status(thm),theory(equality)],[1256,369]),
[iquote('0:Rew:1256.0,369.0')] ).
cnf(1259,plain,
equal(p(index_111),index_105),
inference(rew,[status(thm),theory(equality)],[1256,686]),
[iquote('0:Rew:1256.0,686.0')] ).
cnf(1261,plain,
equal(index_102,index_105),
inference(rew,[status(thm),theory(equality)],[108,1050]),
[iquote('0:Rew:108.0,1050.0')] ).
cnf(1262,plain,
equal(s(index_99),index_105),
inference(rew,[status(thm),theory(equality)],[1261,107]),
[iquote('0:Rew:1261.0,107.0')] ).
cnf(1263,plain,
equal(rstore_tail(queue_101,index_105),q24),
inference(rew,[status(thm),theory(equality)],[1261,370]),
[iquote('0:Rew:1261.0,370.0')] ).
cnf(1264,plain,
equal(p(index_105),index_99),
inference(rew,[status(thm),theory(equality)],[1261,687]),
[iquote('0:Rew:1261.0,687.0')] ).
cnf(1266,plain,
equal(index_264,index_225),
inference(rew,[status(thm),theory(equality)],[664,1149]),
[iquote('0:Rew:664.0,1149.0')] ).
cnf(1267,plain,
equal(select(earray_260,index_225),elem_265),
inference(rew,[status(thm),theory(equality)],[1266,105]),
[iquote('0:Rew:1266.0,105.0')] ).
cnf(1653,plain,
equal(rselect_head(q0),index_0),
inference(spr,[status(thm),theory(equality)],[371,4]),
[iquote('0:SpR:371.0,4.0')] ).
cnf(1660,plain,
equal(p(index_93),s(index_99)),
inference(spr,[status(thm),theory(equality)],[1052,910]),
[iquote('0:SpR:1052.0,910.0')] ).
cnf(1704,plain,
equal(index_87,index_105),
inference(rew,[status(thm),theory(equality)],[1059,1660,1262]),
[iquote('0:Rew:1059.0,1660.0,1262.0,1660.0')] ).
cnf(1708,plain,
equal(s(index_105),index_93),
inference(rew,[status(thm),theory(equality)],[1704,1057]),
[iquote('0:Rew:1704.0,1057.0')] ).
cnf(1712,plain,
equal(p(index_105),index_81),
inference(rew,[status(thm),theory(equality)],[1704,1064]),
[iquote('0:Rew:1704.0,1064.0')] ).
cnf(1714,plain,
equal(rstore_tail(queue_83,index_105),q21),
inference(rew,[status(thm),theory(equality)],[1704,1063]),
[iquote('0:Rew:1704.0,1063.0')] ).
cnf(1715,plain,
equal(index_93,index_111),
inference(rew,[status(thm),theory(equality)],[1257,1708]),
[iquote('0:Rew:1257.0,1708.0')] ).
cnf(1719,plain,
equal(s(index_111),index_99),
inference(rew,[status(thm),theory(equality)],[1715,1052]),
[iquote('0:Rew:1715.0,1052.0')] ).
cnf(1720,plain,
equal(p(index_99),index_111),
inference(rew,[status(thm),theory(equality)],[1715,1054]),
[iquote('0:Rew:1715.0,1054.0')] ).
cnf(1722,plain,
equal(rstore_tail(queue_89,index_111),q22),
inference(rew,[status(thm),theory(equality)],[1715,1058]),
[iquote('0:Rew:1715.0,1058.0')] ).
cnf(1725,plain,
equal(index_81,index_99),
inference(rew,[status(thm),theory(equality)],[1264,1712]),
[iquote('0:Rew:1264.0,1712.0')] ).
cnf(1730,plain,
equal(p(index_99),index_75),
inference(rew,[status(thm),theory(equality)],[1725,1069]),
[iquote('0:Rew:1725.0,1069.0')] ).
cnf(1732,plain,
equal(rstore_tail(queue_77,index_99),q20),
inference(rew,[status(thm),theory(equality)],[1725,1068]),
[iquote('0:Rew:1725.0,1068.0')] ).
cnf(1735,plain,
equal(index_117,index_99),
inference(rew,[status(thm),theory(equality)],[1252,1719]),
[iquote('0:Rew:1252.0,1719.0')] ).
cnf(1739,plain,
equal(s(index_99),index_123),
inference(rew,[status(thm),theory(equality)],[1735,1247]),
[iquote('0:Rew:1735.0,1247.0')] ).
cnf(1742,plain,
equal(s(index_111),index_99),
inference(rew,[status(thm),theory(equality)],[1735,1252]),
[iquote('0:Rew:1735.0,1252.0')] ).
cnf(1745,plain,
equal(rstore_tail(queue_113,index_99),q26),
inference(rew,[status(thm),theory(equality)],[1735,1253]),
[iquote('0:Rew:1735.0,1253.0')] ).
cnf(1746,plain,
equal(index_75,index_111),
inference(rew,[status(thm),theory(equality)],[1720,1730]),
[iquote('0:Rew:1720.0,1730.0')] ).
cnf(1751,plain,
equal(p(index_111),index_63),
inference(rew,[status(thm),theory(equality)],[1746,1084]),
[iquote('0:Rew:1746.0,1084.0')] ).
cnf(1753,plain,
equal(rstore_tail(queue_65,index_111),q19),
inference(rew,[status(thm),theory(equality)],[1746,1083]),
[iquote('0:Rew:1746.0,1083.0')] ).
cnf(1756,plain,
equal(index_123,index_105),
inference(rew,[status(thm),theory(equality)],[1262,1739]),
[iquote('0:Rew:1262.0,1739.0')] ).
cnf(1760,plain,
equal(s(index_105),index_129),
inference(rew,[status(thm),theory(equality)],[1756,1242]),
[iquote('0:Rew:1756.0,1242.0')] ).
cnf(1763,plain,
equal(rstore_tail(queue_119,index_105),q27),
inference(rew,[status(thm),theory(equality)],[1756,1248]),
[iquote('0:Rew:1756.0,1248.0')] ).
cnf(1766,plain,
equal(index_63,index_105),
inference(rew,[status(thm),theory(equality)],[1259,1751]),
[iquote('0:Rew:1259.0,1751.0')] ).
cnf(1771,plain,
equal(p(index_105),index_57),
inference(rew,[status(thm),theory(equality)],[1766,1089]),
[iquote('0:Rew:1766.0,1089.0')] ).
cnf(1773,plain,
equal(rstore_tail(queue_59,index_105),q18),
inference(rew,[status(thm),theory(equality)],[1766,1088]),
[iquote('0:Rew:1766.0,1088.0')] ).
cnf(1776,plain,
equal(index_129,index_111),
inference(rew,[status(thm),theory(equality)],[1257,1760]),
[iquote('0:Rew:1257.0,1760.0')] ).
cnf(1780,plain,
equal(s(index_111),index_141),
inference(rew,[status(thm),theory(equality)],[1776,1232]),
[iquote('0:Rew:1776.0,1232.0')] ).
cnf(1783,plain,
equal(rstore_tail(queue_125,index_111),q28),
inference(rew,[status(thm),theory(equality)],[1776,1243]),
[iquote('0:Rew:1776.0,1243.0')] ).
cnf(1786,plain,
equal(index_57,index_99),
inference(rew,[status(thm),theory(equality)],[1264,1771]),
[iquote('0:Rew:1264.0,1771.0')] ).
cnf(1791,plain,
equal(p(index_99),index_51),
inference(rew,[status(thm),theory(equality)],[1786,1094]),
[iquote('0:Rew:1786.0,1094.0')] ).
cnf(1793,plain,
equal(rstore_tail(queue_53,index_99),q17),
inference(rew,[status(thm),theory(equality)],[1786,1093]),
[iquote('0:Rew:1786.0,1093.0')] ).
cnf(1796,plain,
equal(index_141,index_99),
inference(rew,[status(thm),theory(equality)],[1742,1780]),
[iquote('0:Rew:1742.0,1780.0')] ).
cnf(1800,plain,
equal(s(index_99),index_147),
inference(rew,[status(thm),theory(equality)],[1796,1222]),
[iquote('0:Rew:1796.0,1222.0')] ).
cnf(1803,plain,
equal(rstore_tail(queue_131,index_99),q29),
inference(rew,[status(thm),theory(equality)],[1796,1233]),
[iquote('0:Rew:1796.0,1233.0')] ).
cnf(1806,plain,
equal(index_51,index_111),
inference(rew,[status(thm),theory(equality)],[1720,1791]),
[iquote('0:Rew:1720.0,1791.0')] ).
cnf(1811,plain,
equal(p(index_111),index_45),
inference(rew,[status(thm),theory(equality)],[1806,1099]),
[iquote('0:Rew:1806.0,1099.0')] ).
cnf(1813,plain,
equal(rstore_tail(queue_47,index_111),q16),
inference(rew,[status(thm),theory(equality)],[1806,1098]),
[iquote('0:Rew:1806.0,1098.0')] ).
cnf(1816,plain,
equal(index_147,index_105),
inference(rew,[status(thm),theory(equality)],[1262,1800]),
[iquote('0:Rew:1262.0,1800.0')] ).
cnf(1820,plain,
equal(s(index_105),index_153),
inference(rew,[status(thm),theory(equality)],[1816,1217]),
[iquote('0:Rew:1816.0,1217.0')] ).
cnf(1823,plain,
equal(rstore_tail(queue_143,index_105),q30),
inference(rew,[status(thm),theory(equality)],[1816,1223]),
[iquote('0:Rew:1816.0,1223.0')] ).
cnf(1826,plain,
equal(index_45,index_105),
inference(rew,[status(thm),theory(equality)],[1259,1811]),
[iquote('0:Rew:1259.0,1811.0')] ).
cnf(1831,plain,
equal(p(index_105),index_39),
inference(rew,[status(thm),theory(equality)],[1826,1104]),
[iquote('0:Rew:1826.0,1104.0')] ).
cnf(1833,plain,
equal(rstore_tail(queue_41,index_105),q15),
inference(rew,[status(thm),theory(equality)],[1826,1103]),
[iquote('0:Rew:1826.0,1103.0')] ).
cnf(1836,plain,
equal(index_153,index_111),
inference(rew,[status(thm),theory(equality)],[1257,1820]),
[iquote('0:Rew:1257.0,1820.0')] ).
cnf(1840,plain,
equal(s(index_111),index_159),
inference(rew,[status(thm),theory(equality)],[1836,1212]),
[iquote('0:Rew:1836.0,1212.0')] ).
cnf(1843,plain,
equal(rstore_tail(queue_149,index_111),q31),
inference(rew,[status(thm),theory(equality)],[1836,1218]),
[iquote('0:Rew:1836.0,1218.0')] ).
cnf(1846,plain,
equal(index_39,index_99),
inference(rew,[status(thm),theory(equality)],[1264,1831]),
[iquote('0:Rew:1264.0,1831.0')] ).
cnf(1851,plain,
equal(p(index_99),index_33),
inference(rew,[status(thm),theory(equality)],[1846,1109]),
[iquote('0:Rew:1846.0,1109.0')] ).
cnf(1853,plain,
equal(rstore_tail(queue_35,index_99),q14),
inference(rew,[status(thm),theory(equality)],[1846,1108]),
[iquote('0:Rew:1846.0,1108.0')] ).
cnf(1856,plain,
equal(index_159,index_99),
inference(rew,[status(thm),theory(equality)],[1742,1840]),
[iquote('0:Rew:1742.0,1840.0')] ).
cnf(1860,plain,
equal(s(index_99),index_165),
inference(rew,[status(thm),theory(equality)],[1856,1207]),
[iquote('0:Rew:1856.0,1207.0')] ).
cnf(1863,plain,
equal(rstore_tail(queue_155,index_99),q32),
inference(rew,[status(thm),theory(equality)],[1856,1213]),
[iquote('0:Rew:1856.0,1213.0')] ).
cnf(1866,plain,
equal(index_33,index_111),
inference(rew,[status(thm),theory(equality)],[1720,1851]),
[iquote('0:Rew:1720.0,1851.0')] ).
cnf(1871,plain,
equal(p(index_111),index_27),
inference(rew,[status(thm),theory(equality)],[1866,1114]),
[iquote('0:Rew:1866.0,1114.0')] ).
cnf(1873,plain,
equal(rstore_tail(queue_29,index_111),q13),
inference(rew,[status(thm),theory(equality)],[1866,1113]),
[iquote('0:Rew:1866.0,1113.0')] ).
cnf(1876,plain,
equal(index_165,index_105),
inference(rew,[status(thm),theory(equality)],[1262,1860]),
[iquote('0:Rew:1262.0,1860.0')] ).
cnf(1880,plain,
equal(s(index_105),index_171),
inference(rew,[status(thm),theory(equality)],[1876,1202]),
[iquote('0:Rew:1876.0,1202.0')] ).
cnf(1883,plain,
equal(rstore_tail(queue_161,index_105),q33),
inference(rew,[status(thm),theory(equality)],[1876,1208]),
[iquote('0:Rew:1876.0,1208.0')] ).
cnf(1886,plain,
equal(index_27,index_105),
inference(rew,[status(thm),theory(equality)],[1259,1871]),
[iquote('0:Rew:1259.0,1871.0')] ).
cnf(1891,plain,
equal(p(index_105),index_21),
inference(rew,[status(thm),theory(equality)],[1886,1129]),
[iquote('0:Rew:1886.0,1129.0')] ).
cnf(1893,plain,
equal(rstore_tail(queue_23,index_105),q12),
inference(rew,[status(thm),theory(equality)],[1886,1128]),
[iquote('0:Rew:1886.0,1128.0')] ).
cnf(1896,plain,
equal(index_171,index_111),
inference(rew,[status(thm),theory(equality)],[1257,1880]),
[iquote('0:Rew:1257.0,1880.0')] ).
cnf(1900,plain,
equal(s(index_111),index_177),
inference(rew,[status(thm),theory(equality)],[1896,1197]),
[iquote('0:Rew:1896.0,1197.0')] ).
cnf(1903,plain,
equal(rstore_tail(queue_167,index_111),q34),
inference(rew,[status(thm),theory(equality)],[1896,1203]),
[iquote('0:Rew:1896.0,1203.0')] ).
cnf(1906,plain,
equal(index_21,index_99),
inference(rew,[status(thm),theory(equality)],[1264,1891]),
[iquote('0:Rew:1264.0,1891.0')] ).
cnf(1911,plain,
equal(p(index_99),index_15),
inference(rew,[status(thm),theory(equality)],[1906,1184]),
[iquote('0:Rew:1906.0,1184.0')] ).
cnf(1913,plain,
equal(rstore_tail(queue_17,index_99),q11),
inference(rew,[status(thm),theory(equality)],[1906,1183]),
[iquote('0:Rew:1906.0,1183.0')] ).
cnf(1916,plain,
equal(index_177,index_99),
inference(rew,[status(thm),theory(equality)],[1742,1900]),
[iquote('0:Rew:1742.0,1900.0')] ).
cnf(1920,plain,
equal(s(index_99),index_183),
inference(rew,[status(thm),theory(equality)],[1916,1192]),
[iquote('0:Rew:1916.0,1192.0')] ).
cnf(1923,plain,
equal(rstore_tail(queue_173,index_99),q35),
inference(rew,[status(thm),theory(equality)],[1916,1198]),
[iquote('0:Rew:1916.0,1198.0')] ).
cnf(1926,plain,
equal(index_15,index_111),
inference(rew,[status(thm),theory(equality)],[1720,1911]),
[iquote('0:Rew:1720.0,1911.0')] ).
cnf(1930,plain,
equal(s(index_9),index_111),
inference(rew,[status(thm),theory(equality)],[1926,1237]),
[iquote('0:Rew:1926.0,1237.0')] ).
cnf(1931,plain,
equal(p(index_111),index_9),
inference(rew,[status(thm),theory(equality)],[1926,1239]),
[iquote('0:Rew:1926.0,1239.0')] ).
cnf(1933,plain,
equal(rstore_tail(queue_11,index_111),q10),
inference(rew,[status(thm),theory(equality)],[1926,1238]),
[iquote('0:Rew:1926.0,1238.0')] ).
cnf(1936,plain,
equal(index_183,index_105),
inference(rew,[status(thm),theory(equality)],[1262,1920]),
[iquote('0:Rew:1262.0,1920.0')] ).
cnf(1940,plain,
equal(s(index_105),index_189),
inference(rew,[status(thm),theory(equality)],[1936,1187]),
[iquote('0:Rew:1936.0,1187.0')] ).
cnf(1941,plain,
equal(p(index_189),index_105),
inference(rew,[status(thm),theory(equality)],[1936,1189]),
[iquote('0:Rew:1936.0,1189.0')] ).
cnf(1943,plain,
equal(rstore_tail(queue_179,index_105),q36),
inference(rew,[status(thm),theory(equality)],[1936,1193]),
[iquote('0:Rew:1936.0,1193.0')] ).
cnf(1946,plain,
equal(index_105,index_9),
inference(rew,[status(thm),theory(equality)],[1259,1931]),
[iquote('0:Rew:1259.0,1931.0')] ).
cnf(1953,plain,
equal(s(index_99),index_9),
inference(rew,[status(thm),theory(equality)],[1946,1262]),
[iquote('0:Rew:1946.0,1262.0')] ).
cnf(1954,plain,
equal(p(index_9),index_99),
inference(rew,[status(thm),theory(equality)],[1946,1264]),
[iquote('0:Rew:1946.0,1264.0')] ).
cnf(1956,plain,
equal(rstore_tail(queue_101,index_9),q24),
inference(rew,[status(thm),theory(equality)],[1946,1263]),
[iquote('0:Rew:1946.0,1263.0')] ).
cnf(1981,plain,
equal(index_189,index_111),
inference(rew,[status(thm),theory(equality)],[1930,1940,1946]),
[iquote('0:Rew:1930.0,1940.0,1946.0,1940.0')] ).
cnf(1985,plain,
equal(s(index_111),index_195),
inference(rew,[status(thm),theory(equality)],[1981,1177]),
[iquote('0:Rew:1981.0,1177.0')] ).
cnf(1988,plain,
equal(rstore_tail(queue_185,index_111),q37),
inference(rew,[status(thm),theory(equality)],[1981,1188]),
[iquote('0:Rew:1981.0,1188.0')] ).
cnf(1989,plain,
equal(p(index_111),index_9),
inference(rew,[status(thm),theory(equality)],[1981,1941,1946]),
[iquote('0:Rew:1981.0,1941.0,1946.0,1941.0')] ).
cnf(1991,plain,
equal(index_255,index_99),
inference(rew,[status(thm),theory(equality)],[1119,1954]),
[iquote('0:Rew:1119.0,1954.0')] ).
cnf(1997,plain,
equal(p(index_9),index_99),
inference(rew,[status(thm),theory(equality)],[1991,1119]),
[iquote('0:Rew:1991.0,1119.0')] ).
cnf(1999,plain,
equal(p(index_99),index_249),
inference(rew,[status(thm),theory(equality)],[1991,1124]),
[iquote('0:Rew:1991.0,1124.0')] ).
cnf(2001,plain,
equal(rstore_tail(queue_251,index_99),q8),
inference(rew,[status(thm),theory(equality)],[1991,1123]),
[iquote('0:Rew:1991.0,1123.0')] ).
cnf(2002,plain,
equal(index_195,index_99),
inference(rew,[status(thm),theory(equality)],[1742,1985]),
[iquote('0:Rew:1742.0,1985.0')] ).
cnf(2006,plain,
equal(s(index_99),index_207),
inference(rew,[status(thm),theory(equality)],[2002,1172]),
[iquote('0:Rew:2002.0,1172.0')] ).
cnf(2009,plain,
equal(rstore_tail(queue_191,index_99),q38),
inference(rew,[status(thm),theory(equality)],[2002,1178]),
[iquote('0:Rew:2002.0,1178.0')] ).
cnf(2012,plain,
equal(index_249,index_111),
inference(rew,[status(thm),theory(equality)],[1720,1999]),
[iquote('0:Rew:1720.0,1999.0')] ).
cnf(2017,plain,
equal(p(index_111),index_243),
inference(rew,[status(thm),theory(equality)],[2012,1134]),
[iquote('0:Rew:2012.0,1134.0')] ).
cnf(2019,plain,
equal(rstore_tail(queue_245,index_111),q7),
inference(rew,[status(thm),theory(equality)],[2012,1133]),
[iquote('0:Rew:2012.0,1133.0')] ).
cnf(2022,plain,
equal(index_207,index_9),
inference(rew,[status(thm),theory(equality)],[1953,2006]),
[iquote('0:Rew:1953.0,2006.0')] ).
cnf(2026,plain,
equal(s(index_9),index_213),
inference(rew,[status(thm),theory(equality)],[2022,1162]),
[iquote('0:Rew:2022.0,1162.0')] ).
cnf(2029,plain,
equal(rstore_tail(queue_197,index_9),q39),
inference(rew,[status(thm),theory(equality)],[2022,1173]),
[iquote('0:Rew:2022.0,1173.0')] ).
cnf(2032,plain,
equal(index_243,index_9),
inference(rew,[status(thm),theory(equality)],[1989,2017]),
[iquote('0:Rew:1989.0,2017.0')] ).
cnf(2037,plain,
equal(p(index_9),index_237),
inference(rew,[status(thm),theory(equality)],[2032,1139]),
[iquote('0:Rew:2032.0,1139.0')] ).
cnf(2039,plain,
equal(rstore_tail(queue_239,index_9),q6),
inference(rew,[status(thm),theory(equality)],[2032,1138]),
[iquote('0:Rew:2032.0,1138.0')] ).
cnf(2042,plain,
equal(index_213,index_111),
inference(rew,[status(thm),theory(equality)],[1930,2026]),
[iquote('0:Rew:1930.0,2026.0')] ).
cnf(2046,plain,
equal(s(index_111),index_219),
inference(rew,[status(thm),theory(equality)],[2042,1157]),
[iquote('0:Rew:2042.0,1157.0')] ).
cnf(2049,plain,
equal(rstore_tail(queue_209,index_111),q40),
inference(rew,[status(thm),theory(equality)],[2042,1163]),
[iquote('0:Rew:2042.0,1163.0')] ).
cnf(2052,plain,
equal(index_237,index_99),
inference(rew,[status(thm),theory(equality)],[1997,2037]),
[iquote('0:Rew:1997.0,2037.0')] ).
cnf(2057,plain,
equal(p(index_99),index_231),
inference(rew,[status(thm),theory(equality)],[2052,1144]),
[iquote('0:Rew:2052.0,1144.0')] ).
cnf(2059,plain,
equal(rstore_tail(queue_233,index_99),q5),
inference(rew,[status(thm),theory(equality)],[2052,1143]),
[iquote('0:Rew:2052.0,1143.0')] ).
cnf(2062,plain,
equal(index_219,index_99),
inference(rew,[status(thm),theory(equality)],[1742,2046]),
[iquote('0:Rew:1742.0,2046.0')] ).
cnf(2066,plain,
equal(s(index_99),index_225),
inference(rew,[status(thm),theory(equality)],[2062,1152]),
[iquote('0:Rew:2062.0,1152.0')] ).
cnf(2069,plain,
equal(rstore_tail(queue_215,index_99),q41),
inference(rew,[status(thm),theory(equality)],[2062,1158]),
[iquote('0:Rew:2062.0,1158.0')] ).
cnf(2073,plain,
equal(index_231,index_111),
inference(rew,[status(thm),theory(equality)],[1720,2057]),
[iquote('0:Rew:1720.0,2057.0')] ).
cnf(2078,plain,
equal(p(index_111),index_201),
inference(rew,[status(thm),theory(equality)],[2073,1169]),
[iquote('0:Rew:2073.0,1169.0')] ).
cnf(2080,plain,
equal(rstore_tail(queue_203,index_111),q4),
inference(rew,[status(thm),theory(equality)],[2073,1168]),
[iquote('0:Rew:2073.0,1168.0')] ).
cnf(2083,plain,
equal(index_225,index_9),
inference(rew,[status(thm),theory(equality)],[1953,2066]),
[iquote('0:Rew:1953.0,2066.0')] ).
cnf(2084,plain,
equal(s(index_9),index_228),
inference(rew,[status(thm),theory(equality)],[2083,153]),
[iquote('0:Rew:2083.0,153.0')] ).
cnf(2091,plain,
equal(rstore_tail(queue_221,index_9),q42),
inference(rew,[status(thm),theory(equality)],[2083,1153]),
[iquote('0:Rew:2083.0,1153.0')] ).
cnf(2092,plain,
equal(select(earray_260,index_9),elem_265),
inference(rew,[status(thm),theory(equality)],[2083,1267]),
[iquote('0:Rew:2083.0,1267.0')] ).
cnf(2095,plain,
equal(index_201,index_9),
inference(rew,[status(thm),theory(equality)],[1989,2078]),
[iquote('0:Rew:1989.0,2078.0')] ).
cnf(2100,plain,
equal(p(index_9),index_135),
inference(rew,[status(thm),theory(equality)],[2095,1229]),
[iquote('0:Rew:2095.0,1229.0')] ).
cnf(2102,plain,
equal(rstore_tail(queue_137,index_9),q3),
inference(rew,[status(thm),theory(equality)],[2095,1228]),
[iquote('0:Rew:2095.0,1228.0')] ).
cnf(2105,plain,
equal(index_228,index_111),
inference(rew,[status(thm),theory(equality)],[1930,2084]),
[iquote('0:Rew:1930.0,2084.0')] ).
cnf(2106,plain,
equal(rstore_tail(queue_227,index_111),q43),
inference(rew,[status(thm),theory(equality)],[2105,347]),
[iquote('0:Rew:2105.0,347.0')] ).
cnf(2112,plain,
equal(index_135,index_99),
inference(rew,[status(thm),theory(equality)],[1997,2100]),
[iquote('0:Rew:1997.0,2100.0')] ).
cnf(2117,plain,
equal(p(index_99),index_69),
inference(rew,[status(thm),theory(equality)],[2112,1074]),
[iquote('0:Rew:2112.0,1074.0')] ).
cnf(2119,plain,
equal(rstore_tail(queue_71,index_99),q2),
inference(rew,[status(thm),theory(equality)],[2112,1073]),
[iquote('0:Rew:2112.0,1073.0')] ).
cnf(2122,plain,
equal(index_69,index_111),
inference(rew,[status(thm),theory(equality)],[1720,2117]),
[iquote('0:Rew:1720.0,2117.0')] ).
cnf(2127,plain,
equal(p(index_111),index_3),
inference(rew,[status(thm),theory(equality)],[2122,1079]),
[iquote('0:Rew:2122.0,1079.0')] ).
cnf(2129,plain,
equal(rstore_tail(queue_5,index_111),q1),
inference(rew,[status(thm),theory(equality)],[2122,1078]),
[iquote('0:Rew:2122.0,1078.0')] ).
cnf(2132,plain,
equal(index_3,index_9),
inference(rew,[status(thm),theory(equality)],[1989,2127]),
[iquote('0:Rew:1989.0,2127.0')] ).
cnf(2133,plain,
equal(rselect_tail(q0),index_9),
inference(rew,[status(thm),theory(equality)],[2132,169]),
[iquote('0:Rew:2132.0,169.0')] ).
cnf(2178,plain,
equal(rstore_tail(queue_83,index_9),q21),
inference(rew,[status(thm),theory(equality)],[1946,1714]),
[iquote('0:Rew:1946.0,1714.0')] ).
cnf(2179,plain,
equal(rstore_tail(queue_119,index_9),q27),
inference(rew,[status(thm),theory(equality)],[1946,1763]),
[iquote('0:Rew:1946.0,1763.0')] ).
cnf(2180,plain,
equal(rstore_tail(queue_59,index_9),q18),
inference(rew,[status(thm),theory(equality)],[1946,1773]),
[iquote('0:Rew:1946.0,1773.0')] ).
cnf(2181,plain,
equal(rstore_tail(queue_143,index_9),q30),
inference(rew,[status(thm),theory(equality)],[1946,1823]),
[iquote('0:Rew:1946.0,1823.0')] ).
cnf(2182,plain,
equal(rstore_tail(queue_41,index_9),q15),
inference(rew,[status(thm),theory(equality)],[1946,1833]),
[iquote('0:Rew:1946.0,1833.0')] ).
cnf(2183,plain,
equal(rstore_tail(queue_161,index_9),q33),
inference(rew,[status(thm),theory(equality)],[1946,1883]),
[iquote('0:Rew:1946.0,1883.0')] ).
cnf(2184,plain,
equal(rstore_tail(queue_23,index_9),q12),
inference(rew,[status(thm),theory(equality)],[1946,1893]),
[iquote('0:Rew:1946.0,1893.0')] ).
cnf(2185,plain,
equal(rstore_tail(queue_179,index_9),q36),
inference(rew,[status(thm),theory(equality)],[1946,1943]),
[iquote('0:Rew:1946.0,1943.0')] ).
cnf(2531,plain,
equal(rselect_tail(q),rselect_tail(q0)),
inference(spr,[status(thm),theory(equality)],[371,11]),
[iquote('0:SpR:371.0,11.0')] ).
cnf(2532,plain,
equal(index_0,index_9),
inference(rew,[status(thm),theory(equality)],[106,2531,2133]),
[iquote('0:Rew:106.0,2531.0,2133.0,2531.0')] ).
cnf(2535,plain,
equal(rselect_head(q0),index_9),
inference(rew,[status(thm),theory(equality)],[2532,1653]),
[iquote('0:Rew:2532.0,1653.0')] ).
cnf(2645,plain,
equal(rselect_head(queue_95),rselect_head(q22)),
inference(spr,[status(thm),theory(equality)],[281,9]),
[iquote('0:SpR:281.0,9.0')] ).
cnf(2646,plain,
equal(rselect_head(queue_89),rselect_head(q21)),
inference(spr,[status(thm),theory(equality)],[279,9]),
[iquote('0:SpR:279.0,9.0')] ).
cnf(2647,plain,
equal(rselect_head(queue_83),rselect_head(q20)),
inference(spr,[status(thm),theory(equality)],[277,9]),
[iquote('0:SpR:277.0,9.0')] ).
cnf(2648,plain,
equal(rselect_head(queue_77),rselect_head(q19)),
inference(spr,[status(thm),theory(equality)],[275,9]),
[iquote('0:SpR:275.0,9.0')] ).
cnf(2649,plain,
equal(rselect_head(queue_71),rselect_head(q1)),
inference(spr,[status(thm),theory(equality)],[273,9]),
[iquote('0:SpR:273.0,9.0')] ).
cnf(2650,plain,
equal(rselect_head(queue_65),rselect_head(q18)),
inference(spr,[status(thm),theory(equality)],[270,9]),
[iquote('0:SpR:270.0,9.0')] ).
cnf(2651,plain,
equal(rselect_head(queue_59),rselect_head(q17)),
inference(spr,[status(thm),theory(equality)],[268,9]),
[iquote('0:SpR:268.0,9.0')] ).
cnf(2652,plain,
equal(rselect_head(queue_53),rselect_head(q16)),
inference(spr,[status(thm),theory(equality)],[266,9]),
[iquote('0:SpR:266.0,9.0')] ).
cnf(2653,plain,
equal(rselect_head(queue_5),rselect_head(q0)),
inference(spr,[status(thm),theory(equality)],[265,9]),
[iquote('0:SpR:265.0,9.0')] ).
cnf(2654,plain,
equal(rselect_head(queue_47),rselect_head(q15)),
inference(spr,[status(thm),theory(equality)],[263,9]),
[iquote('0:SpR:263.0,9.0')] ).
cnf(2655,plain,
equal(rselect_head(queue_41),rselect_head(q14)),
inference(spr,[status(thm),theory(equality)],[261,9]),
[iquote('0:SpR:261.0,9.0')] ).
cnf(2656,plain,
equal(rselect_head(queue_35),rselect_head(q13)),
inference(spr,[status(thm),theory(equality)],[259,9]),
[iquote('0:SpR:259.0,9.0')] ).
cnf(2657,plain,
equal(rselect_head(queue_29),rselect_head(q12)),
inference(spr,[status(thm),theory(equality)],[257,9]),
[iquote('0:SpR:257.0,9.0')] ).
cnf(2658,plain,
equal(rselect_head(queue_257),rselect_head(q8)),
inference(spr,[status(thm),theory(equality)],[255,9]),
[iquote('0:SpR:255.0,9.0')] ).
cnf(2659,plain,
equal(rselect_head(queue_251),rselect_head(q7)),
inference(spr,[status(thm),theory(equality)],[253,9]),
[iquote('0:SpR:253.0,9.0')] ).
cnf(2660,plain,
equal(rselect_head(queue_245),rselect_head(q6)),
inference(spr,[status(thm),theory(equality)],[250,9]),
[iquote('0:SpR:250.0,9.0')] ).
cnf(2661,plain,
equal(rselect_head(queue_239),rselect_head(q5)),
inference(spr,[status(thm),theory(equality)],[248,9]),
[iquote('0:SpR:248.0,9.0')] ).
cnf(2662,plain,
equal(rselect_head(queue_233),rselect_head(q4)),
inference(spr,[status(thm),theory(equality)],[246,9]),
[iquote('0:SpR:246.0,9.0')] ).
cnf(2663,plain,
equal(rselect_head(queue_23),rselect_head(q11)),
inference(spr,[status(thm),theory(equality)],[245,9]),
[iquote('0:SpR:245.0,9.0')] ).
cnf(2664,plain,
equal(rselect_head(queue_227),rselect_head(q42)),
inference(spr,[status(thm),theory(equality)],[243,9]),
[iquote('0:SpR:243.0,9.0')] ).
cnf(2665,plain,
equal(rselect_head(queue_221),rselect_head(q41)),
inference(spr,[status(thm),theory(equality)],[241,9]),
[iquote('0:SpR:241.0,9.0')] ).
cnf(2666,plain,
equal(rselect_head(queue_215),rselect_head(q40)),
inference(spr,[status(thm),theory(equality)],[239,9]),
[iquote('0:SpR:239.0,9.0')] ).
cnf(2667,plain,
equal(rselect_head(queue_209),rselect_head(q39)),
inference(spr,[status(thm),theory(equality)],[237,9]),
[iquote('0:SpR:237.0,9.0')] ).
cnf(2668,plain,
equal(rselect_head(queue_203),rselect_head(q3)),
inference(spr,[status(thm),theory(equality)],[235,9]),
[iquote('0:SpR:235.0,9.0')] ).
cnf(2669,plain,
equal(rselect_head(queue_197),rselect_head(q38)),
inference(spr,[status(thm),theory(equality)],[233,9]),
[iquote('0:SpR:233.0,9.0')] ).
cnf(2670,plain,
equal(rselect_head(queue_191),rselect_head(q37)),
inference(spr,[status(thm),theory(equality)],[231,9]),
[iquote('0:SpR:231.0,9.0')] ).
cnf(2671,plain,
equal(rselect_head(queue_185),rselect_head(q36)),
inference(spr,[status(thm),theory(equality)],[228,9]),
[iquote('0:SpR:228.0,9.0')] ).
cnf(2672,plain,
equal(rselect_head(queue_179),rselect_head(q35)),
inference(spr,[status(thm),theory(equality)],[226,9]),
[iquote('0:SpR:226.0,9.0')] ).
cnf(2673,plain,
equal(rselect_head(queue_173),rselect_head(q34)),
inference(spr,[status(thm),theory(equality)],[224,9]),
[iquote('0:SpR:224.0,9.0')] ).
cnf(2674,plain,
equal(rselect_head(queue_17),rselect_head(q10)),
inference(spr,[status(thm),theory(equality)],[223,9]),
[iquote('0:SpR:223.0,9.0')] ).
cnf(2675,plain,
equal(rselect_head(queue_167),rselect_head(q33)),
inference(spr,[status(thm),theory(equality)],[221,9]),
[iquote('0:SpR:221.0,9.0')] ).
cnf(2676,plain,
equal(rselect_head(queue_161),rselect_head(q32)),
inference(spr,[status(thm),theory(equality)],[219,9]),
[iquote('0:SpR:219.0,9.0')] ).
cnf(2677,plain,
equal(rselect_head(queue_155),rselect_head(q31)),
inference(spr,[status(thm),theory(equality)],[217,9]),
[iquote('0:SpR:217.0,9.0')] ).
cnf(2678,plain,
equal(rselect_head(queue_149),rselect_head(q30)),
inference(spr,[status(thm),theory(equality)],[215,9]),
[iquote('0:SpR:215.0,9.0')] ).
cnf(2679,plain,
equal(rselect_head(queue_143),rselect_head(q29)),
inference(spr,[status(thm),theory(equality)],[213,9]),
[iquote('0:SpR:213.0,9.0')] ).
cnf(2680,plain,
equal(rselect_head(queue_137),rselect_head(q2)),
inference(spr,[status(thm),theory(equality)],[211,9]),
[iquote('0:SpR:211.0,9.0')] ).
cnf(2681,plain,
equal(rselect_head(queue_131),rselect_head(q28)),
inference(spr,[status(thm),theory(equality)],[209,9]),
[iquote('0:SpR:209.0,9.0')] ).
cnf(2682,plain,
equal(rselect_head(queue_125),rselect_head(q27)),
inference(spr,[status(thm),theory(equality)],[206,9]),
[iquote('0:SpR:206.0,9.0')] ).
cnf(2683,plain,
equal(rselect_head(queue_119),rselect_head(q26)),
inference(spr,[status(thm),theory(equality)],[204,9]),
[iquote('0:SpR:204.0,9.0')] ).
cnf(2684,plain,
equal(rselect_head(queue_113),rselect_head(q25)),
inference(spr,[status(thm),theory(equality)],[202,9]),
[iquote('0:SpR:202.0,9.0')] ).
cnf(2685,plain,
equal(rselect_head(queue_11),rselect_head(q9)),
inference(spr,[status(thm),theory(equality)],[201,9]),
[iquote('0:SpR:201.0,9.0')] ).
cnf(2686,plain,
equal(rselect_head(queue_107),rselect_head(q24)),
inference(spr,[status(thm),theory(equality)],[199,9]),
[iquote('0:SpR:199.0,9.0')] ).
cnf(2687,plain,
equal(rselect_head(queue_101),rselect_head(q23)),
inference(spr,[status(thm),theory(equality)],[197,9]),
[iquote('0:SpR:197.0,9.0')] ).
cnf(2688,plain,
equal(rselect_head(queue_5),index_9),
inference(rew,[status(thm),theory(equality)],[2535,2653]),
[iquote('0:Rew:2535.0,2653.0')] ).
cnf(2694,plain,
equal(rselect_head(queue_95),rselect_head(q23)),
inference(spr,[status(thm),theory(equality)],[1053,8]),
[iquote('0:SpR:1053.0,8.0')] ).
cnf(2695,plain,
equal(rselect_head(queue_77),rselect_head(q20)),
inference(spr,[status(thm),theory(equality)],[1732,8]),
[iquote('0:SpR:1732.0,8.0')] ).
cnf(2696,plain,
equal(rselect_head(queue_113),rselect_head(q26)),
inference(spr,[status(thm),theory(equality)],[1745,8]),
[iquote('0:SpR:1745.0,8.0')] ).
cnf(2697,plain,
equal(rselect_head(queue_53),rselect_head(q17)),
inference(spr,[status(thm),theory(equality)],[1793,8]),
[iquote('0:SpR:1793.0,8.0')] ).
cnf(2698,plain,
equal(rselect_head(queue_131),rselect_head(q29)),
inference(spr,[status(thm),theory(equality)],[1803,8]),
[iquote('0:SpR:1803.0,8.0')] ).
cnf(2699,plain,
equal(rselect_head(queue_35),rselect_head(q14)),
inference(spr,[status(thm),theory(equality)],[1853,8]),
[iquote('0:SpR:1853.0,8.0')] ).
cnf(2700,plain,
equal(rselect_head(queue_155),rselect_head(q32)),
inference(spr,[status(thm),theory(equality)],[1863,8]),
[iquote('0:SpR:1863.0,8.0')] ).
cnf(2701,plain,
equal(rselect_head(queue_17),rselect_head(q11)),
inference(spr,[status(thm),theory(equality)],[1913,8]),
[iquote('0:SpR:1913.0,8.0')] ).
cnf(2702,plain,
equal(rselect_head(queue_173),rselect_head(q35)),
inference(spr,[status(thm),theory(equality)],[1923,8]),
[iquote('0:SpR:1923.0,8.0')] ).
cnf(2703,plain,
equal(rselect_head(queue_251),rselect_head(q8)),
inference(spr,[status(thm),theory(equality)],[2001,8]),
[iquote('0:SpR:2001.0,8.0')] ).
cnf(2704,plain,
equal(rselect_head(queue_191),rselect_head(q38)),
inference(spr,[status(thm),theory(equality)],[2009,8]),
[iquote('0:SpR:2009.0,8.0')] ).
cnf(2705,plain,
equal(rselect_head(queue_233),rselect_head(q5)),
inference(spr,[status(thm),theory(equality)],[2059,8]),
[iquote('0:SpR:2059.0,8.0')] ).
cnf(2706,plain,
equal(rselect_head(queue_215),rselect_head(q41)),
inference(spr,[status(thm),theory(equality)],[2069,8]),
[iquote('0:SpR:2069.0,8.0')] ).
cnf(2707,plain,
equal(rselect_head(queue_71),rselect_head(q2)),
inference(spr,[status(thm),theory(equality)],[2119,8]),
[iquote('0:SpR:2119.0,8.0')] ).
cnf(2708,plain,
equal(rselect_head(queue_257),rselect_head(q9)),
inference(spr,[status(thm),theory(equality)],[1118,8]),
[iquote('0:SpR:1118.0,8.0')] ).
cnf(2709,plain,
equal(rselect_head(queue_83),rselect_head(q21)),
inference(spr,[status(thm),theory(equality)],[2178,8]),
[iquote('0:SpR:2178.0,8.0')] ).
cnf(2710,plain,
equal(rselect_head(queue_119),rselect_head(q27)),
inference(spr,[status(thm),theory(equality)],[2179,8]),
[iquote('0:SpR:2179.0,8.0')] ).
cnf(2711,plain,
equal(rselect_head(queue_59),rselect_head(q18)),
inference(spr,[status(thm),theory(equality)],[2180,8]),
[iquote('0:SpR:2180.0,8.0')] ).
cnf(2712,plain,
equal(rselect_head(queue_143),rselect_head(q30)),
inference(spr,[status(thm),theory(equality)],[2181,8]),
[iquote('0:SpR:2181.0,8.0')] ).
cnf(2713,plain,
equal(rselect_head(queue_41),rselect_head(q15)),
inference(spr,[status(thm),theory(equality)],[2182,8]),
[iquote('0:SpR:2182.0,8.0')] ).
cnf(2714,plain,
equal(rselect_head(queue_161),rselect_head(q33)),
inference(spr,[status(thm),theory(equality)],[2183,8]),
[iquote('0:SpR:2183.0,8.0')] ).
cnf(2715,plain,
equal(rselect_head(queue_23),rselect_head(q12)),
inference(spr,[status(thm),theory(equality)],[2184,8]),
[iquote('0:SpR:2184.0,8.0')] ).
cnf(2716,plain,
equal(rselect_head(queue_179),rselect_head(q36)),
inference(spr,[status(thm),theory(equality)],[2185,8]),
[iquote('0:SpR:2185.0,8.0')] ).
cnf(2717,plain,
equal(rselect_head(queue_101),rselect_head(q24)),
inference(spr,[status(thm),theory(equality)],[1956,8]),
[iquote('0:SpR:1956.0,8.0')] ).
cnf(2718,plain,
equal(rselect_head(queue_197),rselect_head(q39)),
inference(spr,[status(thm),theory(equality)],[2029,8]),
[iquote('0:SpR:2029.0,8.0')] ).
cnf(2719,plain,
equal(rselect_head(queue_239),rselect_head(q6)),
inference(spr,[status(thm),theory(equality)],[2039,8]),
[iquote('0:SpR:2039.0,8.0')] ).
cnf(2720,plain,
equal(rselect_head(queue_221),rselect_head(q42)),
inference(spr,[status(thm),theory(equality)],[2091,8]),
[iquote('0:SpR:2091.0,8.0')] ).
cnf(2721,plain,
equal(rselect_head(queue_137),rselect_head(q3)),
inference(spr,[status(thm),theory(equality)],[2102,8]),
[iquote('0:SpR:2102.0,8.0')] ).
cnf(2722,plain,
equal(rselect_head(queue_107),rselect_head(q25)),
inference(spr,[status(thm),theory(equality)],[1258,8]),
[iquote('0:SpR:1258.0,8.0')] ).
cnf(2723,plain,
equal(rselect_head(queue_89),rselect_head(q22)),
inference(spr,[status(thm),theory(equality)],[1722,8]),
[iquote('0:SpR:1722.0,8.0')] ).
cnf(2724,plain,
equal(rselect_head(queue_65),rselect_head(q19)),
inference(spr,[status(thm),theory(equality)],[1753,8]),
[iquote('0:SpR:1753.0,8.0')] ).
cnf(2725,plain,
equal(rselect_head(queue_125),rselect_head(q28)),
inference(spr,[status(thm),theory(equality)],[1783,8]),
[iquote('0:SpR:1783.0,8.0')] ).
cnf(2726,plain,
equal(rselect_head(queue_47),rselect_head(q16)),
inference(spr,[status(thm),theory(equality)],[1813,8]),
[iquote('0:SpR:1813.0,8.0')] ).
cnf(2727,plain,
equal(rselect_head(queue_149),rselect_head(q31)),
inference(spr,[status(thm),theory(equality)],[1843,8]),
[iquote('0:SpR:1843.0,8.0')] ).
cnf(2728,plain,
equal(rselect_head(queue_29),rselect_head(q13)),
inference(spr,[status(thm),theory(equality)],[1873,8]),
[iquote('0:SpR:1873.0,8.0')] ).
cnf(2729,plain,
equal(rselect_head(queue_167),rselect_head(q34)),
inference(spr,[status(thm),theory(equality)],[1903,8]),
[iquote('0:SpR:1903.0,8.0')] ).
cnf(2730,plain,
equal(rselect_head(queue_11),rselect_head(q10)),
inference(spr,[status(thm),theory(equality)],[1933,8]),
[iquote('0:SpR:1933.0,8.0')] ).
cnf(2731,plain,
equal(rselect_head(queue_185),rselect_head(q37)),
inference(spr,[status(thm),theory(equality)],[1988,8]),
[iquote('0:SpR:1988.0,8.0')] ).
cnf(2732,plain,
equal(rselect_head(queue_245),rselect_head(q7)),
inference(spr,[status(thm),theory(equality)],[2019,8]),
[iquote('0:SpR:2019.0,8.0')] ).
cnf(2733,plain,
equal(rselect_head(queue_209),rselect_head(q40)),
inference(spr,[status(thm),theory(equality)],[2049,8]),
[iquote('0:SpR:2049.0,8.0')] ).
cnf(2734,plain,
equal(rselect_head(queue_203),rselect_head(q4)),
inference(spr,[status(thm),theory(equality)],[2080,8]),
[iquote('0:SpR:2080.0,8.0')] ).
cnf(2735,plain,
equal(rselect_head(queue_227),rselect_head(q43)),
inference(spr,[status(thm),theory(equality)],[2106,8]),
[iquote('0:SpR:2106.0,8.0')] ).
cnf(2736,plain,
equal(rselect_head(queue_5),rselect_head(q1)),
inference(spr,[status(thm),theory(equality)],[2129,8]),
[iquote('0:SpR:2129.0,8.0')] ).
cnf(2737,plain,
equal(rselect_head(q23),rselect_head(q22)),
inference(rew,[status(thm),theory(equality)],[2645,2694]),
[iquote('0:Rew:2645.0,2694.0')] ).
cnf(2738,plain,
equal(rselect_head(queue_101),rselect_head(q22)),
inference(rew,[status(thm),theory(equality)],[2737,2687]),
[iquote('0:Rew:2737.0,2687.0')] ).
cnf(2739,plain,
equal(rselect_head(q20),rselect_head(q19)),
inference(rew,[status(thm),theory(equality)],[2648,2695]),
[iquote('0:Rew:2648.0,2695.0')] ).
cnf(2740,plain,
equal(rselect_head(queue_83),rselect_head(q19)),
inference(rew,[status(thm),theory(equality)],[2739,2647]),
[iquote('0:Rew:2739.0,2647.0')] ).
cnf(2741,plain,
equal(rselect_head(q26),rselect_head(q25)),
inference(rew,[status(thm),theory(equality)],[2684,2696]),
[iquote('0:Rew:2684.0,2696.0')] ).
cnf(2742,plain,
equal(rselect_head(queue_119),rselect_head(q25)),
inference(rew,[status(thm),theory(equality)],[2741,2683]),
[iquote('0:Rew:2741.0,2683.0')] ).
cnf(2743,plain,
equal(rselect_head(q17),rselect_head(q16)),
inference(rew,[status(thm),theory(equality)],[2652,2697]),
[iquote('0:Rew:2652.0,2697.0')] ).
cnf(2744,plain,
equal(rselect_head(queue_59),rselect_head(q16)),
inference(rew,[status(thm),theory(equality)],[2743,2651]),
[iquote('0:Rew:2743.0,2651.0')] ).
cnf(2745,plain,
equal(rselect_head(q29),rselect_head(q28)),
inference(rew,[status(thm),theory(equality)],[2681,2698]),
[iquote('0:Rew:2681.0,2698.0')] ).
cnf(2746,plain,
equal(rselect_head(queue_143),rselect_head(q28)),
inference(rew,[status(thm),theory(equality)],[2745,2679]),
[iquote('0:Rew:2745.0,2679.0')] ).
cnf(2747,plain,
equal(rselect_head(q14),rselect_head(q13)),
inference(rew,[status(thm),theory(equality)],[2656,2699]),
[iquote('0:Rew:2656.0,2699.0')] ).
cnf(2748,plain,
equal(rselect_head(queue_41),rselect_head(q13)),
inference(rew,[status(thm),theory(equality)],[2747,2655]),
[iquote('0:Rew:2747.0,2655.0')] ).
cnf(2749,plain,
equal(rselect_head(q32),rselect_head(q31)),
inference(rew,[status(thm),theory(equality)],[2677,2700]),
[iquote('0:Rew:2677.0,2700.0')] ).
cnf(2750,plain,
equal(rselect_head(queue_161),rselect_head(q31)),
inference(rew,[status(thm),theory(equality)],[2749,2676]),
[iquote('0:Rew:2749.0,2676.0')] ).
cnf(2751,plain,
equal(rselect_head(q11),rselect_head(q10)),
inference(rew,[status(thm),theory(equality)],[2674,2701]),
[iquote('0:Rew:2674.0,2701.0')] ).
cnf(2752,plain,
equal(rselect_head(queue_23),rselect_head(q10)),
inference(rew,[status(thm),theory(equality)],[2751,2663]),
[iquote('0:Rew:2751.0,2663.0')] ).
cnf(2753,plain,
equal(rselect_head(q35),rselect_head(q34)),
inference(rew,[status(thm),theory(equality)],[2673,2702]),
[iquote('0:Rew:2673.0,2702.0')] ).
cnf(2754,plain,
equal(rselect_head(queue_179),rselect_head(q34)),
inference(rew,[status(thm),theory(equality)],[2753,2672]),
[iquote('0:Rew:2753.0,2672.0')] ).
cnf(2755,plain,
equal(rselect_head(q8),rselect_head(q7)),
inference(rew,[status(thm),theory(equality)],[2659,2703]),
[iquote('0:Rew:2659.0,2703.0')] ).
cnf(2756,plain,
equal(rselect_head(queue_257),rselect_head(q7)),
inference(rew,[status(thm),theory(equality)],[2755,2658]),
[iquote('0:Rew:2755.0,2658.0')] ).
cnf(2757,plain,
equal(rselect_head(q38),rselect_head(q37)),
inference(rew,[status(thm),theory(equality)],[2670,2704]),
[iquote('0:Rew:2670.0,2704.0')] ).
cnf(2758,plain,
equal(rselect_head(queue_197),rselect_head(q37)),
inference(rew,[status(thm),theory(equality)],[2757,2669]),
[iquote('0:Rew:2757.0,2669.0')] ).
cnf(2759,plain,
equal(rselect_head(q5),rselect_head(q4)),
inference(rew,[status(thm),theory(equality)],[2662,2705]),
[iquote('0:Rew:2662.0,2705.0')] ).
cnf(2760,plain,
equal(rselect_head(queue_239),rselect_head(q4)),
inference(rew,[status(thm),theory(equality)],[2759,2661]),
[iquote('0:Rew:2759.0,2661.0')] ).
cnf(2761,plain,
equal(rselect_head(q41),rselect_head(q40)),
inference(rew,[status(thm),theory(equality)],[2666,2706]),
[iquote('0:Rew:2666.0,2706.0')] ).
cnf(2762,plain,
equal(rselect_head(queue_221),rselect_head(q40)),
inference(rew,[status(thm),theory(equality)],[2761,2665]),
[iquote('0:Rew:2761.0,2665.0')] ).
cnf(2763,plain,
equal(rselect_head(q1),rselect_head(q2)),
inference(rew,[status(thm),theory(equality)],[2649,2707]),
[iquote('0:Rew:2649.0,2707.0')] ).
cnf(2765,plain,
equal(rselect_head(q3),rselect_head(q2)),
inference(rew,[status(thm),theory(equality)],[2680,2721]),
[iquote('0:Rew:2680.0,2721.0')] ).
cnf(2766,plain,
equal(rselect_head(queue_203),rselect_head(q2)),
inference(rew,[status(thm),theory(equality)],[2765,2668]),
[iquote('0:Rew:2765.0,2668.0')] ).
cnf(2767,plain,
equal(rselect_head(q25),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2686,2722]),
[iquote('0:Rew:2686.0,2722.0')] ).
cnf(2770,plain,
equal(rselect_head(q22),rselect_head(q21)),
inference(rew,[status(thm),theory(equality)],[2646,2723]),
[iquote('0:Rew:2646.0,2723.0')] ).
cnf(2773,plain,
equal(rselect_head(q19),rselect_head(q18)),
inference(rew,[status(thm),theory(equality)],[2650,2724]),
[iquote('0:Rew:2650.0,2724.0')] ).
cnf(2776,plain,
equal(rselect_head(q28),rselect_head(q27)),
inference(rew,[status(thm),theory(equality)],[2682,2725]),
[iquote('0:Rew:2682.0,2725.0')] ).
cnf(2779,plain,
equal(rselect_head(q16),rselect_head(q15)),
inference(rew,[status(thm),theory(equality)],[2654,2726]),
[iquote('0:Rew:2654.0,2726.0')] ).
cnf(2782,plain,
equal(rselect_head(q31),rselect_head(q30)),
inference(rew,[status(thm),theory(equality)],[2678,2727]),
[iquote('0:Rew:2678.0,2727.0')] ).
cnf(2785,plain,
equal(rselect_head(q13),rselect_head(q12)),
inference(rew,[status(thm),theory(equality)],[2657,2728]),
[iquote('0:Rew:2657.0,2728.0')] ).
cnf(2788,plain,
equal(rselect_head(q34),rselect_head(q33)),
inference(rew,[status(thm),theory(equality)],[2675,2729]),
[iquote('0:Rew:2675.0,2729.0')] ).
cnf(2791,plain,
equal(rselect_head(q9),rselect_head(q10)),
inference(rew,[status(thm),theory(equality)],[2685,2730]),
[iquote('0:Rew:2685.0,2730.0')] ).
cnf(2793,plain,
equal(rselect_head(queue_257),rselect_head(q10)),
inference(rew,[status(thm),theory(equality)],[2791,2708]),
[iquote('0:Rew:2791.0,2708.0')] ).
cnf(2794,plain,
equal(rselect_head(q37),rselect_head(q36)),
inference(rew,[status(thm),theory(equality)],[2671,2731]),
[iquote('0:Rew:2671.0,2731.0')] ).
cnf(2797,plain,
equal(rselect_head(q7),rselect_head(q6)),
inference(rew,[status(thm),theory(equality)],[2660,2732]),
[iquote('0:Rew:2660.0,2732.0')] ).
cnf(2800,plain,
equal(rselect_head(q40),rselect_head(q39)),
inference(rew,[status(thm),theory(equality)],[2667,2733]),
[iquote('0:Rew:2667.0,2733.0')] ).
cnf(2803,plain,
equal(rselect_head(queue_227),index_261),
inference(rew,[status(thm),theory(equality)],[165,2735]),
[iquote('0:Rew:165.0,2735.0')] ).
cnf(2804,plain,
equal(rselect_head(q42),index_261),
inference(rew,[status(thm),theory(equality)],[2664,2803]),
[iquote('0:Rew:2664.0,2803.0')] ).
cnf(2806,plain,
equal(rselect_head(queue_221),index_261),
inference(rew,[status(thm),theory(equality)],[2804,2720]),
[iquote('0:Rew:2804.0,2720.0')] ).
cnf(2807,plain,
equal(rselect_head(q2),index_9),
inference(rew,[status(thm),theory(equality)],[2688,2736,2763]),
[iquote('0:Rew:2688.0,2736.0,2763.0,2736.0')] ).
cnf(2811,plain,
equal(rselect_head(q21),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2717,2738,2770]),
[iquote('0:Rew:2717.0,2738.0,2770.0,2738.0')] ).
cnf(2813,plain,
equal(rselect_head(queue_83),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2811,2709]),
[iquote('0:Rew:2811.0,2709.0')] ).
cnf(2815,plain,
equal(rselect_head(queue_83),rselect_head(q18)),
inference(rew,[status(thm),theory(equality)],[2773,2740]),
[iquote('0:Rew:2773.0,2740.0')] ).
cnf(2816,plain,
equal(rselect_head(q27),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2710,2742,2767]),
[iquote('0:Rew:2710.0,2742.0,2767.0,2742.0')] ).
cnf(2819,plain,
equal(rselect_head(q28),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2816,2776]),
[iquote('0:Rew:2816.0,2776.0')] ).
cnf(2820,plain,
equal(rselect_head(q18),rselect_head(q15)),
inference(rew,[status(thm),theory(equality)],[2711,2744,2779]),
[iquote('0:Rew:2711.0,2744.0,2779.0,2744.0')] ).
cnf(2824,plain,
equal(rselect_head(queue_83),rselect_head(q15)),
inference(rew,[status(thm),theory(equality)],[2820,2815]),
[iquote('0:Rew:2820.0,2815.0')] ).
cnf(2825,plain,
equal(rselect_head(q30),rselect_head(q28)),
inference(rew,[status(thm),theory(equality)],[2712,2746]),
[iquote('0:Rew:2712.0,2746.0')] ).
cnf(2828,plain,
equal(rselect_head(q31),rselect_head(q28)),
inference(rew,[status(thm),theory(equality)],[2825,2782]),
[iquote('0:Rew:2825.0,2782.0')] ).
cnf(2829,plain,
equal(rselect_head(q15),rselect_head(q12)),
inference(rew,[status(thm),theory(equality)],[2713,2748,2785]),
[iquote('0:Rew:2713.0,2748.0,2785.0,2748.0')] ).
cnf(2834,plain,
equal(rselect_head(q33),rselect_head(q31)),
inference(rew,[status(thm),theory(equality)],[2714,2750]),
[iquote('0:Rew:2714.0,2750.0')] ).
cnf(2837,plain,
equal(rselect_head(q34),rselect_head(q31)),
inference(rew,[status(thm),theory(equality)],[2834,2788]),
[iquote('0:Rew:2834.0,2788.0')] ).
cnf(2838,plain,
equal(rselect_head(q12),rselect_head(q10)),
inference(rew,[status(thm),theory(equality)],[2715,2752]),
[iquote('0:Rew:2715.0,2752.0')] ).
cnf(2842,plain,
equal(rselect_head(q15),rselect_head(q10)),
inference(rew,[status(thm),theory(equality)],[2838,2829]),
[iquote('0:Rew:2838.0,2829.0')] ).
cnf(2843,plain,
equal(rselect_head(q36),rselect_head(q34)),
inference(rew,[status(thm),theory(equality)],[2716,2754]),
[iquote('0:Rew:2716.0,2754.0')] ).
cnf(2846,plain,
equal(rselect_head(q37),rselect_head(q34)),
inference(rew,[status(thm),theory(equality)],[2843,2794]),
[iquote('0:Rew:2843.0,2794.0')] ).
cnf(2847,plain,
equal(rselect_head(queue_257),rselect_head(q6)),
inference(rew,[status(thm),theory(equality)],[2797,2756]),
[iquote('0:Rew:2797.0,2756.0')] ).
cnf(2848,plain,
equal(rselect_head(q39),rselect_head(q37)),
inference(rew,[status(thm),theory(equality)],[2718,2758]),
[iquote('0:Rew:2718.0,2758.0')] ).
cnf(2851,plain,
equal(rselect_head(q40),rselect_head(q37)),
inference(rew,[status(thm),theory(equality)],[2848,2800]),
[iquote('0:Rew:2848.0,2800.0')] ).
cnf(2852,plain,
equal(rselect_head(q6),rselect_head(q4)),
inference(rew,[status(thm),theory(equality)],[2719,2760]),
[iquote('0:Rew:2719.0,2760.0')] ).
cnf(2856,plain,
equal(rselect_head(queue_257),rselect_head(q4)),
inference(rew,[status(thm),theory(equality)],[2852,2847]),
[iquote('0:Rew:2852.0,2847.0')] ).
cnf(2857,plain,
equal(rselect_head(q40),index_261),
inference(rew,[status(thm),theory(equality)],[2806,2762]),
[iquote('0:Rew:2806.0,2762.0')] ).
cnf(2859,plain,
equal(rselect_head(q4),index_9),
inference(rew,[status(thm),theory(equality)],[2734,2766,2807]),
[iquote('0:Rew:2734.0,2766.0,2807.0,2766.0')] ).
cnf(2883,plain,
equal(rselect_head(q15),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2813,2824]),
[iquote('0:Rew:2813.0,2824.0')] ).
cnf(2891,plain,
equal(rselect_head(q31),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2819,2828]),
[iquote('0:Rew:2819.0,2828.0')] ).
cnf(2903,plain,
equal(rselect_head(q34),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2891,2837]),
[iquote('0:Rew:2891.0,2837.0')] ).
cnf(2907,plain,
equal(rselect_head(q10),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2883,2842]),
[iquote('0:Rew:2883.0,2842.0')] ).
cnf(2915,plain,
equal(rselect_head(queue_257),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2907,2793]),
[iquote('0:Rew:2907.0,2793.0')] ).
cnf(2925,plain,
equal(rselect_head(q37),rselect_head(q24)),
inference(rew,[status(thm),theory(equality)],[2903,2846]),
[iquote('0:Rew:2903.0,2846.0')] ).
cnf(2931,plain,
equal(rselect_head(q24),index_261),
inference(rew,[status(thm),theory(equality)],[2857,2851,2925]),
[iquote('0:Rew:2857.0,2851.0,2925.0,2851.0')] ).
cnf(2965,plain,
equal(rselect_head(queue_257),index_9),
inference(rew,[status(thm),theory(equality)],[2859,2856]),
[iquote('0:Rew:2859.0,2856.0')] ).
cnf(2989,plain,
equal(index_261,index_9),
inference(rew,[status(thm),theory(equality)],[2965,2915,2931]),
[iquote('0:Rew:2965.0,2915.0,2931.0,2915.0')] ).
cnf(2991,plain,
equal(select(earray_260,index_9),elem_262),
inference(rew,[status(thm),theory(equality)],[2989,104]),
[iquote('0:Rew:2989.0,104.0')] ).
cnf(3060,plain,
equal(elem_265,elem_262),
inference(rew,[status(thm),theory(equality)],[2092,2991]),
[iquote('0:Rew:2092.0,2991.0')] ).
cnf(3061,plain,
$false,
inference(mrr,[status(thm)],[3060,327]),
[iquote('0:MRR:3060.0,327.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.07 % Problem : SWV570-1.043 : TPTP v8.1.0. Bugfixed v5.0.0.
% 0.02/0.07 % Command : run_spass %d %s
% 0.07/0.26 % Computer : n017.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % WCLimit : 600
% 0.07/0.26 % DateTime : Thu Jun 16 01:15:40 EDT 2022
% 0.07/0.26 % CPUTime :
% 0.54/0.75
% 0.54/0.75 SPASS V 3.9
% 0.54/0.75 SPASS beiseite: Proof found.
% 0.54/0.75 % SZS status Theorem
% 0.54/0.75 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.54/0.75 SPASS derived 2311 clauses, backtracked 0 clauses, performed 0 splits and kept 1320 clauses.
% 0.54/0.75 SPASS allocated 64856 KBytes.
% 0.54/0.75 SPASS spent 0:00:00.49 on the problem.
% 0.54/0.75 0:00:00.03 for the input.
% 0.54/0.75 0:00:00.00 for the FLOTTER CNF translation.
% 0.54/0.75 0:00:00.04 for inferences.
% 0.54/0.75 0:00:00.00 for the backtracking.
% 0.54/0.75 0:00:00.33 for the reduction.
% 0.54/0.75
% 0.54/0.75
% 0.54/0.75 Here is a proof with depth 2, length 794 :
% 0.54/0.75 % SZS output start Refutation
% See solution above
% 0.60/0.79 Formulae used in the proof : a1_head a1_tail a2_head_tail a2_head_seq a2_tail_head ps circular 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 hyp142 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 goal
% 0.60/0.79
%------------------------------------------------------------------------------