%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV569-1.030 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n011.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:21 EDT 2022
% Result : Unsatisfiable 12.84s 13.08s
% Output : Refutation 13.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 249
% Syntax : Number of clauses : 863 ( 596 unt; 267 nHn; 863 RR)
% Number of literals : 1254 ( 0 equ; 111 neg)
% Maximal clause size : 11 ( 1 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 267 ( 267 usr; 264 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(select(store(u,v,w),v),w),
file('SWV569-1.030.p',unknown),
[] ).
cnf(2,axiom,
( equal(u,v)
| equal(select(store(w,u,x),v),select(w,v)) ),
file('SWV569-1.030.p',unknown),
[] ).
cnf(3,axiom,
~ equal(tail,head),
file('SWV569-1.030.p',unknown),
[] ).
cnf(4,axiom,
~ equal(seq,head),
file('SWV569-1.030.p',unknown),
[] ).
cnf(5,axiom,
~ equal(seq,tail),
file('SWV569-1.030.p',unknown),
[] ).
cnf(37,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(38,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(39,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(40,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(41,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(42,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(43,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(u))))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(44,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(u)))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(45,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(s(u))))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(46,axiom,
~ equal(s(s(s(s(s(s(s(s(s(s(u)))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(47,axiom,
~ equal(s(s(s(s(s(s(s(s(s(u))))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(48,axiom,
~ equal(s(s(s(s(s(s(s(s(u)))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(49,axiom,
~ equal(s(s(s(s(s(s(s(u))))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(50,axiom,
~ equal(s(s(s(s(s(s(u)))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(51,axiom,
~ equal(s(s(s(s(s(u))))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(52,axiom,
~ equal(s(s(s(s(u)))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(53,axiom,
~ equal(s(s(s(u))),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(54,axiom,
~ equal(s(s(u)),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(55,axiom,
~ equal(s(u),u),
file('SWV569-1.030.p',unknown),
[] ).
cnf(57,axiom,
equal(store(earray_98,index_99,e21),earray_100),
file('SWV569-1.030.p',unknown),
[] ).
cnf(58,axiom,
equal(select(q22,seq),earray_104),
file('SWV569-1.030.p',unknown),
[] ).
cnf(59,axiom,
equal(store(earray_104,index_105,e22),earray_106),
file('SWV569-1.030.p',unknown),
[] ).
cnf(60,axiom,
equal(select(q23,seq),earray_110),
file('SWV569-1.030.p',unknown),
[] ).
cnf(61,axiom,
equal(store(earray_110,index_111,e23),earray_112),
file('SWV569-1.030.p',unknown),
[] ).
cnf(62,axiom,
equal(select(q24,seq),earray_119),
file('SWV569-1.030.p',unknown),
[] ).
cnf(63,axiom,
equal(store(earray_119,index_120,e24),earray_121),
file('SWV569-1.030.p',unknown),
[] ).
cnf(64,axiom,
equal(select(q25,seq),earray_125),
file('SWV569-1.030.p',unknown),
[] ).
cnf(65,axiom,
equal(store(earray_125,index_126,e25),earray_127),
file('SWV569-1.030.p',unknown),
[] ).
cnf(66,axiom,
equal(select(q26,seq),earray_131),
file('SWV569-1.030.p',unknown),
[] ).
cnf(67,axiom,
equal(store(earray_131,index_132,e26),earray_133),
file('SWV569-1.030.p',unknown),
[] ).
cnf(69,axiom,
equal(select(q27,seq),earray_140),
file('SWV569-1.030.p',unknown),
[] ).
cnf(70,axiom,
equal(store(earray_140,index_141,e27),earray_142),
file('SWV569-1.030.p',unknown),
[] ).
cnf(71,axiom,
equal(select(q28,seq),earray_146),
file('SWV569-1.030.p',unknown),
[] ).
cnf(72,axiom,
equal(store(earray_146,index_147,e28),earray_148),
file('SWV569-1.030.p',unknown),
[] ).
cnf(75,axiom,
equal(store(earray_14,index_15,e10),earray_16),
file('SWV569-1.030.p',unknown),
[] ).
cnf(76,axiom,
equal(select(q29,seq),earray_161),
file('SWV569-1.030.p',unknown),
[] ).
cnf(77,axiom,
equal(store(earray_161,index_162,e29),earray_163),
file('SWV569-1.030.p',unknown),
[] ).
cnf(89,axiom,
equal(select(q11,seq),earray_20),
file('SWV569-1.030.p',unknown),
[] ).
cnf(92,axiom,
equal(select(q30,seq),earray_212),
file('SWV569-1.030.p',unknown),
[] ).
cnf(93,axiom,
equal(store(earray_20,index_21,e11),earray_22),
file('SWV569-1.030.p',unknown),
[] ).
cnf(94,axiom,
equal(select(q12,seq),earray_29),
file('SWV569-1.030.p',unknown),
[] ).
cnf(95,axiom,
equal(store(earray_29,index_30,e12),earray_31),
file('SWV569-1.030.p',unknown),
[] ).
cnf(96,axiom,
equal(select(q13,seq),earray_35),
file('SWV569-1.030.p',unknown),
[] ).
cnf(97,axiom,
equal(store(earray_35,index_36,e13),earray_37),
file('SWV569-1.030.p',unknown),
[] ).
cnf(99,axiom,
equal(select(q14,seq),earray_41),
file('SWV569-1.030.p',unknown),
[] ).
cnf(100,axiom,
equal(store(earray_41,index_42,e14),earray_43),
file('SWV569-1.030.p',unknown),
[] ).
cnf(101,axiom,
equal(select(q15,seq),earray_50),
file('SWV569-1.030.p',unknown),
[] ).
cnf(102,axiom,
equal(store(earray_50,index_51,e15),earray_52),
file('SWV569-1.030.p',unknown),
[] ).
cnf(103,axiom,
equal(select(q16,seq),earray_56),
file('SWV569-1.030.p',unknown),
[] ).
cnf(104,axiom,
equal(store(earray_56,index_57,e16),earray_58),
file('SWV569-1.030.p',unknown),
[] ).
cnf(105,axiom,
equal(select(q17,seq),earray_62),
file('SWV569-1.030.p',unknown),
[] ).
cnf(106,axiom,
equal(store(earray_62,index_63,e17),earray_64),
file('SWV569-1.030.p',unknown),
[] ).
cnf(107,axiom,
equal(select(q18,seq),earray_71),
file('SWV569-1.030.p',unknown),
[] ).
cnf(108,axiom,
equal(store(earray_71,index_72,e18),earray_73),
file('SWV569-1.030.p',unknown),
[] ).
cnf(112,axiom,
equal(select(q19,seq),earray_83),
file('SWV569-1.030.p',unknown),
[] ).
cnf(113,axiom,
equal(store(earray_83,index_84,e19),earray_85),
file('SWV569-1.030.p',unknown),
[] ).
cnf(114,axiom,
equal(select(q20,seq),earray_89),
file('SWV569-1.030.p',unknown),
[] ).
cnf(115,axiom,
equal(store(earray_89,index_90,e20),earray_91),
file('SWV569-1.030.p',unknown),
[] ).
cnf(116,axiom,
equal(select(q21,seq),earray_98),
file('SWV569-1.030.p',unknown),
[] ).
cnf(117,axiom,
equal(select(earray_212,index_213),elem_214),
file('SWV569-1.030.p',unknown),
[] ).
cnf(118,axiom,
equal(select(q,tail),index_0),
file('SWV569-1.030.p',unknown),
[] ).
cnf(119,axiom,
equal(s(index_99),index_102),
file('SWV569-1.030.p',unknown),
[] ).
cnf(120,axiom,
equal(select(q22,tail),index_105),
file('SWV569-1.030.p',unknown),
[] ).
cnf(121,axiom,
equal(s(index_105),index_108),
file('SWV569-1.030.p',unknown),
[] ).
cnf(122,axiom,
equal(select(q23,tail),index_111),
file('SWV569-1.030.p',unknown),
[] ).
cnf(123,axiom,
equal(s(index_111),index_114),
file('SWV569-1.030.p',unknown),
[] ).
cnf(124,axiom,
equal(select(queue_115,head),index_116),
file('SWV569-1.030.p',unknown),
[] ).
cnf(125,axiom,
equal(s(index_116),index_117),
file('SWV569-1.030.p',unknown),
[] ).
cnf(126,axiom,
equal(s(index_9),index_12),
file('SWV569-1.030.p',unknown),
[] ).
cnf(127,axiom,
equal(select(q24,tail),index_120),
file('SWV569-1.030.p',unknown),
[] ).
cnf(128,axiom,
equal(s(index_120),index_123),
file('SWV569-1.030.p',unknown),
[] ).
cnf(129,axiom,
equal(select(q25,tail),index_126),
file('SWV569-1.030.p',unknown),
[] ).
cnf(130,axiom,
equal(s(index_126),index_129),
file('SWV569-1.030.p',unknown),
[] ).
cnf(131,axiom,
equal(select(q26,tail),index_132),
file('SWV569-1.030.p',unknown),
[] ).
cnf(132,axiom,
equal(s(index_132),index_135),
file('SWV569-1.030.p',unknown),
[] ).
cnf(133,axiom,
equal(select(queue_136,head),index_137),
file('SWV569-1.030.p',unknown),
[] ).
cnf(134,axiom,
equal(s(index_137),index_138),
file('SWV569-1.030.p',unknown),
[] ).
cnf(135,axiom,
equal(select(q27,tail),index_141),
file('SWV569-1.030.p',unknown),
[] ).
cnf(136,axiom,
equal(s(index_141),index_144),
file('SWV569-1.030.p',unknown),
[] ).
cnf(137,axiom,
equal(select(q28,tail),index_147),
file('SWV569-1.030.p',unknown),
[] ).
cnf(138,axiom,
equal(select(q10,tail),index_15),
file('SWV569-1.030.p',unknown),
[] ).
cnf(139,axiom,
equal(s(index_147),index_150),
file('SWV569-1.030.p',unknown),
[] ).
cnf(140,axiom,
equal(select(q2,tail),index_153),
file('SWV569-1.030.p',unknown),
[] ).
cnf(141,axiom,
equal(s(index_153),index_156),
file('SWV569-1.030.p',unknown),
[] ).
cnf(142,axiom,
equal(select(queue_157,head),index_158),
file('SWV569-1.030.p',unknown),
[] ).
cnf(143,axiom,
equal(s(index_158),index_159),
file('SWV569-1.030.p',unknown),
[] ).
cnf(144,axiom,
equal(select(q29,tail),index_162),
file('SWV569-1.030.p',unknown),
[] ).
cnf(146,axiom,
equal(select(queue_166,head),index_167),
file('SWV569-1.030.p',unknown),
[] ).
cnf(147,axiom,
equal(s(index_167),index_168),
file('SWV569-1.030.p',unknown),
[] ).
cnf(148,axiom,
equal(select(q3,tail),index_171),
file('SWV569-1.030.p',unknown),
[] ).
cnf(149,axiom,
equal(s(index_171),index_174),
file('SWV569-1.030.p',unknown),
[] ).
cnf(150,axiom,
equal(select(q4,tail),index_177),
file('SWV569-1.030.p',unknown),
[] ).
cnf(151,axiom,
equal(s(index_15),index_18),
file('SWV569-1.030.p',unknown),
[] ).
cnf(152,axiom,
equal(s(index_177),index_180),
file('SWV569-1.030.p',unknown),
[] ).
cnf(153,axiom,
equal(select(q5,tail),index_183),
file('SWV569-1.030.p',unknown),
[] ).
cnf(154,axiom,
equal(s(index_183),index_186),
file('SWV569-1.030.p',unknown),
[] ).
cnf(155,axiom,
equal(select(queue_187,head),index_188),
file('SWV569-1.030.p',unknown),
[] ).
cnf(156,axiom,
equal(s(index_188),index_189),
file('SWV569-1.030.p',unknown),
[] ).
cnf(157,axiom,
equal(select(q6,tail),index_192),
file('SWV569-1.030.p',unknown),
[] ).
cnf(158,axiom,
equal(s(index_192),index_195),
file('SWV569-1.030.p',unknown),
[] ).
cnf(159,axiom,
equal(select(q7,tail),index_198),
file('SWV569-1.030.p',unknown),
[] ).
cnf(160,axiom,
equal(s(index_198),index_201),
file('SWV569-1.030.p',unknown),
[] ).
cnf(161,axiom,
equal(select(q8,tail),index_204),
file('SWV569-1.030.p',unknown),
[] ).
cnf(162,axiom,
equal(s(index_204),index_207),
file('SWV569-1.030.p',unknown),
[] ).
cnf(163,axiom,
equal(select(queue_208,head),index_209),
file('SWV569-1.030.p',unknown),
[] ).
cnf(164,axiom,
equal(select(q11,tail),index_21),
file('SWV569-1.030.p',unknown),
[] ).
cnf(165,axiom,
equal(s(index_209),index_210),
file('SWV569-1.030.p',unknown),
[] ).
cnf(166,axiom,
equal(select(q30,head),index_213),
file('SWV569-1.030.p',unknown),
[] ).
cnf(167,axiom,
equal(s(index_21),index_24),
file('SWV569-1.030.p',unknown),
[] ).
cnf(168,axiom,
equal(select(queue_25,head),index_26),
file('SWV569-1.030.p',unknown),
[] ).
cnf(169,axiom,
equal(s(index_26),index_27),
file('SWV569-1.030.p',unknown),
[] ).
cnf(170,axiom,
equal(select(q0,tail),index_3),
file('SWV569-1.030.p',unknown),
[] ).
cnf(171,axiom,
equal(select(q12,tail),index_30),
file('SWV569-1.030.p',unknown),
[] ).
cnf(172,axiom,
equal(s(index_30),index_33),
file('SWV569-1.030.p',unknown),
[] ).
cnf(173,axiom,
equal(select(q13,tail),index_36),
file('SWV569-1.030.p',unknown),
[] ).
cnf(174,axiom,
equal(s(index_36),index_39),
file('SWV569-1.030.p',unknown),
[] ).
cnf(175,axiom,
equal(select(q14,tail),index_42),
file('SWV569-1.030.p',unknown),
[] ).
cnf(176,axiom,
equal(s(index_42),index_45),
file('SWV569-1.030.p',unknown),
[] ).
cnf(177,axiom,
equal(select(queue_46,head),index_47),
file('SWV569-1.030.p',unknown),
[] ).
cnf(178,axiom,
equal(s(index_47),index_48),
file('SWV569-1.030.p',unknown),
[] ).
cnf(179,axiom,
equal(select(q15,tail),index_51),
file('SWV569-1.030.p',unknown),
[] ).
cnf(180,axiom,
equal(s(index_51),index_54),
file('SWV569-1.030.p',unknown),
[] ).
cnf(181,axiom,
equal(select(q16,tail),index_57),
file('SWV569-1.030.p',unknown),
[] ).
cnf(182,axiom,
equal(s(index_3),index_6),
file('SWV569-1.030.p',unknown),
[] ).
cnf(183,axiom,
equal(s(index_57),index_60),
file('SWV569-1.030.p',unknown),
[] ).
cnf(184,axiom,
equal(select(q17,tail),index_63),
file('SWV569-1.030.p',unknown),
[] ).
cnf(185,axiom,
equal(s(index_63),index_66),
file('SWV569-1.030.p',unknown),
[] ).
cnf(186,axiom,
equal(select(queue_67,head),index_68),
file('SWV569-1.030.p',unknown),
[] ).
cnf(187,axiom,
equal(s(index_68),index_69),
file('SWV569-1.030.p',unknown),
[] ).
cnf(188,axiom,
equal(select(q18,tail),index_72),
file('SWV569-1.030.p',unknown),
[] ).
cnf(189,axiom,
equal(s(index_72),index_75),
file('SWV569-1.030.p',unknown),
[] ).
cnf(190,axiom,
equal(select(q1,tail),index_78),
file('SWV569-1.030.p',unknown),
[] ).
cnf(191,axiom,
equal(s(index_78),index_81),
file('SWV569-1.030.p',unknown),
[] ).
cnf(192,axiom,
equal(select(q19,tail),index_84),
file('SWV569-1.030.p',unknown),
[] ).
cnf(193,axiom,
equal(s(index_84),index_87),
file('SWV569-1.030.p',unknown),
[] ).
cnf(194,axiom,
equal(select(q9,tail),index_9),
file('SWV569-1.030.p',unknown),
[] ).
cnf(195,axiom,
equal(select(q20,tail),index_90),
file('SWV569-1.030.p',unknown),
[] ).
cnf(196,axiom,
equal(s(index_90),index_93),
file('SWV569-1.030.p',unknown),
[] ).
cnf(197,axiom,
equal(select(queue_94,head),index_95),
file('SWV569-1.030.p',unknown),
[] ).
cnf(198,axiom,
equal(s(index_95),index_96),
file('SWV569-1.030.p',unknown),
[] ).
cnf(199,axiom,
equal(select(q21,tail),index_99),
file('SWV569-1.030.p',unknown),
[] ).
cnf(200,axiom,
equal(store(q,head,index_0),queue_1),
file('SWV569-1.030.p',unknown),
[] ).
cnf(201,axiom,
equal(store(q21,seq,earray_100),queue_101),
file('SWV569-1.030.p',unknown),
[] ).
cnf(202,axiom,
equal(store(queue_101,tail,index_102),queue_103),
file('SWV569-1.030.p',unknown),
[] ).
cnf(203,axiom,
equal(store(q22,seq,earray_106),queue_107),
file('SWV569-1.030.p',unknown),
[] ).
cnf(204,axiom,
equal(store(queue_107,tail,index_108),queue_109),
file('SWV569-1.030.p',unknown),
[] ).
cnf(205,axiom,
equal(store(q9,seq,earray_10),queue_11),
file('SWV569-1.030.p',unknown),
[] ).
cnf(206,axiom,
equal(store(q23,seq,earray_112),queue_113),
file('SWV569-1.030.p',unknown),
[] ).
cnf(207,axiom,
equal(store(queue_113,tail,index_114),queue_115),
file('SWV569-1.030.p',unknown),
[] ).
cnf(208,axiom,
equal(store(queue_115,head,index_117),queue_118),
file('SWV569-1.030.p',unknown),
[] ).
cnf(209,axiom,
equal(store(q24,seq,earray_121),queue_122),
file('SWV569-1.030.p',unknown),
[] ).
cnf(210,axiom,
equal(store(queue_122,tail,index_123),queue_124),
file('SWV569-1.030.p',unknown),
[] ).
cnf(211,axiom,
equal(store(q25,seq,earray_127),queue_128),
file('SWV569-1.030.p',unknown),
[] ).
cnf(212,axiom,
equal(store(queue_11,tail,index_12),queue_13),
file('SWV569-1.030.p',unknown),
[] ).
cnf(213,axiom,
equal(store(queue_128,tail,index_129),queue_130),
file('SWV569-1.030.p',unknown),
[] ).
cnf(214,axiom,
equal(store(q26,seq,earray_133),queue_134),
file('SWV569-1.030.p',unknown),
[] ).
cnf(215,axiom,
equal(store(queue_134,tail,index_135),queue_136),
file('SWV569-1.030.p',unknown),
[] ).
cnf(216,axiom,
equal(store(queue_136,head,index_138),queue_139),
file('SWV569-1.030.p',unknown),
[] ).
cnf(217,axiom,
equal(store(q27,seq,earray_142),queue_143),
file('SWV569-1.030.p',unknown),
[] ).
cnf(218,axiom,
equal(store(queue_143,tail,index_144),queue_145),
file('SWV569-1.030.p',unknown),
[] ).
cnf(219,axiom,
equal(store(q28,seq,earray_148),queue_149),
file('SWV569-1.030.p',unknown),
[] ).
cnf(220,axiom,
equal(store(queue_149,tail,index_150),queue_151),
file('SWV569-1.030.p',unknown),
[] ).
cnf(221,axiom,
equal(store(q2,seq,earray_154),queue_155),
file('SWV569-1.030.p',unknown),
[] ).
cnf(222,axiom,
equal(store(queue_155,tail,index_156),queue_157),
file('SWV569-1.030.p',unknown),
[] ).
cnf(223,axiom,
equal(store(queue_157,head,index_159),queue_160),
file('SWV569-1.030.p',unknown),
[] ).
cnf(224,axiom,
equal(store(q29,seq,earray_163),queue_164),
file('SWV569-1.030.p',unknown),
[] ).
cnf(225,axiom,
equal(store(queue_164,tail,index_165),queue_166),
file('SWV569-1.030.p',unknown),
[] ).
cnf(226,axiom,
equal(store(queue_166,head,index_168),queue_169),
file('SWV569-1.030.p',unknown),
[] ).
cnf(227,axiom,
equal(store(q10,seq,earray_16),queue_17),
file('SWV569-1.030.p',unknown),
[] ).
cnf(228,axiom,
equal(store(q3,seq,earray_172),queue_173),
file('SWV569-1.030.p',unknown),
[] ).
cnf(229,axiom,
equal(store(queue_173,tail,index_174),queue_175),
file('SWV569-1.030.p',unknown),
[] ).
cnf(230,axiom,
equal(store(q4,seq,earray_178),queue_179),
file('SWV569-1.030.p',unknown),
[] ).
cnf(231,axiom,
equal(store(queue_179,tail,index_180),queue_181),
file('SWV569-1.030.p',unknown),
[] ).
cnf(232,axiom,
equal(store(q5,seq,earray_184),queue_185),
file('SWV569-1.030.p',unknown),
[] ).
cnf(233,axiom,
equal(store(queue_185,tail,index_186),queue_187),
file('SWV569-1.030.p',unknown),
[] ).
cnf(234,axiom,
equal(store(queue_17,tail,index_18),queue_19),
file('SWV569-1.030.p',unknown),
[] ).
cnf(235,axiom,
equal(store(queue_187,head,index_189),queue_190),
file('SWV569-1.030.p',unknown),
[] ).
cnf(236,axiom,
equal(store(q6,seq,earray_193),queue_194),
file('SWV569-1.030.p',unknown),
[] ).
cnf(237,axiom,
equal(store(queue_194,tail,index_195),queue_196),
file('SWV569-1.030.p',unknown),
[] ).
cnf(238,axiom,
equal(store(q7,seq,earray_199),queue_200),
file('SWV569-1.030.p',unknown),
[] ).
cnf(239,axiom,
equal(store(queue_200,tail,index_201),queue_202),
file('SWV569-1.030.p',unknown),
[] ).
cnf(240,axiom,
equal(store(q8,seq,earray_205),queue_206),
file('SWV569-1.030.p',unknown),
[] ).
cnf(241,axiom,
equal(store(queue_206,tail,index_207),queue_208),
file('SWV569-1.030.p',unknown),
[] ).
cnf(242,axiom,
equal(store(queue_208,head,index_210),queue_211),
file('SWV569-1.030.p',unknown),
[] ).
cnf(243,axiom,
equal(store(q11,seq,earray_22),queue_23),
file('SWV569-1.030.p',unknown),
[] ).
cnf(244,axiom,
equal(store(queue_23,tail,index_24),queue_25),
file('SWV569-1.030.p',unknown),
[] ).
cnf(245,axiom,
equal(store(queue_25,head,index_27),queue_28),
file('SWV569-1.030.p',unknown),
[] ).
cnf(246,axiom,
equal(store(q12,seq,earray_31),queue_32),
file('SWV569-1.030.p',unknown),
[] ).
cnf(247,axiom,
equal(store(queue_32,tail,index_33),queue_34),
file('SWV569-1.030.p',unknown),
[] ).
cnf(248,axiom,
equal(store(q13,seq,earray_37),queue_38),
file('SWV569-1.030.p',unknown),
[] ).
cnf(249,axiom,
equal(store(queue_38,tail,index_39),queue_40),
file('SWV569-1.030.p',unknown),
[] ).
cnf(250,axiom,
equal(store(q14,seq,earray_43),queue_44),
file('SWV569-1.030.p',unknown),
[] ).
cnf(251,axiom,
equal(store(queue_44,tail,index_45),queue_46),
file('SWV569-1.030.p',unknown),
[] ).
cnf(252,axiom,
equal(store(queue_46,head,index_48),queue_49),
file('SWV569-1.030.p',unknown),
[] ).
cnf(253,axiom,
equal(store(q0,seq,earray_4),queue_5),
file('SWV569-1.030.p',unknown),
[] ).
cnf(254,axiom,
equal(store(q15,seq,earray_52),queue_53),
file('SWV569-1.030.p',unknown),
[] ).
cnf(255,axiom,
equal(store(queue_53,tail,index_54),queue_55),
file('SWV569-1.030.p',unknown),
[] ).
cnf(256,axiom,
equal(store(q16,seq,earray_58),queue_59),
file('SWV569-1.030.p',unknown),
[] ).
cnf(257,axiom,
equal(store(queue_59,tail,index_60),queue_61),
file('SWV569-1.030.p',unknown),
[] ).
cnf(258,axiom,
equal(store(q17,seq,earray_64),queue_65),
file('SWV569-1.030.p',unknown),
[] ).
cnf(259,axiom,
equal(store(queue_65,tail,index_66),queue_67),
file('SWV569-1.030.p',unknown),
[] ).
cnf(260,axiom,
equal(store(queue_5,tail,index_6),queue_7),
file('SWV569-1.030.p',unknown),
[] ).
cnf(261,axiom,
equal(store(queue_67,head,index_69),queue_70),
file('SWV569-1.030.p',unknown),
[] ).
cnf(262,axiom,
equal(store(q18,seq,earray_73),queue_74),
file('SWV569-1.030.p',unknown),
[] ).
cnf(263,axiom,
equal(store(queue_74,tail,index_75),queue_76),
file('SWV569-1.030.p',unknown),
[] ).
cnf(264,axiom,
equal(store(q1,seq,earray_79),queue_80),
file('SWV569-1.030.p',unknown),
[] ).
cnf(265,axiom,
equal(store(queue_80,tail,index_81),queue_82),
file('SWV569-1.030.p',unknown),
[] ).
cnf(266,axiom,
equal(store(q19,seq,earray_85),queue_86),
file('SWV569-1.030.p',unknown),
[] ).
cnf(267,axiom,
equal(store(queue_86,tail,index_87),queue_88),
file('SWV569-1.030.p',unknown),
[] ).
cnf(268,axiom,
equal(store(q20,seq,earray_91),queue_92),
file('SWV569-1.030.p',unknown),
[] ).
cnf(269,axiom,
equal(store(queue_92,tail,index_93),queue_94),
file('SWV569-1.030.p',unknown),
[] ).
cnf(270,axiom,
equal(store(queue_94,head,index_96),queue_97),
file('SWV569-1.030.p',unknown),
[] ).
cnf(271,axiom,
equal(queue_1,q0),
file('SWV569-1.030.p',unknown),
[] ).
cnf(272,axiom,
equal(queue_7,q1),
file('SWV569-1.030.p',unknown),
[] ).
cnf(273,axiom,
equal(queue_13,q10),
file('SWV569-1.030.p',unknown),
[] ).
cnf(274,axiom,
equal(queue_19,q11),
file('SWV569-1.030.p',unknown),
[] ).
cnf(275,axiom,
equal(queue_28,q12),
file('SWV569-1.030.p',unknown),
[] ).
cnf(276,axiom,
equal(queue_34,q13),
file('SWV569-1.030.p',unknown),
[] ).
cnf(277,axiom,
equal(queue_40,q14),
file('SWV569-1.030.p',unknown),
[] ).
cnf(278,axiom,
equal(queue_49,q15),
file('SWV569-1.030.p',unknown),
[] ).
cnf(279,axiom,
equal(queue_55,q16),
file('SWV569-1.030.p',unknown),
[] ).
cnf(280,axiom,
equal(queue_61,q17),
file('SWV569-1.030.p',unknown),
[] ).
cnf(281,axiom,
equal(queue_70,q18),
file('SWV569-1.030.p',unknown),
[] ).
cnf(282,axiom,
equal(queue_76,q19),
file('SWV569-1.030.p',unknown),
[] ).
cnf(283,axiom,
equal(queue_82,q2),
file('SWV569-1.030.p',unknown),
[] ).
cnf(284,axiom,
equal(queue_88,q20),
file('SWV569-1.030.p',unknown),
[] ).
cnf(285,axiom,
equal(queue_97,q21),
file('SWV569-1.030.p',unknown),
[] ).
cnf(286,axiom,
equal(queue_103,q22),
file('SWV569-1.030.p',unknown),
[] ).
cnf(287,axiom,
equal(queue_109,q23),
file('SWV569-1.030.p',unknown),
[] ).
cnf(288,axiom,
equal(queue_118,q24),
file('SWV569-1.030.p',unknown),
[] ).
cnf(289,axiom,
equal(queue_124,q25),
file('SWV569-1.030.p',unknown),
[] ).
cnf(290,axiom,
equal(queue_130,q26),
file('SWV569-1.030.p',unknown),
[] ).
cnf(291,axiom,
equal(queue_139,q27),
file('SWV569-1.030.p',unknown),
[] ).
cnf(292,axiom,
equal(queue_145,q28),
file('SWV569-1.030.p',unknown),
[] ).
cnf(293,axiom,
equal(queue_151,q29),
file('SWV569-1.030.p',unknown),
[] ).
cnf(294,axiom,
equal(queue_160,q3),
file('SWV569-1.030.p',unknown),
[] ).
cnf(295,axiom,
equal(queue_169,q30),
file('SWV569-1.030.p',unknown),
[] ).
cnf(296,axiom,
equal(queue_175,q4),
file('SWV569-1.030.p',unknown),
[] ).
cnf(297,axiom,
equal(queue_181,q5),
file('SWV569-1.030.p',unknown),
[] ).
cnf(298,axiom,
equal(queue_190,q6),
file('SWV569-1.030.p',unknown),
[] ).
cnf(299,axiom,
equal(queue_196,q7),
file('SWV569-1.030.p',unknown),
[] ).
cnf(300,axiom,
equal(queue_202,q8),
file('SWV569-1.030.p',unknown),
[] ).
cnf(301,axiom,
equal(queue_211,q9),
file('SWV569-1.030.p',unknown),
[] ).
cnf(302,axiom,
~ equal(elem_214,e10),
file('SWV569-1.030.p',unknown),
[] ).
cnf(303,plain,
equal(store(queue_94,head,index_96),q21),
inference(rew,[status(thm),theory(equality)],[285,270]),
[iquote('0:Rew:285.0,270.0')] ).
cnf(304,plain,
equal(store(queue_86,tail,index_87),q20),
inference(rew,[status(thm),theory(equality)],[284,267]),
[iquote('0:Rew:284.0,267.0')] ).
cnf(305,plain,
equal(store(queue_80,tail,index_81),q2),
inference(rew,[status(thm),theory(equality)],[283,265]),
[iquote('0:Rew:283.0,265.0')] ).
cnf(306,plain,
equal(store(queue_74,tail,index_75),q19),
inference(rew,[status(thm),theory(equality)],[282,263]),
[iquote('0:Rew:282.0,263.0')] ).
cnf(307,plain,
equal(store(queue_67,head,index_69),q18),
inference(rew,[status(thm),theory(equality)],[281,261]),
[iquote('0:Rew:281.0,261.0')] ).
cnf(308,plain,
equal(store(queue_5,tail,index_6),q1),
inference(rew,[status(thm),theory(equality)],[272,260]),
[iquote('0:Rew:272.0,260.0')] ).
cnf(309,plain,
equal(store(queue_59,tail,index_60),q17),
inference(rew,[status(thm),theory(equality)],[280,257]),
[iquote('0:Rew:280.0,257.0')] ).
cnf(310,plain,
equal(store(queue_53,tail,index_54),q16),
inference(rew,[status(thm),theory(equality)],[279,255]),
[iquote('0:Rew:279.0,255.0')] ).
cnf(311,plain,
equal(store(queue_46,head,index_48),q15),
inference(rew,[status(thm),theory(equality)],[278,252]),
[iquote('0:Rew:278.0,252.0')] ).
cnf(312,plain,
equal(store(queue_38,tail,index_39),q14),
inference(rew,[status(thm),theory(equality)],[277,249]),
[iquote('0:Rew:277.0,249.0')] ).
cnf(313,plain,
equal(store(queue_32,tail,index_33),q13),
inference(rew,[status(thm),theory(equality)],[276,247]),
[iquote('0:Rew:276.0,247.0')] ).
cnf(314,plain,
equal(store(queue_25,head,index_27),q12),
inference(rew,[status(thm),theory(equality)],[275,245]),
[iquote('0:Rew:275.0,245.0')] ).
cnf(315,plain,
equal(store(queue_208,head,index_210),q9),
inference(rew,[status(thm),theory(equality)],[301,242]),
[iquote('0:Rew:301.0,242.0')] ).
cnf(316,plain,
equal(store(queue_200,tail,index_201),q8),
inference(rew,[status(thm),theory(equality)],[300,239]),
[iquote('0:Rew:300.0,239.0')] ).
cnf(317,plain,
equal(store(queue_194,tail,index_195),q7),
inference(rew,[status(thm),theory(equality)],[299,237]),
[iquote('0:Rew:299.0,237.0')] ).
cnf(318,plain,
equal(store(queue_187,head,index_189),q6),
inference(rew,[status(thm),theory(equality)],[298,235]),
[iquote('0:Rew:298.0,235.0')] ).
cnf(319,plain,
equal(store(queue_17,tail,index_18),q11),
inference(rew,[status(thm),theory(equality)],[274,234]),
[iquote('0:Rew:274.0,234.0')] ).
cnf(320,plain,
equal(store(queue_179,tail,index_180),q5),
inference(rew,[status(thm),theory(equality)],[297,231]),
[iquote('0:Rew:297.0,231.0')] ).
cnf(321,plain,
equal(store(queue_173,tail,index_174),q4),
inference(rew,[status(thm),theory(equality)],[296,229]),
[iquote('0:Rew:296.0,229.0')] ).
cnf(322,plain,
equal(store(queue_166,head,index_168),q30),
inference(rew,[status(thm),theory(equality)],[295,226]),
[iquote('0:Rew:295.0,226.0')] ).
cnf(323,plain,
equal(store(queue_157,head,index_159),q3),
inference(rew,[status(thm),theory(equality)],[294,223]),
[iquote('0:Rew:294.0,223.0')] ).
cnf(324,plain,
equal(store(queue_149,tail,index_150),q29),
inference(rew,[status(thm),theory(equality)],[293,220]),
[iquote('0:Rew:293.0,220.0')] ).
cnf(325,plain,
equal(store(queue_143,tail,index_144),q28),
inference(rew,[status(thm),theory(equality)],[292,218]),
[iquote('0:Rew:292.0,218.0')] ).
cnf(326,plain,
equal(store(queue_136,head,index_138),q27),
inference(rew,[status(thm),theory(equality)],[291,216]),
[iquote('0:Rew:291.0,216.0')] ).
cnf(327,plain,
equal(store(queue_128,tail,index_129),q26),
inference(rew,[status(thm),theory(equality)],[290,213]),
[iquote('0:Rew:290.0,213.0')] ).
cnf(328,plain,
equal(store(queue_11,tail,index_12),q10),
inference(rew,[status(thm),theory(equality)],[273,212]),
[iquote('0:Rew:273.0,212.0')] ).
cnf(329,plain,
equal(store(queue_122,tail,index_123),q25),
inference(rew,[status(thm),theory(equality)],[289,210]),
[iquote('0:Rew:289.0,210.0')] ).
cnf(330,plain,
equal(store(queue_115,head,index_117),q24),
inference(rew,[status(thm),theory(equality)],[288,208]),
[iquote('0:Rew:288.0,208.0')] ).
cnf(331,plain,
equal(store(queue_107,tail,index_108),q23),
inference(rew,[status(thm),theory(equality)],[287,204]),
[iquote('0:Rew:287.0,204.0')] ).
cnf(332,plain,
equal(store(queue_101,tail,index_102),q22),
inference(rew,[status(thm),theory(equality)],[286,202]),
[iquote('0:Rew:286.0,202.0')] ).
cnf(333,plain,
equal(store(q,head,index_0),q0),
inference(rew,[status(thm),theory(equality)],[271,200]),
[iquote('0:Rew:271.0,200.0')] ).
cnf(504,plain,
~ equal(index_18,index_15),
inference(spl,[status(thm),theory(equality)],[151,55]),
[iquote('0:SpL:151.0,55.0')] ).
cnf(645,plain,
~ equal(s(index_18),index_15),
inference(spl,[status(thm),theory(equality)],[151,54]),
[iquote('0:SpL:151.0,54.0')] ).
cnf(685,plain,
~ equal(s(s(index_18)),index_15),
inference(spl,[status(thm),theory(equality)],[151,53]),
[iquote('0:SpL:151.0,53.0')] ).
cnf(725,plain,
~ equal(s(s(s(index_18))),index_15),
inference(spl,[status(thm),theory(equality)],[151,52]),
[iquote('0:SpL:151.0,52.0')] ).
cnf(743,plain,
equal(select(q21,head),index_96),
inference(spr,[status(thm),theory(equality)],[303,1]),
[iquote('0:SpR:303.0,1.0')] ).
cnf(744,plain,
equal(select(q18,head),index_69),
inference(spr,[status(thm),theory(equality)],[307,1]),
[iquote('0:SpR:307.0,1.0')] ).
cnf(745,plain,
equal(select(q15,head),index_48),
inference(spr,[status(thm),theory(equality)],[311,1]),
[iquote('0:SpR:311.0,1.0')] ).
cnf(746,plain,
equal(select(q12,head),index_27),
inference(spr,[status(thm),theory(equality)],[314,1]),
[iquote('0:SpR:314.0,1.0')] ).
cnf(747,plain,
equal(select(q9,head),index_210),
inference(spr,[status(thm),theory(equality)],[315,1]),
[iquote('0:SpR:315.0,1.0')] ).
cnf(748,plain,
equal(select(q6,head),index_189),
inference(spr,[status(thm),theory(equality)],[318,1]),
[iquote('0:SpR:318.0,1.0')] ).
cnf(749,plain,
equal(select(q30,head),index_168),
inference(spr,[status(thm),theory(equality)],[322,1]),
[iquote('0:SpR:322.0,1.0')] ).
cnf(750,plain,
equal(select(q3,head),index_159),
inference(spr,[status(thm),theory(equality)],[323,1]),
[iquote('0:SpR:323.0,1.0')] ).
cnf(751,plain,
equal(select(q27,head),index_138),
inference(spr,[status(thm),theory(equality)],[326,1]),
[iquote('0:SpR:326.0,1.0')] ).
cnf(752,plain,
equal(select(q24,head),index_117),
inference(spr,[status(thm),theory(equality)],[330,1]),
[iquote('0:SpR:330.0,1.0')] ).
cnf(753,plain,
equal(select(q0,head),index_0),
inference(spr,[status(thm),theory(equality)],[333,1]),
[iquote('0:SpR:333.0,1.0')] ).
cnf(754,plain,
equal(select(queue_94,tail),index_93),
inference(spr,[status(thm),theory(equality)],[269,1]),
[iquote('0:SpR:269.0,1.0')] ).
cnf(755,plain,
equal(select(q20,tail),index_87),
inference(spr,[status(thm),theory(equality)],[304,1]),
[iquote('0:SpR:304.0,1.0')] ).
cnf(756,plain,
equal(select(q2,tail),index_81),
inference(spr,[status(thm),theory(equality)],[305,1]),
[iquote('0:SpR:305.0,1.0')] ).
cnf(757,plain,
equal(select(q19,tail),index_75),
inference(spr,[status(thm),theory(equality)],[306,1]),
[iquote('0:SpR:306.0,1.0')] ).
cnf(758,plain,
equal(select(q1,tail),index_6),
inference(spr,[status(thm),theory(equality)],[308,1]),
[iquote('0:SpR:308.0,1.0')] ).
cnf(759,plain,
equal(select(queue_67,tail),index_66),
inference(spr,[status(thm),theory(equality)],[259,1]),
[iquote('0:SpR:259.0,1.0')] ).
cnf(760,plain,
equal(select(q17,tail),index_60),
inference(spr,[status(thm),theory(equality)],[309,1]),
[iquote('0:SpR:309.0,1.0')] ).
cnf(761,plain,
equal(select(q16,tail),index_54),
inference(spr,[status(thm),theory(equality)],[310,1]),
[iquote('0:SpR:310.0,1.0')] ).
cnf(762,plain,
equal(select(queue_46,tail),index_45),
inference(spr,[status(thm),theory(equality)],[251,1]),
[iquote('0:SpR:251.0,1.0')] ).
cnf(763,plain,
equal(select(q14,tail),index_39),
inference(spr,[status(thm),theory(equality)],[312,1]),
[iquote('0:SpR:312.0,1.0')] ).
cnf(764,plain,
equal(select(q13,tail),index_33),
inference(spr,[status(thm),theory(equality)],[313,1]),
[iquote('0:SpR:313.0,1.0')] ).
cnf(765,plain,
equal(select(queue_25,tail),index_24),
inference(spr,[status(thm),theory(equality)],[244,1]),
[iquote('0:SpR:244.0,1.0')] ).
cnf(766,plain,
equal(select(queue_208,tail),index_207),
inference(spr,[status(thm),theory(equality)],[241,1]),
[iquote('0:SpR:241.0,1.0')] ).
cnf(767,plain,
equal(select(q8,tail),index_201),
inference(spr,[status(thm),theory(equality)],[316,1]),
[iquote('0:SpR:316.0,1.0')] ).
cnf(768,plain,
equal(select(q7,tail),index_195),
inference(spr,[status(thm),theory(equality)],[317,1]),
[iquote('0:SpR:317.0,1.0')] ).
cnf(769,plain,
equal(select(q11,tail),index_18),
inference(spr,[status(thm),theory(equality)],[319,1]),
[iquote('0:SpR:319.0,1.0')] ).
cnf(770,plain,
equal(select(queue_187,tail),index_186),
inference(spr,[status(thm),theory(equality)],[233,1]),
[iquote('0:SpR:233.0,1.0')] ).
cnf(771,plain,
equal(select(q5,tail),index_180),
inference(spr,[status(thm),theory(equality)],[320,1]),
[iquote('0:SpR:320.0,1.0')] ).
cnf(772,plain,
equal(select(q4,tail),index_174),
inference(spr,[status(thm),theory(equality)],[321,1]),
[iquote('0:SpR:321.0,1.0')] ).
cnf(774,plain,
equal(select(queue_157,tail),index_156),
inference(spr,[status(thm),theory(equality)],[222,1]),
[iquote('0:SpR:222.0,1.0')] ).
cnf(775,plain,
equal(select(q29,tail),index_150),
inference(spr,[status(thm),theory(equality)],[324,1]),
[iquote('0:SpR:324.0,1.0')] ).
cnf(776,plain,
equal(select(q28,tail),index_144),
inference(spr,[status(thm),theory(equality)],[325,1]),
[iquote('0:SpR:325.0,1.0')] ).
cnf(777,plain,
equal(select(queue_136,tail),index_135),
inference(spr,[status(thm),theory(equality)],[215,1]),
[iquote('0:SpR:215.0,1.0')] ).
cnf(778,plain,
equal(select(q26,tail),index_129),
inference(spr,[status(thm),theory(equality)],[327,1]),
[iquote('0:SpR:327.0,1.0')] ).
cnf(779,plain,
equal(select(q10,tail),index_12),
inference(spr,[status(thm),theory(equality)],[328,1]),
[iquote('0:SpR:328.0,1.0')] ).
cnf(780,plain,
equal(select(q25,tail),index_123),
inference(spr,[status(thm),theory(equality)],[329,1]),
[iquote('0:SpR:329.0,1.0')] ).
cnf(781,plain,
equal(select(queue_115,tail),index_114),
inference(spr,[status(thm),theory(equality)],[207,1]),
[iquote('0:SpR:207.0,1.0')] ).
cnf(782,plain,
equal(select(q23,tail),index_108),
inference(spr,[status(thm),theory(equality)],[331,1]),
[iquote('0:SpR:331.0,1.0')] ).
cnf(783,plain,
equal(select(q22,tail),index_102),
inference(spr,[status(thm),theory(equality)],[332,1]),
[iquote('0:SpR:332.0,1.0')] ).
cnf(784,plain,
equal(select(queue_92,seq),earray_91),
inference(spr,[status(thm),theory(equality)],[268,1]),
[iquote('0:SpR:268.0,1.0')] ).
cnf(785,plain,
equal(select(queue_86,seq),earray_85),
inference(spr,[status(thm),theory(equality)],[266,1]),
[iquote('0:SpR:266.0,1.0')] ).
cnf(787,plain,
equal(select(queue_74,seq),earray_73),
inference(spr,[status(thm),theory(equality)],[262,1]),
[iquote('0:SpR:262.0,1.0')] ).
cnf(788,plain,
equal(select(queue_65,seq),earray_64),
inference(spr,[status(thm),theory(equality)],[258,1]),
[iquote('0:SpR:258.0,1.0')] ).
cnf(789,plain,
equal(select(queue_59,seq),earray_58),
inference(spr,[status(thm),theory(equality)],[256,1]),
[iquote('0:SpR:256.0,1.0')] ).
cnf(790,plain,
equal(select(queue_53,seq),earray_52),
inference(spr,[status(thm),theory(equality)],[254,1]),
[iquote('0:SpR:254.0,1.0')] ).
cnf(792,plain,
equal(select(queue_44,seq),earray_43),
inference(spr,[status(thm),theory(equality)],[250,1]),
[iquote('0:SpR:250.0,1.0')] ).
cnf(793,plain,
equal(select(queue_38,seq),earray_37),
inference(spr,[status(thm),theory(equality)],[248,1]),
[iquote('0:SpR:248.0,1.0')] ).
cnf(794,plain,
equal(select(queue_32,seq),earray_31),
inference(spr,[status(thm),theory(equality)],[246,1]),
[iquote('0:SpR:246.0,1.0')] ).
cnf(795,plain,
equal(select(queue_23,seq),earray_22),
inference(spr,[status(thm),theory(equality)],[243,1]),
[iquote('0:SpR:243.0,1.0')] ).
cnf(802,plain,
equal(select(queue_17,seq),earray_16),
inference(spr,[status(thm),theory(equality)],[227,1]),
[iquote('0:SpR:227.0,1.0')] ).
cnf(803,plain,
equal(select(queue_164,seq),earray_163),
inference(spr,[status(thm),theory(equality)],[224,1]),
[iquote('0:SpR:224.0,1.0')] ).
cnf(805,plain,
equal(select(queue_149,seq),earray_148),
inference(spr,[status(thm),theory(equality)],[219,1]),
[iquote('0:SpR:219.0,1.0')] ).
cnf(806,plain,
equal(select(queue_143,seq),earray_142),
inference(spr,[status(thm),theory(equality)],[217,1]),
[iquote('0:SpR:217.0,1.0')] ).
cnf(807,plain,
equal(select(queue_134,seq),earray_133),
inference(spr,[status(thm),theory(equality)],[214,1]),
[iquote('0:SpR:214.0,1.0')] ).
cnf(808,plain,
equal(select(queue_128,seq),earray_127),
inference(spr,[status(thm),theory(equality)],[211,1]),
[iquote('0:SpR:211.0,1.0')] ).
cnf(809,plain,
equal(select(queue_122,seq),earray_121),
inference(spr,[status(thm),theory(equality)],[209,1]),
[iquote('0:SpR:209.0,1.0')] ).
cnf(810,plain,
equal(select(queue_113,seq),earray_112),
inference(spr,[status(thm),theory(equality)],[206,1]),
[iquote('0:SpR:206.0,1.0')] ).
cnf(812,plain,
equal(select(queue_107,seq),earray_106),
inference(spr,[status(thm),theory(equality)],[203,1]),
[iquote('0:SpR:203.0,1.0')] ).
cnf(813,plain,
equal(select(queue_101,seq),earray_100),
inference(spr,[status(thm),theory(equality)],[201,1]),
[iquote('0:SpR:201.0,1.0')] ).
cnf(833,plain,
equal(select(earray_16,index_15),e10),
inference(spr,[status(thm),theory(equality)],[75,1]),
[iquote('0:SpR:75.0,1.0')] ).
cnf(844,plain,
equal(index_168,index_213),
inference(rew,[status(thm),theory(equality)],[166,749]),
[iquote('0:Rew:166.0,749.0')] ).
cnf(845,plain,
equal(s(index_167),index_213),
inference(rew,[status(thm),theory(equality)],[844,147]),
[iquote('0:Rew:844.0,147.0')] ).
cnf(847,plain,
equal(store(queue_166,head,index_213),q30),
inference(rew,[status(thm),theory(equality)],[844,322]),
[iquote('0:Rew:844.0,322.0')] ).
cnf(851,plain,
equal(index_87,index_90),
inference(rew,[status(thm),theory(equality)],[195,755]),
[iquote('0:Rew:195.0,755.0')] ).
cnf(852,plain,
equal(s(index_84),index_90),
inference(rew,[status(thm),theory(equality)],[851,193]),
[iquote('0:Rew:851.0,193.0')] ).
cnf(854,plain,
equal(store(queue_86,tail,index_90),q20),
inference(rew,[status(thm),theory(equality)],[851,304]),
[iquote('0:Rew:851.0,304.0')] ).
cnf(858,plain,
equal(index_81,index_153),
inference(rew,[status(thm),theory(equality)],[140,756]),
[iquote('0:Rew:140.0,756.0')] ).
cnf(859,plain,
equal(s(index_78),index_153),
inference(rew,[status(thm),theory(equality)],[858,191]),
[iquote('0:Rew:858.0,191.0')] ).
cnf(861,plain,
equal(store(queue_80,tail,index_153),q2),
inference(rew,[status(thm),theory(equality)],[858,305]),
[iquote('0:Rew:858.0,305.0')] ).
cnf(865,plain,
equal(index_75,index_84),
inference(rew,[status(thm),theory(equality)],[192,757]),
[iquote('0:Rew:192.0,757.0')] ).
cnf(866,plain,
equal(s(index_72),index_84),
inference(rew,[status(thm),theory(equality)],[865,189]),
[iquote('0:Rew:865.0,189.0')] ).
cnf(868,plain,
equal(store(queue_74,tail,index_84),q19),
inference(rew,[status(thm),theory(equality)],[865,306]),
[iquote('0:Rew:865.0,306.0')] ).
cnf(872,plain,
equal(index_6,index_78),
inference(rew,[status(thm),theory(equality)],[190,758]),
[iquote('0:Rew:190.0,758.0')] ).
cnf(873,plain,
equal(s(index_3),index_78),
inference(rew,[status(thm),theory(equality)],[872,182]),
[iquote('0:Rew:872.0,182.0')] ).
cnf(875,plain,
equal(store(queue_5,tail,index_78),q1),
inference(rew,[status(thm),theory(equality)],[872,308]),
[iquote('0:Rew:872.0,308.0')] ).
cnf(879,plain,
equal(index_60,index_63),
inference(rew,[status(thm),theory(equality)],[184,760]),
[iquote('0:Rew:184.0,760.0')] ).
cnf(880,plain,
equal(s(index_57),index_63),
inference(rew,[status(thm),theory(equality)],[879,183]),
[iquote('0:Rew:879.0,183.0')] ).
cnf(882,plain,
equal(store(queue_59,tail,index_63),q17),
inference(rew,[status(thm),theory(equality)],[879,309]),
[iquote('0:Rew:879.0,309.0')] ).
cnf(886,plain,
equal(index_54,index_57),
inference(rew,[status(thm),theory(equality)],[181,761]),
[iquote('0:Rew:181.0,761.0')] ).
cnf(887,plain,
equal(s(index_51),index_57),
inference(rew,[status(thm),theory(equality)],[886,180]),
[iquote('0:Rew:886.0,180.0')] ).
cnf(889,plain,
equal(store(queue_53,tail,index_57),q16),
inference(rew,[status(thm),theory(equality)],[886,310]),
[iquote('0:Rew:886.0,310.0')] ).
cnf(893,plain,
equal(index_39,index_42),
inference(rew,[status(thm),theory(equality)],[175,763]),
[iquote('0:Rew:175.0,763.0')] ).
cnf(894,plain,
equal(s(index_36),index_42),
inference(rew,[status(thm),theory(equality)],[893,174]),
[iquote('0:Rew:893.0,174.0')] ).
cnf(896,plain,
equal(store(queue_38,tail,index_42),q14),
inference(rew,[status(thm),theory(equality)],[893,312]),
[iquote('0:Rew:893.0,312.0')] ).
cnf(900,plain,
equal(index_33,index_36),
inference(rew,[status(thm),theory(equality)],[173,764]),
[iquote('0:Rew:173.0,764.0')] ).
cnf(901,plain,
equal(s(index_30),index_36),
inference(rew,[status(thm),theory(equality)],[900,172]),
[iquote('0:Rew:900.0,172.0')] ).
cnf(903,plain,
equal(store(queue_32,tail,index_36),q13),
inference(rew,[status(thm),theory(equality)],[900,313]),
[iquote('0:Rew:900.0,313.0')] ).
cnf(907,plain,
equal(index_201,index_204),
inference(rew,[status(thm),theory(equality)],[161,767]),
[iquote('0:Rew:161.0,767.0')] ).
cnf(908,plain,
equal(s(index_198),index_204),
inference(rew,[status(thm),theory(equality)],[907,160]),
[iquote('0:Rew:907.0,160.0')] ).
cnf(910,plain,
equal(store(queue_200,tail,index_204),q8),
inference(rew,[status(thm),theory(equality)],[907,316]),
[iquote('0:Rew:907.0,316.0')] ).
cnf(914,plain,
equal(index_195,index_198),
inference(rew,[status(thm),theory(equality)],[159,768]),
[iquote('0:Rew:159.0,768.0')] ).
cnf(915,plain,
equal(s(index_192),index_198),
inference(rew,[status(thm),theory(equality)],[914,158]),
[iquote('0:Rew:914.0,158.0')] ).
cnf(917,plain,
equal(store(queue_194,tail,index_198),q7),
inference(rew,[status(thm),theory(equality)],[914,317]),
[iquote('0:Rew:914.0,317.0')] ).
cnf(921,plain,
equal(index_18,index_21),
inference(rew,[status(thm),theory(equality)],[164,769]),
[iquote('0:Rew:164.0,769.0')] ).
cnf(922,plain,
equal(s(index_15),index_21),
inference(rew,[status(thm),theory(equality)],[921,151]),
[iquote('0:Rew:921.0,151.0')] ).
cnf(923,plain,
~ equal(index_21,index_15),
inference(rew,[status(thm),theory(equality)],[921,504]),
[iquote('0:Rew:921.0,504.0')] ).
cnf(924,plain,
equal(store(queue_17,tail,index_21),q11),
inference(rew,[status(thm),theory(equality)],[921,319]),
[iquote('0:Rew:921.0,319.0')] ).
cnf(925,plain,
~ equal(s(index_21),index_15),
inference(rew,[status(thm),theory(equality)],[921,645]),
[iquote('0:Rew:921.0,645.0')] ).
cnf(926,plain,
~ equal(s(s(index_21)),index_15),
inference(rew,[status(thm),theory(equality)],[921,685]),
[iquote('0:Rew:921.0,685.0')] ).
cnf(927,plain,
~ equal(s(s(s(index_21))),index_15),
inference(rew,[status(thm),theory(equality)],[921,725]),
[iquote('0:Rew:921.0,725.0')] ).
cnf(928,plain,
equal(index_180,index_183),
inference(rew,[status(thm),theory(equality)],[153,771]),
[iquote('0:Rew:153.0,771.0')] ).
cnf(929,plain,
equal(s(index_177),index_183),
inference(rew,[status(thm),theory(equality)],[928,152]),
[iquote('0:Rew:928.0,152.0')] ).
cnf(931,plain,
equal(store(queue_179,tail,index_183),q5),
inference(rew,[status(thm),theory(equality)],[928,320]),
[iquote('0:Rew:928.0,320.0')] ).
cnf(935,plain,
equal(index_174,index_177),
inference(rew,[status(thm),theory(equality)],[150,772]),
[iquote('0:Rew:150.0,772.0')] ).
cnf(936,plain,
equal(s(index_171),index_177),
inference(rew,[status(thm),theory(equality)],[935,149]),
[iquote('0:Rew:935.0,149.0')] ).
cnf(938,plain,
equal(store(queue_173,tail,index_177),q4),
inference(rew,[status(thm),theory(equality)],[935,321]),
[iquote('0:Rew:935.0,321.0')] ).
cnf(942,plain,
equal(index_150,index_162),
inference(rew,[status(thm),theory(equality)],[144,775]),
[iquote('0:Rew:144.0,775.0')] ).
cnf(943,plain,
equal(s(index_147),index_162),
inference(rew,[status(thm),theory(equality)],[942,139]),
[iquote('0:Rew:942.0,139.0')] ).
cnf(945,plain,
equal(store(queue_149,tail,index_162),q29),
inference(rew,[status(thm),theory(equality)],[942,324]),
[iquote('0:Rew:942.0,324.0')] ).
cnf(949,plain,
equal(index_144,index_147),
inference(rew,[status(thm),theory(equality)],[137,776]),
[iquote('0:Rew:137.0,776.0')] ).
cnf(950,plain,
equal(s(index_141),index_147),
inference(rew,[status(thm),theory(equality)],[949,136]),
[iquote('0:Rew:949.0,136.0')] ).
cnf(952,plain,
equal(store(queue_143,tail,index_147),q28),
inference(rew,[status(thm),theory(equality)],[949,325]),
[iquote('0:Rew:949.0,325.0')] ).
cnf(956,plain,
equal(index_129,index_132),
inference(rew,[status(thm),theory(equality)],[131,778]),
[iquote('0:Rew:131.0,778.0')] ).
cnf(957,plain,
equal(s(index_126),index_132),
inference(rew,[status(thm),theory(equality)],[956,130]),
[iquote('0:Rew:956.0,130.0')] ).
cnf(959,plain,
equal(store(queue_128,tail,index_132),q26),
inference(rew,[status(thm),theory(equality)],[956,327]),
[iquote('0:Rew:956.0,327.0')] ).
cnf(963,plain,
equal(index_12,index_15),
inference(rew,[status(thm),theory(equality)],[138,779]),
[iquote('0:Rew:138.0,779.0')] ).
cnf(964,plain,
equal(s(index_9),index_15),
inference(rew,[status(thm),theory(equality)],[963,126]),
[iquote('0:Rew:963.0,126.0')] ).
cnf(966,plain,
equal(store(queue_11,tail,index_15),q10),
inference(rew,[status(thm),theory(equality)],[963,328]),
[iquote('0:Rew:963.0,328.0')] ).
cnf(970,plain,
equal(index_123,index_126),
inference(rew,[status(thm),theory(equality)],[129,780]),
[iquote('0:Rew:129.0,780.0')] ).
cnf(971,plain,
equal(s(index_120),index_126),
inference(rew,[status(thm),theory(equality)],[970,128]),
[iquote('0:Rew:970.0,128.0')] ).
cnf(973,plain,
equal(store(queue_122,tail,index_126),q25),
inference(rew,[status(thm),theory(equality)],[970,329]),
[iquote('0:Rew:970.0,329.0')] ).
cnf(977,plain,
equal(index_108,index_111),
inference(rew,[status(thm),theory(equality)],[122,782]),
[iquote('0:Rew:122.0,782.0')] ).
cnf(978,plain,
equal(s(index_105),index_111),
inference(rew,[status(thm),theory(equality)],[977,121]),
[iquote('0:Rew:977.0,121.0')] ).
cnf(980,plain,
equal(store(queue_107,tail,index_111),q23),
inference(rew,[status(thm),theory(equality)],[977,331]),
[iquote('0:Rew:977.0,331.0')] ).
cnf(984,plain,
equal(index_102,index_105),
inference(rew,[status(thm),theory(equality)],[120,783]),
[iquote('0:Rew:120.0,783.0')] ).
cnf(985,plain,
equal(s(index_99),index_105),
inference(rew,[status(thm),theory(equality)],[984,119]),
[iquote('0:Rew:984.0,119.0')] ).
cnf(987,plain,
equal(store(queue_101,tail,index_105),q22),
inference(rew,[status(thm),theory(equality)],[984,332]),
[iquote('0:Rew:984.0,332.0')] ).
cnf(1001,plain,
~ equal(index_24,index_15),
inference(rew,[status(thm),theory(equality)],[167,925]),
[iquote('0:Rew:167.0,925.0')] ).
cnf(1026,plain,
~ equal(s(index_24),index_15),
inference(rew,[status(thm),theory(equality)],[167,926]),
[iquote('0:Rew:167.0,926.0')] ).
cnf(1056,plain,
~ equal(s(s(index_24)),index_15),
inference(rew,[status(thm),theory(equality)],[167,927]),
[iquote('0:Rew:167.0,927.0')] ).
cnf(1369,plain,
~ equal(s(s(s(s(index_21)))),index_15),
inference(spl,[status(thm),theory(equality)],[922,51]),
[iquote('0:SpL:922.0,51.0')] ).
cnf(1389,plain,
~ equal(s(s(s(index_24))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1369]),
[iquote('0:Rew:167.0,1369.0')] ).
cnf(1433,plain,
~ equal(s(s(s(s(s(index_21))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,50]),
[iquote('0:SpL:922.0,50.0')] ).
cnf(1453,plain,
~ equal(s(s(s(s(index_24)))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1433]),
[iquote('0:Rew:167.0,1433.0')] ).
cnf(1497,plain,
~ equal(s(s(s(s(s(s(index_21)))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,49]),
[iquote('0:SpL:922.0,49.0')] ).
cnf(1517,plain,
~ equal(s(s(s(s(s(index_24))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1497]),
[iquote('0:Rew:167.0,1497.0')] ).
cnf(1561,plain,
~ equal(s(s(s(s(s(s(s(index_21))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,48]),
[iquote('0:SpL:922.0,48.0')] ).
cnf(1581,plain,
~ equal(s(s(s(s(s(s(index_24)))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1561]),
[iquote('0:Rew:167.0,1561.0')] ).
cnf(1625,plain,
~ equal(s(s(s(s(s(s(s(s(index_21)))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,47]),
[iquote('0:SpL:922.0,47.0')] ).
cnf(1645,plain,
~ equal(s(s(s(s(s(s(s(index_24))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1625]),
[iquote('0:Rew:167.0,1625.0')] ).
cnf(1661,plain,
( equal(head,u)
| equal(select(queue_94,u),select(q21,u)) ),
inference(spr,[status(thm),theory(equality)],[303,2]),
[iquote('0:SpR:303.0,2.1')] ).
cnf(1662,plain,
( equal(head,u)
| equal(select(queue_67,u),select(q18,u)) ),
inference(spr,[status(thm),theory(equality)],[307,2]),
[iquote('0:SpR:307.0,2.1')] ).
cnf(1663,plain,
( equal(head,u)
| equal(select(queue_46,u),select(q15,u)) ),
inference(spr,[status(thm),theory(equality)],[311,2]),
[iquote('0:SpR:311.0,2.1')] ).
cnf(1664,plain,
( equal(head,u)
| equal(select(queue_25,u),select(q12,u)) ),
inference(spr,[status(thm),theory(equality)],[314,2]),
[iquote('0:SpR:314.0,2.1')] ).
cnf(1665,plain,
( equal(head,u)
| equal(select(queue_208,u),select(q9,u)) ),
inference(spr,[status(thm),theory(equality)],[315,2]),
[iquote('0:SpR:315.0,2.1')] ).
cnf(1666,plain,
( equal(head,u)
| equal(select(queue_187,u),select(q6,u)) ),
inference(spr,[status(thm),theory(equality)],[318,2]),
[iquote('0:SpR:318.0,2.1')] ).
cnf(1667,plain,
( equal(head,u)
| equal(select(queue_157,u),select(q3,u)) ),
inference(spr,[status(thm),theory(equality)],[323,2]),
[iquote('0:SpR:323.0,2.1')] ).
cnf(1668,plain,
( equal(head,u)
| equal(select(queue_136,u),select(q27,u)) ),
inference(spr,[status(thm),theory(equality)],[326,2]),
[iquote('0:SpR:326.0,2.1')] ).
cnf(1669,plain,
( equal(head,u)
| equal(select(queue_115,u),select(q24,u)) ),
inference(spr,[status(thm),theory(equality)],[330,2]),
[iquote('0:SpR:330.0,2.1')] ).
cnf(1670,plain,
( equal(head,u)
| equal(select(q,u),select(q0,u)) ),
inference(spr,[status(thm),theory(equality)],[333,2]),
[iquote('0:SpR:333.0,2.1')] ).
cnf(1671,plain,
( equal(head,u)
| equal(select(queue_166,u),select(q30,u)) ),
inference(spr,[status(thm),theory(equality)],[847,2]),
[iquote('0:SpR:847.0,2.1')] ).
cnf(1672,plain,
( equal(tail,u)
| equal(select(queue_92,u),select(queue_94,u)) ),
inference(spr,[status(thm),theory(equality)],[269,2]),
[iquote('0:SpR:269.0,2.1')] ).
cnf(1673,plain,
( equal(tail,u)
| equal(select(queue_65,u),select(queue_67,u)) ),
inference(spr,[status(thm),theory(equality)],[259,2]),
[iquote('0:SpR:259.0,2.1')] ).
cnf(1674,plain,
( equal(tail,u)
| equal(select(queue_44,u),select(queue_46,u)) ),
inference(spr,[status(thm),theory(equality)],[251,2]),
[iquote('0:SpR:251.0,2.1')] ).
cnf(1675,plain,
( equal(tail,u)
| equal(select(queue_23,u),select(queue_25,u)) ),
inference(spr,[status(thm),theory(equality)],[244,2]),
[iquote('0:SpR:244.0,2.1')] ).
cnf(1676,plain,
( equal(tail,u)
| equal(select(queue_206,u),select(queue_208,u)) ),
inference(spr,[status(thm),theory(equality)],[241,2]),
[iquote('0:SpR:241.0,2.1')] ).
cnf(1677,plain,
( equal(tail,u)
| equal(select(queue_185,u),select(queue_187,u)) ),
inference(spr,[status(thm),theory(equality)],[233,2]),
[iquote('0:SpR:233.0,2.1')] ).
cnf(1678,plain,
( equal(tail,u)
| equal(select(queue_164,u),select(queue_166,u)) ),
inference(spr,[status(thm),theory(equality)],[225,2]),
[iquote('0:SpR:225.0,2.1')] ).
cnf(1679,plain,
( equal(tail,u)
| equal(select(queue_155,u),select(queue_157,u)) ),
inference(spr,[status(thm),theory(equality)],[222,2]),
[iquote('0:SpR:222.0,2.1')] ).
cnf(1680,plain,
( equal(tail,u)
| equal(select(queue_134,u),select(queue_136,u)) ),
inference(spr,[status(thm),theory(equality)],[215,2]),
[iquote('0:SpR:215.0,2.1')] ).
cnf(1681,plain,
( equal(tail,u)
| equal(select(queue_113,u),select(queue_115,u)) ),
inference(spr,[status(thm),theory(equality)],[207,2]),
[iquote('0:SpR:207.0,2.1')] ).
cnf(1682,plain,
( equal(tail,u)
| equal(select(queue_86,u),select(q20,u)) ),
inference(spr,[status(thm),theory(equality)],[854,2]),
[iquote('0:SpR:854.0,2.1')] ).
cnf(1683,plain,
( equal(tail,u)
| equal(select(queue_80,u),select(q2,u)) ),
inference(spr,[status(thm),theory(equality)],[861,2]),
[iquote('0:SpR:861.0,2.1')] ).
cnf(1684,plain,
( equal(tail,u)
| equal(select(queue_74,u),select(q19,u)) ),
inference(spr,[status(thm),theory(equality)],[868,2]),
[iquote('0:SpR:868.0,2.1')] ).
cnf(1685,plain,
( equal(tail,u)
| equal(select(queue_5,u),select(q1,u)) ),
inference(spr,[status(thm),theory(equality)],[875,2]),
[iquote('0:SpR:875.0,2.1')] ).
cnf(1686,plain,
( equal(tail,u)
| equal(select(queue_59,u),select(q17,u)) ),
inference(spr,[status(thm),theory(equality)],[882,2]),
[iquote('0:SpR:882.0,2.1')] ).
cnf(1687,plain,
( equal(tail,u)
| equal(select(queue_53,u),select(q16,u)) ),
inference(spr,[status(thm),theory(equality)],[889,2]),
[iquote('0:SpR:889.0,2.1')] ).
cnf(1688,plain,
( equal(tail,u)
| equal(select(queue_38,u),select(q14,u)) ),
inference(spr,[status(thm),theory(equality)],[896,2]),
[iquote('0:SpR:896.0,2.1')] ).
cnf(1689,plain,
( equal(tail,u)
| equal(select(queue_32,u),select(q13,u)) ),
inference(spr,[status(thm),theory(equality)],[903,2]),
[iquote('0:SpR:903.0,2.1')] ).
cnf(1690,plain,
( equal(tail,u)
| equal(select(queue_200,u),select(q8,u)) ),
inference(spr,[status(thm),theory(equality)],[910,2]),
[iquote('0:SpR:910.0,2.1')] ).
cnf(1691,plain,
( equal(tail,u)
| equal(select(queue_194,u),select(q7,u)) ),
inference(spr,[status(thm),theory(equality)],[917,2]),
[iquote('0:SpR:917.0,2.1')] ).
cnf(1692,plain,
( equal(tail,u)
| equal(select(queue_17,u),select(q11,u)) ),
inference(spr,[status(thm),theory(equality)],[924,2]),
[iquote('0:SpR:924.0,2.1')] ).
cnf(1693,plain,
( equal(tail,u)
| equal(select(queue_179,u),select(q5,u)) ),
inference(spr,[status(thm),theory(equality)],[931,2]),
[iquote('0:SpR:931.0,2.1')] ).
cnf(1694,plain,
( equal(tail,u)
| equal(select(queue_173,u),select(q4,u)) ),
inference(spr,[status(thm),theory(equality)],[938,2]),
[iquote('0:SpR:938.0,2.1')] ).
cnf(1695,plain,
( equal(tail,u)
| equal(select(queue_149,u),select(q29,u)) ),
inference(spr,[status(thm),theory(equality)],[945,2]),
[iquote('0:SpR:945.0,2.1')] ).
cnf(1696,plain,
( equal(tail,u)
| equal(select(queue_143,u),select(q28,u)) ),
inference(spr,[status(thm),theory(equality)],[952,2]),
[iquote('0:SpR:952.0,2.1')] ).
cnf(1697,plain,
( equal(tail,u)
| equal(select(queue_128,u),select(q26,u)) ),
inference(spr,[status(thm),theory(equality)],[959,2]),
[iquote('0:SpR:959.0,2.1')] ).
cnf(1698,plain,
( equal(tail,u)
| equal(select(queue_11,u),select(q10,u)) ),
inference(spr,[status(thm),theory(equality)],[966,2]),
[iquote('0:SpR:966.0,2.1')] ).
cnf(1699,plain,
( equal(tail,u)
| equal(select(queue_122,u),select(q25,u)) ),
inference(spr,[status(thm),theory(equality)],[973,2]),
[iquote('0:SpR:973.0,2.1')] ).
cnf(1700,plain,
( equal(tail,u)
| equal(select(queue_107,u),select(q23,u)) ),
inference(spr,[status(thm),theory(equality)],[980,2]),
[iquote('0:SpR:980.0,2.1')] ).
cnf(1701,plain,
( equal(tail,u)
| equal(select(queue_101,u),select(q22,u)) ),
inference(spr,[status(thm),theory(equality)],[987,2]),
[iquote('0:SpR:987.0,2.1')] ).
cnf(1702,plain,
( equal(seq,u)
| equal(select(queue_92,u),select(q20,u)) ),
inference(spr,[status(thm),theory(equality)],[268,2]),
[iquote('0:SpR:268.0,2.1')] ).
cnf(1703,plain,
( equal(seq,u)
| equal(select(queue_86,u),select(q19,u)) ),
inference(spr,[status(thm),theory(equality)],[266,2]),
[iquote('0:SpR:266.0,2.1')] ).
cnf(1704,plain,
( equal(seq,u)
| equal(select(queue_80,u),select(q1,u)) ),
inference(spr,[status(thm),theory(equality)],[264,2]),
[iquote('0:SpR:264.0,2.1')] ).
cnf(1705,plain,
( equal(seq,u)
| equal(select(queue_74,u),select(q18,u)) ),
inference(spr,[status(thm),theory(equality)],[262,2]),
[iquote('0:SpR:262.0,2.1')] ).
cnf(1706,plain,
( equal(seq,u)
| equal(select(queue_65,u),select(q17,u)) ),
inference(spr,[status(thm),theory(equality)],[258,2]),
[iquote('0:SpR:258.0,2.1')] ).
cnf(1707,plain,
( equal(seq,u)
| equal(select(queue_59,u),select(q16,u)) ),
inference(spr,[status(thm),theory(equality)],[256,2]),
[iquote('0:SpR:256.0,2.1')] ).
cnf(1708,plain,
( equal(seq,u)
| equal(select(queue_53,u),select(q15,u)) ),
inference(spr,[status(thm),theory(equality)],[254,2]),
[iquote('0:SpR:254.0,2.1')] ).
cnf(1709,plain,
( equal(seq,u)
| equal(select(queue_5,u),select(q0,u)) ),
inference(spr,[status(thm),theory(equality)],[253,2]),
[iquote('0:SpR:253.0,2.1')] ).
cnf(1710,plain,
( equal(seq,u)
| equal(select(queue_44,u),select(q14,u)) ),
inference(spr,[status(thm),theory(equality)],[250,2]),
[iquote('0:SpR:250.0,2.1')] ).
cnf(1711,plain,
( equal(seq,u)
| equal(select(queue_38,u),select(q13,u)) ),
inference(spr,[status(thm),theory(equality)],[248,2]),
[iquote('0:SpR:248.0,2.1')] ).
cnf(1712,plain,
( equal(seq,u)
| equal(select(queue_32,u),select(q12,u)) ),
inference(spr,[status(thm),theory(equality)],[246,2]),
[iquote('0:SpR:246.0,2.1')] ).
cnf(1713,plain,
( equal(seq,u)
| equal(select(queue_23,u),select(q11,u)) ),
inference(spr,[status(thm),theory(equality)],[243,2]),
[iquote('0:SpR:243.0,2.1')] ).
cnf(1714,plain,
( equal(seq,u)
| equal(select(queue_206,u),select(q8,u)) ),
inference(spr,[status(thm),theory(equality)],[240,2]),
[iquote('0:SpR:240.0,2.1')] ).
cnf(1715,plain,
( equal(seq,u)
| equal(select(queue_200,u),select(q7,u)) ),
inference(spr,[status(thm),theory(equality)],[238,2]),
[iquote('0:SpR:238.0,2.1')] ).
cnf(1716,plain,
( equal(seq,u)
| equal(select(queue_194,u),select(q6,u)) ),
inference(spr,[status(thm),theory(equality)],[236,2]),
[iquote('0:SpR:236.0,2.1')] ).
cnf(1717,plain,
( equal(seq,u)
| equal(select(queue_185,u),select(q5,u)) ),
inference(spr,[status(thm),theory(equality)],[232,2]),
[iquote('0:SpR:232.0,2.1')] ).
cnf(1718,plain,
( equal(seq,u)
| equal(select(queue_179,u),select(q4,u)) ),
inference(spr,[status(thm),theory(equality)],[230,2]),
[iquote('0:SpR:230.0,2.1')] ).
cnf(1719,plain,
( equal(seq,u)
| equal(select(queue_173,u),select(q3,u)) ),
inference(spr,[status(thm),theory(equality)],[228,2]),
[iquote('0:SpR:228.0,2.1')] ).
cnf(1720,plain,
( equal(seq,u)
| equal(select(queue_17,u),select(q10,u)) ),
inference(spr,[status(thm),theory(equality)],[227,2]),
[iquote('0:SpR:227.0,2.1')] ).
cnf(1721,plain,
( equal(seq,u)
| equal(select(queue_164,u),select(q29,u)) ),
inference(spr,[status(thm),theory(equality)],[224,2]),
[iquote('0:SpR:224.0,2.1')] ).
cnf(1722,plain,
( equal(seq,u)
| equal(select(queue_155,u),select(q2,u)) ),
inference(spr,[status(thm),theory(equality)],[221,2]),
[iquote('0:SpR:221.0,2.1')] ).
cnf(1723,plain,
( equal(seq,u)
| equal(select(queue_149,u),select(q28,u)) ),
inference(spr,[status(thm),theory(equality)],[219,2]),
[iquote('0:SpR:219.0,2.1')] ).
cnf(1724,plain,
( equal(seq,u)
| equal(select(queue_143,u),select(q27,u)) ),
inference(spr,[status(thm),theory(equality)],[217,2]),
[iquote('0:SpR:217.0,2.1')] ).
cnf(1725,plain,
( equal(seq,u)
| equal(select(queue_134,u),select(q26,u)) ),
inference(spr,[status(thm),theory(equality)],[214,2]),
[iquote('0:SpR:214.0,2.1')] ).
cnf(1726,plain,
( equal(seq,u)
| equal(select(queue_128,u),select(q25,u)) ),
inference(spr,[status(thm),theory(equality)],[211,2]),
[iquote('0:SpR:211.0,2.1')] ).
cnf(1727,plain,
( equal(seq,u)
| equal(select(queue_122,u),select(q24,u)) ),
inference(spr,[status(thm),theory(equality)],[209,2]),
[iquote('0:SpR:209.0,2.1')] ).
cnf(1728,plain,
( equal(seq,u)
| equal(select(queue_113,u),select(q23,u)) ),
inference(spr,[status(thm),theory(equality)],[206,2]),
[iquote('0:SpR:206.0,2.1')] ).
cnf(1729,plain,
( equal(seq,u)
| equal(select(queue_11,u),select(q9,u)) ),
inference(spr,[status(thm),theory(equality)],[205,2]),
[iquote('0:SpR:205.0,2.1')] ).
cnf(1730,plain,
( equal(seq,u)
| equal(select(queue_107,u),select(q22,u)) ),
inference(spr,[status(thm),theory(equality)],[203,2]),
[iquote('0:SpR:203.0,2.1')] ).
cnf(1731,plain,
( equal(seq,u)
| equal(select(queue_101,u),select(q21,u)) ),
inference(spr,[status(thm),theory(equality)],[201,2]),
[iquote('0:SpR:201.0,2.1')] ).
cnf(1732,plain,
( equal(index_90,u)
| equal(select(earray_91,u),select(earray_89,u)) ),
inference(spr,[status(thm),theory(equality)],[115,2]),
[iquote('0:SpR:115.0,2.1')] ).
cnf(1733,plain,
( equal(index_84,u)
| equal(select(earray_85,u),select(earray_83,u)) ),
inference(spr,[status(thm),theory(equality)],[113,2]),
[iquote('0:SpR:113.0,2.1')] ).
cnf(1735,plain,
( equal(index_72,u)
| equal(select(earray_73,u),select(earray_71,u)) ),
inference(spr,[status(thm),theory(equality)],[108,2]),
[iquote('0:SpR:108.0,2.1')] ).
cnf(1736,plain,
( equal(index_63,u)
| equal(select(earray_64,u),select(earray_62,u)) ),
inference(spr,[status(thm),theory(equality)],[106,2]),
[iquote('0:SpR:106.0,2.1')] ).
cnf(1737,plain,
( equal(index_57,u)
| equal(select(earray_58,u),select(earray_56,u)) ),
inference(spr,[status(thm),theory(equality)],[104,2]),
[iquote('0:SpR:104.0,2.1')] ).
cnf(1738,plain,
( equal(index_51,u)
| equal(select(earray_52,u),select(earray_50,u)) ),
inference(spr,[status(thm),theory(equality)],[102,2]),
[iquote('0:SpR:102.0,2.1')] ).
cnf(1739,plain,
( equal(index_42,u)
| equal(select(earray_43,u),select(earray_41,u)) ),
inference(spr,[status(thm),theory(equality)],[100,2]),
[iquote('0:SpR:100.0,2.1')] ).
cnf(1741,plain,
( equal(index_36,u)
| equal(select(earray_37,u),select(earray_35,u)) ),
inference(spr,[status(thm),theory(equality)],[97,2]),
[iquote('0:SpR:97.0,2.1')] ).
cnf(1742,plain,
( equal(index_30,u)
| equal(select(earray_31,u),select(earray_29,u)) ),
inference(spr,[status(thm),theory(equality)],[95,2]),
[iquote('0:SpR:95.0,2.1')] ).
cnf(1743,plain,
( equal(index_21,u)
| equal(select(earray_22,u),select(earray_20,u)) ),
inference(spr,[status(thm),theory(equality)],[93,2]),
[iquote('0:SpR:93.0,2.1')] ).
cnf(1750,plain,
( equal(index_162,u)
| equal(select(earray_163,u),select(earray_161,u)) ),
inference(spr,[status(thm),theory(equality)],[77,2]),
[iquote('0:SpR:77.0,2.1')] ).
cnf(1753,plain,
( equal(index_147,u)
| equal(select(earray_148,u),select(earray_146,u)) ),
inference(spr,[status(thm),theory(equality)],[72,2]),
[iquote('0:SpR:72.0,2.1')] ).
cnf(1754,plain,
( equal(index_141,u)
| equal(select(earray_142,u),select(earray_140,u)) ),
inference(spr,[status(thm),theory(equality)],[70,2]),
[iquote('0:SpR:70.0,2.1')] ).
cnf(1755,plain,
( equal(index_132,u)
| equal(select(earray_133,u),select(earray_131,u)) ),
inference(spr,[status(thm),theory(equality)],[67,2]),
[iquote('0:SpR:67.0,2.1')] ).
cnf(1756,plain,
( equal(index_126,u)
| equal(select(earray_127,u),select(earray_125,u)) ),
inference(spr,[status(thm),theory(equality)],[65,2]),
[iquote('0:SpR:65.0,2.1')] ).
cnf(1757,plain,
( equal(index_120,u)
| equal(select(earray_121,u),select(earray_119,u)) ),
inference(spr,[status(thm),theory(equality)],[63,2]),
[iquote('0:SpR:63.0,2.1')] ).
cnf(1758,plain,
( equal(index_111,u)
| equal(select(earray_112,u),select(earray_110,u)) ),
inference(spr,[status(thm),theory(equality)],[61,2]),
[iquote('0:SpR:61.0,2.1')] ).
cnf(1759,plain,
( equal(index_105,u)
| equal(select(earray_106,u),select(earray_104,u)) ),
inference(spr,[status(thm),theory(equality)],[59,2]),
[iquote('0:SpR:59.0,2.1')] ).
cnf(1760,plain,
( equal(index_99,u)
| equal(select(earray_98,u),select(earray_100,u)) ),
inference(spr,[status(thm),theory(equality)],[57,2]),
[iquote('0:SpR:57.0,2.1')] ).
cnf(1796,plain,
~ equal(s(s(s(s(s(s(s(s(s(index_21))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,46]),
[iquote('0:SpL:922.0,46.0')] ).
cnf(1816,plain,
~ equal(s(s(s(s(s(s(s(s(index_24)))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1796]),
[iquote('0:Rew:167.0,1796.0')] ).
cnf(1860,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(index_21)))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,45]),
[iquote('0:SpL:922.0,45.0')] ).
cnf(1880,plain,
~ equal(s(s(s(s(s(s(s(s(s(index_24))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1860]),
[iquote('0:Rew:167.0,1860.0')] ).
cnf(1924,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,44]),
[iquote('0:SpL:922.0,44.0')] ).
cnf(1944,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(index_24)))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1924]),
[iquote('0:Rew:167.0,1924.0')] ).
cnf(1988,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,43]),
[iquote('0:SpL:922.0,43.0')] ).
cnf(2008,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,1988]),
[iquote('0:Rew:167.0,1988.0')] ).
cnf(2052,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,42]),
[iquote('0:SpL:922.0,42.0')] ).
cnf(2072,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,2052]),
[iquote('0:Rew:167.0,2052.0')] ).
cnf(2112,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,41]),
[iquote('0:SpL:922.0,41.0')] ).
cnf(2132,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,2112]),
[iquote('0:Rew:167.0,2112.0')] ).
cnf(2172,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,40]),
[iquote('0:SpL:922.0,40.0')] ).
cnf(2192,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,2172]),
[iquote('0:Rew:167.0,2172.0')] ).
cnf(2232,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,39]),
[iquote('0:SpL:922.0,39.0')] ).
cnf(2251,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,2232]),
[iquote('0:Rew:167.0,2232.0')] ).
cnf(2292,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,38]),
[iquote('0:SpL:922.0,38.0')] ).
cnf(2311,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,2292]),
[iquote('0:Rew:167.0,2292.0')] ).
cnf(2352,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))))),index_15),
inference(spl,[status(thm),theory(equality)],[922,37]),
[iquote('0:SpL:922.0,37.0')] ).
cnf(2371,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[167,2352]),
[iquote('0:Rew:167.0,2352.0')] ).
cnf(4246,plain,
( equal(tail,head)
| equal(select(q21,tail),index_93) ),
inference(spr,[status(thm),theory(equality)],[1661,754]),
[iquote('0:SpR:1661.1,754.0')] ).
cnf(4249,plain,
( equal(tail,head)
| equal(index_93,index_99) ),
inference(rew,[status(thm),theory(equality)],[199,4246]),
[iquote('0:Rew:199.0,4246.1')] ).
cnf(4250,plain,
equal(index_93,index_99),
inference(mrr,[status(thm)],[4249,3]),
[iquote('0:MRR:4249.0,3.0')] ).
cnf(4251,plain,
equal(s(index_90),index_99),
inference(rew,[status(thm),theory(equality)],[4250,196]),
[iquote('0:Rew:4250.0,196.0')] ).
cnf(4651,plain,
( equal(tail,head)
| equal(select(q18,tail),index_66) ),
inference(spr,[status(thm),theory(equality)],[1662,759]),
[iquote('0:SpR:1662.1,759.0')] ).
cnf(4654,plain,
( equal(tail,head)
| equal(index_66,index_72) ),
inference(rew,[status(thm),theory(equality)],[188,4651]),
[iquote('0:Rew:188.0,4651.1')] ).
cnf(4655,plain,
equal(index_66,index_72),
inference(mrr,[status(thm)],[4654,3]),
[iquote('0:MRR:4654.0,3.0')] ).
cnf(4656,plain,
equal(s(index_63),index_72),
inference(rew,[status(thm),theory(equality)],[4655,185]),
[iquote('0:Rew:4655.0,185.0')] ).
cnf(5056,plain,
( equal(tail,head)
| equal(select(q15,tail),index_45) ),
inference(spr,[status(thm),theory(equality)],[1663,762]),
[iquote('0:SpR:1663.1,762.0')] ).
cnf(5059,plain,
( equal(tail,head)
| equal(index_45,index_51) ),
inference(rew,[status(thm),theory(equality)],[179,5056]),
[iquote('0:Rew:179.0,5056.1')] ).
cnf(5060,plain,
equal(index_45,index_51),
inference(mrr,[status(thm)],[5059,3]),
[iquote('0:MRR:5059.0,3.0')] ).
cnf(5061,plain,
equal(s(index_42),index_51),
inference(rew,[status(thm),theory(equality)],[5060,176]),
[iquote('0:Rew:5060.0,176.0')] ).
cnf(5461,plain,
( equal(tail,head)
| equal(select(q12,tail),index_24) ),
inference(spr,[status(thm),theory(equality)],[1664,765]),
[iquote('0:SpR:1664.1,765.0')] ).
cnf(5464,plain,
( equal(tail,head)
| equal(index_24,index_30) ),
inference(rew,[status(thm),theory(equality)],[171,5461]),
[iquote('0:Rew:171.0,5461.1')] ).
cnf(5465,plain,
equal(index_24,index_30),
inference(mrr,[status(thm)],[5464,3]),
[iquote('0:MRR:5464.0,3.0')] ).
cnf(5469,plain,
~ equal(index_30,index_15),
inference(rew,[status(thm),theory(equality)],[5465,1001]),
[iquote('0:Rew:5465.0,1001.0')] ).
cnf(5472,plain,
~ equal(s(index_30),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1026]),
[iquote('0:Rew:5465.0,1026.0')] ).
cnf(5475,plain,
~ equal(s(s(index_30)),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1056]),
[iquote('0:Rew:5465.0,1056.0')] ).
cnf(5478,plain,
~ equal(s(s(s(index_30))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1389]),
[iquote('0:Rew:5465.0,1389.0')] ).
cnf(5481,plain,
~ equal(s(s(s(s(index_30)))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1453]),
[iquote('0:Rew:5465.0,1453.0')] ).
cnf(5484,plain,
~ equal(s(s(s(s(s(index_30))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1517]),
[iquote('0:Rew:5465.0,1517.0')] ).
cnf(5487,plain,
~ equal(s(s(s(s(s(s(index_30)))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1581]),
[iquote('0:Rew:5465.0,1581.0')] ).
cnf(5499,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,2251]),
[iquote('0:Rew:5465.0,2251.0')] ).
cnf(5501,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,2311]),
[iquote('0:Rew:5465.0,2311.0')] ).
cnf(5503,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,2371]),
[iquote('0:Rew:5465.0,2371.0')] ).
cnf(5600,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,2192]),
[iquote('0:Rew:5465.0,2192.0')] ).
cnf(5602,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,2132]),
[iquote('0:Rew:5465.0,2132.0')] ).
cnf(5604,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,2072]),
[iquote('0:Rew:5465.0,2072.0')] ).
cnf(5606,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,2008]),
[iquote('0:Rew:5465.0,2008.0')] ).
cnf(5608,plain,
~ equal(s(s(s(s(s(s(s(s(s(s(index_30)))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1944]),
[iquote('0:Rew:5465.0,1944.0')] ).
cnf(5610,plain,
~ equal(s(s(s(s(s(s(s(s(s(index_30))))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1880]),
[iquote('0:Rew:5465.0,1880.0')] ).
cnf(5612,plain,
~ equal(s(s(s(s(s(s(s(s(index_30)))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1816]),
[iquote('0:Rew:5465.0,1816.0')] ).
cnf(5614,plain,
~ equal(s(s(s(s(s(s(s(index_30))))))),index_15),
inference(rew,[status(thm),theory(equality)],[5465,1645]),
[iquote('0:Rew:5465.0,1645.0')] ).
cnf(5617,plain,
~ equal(index_36,index_15),
inference(rew,[status(thm),theory(equality)],[901,5472]),
[iquote('0:Rew:901.0,5472.0')] ).
cnf(5620,plain,
~ equal(index_42,index_15),
inference(rew,[status(thm),theory(equality)],[894,5475,901]),
[iquote('0:Rew:894.0,5475.0,901.0,5475.0')] ).
cnf(5623,plain,
~ equal(index_51,index_15),
inference(rew,[status(thm),theory(equality)],[5061,5478,894,901]),
[iquote('0:Rew:5061.0,5478.0,894.0,5478.0,901.0,5478.0')] ).
cnf(5626,plain,
~ equal(index_57,index_15),
inference(rew,[status(thm),theory(equality)],[887,5481,5061,894,901]),
[iquote('0:Rew:887.0,5481.0,5061.0,5481.0,894.0,5481.0,901.0,5481.0')] ).
cnf(5629,plain,
~ equal(index_63,index_15),
inference(rew,[status(thm),theory(equality)],[880,5484,887,5061,894,901]),
[iquote('0:Rew:880.0,5484.0,887.0,5484.0,5061.0,5484.0,894.0,5484.0,901.0,5484.0')] ).
cnf(5632,plain,
~ equal(index_72,index_15),
inference(rew,[status(thm),theory(equality)],[4656,5487,880,887,5061,894,901]),
[iquote('0:Rew:4656.0,5487.0,880.0,5487.0,887.0,5487.0,5061.0,5487.0,894.0,5487.0,901.0,5487.0')] ).
cnf(5635,plain,
~ equal(index_84,index_15),
inference(rew,[status(thm),theory(equality)],[866,5614,4656,880,887,5061,894,901]),
[iquote('0:Rew:866.0,5614.0,4656.0,5614.0,880.0,5614.0,887.0,5614.0,5061.0,5614.0,894.0,5614.0,901.0,5614.0')] ).
cnf(5638,plain,
~ equal(index_90,index_15),
inference(rew,[status(thm),theory(equality)],[852,5612,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:852.0,5612.0,866.0,5612.0,4656.0,5612.0,880.0,5612.0,887.0,5612.0,5061.0,5612.0,894.0,5612.0,901.0,5612.0')] ).
cnf(5641,plain,
~ equal(index_15,index_99),
inference(rew,[status(thm),theory(equality)],[4251,5610,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:4251.0,5610.0,852.0,5610.0,866.0,5610.0,4656.0,5610.0,880.0,5610.0,887.0,5610.0,5061.0,5610.0,894.0,5610.0,901.0,5610.0')] ).
cnf(5644,plain,
~ equal(index_15,index_105),
inference(rew,[status(thm),theory(equality)],[985,5608,4251,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:985.0,5608.0,4251.0,5608.0,852.0,5608.0,866.0,5608.0,4656.0,5608.0,880.0,5608.0,887.0,5608.0,5061.0,5608.0,894.0,5608.0,901.0,5608.0')] ).
cnf(5647,plain,
~ equal(index_15,index_111),
inference(rew,[status(thm),theory(equality)],[978,5606,985,4251,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:978.0,5606.0,985.0,5606.0,4251.0,5606.0,852.0,5606.0,866.0,5606.0,4656.0,5606.0,880.0,5606.0,887.0,5606.0,5061.0,5606.0,894.0,5606.0,901.0,5606.0')] ).
cnf(5650,plain,
~ equal(index_114,index_15),
inference(rew,[status(thm),theory(equality)],[123,5604,978,985,4251,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:123.0,5604.0,978.0,5604.0,985.0,5604.0,4251.0,5604.0,852.0,5604.0,866.0,5604.0,4656.0,5604.0,880.0,5604.0,887.0,5604.0,5061.0,5604.0,894.0,5604.0,901.0,5604.0')] ).
cnf(5653,plain,
~ equal(s(index_114),index_15),
inference(rew,[status(thm),theory(equality)],[123,5602,978,985,4251,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:123.0,5602.0,978.0,5602.0,985.0,5602.0,4251.0,5602.0,852.0,5602.0,866.0,5602.0,4656.0,5602.0,880.0,5602.0,887.0,5602.0,5061.0,5602.0,894.0,5602.0,901.0,5602.0')] ).
cnf(5656,plain,
~ equal(s(s(index_114)),index_15),
inference(rew,[status(thm),theory(equality)],[123,5600,978,985,4251,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:123.0,5600.0,978.0,5600.0,985.0,5600.0,4251.0,5600.0,852.0,5600.0,866.0,5600.0,4656.0,5600.0,880.0,5600.0,887.0,5600.0,5061.0,5600.0,894.0,5600.0,901.0,5600.0')] ).
cnf(5659,plain,
~ equal(s(s(s(index_114))),index_15),
inference(rew,[status(thm),theory(equality)],[123,5499,978,985,4251,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:123.0,5499.0,978.0,5499.0,985.0,5499.0,4251.0,5499.0,852.0,5499.0,866.0,5499.0,4656.0,5499.0,880.0,5499.0,887.0,5499.0,5061.0,5499.0,894.0,5499.0,901.0,5499.0')] ).
cnf(5662,plain,
~ equal(s(s(s(s(index_114)))),index_15),
inference(rew,[status(thm),theory(equality)],[123,5501,978,985,4251,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:123.0,5501.0,978.0,5501.0,985.0,5501.0,4251.0,5501.0,852.0,5501.0,866.0,5501.0,4656.0,5501.0,880.0,5501.0,887.0,5501.0,5061.0,5501.0,894.0,5501.0,901.0,5501.0')] ).
cnf(5665,plain,
~ equal(s(s(s(s(s(index_114))))),index_15),
inference(rew,[status(thm),theory(equality)],[123,5503,978,985,4251,852,866,4656,880,887,5061,894,901]),
[iquote('0:Rew:123.0,5503.0,978.0,5503.0,985.0,5503.0,4251.0,5503.0,852.0,5503.0,866.0,5503.0,4656.0,5503.0,880.0,5503.0,887.0,5503.0,5061.0,5503.0,894.0,5503.0,901.0,5503.0')] ).
cnf(5866,plain,
( equal(tail,head)
| equal(select(q9,tail),index_207) ),
inference(spr,[status(thm),theory(equality)],[1665,766]),
[iquote('0:SpR:1665.1,766.0')] ).
cnf(5869,plain,
( equal(tail,head)
| equal(index_207,index_9) ),
inference(rew,[status(thm),theory(equality)],[194,5866]),
[iquote('0:Rew:194.0,5866.1')] ).
cnf(5870,plain,
equal(index_207,index_9),
inference(mrr,[status(thm)],[5869,3]),
[iquote('0:MRR:5869.0,3.0')] ).
cnf(5871,plain,
equal(s(index_204),index_9),
inference(rew,[status(thm),theory(equality)],[5870,162]),
[iquote('0:Rew:5870.0,162.0')] ).
cnf(6271,plain,
( equal(tail,head)
| equal(select(q6,tail),index_186) ),
inference(spr,[status(thm),theory(equality)],[1666,770]),
[iquote('0:SpR:1666.1,770.0')] ).
cnf(6274,plain,
( equal(tail,head)
| equal(index_186,index_192) ),
inference(rew,[status(thm),theory(equality)],[157,6271]),
[iquote('0:Rew:157.0,6271.1')] ).
cnf(6275,plain,
equal(index_186,index_192),
inference(mrr,[status(thm)],[6274,3]),
[iquote('0:MRR:6274.0,3.0')] ).
cnf(6276,plain,
equal(s(index_183),index_192),
inference(rew,[status(thm),theory(equality)],[6275,154]),
[iquote('0:Rew:6275.0,154.0')] ).
cnf(6676,plain,
( equal(tail,head)
| equal(select(q3,tail),index_156) ),
inference(spr,[status(thm),theory(equality)],[1667,774]),
[iquote('0:SpR:1667.1,774.0')] ).
cnf(6679,plain,
( equal(tail,head)
| equal(index_156,index_171) ),
inference(rew,[status(thm),theory(equality)],[148,6676]),
[iquote('0:Rew:148.0,6676.1')] ).
cnf(6680,plain,
equal(index_156,index_171),
inference(mrr,[status(thm)],[6679,3]),
[iquote('0:MRR:6679.0,3.0')] ).
cnf(6681,plain,
equal(s(index_153),index_171),
inference(rew,[status(thm),theory(equality)],[6680,141]),
[iquote('0:Rew:6680.0,141.0')] ).
cnf(7081,plain,
( equal(tail,head)
| equal(select(q27,tail),index_135) ),
inference(spr,[status(thm),theory(equality)],[1668,777]),
[iquote('0:SpR:1668.1,777.0')] ).
cnf(7084,plain,
( equal(tail,head)
| equal(index_135,index_141) ),
inference(rew,[status(thm),theory(equality)],[135,7081]),
[iquote('0:Rew:135.0,7081.1')] ).
cnf(7085,plain,
equal(index_135,index_141),
inference(mrr,[status(thm)],[7084,3]),
[iquote('0:MRR:7084.0,3.0')] ).
cnf(7086,plain,
equal(s(index_132),index_141),
inference(rew,[status(thm),theory(equality)],[7085,132]),
[iquote('0:Rew:7085.0,132.0')] ).
cnf(7486,plain,
( equal(tail,head)
| equal(select(q24,tail),index_114) ),
inference(spr,[status(thm),theory(equality)],[1669,781]),
[iquote('0:SpR:1669.1,781.0')] ).
cnf(7489,plain,
( equal(tail,head)
| equal(index_114,index_120) ),
inference(rew,[status(thm),theory(equality)],[127,7486]),
[iquote('0:Rew:127.0,7486.1')] ).
cnf(7490,plain,
equal(index_114,index_120),
inference(mrr,[status(thm)],[7489,3]),
[iquote('0:MRR:7489.0,3.0')] ).
cnf(7545,plain,
~ equal(s(s(s(s(s(index_120))))),index_15),
inference(rew,[status(thm),theory(equality)],[7490,5665]),
[iquote('0:Rew:7490.0,5665.0')] ).
cnf(7566,plain,
~ equal(s(s(s(s(index_120)))),index_15),
inference(rew,[status(thm),theory(equality)],[7490,5662]),
[iquote('0:Rew:7490.0,5662.0')] ).
cnf(7587,plain,
~ equal(s(s(s(index_120))),index_15),
inference(rew,[status(thm),theory(equality)],[7490,5659]),
[iquote('0:Rew:7490.0,5659.0')] ).
cnf(7608,plain,
~ equal(s(s(index_120)),index_15),
inference(rew,[status(thm),theory(equality)],[7490,5656]),
[iquote('0:Rew:7490.0,5656.0')] ).
cnf(7629,plain,
~ equal(s(index_120),index_15),
inference(rew,[status(thm),theory(equality)],[7490,5653]),
[iquote('0:Rew:7490.0,5653.0')] ).
cnf(7651,plain,
~ equal(index_15,index_120),
inference(rew,[status(thm),theory(equality)],[7490,5650]),
[iquote('0:Rew:7490.0,5650.0')] ).
cnf(8431,plain,
~ equal(index_15,index_126),
inference(rew,[status(thm),theory(equality)],[971,7629]),
[iquote('0:Rew:971.0,7629.0')] ).
cnf(8455,plain,
~ equal(index_15,index_132),
inference(rew,[status(thm),theory(equality)],[957,7608,971]),
[iquote('0:Rew:957.0,7608.0,971.0,7608.0')] ).
cnf(8479,plain,
~ equal(index_15,index_141),
inference(rew,[status(thm),theory(equality)],[7086,7587,957,971]),
[iquote('0:Rew:7086.0,7587.0,957.0,7587.0,971.0,7587.0')] ).
cnf(8503,plain,
~ equal(index_15,index_147),
inference(rew,[status(thm),theory(equality)],[950,7566,7086,957,971]),
[iquote('0:Rew:950.0,7566.0,7086.0,7566.0,957.0,7566.0,971.0,7566.0')] ).
cnf(8527,plain,
~ equal(index_162,index_15),
inference(rew,[status(thm),theory(equality)],[943,7545,950,7086,957,971]),
[iquote('0:Rew:943.0,7545.0,950.0,7545.0,7086.0,7545.0,957.0,7545.0,971.0,7545.0')] ).
cnf(9424,plain,
( equal(tail,head)
| equal(select(q0,tail),index_0) ),
inference(spr,[status(thm),theory(equality)],[1670,118]),
[iquote('0:SpR:1670.1,118.0')] ).
cnf(9426,plain,
( equal(tail,head)
| equal(index_0,index_3) ),
inference(rew,[status(thm),theory(equality)],[170,9424]),
[iquote('0:Rew:170.0,9424.1')] ).
cnf(9427,plain,
equal(index_0,index_3),
inference(mrr,[status(thm)],[9426,3]),
[iquote('0:MRR:9426.0,3.0')] ).
cnf(9430,plain,
equal(select(q0,head),index_3),
inference(rew,[status(thm),theory(equality)],[9427,753]),
[iquote('0:Rew:9427.0,753.0')] ).
cnf(9443,plain,
( equal(seq,tail)
| equal(select(queue_94,seq),earray_91) ),
inference(spr,[status(thm),theory(equality)],[1672,784]),
[iquote('0:SpR:1672.1,784.0')] ).
cnf(9445,plain,
equal(select(queue_94,seq),earray_91),
inference(mrr,[status(thm)],[9443,5]),
[iquote('0:MRR:9443.0,5.0')] ).
cnf(9447,plain,
( equal(seq,head)
| equal(select(q21,seq),earray_91) ),
inference(spr,[status(thm),theory(equality)],[9445,1661]),
[iquote('0:SpR:9445.0,1661.1')] ).
cnf(9448,plain,
( equal(seq,head)
| equal(earray_91,earray_98) ),
inference(rew,[status(thm),theory(equality)],[116,9447]),
[iquote('0:Rew:116.0,9447.1')] ).
cnf(9449,plain,
equal(earray_91,earray_98),
inference(mrr,[status(thm)],[9448,4]),
[iquote('0:MRR:9448.0,4.0')] ).
cnf(9455,plain,
( equal(index_90,u)
| equal(select(earray_89,u),select(earray_98,u)) ),
inference(rew,[status(thm),theory(equality)],[9449,1732]),
[iquote('0:Rew:9449.0,1732.1')] ).
cnf(9468,plain,
( equal(seq,tail)
| equal(select(queue_67,seq),earray_64) ),
inference(spr,[status(thm),theory(equality)],[1673,788]),
[iquote('0:SpR:1673.1,788.0')] ).
cnf(9470,plain,
equal(select(queue_67,seq),earray_64),
inference(mrr,[status(thm)],[9468,5]),
[iquote('0:MRR:9468.0,5.0')] ).
cnf(9472,plain,
( equal(seq,head)
| equal(select(q18,seq),earray_64) ),
inference(spr,[status(thm),theory(equality)],[9470,1662]),
[iquote('0:SpR:9470.0,1662.1')] ).
cnf(9473,plain,
( equal(seq,head)
| equal(earray_71,earray_64) ),
inference(rew,[status(thm),theory(equality)],[107,9472]),
[iquote('0:Rew:107.0,9472.1')] ).
cnf(9474,plain,
equal(earray_71,earray_64),
inference(mrr,[status(thm)],[9473,4]),
[iquote('0:MRR:9473.0,4.0')] ).
cnf(9477,plain,
( equal(index_72,u)
| equal(select(earray_73,u),select(earray_64,u)) ),
inference(rew,[status(thm),theory(equality)],[9474,1735]),
[iquote('0:Rew:9474.0,1735.1')] ).
cnf(9483,plain,
( equal(seq,tail)
| equal(select(queue_46,seq),earray_43) ),
inference(spr,[status(thm),theory(equality)],[1674,792]),
[iquote('0:SpR:1674.1,792.0')] ).
cnf(9485,plain,
equal(select(queue_46,seq),earray_43),
inference(mrr,[status(thm)],[9483,5]),
[iquote('0:MRR:9483.0,5.0')] ).
cnf(9487,plain,
( equal(seq,head)
| equal(select(q15,seq),earray_43) ),
inference(spr,[status(thm),theory(equality)],[9485,1663]),
[iquote('0:SpR:9485.0,1663.1')] ).
cnf(9488,plain,
( equal(seq,head)
| equal(earray_50,earray_43) ),
inference(rew,[status(thm),theory(equality)],[101,9487]),
[iquote('0:Rew:101.0,9487.1')] ).
cnf(9489,plain,
equal(earray_50,earray_43),
inference(mrr,[status(thm)],[9488,4]),
[iquote('0:MRR:9488.0,4.0')] ).
cnf(9492,plain,
( equal(index_51,u)
| equal(select(earray_52,u),select(earray_43,u)) ),
inference(rew,[status(thm),theory(equality)],[9489,1738]),
[iquote('0:Rew:9489.0,1738.1')] ).
cnf(9498,plain,
( equal(seq,tail)
| equal(select(queue_25,seq),earray_22) ),
inference(spr,[status(thm),theory(equality)],[1675,795]),
[iquote('0:SpR:1675.1,795.0')] ).
cnf(9500,plain,
equal(select(queue_25,seq),earray_22),
inference(mrr,[status(thm)],[9498,5]),
[iquote('0:MRR:9498.0,5.0')] ).
cnf(9502,plain,
( equal(seq,head)
| equal(select(q12,seq),earray_22) ),
inference(spr,[status(thm),theory(equality)],[9500,1664]),
[iquote('0:SpR:9500.0,1664.1')] ).
cnf(9503,plain,
( equal(seq,head)
| equal(earray_29,earray_22) ),
inference(rew,[status(thm),theory(equality)],[94,9502]),
[iquote('0:Rew:94.0,9502.1')] ).
cnf(9504,plain,
equal(earray_29,earray_22),
inference(mrr,[status(thm)],[9503,4]),
[iquote('0:MRR:9503.0,4.0')] ).
cnf(9507,plain,
( equal(index_30,u)
| equal(select(earray_31,u),select(earray_22,u)) ),
inference(rew,[status(thm),theory(equality)],[9504,1742]),
[iquote('0:Rew:9504.0,1742.1')] ).
cnf(9541,plain,
( equal(seq,tail)
| equal(select(queue_166,seq),earray_163) ),
inference(spr,[status(thm),theory(equality)],[1678,803]),
[iquote('0:SpR:1678.1,803.0')] ).
cnf(9543,plain,
equal(select(queue_166,seq),earray_163),
inference(mrr,[status(thm)],[9541,5]),
[iquote('0:MRR:9541.0,5.0')] ).
cnf(9553,plain,
( equal(seq,head)
| equal(select(q30,seq),earray_163) ),
inference(spr,[status(thm),theory(equality)],[9543,1671]),
[iquote('0:SpR:9543.0,1671.1')] ).
cnf(9554,plain,
( equal(seq,head)
| equal(earray_212,earray_163) ),
inference(rew,[status(thm),theory(equality)],[92,9553]),
[iquote('0:Rew:92.0,9553.1')] ).
cnf(9555,plain,
equal(earray_212,earray_163),
inference(mrr,[status(thm)],[9554,4]),
[iquote('0:MRR:9554.0,4.0')] ).
cnf(9556,plain,
equal(select(earray_163,index_213),elem_214),
inference(rew,[status(thm),theory(equality)],[9555,117]),
[iquote('0:Rew:9555.0,117.0')] ).
cnf(9568,plain,
( equal(seq,tail)
| equal(select(queue_136,seq),earray_133) ),
inference(spr,[status(thm),theory(equality)],[1680,807]),
[iquote('0:SpR:1680.1,807.0')] ).
cnf(9570,plain,
equal(select(queue_136,seq),earray_133),
inference(mrr,[status(thm)],[9568,5]),
[iquote('0:MRR:9568.0,5.0')] ).
cnf(9580,plain,
( equal(seq,head)
| equal(select(q27,seq),earray_133) ),
inference(spr,[status(thm),theory(equality)],[9570,1668]),
[iquote('0:SpR:9570.0,1668.1')] ).
cnf(9581,plain,
( equal(seq,head)
| equal(earray_140,earray_133) ),
inference(rew,[status(thm),theory(equality)],[69,9580]),
[iquote('0:Rew:69.0,9580.1')] ).
cnf(9582,plain,
equal(earray_140,earray_133),
inference(mrr,[status(thm)],[9581,4]),
[iquote('0:MRR:9581.0,4.0')] ).
cnf(9585,plain,
( equal(index_141,u)
| equal(select(earray_142,u),select(earray_133,u)) ),
inference(rew,[status(thm),theory(equality)],[9582,1754]),
[iquote('0:Rew:9582.0,1754.1')] ).
cnf(9595,plain,
( equal(seq,tail)
| equal(select(queue_115,seq),earray_112) ),
inference(spr,[status(thm),theory(equality)],[1681,810]),
[iquote('0:SpR:1681.1,810.0')] ).
cnf(9597,plain,
equal(select(queue_115,seq),earray_112),
inference(mrr,[status(thm)],[9595,5]),
[iquote('0:MRR:9595.0,5.0')] ).
cnf(9598,plain,
( equal(seq,tail)
| equal(select(q20,seq),earray_85) ),
inference(spr,[status(thm),theory(equality)],[1682,785]),
[iquote('0:SpR:1682.1,785.0')] ).
cnf(9600,plain,
( equal(seq,tail)
| equal(earray_89,earray_85) ),
inference(rew,[status(thm),theory(equality)],[114,9598]),
[iquote('0:Rew:114.0,9598.1')] ).
cnf(9601,plain,
equal(earray_89,earray_85),
inference(mrr,[status(thm)],[9600,5]),
[iquote('0:MRR:9600.0,5.0')] ).
cnf(9604,plain,
( equal(index_90,u)
| equal(select(earray_85,u),select(earray_98,u)) ),
inference(rew,[status(thm),theory(equality)],[9601,9455]),
[iquote('0:Rew:9601.0,9455.1')] ).
cnf(9607,plain,
( equal(seq,head)
| equal(select(q24,seq),earray_112) ),
inference(spr,[status(thm),theory(equality)],[9597,1669]),
[iquote('0:SpR:9597.0,1669.1')] ).
cnf(9608,plain,
( equal(seq,head)
| equal(earray_119,earray_112) ),
inference(rew,[status(thm),theory(equality)],[62,9607]),
[iquote('0:Rew:62.0,9607.1')] ).
cnf(9609,plain,
equal(earray_119,earray_112),
inference(mrr,[status(thm)],[9608,4]),
[iquote('0:MRR:9608.0,4.0')] ).
cnf(9612,plain,
( equal(index_120,u)
| equal(select(earray_121,u),select(earray_112,u)) ),
inference(rew,[status(thm),theory(equality)],[9609,1757]),
[iquote('0:Rew:9609.0,1757.1')] ).
cnf(9641,plain,
( equal(seq,tail)
| equal(select(q19,seq),earray_73) ),
inference(spr,[status(thm),theory(equality)],[1684,787]),
[iquote('0:SpR:1684.1,787.0')] ).
cnf(9643,plain,
( equal(seq,tail)
| equal(earray_83,earray_73) ),
inference(rew,[status(thm),theory(equality)],[112,9641]),
[iquote('0:Rew:112.0,9641.1')] ).
cnf(9644,plain,
equal(earray_83,earray_73),
inference(mrr,[status(thm)],[9643,5]),
[iquote('0:MRR:9643.0,5.0')] ).
cnf(9647,plain,
( equal(index_84,u)
| equal(select(earray_85,u),select(earray_73,u)) ),
inference(rew,[status(thm),theory(equality)],[9644,1733]),
[iquote('0:Rew:9644.0,1733.1')] ).
cnf(9665,plain,
( equal(seq,tail)
| equal(select(q17,seq),earray_58) ),
inference(spr,[status(thm),theory(equality)],[1686,789]),
[iquote('0:SpR:1686.1,789.0')] ).
cnf(9667,plain,
( equal(seq,tail)
| equal(earray_62,earray_58) ),
inference(rew,[status(thm),theory(equality)],[105,9665]),
[iquote('0:Rew:105.0,9665.1')] ).
cnf(9668,plain,
equal(earray_62,earray_58),
inference(mrr,[status(thm)],[9667,5]),
[iquote('0:MRR:9667.0,5.0')] ).
cnf(9671,plain,
( equal(index_63,u)
| equal(select(earray_64,u),select(earray_58,u)) ),
inference(rew,[status(thm),theory(equality)],[9668,1736]),
[iquote('0:Rew:9668.0,1736.1')] ).
cnf(9677,plain,
( equal(seq,tail)
| equal(select(q16,seq),earray_52) ),
inference(spr,[status(thm),theory(equality)],[1687,790]),
[iquote('0:SpR:1687.1,790.0')] ).
cnf(9679,plain,
( equal(seq,tail)
| equal(earray_56,earray_52) ),
inference(rew,[status(thm),theory(equality)],[103,9677]),
[iquote('0:Rew:103.0,9677.1')] ).
cnf(9680,plain,
equal(earray_56,earray_52),
inference(mrr,[status(thm)],[9679,5]),
[iquote('0:MRR:9679.0,5.0')] ).
cnf(9683,plain,
( equal(index_57,u)
| equal(select(earray_58,u),select(earray_52,u)) ),
inference(rew,[status(thm),theory(equality)],[9680,1737]),
[iquote('0:Rew:9680.0,1737.1')] ).
cnf(9689,plain,
( equal(seq,tail)
| equal(select(q14,seq),earray_37) ),
inference(spr,[status(thm),theory(equality)],[1688,793]),
[iquote('0:SpR:1688.1,793.0')] ).
cnf(9691,plain,
( equal(seq,tail)
| equal(earray_41,earray_37) ),
inference(rew,[status(thm),theory(equality)],[99,9689]),
[iquote('0:Rew:99.0,9689.1')] ).
cnf(9692,plain,
equal(earray_41,earray_37),
inference(mrr,[status(thm)],[9691,5]),
[iquote('0:MRR:9691.0,5.0')] ).
cnf(9695,plain,
( equal(index_42,u)
| equal(select(earray_43,u),select(earray_37,u)) ),
inference(rew,[status(thm),theory(equality)],[9692,1739]),
[iquote('0:Rew:9692.0,1739.1')] ).
cnf(9701,plain,
( equal(seq,tail)
| equal(select(q13,seq),earray_31) ),
inference(spr,[status(thm),theory(equality)],[1689,794]),
[iquote('0:SpR:1689.1,794.0')] ).
cnf(9703,plain,
( equal(seq,tail)
| equal(earray_35,earray_31) ),
inference(rew,[status(thm),theory(equality)],[96,9701]),
[iquote('0:Rew:96.0,9701.1')] ).
cnf(9704,plain,
equal(earray_35,earray_31),
inference(mrr,[status(thm)],[9703,5]),
[iquote('0:MRR:9703.0,5.0')] ).
cnf(9707,plain,
( equal(index_36,u)
| equal(select(earray_37,u),select(earray_31,u)) ),
inference(rew,[status(thm),theory(equality)],[9704,1741]),
[iquote('0:Rew:9704.0,1741.1')] ).
cnf(9737,plain,
( equal(seq,tail)
| equal(select(q11,seq),earray_16) ),
inference(spr,[status(thm),theory(equality)],[1692,802]),
[iquote('0:SpR:1692.1,802.0')] ).
cnf(9739,plain,
( equal(seq,tail)
| equal(earray_20,earray_16) ),
inference(rew,[status(thm),theory(equality)],[89,9737]),
[iquote('0:Rew:89.0,9737.1')] ).
cnf(9740,plain,
equal(earray_20,earray_16),
inference(mrr,[status(thm)],[9739,5]),
[iquote('0:MRR:9739.0,5.0')] ).
cnf(9743,plain,
( equal(index_21,u)
| equal(select(earray_22,u),select(earray_16,u)) ),
inference(rew,[status(thm),theory(equality)],[9740,1743]),
[iquote('0:Rew:9740.0,1743.1')] ).
cnf(9773,plain,
( equal(seq,tail)
| equal(select(q29,seq),earray_148) ),
inference(spr,[status(thm),theory(equality)],[1695,805]),
[iquote('0:SpR:1695.1,805.0')] ).
cnf(9775,plain,
( equal(seq,tail)
| equal(earray_161,earray_148) ),
inference(rew,[status(thm),theory(equality)],[76,9773]),
[iquote('0:Rew:76.0,9773.1')] ).
cnf(9776,plain,
equal(earray_161,earray_148),
inference(mrr,[status(thm)],[9775,5]),
[iquote('0:MRR:9775.0,5.0')] ).
cnf(9779,plain,
( equal(index_162,u)
| equal(select(earray_163,u),select(earray_148,u)) ),
inference(rew,[status(thm),theory(equality)],[9776,1750]),
[iquote('0:Rew:9776.0,1750.1')] ).
cnf(9785,plain,
( equal(seq,tail)
| equal(select(q28,seq),earray_142) ),
inference(spr,[status(thm),theory(equality)],[1696,806]),
[iquote('0:SpR:1696.1,806.0')] ).
cnf(9787,plain,
( equal(seq,tail)
| equal(earray_146,earray_142) ),
inference(rew,[status(thm),theory(equality)],[71,9785]),
[iquote('0:Rew:71.0,9785.1')] ).
cnf(9788,plain,
equal(earray_146,earray_142),
inference(mrr,[status(thm)],[9787,5]),
[iquote('0:MRR:9787.0,5.0')] ).
cnf(9791,plain,
( equal(index_147,u)
| equal(select(earray_148,u),select(earray_142,u)) ),
inference(rew,[status(thm),theory(equality)],[9788,1753]),
[iquote('0:Rew:9788.0,1753.1')] ).
cnf(9797,plain,
( equal(seq,tail)
| equal(select(q26,seq),earray_127) ),
inference(spr,[status(thm),theory(equality)],[1697,808]),
[iquote('0:SpR:1697.1,808.0')] ).
cnf(9799,plain,
( equal(seq,tail)
| equal(earray_131,earray_127) ),
inference(rew,[status(thm),theory(equality)],[66,9797]),
[iquote('0:Rew:66.0,9797.1')] ).
cnf(9800,plain,
equal(earray_131,earray_127),
inference(mrr,[status(thm)],[9799,5]),
[iquote('0:MRR:9799.0,5.0')] ).
cnf(9803,plain,
( equal(index_132,u)
| equal(select(earray_133,u),select(earray_127,u)) ),
inference(rew,[status(thm),theory(equality)],[9800,1755]),
[iquote('0:Rew:9800.0,1755.1')] ).
cnf(9821,plain,
( equal(seq,tail)
| equal(select(q25,seq),earray_121) ),
inference(spr,[status(thm),theory(equality)],[1699,809]),
[iquote('0:SpR:1699.1,809.0')] ).
cnf(9823,plain,
( equal(seq,tail)
| equal(earray_125,earray_121) ),
inference(rew,[status(thm),theory(equality)],[64,9821]),
[iquote('0:Rew:64.0,9821.1')] ).
cnf(9824,plain,
equal(earray_125,earray_121),
inference(mrr,[status(thm)],[9823,5]),
[iquote('0:MRR:9823.0,5.0')] ).
cnf(9827,plain,
( equal(index_126,u)
| equal(select(earray_127,u),select(earray_121,u)) ),
inference(rew,[status(thm),theory(equality)],[9824,1756]),
[iquote('0:Rew:9824.0,1756.1')] ).
cnf(9833,plain,
( equal(seq,tail)
| equal(select(q23,seq),earray_106) ),
inference(spr,[status(thm),theory(equality)],[1700,812]),
[iquote('0:SpR:1700.1,812.0')] ).
cnf(9835,plain,
( equal(seq,tail)
| equal(earray_110,earray_106) ),
inference(rew,[status(thm),theory(equality)],[60,9833]),
[iquote('0:Rew:60.0,9833.1')] ).
cnf(9836,plain,
equal(earray_110,earray_106),
inference(mrr,[status(thm)],[9835,5]),
[iquote('0:MRR:9835.0,5.0')] ).
cnf(9839,plain,
( equal(index_111,u)
| equal(select(earray_112,u),select(earray_106,u)) ),
inference(rew,[status(thm),theory(equality)],[9836,1758]),
[iquote('0:Rew:9836.0,1758.1')] ).
cnf(9845,plain,
( equal(seq,tail)
| equal(select(q22,seq),earray_100) ),
inference(spr,[status(thm),theory(equality)],[1701,813]),
[iquote('0:SpR:1701.1,813.0')] ).
cnf(9847,plain,
( equal(seq,tail)
| equal(earray_104,earray_100) ),
inference(rew,[status(thm),theory(equality)],[58,9845]),
[iquote('0:Rew:58.0,9845.1')] ).
cnf(9848,plain,
equal(earray_104,earray_100),
inference(mrr,[status(thm)],[9847,5]),
[iquote('0:MRR:9847.0,5.0')] ).
cnf(9851,plain,
( equal(index_105,u)
| equal(select(earray_106,u),select(earray_100,u)) ),
inference(rew,[status(thm),theory(equality)],[9848,1759]),
[iquote('0:Rew:9848.0,1759.1')] ).
cnf(9858,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_94,u),select(q20,u)) ),
inference(spr,[status(thm),theory(equality)],[1702,1672]),
[iquote('0:SpR:1702.1,1672.1')] ).
cnf(9861,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q20,u),select(q19,u)) ),
inference(spr,[status(thm),theory(equality)],[1703,1682]),
[iquote('0:SpR:1703.1,1682.1')] ).
cnf(9863,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_94,u),select(q19,u)) ),
inference(rew,[status(thm),theory(equality)],[9861,9858]),
[iquote('0:Rew:9861.2,9858.2')] ).
cnf(9865,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q1,u),select(q2,u)) ),
inference(spr,[status(thm),theory(equality)],[1704,1683]),
[iquote('0:SpR:1704.1,1683.1')] ).
cnf(9868,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q19,u),select(q18,u)) ),
inference(spr,[status(thm),theory(equality)],[1705,1684]),
[iquote('0:SpR:1705.1,1684.1')] ).
cnf(9871,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_94,u),select(q18,u)) ),
inference(rew,[status(thm),theory(equality)],[9868,9863]),
[iquote('0:Rew:9868.2,9863.2')] ).
cnf(9873,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_67,u),select(q17,u)) ),
inference(spr,[status(thm),theory(equality)],[1706,1673]),
[iquote('0:SpR:1706.1,1673.1')] ).
cnf(9876,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q17,u),select(q16,u)) ),
inference(spr,[status(thm),theory(equality)],[1707,1686]),
[iquote('0:SpR:1707.1,1686.1')] ).
cnf(9878,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_67,u),select(q16,u)) ),
inference(rew,[status(thm),theory(equality)],[9876,9873]),
[iquote('0:Rew:9876.2,9873.2')] ).
cnf(9880,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q16,u),select(q15,u)) ),
inference(spr,[status(thm),theory(equality)],[1708,1687]),
[iquote('0:SpR:1708.1,1687.1')] ).
cnf(9883,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_67,u),select(q15,u)) ),
inference(rew,[status(thm),theory(equality)],[9880,9878]),
[iquote('0:Rew:9880.2,9878.2')] ).
cnf(9885,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q1,u),select(q0,u)) ),
inference(spr,[status(thm),theory(equality)],[1709,1685]),
[iquote('0:SpR:1709.1,1685.1')] ).
cnf(9887,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q0,u),select(q2,u)) ),
inference(rew,[status(thm),theory(equality)],[9865,9885]),
[iquote('0:Rew:9865.2,9885.2')] ).
cnf(9889,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_46,u),select(q14,u)) ),
inference(spr,[status(thm),theory(equality)],[1710,1674]),
[iquote('0:SpR:1710.1,1674.1')] ).
cnf(9892,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q14,u),select(q13,u)) ),
inference(spr,[status(thm),theory(equality)],[1711,1688]),
[iquote('0:SpR:1711.1,1688.1')] ).
cnf(9894,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_46,u),select(q13,u)) ),
inference(rew,[status(thm),theory(equality)],[9892,9889]),
[iquote('0:Rew:9892.2,9889.2')] ).
cnf(9896,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q13,u),select(q12,u)) ),
inference(spr,[status(thm),theory(equality)],[1712,1689]),
[iquote('0:SpR:1712.1,1689.1')] ).
cnf(9899,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_46,u),select(q12,u)) ),
inference(rew,[status(thm),theory(equality)],[9896,9894]),
[iquote('0:Rew:9896.2,9894.2')] ).
cnf(9901,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_25,u),select(q11,u)) ),
inference(spr,[status(thm),theory(equality)],[1713,1675]),
[iquote('0:SpR:1713.1,1675.1')] ).
cnf(9904,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_208,u),select(q8,u)) ),
inference(spr,[status(thm),theory(equality)],[1714,1676]),
[iquote('0:SpR:1714.1,1676.1')] ).
cnf(9907,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q8,u),select(q7,u)) ),
inference(spr,[status(thm),theory(equality)],[1715,1690]),
[iquote('0:SpR:1715.1,1690.1')] ).
cnf(9909,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_208,u),select(q7,u)) ),
inference(rew,[status(thm),theory(equality)],[9907,9904]),
[iquote('0:Rew:9907.2,9904.2')] ).
cnf(9911,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q7,u),select(q6,u)) ),
inference(spr,[status(thm),theory(equality)],[1716,1691]),
[iquote('0:SpR:1716.1,1691.1')] ).
cnf(9914,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_208,u),select(q6,u)) ),
inference(rew,[status(thm),theory(equality)],[9911,9909]),
[iquote('0:Rew:9911.2,9909.2')] ).
cnf(9916,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_187,u),select(q5,u)) ),
inference(spr,[status(thm),theory(equality)],[1717,1677]),
[iquote('0:SpR:1717.1,1677.1')] ).
cnf(9919,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q5,u),select(q4,u)) ),
inference(spr,[status(thm),theory(equality)],[1718,1693]),
[iquote('0:SpR:1718.1,1693.1')] ).
cnf(9921,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_187,u),select(q4,u)) ),
inference(rew,[status(thm),theory(equality)],[9919,9916]),
[iquote('0:Rew:9919.2,9916.2')] ).
cnf(9923,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q4,u),select(q3,u)) ),
inference(spr,[status(thm),theory(equality)],[1719,1694]),
[iquote('0:SpR:1719.1,1694.1')] ).
cnf(9926,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_187,u),select(q3,u)) ),
inference(rew,[status(thm),theory(equality)],[9923,9921]),
[iquote('0:Rew:9923.2,9921.2')] ).
cnf(9928,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q11,u),select(q10,u)) ),
inference(spr,[status(thm),theory(equality)],[1720,1692]),
[iquote('0:SpR:1720.1,1692.1')] ).
cnf(9930,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_25,u),select(q10,u)) ),
inference(rew,[status(thm),theory(equality)],[9928,9901]),
[iquote('0:Rew:9928.2,9901.2')] ).
cnf(9932,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_166,u),select(q29,u)) ),
inference(spr,[status(thm),theory(equality)],[1721,1678]),
[iquote('0:SpR:1721.1,1678.1')] ).
cnf(9935,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_157,u),select(q2,u)) ),
inference(spr,[status(thm),theory(equality)],[1722,1679]),
[iquote('0:SpR:1722.1,1679.1')] ).
cnf(9938,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q29,u),select(q28,u)) ),
inference(spr,[status(thm),theory(equality)],[1723,1695]),
[iquote('0:SpR:1723.1,1695.1')] ).
cnf(9940,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_166,u),select(q28,u)) ),
inference(rew,[status(thm),theory(equality)],[9938,9932]),
[iquote('0:Rew:9938.2,9932.2')] ).
cnf(9942,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q28,u),select(q27,u)) ),
inference(spr,[status(thm),theory(equality)],[1724,1696]),
[iquote('0:SpR:1724.1,1696.1')] ).
cnf(9945,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_166,u),select(q27,u)) ),
inference(rew,[status(thm),theory(equality)],[9942,9940]),
[iquote('0:Rew:9942.2,9940.2')] ).
cnf(9947,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_136,u),select(q26,u)) ),
inference(spr,[status(thm),theory(equality)],[1725,1680]),
[iquote('0:SpR:1725.1,1680.1')] ).
cnf(9950,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q26,u),select(q25,u)) ),
inference(spr,[status(thm),theory(equality)],[1726,1697]),
[iquote('0:SpR:1726.1,1697.1')] ).
cnf(9952,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_136,u),select(q25,u)) ),
inference(rew,[status(thm),theory(equality)],[9950,9947]),
[iquote('0:Rew:9950.2,9947.2')] ).
cnf(9954,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q25,u),select(q24,u)) ),
inference(spr,[status(thm),theory(equality)],[1727,1699]),
[iquote('0:SpR:1727.1,1699.1')] ).
cnf(9957,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_136,u),select(q24,u)) ),
inference(rew,[status(thm),theory(equality)],[9954,9952]),
[iquote('0:Rew:9954.2,9952.2')] ).
cnf(9959,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_115,u),select(q23,u)) ),
inference(spr,[status(thm),theory(equality)],[1728,1681]),
[iquote('0:SpR:1728.1,1681.1')] ).
cnf(9962,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q9,u),select(q10,u)) ),
inference(spr,[status(thm),theory(equality)],[1729,1698]),
[iquote('0:SpR:1729.1,1698.1')] ).
cnf(9965,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q23,u),select(q22,u)) ),
inference(spr,[status(thm),theory(equality)],[1730,1700]),
[iquote('0:SpR:1730.1,1700.1')] ).
cnf(9967,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(queue_115,u),select(q22,u)) ),
inference(rew,[status(thm),theory(equality)],[9965,9959]),
[iquote('0:Rew:9965.2,9959.2')] ).
cnf(9969,plain,
( equal(seq,u)
| equal(tail,u)
| equal(select(q21,u),select(q22,u)) ),
inference(spr,[status(thm),theory(equality)],[1731,1701]),
[iquote('0:SpR:1731.1,1701.1')] ).
cnf(10005,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(select(earray_73,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[9647,9604]),
[iquote('0:SpR:9647.1,9604.1')] ).
cnf(10037,plain,
( equal(index_213,index_162)
| equal(select(earray_148,index_213),elem_214) ),
inference(spr,[status(thm),theory(equality)],[9779,9556]),
[iquote('0:SpR:9779.1,9556.0')] ).
cnf(10039,plain,
equal(index_213,index_162),
inference(spt,[spt(split,[position(s1)])],[10037]),
[iquote('1:Spt:10037.0')] ).
cnf(10042,plain,
equal(s(index_167),index_162),
inference(rew,[status(thm),theory(equality)],[10039,845]),
[iquote('1:Rew:10039.0,845.0')] ).
cnf(10281,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q18,head),index_95) ),
inference(spr,[status(thm),theory(equality)],[9871,197]),
[iquote('0:SpR:9871.2,197.0')] ).
cnf(10285,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_95,index_69) ),
inference(rew,[status(thm),theory(equality)],[744,10281]),
[iquote('0:Rew:744.0,10281.2')] ).
cnf(10286,plain,
equal(index_95,index_69),
inference(mrr,[status(thm)],[10285,4,3]),
[iquote('0:MRR:10285.0,10285.1,4.0,3.0')] ).
cnf(10287,plain,
equal(s(index_69),index_96),
inference(rew,[status(thm),theory(equality)],[10286,198]),
[iquote('0:Rew:10286.0,198.0')] ).
cnf(10451,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q15,head),index_68) ),
inference(spr,[status(thm),theory(equality)],[9883,186]),
[iquote('0:SpR:9883.2,186.0')] ).
cnf(10455,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_68,index_48) ),
inference(rew,[status(thm),theory(equality)],[745,10451]),
[iquote('0:Rew:745.0,10451.2')] ).
cnf(10456,plain,
equal(index_68,index_48),
inference(mrr,[status(thm)],[10455,4,3]),
[iquote('0:MRR:10455.0,10455.1,4.0,3.0')] ).
cnf(10457,plain,
equal(s(index_48),index_69),
inference(rew,[status(thm),theory(equality)],[10456,187]),
[iquote('0:Rew:10456.0,187.0')] ).
cnf(10712,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q2,head),index_3) ),
inference(spr,[status(thm),theory(equality)],[9887,9430]),
[iquote('0:SpR:9887.2,9430.0')] ).
cnf(10715,plain,
equal(select(q2,head),index_3),
inference(mrr,[status(thm)],[10712,4,3]),
[iquote('0:MRR:10712.0,10712.1,4.0,3.0')] ).
cnf(10724,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q12,head),index_47) ),
inference(spr,[status(thm),theory(equality)],[9899,177]),
[iquote('0:SpR:9899.2,177.0')] ).
cnf(10728,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_47,index_27) ),
inference(rew,[status(thm),theory(equality)],[746,10724]),
[iquote('0:Rew:746.0,10724.2')] ).
cnf(10729,plain,
equal(index_47,index_27),
inference(mrr,[status(thm)],[10728,4,3]),
[iquote('0:MRR:10728.0,10728.1,4.0,3.0')] ).
cnf(10730,plain,
equal(s(index_27),index_48),
inference(rew,[status(thm),theory(equality)],[10729,178]),
[iquote('0:Rew:10729.0,178.0')] ).
cnf(10991,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q6,head),index_209) ),
inference(spr,[status(thm),theory(equality)],[9914,163]),
[iquote('0:SpR:9914.2,163.0')] ).
cnf(10995,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_209,index_189) ),
inference(rew,[status(thm),theory(equality)],[748,10991]),
[iquote('0:Rew:748.0,10991.2')] ).
cnf(10996,plain,
equal(index_209,index_189),
inference(mrr,[status(thm)],[10995,4,3]),
[iquote('0:MRR:10995.0,10995.1,4.0,3.0')] ).
cnf(10997,plain,
equal(s(index_189),index_210),
inference(rew,[status(thm),theory(equality)],[10996,165]),
[iquote('0:Rew:10996.0,165.0')] ).
cnf(11161,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q3,head),index_188) ),
inference(spr,[status(thm),theory(equality)],[9926,155]),
[iquote('0:SpR:9926.2,155.0')] ).
cnf(11165,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_188,index_159) ),
inference(rew,[status(thm),theory(equality)],[750,11161]),
[iquote('0:Rew:750.0,11161.2')] ).
cnf(11166,plain,
equal(index_188,index_159),
inference(mrr,[status(thm)],[11165,4,3]),
[iquote('0:MRR:11165.0,11165.1,4.0,3.0')] ).
cnf(11167,plain,
equal(s(index_159),index_189),
inference(rew,[status(thm),theory(equality)],[11166,156]),
[iquote('0:Rew:11166.0,156.0')] ).
cnf(11425,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q10,head),index_26) ),
inference(spr,[status(thm),theory(equality)],[9930,168]),
[iquote('0:SpR:9930.2,168.0')] ).
cnf(11429,plain,
equal(select(q10,head),index_26),
inference(mrr,[status(thm)],[11425,4,3]),
[iquote('0:MRR:11425.0,11425.1,4.0,3.0')] ).
cnf(11435,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q2,head),index_158) ),
inference(spr,[status(thm),theory(equality)],[9935,142]),
[iquote('0:SpR:9935.2,142.0')] ).
cnf(11439,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_158,index_3) ),
inference(rew,[status(thm),theory(equality)],[10715,11435]),
[iquote('0:Rew:10715.0,11435.2')] ).
cnf(11440,plain,
equal(index_158,index_3),
inference(mrr,[status(thm)],[11439,4,3]),
[iquote('0:MRR:11439.0,11439.1,4.0,3.0')] ).
cnf(11441,plain,
equal(s(index_3),index_159),
inference(rew,[status(thm),theory(equality)],[11440,143]),
[iquote('0:Rew:11440.0,143.0')] ).
cnf(11493,plain,
equal(index_159,index_78),
inference(rew,[status(thm),theory(equality)],[873,11441]),
[iquote('0:Rew:873.0,11441.0')] ).
cnf(11496,plain,
equal(s(index_78),index_189),
inference(rew,[status(thm),theory(equality)],[11493,11167]),
[iquote('0:Rew:11493.0,11167.0')] ).
cnf(11550,plain,
equal(index_189,index_153),
inference(rew,[status(thm),theory(equality)],[859,11496]),
[iquote('0:Rew:859.0,11496.0')] ).
cnf(11554,plain,
equal(s(index_153),index_210),
inference(rew,[status(thm),theory(equality)],[11550,10997]),
[iquote('0:Rew:11550.0,10997.0')] ).
cnf(11608,plain,
equal(index_210,index_171),
inference(rew,[status(thm),theory(equality)],[6681,11554]),
[iquote('0:Rew:6681.0,11554.0')] ).
cnf(11610,plain,
equal(select(q9,head),index_171),
inference(rew,[status(thm),theory(equality)],[11608,747]),
[iquote('0:Rew:11608.0,747.0')] ).
cnf(11937,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q27,head),index_167) ),
inference(spr,[status(thm),theory(equality)],[9945,146]),
[iquote('0:SpR:9945.2,146.0')] ).
cnf(11941,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_167,index_138) ),
inference(rew,[status(thm),theory(equality)],[751,11937]),
[iquote('0:Rew:751.0,11937.2')] ).
cnf(11942,plain,
equal(index_167,index_138),
inference(mrr,[status(thm)],[11941,4,3]),
[iquote('0:MRR:11941.0,11941.1,4.0,3.0')] ).
cnf(11944,plain,
equal(s(index_138),index_162),
inference(rew,[status(thm),theory(equality)],[11942,10042]),
[iquote('1:Rew:11942.0,10042.0')] ).
cnf(12203,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q24,head),index_137) ),
inference(spr,[status(thm),theory(equality)],[9957,133]),
[iquote('0:SpR:9957.2,133.0')] ).
cnf(12207,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_137,index_117) ),
inference(rew,[status(thm),theory(equality)],[752,12203]),
[iquote('0:Rew:752.0,12203.2')] ).
cnf(12208,plain,
equal(index_137,index_117),
inference(mrr,[status(thm)],[12207,4,3]),
[iquote('0:MRR:12207.0,12207.1,4.0,3.0')] ).
cnf(12209,plain,
equal(s(index_117),index_138),
inference(rew,[status(thm),theory(equality)],[12208,134]),
[iquote('0:Rew:12208.0,134.0')] ).
cnf(12464,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q10,head),index_171) ),
inference(spr,[status(thm),theory(equality)],[9962,11610]),
[iquote('0:SpR:9962.2,11610.0')] ).
cnf(12467,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_26,index_171) ),
inference(rew,[status(thm),theory(equality)],[11429,12464]),
[iquote('0:Rew:11429.0,12464.2')] ).
cnf(12468,plain,
equal(index_26,index_171),
inference(mrr,[status(thm)],[12467,4,3]),
[iquote('0:MRR:12467.0,12467.1,4.0,3.0')] ).
cnf(12469,plain,
equal(s(index_171),index_27),
inference(rew,[status(thm),theory(equality)],[12468,169]),
[iquote('0:Rew:12468.0,169.0')] ).
cnf(12522,plain,
equal(index_27,index_177),
inference(rew,[status(thm),theory(equality)],[936,12469]),
[iquote('0:Rew:936.0,12469.0')] ).
cnf(12526,plain,
equal(s(index_177),index_48),
inference(rew,[status(thm),theory(equality)],[12522,10730]),
[iquote('0:Rew:12522.0,10730.0')] ).
cnf(12579,plain,
equal(index_48,index_183),
inference(rew,[status(thm),theory(equality)],[929,12526]),
[iquote('0:Rew:929.0,12526.0')] ).
cnf(12583,plain,
equal(s(index_183),index_69),
inference(rew,[status(thm),theory(equality)],[12579,10457]),
[iquote('0:Rew:12579.0,10457.0')] ).
cnf(12637,plain,
equal(index_69,index_192),
inference(rew,[status(thm),theory(equality)],[6276,12583]),
[iquote('0:Rew:6276.0,12583.0')] ).
cnf(12640,plain,
equal(s(index_192),index_96),
inference(rew,[status(thm),theory(equality)],[12637,10287]),
[iquote('0:Rew:12637.0,10287.0')] ).
cnf(12696,plain,
equal(index_96,index_198),
inference(rew,[status(thm),theory(equality)],[915,12640]),
[iquote('0:Rew:915.0,12640.0')] ).
cnf(12698,plain,
equal(select(q21,head),index_198),
inference(rew,[status(thm),theory(equality)],[12696,743]),
[iquote('0:Rew:12696.0,743.0')] ).
cnf(13124,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q22,head),index_116) ),
inference(spr,[status(thm),theory(equality)],[9967,124]),
[iquote('0:SpR:9967.2,124.0')] ).
cnf(13128,plain,
equal(select(q22,head),index_116),
inference(mrr,[status(thm)],[13124,4,3]),
[iquote('0:MRR:13124.0,13124.1,4.0,3.0')] ).
cnf(13133,plain,
( equal(seq,head)
| equal(tail,head)
| equal(select(q22,head),index_198) ),
inference(spr,[status(thm),theory(equality)],[9969,12698]),
[iquote('0:SpR:9969.2,12698.0')] ).
cnf(13136,plain,
( equal(seq,head)
| equal(tail,head)
| equal(index_116,index_198) ),
inference(rew,[status(thm),theory(equality)],[13128,13133]),
[iquote('0:Rew:13128.0,13133.2')] ).
cnf(13137,plain,
equal(index_116,index_198),
inference(mrr,[status(thm)],[13136,4,3]),
[iquote('0:MRR:13136.0,13136.1,4.0,3.0')] ).
cnf(13138,plain,
equal(s(index_198),index_117),
inference(rew,[status(thm),theory(equality)],[13137,125]),
[iquote('0:Rew:13137.0,125.0')] ).
cnf(13191,plain,
equal(index_117,index_204),
inference(rew,[status(thm),theory(equality)],[908,13138]),
[iquote('0:Rew:908.0,13138.0')] ).
cnf(13195,plain,
equal(s(index_204),index_138),
inference(rew,[status(thm),theory(equality)],[13191,12209]),
[iquote('0:Rew:13191.0,12209.0')] ).
cnf(13248,plain,
equal(index_138,index_9),
inference(rew,[status(thm),theory(equality)],[5871,13195]),
[iquote('0:Rew:5871.0,13195.0')] ).
cnf(13251,plain,
equal(index_167,index_9),
inference(rew,[status(thm),theory(equality)],[13248,11942]),
[iquote('0:Rew:13248.0,11942.0')] ).
cnf(13252,plain,
equal(s(index_9),index_162),
inference(rew,[status(thm),theory(equality)],[13248,11944]),
[iquote('1:Rew:13248.0,11944.0')] ).
cnf(13306,plain,
equal(index_162,index_15),
inference(rew,[status(thm),theory(equality)],[964,13252]),
[iquote('1:Rew:964.0,13252.0')] ).
cnf(13307,plain,
$false,
inference(mrr,[status(thm)],[13306,8527]),
[iquote('1:MRR:13306.0,8527.0')] ).
cnf(13308,plain,
~ equal(index_213,index_162),
inference(spt,[spt(split,[position(sa)])],[13307,10039]),
[iquote('1:Spt:13307.0,10037.0,10039.0')] ).
cnf(13309,plain,
equal(select(earray_148,index_213),elem_214),
inference(spt,[spt(split,[position(s2)])],[10037]),
[iquote('1:Spt:13307.0,10037.1')] ).
cnf(13311,plain,
equal(s(index_9),index_213),
inference(rew,[status(thm),theory(equality)],[13251,845]),
[iquote('0:Rew:13251.0,845.0')] ).
cnf(13312,plain,
equal(index_213,index_15),
inference(rew,[status(thm),theory(equality)],[964,13311]),
[iquote('0:Rew:964.0,13311.0')] ).
cnf(13326,plain,
equal(select(earray_148,index_15),elem_214),
inference(rew,[status(thm),theory(equality)],[13312,13309]),
[iquote('1:Rew:13312.0,13309.0')] ).
cnf(13733,plain,
( equal(index_15,index_147)
| equal(select(earray_142,index_15),elem_214) ),
inference(spr,[status(thm),theory(equality)],[13326,9791]),
[iquote('1:SpR:13326.0,9791.1')] ).
cnf(13734,plain,
equal(select(earray_142,index_15),elem_214),
inference(mrr,[status(thm)],[13733,8503]),
[iquote('1:MRR:13733.0,8503.0')] ).
cnf(13739,plain,
( equal(index_15,index_141)
| equal(select(earray_133,index_15),elem_214) ),
inference(spr,[status(thm),theory(equality)],[13734,9585]),
[iquote('1:SpR:13734.0,9585.1')] ).
cnf(13740,plain,
equal(select(earray_133,index_15),elem_214),
inference(mrr,[status(thm)],[13739,8479]),
[iquote('1:MRR:13739.0,8479.0')] ).
cnf(13742,plain,
( equal(index_15,index_132)
| equal(select(earray_127,index_15),elem_214) ),
inference(spr,[status(thm),theory(equality)],[13740,9803]),
[iquote('1:SpR:13740.0,9803.1')] ).
cnf(13743,plain,
equal(select(earray_127,index_15),elem_214),
inference(mrr,[status(thm)],[13742,8455]),
[iquote('1:MRR:13742.0,8455.0')] ).
cnf(13745,plain,
( equal(index_15,index_126)
| equal(select(earray_121,index_15),elem_214) ),
inference(spr,[status(thm),theory(equality)],[13743,9827]),
[iquote('1:SpR:13743.0,9827.1')] ).
cnf(13746,plain,
equal(select(earray_121,index_15),elem_214),
inference(mrr,[status(thm)],[13745,8431]),
[iquote('1:MRR:13745.0,8431.0')] ).
cnf(13748,plain,
( equal(index_15,index_120)
| equal(select(earray_112,index_15),elem_214) ),
inference(spr,[status(thm),theory(equality)],[13746,9612]),
[iquote('1:SpR:13746.0,9612.1')] ).
cnf(13749,plain,
equal(select(earray_112,index_15),elem_214),
inference(mrr,[status(thm)],[13748,7651]),
[iquote('1:MRR:13748.0,7651.0')] ).
cnf(13754,plain,
( equal(index_15,index_111)
| equal(select(earray_106,index_15),elem_214) ),
inference(spr,[status(thm),theory(equality)],[13749,9839]),
[iquote('1:SpR:13749.0,9839.1')] ).
cnf(13755,plain,
equal(select(earray_106,index_15),elem_214),
inference(mrr,[status(thm)],[13754,5647]),
[iquote('1:MRR:13754.0,5647.0')] ).
cnf(13757,plain,
( equal(index_15,index_105)
| equal(select(earray_100,index_15),elem_214) ),
inference(spr,[status(thm),theory(equality)],[13755,9851]),
[iquote('1:SpR:13755.0,9851.1')] ).
cnf(13758,plain,
equal(select(earray_100,index_15),elem_214),
inference(mrr,[status(thm)],[13757,5644]),
[iquote('1:MRR:13757.0,5644.0')] ).
cnf(13768,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(select(earray_64,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[10005,9477]),
[iquote('0:SpR:10005.2,9477.1')] ).
cnf(13825,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(select(earray_58,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[13768,9671]),
[iquote('0:SpR:13768.3,9671.1')] ).
cnf(13841,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(select(earray_52,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[13825,9683]),
[iquote('0:SpR:13825.4,9683.1')] ).
cnf(13857,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(index_51,u)
| equal(select(earray_43,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[13841,9492]),
[iquote('0:SpR:13841.5,9492.1')] ).
cnf(13873,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(index_51,u)
| equal(index_42,u)
| equal(select(earray_37,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[13857,9695]),
[iquote('0:SpR:13857.6,9695.1')] ).
cnf(13889,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(index_51,u)
| equal(index_42,u)
| equal(index_36,u)
| equal(select(earray_31,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[13873,9707]),
[iquote('0:SpR:13873.7,9707.1')] ).
cnf(13910,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(index_51,u)
| equal(index_42,u)
| equal(index_36,u)
| equal(index_30,u)
| equal(select(earray_22,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[13889,9507]),
[iquote('0:SpR:13889.8,9507.1')] ).
cnf(13918,plain,
( equal(index_84,u)
| equal(index_90,u)
| equal(index_72,u)
| equal(index_63,u)
| equal(index_57,u)
| equal(index_51,u)
| equal(index_42,u)
| equal(index_36,u)
| equal(index_30,u)
| equal(index_21,u)
| equal(select(earray_16,u),select(earray_98,u)) ),
inference(spr,[status(thm),theory(equality)],[13910,9743]),
[iquote('0:SpR:13910.9,9743.1')] ).
cnf(13925,plain,
( equal(index_84,index_15)
| equal(index_90,index_15)
| equal(index_72,index_15)
| equal(index_63,index_15)
| equal(index_57,index_15)
| equal(index_51,index_15)
| equal(index_42,index_15)
| equal(index_36,index_15)
| equal(index_30,index_15)
| equal(index_21,index_15)
| equal(select(earray_98,index_15),e10) ),
inference(spr,[status(thm),theory(equality)],[13918,833]),
[iquote('0:SpR:13918.10,833.0')] ).
cnf(13928,plain,
equal(select(earray_98,index_15),e10),
inference(mrr,[status(thm)],[13925,5635,5638,5632,5629,5626,5623,5620,5617,5469,923]),
[iquote('0:MRR:13925.0,13925.1,13925.2,13925.3,13925.4,13925.5,13925.6,13925.7,13925.8,13925.9,5635.0,5638.0,5632.0,5629.0,5626.0,5623.0,5620.0,5617.0,5469.0,923.0')] ).
cnf(13930,plain,
( equal(index_15,index_99)
| equal(select(earray_100,index_15),e10) ),
inference(spr,[status(thm),theory(equality)],[13928,1760]),
[iquote('0:SpR:13928.0,1760.1')] ).
cnf(13931,plain,
( equal(index_15,index_99)
| equal(elem_214,e10) ),
inference(rew,[status(thm),theory(equality)],[13758,13930]),
[iquote('1:Rew:13758.0,13930.1')] ).
cnf(13932,plain,
$false,
inference(mrr,[status(thm)],[13931,5641,302]),
[iquote('1:MRR:13931.0,13931.1,5641.0,302.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SWV569-1.030 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.11/0.33 % Computer : n011.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Thu Jun 16 00:58:05 EDT 2022
% 0.11/0.33 % CPUTime :
% 12.84/13.08
% 12.84/13.08 SPASS V 3.9
% 12.84/13.08 SPASS beiseite: Proof found.
% 12.84/13.08 % SZS status Theorem
% 12.84/13.08 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.84/13.08 SPASS derived 8184 clauses, backtracked 206 clauses, performed 1 splits and kept 5946 clauses.
% 12.84/13.08 SPASS allocated 73400 KBytes.
% 12.84/13.08 SPASS spent 0:0:12.73 on the problem.
% 12.84/13.08 0:00:00.04 for the input.
% 12.84/13.08 0:00:00.00 for the FLOTTER CNF translation.
% 12.84/13.08 0:00:00.73 for inferences.
% 12.84/13.08 0:00:00.01 for the backtracking.
% 12.84/13.08 0:0:11.62 for the reduction.
% 12.84/13.08
% 12.84/13.08
% 12.84/13.08 Here is a proof with depth 12, length 863 :
% 12.84/13.08 % SZS output start Refutation
% See solution above
% 13.16/13.40 Formulae used in the proof : a1 a2 head_distinct_from_tail head_distinct_from_seq tail_distinct_from_seq as19 as18 as17 as16 as15 as14 as13 as12 as11 as10 as9 as8 as7 as6 as5 as4 as3 as2 as1 hyp1 hyp2 hyp3 hyp4 hyp5 hyp6 hyp7 hyp8 hyp9 hyp10 hyp11 hyp13 hyp14 hyp15 hyp16 hyp19 hyp20 hyp21 hyp33 hyp36 hyp37 hyp38 hyp39 hyp40 hyp41 hyp43 hyp44 hyp45 hyp46 hyp47 hyp48 hyp49 hyp50 hyp51 hyp52 hyp56 hyp57 hyp58 hyp59 hyp60 hyp61 hyp62 hyp63 hyp64 hyp65 hyp66 hyp67 hyp68 hyp69 hyp70 hyp71 hyp72 hyp73 hyp74 hyp75 hyp76 hyp77 hyp78 hyp79 hyp80 hyp81 hyp82 hyp83 hyp84 hyp85 hyp86 hyp87 hyp88 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 goal
% 13.16/13.40
%------------------------------------------------------------------------------