%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV505-1.030 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n016.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:43:39 EDT 2022
% Result : Unsatisfiable 0.85s 1.06s
% Output : Refutation 0.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 305
% Syntax : Number of clauses : 1241 ( 827 unt; 414 nHn;1241 RR)
% Number of literals : 1655 ( 0 equ; 301 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 130 ( 130 usr; 128 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(select(store(u,v,w),v),w),
file('SWV505-1.030.p',unknown),
[] ).
cnf(2,axiom,
( equal(u,v)
| equal(select(store(w,u,x),v),select(w,v)) ),
file('SWV505-1.030.p',unknown),
[] ).
cnf(3,axiom,
equal(store(a1,i1,e1),a_1069),
file('SWV505-1.030.p',unknown),
[] ).
cnf(4,axiom,
equal(store(a_1069,i2,e2),a_1070),
file('SWV505-1.030.p',unknown),
[] ).
cnf(5,axiom,
equal(store(a_1070,i3,e3),a_1071),
file('SWV505-1.030.p',unknown),
[] ).
cnf(6,axiom,
equal(store(a_1071,i4,e4),a_1072),
file('SWV505-1.030.p',unknown),
[] ).
cnf(7,axiom,
equal(store(a_1072,i5,e5),a_1073),
file('SWV505-1.030.p',unknown),
[] ).
cnf(8,axiom,
equal(store(a_1073,i6,e6),a_1074),
file('SWV505-1.030.p',unknown),
[] ).
cnf(9,axiom,
equal(store(a_1074,i7,e7),a_1075),
file('SWV505-1.030.p',unknown),
[] ).
cnf(10,axiom,
equal(store(a_1075,i8,e8),a_1076),
file('SWV505-1.030.p',unknown),
[] ).
cnf(11,axiom,
equal(store(a_1076,i9,e9),a_1077),
file('SWV505-1.030.p',unknown),
[] ).
cnf(12,axiom,
equal(store(a_1077,i10,e10),a_1078),
file('SWV505-1.030.p',unknown),
[] ).
cnf(13,axiom,
equal(store(a_1078,i11,e11),a_1079),
file('SWV505-1.030.p',unknown),
[] ).
cnf(14,axiom,
equal(store(a_1079,i12,e12),a_1080),
file('SWV505-1.030.p',unknown),
[] ).
cnf(15,axiom,
equal(store(a_1080,i13,e13),a_1081),
file('SWV505-1.030.p',unknown),
[] ).
cnf(16,axiom,
equal(store(a_1081,i14,e14),a_1082),
file('SWV505-1.030.p',unknown),
[] ).
cnf(17,axiom,
equal(store(a_1082,i15,e15),a_1083),
file('SWV505-1.030.p',unknown),
[] ).
cnf(18,axiom,
equal(store(a_1083,i16,e16),a_1084),
file('SWV505-1.030.p',unknown),
[] ).
cnf(19,axiom,
equal(store(a_1084,i17,e17),a_1085),
file('SWV505-1.030.p',unknown),
[] ).
cnf(20,axiom,
equal(store(a_1085,i18,e18),a_1086),
file('SWV505-1.030.p',unknown),
[] ).
cnf(21,axiom,
equal(store(a_1086,i19,e19),a_1087),
file('SWV505-1.030.p',unknown),
[] ).
cnf(22,axiom,
equal(store(a_1087,i20,e20),a_1088),
file('SWV505-1.030.p',unknown),
[] ).
cnf(23,axiom,
equal(store(a_1088,i21,e21),a_1089),
file('SWV505-1.030.p',unknown),
[] ).
cnf(24,axiom,
equal(store(a_1089,i22,e22),a_1090),
file('SWV505-1.030.p',unknown),
[] ).
cnf(25,axiom,
equal(store(a_1090,i23,e23),a_1091),
file('SWV505-1.030.p',unknown),
[] ).
cnf(26,axiom,
equal(store(a_1091,i24,e24),a_1092),
file('SWV505-1.030.p',unknown),
[] ).
cnf(27,axiom,
equal(store(a_1092,i25,e25),a_1093),
file('SWV505-1.030.p',unknown),
[] ).
cnf(28,axiom,
equal(store(a_1093,i26,e26),a_1094),
file('SWV505-1.030.p',unknown),
[] ).
cnf(29,axiom,
equal(store(a_1094,i27,e27),a_1095),
file('SWV505-1.030.p',unknown),
[] ).
cnf(30,axiom,
equal(store(a_1095,i28,e28),a_1096),
file('SWV505-1.030.p',unknown),
[] ).
cnf(31,axiom,
equal(store(a_1096,i29,e29),a_1097),
file('SWV505-1.030.p',unknown),
[] ).
cnf(32,axiom,
equal(store(a_1097,i30,e30),a_1098),
file('SWV505-1.030.p',unknown),
[] ).
cnf(33,axiom,
equal(store(a1,i13,e13),a_1099),
file('SWV505-1.030.p',unknown),
[] ).
cnf(34,axiom,
equal(store(a_1099,i1,e1),a_1100),
file('SWV505-1.030.p',unknown),
[] ).
cnf(35,axiom,
equal(store(a_1100,i19,e19),a_1101),
file('SWV505-1.030.p',unknown),
[] ).
cnf(36,axiom,
equal(store(a_1101,i4,e4),a_1102),
file('SWV505-1.030.p',unknown),
[] ).
cnf(37,axiom,
equal(store(a_1102,i9,e9),a_1103),
file('SWV505-1.030.p',unknown),
[] ).
cnf(38,axiom,
equal(store(a_1103,i30,e30),a_1104),
file('SWV505-1.030.p',unknown),
[] ).
cnf(39,axiom,
equal(store(a_1104,i2,e2),a_1105),
file('SWV505-1.030.p',unknown),
[] ).
cnf(40,axiom,
equal(store(a_1105,i15,e15),a_1106),
file('SWV505-1.030.p',unknown),
[] ).
cnf(41,axiom,
equal(store(a_1106,i25,e25),a_1107),
file('SWV505-1.030.p',unknown),
[] ).
cnf(42,axiom,
equal(store(a_1107,i18,e18),a_1108),
file('SWV505-1.030.p',unknown),
[] ).
cnf(43,axiom,
equal(store(a_1108,i20,e20),a_1109),
file('SWV505-1.030.p',unknown),
[] ).
cnf(44,axiom,
equal(store(a_1109,i8,e8),a_1110),
file('SWV505-1.030.p',unknown),
[] ).
cnf(45,axiom,
equal(store(a_1110,i21,e21),a_1111),
file('SWV505-1.030.p',unknown),
[] ).
cnf(46,axiom,
equal(store(a_1111,i6,e6),a_1112),
file('SWV505-1.030.p',unknown),
[] ).
cnf(47,axiom,
equal(store(a_1112,i11,e11),a_1113),
file('SWV505-1.030.p',unknown),
[] ).
cnf(48,axiom,
equal(store(a_1113,i14,e14),a_1114),
file('SWV505-1.030.p',unknown),
[] ).
cnf(49,axiom,
equal(store(a_1114,i29,e29),a_1115),
file('SWV505-1.030.p',unknown),
[] ).
cnf(50,axiom,
equal(store(a_1115,i5,e5),a_1116),
file('SWV505-1.030.p',unknown),
[] ).
cnf(51,axiom,
equal(store(a_1116,i26,e26),a_1117),
file('SWV505-1.030.p',unknown),
[] ).
cnf(52,axiom,
equal(store(a_1117,i22,e22),a_1118),
file('SWV505-1.030.p',unknown),
[] ).
cnf(53,axiom,
equal(store(a_1118,i27,e27),a_1119),
file('SWV505-1.030.p',unknown),
[] ).
cnf(54,axiom,
equal(store(a_1119,i3,e3),a_1120),
file('SWV505-1.030.p',unknown),
[] ).
cnf(55,axiom,
equal(store(a_1120,i12,e12),a_1121),
file('SWV505-1.030.p',unknown),
[] ).
cnf(56,axiom,
equal(store(a_1121,i16,e16),a_1122),
file('SWV505-1.030.p',unknown),
[] ).
cnf(57,axiom,
equal(store(a_1122,i28,e28),a_1123),
file('SWV505-1.030.p',unknown),
[] ).
cnf(58,axiom,
equal(store(a_1123,i17,e17),a_1124),
file('SWV505-1.030.p',unknown),
[] ).
cnf(59,axiom,
equal(store(a_1124,i23,e23),a_1125),
file('SWV505-1.030.p',unknown),
[] ).
cnf(60,axiom,
equal(store(a_1125,i24,e24),a_1126),
file('SWV505-1.030.p',unknown),
[] ).
cnf(61,axiom,
equal(store(a_1126,i7,e7),a_1127),
file('SWV505-1.030.p',unknown),
[] ).
cnf(62,axiom,
equal(store(a_1127,i10,e10),a_1128),
file('SWV505-1.030.p',unknown),
[] ).
cnf(63,axiom,
equal(select(a_1098,i_1129),e_1130),
file('SWV505-1.030.p',unknown),
[] ).
cnf(64,axiom,
equal(select(a_1128,i_1129),e_1131),
file('SWV505-1.030.p',unknown),
[] ).
cnf(66,axiom,
~ equal(i30,i29),
file('SWV505-1.030.p',unknown),
[] ).
cnf(67,axiom,
~ equal(i30,i28),
file('SWV505-1.030.p',unknown),
[] ).
cnf(68,axiom,
~ equal(i29,i28),
file('SWV505-1.030.p',unknown),
[] ).
cnf(69,axiom,
~ equal(i30,i27),
file('SWV505-1.030.p',unknown),
[] ).
cnf(70,axiom,
~ equal(i29,i27),
file('SWV505-1.030.p',unknown),
[] ).
cnf(72,axiom,
~ equal(i30,i26),
file('SWV505-1.030.p',unknown),
[] ).
cnf(73,axiom,
~ equal(i29,i26),
file('SWV505-1.030.p',unknown),
[] ).
cnf(75,axiom,
~ equal(i27,i26),
file('SWV505-1.030.p',unknown),
[] ).
cnf(76,axiom,
~ equal(i30,i25),
file('SWV505-1.030.p',unknown),
[] ).
cnf(77,axiom,
~ equal(i29,i25),
file('SWV505-1.030.p',unknown),
[] ).
cnf(79,axiom,
~ equal(i27,i25),
file('SWV505-1.030.p',unknown),
[] ).
cnf(80,axiom,
~ equal(i26,i25),
file('SWV505-1.030.p',unknown),
[] ).
cnf(81,axiom,
~ equal(i30,i24),
file('SWV505-1.030.p',unknown),
[] ).
cnf(82,axiom,
~ equal(i29,i24),
file('SWV505-1.030.p',unknown),
[] ).
cnf(83,axiom,
~ equal(i28,i24),
file('SWV505-1.030.p',unknown),
[] ).
cnf(84,axiom,
~ equal(i27,i24),
file('SWV505-1.030.p',unknown),
[] ).
cnf(85,axiom,
~ equal(i26,i24),
file('SWV505-1.030.p',unknown),
[] ).
cnf(86,axiom,
~ equal(i25,i24),
file('SWV505-1.030.p',unknown),
[] ).
cnf(87,axiom,
~ equal(i30,i23),
file('SWV505-1.030.p',unknown),
[] ).
cnf(88,axiom,
~ equal(i29,i23),
file('SWV505-1.030.p',unknown),
[] ).
cnf(89,axiom,
~ equal(i28,i23),
file('SWV505-1.030.p',unknown),
[] ).
cnf(90,axiom,
~ equal(i27,i23),
file('SWV505-1.030.p',unknown),
[] ).
cnf(91,axiom,
~ equal(i26,i23),
file('SWV505-1.030.p',unknown),
[] ).
cnf(92,axiom,
~ equal(i25,i23),
file('SWV505-1.030.p',unknown),
[] ).
cnf(93,axiom,
~ equal(i24,i23),
file('SWV505-1.030.p',unknown),
[] ).
cnf(94,axiom,
~ equal(i30,i22),
file('SWV505-1.030.p',unknown),
[] ).
cnf(95,axiom,
~ equal(i29,i22),
file('SWV505-1.030.p',unknown),
[] ).
cnf(98,axiom,
~ equal(i26,i22),
file('SWV505-1.030.p',unknown),
[] ).
cnf(99,axiom,
~ equal(i25,i22),
file('SWV505-1.030.p',unknown),
[] ).
cnf(102,axiom,
~ equal(i30,i21),
file('SWV505-1.030.p',unknown),
[] ).
cnf(103,axiom,
~ equal(i29,i21),
file('SWV505-1.030.p',unknown),
[] ).
cnf(107,axiom,
~ equal(i25,i21),
file('SWV505-1.030.p',unknown),
[] ).
cnf(111,axiom,
~ equal(i30,i20),
file('SWV505-1.030.p',unknown),
[] ).
cnf(116,axiom,
~ equal(i25,i20),
file('SWV505-1.030.p',unknown),
[] ).
cnf(120,axiom,
~ equal(i21,i20),
file('SWV505-1.030.p',unknown),
[] ).
cnf(121,axiom,
~ equal(i30,i19),
file('SWV505-1.030.p',unknown),
[] ).
cnf(126,axiom,
~ equal(i25,i19),
file('SWV505-1.030.p',unknown),
[] ).
cnf(130,axiom,
~ equal(i21,i19),
file('SWV505-1.030.p',unknown),
[] ).
cnf(131,axiom,
~ equal(i20,i19),
file('SWV505-1.030.p',unknown),
[] ).
cnf(132,axiom,
~ equal(i30,i18),
file('SWV505-1.030.p',unknown),
[] ).
cnf(137,axiom,
~ equal(i25,i18),
file('SWV505-1.030.p',unknown),
[] ).
cnf(141,axiom,
~ equal(i21,i18),
file('SWV505-1.030.p',unknown),
[] ).
cnf(142,axiom,
~ equal(i20,i18),
file('SWV505-1.030.p',unknown),
[] ).
cnf(143,axiom,
~ equal(i19,i18),
file('SWV505-1.030.p',unknown),
[] ).
cnf(144,axiom,
~ equal(i30,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(145,axiom,
~ equal(i29,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(146,axiom,
~ equal(i28,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(147,axiom,
~ equal(i27,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(148,axiom,
~ equal(i26,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(149,axiom,
~ equal(i25,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(150,axiom,
~ equal(i24,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(151,axiom,
~ equal(i23,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(152,axiom,
~ equal(i22,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(153,axiom,
~ equal(i21,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(154,axiom,
~ equal(i20,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(155,axiom,
~ equal(i19,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(156,axiom,
~ equal(i18,i17),
file('SWV505-1.030.p',unknown),
[] ).
cnf(157,axiom,
~ equal(i30,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(158,axiom,
~ equal(i29,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(160,axiom,
~ equal(i27,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(161,axiom,
~ equal(i26,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(162,axiom,
~ equal(i25,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(163,axiom,
~ equal(i24,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(164,axiom,
~ equal(i23,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(165,axiom,
~ equal(i22,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(166,axiom,
~ equal(i21,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(167,axiom,
~ equal(i20,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(168,axiom,
~ equal(i19,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(169,axiom,
~ equal(i18,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(170,axiom,
~ equal(i17,i16),
file('SWV505-1.030.p',unknown),
[] ).
cnf(171,axiom,
~ equal(i30,i15),
file('SWV505-1.030.p',unknown),
[] ).
cnf(176,axiom,
~ equal(i25,i15),
file('SWV505-1.030.p',unknown),
[] ).
cnf(180,axiom,
~ equal(i21,i15),
file('SWV505-1.030.p',unknown),
[] ).
cnf(181,axiom,
~ equal(i20,i15),
file('SWV505-1.030.p',unknown),
[] ).
cnf(182,axiom,
~ equal(i19,i15),
file('SWV505-1.030.p',unknown),
[] ).
cnf(183,axiom,
~ equal(i18,i15),
file('SWV505-1.030.p',unknown),
[] ).
cnf(186,axiom,
~ equal(i30,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(191,axiom,
~ equal(i25,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(195,axiom,
~ equal(i21,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(196,axiom,
~ equal(i20,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(197,axiom,
~ equal(i19,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(198,axiom,
~ equal(i18,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(199,axiom,
~ equal(i17,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(200,axiom,
~ equal(i16,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(201,axiom,
~ equal(i15,i14),
file('SWV505-1.030.p',unknown),
[] ).
cnf(202,axiom,
~ equal(i30,i13),
file('SWV505-1.030.p',unknown),
[] ).
cnf(207,axiom,
~ equal(i25,i13),
file('SWV505-1.030.p',unknown),
[] ).
cnf(212,axiom,
~ equal(i20,i13),
file('SWV505-1.030.p',unknown),
[] ).
cnf(213,axiom,
~ equal(i19,i13),
file('SWV505-1.030.p',unknown),
[] ).
cnf(214,axiom,
~ equal(i18,i13),
file('SWV505-1.030.p',unknown),
[] ).
cnf(217,axiom,
~ equal(i15,i13),
file('SWV505-1.030.p',unknown),
[] ).
cnf(219,axiom,
~ equal(i30,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(220,axiom,
~ equal(i29,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(222,axiom,
~ equal(i27,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(223,axiom,
~ equal(i26,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(224,axiom,
~ equal(i25,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(225,axiom,
~ equal(i24,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(226,axiom,
~ equal(i23,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(227,axiom,
~ equal(i22,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(228,axiom,
~ equal(i21,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(229,axiom,
~ equal(i20,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(230,axiom,
~ equal(i19,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(231,axiom,
~ equal(i18,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(232,axiom,
~ equal(i17,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(233,axiom,
~ equal(i16,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(234,axiom,
~ equal(i15,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(235,axiom,
~ equal(i14,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(236,axiom,
~ equal(i13,i12),
file('SWV505-1.030.p',unknown),
[] ).
cnf(237,axiom,
~ equal(i30,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(242,axiom,
~ equal(i25,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(246,axiom,
~ equal(i21,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(247,axiom,
~ equal(i20,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(248,axiom,
~ equal(i19,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(249,axiom,
~ equal(i18,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(252,axiom,
~ equal(i15,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(253,axiom,
~ equal(i14,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(254,axiom,
~ equal(i13,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(255,axiom,
~ equal(i12,i11),
file('SWV505-1.030.p',unknown),
[] ).
cnf(256,axiom,
~ equal(i30,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(257,axiom,
~ equal(i29,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(258,axiom,
~ equal(i28,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(259,axiom,
~ equal(i27,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(260,axiom,
~ equal(i26,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(261,axiom,
~ equal(i25,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(262,axiom,
~ equal(i24,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(263,axiom,
~ equal(i23,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(264,axiom,
~ equal(i22,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(265,axiom,
~ equal(i21,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(266,axiom,
~ equal(i20,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(267,axiom,
~ equal(i19,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(268,axiom,
~ equal(i18,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(269,axiom,
~ equal(i17,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(270,axiom,
~ equal(i16,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(271,axiom,
~ equal(i15,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(272,axiom,
~ equal(i14,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(273,axiom,
~ equal(i13,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(274,axiom,
~ equal(i12,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(275,axiom,
~ equal(i11,i10),
file('SWV505-1.030.p',unknown),
[] ).
cnf(276,axiom,
~ equal(i30,i9),
file('SWV505-1.030.p',unknown),
[] ).
cnf(287,axiom,
~ equal(i19,i9),
file('SWV505-1.030.p',unknown),
[] ).
cnf(293,axiom,
~ equal(i13,i9),
file('SWV505-1.030.p',unknown),
[] ).
cnf(297,axiom,
~ equal(i30,i8),
file('SWV505-1.030.p',unknown),
[] ).
cnf(302,axiom,
~ equal(i25,i8),
file('SWV505-1.030.p',unknown),
[] ).
cnf(307,axiom,
~ equal(i20,i8),
file('SWV505-1.030.p',unknown),
[] ).
cnf(308,axiom,
~ equal(i19,i8),
file('SWV505-1.030.p',unknown),
[] ).
cnf(309,axiom,
~ equal(i18,i8),
file('SWV505-1.030.p',unknown),
[] ).
cnf(312,axiom,
~ equal(i15,i8),
file('SWV505-1.030.p',unknown),
[] ).
cnf(314,axiom,
~ equal(i13,i8),
file('SWV505-1.030.p',unknown),
[] ).
cnf(318,axiom,
~ equal(i9,i8),
file('SWV505-1.030.p',unknown),
[] ).
cnf(319,axiom,
~ equal(i30,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(320,axiom,
~ equal(i29,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(321,axiom,
~ equal(i28,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(322,axiom,
~ equal(i27,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(323,axiom,
~ equal(i26,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(324,axiom,
~ equal(i25,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(325,axiom,
~ equal(i24,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(326,axiom,
~ equal(i23,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(327,axiom,
~ equal(i22,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(328,axiom,
~ equal(i21,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(329,axiom,
~ equal(i20,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(330,axiom,
~ equal(i19,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(331,axiom,
~ equal(i18,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(332,axiom,
~ equal(i17,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(333,axiom,
~ equal(i16,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(334,axiom,
~ equal(i15,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(335,axiom,
~ equal(i14,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(336,axiom,
~ equal(i13,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(337,axiom,
~ equal(i12,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(338,axiom,
~ equal(i11,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(339,axiom,
~ equal(i10,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(340,axiom,
~ equal(i9,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(341,axiom,
~ equal(i8,i7),
file('SWV505-1.030.p',unknown),
[] ).
cnf(342,axiom,
~ equal(i30,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(347,axiom,
~ equal(i25,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(351,axiom,
~ equal(i21,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(352,axiom,
~ equal(i20,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(353,axiom,
~ equal(i19,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(354,axiom,
~ equal(i18,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(357,axiom,
~ equal(i15,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(359,axiom,
~ equal(i13,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(360,axiom,
~ equal(i12,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(361,axiom,
~ equal(i11,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(362,axiom,
~ equal(i10,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(363,axiom,
~ equal(i9,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(364,axiom,
~ equal(i8,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(365,axiom,
~ equal(i7,i6),
file('SWV505-1.030.p',unknown),
[] ).
cnf(366,axiom,
~ equal(i30,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(367,axiom,
~ equal(i29,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(371,axiom,
~ equal(i25,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(375,axiom,
~ equal(i21,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(376,axiom,
~ equal(i20,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(377,axiom,
~ equal(i19,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(378,axiom,
~ equal(i18,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(379,axiom,
~ equal(i17,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(380,axiom,
~ equal(i16,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(381,axiom,
~ equal(i15,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(382,axiom,
~ equal(i14,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(383,axiom,
~ equal(i13,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(384,axiom,
~ equal(i12,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(385,axiom,
~ equal(i11,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(386,axiom,
~ equal(i10,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(387,axiom,
~ equal(i9,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(388,axiom,
~ equal(i8,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(389,axiom,
~ equal(i7,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(390,axiom,
~ equal(i6,i5),
file('SWV505-1.030.p',unknown),
[] ).
cnf(402,axiom,
~ equal(i19,i4),
file('SWV505-1.030.p',unknown),
[] ).
cnf(408,axiom,
~ equal(i13,i4),
file('SWV505-1.030.p',unknown),
[] ).
cnf(417,axiom,
~ equal(i30,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(418,axiom,
~ equal(i29,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(420,axiom,
~ equal(i27,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(421,axiom,
~ equal(i26,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(422,axiom,
~ equal(i25,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(425,axiom,
~ equal(i22,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(426,axiom,
~ equal(i21,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(427,axiom,
~ equal(i20,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(428,axiom,
~ equal(i19,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(429,axiom,
~ equal(i18,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(430,axiom,
~ equal(i17,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(431,axiom,
~ equal(i16,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(432,axiom,
~ equal(i15,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(433,axiom,
~ equal(i14,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(434,axiom,
~ equal(i13,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(435,axiom,
~ equal(i12,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(436,axiom,
~ equal(i11,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(437,axiom,
~ equal(i10,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(438,axiom,
~ equal(i9,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(439,axiom,
~ equal(i8,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(440,axiom,
~ equal(i7,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(441,axiom,
~ equal(i6,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(442,axiom,
~ equal(i5,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(443,axiom,
~ equal(i4,i3),
file('SWV505-1.030.p',unknown),
[] ).
cnf(444,axiom,
~ equal(i30,i2),
file('SWV505-1.030.p',unknown),
[] ).
cnf(455,axiom,
~ equal(i19,i2),
file('SWV505-1.030.p',unknown),
[] ).
cnf(461,axiom,
~ equal(i13,i2),
file('SWV505-1.030.p',unknown),
[] ).
cnf(465,axiom,
~ equal(i9,i2),
file('SWV505-1.030.p',unknown),
[] ).
cnf(468,axiom,
~ equal(i6,i2),
file('SWV505-1.030.p',unknown),
[] ).
cnf(469,axiom,
~ equal(i5,i2),
file('SWV505-1.030.p',unknown),
[] ).
cnf(470,axiom,
~ equal(i4,i2),
file('SWV505-1.030.p',unknown),
[] ).
cnf(471,axiom,
~ equal(i3,i2),
file('SWV505-1.030.p',unknown),
[] ).
cnf(489,axiom,
~ equal(i13,i1),
file('SWV505-1.030.p',unknown),
[] ).
cnf(501,axiom,
~ equal(e_1131,e_1130),
file('SWV505-1.030.p',unknown),
[] ).
cnf(568,plain,
equal(select(a_1128,i10),e10),
inference(spr,[status(thm),theory(equality)],[62,1]),
[iquote('0:SpR:62.0,1.0')] ).
cnf(569,plain,
equal(select(a_1078,i10),e10),
inference(spr,[status(thm),theory(equality)],[12,1]),
[iquote('0:SpR:12.0,1.0')] ).
cnf(570,plain,
equal(select(a_1127,i7),e7),
inference(spr,[status(thm),theory(equality)],[61,1]),
[iquote('0:SpR:61.0,1.0')] ).
cnf(571,plain,
equal(select(a_1075,i7),e7),
inference(spr,[status(thm),theory(equality)],[9,1]),
[iquote('0:SpR:9.0,1.0')] ).
cnf(572,plain,
equal(select(a_1126,i24),e24),
inference(spr,[status(thm),theory(equality)],[60,1]),
[iquote('0:SpR:60.0,1.0')] ).
cnf(573,plain,
equal(select(a_1092,i24),e24),
inference(spr,[status(thm),theory(equality)],[26,1]),
[iquote('0:SpR:26.0,1.0')] ).
cnf(574,plain,
equal(select(a_1125,i23),e23),
inference(spr,[status(thm),theory(equality)],[59,1]),
[iquote('0:SpR:59.0,1.0')] ).
cnf(575,plain,
equal(select(a_1091,i23),e23),
inference(spr,[status(thm),theory(equality)],[25,1]),
[iquote('0:SpR:25.0,1.0')] ).
cnf(576,plain,
equal(select(a_1124,i17),e17),
inference(spr,[status(thm),theory(equality)],[58,1]),
[iquote('0:SpR:58.0,1.0')] ).
cnf(577,plain,
equal(select(a_1085,i17),e17),
inference(spr,[status(thm),theory(equality)],[19,1]),
[iquote('0:SpR:19.0,1.0')] ).
cnf(578,plain,
equal(select(a_1123,i28),e28),
inference(spr,[status(thm),theory(equality)],[57,1]),
[iquote('0:SpR:57.0,1.0')] ).
cnf(579,plain,
equal(select(a_1096,i28),e28),
inference(spr,[status(thm),theory(equality)],[30,1]),
[iquote('0:SpR:30.0,1.0')] ).
cnf(580,plain,
equal(select(a_1122,i16),e16),
inference(spr,[status(thm),theory(equality)],[56,1]),
[iquote('0:SpR:56.0,1.0')] ).
cnf(581,plain,
equal(select(a_1084,i16),e16),
inference(spr,[status(thm),theory(equality)],[18,1]),
[iquote('0:SpR:18.0,1.0')] ).
cnf(582,plain,
equal(select(a_1121,i12),e12),
inference(spr,[status(thm),theory(equality)],[55,1]),
[iquote('0:SpR:55.0,1.0')] ).
cnf(583,plain,
equal(select(a_1080,i12),e12),
inference(spr,[status(thm),theory(equality)],[14,1]),
[iquote('0:SpR:14.0,1.0')] ).
cnf(584,plain,
equal(select(a_1120,i3),e3),
inference(spr,[status(thm),theory(equality)],[54,1]),
[iquote('0:SpR:54.0,1.0')] ).
cnf(585,plain,
equal(select(a_1071,i3),e3),
inference(spr,[status(thm),theory(equality)],[5,1]),
[iquote('0:SpR:5.0,1.0')] ).
cnf(586,plain,
equal(select(a_1119,i27),e27),
inference(spr,[status(thm),theory(equality)],[53,1]),
[iquote('0:SpR:53.0,1.0')] ).
cnf(587,plain,
equal(select(a_1095,i27),e27),
inference(spr,[status(thm),theory(equality)],[29,1]),
[iquote('0:SpR:29.0,1.0')] ).
cnf(588,plain,
equal(select(a_1118,i22),e22),
inference(spr,[status(thm),theory(equality)],[52,1]),
[iquote('0:SpR:52.0,1.0')] ).
cnf(589,plain,
equal(select(a_1090,i22),e22),
inference(spr,[status(thm),theory(equality)],[24,1]),
[iquote('0:SpR:24.0,1.0')] ).
cnf(590,plain,
equal(select(a_1117,i26),e26),
inference(spr,[status(thm),theory(equality)],[51,1]),
[iquote('0:SpR:51.0,1.0')] ).
cnf(591,plain,
equal(select(a_1094,i26),e26),
inference(spr,[status(thm),theory(equality)],[28,1]),
[iquote('0:SpR:28.0,1.0')] ).
cnf(592,plain,
equal(select(a_1116,i5),e5),
inference(spr,[status(thm),theory(equality)],[50,1]),
[iquote('0:SpR:50.0,1.0')] ).
cnf(593,plain,
equal(select(a_1073,i5),e5),
inference(spr,[status(thm),theory(equality)],[7,1]),
[iquote('0:SpR:7.0,1.0')] ).
cnf(594,plain,
equal(select(a_1115,i29),e29),
inference(spr,[status(thm),theory(equality)],[49,1]),
[iquote('0:SpR:49.0,1.0')] ).
cnf(595,plain,
equal(select(a_1097,i29),e29),
inference(spr,[status(thm),theory(equality)],[31,1]),
[iquote('0:SpR:31.0,1.0')] ).
cnf(596,plain,
equal(select(a_1114,i14),e14),
inference(spr,[status(thm),theory(equality)],[48,1]),
[iquote('0:SpR:48.0,1.0')] ).
cnf(597,plain,
equal(select(a_1082,i14),e14),
inference(spr,[status(thm),theory(equality)],[16,1]),
[iquote('0:SpR:16.0,1.0')] ).
cnf(598,plain,
equal(select(a_1113,i11),e11),
inference(spr,[status(thm),theory(equality)],[47,1]),
[iquote('0:SpR:47.0,1.0')] ).
cnf(599,plain,
equal(select(a_1079,i11),e11),
inference(spr,[status(thm),theory(equality)],[13,1]),
[iquote('0:SpR:13.0,1.0')] ).
cnf(600,plain,
equal(select(a_1112,i6),e6),
inference(spr,[status(thm),theory(equality)],[46,1]),
[iquote('0:SpR:46.0,1.0')] ).
cnf(601,plain,
equal(select(a_1074,i6),e6),
inference(spr,[status(thm),theory(equality)],[8,1]),
[iquote('0:SpR:8.0,1.0')] ).
cnf(602,plain,
equal(select(a_1111,i21),e21),
inference(spr,[status(thm),theory(equality)],[45,1]),
[iquote('0:SpR:45.0,1.0')] ).
cnf(603,plain,
equal(select(a_1089,i21),e21),
inference(spr,[status(thm),theory(equality)],[23,1]),
[iquote('0:SpR:23.0,1.0')] ).
cnf(604,plain,
equal(select(a_1110,i8),e8),
inference(spr,[status(thm),theory(equality)],[44,1]),
[iquote('0:SpR:44.0,1.0')] ).
cnf(605,plain,
equal(select(a_1076,i8),e8),
inference(spr,[status(thm),theory(equality)],[10,1]),
[iquote('0:SpR:10.0,1.0')] ).
cnf(606,plain,
equal(select(a_1109,i20),e20),
inference(spr,[status(thm),theory(equality)],[43,1]),
[iquote('0:SpR:43.0,1.0')] ).
cnf(607,plain,
equal(select(a_1088,i20),e20),
inference(spr,[status(thm),theory(equality)],[22,1]),
[iquote('0:SpR:22.0,1.0')] ).
cnf(608,plain,
equal(select(a_1108,i18),e18),
inference(spr,[status(thm),theory(equality)],[42,1]),
[iquote('0:SpR:42.0,1.0')] ).
cnf(609,plain,
equal(select(a_1086,i18),e18),
inference(spr,[status(thm),theory(equality)],[20,1]),
[iquote('0:SpR:20.0,1.0')] ).
cnf(610,plain,
equal(select(a_1107,i25),e25),
inference(spr,[status(thm),theory(equality)],[41,1]),
[iquote('0:SpR:41.0,1.0')] ).
cnf(611,plain,
equal(select(a_1093,i25),e25),
inference(spr,[status(thm),theory(equality)],[27,1]),
[iquote('0:SpR:27.0,1.0')] ).
cnf(612,plain,
equal(select(a_1106,i15),e15),
inference(spr,[status(thm),theory(equality)],[40,1]),
[iquote('0:SpR:40.0,1.0')] ).
cnf(613,plain,
equal(select(a_1083,i15),e15),
inference(spr,[status(thm),theory(equality)],[17,1]),
[iquote('0:SpR:17.0,1.0')] ).
cnf(614,plain,
equal(select(a_1105,i2),e2),
inference(spr,[status(thm),theory(equality)],[39,1]),
[iquote('0:SpR:39.0,1.0')] ).
cnf(615,plain,
equal(select(a_1070,i2),e2),
inference(spr,[status(thm),theory(equality)],[4,1]),
[iquote('0:SpR:4.0,1.0')] ).
cnf(616,plain,
equal(select(a_1104,i30),e30),
inference(spr,[status(thm),theory(equality)],[38,1]),
[iquote('0:SpR:38.0,1.0')] ).
cnf(617,plain,
equal(select(a_1098,i30),e30),
inference(spr,[status(thm),theory(equality)],[32,1]),
[iquote('0:SpR:32.0,1.0')] ).
cnf(618,plain,
equal(select(a_1103,i9),e9),
inference(spr,[status(thm),theory(equality)],[37,1]),
[iquote('0:SpR:37.0,1.0')] ).
cnf(619,plain,
equal(select(a_1077,i9),e9),
inference(spr,[status(thm),theory(equality)],[11,1]),
[iquote('0:SpR:11.0,1.0')] ).
cnf(620,plain,
equal(select(a_1102,i4),e4),
inference(spr,[status(thm),theory(equality)],[36,1]),
[iquote('0:SpR:36.0,1.0')] ).
cnf(621,plain,
equal(select(a_1072,i4),e4),
inference(spr,[status(thm),theory(equality)],[6,1]),
[iquote('0:SpR:6.0,1.0')] ).
cnf(622,plain,
equal(select(a_1101,i19),e19),
inference(spr,[status(thm),theory(equality)],[35,1]),
[iquote('0:SpR:35.0,1.0')] ).
cnf(623,plain,
equal(select(a_1087,i19),e19),
inference(spr,[status(thm),theory(equality)],[21,1]),
[iquote('0:SpR:21.0,1.0')] ).
cnf(624,plain,
equal(select(a_1100,i1),e1),
inference(spr,[status(thm),theory(equality)],[34,1]),
[iquote('0:SpR:34.0,1.0')] ).
cnf(625,plain,
equal(select(a_1069,i1),e1),
inference(spr,[status(thm),theory(equality)],[3,1]),
[iquote('0:SpR:3.0,1.0')] ).
cnf(626,plain,
equal(select(a_1099,i13),e13),
inference(spr,[status(thm),theory(equality)],[33,1]),
[iquote('0:SpR:33.0,1.0')] ).
cnf(627,plain,
equal(select(a_1081,i13),e13),
inference(spr,[status(thm),theory(equality)],[15,1]),
[iquote('0:SpR:15.0,1.0')] ).
cnf(634,plain,
( equal(i10,u)
| equal(select(a_1128,u),select(a_1127,u)) ),
inference(spr,[status(thm),theory(equality)],[62,2]),
[iquote('0:SpR:62.0,2.1')] ).
cnf(635,plain,
( equal(i10,u)
| equal(select(a_1078,u),select(a_1077,u)) ),
inference(spr,[status(thm),theory(equality)],[12,2]),
[iquote('0:SpR:12.0,2.1')] ).
cnf(636,plain,
( equal(i7,u)
| equal(select(a_1127,u),select(a_1126,u)) ),
inference(spr,[status(thm),theory(equality)],[61,2]),
[iquote('0:SpR:61.0,2.1')] ).
cnf(637,plain,
( equal(i7,u)
| equal(select(a_1075,u),select(a_1074,u)) ),
inference(spr,[status(thm),theory(equality)],[9,2]),
[iquote('0:SpR:9.0,2.1')] ).
cnf(638,plain,
( equal(i24,u)
| equal(select(a_1126,u),select(a_1125,u)) ),
inference(spr,[status(thm),theory(equality)],[60,2]),
[iquote('0:SpR:60.0,2.1')] ).
cnf(639,plain,
( equal(i24,u)
| equal(select(a_1092,u),select(a_1091,u)) ),
inference(spr,[status(thm),theory(equality)],[26,2]),
[iquote('0:SpR:26.0,2.1')] ).
cnf(640,plain,
( equal(i23,u)
| equal(select(a_1125,u),select(a_1124,u)) ),
inference(spr,[status(thm),theory(equality)],[59,2]),
[iquote('0:SpR:59.0,2.1')] ).
cnf(641,plain,
( equal(i23,u)
| equal(select(a_1091,u),select(a_1090,u)) ),
inference(spr,[status(thm),theory(equality)],[25,2]),
[iquote('0:SpR:25.0,2.1')] ).
cnf(642,plain,
( equal(i17,u)
| equal(select(a_1124,u),select(a_1123,u)) ),
inference(spr,[status(thm),theory(equality)],[58,2]),
[iquote('0:SpR:58.0,2.1')] ).
cnf(643,plain,
( equal(i17,u)
| equal(select(a_1085,u),select(a_1084,u)) ),
inference(spr,[status(thm),theory(equality)],[19,2]),
[iquote('0:SpR:19.0,2.1')] ).
cnf(644,plain,
( equal(i28,u)
| equal(select(a_1123,u),select(a_1122,u)) ),
inference(spr,[status(thm),theory(equality)],[57,2]),
[iquote('0:SpR:57.0,2.1')] ).
cnf(645,plain,
( equal(i28,u)
| equal(select(a_1096,u),select(a_1095,u)) ),
inference(spr,[status(thm),theory(equality)],[30,2]),
[iquote('0:SpR:30.0,2.1')] ).
cnf(646,plain,
( equal(i16,u)
| equal(select(a_1122,u),select(a_1121,u)) ),
inference(spr,[status(thm),theory(equality)],[56,2]),
[iquote('0:SpR:56.0,2.1')] ).
cnf(647,plain,
( equal(i16,u)
| equal(select(a_1084,u),select(a_1083,u)) ),
inference(spr,[status(thm),theory(equality)],[18,2]),
[iquote('0:SpR:18.0,2.1')] ).
cnf(648,plain,
( equal(i12,u)
| equal(select(a_1121,u),select(a_1120,u)) ),
inference(spr,[status(thm),theory(equality)],[55,2]),
[iquote('0:SpR:55.0,2.1')] ).
cnf(649,plain,
( equal(i12,u)
| equal(select(a_1080,u),select(a_1079,u)) ),
inference(spr,[status(thm),theory(equality)],[14,2]),
[iquote('0:SpR:14.0,2.1')] ).
cnf(650,plain,
( equal(i3,u)
| equal(select(a_1120,u),select(a_1119,u)) ),
inference(spr,[status(thm),theory(equality)],[54,2]),
[iquote('0:SpR:54.0,2.1')] ).
cnf(651,plain,
( equal(i3,u)
| equal(select(a_1071,u),select(a_1070,u)) ),
inference(spr,[status(thm),theory(equality)],[5,2]),
[iquote('0:SpR:5.0,2.1')] ).
cnf(652,plain,
( equal(i27,u)
| equal(select(a_1119,u),select(a_1118,u)) ),
inference(spr,[status(thm),theory(equality)],[53,2]),
[iquote('0:SpR:53.0,2.1')] ).
cnf(653,plain,
( equal(i27,u)
| equal(select(a_1095,u),select(a_1094,u)) ),
inference(spr,[status(thm),theory(equality)],[29,2]),
[iquote('0:SpR:29.0,2.1')] ).
cnf(654,plain,
( equal(i22,u)
| equal(select(a_1118,u),select(a_1117,u)) ),
inference(spr,[status(thm),theory(equality)],[52,2]),
[iquote('0:SpR:52.0,2.1')] ).
cnf(655,plain,
( equal(i22,u)
| equal(select(a_1090,u),select(a_1089,u)) ),
inference(spr,[status(thm),theory(equality)],[24,2]),
[iquote('0:SpR:24.0,2.1')] ).
cnf(656,plain,
( equal(i26,u)
| equal(select(a_1117,u),select(a_1116,u)) ),
inference(spr,[status(thm),theory(equality)],[51,2]),
[iquote('0:SpR:51.0,2.1')] ).
cnf(657,plain,
( equal(i26,u)
| equal(select(a_1094,u),select(a_1093,u)) ),
inference(spr,[status(thm),theory(equality)],[28,2]),
[iquote('0:SpR:28.0,2.1')] ).
cnf(658,plain,
( equal(i5,u)
| equal(select(a_1116,u),select(a_1115,u)) ),
inference(spr,[status(thm),theory(equality)],[50,2]),
[iquote('0:SpR:50.0,2.1')] ).
cnf(659,plain,
( equal(i5,u)
| equal(select(a_1073,u),select(a_1072,u)) ),
inference(spr,[status(thm),theory(equality)],[7,2]),
[iquote('0:SpR:7.0,2.1')] ).
cnf(660,plain,
( equal(i29,u)
| equal(select(a_1115,u),select(a_1114,u)) ),
inference(spr,[status(thm),theory(equality)],[49,2]),
[iquote('0:SpR:49.0,2.1')] ).
cnf(661,plain,
( equal(i29,u)
| equal(select(a_1097,u),select(a_1096,u)) ),
inference(spr,[status(thm),theory(equality)],[31,2]),
[iquote('0:SpR:31.0,2.1')] ).
cnf(662,plain,
( equal(i14,u)
| equal(select(a_1114,u),select(a_1113,u)) ),
inference(spr,[status(thm),theory(equality)],[48,2]),
[iquote('0:SpR:48.0,2.1')] ).
cnf(663,plain,
( equal(i14,u)
| equal(select(a_1082,u),select(a_1081,u)) ),
inference(spr,[status(thm),theory(equality)],[16,2]),
[iquote('0:SpR:16.0,2.1')] ).
cnf(664,plain,
( equal(i11,u)
| equal(select(a_1113,u),select(a_1112,u)) ),
inference(spr,[status(thm),theory(equality)],[47,2]),
[iquote('0:SpR:47.0,2.1')] ).
cnf(665,plain,
( equal(i11,u)
| equal(select(a_1079,u),select(a_1078,u)) ),
inference(spr,[status(thm),theory(equality)],[13,2]),
[iquote('0:SpR:13.0,2.1')] ).
cnf(666,plain,
( equal(i6,u)
| equal(select(a_1112,u),select(a_1111,u)) ),
inference(spr,[status(thm),theory(equality)],[46,2]),
[iquote('0:SpR:46.0,2.1')] ).
cnf(667,plain,
( equal(i6,u)
| equal(select(a_1074,u),select(a_1073,u)) ),
inference(spr,[status(thm),theory(equality)],[8,2]),
[iquote('0:SpR:8.0,2.1')] ).
cnf(668,plain,
( equal(i21,u)
| equal(select(a_1111,u),select(a_1110,u)) ),
inference(spr,[status(thm),theory(equality)],[45,2]),
[iquote('0:SpR:45.0,2.1')] ).
cnf(669,plain,
( equal(i21,u)
| equal(select(a_1089,u),select(a_1088,u)) ),
inference(spr,[status(thm),theory(equality)],[23,2]),
[iquote('0:SpR:23.0,2.1')] ).
cnf(670,plain,
( equal(i8,u)
| equal(select(a_1110,u),select(a_1109,u)) ),
inference(spr,[status(thm),theory(equality)],[44,2]),
[iquote('0:SpR:44.0,2.1')] ).
cnf(671,plain,
( equal(i8,u)
| equal(select(a_1076,u),select(a_1075,u)) ),
inference(spr,[status(thm),theory(equality)],[10,2]),
[iquote('0:SpR:10.0,2.1')] ).
cnf(672,plain,
( equal(i20,u)
| equal(select(a_1109,u),select(a_1108,u)) ),
inference(spr,[status(thm),theory(equality)],[43,2]),
[iquote('0:SpR:43.0,2.1')] ).
cnf(673,plain,
( equal(i20,u)
| equal(select(a_1088,u),select(a_1087,u)) ),
inference(spr,[status(thm),theory(equality)],[22,2]),
[iquote('0:SpR:22.0,2.1')] ).
cnf(674,plain,
( equal(i18,u)
| equal(select(a_1108,u),select(a_1107,u)) ),
inference(spr,[status(thm),theory(equality)],[42,2]),
[iquote('0:SpR:42.0,2.1')] ).
cnf(675,plain,
( equal(i18,u)
| equal(select(a_1086,u),select(a_1085,u)) ),
inference(spr,[status(thm),theory(equality)],[20,2]),
[iquote('0:SpR:20.0,2.1')] ).
cnf(676,plain,
( equal(i25,u)
| equal(select(a_1107,u),select(a_1106,u)) ),
inference(spr,[status(thm),theory(equality)],[41,2]),
[iquote('0:SpR:41.0,2.1')] ).
cnf(677,plain,
( equal(i25,u)
| equal(select(a_1093,u),select(a_1092,u)) ),
inference(spr,[status(thm),theory(equality)],[27,2]),
[iquote('0:SpR:27.0,2.1')] ).
cnf(678,plain,
( equal(i15,u)
| equal(select(a_1106,u),select(a_1105,u)) ),
inference(spr,[status(thm),theory(equality)],[40,2]),
[iquote('0:SpR:40.0,2.1')] ).
cnf(679,plain,
( equal(i15,u)
| equal(select(a_1083,u),select(a_1082,u)) ),
inference(spr,[status(thm),theory(equality)],[17,2]),
[iquote('0:SpR:17.0,2.1')] ).
cnf(680,plain,
( equal(i2,u)
| equal(select(a_1105,u),select(a_1104,u)) ),
inference(spr,[status(thm),theory(equality)],[39,2]),
[iquote('0:SpR:39.0,2.1')] ).
cnf(681,plain,
( equal(i2,u)
| equal(select(a_1070,u),select(a_1069,u)) ),
inference(spr,[status(thm),theory(equality)],[4,2]),
[iquote('0:SpR:4.0,2.1')] ).
cnf(682,plain,
( equal(i30,u)
| equal(select(a_1104,u),select(a_1103,u)) ),
inference(spr,[status(thm),theory(equality)],[38,2]),
[iquote('0:SpR:38.0,2.1')] ).
cnf(683,plain,
( equal(i30,u)
| equal(select(a_1098,u),select(a_1097,u)) ),
inference(spr,[status(thm),theory(equality)],[32,2]),
[iquote('0:SpR:32.0,2.1')] ).
cnf(684,plain,
( equal(i9,u)
| equal(select(a_1103,u),select(a_1102,u)) ),
inference(spr,[status(thm),theory(equality)],[37,2]),
[iquote('0:SpR:37.0,2.1')] ).
cnf(685,plain,
( equal(i9,u)
| equal(select(a_1077,u),select(a_1076,u)) ),
inference(spr,[status(thm),theory(equality)],[11,2]),
[iquote('0:SpR:11.0,2.1')] ).
cnf(686,plain,
( equal(i4,u)
| equal(select(a_1102,u),select(a_1101,u)) ),
inference(spr,[status(thm),theory(equality)],[36,2]),
[iquote('0:SpR:36.0,2.1')] ).
cnf(687,plain,
( equal(i4,u)
| equal(select(a_1072,u),select(a_1071,u)) ),
inference(spr,[status(thm),theory(equality)],[6,2]),
[iquote('0:SpR:6.0,2.1')] ).
cnf(688,plain,
( equal(i19,u)
| equal(select(a_1101,u),select(a_1100,u)) ),
inference(spr,[status(thm),theory(equality)],[35,2]),
[iquote('0:SpR:35.0,2.1')] ).
cnf(689,plain,
( equal(i19,u)
| equal(select(a_1087,u),select(a_1086,u)) ),
inference(spr,[status(thm),theory(equality)],[21,2]),
[iquote('0:SpR:21.0,2.1')] ).
cnf(690,plain,
( equal(i1,u)
| equal(select(a_1100,u),select(a_1099,u)) ),
inference(spr,[status(thm),theory(equality)],[34,2]),
[iquote('0:SpR:34.0,2.1')] ).
cnf(691,plain,
( equal(i1,u)
| equal(select(a1,u),select(a_1069,u)) ),
inference(spr,[status(thm),theory(equality)],[3,2]),
[iquote('0:SpR:3.0,2.1')] ).
cnf(692,plain,
( equal(i13,u)
| equal(select(a_1099,u),select(a1,u)) ),
inference(spr,[status(thm),theory(equality)],[33,2]),
[iquote('0:SpR:33.0,2.1')] ).
cnf(693,plain,
( equal(i13,u)
| equal(select(a_1081,u),select(a_1080,u)) ),
inference(spr,[status(thm),theory(equality)],[15,2]),
[iquote('0:SpR:15.0,2.1')] ).
cnf(754,plain,
( equal(i_1129,i10)
| equal(select(a_1127,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[634,64]),
[iquote('0:SpR:634.1,64.0')] ).
cnf(759,plain,
equal(i_1129,i10),
inference(spt,[spt(split,[position(s1)])],[754]),
[iquote('1:Spt:754.0')] ).
cnf(761,plain,
equal(select(a_1128,i10),e_1131),
inference(rew,[status(thm),theory(equality)],[759,64]),
[iquote('1:Rew:759.0,64.0')] ).
cnf(762,plain,
equal(select(a_1098,i10),e_1130),
inference(rew,[status(thm),theory(equality)],[759,63]),
[iquote('1:Rew:759.0,63.0')] ).
cnf(763,plain,
equal(e_1131,e10),
inference(rew,[status(thm),theory(equality)],[568,761]),
[iquote('1:Rew:568.0,761.0')] ).
cnf(764,plain,
~ equal(e_1130,e10),
inference(rew,[status(thm),theory(equality)],[763,501]),
[iquote('1:Rew:763.0,501.0')] ).
cnf(865,plain,
( equal(i30,i10)
| equal(select(a_1097,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[683,762]),
[iquote('1:SpR:683.1,762.0')] ).
cnf(868,plain,
equal(select(a_1097,i10),e_1130),
inference(mrr,[status(thm)],[865,256]),
[iquote('1:MRR:865.0,256.0')] ).
cnf(870,plain,
( equal(i29,i10)
| equal(select(a_1096,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[868,661]),
[iquote('1:SpR:868.0,661.1')] ).
cnf(871,plain,
equal(select(a_1096,i10),e_1130),
inference(mrr,[status(thm)],[870,257]),
[iquote('1:MRR:870.0,257.0')] ).
cnf(875,plain,
( equal(i28,i10)
| equal(select(a_1095,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[871,645]),
[iquote('1:SpR:871.0,645.1')] ).
cnf(876,plain,
equal(select(a_1095,i10),e_1130),
inference(mrr,[status(thm)],[875,258]),
[iquote('1:MRR:875.0,258.0')] ).
cnf(878,plain,
( equal(i27,i10)
| equal(select(a_1094,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[876,653]),
[iquote('1:SpR:876.0,653.1')] ).
cnf(879,plain,
equal(select(a_1094,i10),e_1130),
inference(mrr,[status(thm)],[878,259]),
[iquote('1:MRR:878.0,259.0')] ).
cnf(881,plain,
( equal(i26,i10)
| equal(select(a_1093,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[879,657]),
[iquote('1:SpR:879.0,657.1')] ).
cnf(882,plain,
equal(select(a_1093,i10),e_1130),
inference(mrr,[status(thm)],[881,260]),
[iquote('1:MRR:881.0,260.0')] ).
cnf(884,plain,
( equal(i25,i10)
| equal(select(a_1092,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[882,677]),
[iquote('1:SpR:882.0,677.1')] ).
cnf(885,plain,
equal(select(a_1092,i10),e_1130),
inference(mrr,[status(thm)],[884,261]),
[iquote('1:MRR:884.0,261.0')] ).
cnf(889,plain,
( equal(i24,i10)
| equal(select(a_1091,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[885,639]),
[iquote('1:SpR:885.0,639.1')] ).
cnf(890,plain,
equal(select(a_1091,i10),e_1130),
inference(mrr,[status(thm)],[889,262]),
[iquote('1:MRR:889.0,262.0')] ).
cnf(892,plain,
( equal(i23,i10)
| equal(select(a_1090,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[890,641]),
[iquote('1:SpR:890.0,641.1')] ).
cnf(893,plain,
equal(select(a_1090,i10),e_1130),
inference(mrr,[status(thm)],[892,263]),
[iquote('1:MRR:892.0,263.0')] ).
cnf(895,plain,
( equal(i22,i10)
| equal(select(a_1089,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[893,655]),
[iquote('1:SpR:893.0,655.1')] ).
cnf(896,plain,
equal(select(a_1089,i10),e_1130),
inference(mrr,[status(thm)],[895,264]),
[iquote('1:MRR:895.0,264.0')] ).
cnf(898,plain,
( equal(i21,i10)
| equal(select(a_1088,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[896,669]),
[iquote('1:SpR:896.0,669.1')] ).
cnf(899,plain,
equal(select(a_1088,i10),e_1130),
inference(mrr,[status(thm)],[898,265]),
[iquote('1:MRR:898.0,265.0')] ).
cnf(903,plain,
( equal(i20,i10)
| equal(select(a_1087,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[899,673]),
[iquote('1:SpR:899.0,673.1')] ).
cnf(904,plain,
equal(select(a_1087,i10),e_1130),
inference(mrr,[status(thm)],[903,266]),
[iquote('1:MRR:903.0,266.0')] ).
cnf(910,plain,
( equal(i19,i10)
| equal(select(a_1086,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[689,904]),
[iquote('1:SpR:689.1,904.0')] ).
cnf(913,plain,
equal(select(a_1086,i10),e_1130),
inference(mrr,[status(thm)],[910,267]),
[iquote('1:MRR:910.0,267.0')] ).
cnf(915,plain,
( equal(i18,i10)
| equal(select(a_1085,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[913,675]),
[iquote('1:SpR:913.0,675.1')] ).
cnf(916,plain,
equal(select(a_1085,i10),e_1130),
inference(mrr,[status(thm)],[915,268]),
[iquote('1:MRR:915.0,268.0')] ).
cnf(918,plain,
( equal(i17,i10)
| equal(select(a_1084,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[916,643]),
[iquote('1:SpR:916.0,643.1')] ).
cnf(919,plain,
equal(select(a_1084,i10),e_1130),
inference(mrr,[status(thm)],[918,269]),
[iquote('1:MRR:918.0,269.0')] ).
cnf(921,plain,
( equal(i16,i10)
| equal(select(a_1083,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[919,647]),
[iquote('1:SpR:919.0,647.1')] ).
cnf(922,plain,
equal(select(a_1083,i10),e_1130),
inference(mrr,[status(thm)],[921,270]),
[iquote('1:MRR:921.0,270.0')] ).
cnf(924,plain,
( equal(i15,i10)
| equal(select(a_1082,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[922,679]),
[iquote('1:SpR:922.0,679.1')] ).
cnf(925,plain,
equal(select(a_1082,i10),e_1130),
inference(mrr,[status(thm)],[924,271]),
[iquote('1:MRR:924.0,271.0')] ).
cnf(929,plain,
( equal(i14,i10)
| equal(select(a_1081,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[925,663]),
[iquote('1:SpR:925.0,663.1')] ).
cnf(930,plain,
equal(select(a_1081,i10),e_1130),
inference(mrr,[status(thm)],[929,272]),
[iquote('1:MRR:929.0,272.0')] ).
cnf(935,plain,
( equal(i13,i10)
| equal(select(a_1080,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[693,930]),
[iquote('1:SpR:693.1,930.0')] ).
cnf(938,plain,
equal(select(a_1080,i10),e_1130),
inference(mrr,[status(thm)],[935,273]),
[iquote('1:MRR:935.0,273.0')] ).
cnf(940,plain,
( equal(i12,i10)
| equal(select(a_1079,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[938,649]),
[iquote('1:SpR:938.0,649.1')] ).
cnf(941,plain,
equal(select(a_1079,i10),e_1130),
inference(mrr,[status(thm)],[940,274]),
[iquote('1:MRR:940.0,274.0')] ).
cnf(943,plain,
( equal(i11,i10)
| equal(select(a_1078,i10),e_1130) ),
inference(spr,[status(thm),theory(equality)],[941,665]),
[iquote('1:SpR:941.0,665.1')] ).
cnf(944,plain,
( equal(i11,i10)
| equal(e_1130,e10) ),
inference(rew,[status(thm),theory(equality)],[569,943]),
[iquote('1:Rew:569.0,943.1')] ).
cnf(945,plain,
$false,
inference(mrr,[status(thm)],[944,275,764]),
[iquote('1:MRR:944.0,944.1,275.0,764.0')] ).
cnf(946,plain,
~ equal(i_1129,i10),
inference(spt,[spt(split,[position(sa)])],[945,759]),
[iquote('1:Spt:945.0,754.0,759.0')] ).
cnf(947,plain,
equal(select(a_1127,i_1129),e_1131),
inference(spt,[spt(split,[position(s2)])],[754]),
[iquote('1:Spt:945.0,754.1')] ).
cnf(948,plain,
( equal(i_1129,i7)
| equal(select(a_1126,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[947,636]),
[iquote('1:SpR:947.0,636.1')] ).
cnf(950,plain,
( equal(i_1129,i30)
| equal(select(a_1097,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[63,683]),
[iquote('0:SpR:63.0,683.1')] ).
cnf(955,plain,
equal(i_1129,i7),
inference(spt,[spt(split,[position(s2s1)])],[948]),
[iquote('2:Spt:948.0')] ).
cnf(956,plain,
equal(select(a_1127,i7),e_1131),
inference(rew,[status(thm),theory(equality)],[955,947]),
[iquote('2:Rew:955.0,947.0')] ).
cnf(961,plain,
( equal(i30,i7)
| equal(select(a_1097,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[955,950]),
[iquote('2:Rew:955.0,950.0')] ).
cnf(962,plain,
equal(e_1131,e7),
inference(rew,[status(thm),theory(equality)],[570,956]),
[iquote('2:Rew:570.0,956.0')] ).
cnf(963,plain,
~ equal(e_1130,e7),
inference(rew,[status(thm),theory(equality)],[962,501]),
[iquote('2:Rew:962.0,501.0')] ).
cnf(967,plain,
( equal(i30,i7)
| equal(select(a_1097,i7),e_1130) ),
inference(rew,[status(thm),theory(equality)],[955,961]),
[iquote('2:Rew:955.0,961.1')] ).
cnf(968,plain,
equal(select(a_1097,i7),e_1130),
inference(mrr,[status(thm)],[967,319]),
[iquote('2:MRR:967.0,319.0')] ).
cnf(977,plain,
( equal(i29,i7)
| equal(select(a_1096,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[968,661]),
[iquote('2:SpR:968.0,661.1')] ).
cnf(978,plain,
equal(select(a_1096,i7),e_1130),
inference(mrr,[status(thm)],[977,320]),
[iquote('2:MRR:977.0,320.0')] ).
cnf(982,plain,
( equal(i28,i7)
| equal(select(a_1095,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[978,645]),
[iquote('2:SpR:978.0,645.1')] ).
cnf(983,plain,
equal(select(a_1095,i7),e_1130),
inference(mrr,[status(thm)],[982,321]),
[iquote('2:MRR:982.0,321.0')] ).
cnf(985,plain,
( equal(i27,i7)
| equal(select(a_1094,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[983,653]),
[iquote('2:SpR:983.0,653.1')] ).
cnf(986,plain,
equal(select(a_1094,i7),e_1130),
inference(mrr,[status(thm)],[985,322]),
[iquote('2:MRR:985.0,322.0')] ).
cnf(988,plain,
( equal(i26,i7)
| equal(select(a_1093,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[986,657]),
[iquote('2:SpR:986.0,657.1')] ).
cnf(989,plain,
equal(select(a_1093,i7),e_1130),
inference(mrr,[status(thm)],[988,323]),
[iquote('2:MRR:988.0,323.0')] ).
cnf(991,plain,
( equal(i25,i7)
| equal(select(a_1092,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[989,677]),
[iquote('2:SpR:989.0,677.1')] ).
cnf(992,plain,
equal(select(a_1092,i7),e_1130),
inference(mrr,[status(thm)],[991,324]),
[iquote('2:MRR:991.0,324.0')] ).
cnf(996,plain,
( equal(i24,i7)
| equal(select(a_1091,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[992,639]),
[iquote('2:SpR:992.0,639.1')] ).
cnf(997,plain,
equal(select(a_1091,i7),e_1130),
inference(mrr,[status(thm)],[996,325]),
[iquote('2:MRR:996.0,325.0')] ).
cnf(999,plain,
( equal(i23,i7)
| equal(select(a_1090,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[997,641]),
[iquote('2:SpR:997.0,641.1')] ).
cnf(1000,plain,
equal(select(a_1090,i7),e_1130),
inference(mrr,[status(thm)],[999,326]),
[iquote('2:MRR:999.0,326.0')] ).
cnf(1002,plain,
( equal(i22,i7)
| equal(select(a_1089,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1000,655]),
[iquote('2:SpR:1000.0,655.1')] ).
cnf(1003,plain,
equal(select(a_1089,i7),e_1130),
inference(mrr,[status(thm)],[1002,327]),
[iquote('2:MRR:1002.0,327.0')] ).
cnf(1005,plain,
( equal(i21,i7)
| equal(select(a_1088,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1003,669]),
[iquote('2:SpR:1003.0,669.1')] ).
cnf(1006,plain,
equal(select(a_1088,i7),e_1130),
inference(mrr,[status(thm)],[1005,328]),
[iquote('2:MRR:1005.0,328.0')] ).
cnf(1008,plain,
( equal(i20,i7)
| equal(select(a_1087,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1006,673]),
[iquote('2:SpR:1006.0,673.1')] ).
cnf(1009,plain,
equal(select(a_1087,i7),e_1130),
inference(mrr,[status(thm)],[1008,329]),
[iquote('2:MRR:1008.0,329.0')] ).
cnf(1011,plain,
( equal(i19,i7)
| equal(select(a_1086,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1009,689]),
[iquote('2:SpR:1009.0,689.1')] ).
cnf(1012,plain,
equal(select(a_1086,i7),e_1130),
inference(mrr,[status(thm)],[1011,330]),
[iquote('2:MRR:1011.0,330.0')] ).
cnf(1014,plain,
( equal(i18,i7)
| equal(select(a_1085,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1012,675]),
[iquote('2:SpR:1012.0,675.1')] ).
cnf(1015,plain,
equal(select(a_1085,i7),e_1130),
inference(mrr,[status(thm)],[1014,331]),
[iquote('2:MRR:1014.0,331.0')] ).
cnf(1017,plain,
( equal(i17,i7)
| equal(select(a_1084,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1015,643]),
[iquote('2:SpR:1015.0,643.1')] ).
cnf(1018,plain,
equal(select(a_1084,i7),e_1130),
inference(mrr,[status(thm)],[1017,332]),
[iquote('2:MRR:1017.0,332.0')] ).
cnf(1020,plain,
( equal(i16,i7)
| equal(select(a_1083,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1018,647]),
[iquote('2:SpR:1018.0,647.1')] ).
cnf(1021,plain,
equal(select(a_1083,i7),e_1130),
inference(mrr,[status(thm)],[1020,333]),
[iquote('2:MRR:1020.0,333.0')] ).
cnf(1023,plain,
( equal(i15,i7)
| equal(select(a_1082,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1021,679]),
[iquote('2:SpR:1021.0,679.1')] ).
cnf(1024,plain,
equal(select(a_1082,i7),e_1130),
inference(mrr,[status(thm)],[1023,334]),
[iquote('2:MRR:1023.0,334.0')] ).
cnf(1026,plain,
( equal(i14,i7)
| equal(select(a_1081,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1024,663]),
[iquote('2:SpR:1024.0,663.1')] ).
cnf(1027,plain,
equal(select(a_1081,i7),e_1130),
inference(mrr,[status(thm)],[1026,335]),
[iquote('2:MRR:1026.0,335.0')] ).
cnf(1029,plain,
( equal(i13,i7)
| equal(select(a_1080,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1027,693]),
[iquote('2:SpR:1027.0,693.1')] ).
cnf(1030,plain,
equal(select(a_1080,i7),e_1130),
inference(mrr,[status(thm)],[1029,336]),
[iquote('2:MRR:1029.0,336.0')] ).
cnf(1032,plain,
( equal(i12,i7)
| equal(select(a_1079,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1030,649]),
[iquote('2:SpR:1030.0,649.1')] ).
cnf(1033,plain,
equal(select(a_1079,i7),e_1130),
inference(mrr,[status(thm)],[1032,337]),
[iquote('2:MRR:1032.0,337.0')] ).
cnf(1035,plain,
( equal(i11,i7)
| equal(select(a_1078,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1033,665]),
[iquote('2:SpR:1033.0,665.1')] ).
cnf(1036,plain,
equal(select(a_1078,i7),e_1130),
inference(mrr,[status(thm)],[1035,338]),
[iquote('2:MRR:1035.0,338.0')] ).
cnf(1038,plain,
( equal(i10,i7)
| equal(select(a_1077,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1036,635]),
[iquote('2:SpR:1036.0,635.1')] ).
cnf(1039,plain,
equal(select(a_1077,i7),e_1130),
inference(mrr,[status(thm)],[1038,339]),
[iquote('2:MRR:1038.0,339.0')] ).
cnf(1041,plain,
( equal(i9,i7)
| equal(select(a_1076,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1039,685]),
[iquote('2:SpR:1039.0,685.1')] ).
cnf(1042,plain,
equal(select(a_1076,i7),e_1130),
inference(mrr,[status(thm)],[1041,340]),
[iquote('2:MRR:1041.0,340.0')] ).
cnf(1044,plain,
( equal(i8,i7)
| equal(select(a_1075,i7),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1042,671]),
[iquote('2:SpR:1042.0,671.1')] ).
cnf(1045,plain,
( equal(i8,i7)
| equal(e_1130,e7) ),
inference(rew,[status(thm),theory(equality)],[571,1044]),
[iquote('2:Rew:571.0,1044.1')] ).
cnf(1046,plain,
$false,
inference(mrr,[status(thm)],[1045,341,963]),
[iquote('2:MRR:1045.0,1045.1,341.0,963.0')] ).
cnf(1047,plain,
~ equal(i_1129,i7),
inference(spt,[spt(split,[position(s2sa)])],[1046,955]),
[iquote('2:Spt:1046.0,948.0,955.0')] ).
cnf(1048,plain,
equal(select(a_1126,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2)])],[948]),
[iquote('2:Spt:1046.0,948.1')] ).
cnf(1049,plain,
( equal(i_1129,i24)
| equal(select(a_1125,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1048,638]),
[iquote('2:SpR:1048.0,638.1')] ).
cnf(1060,plain,
equal(i_1129,i30),
inference(spt,[spt(split,[position(s2s2s1)])],[950]),
[iquote('3:Spt:950.0')] ).
cnf(1066,plain,
equal(select(a_1098,i30),e_1130),
inference(rew,[status(thm),theory(equality)],[1060,63]),
[iquote('3:Rew:1060.0,63.0')] ).
cnf(1068,plain,
( equal(i30,i24)
| equal(select(a_1125,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1060,1049]),
[iquote('3:Rew:1060.0,1049.0')] ).
cnf(1069,plain,
equal(e_1130,e30),
inference(rew,[status(thm),theory(equality)],[617,1066]),
[iquote('3:Rew:617.0,1066.0')] ).
cnf(1070,plain,
~ equal(e_1131,e30),
inference(rew,[status(thm),theory(equality)],[1069,501]),
[iquote('3:Rew:1069.0,501.0')] ).
cnf(1073,plain,
( equal(i30,i24)
| equal(select(a_1125,i30),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1060,1068]),
[iquote('3:Rew:1060.0,1068.1')] ).
cnf(1074,plain,
equal(select(a_1125,i30),e_1131),
inference(mrr,[status(thm)],[1073,81]),
[iquote('3:MRR:1073.0,81.0')] ).
cnf(1085,plain,
( equal(i30,i23)
| equal(select(a_1124,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1074,640]),
[iquote('3:SpR:1074.0,640.1')] ).
cnf(1086,plain,
equal(select(a_1124,i30),e_1131),
inference(mrr,[status(thm)],[1085,87]),
[iquote('3:MRR:1085.0,87.0')] ).
cnf(1088,plain,
( equal(i30,i17)
| equal(select(a_1123,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1086,642]),
[iquote('3:SpR:1086.0,642.1')] ).
cnf(1089,plain,
equal(select(a_1123,i30),e_1131),
inference(mrr,[status(thm)],[1088,144]),
[iquote('3:MRR:1088.0,144.0')] ).
cnf(1093,plain,
( equal(i30,i28)
| equal(select(a_1122,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1089,644]),
[iquote('3:SpR:1089.0,644.1')] ).
cnf(1094,plain,
equal(select(a_1122,i30),e_1131),
inference(mrr,[status(thm)],[1093,67]),
[iquote('3:MRR:1093.0,67.0')] ).
cnf(1096,plain,
( equal(i30,i16)
| equal(select(a_1121,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1094,646]),
[iquote('3:SpR:1094.0,646.1')] ).
cnf(1097,plain,
equal(select(a_1121,i30),e_1131),
inference(mrr,[status(thm)],[1096,157]),
[iquote('3:MRR:1096.0,157.0')] ).
cnf(1099,plain,
( equal(i30,i12)
| equal(select(a_1120,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1097,648]),
[iquote('3:SpR:1097.0,648.1')] ).
cnf(1100,plain,
equal(select(a_1120,i30),e_1131),
inference(mrr,[status(thm)],[1099,219]),
[iquote('3:MRR:1099.0,219.0')] ).
cnf(1102,plain,
( equal(i30,i3)
| equal(select(a_1119,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1100,650]),
[iquote('3:SpR:1100.0,650.1')] ).
cnf(1103,plain,
equal(select(a_1119,i30),e_1131),
inference(mrr,[status(thm)],[1102,417]),
[iquote('3:MRR:1102.0,417.0')] ).
cnf(1107,plain,
( equal(i30,i27)
| equal(select(a_1118,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1103,652]),
[iquote('3:SpR:1103.0,652.1')] ).
cnf(1108,plain,
equal(select(a_1118,i30),e_1131),
inference(mrr,[status(thm)],[1107,69]),
[iquote('3:MRR:1107.0,69.0')] ).
cnf(1110,plain,
( equal(i30,i22)
| equal(select(a_1117,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1108,654]),
[iquote('3:SpR:1108.0,654.1')] ).
cnf(1111,plain,
equal(select(a_1117,i30),e_1131),
inference(mrr,[status(thm)],[1110,94]),
[iquote('3:MRR:1110.0,94.0')] ).
cnf(1113,plain,
( equal(i30,i26)
| equal(select(a_1116,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1111,656]),
[iquote('3:SpR:1111.0,656.1')] ).
cnf(1114,plain,
equal(select(a_1116,i30),e_1131),
inference(mrr,[status(thm)],[1113,72]),
[iquote('3:MRR:1113.0,72.0')] ).
cnf(1116,plain,
( equal(i30,i5)
| equal(select(a_1115,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1114,658]),
[iquote('3:SpR:1114.0,658.1')] ).
cnf(1117,plain,
equal(select(a_1115,i30),e_1131),
inference(mrr,[status(thm)],[1116,366]),
[iquote('3:MRR:1116.0,366.0')] ).
cnf(1119,plain,
( equal(i30,i29)
| equal(select(a_1114,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1117,660]),
[iquote('3:SpR:1117.0,660.1')] ).
cnf(1120,plain,
equal(select(a_1114,i30),e_1131),
inference(mrr,[status(thm)],[1119,66]),
[iquote('3:MRR:1119.0,66.0')] ).
cnf(1122,plain,
( equal(i30,i14)
| equal(select(a_1113,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1120,662]),
[iquote('3:SpR:1120.0,662.1')] ).
cnf(1123,plain,
equal(select(a_1113,i30),e_1131),
inference(mrr,[status(thm)],[1122,186]),
[iquote('3:MRR:1122.0,186.0')] ).
cnf(1125,plain,
( equal(i30,i11)
| equal(select(a_1112,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1123,664]),
[iquote('3:SpR:1123.0,664.1')] ).
cnf(1126,plain,
equal(select(a_1112,i30),e_1131),
inference(mrr,[status(thm)],[1125,237]),
[iquote('3:MRR:1125.0,237.0')] ).
cnf(1128,plain,
( equal(i30,i6)
| equal(select(a_1111,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1126,666]),
[iquote('3:SpR:1126.0,666.1')] ).
cnf(1129,plain,
equal(select(a_1111,i30),e_1131),
inference(mrr,[status(thm)],[1128,342]),
[iquote('3:MRR:1128.0,342.0')] ).
cnf(1131,plain,
( equal(i30,i21)
| equal(select(a_1110,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1129,668]),
[iquote('3:SpR:1129.0,668.1')] ).
cnf(1132,plain,
equal(select(a_1110,i30),e_1131),
inference(mrr,[status(thm)],[1131,102]),
[iquote('3:MRR:1131.0,102.0')] ).
cnf(1134,plain,
( equal(i30,i8)
| equal(select(a_1109,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1132,670]),
[iquote('3:SpR:1132.0,670.1')] ).
cnf(1135,plain,
equal(select(a_1109,i30),e_1131),
inference(mrr,[status(thm)],[1134,297]),
[iquote('3:MRR:1134.0,297.0')] ).
cnf(1137,plain,
( equal(i30,i20)
| equal(select(a_1108,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1135,672]),
[iquote('3:SpR:1135.0,672.1')] ).
cnf(1138,plain,
equal(select(a_1108,i30),e_1131),
inference(mrr,[status(thm)],[1137,111]),
[iquote('3:MRR:1137.0,111.0')] ).
cnf(1140,plain,
( equal(i30,i18)
| equal(select(a_1107,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1138,674]),
[iquote('3:SpR:1138.0,674.1')] ).
cnf(1141,plain,
equal(select(a_1107,i30),e_1131),
inference(mrr,[status(thm)],[1140,132]),
[iquote('3:MRR:1140.0,132.0')] ).
cnf(1143,plain,
( equal(i30,i25)
| equal(select(a_1106,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1141,676]),
[iquote('3:SpR:1141.0,676.1')] ).
cnf(1144,plain,
equal(select(a_1106,i30),e_1131),
inference(mrr,[status(thm)],[1143,76]),
[iquote('3:MRR:1143.0,76.0')] ).
cnf(1146,plain,
( equal(i30,i15)
| equal(select(a_1105,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1144,678]),
[iquote('3:SpR:1144.0,678.1')] ).
cnf(1147,plain,
equal(select(a_1105,i30),e_1131),
inference(mrr,[status(thm)],[1146,171]),
[iquote('3:MRR:1146.0,171.0')] ).
cnf(1149,plain,
( equal(i30,i2)
| equal(select(a_1104,i30),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1147,680]),
[iquote('3:SpR:1147.0,680.1')] ).
cnf(1150,plain,
( equal(i30,i2)
| equal(e_1131,e30) ),
inference(rew,[status(thm),theory(equality)],[616,1149]),
[iquote('3:Rew:616.0,1149.1')] ).
cnf(1151,plain,
$false,
inference(mrr,[status(thm)],[1150,444,1070]),
[iquote('3:MRR:1150.0,1150.1,444.0,1070.0')] ).
cnf(1152,plain,
~ equal(i_1129,i30),
inference(spt,[spt(split,[position(s2s2sa)])],[1151,1060]),
[iquote('3:Spt:1151.0,950.0,1060.0')] ).
cnf(1153,plain,
equal(select(a_1097,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2)])],[950]),
[iquote('3:Spt:1151.0,950.1')] ).
cnf(1154,plain,
( equal(i_1129,i29)
| equal(select(a_1096,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1153,661]),
[iquote('3:SpR:1153.0,661.1')] ).
cnf(1167,plain,
equal(i_1129,i24),
inference(spt,[spt(split,[position(s2s2s2s1)])],[1049]),
[iquote('4:Spt:1049.0')] ).
cnf(1176,plain,
equal(select(a_1126,i24),e_1131),
inference(rew,[status(thm),theory(equality)],[1167,1048]),
[iquote('4:Rew:1167.0,1048.0')] ).
cnf(1177,plain,
( equal(i29,i24)
| equal(select(a_1096,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1167,1154]),
[iquote('4:Rew:1167.0,1154.0')] ).
cnf(1178,plain,
equal(e_1131,e24),
inference(rew,[status(thm),theory(equality)],[572,1176]),
[iquote('4:Rew:572.0,1176.0')] ).
cnf(1179,plain,
~ equal(e_1130,e24),
inference(rew,[status(thm),theory(equality)],[1178,501]),
[iquote('4:Rew:1178.0,501.0')] ).
cnf(1184,plain,
( equal(i29,i24)
| equal(select(a_1096,i24),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1167,1177]),
[iquote('4:Rew:1167.0,1177.1')] ).
cnf(1185,plain,
equal(select(a_1096,i24),e_1130),
inference(mrr,[status(thm)],[1184,82]),
[iquote('4:MRR:1184.0,82.0')] ).
cnf(1198,plain,
( equal(i28,i24)
| equal(select(a_1095,i24),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1185,645]),
[iquote('4:SpR:1185.0,645.1')] ).
cnf(1199,plain,
equal(select(a_1095,i24),e_1130),
inference(mrr,[status(thm)],[1198,83]),
[iquote('4:MRR:1198.0,83.0')] ).
cnf(1203,plain,
( equal(i27,i24)
| equal(select(a_1094,i24),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1199,653]),
[iquote('4:SpR:1199.0,653.1')] ).
cnf(1204,plain,
equal(select(a_1094,i24),e_1130),
inference(mrr,[status(thm)],[1203,84]),
[iquote('4:MRR:1203.0,84.0')] ).
cnf(1206,plain,
( equal(i26,i24)
| equal(select(a_1093,i24),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1204,657]),
[iquote('4:SpR:1204.0,657.1')] ).
cnf(1207,plain,
equal(select(a_1093,i24),e_1130),
inference(mrr,[status(thm)],[1206,85]),
[iquote('4:MRR:1206.0,85.0')] ).
cnf(1209,plain,
( equal(i25,i24)
| equal(select(a_1092,i24),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1207,677]),
[iquote('4:SpR:1207.0,677.1')] ).
cnf(1210,plain,
( equal(i25,i24)
| equal(e_1130,e24) ),
inference(rew,[status(thm),theory(equality)],[573,1209]),
[iquote('4:Rew:573.0,1209.1')] ).
cnf(1211,plain,
$false,
inference(mrr,[status(thm)],[1210,86,1179]),
[iquote('4:MRR:1210.0,1210.1,86.0,1179.0')] ).
cnf(1212,plain,
~ equal(i_1129,i24),
inference(spt,[spt(split,[position(s2s2s2sa)])],[1211,1167]),
[iquote('4:Spt:1211.0,1049.0,1167.0')] ).
cnf(1213,plain,
equal(select(a_1125,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2)])],[1049]),
[iquote('4:Spt:1211.0,1049.1')] ).
cnf(1214,plain,
( equal(i_1129,i23)
| equal(select(a_1124,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1213,640]),
[iquote('4:SpR:1213.0,640.1')] ).
cnf(1229,plain,
equal(i_1129,i29),
inference(spt,[spt(split,[position(s2s2s2s2s1)])],[1154]),
[iquote('5:Spt:1154.0')] ).
cnf(1240,plain,
equal(select(a_1097,i29),e_1130),
inference(rew,[status(thm),theory(equality)],[1229,1153]),
[iquote('5:Rew:1229.0,1153.0')] ).
cnf(1241,plain,
( equal(i29,i23)
| equal(select(a_1124,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1229,1214]),
[iquote('5:Rew:1229.0,1214.0')] ).
cnf(1242,plain,
equal(e_1130,e29),
inference(rew,[status(thm),theory(equality)],[595,1240]),
[iquote('5:Rew:595.0,1240.0')] ).
cnf(1243,plain,
~ equal(e_1131,e29),
inference(rew,[status(thm),theory(equality)],[1242,501]),
[iquote('5:Rew:1242.0,501.0')] ).
cnf(1247,plain,
( equal(i29,i23)
| equal(select(a_1124,i29),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1229,1241]),
[iquote('5:Rew:1229.0,1241.1')] ).
cnf(1248,plain,
equal(select(a_1124,i29),e_1131),
inference(mrr,[status(thm)],[1247,88]),
[iquote('5:MRR:1247.0,88.0')] ).
cnf(1265,plain,
( equal(i29,i17)
| equal(select(a_1123,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1248,642]),
[iquote('5:SpR:1248.0,642.1')] ).
cnf(1266,plain,
equal(select(a_1123,i29),e_1131),
inference(mrr,[status(thm)],[1265,145]),
[iquote('5:MRR:1265.0,145.0')] ).
cnf(1268,plain,
( equal(i29,i28)
| equal(select(a_1122,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1266,644]),
[iquote('5:SpR:1266.0,644.1')] ).
cnf(1269,plain,
equal(select(a_1122,i29),e_1131),
inference(mrr,[status(thm)],[1268,68]),
[iquote('5:MRR:1268.0,68.0')] ).
cnf(1271,plain,
( equal(i29,i16)
| equal(select(a_1121,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1269,646]),
[iquote('5:SpR:1269.0,646.1')] ).
cnf(1272,plain,
equal(select(a_1121,i29),e_1131),
inference(mrr,[status(thm)],[1271,158]),
[iquote('5:MRR:1271.0,158.0')] ).
cnf(1274,plain,
( equal(i29,i12)
| equal(select(a_1120,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1272,648]),
[iquote('5:SpR:1272.0,648.1')] ).
cnf(1275,plain,
equal(select(a_1120,i29),e_1131),
inference(mrr,[status(thm)],[1274,220]),
[iquote('5:MRR:1274.0,220.0')] ).
cnf(1279,plain,
( equal(i29,i3)
| equal(select(a_1119,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1275,650]),
[iquote('5:SpR:1275.0,650.1')] ).
cnf(1280,plain,
equal(select(a_1119,i29),e_1131),
inference(mrr,[status(thm)],[1279,418]),
[iquote('5:MRR:1279.0,418.0')] ).
cnf(1282,plain,
( equal(i29,i27)
| equal(select(a_1118,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1280,652]),
[iquote('5:SpR:1280.0,652.1')] ).
cnf(1283,plain,
equal(select(a_1118,i29),e_1131),
inference(mrr,[status(thm)],[1282,70]),
[iquote('5:MRR:1282.0,70.0')] ).
cnf(1285,plain,
( equal(i29,i22)
| equal(select(a_1117,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1283,654]),
[iquote('5:SpR:1283.0,654.1')] ).
cnf(1286,plain,
equal(select(a_1117,i29),e_1131),
inference(mrr,[status(thm)],[1285,95]),
[iquote('5:MRR:1285.0,95.0')] ).
cnf(1288,plain,
( equal(i29,i26)
| equal(select(a_1116,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1286,656]),
[iquote('5:SpR:1286.0,656.1')] ).
cnf(1289,plain,
equal(select(a_1116,i29),e_1131),
inference(mrr,[status(thm)],[1288,73]),
[iquote('5:MRR:1288.0,73.0')] ).
cnf(1291,plain,
( equal(i29,i5)
| equal(select(a_1115,i29),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1289,658]),
[iquote('5:SpR:1289.0,658.1')] ).
cnf(1292,plain,
( equal(i29,i5)
| equal(e_1131,e29) ),
inference(rew,[status(thm),theory(equality)],[594,1291]),
[iquote('5:Rew:594.0,1291.1')] ).
cnf(1293,plain,
$false,
inference(mrr,[status(thm)],[1292,367,1243]),
[iquote('5:MRR:1292.0,1292.1,367.0,1243.0')] ).
cnf(1294,plain,
~ equal(i_1129,i29),
inference(spt,[spt(split,[position(s2s2s2s2sa)])],[1293,1229]),
[iquote('5:Spt:1293.0,1154.0,1229.0')] ).
cnf(1295,plain,
equal(select(a_1096,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2)])],[1154]),
[iquote('5:Spt:1293.0,1154.1')] ).
cnf(1296,plain,
( equal(i_1129,i28)
| equal(select(a_1095,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1295,645]),
[iquote('5:SpR:1295.0,645.1')] ).
cnf(1311,plain,
equal(i_1129,i23),
inference(spt,[spt(split,[position(s2s2s2s2s2s1)])],[1214]),
[iquote('6:Spt:1214.0')] ).
cnf(1324,plain,
equal(select(a_1125,i23),e_1131),
inference(rew,[status(thm),theory(equality)],[1311,1213]),
[iquote('6:Rew:1311.0,1213.0')] ).
cnf(1325,plain,
( equal(i28,i23)
| equal(select(a_1095,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1311,1296]),
[iquote('6:Rew:1311.0,1296.0')] ).
cnf(1326,plain,
equal(e_1131,e23),
inference(rew,[status(thm),theory(equality)],[574,1324]),
[iquote('6:Rew:574.0,1324.0')] ).
cnf(1327,plain,
~ equal(e_1130,e23),
inference(rew,[status(thm),theory(equality)],[1326,501]),
[iquote('6:Rew:1326.0,501.0')] ).
cnf(1333,plain,
( equal(i28,i23)
| equal(select(a_1095,i23),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1311,1325]),
[iquote('6:Rew:1311.0,1325.1')] ).
cnf(1334,plain,
equal(select(a_1095,i23),e_1130),
inference(mrr,[status(thm)],[1333,89]),
[iquote('6:MRR:1333.0,89.0')] ).
cnf(1351,plain,
( equal(i27,i23)
| equal(select(a_1094,i23),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1334,653]),
[iquote('6:SpR:1334.0,653.1')] ).
cnf(1352,plain,
equal(select(a_1094,i23),e_1130),
inference(mrr,[status(thm)],[1351,90]),
[iquote('6:MRR:1351.0,90.0')] ).
cnf(1356,plain,
( equal(i26,i23)
| equal(select(a_1093,i23),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1352,657]),
[iquote('6:SpR:1352.0,657.1')] ).
cnf(1357,plain,
equal(select(a_1093,i23),e_1130),
inference(mrr,[status(thm)],[1356,91]),
[iquote('6:MRR:1356.0,91.0')] ).
cnf(1359,plain,
( equal(i25,i23)
| equal(select(a_1092,i23),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1357,677]),
[iquote('6:SpR:1357.0,677.1')] ).
cnf(1360,plain,
equal(select(a_1092,i23),e_1130),
inference(mrr,[status(thm)],[1359,92]),
[iquote('6:MRR:1359.0,92.0')] ).
cnf(1362,plain,
( equal(i24,i23)
| equal(select(a_1091,i23),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1360,639]),
[iquote('6:SpR:1360.0,639.1')] ).
cnf(1363,plain,
( equal(i24,i23)
| equal(e_1130,e23) ),
inference(rew,[status(thm),theory(equality)],[575,1362]),
[iquote('6:Rew:575.0,1362.1')] ).
cnf(1364,plain,
$false,
inference(mrr,[status(thm)],[1363,93,1327]),
[iquote('6:MRR:1363.0,1363.1,93.0,1327.0')] ).
cnf(1365,plain,
~ equal(i_1129,i23),
inference(spt,[spt(split,[position(s2s2s2s2s2sa)])],[1364,1311]),
[iquote('6:Spt:1364.0,1214.0,1311.0')] ).
cnf(1366,plain,
equal(select(a_1124,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2)])],[1214]),
[iquote('6:Spt:1364.0,1214.1')] ).
cnf(1367,plain,
( equal(i_1129,i17)
| equal(select(a_1123,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1366,642]),
[iquote('6:SpR:1366.0,642.1')] ).
cnf(1384,plain,
equal(i_1129,i28),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s1)])],[1296]),
[iquote('7:Spt:1296.0')] ).
cnf(1399,plain,
equal(select(a_1096,i28),e_1130),
inference(rew,[status(thm),theory(equality)],[1384,1295]),
[iquote('7:Rew:1384.0,1295.0')] ).
cnf(1400,plain,
( equal(i28,i17)
| equal(select(a_1123,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1384,1367]),
[iquote('7:Rew:1384.0,1367.0')] ).
cnf(1401,plain,
equal(e_1130,e28),
inference(rew,[status(thm),theory(equality)],[579,1399]),
[iquote('7:Rew:579.0,1399.0')] ).
cnf(1402,plain,
~ equal(e_1131,e28),
inference(rew,[status(thm),theory(equality)],[1401,501]),
[iquote('7:Rew:1401.0,501.0')] ).
cnf(1407,plain,
( equal(i28,i17)
| equal(select(a_1123,i28),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1384,1400]),
[iquote('7:Rew:1384.0,1400.1')] ).
cnf(1408,plain,
( equal(i28,i17)
| equal(e_1131,e28) ),
inference(rew,[status(thm),theory(equality)],[578,1407]),
[iquote('7:Rew:578.0,1407.1')] ).
cnf(1409,plain,
equal(e_1131,e28),
inference(mrr,[status(thm)],[1408,146]),
[iquote('7:MRR:1408.0,146.0')] ).
cnf(1410,plain,
$false,
inference(mrr,[status(thm)],[1409,1402]),
[iquote('7:MRR:1409.0,1402.0')] ).
cnf(1411,plain,
~ equal(i_1129,i28),
inference(spt,[spt(split,[position(s2s2s2s2s2s2sa)])],[1410,1384]),
[iquote('7:Spt:1410.0,1296.0,1384.0')] ).
cnf(1412,plain,
equal(select(a_1095,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2)])],[1296]),
[iquote('7:Spt:1410.0,1296.1')] ).
cnf(1413,plain,
( equal(i_1129,i27)
| equal(select(a_1094,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1412,653]),
[iquote('7:SpR:1412.0,653.1')] ).
cnf(1434,plain,
equal(i_1129,i17),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s1)])],[1367]),
[iquote('8:Spt:1367.0')] ).
cnf(1451,plain,
equal(select(a_1124,i17),e_1131),
inference(rew,[status(thm),theory(equality)],[1434,1366]),
[iquote('8:Rew:1434.0,1366.0')] ).
cnf(1452,plain,
( equal(i27,i17)
| equal(select(a_1094,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1434,1413]),
[iquote('8:Rew:1434.0,1413.0')] ).
cnf(1453,plain,
equal(e_1131,e17),
inference(rew,[status(thm),theory(equality)],[576,1451]),
[iquote('8:Rew:576.0,1451.0')] ).
cnf(1454,plain,
~ equal(e_1130,e17),
inference(rew,[status(thm),theory(equality)],[1453,501]),
[iquote('8:Rew:1453.0,501.0')] ).
cnf(1461,plain,
( equal(i27,i17)
| equal(select(a_1094,i17),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1434,1452]),
[iquote('8:Rew:1434.0,1452.1')] ).
cnf(1462,plain,
equal(select(a_1094,i17),e_1130),
inference(mrr,[status(thm)],[1461,147]),
[iquote('8:MRR:1461.0,147.0')] ).
cnf(1485,plain,
( equal(i26,i17)
| equal(select(a_1093,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1462,657]),
[iquote('8:SpR:1462.0,657.1')] ).
cnf(1486,plain,
equal(select(a_1093,i17),e_1130),
inference(mrr,[status(thm)],[1485,148]),
[iquote('8:MRR:1485.0,148.0')] ).
cnf(1488,plain,
( equal(i25,i17)
| equal(select(a_1092,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1486,677]),
[iquote('8:SpR:1486.0,677.1')] ).
cnf(1489,plain,
equal(select(a_1092,i17),e_1130),
inference(mrr,[status(thm)],[1488,149]),
[iquote('8:MRR:1488.0,149.0')] ).
cnf(1491,plain,
( equal(i24,i17)
| equal(select(a_1091,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1489,639]),
[iquote('8:SpR:1489.0,639.1')] ).
cnf(1492,plain,
equal(select(a_1091,i17),e_1130),
inference(mrr,[status(thm)],[1491,150]),
[iquote('8:MRR:1491.0,150.0')] ).
cnf(1494,plain,
( equal(i23,i17)
| equal(select(a_1090,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1492,641]),
[iquote('8:SpR:1492.0,641.1')] ).
cnf(1495,plain,
equal(select(a_1090,i17),e_1130),
inference(mrr,[status(thm)],[1494,151]),
[iquote('8:MRR:1494.0,151.0')] ).
cnf(1499,plain,
( equal(i22,i17)
| equal(select(a_1089,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1495,655]),
[iquote('8:SpR:1495.0,655.1')] ).
cnf(1500,plain,
equal(select(a_1089,i17),e_1130),
inference(mrr,[status(thm)],[1499,152]),
[iquote('8:MRR:1499.0,152.0')] ).
cnf(1502,plain,
( equal(i21,i17)
| equal(select(a_1088,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1500,669]),
[iquote('8:SpR:1500.0,669.1')] ).
cnf(1503,plain,
equal(select(a_1088,i17),e_1130),
inference(mrr,[status(thm)],[1502,153]),
[iquote('8:MRR:1502.0,153.0')] ).
cnf(1505,plain,
( equal(i20,i17)
| equal(select(a_1087,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1503,673]),
[iquote('8:SpR:1503.0,673.1')] ).
cnf(1506,plain,
equal(select(a_1087,i17),e_1130),
inference(mrr,[status(thm)],[1505,154]),
[iquote('8:MRR:1505.0,154.0')] ).
cnf(1508,plain,
( equal(i19,i17)
| equal(select(a_1086,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1506,689]),
[iquote('8:SpR:1506.0,689.1')] ).
cnf(1509,plain,
equal(select(a_1086,i17),e_1130),
inference(mrr,[status(thm)],[1508,155]),
[iquote('8:MRR:1508.0,155.0')] ).
cnf(1511,plain,
( equal(i18,i17)
| equal(select(a_1085,i17),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1509,675]),
[iquote('8:SpR:1509.0,675.1')] ).
cnf(1512,plain,
( equal(i18,i17)
| equal(e_1130,e17) ),
inference(rew,[status(thm),theory(equality)],[577,1511]),
[iquote('8:Rew:577.0,1511.1')] ).
cnf(1513,plain,
$false,
inference(mrr,[status(thm)],[1512,156,1454]),
[iquote('8:MRR:1512.0,1512.1,156.0,1454.0')] ).
cnf(1514,plain,
~ equal(i_1129,i17),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2sa)])],[1513,1434]),
[iquote('8:Spt:1513.0,1367.0,1434.0')] ).
cnf(1515,plain,
equal(select(a_1123,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2)])],[1367]),
[iquote('8:Spt:1513.0,1367.1')] ).
cnf(1516,plain,
( equal(i_1129,i28)
| equal(select(a_1122,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1515,644]),
[iquote('8:SpR:1515.0,644.1')] ).
cnf(1518,plain,
equal(select(a_1122,i_1129),e_1131),
inference(mrr,[status(thm)],[1516,1411]),
[iquote('8:MRR:1516.0,1411.0')] ).
cnf(1540,plain,
( equal(i_1129,i16)
| equal(select(a_1121,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1518,646]),
[iquote('8:SpR:1518.0,646.1')] ).
cnf(1542,plain,
equal(i_1129,i27),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s1)])],[1413]),
[iquote('9:Spt:1413.0')] ).
cnf(1561,plain,
equal(select(a_1095,i27),e_1130),
inference(rew,[status(thm),theory(equality)],[1542,1412]),
[iquote('9:Rew:1542.0,1412.0')] ).
cnf(1563,plain,
( equal(i27,i16)
| equal(select(a_1121,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1542,1540]),
[iquote('9:Rew:1542.0,1540.0')] ).
cnf(1564,plain,
equal(e_1130,e27),
inference(rew,[status(thm),theory(equality)],[587,1561]),
[iquote('9:Rew:587.0,1561.0')] ).
cnf(1565,plain,
~ equal(e_1131,e27),
inference(rew,[status(thm),theory(equality)],[1564,501]),
[iquote('9:Rew:1564.0,501.0')] ).
cnf(1571,plain,
( equal(i27,i16)
| equal(select(a_1121,i27),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1542,1563]),
[iquote('9:Rew:1542.0,1563.1')] ).
cnf(1572,plain,
equal(select(a_1121,i27),e_1131),
inference(mrr,[status(thm)],[1571,160]),
[iquote('9:MRR:1571.0,160.0')] ).
cnf(1599,plain,
( equal(i27,i12)
| equal(select(a_1120,i27),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1572,648]),
[iquote('9:SpR:1572.0,648.1')] ).
cnf(1600,plain,
equal(select(a_1120,i27),e_1131),
inference(mrr,[status(thm)],[1599,222]),
[iquote('9:MRR:1599.0,222.0')] ).
cnf(1602,plain,
( equal(i27,i3)
| equal(select(a_1119,i27),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1600,650]),
[iquote('9:SpR:1600.0,650.1')] ).
cnf(1603,plain,
( equal(i27,i3)
| equal(e_1131,e27) ),
inference(rew,[status(thm),theory(equality)],[586,1602]),
[iquote('9:Rew:586.0,1602.1')] ).
cnf(1604,plain,
$false,
inference(mrr,[status(thm)],[1603,420,1565]),
[iquote('9:MRR:1603.0,1603.1,420.0,1565.0')] ).
cnf(1605,plain,
~ equal(i_1129,i27),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2sa)])],[1604,1542]),
[iquote('9:Spt:1604.0,1413.0,1542.0')] ).
cnf(1606,plain,
equal(select(a_1094,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2)])],[1413]),
[iquote('9:Spt:1604.0,1413.1')] ).
cnf(1607,plain,
( equal(i_1129,i26)
| equal(select(a_1093,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1606,657]),
[iquote('9:SpR:1606.0,657.1')] ).
cnf(1634,plain,
equal(i_1129,i16),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s1)])],[1540]),
[iquote('10:Spt:1540.0')] ).
cnf(1645,plain,
equal(select(a_1122,i16),e_1131),
inference(rew,[status(thm),theory(equality)],[1634,1518]),
[iquote('10:Rew:1634.0,1518.0')] ).
cnf(1657,plain,
( equal(i26,i16)
| equal(select(a_1093,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1634,1607]),
[iquote('10:Rew:1634.0,1607.0')] ).
cnf(1658,plain,
equal(e_1131,e16),
inference(rew,[status(thm),theory(equality)],[580,1645]),
[iquote('10:Rew:580.0,1645.0')] ).
cnf(1659,plain,
~ equal(e_1130,e16),
inference(rew,[status(thm),theory(equality)],[1658,501]),
[iquote('10:Rew:1658.0,501.0')] ).
cnf(1668,plain,
( equal(i26,i16)
| equal(select(a_1093,i16),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1634,1657]),
[iquote('10:Rew:1634.0,1657.1')] ).
cnf(1669,plain,
equal(select(a_1093,i16),e_1130),
inference(mrr,[status(thm)],[1668,161]),
[iquote('10:MRR:1668.0,161.0')] ).
cnf(1696,plain,
( equal(i25,i16)
| equal(select(a_1092,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1669,677]),
[iquote('10:SpR:1669.0,677.1')] ).
cnf(1697,plain,
equal(select(a_1092,i16),e_1130),
inference(mrr,[status(thm)],[1696,162]),
[iquote('10:MRR:1696.0,162.0')] ).
cnf(1699,plain,
( equal(i24,i16)
| equal(select(a_1091,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1697,639]),
[iquote('10:SpR:1697.0,639.1')] ).
cnf(1700,plain,
equal(select(a_1091,i16),e_1130),
inference(mrr,[status(thm)],[1699,163]),
[iquote('10:MRR:1699.0,163.0')] ).
cnf(1702,plain,
( equal(i23,i16)
| equal(select(a_1090,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1700,641]),
[iquote('10:SpR:1700.0,641.1')] ).
cnf(1703,plain,
equal(select(a_1090,i16),e_1130),
inference(mrr,[status(thm)],[1702,164]),
[iquote('10:MRR:1702.0,164.0')] ).
cnf(1707,plain,
( equal(i22,i16)
| equal(select(a_1089,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1703,655]),
[iquote('10:SpR:1703.0,655.1')] ).
cnf(1708,plain,
equal(select(a_1089,i16),e_1130),
inference(mrr,[status(thm)],[1707,165]),
[iquote('10:MRR:1707.0,165.0')] ).
cnf(1710,plain,
( equal(i21,i16)
| equal(select(a_1088,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1708,669]),
[iquote('10:SpR:1708.0,669.1')] ).
cnf(1711,plain,
equal(select(a_1088,i16),e_1130),
inference(mrr,[status(thm)],[1710,166]),
[iquote('10:MRR:1710.0,166.0')] ).
cnf(1713,plain,
( equal(i20,i16)
| equal(select(a_1087,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1711,673]),
[iquote('10:SpR:1711.0,673.1')] ).
cnf(1714,plain,
equal(select(a_1087,i16),e_1130),
inference(mrr,[status(thm)],[1713,167]),
[iquote('10:MRR:1713.0,167.0')] ).
cnf(1716,plain,
( equal(i19,i16)
| equal(select(a_1086,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1714,689]),
[iquote('10:SpR:1714.0,689.1')] ).
cnf(1717,plain,
equal(select(a_1086,i16),e_1130),
inference(mrr,[status(thm)],[1716,168]),
[iquote('10:MRR:1716.0,168.0')] ).
cnf(1721,plain,
( equal(i18,i16)
| equal(select(a_1085,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1717,675]),
[iquote('10:SpR:1717.0,675.1')] ).
cnf(1722,plain,
equal(select(a_1085,i16),e_1130),
inference(mrr,[status(thm)],[1721,169]),
[iquote('10:MRR:1721.0,169.0')] ).
cnf(1724,plain,
( equal(i17,i16)
| equal(select(a_1084,i16),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1722,643]),
[iquote('10:SpR:1722.0,643.1')] ).
cnf(1725,plain,
( equal(i17,i16)
| equal(e_1130,e16) ),
inference(rew,[status(thm),theory(equality)],[581,1724]),
[iquote('10:Rew:581.0,1724.1')] ).
cnf(1726,plain,
$false,
inference(mrr,[status(thm)],[1725,170,1659]),
[iquote('10:MRR:1725.0,1725.1,170.0,1659.0')] ).
cnf(1727,plain,
~ equal(i_1129,i16),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2sa)])],[1726,1634]),
[iquote('10:Spt:1726.0,1540.0,1634.0')] ).
cnf(1728,plain,
equal(select(a_1121,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2)])],[1540]),
[iquote('10:Spt:1726.0,1540.1')] ).
cnf(1729,plain,
( equal(i_1129,i12)
| equal(select(a_1120,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1728,648]),
[iquote('10:SpR:1728.0,648.1')] ).
cnf(1758,plain,
equal(i_1129,i26),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s1)])],[1607]),
[iquote('11:Spt:1607.0')] ).
cnf(1782,plain,
equal(select(a_1094,i26),e_1130),
inference(rew,[status(thm),theory(equality)],[1758,1606]),
[iquote('11:Rew:1758.0,1606.0')] ).
cnf(1783,plain,
( equal(i26,i12)
| equal(select(a_1120,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1758,1729]),
[iquote('11:Rew:1758.0,1729.0')] ).
cnf(1784,plain,
equal(e_1130,e26),
inference(rew,[status(thm),theory(equality)],[591,1782]),
[iquote('11:Rew:591.0,1782.0')] ).
cnf(1785,plain,
~ equal(e_1131,e26),
inference(rew,[status(thm),theory(equality)],[1784,501]),
[iquote('11:Rew:1784.0,501.0')] ).
cnf(1792,plain,
( equal(i26,i12)
| equal(select(a_1120,i26),e_1131) ),
inference(rew,[status(thm),theory(equality)],[1758,1783]),
[iquote('11:Rew:1758.0,1783.1')] ).
cnf(1793,plain,
equal(select(a_1120,i26),e_1131),
inference(mrr,[status(thm)],[1792,223]),
[iquote('11:MRR:1792.0,223.0')] ).
cnf(1822,plain,
( equal(i26,i3)
| equal(select(a_1119,i26),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1793,650]),
[iquote('11:SpR:1793.0,650.1')] ).
cnf(1823,plain,
equal(select(a_1119,i26),e_1131),
inference(mrr,[status(thm)],[1822,421]),
[iquote('11:MRR:1822.0,421.0')] ).
cnf(1827,plain,
( equal(i27,i26)
| equal(select(a_1118,i26),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1823,652]),
[iquote('11:SpR:1823.0,652.1')] ).
cnf(1828,plain,
equal(select(a_1118,i26),e_1131),
inference(mrr,[status(thm)],[1827,75]),
[iquote('11:MRR:1827.0,75.0')] ).
cnf(1830,plain,
( equal(i26,i22)
| equal(select(a_1117,i26),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1828,654]),
[iquote('11:SpR:1828.0,654.1')] ).
cnf(1831,plain,
( equal(i26,i22)
| equal(e_1131,e26) ),
inference(rew,[status(thm),theory(equality)],[590,1830]),
[iquote('11:Rew:590.0,1830.1')] ).
cnf(1832,plain,
$false,
inference(mrr,[status(thm)],[1831,98,1785]),
[iquote('11:MRR:1831.0,1831.1,98.0,1785.0')] ).
cnf(1833,plain,
~ equal(i_1129,i26),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2sa)])],[1832,1758]),
[iquote('11:Spt:1832.0,1607.0,1758.0')] ).
cnf(1834,plain,
equal(select(a_1093,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2)])],[1607]),
[iquote('11:Spt:1832.0,1607.1')] ).
cnf(1835,plain,
( equal(i_1129,i25)
| equal(select(a_1092,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1834,677]),
[iquote('11:SpR:1834.0,677.1')] ).
cnf(1864,plain,
equal(i_1129,i12),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s1)])],[1729]),
[iquote('12:Spt:1729.0')] ).
cnf(1890,plain,
equal(select(a_1121,i12),e_1131),
inference(rew,[status(thm),theory(equality)],[1864,1728]),
[iquote('12:Rew:1864.0,1728.0')] ).
cnf(1891,plain,
( equal(i25,i12)
| equal(select(a_1092,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1864,1835]),
[iquote('12:Rew:1864.0,1835.0')] ).
cnf(1892,plain,
equal(e_1131,e12),
inference(rew,[status(thm),theory(equality)],[582,1890]),
[iquote('12:Rew:582.0,1890.0')] ).
cnf(1893,plain,
~ equal(e_1130,e12),
inference(rew,[status(thm),theory(equality)],[1892,501]),
[iquote('12:Rew:1892.0,501.0')] ).
cnf(1903,plain,
( equal(i25,i12)
| equal(select(a_1092,i12),e_1130) ),
inference(rew,[status(thm),theory(equality)],[1864,1891]),
[iquote('12:Rew:1864.0,1891.1')] ).
cnf(1904,plain,
equal(select(a_1092,i12),e_1130),
inference(mrr,[status(thm)],[1903,224]),
[iquote('12:MRR:1903.0,224.0')] ).
cnf(1937,plain,
( equal(i24,i12)
| equal(select(a_1091,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1904,639]),
[iquote('12:SpR:1904.0,639.1')] ).
cnf(1938,plain,
equal(select(a_1091,i12),e_1130),
inference(mrr,[status(thm)],[1937,225]),
[iquote('12:MRR:1937.0,225.0')] ).
cnf(1940,plain,
( equal(i23,i12)
| equal(select(a_1090,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1938,641]),
[iquote('12:SpR:1938.0,641.1')] ).
cnf(1941,plain,
equal(select(a_1090,i12),e_1130),
inference(mrr,[status(thm)],[1940,226]),
[iquote('12:MRR:1940.0,226.0')] ).
cnf(1943,plain,
( equal(i22,i12)
| equal(select(a_1089,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1941,655]),
[iquote('12:SpR:1941.0,655.1')] ).
cnf(1944,plain,
equal(select(a_1089,i12),e_1130),
inference(mrr,[status(thm)],[1943,227]),
[iquote('12:MRR:1943.0,227.0')] ).
cnf(1948,plain,
( equal(i21,i12)
| equal(select(a_1088,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1944,669]),
[iquote('12:SpR:1944.0,669.1')] ).
cnf(1949,plain,
equal(select(a_1088,i12),e_1130),
inference(mrr,[status(thm)],[1948,228]),
[iquote('12:MRR:1948.0,228.0')] ).
cnf(1951,plain,
( equal(i20,i12)
| equal(select(a_1087,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1949,673]),
[iquote('12:SpR:1949.0,673.1')] ).
cnf(1952,plain,
equal(select(a_1087,i12),e_1130),
inference(mrr,[status(thm)],[1951,229]),
[iquote('12:MRR:1951.0,229.0')] ).
cnf(1954,plain,
( equal(i19,i12)
| equal(select(a_1086,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1952,689]),
[iquote('12:SpR:1952.0,689.1')] ).
cnf(1955,plain,
equal(select(a_1086,i12),e_1130),
inference(mrr,[status(thm)],[1954,230]),
[iquote('12:MRR:1954.0,230.0')] ).
cnf(1957,plain,
( equal(i18,i12)
| equal(select(a_1085,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1955,675]),
[iquote('12:SpR:1955.0,675.1')] ).
cnf(1958,plain,
equal(select(a_1085,i12),e_1130),
inference(mrr,[status(thm)],[1957,231]),
[iquote('12:MRR:1957.0,231.0')] ).
cnf(1960,plain,
( equal(i17,i12)
| equal(select(a_1084,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1958,643]),
[iquote('12:SpR:1958.0,643.1')] ).
cnf(1961,plain,
equal(select(a_1084,i12),e_1130),
inference(mrr,[status(thm)],[1960,232]),
[iquote('12:MRR:1960.0,232.0')] ).
cnf(1963,plain,
( equal(i16,i12)
| equal(select(a_1083,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1961,647]),
[iquote('12:SpR:1961.0,647.1')] ).
cnf(1964,plain,
equal(select(a_1083,i12),e_1130),
inference(mrr,[status(thm)],[1963,233]),
[iquote('12:MRR:1963.0,233.0')] ).
cnf(1966,plain,
( equal(i15,i12)
| equal(select(a_1082,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1964,679]),
[iquote('12:SpR:1964.0,679.1')] ).
cnf(1967,plain,
equal(select(a_1082,i12),e_1130),
inference(mrr,[status(thm)],[1966,234]),
[iquote('12:MRR:1966.0,234.0')] ).
cnf(1969,plain,
( equal(i14,i12)
| equal(select(a_1081,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1967,663]),
[iquote('12:SpR:1967.0,663.1')] ).
cnf(1970,plain,
equal(select(a_1081,i12),e_1130),
inference(mrr,[status(thm)],[1969,235]),
[iquote('12:MRR:1969.0,235.0')] ).
cnf(1972,plain,
( equal(i13,i12)
| equal(select(a_1080,i12),e_1130) ),
inference(spr,[status(thm),theory(equality)],[1970,693]),
[iquote('12:SpR:1970.0,693.1')] ).
cnf(1973,plain,
( equal(i13,i12)
| equal(e_1130,e12) ),
inference(rew,[status(thm),theory(equality)],[583,1972]),
[iquote('12:Rew:583.0,1972.1')] ).
cnf(1974,plain,
$false,
inference(mrr,[status(thm)],[1973,236,1893]),
[iquote('12:MRR:1973.0,1973.1,236.0,1893.0')] ).
cnf(1975,plain,
~ equal(i_1129,i12),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2sa)])],[1974,1864]),
[iquote('12:Spt:1974.0,1729.0,1864.0')] ).
cnf(1976,plain,
equal(select(a_1120,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2)])],[1729]),
[iquote('12:Spt:1974.0,1729.1')] ).
cnf(1977,plain,
( equal(i_1129,i3)
| equal(select(a_1119,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[1976,650]),
[iquote('12:SpR:1976.0,650.1')] ).
cnf(2008,plain,
equal(i_1129,i25),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[1835]),
[iquote('13:Spt:1835.0')] ).
cnf(2036,plain,
equal(select(a_1093,i25),e_1130),
inference(rew,[status(thm),theory(equality)],[2008,1834]),
[iquote('13:Rew:2008.0,1834.0')] ).
cnf(2037,plain,
( equal(i25,i3)
| equal(select(a_1119,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[2008,1977]),
[iquote('13:Rew:2008.0,1977.0')] ).
cnf(2038,plain,
equal(e_1130,e25),
inference(rew,[status(thm),theory(equality)],[611,2036]),
[iquote('13:Rew:611.0,2036.0')] ).
cnf(2039,plain,
~ equal(e_1131,e25),
inference(rew,[status(thm),theory(equality)],[2038,501]),
[iquote('13:Rew:2038.0,501.0')] ).
cnf(2047,plain,
( equal(i25,i3)
| equal(select(a_1119,i25),e_1131) ),
inference(rew,[status(thm),theory(equality)],[2008,2037]),
[iquote('13:Rew:2008.0,2037.1')] ).
cnf(2048,plain,
equal(select(a_1119,i25),e_1131),
inference(mrr,[status(thm)],[2047,422]),
[iquote('13:MRR:2047.0,422.0')] ).
cnf(2083,plain,
( equal(i27,i25)
| equal(select(a_1118,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2048,652]),
[iquote('13:SpR:2048.0,652.1')] ).
cnf(2084,plain,
equal(select(a_1118,i25),e_1131),
inference(mrr,[status(thm)],[2083,79]),
[iquote('13:MRR:2083.0,79.0')] ).
cnf(2086,plain,
( equal(i25,i22)
| equal(select(a_1117,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2084,654]),
[iquote('13:SpR:2084.0,654.1')] ).
cnf(2087,plain,
equal(select(a_1117,i25),e_1131),
inference(mrr,[status(thm)],[2086,99]),
[iquote('13:MRR:2086.0,99.0')] ).
cnf(2089,plain,
( equal(i26,i25)
| equal(select(a_1116,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2087,656]),
[iquote('13:SpR:2087.0,656.1')] ).
cnf(2090,plain,
equal(select(a_1116,i25),e_1131),
inference(mrr,[status(thm)],[2089,80]),
[iquote('13:MRR:2089.0,80.0')] ).
cnf(2094,plain,
( equal(i25,i5)
| equal(select(a_1115,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2090,658]),
[iquote('13:SpR:2090.0,658.1')] ).
cnf(2095,plain,
equal(select(a_1115,i25),e_1131),
inference(mrr,[status(thm)],[2094,371]),
[iquote('13:MRR:2094.0,371.0')] ).
cnf(2097,plain,
( equal(i29,i25)
| equal(select(a_1114,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2095,660]),
[iquote('13:SpR:2095.0,660.1')] ).
cnf(2098,plain,
equal(select(a_1114,i25),e_1131),
inference(mrr,[status(thm)],[2097,77]),
[iquote('13:MRR:2097.0,77.0')] ).
cnf(2100,plain,
( equal(i25,i14)
| equal(select(a_1113,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2098,662]),
[iquote('13:SpR:2098.0,662.1')] ).
cnf(2101,plain,
equal(select(a_1113,i25),e_1131),
inference(mrr,[status(thm)],[2100,191]),
[iquote('13:MRR:2100.0,191.0')] ).
cnf(2103,plain,
( equal(i25,i11)
| equal(select(a_1112,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2101,664]),
[iquote('13:SpR:2101.0,664.1')] ).
cnf(2104,plain,
equal(select(a_1112,i25),e_1131),
inference(mrr,[status(thm)],[2103,242]),
[iquote('13:MRR:2103.0,242.0')] ).
cnf(2106,plain,
( equal(i25,i6)
| equal(select(a_1111,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2104,666]),
[iquote('13:SpR:2104.0,666.1')] ).
cnf(2107,plain,
equal(select(a_1111,i25),e_1131),
inference(mrr,[status(thm)],[2106,347]),
[iquote('13:MRR:2106.0,347.0')] ).
cnf(2109,plain,
( equal(i25,i21)
| equal(select(a_1110,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2107,668]),
[iquote('13:SpR:2107.0,668.1')] ).
cnf(2110,plain,
equal(select(a_1110,i25),e_1131),
inference(mrr,[status(thm)],[2109,107]),
[iquote('13:MRR:2109.0,107.0')] ).
cnf(2112,plain,
( equal(i25,i8)
| equal(select(a_1109,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2110,670]),
[iquote('13:SpR:2110.0,670.1')] ).
cnf(2113,plain,
equal(select(a_1109,i25),e_1131),
inference(mrr,[status(thm)],[2112,302]),
[iquote('13:MRR:2112.0,302.0')] ).
cnf(2115,plain,
( equal(i25,i20)
| equal(select(a_1108,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2113,672]),
[iquote('13:SpR:2113.0,672.1')] ).
cnf(2116,plain,
equal(select(a_1108,i25),e_1131),
inference(mrr,[status(thm)],[2115,116]),
[iquote('13:MRR:2115.0,116.0')] ).
cnf(2118,plain,
( equal(i25,i18)
| equal(select(a_1107,i25),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2116,674]),
[iquote('13:SpR:2116.0,674.1')] ).
cnf(2119,plain,
( equal(i25,i18)
| equal(e_1131,e25) ),
inference(rew,[status(thm),theory(equality)],[610,2118]),
[iquote('13:Rew:610.0,2118.1')] ).
cnf(2120,plain,
$false,
inference(mrr,[status(thm)],[2119,137,2039]),
[iquote('13:MRR:2119.0,2119.1,137.0,2039.0')] ).
cnf(2121,plain,
~ equal(i_1129,i25),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[2120,2008]),
[iquote('13:Spt:2120.0,1835.0,2008.0')] ).
cnf(2122,plain,
equal(select(a_1092,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[1835]),
[iquote('13:Spt:2120.0,1835.1')] ).
cnf(2123,plain,
( equal(i_1129,i24)
| equal(select(a_1091,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2122,639]),
[iquote('13:SpR:2122.0,639.1')] ).
cnf(2125,plain,
equal(select(a_1091,i_1129),e_1130),
inference(mrr,[status(thm)],[2123,1212]),
[iquote('13:MRR:2123.0,1212.0')] ).
cnf(2159,plain,
( equal(i_1129,i23)
| equal(select(a_1090,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2125,641]),
[iquote('13:SpR:2125.0,641.1')] ).
cnf(2161,plain,
equal(select(a_1090,i_1129),e_1130),
inference(mrr,[status(thm)],[2159,1365]),
[iquote('13:MRR:2159.0,1365.0')] ).
cnf(2162,plain,
( equal(i_1129,i22)
| equal(select(a_1089,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2161,655]),
[iquote('13:SpR:2161.0,655.1')] ).
cnf(2164,plain,
equal(i_1129,i3),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[1977]),
[iquote('14:Spt:1977.0')] ).
cnf(2194,plain,
equal(select(a_1120,i3),e_1131),
inference(rew,[status(thm),theory(equality)],[2164,1976]),
[iquote('14:Rew:2164.0,1976.0')] ).
cnf(2197,plain,
( equal(i22,i3)
| equal(select(a_1089,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[2164,2162]),
[iquote('14:Rew:2164.0,2162.0')] ).
cnf(2198,plain,
equal(e_1131,e3),
inference(rew,[status(thm),theory(equality)],[584,2194]),
[iquote('14:Rew:584.0,2194.0')] ).
cnf(2199,plain,
~ equal(e_1130,e3),
inference(rew,[status(thm),theory(equality)],[2198,501]),
[iquote('14:Rew:2198.0,501.0')] ).
cnf(2210,plain,
( equal(i22,i3)
| equal(select(a_1089,i3),e_1130) ),
inference(rew,[status(thm),theory(equality)],[2164,2197]),
[iquote('14:Rew:2164.0,2197.1')] ).
cnf(2211,plain,
equal(select(a_1089,i3),e_1130),
inference(mrr,[status(thm)],[2210,425]),
[iquote('14:MRR:2210.0,425.0')] ).
cnf(2254,plain,
( equal(i21,i3)
| equal(select(a_1088,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2211,669]),
[iquote('14:SpR:2211.0,669.1')] ).
cnf(2255,plain,
equal(select(a_1088,i3),e_1130),
inference(mrr,[status(thm)],[2254,426]),
[iquote('14:MRR:2254.0,426.0')] ).
cnf(2257,plain,
( equal(i20,i3)
| equal(select(a_1087,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2255,673]),
[iquote('14:SpR:2255.0,673.1')] ).
cnf(2258,plain,
equal(select(a_1087,i3),e_1130),
inference(mrr,[status(thm)],[2257,427]),
[iquote('14:MRR:2257.0,427.0')] ).
cnf(2260,plain,
( equal(i19,i3)
| equal(select(a_1086,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2258,689]),
[iquote('14:SpR:2258.0,689.1')] ).
cnf(2261,plain,
equal(select(a_1086,i3),e_1130),
inference(mrr,[status(thm)],[2260,428]),
[iquote('14:MRR:2260.0,428.0')] ).
cnf(2263,plain,
( equal(i18,i3)
| equal(select(a_1085,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2261,675]),
[iquote('14:SpR:2261.0,675.1')] ).
cnf(2264,plain,
equal(select(a_1085,i3),e_1130),
inference(mrr,[status(thm)],[2263,429]),
[iquote('14:MRR:2263.0,429.0')] ).
cnf(2266,plain,
( equal(i17,i3)
| equal(select(a_1084,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2264,643]),
[iquote('14:SpR:2264.0,643.1')] ).
cnf(2267,plain,
equal(select(a_1084,i3),e_1130),
inference(mrr,[status(thm)],[2266,430]),
[iquote('14:MRR:2266.0,430.0')] ).
cnf(2269,plain,
( equal(i16,i3)
| equal(select(a_1083,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2267,647]),
[iquote('14:SpR:2267.0,647.1')] ).
cnf(2270,plain,
equal(select(a_1083,i3),e_1130),
inference(mrr,[status(thm)],[2269,431]),
[iquote('14:MRR:2269.0,431.0')] ).
cnf(2272,plain,
( equal(i15,i3)
| equal(select(a_1082,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2270,679]),
[iquote('14:SpR:2270.0,679.1')] ).
cnf(2273,plain,
equal(select(a_1082,i3),e_1130),
inference(mrr,[status(thm)],[2272,432]),
[iquote('14:MRR:2272.0,432.0')] ).
cnf(2275,plain,
( equal(i14,i3)
| equal(select(a_1081,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2273,663]),
[iquote('14:SpR:2273.0,663.1')] ).
cnf(2276,plain,
equal(select(a_1081,i3),e_1130),
inference(mrr,[status(thm)],[2275,433]),
[iquote('14:MRR:2275.0,433.0')] ).
cnf(2278,plain,
( equal(i13,i3)
| equal(select(a_1080,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2276,693]),
[iquote('14:SpR:2276.0,693.1')] ).
cnf(2279,plain,
equal(select(a_1080,i3),e_1130),
inference(mrr,[status(thm)],[2278,434]),
[iquote('14:MRR:2278.0,434.0')] ).
cnf(2281,plain,
( equal(i12,i3)
| equal(select(a_1079,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2279,649]),
[iquote('14:SpR:2279.0,649.1')] ).
cnf(2282,plain,
equal(select(a_1079,i3),e_1130),
inference(mrr,[status(thm)],[2281,435]),
[iquote('14:MRR:2281.0,435.0')] ).
cnf(2284,plain,
( equal(i11,i3)
| equal(select(a_1078,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2282,665]),
[iquote('14:SpR:2282.0,665.1')] ).
cnf(2285,plain,
equal(select(a_1078,i3),e_1130),
inference(mrr,[status(thm)],[2284,436]),
[iquote('14:MRR:2284.0,436.0')] ).
cnf(2287,plain,
( equal(i10,i3)
| equal(select(a_1077,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2285,635]),
[iquote('14:SpR:2285.0,635.1')] ).
cnf(2288,plain,
equal(select(a_1077,i3),e_1130),
inference(mrr,[status(thm)],[2287,437]),
[iquote('14:MRR:2287.0,437.0')] ).
cnf(2290,plain,
( equal(i9,i3)
| equal(select(a_1076,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2288,685]),
[iquote('14:SpR:2288.0,685.1')] ).
cnf(2291,plain,
equal(select(a_1076,i3),e_1130),
inference(mrr,[status(thm)],[2290,438]),
[iquote('14:MRR:2290.0,438.0')] ).
cnf(2293,plain,
( equal(i8,i3)
| equal(select(a_1075,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2291,671]),
[iquote('14:SpR:2291.0,671.1')] ).
cnf(2294,plain,
equal(select(a_1075,i3),e_1130),
inference(mrr,[status(thm)],[2293,439]),
[iquote('14:MRR:2293.0,439.0')] ).
cnf(2296,plain,
( equal(i7,i3)
| equal(select(a_1074,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2294,637]),
[iquote('14:SpR:2294.0,637.1')] ).
cnf(2297,plain,
equal(select(a_1074,i3),e_1130),
inference(mrr,[status(thm)],[2296,440]),
[iquote('14:MRR:2296.0,440.0')] ).
cnf(2299,plain,
( equal(i6,i3)
| equal(select(a_1073,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2297,667]),
[iquote('14:SpR:2297.0,667.1')] ).
cnf(2300,plain,
equal(select(a_1073,i3),e_1130),
inference(mrr,[status(thm)],[2299,441]),
[iquote('14:MRR:2299.0,441.0')] ).
cnf(2302,plain,
( equal(i5,i3)
| equal(select(a_1072,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2300,659]),
[iquote('14:SpR:2300.0,659.1')] ).
cnf(2303,plain,
equal(select(a_1072,i3),e_1130),
inference(mrr,[status(thm)],[2302,442]),
[iquote('14:MRR:2302.0,442.0')] ).
cnf(2305,plain,
( equal(i4,i3)
| equal(select(a_1071,i3),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2303,687]),
[iquote('14:SpR:2303.0,687.1')] ).
cnf(2306,plain,
( equal(i4,i3)
| equal(e_1130,e3) ),
inference(rew,[status(thm),theory(equality)],[585,2305]),
[iquote('14:Rew:585.0,2305.1')] ).
cnf(2307,plain,
$false,
inference(mrr,[status(thm)],[2306,443,2199]),
[iquote('14:MRR:2306.0,2306.1,443.0,2199.0')] ).
cnf(2308,plain,
~ equal(i_1129,i3),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[2307,2164]),
[iquote('14:Spt:2307.0,1977.0,2164.0')] ).
cnf(2309,plain,
equal(select(a_1119,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[1977]),
[iquote('14:Spt:2307.0,1977.1')] ).
cnf(2310,plain,
( equal(i_1129,i27)
| equal(select(a_1118,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2309,652]),
[iquote('14:SpR:2309.0,652.1')] ).
cnf(2312,plain,
equal(select(a_1118,i_1129),e_1131),
inference(mrr,[status(thm)],[2310,1605]),
[iquote('14:MRR:2310.0,1605.0')] ).
cnf(2352,plain,
( equal(i_1129,i22)
| equal(select(a_1117,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2312,654]),
[iquote('14:SpR:2312.0,654.1')] ).
cnf(2356,plain,
equal(i_1129,i22),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[2162]),
[iquote('15:Spt:2162.0')] ).
cnf(2372,plain,
equal(select(a_1090,i22),e_1130),
inference(rew,[status(thm),theory(equality)],[2356,2161]),
[iquote('15:Rew:2356.0,2161.0')] ).
cnf(2391,plain,
equal(select(a_1118,i22),e_1131),
inference(rew,[status(thm),theory(equality)],[2356,2312]),
[iquote('15:Rew:2356.0,2312.0')] ).
cnf(2392,plain,
equal(e_1130,e22),
inference(rew,[status(thm),theory(equality)],[589,2372]),
[iquote('15:Rew:589.0,2372.0')] ).
cnf(2393,plain,
~ equal(e_1131,e22),
inference(rew,[status(thm),theory(equality)],[2392,501]),
[iquote('15:Rew:2392.0,501.0')] ).
cnf(2404,plain,
equal(e_1131,e22),
inference(rew,[status(thm),theory(equality)],[588,2391]),
[iquote('15:Rew:588.0,2391.0')] ).
cnf(2405,plain,
$false,
inference(mrr,[status(thm)],[2404,2393]),
[iquote('15:MRR:2404.0,2393.0')] ).
cnf(2406,plain,
~ equal(i_1129,i22),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[2405,2356]),
[iquote('15:Spt:2405.0,2162.0,2356.0')] ).
cnf(2407,plain,
equal(select(a_1089,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[2162]),
[iquote('15:Spt:2405.0,2162.1')] ).
cnf(2408,plain,
equal(select(a_1117,i_1129),e_1131),
inference(mrr,[status(thm)],[2352,2406]),
[iquote('15:MRR:2352.0,2406.0')] ).
cnf(2409,plain,
( equal(i_1129,i21)
| equal(select(a_1088,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2407,669]),
[iquote('15:SpR:2407.0,669.1')] ).
cnf(2456,plain,
( equal(i_1129,i26)
| equal(select(a_1116,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2408,656]),
[iquote('15:SpR:2408.0,656.1')] ).
cnf(2458,plain,
equal(select(a_1116,i_1129),e_1131),
inference(mrr,[status(thm)],[2456,1833]),
[iquote('15:MRR:2456.0,1833.0')] ).
cnf(2459,plain,
( equal(i_1129,i5)
| equal(select(a_1115,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2458,658]),
[iquote('15:SpR:2458.0,658.1')] ).
cnf(2461,plain,
equal(i_1129,i21),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[2409]),
[iquote('16:Spt:2409.0')] ).
cnf(2462,plain,
equal(select(a_1089,i21),e_1130),
inference(rew,[status(thm),theory(equality)],[2461,2407]),
[iquote('16:Rew:2461.0,2407.0')] ).
cnf(2501,plain,
( equal(i21,i5)
| equal(select(a_1115,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[2461,2459]),
[iquote('16:Rew:2461.0,2459.0')] ).
cnf(2502,plain,
equal(e_1130,e21),
inference(rew,[status(thm),theory(equality)],[603,2462]),
[iquote('16:Rew:603.0,2462.0')] ).
cnf(2503,plain,
~ equal(e_1131,e21),
inference(rew,[status(thm),theory(equality)],[2502,501]),
[iquote('16:Rew:2502.0,501.0')] ).
cnf(2515,plain,
( equal(i21,i5)
| equal(select(a_1115,i21),e_1131) ),
inference(rew,[status(thm),theory(equality)],[2461,2501]),
[iquote('16:Rew:2461.0,2501.1')] ).
cnf(2516,plain,
equal(select(a_1115,i21),e_1131),
inference(mrr,[status(thm)],[2515,375]),
[iquote('16:MRR:2515.0,375.0')] ).
cnf(2569,plain,
( equal(i29,i21)
| equal(select(a_1114,i21),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2516,660]),
[iquote('16:SpR:2516.0,660.1')] ).
cnf(2570,plain,
equal(select(a_1114,i21),e_1131),
inference(mrr,[status(thm)],[2569,103]),
[iquote('16:MRR:2569.0,103.0')] ).
cnf(2572,plain,
( equal(i21,i14)
| equal(select(a_1113,i21),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2570,662]),
[iquote('16:SpR:2570.0,662.1')] ).
cnf(2573,plain,
equal(select(a_1113,i21),e_1131),
inference(mrr,[status(thm)],[2572,195]),
[iquote('16:MRR:2572.0,195.0')] ).
cnf(2575,plain,
( equal(i21,i11)
| equal(select(a_1112,i21),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2573,664]),
[iquote('16:SpR:2573.0,664.1')] ).
cnf(2576,plain,
equal(select(a_1112,i21),e_1131),
inference(mrr,[status(thm)],[2575,246]),
[iquote('16:MRR:2575.0,246.0')] ).
cnf(2578,plain,
( equal(i21,i6)
| equal(select(a_1111,i21),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2576,666]),
[iquote('16:SpR:2576.0,666.1')] ).
cnf(2579,plain,
( equal(i21,i6)
| equal(e_1131,e21) ),
inference(rew,[status(thm),theory(equality)],[602,2578]),
[iquote('16:Rew:602.0,2578.1')] ).
cnf(2580,plain,
$false,
inference(mrr,[status(thm)],[2579,351,2503]),
[iquote('16:MRR:2579.0,2579.1,351.0,2503.0')] ).
cnf(2581,plain,
~ equal(i_1129,i21),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[2580,2461]),
[iquote('16:Spt:2580.0,2409.0,2461.0')] ).
cnf(2582,plain,
equal(select(a_1088,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[2409]),
[iquote('16:Spt:2580.0,2409.1')] ).
cnf(2583,plain,
( equal(i_1129,i20)
| equal(select(a_1087,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2582,673]),
[iquote('16:SpR:2582.0,673.1')] ).
cnf(2636,plain,
equal(i_1129,i5),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[2459]),
[iquote('17:Spt:2459.0')] ).
cnf(2654,plain,
equal(select(a_1116,i5),e_1131),
inference(rew,[status(thm),theory(equality)],[2636,2458]),
[iquote('17:Rew:2636.0,2458.0')] ).
cnf(2678,plain,
( equal(i20,i5)
| equal(select(a_1087,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[2636,2583]),
[iquote('17:Rew:2636.0,2583.0')] ).
cnf(2679,plain,
equal(e_1131,e5),
inference(rew,[status(thm),theory(equality)],[592,2654]),
[iquote('17:Rew:592.0,2654.0')] ).
cnf(2680,plain,
~ equal(e_1130,e5),
inference(rew,[status(thm),theory(equality)],[2679,501]),
[iquote('17:Rew:2679.0,501.0')] ).
cnf(2695,plain,
( equal(i20,i5)
| equal(select(a_1087,i5),e_1130) ),
inference(rew,[status(thm),theory(equality)],[2636,2678]),
[iquote('17:Rew:2636.0,2678.1')] ).
cnf(2696,plain,
equal(select(a_1087,i5),e_1130),
inference(mrr,[status(thm)],[2695,376]),
[iquote('17:MRR:2695.0,376.0')] ).
cnf(2751,plain,
( equal(i19,i5)
| equal(select(a_1086,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2696,689]),
[iquote('17:SpR:2696.0,689.1')] ).
cnf(2752,plain,
equal(select(a_1086,i5),e_1130),
inference(mrr,[status(thm)],[2751,377]),
[iquote('17:MRR:2751.0,377.0')] ).
cnf(2754,plain,
( equal(i18,i5)
| equal(select(a_1085,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2752,675]),
[iquote('17:SpR:2752.0,675.1')] ).
cnf(2755,plain,
equal(select(a_1085,i5),e_1130),
inference(mrr,[status(thm)],[2754,378]),
[iquote('17:MRR:2754.0,378.0')] ).
cnf(2757,plain,
( equal(i17,i5)
| equal(select(a_1084,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2755,643]),
[iquote('17:SpR:2755.0,643.1')] ).
cnf(2758,plain,
equal(select(a_1084,i5),e_1130),
inference(mrr,[status(thm)],[2757,379]),
[iquote('17:MRR:2757.0,379.0')] ).
cnf(2760,plain,
( equal(i16,i5)
| equal(select(a_1083,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2758,647]),
[iquote('17:SpR:2758.0,647.1')] ).
cnf(2761,plain,
equal(select(a_1083,i5),e_1130),
inference(mrr,[status(thm)],[2760,380]),
[iquote('17:MRR:2760.0,380.0')] ).
cnf(2763,plain,
( equal(i15,i5)
| equal(select(a_1082,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2761,679]),
[iquote('17:SpR:2761.0,679.1')] ).
cnf(2764,plain,
equal(select(a_1082,i5),e_1130),
inference(mrr,[status(thm)],[2763,381]),
[iquote('17:MRR:2763.0,381.0')] ).
cnf(2766,plain,
( equal(i14,i5)
| equal(select(a_1081,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2764,663]),
[iquote('17:SpR:2764.0,663.1')] ).
cnf(2767,plain,
equal(select(a_1081,i5),e_1130),
inference(mrr,[status(thm)],[2766,382]),
[iquote('17:MRR:2766.0,382.0')] ).
cnf(2769,plain,
( equal(i13,i5)
| equal(select(a_1080,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2767,693]),
[iquote('17:SpR:2767.0,693.1')] ).
cnf(2770,plain,
equal(select(a_1080,i5),e_1130),
inference(mrr,[status(thm)],[2769,383]),
[iquote('17:MRR:2769.0,383.0')] ).
cnf(2772,plain,
( equal(i12,i5)
| equal(select(a_1079,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2770,649]),
[iquote('17:SpR:2770.0,649.1')] ).
cnf(2773,plain,
equal(select(a_1079,i5),e_1130),
inference(mrr,[status(thm)],[2772,384]),
[iquote('17:MRR:2772.0,384.0')] ).
cnf(2775,plain,
( equal(i11,i5)
| equal(select(a_1078,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2773,665]),
[iquote('17:SpR:2773.0,665.1')] ).
cnf(2776,plain,
equal(select(a_1078,i5),e_1130),
inference(mrr,[status(thm)],[2775,385]),
[iquote('17:MRR:2775.0,385.0')] ).
cnf(2778,plain,
( equal(i10,i5)
| equal(select(a_1077,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2776,635]),
[iquote('17:SpR:2776.0,635.1')] ).
cnf(2779,plain,
equal(select(a_1077,i5),e_1130),
inference(mrr,[status(thm)],[2778,386]),
[iquote('17:MRR:2778.0,386.0')] ).
cnf(2781,plain,
( equal(i9,i5)
| equal(select(a_1076,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2779,685]),
[iquote('17:SpR:2779.0,685.1')] ).
cnf(2782,plain,
equal(select(a_1076,i5),e_1130),
inference(mrr,[status(thm)],[2781,387]),
[iquote('17:MRR:2781.0,387.0')] ).
cnf(2784,plain,
( equal(i8,i5)
| equal(select(a_1075,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2782,671]),
[iquote('17:SpR:2782.0,671.1')] ).
cnf(2785,plain,
equal(select(a_1075,i5),e_1130),
inference(mrr,[status(thm)],[2784,388]),
[iquote('17:MRR:2784.0,388.0')] ).
cnf(2787,plain,
( equal(i7,i5)
| equal(select(a_1074,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2785,637]),
[iquote('17:SpR:2785.0,637.1')] ).
cnf(2788,plain,
equal(select(a_1074,i5),e_1130),
inference(mrr,[status(thm)],[2787,389]),
[iquote('17:MRR:2787.0,389.0')] ).
cnf(2790,plain,
( equal(i6,i5)
| equal(select(a_1073,i5),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2788,667]),
[iquote('17:SpR:2788.0,667.1')] ).
cnf(2791,plain,
( equal(i6,i5)
| equal(e_1130,e5) ),
inference(rew,[status(thm),theory(equality)],[593,2790]),
[iquote('17:Rew:593.0,2790.1')] ).
cnf(2792,plain,
$false,
inference(mrr,[status(thm)],[2791,390,2680]),
[iquote('17:MRR:2791.0,2791.1,390.0,2680.0')] ).
cnf(2793,plain,
~ equal(i_1129,i5),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[2792,2636]),
[iquote('17:Spt:2792.0,2459.0,2636.0')] ).
cnf(2794,plain,
equal(select(a_1115,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[2459]),
[iquote('17:Spt:2792.0,2459.1')] ).
cnf(2795,plain,
( equal(i_1129,i29)
| equal(select(a_1114,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2794,660]),
[iquote('17:SpR:2794.0,660.1')] ).
cnf(2797,plain,
equal(select(a_1114,i_1129),e_1131),
inference(mrr,[status(thm)],[2795,1294]),
[iquote('17:MRR:2795.0,1294.0')] ).
cnf(2851,plain,
( equal(i_1129,i14)
| equal(select(a_1113,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2797,662]),
[iquote('17:SpR:2797.0,662.1')] ).
cnf(2853,plain,
equal(i_1129,i20),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[2583]),
[iquote('18:Spt:2583.0')] ).
cnf(2896,plain,
equal(select(a_1088,i20),e_1130),
inference(rew,[status(thm),theory(equality)],[2853,2582]),
[iquote('18:Rew:2853.0,2582.0')] ).
cnf(2898,plain,
( equal(i20,i14)
| equal(select(a_1113,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[2853,2851]),
[iquote('18:Rew:2853.0,2851.0')] ).
cnf(2899,plain,
equal(e_1130,e20),
inference(rew,[status(thm),theory(equality)],[607,2896]),
[iquote('18:Rew:607.0,2896.0')] ).
cnf(2900,plain,
~ equal(e_1131,e20),
inference(rew,[status(thm),theory(equality)],[2899,501]),
[iquote('18:Rew:2899.0,501.0')] ).
cnf(2913,plain,
( equal(i20,i14)
| equal(select(a_1113,i20),e_1131) ),
inference(rew,[status(thm),theory(equality)],[2853,2898]),
[iquote('18:Rew:2853.0,2898.1')] ).
cnf(2914,plain,
equal(select(a_1113,i20),e_1131),
inference(mrr,[status(thm)],[2913,196]),
[iquote('18:MRR:2913.0,196.0')] ).
cnf(2973,plain,
( equal(i20,i11)
| equal(select(a_1112,i20),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2914,664]),
[iquote('18:SpR:2914.0,664.1')] ).
cnf(2974,plain,
equal(select(a_1112,i20),e_1131),
inference(mrr,[status(thm)],[2973,247]),
[iquote('18:MRR:2973.0,247.0')] ).
cnf(2976,plain,
( equal(i20,i6)
| equal(select(a_1111,i20),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2974,666]),
[iquote('18:SpR:2974.0,666.1')] ).
cnf(2977,plain,
equal(select(a_1111,i20),e_1131),
inference(mrr,[status(thm)],[2976,352]),
[iquote('18:MRR:2976.0,352.0')] ).
cnf(2979,plain,
( equal(i21,i20)
| equal(select(a_1110,i20),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2977,668]),
[iquote('18:SpR:2977.0,668.1')] ).
cnf(2980,plain,
equal(select(a_1110,i20),e_1131),
inference(mrr,[status(thm)],[2979,120]),
[iquote('18:MRR:2979.0,120.0')] ).
cnf(2982,plain,
( equal(i20,i8)
| equal(select(a_1109,i20),e_1131) ),
inference(spr,[status(thm),theory(equality)],[2980,670]),
[iquote('18:SpR:2980.0,670.1')] ).
cnf(2983,plain,
( equal(i20,i8)
| equal(e_1131,e20) ),
inference(rew,[status(thm),theory(equality)],[606,2982]),
[iquote('18:Rew:606.0,2982.1')] ).
cnf(2984,plain,
$false,
inference(mrr,[status(thm)],[2983,307,2900]),
[iquote('18:MRR:2983.0,2983.1,307.0,2900.0')] ).
cnf(2985,plain,
~ equal(i_1129,i20),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[2984,2853]),
[iquote('18:Spt:2984.0,2583.0,2853.0')] ).
cnf(2986,plain,
equal(select(a_1087,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[2583]),
[iquote('18:Spt:2984.0,2583.1')] ).
cnf(2987,plain,
( equal(i_1129,i19)
| equal(select(a_1086,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[2986,689]),
[iquote('18:SpR:2986.0,689.1')] ).
cnf(3046,plain,
equal(i_1129,i19),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[2987]),
[iquote('19:Spt:2987.0')] ).
cnf(3047,plain,
equal(select(a_1087,i19),e_1130),
inference(rew,[status(thm),theory(equality)],[3046,2986]),
[iquote('19:Rew:3046.0,2986.0')] ).
cnf(3093,plain,
( equal(i19,i14)
| equal(select(a_1113,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[3046,2851]),
[iquote('19:Rew:3046.0,2851.0')] ).
cnf(3094,plain,
equal(e_1130,e19),
inference(rew,[status(thm),theory(equality)],[623,3047]),
[iquote('19:Rew:623.0,3047.0')] ).
cnf(3095,plain,
~ equal(e_1131,e19),
inference(rew,[status(thm),theory(equality)],[3094,501]),
[iquote('19:Rew:3094.0,501.0')] ).
cnf(3109,plain,
( equal(i19,i14)
| equal(select(a_1113,i19),e_1131) ),
inference(rew,[status(thm),theory(equality)],[3046,3093]),
[iquote('19:Rew:3046.0,3093.1')] ).
cnf(3110,plain,
equal(select(a_1113,i19),e_1131),
inference(mrr,[status(thm)],[3109,197]),
[iquote('19:MRR:3109.0,197.0')] ).
cnf(3171,plain,
( equal(i19,i11)
| equal(select(a_1112,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3110,664]),
[iquote('19:SpR:3110.0,664.1')] ).
cnf(3172,plain,
equal(select(a_1112,i19),e_1131),
inference(mrr,[status(thm)],[3171,248]),
[iquote('19:MRR:3171.0,248.0')] ).
cnf(3174,plain,
( equal(i19,i6)
| equal(select(a_1111,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3172,666]),
[iquote('19:SpR:3172.0,666.1')] ).
cnf(3175,plain,
equal(select(a_1111,i19),e_1131),
inference(mrr,[status(thm)],[3174,353]),
[iquote('19:MRR:3174.0,353.0')] ).
cnf(3177,plain,
( equal(i21,i19)
| equal(select(a_1110,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3175,668]),
[iquote('19:SpR:3175.0,668.1')] ).
cnf(3178,plain,
equal(select(a_1110,i19),e_1131),
inference(mrr,[status(thm)],[3177,130]),
[iquote('19:MRR:3177.0,130.0')] ).
cnf(3180,plain,
( equal(i19,i8)
| equal(select(a_1109,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3178,670]),
[iquote('19:SpR:3178.0,670.1')] ).
cnf(3181,plain,
equal(select(a_1109,i19),e_1131),
inference(mrr,[status(thm)],[3180,308]),
[iquote('19:MRR:3180.0,308.0')] ).
cnf(3183,plain,
( equal(i20,i19)
| equal(select(a_1108,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3181,672]),
[iquote('19:SpR:3181.0,672.1')] ).
cnf(3184,plain,
equal(select(a_1108,i19),e_1131),
inference(mrr,[status(thm)],[3183,131]),
[iquote('19:MRR:3183.0,131.0')] ).
cnf(3186,plain,
( equal(i19,i18)
| equal(select(a_1107,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3184,674]),
[iquote('19:SpR:3184.0,674.1')] ).
cnf(3187,plain,
equal(select(a_1107,i19),e_1131),
inference(mrr,[status(thm)],[3186,143]),
[iquote('19:MRR:3186.0,143.0')] ).
cnf(3189,plain,
( equal(i25,i19)
| equal(select(a_1106,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3187,676]),
[iquote('19:SpR:3187.0,676.1')] ).
cnf(3190,plain,
equal(select(a_1106,i19),e_1131),
inference(mrr,[status(thm)],[3189,126]),
[iquote('19:MRR:3189.0,126.0')] ).
cnf(3192,plain,
( equal(i19,i15)
| equal(select(a_1105,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3190,678]),
[iquote('19:SpR:3190.0,678.1')] ).
cnf(3193,plain,
equal(select(a_1105,i19),e_1131),
inference(mrr,[status(thm)],[3192,182]),
[iquote('19:MRR:3192.0,182.0')] ).
cnf(3195,plain,
( equal(i19,i2)
| equal(select(a_1104,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3193,680]),
[iquote('19:SpR:3193.0,680.1')] ).
cnf(3196,plain,
equal(select(a_1104,i19),e_1131),
inference(mrr,[status(thm)],[3195,455]),
[iquote('19:MRR:3195.0,455.0')] ).
cnf(3198,plain,
( equal(i30,i19)
| equal(select(a_1103,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3196,682]),
[iquote('19:SpR:3196.0,682.1')] ).
cnf(3199,plain,
equal(select(a_1103,i19),e_1131),
inference(mrr,[status(thm)],[3198,121]),
[iquote('19:MRR:3198.0,121.0')] ).
cnf(3201,plain,
( equal(i19,i9)
| equal(select(a_1102,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3199,684]),
[iquote('19:SpR:3199.0,684.1')] ).
cnf(3202,plain,
equal(select(a_1102,i19),e_1131),
inference(mrr,[status(thm)],[3201,287]),
[iquote('19:MRR:3201.0,287.0')] ).
cnf(3204,plain,
( equal(i19,i4)
| equal(select(a_1101,i19),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3202,686]),
[iquote('19:SpR:3202.0,686.1')] ).
cnf(3205,plain,
( equal(i19,i4)
| equal(e_1131,e19) ),
inference(rew,[status(thm),theory(equality)],[622,3204]),
[iquote('19:Rew:622.0,3204.1')] ).
cnf(3206,plain,
$false,
inference(mrr,[status(thm)],[3205,402,3095]),
[iquote('19:MRR:3205.0,3205.1,402.0,3095.0')] ).
cnf(3207,plain,
~ equal(i_1129,i19),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[3206,3046]),
[iquote('19:Spt:3206.0,2987.0,3046.0')] ).
cnf(3208,plain,
equal(select(a_1086,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[2987]),
[iquote('19:Spt:3206.0,2987.1')] ).
cnf(3209,plain,
( equal(i_1129,i18)
| equal(select(a_1085,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3208,675]),
[iquote('19:SpR:3208.0,675.1')] ).
cnf(3270,plain,
equal(i_1129,i14),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[2851]),
[iquote('20:Spt:2851.0')] ).
cnf(3317,plain,
equal(select(a_1114,i14),e_1131),
inference(rew,[status(thm),theory(equality)],[3270,2797]),
[iquote('20:Rew:3270.0,2797.0')] ).
cnf(3319,plain,
( equal(i18,i14)
| equal(select(a_1085,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[3270,3209]),
[iquote('20:Rew:3270.0,3209.0')] ).
cnf(3320,plain,
equal(e_1131,e14),
inference(rew,[status(thm),theory(equality)],[596,3317]),
[iquote('20:Rew:596.0,3317.0')] ).
cnf(3321,plain,
~ equal(e_1130,e14),
inference(rew,[status(thm),theory(equality)],[3320,501]),
[iquote('20:Rew:3320.0,501.0')] ).
cnf(3338,plain,
( equal(i18,i14)
| equal(select(a_1085,i14),e_1130) ),
inference(rew,[status(thm),theory(equality)],[3270,3319]),
[iquote('20:Rew:3270.0,3319.1')] ).
cnf(3339,plain,
equal(select(a_1085,i14),e_1130),
inference(mrr,[status(thm)],[3338,198]),
[iquote('20:MRR:3338.0,198.0')] ).
cnf(3402,plain,
( equal(i17,i14)
| equal(select(a_1084,i14),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3339,643]),
[iquote('20:SpR:3339.0,643.1')] ).
cnf(3403,plain,
equal(select(a_1084,i14),e_1130),
inference(mrr,[status(thm)],[3402,199]),
[iquote('20:MRR:3402.0,199.0')] ).
cnf(3405,plain,
( equal(i16,i14)
| equal(select(a_1083,i14),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3403,647]),
[iquote('20:SpR:3403.0,647.1')] ).
cnf(3406,plain,
equal(select(a_1083,i14),e_1130),
inference(mrr,[status(thm)],[3405,200]),
[iquote('20:MRR:3405.0,200.0')] ).
cnf(3408,plain,
( equal(i15,i14)
| equal(select(a_1082,i14),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3406,679]),
[iquote('20:SpR:3406.0,679.1')] ).
cnf(3409,plain,
( equal(i15,i14)
| equal(e_1130,e14) ),
inference(rew,[status(thm),theory(equality)],[597,3408]),
[iquote('20:Rew:597.0,3408.1')] ).
cnf(3410,plain,
$false,
inference(mrr,[status(thm)],[3409,201,3321]),
[iquote('20:MRR:3409.0,3409.1,201.0,3321.0')] ).
cnf(3411,plain,
~ equal(i_1129,i14),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[3410,3270]),
[iquote('20:Spt:3410.0,2851.0,3270.0')] ).
cnf(3412,plain,
equal(select(a_1113,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[2851]),
[iquote('20:Spt:3410.0,2851.1')] ).
cnf(3413,plain,
( equal(i_1129,i11)
| equal(select(a_1112,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3412,664]),
[iquote('20:SpR:3412.0,664.1')] ).
cnf(3476,plain,
equal(i_1129,i18),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[3209]),
[iquote('21:Spt:3209.0')] ).
cnf(3526,plain,
equal(select(a_1086,i18),e_1130),
inference(rew,[status(thm),theory(equality)],[3476,3208]),
[iquote('21:Rew:3476.0,3208.0')] ).
cnf(3527,plain,
( equal(i18,i11)
| equal(select(a_1112,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[3476,3413]),
[iquote('21:Rew:3476.0,3413.0')] ).
cnf(3528,plain,
equal(e_1130,e18),
inference(rew,[status(thm),theory(equality)],[609,3526]),
[iquote('21:Rew:609.0,3526.0')] ).
cnf(3529,plain,
~ equal(e_1131,e18),
inference(rew,[status(thm),theory(equality)],[3528,501]),
[iquote('21:Rew:3528.0,501.0')] ).
cnf(3544,plain,
( equal(i18,i11)
| equal(select(a_1112,i18),e_1131) ),
inference(rew,[status(thm),theory(equality)],[3476,3527]),
[iquote('21:Rew:3476.0,3527.1')] ).
cnf(3545,plain,
equal(select(a_1112,i18),e_1131),
inference(mrr,[status(thm)],[3544,249]),
[iquote('21:MRR:3544.0,249.0')] ).
cnf(3610,plain,
( equal(i18,i6)
| equal(select(a_1111,i18),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3545,666]),
[iquote('21:SpR:3545.0,666.1')] ).
cnf(3611,plain,
equal(select(a_1111,i18),e_1131),
inference(mrr,[status(thm)],[3610,354]),
[iquote('21:MRR:3610.0,354.0')] ).
cnf(3613,plain,
( equal(i21,i18)
| equal(select(a_1110,i18),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3611,668]),
[iquote('21:SpR:3611.0,668.1')] ).
cnf(3614,plain,
equal(select(a_1110,i18),e_1131),
inference(mrr,[status(thm)],[3613,141]),
[iquote('21:MRR:3613.0,141.0')] ).
cnf(3616,plain,
( equal(i18,i8)
| equal(select(a_1109,i18),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3614,670]),
[iquote('21:SpR:3614.0,670.1')] ).
cnf(3617,plain,
equal(select(a_1109,i18),e_1131),
inference(mrr,[status(thm)],[3616,309]),
[iquote('21:MRR:3616.0,309.0')] ).
cnf(3619,plain,
( equal(i20,i18)
| equal(select(a_1108,i18),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3617,672]),
[iquote('21:SpR:3617.0,672.1')] ).
cnf(3620,plain,
( equal(i20,i18)
| equal(e_1131,e18) ),
inference(rew,[status(thm),theory(equality)],[608,3619]),
[iquote('21:Rew:608.0,3619.1')] ).
cnf(3621,plain,
$false,
inference(mrr,[status(thm)],[3620,142,3529]),
[iquote('21:MRR:3620.0,3620.1,142.0,3529.0')] ).
cnf(3622,plain,
~ equal(i_1129,i18),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[3621,3476]),
[iquote('21:Spt:3621.0,3209.0,3476.0')] ).
cnf(3623,plain,
equal(select(a_1085,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[3209]),
[iquote('21:Spt:3621.0,3209.1')] ).
cnf(3624,plain,
( equal(i_1129,i17)
| equal(select(a_1084,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3623,643]),
[iquote('21:SpR:3623.0,643.1')] ).
cnf(3626,plain,
equal(select(a_1084,i_1129),e_1130),
inference(mrr,[status(thm)],[3624,1514]),
[iquote('21:MRR:3624.0,1514.0')] ).
cnf(3690,plain,
( equal(i_1129,i16)
| equal(select(a_1083,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3626,647]),
[iquote('21:SpR:3626.0,647.1')] ).
cnf(3692,plain,
equal(select(a_1083,i_1129),e_1130),
inference(mrr,[status(thm)],[3690,1727]),
[iquote('21:MRR:3690.0,1727.0')] ).
cnf(3693,plain,
( equal(i_1129,i15)
| equal(select(a_1082,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3692,679]),
[iquote('21:SpR:3692.0,679.1')] ).
cnf(3695,plain,
equal(i_1129,i11),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[3413]),
[iquote('22:Spt:3413.0')] ).
cnf(3747,plain,
equal(select(a_1113,i11),e_1131),
inference(rew,[status(thm),theory(equality)],[3695,3412]),
[iquote('22:Rew:3695.0,3412.0')] ).
cnf(3750,plain,
( equal(i15,i11)
| equal(select(a_1082,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[3695,3693]),
[iquote('22:Rew:3695.0,3693.0')] ).
cnf(3751,plain,
equal(e_1131,e11),
inference(rew,[status(thm),theory(equality)],[598,3747]),
[iquote('22:Rew:598.0,3747.0')] ).
cnf(3752,plain,
~ equal(e_1130,e11),
inference(rew,[status(thm),theory(equality)],[3751,501]),
[iquote('22:Rew:3751.0,501.0')] ).
cnf(3770,plain,
( equal(i15,i11)
| equal(select(a_1082,i11),e_1130) ),
inference(rew,[status(thm),theory(equality)],[3695,3750]),
[iquote('22:Rew:3695.0,3750.1')] ).
cnf(3771,plain,
equal(select(a_1082,i11),e_1130),
inference(mrr,[status(thm)],[3770,252]),
[iquote('22:MRR:3770.0,252.0')] ).
cnf(3842,plain,
( equal(i14,i11)
| equal(select(a_1081,i11),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3771,663]),
[iquote('22:SpR:3771.0,663.1')] ).
cnf(3843,plain,
equal(select(a_1081,i11),e_1130),
inference(mrr,[status(thm)],[3842,253]),
[iquote('22:MRR:3842.0,253.0')] ).
cnf(3845,plain,
( equal(i13,i11)
| equal(select(a_1080,i11),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3843,693]),
[iquote('22:SpR:3843.0,693.1')] ).
cnf(3846,plain,
equal(select(a_1080,i11),e_1130),
inference(mrr,[status(thm)],[3845,254]),
[iquote('22:MRR:3845.0,254.0')] ).
cnf(3848,plain,
( equal(i12,i11)
| equal(select(a_1079,i11),e_1130) ),
inference(spr,[status(thm),theory(equality)],[3846,649]),
[iquote('22:SpR:3846.0,649.1')] ).
cnf(3849,plain,
( equal(i12,i11)
| equal(e_1130,e11) ),
inference(rew,[status(thm),theory(equality)],[599,3848]),
[iquote('22:Rew:599.0,3848.1')] ).
cnf(3850,plain,
$false,
inference(mrr,[status(thm)],[3849,255,3752]),
[iquote('22:MRR:3849.0,3849.1,255.0,3752.0')] ).
cnf(3851,plain,
~ equal(i_1129,i11),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[3850,3695]),
[iquote('22:Spt:3850.0,3413.0,3695.0')] ).
cnf(3852,plain,
equal(select(a_1112,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[3413]),
[iquote('22:Spt:3850.0,3413.1')] ).
cnf(3853,plain,
( equal(i_1129,i6)
| equal(select(a_1111,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[3852,666]),
[iquote('22:SpR:3852.0,666.1')] ).
cnf(3924,plain,
equal(i_1129,i15),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[3693]),
[iquote('23:Spt:3693.0')] ).
cnf(3948,plain,
equal(select(a_1083,i15),e_1130),
inference(rew,[status(thm),theory(equality)],[3924,3692]),
[iquote('23:Rew:3924.0,3692.0')] ).
cnf(3981,plain,
( equal(i15,i6)
| equal(select(a_1111,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[3924,3853]),
[iquote('23:Rew:3924.0,3853.0')] ).
cnf(3982,plain,
equal(e_1130,e15),
inference(rew,[status(thm),theory(equality)],[613,3948]),
[iquote('23:Rew:613.0,3948.0')] ).
cnf(3983,plain,
~ equal(e_1131,e15),
inference(rew,[status(thm),theory(equality)],[3982,501]),
[iquote('23:Rew:3982.0,501.0')] ).
cnf(4001,plain,
( equal(i15,i6)
| equal(select(a_1111,i15),e_1131) ),
inference(rew,[status(thm),theory(equality)],[3924,3981]),
[iquote('23:Rew:3924.0,3981.1')] ).
cnf(4002,plain,
equal(select(a_1111,i15),e_1131),
inference(mrr,[status(thm)],[4001,357]),
[iquote('23:MRR:4001.0,357.0')] ).
cnf(4075,plain,
( equal(i21,i15)
| equal(select(a_1110,i15),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4002,668]),
[iquote('23:SpR:4002.0,668.1')] ).
cnf(4076,plain,
equal(select(a_1110,i15),e_1131),
inference(mrr,[status(thm)],[4075,180]),
[iquote('23:MRR:4075.0,180.0')] ).
cnf(4078,plain,
( equal(i15,i8)
| equal(select(a_1109,i15),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4076,670]),
[iquote('23:SpR:4076.0,670.1')] ).
cnf(4079,plain,
equal(select(a_1109,i15),e_1131),
inference(mrr,[status(thm)],[4078,312]),
[iquote('23:MRR:4078.0,312.0')] ).
cnf(4081,plain,
( equal(i20,i15)
| equal(select(a_1108,i15),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4079,672]),
[iquote('23:SpR:4079.0,672.1')] ).
cnf(4082,plain,
equal(select(a_1108,i15),e_1131),
inference(mrr,[status(thm)],[4081,181]),
[iquote('23:MRR:4081.0,181.0')] ).
cnf(4084,plain,
( equal(i18,i15)
| equal(select(a_1107,i15),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4082,674]),
[iquote('23:SpR:4082.0,674.1')] ).
cnf(4085,plain,
equal(select(a_1107,i15),e_1131),
inference(mrr,[status(thm)],[4084,183]),
[iquote('23:MRR:4084.0,183.0')] ).
cnf(4087,plain,
( equal(i25,i15)
| equal(select(a_1106,i15),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4085,676]),
[iquote('23:SpR:4085.0,676.1')] ).
cnf(4088,plain,
( equal(i25,i15)
| equal(e_1131,e15) ),
inference(rew,[status(thm),theory(equality)],[612,4087]),
[iquote('23:Rew:612.0,4087.1')] ).
cnf(4089,plain,
$false,
inference(mrr,[status(thm)],[4088,176,3983]),
[iquote('23:MRR:4088.0,4088.1,176.0,3983.0')] ).
cnf(4090,plain,
~ equal(i_1129,i15),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[4089,3924]),
[iquote('23:Spt:4089.0,3693.0,3924.0')] ).
cnf(4091,plain,
equal(select(a_1082,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[3693]),
[iquote('23:Spt:4089.0,3693.1')] ).
cnf(4092,plain,
( equal(i_1129,i14)
| equal(select(a_1081,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4091,663]),
[iquote('23:SpR:4091.0,663.1')] ).
cnf(4094,plain,
equal(select(a_1081,i_1129),e_1130),
inference(mrr,[status(thm)],[4092,3411]),
[iquote('23:MRR:4092.0,3411.0')] ).
cnf(4166,plain,
( equal(i_1129,i13)
| equal(select(a_1080,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4094,693]),
[iquote('23:SpR:4094.0,693.1')] ).
cnf(4168,plain,
equal(i_1129,i6),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[3853]),
[iquote('24:Spt:3853.0')] ).
cnf(4226,plain,
equal(select(a_1112,i6),e_1131),
inference(rew,[status(thm),theory(equality)],[4168,3852]),
[iquote('24:Rew:4168.0,3852.0')] ).
cnf(4228,plain,
( equal(i13,i6)
| equal(select(a_1080,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[4168,4166]),
[iquote('24:Rew:4168.0,4166.0')] ).
cnf(4229,plain,
equal(e_1131,e6),
inference(rew,[status(thm),theory(equality)],[600,4226]),
[iquote('24:Rew:600.0,4226.0')] ).
cnf(4230,plain,
~ equal(e_1130,e6),
inference(rew,[status(thm),theory(equality)],[4229,501]),
[iquote('24:Rew:4229.0,501.0')] ).
cnf(4249,plain,
( equal(i13,i6)
| equal(select(a_1080,i6),e_1130) ),
inference(rew,[status(thm),theory(equality)],[4168,4228]),
[iquote('24:Rew:4168.0,4228.1')] ).
cnf(4250,plain,
equal(select(a_1080,i6),e_1130),
inference(mrr,[status(thm)],[4249,359]),
[iquote('24:MRR:4249.0,359.0')] ).
cnf(4327,plain,
( equal(i12,i6)
| equal(select(a_1079,i6),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4250,649]),
[iquote('24:SpR:4250.0,649.1')] ).
cnf(4328,plain,
equal(select(a_1079,i6),e_1130),
inference(mrr,[status(thm)],[4327,360]),
[iquote('24:MRR:4327.0,360.0')] ).
cnf(4330,plain,
( equal(i11,i6)
| equal(select(a_1078,i6),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4328,665]),
[iquote('24:SpR:4328.0,665.1')] ).
cnf(4331,plain,
equal(select(a_1078,i6),e_1130),
inference(mrr,[status(thm)],[4330,361]),
[iquote('24:MRR:4330.0,361.0')] ).
cnf(4333,plain,
( equal(i10,i6)
| equal(select(a_1077,i6),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4331,635]),
[iquote('24:SpR:4331.0,635.1')] ).
cnf(4334,plain,
equal(select(a_1077,i6),e_1130),
inference(mrr,[status(thm)],[4333,362]),
[iquote('24:MRR:4333.0,362.0')] ).
cnf(4336,plain,
( equal(i9,i6)
| equal(select(a_1076,i6),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4334,685]),
[iquote('24:SpR:4334.0,685.1')] ).
cnf(4337,plain,
equal(select(a_1076,i6),e_1130),
inference(mrr,[status(thm)],[4336,363]),
[iquote('24:MRR:4336.0,363.0')] ).
cnf(4339,plain,
( equal(i8,i6)
| equal(select(a_1075,i6),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4337,671]),
[iquote('24:SpR:4337.0,671.1')] ).
cnf(4340,plain,
equal(select(a_1075,i6),e_1130),
inference(mrr,[status(thm)],[4339,364]),
[iquote('24:MRR:4339.0,364.0')] ).
cnf(4342,plain,
( equal(i7,i6)
| equal(select(a_1074,i6),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4340,637]),
[iquote('24:SpR:4340.0,637.1')] ).
cnf(4343,plain,
( equal(i7,i6)
| equal(e_1130,e6) ),
inference(rew,[status(thm),theory(equality)],[601,4342]),
[iquote('24:Rew:601.0,4342.1')] ).
cnf(4344,plain,
$false,
inference(mrr,[status(thm)],[4343,365,4230]),
[iquote('24:MRR:4343.0,4343.1,365.0,4230.0')] ).
cnf(4345,plain,
~ equal(i_1129,i6),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[4344,4168]),
[iquote('24:Spt:4344.0,3853.0,4168.0')] ).
cnf(4346,plain,
equal(select(a_1111,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[3853]),
[iquote('24:Spt:4344.0,3853.1')] ).
cnf(4347,plain,
( equal(i_1129,i21)
| equal(select(a_1110,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4346,668]),
[iquote('24:SpR:4346.0,668.1')] ).
cnf(4349,plain,
equal(select(a_1110,i_1129),e_1131),
inference(mrr,[status(thm)],[4347,2581]),
[iquote('24:MRR:4347.0,2581.0')] ).
cnf(4425,plain,
( equal(i_1129,i8)
| equal(select(a_1109,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4349,670]),
[iquote('24:SpR:4349.0,670.1')] ).
cnf(4427,plain,
equal(i_1129,i13),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[4166]),
[iquote('25:Spt:4166.0')] ).
cnf(4453,plain,
equal(select(a_1081,i13),e_1130),
inference(rew,[status(thm),theory(equality)],[4427,4094]),
[iquote('25:Rew:4427.0,4094.0')] ).
cnf(4490,plain,
( equal(i13,i8)
| equal(select(a_1109,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[4427,4425]),
[iquote('25:Rew:4427.0,4425.0')] ).
cnf(4491,plain,
equal(e_1130,e13),
inference(rew,[status(thm),theory(equality)],[627,4453]),
[iquote('25:Rew:627.0,4453.0')] ).
cnf(4492,plain,
~ equal(e_1131,e13),
inference(rew,[status(thm),theory(equality)],[4491,501]),
[iquote('25:Rew:4491.0,501.0')] ).
cnf(4512,plain,
( equal(i13,i8)
| equal(select(a_1109,i13),e_1131) ),
inference(rew,[status(thm),theory(equality)],[4427,4490]),
[iquote('25:Rew:4427.0,4490.1')] ).
cnf(4513,plain,
equal(select(a_1109,i13),e_1131),
inference(mrr,[status(thm)],[4512,314]),
[iquote('25:MRR:4512.0,314.0')] ).
cnf(4594,plain,
( equal(i20,i13)
| equal(select(a_1108,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4513,672]),
[iquote('25:SpR:4513.0,672.1')] ).
cnf(4595,plain,
equal(select(a_1108,i13),e_1131),
inference(mrr,[status(thm)],[4594,212]),
[iquote('25:MRR:4594.0,212.0')] ).
cnf(4597,plain,
( equal(i18,i13)
| equal(select(a_1107,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4595,674]),
[iquote('25:SpR:4595.0,674.1')] ).
cnf(4598,plain,
equal(select(a_1107,i13),e_1131),
inference(mrr,[status(thm)],[4597,214]),
[iquote('25:MRR:4597.0,214.0')] ).
cnf(4600,plain,
( equal(i25,i13)
| equal(select(a_1106,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4598,676]),
[iquote('25:SpR:4598.0,676.1')] ).
cnf(4601,plain,
equal(select(a_1106,i13),e_1131),
inference(mrr,[status(thm)],[4600,207]),
[iquote('25:MRR:4600.0,207.0')] ).
cnf(4603,plain,
( equal(i15,i13)
| equal(select(a_1105,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4601,678]),
[iquote('25:SpR:4601.0,678.1')] ).
cnf(4604,plain,
equal(select(a_1105,i13),e_1131),
inference(mrr,[status(thm)],[4603,217]),
[iquote('25:MRR:4603.0,217.0')] ).
cnf(4606,plain,
( equal(i13,i2)
| equal(select(a_1104,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4604,680]),
[iquote('25:SpR:4604.0,680.1')] ).
cnf(4607,plain,
equal(select(a_1104,i13),e_1131),
inference(mrr,[status(thm)],[4606,461]),
[iquote('25:MRR:4606.0,461.0')] ).
cnf(4609,plain,
( equal(i30,i13)
| equal(select(a_1103,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4607,682]),
[iquote('25:SpR:4607.0,682.1')] ).
cnf(4610,plain,
equal(select(a_1103,i13),e_1131),
inference(mrr,[status(thm)],[4609,202]),
[iquote('25:MRR:4609.0,202.0')] ).
cnf(4612,plain,
( equal(i13,i9)
| equal(select(a_1102,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4610,684]),
[iquote('25:SpR:4610.0,684.1')] ).
cnf(4613,plain,
equal(select(a_1102,i13),e_1131),
inference(mrr,[status(thm)],[4612,293]),
[iquote('25:MRR:4612.0,293.0')] ).
cnf(4615,plain,
( equal(i13,i4)
| equal(select(a_1101,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4613,686]),
[iquote('25:SpR:4613.0,686.1')] ).
cnf(4616,plain,
equal(select(a_1101,i13),e_1131),
inference(mrr,[status(thm)],[4615,408]),
[iquote('25:MRR:4615.0,408.0')] ).
cnf(4618,plain,
( equal(i19,i13)
| equal(select(a_1100,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4616,688]),
[iquote('25:SpR:4616.0,688.1')] ).
cnf(4619,plain,
equal(select(a_1100,i13),e_1131),
inference(mrr,[status(thm)],[4618,213]),
[iquote('25:MRR:4618.0,213.0')] ).
cnf(4621,plain,
( equal(i13,i1)
| equal(select(a_1099,i13),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4619,690]),
[iquote('25:SpR:4619.0,690.1')] ).
cnf(4622,plain,
( equal(i13,i1)
| equal(e_1131,e13) ),
inference(rew,[status(thm),theory(equality)],[626,4621]),
[iquote('25:Rew:626.0,4621.1')] ).
cnf(4623,plain,
$false,
inference(mrr,[status(thm)],[4622,489,4492]),
[iquote('25:MRR:4622.0,4622.1,489.0,4492.0')] ).
cnf(4624,plain,
~ equal(i_1129,i13),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[4623,4427]),
[iquote('25:Spt:4623.0,4166.0,4427.0')] ).
cnf(4625,plain,
equal(select(a_1080,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[4166]),
[iquote('25:Spt:4623.0,4166.1')] ).
cnf(4626,plain,
( equal(i_1129,i12)
| equal(select(a_1079,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4625,649]),
[iquote('25:SpR:4625.0,649.1')] ).
cnf(4628,plain,
equal(select(a_1079,i_1129),e_1130),
inference(mrr,[status(thm)],[4626,1975]),
[iquote('25:MRR:4626.0,1975.0')] ).
cnf(4708,plain,
( equal(i_1129,i11)
| equal(select(a_1078,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4628,665]),
[iquote('25:SpR:4628.0,665.1')] ).
cnf(4710,plain,
equal(select(a_1078,i_1129),e_1130),
inference(mrr,[status(thm)],[4708,3851]),
[iquote('25:MRR:4708.0,3851.0')] ).
cnf(4711,plain,
( equal(i_1129,i10)
| equal(select(a_1077,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4710,635]),
[iquote('25:SpR:4710.0,635.1')] ).
cnf(4713,plain,
equal(select(a_1077,i_1129),e_1130),
inference(mrr,[status(thm)],[4711,946]),
[iquote('25:MRR:4711.0,946.0')] ).
cnf(4714,plain,
( equal(i_1129,i9)
| equal(select(a_1076,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[4713,685]),
[iquote('25:SpR:4713.0,685.1')] ).
cnf(4716,plain,
equal(i_1129,i8),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[4425]),
[iquote('26:Spt:4425.0')] ).
cnf(4743,plain,
equal(select(a_1110,i8),e_1131),
inference(rew,[status(thm),theory(equality)],[4716,4349]),
[iquote('26:Rew:4716.0,4349.0')] ).
cnf(4784,plain,
( equal(i9,i8)
| equal(select(a_1076,i_1129),e_1130) ),
inference(rew,[status(thm),theory(equality)],[4716,4714]),
[iquote('26:Rew:4716.0,4714.0')] ).
cnf(4785,plain,
equal(e_1131,e8),
inference(rew,[status(thm),theory(equality)],[604,4743]),
[iquote('26:Rew:604.0,4743.0')] ).
cnf(4786,plain,
~ equal(e_1130,e8),
inference(rew,[status(thm),theory(equality)],[4785,501]),
[iquote('26:Rew:4785.0,501.0')] ).
cnf(4807,plain,
( equal(i9,i8)
| equal(select(a_1076,i8),e_1130) ),
inference(rew,[status(thm),theory(equality)],[4716,4784]),
[iquote('26:Rew:4716.0,4784.1')] ).
cnf(4808,plain,
( equal(i9,i8)
| equal(e_1130,e8) ),
inference(rew,[status(thm),theory(equality)],[605,4807]),
[iquote('26:Rew:605.0,4807.1')] ).
cnf(4809,plain,
equal(e_1130,e8),
inference(mrr,[status(thm)],[4808,318]),
[iquote('26:MRR:4808.0,318.0')] ).
cnf(4810,plain,
$false,
inference(mrr,[status(thm)],[4809,4786]),
[iquote('26:MRR:4809.0,4786.0')] ).
cnf(4811,plain,
~ equal(i_1129,i8),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[4810,4716]),
[iquote('26:Spt:4810.0,4425.0,4716.0')] ).
cnf(4812,plain,
equal(select(a_1109,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[4425]),
[iquote('26:Spt:4810.0,4425.1')] ).
cnf(4813,plain,
( equal(i_1129,i20)
| equal(select(a_1108,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4812,672]),
[iquote('26:SpR:4812.0,672.1')] ).
cnf(4815,plain,
equal(select(a_1108,i_1129),e_1131),
inference(mrr,[status(thm)],[4813,2985]),
[iquote('26:MRR:4813.0,2985.0')] ).
cnf(4903,plain,
( equal(i_1129,i18)
| equal(select(a_1107,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4815,674]),
[iquote('26:SpR:4815.0,674.1')] ).
cnf(4905,plain,
equal(select(a_1107,i_1129),e_1131),
inference(mrr,[status(thm)],[4903,3622]),
[iquote('26:MRR:4903.0,3622.0')] ).
cnf(4906,plain,
( equal(i_1129,i25)
| equal(select(a_1106,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4905,676]),
[iquote('26:SpR:4905.0,676.1')] ).
cnf(4908,plain,
equal(select(a_1106,i_1129),e_1131),
inference(mrr,[status(thm)],[4906,2121]),
[iquote('26:MRR:4906.0,2121.0')] ).
cnf(4909,plain,
( equal(i_1129,i15)
| equal(select(a_1105,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4908,678]),
[iquote('26:SpR:4908.0,678.1')] ).
cnf(4911,plain,
equal(select(a_1105,i_1129),e_1131),
inference(mrr,[status(thm)],[4909,4090]),
[iquote('26:MRR:4909.0,4090.0')] ).
cnf(4912,plain,
( equal(i_1129,i2)
| equal(select(a_1104,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[4911,680]),
[iquote('26:SpR:4911.0,680.1')] ).
cnf(4914,plain,
equal(i_1129,i9),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[4714]),
[iquote('27:Spt:4714.0')] ).
cnf(4942,plain,
equal(select(a_1077,i9),e_1130),
inference(rew,[status(thm),theory(equality)],[4914,4713]),
[iquote('27:Rew:4914.0,4713.0')] ).
cnf(4988,plain,
( equal(i9,i2)
| equal(select(a_1104,i_1129),e_1131) ),
inference(rew,[status(thm),theory(equality)],[4914,4912]),
[iquote('27:Rew:4914.0,4912.0')] ).
cnf(4989,plain,
equal(e_1130,e9),
inference(rew,[status(thm),theory(equality)],[619,4942]),
[iquote('27:Rew:619.0,4942.0')] ).
cnf(4990,plain,
~ equal(e_1131,e9),
inference(rew,[status(thm),theory(equality)],[4989,501]),
[iquote('27:Rew:4989.0,501.0')] ).
cnf(5014,plain,
( equal(i9,i2)
| equal(select(a_1104,i9),e_1131) ),
inference(rew,[status(thm),theory(equality)],[4914,4988]),
[iquote('27:Rew:4914.0,4988.1')] ).
cnf(5015,plain,
equal(select(a_1104,i9),e_1131),
inference(mrr,[status(thm)],[5014,465]),
[iquote('27:MRR:5014.0,465.0')] ).
cnf(5114,plain,
( equal(i30,i9)
| equal(select(a_1103,i9),e_1131) ),
inference(spr,[status(thm),theory(equality)],[5015,682]),
[iquote('27:SpR:5015.0,682.1')] ).
cnf(5115,plain,
( equal(i30,i9)
| equal(e_1131,e9) ),
inference(rew,[status(thm),theory(equality)],[618,5114]),
[iquote('27:Rew:618.0,5114.1')] ).
cnf(5116,plain,
$false,
inference(mrr,[status(thm)],[5115,276,4990]),
[iquote('27:MRR:5115.0,5115.1,276.0,4990.0')] ).
cnf(5117,plain,
~ equal(i_1129,i9),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[5116,4914]),
[iquote('27:Spt:5116.0,4714.0,4914.0')] ).
cnf(5118,plain,
equal(select(a_1076,i_1129),e_1130),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[4714]),
[iquote('27:Spt:5116.0,4714.1')] ).
cnf(5119,plain,
( equal(i_1129,i8)
| equal(select(a_1075,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5118,671]),
[iquote('27:SpR:5118.0,671.1')] ).
cnf(5121,plain,
equal(select(a_1075,i_1129),e_1130),
inference(mrr,[status(thm)],[5119,4811]),
[iquote('27:MRR:5119.0,4811.0')] ).
cnf(5219,plain,
( equal(i_1129,i7)
| equal(select(a_1074,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5121,637]),
[iquote('27:SpR:5121.0,637.1')] ).
cnf(5221,plain,
equal(select(a_1074,i_1129),e_1130),
inference(mrr,[status(thm)],[5219,1047]),
[iquote('27:MRR:5219.0,1047.0')] ).
cnf(5222,plain,
equal(i_1129,i2),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[4912]),
[iquote('28:Spt:4912.0')] ).
cnf(5252,plain,
equal(select(a_1105,i2),e_1131),
inference(rew,[status(thm),theory(equality)],[5222,4911]),
[iquote('28:Rew:5222.0,4911.0')] ).
cnf(5299,plain,
equal(select(a_1074,i2),e_1130),
inference(rew,[status(thm),theory(equality)],[5222,5221]),
[iquote('28:Rew:5222.0,5221.0')] ).
cnf(5300,plain,
equal(e_1131,e2),
inference(rew,[status(thm),theory(equality)],[614,5252]),
[iquote('28:Rew:614.0,5252.0')] ).
cnf(5301,plain,
~ equal(e_1130,e2),
inference(rew,[status(thm),theory(equality)],[5300,501]),
[iquote('28:Rew:5300.0,501.0')] ).
cnf(5429,plain,
( equal(i6,i2)
| equal(select(a_1073,i2),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5299,667]),
[iquote('28:SpR:5299.0,667.1')] ).
cnf(5430,plain,
equal(select(a_1073,i2),e_1130),
inference(mrr,[status(thm)],[5429,468]),
[iquote('28:MRR:5429.0,468.0')] ).
cnf(5432,plain,
( equal(i5,i2)
| equal(select(a_1072,i2),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5430,659]),
[iquote('28:SpR:5430.0,659.1')] ).
cnf(5433,plain,
equal(select(a_1072,i2),e_1130),
inference(mrr,[status(thm)],[5432,469]),
[iquote('28:MRR:5432.0,469.0')] ).
cnf(5435,plain,
( equal(i4,i2)
| equal(select(a_1071,i2),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5433,687]),
[iquote('28:SpR:5433.0,687.1')] ).
cnf(5436,plain,
equal(select(a_1071,i2),e_1130),
inference(mrr,[status(thm)],[5435,470]),
[iquote('28:MRR:5435.0,470.0')] ).
cnf(5438,plain,
( equal(i3,i2)
| equal(select(a_1070,i2),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5436,651]),
[iquote('28:SpR:5436.0,651.1')] ).
cnf(5439,plain,
( equal(i3,i2)
| equal(e_1130,e2) ),
inference(rew,[status(thm),theory(equality)],[615,5438]),
[iquote('28:Rew:615.0,5438.1')] ).
cnf(5440,plain,
$false,
inference(mrr,[status(thm)],[5439,471,5301]),
[iquote('28:MRR:5439.0,5439.1,471.0,5301.0')] ).
cnf(5441,plain,
~ equal(i_1129,i2),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[5440,5222]),
[iquote('28:Spt:5440.0,4912.0,5222.0')] ).
cnf(5442,plain,
equal(select(a_1104,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[4912]),
[iquote('28:Spt:5440.0,4912.1')] ).
cnf(5443,plain,
( equal(i_1129,i30)
| equal(select(a_1103,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[5442,682]),
[iquote('28:SpR:5442.0,682.1')] ).
cnf(5445,plain,
equal(select(a_1103,i_1129),e_1131),
inference(mrr,[status(thm)],[5443,1152]),
[iquote('28:MRR:5443.0,1152.0')] ).
cnf(5547,plain,
( equal(i_1129,i6)
| equal(select(a_1073,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5221,667]),
[iquote('27:SpR:5221.0,667.1')] ).
cnf(5549,plain,
equal(select(a_1073,i_1129),e_1130),
inference(mrr,[status(thm)],[5547,4345]),
[iquote('27:MRR:5547.0,4345.0')] ).
cnf(5550,plain,
( equal(i_1129,i9)
| equal(select(a_1102,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[5445,684]),
[iquote('28:SpR:5445.0,684.1')] ).
cnf(5552,plain,
equal(select(a_1102,i_1129),e_1131),
inference(mrr,[status(thm)],[5550,5117]),
[iquote('28:MRR:5550.0,5117.0')] ).
cnf(5553,plain,
( equal(i_1129,i5)
| equal(select(a_1072,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5549,659]),
[iquote('27:SpR:5549.0,659.1')] ).
cnf(5555,plain,
equal(select(a_1072,i_1129),e_1130),
inference(mrr,[status(thm)],[5553,2793]),
[iquote('27:MRR:5553.0,2793.0')] ).
cnf(5556,plain,
( equal(i_1129,i4)
| equal(select(a_1101,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[5552,686]),
[iquote('28:SpR:5552.0,686.1')] ).
cnf(5558,plain,
( equal(i_1129,i4)
| equal(select(a_1071,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5555,687]),
[iquote('27:SpR:5555.0,687.1')] ).
cnf(5560,plain,
equal(i_1129,i4),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[5556]),
[iquote('29:Spt:5556.0')] ).
cnf(5642,plain,
equal(select(a_1102,i4),e_1131),
inference(rew,[status(thm),theory(equality)],[5560,5552]),
[iquote('29:Rew:5560.0,5552.0')] ).
cnf(5643,plain,
equal(select(a_1072,i4),e_1130),
inference(rew,[status(thm),theory(equality)],[5560,5555]),
[iquote('29:Rew:5560.0,5555.0')] ).
cnf(5644,plain,
equal(e_1131,e4),
inference(rew,[status(thm),theory(equality)],[620,5642]),
[iquote('29:Rew:620.0,5642.0')] ).
cnf(5645,plain,
~ equal(e_1130,e4),
inference(rew,[status(thm),theory(equality)],[5644,501]),
[iquote('29:Rew:5644.0,501.0')] ).
cnf(5674,plain,
equal(e_1130,e4),
inference(rew,[status(thm),theory(equality)],[621,5643]),
[iquote('29:Rew:621.0,5643.0')] ).
cnf(5675,plain,
$false,
inference(mrr,[status(thm)],[5674,5645]),
[iquote('29:MRR:5674.0,5645.0')] ).
cnf(5676,plain,
~ equal(i_1129,i4),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[5675,5560]),
[iquote('29:Spt:5675.0,5556.0,5560.0')] ).
cnf(5677,plain,
equal(select(a_1101,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[5556]),
[iquote('29:Spt:5675.0,5556.1')] ).
cnf(5678,plain,
equal(select(a_1071,i_1129),e_1130),
inference(mrr,[status(thm)],[5558,5676]),
[iquote('29:MRR:5558.0,5676.0')] ).
cnf(5679,plain,
( equal(i_1129,i19)
| equal(select(a_1100,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[5677,688]),
[iquote('29:SpR:5677.0,688.1')] ).
cnf(5681,plain,
equal(select(a_1100,i_1129),e_1131),
inference(mrr,[status(thm)],[5679,3207]),
[iquote('29:MRR:5679.0,3207.0')] ).
cnf(5795,plain,
( equal(i_1129,i3)
| equal(select(a_1070,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5678,651]),
[iquote('29:SpR:5678.0,651.1')] ).
cnf(5797,plain,
equal(select(a_1070,i_1129),e_1130),
inference(mrr,[status(thm)],[5795,2308]),
[iquote('29:MRR:5795.0,2308.0')] ).
cnf(5798,plain,
( equal(i_1129,i1)
| equal(select(a_1099,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[5681,690]),
[iquote('29:SpR:5681.0,690.1')] ).
cnf(5800,plain,
( equal(i_1129,i2)
| equal(select(a_1069,i_1129),e_1130) ),
inference(spr,[status(thm),theory(equality)],[5797,681]),
[iquote('29:SpR:5797.0,681.1')] ).
cnf(5802,plain,
equal(select(a_1069,i_1129),e_1130),
inference(mrr,[status(thm)],[5800,5441]),
[iquote('29:MRR:5800.0,5441.0')] ).
cnf(5804,plain,
equal(i_1129,i1),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s1)])],[5798]),
[iquote('30:Spt:5798.0')] ).
cnf(5891,plain,
equal(select(a_1100,i1),e_1131),
inference(rew,[status(thm),theory(equality)],[5804,5681]),
[iquote('30:Rew:5804.0,5681.0')] ).
cnf(5893,plain,
equal(select(a_1069,i1),e_1130),
inference(rew,[status(thm),theory(equality)],[5804,5802]),
[iquote('30:Rew:5804.0,5802.0')] ).
cnf(5894,plain,
equal(e_1131,e1),
inference(rew,[status(thm),theory(equality)],[624,5891]),
[iquote('30:Rew:624.0,5891.0')] ).
cnf(5895,plain,
~ equal(e_1130,e1),
inference(rew,[status(thm),theory(equality)],[5894,501]),
[iquote('30:Rew:5894.0,501.0')] ).
cnf(5926,plain,
equal(e_1130,e1),
inference(rew,[status(thm),theory(equality)],[625,5893]),
[iquote('30:Rew:625.0,5893.0')] ).
cnf(5927,plain,
$false,
inference(mrr,[status(thm)],[5926,5895]),
[iquote('30:MRR:5926.0,5895.0')] ).
cnf(5928,plain,
~ equal(i_1129,i1),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2sa)])],[5927,5804]),
[iquote('30:Spt:5927.0,5798.0,5804.0')] ).
cnf(5929,plain,
equal(select(a_1099,i_1129),e_1131),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2s2)])],[5798]),
[iquote('30:Spt:5927.0,5798.1')] ).
cnf(5930,plain,
( equal(i_1129,i13)
| equal(select(a1,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[5929,692]),
[iquote('30:SpR:5929.0,692.1')] ).
cnf(5932,plain,
equal(select(a1,i_1129),e_1131),
inference(mrr,[status(thm)],[5930,4624]),
[iquote('30:MRR:5930.0,4624.0')] ).
cnf(6055,plain,
( equal(i_1129,i1)
| equal(select(a_1069,i_1129),e_1131) ),
inference(spr,[status(thm),theory(equality)],[5932,691]),
[iquote('30:SpR:5932.0,691.1')] ).
cnf(6057,plain,
( equal(i_1129,i1)
| equal(e_1131,e_1130) ),
inference(rew,[status(thm),theory(equality)],[5802,6055]),
[iquote('30:Rew:5802.0,6055.1')] ).
cnf(6058,plain,
$false,
inference(mrr,[status(thm)],[6057,5928,501]),
[iquote('30:MRR:6057.0,6057.1,5928.0,501.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.07 % Problem : SWV505-1.030 : TPTP v8.1.0. Released v4.0.0.
% 0.01/0.07 % Command : run_spass %d %s
% 0.06/0.26 % Computer : n016.cluster.edu
% 0.06/0.26 % Model : x86_64 x86_64
% 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.26 % Memory : 8042.1875MB
% 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.26 % CPULimit : 300
% 0.06/0.26 % WCLimit : 600
% 0.06/0.26 % DateTime : Wed Jun 15 00:24:16 EDT 2022
% 0.06/0.26 % CPUTime :
% 0.85/1.06
% 0.85/1.06 SPASS V 3.9
% 0.85/1.06 SPASS beiseite: Proof found.
% 0.85/1.06 % SZS status Theorem
% 0.85/1.06 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.85/1.06 SPASS derived 4995 clauses, backtracked 1332 clauses, performed 30 splits and kept 3255 clauses.
% 0.85/1.06 SPASS allocated 66154 KBytes.
% 0.85/1.06 SPASS spent 0:00:00.79 on the problem.
% 0.85/1.06 0:00:00.04 for the input.
% 0.85/1.06 0:00:00.00 for the FLOTTER CNF translation.
% 0.85/1.06 0:00:00.12 for inferences.
% 0.85/1.06 0:00:00.03 for the backtracking.
% 0.85/1.06 0:00:00.46 for the reduction.
% 0.85/1.06
% 0.85/1.06
% 0.85/1.06 Here is a proof with depth 48, length 1241 :
% 0.85/1.06 % SZS output start Refutation
% See solution above
% 0.85/1.09 Formulae used in the proof : a1 a2 hyp0 hyp1 hyp2 hyp3 hyp4 hyp5 hyp6 hyp7 hyp8 hyp9 hyp10 hyp11 hyp12 hyp13 hyp14 hyp15 hyp16 hyp17 hyp18 hyp19 hyp20 hyp21 hyp22 hyp23 hyp24 hyp25 hyp26 hyp27 hyp28 hyp29 hyp30 hyp31 hyp32 hyp33 hyp34 hyp35 hyp36 hyp37 hyp38 hyp39 hyp40 hyp41 hyp42 hyp43 hyp44 hyp45 hyp46 hyp47 hyp48 hyp49 hyp50 hyp51 hyp52 hyp53 hyp54 hyp55 hyp56 hyp57 hyp58 hyp59 hyp60 hyp61 hyp63 hyp64 hyp65 hyp66 hyp67 hyp69 hyp70 hyp72 hyp73 hyp74 hyp76 hyp77 hyp78 hyp79 hyp80 hyp81 hyp82 hyp83 hyp84 hyp85 hyp86 hyp87 hyp88 hyp89 hyp90 hyp91 hyp92 hyp95 hyp96 hyp99 hyp100 hyp104 hyp108 hyp113 hyp117 hyp118 hyp123 hyp127 hyp128 hyp129 hyp134 hyp138 hyp139 hyp140 hyp141 hyp142 hyp143 hyp144 hyp145 hyp146 hyp147 hyp148 hyp149 hyp150 hyp151 hyp152 hyp153 hyp154 hyp155 hyp157 hyp158 hyp159 hyp160 hyp161 hyp162 hyp163 hyp164 hyp165 hyp166 hyp167 hyp168 hyp173 hyp177 hyp178 hyp179 hyp180 hyp183 hyp188 hyp192 hyp193 hyp194 hyp195 hyp196 hyp197 hyp198 hyp199 hyp204 hyp209 hyp210 hyp211 hyp214 hyp216 hyp217 hyp219 hyp220 hyp221 hyp222 hyp223 hyp224 hyp225 hyp226 hyp227 hyp228 hyp229 hyp230 hyp231 hyp232 hyp233 hyp234 hyp239 hyp243 hyp244 hyp245 hyp246 hyp249 hyp250 hyp251 hyp252 hyp253 hyp254 hyp255 hyp256 hyp257 hyp258 hyp259 hyp260 hyp261 hyp262 hyp263 hyp264 hyp265 hyp266 hyp267 hyp268 hyp269 hyp270 hyp271 hyp272 hyp273 hyp284 hyp290 hyp294 hyp299 hyp304 hyp305 hyp306 hyp309 hyp311 hyp315 hyp316 hyp317 hyp318 hyp319 hyp320 hyp321 hyp322 hyp323 hyp324 hyp325 hyp326 hyp327 hyp328 hyp329 hyp330 hyp331 hyp332 hyp333 hyp334 hyp335 hyp336 hyp337 hyp338 hyp339 hyp344 hyp348 hyp349 hyp350 hyp351 hyp354 hyp356 hyp357 hyp358 hyp359 hyp360 hyp361 hyp362 hyp363 hyp364 hyp368 hyp372 hyp373 hyp374 hyp375 hyp376 hyp377 hyp378 hyp379 hyp380 hyp381 hyp382 hyp383 hyp384 hyp385 hyp386 hyp387 hyp399 hyp405 hyp414 hyp415 hyp417 hyp418 hyp419 hyp422 hyp423 hyp424 hyp425 hyp426 hyp427 hyp428 hyp429 hyp430 hyp431 hyp432 hyp433 hyp434 hyp435 hyp436 hyp437 hyp438 hyp439 hyp440 hyp441 hyp452 hyp458 hyp462 hyp465 hyp466 hyp467 hyp468 hyp486 goal
% 0.85/1.09
%------------------------------------------------------------------------------