%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG064+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n022.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:11 EDT 2022
% Result : Theorem 0.37s 0.57s
% Output : Refutation 0.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 129
% Syntax : Number of clauses : 421 ( 235 unt; 113 nHn; 421 RR)
% Number of literals : 945 ( 0 equ; 290 neg)
% Maximal clause size : 25 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 25 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('ALG064+1.p',unknown),
[] ).
cnf(2,axiom,
~ equal(e2,e0),
file('ALG064+1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(e3,e0),
file('ALG064+1.p',unknown),
[] ).
cnf(4,axiom,
~ equal(e4,e0),
file('ALG064+1.p',unknown),
[] ).
cnf(5,axiom,
~ equal(e2,e1),
file('ALG064+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e3,e1),
file('ALG064+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(e4,e1),
file('ALG064+1.p',unknown),
[] ).
cnf(8,axiom,
~ equal(e3,e2),
file('ALG064+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(e4,e2),
file('ALG064+1.p',unknown),
[] ).
cnf(10,axiom,
~ equal(e4,e3),
file('ALG064+1.p',unknown),
[] ).
cnf(11,axiom,
equal(op(unit,e0),e0),
file('ALG064+1.p',unknown),
[] ).
cnf(12,axiom,
equal(op(e0,unit),e0),
file('ALG064+1.p',unknown),
[] ).
cnf(13,axiom,
equal(op(unit,e1),e1),
file('ALG064+1.p',unknown),
[] ).
cnf(14,axiom,
equal(op(e1,unit),e1),
file('ALG064+1.p',unknown),
[] ).
cnf(15,axiom,
equal(op(unit,e2),e2),
file('ALG064+1.p',unknown),
[] ).
cnf(16,axiom,
equal(op(e2,unit),e2),
file('ALG064+1.p',unknown),
[] ).
cnf(17,axiom,
equal(op(unit,e3),e3),
file('ALG064+1.p',unknown),
[] ).
cnf(18,axiom,
equal(op(e3,unit),e3),
file('ALG064+1.p',unknown),
[] ).
cnf(19,axiom,
equal(op(unit,e4),e4),
file('ALG064+1.p',unknown),
[] ).
cnf(20,axiom,
equal(op(e4,unit),e4),
file('ALG064+1.p',unknown),
[] ).
cnf(21,axiom,
equal(op(e1,e1),e4),
file('ALG064+1.p',unknown),
[] ).
cnf(22,axiom,
~ equal(op(e1,e0),op(e0,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(23,axiom,
~ equal(op(e2,e0),op(e0,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(26,axiom,
~ equal(op(e2,e0),op(e1,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(28,axiom,
~ equal(op(e4,e0),op(e1,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(30,axiom,
~ equal(op(e4,e0),op(e2,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(33,axiom,
~ equal(op(e2,e1),op(e0,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(36,axiom,
~ equal(op(e2,e1),op(e1,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(44,axiom,
~ equal(op(e3,e2),op(e0,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(45,axiom,
~ equal(op(e4,e2),op(e0,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(47,axiom,
~ equal(op(e3,e2),op(e1,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(48,axiom,
~ equal(op(e4,e2),op(e1,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(49,axiom,
~ equal(op(e3,e2),op(e2,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(50,axiom,
~ equal(op(e4,e2),op(e2,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(51,axiom,
~ equal(op(e4,e2),op(e3,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(54,axiom,
~ equal(op(e3,e3),op(e0,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(55,axiom,
~ equal(op(e4,e3),op(e0,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(56,axiom,
~ equal(op(e2,e3),op(e1,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(59,axiom,
~ equal(op(e3,e3),op(e2,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(60,axiom,
~ equal(op(e4,e3),op(e2,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(61,axiom,
~ equal(op(e4,e3),op(e3,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(62,axiom,
~ equal(op(e1,e4),op(e0,e4)),
file('ALG064+1.p',unknown),
[] ).
cnf(63,axiom,
~ equal(op(e2,e4),op(e0,e4)),
file('ALG064+1.p',unknown),
[] ).
cnf(64,axiom,
~ equal(op(e3,e4),op(e0,e4)),
file('ALG064+1.p',unknown),
[] ).
cnf(65,axiom,
~ equal(op(e4,e4),op(e0,e4)),
file('ALG064+1.p',unknown),
[] ).
cnf(68,axiom,
~ equal(op(e4,e4),op(e1,e4)),
file('ALG064+1.p',unknown),
[] ).
cnf(70,axiom,
~ equal(op(e4,e4),op(e2,e4)),
file('ALG064+1.p',unknown),
[] ).
cnf(72,axiom,
~ equal(op(e0,e1),op(e0,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(74,axiom,
~ equal(op(e0,e3),op(e0,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(75,axiom,
~ equal(op(e0,e4),op(e0,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(77,axiom,
~ equal(op(e0,e3),op(e0,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(78,axiom,
~ equal(op(e0,e4),op(e0,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(79,axiom,
~ equal(op(e0,e3),op(e0,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(81,axiom,
~ equal(op(e0,e4),op(e0,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(85,axiom,
~ equal(op(e1,e4),op(e1,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(87,axiom,
~ equal(op(e1,e3),op(e1,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(88,axiom,
~ equal(op(e1,e4),op(e1,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(90,axiom,
~ equal(op(e1,e4),op(e1,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(91,axiom,
~ equal(op(e1,e4),op(e1,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(92,axiom,
~ equal(op(e2,e1),op(e2,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(93,axiom,
~ equal(op(e2,e2),op(e2,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(96,axiom,
~ equal(op(e2,e2),op(e2,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(98,axiom,
~ equal(op(e2,e4),op(e2,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(100,axiom,
~ equal(op(e2,e4),op(e2,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(106,axiom,
~ equal(op(e3,e2),op(e3,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(111,axiom,
~ equal(op(e3,e4),op(e3,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(113,axiom,
~ equal(op(e4,e2),op(e4,e0)),
file('ALG064+1.p',unknown),
[] ).
cnf(117,axiom,
~ equal(op(e4,e3),op(e4,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(118,axiom,
~ equal(op(e4,e4),op(e4,e1)),
file('ALG064+1.p',unknown),
[] ).
cnf(119,axiom,
~ equal(op(e4,e3),op(e4,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(120,axiom,
~ equal(op(e4,e4),op(e4,e2)),
file('ALG064+1.p',unknown),
[] ).
cnf(121,axiom,
~ equal(op(e4,e4),op(e4,e3)),
file('ALG064+1.p',unknown),
[] ).
cnf(122,axiom,
( ~ skC0
| equal(op(op(e0,e0),e0),e0) ),
file('ALG064+1.p',unknown),
[] ).
cnf(123,axiom,
( ~ skC1
| equal(op(op(e0,e1),e1),e0) ),
file('ALG064+1.p',unknown),
[] ).
cnf(124,axiom,
( ~ skC2
| equal(op(op(e0,e2),e2),e0) ),
file('ALG064+1.p',unknown),
[] ).
cnf(126,axiom,
( ~ skC4
| equal(op(op(e0,e4),e4),e0) ),
file('ALG064+1.p',unknown),
[] ).
cnf(128,axiom,
( ~ skC6
| equal(op(op(e1,e1),e1),e1) ),
file('ALG064+1.p',unknown),
[] ).
cnf(129,axiom,
( ~ skC7
| equal(op(op(e1,e2),e2),e1) ),
file('ALG064+1.p',unknown),
[] ).
cnf(130,axiom,
( ~ skC8
| equal(op(op(e1,e3),e3),e1) ),
file('ALG064+1.p',unknown),
[] ).
cnf(131,axiom,
( ~ skC9
| equal(op(op(e1,e4),e4),e1) ),
file('ALG064+1.p',unknown),
[] ).
cnf(134,axiom,
( ~ skC12
| equal(op(op(e2,e2),e2),e2) ),
file('ALG064+1.p',unknown),
[] ).
cnf(139,axiom,
( ~ skC17
| equal(op(op(e3,e2),e2),e3) ),
file('ALG064+1.p',unknown),
[] ).
cnf(140,axiom,
( ~ skC18
| equal(op(op(e3,e3),e3),e3) ),
file('ALG064+1.p',unknown),
[] ).
cnf(141,axiom,
( ~ skC19
| equal(op(op(e3,e4),e4),e3) ),
file('ALG064+1.p',unknown),
[] ).
cnf(144,axiom,
( ~ skC22
| equal(op(op(e4,e2),e2),e4) ),
file('ALG064+1.p',unknown),
[] ).
cnf(146,axiom,
equal(op(op(e1,e1),op(e1,e1)),e2),
file('ALG064+1.p',unknown),
[] ).
cnf(148,axiom,
( ~ equal(op(op(e0,e0),e0),e0)
| ~ skC0 ),
file('ALG064+1.p',unknown),
[] ).
cnf(153,axiom,
( ~ skC3
| ~ equal(op(e3,e0),op(e0,e3)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(157,axiom,
( ~ skC5
| ~ equal(op(e1,e0),op(e0,e1)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(160,axiom,
( ~ equal(op(op(e1,e1),e1),e1)
| ~ skC6 ),
file('ALG064+1.p',unknown),
[] ).
cnf(167,axiom,
( ~ skC10
| ~ equal(op(e2,e0),op(e0,e2)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(169,axiom,
( ~ equal(op(e2,e1),op(e1,e2))
| ~ skC11 ),
file('ALG064+1.p',unknown),
[] ).
cnf(172,axiom,
( ~ equal(op(op(e2,e2),e2),e2)
| ~ skC12 ),
file('ALG064+1.p',unknown),
[] ).
cnf(173,axiom,
( ~ skC13
| ~ equal(op(e3,e2),op(e2,e3)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(175,axiom,
( ~ skC14
| ~ equal(op(e4,e2),op(e2,e4)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(177,axiom,
( ~ skC15
| ~ equal(op(e3,e0),op(e0,e3)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(179,axiom,
( ~ skC16
| ~ equal(op(e3,e1),op(e1,e3)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(184,axiom,
( ~ equal(op(op(e3,e3),e3),e3)
| ~ skC18 ),
file('ALG064+1.p',unknown),
[] ).
cnf(187,axiom,
( ~ skC20
| ~ equal(op(e4,e0),op(e0,e4)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(189,axiom,
( ~ skC21
| ~ equal(op(e4,e1),op(e1,e4)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(193,axiom,
( ~ skC23
| ~ equal(op(e4,e3),op(e3,e4)) ),
file('ALG064+1.p',unknown),
[] ).
cnf(195,axiom,
equal(op(e1,op(op(e1,e1),op(e1,e1))),e0),
file('ALG064+1.p',unknown),
[] ).
cnf(196,axiom,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit)
| equal(e0,unit) ),
file('ALG064+1.p',unknown),
[] ).
cnf(197,axiom,
equal(op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))),e3),
file('ALG064+1.p',unknown),
[] ).
cnf(201,axiom,
( equal(op(e4,e0),e3)
| equal(op(e4,e1),e3)
| equal(op(e4,e2),e3)
| equal(op(e4,e3),e3)
| equal(op(e4,e4),e3) ),
file('ALG064+1.p',unknown),
[] ).
cnf(206,axiom,
( equal(op(e0,e4),e0)
| equal(op(e1,e4),e0)
| equal(op(e2,e4),e0)
| equal(op(e3,e4),e0)
| equal(op(e4,e4),e0) ),
file('ALG064+1.p',unknown),
[] ).
cnf(207,axiom,
( equal(op(e4,e0),e0)
| equal(op(e4,e1),e0)
| equal(op(e4,e2),e0)
| equal(op(e4,e3),e0)
| equal(op(e4,e4),e0) ),
file('ALG064+1.p',unknown),
[] ).
cnf(208,axiom,
( equal(op(e0,e3),e4)
| equal(op(e1,e3),e4)
| equal(op(e2,e3),e4)
| equal(op(e3,e3),e4)
| equal(op(e4,e3),e4) ),
file('ALG064+1.p',unknown),
[] ).
cnf(212,axiom,
( equal(op(e0,e3),e2)
| equal(op(e1,e3),e2)
| equal(op(e2,e3),e2)
| equal(op(e3,e3),e2)
| equal(op(e4,e3),e2) ),
file('ALG064+1.p',unknown),
[] ).
cnf(218,axiom,
( equal(op(e0,e2),e4)
| equal(op(e1,e2),e4)
| equal(op(e2,e2),e4)
| equal(op(e3,e2),e4)
| equal(op(e4,e2),e4) ),
file('ALG064+1.p',unknown),
[] ).
cnf(219,axiom,
( equal(op(e2,e0),e4)
| equal(op(e2,e1),e4)
| equal(op(e2,e2),e4)
| equal(op(e2,e3),e4)
| equal(op(e2,e4),e4) ),
file('ALG064+1.p',unknown),
[] ).
cnf(222,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('ALG064+1.p',unknown),
[] ).
cnf(225,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('ALG064+1.p',unknown),
[] ).
cnf(231,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('ALG064+1.p',unknown),
[] ).
cnf(232,axiom,
( equal(op(e0,e1),e2)
| equal(op(e1,e1),e2)
| equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(e4,e1),e2) ),
file('ALG064+1.p',unknown),
[] ).
cnf(233,axiom,
( equal(op(e1,e0),e2)
| equal(op(e1,e1),e2)
| equal(op(e1,e2),e2)
| equal(op(e1,e3),e2)
| equal(op(e1,e4),e2) ),
file('ALG064+1.p',unknown),
[] ).
cnf(235,axiom,
( equal(op(e1,e0),e1)
| equal(op(e1,e1),e1)
| equal(op(e1,e2),e1)
| equal(op(e1,e3),e1)
| equal(op(e1,e4),e1) ),
file('ALG064+1.p',unknown),
[] ).
cnf(250,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('ALG064+1.p',unknown),
[] ).
cnf(255,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('ALG064+1.p',unknown),
[] ).
cnf(258,axiom,
( equal(op(e2,e4),e0)
| equal(op(e2,e4),e1)
| equal(op(e2,e4),e2)
| equal(op(e2,e4),e3)
| equal(op(e2,e4),e4) ),
file('ALG064+1.p',unknown),
[] ).
cnf(261,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('ALG064+1.p',unknown),
[] ).
cnf(262,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('ALG064+1.p',unknown),
[] ).
cnf(263,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('ALG064+1.p',unknown),
[] ).
cnf(268,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('ALG064+1.p',unknown),
[] ).
cnf(269,axiom,
( equal(op(e0,e3),e3)
| equal(op(e0,e3),e0)
| equal(op(e0,e3),e4)
| equal(op(e0,e3),e2)
| equal(op(e0,e3),e1) ),
file('ALG064+1.p',unknown),
[] ).
cnf(276,axiom,
( equal(op(e0,e0),e1)
| equal(op(e1,e1),e1)
| equal(op(e2,e2),e1)
| equal(op(e3,e3),e1)
| equal(op(e4,e4),e1) ),
file('ALG064+1.p',unknown),
[] ).
cnf(277,axiom,
( equal(op(e0,e0),e0)
| equal(op(e1,e1),e0)
| equal(op(e2,e2),e0)
| equal(op(e3,e3),e0)
| equal(op(e4,e4),e0) ),
file('ALG064+1.p',unknown),
[] ).
cnf(278,axiom,
( equal(op(op(e4,e4),e4),e4)
| skC0
| skC1
| skC2
| skC3
| skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23 ),
file('ALG064+1.p',unknown),
[] ).
cnf(279,axiom,
( ~ equal(op(op(e4,e4),e4),e4)
| skC0
| skC1
| skC2
| skC3
| skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23 ),
file('ALG064+1.p',unknown),
[] ).
cnf(281,plain,
~ equal(op(e1,e4),e4),
inference(rew,[status(thm),theory(equality)],[21,88]),
[iquote('0:Rew:21.0,88.0')] ).
cnf(282,plain,
~ equal(op(e1,e3),e4),
inference(rew,[status(thm),theory(equality)],[21,87]),
[iquote('0:Rew:21.0,87.0')] ).
cnf(287,plain,
~ equal(op(e2,e1),e4),
inference(rew,[status(thm),theory(equality)],[21,36]),
[iquote('0:Rew:21.0,36.0')] ).
cnf(289,plain,
equal(op(e4,e4),e2),
inference(rew,[status(thm),theory(equality)],[21,146]),
[iquote('0:Rew:21.0,146.0')] ).
cnf(290,plain,
~ equal(op(e4,e3),e2),
inference(rew,[status(thm),theory(equality)],[289,121]),
[iquote('0:Rew:289.0,121.0')] ).
cnf(291,plain,
~ equal(op(e4,e2),e2),
inference(rew,[status(thm),theory(equality)],[289,120]),
[iquote('0:Rew:289.0,120.0')] ).
cnf(292,plain,
~ equal(op(e4,e1),e2),
inference(rew,[status(thm),theory(equality)],[289,118]),
[iquote('0:Rew:289.0,118.0')] ).
cnf(295,plain,
~ equal(op(e2,e4),e2),
inference(rew,[status(thm),theory(equality)],[289,70]),
[iquote('0:Rew:289.0,70.0')] ).
cnf(296,plain,
~ equal(op(e1,e4),e2),
inference(rew,[status(thm),theory(equality)],[289,68]),
[iquote('0:Rew:289.0,68.0')] ).
cnf(297,plain,
~ equal(op(e0,e4),e2),
inference(rew,[status(thm),theory(equality)],[289,65]),
[iquote('0:Rew:289.0,65.0')] ).
cnf(298,plain,
( ~ skC6
| equal(op(e4,e1),e1) ),
inference(rew,[status(thm),theory(equality)],[21,128]),
[iquote('0:Rew:21.0,128.1')] ).
cnf(299,plain,
( ~ equal(e3,e3)
| ~ skC18 ),
inference(rew,[status(thm),theory(equality)],[140,184]),
[iquote('0:Rew:140.1,184.0')] ).
cnf(300,plain,
~ skC18,
inference(obv,[status(thm),theory(equality)],[299]),
[iquote('0:Obv:299.0')] ).
cnf(302,plain,
( ~ equal(e2,e2)
| ~ skC12 ),
inference(rew,[status(thm),theory(equality)],[134,172]),
[iquote('0:Rew:134.1,172.0')] ).
cnf(303,plain,
~ skC12,
inference(obv,[status(thm),theory(equality)],[302]),
[iquote('0:Obv:302.0')] ).
cnf(305,plain,
( ~ equal(e1,e1)
| ~ skC6 ),
inference(rew,[status(thm),theory(equality)],[298,160,21]),
[iquote('0:Rew:298.1,160.0,21.0,160.0')] ).
cnf(306,plain,
~ skC6,
inference(obv,[status(thm),theory(equality)],[305]),
[iquote('0:Obv:305.0')] ).
cnf(308,plain,
( ~ equal(e0,e0)
| ~ skC0 ),
inference(rew,[status(thm),theory(equality)],[122,148]),
[iquote('0:Rew:122.1,148.0')] ).
cnf(309,plain,
~ skC0,
inference(obv,[status(thm),theory(equality)],[308]),
[iquote('0:Obv:308.0')] ).
cnf(311,plain,
equal(op(e1,e2),e0),
inference(rew,[status(thm),theory(equality)],[289,195,21]),
[iquote('0:Rew:289.0,195.0,21.0,195.0')] ).
cnf(312,plain,
~ equal(op(e1,e4),e0),
inference(rew,[status(thm),theory(equality)],[311,90]),
[iquote('0:Rew:311.0,90.0')] ).
cnf(316,plain,
~ equal(op(e4,e2),e0),
inference(rew,[status(thm),theory(equality)],[311,48]),
[iquote('0:Rew:311.0,48.0')] ).
cnf(317,plain,
~ equal(op(e3,e2),e0),
inference(rew,[status(thm),theory(equality)],[311,47]),
[iquote('0:Rew:311.0,47.0')] ).
cnf(320,plain,
( ~ skC7
| equal(op(e0,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[311,129]),
[iquote('0:Rew:311.0,129.1')] ).
cnf(322,plain,
( ~ skC11
| ~ equal(op(e2,e1),e0) ),
inference(rew,[status(thm),theory(equality)],[311,169]),
[iquote('0:Rew:311.0,169.0')] ).
cnf(324,plain,
equal(op(e2,e2),e3),
inference(rew,[status(thm),theory(equality)],[289,197,21]),
[iquote('0:Rew:289.0,197.0,21.0,197.0')] ).
cnf(325,plain,
~ equal(op(e2,e4),e3),
inference(rew,[status(thm),theory(equality)],[324,100]),
[iquote('0:Rew:324.0,100.0')] ).
cnf(327,plain,
~ equal(op(e2,e1),e3),
inference(rew,[status(thm),theory(equality)],[324,96]),
[iquote('0:Rew:324.0,96.0')] ).
cnf(328,plain,
~ equal(op(e2,e0),e3),
inference(rew,[status(thm),theory(equality)],[324,93]),
[iquote('0:Rew:324.0,93.0')] ).
cnf(329,plain,
~ equal(op(e4,e2),e3),
inference(rew,[status(thm),theory(equality)],[324,50]),
[iquote('0:Rew:324.0,50.0')] ).
cnf(330,plain,
~ equal(op(e3,e2),e3),
inference(rew,[status(thm),theory(equality)],[324,49]),
[iquote('0:Rew:324.0,49.0')] ).
cnf(339,plain,
( equal(op(e4,e0),e3)
| equal(op(e4,e1),e3)
| equal(op(e4,e2),e3)
| equal(op(e4,e3),e3)
| equal(e3,e2) ),
inference(rew,[status(thm),theory(equality)],[289,201]),
[iquote('0:Rew:289.0,201.4')] ).
cnf(340,plain,
( equal(op(e4,e3),e3)
| equal(op(e4,e1),e3)
| equal(op(e4,e0),e3) ),
inference(mrr,[status(thm)],[339,329,8]),
[iquote('0:MRR:339.2,339.4,329.0,8.0')] ).
cnf(345,plain,
( equal(op(e0,e4),e0)
| equal(op(e1,e4),e0)
| equal(op(e2,e4),e0)
| equal(op(e3,e4),e0)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[289,206]),
[iquote('0:Rew:289.0,206.4')] ).
cnf(346,plain,
( equal(op(e0,e4),e0)
| equal(op(e3,e4),e0)
| equal(op(e2,e4),e0) ),
inference(mrr,[status(thm)],[345,312,2]),
[iquote('0:MRR:345.1,345.4,312.0,2.0')] ).
cnf(347,plain,
( equal(op(e4,e0),e0)
| equal(op(e4,e1),e0)
| equal(op(e4,e2),e0)
| equal(op(e4,e3),e0)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[289,207]),
[iquote('0:Rew:289.0,207.4')] ).
cnf(348,plain,
( equal(op(e4,e0),e0)
| equal(op(e4,e3),e0)
| equal(op(e4,e1),e0) ),
inference(mrr,[status(thm)],[347,316,2]),
[iquote('0:MRR:347.2,347.4,316.0,2.0')] ).
cnf(349,plain,
( equal(op(e4,e3),e4)
| equal(op(e3,e3),e4)
| equal(op(e2,e3),e4)
| equal(op(e0,e3),e4) ),
inference(mrr,[status(thm)],[208,282]),
[iquote('0:MRR:208.1,282.0')] ).
cnf(353,plain,
( equal(op(e3,e3),e2)
| equal(op(e2,e3),e2)
| equal(op(e1,e3),e2)
| equal(op(e0,e3),e2) ),
inference(mrr,[status(thm)],[212,290]),
[iquote('0:MRR:212.4,290.0')] ).
cnf(357,plain,
( equal(op(e0,e2),e4)
| equal(e4,e0)
| equal(e4,e3)
| equal(op(e3,e2),e4)
| equal(op(e4,e2),e4) ),
inference(rew,[status(thm),theory(equality)],[324,218,311]),
[iquote('0:Rew:324.0,218.2,311.0,218.1')] ).
cnf(358,plain,
( equal(op(e4,e2),e4)
| equal(op(e3,e2),e4)
| equal(op(e0,e2),e4) ),
inference(mrr,[status(thm)],[357,4,10]),
[iquote('0:MRR:357.1,357.2,4.0,10.0')] ).
cnf(359,plain,
( equal(op(e2,e0),e4)
| equal(op(e2,e1),e4)
| equal(e4,e3)
| equal(op(e2,e3),e4)
| equal(op(e2,e4),e4) ),
inference(rew,[status(thm),theory(equality)],[324,219]),
[iquote('0:Rew:324.0,219.2')] ).
cnf(360,plain,
( equal(op(e2,e4),e4)
| equal(op(e2,e3),e4)
| equal(op(e2,e0),e4) ),
inference(mrr,[status(thm)],[359,287,10]),
[iquote('0:MRR:359.1,359.2,287.0,10.0')] ).
cnf(361,plain,
( equal(op(e0,e2),e2)
| equal(e2,e0)
| equal(e3,e2)
| equal(op(e3,e2),e2)
| equal(op(e4,e2),e2) ),
inference(rew,[status(thm),theory(equality)],[324,222,311]),
[iquote('0:Rew:324.0,222.2,311.0,222.1')] ).
cnf(362,plain,
( equal(op(e3,e2),e2)
| equal(op(e0,e2),e2) ),
inference(mrr,[status(thm)],[361,2,8,291]),
[iquote('0:MRR:361.1,361.2,361.4,2.0,8.0,291.0')] ).
cnf(367,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)],[324,225]),
[iquote('0:Rew:324.0,225.2')] ).
cnf(368,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)],[367,6]),
[iquote('0:MRR:367.2,6.0')] ).
cnf(373,plain,
( equal(op(e1,e0),e3)
| equal(e4,e3)
| equal(e3,e0)
| equal(op(e1,e3),e3)
| equal(op(e1,e4),e3) ),
inference(rew,[status(thm),theory(equality)],[311,231,21]),
[iquote('0:Rew:311.0,231.2,21.0,231.1')] ).
cnf(374,plain,
( equal(op(e1,e3),e3)
| equal(op(e1,e4),e3)
| equal(op(e1,e0),e3) ),
inference(mrr,[status(thm)],[373,10,3]),
[iquote('0:MRR:373.1,373.2,10.0,3.0')] ).
cnf(375,plain,
( equal(op(e0,e1),e2)
| equal(e4,e2)
| equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(e4,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[21,232]),
[iquote('0:Rew:21.0,232.1')] ).
cnf(376,plain,
( equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(e0,e1),e2) ),
inference(mrr,[status(thm)],[375,9,292]),
[iquote('0:MRR:375.1,375.4,9.0,292.0')] ).
cnf(377,plain,
( equal(op(e1,e0),e2)
| equal(e4,e2)
| equal(e2,e0)
| equal(op(e1,e3),e2)
| equal(op(e1,e4),e2) ),
inference(rew,[status(thm),theory(equality)],[311,233,21]),
[iquote('0:Rew:311.0,233.2,21.0,233.1')] ).
cnf(378,plain,
( equal(op(e1,e3),e2)
| equal(op(e1,e0),e2) ),
inference(mrr,[status(thm)],[377,9,2,296]),
[iquote('0:MRR:377.1,377.2,377.4,9.0,2.0,296.0')] ).
cnf(381,plain,
( equal(op(e1,e0),e1)
| equal(e4,e1)
| equal(e1,e0)
| equal(op(e1,e3),e1)
| equal(op(e1,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[311,235,21]),
[iquote('0:Rew:311.0,235.2,21.0,235.1')] ).
cnf(382,plain,
( equal(op(e1,e4),e1)
| equal(op(e1,e3),e1)
| equal(op(e1,e0),e1) ),
inference(mrr,[status(thm)],[381,7,1]),
[iquote('0:MRR:381.1,381.2,7.0,1.0')] ).
cnf(394,plain,
( equal(op(e4,e2),e4)
| equal(op(e4,e2),e1) ),
inference(mrr,[status(thm)],[250,316,291,329]),
[iquote('0:MRR:250.0,250.2,250.3,316.0,291.0,329.0')] ).
cnf(398,plain,
( equal(op(e3,e2),e2)
| equal(op(e3,e2),e4)
| equal(op(e3,e2),e1) ),
inference(mrr,[status(thm)],[255,317,330]),
[iquote('0:MRR:255.0,255.3,317.0,330.0')] ).
cnf(400,plain,
( equal(op(e2,e4),e4)
| equal(op(e2,e4),e1)
| equal(op(e2,e4),e0) ),
inference(mrr,[status(thm)],[258,295,325]),
[iquote('0:MRR:258.2,258.3,295.0,325.0')] ).
cnf(402,plain,
( equal(op(e2,e1),e2)
| equal(op(e2,e1),e1)
| equal(op(e2,e1),e0) ),
inference(mrr,[status(thm)],[261,327,287]),
[iquote('0:MRR:261.3,261.4,327.0,287.0')] ).
cnf(403,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)],[262,328]),
[iquote('0:MRR:262.3,328.0')] ).
cnf(404,plain,
( equal(op(e1,e4),e1)
| equal(op(e1,e4),e3) ),
inference(mrr,[status(thm)],[263,312,296,281]),
[iquote('0:MRR:263.0,263.2,263.4,312.0,296.0,281.0')] ).
cnf(407,plain,
( equal(op(e0,e4),e4)
| equal(op(e0,e4),e0)
| equal(op(e0,e4),e3)
| equal(op(e0,e4),e1) ),
inference(mrr,[status(thm)],[268,297]),
[iquote('0:MRR:268.2,297.0')] ).
cnf(410,plain,
( equal(op(e0,e0),e1)
| equal(e4,e1)
| equal(e3,e1)
| equal(op(e3,e3),e1)
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[289,276,324,21]),
[iquote('0:Rew:289.0,276.4,324.0,276.2,21.0,276.1')] ).
cnf(411,plain,
( equal(op(e3,e3),e1)
| equal(op(e0,e0),e1) ),
inference(mrr,[status(thm)],[410,7,6,5]),
[iquote('0:MRR:410.1,410.2,410.4,7.0,6.0,5.0')] ).
cnf(412,plain,
( equal(op(e0,e0),e0)
| equal(e4,e0)
| equal(e3,e0)
| equal(op(e3,e3),e0)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[289,277,324,21]),
[iquote('0:Rew:289.0,277.4,324.0,277.2,21.0,277.1')] ).
cnf(413,plain,
( equal(op(e0,e0),e0)
| equal(op(e3,e3),e0) ),
inference(mrr,[status(thm)],[412,4,3,2]),
[iquote('0:MRR:412.1,412.2,412.4,4.0,3.0,2.0')] ).
cnf(414,plain,
( equal(op(e2,e4),e4)
| skC0
| skC1
| skC2
| skC3
| skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23 ),
inference(rew,[status(thm),theory(equality)],[289,278]),
[iquote('0:Rew:289.0,278.0')] ).
cnf(415,plain,
( equal(op(e2,e4),e4)
| skC1
| skC2
| skC3
| skC4
| skC5
| skC7
| skC8
| skC9
| skC10
| skC11
| skC13
| skC14
| skC15
| skC16
| skC17
| skC19
| skC20
| skC21
| skC22
| skC23 ),
inference(mrr,[status(thm)],[414,309,306,303,300]),
[iquote('0:MRR:414.1,414.7,414.13,414.19,309.0,306.0,303.0,300.0')] ).
cnf(416,plain,
( ~ equal(e4,e4)
| skC0
| skC1
| skC2
| skC3
| skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23 ),
inference(rew,[status(thm),theory(equality)],[415,279,289]),
[iquote('0:Rew:415.0,279.0,289.0,279.0')] ).
cnf(417,plain,
( skC0
| skC1
| skC2
| skC3
| skC4
| skC5
| skC6
| skC7
| skC8
| skC9
| skC10
| skC11
| skC12
| skC13
| skC14
| skC15
| skC16
| skC17
| skC18
| skC19
| skC20
| skC21
| skC22
| skC23 ),
inference(obv,[status(thm),theory(equality)],[416]),
[iquote('0:Obv:416.0')] ).
cnf(418,plain,
( skC23
| skC22
| skC21
| skC20
| skC19
| skC17
| skC16
| skC15
| skC14
| skC13
| skC11
| skC10
| skC9
| skC8
| skC7
| skC5
| skC4
| skC3
| skC2
| skC1 ),
inference(mrr,[status(thm)],[417,309,306,303,300]),
[iquote('0:MRR:417.0,417.6,417.12,417.18,309.0,306.0,303.0,300.0')] ).
cnf(420,plain,
equal(e0,unit),
inference(spt,[spt(split,[position(s1)])],[196]),
[iquote('1:Spt:196.4')] ).
cnf(425,plain,
( equal(op(e4,e3),e3)
| equal(op(e4,e1),e3)
| equal(op(e4,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[420,340]),
[iquote('1:Rew:420.0,340.2')] ).
cnf(430,plain,
~ equal(op(e4,e2),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[420,113]),
[iquote('1:Rew:420.0,113.0')] ).
cnf(444,plain,
( equal(op(e2,e4),e4)
| equal(op(e2,e3),e4)
| equal(op(e2,unit),e4) ),
inference(rew,[status(thm),theory(equality)],[420,360]),
[iquote('1:Rew:420.0,360.2')] ).
cnf(450,plain,
~ equal(op(e2,e1),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[420,92]),
[iquote('1:Rew:420.0,92.0')] ).
cnf(455,plain,
( equal(op(e1,e3),e2)
| equal(op(e1,unit),e2) ),
inference(rew,[status(thm),theory(equality)],[420,378]),
[iquote('1:Rew:420.0,378.1')] ).
cnf(458,plain,
~ equal(op(e1,e4),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[420,85]),
[iquote('1:Rew:420.0,85.0')] ).
cnf(463,plain,
( ~ skC3
| ~ equal(op(e3,unit),op(unit,e3)) ),
inference(rew,[status(thm),theory(equality)],[420,153]),
[iquote('1:Rew:420.0,153.1')] ).
cnf(464,plain,
( ~ skC15
| ~ equal(op(e3,unit),op(unit,e3)) ),
inference(rew,[status(thm),theory(equality)],[420,177]),
[iquote('1:Rew:420.0,177.1')] ).
cnf(474,plain,
~ equal(op(e4,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[420,55]),
[iquote('1:Rew:420.0,55.0')] ).
cnf(479,plain,
( ~ skC20
| ~ equal(op(e4,unit),op(unit,e4)) ),
inference(rew,[status(thm),theory(equality)],[420,187]),
[iquote('1:Rew:420.0,187.1')] ).
cnf(487,plain,
~ equal(op(e2,e4),op(unit,e4)),
inference(rew,[status(thm),theory(equality)],[420,63]),
[iquote('1:Rew:420.0,63.0')] ).
cnf(490,plain,
( ~ skC10
| ~ equal(op(e2,unit),op(unit,e2)) ),
inference(rew,[status(thm),theory(equality)],[420,167]),
[iquote('1:Rew:420.0,167.1')] ).
cnf(493,plain,
( ~ skC7
| equal(op(unit,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[420,320]),
[iquote('1:Rew:420.0,320.1')] ).
cnf(500,plain,
~ equal(op(e3,e2),op(unit,e2)),
inference(rew,[status(thm),theory(equality)],[420,44]),
[iquote('1:Rew:420.0,44.0')] ).
cnf(502,plain,
( ~ skC5
| ~ equal(op(e1,unit),op(unit,e1)) ),
inference(rew,[status(thm),theory(equality)],[420,157]),
[iquote('1:Rew:420.0,157.1')] ).
cnf(504,plain,
( equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(unit,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[420,376]),
[iquote('1:Rew:420.0,376.2')] ).
cnf(514,plain,
~ equal(op(e2,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[420,33]),
[iquote('1:Rew:420.0,33.0')] ).
cnf(516,plain,
( equal(op(e3,e3),e1)
| equal(op(unit,unit),e1) ),
inference(rew,[status(thm),theory(equality)],[420,411]),
[iquote('1:Rew:420.0,411.1')] ).
cnf(527,plain,
( equal(op(e2,e1),e2)
| equal(op(e2,e1),e1)
| equal(op(e2,e1),unit) ),
inference(rew,[status(thm),theory(equality)],[420,402]),
[iquote('1:Rew:420.0,402.2')] ).
cnf(528,plain,
( ~ skC11
| ~ equal(op(e2,e1),unit) ),
inference(rew,[status(thm),theory(equality)],[420,322]),
[iquote('1:Rew:420.0,322.1')] ).
cnf(531,plain,
( equal(op(unit,e4),unit)
| equal(op(e3,e4),e0)
| equal(op(e2,e4),e0) ),
inference(rew,[status(thm),theory(equality)],[420,346]),
[iquote('1:Rew:420.0,346.0')] ).
cnf(532,plain,
( equal(op(e2,e4),e4)
| equal(op(e2,e4),e1)
| equal(op(e2,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[420,400]),
[iquote('1:Rew:420.0,400.2')] ).
cnf(536,plain,
( equal(op(e4,unit),unit)
| equal(op(e4,e3),e0)
| equal(op(e4,e1),e0) ),
inference(rew,[status(thm),theory(equality)],[420,348]),
[iquote('1:Rew:420.0,348.0')] ).
cnf(544,plain,
~ equal(e4,unit),
inference(rew,[status(thm),theory(equality)],[420,4]),
[iquote('1:Rew:420.0,4.0')] ).
cnf(545,plain,
~ equal(e3,unit),
inference(rew,[status(thm),theory(equality)],[420,3]),
[iquote('1:Rew:420.0,3.0')] ).
cnf(546,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[420,2]),
[iquote('1:Rew:420.0,2.0')] ).
cnf(547,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[420,1]),
[iquote('1:Rew:420.0,1.0')] ).
cnf(548,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[420,12]),
[iquote('1:Rew:420.0,12.0')] ).
cnf(550,plain,
equal(op(e1,e2),unit),
inference(rew,[status(thm),theory(equality)],[420,311]),
[iquote('1:Rew:420.0,311.0')] ).
cnf(561,plain,
( ~ skC4
| equal(op(op(unit,e4),e4),unit) ),
inference(rew,[status(thm),theory(equality)],[420,126]),
[iquote('1:Rew:420.0,126.1')] ).
cnf(563,plain,
( ~ skC2
| equal(op(op(unit,e2),e2),unit) ),
inference(rew,[status(thm),theory(equality)],[420,124]),
[iquote('1:Rew:420.0,124.1')] ).
cnf(564,plain,
( ~ skC1
| equal(op(op(unit,e1),e1),unit) ),
inference(rew,[status(thm),theory(equality)],[420,123]),
[iquote('1:Rew:420.0,123.1')] ).
cnf(581,plain,
( ~ skC7
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[15,493]),
[iquote('1:Rew:15.0,493.1')] ).
cnf(582,plain,
~ skC7,
inference(mrr,[status(thm)],[581,5]),
[iquote('1:MRR:581.1,5.0')] ).
cnf(583,plain,
( skC23
| skC22
| skC21
| skC20
| skC19
| skC17
| skC16
| skC15
| skC14
| skC13
| skC11
| skC10
| skC9
| skC8
| skC5
| skC4
| skC3
| skC2
| skC1 ),
inference(mrr,[status(thm)],[418,582]),
[iquote('1:MRR:418.14,582.0')] ).
cnf(585,plain,
~ equal(op(e4,e2),e4),
inference(rew,[status(thm),theory(equality)],[20,430]),
[iquote('1:Rew:20.0,430.0')] ).
cnf(586,plain,
equal(op(e4,e2),e1),
inference(mrr,[status(thm)],[394,585]),
[iquote('1:MRR:394.0,585.0')] ).
cnf(587,plain,
( ~ skC14
| ~ equal(op(e2,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[586,175]),
[iquote('1:Rew:586.0,175.1')] ).
cnf(593,plain,
~ equal(op(e3,e2),e1),
inference(rew,[status(thm),theory(equality)],[586,51]),
[iquote('1:Rew:586.0,51.0')] ).
cnf(594,plain,
( ~ skC22
| equal(op(e1,e2),e4) ),
inference(rew,[status(thm),theory(equality)],[586,144]),
[iquote('1:Rew:586.0,144.1')] ).
cnf(598,plain,
( equal(op(e3,e2),e2)
| equal(op(e3,e2),e4) ),
inference(mrr,[status(thm)],[398,593]),
[iquote('1:MRR:398.2,593.0')] ).
cnf(599,plain,
( ~ skC22
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[550,594]),
[iquote('1:Rew:550.0,594.1')] ).
cnf(600,plain,
~ skC22,
inference(mrr,[status(thm)],[599,544]),
[iquote('1:MRR:599.1,544.0')] ).
cnf(609,plain,
~ equal(op(e2,e1),e2),
inference(rew,[status(thm),theory(equality)],[16,450]),
[iquote('1:Rew:16.0,450.0')] ).
cnf(612,plain,
~ equal(op(e1,e4),e1),
inference(rew,[status(thm),theory(equality)],[14,458]),
[iquote('1:Rew:14.0,458.0')] ).
cnf(613,plain,
equal(op(e1,e4),e3),
inference(mrr,[status(thm)],[404,612]),
[iquote('1:MRR:404.0,612.0')] ).
cnf(615,plain,
( ~ skC21
| ~ equal(op(e4,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[613,189]),
[iquote('1:Rew:613.0,189.1')] ).
cnf(621,plain,
( ~ skC9
| equal(op(e3,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[613,131]),
[iquote('1:Rew:613.0,131.1')] ).
cnf(630,plain,
~ equal(op(e4,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,474]),
[iquote('1:Rew:17.0,474.0')] ).
cnf(636,plain,
~ equal(op(e2,e4),e4),
inference(rew,[status(thm),theory(equality)],[19,487]),
[iquote('1:Rew:19.0,487.0')] ).
cnf(641,plain,
~ equal(op(e3,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,500]),
[iquote('1:Rew:15.0,500.0')] ).
cnf(647,plain,
~ equal(op(e2,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,514]),
[iquote('1:Rew:13.0,514.0')] ).
cnf(660,plain,
( ~ skC4
| equal(e2,unit) ),
inference(rew,[status(thm),theory(equality)],[289,561,19]),
[iquote('1:Rew:289.0,561.1,19.0,561.1')] ).
cnf(661,plain,
~ skC4,
inference(mrr,[status(thm)],[660,546]),
[iquote('1:MRR:660.1,546.0')] ).
cnf(663,plain,
( ~ skC2
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[324,563,15]),
[iquote('1:Rew:324.0,563.1,15.0,563.1')] ).
cnf(664,plain,
~ skC2,
inference(mrr,[status(thm)],[663,545]),
[iquote('1:MRR:663.1,545.0')] ).
cnf(665,plain,
( ~ skC1
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[21,564,13]),
[iquote('1:Rew:21.0,564.1,13.0,564.1')] ).
cnf(666,plain,
~ skC1,
inference(mrr,[status(thm)],[665,544]),
[iquote('1:MRR:665.1,544.0')] ).
cnf(667,plain,
( equal(op(e1,e3),e2)
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[14,455]),
[iquote('1:Rew:14.0,455.1')] ).
cnf(668,plain,
equal(op(e1,e3),e2),
inference(mrr,[status(thm)],[667,5]),
[iquote('1:MRR:667.1,5.0')] ).
cnf(670,plain,
( ~ skC16
| ~ equal(op(e3,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[668,179]),
[iquote('1:Rew:668.0,179.1')] ).
cnf(675,plain,
( ~ skC8
| equal(op(e2,e3),e1) ),
inference(rew,[status(thm),theory(equality)],[668,130]),
[iquote('1:Rew:668.0,130.1')] ).
cnf(680,plain,
( ~ skC3
| ~ equal(e3,e3) ),
inference(rew,[status(thm),theory(equality)],[18,463,17]),
[iquote('1:Rew:18.0,463.1,17.0,463.1')] ).
cnf(681,plain,
~ skC3,
inference(obv,[status(thm),theory(equality)],[680]),
[iquote('1:Obv:680.1')] ).
cnf(682,plain,
( ~ skC15
| ~ equal(e3,e3) ),
inference(rew,[status(thm),theory(equality)],[18,464,17]),
[iquote('1:Rew:18.0,464.1,17.0,464.1')] ).
cnf(683,plain,
~ skC15,
inference(obv,[status(thm),theory(equality)],[682]),
[iquote('1:Obv:682.1')] ).
cnf(684,plain,
( ~ skC20
| ~ equal(e4,e4) ),
inference(rew,[status(thm),theory(equality)],[20,479,19]),
[iquote('1:Rew:20.0,479.1,19.0,479.1')] ).
cnf(685,plain,
~ skC20,
inference(obv,[status(thm),theory(equality)],[684]),
[iquote('1:Obv:684.1')] ).
cnf(686,plain,
( ~ skC10
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[16,490,15]),
[iquote('1:Rew:16.0,490.1,15.0,490.1')] ).
cnf(687,plain,
~ skC10,
inference(obv,[status(thm),theory(equality)],[686]),
[iquote('1:Obv:686.1')] ).
cnf(688,plain,
( ~ skC5
| ~ equal(e1,e1) ),
inference(rew,[status(thm),theory(equality)],[14,502,13]),
[iquote('1:Rew:14.0,502.1,13.0,502.1')] ).
cnf(689,plain,
~ skC5,
inference(obv,[status(thm),theory(equality)],[688]),
[iquote('1:Obv:688.1')] ).
cnf(690,plain,
( equal(op(e3,e3),e1)
| equal(e1,unit) ),
inference(rew,[status(thm),theory(equality)],[548,516]),
[iquote('1:Rew:548.0,516.1')] ).
cnf(691,plain,
equal(op(e3,e3),e1),
inference(mrr,[status(thm)],[690,547]),
[iquote('1:MRR:690.1,547.0')] ).
cnf(692,plain,
~ equal(op(e3,e4),e1),
inference(rew,[status(thm),theory(equality)],[691,111]),
[iquote('1:Rew:691.0,111.0')] ).
cnf(696,plain,
~ equal(op(e2,e3),e1),
inference(rew,[status(thm),theory(equality)],[691,59]),
[iquote('1:Rew:691.0,59.0')] ).
cnf(699,plain,
~ skC9,
inference(mrr,[status(thm)],[621,692]),
[iquote('1:MRR:621.1,692.0')] ).
cnf(700,plain,
~ skC8,
inference(mrr,[status(thm)],[675,696]),
[iquote('1:MRR:675.1,696.0')] ).
cnf(702,plain,
equal(op(e3,e2),e4),
inference(mrr,[status(thm)],[598,641]),
[iquote('1:MRR:598.0,641.0')] ).
cnf(703,plain,
( ~ skC13
| ~ equal(op(e2,e3),e4) ),
inference(rew,[status(thm),theory(equality)],[702,173]),
[iquote('1:Rew:702.0,173.1')] ).
cnf(708,plain,
( ~ skC17
| equal(op(e4,e2),e3) ),
inference(rew,[status(thm),theory(equality)],[702,139]),
[iquote('1:Rew:702.0,139.1')] ).
cnf(713,plain,
( ~ skC17
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[586,708]),
[iquote('1:Rew:586.0,708.1')] ).
cnf(714,plain,
~ skC17,
inference(mrr,[status(thm)],[713,6]),
[iquote('1:MRR:713.1,6.0')] ).
cnf(715,plain,
( equal(op(e4,e3),e3)
| equal(op(e4,e1),e3)
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[20,425]),
[iquote('1:Rew:20.0,425.2')] ).
cnf(716,plain,
equal(op(e4,e1),e3),
inference(mrr,[status(thm)],[715,630,10]),
[iquote('1:MRR:715.0,715.2,630.0,10.0')] ).
cnf(725,plain,
( ~ skC21
| ~ equal(e3,e3) ),
inference(rew,[status(thm),theory(equality)],[716,615]),
[iquote('1:Rew:716.0,615.1')] ).
cnf(726,plain,
~ skC21,
inference(obv,[status(thm),theory(equality)],[725]),
[iquote('1:Obv:725.1')] ).
cnf(727,plain,
( equal(op(e2,e4),e4)
| equal(op(e2,e3),e4)
| equal(e4,e2) ),
inference(rew,[status(thm),theory(equality)],[16,444]),
[iquote('1:Rew:16.0,444.2')] ).
cnf(728,plain,
equal(op(e2,e3),e4),
inference(mrr,[status(thm)],[727,636,9]),
[iquote('1:MRR:727.0,727.2,636.0,9.0')] ).
cnf(737,plain,
( ~ skC13
| ~ equal(e4,e4) ),
inference(rew,[status(thm),theory(equality)],[728,703]),
[iquote('1:Rew:728.0,703.1')] ).
cnf(738,plain,
~ skC13,
inference(obv,[status(thm),theory(equality)],[737]),
[iquote('1:Obv:737.1')] ).
cnf(741,plain,
( equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[13,504]),
[iquote('1:Rew:13.0,504.2')] ).
cnf(742,plain,
equal(op(e3,e1),e2),
inference(mrr,[status(thm)],[741,609,5]),
[iquote('1:MRR:741.0,741.2,609.0,5.0')] ).
cnf(750,plain,
( ~ skC16
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[742,670]),
[iquote('1:Rew:742.0,670.1')] ).
cnf(751,plain,
~ skC16,
inference(obv,[status(thm),theory(equality)],[750]),
[iquote('1:Obv:750.1')] ).
cnf(752,plain,
equal(op(e2,e1),unit),
inference(mrr,[status(thm)],[527,609,647]),
[iquote('1:MRR:527.0,527.1,609.0,647.0')] ).
cnf(755,plain,
~ equal(op(e2,e4),unit),
inference(rew,[status(thm),theory(equality)],[752,98]),
[iquote('1:Rew:752.0,98.0')] ).
cnf(760,plain,
( ~ skC11
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[752,528]),
[iquote('1:Rew:752.0,528.1')] ).
cnf(761,plain,
~ skC11,
inference(obv,[status(thm),theory(equality)],[760]),
[iquote('1:Obv:760.1')] ).
cnf(762,plain,
( equal(e4,unit)
| equal(op(e3,e4),unit)
| equal(op(e2,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[420,531,19]),
[iquote('1:Rew:420.0,531.2,420.0,531.1,19.0,531.0')] ).
cnf(763,plain,
equal(op(e3,e4),unit),
inference(mrr,[status(thm)],[762,544,755]),
[iquote('1:MRR:762.0,762.2,544.0,755.0')] ).
cnf(765,plain,
( ~ skC23
| ~ equal(op(e4,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[763,193]),
[iquote('1:Rew:763.0,193.1')] ).
cnf(768,plain,
( ~ skC19
| equal(op(unit,e4),e3) ),
inference(rew,[status(thm),theory(equality)],[763,141]),
[iquote('1:Rew:763.0,141.1')] ).
cnf(773,plain,
( ~ skC19
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[19,768]),
[iquote('1:Rew:19.0,768.1')] ).
cnf(774,plain,
~ skC19,
inference(mrr,[status(thm)],[773,10]),
[iquote('1:MRR:773.1,10.0')] ).
cnf(775,plain,
equal(op(e2,e4),e1),
inference(mrr,[status(thm)],[532,636,755]),
[iquote('1:MRR:532.0,532.2,636.0,755.0')] ).
cnf(781,plain,
( ~ skC14
| ~ equal(e1,e1) ),
inference(rew,[status(thm),theory(equality)],[775,587]),
[iquote('1:Rew:775.0,587.1')] ).
cnf(783,plain,
~ skC14,
inference(obv,[status(thm),theory(equality)],[781]),
[iquote('1:Obv:781.1')] ).
cnf(784,plain,
( equal(e4,unit)
| equal(op(e4,e3),unit)
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[716,536,420,20]),
[iquote('1:Rew:716.0,536.2,420.0,536.2,420.0,536.1,20.0,536.0')] ).
cnf(785,plain,
equal(op(e4,e3),unit),
inference(mrr,[status(thm)],[784,544,545]),
[iquote('1:MRR:784.0,784.2,544.0,545.0')] ).
cnf(792,plain,
( ~ skC23
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[785,765]),
[iquote('1:Rew:785.0,765.1')] ).
cnf(793,plain,
~ skC23,
inference(obv,[status(thm),theory(equality)],[792]),
[iquote('1:Obv:792.1')] ).
cnf(794,plain,
$false,
inference(mrr,[status(thm)],[583,793,600,726,685,774,714,751,683,783,738,761,687,699,700,689,661,681,664,666]),
[iquote('1:MRR:583.0,583.1,583.2,583.3,583.4,583.5,583.6,583.7,583.8,583.9,583.10,583.11,583.12,583.13,583.14,583.15,583.16,583.17,583.18,793.0,600.0,726.0,685.0,774.0,714.0,751.0,683.0,783.0,738.0,761.0,687.0,699.0,700.0,689.0,661.0,681.0,664.0,666.0')] ).
cnf(808,plain,
~ equal(e0,unit),
inference(spt,[spt(split,[position(sa)])],[794,420]),
[iquote('1:Spt:794.0,196.4,420.0')] ).
cnf(809,plain,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2)])],[196]),
[iquote('1:Spt:794.0,196.0,196.1,196.2,196.3')] ).
cnf(810,plain,
equal(e4,unit),
inference(spt,[spt(split,[position(s2s1)])],[809]),
[iquote('2:Spt:809.0')] ).
cnf(812,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[810,9]),
[iquote('2:Rew:810.0,9.0')] ).
cnf(822,plain,
~ equal(op(e0,e2),op(unit,e2)),
inference(rew,[status(thm),theory(equality)],[810,45]),
[iquote('2:Rew:810.0,45.0')] ).
cnf(838,plain,
~ equal(op(e0,e0),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[810,75]),
[iquote('2:Rew:810.0,75.0')] ).
cnf(897,plain,
~ equal(op(e2,e1),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[810,98]),
[iquote('2:Rew:810.0,98.0')] ).
cnf(905,plain,
~ equal(op(e0,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[810,55]),
[iquote('2:Rew:810.0,55.0')] ).
cnf(929,plain,
( equal(op(unit,e2),unit)
| equal(op(e3,e2),e4)
| equal(op(e0,e2),e4) ),
inference(rew,[status(thm),theory(equality)],[810,358]),
[iquote('2:Rew:810.0,358.0')] ).
cnf(949,plain,
( equal(op(e0,e3),e3)
| equal(op(e0,e3),e0)
| equal(op(e0,e3),unit)
| equal(op(e0,e3),e2)
| equal(op(e0,e3),e1) ),
inference(rew,[status(thm),theory(equality)],[810,269]),
[iquote('2:Rew:810.0,269.2')] ).
cnf(968,plain,
~ equal(op(e0,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,822]),
[iquote('2:Rew:15.0,822.0')] ).
cnf(969,plain,
equal(op(e3,e2),e2),
inference(mrr,[status(thm)],[362,968]),
[iquote('2:MRR:362.1,968.0')] ).
cnf(976,plain,
~ equal(op(e3,e1),e2),
inference(rew,[status(thm),theory(equality)],[969,106]),
[iquote('2:Rew:969.0,106.0')] ).
cnf(983,plain,
( equal(op(e2,e1),e2)
| equal(op(e0,e1),e2) ),
inference(mrr,[status(thm)],[376,976]),
[iquote('2:MRR:376.1,976.0')] ).
cnf(991,plain,
~ equal(op(e0,e0),e0),
inference(rew,[status(thm),theory(equality)],[12,838]),
[iquote('2:Rew:12.0,838.0')] ).
cnf(992,plain,
equal(op(e3,e3),e0),
inference(mrr,[status(thm)],[413,991]),
[iquote('2:MRR:413.0,991.0')] ).
cnf(993,plain,
~ equal(op(e0,e3),e0),
inference(rew,[status(thm),theory(equality)],[992,54]),
[iquote('2:Rew:992.0,54.0')] ).
cnf(998,plain,
( equal(e1,e0)
| equal(op(e0,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[992,411]),
[iquote('2:Rew:992.0,411.0')] ).
cnf(1027,plain,
~ equal(op(e2,e1),e2),
inference(rew,[status(thm),theory(equality)],[16,897]),
[iquote('2:Rew:16.0,897.0')] ).
cnf(1029,plain,
~ equal(op(e0,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,905]),
[iquote('2:Rew:17.0,905.0')] ).
cnf(1036,plain,
equal(op(e0,e0),e1),
inference(mrr,[status(thm)],[998,1]),
[iquote('2:MRR:998.0,1.0')] ).
cnf(1042,plain,
~ equal(op(e0,e3),e1),
inference(rew,[status(thm),theory(equality)],[1036,74]),
[iquote('2:Rew:1036.0,74.0')] ).
cnf(1069,plain,
equal(op(e0,e1),e2),
inference(mrr,[status(thm)],[983,1027]),
[iquote('2:MRR:983.0,1027.0')] ).
cnf(1073,plain,
~ equal(op(e0,e3),e2),
inference(rew,[status(thm),theory(equality)],[1069,77]),
[iquote('2:Rew:1069.0,77.0')] ).
cnf(1128,plain,
( equal(e2,unit)
| equal(e2,unit)
| equal(op(e0,e2),unit) ),
inference(rew,[status(thm),theory(equality)],[810,929,969,15]),
[iquote('2:Rew:810.0,929.2,969.0,929.1,810.0,929.1,15.0,929.0')] ).
cnf(1129,plain,
( equal(e2,unit)
| equal(op(e0,e2),unit) ),
inference(obv,[status(thm),theory(equality)],[1128]),
[iquote('2:Obv:1128.0')] ).
cnf(1130,plain,
equal(op(e0,e2),unit),
inference(mrr,[status(thm)],[1129,812]),
[iquote('2:MRR:1129.0,812.0')] ).
cnf(1133,plain,
~ equal(op(e0,e3),unit),
inference(rew,[status(thm),theory(equality)],[1130,79]),
[iquote('2:Rew:1130.0,79.0')] ).
cnf(1184,plain,
$false,
inference(mrr,[status(thm)],[949,1029,993,1133,1073,1042]),
[iquote('2:MRR:949.0,949.1,949.2,949.3,949.4,1029.0,993.0,1133.0,1073.0,1042.0')] ).
cnf(1185,plain,
~ equal(e4,unit),
inference(spt,[spt(split,[position(s2sa)])],[1184,810]),
[iquote('2:Spt:1184.0,809.0,810.0')] ).
cnf(1186,plain,
( equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2s2)])],[809]),
[iquote('2:Spt:1184.0,809.1,809.2,809.3')] ).
cnf(1187,plain,
equal(e3,unit),
inference(spt,[spt(split,[position(s2s2s1)])],[1186]),
[iquote('3:Spt:1186.0')] ).
cnf(1189,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[1187,6]),
[iquote('3:Rew:1187.0,6.0')] ).
cnf(1190,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[1187,18]),
[iquote('3:Rew:1187.0,18.0')] ).
cnf(1218,plain,
~ equal(op(e0,e4),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[1187,81]),
[iquote('3:Rew:1187.0,81.0')] ).
cnf(1253,plain,
~ equal(op(e0,e4),op(unit,e4)),
inference(rew,[status(thm),theory(equality)],[1187,64]),
[iquote('3:Rew:1187.0,64.0')] ).
cnf(1263,plain,
~ equal(op(e1,e4),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[1187,91]),
[iquote('3:Rew:1187.0,91.0')] ).
cnf(1310,plain,
( equal(op(unit,unit),e1)
| equal(op(e0,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1187,411]),
[iquote('3:Rew:1187.0,411.0')] ).
cnf(1320,plain,
( equal(op(e1,e4),e1)
| equal(op(e1,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[1187,404]),
[iquote('3:Rew:1187.0,404.1')] ).
cnf(1333,plain,
( equal(op(e0,e4),e4)
| equal(op(e0,e4),e0)
| equal(op(e0,e4),unit)
| equal(op(e0,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[1187,407]),
[iquote('3:Rew:1187.0,407.2')] ).
cnf(1354,plain,
~ equal(op(e0,e4),e0),
inference(rew,[status(thm),theory(equality)],[12,1218]),
[iquote('3:Rew:12.0,1218.0')] ).
cnf(1384,plain,
~ equal(op(e0,e4),e4),
inference(rew,[status(thm),theory(equality)],[19,1253]),
[iquote('3:Rew:19.0,1253.0')] ).
cnf(1386,plain,
~ equal(op(e1,e4),e1),
inference(rew,[status(thm),theory(equality)],[14,1263]),
[iquote('3:Rew:14.0,1263.0')] ).
cnf(1445,plain,
( equal(e1,unit)
| equal(op(e0,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1190,1310]),
[iquote('3:Rew:1190.0,1310.0')] ).
cnf(1446,plain,
equal(op(e0,e0),e1),
inference(mrr,[status(thm)],[1445,1189]),
[iquote('3:MRR:1445.0,1189.0')] ).
cnf(1448,plain,
~ equal(op(e0,e4),e1),
inference(rew,[status(thm),theory(equality)],[1446,75]),
[iquote('3:Rew:1446.0,75.0')] ).
cnf(1455,plain,
equal(op(e1,e4),unit),
inference(mrr,[status(thm)],[1320,1386]),
[iquote('3:MRR:1320.0,1386.0')] ).
cnf(1460,plain,
~ equal(op(e0,e4),unit),
inference(rew,[status(thm),theory(equality)],[1455,62]),
[iquote('3:Rew:1455.0,62.0')] ).
cnf(1558,plain,
$false,
inference(mrr,[status(thm)],[1333,1384,1354,1460,1448]),
[iquote('3:MRR:1333.0,1333.1,1333.2,1333.3,1384.0,1354.0,1460.0,1448.0')] ).
cnf(1563,plain,
~ equal(e3,unit),
inference(spt,[spt(split,[position(s2s2sa)])],[1558,1187]),
[iquote('3:Spt:1558.0,1186.0,1187.0')] ).
cnf(1564,plain,
( equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2s2s2)])],[1186]),
[iquote('3:Spt:1558.0,1186.1,1186.2')] ).
cnf(1565,plain,
equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2s1)])],[1564]),
[iquote('4:Spt:1564.0')] ).
cnf(1566,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[1565,5]),
[iquote('4:Rew:1565.0,5.0')] ).
cnf(1580,plain,
~ equal(op(e0,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1565,23]),
[iquote('4:Rew:1565.0,23.0')] ).
cnf(1581,plain,
~ equal(op(e4,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1565,30]),
[iquote('4:Rew:1565.0,30.0')] ).
cnf(1593,plain,
~ equal(op(e1,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[1565,56]),
[iquote('4:Rew:1565.0,56.0')] ).
cnf(1594,plain,
~ equal(op(e4,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[1565,60]),
[iquote('4:Rew:1565.0,60.0')] ).
cnf(1596,plain,
( equal(op(e4,e3),e4)
| equal(op(e3,e3),e4)
| equal(op(unit,e3),e4)
| equal(op(e0,e3),e4) ),
inference(rew,[status(thm),theory(equality)],[1565,349]),
[iquote('4:Rew:1565.0,349.2')] ).
cnf(1640,plain,
~ equal(op(e4,e3),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1565,119]),
[iquote('4:Rew:1565.0,119.0')] ).
cnf(1681,plain,
( equal(op(e3,e3),e2)
| equal(op(e2,e3),e2)
| equal(op(e1,e3),unit)
| equal(op(e0,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[1565,353]),
[iquote('4:Rew:1565.0,353.2')] ).
cnf(1723,plain,
~ equal(op(e0,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1580]),
[iquote('4:Rew:11.0,1580.0')] ).
cnf(1724,plain,
equal(op(e3,e3),e0),
inference(mrr,[status(thm)],[413,1723]),
[iquote('4:MRR:413.0,1723.0')] ).
cnf(1731,plain,
~ equal(op(e4,e3),e0),
inference(rew,[status(thm),theory(equality)],[1724,61]),
[iquote('4:Rew:1724.0,61.0')] ).
cnf(1732,plain,
( equal(e1,e0)
| equal(op(e0,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1724,411]),
[iquote('4:Rew:1724.0,411.0')] ).
cnf(1736,plain,
( equal(op(e4,e0),e0)
| equal(op(e4,e1),e0) ),
inference(mrr,[status(thm)],[348,1731]),
[iquote('4:MRR:348.1,1731.0')] ).
cnf(1738,plain,
~ equal(op(e4,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1581]),
[iquote('4:Rew:11.0,1581.0')] ).
cnf(1744,plain,
~ equal(op(e1,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,1593]),
[iquote('4:Rew:17.0,1593.0')] ).
cnf(1745,plain,
( equal(op(e1,e4),e3)
| equal(op(e1,e0),e3) ),
inference(mrr,[status(thm)],[374,1744]),
[iquote('4:MRR:374.0,1744.0')] ).
cnf(1746,plain,
~ equal(op(e4,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,1594]),
[iquote('4:Rew:17.0,1594.0')] ).
cnf(1747,plain,
( equal(op(e4,e1),e3)
| equal(op(e4,e0),e3) ),
inference(mrr,[status(thm)],[340,1746]),
[iquote('4:MRR:340.0,1746.0')] ).
cnf(1769,plain,
~ equal(op(e4,e3),e4),
inference(rew,[status(thm),theory(equality)],[20,1640]),
[iquote('4:Rew:20.0,1640.0')] ).
cnf(1779,plain,
equal(op(e0,e0),e1),
inference(mrr,[status(thm)],[1732,1]),
[iquote('4:MRR:1732.0,1.0')] ).
cnf(1782,plain,
~ equal(op(e1,e0),e1),
inference(rew,[status(thm),theory(equality)],[1779,22]),
[iquote('4:Rew:1779.0,22.0')] ).
cnf(1787,plain,
( equal(op(e1,e4),e1)
| equal(op(e1,e3),e1) ),
inference(mrr,[status(thm)],[382,1782]),
[iquote('4:MRR:382.2,1782.0')] ).
cnf(1809,plain,
equal(op(e4,e1),e0),
inference(mrr,[status(thm)],[1736,1738]),
[iquote('4:MRR:1736.0,1738.0')] ).
cnf(1822,plain,
( equal(e3,e0)
| equal(op(e4,e0),e3) ),
inference(rew,[status(thm),theory(equality)],[1809,1747]),
[iquote('4:Rew:1809.0,1747.0')] ).
cnf(1823,plain,
equal(op(e4,e0),e3),
inference(mrr,[status(thm)],[1822,3]),
[iquote('4:MRR:1822.0,3.0')] ).
cnf(1830,plain,
~ equal(op(e1,e0),e3),
inference(rew,[status(thm),theory(equality)],[1823,28]),
[iquote('4:Rew:1823.0,28.0')] ).
cnf(1835,plain,
equal(op(e1,e4),e3),
inference(mrr,[status(thm)],[1745,1830]),
[iquote('4:MRR:1745.1,1830.0')] ).
cnf(1858,plain,
( equal(e3,e1)
| equal(op(e1,e3),e1) ),
inference(rew,[status(thm),theory(equality)],[1835,1787]),
[iquote('4:Rew:1835.0,1787.0')] ).
cnf(1859,plain,
equal(op(e1,e3),e1),
inference(mrr,[status(thm)],[1858,6]),
[iquote('4:MRR:1858.0,6.0')] ).
cnf(1942,plain,
( equal(op(e4,e3),e4)
| equal(e4,e0)
| equal(e4,e3)
| equal(op(e0,e3),e4) ),
inference(rew,[status(thm),theory(equality)],[17,1596,1724]),
[iquote('4:Rew:17.0,1596.2,1724.0,1596.1')] ).
cnf(1943,plain,
equal(op(e0,e3),e4),
inference(mrr,[status(thm)],[1942,1769,4,10]),
[iquote('4:MRR:1942.0,1942.1,1942.2,1769.0,4.0,10.0')] ).
cnf(1962,plain,
( equal(e0,unit)
| equal(e3,unit)
| equal(e1,unit)
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[1943,1681,1565,1859,17,1724]),
[iquote('4:Rew:1943.0,1681.3,1565.0,1681.3,1859.0,1681.2,17.0,1681.1,1565.0,1681.1,1724.0,1681.0,1565.0,1681.0')] ).
cnf(1963,plain,
$false,
inference(mrr,[status(thm)],[1962,808,1563,1566,1185]),
[iquote('4:MRR:1962.0,1962.1,1962.2,1962.3,808.0,1563.0,1566.0,1185.0')] ).
cnf(1964,plain,
~ equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2sa)])],[1963,1565]),
[iquote('4:Spt:1963.0,1564.0,1565.0')] ).
cnf(1965,plain,
equal(e1,unit),
inference(spt,[spt(split,[position(s2s2s2s2)])],[1564]),
[iquote('4:Spt:1963.0,1564.1')] ).
cnf(1972,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[1965,5]),
[iquote('4:Rew:1965.0,5.0')] ).
cnf(2002,plain,
~ equal(op(e2,e0),e2),
inference(rew,[status(thm),theory(equality)],[16,92,1965]),
[iquote('4:Rew:16.0,92.0,1965.0,92.0')] ).
cnf(2009,plain,
~ equal(op(e2,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,26,1965]),
[iquote('4:Rew:11.0,26.0,1965.0,26.0')] ).
cnf(2012,plain,
~ equal(op(e0,e0),e0),
inference(rew,[status(thm),theory(equality)],[12,72,1965]),
[iquote('4:Rew:12.0,72.0,1965.0,72.0')] ).
cnf(2017,plain,
~ equal(op(e4,e3),e4),
inference(rew,[status(thm),theory(equality)],[20,117,1965]),
[iquote('4:Rew:20.0,117.0,1965.0,117.0')] ).
cnf(2023,plain,
~ equal(op(e0,e4),e0),
inference(rew,[status(thm),theory(equality)],[12,78,1965]),
[iquote('4:Rew:12.0,78.0,1965.0,78.0')] ).
cnf(2060,plain,
equal(op(e3,e3),e0),
inference(mrr,[status(thm)],[413,2012]),
[iquote('4:MRR:413.0,2012.0')] ).
cnf(2064,plain,
~ equal(op(e3,e4),e0),
inference(rew,[status(thm),theory(equality)],[2060,111]),
[iquote('4:Rew:2060.0,111.0')] ).
cnf(2070,plain,
( equal(e0,unit)
| equal(op(e0,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[1965,411,2060]),
[iquote('4:Rew:1965.0,411.1,2060.0,411.0,1965.0,411.0')] ).
cnf(2071,plain,
equal(op(e0,e0),unit),
inference(mrr,[status(thm)],[2070,808]),
[iquote('4:MRR:2070.0,808.0')] ).
cnf(2073,plain,
~ equal(op(e2,e0),unit),
inference(rew,[status(thm),theory(equality)],[2071,23]),
[iquote('4:Rew:2071.0,23.0')] ).
cnf(2095,plain,
equal(op(e2,e4),e0),
inference(mrr,[status(thm)],[346,2023,2064]),
[iquote('4:MRR:346.0,346.1,2023.0,2064.0')] ).
cnf(2179,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e0)
| equal(op(e2,e0),e4)
| equal(op(e2,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[1965,403]),
[iquote('4:Rew:1965.0,403.3')] ).
cnf(2180,plain,
equal(op(e2,e0),e4),
inference(mrr,[status(thm)],[2179,2002,2009,2073]),
[iquote('4:MRR:2179.0,2179.1,2179.3,2002.0,2009.0,2073.0')] ).
cnf(2196,plain,
( equal(e2,unit)
| equal(e0,unit)
| equal(op(e2,e3),unit)
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[2180,368,1965,2095,16]),
[iquote('4:Rew:2180.0,368.3,1965.0,368.3,1965.0,368.2,2095.0,368.1,1965.0,368.1,16.0,368.0,1965.0,368.0')] ).
cnf(2197,plain,
equal(op(e2,e3),unit),
inference(mrr,[status(thm)],[2196,1972,808,1185]),
[iquote('4:MRR:2196.0,2196.1,2196.3,1972.0,808.0,1185.0')] ).
cnf(2212,plain,
( equal(op(e4,e3),e4)
| equal(e4,e0)
| equal(e4,unit)
| equal(op(e0,e3),e4) ),
inference(rew,[status(thm),theory(equality)],[2197,349,2060]),
[iquote('4:Rew:2197.0,349.2,2060.0,349.1')] ).
cnf(2213,plain,
equal(op(e0,e3),e4),
inference(mrr,[status(thm)],[2212,2017,4,1185]),
[iquote('4:MRR:2212.0,2212.1,2212.2,2017.0,4.0,1185.0')] ).
cnf(2265,plain,
( equal(e2,e0)
| equal(e2,unit)
| equal(e3,e2)
| equal(e4,e2) ),
inference(rew,[status(thm),theory(equality)],[2213,353,17,1965,2197,2060]),
[iquote('4:Rew:2213.0,353.3,17.0,353.2,1965.0,353.2,2197.0,353.1,2060.0,353.0')] ).
cnf(2266,plain,
$false,
inference(mrr,[status(thm)],[2265,2,1972,8,9]),
[iquote('4:MRR:2265.0,2265.1,2265.2,2265.3,2.0,1972.0,8.0,9.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : ALG064+1 : TPTP v8.1.0. Released v2.7.0.
% 0.07/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n022.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 12:13:05 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.37/0.57
% 0.37/0.57 SPASS V 3.9
% 0.37/0.57 SPASS beiseite: Proof found.
% 0.37/0.57 % SZS status Theorem
% 0.37/0.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.57 SPASS derived 1184 clauses, backtracked 914 clauses, performed 4 splits and kept 1510 clauses.
% 0.37/0.57 SPASS allocated 86259 KBytes.
% 0.37/0.57 SPASS spent 0:00:00.23 on the problem.
% 0.37/0.57 0:00:00.04 for the input.
% 0.37/0.57 0:00:00.06 for the FLOTTER CNF translation.
% 0.37/0.57 0:00:00.00 for inferences.
% 0.37/0.57 0:00:00.00 for the backtracking.
% 0.37/0.57 0:00:00.10 for the reduction.
% 0.37/0.57
% 0.37/0.57
% 0.37/0.57 Here is a proof with depth 4, length 421 :
% 0.37/0.57 % SZS output start Refutation
% See solution above
% 0.37/0.58 Formulae used in the proof : ax5 ax2 ax6 ax4 co1 ax3 ax1
% 0.37/0.58
%------------------------------------------------------------------------------