%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG067+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n026.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:12 EDT 2022
% Result : Theorem 0.47s 0.63s
% Output : Refutation 0.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 126
% Syntax : Number of clauses : 379 ( 209 unt; 105 nHn; 379 RR)
% Number of literals : 832 ( 0 equ; 239 neg)
% Maximal clause size : 25 ( 2 avg)
% Maximal term depth : 3 ( 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(2,axiom,
~ equal(e2,e0),
file('ALG067+1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(e3,e0),
file('ALG067+1.p',unknown),
[] ).
cnf(4,axiom,
~ equal(e4,e0),
file('ALG067+1.p',unknown),
[] ).
cnf(5,axiom,
~ equal(e2,e1),
file('ALG067+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e3,e1),
file('ALG067+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(e4,e1),
file('ALG067+1.p',unknown),
[] ).
cnf(8,axiom,
~ equal(e3,e2),
file('ALG067+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(e4,e2),
file('ALG067+1.p',unknown),
[] ).
cnf(10,axiom,
~ equal(e4,e3),
file('ALG067+1.p',unknown),
[] ).
cnf(11,axiom,
equal(op(unit,e0),e0),
file('ALG067+1.p',unknown),
[] ).
cnf(12,axiom,
equal(op(e0,unit),e0),
file('ALG067+1.p',unknown),
[] ).
cnf(13,axiom,
equal(op(unit,e1),e1),
file('ALG067+1.p',unknown),
[] ).
cnf(14,axiom,
equal(op(e1,unit),e1),
file('ALG067+1.p',unknown),
[] ).
cnf(15,axiom,
equal(op(unit,e2),e2),
file('ALG067+1.p',unknown),
[] ).
cnf(16,axiom,
equal(op(e2,unit),e2),
file('ALG067+1.p',unknown),
[] ).
cnf(17,axiom,
equal(op(unit,e3),e3),
file('ALG067+1.p',unknown),
[] ).
cnf(18,axiom,
equal(op(e3,unit),e3),
file('ALG067+1.p',unknown),
[] ).
cnf(20,axiom,
equal(op(e4,unit),e4),
file('ALG067+1.p',unknown),
[] ).
cnf(21,axiom,
equal(op(e4,e2),e1),
file('ALG067+1.p',unknown),
[] ).
cnf(22,axiom,
equal(op(e2,e4),e3),
file('ALG067+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ skC0
| equal(op(e0,e0),e0) ),
file('ALG067+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ skC1
| equal(op(e0,e0),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ skC2
| equal(op(e0,e0),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ skC3
| equal(op(e0,e0),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ skC3
| equal(op(e3,e3),e0) ),
file('ALG067+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ skC4
| equal(op(e0,e0),e4) ),
file('ALG067+1.p',unknown),
[] ).
cnf(33,axiom,
( ~ skC5
| equal(op(e0,e0),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ skC6
| equal(op(e1,e1),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ skC7
| equal(op(e2,e2),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(37,axiom,
( ~ skC8
| equal(op(e1,e1),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ skC9
| equal(op(e4,e4),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(43,axiom,
( ~ skC11
| equal(op(e2,e2),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ skC12
| equal(op(e2,e2),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ skC13
| equal(op(e2,e2),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ skC14
| equal(op(e4,e4),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ skC15
| equal(op(e3,e3),e0) ),
file('ALG067+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ skC15
| equal(op(e0,e0),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ skC16
| equal(op(e1,e1),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ skC17
| equal(op(e2,e2),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ skC18
| equal(op(e3,e3),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ skC19
| equal(op(e4,e4),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ skC20
| equal(op(e0,e0),e4) ),
file('ALG067+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ skC21
| equal(op(e4,e4),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(63,axiom,
( ~ skC22
| equal(op(e4,e4),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ skC23
| equal(op(e4,e4),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ equal(op(e0,e0),e0)
| ~ skC0 ),
file('ALG067+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ equal(op(e1,e1),e1)
| ~ skC6 ),
file('ALG067+1.p',unknown),
[] ).
cnf(77,axiom,
( ~ skC10
| ~ equal(op(e2,e0),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ equal(op(e2,e2),e2)
| ~ skC12 ),
file('ALG067+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ equal(op(e3,e3),e3)
| ~ skC18 ),
file('ALG067+1.p',unknown),
[] ).
cnf(91,axiom,
~ equal(op(e1,e0),op(e0,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(95,axiom,
~ equal(op(e2,e0),op(e1,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(96,axiom,
~ equal(op(e3,e0),op(e1,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(98,axiom,
~ equal(op(e3,e0),op(e2,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(106,axiom,
~ equal(op(e3,e1),op(e1,e1)),
file('ALG067+1.p',unknown),
[] ).
cnf(107,axiom,
~ equal(op(e4,e1),op(e1,e1)),
file('ALG067+1.p',unknown),
[] ).
cnf(109,axiom,
~ equal(op(e4,e1),op(e2,e1)),
file('ALG067+1.p',unknown),
[] ).
cnf(112,axiom,
~ equal(op(e2,e2),op(e0,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(119,axiom,
~ equal(op(e4,e2),op(e2,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(120,axiom,
~ equal(op(e4,e2),op(e3,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(121,axiom,
~ equal(op(e1,e3),op(e0,e3)),
file('ALG067+1.p',unknown),
[] ).
cnf(122,axiom,
~ equal(op(e2,e3),op(e0,e3)),
file('ALG067+1.p',unknown),
[] ).
cnf(124,axiom,
~ equal(op(e4,e3),op(e0,e3)),
file('ALG067+1.p',unknown),
[] ).
cnf(127,axiom,
~ equal(op(e4,e3),op(e1,e3)),
file('ALG067+1.p',unknown),
[] ).
cnf(128,axiom,
~ equal(op(e3,e3),op(e2,e3)),
file('ALG067+1.p',unknown),
[] ).
cnf(130,axiom,
~ equal(op(e4,e3),op(e3,e3)),
file('ALG067+1.p',unknown),
[] ).
cnf(134,axiom,
~ equal(op(e4,e4),op(e0,e4)),
file('ALG067+1.p',unknown),
[] ).
cnf(135,axiom,
~ equal(op(e2,e4),op(e1,e4)),
file('ALG067+1.p',unknown),
[] ).
cnf(138,axiom,
~ equal(op(e3,e4),op(e2,e4)),
file('ALG067+1.p',unknown),
[] ).
cnf(139,axiom,
~ equal(op(e4,e4),op(e2,e4)),
file('ALG067+1.p',unknown),
[] ).
cnf(143,axiom,
~ equal(op(e0,e3),op(e0,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(144,axiom,
~ equal(op(e0,e4),op(e0,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(148,axiom,
~ equal(op(e0,e3),op(e0,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(149,axiom,
~ equal(op(e0,e4),op(e0,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(150,axiom,
~ equal(op(e0,e4),op(e0,e3)),
file('ALG067+1.p',unknown),
[] ).
cnf(161,axiom,
~ equal(op(e2,e1),op(e2,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(164,axiom,
~ equal(op(e2,e4),op(e2,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(166,axiom,
~ equal(op(e2,e3),op(e2,e1)),
file('ALG067+1.p',unknown),
[] ).
cnf(167,axiom,
~ equal(op(e2,e4),op(e2,e1)),
file('ALG067+1.p',unknown),
[] ).
cnf(168,axiom,
~ equal(op(e2,e3),op(e2,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(169,axiom,
~ equal(op(e2,e4),op(e2,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(171,axiom,
~ equal(op(e3,e1),op(e3,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(172,axiom,
~ equal(op(e3,e2),op(e3,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(175,axiom,
~ equal(op(e3,e2),op(e3,e1)),
file('ALG067+1.p',unknown),
[] ).
cnf(178,axiom,
~ equal(op(e3,e3),op(e3,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(181,axiom,
~ equal(op(e4,e1),op(e4,e0)),
file('ALG067+1.p',unknown),
[] ).
cnf(185,axiom,
~ equal(op(e4,e2),op(e4,e1)),
file('ALG067+1.p',unknown),
[] ).
cnf(186,axiom,
~ equal(op(e4,e3),op(e4,e1)),
file('ALG067+1.p',unknown),
[] ).
cnf(189,axiom,
~ equal(op(e4,e4),op(e4,e2)),
file('ALG067+1.p',unknown),
[] ).
cnf(190,axiom,
~ equal(op(e4,e4),op(e4,e3)),
file('ALG067+1.p',unknown),
[] ).
cnf(191,axiom,
equal(op(op(e4,e2),op(e4,e2)),e0),
file('ALG067+1.p',unknown),
[] ).
cnf(193,axiom,
( ~ equal(op(e0,e0),e2)
| equal(op(e0,e2),e0) ),
file('ALG067+1.p',unknown),
[] ).
cnf(194,axiom,
( ~ equal(op(e0,e0),e3)
| equal(op(e0,e3),e0) ),
file('ALG067+1.p',unknown),
[] ).
cnf(195,axiom,
( ~ equal(op(e0,e0),e4)
| equal(op(e0,e4),e0) ),
file('ALG067+1.p',unknown),
[] ).
cnf(196,axiom,
( ~ equal(op(e1,e1),e0)
| equal(op(e1,e0),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(203,axiom,
( ~ equal(op(e2,e2),e4)
| equal(op(e2,e4),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(204,axiom,
( ~ equal(op(e3,e3),e0)
| equal(op(e3,e0),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(205,axiom,
( ~ equal(op(e3,e3),e1)
| equal(op(e3,e1),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(206,axiom,
( ~ equal(op(e3,e3),e2)
| equal(op(e3,e2),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(207,axiom,
( ~ equal(op(e3,e3),e4)
| equal(op(e3,e4),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(210,axiom,
( ~ equal(op(e4,e4),e2)
| equal(op(e4,e2),e4) ),
file('ALG067+1.p',unknown),
[] ).
cnf(212,axiom,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit)
| equal(e0,unit) ),
file('ALG067+1.p',unknown),
[] ).
cnf(218,axiom,
( equal(op(e4,e0),e2)
| equal(op(e4,e1),e2)
| equal(op(e4,e2),e2)
| equal(op(e4,e3),e2)
| equal(op(e4,e4),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(228,axiom,
( equal(op(e3,e3),e2)
| equal(op(e3,e2),e2)
| equal(op(e3,e4),e2)
| equal(op(e3,e1),e2)
| equal(op(e3,e0),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(230,axiom,
( equal(op(e3,e0),e1)
| equal(op(e3,e1),e1)
| equal(op(e3,e2),e1)
| equal(op(e3,e3),e1)
| equal(op(e3,e4),e1) ),
file('ALG067+1.p',unknown),
[] ).
cnf(232,axiom,
( equal(op(e3,e0),e0)
| equal(op(e3,e1),e0)
| equal(op(e3,e2),e0)
| equal(op(e3,e3),e0)
| equal(op(e3,e4),e0) ),
file('ALG067+1.p',unknown),
[] ).
cnf(233,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('ALG067+1.p',unknown),
[] ).
cnf(235,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('ALG067+1.p',unknown),
[] ).
cnf(240,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('ALG067+1.p',unknown),
[] ).
cnf(243,axiom,
( equal(op(e0,e1),e4)
| equal(op(e1,e1),e4)
| equal(op(e2,e1),e4)
| equal(op(e3,e1),e4)
| equal(op(e4,e1),e4) ),
file('ALG067+1.p',unknown),
[] ).
cnf(245,axiom,
( equal(op(e0,e1),e3)
| equal(op(e1,e1),e3)
| equal(op(e2,e1),e3)
| equal(op(e3,e1),e3)
| equal(op(e4,e1),e3) ),
file('ALG067+1.p',unknown),
[] ).
cnf(246,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('ALG067+1.p',unknown),
[] ).
cnf(247,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('ALG067+1.p',unknown),
[] ).
cnf(248,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('ALG067+1.p',unknown),
[] ).
cnf(253,axiom,
( equal(op(e0,e0),e4)
| equal(op(e1,e0),e4)
| equal(op(e2,e0),e4)
| equal(op(e3,e0),e4)
| equal(op(e4,e0),e4) ),
file('ALG067+1.p',unknown),
[] ).
cnf(255,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('ALG067+1.p',unknown),
[] ).
cnf(257,axiom,
( equal(op(e0,e0),e2)
| equal(op(e1,e0),e2)
| equal(op(e2,e0),e2)
| equal(op(e3,e0),e2)
| equal(op(e4,e0),e2) ),
file('ALG067+1.p',unknown),
[] ).
cnf(263,axiom,
( equal(op(e4,e4),e0)
| equal(op(e4,e4),e1)
| equal(op(e4,e4),e2)
| equal(op(e4,e4),e3)
| equal(op(e4,e4),e4) ),
file('ALG067+1.p',unknown),
[] ).
cnf(266,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('ALG067+1.p',unknown),
[] ).
cnf(269,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('ALG067+1.p',unknown),
[] ).
cnf(275,axiom,
( equal(op(e2,e2),e0)
| equal(op(e2,e2),e1)
| equal(op(e2,e2),e2)
| equal(op(e2,e2),e3)
| equal(op(e2,e2),e4) ),
file('ALG067+1.p',unknown),
[] ).
cnf(277,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('ALG067+1.p',unknown),
[] ).
cnf(284,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('ALG067+1.p',unknown),
[] ).
cnf(287,axiom,
( equal(op(e0,e0),e0)
| equal(op(e0,e0),e1)
| equal(op(e0,e0),e2)
| equal(op(e0,e0),e3)
| equal(op(e0,e0),e4) ),
file('ALG067+1.p',unknown),
[] ).
cnf(288,axiom,
( equal(op(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('ALG067+1.p',unknown),
[] ).
cnf(289,axiom,
( ~ equal(op(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('ALG067+1.p',unknown),
[] ).
cnf(290,plain,
~ equal(op(e4,e4),e1),
inference(rew,[status(thm),theory(equality)],[21,189]),
[iquote('0:Rew:21.0,189.0')] ).
cnf(291,plain,
~ skC21,
inference(mrr,[status(thm)],[61,290]),
[iquote('0:MRR:61.1,290.0')] ).
cnf(292,plain,
~ skC9,
inference(mrr,[status(thm)],[40,290]),
[iquote('0:MRR:40.1,290.0')] ).
cnf(294,plain,
~ equal(op(e4,e1),e1),
inference(rew,[status(thm),theory(equality)],[21,185]),
[iquote('0:Rew:21.0,185.0')] ).
cnf(297,plain,
~ equal(op(e2,e2),e3),
inference(rew,[status(thm),theory(equality)],[22,169]),
[iquote('0:Rew:22.0,169.0')] ).
cnf(298,plain,
~ skC17,
inference(mrr,[status(thm)],[55,297]),
[iquote('0:MRR:55.1,297.0')] ).
cnf(299,plain,
~ skC13,
inference(mrr,[status(thm)],[46,297]),
[iquote('0:MRR:46.1,297.0')] ).
cnf(300,plain,
~ equal(op(e2,e1),e3),
inference(rew,[status(thm),theory(equality)],[22,167]),
[iquote('0:Rew:22.0,167.0')] ).
cnf(301,plain,
~ equal(op(e2,e0),e3),
inference(rew,[status(thm),theory(equality)],[22,164]),
[iquote('0:Rew:22.0,164.0')] ).
cnf(302,plain,
~ equal(op(e4,e4),e3),
inference(rew,[status(thm),theory(equality)],[22,139]),
[iquote('0:Rew:22.0,139.0')] ).
cnf(303,plain,
~ skC23,
inference(mrr,[status(thm)],[65,302]),
[iquote('0:MRR:65.1,302.0')] ).
cnf(304,plain,
~ skC19,
inference(mrr,[status(thm)],[58,302]),
[iquote('0:MRR:58.1,302.0')] ).
cnf(305,plain,
~ equal(op(e3,e4),e3),
inference(rew,[status(thm),theory(equality)],[22,138]),
[iquote('0:Rew:22.0,138.0')] ).
cnf(306,plain,
~ equal(op(e1,e4),e3),
inference(rew,[status(thm),theory(equality)],[22,135]),
[iquote('0:Rew:22.0,135.0')] ).
cnf(308,plain,
~ equal(op(e3,e2),e1),
inference(rew,[status(thm),theory(equality)],[21,120]),
[iquote('0:Rew:21.0,120.0')] ).
cnf(309,plain,
~ equal(op(e2,e2),e1),
inference(rew,[status(thm),theory(equality)],[21,119]),
[iquote('0:Rew:21.0,119.0')] ).
cnf(310,plain,
~ skC11,
inference(mrr,[status(thm)],[43,309]),
[iquote('0:MRR:43.1,309.0')] ).
cnf(311,plain,
~ skC7,
inference(mrr,[status(thm)],[36,309]),
[iquote('0:MRR:36.1,309.0')] ).
cnf(315,plain,
( ~ equal(e3,e3)
| ~ skC18 ),
inference(rew,[status(thm),theory(equality)],[56,85]),
[iquote('0:Rew:56.1,85.0')] ).
cnf(316,plain,
~ skC18,
inference(obv,[status(thm),theory(equality)],[315]),
[iquote('0:Obv:315.0')] ).
cnf(318,plain,
( ~ equal(e2,e2)
| ~ skC12 ),
inference(rew,[status(thm),theory(equality)],[45,79]),
[iquote('0:Rew:45.1,79.0')] ).
cnf(319,plain,
~ skC12,
inference(obv,[status(thm),theory(equality)],[318]),
[iquote('0:Obv:318.0')] ).
cnf(320,plain,
( ~ equal(e1,e1)
| ~ skC6 ),
inference(rew,[status(thm),theory(equality)],[34,73]),
[iquote('0:Rew:34.1,73.0')] ).
cnf(321,plain,
~ skC6,
inference(obv,[status(thm),theory(equality)],[320]),
[iquote('0:Obv:320.0')] ).
cnf(322,plain,
( ~ equal(e0,e0)
| ~ skC0 ),
inference(rew,[status(thm),theory(equality)],[23,67]),
[iquote('0:Rew:23.1,67.0')] ).
cnf(323,plain,
~ skC0,
inference(obv,[status(thm),theory(equality)],[322]),
[iquote('0:Obv:322.0')] ).
cnf(324,plain,
equal(op(e1,e1),e0),
inference(rew,[status(thm),theory(equality)],[21,191]),
[iquote('0:Rew:21.0,191.0')] ).
cnf(325,plain,
( ~ skC8
| equal(e3,e0) ),
inference(rew,[status(thm),theory(equality)],[324,37]),
[iquote('0:Rew:324.0,37.1')] ).
cnf(326,plain,
( ~ skC16
| equal(e3,e0) ),
inference(rew,[status(thm),theory(equality)],[324,53]),
[iquote('0:Rew:324.0,53.1')] ).
cnf(331,plain,
~ equal(op(e4,e1),e0),
inference(rew,[status(thm),theory(equality)],[324,107]),
[iquote('0:Rew:324.0,107.0')] ).
cnf(332,plain,
~ equal(op(e3,e1),e0),
inference(rew,[status(thm),theory(equality)],[324,106]),
[iquote('0:Rew:324.0,106.0')] ).
cnf(335,plain,
~ skC8,
inference(mrr,[status(thm)],[325,3]),
[iquote('0:MRR:325.1,3.0')] ).
cnf(336,plain,
~ skC16,
inference(mrr,[status(thm)],[326,3]),
[iquote('0:MRR:326.1,3.0')] ).
cnf(337,plain,
( ~ equal(op(e4,e4),e2)
| equal(e4,e1) ),
inference(rew,[status(thm),theory(equality)],[21,210]),
[iquote('0:Rew:21.0,210.1')] ).
cnf(338,plain,
~ equal(op(e4,e4),e2),
inference(mrr,[status(thm)],[337,7]),
[iquote('0:MRR:337.1,7.0')] ).
cnf(339,plain,
~ skC22,
inference(mrr,[status(thm)],[63,338]),
[iquote('0:MRR:63.1,338.0')] ).
cnf(340,plain,
~ skC14,
inference(mrr,[status(thm)],[49,338]),
[iquote('0:MRR:49.1,338.0')] ).
cnf(341,plain,
~ equal(op(e3,e3),e4),
inference(mrr,[status(thm)],[207,305]),
[iquote('0:MRR:207.1,305.0')] ).
cnf(342,plain,
( ~ equal(op(e2,e2),e4)
| equal(e3,e2) ),
inference(rew,[status(thm),theory(equality)],[22,203]),
[iquote('0:Rew:22.0,203.1')] ).
cnf(343,plain,
~ equal(op(e2,e2),e4),
inference(mrr,[status(thm)],[342,8]),
[iquote('0:MRR:342.1,8.0')] ).
cnf(347,plain,
( ~ equal(e0,e0)
| equal(op(e1,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[324,196]),
[iquote('0:Rew:324.0,196.0')] ).
cnf(348,plain,
equal(op(e1,e0),e1),
inference(obv,[status(thm),theory(equality)],[347]),
[iquote('0:Obv:347.0')] ).
cnf(353,plain,
~ equal(op(e3,e0),e1),
inference(rew,[status(thm),theory(equality)],[348,96]),
[iquote('0:Rew:348.0,96.0')] ).
cnf(354,plain,
~ equal(op(e2,e0),e1),
inference(rew,[status(thm),theory(equality)],[348,95]),
[iquote('0:Rew:348.0,95.0')] ).
cnf(355,plain,
~ equal(op(e0,e0),e1),
inference(rew,[status(thm),theory(equality)],[348,91]),
[iquote('0:Rew:348.0,91.0')] ).
cnf(358,plain,
~ skC5,
inference(mrr,[status(thm)],[33,355]),
[iquote('0:MRR:33.1,355.0')] ).
cnf(359,plain,
~ skC1,
inference(mrr,[status(thm)],[24,355]),
[iquote('0:MRR:24.1,355.0')] ).
cnf(369,plain,
( equal(op(e4,e0),e2)
| equal(op(e4,e1),e2)
| equal(e2,e1)
| equal(op(e4,e3),e2)
| equal(op(e4,e4),e2) ),
inference(rew,[status(thm),theory(equality)],[21,218]),
[iquote('0:Rew:21.0,218.2')] ).
cnf(370,plain,
( equal(op(e4,e3),e2)
| equal(op(e4,e1),e2)
| equal(op(e4,e0),e2) ),
inference(mrr,[status(thm)],[369,5,338]),
[iquote('0:MRR:369.2,369.4,5.0,338.0')] ).
cnf(382,plain,
( equal(op(e3,e3),e1)
| equal(op(e3,e1),e1)
| equal(op(e3,e4),e1) ),
inference(mrr,[status(thm)],[230,353,308]),
[iquote('0:MRR:230.0,230.2,353.0,308.0')] ).
cnf(384,plain,
( equal(op(e3,e3),e0)
| equal(op(e3,e0),e0)
| equal(op(e3,e4),e0)
| equal(op(e3,e2),e0) ),
inference(mrr,[status(thm)],[232,332]),
[iquote('0:MRR:232.1,332.0')] ).
cnf(385,plain,
( equal(op(e0,e2),e4)
| equal(op(e1,e2),e4)
| equal(op(e2,e2),e4)
| equal(op(e3,e2),e4)
| equal(e4,e1) ),
inference(rew,[status(thm),theory(equality)],[21,233]),
[iquote('0:Rew:21.0,233.4')] ).
cnf(386,plain,
( equal(op(e3,e2),e4)
| equal(op(e1,e2),e4)
| equal(op(e0,e2),e4) ),
inference(mrr,[status(thm)],[385,343,7]),
[iquote('0:MRR:385.2,385.4,343.0,7.0')] ).
cnf(389,plain,
( equal(op(e0,e2),e3)
| equal(op(e1,e2),e3)
| equal(op(e2,e2),e3)
| equal(op(e3,e2),e3)
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[21,235]),
[iquote('0:Rew:21.0,235.4')] ).
cnf(390,plain,
( equal(op(e3,e2),e3)
| equal(op(e1,e2),e3)
| equal(op(e0,e2),e3) ),
inference(mrr,[status(thm)],[389,297,6]),
[iquote('0:MRR:389.2,389.4,297.0,6.0')] ).
cnf(395,plain,
( equal(op(e2,e0),e1)
| equal(op(e2,e1),e1)
| equal(op(e2,e2),e1)
| equal(op(e2,e3),e1)
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[22,240]),
[iquote('0:Rew:22.0,240.4')] ).
cnf(396,plain,
( equal(op(e2,e1),e1)
| equal(op(e2,e3),e1) ),
inference(mrr,[status(thm)],[395,354,309,6]),
[iquote('0:MRR:395.0,395.2,395.4,354.0,309.0,6.0')] ).
cnf(401,plain,
( equal(op(e0,e1),e4)
| equal(e4,e0)
| equal(op(e2,e1),e4)
| equal(op(e3,e1),e4)
| equal(op(e4,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[324,243]),
[iquote('0:Rew:324.0,243.1')] ).
cnf(402,plain,
( equal(op(e4,e1),e4)
| equal(op(e3,e1),e4)
| equal(op(e2,e1),e4)
| equal(op(e0,e1),e4) ),
inference(mrr,[status(thm)],[401,4]),
[iquote('0:MRR:401.1,4.0')] ).
cnf(405,plain,
( equal(op(e0,e1),e3)
| equal(e3,e0)
| equal(op(e2,e1),e3)
| equal(op(e3,e1),e3)
| equal(op(e4,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[324,245]),
[iquote('0:Rew:324.0,245.1')] ).
cnf(406,plain,
( equal(op(e3,e1),e3)
| equal(op(e4,e1),e3)
| equal(op(e0,e1),e3) ),
inference(mrr,[status(thm)],[405,3,300]),
[iquote('0:MRR:405.1,405.2,3.0,300.0')] ).
cnf(407,plain,
( equal(e3,e1)
| equal(e3,e0)
| equal(op(e1,e2),e3)
| equal(op(e1,e3),e3)
| equal(op(e1,e4),e3) ),
inference(rew,[status(thm),theory(equality)],[324,246,348]),
[iquote('0:Rew:324.0,246.1,348.0,246.0')] ).
cnf(408,plain,
( equal(op(e1,e3),e3)
| equal(op(e1,e2),e3) ),
inference(mrr,[status(thm)],[407,6,3,306]),
[iquote('0:MRR:407.0,407.1,407.4,6.0,3.0,306.0')] ).
cnf(409,plain,
( equal(op(e0,e1),e2)
| equal(e2,e0)
| equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(e4,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[324,247]),
[iquote('0:Rew:324.0,247.1')] ).
cnf(410,plain,
( equal(op(e2,e1),e2)
| equal(op(e4,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(e0,e1),e2) ),
inference(mrr,[status(thm)],[409,2]),
[iquote('0:MRR:409.1,2.0')] ).
cnf(411,plain,
( equal(e2,e1)
| equal(e2,e0)
| equal(op(e1,e2),e2)
| equal(op(e1,e3),e2)
| equal(op(e1,e4),e2) ),
inference(rew,[status(thm),theory(equality)],[324,248,348]),
[iquote('0:Rew:324.0,248.1,348.0,248.0')] ).
cnf(412,plain,
( equal(op(e1,e2),e2)
| equal(op(e1,e4),e2)
| equal(op(e1,e3),e2) ),
inference(mrr,[status(thm)],[411,5,2]),
[iquote('0:MRR:411.0,411.1,5.0,2.0')] ).
cnf(415,plain,
( equal(op(e0,e0),e4)
| equal(e4,e1)
| equal(op(e2,e0),e4)
| equal(op(e3,e0),e4)
| equal(op(e4,e0),e4) ),
inference(rew,[status(thm),theory(equality)],[348,253]),
[iquote('0:Rew:348.0,253.1')] ).
cnf(416,plain,
( equal(op(e4,e0),e4)
| equal(op(e0,e0),e4)
| equal(op(e3,e0),e4)
| equal(op(e2,e0),e4) ),
inference(mrr,[status(thm)],[415,7]),
[iquote('0:MRR:415.1,7.0')] ).
cnf(417,plain,
( equal(op(e0,e0),e3)
| equal(e3,e1)
| equal(op(e2,e0),e3)
| equal(op(e3,e0),e3)
| equal(op(e4,e0),e3) ),
inference(rew,[status(thm),theory(equality)],[348,255]),
[iquote('0:Rew:348.0,255.1')] ).
cnf(418,plain,
( equal(op(e3,e0),e3)
| equal(op(e0,e0),e3)
| equal(op(e4,e0),e3) ),
inference(mrr,[status(thm)],[417,6,301]),
[iquote('0:MRR:417.1,417.2,6.0,301.0')] ).
cnf(420,plain,
( equal(op(e0,e0),e2)
| equal(e2,e1)
| equal(op(e2,e0),e2)
| equal(op(e3,e0),e2)
| equal(op(e4,e0),e2) ),
inference(rew,[status(thm),theory(equality)],[348,257]),
[iquote('0:Rew:348.0,257.1')] ).
cnf(421,plain,
( equal(op(e2,e0),e2)
| equal(op(e0,e0),e2)
| equal(op(e4,e0),e2)
| equal(op(e3,e0),e2) ),
inference(mrr,[status(thm)],[420,5]),
[iquote('0:MRR:420.1,5.0')] ).
cnf(426,plain,
( equal(op(e4,e4),e4)
| equal(op(e4,e4),e0) ),
inference(mrr,[status(thm)],[263,290,338,302]),
[iquote('0:MRR:263.1,263.2,263.3,290.0,338.0,302.0')] ).
cnf(428,plain,
( equal(op(e4,e1),e4)
| equal(op(e4,e1),e3)
| equal(op(e4,e1),e2) ),
inference(mrr,[status(thm)],[266,331,294]),
[iquote('0:MRR:266.0,266.1,331.0,294.0')] ).
cnf(431,plain,
( equal(op(e3,e3),e3)
| equal(op(e3,e3),e2)
| equal(op(e3,e3),e1)
| equal(op(e3,e3),e0) ),
inference(mrr,[status(thm)],[269,341]),
[iquote('0:MRR:269.4,341.0')] ).
cnf(436,plain,
( equal(op(e2,e2),e2)
| equal(op(e2,e2),e0) ),
inference(mrr,[status(thm)],[275,309,297,343]),
[iquote('0:MRR:275.1,275.3,275.4,309.0,297.0,343.0')] ).
cnf(438,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e0)
| equal(op(e2,e0),e4) ),
inference(mrr,[status(thm)],[277,354,301]),
[iquote('0:MRR:277.1,277.3,354.0,301.0')] ).
cnf(445,plain,
( equal(op(e0,e0),e0)
| equal(op(e0,e0),e4)
| equal(op(e0,e0),e3)
| equal(op(e0,e0),e2) ),
inference(mrr,[status(thm)],[287,355]),
[iquote('0:MRR:287.1,355.0')] ).
cnf(446,plain,
( equal(op(e4,e4),e4)
| skC2
| skC3
| skC4
| skC10
| skC15
| skC20 ),
inference(mrr,[status(thm)],[288,323,359,358,321,311,335,292,310,319,299,340,336,298,316,304,291,339,303]),
[iquote('0:MRR:288.1,288.2,288.6,288.7,288.8,288.9,288.10,288.12,288.13,288.14,288.15,288.17,288.18,288.19,288.20,288.22,288.23,288.24,323.0,359.0,358.0,321.0,311.0,335.0,292.0,310.0,319.0,299.0,340.0,336.0,298.0,316.0,304.0,291.0,339.0,303.0')] ).
cnf(447,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)],[446,289]),
[iquote('0:Rew:446.0,289.0')] ).
cnf(448,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)],[447]),
[iquote('0:Obv:447.0')] ).
cnf(449,plain,
( skC20
| skC15
| skC10
| skC4
| skC3
| skC2 ),
inference(mrr,[status(thm)],[448,323,359,358,321,311,335,292,310,319,299,340,336,298,316,304,291,339,303]),
[iquote('0:MRR:448.0,448.1,448.5,448.6,448.7,448.8,448.9,448.11,448.12,448.13,448.14,448.16,448.17,448.18,448.19,448.21,448.22,448.23,323.0,359.0,358.0,321.0,311.0,335.0,292.0,310.0,319.0,299.0,340.0,336.0,298.0,316.0,304.0,291.0,339.0,303.0')] ).
cnf(450,plain,
equal(e0,unit),
inference(spt,[spt(split,[position(s1)])],[212]),
[iquote('1:Spt:212.4')] ).
cnf(455,plain,
( ~ skC4
| equal(op(unit,unit),e4) ),
inference(rew,[status(thm),theory(equality)],[450,30]),
[iquote('1:Rew:450.0,30.1')] ).
cnf(456,plain,
( ~ skC20
| equal(op(unit,unit),e4) ),
inference(rew,[status(thm),theory(equality)],[450,60]),
[iquote('1:Rew:450.0,60.1')] ).
cnf(460,plain,
( ~ skC3
| equal(op(unit,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[450,28]),
[iquote('1:Rew:450.0,28.1')] ).
cnf(461,plain,
( ~ skC15
| equal(op(unit,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[450,51]),
[iquote('1:Rew:450.0,51.1')] ).
cnf(465,plain,
( ~ skC2
| equal(op(unit,unit),e2) ),
inference(rew,[status(thm),theory(equality)],[450,26]),
[iquote('1:Rew:450.0,26.1')] ).
cnf(510,plain,
( ~ skC10
| ~ equal(op(e2,unit),e2) ),
inference(rew,[status(thm),theory(equality)],[450,77]),
[iquote('1:Rew:450.0,77.1')] ).
cnf(573,plain,
~ equal(e4,unit),
inference(rew,[status(thm),theory(equality)],[450,4]),
[iquote('1:Rew:450.0,4.0')] ).
cnf(574,plain,
~ equal(e3,unit),
inference(rew,[status(thm),theory(equality)],[450,3]),
[iquote('1:Rew:450.0,3.0')] ).
cnf(575,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[450,2]),
[iquote('1:Rew:450.0,2.0')] ).
cnf(577,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[450,12]),
[iquote('1:Rew:450.0,12.0')] ).
cnf(596,plain,
( ~ skC4
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[577,455]),
[iquote('1:Rew:577.0,455.1')] ).
cnf(597,plain,
~ skC4,
inference(mrr,[status(thm)],[596,573]),
[iquote('1:MRR:596.1,573.0')] ).
cnf(598,plain,
( skC20
| skC15
| skC10
| skC3
| skC2 ),
inference(mrr,[status(thm)],[449,597]),
[iquote('1:MRR:449.3,597.0')] ).
cnf(599,plain,
( ~ skC20
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[577,456]),
[iquote('1:Rew:577.0,456.1')] ).
cnf(600,plain,
~ skC20,
inference(mrr,[status(thm)],[599,573]),
[iquote('1:MRR:599.1,573.0')] ).
cnf(601,plain,
( skC15
| skC10
| skC3
| skC2 ),
inference(mrr,[status(thm)],[598,600]),
[iquote('1:MRR:598.0,600.0')] ).
cnf(602,plain,
( ~ skC3
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[577,460]),
[iquote('1:Rew:577.0,460.1')] ).
cnf(603,plain,
~ skC3,
inference(mrr,[status(thm)],[602,574]),
[iquote('1:MRR:602.1,574.0')] ).
cnf(604,plain,
( skC15
| skC10
| skC2 ),
inference(mrr,[status(thm)],[601,603]),
[iquote('1:MRR:601.2,603.0')] ).
cnf(605,plain,
( ~ skC15
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[577,461]),
[iquote('1:Rew:577.0,461.1')] ).
cnf(606,plain,
~ skC15,
inference(mrr,[status(thm)],[605,574]),
[iquote('1:MRR:605.1,574.0')] ).
cnf(607,plain,
( skC10
| skC2 ),
inference(mrr,[status(thm)],[604,606]),
[iquote('1:MRR:604.0,606.0')] ).
cnf(608,plain,
( ~ skC2
| equal(e2,unit) ),
inference(rew,[status(thm),theory(equality)],[577,465]),
[iquote('1:Rew:577.0,465.1')] ).
cnf(609,plain,
~ skC2,
inference(mrr,[status(thm)],[608,575]),
[iquote('1:MRR:608.1,575.0')] ).
cnf(610,plain,
skC10,
inference(mrr,[status(thm)],[607,609]),
[iquote('1:MRR:607.1,609.0')] ).
cnf(636,plain,
( ~ skC10
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[16,510]),
[iquote('1:Rew:16.0,510.1')] ).
cnf(637,plain,
~ skC10,
inference(obv,[status(thm),theory(equality)],[636]),
[iquote('1:Obv:636.1')] ).
cnf(638,plain,
$false,
inference(mrr,[status(thm)],[637,610]),
[iquote('1:MRR:637.0,610.0')] ).
cnf(778,plain,
~ equal(e0,unit),
inference(spt,[spt(split,[position(sa)])],[638,450]),
[iquote('1:Spt:638.0,212.4,450.0')] ).
cnf(779,plain,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2)])],[212]),
[iquote('1:Spt:638.0,212.0,212.1,212.2,212.3')] ).
cnf(780,plain,
equal(e4,unit),
inference(spt,[spt(split,[position(s2s1)])],[779]),
[iquote('2:Spt:779.0')] ).
cnf(792,plain,
~ equal(op(e2,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[780,109]),
[iquote('2:Rew:780.0,109.0')] ).
cnf(804,plain,
( equal(op(e1,e2),e2)
| equal(op(e1,unit),e2)
| equal(op(e1,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[780,412]),
[iquote('2:Rew:780.0,412.1')] ).
cnf(814,plain,
~ equal(op(e0,e2),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[780,149]),
[iquote('2:Rew:780.0,149.0')] ).
cnf(816,plain,
~ equal(op(e0,e0),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[780,144]),
[iquote('2:Rew:780.0,144.0')] ).
cnf(817,plain,
~ equal(op(e0,e3),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[780,150]),
[iquote('2:Rew:780.0,150.0')] ).
cnf(856,plain,
~ equal(op(e0,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[780,124]),
[iquote('2:Rew:780.0,124.0')] ).
cnf(860,plain,
~ equal(op(e1,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[780,127]),
[iquote('2:Rew:780.0,127.0')] ).
cnf(869,plain,
( equal(op(e0,e0),e0)
| equal(op(e0,e0),unit)
| equal(op(e0,e0),e3)
| equal(op(e0,e0),e2) ),
inference(rew,[status(thm),theory(equality)],[780,445]),
[iquote('2:Rew:780.0,445.1')] ).
cnf(891,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)],[780,284]),
[iquote('2:Rew:780.0,284.2')] ).
cnf(920,plain,
~ equal(op(e2,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,792]),
[iquote('2:Rew:13.0,792.0')] ).
cnf(921,plain,
equal(op(e2,e3),e1),
inference(mrr,[status(thm)],[396,920]),
[iquote('2:MRR:396.0,920.0')] ).
cnf(923,plain,
~ equal(op(e0,e3),e1),
inference(rew,[status(thm),theory(equality)],[921,122]),
[iquote('2:Rew:921.0,122.0')] ).
cnf(936,plain,
~ equal(op(e0,e2),e0),
inference(rew,[status(thm),theory(equality)],[12,814]),
[iquote('2:Rew:12.0,814.0')] ).
cnf(937,plain,
~ equal(op(e0,e0),e2),
inference(mrr,[status(thm)],[193,936]),
[iquote('2:MRR:193.1,936.0')] ).
cnf(944,plain,
~ equal(op(e0,e0),e0),
inference(rew,[status(thm),theory(equality)],[12,816]),
[iquote('2:Rew:12.0,816.0')] ).
cnf(945,plain,
~ equal(op(e0,e3),e0),
inference(rew,[status(thm),theory(equality)],[12,817]),
[iquote('2:Rew:12.0,817.0')] ).
cnf(946,plain,
~ equal(op(e0,e0),e3),
inference(mrr,[status(thm)],[194,945]),
[iquote('2:MRR:194.1,945.0')] ).
cnf(979,plain,
~ equal(op(e0,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,856]),
[iquote('2:Rew:17.0,856.0')] ).
cnf(983,plain,
~ equal(op(e1,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,860]),
[iquote('2:Rew:17.0,860.0')] ).
cnf(984,plain,
equal(op(e1,e2),e3),
inference(mrr,[status(thm)],[408,983]),
[iquote('2:MRR:408.0,983.0')] ).
cnf(1033,plain,
( equal(e3,e2)
| equal(e2,e1)
| equal(op(e1,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[14,804,984]),
[iquote('2:Rew:14.0,804.1,984.0,804.0')] ).
cnf(1034,plain,
equal(op(e1,e3),e2),
inference(mrr,[status(thm)],[1033,8,5]),
[iquote('2:MRR:1033.0,1033.1,8.0,5.0')] ).
cnf(1037,plain,
~ equal(op(e0,e3),e2),
inference(rew,[status(thm),theory(equality)],[1034,121]),
[iquote('2:Rew:1034.0,121.0')] ).
cnf(1087,plain,
equal(op(e0,e0),unit),
inference(mrr,[status(thm)],[869,944,946,937]),
[iquote('2:MRR:869.0,869.2,869.3,944.0,946.0,937.0')] ).
cnf(1089,plain,
~ equal(op(e0,e3),unit),
inference(rew,[status(thm),theory(equality)],[1087,143]),
[iquote('2:Rew:1087.0,143.0')] ).
cnf(1098,plain,
$false,
inference(mrr,[status(thm)],[891,979,945,1089,1037,923]),
[iquote('2:MRR:891.0,891.1,891.2,891.3,891.4,979.0,945.0,1089.0,1037.0,923.0')] ).
cnf(1099,plain,
~ equal(e4,unit),
inference(spt,[spt(split,[position(s2sa)])],[1098,780]),
[iquote('2:Spt:1098.0,779.0,780.0')] ).
cnf(1100,plain,
( equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2s2)])],[779]),
[iquote('2:Spt:1098.0,779.1,779.2,779.3')] ).
cnf(1101,plain,
equal(e3,unit),
inference(spt,[spt(split,[position(s2s2s1)])],[1100]),
[iquote('3:Spt:1100.0')] ).
cnf(1102,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[1101,8]),
[iquote('3:Rew:1101.0,8.0')] ).
cnf(1104,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[1101,18]),
[iquote('3:Rew:1101.0,18.0')] ).
cnf(1109,plain,
~ equal(op(e2,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1101,98]),
[iquote('3:Rew:1101.0,98.0')] ).
cnf(1113,plain,
( equal(op(e2,e0),e2)
| equal(op(e0,e0),e2)
| equal(op(e4,e0),e2)
| equal(op(unit,e0),e2) ),
inference(rew,[status(thm),theory(equality)],[1101,421]),
[iquote('3:Rew:1101.0,421.3')] ).
cnf(1124,plain,
( ~ skC3
| equal(op(unit,unit),e0) ),
inference(rew,[status(thm),theory(equality)],[1101,29]),
[iquote('3:Rew:1101.0,29.1')] ).
cnf(1125,plain,
( ~ skC15
| equal(op(unit,unit),e0) ),
inference(rew,[status(thm),theory(equality)],[1101,50]),
[iquote('3:Rew:1101.0,50.1')] ).
cnf(1134,plain,
~ equal(op(e4,e1),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1101,186]),
[iquote('3:Rew:1101.0,186.0')] ).
cnf(1135,plain,
~ equal(op(e4,e4),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[1101,190]),
[iquote('3:Rew:1101.0,190.0')] ).
cnf(1157,plain,
~ equal(op(e2,e1),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[1101,166]),
[iquote('3:Rew:1101.0,166.0')] ).
cnf(1159,plain,
~ equal(op(e2,e2),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[1101,168]),
[iquote('3:Rew:1101.0,168.0')] ).
cnf(1189,plain,
( equal(op(e2,e1),e2)
| equal(op(e4,e1),e2)
| equal(op(unit,e1),e2)
| equal(op(e0,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[1101,410]),
[iquote('3:Rew:1101.0,410.2')] ).
cnf(1190,plain,
( equal(op(e4,e1),e4)
| equal(op(unit,e1),e4)
| equal(op(e2,e1),e4)
| equal(op(e0,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[1101,402]),
[iquote('3:Rew:1101.0,402.1')] ).
cnf(1232,plain,
( equal(op(e4,e1),e4)
| equal(op(e4,e1),unit)
| equal(op(e4,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[1101,428]),
[iquote('3:Rew:1101.0,428.1')] ).
cnf(1245,plain,
( ~ skC3
| equal(e0,unit) ),
inference(rew,[status(thm),theory(equality)],[1104,1124]),
[iquote('3:Rew:1104.0,1124.1')] ).
cnf(1246,plain,
~ skC3,
inference(mrr,[status(thm)],[1245,778]),
[iquote('3:MRR:1245.1,778.0')] ).
cnf(1247,plain,
( skC20
| skC15
| skC10
| skC4
| skC2 ),
inference(mrr,[status(thm)],[449,1246]),
[iquote('3:MRR:449.4,1246.0')] ).
cnf(1248,plain,
( ~ skC15
| equal(e0,unit) ),
inference(rew,[status(thm),theory(equality)],[1104,1125]),
[iquote('3:Rew:1104.0,1125.1')] ).
cnf(1249,plain,
~ skC15,
inference(mrr,[status(thm)],[1248,778]),
[iquote('3:MRR:1248.1,778.0')] ).
cnf(1250,plain,
( skC20
| skC10
| skC4
| skC2 ),
inference(mrr,[status(thm)],[1247,1249]),
[iquote('3:MRR:1247.1,1249.0')] ).
cnf(1252,plain,
~ equal(op(e2,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1109]),
[iquote('3:Rew:11.0,1109.0')] ).
cnf(1253,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e4) ),
inference(mrr,[status(thm)],[438,1252]),
[iquote('3:MRR:438.1,1252.0')] ).
cnf(1257,plain,
~ equal(op(e4,e1),e4),
inference(rew,[status(thm),theory(equality)],[20,1134]),
[iquote('3:Rew:20.0,1134.0')] ).
cnf(1258,plain,
~ equal(op(e4,e4),e4),
inference(rew,[status(thm),theory(equality)],[20,1135]),
[iquote('3:Rew:20.0,1135.0')] ).
cnf(1259,plain,
equal(op(e4,e4),e0),
inference(mrr,[status(thm)],[426,1258]),
[iquote('3:MRR:426.0,1258.0')] ).
cnf(1266,plain,
~ equal(op(e0,e4),e0),
inference(rew,[status(thm),theory(equality)],[1259,134]),
[iquote('3:Rew:1259.0,134.0')] ).
cnf(1269,plain,
~ equal(op(e0,e0),e4),
inference(mrr,[status(thm)],[195,1266]),
[iquote('3:MRR:195.1,1266.0')] ).
cnf(1271,plain,
~ skC20,
inference(mrr,[status(thm)],[60,1269]),
[iquote('3:MRR:60.1,1269.0')] ).
cnf(1272,plain,
~ skC4,
inference(mrr,[status(thm)],[30,1269]),
[iquote('3:MRR:30.1,1269.0')] ).
cnf(1273,plain,
( skC10
| skC4
| skC2 ),
inference(mrr,[status(thm)],[1250,1271]),
[iquote('3:MRR:1250.0,1271.0')] ).
cnf(1274,plain,
( skC10
| skC2 ),
inference(mrr,[status(thm)],[1273,1272]),
[iquote('3:MRR:1273.1,1272.0')] ).
cnf(1289,plain,
~ equal(op(e2,e1),e2),
inference(rew,[status(thm),theory(equality)],[16,1157]),
[iquote('3:Rew:16.0,1157.0')] ).
cnf(1292,plain,
~ equal(op(e2,e2),e2),
inference(rew,[status(thm),theory(equality)],[16,1159]),
[iquote('3:Rew:16.0,1159.0')] ).
cnf(1293,plain,
equal(op(e2,e2),e0),
inference(mrr,[status(thm)],[436,1292]),
[iquote('3:MRR:436.0,1292.0')] ).
cnf(1300,plain,
~ equal(op(e0,e2),e0),
inference(rew,[status(thm),theory(equality)],[1293,112]),
[iquote('3:Rew:1293.0,112.0')] ).
cnf(1303,plain,
~ equal(op(e0,e0),e2),
inference(mrr,[status(thm)],[193,1300]),
[iquote('3:MRR:193.1,1300.0')] ).
cnf(1304,plain,
~ skC2,
inference(mrr,[status(thm)],[26,1303]),
[iquote('3:MRR:26.1,1303.0')] ).
cnf(1306,plain,
skC10,
inference(mrr,[status(thm)],[1274,1304]),
[iquote('3:MRR:1274.1,1304.0')] ).
cnf(1307,plain,
~ equal(op(e2,e0),e2),
inference(mrr,[status(thm)],[77,1306]),
[iquote('3:MRR:77.0,1306.0')] ).
cnf(1357,plain,
equal(op(e2,e0),e4),
inference(mrr,[status(thm)],[1253,1307]),
[iquote('3:MRR:1253.0,1307.0')] ).
cnf(1360,plain,
~ equal(op(e2,e1),e4),
inference(rew,[status(thm),theory(equality)],[1357,161]),
[iquote('3:Rew:1357.0,161.0')] ).
cnf(1393,plain,
( equal(op(e4,e1),unit)
| equal(op(e4,e1),e2) ),
inference(mrr,[status(thm)],[1232,1257]),
[iquote('3:MRR:1232.0,1257.0')] ).
cnf(1395,plain,
( equal(e4,e2)
| equal(op(e0,e0),e2)
| equal(op(e4,e0),e2)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[11,1113,1357]),
[iquote('3:Rew:11.0,1113.3,1357.0,1113.0')] ).
cnf(1396,plain,
equal(op(e4,e0),e2),
inference(mrr,[status(thm)],[1395,9,1303,2]),
[iquote('3:MRR:1395.0,1395.1,1395.3,9.0,1303.0,2.0')] ).
cnf(1398,plain,
~ equal(op(e4,e1),e2),
inference(rew,[status(thm),theory(equality)],[1396,181]),
[iquote('3:Rew:1396.0,181.0')] ).
cnf(1404,plain,
equal(op(e4,e1),unit),
inference(mrr,[status(thm)],[1393,1398]),
[iquote('3:MRR:1393.1,1398.0')] ).
cnf(1423,plain,
( equal(op(e2,e1),e2)
| equal(e2,unit)
| equal(e2,e1)
| equal(op(e0,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[13,1189,1404]),
[iquote('3:Rew:13.0,1189.2,1404.0,1189.1')] ).
cnf(1424,plain,
equal(op(e0,e1),e2),
inference(mrr,[status(thm)],[1423,1289,1102,5]),
[iquote('3:MRR:1423.0,1423.1,1423.2,1289.0,1102.0,5.0')] ).
cnf(1430,plain,
( equal(e4,unit)
| equal(e4,e1)
| equal(op(e2,e1),e4)
| equal(e4,e2) ),
inference(rew,[status(thm),theory(equality)],[1424,1190,13,1404]),
[iquote('3:Rew:1424.0,1190.3,13.0,1190.1,1404.0,1190.0')] ).
cnf(1431,plain,
$false,
inference(mrr,[status(thm)],[1430,1099,7,1360,9]),
[iquote('3:MRR:1430.0,1430.1,1430.2,1430.3,1099.0,7.0,1360.0,9.0')] ).
cnf(1437,plain,
~ equal(e3,unit),
inference(spt,[spt(split,[position(s2s2sa)])],[1431,1101]),
[iquote('3:Spt:1431.0,1100.0,1101.0')] ).
cnf(1438,plain,
( equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2s2s2)])],[1100]),
[iquote('3:Spt:1431.0,1100.1,1100.2')] ).
cnf(1439,plain,
equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2s1)])],[1438]),
[iquote('4:Spt:1438.0')] ).
cnf(1454,plain,
( equal(op(e4,e1),e4)
| equal(op(e3,e1),e4)
| equal(op(unit,e1),e4)
| equal(op(e0,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[1439,402]),
[iquote('4:Rew:1439.0,402.2')] ).
cnf(1459,plain,
~ equal(op(e3,e0),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[1439,172]),
[iquote('4:Rew:1439.0,172.0')] ).
cnf(1460,plain,
~ equal(op(e3,e1),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[1439,175]),
[iquote('4:Rew:1439.0,175.0')] ).
cnf(1461,plain,
~ equal(op(e3,e3),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[1439,178]),
[iquote('4:Rew:1439.0,178.0')] ).
cnf(1480,plain,
( equal(op(e4,e0),e4)
| equal(op(e0,e0),e4)
| equal(op(e3,e0),e4)
| equal(op(unit,e0),e4) ),
inference(rew,[status(thm),theory(equality)],[1439,416]),
[iquote('4:Rew:1439.0,416.3')] ).
cnf(1514,plain,
~ equal(op(e0,e3),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[1439,148]),
[iquote('4:Rew:1439.0,148.0')] ).
cnf(1521,plain,
~ equal(op(e0,e4),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[1439,149]),
[iquote('4:Rew:1439.0,149.0')] ).
cnf(1540,plain,
( equal(op(e3,e3),e3)
| equal(op(e3,e3),unit)
| equal(op(e3,e3),e1)
| equal(op(e3,e3),e0) ),
inference(rew,[status(thm),theory(equality)],[1439,431]),
[iquote('4:Rew:1439.0,431.1')] ).
cnf(1542,plain,
( equal(op(e4,e3),e2)
| equal(op(e4,e1),unit)
| equal(op(e4,e0),e2) ),
inference(rew,[status(thm),theory(equality)],[1439,370]),
[iquote('4:Rew:1439.0,370.1')] ).
cnf(1582,plain,
~ equal(op(e3,e0),e3),
inference(rew,[status(thm),theory(equality)],[18,1459]),
[iquote('4:Rew:18.0,1459.0')] ).
cnf(1583,plain,
~ equal(op(e3,e3),e0),
inference(mrr,[status(thm)],[204,1582]),
[iquote('4:MRR:204.1,1582.0')] ).
cnf(1584,plain,
( equal(op(e0,e0),e3)
| equal(op(e4,e0),e3) ),
inference(mrr,[status(thm)],[418,1582]),
[iquote('4:MRR:418.0,1582.0')] ).
cnf(1589,plain,
~ equal(op(e3,e1),e3),
inference(rew,[status(thm),theory(equality)],[18,1460]),
[iquote('4:Rew:18.0,1460.0')] ).
cnf(1590,plain,
~ equal(op(e3,e3),e1),
inference(mrr,[status(thm)],[205,1589]),
[iquote('4:MRR:205.1,1589.0')] ).
cnf(1591,plain,
( equal(op(e4,e1),e3)
| equal(op(e0,e1),e3) ),
inference(mrr,[status(thm)],[406,1589]),
[iquote('4:MRR:406.0,1589.0')] ).
cnf(1592,plain,
~ equal(op(e3,e3),e3),
inference(rew,[status(thm),theory(equality)],[18,1461]),
[iquote('4:Rew:18.0,1461.0')] ).
cnf(1615,plain,
~ equal(op(e0,e3),e0),
inference(rew,[status(thm),theory(equality)],[12,1514]),
[iquote('4:Rew:12.0,1514.0')] ).
cnf(1616,plain,
~ equal(op(e0,e0),e3),
inference(mrr,[status(thm)],[194,1615]),
[iquote('4:MRR:194.1,1615.0')] ).
cnf(1619,plain,
~ equal(op(e0,e4),e0),
inference(rew,[status(thm),theory(equality)],[12,1521]),
[iquote('4:Rew:12.0,1521.0')] ).
cnf(1620,plain,
~ equal(op(e0,e0),e4),
inference(mrr,[status(thm)],[195,1619]),
[iquote('4:MRR:195.1,1619.0')] ).
cnf(1665,plain,
equal(op(e4,e0),e3),
inference(mrr,[status(thm)],[1584,1616]),
[iquote('4:MRR:1584.0,1616.0')] ).
cnf(1670,plain,
~ equal(op(e4,e1),e3),
inference(rew,[status(thm),theory(equality)],[1665,181]),
[iquote('4:Rew:1665.0,181.0')] ).
cnf(1673,plain,
equal(op(e0,e1),e3),
inference(mrr,[status(thm)],[1591,1670]),
[iquote('4:MRR:1591.0,1670.0')] ).
cnf(1694,plain,
( equal(op(e4,e3),unit)
| equal(op(e4,e1),unit)
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[1665,1542,1439]),
[iquote('4:Rew:1665.0,1542.2,1439.0,1542.2,1439.0,1542.0')] ).
cnf(1695,plain,
( equal(op(e4,e3),unit)
| equal(op(e4,e1),unit) ),
inference(mrr,[status(thm)],[1694,1437]),
[iquote('4:MRR:1694.2,1437.0')] ).
cnf(1704,plain,
( equal(op(e4,e1),e4)
| equal(op(e3,e1),e4)
| equal(e4,e1)
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[1673,1454,13]),
[iquote('4:Rew:1673.0,1454.3,13.0,1454.2')] ).
cnf(1705,plain,
( equal(op(e4,e1),e4)
| equal(op(e3,e1),e4) ),
inference(mrr,[status(thm)],[1704,7,10]),
[iquote('4:MRR:1704.2,1704.3,7.0,10.0')] ).
cnf(1710,plain,
( equal(e4,e3)
| equal(op(e0,e0),e4)
| equal(op(e3,e0),e4)
| equal(e4,e0) ),
inference(rew,[status(thm),theory(equality)],[11,1480,1665]),
[iquote('4:Rew:11.0,1480.3,1665.0,1480.0')] ).
cnf(1711,plain,
equal(op(e3,e0),e4),
inference(mrr,[status(thm)],[1710,10,1620,4]),
[iquote('4:MRR:1710.0,1710.1,1710.3,10.0,1620.0,4.0')] ).
cnf(1713,plain,
~ equal(op(e3,e1),e4),
inference(rew,[status(thm),theory(equality)],[1711,171]),
[iquote('4:Rew:1711.0,171.0')] ).
cnf(1718,plain,
equal(op(e4,e1),e4),
inference(mrr,[status(thm)],[1705,1713]),
[iquote('4:MRR:1705.1,1713.0')] ).
cnf(1724,plain,
( equal(op(e4,e3),unit)
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[1718,1695]),
[iquote('4:Rew:1718.0,1695.1')] ).
cnf(1725,plain,
equal(op(e4,e3),unit),
inference(mrr,[status(thm)],[1724,1099]),
[iquote('4:MRR:1724.1,1099.0')] ).
cnf(1728,plain,
~ equal(op(e3,e3),unit),
inference(rew,[status(thm),theory(equality)],[1725,130]),
[iquote('4:Rew:1725.0,130.0')] ).
cnf(1763,plain,
$false,
inference(mrr,[status(thm)],[1540,1592,1728,1590,1583]),
[iquote('4:MRR:1540.0,1540.1,1540.2,1540.3,1592.0,1728.0,1590.0,1583.0')] ).
cnf(1773,plain,
~ equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2sa)])],[1763,1439]),
[iquote('4:Spt:1763.0,1438.0,1439.0')] ).
cnf(1774,plain,
equal(e1,unit),
inference(spt,[spt(split,[position(s2s2s2s2)])],[1438]),
[iquote('4:Spt:1763.0,1438.1')] ).
cnf(1782,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[1774,5]),
[iquote('4:Rew:1774.0,5.0')] ).
cnf(1821,plain,
~ equal(op(e3,e2),e3),
inference(rew,[status(thm),theory(equality)],[18,175,1774]),
[iquote('4:Rew:18.0,175.0,1774.0,175.0')] ).
cnf(1836,plain,
~ equal(op(e3,e0),e3),
inference(rew,[status(thm),theory(equality)],[18,171,1774]),
[iquote('4:Rew:18.0,171.0,1774.0,171.0')] ).
cnf(1855,plain,
( equal(e2,unit)
| equal(op(e2,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[1774,396,16]),
[iquote('4:Rew:1774.0,396.1,16.0,396.0,1774.0,396.0')] ).
cnf(1856,plain,
equal(op(e2,e3),unit),
inference(mrr,[status(thm)],[1855,1782]),
[iquote('4:MRR:1855.0,1782.0')] ).
cnf(1860,plain,
~ equal(op(e3,e3),unit),
inference(rew,[status(thm),theory(equality)],[1856,128]),
[iquote('4:Rew:1856.0,128.0')] ).
cnf(1882,plain,
~ equal(op(e3,e3),e2),
inference(mrr,[status(thm)],[206,1821]),
[iquote('4:MRR:206.1,1821.0')] ).
cnf(1883,plain,
~ equal(op(e3,e3),e0),
inference(mrr,[status(thm)],[204,1836]),
[iquote('4:MRR:204.1,1836.0')] ).
cnf(1916,plain,
( equal(op(e3,e2),e4)
| equal(e4,e2)
| equal(op(e0,e2),e4) ),
inference(rew,[status(thm),theory(equality)],[15,386,1774]),
[iquote('4:Rew:15.0,386.1,1774.0,386.1')] ).
cnf(1917,plain,
( equal(op(e3,e2),e4)
| equal(op(e0,e2),e4) ),
inference(mrr,[status(thm)],[1916,9]),
[iquote('4:MRR:1916.1,9.0')] ).
cnf(1918,plain,
( equal(op(e3,e2),e3)
| equal(e3,e2)
| equal(op(e0,e2),e3) ),
inference(rew,[status(thm),theory(equality)],[15,390,1774]),
[iquote('4:Rew:15.0,390.1,1774.0,390.1')] ).
cnf(1919,plain,
equal(op(e0,e2),e3),
inference(mrr,[status(thm)],[1918,1821,8]),
[iquote('4:MRR:1918.0,1918.1,1821.0,8.0')] ).
cnf(1927,plain,
( equal(op(e3,e2),e4)
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[1919,1917]),
[iquote('4:Rew:1919.0,1917.1')] ).
cnf(1928,plain,
equal(op(e3,e2),e4),
inference(mrr,[status(thm)],[1927,10]),
[iquote('4:MRR:1927.1,10.0')] ).
cnf(1939,plain,
( equal(op(e3,e3),unit)
| equal(e3,unit)
| equal(op(e3,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[1774,382,18]),
[iquote('4:Rew:1774.0,382.2,18.0,382.1,1774.0,382.1,1774.0,382.0')] ).
cnf(1940,plain,
equal(op(e3,e4),unit),
inference(mrr,[status(thm)],[1939,1860,1437]),
[iquote('4:MRR:1939.0,1939.1,1860.0,1437.0')] ).
cnf(1978,plain,
( equal(op(e3,e3),e0)
| equal(op(e3,e0),e0)
| equal(e0,unit)
| equal(e4,e0) ),
inference(rew,[status(thm),theory(equality)],[1928,384,1940]),
[iquote('4:Rew:1928.0,384.3,1940.0,384.2')] ).
cnf(1979,plain,
equal(op(e3,e0),e0),
inference(mrr,[status(thm)],[1978,1883,778,4]),
[iquote('4:MRR:1978.0,1978.2,1978.3,1883.0,778.0,4.0')] ).
cnf(2010,plain,
( equal(op(e3,e3),e2)
| equal(e4,e2)
| equal(e2,unit)
| equal(e3,e2)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[1979,228,18,1774,1940,1928]),
[iquote('4:Rew:1979.0,228.4,18.0,228.3,1774.0,228.3,1940.0,228.2,1928.0,228.1')] ).
cnf(2011,plain,
$false,
inference(mrr,[status(thm)],[2010,1882,9,1782,8,2]),
[iquote('4:MRR:2010.0,2010.1,2010.2,2010.3,2010.4,1882.0,9.0,1782.0,8.0,2.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG067+1 : TPTP v8.1.0. Released v2.7.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Wed Jun 8 00:51:46 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.47/0.63
% 0.47/0.63 SPASS V 3.9
% 0.47/0.63 SPASS beiseite: Proof found.
% 0.47/0.63 % SZS status Theorem
% 0.47/0.63 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.63 SPASS derived 1019 clauses, backtracked 796 clauses, performed 4 splits and kept 1329 clauses.
% 0.47/0.63 SPASS allocated 86127 KBytes.
% 0.47/0.63 SPASS spent 0:00:00.27 on the problem.
% 0.47/0.63 0:00:00.04 for the input.
% 0.47/0.63 0:00:00.06 for the FLOTTER CNF translation.
% 0.47/0.63 0:00:00.00 for inferences.
% 0.47/0.63 0:00:00.00 for the backtracking.
% 0.47/0.63 0:00:00.14 for the reduction.
% 0.47/0.63
% 0.47/0.63
% 0.47/0.63 Here is a proof with depth 4, length 379 :
% 0.47/0.63 % SZS output start Refutation
% See solution above
% 0.47/0.64 Formulae used in the proof : ax5 ax2 ax6 co1 ax4 ax3 ax1
% 0.47/0.64
%------------------------------------------------------------------------------