%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG209+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n023.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 : Thu Jul 14 18:02:58 EDT 2022
% Result : Theorem 0.75s 0.93s
% Output : Refutation 0.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 199
% Syntax : Number of clauses : 498 ( 199 unt; 2 nHn; 498 RR)
% Number of literals : 1335 ( 0 equ; 839 neg)
% Maximal clause size : 198 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 150 ( 149 usr; 149 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(21,axiom,
~ equal(e6,e5),
file('ALG209+1.p',unknown),
[] ).
cnf(22,axiom,
equal(op(e0,e0),e2),
file('ALG209+1.p',unknown),
[] ).
cnf(23,axiom,
equal(op(e0,e1),e0),
file('ALG209+1.p',unknown),
[] ).
cnf(24,axiom,
equal(op(e0,e2),e1),
file('ALG209+1.p',unknown),
[] ).
cnf(25,axiom,
equal(op(e0,e3),e5),
file('ALG209+1.p',unknown),
[] ).
cnf(26,axiom,
equal(op(e0,e4),e3),
file('ALG209+1.p',unknown),
[] ).
cnf(27,axiom,
equal(op(e0,e5),e4),
file('ALG209+1.p',unknown),
[] ).
cnf(28,axiom,
equal(op(e0,e6),e6),
file('ALG209+1.p',unknown),
[] ).
cnf(29,axiom,
equal(op(e1,e0),e0),
file('ALG209+1.p',unknown),
[] ).
cnf(30,axiom,
equal(op(e1,e1),e6),
file('ALG209+1.p',unknown),
[] ).
cnf(31,axiom,
equal(op(e1,e2),e4),
file('ALG209+1.p',unknown),
[] ).
cnf(32,axiom,
equal(op(e1,e3),e1),
file('ALG209+1.p',unknown),
[] ).
cnf(33,axiom,
equal(op(e1,e4),e5),
file('ALG209+1.p',unknown),
[] ).
cnf(34,axiom,
equal(op(e1,e5),e2),
file('ALG209+1.p',unknown),
[] ).
cnf(35,axiom,
equal(op(e1,e6),e3),
file('ALG209+1.p',unknown),
[] ).
cnf(36,axiom,
equal(op(e2,e0),e1),
file('ALG209+1.p',unknown),
[] ).
cnf(37,axiom,
equal(op(e2,e1),e4),
file('ALG209+1.p',unknown),
[] ).
cnf(38,axiom,
equal(op(e2,e2),e3),
file('ALG209+1.p',unknown),
[] ).
cnf(39,axiom,
equal(op(e2,e3),e6),
file('ALG209+1.p',unknown),
[] ).
cnf(40,axiom,
equal(op(e2,e4),e0),
file('ALG209+1.p',unknown),
[] ).
cnf(41,axiom,
equal(op(e2,e5),e5),
file('ALG209+1.p',unknown),
[] ).
cnf(42,axiom,
equal(op(e2,e6),e2),
file('ALG209+1.p',unknown),
[] ).
cnf(43,axiom,
equal(op(e3,e0),e5),
file('ALG209+1.p',unknown),
[] ).
cnf(44,axiom,
equal(op(e3,e1),e1),
file('ALG209+1.p',unknown),
[] ).
cnf(45,axiom,
equal(op(e3,e2),e6),
file('ALG209+1.p',unknown),
[] ).
cnf(46,axiom,
equal(op(e3,e3),e0),
file('ALG209+1.p',unknown),
[] ).
cnf(47,axiom,
equal(op(e3,e4),e2),
file('ALG209+1.p',unknown),
[] ).
cnf(48,axiom,
equal(op(e3,e5),e3),
file('ALG209+1.p',unknown),
[] ).
cnf(49,axiom,
equal(op(e3,e6),e4),
file('ALG209+1.p',unknown),
[] ).
cnf(50,axiom,
equal(op(e4,e0),e3),
file('ALG209+1.p',unknown),
[] ).
cnf(51,axiom,
equal(op(e4,e1),e5),
file('ALG209+1.p',unknown),
[] ).
cnf(52,axiom,
equal(op(e4,e2),e0),
file('ALG209+1.p',unknown),
[] ).
cnf(53,axiom,
equal(op(e4,e3),e2),
file('ALG209+1.p',unknown),
[] ).
cnf(54,axiom,
equal(op(e4,e4),e4),
file('ALG209+1.p',unknown),
[] ).
cnf(55,axiom,
equal(op(e4,e5),e6),
file('ALG209+1.p',unknown),
[] ).
cnf(56,axiom,
equal(op(e4,e6),e1),
file('ALG209+1.p',unknown),
[] ).
cnf(57,axiom,
equal(op(e5,e0),e4),
file('ALG209+1.p',unknown),
[] ).
cnf(58,axiom,
equal(op(e5,e1),e2),
file('ALG209+1.p',unknown),
[] ).
cnf(59,axiom,
equal(op(e5,e2),e5),
file('ALG209+1.p',unknown),
[] ).
cnf(60,axiom,
equal(op(e5,e3),e3),
file('ALG209+1.p',unknown),
[] ).
cnf(61,axiom,
equal(op(e5,e4),e6),
file('ALG209+1.p',unknown),
[] ).
cnf(62,axiom,
equal(op(e5,e5),e1),
file('ALG209+1.p',unknown),
[] ).
cnf(63,axiom,
equal(op(e5,e6),e0),
file('ALG209+1.p',unknown),
[] ).
cnf(64,axiom,
equal(op(e6,e0),e6),
file('ALG209+1.p',unknown),
[] ).
cnf(65,axiom,
equal(op(e6,e1),e3),
file('ALG209+1.p',unknown),
[] ).
cnf(66,axiom,
equal(op(e6,e2),e2),
file('ALG209+1.p',unknown),
[] ).
cnf(67,axiom,
equal(op(e6,e3),e4),
file('ALG209+1.p',unknown),
[] ).
cnf(68,axiom,
equal(op(e6,e4),e1),
file('ALG209+1.p',unknown),
[] ).
cnf(69,axiom,
equal(op(e6,e5),e0),
file('ALG209+1.p',unknown),
[] ).
cnf(70,axiom,
equal(op(e6,e6),e5),
file('ALG209+1.p',unknown),
[] ).
cnf(77,axiom,
( equal(op(e6,e6),e6)
| skC1 ),
file('ALG209+1.p',unknown),
[] ).
cnf(82,axiom,
( ~ equal(op(e4,e4),e4)
| skC0 ),
file('ALG209+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ equal(op(e0,e0),e2)
| skC2 ),
file('ALG209+1.p',unknown),
[] ).
cnf(92,axiom,
( ~ equal(op(e0,e1),e0)
| skC3 ),
file('ALG209+1.p',unknown),
[] ).
cnf(100,axiom,
( ~ equal(op(e0,e2),e1)
| skC4 ),
file('ALG209+1.p',unknown),
[] ).
cnf(111,axiom,
( ~ equal(op(e0,e3),e5)
| skC5 ),
file('ALG209+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ equal(op(e0,e4),e3)
| skC6 ),
file('ALG209+1.p',unknown),
[] ).
cnf(124,axiom,
( ~ equal(op(e0,e5),e4)
| skC7 ),
file('ALG209+1.p',unknown),
[] ).
cnf(133,axiom,
( ~ equal(op(e0,e6),e6)
| skC8 ),
file('ALG209+1.p',unknown),
[] ).
cnf(134,axiom,
( ~ equal(op(e1,e0),e0)
| skC9 ),
file('ALG209+1.p',unknown),
[] ).
cnf(147,axiom,
( ~ equal(op(e1,e1),e6)
| skC10 ),
file('ALG209+1.p',unknown),
[] ).
cnf(152,axiom,
( ~ equal(op(e1,e2),e4)
| skC11 ),
file('ALG209+1.p',unknown),
[] ).
cnf(156,axiom,
( ~ equal(op(e1,e3),e1)
| skC12 ),
file('ALG209+1.p',unknown),
[] ).
cnf(167,axiom,
( ~ equal(op(e1,e4),e5)
| skC13 ),
file('ALG209+1.p',unknown),
[] ).
cnf(171,axiom,
( ~ equal(op(e1,e5),e2)
| skC14 ),
file('ALG209+1.p',unknown),
[] ).
cnf(179,axiom,
( ~ equal(op(e1,e6),e3)
| skC15 ),
file('ALG209+1.p',unknown),
[] ).
cnf(184,axiom,
( ~ equal(op(e2,e0),e1)
| skC16 ),
file('ALG209+1.p',unknown),
[] ).
cnf(194,axiom,
( ~ equal(op(e2,e1),e4)
| skC17 ),
file('ALG209+1.p',unknown),
[] ).
cnf(200,axiom,
( ~ equal(op(e2,e2),e3)
| skC18 ),
file('ALG209+1.p',unknown),
[] ).
cnf(210,axiom,
( ~ equal(op(e2,e3),e6)
| skC19 ),
file('ALG209+1.p',unknown),
[] ).
cnf(211,axiom,
( ~ equal(op(e2,e4),e0)
| skC20 ),
file('ALG209+1.p',unknown),
[] ).
cnf(223,axiom,
( ~ equal(op(e2,e5),e5)
| skC21 ),
file('ALG209+1.p',unknown),
[] ).
cnf(227,axiom,
( ~ equal(op(e2,e6),e2)
| skC22 ),
file('ALG209+1.p',unknown),
[] ).
cnf(237,axiom,
( ~ equal(op(e3,e0),e5)
| skC23 ),
file('ALG209+1.p',unknown),
[] ).
cnf(240,axiom,
( ~ equal(op(e3,e1),e1)
| skC24 ),
file('ALG209+1.p',unknown),
[] ).
cnf(252,axiom,
( ~ equal(op(e3,e2),e6)
| skC25 ),
file('ALG209+1.p',unknown),
[] ).
cnf(253,axiom,
( ~ equal(op(e3,e3),e0)
| skC26 ),
file('ALG209+1.p',unknown),
[] ).
cnf(262,axiom,
( ~ equal(op(e3,e4),e2)
| skC27 ),
file('ALG209+1.p',unknown),
[] ).
cnf(270,axiom,
( ~ equal(op(e3,e5),e3)
| skC28 ),
file('ALG209+1.p',unknown),
[] ).
cnf(278,axiom,
( ~ equal(op(e3,e6),e4)
| skC29 ),
file('ALG209+1.p',unknown),
[] ).
cnf(284,axiom,
( ~ equal(op(e4,e0),e3)
| skC30 ),
file('ALG209+1.p',unknown),
[] ).
cnf(293,axiom,
( ~ equal(op(e4,e1),e5)
| skC31 ),
file('ALG209+1.p',unknown),
[] ).
cnf(295,axiom,
( ~ equal(op(e4,e2),e0)
| skC32 ),
file('ALG209+1.p',unknown),
[] ).
cnf(304,axiom,
( ~ equal(op(e4,e3),e2)
| skC33 ),
file('ALG209+1.p',unknown),
[] ).
cnf(313,axiom,
( ~ equal(op(e4,e4),e4)
| skC34 ),
file('ALG209+1.p',unknown),
[] ).
cnf(322,axiom,
( ~ equal(op(e4,e5),e6)
| skC35 ),
file('ALG209+1.p',unknown),
[] ).
cnf(324,axiom,
( ~ equal(op(e4,e6),e1)
| skC36 ),
file('ALG209+1.p',unknown),
[] ).
cnf(334,axiom,
( ~ equal(op(e5,e0),e4)
| skC37 ),
file('ALG209+1.p',unknown),
[] ).
cnf(339,axiom,
( ~ equal(op(e5,e1),e2)
| skC38 ),
file('ALG209+1.p',unknown),
[] ).
cnf(349,axiom,
( ~ equal(op(e5,e2),e5)
| skC39 ),
file('ALG209+1.p',unknown),
[] ).
cnf(354,axiom,
( ~ equal(op(e5,e3),e3)
| skC40 ),
file('ALG209+1.p',unknown),
[] ).
cnf(364,axiom,
( ~ equal(op(e5,e4),e6)
| skC41 ),
file('ALG209+1.p',unknown),
[] ).
cnf(366,axiom,
( ~ equal(op(e5,e5),e1)
| skC42 ),
file('ALG209+1.p',unknown),
[] ).
cnf(372,axiom,
( ~ equal(op(e5,e6),e0)
| skC43 ),
file('ALG209+1.p',unknown),
[] ).
cnf(385,axiom,
( ~ equal(op(e6,e0),e6)
| skC44 ),
file('ALG209+1.p',unknown),
[] ).
cnf(389,axiom,
( ~ equal(op(e6,e1),e3)
| skC45 ),
file('ALG209+1.p',unknown),
[] ).
cnf(395,axiom,
( ~ equal(op(e6,e2),e2)
| skC46 ),
file('ALG209+1.p',unknown),
[] ).
cnf(404,axiom,
( ~ equal(op(e6,e3),e4)
| skC47 ),
file('ALG209+1.p',unknown),
[] ).
cnf(408,axiom,
( ~ equal(op(e6,e4),e1)
| skC48 ),
file('ALG209+1.p',unknown),
[] ).
cnf(414,axiom,
( ~ equal(op(e6,e5),e0)
| skC49 ),
file('ALG209+1.p',unknown),
[] ).
cnf(426,axiom,
( ~ equal(op(e6,e6),e5)
| skC50 ),
file('ALG209+1.p',unknown),
[] ).
cnf(429,axiom,
( ~ equal(op(e0,e1),e0)
| skC51 ),
file('ALG209+1.p',unknown),
[] ).
cnf(436,axiom,
( ~ equal(op(e1,e0),e0)
| skC52 ),
file('ALG209+1.p',unknown),
[] ).
cnf(444,axiom,
( ~ equal(op(e0,e2),e1)
| skC53 ),
file('ALG209+1.p',unknown),
[] ).
cnf(451,axiom,
( ~ equal(op(e2,e0),e1)
| skC54 ),
file('ALG209+1.p',unknown),
[] ).
cnf(456,axiom,
( ~ equal(op(e0,e0),e2)
| skC55 ),
file('ALG209+1.p',unknown),
[] ).
cnf(463,axiom,
( ~ equal(op(e0,e0),e2)
| skC56 ),
file('ALG209+1.p',unknown),
[] ).
cnf(474,axiom,
( ~ equal(op(e0,e4),e3)
| skC57 ),
file('ALG209+1.p',unknown),
[] ).
cnf(481,axiom,
( ~ equal(op(e4,e0),e3)
| skC58 ),
file('ALG209+1.p',unknown),
[] ).
cnf(489,axiom,
( ~ equal(op(e0,e5),e4)
| skC59 ),
file('ALG209+1.p',unknown),
[] ).
cnf(496,axiom,
( ~ equal(op(e5,e0),e4)
| skC60 ),
file('ALG209+1.p',unknown),
[] ).
cnf(501,axiom,
( ~ equal(op(e0,e3),e5)
| skC61 ),
file('ALG209+1.p',unknown),
[] ).
cnf(508,axiom,
( ~ equal(op(e3,e0),e5)
| skC62 ),
file('ALG209+1.p',unknown),
[] ).
cnf(518,axiom,
( ~ equal(op(e0,e6),e6)
| skC63 ),
file('ALG209+1.p',unknown),
[] ).
cnf(525,axiom,
( ~ equal(op(e6,e0),e6)
| skC64 ),
file('ALG209+1.p',unknown),
[] ).
cnf(526,axiom,
( ~ equal(op(e1,e0),e0)
| skC65 ),
file('ALG209+1.p',unknown),
[] ).
cnf(533,axiom,
( ~ equal(op(e0,e1),e0)
| skC66 ),
file('ALG209+1.p',unknown),
[] ).
cnf(543,axiom,
( ~ equal(op(e1,e3),e1)
| skC67 ),
file('ALG209+1.p',unknown),
[] ).
cnf(550,axiom,
( ~ equal(op(e3,e1),e1)
| skC68 ),
file('ALG209+1.p',unknown),
[] ).
cnf(559,axiom,
( ~ equal(op(e1,e5),e2)
| skC69 ),
file('ALG209+1.p',unknown),
[] ).
cnf(566,axiom,
( ~ equal(op(e5,e1),e2)
| skC70 ),
file('ALG209+1.p',unknown),
[] ).
cnf(574,axiom,
( ~ equal(op(e1,e6),e3)
| skC71 ),
file('ALG209+1.p',unknown),
[] ).
cnf(581,axiom,
( ~ equal(op(e6,e1),e3)
| skC72 ),
file('ALG209+1.p',unknown),
[] ).
cnf(584,axiom,
( ~ equal(op(e1,e2),e4)
| skC73 ),
file('ALG209+1.p',unknown),
[] ).
cnf(591,axiom,
( ~ equal(op(e2,e1),e4)
| skC74 ),
file('ALG209+1.p',unknown),
[] ).
cnf(600,axiom,
( ~ equal(op(e1,e4),e5)
| skC75 ),
file('ALG209+1.p',unknown),
[] ).
cnf(607,axiom,
( ~ equal(op(e4,e1),e5)
| skC76 ),
file('ALG209+1.p',unknown),
[] ).
cnf(611,axiom,
( ~ equal(op(e1,e1),e6)
| skC77 ),
file('ALG209+1.p',unknown),
[] ).
cnf(618,axiom,
( ~ equal(op(e1,e1),e6)
| skC78 ),
file('ALG209+1.p',unknown),
[] ).
cnf(628,axiom,
( ~ equal(op(e2,e4),e0)
| skC79 ),
file('ALG209+1.p',unknown),
[] ).
cnf(635,axiom,
( ~ equal(op(e4,e2),e0)
| skC80 ),
file('ALG209+1.p',unknown),
[] ).
cnf(638,axiom,
( ~ equal(op(e2,e0),e1)
| skC81 ),
file('ALG209+1.p',unknown),
[] ).
cnf(645,axiom,
( ~ equal(op(e0,e2),e1)
| skC82 ),
file('ALG209+1.p',unknown),
[] ).
cnf(658,axiom,
( ~ equal(op(e2,e6),e2)
| skC83 ),
file('ALG209+1.p',unknown),
[] ).
cnf(665,axiom,
( ~ equal(op(e6,e2),e2)
| skC84 ),
file('ALG209+1.p',unknown),
[] ).
cnf(668,axiom,
( ~ equal(op(e2,e2),e3)
| skC85 ),
file('ALG209+1.p',unknown),
[] ).
cnf(675,axiom,
( ~ equal(op(e2,e2),e3)
| skC86 ),
file('ALG209+1.p',unknown),
[] ).
cnf(681,axiom,
( ~ equal(op(e2,e1),e4)
| skC87 ),
file('ALG209+1.p',unknown),
[] ).
cnf(688,axiom,
( ~ equal(op(e1,e2),e4)
| skC88 ),
file('ALG209+1.p',unknown),
[] ).
cnf(699,axiom,
( ~ equal(op(e2,e5),e5)
| skC89 ),
file('ALG209+1.p',unknown),
[] ).
cnf(706,axiom,
( ~ equal(op(e5,e2),e5)
| skC90 ),
file('ALG209+1.p',unknown),
[] ).
cnf(711,axiom,
( ~ equal(op(e2,e3),e6)
| skC91 ),
file('ALG209+1.p',unknown),
[] ).
cnf(718,axiom,
( ~ equal(op(e3,e2),e6)
| skC92 ),
file('ALG209+1.p',unknown),
[] ).
cnf(725,axiom,
( ~ equal(op(e3,e3),e0)
| skC93 ),
file('ALG209+1.p',unknown),
[] ).
cnf(732,axiom,
( ~ equal(op(e3,e3),e0)
| skC94 ),
file('ALG209+1.p',unknown),
[] ).
cnf(737,axiom,
( ~ equal(op(e3,e1),e1)
| skC95 ),
file('ALG209+1.p',unknown),
[] ).
cnf(744,axiom,
( ~ equal(op(e1,e3),e1)
| skC96 ),
file('ALG209+1.p',unknown),
[] ).
cnf(754,axiom,
( ~ equal(op(e3,e4),e2)
| skC97 ),
file('ALG209+1.p',unknown),
[] ).
cnf(761,axiom,
( ~ equal(op(e4,e3),e2)
| skC98 ),
file('ALG209+1.p',unknown),
[] ).
cnf(769,axiom,
( ~ equal(op(e3,e5),e3)
| skC99 ),
file('ALG209+1.p',unknown),
[] ).
cnf(776,axiom,
( ~ equal(op(e5,e3),e3)
| skC100 ),
file('ALG209+1.p',unknown),
[] ).
cnf(784,axiom,
( ~ equal(op(e3,e6),e4)
| skC101 ),
file('ALG209+1.p',unknown),
[] ).
cnf(791,axiom,
( ~ equal(op(e6,e3),e4)
| skC102 ),
file('ALG209+1.p',unknown),
[] ).
cnf(792,axiom,
( ~ equal(op(e3,e0),e5)
| skC103 ),
file('ALG209+1.p',unknown),
[] ).
cnf(799,axiom,
( ~ equal(op(e0,e3),e5)
| skC104 ),
file('ALG209+1.p',unknown),
[] ).
cnf(808,axiom,
( ~ equal(op(e3,e2),e6)
| skC105 ),
file('ALG209+1.p',unknown),
[] ).
cnf(815,axiom,
( ~ equal(op(e2,e3),e6)
| skC106 ),
file('ALG209+1.p',unknown),
[] ).
cnf(822,axiom,
( ~ equal(op(e4,e2),e0)
| skC107 ),
file('ALG209+1.p',unknown),
[] ).
cnf(829,axiom,
( ~ equal(op(e2,e4),e0)
| skC108 ),
file('ALG209+1.p',unknown),
[] ).
cnf(840,axiom,
( ~ equal(op(e4,e6),e1)
| skC109 ),
file('ALG209+1.p',unknown),
[] ).
cnf(847,axiom,
( ~ equal(op(e6,e4),e1)
| skC110 ),
file('ALG209+1.p',unknown),
[] ).
cnf(851,axiom,
( ~ equal(op(e4,e3),e2)
| skC111 ),
file('ALG209+1.p',unknown),
[] ).
cnf(858,axiom,
( ~ equal(op(e3,e4),e2)
| skC112 ),
file('ALG209+1.p',unknown),
[] ).
cnf(862,axiom,
( ~ equal(op(e4,e0),e3)
| skC113 ),
file('ALG209+1.p',unknown),
[] ).
cnf(869,axiom,
( ~ equal(op(e0,e4),e3)
| skC114 ),
file('ALG209+1.p',unknown),
[] ).
cnf(880,axiom,
( ~ equal(op(e4,e4),e4)
| skC115 ),
file('ALG209+1.p',unknown),
[] ).
cnf(887,axiom,
( ~ equal(op(e4,e4),e4)
| skC116 ),
file('ALG209+1.p',unknown),
[] ).
cnf(891,axiom,
( ~ equal(op(e4,e1),e5)
| skC117 ),
file('ALG209+1.p',unknown),
[] ).
cnf(898,axiom,
( ~ equal(op(e1,e4),e5)
| skC118 ),
file('ALG209+1.p',unknown),
[] ).
cnf(909,axiom,
( ~ equal(op(e4,e5),e6)
| skC119 ),
file('ALG209+1.p',unknown),
[] ).
cnf(916,axiom,
( ~ equal(op(e5,e4),e6)
| skC120 ),
file('ALG209+1.p',unknown),
[] ).
cnf(924,axiom,
( ~ equal(op(e5,e6),e0)
| skC121 ),
file('ALG209+1.p',unknown),
[] ).
cnf(931,axiom,
( ~ equal(op(e6,e5),e0)
| skC122 ),
file('ALG209+1.p',unknown),
[] ).
cnf(937,axiom,
( ~ equal(op(e5,e5),e1)
| skC123 ),
file('ALG209+1.p',unknown),
[] ).
cnf(944,axiom,
( ~ equal(op(e5,e5),e1)
| skC124 ),
file('ALG209+1.p',unknown),
[] ).
cnf(947,axiom,
( ~ equal(op(e5,e1),e2)
| skC125 ),
file('ALG209+1.p',unknown),
[] ).
cnf(954,axiom,
( ~ equal(op(e1,e5),e2)
| skC126 ),
file('ALG209+1.p',unknown),
[] ).
cnf(963,axiom,
( ~ equal(op(e5,e3),e3)
| skC127 ),
file('ALG209+1.p',unknown),
[] ).
cnf(970,axiom,
( ~ equal(op(e3,e5),e3)
| skC128 ),
file('ALG209+1.p',unknown),
[] ).
cnf(974,axiom,
( ~ equal(op(e5,e0),e4)
| skC129 ),
file('ALG209+1.p',unknown),
[] ).
cnf(981,axiom,
( ~ equal(op(e0,e5),e4)
| skC130 ),
file('ALG209+1.p',unknown),
[] ).
cnf(990,axiom,
( ~ equal(op(e5,e2),e5)
| skC131 ),
file('ALG209+1.p',unknown),
[] ).
cnf(997,axiom,
( ~ equal(op(e2,e5),e5)
| skC132 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1006,axiom,
( ~ equal(op(e5,e4),e6)
| skC133 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1013,axiom,
( ~ equal(op(e4,e5),e6)
| skC134 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1021,axiom,
( ~ equal(op(e6,e5),e0)
| skC135 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1028,axiom,
( ~ equal(op(e5,e6),e0)
| skC136 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1034,axiom,
( ~ equal(op(e6,e4),e1)
| skC137 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1041,axiom,
( ~ equal(op(e4,e6),e1)
| skC138 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1046,axiom,
( ~ equal(op(e6,e2),e2)
| skC139 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1053,axiom,
( ~ equal(op(e2,e6),e2)
| skC140 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1059,axiom,
( ~ equal(op(e6,e1),e3)
| skC141 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1066,axiom,
( ~ equal(op(e1,e6),e3)
| skC142 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1075,axiom,
( ~ equal(op(e6,e3),e4)
| skC143 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1082,axiom,
( ~ equal(op(e3,e6),e4)
| skC144 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1092,axiom,
( ~ equal(op(e6,e6),e5)
| skC145 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1099,axiom,
( ~ equal(op(e6,e6),e5)
| skC146 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1100,axiom,
( ~ equal(op(e6,e0),e6)
| skC147 ),
file('ALG209+1.p',unknown),
[] ).
cnf(1113,axiom,
( ~ equal(op(e0,e6),e6)
| ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ skC36
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41
| ~ skC42
| ~ skC43
| ~ skC44
| ~ skC45
| ~ skC46
| ~ skC47
| ~ skC48
| ~ skC49
| ~ skC50
| ~ skC51
| ~ skC52
| ~ skC53
| ~ skC54
| ~ skC55
| ~ skC56
| ~ skC57
| ~ skC58
| ~ skC59
| ~ skC60
| ~ skC61
| ~ skC62
| ~ skC63
| ~ skC64
| ~ skC65
| ~ skC66
| ~ skC67
| ~ skC68
| ~ skC69
| ~ skC70
| ~ skC71
| ~ skC72
| ~ skC73
| ~ skC74
| ~ skC75
| ~ skC76
| ~ skC77
| ~ skC78
| ~ skC79
| ~ skC80
| ~ skC81
| ~ skC82
| ~ skC83
| ~ skC84
| ~ skC85
| ~ skC86
| ~ skC87
| ~ skC88
| ~ skC89
| ~ skC90
| ~ skC91
| ~ skC92
| ~ skC93
| ~ skC94
| ~ skC95
| ~ skC96
| ~ skC97
| ~ skC98
| ~ skC99
| ~ skC100
| ~ skC101
| ~ skC102
| ~ skC103
| ~ skC104
| ~ skC105
| ~ skC106
| ~ skC107
| ~ skC108
| ~ skC109
| ~ skC110
| ~ skC111
| ~ skC112
| ~ skC113
| ~ skC114
| ~ skC115
| ~ skC116
| ~ skC117
| ~ skC118
| ~ skC119
| ~ skC120
| ~ skC121
| ~ skC122
| ~ skC123
| ~ skC124
| ~ skC125
| ~ skC126
| ~ skC127
| ~ skC128
| ~ skC129
| ~ skC130
| ~ skC131
| ~ skC132
| ~ skC133
| ~ skC134
| ~ skC135
| ~ skC136
| ~ skC137
| ~ skC138
| ~ skC139
| ~ skC140
| ~ skC141
| ~ skC142
| ~ skC143
| ~ skC144
| ~ skC145
| ~ skC146
| ~ skC147
| ~ equal(op(op(op(e0,e0),e0),e0),e0)
| ~ equal(op(op(op(e1,e0),e1),e1),e0)
| ~ equal(op(op(op(e2,e0),e2),e2),e0)
| ~ equal(op(op(op(e3,e0),e3),e3),e0)
| ~ equal(op(op(op(e4,e0),e4),e4),e0)
| ~ equal(op(op(op(e5,e0),e5),e5),e0)
| ~ equal(op(op(op(e6,e0),e6),e6),e0)
| ~ equal(op(op(op(e0,e1),e0),e0),e1)
| ~ equal(op(op(op(e1,e1),e1),e1),e1)
| ~ equal(op(op(op(e2,e1),e2),e2),e1)
| ~ equal(op(op(op(e3,e1),e3),e3),e1)
| ~ equal(op(op(op(e4,e1),e4),e4),e1)
| ~ equal(op(op(op(e5,e1),e5),e5),e1)
| ~ equal(op(op(op(e6,e1),e6),e6),e1)
| ~ equal(op(op(op(e0,e2),e0),e0),e2)
| ~ equal(op(op(op(e1,e2),e1),e1),e2)
| ~ equal(op(op(op(e2,e2),e2),e2),e2)
| ~ equal(op(op(op(e3,e2),e3),e3),e2)
| ~ equal(op(op(op(e4,e2),e4),e4),e2)
| ~ equal(op(op(op(e5,e2),e5),e5),e2)
| ~ equal(op(op(op(e6,e2),e6),e6),e2)
| ~ equal(op(op(op(e0,e3),e0),e0),e3)
| ~ equal(op(op(op(e1,e3),e1),e1),e3)
| ~ equal(op(op(op(e2,e3),e2),e2),e3)
| ~ equal(op(op(op(e3,e3),e3),e3),e3)
| ~ equal(op(op(op(e4,e3),e4),e4),e3)
| ~ equal(op(op(op(e5,e3),e5),e5),e3)
| ~ equal(op(op(op(e6,e3),e6),e6),e3)
| ~ equal(op(op(op(e0,e4),e0),e0),e4)
| ~ equal(op(op(op(e1,e4),e1),e1),e4)
| ~ equal(op(op(op(e2,e4),e2),e2),e4)
| ~ equal(op(op(op(e3,e4),e3),e3),e4)
| ~ equal(op(op(op(e4,e4),e4),e4),e4)
| ~ equal(op(op(op(e5,e4),e5),e5),e4)
| ~ equal(op(op(op(e6,e4),e6),e6),e4)
| ~ equal(op(op(op(e0,e5),e0),e0),e5)
| ~ equal(op(op(op(e1,e5),e1),e1),e5)
| ~ equal(op(op(op(e2,e5),e2),e2),e5)
| ~ equal(op(op(op(e3,e5),e3),e3),e5)
| ~ equal(op(op(op(e4,e5),e4),e4),e5)
| ~ equal(op(op(op(e5,e5),e5),e5),e5)
| ~ equal(op(op(op(e6,e5),e6),e6),e5)
| ~ equal(op(op(op(e0,e6),e0),e0),e6)
| ~ equal(op(op(op(e1,e6),e1),e1),e6)
| ~ equal(op(op(op(e2,e6),e2),e2),e6)
| ~ equal(op(op(op(e3,e6),e3),e3),e6)
| ~ equal(op(op(op(e4,e6),e4),e4),e6)
| ~ equal(op(op(op(e5,e6),e5),e5),e6)
| ~ equal(op(op(op(e6,e6),e6),e6),e6) ),
file('ALG209+1.p',unknown),
[] ).
cnf(1114,plain,
( equal(e6,e5)
| skC1 ),
inference(rew,[status(thm),theory(equality)],[70,77]),
[iquote('0:Rew:70.0,77.0')] ).
cnf(1115,plain,
skC1,
inference(mrr,[status(thm)],[1114,21]),
[iquote('0:MRR:1114.0,21.0')] ).
cnf(1122,plain,
( ~ equal(e6,e6)
| skC147 ),
inference(rew,[status(thm),theory(equality)],[64,1100]),
[iquote('0:Rew:64.0,1100.0')] ).
cnf(1123,plain,
skC147,
inference(obv,[status(thm),theory(equality)],[1122]),
[iquote('0:Obv:1122.0')] ).
cnf(1124,plain,
( ~ equal(e5,e5)
| skC146 ),
inference(rew,[status(thm),theory(equality)],[70,1099]),
[iquote('0:Rew:70.0,1099.0')] ).
cnf(1125,plain,
skC146,
inference(obv,[status(thm),theory(equality)],[1124]),
[iquote('0:Obv:1124.0')] ).
cnf(1126,plain,
( ~ equal(e5,e5)
| skC145 ),
inference(rew,[status(thm),theory(equality)],[70,1092]),
[iquote('0:Rew:70.0,1092.0')] ).
cnf(1127,plain,
skC145,
inference(obv,[status(thm),theory(equality)],[1126]),
[iquote('0:Obv:1126.0')] ).
cnf(1131,plain,
( ~ equal(e4,e4)
| skC144 ),
inference(rew,[status(thm),theory(equality)],[49,1082]),
[iquote('0:Rew:49.0,1082.0')] ).
cnf(1132,plain,
skC144,
inference(obv,[status(thm),theory(equality)],[1131]),
[iquote('0:Obv:1131.0')] ).
cnf(1136,plain,
( ~ equal(e4,e4)
| skC143 ),
inference(rew,[status(thm),theory(equality)],[67,1075]),
[iquote('0:Rew:67.0,1075.0')] ).
cnf(1137,plain,
skC143,
inference(obv,[status(thm),theory(equality)],[1136]),
[iquote('0:Obv:1136.0')] ).
cnf(1143,plain,
( ~ equal(e3,e3)
| skC142 ),
inference(rew,[status(thm),theory(equality)],[35,1066]),
[iquote('0:Rew:35.0,1066.0')] ).
cnf(1144,plain,
skC142,
inference(obv,[status(thm),theory(equality)],[1143]),
[iquote('0:Obv:1143.0')] ).
cnf(1150,plain,
( ~ equal(e3,e3)
| skC141 ),
inference(rew,[status(thm),theory(equality)],[65,1059]),
[iquote('0:Rew:65.0,1059.0')] ).
cnf(1151,plain,
skC141,
inference(obv,[status(thm),theory(equality)],[1150]),
[iquote('0:Obv:1150.0')] ).
cnf(1156,plain,
( ~ equal(e2,e2)
| skC140 ),
inference(rew,[status(thm),theory(equality)],[42,1053]),
[iquote('0:Rew:42.0,1053.0')] ).
cnf(1157,plain,
skC140,
inference(obv,[status(thm),theory(equality)],[1156]),
[iquote('0:Obv:1156.0')] ).
cnf(1162,plain,
( ~ equal(e2,e2)
| skC139 ),
inference(rew,[status(thm),theory(equality)],[66,1046]),
[iquote('0:Rew:66.0,1046.0')] ).
cnf(1163,plain,
skC139,
inference(obv,[status(thm),theory(equality)],[1162]),
[iquote('0:Obv:1162.0')] ).
cnf(1166,plain,
( ~ equal(e1,e1)
| skC138 ),
inference(rew,[status(thm),theory(equality)],[56,1041]),
[iquote('0:Rew:56.0,1041.0')] ).
cnf(1167,plain,
skC138,
inference(obv,[status(thm),theory(equality)],[1166]),
[iquote('0:Obv:1166.0')] ).
cnf(1170,plain,
( ~ equal(e1,e1)
| skC137 ),
inference(rew,[status(thm),theory(equality)],[68,1034]),
[iquote('0:Rew:68.0,1034.0')] ).
cnf(1171,plain,
skC137,
inference(obv,[status(thm),theory(equality)],[1170]),
[iquote('0:Obv:1170.0')] ).
cnf(1173,plain,
( ~ equal(e0,e0)
| skC136 ),
inference(rew,[status(thm),theory(equality)],[63,1028]),
[iquote('0:Rew:63.0,1028.0')] ).
cnf(1174,plain,
skC136,
inference(obv,[status(thm),theory(equality)],[1173]),
[iquote('0:Obv:1173.0')] ).
cnf(1176,plain,
( ~ equal(e0,e0)
| skC135 ),
inference(rew,[status(thm),theory(equality)],[69,1021]),
[iquote('0:Rew:69.0,1021.0')] ).
cnf(1177,plain,
skC135,
inference(obv,[status(thm),theory(equality)],[1176]),
[iquote('0:Obv:1176.0')] ).
cnf(1180,plain,
( ~ equal(e6,e6)
| skC134 ),
inference(rew,[status(thm),theory(equality)],[55,1013]),
[iquote('0:Rew:55.0,1013.0')] ).
cnf(1181,plain,
skC134,
inference(obv,[status(thm),theory(equality)],[1180]),
[iquote('0:Obv:1180.0')] ).
cnf(1184,plain,
( ~ equal(e6,e6)
| skC133 ),
inference(rew,[status(thm),theory(equality)],[61,1006]),
[iquote('0:Rew:61.0,1006.0')] ).
cnf(1185,plain,
skC133,
inference(obv,[status(thm),theory(equality)],[1184]),
[iquote('0:Obv:1184.0')] ).
cnf(1190,plain,
( ~ equal(e5,e5)
| skC132 ),
inference(rew,[status(thm),theory(equality)],[41,997]),
[iquote('0:Rew:41.0,997.0')] ).
cnf(1191,plain,
skC132,
inference(obv,[status(thm),theory(equality)],[1190]),
[iquote('0:Obv:1190.0')] ).
cnf(1196,plain,
( ~ equal(e5,e5)
| skC131 ),
inference(rew,[status(thm),theory(equality)],[59,990]),
[iquote('0:Rew:59.0,990.0')] ).
cnf(1197,plain,
skC131,
inference(obv,[status(thm),theory(equality)],[1196]),
[iquote('0:Obv:1196.0')] ).
cnf(1204,plain,
( ~ equal(e4,e4)
| skC130 ),
inference(rew,[status(thm),theory(equality)],[27,981]),
[iquote('0:Rew:27.0,981.0')] ).
cnf(1205,plain,
skC130,
inference(obv,[status(thm),theory(equality)],[1204]),
[iquote('0:Obv:1204.0')] ).
cnf(1212,plain,
( ~ equal(e4,e4)
| skC129 ),
inference(rew,[status(thm),theory(equality)],[57,974]),
[iquote('0:Rew:57.0,974.0')] ).
cnf(1213,plain,
skC129,
inference(obv,[status(thm),theory(equality)],[1212]),
[iquote('0:Obv:1212.0')] ).
cnf(1217,plain,
( ~ equal(e3,e3)
| skC128 ),
inference(rew,[status(thm),theory(equality)],[48,970]),
[iquote('0:Rew:48.0,970.0')] ).
cnf(1218,plain,
skC128,
inference(obv,[status(thm),theory(equality)],[1217]),
[iquote('0:Obv:1217.0')] ).
cnf(1222,plain,
( ~ equal(e3,e3)
| skC127 ),
inference(rew,[status(thm),theory(equality)],[60,963]),
[iquote('0:Rew:60.0,963.0')] ).
cnf(1223,plain,
skC127,
inference(obv,[status(thm),theory(equality)],[1222]),
[iquote('0:Obv:1222.0')] ).
cnf(1229,plain,
( ~ equal(e2,e2)
| skC126 ),
inference(rew,[status(thm),theory(equality)],[34,954]),
[iquote('0:Rew:34.0,954.0')] ).
cnf(1230,plain,
skC126,
inference(obv,[status(thm),theory(equality)],[1229]),
[iquote('0:Obv:1229.0')] ).
cnf(1236,plain,
( ~ equal(e2,e2)
| skC125 ),
inference(rew,[status(thm),theory(equality)],[58,947]),
[iquote('0:Rew:58.0,947.0')] ).
cnf(1237,plain,
skC125,
inference(obv,[status(thm),theory(equality)],[1236]),
[iquote('0:Obv:1236.0')] ).
cnf(1239,plain,
( ~ equal(e1,e1)
| skC124 ),
inference(rew,[status(thm),theory(equality)],[62,944]),
[iquote('0:Rew:62.0,944.0')] ).
cnf(1240,plain,
skC124,
inference(obv,[status(thm),theory(equality)],[1239]),
[iquote('0:Obv:1239.0')] ).
cnf(1242,plain,
( ~ equal(e1,e1)
| skC123 ),
inference(rew,[status(thm),theory(equality)],[62,937]),
[iquote('0:Rew:62.0,937.0')] ).
cnf(1243,plain,
skC123,
inference(obv,[status(thm),theory(equality)],[1242]),
[iquote('0:Obv:1242.0')] ).
cnf(1244,plain,
( ~ equal(e0,e0)
| skC122 ),
inference(rew,[status(thm),theory(equality)],[69,931]),
[iquote('0:Rew:69.0,931.0')] ).
cnf(1245,plain,
skC122,
inference(obv,[status(thm),theory(equality)],[1244]),
[iquote('0:Obv:1244.0')] ).
cnf(1246,plain,
( ~ equal(e0,e0)
| skC121 ),
inference(rew,[status(thm),theory(equality)],[63,924]),
[iquote('0:Rew:63.0,924.0')] ).
cnf(1247,plain,
skC121,
inference(obv,[status(thm),theory(equality)],[1246]),
[iquote('0:Obv:1246.0')] ).
cnf(1249,plain,
( ~ equal(e6,e6)
| skC120 ),
inference(rew,[status(thm),theory(equality)],[61,916]),
[iquote('0:Rew:61.0,916.0')] ).
cnf(1250,plain,
skC120,
inference(obv,[status(thm),theory(equality)],[1249]),
[iquote('0:Obv:1249.0')] ).
cnf(1252,plain,
( ~ equal(e6,e6)
| skC119 ),
inference(rew,[status(thm),theory(equality)],[55,909]),
[iquote('0:Rew:55.0,909.0')] ).
cnf(1253,plain,
skC119,
inference(obv,[status(thm),theory(equality)],[1252]),
[iquote('0:Obv:1252.0')] ).
cnf(1259,plain,
( ~ equal(e5,e5)
| skC118 ),
inference(rew,[status(thm),theory(equality)],[33,898]),
[iquote('0:Rew:33.0,898.0')] ).
cnf(1260,plain,
skC118,
inference(obv,[status(thm),theory(equality)],[1259]),
[iquote('0:Obv:1259.0')] ).
cnf(1266,plain,
( ~ equal(e5,e5)
| skC117 ),
inference(rew,[status(thm),theory(equality)],[51,891]),
[iquote('0:Rew:51.0,891.0')] ).
cnf(1267,plain,
skC117,
inference(obv,[status(thm),theory(equality)],[1266]),
[iquote('0:Obv:1266.0')] ).
cnf(1270,plain,
( ~ equal(e4,e4)
| skC116 ),
inference(rew,[status(thm),theory(equality)],[54,887]),
[iquote('0:Rew:54.0,887.0')] ).
cnf(1271,plain,
skC116,
inference(obv,[status(thm),theory(equality)],[1270]),
[iquote('0:Obv:1270.0')] ).
cnf(1274,plain,
( ~ equal(e4,e4)
| skC115 ),
inference(rew,[status(thm),theory(equality)],[54,880]),
[iquote('0:Rew:54.0,880.0')] ).
cnf(1275,plain,
skC115,
inference(obv,[status(thm),theory(equality)],[1274]),
[iquote('0:Obv:1274.0')] ).
cnf(1282,plain,
( ~ equal(e3,e3)
| skC114 ),
inference(rew,[status(thm),theory(equality)],[26,869]),
[iquote('0:Rew:26.0,869.0')] ).
cnf(1283,plain,
skC114,
inference(obv,[status(thm),theory(equality)],[1282]),
[iquote('0:Obv:1282.0')] ).
cnf(1290,plain,
( ~ equal(e3,e3)
| skC113 ),
inference(rew,[status(thm),theory(equality)],[50,862]),
[iquote('0:Rew:50.0,862.0')] ).
cnf(1291,plain,
skC113,
inference(obv,[status(thm),theory(equality)],[1290]),
[iquote('0:Obv:1290.0')] ).
cnf(1295,plain,
( ~ equal(e2,e2)
| skC112 ),
inference(rew,[status(thm),theory(equality)],[47,858]),
[iquote('0:Rew:47.0,858.0')] ).
cnf(1296,plain,
skC112,
inference(obv,[status(thm),theory(equality)],[1295]),
[iquote('0:Obv:1295.0')] ).
cnf(1300,plain,
( ~ equal(e2,e2)
| skC111 ),
inference(rew,[status(thm),theory(equality)],[53,851]),
[iquote('0:Rew:53.0,851.0')] ).
cnf(1301,plain,
skC111,
inference(obv,[status(thm),theory(equality)],[1300]),
[iquote('0:Obv:1300.0')] ).
cnf(1302,plain,
( ~ equal(e1,e1)
| skC110 ),
inference(rew,[status(thm),theory(equality)],[68,847]),
[iquote('0:Rew:68.0,847.0')] ).
cnf(1303,plain,
skC110,
inference(obv,[status(thm),theory(equality)],[1302]),
[iquote('0:Obv:1302.0')] ).
cnf(1304,plain,
( ~ equal(e1,e1)
| skC109 ),
inference(rew,[status(thm),theory(equality)],[56,840]),
[iquote('0:Rew:56.0,840.0')] ).
cnf(1305,plain,
skC109,
inference(obv,[status(thm),theory(equality)],[1304]),
[iquote('0:Obv:1304.0')] ).
cnf(1310,plain,
( ~ equal(e0,e0)
| skC108 ),
inference(rew,[status(thm),theory(equality)],[40,829]),
[iquote('0:Rew:40.0,829.0')] ).
cnf(1311,plain,
skC108,
inference(obv,[status(thm),theory(equality)],[1310]),
[iquote('0:Obv:1310.0')] ).
cnf(1316,plain,
( ~ equal(e0,e0)
| skC107 ),
inference(rew,[status(thm),theory(equality)],[52,822]),
[iquote('0:Rew:52.0,822.0')] ).
cnf(1317,plain,
skC107,
inference(obv,[status(thm),theory(equality)],[1316]),
[iquote('0:Obv:1316.0')] ).
cnf(1322,plain,
( ~ equal(e6,e6)
| skC106 ),
inference(rew,[status(thm),theory(equality)],[39,815]),
[iquote('0:Rew:39.0,815.0')] ).
cnf(1323,plain,
skC106,
inference(obv,[status(thm),theory(equality)],[1322]),
[iquote('0:Obv:1322.0')] ).
cnf(1328,plain,
( ~ equal(e6,e6)
| skC105 ),
inference(rew,[status(thm),theory(equality)],[45,808]),
[iquote('0:Rew:45.0,808.0')] ).
cnf(1329,plain,
skC105,
inference(obv,[status(thm),theory(equality)],[1328]),
[iquote('0:Obv:1328.0')] ).
cnf(1336,plain,
( ~ equal(e5,e5)
| skC104 ),
inference(rew,[status(thm),theory(equality)],[25,799]),
[iquote('0:Rew:25.0,799.0')] ).
cnf(1337,plain,
skC104,
inference(obv,[status(thm),theory(equality)],[1336]),
[iquote('0:Obv:1336.0')] ).
cnf(1344,plain,
( ~ equal(e5,e5)
| skC103 ),
inference(rew,[status(thm),theory(equality)],[43,792]),
[iquote('0:Rew:43.0,792.0')] ).
cnf(1345,plain,
skC103,
inference(obv,[status(thm),theory(equality)],[1344]),
[iquote('0:Obv:1344.0')] ).
cnf(1346,plain,
( ~ equal(e4,e4)
| skC102 ),
inference(rew,[status(thm),theory(equality)],[67,791]),
[iquote('0:Rew:67.0,791.0')] ).
cnf(1347,plain,
skC102,
inference(obv,[status(thm),theory(equality)],[1346]),
[iquote('0:Obv:1346.0')] ).
cnf(1348,plain,
( ~ equal(e4,e4)
| skC101 ),
inference(rew,[status(thm),theory(equality)],[49,784]),
[iquote('0:Rew:49.0,784.0')] ).
cnf(1349,plain,
skC101,
inference(obv,[status(thm),theory(equality)],[1348]),
[iquote('0:Obv:1348.0')] ).
cnf(1351,plain,
( ~ equal(e3,e3)
| skC100 ),
inference(rew,[status(thm),theory(equality)],[60,776]),
[iquote('0:Rew:60.0,776.0')] ).
cnf(1352,plain,
skC100,
inference(obv,[status(thm),theory(equality)],[1351]),
[iquote('0:Obv:1351.0')] ).
cnf(1354,plain,
( ~ equal(e3,e3)
| skC99 ),
inference(rew,[status(thm),theory(equality)],[48,769]),
[iquote('0:Rew:48.0,769.0')] ).
cnf(1355,plain,
skC99,
inference(obv,[status(thm),theory(equality)],[1354]),
[iquote('0:Obv:1354.0')] ).
cnf(1358,plain,
( ~ equal(e2,e2)
| skC98 ),
inference(rew,[status(thm),theory(equality)],[53,761]),
[iquote('0:Rew:53.0,761.0')] ).
cnf(1359,plain,
skC98,
inference(obv,[status(thm),theory(equality)],[1358]),
[iquote('0:Obv:1358.0')] ).
cnf(1362,plain,
( ~ equal(e2,e2)
| skC97 ),
inference(rew,[status(thm),theory(equality)],[47,754]),
[iquote('0:Rew:47.0,754.0')] ).
cnf(1363,plain,
skC97,
inference(obv,[status(thm),theory(equality)],[1362]),
[iquote('0:Obv:1362.0')] ).
cnf(1369,plain,
( ~ equal(e1,e1)
| skC96 ),
inference(rew,[status(thm),theory(equality)],[32,744]),
[iquote('0:Rew:32.0,744.0')] ).
cnf(1370,plain,
skC96,
inference(obv,[status(thm),theory(equality)],[1369]),
[iquote('0:Obv:1369.0')] ).
cnf(1376,plain,
( ~ equal(e1,e1)
| skC95 ),
inference(rew,[status(thm),theory(equality)],[44,737]),
[iquote('0:Rew:44.0,737.0')] ).
cnf(1377,plain,
skC95,
inference(obv,[status(thm),theory(equality)],[1376]),
[iquote('0:Obv:1376.0')] ).
cnf(1381,plain,
( ~ equal(e0,e0)
| skC94 ),
inference(rew,[status(thm),theory(equality)],[46,732]),
[iquote('0:Rew:46.0,732.0')] ).
cnf(1382,plain,
skC94,
inference(obv,[status(thm),theory(equality)],[1381]),
[iquote('0:Obv:1381.0')] ).
cnf(1386,plain,
( ~ equal(e0,e0)
| skC93 ),
inference(rew,[status(thm),theory(equality)],[46,725]),
[iquote('0:Rew:46.0,725.0')] ).
cnf(1387,plain,
skC93,
inference(obv,[status(thm),theory(equality)],[1386]),
[iquote('0:Obv:1386.0')] ).
cnf(1391,plain,
( ~ equal(e6,e6)
| skC92 ),
inference(rew,[status(thm),theory(equality)],[45,718]),
[iquote('0:Rew:45.0,718.0')] ).
cnf(1392,plain,
skC92,
inference(obv,[status(thm),theory(equality)],[1391]),
[iquote('0:Obv:1391.0')] ).
cnf(1396,plain,
( ~ equal(e6,e6)
| skC91 ),
inference(rew,[status(thm),theory(equality)],[39,711]),
[iquote('0:Rew:39.0,711.0')] ).
cnf(1397,plain,
skC91,
inference(obv,[status(thm),theory(equality)],[1396]),
[iquote('0:Obv:1396.0')] ).
cnf(1399,plain,
( ~ equal(e5,e5)
| skC90 ),
inference(rew,[status(thm),theory(equality)],[59,706]),
[iquote('0:Rew:59.0,706.0')] ).
cnf(1400,plain,
skC90,
inference(obv,[status(thm),theory(equality)],[1399]),
[iquote('0:Obv:1399.0')] ).
cnf(1402,plain,
( ~ equal(e5,e5)
| skC89 ),
inference(rew,[status(thm),theory(equality)],[41,699]),
[iquote('0:Rew:41.0,699.0')] ).
cnf(1403,plain,
skC89,
inference(obv,[status(thm),theory(equality)],[1402]),
[iquote('0:Obv:1402.0')] ).
cnf(1409,plain,
( ~ equal(e4,e4)
| skC88 ),
inference(rew,[status(thm),theory(equality)],[31,688]),
[iquote('0:Rew:31.0,688.0')] ).
cnf(1410,plain,
skC88,
inference(obv,[status(thm),theory(equality)],[1409]),
[iquote('0:Obv:1409.0')] ).
cnf(1416,plain,
( ~ equal(e4,e4)
| skC87 ),
inference(rew,[status(thm),theory(equality)],[37,681]),
[iquote('0:Rew:37.0,681.0')] ).
cnf(1417,plain,
skC87,
inference(obv,[status(thm),theory(equality)],[1416]),
[iquote('0:Obv:1416.0')] ).
cnf(1422,plain,
( ~ equal(e3,e3)
| skC86 ),
inference(rew,[status(thm),theory(equality)],[38,675]),
[iquote('0:Rew:38.0,675.0')] ).
cnf(1423,plain,
skC86,
inference(obv,[status(thm),theory(equality)],[1422]),
[iquote('0:Obv:1422.0')] ).
cnf(1428,plain,
( ~ equal(e3,e3)
| skC85 ),
inference(rew,[status(thm),theory(equality)],[38,668]),
[iquote('0:Rew:38.0,668.0')] ).
cnf(1429,plain,
skC85,
inference(obv,[status(thm),theory(equality)],[1428]),
[iquote('0:Obv:1428.0')] ).
cnf(1430,plain,
( ~ equal(e2,e2)
| skC84 ),
inference(rew,[status(thm),theory(equality)],[66,665]),
[iquote('0:Rew:66.0,665.0')] ).
cnf(1431,plain,
skC84,
inference(obv,[status(thm),theory(equality)],[1430]),
[iquote('0:Obv:1430.0')] ).
cnf(1432,plain,
( ~ equal(e2,e2)
| skC83 ),
inference(rew,[status(thm),theory(equality)],[42,658]),
[iquote('0:Rew:42.0,658.0')] ).
cnf(1433,plain,
skC83,
inference(obv,[status(thm),theory(equality)],[1432]),
[iquote('0:Obv:1432.0')] ).
cnf(1440,plain,
( ~ equal(e1,e1)
| skC82 ),
inference(rew,[status(thm),theory(equality)],[24,645]),
[iquote('0:Rew:24.0,645.0')] ).
cnf(1441,plain,
skC82,
inference(obv,[status(thm),theory(equality)],[1440]),
[iquote('0:Obv:1440.0')] ).
cnf(1448,plain,
( ~ equal(e1,e1)
| skC81 ),
inference(rew,[status(thm),theory(equality)],[36,638]),
[iquote('0:Rew:36.0,638.0')] ).
cnf(1449,plain,
skC81,
inference(obv,[status(thm),theory(equality)],[1448]),
[iquote('0:Obv:1448.0')] ).
cnf(1452,plain,
( ~ equal(e0,e0)
| skC80 ),
inference(rew,[status(thm),theory(equality)],[52,635]),
[iquote('0:Rew:52.0,635.0')] ).
cnf(1453,plain,
skC80,
inference(obv,[status(thm),theory(equality)],[1452]),
[iquote('0:Obv:1452.0')] ).
cnf(1456,plain,
( ~ equal(e0,e0)
| skC79 ),
inference(rew,[status(thm),theory(equality)],[40,628]),
[iquote('0:Rew:40.0,628.0')] ).
cnf(1457,plain,
skC79,
inference(obv,[status(thm),theory(equality)],[1456]),
[iquote('0:Obv:1456.0')] ).
cnf(1463,plain,
( ~ equal(e6,e6)
| skC78 ),
inference(rew,[status(thm),theory(equality)],[30,618]),
[iquote('0:Rew:30.0,618.0')] ).
cnf(1464,plain,
skC78,
inference(obv,[status(thm),theory(equality)],[1463]),
[iquote('0:Obv:1463.0')] ).
cnf(1470,plain,
( ~ equal(e6,e6)
| skC77 ),
inference(rew,[status(thm),theory(equality)],[30,611]),
[iquote('0:Rew:30.0,611.0')] ).
cnf(1471,plain,
skC77,
inference(obv,[status(thm),theory(equality)],[1470]),
[iquote('0:Obv:1470.0')] ).
cnf(1474,plain,
( ~ equal(e5,e5)
| skC76 ),
inference(rew,[status(thm),theory(equality)],[51,607]),
[iquote('0:Rew:51.0,607.0')] ).
cnf(1475,plain,
skC76,
inference(obv,[status(thm),theory(equality)],[1474]),
[iquote('0:Obv:1474.0')] ).
cnf(1478,plain,
( ~ equal(e5,e5)
| skC75 ),
inference(rew,[status(thm),theory(equality)],[33,600]),
[iquote('0:Rew:33.0,600.0')] ).
cnf(1479,plain,
skC75,
inference(obv,[status(thm),theory(equality)],[1478]),
[iquote('0:Obv:1478.0')] ).
cnf(1484,plain,
( ~ equal(e4,e4)
| skC74 ),
inference(rew,[status(thm),theory(equality)],[37,591]),
[iquote('0:Rew:37.0,591.0')] ).
cnf(1485,plain,
skC74,
inference(obv,[status(thm),theory(equality)],[1484]),
[iquote('0:Obv:1484.0')] ).
cnf(1490,plain,
( ~ equal(e4,e4)
| skC73 ),
inference(rew,[status(thm),theory(equality)],[31,584]),
[iquote('0:Rew:31.0,584.0')] ).
cnf(1491,plain,
skC73,
inference(obv,[status(thm),theory(equality)],[1490]),
[iquote('0:Obv:1490.0')] ).
cnf(1492,plain,
( ~ equal(e3,e3)
| skC72 ),
inference(rew,[status(thm),theory(equality)],[65,581]),
[iquote('0:Rew:65.0,581.0')] ).
cnf(1493,plain,
skC72,
inference(obv,[status(thm),theory(equality)],[1492]),
[iquote('0:Obv:1492.0')] ).
cnf(1494,plain,
( ~ equal(e3,e3)
| skC71 ),
inference(rew,[status(thm),theory(equality)],[35,574]),
[iquote('0:Rew:35.0,574.0')] ).
cnf(1495,plain,
skC71,
inference(obv,[status(thm),theory(equality)],[1494]),
[iquote('0:Obv:1494.0')] ).
cnf(1497,plain,
( ~ equal(e2,e2)
| skC70 ),
inference(rew,[status(thm),theory(equality)],[58,566]),
[iquote('0:Rew:58.0,566.0')] ).
cnf(1498,plain,
skC70,
inference(obv,[status(thm),theory(equality)],[1497]),
[iquote('0:Obv:1497.0')] ).
cnf(1500,plain,
( ~ equal(e2,e2)
| skC69 ),
inference(rew,[status(thm),theory(equality)],[34,559]),
[iquote('0:Rew:34.0,559.0')] ).
cnf(1501,plain,
skC69,
inference(obv,[status(thm),theory(equality)],[1500]),
[iquote('0:Obv:1500.0')] ).
cnf(1505,plain,
( ~ equal(e1,e1)
| skC68 ),
inference(rew,[status(thm),theory(equality)],[44,550]),
[iquote('0:Rew:44.0,550.0')] ).
cnf(1506,plain,
skC68,
inference(obv,[status(thm),theory(equality)],[1505]),
[iquote('0:Obv:1505.0')] ).
cnf(1510,plain,
( ~ equal(e1,e1)
| skC67 ),
inference(rew,[status(thm),theory(equality)],[32,543]),
[iquote('0:Rew:32.0,543.0')] ).
cnf(1511,plain,
skC67,
inference(obv,[status(thm),theory(equality)],[1510]),
[iquote('0:Obv:1510.0')] ).
cnf(1518,plain,
( ~ equal(e0,e0)
| skC66 ),
inference(rew,[status(thm),theory(equality)],[23,533]),
[iquote('0:Rew:23.0,533.0')] ).
cnf(1519,plain,
skC66,
inference(obv,[status(thm),theory(equality)],[1518]),
[iquote('0:Obv:1518.0')] ).
cnf(1526,plain,
( ~ equal(e0,e0)
| skC65 ),
inference(rew,[status(thm),theory(equality)],[29,526]),
[iquote('0:Rew:29.0,526.0')] ).
cnf(1527,plain,
skC65,
inference(obv,[status(thm),theory(equality)],[1526]),
[iquote('0:Obv:1526.0')] ).
cnf(1528,plain,
( ~ equal(e6,e6)
| skC64 ),
inference(rew,[status(thm),theory(equality)],[64,525]),
[iquote('0:Rew:64.0,525.0')] ).
cnf(1529,plain,
skC64,
inference(obv,[status(thm),theory(equality)],[1528]),
[iquote('0:Obv:1528.0')] ).
cnf(1530,plain,
( ~ equal(e6,e6)
| skC63 ),
inference(rew,[status(thm),theory(equality)],[28,518]),
[iquote('0:Rew:28.0,518.0')] ).
cnf(1531,plain,
skC63,
inference(obv,[status(thm),theory(equality)],[1530]),
[iquote('0:Obv:1530.0')] ).
cnf(1535,plain,
( ~ equal(e5,e5)
| skC62 ),
inference(rew,[status(thm),theory(equality)],[43,508]),
[iquote('0:Rew:43.0,508.0')] ).
cnf(1536,plain,
skC62,
inference(obv,[status(thm),theory(equality)],[1535]),
[iquote('0:Obv:1535.0')] ).
cnf(1540,plain,
( ~ equal(e5,e5)
| skC61 ),
inference(rew,[status(thm),theory(equality)],[25,501]),
[iquote('0:Rew:25.0,501.0')] ).
cnf(1541,plain,
skC61,
inference(obv,[status(thm),theory(equality)],[1540]),
[iquote('0:Obv:1540.0')] ).
cnf(1543,plain,
( ~ equal(e4,e4)
| skC60 ),
inference(rew,[status(thm),theory(equality)],[57,496]),
[iquote('0:Rew:57.0,496.0')] ).
cnf(1544,plain,
skC60,
inference(obv,[status(thm),theory(equality)],[1543]),
[iquote('0:Obv:1543.0')] ).
cnf(1546,plain,
( ~ equal(e4,e4)
| skC59 ),
inference(rew,[status(thm),theory(equality)],[27,489]),
[iquote('0:Rew:27.0,489.0')] ).
cnf(1547,plain,
skC59,
inference(obv,[status(thm),theory(equality)],[1546]),
[iquote('0:Obv:1546.0')] ).
cnf(1550,plain,
( ~ equal(e3,e3)
| skC58 ),
inference(rew,[status(thm),theory(equality)],[50,481]),
[iquote('0:Rew:50.0,481.0')] ).
cnf(1551,plain,
skC58,
inference(obv,[status(thm),theory(equality)],[1550]),
[iquote('0:Obv:1550.0')] ).
cnf(1554,plain,
( ~ equal(e3,e3)
| skC57 ),
inference(rew,[status(thm),theory(equality)],[26,474]),
[iquote('0:Rew:26.0,474.0')] ).
cnf(1555,plain,
skC57,
inference(obv,[status(thm),theory(equality)],[1554]),
[iquote('0:Obv:1554.0')] ).
cnf(1562,plain,
( ~ equal(e2,e2)
| skC56 ),
inference(rew,[status(thm),theory(equality)],[22,463]),
[iquote('0:Rew:22.0,463.0')] ).
cnf(1563,plain,
skC56,
inference(obv,[status(thm),theory(equality)],[1562]),
[iquote('0:Obv:1562.0')] ).
cnf(1570,plain,
( ~ equal(e2,e2)
| skC55 ),
inference(rew,[status(thm),theory(equality)],[22,456]),
[iquote('0:Rew:22.0,456.0')] ).
cnf(1571,plain,
skC55,
inference(obv,[status(thm),theory(equality)],[1570]),
[iquote('0:Obv:1570.0')] ).
cnf(1576,plain,
( ~ equal(e1,e1)
| skC54 ),
inference(rew,[status(thm),theory(equality)],[36,451]),
[iquote('0:Rew:36.0,451.0')] ).
cnf(1577,plain,
skC54,
inference(obv,[status(thm),theory(equality)],[1576]),
[iquote('0:Obv:1576.0')] ).
cnf(1582,plain,
( ~ equal(e1,e1)
| skC53 ),
inference(rew,[status(thm),theory(equality)],[24,444]),
[iquote('0:Rew:24.0,444.0')] ).
cnf(1583,plain,
skC53,
inference(obv,[status(thm),theory(equality)],[1582]),
[iquote('0:Obv:1582.0')] ).
cnf(1589,plain,
( ~ equal(e0,e0)
| skC52 ),
inference(rew,[status(thm),theory(equality)],[29,436]),
[iquote('0:Rew:29.0,436.0')] ).
cnf(1590,plain,
skC52,
inference(obv,[status(thm),theory(equality)],[1589]),
[iquote('0:Obv:1589.0')] ).
cnf(1596,plain,
( ~ equal(e0,e0)
| skC51 ),
inference(rew,[status(thm),theory(equality)],[23,429]),
[iquote('0:Rew:23.0,429.0')] ).
cnf(1597,plain,
skC51,
inference(obv,[status(thm),theory(equality)],[1596]),
[iquote('0:Obv:1596.0')] ).
cnf(1599,plain,
( ~ equal(e5,e5)
| skC50 ),
inference(rew,[status(thm),theory(equality)],[70,426]),
[iquote('0:Rew:70.0,426.0')] ).
cnf(1600,plain,
skC50,
inference(obv,[status(thm),theory(equality)],[1599]),
[iquote('0:Obv:1599.0')] ).
cnf(1607,plain,
( ~ equal(e0,e0)
| skC49 ),
inference(rew,[status(thm),theory(equality)],[69,414]),
[iquote('0:Rew:69.0,414.0')] ).
cnf(1608,plain,
skC49,
inference(obv,[status(thm),theory(equality)],[1607]),
[iquote('0:Obv:1607.0')] ).
cnf(1614,plain,
( ~ equal(e1,e1)
| skC48 ),
inference(rew,[status(thm),theory(equality)],[68,408]),
[iquote('0:Rew:68.0,408.0')] ).
cnf(1615,plain,
skC48,
inference(obv,[status(thm),theory(equality)],[1614]),
[iquote('0:Obv:1614.0')] ).
cnf(1618,plain,
( ~ equal(e4,e4)
| skC47 ),
inference(rew,[status(thm),theory(equality)],[67,404]),
[iquote('0:Rew:67.0,404.0')] ).
cnf(1619,plain,
skC47,
inference(obv,[status(thm),theory(equality)],[1618]),
[iquote('0:Obv:1618.0')] ).
cnf(1624,plain,
( ~ equal(e2,e2)
| skC46 ),
inference(rew,[status(thm),theory(equality)],[66,395]),
[iquote('0:Rew:66.0,395.0')] ).
cnf(1625,plain,
skC46,
inference(obv,[status(thm),theory(equality)],[1624]),
[iquote('0:Obv:1624.0')] ).
cnf(1629,plain,
( ~ equal(e3,e3)
| skC45 ),
inference(rew,[status(thm),theory(equality)],[65,389]),
[iquote('0:Rew:65.0,389.0')] ).
cnf(1630,plain,
skC45,
inference(obv,[status(thm),theory(equality)],[1629]),
[iquote('0:Obv:1629.0')] ).
cnf(1631,plain,
( ~ equal(e6,e6)
| skC44 ),
inference(rew,[status(thm),theory(equality)],[64,385]),
[iquote('0:Rew:64.0,385.0')] ).
cnf(1632,plain,
skC44,
inference(obv,[status(thm),theory(equality)],[1631]),
[iquote('0:Obv:1631.0')] ).
cnf(1639,plain,
( ~ equal(e0,e0)
| skC43 ),
inference(rew,[status(thm),theory(equality)],[63,372]),
[iquote('0:Rew:63.0,372.0')] ).
cnf(1640,plain,
skC43,
inference(obv,[status(thm),theory(equality)],[1639]),
[iquote('0:Obv:1639.0')] ).
cnf(1646,plain,
( ~ equal(e1,e1)
| skC42 ),
inference(rew,[status(thm),theory(equality)],[62,366]),
[iquote('0:Rew:62.0,366.0')] ).
cnf(1647,plain,
skC42,
inference(obv,[status(thm),theory(equality)],[1646]),
[iquote('0:Obv:1646.0')] ).
cnf(1648,plain,
( ~ equal(e6,e6)
| skC41 ),
inference(rew,[status(thm),theory(equality)],[61,364]),
[iquote('0:Rew:61.0,364.0')] ).
cnf(1649,plain,
skC41,
inference(obv,[status(thm),theory(equality)],[1648]),
[iquote('0:Obv:1648.0')] ).
cnf(1653,plain,
( ~ equal(e3,e3)
| skC40 ),
inference(rew,[status(thm),theory(equality)],[60,354]),
[iquote('0:Rew:60.0,354.0')] ).
cnf(1654,plain,
skC40,
inference(obv,[status(thm),theory(equality)],[1653]),
[iquote('0:Obv:1653.0')] ).
cnf(1656,plain,
( ~ equal(e5,e5)
| skC39 ),
inference(rew,[status(thm),theory(equality)],[59,349]),
[iquote('0:Rew:59.0,349.0')] ).
cnf(1657,plain,
skC39,
inference(obv,[status(thm),theory(equality)],[1656]),
[iquote('0:Obv:1656.0')] ).
cnf(1662,plain,
( ~ equal(e2,e2)
| skC38 ),
inference(rew,[status(thm),theory(equality)],[58,339]),
[iquote('0:Rew:58.0,339.0')] ).
cnf(1663,plain,
skC38,
inference(obv,[status(thm),theory(equality)],[1662]),
[iquote('0:Obv:1662.0')] ).
cnf(1666,plain,
( ~ equal(e4,e4)
| skC37 ),
inference(rew,[status(thm),theory(equality)],[57,334]),
[iquote('0:Rew:57.0,334.0')] ).
cnf(1667,plain,
skC37,
inference(obv,[status(thm),theory(equality)],[1666]),
[iquote('0:Obv:1666.0')] ).
cnf(1673,plain,
( ~ equal(e1,e1)
| skC36 ),
inference(rew,[status(thm),theory(equality)],[56,324]),
[iquote('0:Rew:56.0,324.0')] ).
cnf(1674,plain,
skC36,
inference(obv,[status(thm),theory(equality)],[1673]),
[iquote('0:Obv:1673.0')] ).
cnf(1675,plain,
( ~ equal(e6,e6)
| skC35 ),
inference(rew,[status(thm),theory(equality)],[55,322]),
[iquote('0:Rew:55.0,322.0')] ).
cnf(1676,plain,
skC35,
inference(obv,[status(thm),theory(equality)],[1675]),
[iquote('0:Obv:1675.0')] ).
cnf(1679,plain,
( ~ equal(e4,e4)
| skC34 ),
inference(rew,[status(thm),theory(equality)],[54,313]),
[iquote('0:Rew:54.0,313.0')] ).
cnf(1680,plain,
skC34,
inference(obv,[status(thm),theory(equality)],[1679]),
[iquote('0:Obv:1679.0')] ).
cnf(1685,plain,
( ~ equal(e2,e2)
| skC33 ),
inference(rew,[status(thm),theory(equality)],[53,304]),
[iquote('0:Rew:53.0,304.0')] ).
cnf(1686,plain,
skC33,
inference(obv,[status(thm),theory(equality)],[1685]),
[iquote('0:Obv:1685.0')] ).
cnf(1693,plain,
( ~ equal(e0,e0)
| skC32 ),
inference(rew,[status(thm),theory(equality)],[52,295]),
[iquote('0:Rew:52.0,295.0')] ).
cnf(1694,plain,
skC32,
inference(obv,[status(thm),theory(equality)],[1693]),
[iquote('0:Obv:1693.0')] ).
cnf(1696,plain,
( ~ equal(e5,e5)
| skC31 ),
inference(rew,[status(thm),theory(equality)],[51,293]),
[iquote('0:Rew:51.0,293.0')] ).
cnf(1697,plain,
skC31,
inference(obv,[status(thm),theory(equality)],[1696]),
[iquote('0:Obv:1696.0')] ).
cnf(1701,plain,
( ~ equal(e3,e3)
| skC30 ),
inference(rew,[status(thm),theory(equality)],[50,284]),
[iquote('0:Rew:50.0,284.0')] ).
cnf(1702,plain,
skC30,
inference(obv,[status(thm),theory(equality)],[1701]),
[iquote('0:Obv:1701.0')] ).
cnf(1705,plain,
( ~ equal(e4,e4)
| skC29 ),
inference(rew,[status(thm),theory(equality)],[49,278]),
[iquote('0:Rew:49.0,278.0')] ).
cnf(1706,plain,
skC29,
inference(obv,[status(thm),theory(equality)],[1705]),
[iquote('0:Obv:1705.0')] ).
cnf(1710,plain,
( ~ equal(e3,e3)
| skC28 ),
inference(rew,[status(thm),theory(equality)],[48,270]),
[iquote('0:Rew:48.0,270.0')] ).
cnf(1711,plain,
skC28,
inference(obv,[status(thm),theory(equality)],[1710]),
[iquote('0:Obv:1710.0')] ).
cnf(1716,plain,
( ~ equal(e2,e2)
| skC27 ),
inference(rew,[status(thm),theory(equality)],[47,262]),
[iquote('0:Rew:47.0,262.0')] ).
cnf(1717,plain,
skC27,
inference(obv,[status(thm),theory(equality)],[1716]),
[iquote('0:Obv:1716.0')] ).
cnf(1724,plain,
( ~ equal(e0,e0)
| skC26 ),
inference(rew,[status(thm),theory(equality)],[46,253]),
[iquote('0:Rew:46.0,253.0')] ).
cnf(1725,plain,
skC26,
inference(obv,[status(thm),theory(equality)],[1724]),
[iquote('0:Obv:1724.0')] ).
cnf(1726,plain,
( ~ equal(e6,e6)
| skC25 ),
inference(rew,[status(thm),theory(equality)],[45,252]),
[iquote('0:Rew:45.0,252.0')] ).
cnf(1727,plain,
skC25,
inference(obv,[status(thm),theory(equality)],[1726]),
[iquote('0:Obv:1726.0')] ).
cnf(1733,plain,
( ~ equal(e1,e1)
| skC24 ),
inference(rew,[status(thm),theory(equality)],[44,240]),
[iquote('0:Rew:44.0,240.0')] ).
cnf(1734,plain,
skC24,
inference(obv,[status(thm),theory(equality)],[1733]),
[iquote('0:Obv:1733.0')] ).
cnf(1736,plain,
( ~ equal(e5,e5)
| skC23 ),
inference(rew,[status(thm),theory(equality)],[43,237]),
[iquote('0:Rew:43.0,237.0')] ).
cnf(1737,plain,
skC23,
inference(obv,[status(thm),theory(equality)],[1736]),
[iquote('0:Obv:1736.0')] ).
cnf(1742,plain,
( ~ equal(e2,e2)
| skC22 ),
inference(rew,[status(thm),theory(equality)],[42,227]),
[iquote('0:Rew:42.0,227.0')] ).
cnf(1743,plain,
skC22,
inference(obv,[status(thm),theory(equality)],[1742]),
[iquote('0:Obv:1742.0')] ).
cnf(1745,plain,
( ~ equal(e5,e5)
| skC21 ),
inference(rew,[status(thm),theory(equality)],[41,223]),
[iquote('0:Rew:41.0,223.0')] ).
cnf(1746,plain,
skC21,
inference(obv,[status(thm),theory(equality)],[1745]),
[iquote('0:Obv:1745.0')] ).
cnf(1753,plain,
( ~ equal(e0,e0)
| skC20 ),
inference(rew,[status(thm),theory(equality)],[40,211]),
[iquote('0:Rew:40.0,211.0')] ).
cnf(1754,plain,
skC20,
inference(obv,[status(thm),theory(equality)],[1753]),
[iquote('0:Obv:1753.0')] ).
cnf(1755,plain,
( ~ equal(e6,e6)
| skC19 ),
inference(rew,[status(thm),theory(equality)],[39,210]),
[iquote('0:Rew:39.0,210.0')] ).
cnf(1756,plain,
skC19,
inference(obv,[status(thm),theory(equality)],[1755]),
[iquote('0:Obv:1755.0')] ).
cnf(1760,plain,
( ~ equal(e3,e3)
| skC18 ),
inference(rew,[status(thm),theory(equality)],[38,200]),
[iquote('0:Rew:38.0,200.0')] ).
cnf(1761,plain,
skC18,
inference(obv,[status(thm),theory(equality)],[1760]),
[iquote('0:Obv:1760.0')] ).
cnf(1764,plain,
( ~ equal(e4,e4)
| skC17 ),
inference(rew,[status(thm),theory(equality)],[37,194]),
[iquote('0:Rew:37.0,194.0')] ).
cnf(1765,plain,
skC17,
inference(obv,[status(thm),theory(equality)],[1764]),
[iquote('0:Obv:1764.0')] ).
cnf(1771,plain,
( ~ equal(e1,e1)
| skC16 ),
inference(rew,[status(thm),theory(equality)],[36,184]),
[iquote('0:Rew:36.0,184.0')] ).
cnf(1772,plain,
skC16,
inference(obv,[status(thm),theory(equality)],[1771]),
[iquote('0:Obv:1771.0')] ).
cnf(1776,plain,
( ~ equal(e3,e3)
| skC15 ),
inference(rew,[status(thm),theory(equality)],[35,179]),
[iquote('0:Rew:35.0,179.0')] ).
cnf(1777,plain,
skC15,
inference(obv,[status(thm),theory(equality)],[1776]),
[iquote('0:Obv:1776.0')] ).
cnf(1782,plain,
( ~ equal(e2,e2)
| skC14 ),
inference(rew,[status(thm),theory(equality)],[34,171]),
[iquote('0:Rew:34.0,171.0')] ).
cnf(1783,plain,
skC14,
inference(obv,[status(thm),theory(equality)],[1782]),
[iquote('0:Obv:1782.0')] ).
cnf(1785,plain,
( ~ equal(e5,e5)
| skC13 ),
inference(rew,[status(thm),theory(equality)],[33,167]),
[iquote('0:Rew:33.0,167.0')] ).
cnf(1786,plain,
skC13,
inference(obv,[status(thm),theory(equality)],[1785]),
[iquote('0:Obv:1785.0')] ).
cnf(1792,plain,
( ~ equal(e1,e1)
| skC12 ),
inference(rew,[status(thm),theory(equality)],[32,156]),
[iquote('0:Rew:32.0,156.0')] ).
cnf(1793,plain,
skC12,
inference(obv,[status(thm),theory(equality)],[1792]),
[iquote('0:Obv:1792.0')] ).
cnf(1796,plain,
( ~ equal(e4,e4)
| skC11 ),
inference(rew,[status(thm),theory(equality)],[31,152]),
[iquote('0:Rew:31.0,152.0')] ).
cnf(1797,plain,
skC11,
inference(obv,[status(thm),theory(equality)],[1796]),
[iquote('0:Obv:1796.0')] ).
cnf(1798,plain,
( ~ equal(e6,e6)
| skC10 ),
inference(rew,[status(thm),theory(equality)],[30,147]),
[iquote('0:Rew:30.0,147.0')] ).
cnf(1799,plain,
skC10,
inference(obv,[status(thm),theory(equality)],[1798]),
[iquote('0:Obv:1798.0')] ).
cnf(1806,plain,
( ~ equal(e0,e0)
| skC9 ),
inference(rew,[status(thm),theory(equality)],[29,134]),
[iquote('0:Rew:29.0,134.0')] ).
cnf(1807,plain,
skC9,
inference(obv,[status(thm),theory(equality)],[1806]),
[iquote('0:Obv:1806.0')] ).
cnf(1808,plain,
( ~ equal(e6,e6)
| skC8 ),
inference(rew,[status(thm),theory(equality)],[28,133]),
[iquote('0:Rew:28.0,133.0')] ).
cnf(1809,plain,
skC8,
inference(obv,[status(thm),theory(equality)],[1808]),
[iquote('0:Obv:1808.0')] ).
cnf(1812,plain,
( ~ equal(e4,e4)
| skC7 ),
inference(rew,[status(thm),theory(equality)],[27,124]),
[iquote('0:Rew:27.0,124.0')] ).
cnf(1813,plain,
skC7,
inference(obv,[status(thm),theory(equality)],[1812]),
[iquote('0:Obv:1812.0')] ).
cnf(1817,plain,
( ~ equal(e3,e3)
| skC6 ),
inference(rew,[status(thm),theory(equality)],[26,116]),
[iquote('0:Rew:26.0,116.0')] ).
cnf(1818,plain,
skC6,
inference(obv,[status(thm),theory(equality)],[1817]),
[iquote('0:Obv:1817.0')] ).
cnf(1820,plain,
( ~ equal(e5,e5)
| skC5 ),
inference(rew,[status(thm),theory(equality)],[25,111]),
[iquote('0:Rew:25.0,111.0')] ).
cnf(1821,plain,
skC5,
inference(obv,[status(thm),theory(equality)],[1820]),
[iquote('0:Obv:1820.0')] ).
cnf(1827,plain,
( ~ equal(e1,e1)
| skC4 ),
inference(rew,[status(thm),theory(equality)],[24,100]),
[iquote('0:Rew:24.0,100.0')] ).
cnf(1828,plain,
skC4,
inference(obv,[status(thm),theory(equality)],[1827]),
[iquote('0:Obv:1827.0')] ).
cnf(1835,plain,
( ~ equal(e0,e0)
| skC3 ),
inference(rew,[status(thm),theory(equality)],[23,92]),
[iquote('0:Rew:23.0,92.0')] ).
cnf(1836,plain,
skC3,
inference(obv,[status(thm),theory(equality)],[1835]),
[iquote('0:Obv:1835.0')] ).
cnf(1841,plain,
( ~ equal(e2,e2)
| skC2 ),
inference(rew,[status(thm),theory(equality)],[22,87]),
[iquote('0:Rew:22.0,87.0')] ).
cnf(1842,plain,
skC2,
inference(obv,[status(thm),theory(equality)],[1841]),
[iquote('0:Obv:1841.0')] ).
cnf(1845,plain,
( ~ equal(e4,e4)
| skC0 ),
inference(rew,[status(thm),theory(equality)],[54,82]),
[iquote('0:Rew:54.0,82.0')] ).
cnf(1846,plain,
skC0,
inference(obv,[status(thm),theory(equality)],[1845]),
[iquote('0:Obv:1845.0')] ).
cnf(1859,plain,
( ~ equal(e6,e6)
| ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ skC36
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41
| ~ skC42
| ~ skC43
| ~ skC44
| ~ skC45
| ~ skC46
| ~ skC47
| ~ skC48
| ~ skC49
| ~ skC50
| ~ skC51
| ~ skC52
| ~ skC53
| ~ skC54
| ~ skC55
| ~ skC56
| ~ skC57
| ~ skC58
| ~ skC59
| ~ skC60
| ~ skC61
| ~ skC62
| ~ skC63
| ~ skC64
| ~ skC65
| ~ skC66
| ~ skC67
| ~ skC68
| ~ skC69
| ~ skC70
| ~ skC71
| ~ skC72
| ~ skC73
| ~ skC74
| ~ skC75
| ~ skC76
| ~ skC77
| ~ skC78
| ~ skC79
| ~ skC80
| ~ skC81
| ~ skC82
| ~ skC83
| ~ skC84
| ~ skC85
| ~ skC86
| ~ skC87
| ~ skC88
| ~ skC89
| ~ skC90
| ~ skC91
| ~ skC92
| ~ skC93
| ~ skC94
| ~ skC95
| ~ skC96
| ~ skC97
| ~ skC98
| ~ skC99
| ~ skC100
| ~ skC101
| ~ skC102
| ~ skC103
| ~ skC104
| ~ skC105
| ~ skC106
| ~ skC107
| ~ skC108
| ~ skC109
| ~ skC110
| ~ skC111
| ~ skC112
| ~ skC113
| ~ skC114
| ~ skC115
| ~ skC116
| ~ skC117
| ~ skC118
| ~ skC119
| ~ skC120
| ~ skC121
| ~ skC122
| ~ skC123
| ~ skC124
| ~ skC125
| ~ skC126
| ~ skC127
| ~ skC128
| ~ skC129
| ~ skC130
| ~ skC131
| ~ skC132
| ~ skC133
| ~ skC134
| ~ skC135
| ~ skC136
| ~ skC137
| ~ skC138
| ~ skC139
| ~ skC140
| ~ skC141
| ~ skC142
| ~ skC143
| ~ skC144
| ~ skC145
| ~ skC146
| ~ skC147
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ equal(e6,e6)
| ~ equal(e6,e6)
| ~ equal(e6,e6)
| ~ equal(e6,e6)
| ~ equal(e6,e6)
| ~ equal(e6,e6)
| ~ equal(e6,e6) ),
inference(rew,[status(thm),theory(equality)],[28,1113,63,70,55,27,61,33,56,39,53,49,45,38,42,30,44,35,64,69,41,34,62,68,25,46,48,59,51,37,43,50,54,67,47,31,24,40,58,57,26,60,66,65,32,52,22,29,36,23]),
[iquote('0:Rew:28.0,1113.197,63.0,1113.197,70.0,1113.197,55.0,1113.196,27.0,1113.196,63.0,1113.196,61.0,1113.195,33.0,1113.195,56.0,1113.195,39.0,1113.194,53.0,1113.194,49.0,1113.194,45.0,1113.193,38.0,1113.193,42.0,1113.193,30.0,1113.192,44.0,1113.192,35.0,1113.192,64.0,1113.191,64.0,1113.191,28.0,1113.191,70.0,1113.190,28.0,1113.190,69.0,1113.190,41.0,1113.189,34.0,1113.189,62.0,1113.189,33.0,1113.188,68.0,1113.188,55.0,1113.188,25.0,1113.187,46.0,1113.187,48.0,1113.187,59.0,1113.186,59.0,1113.186,41.0,1113.186,51.0,1113.185,37.0,1113.185,34.0,1113.185,43.0,1113.184,50.0,1113.184,27.0,1113.184,49.0,1113.183,35.0,1113.183,68.0,1113.183,27.0,1113.182,69.0,1113.182,61.0,1113.182,54.0,1113.181,54.0,1113.181,54.0,1113.181,67.0,1113.180,39.0,1113.180,47.0,1113.180,31.0,1113.179,24.0,1113.179,40.0,1113.179,37.0,1113.178,58.0,1113.178,33.0,1113.178,57.0,1113.177,43.0,1113.177,26.0,1113.177,35.0,1113.176,56.0,1113.176,67.0,1113.176,48.0,1113.175,48.0,1113.175,60.0,1113.175,26.0,1113.174,40.0,1113.174,53.0,1113.174,60.0,1113.173,25.0,1113.173,46.0,1113.173,38.0,1113.172,66.0,1113.172,39.0,1113.172,65.0,1113.171,30.0,1113.171,32.0,1113.171,50.0,1113.170,57.0,1113.170,25.0,1113.170,42.0,1113.169,42.0,1113.169,66.0,1113.169,34.0,1113.168,62.0,1113.168,59.0,1113.168,47.0,1113.167,26.0,1113.167,52.0,1113.167,53.0,1113.166,67.0,1113.166,45.0,1113.166,66.0,1113.165,45.0,1113.165,38.0,1113.165,58.0,1113.164,51.0,1113.164,31.0,1113.164,22.0,1113.163,29.0,1113.163,24.0,1113.163,56.0,1113.162,49.0,1113.162,65.0,1113.162,62.0,1113.161,41.0,1113.161,58.0,1113.161,68.0,1113.160,61.0,1113.160,51.0,1113.160,32.0,1113.159,32.0,1113.159,44.0,1113.159,24.0,1113.158,52.0,1113.158,37.0,1113.158,44.0,1113.157,65.0,1113.157,30.0,1113.157,36.0,1113.156,22.0,1113.156,23.0,1113.156,63.0,1113.155,70.0,1113.155,64.0,1113.155,69.0,1113.154,55.0,1113.154,57.0,1113.154,40.0,1113.153,47.0,1113.153,50.0,1113.153,46.0,1113.152,60.0,1113.152,43.0,1113.152,52.0,1113.151,31.0,1113.151,36.0,1113.151,23.0,1113.150,23.0,1113.150,29.0,1113.150,29.0,1113.149,36.0,1113.149,22.0,1113.149,28.0,1113.0')] ).
cnf(1860,plain,
( ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ skC36
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41
| ~ skC42
| ~ skC43
| ~ skC44
| ~ skC45
| ~ skC46
| ~ skC47
| ~ skC48
| ~ skC49
| ~ skC50
| ~ skC51
| ~ skC52
| ~ skC53
| ~ skC54
| ~ skC55
| ~ skC56
| ~ skC57
| ~ skC58
| ~ skC59
| ~ skC60
| ~ skC61
| ~ skC62
| ~ skC63
| ~ skC64
| ~ skC65
| ~ skC66
| ~ skC67
| ~ skC68
| ~ skC69
| ~ skC70
| ~ skC71
| ~ skC72
| ~ skC73
| ~ skC74
| ~ skC75
| ~ skC76
| ~ skC77
| ~ skC78
| ~ skC79
| ~ skC80
| ~ skC81
| ~ skC82
| ~ skC83
| ~ skC84
| ~ skC85
| ~ skC86
| ~ skC87
| ~ skC88
| ~ skC89
| ~ skC90
| ~ skC91
| ~ skC92
| ~ skC93
| ~ skC94
| ~ skC95
| ~ skC96
| ~ skC97
| ~ skC98
| ~ skC99
| ~ skC100
| ~ skC101
| ~ skC102
| ~ skC103
| ~ skC104
| ~ skC105
| ~ skC106
| ~ skC107
| ~ skC108
| ~ skC109
| ~ skC110
| ~ skC111
| ~ skC112
| ~ skC113
| ~ skC114
| ~ skC115
| ~ skC116
| ~ skC117
| ~ skC118
| ~ skC119
| ~ skC120
| ~ skC121
| ~ skC122
| ~ skC123
| ~ skC124
| ~ skC125
| ~ skC126
| ~ skC127
| ~ skC128
| ~ skC129
| ~ skC130
| ~ skC131
| ~ skC132
| ~ skC133
| ~ skC134
| ~ skC135
| ~ skC136
| ~ skC137
| ~ skC138
| ~ skC139
| ~ skC140
| ~ skC141
| ~ skC142
| ~ skC143
| ~ skC144
| ~ skC145
| ~ skC146
| ~ skC147 ),
inference(obv,[status(thm),theory(equality)],[1859]),
[iquote('0:Obv:1859.197')] ).
cnf(1861,plain,
$false,
inference(mrr,[status(thm)],[1860,1846,1115,1842,1836,1828,1821,1818,1813,1809,1807,1799,1797,1793,1786,1783,1777,1772,1765,1761,1756,1754,1746,1743,1737,1734,1727,1725,1717,1711,1706,1702,1697,1694,1686,1680,1676,1674,1667,1663,1657,1654,1649,1647,1640,1632,1630,1625,1619,1615,1608,1600,1597,1590,1583,1577,1571,1563,1555,1551,1547,1544,1541,1536,1531,1529,1527,1519,1511,1506,1501,1498,1495,1493,1491,1485,1479,1475,1471,1464,1457,1453,1449,1441,1433,1431,1429,1423,1417,1410,1403,1400,1397,1392,1387,1382,1377,1370,1363,1359,1355,1352,1349,1347,1345,1337,1329,1323,1317,1311,1305,1303,1301,1296,1291,1283,1275,1271,1267,1260,1253,1250,1247,1245,1243,1240,1237,1230,1223,1218,1213,1205,1197,1191,1185,1181,1177,1174,1171,1167,1163,1157,1151,1144,1137,1132,1127,1125,1123]),
[iquote('0:MRR:1860.0,1860.1,1860.2,1860.3,1860.4,1860.5,1860.6,1860.7,1860.8,1860.9,1860.10,1860.11,1860.12,1860.13,1860.14,1860.15,1860.16,1860.17,1860.18,1860.19,1860.20,1860.21,1860.22,1860.23,1860.24,1860.25,1860.26,1860.27,1860.28,1860.29,1860.30,1860.31,1860.32,1860.33,1860.34,1860.35,1860.36,1860.37,1860.38,1860.39,1860.40,1860.41,1860.42,1860.43,1860.44,1860.45,1860.46,1860.47,1860.48,1860.49,1860.50,1860.51,1860.52,1860.53,1860.54,1860.55,1860.56,1860.57,1860.58,1860.59,1860.60,1860.61,1860.62,1860.63,1860.64,1860.65,1860.66,1860.67,1860.68,1860.69,1860.70,1860.71,1860.72,1860.73,1860.74,1860.75,1860.76,1860.77,1860.78,1860.79,1860.80,1860.81,1860.82,1860.83,1860.84,1860.85,1860.86,1860.87,1860.88,1860.89,1860.90,1860.91,1860.92,1860.93,1860.94,1860.95,1860.96,1860.97,1860.98,1860.99,1860.100,1860.101,1860.102,1860.103,1860.104,1860.105,1860.106,1860.107,1860.108,1860.109,1860.110,1860.111,1860.112,1860.113,1860.114,1860.115,1860.116,1860.117,1860.118,1860.119,1860.120,1860.121,1860.122,1860.123,1860.124,1860.125,1860.126,1860.127,1860.128,1860.129,1860.130,1860.131,1860.132,1860.133,1860.134,1860.135,1860.136,1860.137,1860.138,1860.139,1860.140,1860.141,1860.142,1860.143,1860.144,1860.145,1860.146,1860.147,1846.0,1115.0,1842.0,1836.0,1828.0,1821.0,1818.0,1813.0,1809.0,1807.0,1799.0,1797.0,1793.0,1786.0,1783.0,1777.0,1772.0,1765.0,1761.0,1756.0,1754.0,1746.0,1743.0,1737.0,1734.0,1727.0,1725.0,1717.0,1711.0,1706.0,1702.0,1697.0,1694.0,1686.0,1680.0,1676.0,1674.0,1667.0,1663.0,1657.0,1654.0,1649.0,1647.0,1640.0,1632.0,1630.0,1625.0,1619.0,1615.0,1608.0,1600.0,1597.0,1590.0,1583.0,1577.0,1571.0,1563.0,1555.0,1551.0,1547.0,1544.0,1541.0,1536.0,1531.0,1529.0,1527.0,1519.0,1511.0,1506.0,1501.0,1498.0,1495.0,1493.0,1491.0,1485.0,1479.0,1475.0,1471.0,1464.0,1457.0,1453.0,1449.0,1441.0,1433.0,1431.0,1429.0,1423.0,1417.0,1410.0,1403.0,1400.0,1397.0,1392.0,1387.0,1382.0,1377.0,1370.0,1363.0,1359.0,1355.0,1352.0,1349.0,1347.0,1345.0,1337.0,1329.0,1323.0,1317.0,1311.0,1305.0,1303.0,1301.0,1296.0,1291.0,1283.0,1275.0,1271.0,1267.0,1260.0,1253.0,1250.0,1247.0,1245.0,1243.0,1240.0,1237.0,1230.0,1223.0,1218.0,1213.0,1205.0,1197.0,1191.0,1185.0,1181.0,1177.0,1174.0,1171.0,1167.0,1163.0,1157.0,1151.0,1144.0,1137.0,1132.0,1127.0,1125.0,1123.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : ALG209+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 8 00:57:53 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.75/0.93
% 0.75/0.93 SPASS V 3.9
% 0.75/0.93 SPASS beiseite: Proof found.
% 0.75/0.93 % SZS status Theorem
% 0.75/0.93 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.75/0.93 SPASS derived 0 clauses, backtracked 0 clauses, performed 0 splits and kept 219 clauses.
% 0.75/0.93 SPASS allocated 88339 KBytes.
% 0.75/0.93 SPASS spent 0:00:00.59 on the problem.
% 0.75/0.93 0:00:00.04 for the input.
% 0.75/0.93 0:00:00.41 for the FLOTTER CNF translation.
% 0.75/0.93 0:00:00.00 for inferences.
% 0.75/0.93 0:00:00.00 for the backtracking.
% 0.75/0.93 0:00:00.10 for the reduction.
% 0.75/0.93
% 0.75/0.93
% 0.75/0.93 Here is a proof with depth 0, length 498 :
% 0.75/0.93 % SZS output start Refutation
% See solution above
% 0.75/0.93 Formulae used in the proof : ax1 ax2 co1
% 0.75/0.93
%------------------------------------------------------------------------------