%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG056+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.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:09 EDT 2022
% Result : Theorem 0.43s 0.61s
% Output : Refutation 0.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 143
% Syntax : Number of clauses : 429 ( 238 unt; 105 nHn; 429 RR)
% Number of literals : 857 ( 0 equ; 288 neg)
% Maximal clause size : 25 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 37 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('ALG056+1.p',unknown),
[] ).
cnf(2,axiom,
~ equal(e2,e0),
file('ALG056+1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(e3,e0),
file('ALG056+1.p',unknown),
[] ).
cnf(4,axiom,
~ equal(e4,e0),
file('ALG056+1.p',unknown),
[] ).
cnf(5,axiom,
~ equal(e2,e1),
file('ALG056+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e3,e1),
file('ALG056+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(e4,e1),
file('ALG056+1.p',unknown),
[] ).
cnf(8,axiom,
~ equal(e3,e2),
file('ALG056+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(e4,e2),
file('ALG056+1.p',unknown),
[] ).
cnf(10,axiom,
~ equal(e4,e3),
file('ALG056+1.p',unknown),
[] ).
cnf(11,axiom,
equal(op(unit,e0),e0),
file('ALG056+1.p',unknown),
[] ).
cnf(12,axiom,
equal(op(e0,unit),e0),
file('ALG056+1.p',unknown),
[] ).
cnf(13,axiom,
equal(op(unit,e1),e1),
file('ALG056+1.p',unknown),
[] ).
cnf(14,axiom,
equal(op(e1,unit),e1),
file('ALG056+1.p',unknown),
[] ).
cnf(15,axiom,
equal(op(unit,e2),e2),
file('ALG056+1.p',unknown),
[] ).
cnf(16,axiom,
equal(op(e2,unit),e2),
file('ALG056+1.p',unknown),
[] ).
cnf(17,axiom,
equal(op(unit,e3),e3),
file('ALG056+1.p',unknown),
[] ).
cnf(18,axiom,
equal(op(e3,unit),e3),
file('ALG056+1.p',unknown),
[] ).
cnf(19,axiom,
equal(op(unit,e4),e4),
file('ALG056+1.p',unknown),
[] ).
cnf(20,axiom,
equal(op(e4,unit),e4),
file('ALG056+1.p',unknown),
[] ).
cnf(21,axiom,
equal(op(e2,e2),e4),
file('ALG056+1.p',unknown),
[] ).
cnf(22,axiom,
( ~ skC20
| equal(op(e0,e0),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ skC21
| equal(op(e0,e0),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ skC22
| equal(op(e2,e2),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(27,axiom,
( ~ skC23
| equal(op(e0,e0),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ skC24
| equal(op(e0,e0),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(31,axiom,
( ~ skC25
| equal(op(e1,e1),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ skC26
| equal(op(e1,e1),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ skC27
| equal(op(e2,e2),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(37,axiom,
( ~ skC28
| equal(op(e3,e3),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ skC29
| equal(op(e4,e4),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ skC30
| equal(op(e2,e2),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ skC31
| equal(op(e2,e2),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ skC32
| equal(op(e2,e2),e2) ),
file('ALG056+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ skC33
| equal(op(e2,e2),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(48,axiom,
( ~ skC34
| equal(op(e4,e4),e2) ),
file('ALG056+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ skC35
| equal(op(e0,e0),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ skC36
| equal(op(e3,e3),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ skC37
| equal(op(e2,e2),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ skC38
| equal(op(e3,e3),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ skC39
| equal(op(e4,e4),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ skC40
| equal(op(e0,e0),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ skC41
| equal(op(e4,e4),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ skC42
| equal(op(e4,e4),e2) ),
file('ALG056+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ skC43
| equal(op(e4,e4),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(66,axiom,
equal(op(e2,op(e2,e2)),e3),
file('ALG056+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ equal(op(e0,e0),e0)
| ~ skC20 ),
file('ALG056+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ equal(op(e1,e1),e1)
| ~ skC26 ),
file('ALG056+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ equal(op(e3,e3),e3)
| ~ skC38 ),
file('ALG056+1.p',unknown),
[] ).
cnf(92,axiom,
~ equal(op(e2,e0),op(e0,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(95,axiom,
~ equal(op(e2,e0),op(e1,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(98,axiom,
~ equal(op(e3,e0),op(e2,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(99,axiom,
~ equal(op(e4,e0),op(e2,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(102,axiom,
~ equal(op(e2,e1),op(e0,e1)),
file('ALG056+1.p',unknown),
[] ).
cnf(103,axiom,
~ equal(op(e3,e1),op(e0,e1)),
file('ALG056+1.p',unknown),
[] ).
cnf(110,axiom,
~ equal(op(e4,e1),op(e3,e1)),
file('ALG056+1.p',unknown),
[] ).
cnf(113,axiom,
~ equal(op(e3,e2),op(e0,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(114,axiom,
~ equal(op(e4,e2),op(e0,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(118,axiom,
~ equal(op(e3,e2),op(e2,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(119,axiom,
~ equal(op(e4,e2),op(e2,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(120,axiom,
~ equal(op(e4,e2),op(e3,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(121,axiom,
~ equal(op(e1,e3),op(e0,e3)),
file('ALG056+1.p',unknown),
[] ).
cnf(124,axiom,
~ equal(op(e4,e3),op(e0,e3)),
file('ALG056+1.p',unknown),
[] ).
cnf(126,axiom,
~ equal(op(e3,e3),op(e1,e3)),
file('ALG056+1.p',unknown),
[] ).
cnf(129,axiom,
~ equal(op(e4,e3),op(e2,e3)),
file('ALG056+1.p',unknown),
[] ).
cnf(130,axiom,
~ equal(op(e4,e3),op(e3,e3)),
file('ALG056+1.p',unknown),
[] ).
cnf(131,axiom,
~ equal(op(e1,e4),op(e0,e4)),
file('ALG056+1.p',unknown),
[] ).
cnf(132,axiom,
~ equal(op(e2,e4),op(e0,e4)),
file('ALG056+1.p',unknown),
[] ).
cnf(133,axiom,
~ equal(op(e3,e4),op(e0,e4)),
file('ALG056+1.p',unknown),
[] ).
cnf(134,axiom,
~ equal(op(e4,e4),op(e0,e4)),
file('ALG056+1.p',unknown),
[] ).
cnf(135,axiom,
~ equal(op(e2,e4),op(e1,e4)),
file('ALG056+1.p',unknown),
[] ).
cnf(136,axiom,
~ equal(op(e3,e4),op(e1,e4)),
file('ALG056+1.p',unknown),
[] ).
cnf(137,axiom,
~ equal(op(e4,e4),op(e1,e4)),
file('ALG056+1.p',unknown),
[] ).
cnf(139,axiom,
~ equal(op(e4,e4),op(e2,e4)),
file('ALG056+1.p',unknown),
[] ).
cnf(142,axiom,
~ equal(op(e0,e2),op(e0,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(145,axiom,
~ equal(op(e0,e2),op(e0,e1)),
file('ALG056+1.p',unknown),
[] ).
cnf(148,axiom,
~ equal(op(e0,e3),op(e0,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(153,axiom,
~ equal(op(e1,e3),op(e1,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(154,axiom,
~ equal(op(e1,e4),op(e1,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(156,axiom,
~ equal(op(e1,e3),op(e1,e1)),
file('ALG056+1.p',unknown),
[] ).
cnf(159,axiom,
~ equal(op(e1,e4),op(e1,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(160,axiom,
~ equal(op(e1,e4),op(e1,e3)),
file('ALG056+1.p',unknown),
[] ).
cnf(162,axiom,
~ equal(op(e2,e2),op(e2,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(163,axiom,
~ equal(op(e2,e3),op(e2,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(164,axiom,
~ equal(op(e2,e4),op(e2,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(171,axiom,
~ equal(op(e3,e1),op(e3,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(172,axiom,
~ equal(op(e3,e2),op(e3,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(173,axiom,
~ equal(op(e3,e3),op(e3,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(174,axiom,
~ equal(op(e3,e4),op(e3,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(178,axiom,
~ equal(op(e3,e3),op(e3,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(179,axiom,
~ equal(op(e3,e4),op(e3,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(180,axiom,
~ equal(op(e3,e4),op(e3,e3)),
file('ALG056+1.p',unknown),
[] ).
cnf(181,axiom,
~ equal(op(e4,e1),op(e4,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(182,axiom,
~ equal(op(e4,e2),op(e4,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(183,axiom,
~ equal(op(e4,e3),op(e4,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(184,axiom,
~ equal(op(e4,e4),op(e4,e0)),
file('ALG056+1.p',unknown),
[] ).
cnf(185,axiom,
~ equal(op(e4,e2),op(e4,e1)),
file('ALG056+1.p',unknown),
[] ).
cnf(186,axiom,
~ equal(op(e4,e3),op(e4,e1)),
file('ALG056+1.p',unknown),
[] ).
cnf(187,axiom,
~ equal(op(e4,e4),op(e4,e1)),
file('ALG056+1.p',unknown),
[] ).
cnf(189,axiom,
~ equal(op(e4,e4),op(e4,e2)),
file('ALG056+1.p',unknown),
[] ).
cnf(190,axiom,
~ equal(op(e4,e4),op(e4,e3)),
file('ALG056+1.p',unknown),
[] ).
cnf(191,axiom,
( ~ skC0
| equal(op(e0,op(e0,e0)),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(193,axiom,
( ~ skC2
| equal(op(e0,op(e2,e0)),e2) ),
file('ALG056+1.p',unknown),
[] ).
cnf(203,axiom,
( ~ skC12
| equal(op(e3,op(e0,e3)),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(204,axiom,
( ~ skC13
| equal(op(e3,op(e1,e3)),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(205,axiom,
( ~ skC14
| equal(op(e3,op(e2,e3)),e2) ),
file('ALG056+1.p',unknown),
[] ).
cnf(206,axiom,
( ~ skC15
| equal(op(e3,op(e3,e3)),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(207,axiom,
( ~ skC16
| equal(op(e4,op(e0,e4)),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(208,axiom,
( ~ skC17
| equal(op(e4,op(e1,e4)),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(209,axiom,
( ~ skC18
| equal(op(e4,op(e2,e4)),e2) ),
file('ALG056+1.p',unknown),
[] ).
cnf(210,axiom,
( ~ skC19
| equal(op(e4,op(e3,e4)),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(211,axiom,
equal(op(op(e2,e2),op(e2,e2)),e0),
file('ALG056+1.p',unknown),
[] ).
cnf(212,axiom,
( ~ equal(op(e0,op(e0,e0)),e0)
| ~ skC0 ),
file('ALG056+1.p',unknown),
[] ).
cnf(213,axiom,
( ~ skC1
| ~ equal(op(e1,op(e1,e0)),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(215,axiom,
( ~ skC3
| ~ equal(op(e3,op(e3,e0)),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(227,axiom,
( ~ equal(op(e3,op(e3,e3)),e3)
| ~ skC15 ),
file('ALG056+1.p',unknown),
[] ).
cnf(232,axiom,
( equal(op(e0,op(e4,e0)),e4)
| skC0
| skC1
| skC2
| skC3 ),
file('ALG056+1.p',unknown),
[] ).
cnf(235,axiom,
( equal(op(e3,op(e4,e3)),e4)
| skC12
| skC13
| skC14
| skC15 ),
file('ALG056+1.p',unknown),
[] ).
cnf(236,axiom,
( equal(op(e4,op(e4,e4)),e4)
| skC16
| skC17
| skC18
| skC19 ),
file('ALG056+1.p',unknown),
[] ).
cnf(237,axiom,
equal(op(op(e2,op(e2,e2)),op(e2,e2)),e1),
file('ALG056+1.p',unknown),
[] ).
cnf(242,axiom,
( ~ equal(op(e4,op(e4,e4)),e4)
| skC16
| skC17
| skC18
| skC19 ),
file('ALG056+1.p',unknown),
[] ).
cnf(243,axiom,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit)
| equal(e0,unit) ),
file('ALG056+1.p',unknown),
[] ).
cnf(260,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('ALG056+1.p',unknown),
[] ).
cnf(266,axiom,
( equal(op(e0,e2),e3)
| equal(op(e1,e2),e3)
| equal(op(e2,e2),e3)
| equal(op(e3,e2),e3)
| equal(op(e4,e2),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(268,axiom,
( equal(op(e0,e2),e2)
| equal(op(e1,e2),e2)
| equal(op(e2,e2),e2)
| equal(op(e3,e2),e2)
| equal(op(e4,e2),e2) ),
file('ALG056+1.p',unknown),
[] ).
cnf(270,axiom,
( equal(op(e0,e2),e1)
| equal(op(e1,e2),e1)
| equal(op(e2,e2),e1)
| equal(op(e3,e2),e1)
| equal(op(e4,e2),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(271,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('ALG056+1.p',unknown),
[] ).
cnf(272,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('ALG056+1.p',unknown),
[] ).
cnf(273,axiom,
( equal(op(e2,e0),e0)
| equal(op(e2,e1),e0)
| equal(op(e2,e2),e0)
| equal(op(e2,e3),e0)
| equal(op(e2,e4),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(286,axiom,
( equal(op(e0,e0),e3)
| equal(op(e1,e0),e3)
| equal(op(e2,e0),e3)
| equal(op(e3,e0),e3)
| equal(op(e4,e0),e3) ),
file('ALG056+1.p',unknown),
[] ).
cnf(290,axiom,
( equal(op(e0,e0),e1)
| equal(op(e1,e0),e1)
| equal(op(e2,e0),e1)
| equal(op(e3,e0),e1)
| equal(op(e4,e0),e1) ),
file('ALG056+1.p',unknown),
[] ).
cnf(291,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('ALG056+1.p',unknown),
[] ).
cnf(295,axiom,
( equal(op(e4,e3),e0)
| equal(op(e4,e3),e1)
| equal(op(e4,e3),e2)
| equal(op(e4,e3),e3)
| equal(op(e4,e3),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(296,axiom,
( equal(op(e4,e2),e0)
| equal(op(e4,e2),e1)
| equal(op(e4,e2),e2)
| equal(op(e4,e2),e3)
| equal(op(e4,e2),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(297,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('ALG056+1.p',unknown),
[] ).
cnf(298,axiom,
( equal(op(e4,e0),e0)
| equal(op(e4,e0),e1)
| equal(op(e4,e0),e2)
| equal(op(e4,e0),e3)
| equal(op(e4,e0),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(300,axiom,
( equal(op(e3,e3),e0)
| equal(op(e3,e3),e1)
| equal(op(e3,e3),e2)
| equal(op(e3,e3),e3)
| equal(op(e3,e3),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(301,axiom,
( equal(op(e3,e2),e0)
| equal(op(e3,e2),e1)
| equal(op(e3,e2),e2)
| equal(op(e3,e2),e3)
| equal(op(e3,e2),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(308,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('ALG056+1.p',unknown),
[] ).
cnf(309,axiom,
( equal(op(e1,e4),e0)
| equal(op(e1,e4),e1)
| equal(op(e1,e4),e2)
| equal(op(e1,e4),e3)
| equal(op(e1,e4),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(310,axiom,
( equal(op(e1,e3),e3)
| equal(op(e1,e3),e1)
| equal(op(e1,e3),e4)
| equal(op(e1,e3),e2)
| equal(op(e1,e3),e0) ),
file('ALG056+1.p',unknown),
[] ).
cnf(314,axiom,
( equal(op(e0,e4),e0)
| equal(op(e0,e4),e1)
| equal(op(e0,e4),e2)
| equal(op(e0,e4),e3)
| equal(op(e0,e4),e4) ),
file('ALG056+1.p',unknown),
[] ).
cnf(319,axiom,
( equal(op(e4,e4),e4)
| skC20
| skC21
| skC22
| skC23
| skC24
| skC25
| skC26
| skC27
| skC28
| skC29
| skC30
| skC31
| skC32
| skC33
| skC34
| skC35
| skC36
| skC37
| skC38
| skC39
| skC40
| skC41
| skC42
| skC43 ),
file('ALG056+1.p',unknown),
[] ).
cnf(321,plain,
equal(op(e2,e4),e3),
inference(rew,[status(thm),theory(equality)],[21,66]),
[iquote('0:Rew:21.0,66.0')] ).
cnf(322,plain,
( ~ skC37
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[21,54]),
[iquote('0:Rew:21.0,54.1')] ).
cnf(323,plain,
~ skC37,
inference(mrr,[status(thm)],[322,10]),
[iquote('0:MRR:322.1,10.0')] ).
cnf(324,plain,
( ~ skC33
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[21,45]),
[iquote('0:Rew:21.0,45.1')] ).
cnf(325,plain,
~ skC33,
inference(mrr,[status(thm)],[324,10]),
[iquote('0:MRR:324.1,10.0')] ).
cnf(326,plain,
( ~ skC32
| equal(e4,e2) ),
inference(rew,[status(thm),theory(equality)],[21,44]),
[iquote('0:Rew:21.0,44.1')] ).
cnf(327,plain,
~ skC32,
inference(mrr,[status(thm)],[326,9]),
[iquote('0:MRR:326.1,9.0')] ).
cnf(328,plain,
( ~ skC31
| equal(e4,e1) ),
inference(rew,[status(thm),theory(equality)],[21,42]),
[iquote('0:Rew:21.0,42.1')] ).
cnf(329,plain,
~ skC31,
inference(mrr,[status(thm)],[328,7]),
[iquote('0:MRR:328.1,7.0')] ).
cnf(330,plain,
( ~ skC30
| equal(e4,e0) ),
inference(rew,[status(thm),theory(equality)],[21,40]),
[iquote('0:Rew:21.0,40.1')] ).
cnf(331,plain,
~ skC30,
inference(mrr,[status(thm)],[330,4]),
[iquote('0:MRR:330.1,4.0')] ).
cnf(332,plain,
( ~ skC27
| equal(e4,e1) ),
inference(rew,[status(thm),theory(equality)],[21,35]),
[iquote('0:Rew:21.0,35.1')] ).
cnf(333,plain,
~ skC27,
inference(mrr,[status(thm)],[332,7]),
[iquote('0:MRR:332.1,7.0')] ).
cnf(334,plain,
( ~ skC22
| equal(e4,e0) ),
inference(rew,[status(thm),theory(equality)],[21,26]),
[iquote('0:Rew:21.0,26.1')] ).
cnf(335,plain,
~ skC22,
inference(mrr,[status(thm)],[334,4]),
[iquote('0:MRR:334.1,4.0')] ).
cnf(341,plain,
~ equal(op(e2,e0),e3),
inference(rew,[status(thm),theory(equality)],[321,164]),
[iquote('0:Rew:321.0,164.0')] ).
cnf(342,plain,
~ equal(op(e2,e0),e4),
inference(rew,[status(thm),theory(equality)],[21,162]),
[iquote('0:Rew:21.0,162.0')] ).
cnf(343,plain,
~ equal(op(e4,e4),e3),
inference(rew,[status(thm),theory(equality)],[321,139]),
[iquote('0:Rew:321.0,139.0')] ).
cnf(344,plain,
~ skC43,
inference(mrr,[status(thm)],[64,343]),
[iquote('0:MRR:64.1,343.0')] ).
cnf(345,plain,
~ skC39,
inference(mrr,[status(thm)],[57,343]),
[iquote('0:MRR:57.1,343.0')] ).
cnf(347,plain,
~ equal(op(e1,e4),e3),
inference(rew,[status(thm),theory(equality)],[321,135]),
[iquote('0:Rew:321.0,135.0')] ).
cnf(348,plain,
~ equal(op(e0,e4),e3),
inference(rew,[status(thm),theory(equality)],[321,132]),
[iquote('0:Rew:321.0,132.0')] ).
cnf(349,plain,
~ equal(op(e4,e2),e4),
inference(rew,[status(thm),theory(equality)],[21,119]),
[iquote('0:Rew:21.0,119.0')] ).
cnf(350,plain,
~ equal(op(e3,e2),e4),
inference(rew,[status(thm),theory(equality)],[21,118]),
[iquote('0:Rew:21.0,118.0')] ).
cnf(353,plain,
( ~ equal(e3,e3)
| ~ skC38 ),
inference(rew,[status(thm),theory(equality)],[55,85]),
[iquote('0:Rew:55.1,85.0')] ).
cnf(354,plain,
~ skC38,
inference(obv,[status(thm),theory(equality)],[353]),
[iquote('0:Obv:353.0')] ).
cnf(356,plain,
( ~ equal(e1,e1)
| ~ skC26 ),
inference(rew,[status(thm),theory(equality)],[33,73]),
[iquote('0:Rew:33.1,73.0')] ).
cnf(357,plain,
~ skC26,
inference(obv,[status(thm),theory(equality)],[356]),
[iquote('0:Obv:356.0')] ).
cnf(358,plain,
( ~ equal(e0,e0)
| ~ skC20 ),
inference(rew,[status(thm),theory(equality)],[22,67]),
[iquote('0:Rew:22.1,67.0')] ).
cnf(359,plain,
~ skC20,
inference(obv,[status(thm),theory(equality)],[358]),
[iquote('0:Obv:358.0')] ).
cnf(360,plain,
equal(op(e4,e4),e0),
inference(rew,[status(thm),theory(equality)],[21,211]),
[iquote('0:Rew:21.0,211.0')] ).
cnf(361,plain,
( ~ skC34
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[360,48]),
[iquote('0:Rew:360.0,48.1')] ).
cnf(362,plain,
( ~ skC42
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[360,62]),
[iquote('0:Rew:360.0,62.1')] ).
cnf(363,plain,
( ~ skC29
| equal(e1,e0) ),
inference(rew,[status(thm),theory(equality)],[360,39]),
[iquote('0:Rew:360.0,39.1')] ).
cnf(364,plain,
( ~ skC41
| equal(e1,e0) ),
inference(rew,[status(thm),theory(equality)],[360,60]),
[iquote('0:Rew:360.0,60.1')] ).
cnf(365,plain,
~ equal(op(e4,e3),e0),
inference(rew,[status(thm),theory(equality)],[360,190]),
[iquote('0:Rew:360.0,190.0')] ).
cnf(366,plain,
~ equal(op(e4,e2),e0),
inference(rew,[status(thm),theory(equality)],[360,189]),
[iquote('0:Rew:360.0,189.0')] ).
cnf(367,plain,
~ equal(op(e4,e1),e0),
inference(rew,[status(thm),theory(equality)],[360,187]),
[iquote('0:Rew:360.0,187.0')] ).
cnf(368,plain,
~ equal(op(e4,e0),e0),
inference(rew,[status(thm),theory(equality)],[360,184]),
[iquote('0:Rew:360.0,184.0')] ).
cnf(371,plain,
~ equal(op(e1,e4),e0),
inference(rew,[status(thm),theory(equality)],[360,137]),
[iquote('0:Rew:360.0,137.0')] ).
cnf(372,plain,
~ equal(op(e0,e4),e0),
inference(rew,[status(thm),theory(equality)],[360,134]),
[iquote('0:Rew:360.0,134.0')] ).
cnf(373,plain,
~ skC34,
inference(mrr,[status(thm)],[361,2]),
[iquote('0:MRR:361.1,2.0')] ).
cnf(374,plain,
~ skC42,
inference(mrr,[status(thm)],[362,2]),
[iquote('0:MRR:362.1,2.0')] ).
cnf(375,plain,
~ skC29,
inference(mrr,[status(thm)],[363,1]),
[iquote('0:MRR:363.1,1.0')] ).
cnf(376,plain,
~ skC41,
inference(mrr,[status(thm)],[364,1]),
[iquote('0:MRR:364.1,1.0')] ).
cnf(377,plain,
( ~ skC18
| equal(op(e4,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[321,209]),
[iquote('0:Rew:321.0,209.1')] ).
cnf(381,plain,
( ~ equal(e3,e3)
| ~ skC15 ),
inference(rew,[status(thm),theory(equality)],[206,227]),
[iquote('0:Rew:206.1,227.0')] ).
cnf(382,plain,
~ skC15,
inference(obv,[status(thm),theory(equality)],[381]),
[iquote('0:Obv:381.0')] ).
cnf(385,plain,
( ~ equal(e0,e0)
| ~ skC0 ),
inference(rew,[status(thm),theory(equality)],[191,212]),
[iquote('0:Rew:191.1,212.0')] ).
cnf(386,plain,
~ skC0,
inference(obv,[status(thm),theory(equality)],[385]),
[iquote('0:Obv:385.0')] ).
cnf(387,plain,
equal(op(e3,e4),e1),
inference(rew,[status(thm),theory(equality)],[321,237,21]),
[iquote('0:Rew:321.0,237.0,21.0,237.0')] ).
cnf(388,plain,
~ equal(op(e3,e3),e1),
inference(rew,[status(thm),theory(equality)],[387,180]),
[iquote('0:Rew:387.0,180.0')] ).
cnf(389,plain,
~ equal(op(e3,e2),e1),
inference(rew,[status(thm),theory(equality)],[387,179]),
[iquote('0:Rew:387.0,179.0')] ).
cnf(391,plain,
~ equal(op(e3,e0),e1),
inference(rew,[status(thm),theory(equality)],[387,174]),
[iquote('0:Rew:387.0,174.0')] ).
cnf(393,plain,
~ equal(op(e1,e4),e1),
inference(rew,[status(thm),theory(equality)],[387,136]),
[iquote('0:Rew:387.0,136.0')] ).
cnf(394,plain,
~ equal(op(e0,e4),e1),
inference(rew,[status(thm),theory(equality)],[387,133]),
[iquote('0:Rew:387.0,133.0')] ).
cnf(396,plain,
( ~ skC19
| equal(op(e4,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[387,210]),
[iquote('0:Rew:387.0,210.1')] ).
cnf(398,plain,
~ skC36,
inference(mrr,[status(thm)],[51,388]),
[iquote('0:MRR:51.1,388.0')] ).
cnf(399,plain,
~ skC28,
inference(mrr,[status(thm)],[37,388]),
[iquote('0:MRR:37.1,388.0')] ).
cnf(400,plain,
( equal(op(e4,e0),e4)
| skC16
| skC17
| skC18
| skC19 ),
inference(rew,[status(thm),theory(equality)],[360,236]),
[iquote('0:Rew:360.0,236.0')] ).
cnf(401,plain,
( skC14
| skC13
| skC12
| equal(op(e3,op(e4,e3)),e4) ),
inference(mrr,[status(thm)],[235,382]),
[iquote('0:MRR:235.4,382.0')] ).
cnf(404,plain,
( skC3
| skC2
| skC1
| equal(op(e0,op(e4,e0)),e4) ),
inference(mrr,[status(thm)],[232,386]),
[iquote('0:MRR:232.1,386.0')] ).
cnf(405,plain,
( ~ equal(e4,e4)
| skC16
| skC17
| skC18
| skC19 ),
inference(rew,[status(thm),theory(equality)],[400,242,360]),
[iquote('0:Rew:400.0,242.0,360.0,242.0')] ).
cnf(406,plain,
( skC19
| skC18
| skC17
| skC16 ),
inference(obv,[status(thm),theory(equality)],[405]),
[iquote('0:Obv:405.0')] ).
cnf(431,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)],[260,388]),
[iquote('0:MRR:260.3,388.0')] ).
cnf(435,plain,
( equal(op(e0,e2),e3)
| equal(op(e1,e2),e3)
| equal(e4,e3)
| equal(op(e3,e2),e3)
| equal(op(e4,e2),e3) ),
inference(rew,[status(thm),theory(equality)],[21,266]),
[iquote('0:Rew:21.0,266.2')] ).
cnf(436,plain,
( equal(op(e3,e2),e3)
| equal(op(e4,e2),e3)
| equal(op(e1,e2),e3)
| equal(op(e0,e2),e3) ),
inference(mrr,[status(thm)],[435,10]),
[iquote('0:MRR:435.2,10.0')] ).
cnf(437,plain,
( equal(op(e0,e2),e2)
| equal(op(e1,e2),e2)
| equal(e4,e2)
| equal(op(e3,e2),e2)
| equal(op(e4,e2),e2) ),
inference(rew,[status(thm),theory(equality)],[21,268]),
[iquote('0:Rew:21.0,268.2')] ).
cnf(438,plain,
( equal(op(e4,e2),e2)
| equal(op(e3,e2),e2)
| equal(op(e1,e2),e2)
| equal(op(e0,e2),e2) ),
inference(mrr,[status(thm)],[437,9]),
[iquote('0:MRR:437.2,9.0')] ).
cnf(441,plain,
( equal(op(e0,e2),e1)
| equal(op(e1,e2),e1)
| equal(e4,e1)
| equal(op(e3,e2),e1)
| equal(op(e4,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[21,270]),
[iquote('0:Rew:21.0,270.2')] ).
cnf(442,plain,
( equal(op(e1,e2),e1)
| equal(op(e4,e2),e1)
| equal(op(e0,e2),e1) ),
inference(mrr,[status(thm)],[441,7,389]),
[iquote('0:MRR:441.2,441.3,7.0,389.0')] ).
cnf(443,plain,
( equal(op(e2,e0),e1)
| equal(op(e2,e1),e1)
| equal(e4,e1)
| equal(op(e2,e3),e1)
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[321,271,21]),
[iquote('0:Rew:321.0,271.4,21.0,271.2')] ).
cnf(444,plain,
( equal(op(e2,e1),e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[443,7,6]),
[iquote('0:MRR:443.2,443.4,7.0,6.0')] ).
cnf(445,plain,
( equal(op(e0,e2),e0)
| equal(op(e1,e2),e0)
| equal(e4,e0)
| equal(op(e3,e2),e0)
| equal(op(e4,e2),e0) ),
inference(rew,[status(thm),theory(equality)],[21,272]),
[iquote('0:Rew:21.0,272.2')] ).
cnf(446,plain,
( equal(op(e0,e2),e0)
| equal(op(e3,e2),e0)
| equal(op(e1,e2),e0) ),
inference(mrr,[status(thm)],[445,4,366]),
[iquote('0:MRR:445.2,445.4,4.0,366.0')] ).
cnf(447,plain,
( equal(op(e2,e0),e0)
| equal(op(e2,e1),e0)
| equal(e4,e0)
| equal(op(e2,e3),e0)
| equal(e3,e0) ),
inference(rew,[status(thm),theory(equality)],[321,273,21]),
[iquote('0:Rew:321.0,273.4,21.0,273.2')] ).
cnf(448,plain,
( equal(op(e2,e0),e0)
| equal(op(e2,e3),e0)
| equal(op(e2,e1),e0) ),
inference(mrr,[status(thm)],[447,4,3]),
[iquote('0:MRR:447.2,447.4,4.0,3.0')] ).
cnf(459,plain,
( equal(op(e3,e0),e3)
| equal(op(e0,e0),e3)
| equal(op(e4,e0),e3)
| equal(op(e1,e0),e3) ),
inference(mrr,[status(thm)],[286,341]),
[iquote('0:MRR:286.2,341.0')] ).
cnf(461,plain,
( equal(op(e1,e0),e1)
| equal(op(e0,e0),e1)
| equal(op(e4,e0),e1)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[290,391]),
[iquote('0:MRR:290.3,391.0')] ).
cnf(462,plain,
( equal(op(e0,e1),e1)
| equal(op(e0,e0),e1)
| equal(op(e0,e3),e1)
| equal(op(e0,e2),e1) ),
inference(mrr,[status(thm)],[291,394]),
[iquote('0:MRR:291.4,394.0')] ).
cnf(465,plain,
( equal(op(e4,e3),e4)
| equal(op(e4,e3),e3)
| equal(op(e4,e3),e2)
| equal(op(e4,e3),e1) ),
inference(mrr,[status(thm)],[295,365]),
[iquote('0:MRR:295.0,365.0')] ).
cnf(466,plain,
( equal(op(e4,e2),e2)
| equal(op(e4,e2),e3)
| equal(op(e4,e2),e1) ),
inference(mrr,[status(thm)],[296,366,349]),
[iquote('0:MRR:296.0,296.4,366.0,349.0')] ).
cnf(467,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)],[297,367]),
[iquote('0:MRR:297.0,367.0')] ).
cnf(468,plain,
( equal(op(e4,e0),e4)
| equal(op(e4,e0),e3)
| equal(op(e4,e0),e2)
| equal(op(e4,e0),e1) ),
inference(mrr,[status(thm)],[298,368]),
[iquote('0:MRR:298.0,368.0')] ).
cnf(469,plain,
( equal(op(e3,e3),e3)
| equal(op(e3,e3),e4)
| equal(op(e3,e3),e2)
| equal(op(e3,e3),e0) ),
inference(mrr,[status(thm)],[300,388]),
[iquote('0:MRR:300.1,388.0')] ).
cnf(470,plain,
( equal(op(e3,e2),e3)
| equal(op(e3,e2),e2)
| equal(op(e3,e2),e0) ),
inference(mrr,[status(thm)],[301,389,350]),
[iquote('0:MRR:301.1,301.4,389.0,350.0')] ).
cnf(475,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e0)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[308,341,342]),
[iquote('0:MRR:308.3,308.4,341.0,342.0')] ).
cnf(476,plain,
( equal(op(e1,e4),e4)
| equal(op(e1,e4),e2) ),
inference(mrr,[status(thm)],[309,371,393,347]),
[iquote('0:MRR:309.0,309.1,309.3,371.0,393.0,347.0')] ).
cnf(478,plain,
( equal(op(e0,e4),e4)
| equal(op(e0,e4),e2) ),
inference(mrr,[status(thm)],[314,372,394,348]),
[iquote('0:MRR:314.0,314.1,314.3,372.0,394.0,348.0')] ).
cnf(480,plain,
( equal(e4,e0)
| skC20
| skC21
| skC22
| skC23
| skC24
| skC25
| skC26
| skC27
| skC28
| skC29
| skC30
| skC31
| skC32
| skC33
| skC34
| skC35
| skC36
| skC37
| skC38
| skC39
| skC40
| skC41
| skC42
| skC43 ),
inference(rew,[status(thm),theory(equality)],[360,319]),
[iquote('0:Rew:360.0,319.0')] ).
cnf(481,plain,
( skC40
| skC35
| skC25
| skC24
| skC23
| skC21 ),
inference(mrr,[status(thm)],[480,4,359,335,357,333,399,375,331,329,327,325,373,398,323,354,345,376,374,344]),
[iquote('0:MRR:480.0,480.1,480.3,480.7,480.8,480.9,480.10,480.11,480.12,480.13,480.14,480.15,480.17,480.18,480.19,480.20,480.22,480.23,480.24,4.0,359.0,335.0,357.0,333.0,399.0,375.0,331.0,329.0,327.0,325.0,373.0,398.0,323.0,354.0,345.0,376.0,374.0,344.0')] ).
cnf(482,plain,
equal(e0,unit),
inference(spt,[spt(split,[position(s1)])],[243]),
[iquote('1:Spt:243.4')] ).
cnf(486,plain,
( ~ skC24
| equal(op(unit,unit),e4) ),
inference(rew,[status(thm),theory(equality)],[482,29]),
[iquote('1:Rew:482.0,29.1')] ).
cnf(487,plain,
( ~ skC40
| equal(op(unit,unit),e4) ),
inference(rew,[status(thm),theory(equality)],[482,59]),
[iquote('1:Rew:482.0,59.1')] ).
cnf(490,plain,
( ~ skC23
| equal(op(unit,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[482,27]),
[iquote('1:Rew:482.0,27.1')] ).
cnf(491,plain,
( ~ skC35
| equal(op(unit,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[482,50]),
[iquote('1:Rew:482.0,50.1')] ).
cnf(494,plain,
( ~ skC21
| equal(op(unit,unit),e1) ),
inference(rew,[status(thm),theory(equality)],[482,23]),
[iquote('1:Rew:482.0,23.1')] ).
cnf(500,plain,
( equal(op(e3,e3),e3)
| equal(op(e3,e3),e4)
| equal(op(e3,e3),e2)
| equal(op(e3,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[482,469]),
[iquote('1:Rew:482.0,469.3')] ).
cnf(507,plain,
( ~ skC25
| equal(op(e1,e1),unit) ),
inference(rew,[status(thm),theory(equality)],[482,31]),
[iquote('1:Rew:482.0,31.1')] ).
cnf(514,plain,
~ equal(op(e4,e3),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[482,183]),
[iquote('1:Rew:482.0,183.0')] ).
cnf(524,plain,
~ equal(op(e3,e3),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[482,173]),
[iquote('1:Rew:482.0,173.0')] ).
cnf(525,plain,
~ equal(op(e3,e2),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[482,172]),
[iquote('1:Rew:482.0,172.0')] ).
cnf(531,plain,
( equal(op(e2,e1),e1)
| equal(op(e2,e3),e1)
| equal(op(e2,unit),e1) ),
inference(rew,[status(thm),theory(equality)],[482,444]),
[iquote('1:Rew:482.0,444.2')] ).
cnf(546,plain,
~ equal(op(e1,e3),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[482,153]),
[iquote('1:Rew:482.0,153.0')] ).
cnf(559,plain,
~ equal(op(e4,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[482,124]),
[iquote('1:Rew:482.0,124.0')] ).
cnf(562,plain,
~ equal(op(e1,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[482,121]),
[iquote('1:Rew:482.0,121.0')] ).
cnf(570,plain,
~ equal(op(e1,e4),op(unit,e4)),
inference(rew,[status(thm),theory(equality)],[482,131]),
[iquote('1:Rew:482.0,131.0')] ).
cnf(580,plain,
~ equal(op(e3,e2),op(unit,e2)),
inference(rew,[status(thm),theory(equality)],[482,113]),
[iquote('1:Rew:482.0,113.0')] ).
cnf(593,plain,
~ equal(op(e2,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[482,102]),
[iquote('1:Rew:482.0,102.0')] ).
cnf(598,plain,
( equal(op(e1,e3),e3)
| equal(op(e1,e3),e1)
| equal(op(e1,e3),e4)
| equal(op(e1,e3),e2)
| equal(op(e1,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[482,310]),
[iquote('1:Rew:482.0,310.4')] ).
cnf(603,plain,
( equal(op(e3,e2),e3)
| equal(op(e3,e2),e2)
| equal(op(e3,e2),unit) ),
inference(rew,[status(thm),theory(equality)],[482,470]),
[iquote('1:Rew:482.0,470.2')] ).
cnf(607,plain,
~ equal(e4,unit),
inference(rew,[status(thm),theory(equality)],[482,4]),
[iquote('1:Rew:482.0,4.0')] ).
cnf(608,plain,
~ equal(e3,unit),
inference(rew,[status(thm),theory(equality)],[482,3]),
[iquote('1:Rew:482.0,3.0')] ).
cnf(610,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[482,1]),
[iquote('1:Rew:482.0,1.0')] ).
cnf(611,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[482,12]),
[iquote('1:Rew:482.0,12.0')] ).
cnf(644,plain,
( ~ skC24
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[611,486]),
[iquote('1:Rew:611.0,486.1')] ).
cnf(645,plain,
~ skC24,
inference(mrr,[status(thm)],[644,607]),
[iquote('1:MRR:644.1,607.0')] ).
cnf(646,plain,
( skC40
| skC35
| skC25
| skC23
| skC21 ),
inference(mrr,[status(thm)],[481,645]),
[iquote('1:MRR:481.3,645.0')] ).
cnf(647,plain,
( ~ skC40
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[611,487]),
[iquote('1:Rew:611.0,487.1')] ).
cnf(648,plain,
~ skC40,
inference(mrr,[status(thm)],[647,607]),
[iquote('1:MRR:647.1,607.0')] ).
cnf(649,plain,
( skC35
| skC25
| skC23
| skC21 ),
inference(mrr,[status(thm)],[646,648]),
[iquote('1:MRR:646.0,648.0')] ).
cnf(650,plain,
( ~ skC23
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[611,490]),
[iquote('1:Rew:611.0,490.1')] ).
cnf(651,plain,
~ skC23,
inference(mrr,[status(thm)],[650,608]),
[iquote('1:MRR:650.1,608.0')] ).
cnf(652,plain,
( skC35
| skC25
| skC21 ),
inference(mrr,[status(thm)],[649,651]),
[iquote('1:MRR:649.2,651.0')] ).
cnf(653,plain,
( ~ skC35
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[611,491]),
[iquote('1:Rew:611.0,491.1')] ).
cnf(654,plain,
~ skC35,
inference(mrr,[status(thm)],[653,608]),
[iquote('1:MRR:653.1,608.0')] ).
cnf(655,plain,
( skC25
| skC21 ),
inference(mrr,[status(thm)],[652,654]),
[iquote('1:MRR:652.0,654.0')] ).
cnf(656,plain,
( ~ skC21
| equal(e1,unit) ),
inference(rew,[status(thm),theory(equality)],[611,494]),
[iquote('1:Rew:611.0,494.1')] ).
cnf(657,plain,
~ skC21,
inference(mrr,[status(thm)],[656,610]),
[iquote('1:MRR:656.1,610.0')] ).
cnf(658,plain,
skC25,
inference(mrr,[status(thm)],[655,657]),
[iquote('1:MRR:655.1,657.0')] ).
cnf(661,plain,
equal(op(e1,e1),unit),
inference(mrr,[status(thm)],[507,658]),
[iquote('1:MRR:507.0,658.0')] ).
cnf(663,plain,
~ equal(op(e1,e3),unit),
inference(rew,[status(thm),theory(equality)],[661,156]),
[iquote('1:Rew:661.0,156.0')] ).
cnf(668,plain,
~ equal(op(e4,e3),e4),
inference(rew,[status(thm),theory(equality)],[20,514]),
[iquote('1:Rew:20.0,514.0')] ).
cnf(669,plain,
( equal(op(e4,e3),e3)
| equal(op(e4,e3),e2)
| equal(op(e4,e3),e1) ),
inference(mrr,[status(thm)],[465,668]),
[iquote('1:MRR:465.0,668.0')] ).
cnf(674,plain,
~ equal(op(e3,e3),e3),
inference(rew,[status(thm),theory(equality)],[18,524]),
[iquote('1:Rew:18.0,524.0')] ).
cnf(675,plain,
~ equal(op(e3,e2),e3),
inference(rew,[status(thm),theory(equality)],[18,525]),
[iquote('1:Rew:18.0,525.0')] ).
cnf(688,plain,
~ equal(op(e1,e3),e1),
inference(rew,[status(thm),theory(equality)],[14,546]),
[iquote('1:Rew:14.0,546.0')] ).
cnf(696,plain,
~ equal(op(e4,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,559]),
[iquote('1:Rew:17.0,559.0')] ).
cnf(699,plain,
~ equal(op(e1,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,562]),
[iquote('1:Rew:17.0,562.0')] ).
cnf(702,plain,
~ equal(op(e1,e4),e4),
inference(rew,[status(thm),theory(equality)],[19,570]),
[iquote('1:Rew:19.0,570.0')] ).
cnf(703,plain,
equal(op(e1,e4),e2),
inference(mrr,[status(thm)],[476,702]),
[iquote('1:MRR:476.0,702.0')] ).
cnf(706,plain,
~ equal(op(e1,e3),e2),
inference(rew,[status(thm),theory(equality)],[703,160]),
[iquote('1:Rew:703.0,160.0')] ).
cnf(717,plain,
~ equal(op(e3,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,580]),
[iquote('1:Rew:15.0,580.0')] ).
cnf(725,plain,
~ equal(op(e2,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,593]),
[iquote('1:Rew:13.0,593.0')] ).
cnf(758,plain,
( equal(op(e2,e1),e1)
| equal(op(e2,e3),e1)
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[16,531]),
[iquote('1:Rew:16.0,531.2')] ).
cnf(759,plain,
equal(op(e2,e3),e1),
inference(mrr,[status(thm)],[758,725,5]),
[iquote('1:MRR:758.0,758.2,725.0,5.0')] ).
cnf(763,plain,
~ equal(op(e4,e3),e1),
inference(rew,[status(thm),theory(equality)],[759,129]),
[iquote('1:Rew:759.0,129.0')] ).
cnf(783,plain,
equal(op(e3,e2),unit),
inference(mrr,[status(thm)],[603,675,717]),
[iquote('1:MRR:603.0,603.1,675.0,717.0')] ).
cnf(786,plain,
~ equal(op(e3,e3),unit),
inference(rew,[status(thm),theory(equality)],[783,178]),
[iquote('1:Rew:783.0,178.0')] ).
cnf(799,plain,
equal(op(e4,e3),e2),
inference(mrr,[status(thm)],[669,696,763]),
[iquote('1:MRR:669.0,669.2,696.0,763.0')] ).
cnf(801,plain,
~ equal(op(e3,e3),e2),
inference(rew,[status(thm),theory(equality)],[799,130]),
[iquote('1:Rew:799.0,130.0')] ).
cnf(830,plain,
equal(op(e3,e3),e4),
inference(mrr,[status(thm)],[500,674,801,786]),
[iquote('1:MRR:500.0,500.2,500.3,674.0,801.0,786.0')] ).
cnf(833,plain,
~ equal(op(e1,e3),e4),
inference(rew,[status(thm),theory(equality)],[830,126]),
[iquote('1:Rew:830.0,126.0')] ).
cnf(869,plain,
$false,
inference(mrr,[status(thm)],[598,699,688,833,706,663]),
[iquote('1:MRR:598.0,598.1,598.2,598.3,598.4,699.0,688.0,833.0,706.0,663.0')] ).
cnf(870,plain,
~ equal(e0,unit),
inference(spt,[spt(split,[position(sa)])],[869,482]),
[iquote('1:Spt:869.0,243.4,482.0')] ).
cnf(871,plain,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2)])],[243]),
[iquote('1:Spt:869.0,243.0,243.1,243.2,243.3')] ).
cnf(872,plain,
equal(e4,unit),
inference(spt,[spt(split,[position(s2s1)])],[871]),
[iquote('2:Spt:871.0')] ).
cnf(898,plain,
~ equal(op(e1,e0),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[872,154]),
[iquote('2:Rew:872.0,154.0')] ).
cnf(900,plain,
~ equal(op(e1,e2),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[872,159]),
[iquote('2:Rew:872.0,159.0')] ).
cnf(901,plain,
~ equal(op(e1,e3),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[872,160]),
[iquote('2:Rew:872.0,160.0')] ).
cnf(913,plain,
( equal(op(e1,e0),e1)
| equal(op(e0,e0),e1)
| equal(op(unit,e0),e1)
| equal(op(e2,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[872,461]),
[iquote('2:Rew:872.0,461.2')] ).
cnf(934,plain,
( equal(op(e1,e2),e1)
| equal(op(unit,e2),e1)
| equal(op(e0,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[872,442]),
[iquote('2:Rew:872.0,442.1')] ).
cnf(949,plain,
( equal(op(e1,e3),e1)
| equal(op(unit,e3),e1)
| equal(op(e2,e3),e1)
| equal(op(e0,e3),e1) ),
inference(rew,[status(thm),theory(equality)],[872,431]),
[iquote('2:Rew:872.0,431.1')] ).
cnf(1026,plain,
~ equal(op(e1,e0),e1),
inference(rew,[status(thm),theory(equality)],[14,898]),
[iquote('2:Rew:14.0,898.0')] ).
cnf(1029,plain,
~ equal(op(e1,e2),e1),
inference(rew,[status(thm),theory(equality)],[14,900]),
[iquote('2:Rew:14.0,900.0')] ).
cnf(1031,plain,
~ equal(op(e1,e3),e1),
inference(rew,[status(thm),theory(equality)],[14,901]),
[iquote('2:Rew:14.0,901.0')] ).
cnf(1091,plain,
( equal(op(e1,e2),e1)
| equal(e2,e1)
| equal(op(e0,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[15,934]),
[iquote('2:Rew:15.0,934.1')] ).
cnf(1092,plain,
equal(op(e0,e2),e1),
inference(mrr,[status(thm)],[1091,1029,5]),
[iquote('2:MRR:1091.0,1091.1,1029.0,5.0')] ).
cnf(1096,plain,
~ equal(op(e0,e0),e1),
inference(rew,[status(thm),theory(equality)],[1092,142]),
[iquote('2:Rew:1092.0,142.0')] ).
cnf(1097,plain,
~ equal(op(e0,e3),e1),
inference(rew,[status(thm),theory(equality)],[1092,148]),
[iquote('2:Rew:1092.0,148.0')] ).
cnf(1123,plain,
( equal(op(e1,e0),e1)
| equal(op(e0,e0),e1)
| equal(e1,e0)
| equal(op(e2,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[11,913]),
[iquote('2:Rew:11.0,913.2')] ).
cnf(1124,plain,
equal(op(e2,e0),e1),
inference(mrr,[status(thm)],[1123,1026,1096,1]),
[iquote('2:MRR:1123.0,1123.1,1123.2,1026.0,1096.0,1.0')] ).
cnf(1130,plain,
~ equal(op(e2,e3),e1),
inference(rew,[status(thm),theory(equality)],[1124,163]),
[iquote('2:Rew:1124.0,163.0')] ).
cnf(1145,plain,
( equal(op(e1,e3),e1)
| equal(e3,e1)
| equal(op(e2,e3),e1)
| equal(op(e0,e3),e1) ),
inference(rew,[status(thm),theory(equality)],[17,949]),
[iquote('2:Rew:17.0,949.1')] ).
cnf(1146,plain,
$false,
inference(mrr,[status(thm)],[1145,1031,6,1130,1097]),
[iquote('2:MRR:1145.0,1145.1,1145.2,1145.3,1031.0,6.0,1130.0,1097.0')] ).
cnf(1175,plain,
~ equal(e4,unit),
inference(spt,[spt(split,[position(s2sa)])],[1146,872]),
[iquote('2:Spt:1146.0,871.0,872.0')] ).
cnf(1176,plain,
( equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2s2)])],[871]),
[iquote('2:Spt:1146.0,871.1,871.2,871.3')] ).
cnf(1177,plain,
equal(e3,unit),
inference(spt,[spt(split,[position(s2s2s1)])],[1176]),
[iquote('3:Spt:1176.0')] ).
cnf(1203,plain,
~ equal(op(e2,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1177,98]),
[iquote('3:Rew:1177.0,98.0')] ).
cnf(1214,plain,
~ equal(op(e2,e0),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[1177,163]),
[iquote('3:Rew:1177.0,163.0')] ).
cnf(1224,plain,
~ equal(op(e4,e2),op(unit,e2)),
inference(rew,[status(thm),theory(equality)],[1177,120]),
[iquote('3:Rew:1177.0,120.0')] ).
cnf(1238,plain,
~ equal(op(e0,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[1177,103]),
[iquote('3:Rew:1177.0,103.0')] ).
cnf(1247,plain,
~ equal(op(e4,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[1177,110]),
[iquote('3:Rew:1177.0,110.0')] ).
cnf(1265,plain,
( equal(op(e0,e1),e1)
| equal(op(e0,e0),e1)
| equal(op(e0,unit),e1)
| equal(op(e0,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[1177,462]),
[iquote('3:Rew:1177.0,462.2')] ).
cnf(1287,plain,
~ equal(op(e4,e1),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1177,186]),
[iquote('3:Rew:1177.0,186.0')] ).
cnf(1292,plain,
~ equal(op(e4,e0),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1177,183]),
[iquote('3:Rew:1177.0,183.0')] ).
cnf(1299,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)],[1177,467]),
[iquote('3:Rew:1177.0,467.2')] ).
cnf(1306,plain,
( equal(op(e4,e2),e2)
| equal(op(e4,e2),unit)
| equal(op(e4,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[1177,466]),
[iquote('3:Rew:1177.0,466.1')] ).
cnf(1314,plain,
( equal(op(e4,e0),e4)
| equal(op(e4,e0),unit)
| equal(op(e4,e0),e2)
| equal(op(e4,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1177,468]),
[iquote('3:Rew:1177.0,468.1')] ).
cnf(1345,plain,
~ equal(op(e2,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1203]),
[iquote('3:Rew:11.0,1203.0')] ).
cnf(1346,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[475,1345]),
[iquote('3:MRR:475.1,1345.0')] ).
cnf(1350,plain,
~ equal(op(e2,e0),e2),
inference(rew,[status(thm),theory(equality)],[16,1214]),
[iquote('3:Rew:16.0,1214.0')] ).
cnf(1353,plain,
~ equal(op(e4,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,1224]),
[iquote('3:Rew:15.0,1224.0')] ).
cnf(1359,plain,
~ equal(op(e0,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1238]),
[iquote('3:Rew:13.0,1238.0')] ).
cnf(1366,plain,
~ equal(op(e4,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1247]),
[iquote('3:Rew:13.0,1247.0')] ).
cnf(1374,plain,
~ equal(op(e4,e1),e4),
inference(rew,[status(thm),theory(equality)],[20,1287]),
[iquote('3:Rew:20.0,1287.0')] ).
cnf(1379,plain,
~ equal(op(e4,e0),e4),
inference(rew,[status(thm),theory(equality)],[20,1292]),
[iquote('3:Rew:20.0,1292.0')] ).
cnf(1402,plain,
equal(op(e2,e0),e1),
inference(mrr,[status(thm)],[1346,1350]),
[iquote('3:MRR:1346.0,1350.0')] ).
cnf(1404,plain,
~ equal(op(e4,e0),e1),
inference(rew,[status(thm),theory(equality)],[1402,99]),
[iquote('3:Rew:1402.0,99.0')] ).
cnf(1406,plain,
~ equal(op(e0,e0),e1),
inference(rew,[status(thm),theory(equality)],[1402,92]),
[iquote('3:Rew:1402.0,92.0')] ).
cnf(1452,plain,
( equal(op(e4,e2),unit)
| equal(op(e4,e2),e1) ),
inference(mrr,[status(thm)],[1306,1353]),
[iquote('3:MRR:1306.0,1353.0')] ).
cnf(1472,plain,
( equal(op(e0,e1),e1)
| equal(op(e0,e0),e1)
| equal(e1,e0)
| equal(op(e0,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[12,1265]),
[iquote('3:Rew:12.0,1265.2')] ).
cnf(1473,plain,
equal(op(e0,e2),e1),
inference(mrr,[status(thm)],[1472,1359,1406,1]),
[iquote('3:MRR:1472.0,1472.1,1472.2,1359.0,1406.0,1.0')] ).
cnf(1475,plain,
~ equal(op(e4,e2),e1),
inference(rew,[status(thm),theory(equality)],[1473,114]),
[iquote('3:Rew:1473.0,114.0')] ).
cnf(1484,plain,
equal(op(e4,e2),unit),
inference(mrr,[status(thm)],[1452,1475]),
[iquote('3:MRR:1452.1,1475.0')] ).
cnf(1487,plain,
~ equal(op(e4,e1),unit),
inference(rew,[status(thm),theory(equality)],[1484,185]),
[iquote('3:Rew:1484.0,185.0')] ).
cnf(1488,plain,
~ equal(op(e4,e0),unit),
inference(rew,[status(thm),theory(equality)],[1484,182]),
[iquote('3:Rew:1484.0,182.0')] ).
cnf(1507,plain,
equal(op(e4,e1),e2),
inference(mrr,[status(thm)],[1299,1374,1366,1487]),
[iquote('3:MRR:1299.0,1299.1,1299.2,1374.0,1366.0,1487.0')] ).
cnf(1510,plain,
~ equal(op(e4,e0),e2),
inference(rew,[status(thm),theory(equality)],[1507,181]),
[iquote('3:Rew:1507.0,181.0')] ).
cnf(1526,plain,
$false,
inference(mrr,[status(thm)],[1314,1379,1488,1510,1404]),
[iquote('3:MRR:1314.0,1314.1,1314.2,1314.3,1379.0,1488.0,1510.0,1404.0')] ).
cnf(1539,plain,
~ equal(e3,unit),
inference(spt,[spt(split,[position(s2s2sa)])],[1526,1177]),
[iquote('3:Spt:1526.0,1176.0,1177.0')] ).
cnf(1540,plain,
( equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2s2s2)])],[1176]),
[iquote('3:Spt:1526.0,1176.1,1176.2')] ).
cnf(1541,plain,
equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2s1)])],[1540]),
[iquote('4:Spt:1540.0')] ).
cnf(1542,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[1541,5]),
[iquote('4:Rew:1541.0,5.0')] ).
cnf(1648,plain,
( equal(op(e4,unit),unit)
| equal(op(e3,e2),e2)
| equal(op(e1,e2),e2)
| equal(op(e0,e2),e2) ),
inference(rew,[status(thm),theory(equality)],[1541,438]),
[iquote('4:Rew:1541.0,438.0')] ).
cnf(1786,plain,
( equal(e4,unit)
| equal(e3,unit)
| equal(e1,unit)
| equal(e0,unit) ),
inference(rew,[status(thm),theory(equality)],[12,1648,1541,14,18,20]),
[iquote('4:Rew:12.0,1648.3,1541.0,1648.3,14.0,1648.2,1541.0,1648.2,18.0,1648.1,1541.0,1648.1,20.0,1648.0')] ).
cnf(1787,plain,
$false,
inference(mrr,[status(thm)],[1786,1175,1539,1542,870]),
[iquote('4:MRR:1786.0,1786.1,1786.2,1786.3,1175.0,1539.0,1542.0,870.0')] ).
cnf(1811,plain,
~ equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2sa)])],[1787,1541]),
[iquote('4:Spt:1787.0,1540.0,1541.0')] ).
cnf(1812,plain,
equal(e1,unit),
inference(spt,[spt(split,[position(s2s2s2s2)])],[1540]),
[iquote('4:Spt:1787.0,1540.1')] ).
cnf(1829,plain,
( ~ skC1
| ~ equal(op(unit,op(unit,e0)),e0) ),
inference(rew,[status(thm),theory(equality)],[1812,213]),
[iquote('4:Rew:1812.0,213.1')] ).
cnf(1834,plain,
~ equal(op(e0,e4),op(unit,e4)),
inference(rew,[status(thm),theory(equality)],[1812,131]),
[iquote('4:Rew:1812.0,131.0')] ).
cnf(1839,plain,
( ~ skC17
| equal(op(e4,op(unit,e4)),unit) ),
inference(rew,[status(thm),theory(equality)],[1812,208]),
[iquote('4:Rew:1812.0,208.1')] ).
cnf(1847,plain,
~ equal(op(e3,e0),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[1812,171]),
[iquote('4:Rew:1812.0,171.0')] ).
cnf(1850,plain,
~ equal(op(e3,e3),unit),
inference(rew,[status(thm),theory(equality)],[1812,388]),
[iquote('4:Rew:1812.0,388.0')] ).
cnf(1853,plain,
( ~ skC19
| equal(op(e4,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[1812,396]),
[iquote('4:Rew:1812.0,396.1')] ).
cnf(1868,plain,
( ~ skC13
| equal(op(e3,op(unit,e3)),unit) ),
inference(rew,[status(thm),theory(equality)],[1812,204]),
[iquote('4:Rew:1812.0,204.1')] ).
cnf(1873,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[1812,5]),
[iquote('4:Rew:1812.0,5.0')] ).
cnf(1889,plain,
( ~ skC19
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[20,1853]),
[iquote('4:Rew:20.0,1853.1')] ).
cnf(1890,plain,
~ skC19,
inference(mrr,[status(thm)],[1889,10]),
[iquote('4:MRR:1889.1,10.0')] ).
cnf(1891,plain,
( skC18
| skC17
| skC16 ),
inference(mrr,[status(thm)],[406,1890]),
[iquote('4:MRR:406.0,1890.0')] ).
cnf(1894,plain,
~ equal(op(e0,e2),e0),
inference(rew,[status(thm),theory(equality)],[12,145,1812]),
[iquote('4:Rew:12.0,145.0,1812.0,145.0')] ).
cnf(1909,plain,
~ equal(op(e2,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,95,1812]),
[iquote('4:Rew:11.0,95.0,1812.0,95.0')] ).
cnf(1920,plain,
~ equal(op(e0,e4),e4),
inference(rew,[status(thm),theory(equality)],[19,1834]),
[iquote('4:Rew:19.0,1834.0')] ).
cnf(1923,plain,
~ equal(op(e3,e0),e3),
inference(rew,[status(thm),theory(equality)],[18,1847]),
[iquote('4:Rew:18.0,1847.0')] ).
cnf(1940,plain,
( ~ skC17
| equal(e0,unit) ),
inference(rew,[status(thm),theory(equality)],[360,1839,19]),
[iquote('4:Rew:360.0,1839.1,19.0,1839.1')] ).
cnf(1941,plain,
~ skC17,
inference(mrr,[status(thm)],[1940,870]),
[iquote('4:MRR:1940.1,870.0')] ).
cnf(1942,plain,
( skC18
| skC16 ),
inference(mrr,[status(thm)],[1891,1941]),
[iquote('4:MRR:1891.1,1941.0')] ).
cnf(1944,plain,
( ~ skC13
| equal(op(e3,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[17,1868]),
[iquote('4:Rew:17.0,1868.1')] ).
cnf(1945,plain,
~ skC13,
inference(mrr,[status(thm)],[1944,1850]),
[iquote('4:MRR:1944.1,1850.0')] ).
cnf(1949,plain,
equal(op(e0,e4),e2),
inference(mrr,[status(thm)],[478,1920]),
[iquote('4:MRR:478.0,1920.0')] ).
cnf(1952,plain,
( ~ skC16
| equal(op(e4,e2),e0) ),
inference(rew,[status(thm),theory(equality)],[1949,207]),
[iquote('4:Rew:1949.0,207.1')] ).
cnf(1959,plain,
~ skC16,
inference(mrr,[status(thm)],[1952,366]),
[iquote('4:MRR:1952.1,366.0')] ).
cnf(1960,plain,
skC18,
inference(mrr,[status(thm)],[1942,1959]),
[iquote('4:MRR:1942.1,1959.0')] ).
cnf(1961,plain,
equal(op(e4,e3),e2),
inference(mrr,[status(thm)],[377,1960]),
[iquote('4:MRR:377.0,1960.0')] ).
cnf(1971,plain,
( skC14
| skC13
| skC12
| equal(op(e3,e2),e4) ),
inference(rew,[status(thm),theory(equality)],[1961,401]),
[iquote('4:Rew:1961.0,401.3')] ).
cnf(1972,plain,
( skC14
| skC12 ),
inference(mrr,[status(thm)],[1971,1945,350]),
[iquote('4:MRR:1971.1,1971.3,1945.0,350.0')] ).
cnf(1974,plain,
( ~ skC1
| ~ equal(e0,e0) ),
inference(rew,[status(thm),theory(equality)],[11,1829]),
[iquote('4:Rew:11.0,1829.1,11.0,1829.1')] ).
cnf(1975,plain,
~ skC1,
inference(obv,[status(thm),theory(equality)],[1974]),
[iquote('4:Obv:1974.1')] ).
cnf(1976,plain,
( skC3
| skC2
| equal(op(e0,op(e4,e0)),e4) ),
inference(mrr,[status(thm)],[404,1975]),
[iquote('4:MRR:404.2,1975.0')] ).
cnf(1985,plain,
( equal(e2,unit)
| equal(op(e4,e2),unit)
| equal(op(e0,e2),unit) ),
inference(rew,[status(thm),theory(equality)],[1812,442,15]),
[iquote('4:Rew:1812.0,442.2,1812.0,442.1,15.0,442.0,1812.0,442.0')] ).
cnf(1986,plain,
( equal(op(e4,e2),unit)
| equal(op(e0,e2),unit) ),
inference(mrr,[status(thm)],[1985,1873]),
[iquote('4:MRR:1985.0,1873.0')] ).
cnf(1990,plain,
( equal(op(e0,e2),e0)
| equal(op(e3,e2),e0)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[15,446,1812]),
[iquote('4:Rew:15.0,446.2,1812.0,446.2')] ).
cnf(1991,plain,
equal(op(e3,e2),e0),
inference(mrr,[status(thm)],[1990,1894,2]),
[iquote('4:MRR:1990.0,1990.2,1894.0,2.0')] ).
cnf(2009,plain,
( equal(op(e2,e0),e0)
| equal(op(e2,e3),e0)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[16,448,1812]),
[iquote('4:Rew:16.0,448.2,1812.0,448.2')] ).
cnf(2010,plain,
equal(op(e2,e3),e0),
inference(mrr,[status(thm)],[2009,1909,2]),
[iquote('4:MRR:2009.0,2009.2,1909.0,2.0')] ).
cnf(2017,plain,
( ~ skC14
| equal(op(e3,e0),e2) ),
inference(rew,[status(thm),theory(equality)],[2010,205]),
[iquote('4:Rew:2010.0,205.1')] ).
cnf(2019,plain,
( equal(e2,unit)
| equal(e0,unit)
| equal(op(e2,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[1812,444,2010,16]),
[iquote('4:Rew:1812.0,444.2,2010.0,444.1,1812.0,444.1,16.0,444.0,1812.0,444.0')] ).
cnf(2020,plain,
equal(op(e2,e0),unit),
inference(mrr,[status(thm)],[2019,1873,870]),
[iquote('4:MRR:2019.0,2019.1,1873.0,870.0')] ).
cnf(2028,plain,
( ~ skC2
| equal(op(e0,unit),e2) ),
inference(rew,[status(thm),theory(equality)],[2020,193]),
[iquote('4:Rew:2020.0,193.1')] ).
cnf(2030,plain,
( ~ skC2
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[12,2028]),
[iquote('4:Rew:12.0,2028.1')] ).
cnf(2031,plain,
~ skC2,
inference(mrr,[status(thm)],[2030,2]),
[iquote('4:MRR:2030.1,2.0')] ).
cnf(2032,plain,
( skC3
| equal(op(e0,op(e4,e0)),e4) ),
inference(mrr,[status(thm)],[1976,2031]),
[iquote('4:MRR:1976.1,2031.0')] ).
cnf(2043,plain,
( equal(op(e3,e0),e3)
| equal(op(e0,e0),e3)
| equal(op(e4,e0),e3)
| equal(e3,e0) ),
inference(rew,[status(thm),theory(equality)],[11,459,1812]),
[iquote('4:Rew:11.0,459.3,1812.0,459.3')] ).
cnf(2044,plain,
( equal(op(e0,e0),e3)
| equal(op(e4,e0),e3) ),
inference(mrr,[status(thm)],[2043,1923,3]),
[iquote('4:MRR:2043.0,2043.3,1923.0,3.0')] ).
cnf(2049,plain,
( equal(e3,e0)
| equal(op(e4,e2),e3)
| equal(e3,e2)
| equal(op(e0,e2),e3) ),
inference(rew,[status(thm),theory(equality)],[15,436,1812,1991]),
[iquote('4:Rew:15.0,436.2,1812.0,436.2,1991.0,436.0')] ).
cnf(2050,plain,
( equal(op(e4,e2),e3)
| equal(op(e0,e2),e3) ),
inference(mrr,[status(thm)],[2049,3,8]),
[iquote('4:MRR:2049.0,2049.2,3.0,8.0')] ).
cnf(2052,plain,
( equal(e3,unit)
| equal(e2,unit)
| equal(e0,unit)
| equal(op(e0,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[1812,431,2010,1961,17]),
[iquote('4:Rew:1812.0,431.3,2010.0,431.2,1812.0,431.2,1961.0,431.1,1812.0,431.1,17.0,431.0,1812.0,431.0')] ).
cnf(2053,plain,
equal(op(e0,e3),unit),
inference(mrr,[status(thm)],[2052,1539,1873,870]),
[iquote('4:MRR:2052.0,2052.1,2052.2,1539.0,1873.0,870.0')] ).
cnf(2056,plain,
( ~ skC12
| equal(op(e3,unit),e0) ),
inference(rew,[status(thm),theory(equality)],[2053,203]),
[iquote('4:Rew:2053.0,203.1')] ).
cnf(2058,plain,
~ equal(op(e0,e2),unit),
inference(rew,[status(thm),theory(equality)],[2053,148]),
[iquote('4:Rew:2053.0,148.0')] ).
cnf(2063,plain,
equal(op(e4,e2),unit),
inference(mrr,[status(thm)],[1986,2058]),
[iquote('4:MRR:1986.1,2058.0')] ).
cnf(2069,plain,
( equal(e3,unit)
| equal(op(e0,e2),e3) ),
inference(rew,[status(thm),theory(equality)],[2063,2050]),
[iquote('4:Rew:2063.0,2050.0')] ).
cnf(2076,plain,
( ~ skC12
| equal(e3,e0) ),
inference(rew,[status(thm),theory(equality)],[18,2056]),
[iquote('4:Rew:18.0,2056.1')] ).
cnf(2077,plain,
~ skC12,
inference(mrr,[status(thm)],[2076,3]),
[iquote('4:MRR:2076.1,3.0')] ).
cnf(2078,plain,
skC14,
inference(mrr,[status(thm)],[1972,2077]),
[iquote('4:MRR:1972.1,2077.0')] ).
cnf(2079,plain,
equal(op(e3,e0),e2),
inference(mrr,[status(thm)],[2017,2078]),
[iquote('4:MRR:2017.0,2078.0')] ).
cnf(2084,plain,
( ~ skC3
| ~ equal(op(e3,e2),e0) ),
inference(rew,[status(thm),theory(equality)],[2079,215]),
[iquote('4:Rew:2079.0,215.1')] ).
cnf(2095,plain,
equal(op(e0,e2),e3),
inference(mrr,[status(thm)],[2069,1539]),
[iquote('4:MRR:2069.0,1539.0')] ).
cnf(2097,plain,
~ equal(op(e0,e0),e3),
inference(rew,[status(thm),theory(equality)],[2095,142]),
[iquote('4:Rew:2095.0,142.0')] ).
cnf(2102,plain,
equal(op(e4,e0),e3),
inference(mrr,[status(thm)],[2044,2097]),
[iquote('4:MRR:2044.0,2097.0')] ).
cnf(2108,plain,
( skC3
| equal(op(e0,e3),e4) ),
inference(rew,[status(thm),theory(equality)],[2102,2032]),
[iquote('4:Rew:2102.0,2032.1')] ).
cnf(2110,plain,
( skC3
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[2053,2108]),
[iquote('4:Rew:2053.0,2108.1')] ).
cnf(2111,plain,
skC3,
inference(mrr,[status(thm)],[2110,1175]),
[iquote('4:MRR:2110.1,1175.0')] ).
cnf(2113,plain,
( ~ skC3
| ~ equal(e0,e0) ),
inference(rew,[status(thm),theory(equality)],[1991,2084]),
[iquote('4:Rew:1991.0,2084.1')] ).
cnf(2114,plain,
~ skC3,
inference(obv,[status(thm),theory(equality)],[2113]),
[iquote('4:Obv:2113.1')] ).
cnf(2115,plain,
$false,
inference(mrr,[status(thm)],[2114,2111]),
[iquote('4:MRR:2114.0,2111.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : ALG056+1 : TPTP v8.1.0. Released v2.7.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n027.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 08:39:26 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.43/0.61
% 0.43/0.61 SPASS V 3.9
% 0.43/0.61 SPASS beiseite: Proof found.
% 0.43/0.61 % SZS status Theorem
% 0.43/0.61 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.43/0.61 SPASS derived 970 clauses, backtracked 721 clauses, performed 4 splits and kept 1429 clauses.
% 0.43/0.61 SPASS allocated 86249 KBytes.
% 0.43/0.61 SPASS spent 0:00:00.27 on the problem.
% 0.43/0.61 0:00:00.04 for the input.
% 0.43/0.61 0:00:00.07 for the FLOTTER CNF translation.
% 0.43/0.61 0:00:00.00 for inferences.
% 0.43/0.61 0:00:00.00 for the backtracking.
% 0.43/0.61 0:00:00.13 for the reduction.
% 0.43/0.61
% 0.43/0.61
% 0.43/0.61 Here is a proof with depth 4, length 429 :
% 0.43/0.61 % SZS output start Refutation
% See solution above
% 0.45/0.62 Formulae used in the proof : ax5 ax2 ax6 co1 ax4 ax3 ax1
% 0.45/0.62
%------------------------------------------------------------------------------