%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG059+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n032.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:10 EDT 2022
% Result : Theorem 0.36s 0.56s
% Output : Refutation 0.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 161
% Syntax : Number of clauses : 544 ( 301 unt; 123 nHn; 544 RR)
% Number of literals : 1173 ( 0 equ; 446 neg)
% Maximal clause size : 25 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 29 usr; 29 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ equal(e1,e0),
file('ALG059+1.p',unknown),
[] ).
cnf(2,axiom,
~ equal(e2,e0),
file('ALG059+1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(e3,e0),
file('ALG059+1.p',unknown),
[] ).
cnf(4,axiom,
~ equal(e4,e0),
file('ALG059+1.p',unknown),
[] ).
cnf(5,axiom,
~ equal(e2,e1),
file('ALG059+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e3,e1),
file('ALG059+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(e4,e1),
file('ALG059+1.p',unknown),
[] ).
cnf(8,axiom,
~ equal(e3,e2),
file('ALG059+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(e4,e2),
file('ALG059+1.p',unknown),
[] ).
cnf(10,axiom,
~ equal(e4,e3),
file('ALG059+1.p',unknown),
[] ).
cnf(11,axiom,
equal(op(unit,e0),e0),
file('ALG059+1.p',unknown),
[] ).
cnf(12,axiom,
equal(op(e0,unit),e0),
file('ALG059+1.p',unknown),
[] ).
cnf(13,axiom,
equal(op(unit,e1),e1),
file('ALG059+1.p',unknown),
[] ).
cnf(14,axiom,
equal(op(e1,unit),e1),
file('ALG059+1.p',unknown),
[] ).
cnf(15,axiom,
equal(op(unit,e2),e2),
file('ALG059+1.p',unknown),
[] ).
cnf(16,axiom,
equal(op(e2,unit),e2),
file('ALG059+1.p',unknown),
[] ).
cnf(17,axiom,
equal(op(unit,e3),e3),
file('ALG059+1.p',unknown),
[] ).
cnf(18,axiom,
equal(op(e3,unit),e3),
file('ALG059+1.p',unknown),
[] ).
cnf(19,axiom,
equal(op(unit,e4),e4),
file('ALG059+1.p',unknown),
[] ).
cnf(20,axiom,
equal(op(e4,unit),e4),
file('ALG059+1.p',unknown),
[] ).
cnf(21,axiom,
equal(op(e2,e2),e3),
file('ALG059+1.p',unknown),
[] ).
cnf(22,axiom,
equal(op(op(e2,e2),e2),e1),
file('ALG059+1.p',unknown),
[] ).
cnf(24,axiom,
~ equal(op(e2,e0),op(e0,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(26,axiom,
~ equal(op(e4,e0),op(e0,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(28,axiom,
~ equal(op(e3,e0),op(e1,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(29,axiom,
~ equal(op(e4,e0),op(e1,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(30,axiom,
~ equal(op(e3,e0),op(e2,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(31,axiom,
~ equal(op(e4,e0),op(e2,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(32,axiom,
~ equal(op(e4,e0),op(e3,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(33,axiom,
~ equal(op(e1,e1),op(e0,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(34,axiom,
~ equal(op(e2,e1),op(e0,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(35,axiom,
~ equal(op(e3,e1),op(e0,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(37,axiom,
~ equal(op(e2,e1),op(e1,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(38,axiom,
~ equal(op(e3,e1),op(e1,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(39,axiom,
~ equal(op(e4,e1),op(e1,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(40,axiom,
~ equal(op(e3,e1),op(e2,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(42,axiom,
~ equal(op(e4,e1),op(e3,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(43,axiom,
~ equal(op(e1,e2),op(e0,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(44,axiom,
~ equal(op(e2,e2),op(e0,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(45,axiom,
~ equal(op(e3,e2),op(e0,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(46,axiom,
~ equal(op(e4,e2),op(e0,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(47,axiom,
~ equal(op(e2,e2),op(e1,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(48,axiom,
~ equal(op(e3,e2),op(e1,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(49,axiom,
~ equal(op(e4,e2),op(e1,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(52,axiom,
~ equal(op(e4,e2),op(e3,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(53,axiom,
~ equal(op(e1,e3),op(e0,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(55,axiom,
~ equal(op(e3,e3),op(e0,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(56,axiom,
~ equal(op(e4,e3),op(e0,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(57,axiom,
~ equal(op(e2,e3),op(e1,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(58,axiom,
~ equal(op(e3,e3),op(e1,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(59,axiom,
~ equal(op(e4,e3),op(e1,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(60,axiom,
~ equal(op(e3,e3),op(e2,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(66,axiom,
~ equal(op(e4,e4),op(e0,e4)),
file('ALG059+1.p',unknown),
[] ).
cnf(67,axiom,
~ equal(op(e2,e4),op(e1,e4)),
file('ALG059+1.p',unknown),
[] ).
cnf(72,axiom,
~ equal(op(e4,e4),op(e3,e4)),
file('ALG059+1.p',unknown),
[] ).
cnf(77,axiom,
~ equal(op(e0,e2),op(e0,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(80,axiom,
~ equal(op(e0,e3),op(e0,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(82,axiom,
~ equal(op(e0,e4),op(e0,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(85,axiom,
~ equal(op(e1,e3),op(e1,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(87,axiom,
~ equal(op(e1,e2),op(e1,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(88,axiom,
~ equal(op(e1,e3),op(e1,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(90,axiom,
~ equal(op(e1,e3),op(e1,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(92,axiom,
~ equal(op(e1,e4),op(e1,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(93,axiom,
~ equal(op(e2,e1),op(e2,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(94,axiom,
~ equal(op(e2,e2),op(e2,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(95,axiom,
~ equal(op(e2,e3),op(e2,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(97,axiom,
~ equal(op(e2,e2),op(e2,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(98,axiom,
~ equal(op(e2,e3),op(e2,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(100,axiom,
~ equal(op(e2,e3),op(e2,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(103,axiom,
~ equal(op(e3,e1),op(e3,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(104,axiom,
~ equal(op(e3,e2),op(e3,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(105,axiom,
~ equal(op(e3,e3),op(e3,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(106,axiom,
~ equal(op(e3,e4),op(e3,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(107,axiom,
~ equal(op(e3,e2),op(e3,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(108,axiom,
~ equal(op(e3,e3),op(e3,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(109,axiom,
~ equal(op(e3,e4),op(e3,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(113,axiom,
~ equal(op(e4,e1),op(e4,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(114,axiom,
~ equal(op(e4,e2),op(e4,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(116,axiom,
~ equal(op(e4,e4),op(e4,e0)),
file('ALG059+1.p',unknown),
[] ).
cnf(117,axiom,
~ equal(op(e4,e2),op(e4,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(118,axiom,
~ equal(op(e4,e3),op(e4,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(119,axiom,
~ equal(op(e4,e4),op(e4,e1)),
file('ALG059+1.p',unknown),
[] ).
cnf(121,axiom,
~ equal(op(e4,e4),op(e4,e2)),
file('ALG059+1.p',unknown),
[] ).
cnf(122,axiom,
~ equal(op(e4,e4),op(e4,e3)),
file('ALG059+1.p',unknown),
[] ).
cnf(123,axiom,
( ~ skC4
| equal(op(op(e0,e0),e0),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(125,axiom,
( ~ skC6
| equal(op(op(e0,e2),e2),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(126,axiom,
( ~ skC7
| equal(op(op(e0,e3),e3),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(127,axiom,
( ~ skC8
| equal(op(op(e0,e4),e4),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(129,axiom,
( ~ skC10
| equal(op(op(e1,e1),e1),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(130,axiom,
( ~ skC11
| equal(op(op(e1,e2),e2),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(135,axiom,
( ~ skC16
| equal(op(op(e2,e2),e2),e2) ),
file('ALG059+1.p',unknown),
[] ).
cnf(136,axiom,
( ~ skC17
| equal(op(op(e2,e3),e3),e2) ),
file('ALG059+1.p',unknown),
[] ).
cnf(139,axiom,
( ~ skC20
| equal(op(op(e3,e1),e1),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(140,axiom,
( ~ skC21
| equal(op(op(e3,e2),e2),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(141,axiom,
( ~ skC22
| equal(op(op(e3,e3),e3),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(142,axiom,
( ~ skC23
| equal(op(op(e3,e4),e4),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(144,axiom,
( ~ skC25
| equal(op(op(e4,e1),e1),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(145,axiom,
( ~ skC26
| equal(op(op(e4,e2),e2),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(146,axiom,
( ~ skC27
| equal(op(op(e4,e3),e3),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(147,axiom,
equal(op(op(e2,e2),op(e2,e2)),e4),
file('ALG059+1.p',unknown),
[] ).
cnf(149,axiom,
( ~ equal(op(op(e0,e0),e0),e0)
| ~ skC4 ),
file('ALG059+1.p',unknown),
[] ).
cnf(151,axiom,
( ~ skC5
| ~ equal(op(op(e0,e1),e0),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(159,axiom,
( ~ skC9
| ~ equal(op(op(e1,e0),e1),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(161,axiom,
( ~ equal(op(op(e1,e1),e1),e1)
| ~ skC10 ),
file('ALG059+1.p',unknown),
[] ).
cnf(164,axiom,
( ~ skC12
| ~ equal(op(e3,e1),op(e1,e3)) ),
file('ALG059+1.p',unknown),
[] ).
cnf(166,axiom,
( ~ skC13
| ~ equal(op(e4,e1),op(e1,e4)) ),
file('ALG059+1.p',unknown),
[] ).
cnf(168,axiom,
( ~ skC14
| ~ equal(op(e2,e0),op(e0,e2)) ),
file('ALG059+1.p',unknown),
[] ).
cnf(170,axiom,
( ~ skC15
| ~ equal(op(e2,e1),op(e1,e2)) ),
file('ALG059+1.p',unknown),
[] ).
cnf(177,axiom,
( ~ skC18
| ~ equal(op(op(e2,e4),e2),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(178,axiom,
( ~ skC19
| ~ equal(op(e3,e0),op(e0,e3)) ),
file('ALG059+1.p',unknown),
[] ).
cnf(185,axiom,
( ~ equal(op(op(e3,e3),e3),e3)
| ~ skC22 ),
file('ALG059+1.p',unknown),
[] ).
cnf(188,axiom,
( ~ skC24
| ~ equal(op(e4,e0),op(e0,e4)) ),
file('ALG059+1.p',unknown),
[] ).
cnf(202,axiom,
( ~ equal(e0,unit)
| ~ equal(op(e1,e1),e0)
| ~ skC0 ),
file('ALG059+1.p',unknown),
[] ).
cnf(238,axiom,
( ~ equal(e1,unit)
| ~ equal(op(e3,e2),e1)
| ~ skC1 ),
file('ALG059+1.p',unknown),
[] ).
cnf(283,axiom,
( ~ equal(e3,unit)
| ~ equal(op(e2,e2),e3)
| ~ skC3 ),
file('ALG059+1.p',unknown),
[] ).
cnf(300,axiom,
( ~ equal(op(e1,e1),e0)
| ~ skC0
| equal(op(e1,e0),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(311,axiom,
( ~ equal(op(e3,e4),e0)
| ~ skC0
| equal(op(e3,e0),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(316,axiom,
( ~ equal(op(e0,e0),e1)
| ~ skC1
| equal(op(e0,e1),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(318,axiom,
( ~ skC1
| ~ equal(op(e0,e3),e1)
| equal(op(e0,e1),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(326,axiom,
( ~ equal(op(e2,e3),e1)
| ~ skC1
| equal(op(e2,e1),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(329,axiom,
( ~ equal(op(e3,e2),e1)
| ~ skC1
| equal(op(e3,e1),e2) ),
file('ALG059+1.p',unknown),
[] ).
cnf(332,axiom,
( ~ equal(op(e4,e0),e1)
| ~ skC1
| equal(op(e4,e1),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(342,axiom,
( ~ equal(op(e1,e3),e2)
| ~ skC2
| equal(op(e1,e2),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(344,axiom,
( ~ equal(op(e2,e0),e2)
| ~ skC2
| equal(op(e2,e2),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(345,axiom,
( ~ equal(op(e2,e1),e2)
| ~ skC2
| equal(op(e2,e2),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(353,axiom,
( ~ equal(op(e4,e1),e2)
| ~ skC2
| equal(op(e4,e2),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(355,axiom,
( ~ skC2
| ~ equal(op(e4,e4),e2)
| equal(op(e4,e2),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(366,axiom,
( ~ equal(op(e2,e2),e3)
| ~ skC3
| equal(op(e2,e3),e2) ),
file('ALG059+1.p',unknown),
[] ).
cnf(368,axiom,
( ~ equal(op(e3,e0),e3)
| ~ skC3
| equal(op(e3,e3),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(376,axiom,
equal(op(op(op(e2,e2),e2),op(op(e2,e2),e2)),e0),
file('ALG059+1.p',unknown),
[] ).
cnf(404,axiom,
( ~ equal(op(e0,e2),e4)
| skC3
| skC2
| skC1
| skC0
| equal(op(e0,e4),e2) ),
file('ALG059+1.p',unknown),
[] ).
cnf(417,axiom,
( ~ equal(op(e3,e3),e4)
| equal(op(e3,e4),e3)
| skC0
| skC1
| skC2
| skC3 ),
file('ALG059+1.p',unknown),
[] ).
cnf(419,axiom,
( ~ equal(op(e4,e1),e4)
| skC3
| skC2
| skC1
| skC0
| equal(op(e4,e4),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(422,axiom,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit)
| equal(e0,unit) ),
file('ALG059+1.p',unknown),
[] ).
cnf(427,axiom,
( equal(op(e4,e4),e2)
| equal(op(e2,e4),e2)
| equal(op(e3,e4),e2)
| equal(op(e1,e4),e2)
| equal(op(e0,e4),e2) ),
file('ALG059+1.p',unknown),
[] ).
cnf(439,axiom,
( equal(op(e0,e3),e1)
| equal(op(e1,e3),e1)
| equal(op(e2,e3),e1)
| equal(op(e3,e3),e1)
| equal(op(e4,e3),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(442,axiom,
( equal(op(e3,e0),e0)
| equal(op(e3,e1),e0)
| equal(op(e3,e2),e0)
| equal(op(e3,e3),e0)
| equal(op(e3,e4),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(450,axiom,
( equal(op(e2,e0),e1)
| equal(op(e2,e1),e1)
| equal(op(e2,e2),e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e4),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(451,axiom,
( equal(op(e0,e2),e0)
| equal(op(e1,e2),e0)
| equal(op(e2,e2),e0)
| equal(op(e3,e2),e0)
| equal(op(e4,e2),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(453,axiom,
( equal(op(e0,e1),e4)
| equal(op(e1,e1),e4)
| equal(op(e2,e1),e4)
| equal(op(e3,e1),e4)
| equal(op(e4,e1),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(454,axiom,
( equal(op(e1,e0),e4)
| equal(op(e1,e1),e4)
| equal(op(e1,e2),e4)
| equal(op(e1,e3),e4)
| equal(op(e1,e4),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(455,axiom,
( equal(op(e0,e1),e3)
| equal(op(e1,e1),e3)
| equal(op(e2,e1),e3)
| equal(op(e3,e1),e3)
| equal(op(e4,e1),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(456,axiom,
( equal(op(e1,e0),e3)
| equal(op(e1,e1),e3)
| equal(op(e1,e2),e3)
| equal(op(e1,e3),e3)
| equal(op(e1,e4),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(464,axiom,
( equal(op(e0,e0),e4)
| equal(op(e0,e1),e4)
| equal(op(e0,e2),e4)
| equal(op(e0,e3),e4)
| equal(op(e0,e4),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(466,axiom,
( equal(op(e0,e0),e3)
| equal(op(e0,e1),e3)
| equal(op(e0,e2),e3)
| equal(op(e0,e3),e3)
| equal(op(e0,e4),e3) ),
file('ALG059+1.p',unknown),
[] ).
cnf(468,axiom,
( equal(op(e0,e2),e2)
| equal(op(e0,e0),e2)
| equal(op(e0,e4),e2)
| equal(op(e0,e3),e2)
| equal(op(e0,e1),e2) ),
file('ALG059+1.p',unknown),
[] ).
cnf(470,axiom,
( equal(op(e0,e0),e1)
| equal(op(e0,e1),e1)
| equal(op(e0,e2),e1)
| equal(op(e0,e3),e1)
| equal(op(e0,e4),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(473,axiom,
( equal(op(e4,e4),e4)
| equal(op(e4,e4),e3)
| equal(op(e4,e4),e2)
| equal(op(e4,e4),e1)
| equal(op(e4,e4),e0) ),
file('ALG059+1.p',unknown),
[] ).
cnf(476,axiom,
( equal(op(e4,e1),e0)
| equal(op(e4,e1),e1)
| equal(op(e4,e1),e2)
| equal(op(e4,e1),e3)
| equal(op(e4,e1),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(477,axiom,
( equal(op(e4,e0),e4)
| equal(op(e4,e0),e0)
| equal(op(e4,e0),e3)
| equal(op(e4,e0),e2)
| equal(op(e4,e0),e1) ),
file('ALG059+1.p',unknown),
[] ).
cnf(481,axiom,
( equal(op(e3,e1),e0)
| equal(op(e3,e1),e1)
| equal(op(e3,e1),e2)
| equal(op(e3,e1),e3)
| equal(op(e3,e1),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(482,axiom,
( equal(op(e3,e0),e0)
| equal(op(e3,e0),e1)
| equal(op(e3,e0),e2)
| equal(op(e3,e0),e3)
| equal(op(e3,e0),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(484,axiom,
( equal(op(e2,e3),e0)
| equal(op(e2,e3),e1)
| equal(op(e2,e3),e2)
| equal(op(e2,e3),e3)
| equal(op(e2,e3),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(486,axiom,
( equal(op(e2,e1),e0)
| equal(op(e2,e1),e1)
| equal(op(e2,e1),e2)
| equal(op(e2,e1),e3)
| equal(op(e2,e1),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(487,axiom,
( equal(op(e2,e0),e0)
| equal(op(e2,e0),e1)
| equal(op(e2,e0),e2)
| equal(op(e2,e0),e3)
| equal(op(e2,e0),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(489,axiom,
( equal(op(e1,e3),e0)
| equal(op(e1,e3),e1)
| equal(op(e1,e3),e2)
| equal(op(e1,e3),e3)
| equal(op(e1,e3),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(490,axiom,
( equal(op(e1,e2),e0)
| equal(op(e1,e2),e1)
| equal(op(e1,e2),e2)
| equal(op(e1,e2),e3)
| equal(op(e1,e2),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(494,axiom,
( equal(op(e0,e3),e0)
| equal(op(e0,e3),e1)
| equal(op(e0,e3),e2)
| equal(op(e0,e3),e3)
| equal(op(e0,e3),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(495,axiom,
( equal(op(e0,e2),e0)
| equal(op(e0,e2),e1)
| equal(op(e0,e2),e2)
| equal(op(e0,e2),e3)
| equal(op(e0,e2),e4) ),
file('ALG059+1.p',unknown),
[] ).
cnf(498,axiom,
( equal(op(op(e4,e4),e4),e4)
| skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23
| skC24
| skC25
| skC26
| skC27 ),
file('ALG059+1.p',unknown),
[] ).
cnf(499,axiom,
( ~ equal(op(op(e4,e4),e4),e4)
| skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23
| skC24
| skC25
| skC26
| skC27 ),
file('ALG059+1.p',unknown),
[] ).
cnf(501,plain,
equal(op(e3,e2),e1),
inference(rew,[status(thm),theory(equality)],[21,22]),
[iquote('0:Rew:21.0,22.0')] ).
cnf(504,plain,
~ equal(op(e3,e1),e1),
inference(rew,[status(thm),theory(equality)],[501,107]),
[iquote('0:Rew:501.0,107.0')] ).
cnf(505,plain,
~ equal(op(e3,e0),e1),
inference(rew,[status(thm),theory(equality)],[501,104]),
[iquote('0:Rew:501.0,104.0')] ).
cnf(507,plain,
~ equal(op(e2,e3),e3),
inference(rew,[status(thm),theory(equality)],[21,100]),
[iquote('0:Rew:21.0,100.0')] ).
cnf(508,plain,
~ equal(op(e2,e1),e3),
inference(rew,[status(thm),theory(equality)],[21,97]),
[iquote('0:Rew:21.0,97.0')] ).
cnf(509,plain,
~ equal(op(e2,e0),e3),
inference(rew,[status(thm),theory(equality)],[21,94]),
[iquote('0:Rew:21.0,94.0')] ).
cnf(510,plain,
~ equal(op(e4,e2),e1),
inference(rew,[status(thm),theory(equality)],[501,52]),
[iquote('0:Rew:501.0,52.0')] ).
cnf(513,plain,
~ equal(op(e1,e2),e1),
inference(rew,[status(thm),theory(equality)],[501,48]),
[iquote('0:Rew:501.0,48.0')] ).
cnf(514,plain,
~ equal(op(e1,e2),e3),
inference(rew,[status(thm),theory(equality)],[21,47]),
[iquote('0:Rew:21.0,47.0')] ).
cnf(515,plain,
~ equal(op(e0,e2),e1),
inference(rew,[status(thm),theory(equality)],[501,45]),
[iquote('0:Rew:501.0,45.0')] ).
cnf(516,plain,
~ equal(op(e0,e2),e3),
inference(rew,[status(thm),theory(equality)],[21,44]),
[iquote('0:Rew:21.0,44.0')] ).
cnf(517,plain,
equal(op(e3,e3),e4),
inference(rew,[status(thm),theory(equality)],[21,147]),
[iquote('0:Rew:21.0,147.0')] ).
cnf(520,plain,
~ equal(op(e3,e1),e4),
inference(rew,[status(thm),theory(equality)],[517,108]),
[iquote('0:Rew:517.0,108.0')] ).
cnf(521,plain,
~ equal(op(e3,e0),e4),
inference(rew,[status(thm),theory(equality)],[517,105]),
[iquote('0:Rew:517.0,105.0')] ).
cnf(523,plain,
~ equal(op(e2,e3),e4),
inference(rew,[status(thm),theory(equality)],[517,60]),
[iquote('0:Rew:517.0,60.0')] ).
cnf(524,plain,
~ equal(op(e1,e3),e4),
inference(rew,[status(thm),theory(equality)],[517,58]),
[iquote('0:Rew:517.0,58.0')] ).
cnf(525,plain,
~ equal(op(e0,e3),e4),
inference(rew,[status(thm),theory(equality)],[517,55]),
[iquote('0:Rew:517.0,55.0')] ).
cnf(526,plain,
( ~ skC22
| equal(op(e4,e3),e3) ),
inference(rew,[status(thm),theory(equality)],[517,141]),
[iquote('0:Rew:517.0,141.1')] ).
cnf(527,plain,
( ~ skC21
| equal(op(e1,e2),e3) ),
inference(rew,[status(thm),theory(equality)],[501,140]),
[iquote('0:Rew:501.0,140.1')] ).
cnf(528,plain,
~ skC21,
inference(mrr,[status(thm)],[527,514]),
[iquote('0:MRR:527.1,514.0')] ).
cnf(529,plain,
( ~ skC16
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[501,135,21]),
[iquote('0:Rew:501.0,135.1,21.0,135.1')] ).
cnf(530,plain,
~ skC16,
inference(mrr,[status(thm)],[529,5]),
[iquote('0:MRR:529.1,5.0')] ).
cnf(531,plain,
( ~ equal(e3,e3)
| ~ skC22 ),
inference(rew,[status(thm),theory(equality)],[526,185,517]),
[iquote('0:Rew:526.1,185.0,517.0,185.0')] ).
cnf(532,plain,
~ skC22,
inference(obv,[status(thm),theory(equality)],[531]),
[iquote('0:Obv:531.0')] ).
cnf(536,plain,
( ~ equal(e1,e1)
| ~ skC10 ),
inference(rew,[status(thm),theory(equality)],[129,161]),
[iquote('0:Rew:129.1,161.0')] ).
cnf(537,plain,
~ skC10,
inference(obv,[status(thm),theory(equality)],[536]),
[iquote('0:Obv:536.0')] ).
cnf(539,plain,
( ~ equal(e0,e0)
| ~ skC4 ),
inference(rew,[status(thm),theory(equality)],[123,149]),
[iquote('0:Rew:123.1,149.0')] ).
cnf(540,plain,
~ skC4,
inference(obv,[status(thm),theory(equality)],[539]),
[iquote('0:Obv:539.0')] ).
cnf(544,plain,
( ~ equal(e3,unit)
| ~ equal(e3,e3)
| ~ skC3 ),
inference(rew,[status(thm),theory(equality)],[21,283]),
[iquote('0:Rew:21.0,283.1')] ).
cnf(545,plain,
( ~ skC3
| ~ equal(e3,unit) ),
inference(obv,[status(thm),theory(equality)],[544]),
[iquote('0:Obv:544.1')] ).
cnf(550,plain,
( ~ equal(e1,unit)
| ~ equal(e1,e1)
| ~ skC1 ),
inference(rew,[status(thm),theory(equality)],[501,238]),
[iquote('0:Rew:501.0,238.1')] ).
cnf(551,plain,
( ~ skC1
| ~ equal(e1,unit) ),
inference(obv,[status(thm),theory(equality)],[550]),
[iquote('0:Obv:550.1')] ).
cnf(555,plain,
equal(op(e1,e1),e0),
inference(rew,[status(thm),theory(equality)],[501,376,21]),
[iquote('0:Rew:501.0,376.0,21.0,376.0')] ).
cnf(557,plain,
~ equal(op(e1,e3),e0),
inference(rew,[status(thm),theory(equality)],[555,88]),
[iquote('0:Rew:555.0,88.0')] ).
cnf(558,plain,
~ equal(op(e1,e2),e0),
inference(rew,[status(thm),theory(equality)],[555,87]),
[iquote('0:Rew:555.0,87.0')] ).
cnf(560,plain,
~ equal(op(e4,e1),e0),
inference(rew,[status(thm),theory(equality)],[555,39]),
[iquote('0:Rew:555.0,39.0')] ).
cnf(561,plain,
~ equal(op(e3,e1),e0),
inference(rew,[status(thm),theory(equality)],[555,38]),
[iquote('0:Rew:555.0,38.0')] ).
cnf(562,plain,
~ equal(op(e2,e1),e0),
inference(rew,[status(thm),theory(equality)],[555,37]),
[iquote('0:Rew:555.0,37.0')] ).
cnf(563,plain,
~ equal(op(e0,e1),e0),
inference(rew,[status(thm),theory(equality)],[555,33]),
[iquote('0:Rew:555.0,33.0')] ).
cnf(565,plain,
( ~ equal(e0,unit)
| ~ equal(e0,e0)
| ~ skC0 ),
inference(rew,[status(thm),theory(equality)],[555,202]),
[iquote('0:Rew:555.0,202.1')] ).
cnf(566,plain,
( ~ skC0
| ~ equal(e0,unit) ),
inference(obv,[status(thm),theory(equality)],[565]),
[iquote('0:Obv:565.1')] ).
cnf(571,plain,
( ~ equal(op(e3,e0),e3)
| ~ skC3
| equal(e4,e0) ),
inference(rew,[status(thm),theory(equality)],[517,368]),
[iquote('0:Rew:517.0,368.2')] ).
cnf(572,plain,
( ~ skC3
| ~ equal(op(e3,e0),e3) ),
inference(mrr,[status(thm)],[571,4]),
[iquote('0:MRR:571.2,4.0')] ).
cnf(573,plain,
( ~ equal(e3,e3)
| ~ skC3
| equal(op(e2,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[21,366]),
[iquote('0:Rew:21.0,366.0')] ).
cnf(574,plain,
( ~ skC3
| equal(op(e2,e3),e2) ),
inference(obv,[status(thm),theory(equality)],[573]),
[iquote('0:Obv:573.0')] ).
cnf(580,plain,
( ~ skC2
| ~ equal(op(e4,e1),e2) ),
inference(mrr,[status(thm)],[353,510]),
[iquote('0:MRR:353.2,510.0')] ).
cnf(588,plain,
( ~ equal(op(e2,e1),e2)
| ~ skC2
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[21,345]),
[iquote('0:Rew:21.0,345.2')] ).
cnf(589,plain,
( ~ skC2
| ~ equal(op(e2,e1),e2) ),
inference(mrr,[status(thm)],[588,6]),
[iquote('0:MRR:588.2,6.0')] ).
cnf(590,plain,
( ~ equal(op(e2,e0),e2)
| ~ skC2
| equal(e3,e0) ),
inference(rew,[status(thm),theory(equality)],[21,344]),
[iquote('0:Rew:21.0,344.2')] ).
cnf(591,plain,
( ~ skC2
| ~ equal(op(e2,e0),e2) ),
inference(mrr,[status(thm)],[590,3]),
[iquote('0:MRR:590.2,3.0')] ).
cnf(592,plain,
( ~ skC2
| ~ equal(op(e1,e3),e2) ),
inference(mrr,[status(thm)],[342,514]),
[iquote('0:MRR:342.2,514.0')] ).
cnf(597,plain,
( ~ skC1
| ~ equal(op(e4,e0),e1) ),
inference(mrr,[status(thm)],[332,560]),
[iquote('0:MRR:332.2,560.0')] ).
cnf(599,plain,
( ~ equal(e1,e1)
| ~ skC1
| equal(op(e3,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[501,329]),
[iquote('0:Rew:501.0,329.0')] ).
cnf(600,plain,
( ~ skC1
| equal(op(e3,e1),e2) ),
inference(obv,[status(thm),theory(equality)],[599]),
[iquote('0:Obv:599.0')] ).
cnf(601,plain,
( ~ skC1
| ~ equal(op(e2,e3),e1) ),
inference(mrr,[status(thm)],[326,508]),
[iquote('0:MRR:326.2,508.0')] ).
cnf(608,plain,
( ~ skC1
| ~ equal(op(e0,e0),e1) ),
inference(mrr,[status(thm)],[316,563]),
[iquote('0:MRR:316.2,563.0')] ).
cnf(609,plain,
( ~ skC0
| ~ equal(op(e3,e4),e0) ),
inference(mrr,[status(thm)],[311,521]),
[iquote('0:MRR:311.2,521.0')] ).
cnf(614,plain,
( ~ equal(e0,e0)
| ~ skC0
| equal(op(e1,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[555,300]),
[iquote('0:Rew:555.0,300.0')] ).
cnf(615,plain,
( ~ skC0
| equal(op(e1,e0),e1) ),
inference(obv,[status(thm),theory(equality)],[614]),
[iquote('0:Obv:614.0')] ).
cnf(618,plain,
( ~ equal(e4,e4)
| equal(op(e3,e4),e3)
| skC0
| skC1
| skC2
| skC3 ),
inference(rew,[status(thm),theory(equality)],[517,417]),
[iquote('0:Rew:517.0,417.0')] ).
cnf(619,plain,
( skC3
| skC2
| skC1
| skC0
| equal(op(e3,e4),e3) ),
inference(obv,[status(thm),theory(equality)],[618]),
[iquote('0:Obv:618.0')] ).
cnf(640,plain,
( equal(op(e0,e3),e1)
| equal(op(e1,e3),e1)
| equal(op(e2,e3),e1)
| equal(e4,e1)
| equal(op(e4,e3),e1) ),
inference(rew,[status(thm),theory(equality)],[517,439]),
[iquote('0:Rew:517.0,439.3')] ).
cnf(641,plain,
( equal(op(e1,e3),e1)
| equal(op(e4,e3),e1)
| equal(op(e2,e3),e1)
| equal(op(e0,e3),e1) ),
inference(mrr,[status(thm)],[640,7]),
[iquote('0:MRR:640.3,7.0')] ).
cnf(644,plain,
( equal(op(e3,e0),e0)
| equal(op(e3,e1),e0)
| equal(e1,e0)
| equal(e4,e0)
| equal(op(e3,e4),e0) ),
inference(rew,[status(thm),theory(equality)],[517,442,501]),
[iquote('0:Rew:517.0,442.3,501.0,442.2')] ).
cnf(645,plain,
( equal(op(e3,e0),e0)
| equal(op(e3,e4),e0) ),
inference(mrr,[status(thm)],[644,561,1,4]),
[iquote('0:MRR:644.1,644.2,644.3,561.0,1.0,4.0')] ).
cnf(654,plain,
( equal(op(e2,e0),e1)
| equal(op(e2,e1),e1)
| equal(e3,e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[21,450]),
[iquote('0:Rew:21.0,450.2')] ).
cnf(655,plain,
( equal(op(e2,e1),e1)
| equal(op(e2,e4),e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[654,6]),
[iquote('0:MRR:654.2,6.0')] ).
cnf(656,plain,
( equal(op(e0,e2),e0)
| equal(op(e1,e2),e0)
| equal(e3,e0)
| equal(e1,e0)
| equal(op(e4,e2),e0) ),
inference(rew,[status(thm),theory(equality)],[501,451,21]),
[iquote('0:Rew:501.0,451.3,21.0,451.2')] ).
cnf(657,plain,
( equal(op(e0,e2),e0)
| equal(op(e4,e2),e0) ),
inference(mrr,[status(thm)],[656,558,3,1]),
[iquote('0:MRR:656.1,656.2,656.3,558.0,3.0,1.0')] ).
cnf(660,plain,
( equal(op(e0,e1),e4)
| equal(e4,e0)
| equal(op(e2,e1),e4)
| equal(op(e3,e1),e4)
| equal(op(e4,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[555,453]),
[iquote('0:Rew:555.0,453.1')] ).
cnf(661,plain,
( equal(op(e4,e1),e4)
| equal(op(e2,e1),e4)
| equal(op(e0,e1),e4) ),
inference(mrr,[status(thm)],[660,4,520]),
[iquote('0:MRR:660.1,660.3,4.0,520.0')] ).
cnf(662,plain,
( equal(op(e1,e0),e4)
| equal(e4,e0)
| equal(op(e1,e2),e4)
| equal(op(e1,e3),e4)
| equal(op(e1,e4),e4) ),
inference(rew,[status(thm),theory(equality)],[555,454]),
[iquote('0:Rew:555.0,454.1')] ).
cnf(663,plain,
( equal(op(e1,e4),e4)
| equal(op(e1,e2),e4)
| equal(op(e1,e0),e4) ),
inference(mrr,[status(thm)],[662,4,524]),
[iquote('0:MRR:662.1,662.3,4.0,524.0')] ).
cnf(664,plain,
( equal(op(e0,e1),e3)
| equal(e3,e0)
| equal(op(e2,e1),e3)
| equal(op(e3,e1),e3)
| equal(op(e4,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[555,455]),
[iquote('0:Rew:555.0,455.1')] ).
cnf(665,plain,
( equal(op(e3,e1),e3)
| equal(op(e4,e1),e3)
| equal(op(e0,e1),e3) ),
inference(mrr,[status(thm)],[664,3,508]),
[iquote('0:MRR:664.1,664.2,3.0,508.0')] ).
cnf(666,plain,
( equal(op(e1,e0),e3)
| equal(e3,e0)
| equal(op(e1,e2),e3)
| equal(op(e1,e3),e3)
| equal(op(e1,e4),e3) ),
inference(rew,[status(thm),theory(equality)],[555,456]),
[iquote('0:Rew:555.0,456.1')] ).
cnf(667,plain,
( equal(op(e1,e3),e3)
| equal(op(e1,e4),e3)
| equal(op(e1,e0),e3) ),
inference(mrr,[status(thm)],[666,3,514]),
[iquote('0:MRR:666.1,666.2,3.0,514.0')] ).
cnf(677,plain,
( equal(op(e0,e4),e4)
| equal(op(e0,e0),e4)
| equal(op(e0,e2),e4)
| equal(op(e0,e1),e4) ),
inference(mrr,[status(thm)],[464,525]),
[iquote('0:MRR:464.3,525.0')] ).
cnf(679,plain,
( equal(op(e0,e3),e3)
| equal(op(e0,e0),e3)
| equal(op(e0,e4),e3)
| equal(op(e0,e1),e3) ),
inference(mrr,[status(thm)],[466,516]),
[iquote('0:MRR:466.2,516.0')] ).
cnf(681,plain,
( equal(op(e0,e1),e1)
| equal(op(e0,e0),e1)
| equal(op(e0,e4),e1)
| equal(op(e0,e3),e1) ),
inference(mrr,[status(thm)],[470,515]),
[iquote('0:MRR:470.2,515.0')] ).
cnf(686,plain,
( equal(op(e4,e1),e4)
| equal(op(e4,e1),e1)
| equal(op(e4,e1),e3)
| equal(op(e4,e1),e2) ),
inference(mrr,[status(thm)],[476,560]),
[iquote('0:MRR:476.0,560.0')] ).
cnf(688,plain,
( equal(op(e3,e1),e3)
| equal(op(e3,e1),e2) ),
inference(mrr,[status(thm)],[481,561,504,520]),
[iquote('0:MRR:481.0,481.1,481.4,561.0,504.0,520.0')] ).
cnf(689,plain,
( equal(op(e3,e0),e3)
| equal(op(e3,e0),e0)
| equal(op(e3,e0),e2) ),
inference(mrr,[status(thm)],[482,505,521]),
[iquote('0:MRR:482.1,482.4,505.0,521.0')] ).
cnf(691,plain,
( equal(op(e2,e3),e2)
| equal(op(e2,e3),e1)
| equal(op(e2,e3),e0) ),
inference(mrr,[status(thm)],[484,507,523]),
[iquote('0:MRR:484.3,484.4,507.0,523.0')] ).
cnf(692,plain,
( equal(op(e2,e1),e2)
| equal(op(e2,e1),e1)
| equal(op(e2,e1),e4) ),
inference(mrr,[status(thm)],[486,562,508]),
[iquote('0:MRR:486.0,486.3,562.0,508.0')] ).
cnf(693,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e0)
| equal(op(e2,e0),e4)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[487,509]),
[iquote('0:MRR:487.3,509.0')] ).
cnf(695,plain,
( equal(op(e1,e3),e3)
| equal(op(e1,e3),e1)
| equal(op(e1,e3),e2) ),
inference(mrr,[status(thm)],[489,557,524]),
[iquote('0:MRR:489.0,489.4,557.0,524.0')] ).
cnf(696,plain,
( equal(op(e1,e2),e2)
| equal(op(e1,e2),e4) ),
inference(mrr,[status(thm)],[490,558,513,514]),
[iquote('0:MRR:490.0,490.1,490.3,558.0,513.0,514.0')] ).
cnf(698,plain,
( equal(op(e0,e3),e3)
| equal(op(e0,e3),e0)
| equal(op(e0,e3),e2)
| equal(op(e0,e3),e1) ),
inference(mrr,[status(thm)],[494,525]),
[iquote('0:MRR:494.4,525.0')] ).
cnf(699,plain,
( equal(op(e0,e2),e2)
| equal(op(e0,e2),e0)
| equal(op(e0,e2),e4) ),
inference(mrr,[status(thm)],[495,515,516]),
[iquote('0:MRR:495.1,495.3,515.0,516.0')] ).
cnf(701,plain,
( equal(op(op(e4,e4),e4),e4)
| skC5
| skC6
| skC7
| skC8
| skC9
| skC11
| skC12
| skC13
| skC14
| skC15
| skC17
| skC18
| skC19
| skC20
| skC23
| skC24
| skC25
| skC26
| skC27 ),
inference(mrr,[status(thm)],[498,540,537,530,528,532]),
[iquote('0:MRR:498.1,498.7,498.13,498.18,498.19,540.0,537.0,530.0,528.0,532.0')] ).
cnf(702,plain,
( ~ equal(e4,e4)
| skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23
| skC24
| skC25
| skC26
| skC27 ),
inference(rew,[status(thm),theory(equality)],[701,499]),
[iquote('0:Rew:701.0,499.0')] ).
cnf(703,plain,
( skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23
| skC24
| skC25
| skC26
| skC27 ),
inference(obv,[status(thm),theory(equality)],[702]),
[iquote('0:Obv:702.0')] ).
cnf(704,plain,
( skC27
| skC26
| skC25
| skC24
| skC23
| skC20
| skC19
| skC18
| skC17
| skC15
| skC14
| skC13
| skC12
| skC11
| skC9
| skC8
| skC7
| skC6
| skC5 ),
inference(mrr,[status(thm)],[703,540,537,530,528,532]),
[iquote('0:MRR:703.0,703.6,703.12,703.17,703.18,540.0,537.0,530.0,528.0,532.0')] ).
cnf(706,plain,
equal(e4,unit),
inference(spt,[spt(split,[position(s1)])],[422]),
[iquote('1:Spt:422.0')] ).
cnf(722,plain,
~ equal(op(e1,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[706,59]),
[iquote('1:Rew:706.0,59.0')] ).
cnf(723,plain,
~ equal(op(e0,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[706,56]),
[iquote('1:Rew:706.0,56.0')] ).
cnf(748,plain,
~ equal(op(e1,e2),op(unit,e2)),
inference(rew,[status(thm),theory(equality)],[706,49]),
[iquote('1:Rew:706.0,49.0')] ).
cnf(749,plain,
~ equal(op(e0,e2),op(unit,e2)),
inference(rew,[status(thm),theory(equality)],[706,46]),
[iquote('1:Rew:706.0,46.0')] ).
cnf(751,plain,
( equal(op(e3,e1),e3)
| equal(op(unit,e1),e3)
| equal(op(e0,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[706,665]),
[iquote('1:Rew:706.0,665.1')] ).
cnf(787,plain,
~ equal(op(e3,e1),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[706,109]),
[iquote('1:Rew:706.0,109.0')] ).
cnf(819,plain,
~ equal(op(e1,e3),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[706,92]),
[iquote('1:Rew:706.0,92.0')] ).
cnf(827,plain,
( equal(op(e0,e2),e2)
| equal(op(e0,e0),e2)
| equal(op(e0,unit),e2)
| equal(op(e0,e3),e2)
| equal(op(e0,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[706,468]),
[iquote('1:Rew:706.0,468.2')] ).
cnf(840,plain,
~ equal(op(e0,e3),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[706,82]),
[iquote('1:Rew:706.0,82.0')] ).
cnf(851,plain,
( equal(op(e1,e2),e2)
| equal(op(e1,e2),unit) ),
inference(rew,[status(thm),theory(equality)],[706,696]),
[iquote('1:Rew:706.0,696.1')] ).
cnf(852,plain,
( equal(op(e0,e4),e4)
| equal(op(e0,e0),e4)
| equal(op(e0,e2),unit)
| equal(op(e0,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[706,677]),
[iquote('1:Rew:706.0,677.2')] ).
cnf(865,plain,
~ equal(e3,unit),
inference(rew,[status(thm),theory(equality)],[706,10]),
[iquote('1:Rew:706.0,10.0')] ).
cnf(866,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[706,9]),
[iquote('1:Rew:706.0,9.0')] ).
cnf(868,plain,
~ equal(e0,unit),
inference(rew,[status(thm),theory(equality)],[706,4]),
[iquote('1:Rew:706.0,4.0')] ).
cnf(905,plain,
~ equal(op(e1,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,722]),
[iquote('1:Rew:17.0,722.0')] ).
cnf(906,plain,
( equal(op(e1,e3),e1)
| equal(op(e1,e3),e2) ),
inference(mrr,[status(thm)],[695,905]),
[iquote('1:MRR:695.0,905.0')] ).
cnf(907,plain,
~ equal(op(e0,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,723]),
[iquote('1:Rew:17.0,723.0')] ).
cnf(908,plain,
( equal(op(e0,e3),e0)
| equal(op(e0,e3),e2)
| equal(op(e0,e3),e1) ),
inference(mrr,[status(thm)],[698,907]),
[iquote('1:MRR:698.0,907.0')] ).
cnf(913,plain,
~ equal(op(e1,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,748]),
[iquote('1:Rew:15.0,748.0')] ).
cnf(914,plain,
~ equal(op(e0,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,749]),
[iquote('1:Rew:15.0,749.0')] ).
cnf(934,plain,
~ equal(op(e3,e1),e3),
inference(rew,[status(thm),theory(equality)],[18,787]),
[iquote('1:Rew:18.0,787.0')] ).
cnf(935,plain,
equal(op(e3,e1),e2),
inference(mrr,[status(thm)],[688,934]),
[iquote('1:MRR:688.0,934.0')] ).
cnf(962,plain,
~ equal(op(e1,e3),e1),
inference(rew,[status(thm),theory(equality)],[14,819]),
[iquote('1:Rew:14.0,819.0')] ).
cnf(969,plain,
~ equal(op(e0,e3),e0),
inference(rew,[status(thm),theory(equality)],[12,840]),
[iquote('1:Rew:12.0,840.0')] ).
cnf(1005,plain,
equal(op(e1,e2),unit),
inference(mrr,[status(thm)],[851,913]),
[iquote('1:MRR:851.0,913.0')] ).
cnf(1013,plain,
~ equal(op(e0,e2),unit),
inference(rew,[status(thm),theory(equality)],[1005,43]),
[iquote('1:Rew:1005.0,43.0')] ).
cnf(1019,plain,
equal(op(e1,e3),e2),
inference(mrr,[status(thm)],[906,962]),
[iquote('1:MRR:906.0,962.0')] ).
cnf(1023,plain,
~ equal(op(e0,e3),e2),
inference(rew,[status(thm),theory(equality)],[1019,53]),
[iquote('1:Rew:1019.0,53.0')] ).
cnf(1047,plain,
( equal(e3,e2)
| equal(e3,e1)
| equal(op(e0,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[13,751,935]),
[iquote('1:Rew:13.0,751.1,935.0,751.0')] ).
cnf(1048,plain,
equal(op(e0,e1),e3),
inference(mrr,[status(thm)],[1047,8,6]),
[iquote('1:MRR:1047.0,1047.1,8.0,6.0')] ).
cnf(1092,plain,
equal(op(e0,e3),e1),
inference(mrr,[status(thm)],[908,969,1023]),
[iquote('1:MRR:908.0,908.1,969.0,1023.0')] ).
cnf(1131,plain,
( equal(e0,unit)
| equal(op(e0,e0),unit)
| equal(op(e0,e2),unit)
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[1048,852,706,12]),
[iquote('1:Rew:1048.0,852.3,706.0,852.3,706.0,852.1,12.0,852.0,706.0,852.0')] ).
cnf(1132,plain,
equal(op(e0,e0),unit),
inference(mrr,[status(thm)],[1131,868,1013,865]),
[iquote('1:MRR:1131.0,1131.2,1131.3,868.0,1013.0,865.0')] ).
cnf(1146,plain,
( equal(op(e0,e2),e2)
| equal(e2,unit)
| equal(e2,e0)
| equal(e2,e1)
| equal(e3,e2) ),
inference(rew,[status(thm),theory(equality)],[1048,827,1092,12,1132]),
[iquote('1:Rew:1048.0,827.4,1092.0,827.3,12.0,827.2,1132.0,827.1')] ).
cnf(1147,plain,
$false,
inference(mrr,[status(thm)],[1146,914,866,2,5,8]),
[iquote('1:MRR:1146.0,1146.1,1146.2,1146.3,1146.4,914.0,866.0,2.0,5.0,8.0')] ).
cnf(1149,plain,
~ equal(e4,unit),
inference(spt,[spt(split,[position(sa)])],[1147,706]),
[iquote('1:Spt:1147.0,422.0,706.0')] ).
cnf(1150,plain,
( equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit)
| equal(e0,unit) ),
inference(spt,[spt(split,[position(s2)])],[422]),
[iquote('1:Spt:1147.0,422.1,422.2,422.3,422.4')] ).
cnf(1151,plain,
equal(e3,unit),
inference(spt,[spt(split,[position(s2s1)])],[1150]),
[iquote('2:Spt:1150.0')] ).
cnf(1160,plain,
~ equal(op(e2,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1151,30]),
[iquote('2:Rew:1151.0,30.0')] ).
cnf(1185,plain,
~ equal(op(e0,e2),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[1151,80]),
[iquote('2:Rew:1151.0,80.0')] ).
cnf(1188,plain,
( equal(op(e0,e1),e1)
| equal(op(e0,e0),e1)
| equal(op(e0,e4),e1)
| equal(op(e0,unit),e1) ),
inference(rew,[status(thm),theory(equality)],[1151,681]),
[iquote('2:Rew:1151.0,681.3')] ).
cnf(1206,plain,
~ equal(op(e1,e0),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[1151,85]),
[iquote('2:Rew:1151.0,85.0')] ).
cnf(1220,plain,
~ equal(op(e2,e0),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[1151,95]),
[iquote('2:Rew:1151.0,95.0')] ).
cnf(1221,plain,
~ equal(op(e2,e1),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[1151,98]),
[iquote('2:Rew:1151.0,98.0')] ).
cnf(1224,plain,
~ equal(op(e4,e1),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1151,118]),
[iquote('2:Rew:1151.0,118.0')] ).
cnf(1226,plain,
~ equal(op(e4,e4),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1151,122]),
[iquote('2:Rew:1151.0,122.0')] ).
cnf(1245,plain,
( ~ skC1
| equal(op(unit,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[1151,600]),
[iquote('2:Rew:1151.0,600.1')] ).
cnf(1246,plain,
~ equal(op(e4,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[1151,42]),
[iquote('2:Rew:1151.0,42.0')] ).
cnf(1247,plain,
~ equal(op(e0,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[1151,35]),
[iquote('2:Rew:1151.0,35.0')] ).
cnf(1248,plain,
~ equal(op(e2,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[1151,40]),
[iquote('2:Rew:1151.0,40.0')] ).
cnf(1269,plain,
( ~ skC3
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[1151,545]),
[iquote('2:Rew:1151.0,545.1')] ).
cnf(1280,plain,
( equal(op(e4,e4),e4)
| equal(op(e4,e4),unit)
| equal(op(e4,e4),e2)
| equal(op(e4,e4),e1)
| equal(op(e4,e4),e0) ),
inference(rew,[status(thm),theory(equality)],[1151,473]),
[iquote('2:Rew:1151.0,473.1')] ).
cnf(1292,plain,
( skC3
| skC2
| skC1
| skC0
| equal(op(unit,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[1151,619]),
[iquote('2:Rew:1151.0,619.4')] ).
cnf(1304,plain,
( equal(op(e4,e1),e4)
| equal(op(e4,e1),e1)
| equal(op(e4,e1),unit)
| equal(op(e4,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[1151,686]),
[iquote('2:Rew:1151.0,686.2')] ).
cnf(1327,plain,
~ skC3,
inference(obv,[status(thm),theory(equality)],[1269]),
[iquote('2:Obv:1269.1')] ).
cnf(1339,plain,
( ~ skC1
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[13,1245]),
[iquote('2:Rew:13.0,1245.1')] ).
cnf(1340,plain,
~ skC1,
inference(mrr,[status(thm)],[1339,5]),
[iquote('2:MRR:1339.1,5.0')] ).
cnf(1344,plain,
~ equal(op(e2,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1160]),
[iquote('2:Rew:11.0,1160.0')] ).
cnf(1345,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e4)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[693,1344]),
[iquote('2:MRR:693.1,1344.0')] ).
cnf(1351,plain,
~ equal(op(e0,e2),e0),
inference(rew,[status(thm),theory(equality)],[12,1185]),
[iquote('2:Rew:12.0,1185.0')] ).
cnf(1352,plain,
equal(op(e4,e2),e0),
inference(mrr,[status(thm)],[657,1351]),
[iquote('2:MRR:657.0,1351.0')] ).
cnf(1360,plain,
~ equal(op(e4,e4),e0),
inference(rew,[status(thm),theory(equality)],[1352,121]),
[iquote('2:Rew:1352.0,121.0')] ).
cnf(1369,plain,
( ~ skC2
| ~ equal(op(e4,e4),e2)
| equal(e4,e0) ),
inference(rew,[status(thm),theory(equality)],[1352,355]),
[iquote('2:Rew:1352.0,355.2')] ).
cnf(1376,plain,
~ equal(op(e1,e0),e1),
inference(rew,[status(thm),theory(equality)],[14,1206]),
[iquote('2:Rew:14.0,1206.0')] ).
cnf(1377,plain,
~ skC0,
inference(mrr,[status(thm)],[615,1376]),
[iquote('2:MRR:615.1,1376.0')] ).
cnf(1384,plain,
~ equal(op(e2,e0),e2),
inference(rew,[status(thm),theory(equality)],[16,1220]),
[iquote('2:Rew:16.0,1220.0')] ).
cnf(1385,plain,
~ equal(op(e2,e1),e2),
inference(rew,[status(thm),theory(equality)],[16,1221]),
[iquote('2:Rew:16.0,1221.0')] ).
cnf(1386,plain,
( equal(op(e2,e1),e1)
| equal(op(e2,e1),e4) ),
inference(mrr,[status(thm)],[692,1385]),
[iquote('2:MRR:692.0,1385.0')] ).
cnf(1389,plain,
~ equal(op(e4,e1),e4),
inference(rew,[status(thm),theory(equality)],[20,1224]),
[iquote('2:Rew:20.0,1224.0')] ).
cnf(1392,plain,
~ equal(op(e4,e4),e4),
inference(rew,[status(thm),theory(equality)],[20,1226]),
[iquote('2:Rew:20.0,1226.0')] ).
cnf(1398,plain,
~ equal(op(e4,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1246]),
[iquote('2:Rew:13.0,1246.0')] ).
cnf(1400,plain,
~ equal(op(e0,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1247]),
[iquote('2:Rew:13.0,1247.0')] ).
cnf(1401,plain,
~ equal(op(e2,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1248]),
[iquote('2:Rew:13.0,1248.0')] ).
cnf(1416,plain,
( skC3
| skC2
| skC1
| skC0
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[19,1292]),
[iquote('2:Rew:19.0,1292.4')] ).
cnf(1417,plain,
skC2,
inference(mrr,[status(thm)],[1416,1327,1340,1377,1149]),
[iquote('2:MRR:1416.0,1416.2,1416.3,1416.4,1327.0,1340.0,1377.0,1149.0')] ).
cnf(1418,plain,
~ equal(op(e4,e1),e2),
inference(mrr,[status(thm)],[580,1417]),
[iquote('2:MRR:580.0,1417.0')] ).
cnf(1444,plain,
equal(op(e2,e1),e4),
inference(mrr,[status(thm)],[1386,1401]),
[iquote('2:MRR:1386.0,1401.0')] ).
cnf(1451,plain,
~ equal(op(e2,e0),e4),
inference(rew,[status(thm),theory(equality)],[1444,93]),
[iquote('2:Rew:1444.0,93.0')] ).
cnf(1461,plain,
~ equal(op(e4,e4),e2),
inference(mrr,[status(thm)],[1369,1417,4]),
[iquote('2:MRR:1369.0,1369.2,1417.0,4.0')] ).
cnf(1493,plain,
equal(op(e2,e0),e1),
inference(mrr,[status(thm)],[1345,1384,1451]),
[iquote('2:MRR:1345.0,1345.1,1384.0,1451.0')] ).
cnf(1496,plain,
~ equal(op(e0,e0),e1),
inference(rew,[status(thm),theory(equality)],[1493,24]),
[iquote('2:Rew:1493.0,24.0')] ).
cnf(1517,plain,
( equal(op(e0,e1),e1)
| equal(op(e0,e0),e1)
| equal(op(e0,e4),e1)
| equal(e1,e0) ),
inference(rew,[status(thm),theory(equality)],[12,1188]),
[iquote('2:Rew:12.0,1188.3')] ).
cnf(1518,plain,
equal(op(e0,e4),e1),
inference(mrr,[status(thm)],[1517,1400,1496,1]),
[iquote('2:MRR:1517.0,1517.1,1517.3,1400.0,1496.0,1.0')] ).
cnf(1520,plain,
~ equal(op(e4,e4),e1),
inference(rew,[status(thm),theory(equality)],[1518,66]),
[iquote('2:Rew:1518.0,66.0')] ).
cnf(1552,plain,
equal(op(e4,e1),unit),
inference(mrr,[status(thm)],[1304,1389,1398,1418]),
[iquote('2:MRR:1304.0,1304.1,1304.3,1389.0,1398.0,1418.0')] ).
cnf(1556,plain,
~ equal(op(e4,e4),unit),
inference(rew,[status(thm),theory(equality)],[1552,119]),
[iquote('2:Rew:1552.0,119.0')] ).
cnf(1647,plain,
$false,
inference(mrr,[status(thm)],[1280,1392,1556,1461,1520,1360]),
[iquote('2:MRR:1280.0,1280.1,1280.2,1280.3,1280.4,1392.0,1556.0,1461.0,1520.0,1360.0')] ).
cnf(1648,plain,
~ equal(e3,unit),
inference(spt,[spt(split,[position(s2sa)])],[1647,1151]),
[iquote('2:Spt:1647.0,1150.0,1151.0')] ).
cnf(1649,plain,
( equal(e2,unit)
| equal(e1,unit)
| equal(e0,unit) ),
inference(spt,[spt(split,[position(s2s2)])],[1150]),
[iquote('2:Spt:1647.0,1150.1,1150.2,1150.3')] ).
cnf(1650,plain,
equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s1)])],[1649]),
[iquote('3:Spt:1649.0')] ).
cnf(1651,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[1650,5]),
[iquote('3:Rew:1650.0,5.0')] ).
cnf(1652,plain,
~ equal(e0,unit),
inference(rew,[status(thm),theory(equality)],[1650,2]),
[iquote('3:Rew:1650.0,2.0')] ).
cnf(1660,plain,
~ equal(op(e3,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1650,30]),
[iquote('3:Rew:1650.0,30.0')] ).
cnf(1667,plain,
~ equal(op(e4,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1650,31]),
[iquote('3:Rew:1650.0,31.0')] ).
cnf(1679,plain,
~ equal(op(e1,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[1650,57]),
[iquote('3:Rew:1650.0,57.0')] ).
cnf(1689,plain,
~ equal(op(e1,e3),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[1650,90]),
[iquote('3:Rew:1650.0,90.0')] ).
cnf(1692,plain,
( equal(op(e1,e4),e4)
| equal(op(e1,unit),e4)
| equal(op(e1,e0),e4) ),
inference(rew,[status(thm),theory(equality)],[1650,663]),
[iquote('3:Rew:1650.0,663.1')] ).
cnf(1702,plain,
~ equal(op(e4,e1),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1650,117]),
[iquote('3:Rew:1650.0,117.0')] ).
cnf(1703,plain,
~ equal(op(e4,e0),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1650,114]),
[iquote('3:Rew:1650.0,114.0')] ).
cnf(1717,plain,
~ equal(op(e1,e4),op(unit,e4)),
inference(rew,[status(thm),theory(equality)],[1650,67]),
[iquote('3:Rew:1650.0,67.0')] ).
cnf(1749,plain,
~ equal(op(e0,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[1650,34]),
[iquote('3:Rew:1650.0,34.0')] ).
cnf(1754,plain,
( equal(op(e4,e1),e4)
| equal(op(unit,e1),e4)
| equal(op(e0,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[1650,661]),
[iquote('3:Rew:1650.0,661.1')] ).
cnf(1761,plain,
( ~ skC1
| equal(op(e3,e1),unit) ),
inference(rew,[status(thm),theory(equality)],[1650,600]),
[iquote('3:Rew:1650.0,600.1')] ).
cnf(1765,plain,
( ~ skC3
| equal(op(unit,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[1650,574]),
[iquote('3:Rew:1650.0,574.1')] ).
cnf(1766,plain,
( equal(op(e4,e4),e2)
| equal(op(e2,e4),e2)
| equal(op(e3,e4),unit)
| equal(op(e1,e4),e2)
| equal(op(e0,e4),e2) ),
inference(rew,[status(thm),theory(equality)],[1650,427]),
[iquote('3:Rew:1650.0,427.2')] ).
cnf(1773,plain,
( equal(op(e1,e3),e3)
| equal(op(e1,e3),e1)
| equal(op(e1,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[1650,695]),
[iquote('3:Rew:1650.0,695.2')] ).
cnf(1774,plain,
( ~ skC2
| ~ equal(op(e1,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[1650,592]),
[iquote('3:Rew:1650.0,592.1')] ).
cnf(1815,plain,
( equal(op(e4,e0),e4)
| equal(op(e4,e0),e0)
| equal(op(e4,e0),e3)
| equal(op(e4,e0),unit)
| equal(op(e4,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1650,477]),
[iquote('3:Rew:1650.0,477.3')] ).
cnf(1837,plain,
( ~ skC3
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[17,1765]),
[iquote('3:Rew:17.0,1765.1')] ).
cnf(1838,plain,
~ skC3,
inference(mrr,[status(thm)],[1837,1648]),
[iquote('3:MRR:1837.1,1648.0')] ).
cnf(1839,plain,
( skC2
| skC1
| skC0
| equal(op(e3,e4),e3) ),
inference(mrr,[status(thm)],[619,1838]),
[iquote('3:MRR:619.0,1838.0')] ).
cnf(1845,plain,
~ equal(op(e3,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1660]),
[iquote('3:Rew:11.0,1660.0')] ).
cnf(1846,plain,
equal(op(e3,e4),e0),
inference(mrr,[status(thm)],[645,1845]),
[iquote('3:MRR:645.0,1845.0')] ).
cnf(1849,plain,
( ~ skC0
| ~ equal(e0,e0) ),
inference(rew,[status(thm),theory(equality)],[1846,609]),
[iquote('3:Rew:1846.0,609.1')] ).
cnf(1861,plain,
~ skC0,
inference(obv,[status(thm),theory(equality)],[1849]),
[iquote('3:Obv:1849.1')] ).
cnf(1865,plain,
~ equal(op(e4,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1667]),
[iquote('3:Rew:11.0,1667.0')] ).
cnf(1872,plain,
~ equal(op(e1,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,1679]),
[iquote('3:Rew:17.0,1679.0')] ).
cnf(1873,plain,
( equal(op(e1,e4),e3)
| equal(op(e1,e0),e3) ),
inference(mrr,[status(thm)],[667,1872]),
[iquote('3:MRR:667.0,1872.0')] ).
cnf(1876,plain,
~ equal(op(e1,e3),e1),
inference(rew,[status(thm),theory(equality)],[14,1689]),
[iquote('3:Rew:14.0,1689.0')] ).
cnf(1883,plain,
~ equal(op(e4,e1),e4),
inference(rew,[status(thm),theory(equality)],[20,1702]),
[iquote('3:Rew:20.0,1702.0')] ).
cnf(1885,plain,
~ equal(op(e4,e0),e4),
inference(rew,[status(thm),theory(equality)],[20,1703]),
[iquote('3:Rew:20.0,1703.0')] ).
cnf(1890,plain,
~ equal(op(e1,e4),e4),
inference(rew,[status(thm),theory(equality)],[19,1717]),
[iquote('3:Rew:19.0,1717.0')] ).
cnf(1901,plain,
~ equal(op(e0,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1749]),
[iquote('3:Rew:13.0,1749.0')] ).
cnf(1902,plain,
( equal(op(e0,e0),e1)
| equal(op(e0,e4),e1)
| equal(op(e0,e3),e1) ),
inference(mrr,[status(thm)],[681,1901]),
[iquote('3:MRR:681.0,1901.0')] ).
cnf(1910,plain,
( skC2
| skC1
| skC0
| equal(e3,e0) ),
inference(rew,[status(thm),theory(equality)],[1846,1839]),
[iquote('3:Rew:1846.0,1839.3')] ).
cnf(1911,plain,
( skC2
| skC1 ),
inference(mrr,[status(thm)],[1910,1861,3]),
[iquote('3:MRR:1910.2,1910.3,1861.0,3.0')] ).
cnf(1982,plain,
( equal(op(e1,e4),e4)
| equal(e4,e1)
| equal(op(e1,e0),e4) ),
inference(rew,[status(thm),theory(equality)],[14,1692]),
[iquote('3:Rew:14.0,1692.1')] ).
cnf(1983,plain,
equal(op(e1,e0),e4),
inference(mrr,[status(thm)],[1982,1890,7]),
[iquote('3:MRR:1982.0,1982.1,1890.0,7.0')] ).
cnf(1985,plain,
( equal(op(e1,e4),e3)
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[1983,1873]),
[iquote('3:Rew:1983.0,1873.1')] ).
cnf(1998,plain,
equal(op(e1,e4),e3),
inference(mrr,[status(thm)],[1985,10]),
[iquote('3:MRR:1985.1,10.0')] ).
cnf(2014,plain,
( equal(op(e4,e1),e4)
| equal(e4,e1)
| equal(op(e0,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[13,1754]),
[iquote('3:Rew:13.0,1754.1')] ).
cnf(2015,plain,
equal(op(e0,e1),e4),
inference(mrr,[status(thm)],[2014,1883,7]),
[iquote('3:MRR:2014.0,2014.1,1883.0,7.0')] ).
cnf(2024,plain,
( equal(op(e3,e1),e3)
| equal(op(e4,e1),e3)
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[2015,665]),
[iquote('3:Rew:2015.0,665.2')] ).
cnf(2025,plain,
( ~ skC1
| ~ equal(op(e0,e3),e1)
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[2015,318]),
[iquote('3:Rew:2015.0,318.2')] ).
cnf(2032,plain,
( ~ skC1
| ~ equal(op(e0,e3),e1) ),
inference(mrr,[status(thm)],[2025,10]),
[iquote('3:MRR:2025.2,10.0')] ).
cnf(2033,plain,
( equal(op(e3,e1),e3)
| equal(op(e4,e1),e3) ),
inference(mrr,[status(thm)],[2024,10]),
[iquote('3:MRR:2024.2,10.0')] ).
cnf(2037,plain,
equal(op(e1,e3),unit),
inference(mrr,[status(thm)],[1773,1872,1876]),
[iquote('3:MRR:1773.0,1773.1,1872.0,1876.0')] ).
cnf(2047,plain,
( ~ skC2
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[2037,1774]),
[iquote('3:Rew:2037.0,1774.1')] ).
cnf(2048,plain,
~ skC2,
inference(obv,[status(thm),theory(equality)],[2047]),
[iquote('3:Obv:2047.1')] ).
cnf(2049,plain,
skC1,
inference(mrr,[status(thm)],[1911,2048]),
[iquote('3:MRR:1911.0,2048.0')] ).
cnf(2050,plain,
~ equal(op(e4,e0),e1),
inference(mrr,[status(thm)],[597,2049]),
[iquote('3:MRR:597.0,2049.0')] ).
cnf(2051,plain,
~ equal(op(e0,e0),e1),
inference(mrr,[status(thm)],[608,2049]),
[iquote('3:MRR:608.0,2049.0')] ).
cnf(2052,plain,
equal(op(e3,e1),unit),
inference(mrr,[status(thm)],[1761,2049]),
[iquote('3:MRR:1761.0,2049.0')] ).
cnf(2054,plain,
~ equal(op(e0,e3),e1),
inference(mrr,[status(thm)],[2032,2049]),
[iquote('3:MRR:2032.0,2049.0')] ).
cnf(2058,plain,
( equal(e3,unit)
| equal(op(e4,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[2052,2033]),
[iquote('3:Rew:2052.0,2033.0')] ).
cnf(2068,plain,
equal(op(e4,e1),e3),
inference(mrr,[status(thm)],[2058,1648]),
[iquote('3:MRR:2058.0,1648.0')] ).
cnf(2071,plain,
~ equal(op(e4,e0),e3),
inference(rew,[status(thm),theory(equality)],[2068,113]),
[iquote('3:Rew:2068.0,113.0')] ).
cnf(2095,plain,
equal(op(e0,e4),e1),
inference(mrr,[status(thm)],[1902,2051,2054]),
[iquote('3:MRR:1902.0,1902.2,2051.0,2054.0')] ).
cnf(2122,plain,
( equal(op(e4,e4),unit)
| equal(e4,unit)
| equal(e0,unit)
| equal(e3,unit)
| equal(e1,unit) ),
inference(rew,[status(thm),theory(equality)],[2095,1766,1650,1998,1846,19]),
[iquote('3:Rew:2095.0,1766.4,1650.0,1766.4,1998.0,1766.3,1650.0,1766.3,1846.0,1766.2,19.0,1766.1,1650.0,1766.1,1650.0,1766.0')] ).
cnf(2123,plain,
equal(op(e4,e4),unit),
inference(mrr,[status(thm)],[2122,1149,1652,1648,1651]),
[iquote('3:MRR:2122.1,2122.2,2122.3,2122.4,1149.0,1652.0,1648.0,1651.0')] ).
cnf(2124,plain,
~ equal(op(e4,e0),unit),
inference(rew,[status(thm),theory(equality)],[2123,116]),
[iquote('3:Rew:2123.0,116.0')] ).
cnf(2139,plain,
$false,
inference(mrr,[status(thm)],[1815,1885,1865,2071,2124,2050]),
[iquote('3:MRR:1815.0,1815.1,1815.2,1815.3,1815.4,1885.0,1865.0,2071.0,2124.0,2050.0')] ).
cnf(2140,plain,
~ equal(e2,unit),
inference(spt,[spt(split,[position(s2s2sa)])],[2139,1650]),
[iquote('3:Spt:2139.0,1649.0,1650.0')] ).
cnf(2141,plain,
( equal(e1,unit)
| equal(e0,unit) ),
inference(spt,[spt(split,[position(s2s2s2)])],[1649]),
[iquote('3:Spt:2139.0,1649.1,1649.2')] ).
cnf(2142,plain,
equal(e1,unit),
inference(spt,[spt(split,[position(s2s2s2s1)])],[2141]),
[iquote('4:Spt:2141.0')] ).
cnf(2143,plain,
~ equal(e0,unit),
inference(rew,[status(thm),theory(equality)],[2142,1]),
[iquote('4:Rew:2142.0,1.0')] ).
cnf(2156,plain,
( ~ skC2
| ~ equal(op(e2,unit),e2) ),
inference(rew,[status(thm),theory(equality)],[2142,589]),
[iquote('4:Rew:2142.0,589.1')] ).
cnf(2159,plain,
~ equal(op(e2,e3),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[2142,98]),
[iquote('4:Rew:2142.0,98.0')] ).
cnf(2168,plain,
~ equal(op(e0,e2),op(unit,e2)),
inference(rew,[status(thm),theory(equality)],[2142,43]),
[iquote('4:Rew:2142.0,43.0')] ).
cnf(2180,plain,
( ~ skC1
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[2142,551]),
[iquote('4:Rew:2142.0,551.1')] ).
cnf(2191,plain,
~ equal(op(e4,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[2142,29]),
[iquote('4:Rew:2142.0,29.0')] ).
cnf(2193,plain,
~ equal(op(e3,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[2142,28]),
[iquote('4:Rew:2142.0,28.0')] ).
cnf(2213,plain,
~ equal(op(e0,e2),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[2142,77]),
[iquote('4:Rew:2142.0,77.0')] ).
cnf(2219,plain,
( equal(op(e0,e3),e3)
| equal(op(e0,e0),e3)
| equal(op(e0,e4),e3)
| equal(op(e0,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[2142,679]),
[iquote('4:Rew:2142.0,679.3')] ).
cnf(2236,plain,
~ equal(op(e0,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[2142,53]),
[iquote('4:Rew:2142.0,53.0')] ).
cnf(2248,plain,
~ equal(op(e3,e0),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[2142,103]),
[iquote('4:Rew:2142.0,103.0')] ).
cnf(2261,plain,
~ equal(op(e4,e0),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[2142,113]),
[iquote('4:Rew:2142.0,113.0')] ).
cnf(2269,plain,
( ~ equal(op(e4,unit),e4)
| skC3
| skC2
| skC1
| skC0
| equal(op(e4,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[2142,419]),
[iquote('4:Rew:2142.0,419.0')] ).
cnf(2274,plain,
( ~ skC0
| equal(op(unit,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[2142,615]),
[iquote('4:Rew:2142.0,615.1')] ).
cnf(2288,plain,
( equal(op(e4,e0),e4)
| equal(op(e4,e0),e0)
| equal(op(e4,e0),e3)
| equal(op(e4,e0),e2)
| equal(op(e4,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[2142,477]),
[iquote('4:Rew:2142.0,477.4')] ).
cnf(2320,plain,
~ skC1,
inference(obv,[status(thm),theory(equality)],[2180]),
[iquote('4:Obv:2180.1')] ).
cnf(2322,plain,
( ~ equal(op(e0,e2),e4)
| skC3
| skC2
| skC0
| equal(op(e0,e4),e2) ),
inference(mrr,[status(thm)],[404,2320]),
[iquote('4:MRR:404.3,2320.0')] ).
cnf(2338,plain,
( ~ skC0
| equal(e0,unit) ),
inference(rew,[status(thm),theory(equality)],[11,2274]),
[iquote('4:Rew:11.0,2274.1')] ).
cnf(2339,plain,
~ skC0,
inference(mrr,[status(thm)],[2338,2143]),
[iquote('4:MRR:2338.1,2143.0')] ).
cnf(2340,plain,
( ~ skC2
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[16,2156]),
[iquote('4:Rew:16.0,2156.1')] ).
cnf(2341,plain,
~ skC2,
inference(obv,[status(thm),theory(equality)],[2340]),
[iquote('4:Obv:2340.1')] ).
cnf(2344,plain,
~ equal(op(e2,e3),e2),
inference(rew,[status(thm),theory(equality)],[16,2159]),
[iquote('4:Rew:16.0,2159.0')] ).
cnf(2345,plain,
~ skC3,
inference(mrr,[status(thm)],[574,2344]),
[iquote('4:MRR:574.1,2344.0')] ).
cnf(2346,plain,
~ equal(op(e0,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,2168]),
[iquote('4:Rew:15.0,2168.0')] ).
cnf(2347,plain,
( equal(op(e0,e2),e0)
| equal(op(e0,e2),e4) ),
inference(mrr,[status(thm)],[699,2346]),
[iquote('4:MRR:699.0,2346.0')] ).
cnf(2354,plain,
~ equal(op(e4,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,2191]),
[iquote('4:Rew:11.0,2191.0')] ).
cnf(2358,plain,
~ equal(op(e3,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,2193]),
[iquote('4:Rew:11.0,2193.0')] ).
cnf(2360,plain,
( equal(op(e3,e0),e3)
| equal(op(e3,e0),e2) ),
inference(mrr,[status(thm)],[689,2358]),
[iquote('4:MRR:689.1,2358.0')] ).
cnf(2378,plain,
~ equal(op(e0,e2),e0),
inference(rew,[status(thm),theory(equality)],[12,2213]),
[iquote('4:Rew:12.0,2213.0')] ).
cnf(2400,plain,
~ equal(op(e0,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,2236]),
[iquote('4:Rew:17.0,2236.0')] ).
cnf(2404,plain,
~ equal(op(e3,e0),e3),
inference(rew,[status(thm),theory(equality)],[18,2248]),
[iquote('4:Rew:18.0,2248.0')] ).
cnf(2410,plain,
~ equal(op(e4,e0),e4),
inference(rew,[status(thm),theory(equality)],[20,2261]),
[iquote('4:Rew:20.0,2261.0')] ).
cnf(2439,plain,
equal(op(e0,e2),e4),
inference(mrr,[status(thm)],[2347,2378]),
[iquote('4:MRR:2347.0,2378.0')] ).
cnf(2463,plain,
equal(op(e3,e0),e2),
inference(mrr,[status(thm)],[2360,2404]),
[iquote('4:MRR:2360.0,2404.0')] ).
cnf(2466,plain,
~ equal(op(e4,e0),e2),
inference(rew,[status(thm),theory(equality)],[2463,32]),
[iquote('4:Rew:2463.0,32.0')] ).
cnf(2476,plain,
( ~ equal(e4,e4)
| skC3
| skC2
| skC0
| equal(op(e0,e4),e2) ),
inference(rew,[status(thm),theory(equality)],[2439,2322]),
[iquote('4:Rew:2439.0,2322.0')] ).
cnf(2477,plain,
( skC3
| skC2
| skC0
| equal(op(e0,e4),e2) ),
inference(obv,[status(thm),theory(equality)],[2476]),
[iquote('4:Obv:2476.0')] ).
cnf(2478,plain,
equal(op(e0,e4),e2),
inference(mrr,[status(thm)],[2477,2345,2341,2339]),
[iquote('4:MRR:2477.0,2477.1,2477.2,2345.0,2341.0,2339.0')] ).
cnf(2507,plain,
( ~ equal(e4,e4)
| skC3
| skC2
| skC1
| skC0
| equal(op(e4,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[2142,2269,20]),
[iquote('4:Rew:2142.0,2269.5,20.0,2269.0')] ).
cnf(2508,plain,
( skC3
| skC2
| skC1
| skC0
| equal(op(e4,e4),unit) ),
inference(obv,[status(thm),theory(equality)],[2507]),
[iquote('4:Obv:2507.0')] ).
cnf(2509,plain,
equal(op(e4,e4),unit),
inference(mrr,[status(thm)],[2508,2345,2341,2320,2339]),
[iquote('4:MRR:2508.0,2508.1,2508.2,2508.3,2345.0,2341.0,2320.0,2339.0')] ).
cnf(2512,plain,
~ equal(op(e4,e0),unit),
inference(rew,[status(thm),theory(equality)],[2509,116]),
[iquote('4:Rew:2509.0,116.0')] ).
cnf(2536,plain,
( equal(op(e0,e3),e3)
| equal(op(e0,e0),e3)
| equal(e3,e2)
| equal(e3,e0) ),
inference(rew,[status(thm),theory(equality)],[12,2219,2478]),
[iquote('4:Rew:12.0,2219.3,2478.0,2219.2')] ).
cnf(2537,plain,
equal(op(e0,e0),e3),
inference(mrr,[status(thm)],[2536,2400,8,3]),
[iquote('4:MRR:2536.0,2536.2,2536.3,2400.0,8.0,3.0')] ).
cnf(2539,plain,
~ equal(op(e4,e0),e3),
inference(rew,[status(thm),theory(equality)],[2537,26]),
[iquote('4:Rew:2537.0,26.0')] ).
cnf(2589,plain,
$false,
inference(mrr,[status(thm)],[2288,2410,2354,2539,2466,2512]),
[iquote('4:MRR:2288.0,2288.1,2288.2,2288.3,2288.4,2410.0,2354.0,2539.0,2466.0,2512.0')] ).
cnf(2590,plain,
~ equal(e1,unit),
inference(spt,[spt(split,[position(s2s2s2sa)])],[2589,2142]),
[iquote('4:Spt:2589.0,2141.0,2142.0')] ).
cnf(2591,plain,
equal(e0,unit),
inference(spt,[spt(split,[position(s2s2s2s2)])],[2141]),
[iquote('4:Spt:2589.0,2141.1')] ).
cnf(2599,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[2591,1]),
[iquote('4:Rew:2591.0,1.0')] ).
cnf(2600,plain,
equal(op(e1,e1),unit),
inference(rew,[status(thm),theory(equality)],[2591,555]),
[iquote('4:Rew:2591.0,555.0')] ).
cnf(2611,plain,
( ~ skC0
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[2591,566]),
[iquote('4:Rew:2591.0,566.1')] ).
cnf(2612,plain,
~ skC0,
inference(obv,[status(thm),theory(equality)],[2611]),
[iquote('4:Obv:2611.1')] ).
cnf(2624,plain,
~ equal(op(e1,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,53,2591]),
[iquote('4:Rew:17.0,53.0,2591.0,53.0')] ).
cnf(2625,plain,
~ equal(op(e1,e3),e1),
inference(rew,[status(thm),theory(equality)],[14,85,2591]),
[iquote('4:Rew:14.0,85.0,2591.0,85.0')] ).
cnf(2641,plain,
~ equal(op(e1,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,43,2591]),
[iquote('4:Rew:15.0,43.0,2591.0,43.0')] ).
cnf(2643,plain,
( ~ skC2
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[16,591,2591]),
[iquote('4:Rew:16.0,591.1,2591.0,591.1')] ).
cnf(2644,plain,
~ skC2,
inference(obv,[status(thm),theory(equality)],[2643]),
[iquote('4:Obv:2643.1')] ).
cnf(2645,plain,
( ~ skC3
| ~ equal(e3,e3) ),
inference(rew,[status(thm),theory(equality)],[18,572,2591]),
[iquote('4:Rew:18.0,572.1,2591.0,572.1')] ).
cnf(2646,plain,
~ skC3,
inference(obv,[status(thm),theory(equality)],[2645]),
[iquote('4:Obv:2645.1')] ).
cnf(2647,plain,
~ equal(op(e3,e4),e3),
inference(rew,[status(thm),theory(equality)],[18,106,2591]),
[iquote('4:Rew:18.0,106.0,2591.0,106.0')] ).
cnf(2654,plain,
~ equal(op(e2,e3),e2),
inference(rew,[status(thm),theory(equality)],[16,95,2591]),
[iquote('4:Rew:16.0,95.0,2591.0,95.0')] ).
cnf(2673,plain,
skC1,
inference(mrr,[status(thm)],[619,2646,2644,2612,2647]),
[iquote('4:MRR:619.0,619.1,619.3,619.4,2646.0,2644.0,2612.0,2647.0')] ).
cnf(2674,plain,
equal(op(e3,e1),e2),
inference(mrr,[status(thm)],[600,2673]),
[iquote('4:MRR:600.0,2673.0')] ).
cnf(2675,plain,
~ equal(op(e2,e3),e1),
inference(mrr,[status(thm)],[601,2673]),
[iquote('4:MRR:601.0,2673.0')] ).
cnf(2683,plain,
( ~ skC20
| equal(op(e2,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[2674,139]),
[iquote('4:Rew:2674.0,139.1')] ).
cnf(2684,plain,
~ skC20,
inference(mrr,[status(thm)],[2683,508]),
[iquote('4:MRR:2683.1,508.0')] ).
cnf(2685,plain,
( ~ skC6
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[21,125,15,2591]),
[iquote('4:Rew:21.0,125.1,15.0,125.1,2591.0,125.1')] ).
cnf(2686,plain,
~ skC6,
inference(mrr,[status(thm)],[2685,1648]),
[iquote('4:MRR:2685.1,1648.0')] ).
cnf(2688,plain,
( ~ skC8
| equal(op(e4,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[19,127,2591]),
[iquote('4:Rew:19.0,127.1,2591.0,127.1')] ).
cnf(2690,plain,
( ~ skC7
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[517,126,17,2591]),
[iquote('4:Rew:517.0,126.1,17.0,126.1,2591.0,126.1')] ).
cnf(2691,plain,
~ skC7,
inference(mrr,[status(thm)],[2690,1149]),
[iquote('4:MRR:2690.1,1149.0')] ).
cnf(2693,plain,
( ~ skC5
| ~ equal(e1,e1) ),
inference(rew,[status(thm),theory(equality)],[14,151,13,2591]),
[iquote('4:Rew:14.0,151.1,13.0,151.1,2591.0,151.1')] ).
cnf(2694,plain,
~ skC5,
inference(obv,[status(thm),theory(equality)],[2693]),
[iquote('4:Obv:2693.1')] ).
cnf(2695,plain,
( ~ skC9
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[2600,159,14,2591]),
[iquote('4:Rew:2600.0,159.1,14.0,159.1,2591.0,159.1')] ).
cnf(2696,plain,
~ skC9,
inference(obv,[status(thm),theory(equality)],[2695]),
[iquote('4:Obv:2695.1')] ).
cnf(2697,plain,
( ~ skC12
| ~ equal(op(e1,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[2674,164]),
[iquote('4:Rew:2674.0,164.1')] ).
cnf(2698,plain,
equal(op(e1,e2),e4),
inference(mrr,[status(thm)],[696,2641]),
[iquote('4:MRR:696.0,2641.0')] ).
cnf(2706,plain,
( ~ skC11
| equal(op(e4,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[2698,130]),
[iquote('4:Rew:2698.0,130.1')] ).
cnf(2708,plain,
~ skC11,
inference(mrr,[status(thm)],[2706,510]),
[iquote('4:MRR:2706.1,510.0')] ).
cnf(2709,plain,
( ~ skC15
| ~ equal(op(e2,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[2698,170]),
[iquote('4:Rew:2698.0,170.1')] ).
cnf(2710,plain,
( equal(e3,unit)
| equal(op(e3,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[2591,645,18]),
[iquote('4:Rew:2591.0,645.1,18.0,645.0,2591.0,645.0')] ).
cnf(2711,plain,
equal(op(e3,e4),unit),
inference(mrr,[status(thm)],[2710,1648]),
[iquote('4:MRR:2710.0,1648.0')] ).
cnf(2716,plain,
~ equal(op(e4,e4),unit),
inference(rew,[status(thm),theory(equality)],[2711,72]),
[iquote('4:Rew:2711.0,72.0')] ).
cnf(2719,plain,
( ~ skC23
| equal(op(unit,e4),e3) ),
inference(rew,[status(thm),theory(equality)],[2711,142]),
[iquote('4:Rew:2711.0,142.1')] ).
cnf(2720,plain,
~ skC8,
inference(mrr,[status(thm)],[2688,2716]),
[iquote('4:MRR:2688.1,2716.0')] ).
cnf(2721,plain,
( ~ skC23
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[19,2719]),
[iquote('4:Rew:19.0,2719.1')] ).
cnf(2722,plain,
~ skC23,
inference(mrr,[status(thm)],[2721,10]),
[iquote('4:MRR:2721.1,10.0')] ).
cnf(2724,plain,
( equal(e2,unit)
| equal(op(e4,e2),unit) ),
inference(rew,[status(thm),theory(equality)],[2591,657,15]),
[iquote('4:Rew:2591.0,657.1,15.0,657.0,2591.0,657.0')] ).
cnf(2725,plain,
equal(op(e4,e2),unit),
inference(mrr,[status(thm)],[2724,2140]),
[iquote('4:MRR:2724.0,2140.0')] ).
cnf(2733,plain,
( ~ skC26
| equal(op(unit,e2),e4) ),
inference(rew,[status(thm),theory(equality)],[2725,145]),
[iquote('4:Rew:2725.0,145.1')] ).
cnf(2734,plain,
( ~ skC26
| equal(e4,e2) ),
inference(rew,[status(thm),theory(equality)],[15,2733]),
[iquote('4:Rew:15.0,2733.1')] ).
cnf(2735,plain,
~ skC26,
inference(mrr,[status(thm)],[2734,9]),
[iquote('4:MRR:2734.1,9.0')] ).
cnf(2737,plain,
( ~ skC14
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[16,168,15,2591]),
[iquote('4:Rew:16.0,168.1,15.0,168.1,2591.0,168.1')] ).
cnf(2738,plain,
~ skC14,
inference(obv,[status(thm),theory(equality)],[2737]),
[iquote('4:Obv:2737.1')] ).
cnf(2739,plain,
( ~ skC19
| ~ equal(e3,e3) ),
inference(rew,[status(thm),theory(equality)],[18,178,17,2591]),
[iquote('4:Rew:18.0,178.1,17.0,178.1,2591.0,178.1')] ).
cnf(2740,plain,
~ skC19,
inference(obv,[status(thm),theory(equality)],[2739]),
[iquote('4:Obv:2739.1')] ).
cnf(2741,plain,
( ~ skC24
| ~ equal(e4,e4) ),
inference(rew,[status(thm),theory(equality)],[20,188,19,2591]),
[iquote('4:Rew:20.0,188.1,19.0,188.1,2591.0,188.1')] ).
cnf(2742,plain,
~ skC24,
inference(obv,[status(thm),theory(equality)],[2741]),
[iquote('4:Obv:2741.1')] ).
cnf(2749,plain,
( equal(op(e2,e3),e2)
| equal(op(e2,e3),e1)
| equal(op(e2,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[2591,691]),
[iquote('4:Rew:2591.0,691.2')] ).
cnf(2750,plain,
equal(op(e2,e3),unit),
inference(mrr,[status(thm)],[2749,2654,2675]),
[iquote('4:MRR:2749.0,2749.1,2654.0,2675.0')] ).
cnf(2759,plain,
( ~ skC17
| equal(op(unit,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[2750,136]),
[iquote('4:Rew:2750.0,136.1')] ).
cnf(2761,plain,
( ~ skC17
| equal(e3,e2) ),
inference(rew,[status(thm),theory(equality)],[17,2759]),
[iquote('4:Rew:17.0,2759.1')] ).
cnf(2762,plain,
~ skC17,
inference(mrr,[status(thm)],[2761,8]),
[iquote('4:MRR:2761.1,8.0')] ).
cnf(2766,plain,
equal(op(e1,e3),e2),
inference(mrr,[status(thm)],[695,2624,2625]),
[iquote('4:MRR:695.0,695.1,2624.0,2625.0')] ).
cnf(2775,plain,
( ~ skC12
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[2766,2697]),
[iquote('4:Rew:2766.0,2697.1')] ).
cnf(2776,plain,
~ skC12,
inference(obv,[status(thm),theory(equality)],[2775]),
[iquote('4:Obv:2775.1')] ).
cnf(2777,plain,
( equal(e3,e2)
| equal(op(e4,e1),e3)
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[13,665,2591,2674]),
[iquote('4:Rew:13.0,665.2,2591.0,665.2,2674.0,665.0')] ).
cnf(2778,plain,
equal(op(e4,e1),e3),
inference(mrr,[status(thm)],[2777,8,6]),
[iquote('4:MRR:2777.0,2777.2,8.0,6.0')] ).
cnf(2785,plain,
( ~ skC25
| equal(op(e3,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[2778,144]),
[iquote('4:Rew:2778.0,144.1')] ).
cnf(2788,plain,
( ~ skC13
| ~ equal(op(e1,e4),e3) ),
inference(rew,[status(thm),theory(equality)],[2778,166]),
[iquote('4:Rew:2778.0,166.1')] ).
cnf(2790,plain,
( ~ skC25
| equal(e4,e2) ),
inference(rew,[status(thm),theory(equality)],[2674,2785]),
[iquote('4:Rew:2674.0,2785.1')] ).
cnf(2791,plain,
~ skC25,
inference(mrr,[status(thm)],[2790,9]),
[iquote('4:MRR:2790.1,9.0')] ).
cnf(2792,plain,
( equal(e3,e2)
| equal(op(e1,e4),e3)
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[14,667,2591,2766]),
[iquote('4:Rew:14.0,667.2,2591.0,667.2,2766.0,667.0')] ).
cnf(2793,plain,
equal(op(e1,e4),e3),
inference(mrr,[status(thm)],[2792,8,6]),
[iquote('4:MRR:2792.0,2792.2,8.0,6.0')] ).
cnf(2802,plain,
( ~ skC13
| ~ equal(e3,e3) ),
inference(rew,[status(thm),theory(equality)],[2793,2788]),
[iquote('4:Rew:2793.0,2788.1')] ).
cnf(2803,plain,
~ skC13,
inference(obv,[status(thm),theory(equality)],[2802]),
[iquote('4:Obv:2802.1')] ).
cnf(2805,plain,
( equal(e4,e3)
| equal(op(e2,e1),e4)
| equal(e4,e1) ),
inference(rew,[status(thm),theory(equality)],[13,661,2591,2778]),
[iquote('4:Rew:13.0,661.2,2591.0,661.2,2778.0,661.0')] ).
cnf(2806,plain,
equal(op(e2,e1),e4),
inference(mrr,[status(thm)],[2805,10,7]),
[iquote('4:MRR:2805.0,2805.2,10.0,7.0')] ).
cnf(2814,plain,
( ~ skC15
| ~ equal(e4,e4) ),
inference(rew,[status(thm),theory(equality)],[2806,2709]),
[iquote('4:Rew:2806.0,2709.1')] ).
cnf(2815,plain,
~ skC15,
inference(obv,[status(thm),theory(equality)],[2814]),
[iquote('4:Obv:2814.1')] ).
cnf(2822,plain,
( skC27
| skC18 ),
inference(mrr,[status(thm)],[704,2735,2791,2742,2722,2684,2740,2762,2815,2738,2803,2776,2708,2696,2720,2691,2686,2694]),
[iquote('4:MRR:704.1,704.2,704.3,704.4,704.5,704.6,704.8,704.9,704.10,704.11,704.12,704.13,704.14,704.15,704.16,704.17,704.18,2735.0,2791.0,2742.0,2722.0,2684.0,2740.0,2762.0,2815.0,2738.0,2803.0,2776.0,2708.0,2696.0,2720.0,2691.0,2686.0,2694.0')] ).
cnf(2837,plain,
( equal(e2,e1)
| equal(op(e4,e3),e1)
| equal(e1,unit)
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[17,641,2591,2750,2766]),
[iquote('4:Rew:17.0,641.3,2591.0,641.3,2750.0,641.2,2766.0,641.0')] ).
cnf(2838,plain,
equal(op(e4,e3),e1),
inference(mrr,[status(thm)],[2837,5,2599,6]),
[iquote('4:MRR:2837.0,2837.2,2837.3,5.0,2599.0,6.0')] ).
cnf(2842,plain,
( ~ skC27
| equal(op(e1,e3),e4) ),
inference(rew,[status(thm),theory(equality)],[2838,146]),
[iquote('4:Rew:2838.0,146.1')] ).
cnf(2846,plain,
( ~ skC27
| equal(e4,e2) ),
inference(rew,[status(thm),theory(equality)],[2766,2842]),
[iquote('4:Rew:2766.0,2842.1')] ).
cnf(2847,plain,
~ skC27,
inference(mrr,[status(thm)],[2846,9]),
[iquote('4:MRR:2846.1,9.0')] ).
cnf(2848,plain,
skC18,
inference(mrr,[status(thm)],[2822,2847]),
[iquote('4:MRR:2822.0,2847.0')] ).
cnf(2850,plain,
~ equal(op(op(e2,e4),e2),e4),
inference(mrr,[status(thm)],[177,2848]),
[iquote('4:MRR:177.0,2848.0')] ).
cnf(2851,plain,
( equal(e4,e1)
| equal(op(e2,e4),e1)
| equal(e1,unit)
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[16,655,2591,2750,2806]),
[iquote('4:Rew:16.0,655.3,2591.0,655.3,2750.0,655.2,2806.0,655.0')] ).
cnf(2852,plain,
equal(op(e2,e4),e1),
inference(mrr,[status(thm)],[2851,7,2599,5]),
[iquote('4:MRR:2851.0,2851.2,2851.3,7.0,2599.0,5.0')] ).
cnf(2859,plain,
~ equal(op(e1,e2),e4),
inference(rew,[status(thm),theory(equality)],[2852,2850]),
[iquote('4:Rew:2852.0,2850.0')] ).
cnf(2862,plain,
~ equal(e4,e4),
inference(rew,[status(thm),theory(equality)],[2698,2859]),
[iquote('4:Rew:2698.0,2859.0')] ).
cnf(2863,plain,
$false,
inference(obv,[status(thm),theory(equality)],[2862]),
[iquote('4:Obv:2862.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : ALG059+1 : TPTP v8.1.0. Released v2.7.0.
% 0.09/0.10 % Command : run_spass %d %s
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 600
% 0.09/0.28 % DateTime : Tue Jun 7 23:25:21 EDT 2022
% 0.09/0.28 % CPUTime :
% 0.36/0.56
% 0.36/0.56 SPASS V 3.9
% 0.36/0.56 SPASS beiseite: Proof found.
% 0.36/0.56 % SZS status Theorem
% 0.36/0.56 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.56 SPASS derived 1350 clauses, backtracked 1175 clauses, performed 4 splits and kept 1871 clauses.
% 0.36/0.56 SPASS allocated 86744 KBytes.
% 0.36/0.56 SPASS spent 0:00:00.27 on the problem.
% 0.36/0.56 0:00:00.03 for the input.
% 0.36/0.56 0:00:00.07 for the FLOTTER CNF translation.
% 0.36/0.56 0:00:00.00 for inferences.
% 0.36/0.56 0:00:00.00 for the backtracking.
% 0.36/0.56 0:00:00.14 for the reduction.
% 0.36/0.56
% 0.36/0.56
% 0.36/0.56 Here is a proof with depth 4, length 544 :
% 0.36/0.56 % SZS output start Refutation
% See solution above
% 0.36/0.57 Formulae used in the proof : ax5 ax2 ax6 ax4 co1 ax3 ax1
% 0.36/0.57
%------------------------------------------------------------------------------