%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG032+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.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:02 EDT 2022
% Result : Theorem 2.37s 2.57s
% Output : Refutation 2.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 86
% Syntax : Number of clauses : 191 ( 103 unt; 0 nHn; 191 RR)
% Number of literals : 1213 ( 0 equ;1026 neg)
% Maximal clause size : 304 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 44 ( 43 usr; 43 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(e0,unit),
file('ALG032+1.p',unknown),
[] ).
cnf(17,axiom,
equal(inv(e0),e0),
file('ALG032+1.p',unknown),
[] ).
cnf(18,axiom,
equal(inv(e1),e1),
file('ALG032+1.p',unknown),
[] ).
cnf(19,axiom,
equal(inv(e2),e3),
file('ALG032+1.p',unknown),
[] ).
cnf(20,axiom,
equal(inv(e3),e2),
file('ALG032+1.p',unknown),
[] ).
cnf(21,axiom,
equal(inv(e4),e5),
file('ALG032+1.p',unknown),
[] ).
cnf(22,axiom,
equal(inv(e5),e4),
file('ALG032+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ equal(e0,unit)
| skC36 ),
file('ALG032+1.p',unknown),
[] ).
cnf(29,axiom,
equal(op(e0,e0),e0),
file('ALG032+1.p',unknown),
[] ).
cnf(30,axiom,
equal(op(e0,e1),e1),
file('ALG032+1.p',unknown),
[] ).
cnf(31,axiom,
equal(op(e0,e2),e2),
file('ALG032+1.p',unknown),
[] ).
cnf(32,axiom,
equal(op(e0,e3),e3),
file('ALG032+1.p',unknown),
[] ).
cnf(33,axiom,
equal(op(e0,e4),e4),
file('ALG032+1.p',unknown),
[] ).
cnf(34,axiom,
equal(op(e0,e5),e5),
file('ALG032+1.p',unknown),
[] ).
cnf(35,axiom,
equal(op(e1,e0),e1),
file('ALG032+1.p',unknown),
[] ).
cnf(36,axiom,
equal(op(e1,e1),e0),
file('ALG032+1.p',unknown),
[] ).
cnf(37,axiom,
equal(op(e1,e2),e4),
file('ALG032+1.p',unknown),
[] ).
cnf(38,axiom,
equal(op(e1,e3),e5),
file('ALG032+1.p',unknown),
[] ).
cnf(39,axiom,
equal(op(e1,e4),e2),
file('ALG032+1.p',unknown),
[] ).
cnf(40,axiom,
equal(op(e1,e5),e3),
file('ALG032+1.p',unknown),
[] ).
cnf(41,axiom,
equal(op(e2,e0),e2),
file('ALG032+1.p',unknown),
[] ).
cnf(42,axiom,
equal(op(e2,e1),e4),
file('ALG032+1.p',unknown),
[] ).
cnf(43,axiom,
equal(op(e2,e2),e3),
file('ALG032+1.p',unknown),
[] ).
cnf(44,axiom,
equal(op(e2,e3),e0),
file('ALG032+1.p',unknown),
[] ).
cnf(45,axiom,
equal(op(e2,e4),e5),
file('ALG032+1.p',unknown),
[] ).
cnf(46,axiom,
equal(op(e2,e5),e1),
file('ALG032+1.p',unknown),
[] ).
cnf(47,axiom,
equal(op(e3,e0),e3),
file('ALG032+1.p',unknown),
[] ).
cnf(48,axiom,
equal(op(e3,e1),e5),
file('ALG032+1.p',unknown),
[] ).
cnf(49,axiom,
equal(op(e3,e2),e0),
file('ALG032+1.p',unknown),
[] ).
cnf(50,axiom,
equal(op(e3,e3),e2),
file('ALG032+1.p',unknown),
[] ).
cnf(51,axiom,
equal(op(e3,e4),e1),
file('ALG032+1.p',unknown),
[] ).
cnf(52,axiom,
equal(op(e3,e5),e4),
file('ALG032+1.p',unknown),
[] ).
cnf(53,axiom,
equal(op(e4,e0),e4),
file('ALG032+1.p',unknown),
[] ).
cnf(54,axiom,
equal(op(e4,e1),e2),
file('ALG032+1.p',unknown),
[] ).
cnf(55,axiom,
equal(op(e4,e2),e5),
file('ALG032+1.p',unknown),
[] ).
cnf(56,axiom,
equal(op(e4,e3),e1),
file('ALG032+1.p',unknown),
[] ).
cnf(57,axiom,
equal(op(e4,e4),e3),
file('ALG032+1.p',unknown),
[] ).
cnf(58,axiom,
equal(op(e4,e5),e0),
file('ALG032+1.p',unknown),
[] ).
cnf(59,axiom,
equal(op(e5,e0),e5),
file('ALG032+1.p',unknown),
[] ).
cnf(60,axiom,
equal(op(e5,e1),e3),
file('ALG032+1.p',unknown),
[] ).
cnf(61,axiom,
equal(op(e5,e2),e1),
file('ALG032+1.p',unknown),
[] ).
cnf(62,axiom,
equal(op(e5,e3),e4),
file('ALG032+1.p',unknown),
[] ).
cnf(63,axiom,
equal(op(e5,e4),e0),
file('ALG032+1.p',unknown),
[] ).
cnf(64,axiom,
equal(op(e5,e5),e2),
file('ALG032+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ equal(inv(e0),e0)
| skC37 ),
file('ALG032+1.p',unknown),
[] ).
cnf(72,axiom,
( ~ equal(inv(e1),e1)
| skC38 ),
file('ALG032+1.p',unknown),
[] ).
cnf(80,axiom,
( ~ equal(inv(e2),e3)
| skC39 ),
file('ALG032+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ equal(inv(e3),e2)
| skC40 ),
file('ALG032+1.p',unknown),
[] ).
cnf(94,axiom,
( ~ equal(inv(e4),e5)
| skC41 ),
file('ALG032+1.p',unknown),
[] ).
cnf(95,axiom,
( ~ equal(op(e0,e0),e0)
| skC0 ),
file('ALG032+1.p',unknown),
[] ).
cnf(102,axiom,
( ~ equal(op(e0,e1),e1)
| skC1 ),
file('ALG032+1.p',unknown),
[] ).
cnf(109,axiom,
( ~ equal(op(e0,e2),e2)
| skC2 ),
file('ALG032+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ equal(op(e0,e3),e3)
| skC3 ),
file('ALG032+1.p',unknown),
[] ).
cnf(123,axiom,
( ~ equal(op(e0,e4),e4)
| skC4 ),
file('ALG032+1.p',unknown),
[] ).
cnf(130,axiom,
( ~ equal(op(e0,e5),e5)
| skC5 ),
file('ALG032+1.p',unknown),
[] ).
cnf(132,axiom,
( ~ equal(op(e1,e0),e1)
| skC6 ),
file('ALG032+1.p',unknown),
[] ).
cnf(137,axiom,
( ~ equal(op(e1,e1),e0)
| skC7 ),
file('ALG032+1.p',unknown),
[] ).
cnf(147,axiom,
( ~ equal(op(e1,e2),e4)
| skC8 ),
file('ALG032+1.p',unknown),
[] ).
cnf(154,axiom,
( ~ equal(op(e1,e3),e5)
| skC9 ),
file('ALG032+1.p',unknown),
[] ).
cnf(157,axiom,
( ~ equal(op(e1,e4),e2)
| skC10 ),
file('ALG032+1.p',unknown),
[] ).
cnf(164,axiom,
( ~ equal(op(e1,e5),e3)
| skC11 ),
file('ALG032+1.p',unknown),
[] ).
cnf(169,axiom,
( ~ equal(op(e2,e0),e2)
| skC12 ),
file('ALG032+1.p',unknown),
[] ).
cnf(177,axiom,
( ~ equal(op(e2,e1),e4)
| skC13 ),
file('ALG032+1.p',unknown),
[] ).
cnf(182,axiom,
( ~ equal(op(e2,e2),e3)
| skC14 ),
file('ALG032+1.p',unknown),
[] ).
cnf(185,axiom,
( ~ equal(op(e2,e3),e0)
| skC15 ),
file('ALG032+1.p',unknown),
[] ).
cnf(196,axiom,
( ~ equal(op(e2,e4),e5)
| skC16 ),
file('ALG032+1.p',unknown),
[] ).
cnf(198,axiom,
( ~ equal(op(e2,e5),e1)
| skC17 ),
file('ALG032+1.p',unknown),
[] ).
cnf(206,axiom,
( ~ equal(op(e3,e0),e3)
| skC18 ),
file('ALG032+1.p',unknown),
[] ).
cnf(214,axiom,
( ~ equal(op(e3,e1),e5)
| skC19 ),
file('ALG032+1.p',unknown),
[] ).
cnf(215,axiom,
( ~ equal(op(e3,e2),e0)
| skC20 ),
file('ALG032+1.p',unknown),
[] ).
cnf(223,axiom,
( ~ equal(op(e3,e3),e2)
| skC21 ),
file('ALG032+1.p',unknown),
[] ).
cnf(228,axiom,
( ~ equal(op(e3,e4),e1)
| skC22 ),
file('ALG032+1.p',unknown),
[] ).
cnf(237,axiom,
( ~ equal(op(e3,e5),e4)
| skC23 ),
file('ALG032+1.p',unknown),
[] ).
cnf(243,axiom,
( ~ equal(op(e4,e0),e4)
| skC24 ),
file('ALG032+1.p',unknown),
[] ).
cnf(247,axiom,
( ~ equal(op(e4,e1),e2)
| skC25 ),
file('ALG032+1.p',unknown),
[] ).
cnf(256,axiom,
( ~ equal(op(e4,e2),e5)
| skC26 ),
file('ALG032+1.p',unknown),
[] ).
cnf(258,axiom,
( ~ equal(op(e4,e3),e1)
| skC27 ),
file('ALG032+1.p',unknown),
[] ).
cnf(266,axiom,
( ~ equal(op(e4,e4),e3)
| skC28 ),
file('ALG032+1.p',unknown),
[] ).
cnf(269,axiom,
( ~ equal(op(e4,e5),e0)
| skC29 ),
file('ALG032+1.p',unknown),
[] ).
cnf(280,axiom,
( ~ equal(op(e5,e0),e5)
| skC30 ),
file('ALG032+1.p',unknown),
[] ).
cnf(284,axiom,
( ~ equal(op(e5,e1),e3)
| skC31 ),
file('ALG032+1.p',unknown),
[] ).
cnf(288,axiom,
( ~ equal(op(e5,e2),e1)
| skC32 ),
file('ALG032+1.p',unknown),
[] ).
cnf(297,axiom,
( ~ equal(op(e5,e3),e4)
| skC33 ),
file('ALG032+1.p',unknown),
[] ).
cnf(299,axiom,
( ~ equal(op(e5,e4),e0)
| skC34 ),
file('ALG032+1.p',unknown),
[] ).
cnf(307,axiom,
( ~ equal(op(e5,e5),e2)
| skC35 ),
file('ALG032+1.p',unknown),
[] ).
cnf(312,axiom,
( ~ equal(inv(e5),e4)
| ~ equal(op(e0,e0),op(e0,e0))
| ~ equal(op(e0,e1),op(e1,e0))
| ~ equal(op(e2,e0),op(e0,e2))
| ~ equal(op(e3,e0),op(e0,e3))
| ~ equal(op(e4,e0),op(e0,e4))
| ~ equal(op(e5,e0),op(e0,e5))
| ~ equal(op(e1,e1),op(e1,e1))
| ~ equal(op(e2,e1),op(e1,e2))
| ~ equal(op(e3,e1),op(e1,e3))
| ~ equal(op(e4,e1),op(e1,e4))
| ~ equal(op(e5,e1),op(e1,e5))
| ~ equal(op(e2,e2),op(e2,e2))
| ~ equal(op(e2,e3),op(e3,e2))
| ~ equal(op(e4,e2),op(e2,e4))
| ~ equal(op(e5,e2),op(e2,e5))
| ~ equal(op(e3,e3),op(e3,e3))
| ~ equal(op(e4,e3),op(e3,e4))
| ~ equal(op(e5,e3),op(e3,e5))
| ~ equal(op(e4,e4),op(e4,e4))
| ~ equal(op(e4,e5),op(e5,e4))
| ~ equal(op(e5,e5),op(e5,e5))
| ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ equal(op(op(e0,e0),e0),op(e0,op(e0,e0)))
| ~ equal(op(op(e0,e0),e1),op(e0,op(e0,e1)))
| ~ equal(op(op(e0,e0),e2),op(e0,op(e0,e2)))
| ~ equal(op(op(e0,e0),e3),op(e0,op(e0,e3)))
| ~ equal(op(op(e0,e0),e4),op(e0,op(e0,e4)))
| ~ equal(op(op(e0,e0),e5),op(e0,op(e0,e5)))
| ~ equal(op(op(e0,e1),e0),op(e0,op(e1,e0)))
| ~ equal(op(op(e0,e1),e1),op(e0,op(e1,e1)))
| ~ equal(op(op(e0,e1),e2),op(e0,op(e1,e2)))
| ~ equal(op(op(e0,e1),e3),op(e0,op(e1,e3)))
| ~ equal(op(op(e0,e1),e4),op(e0,op(e1,e4)))
| ~ equal(op(op(e0,e1),e5),op(e0,op(e1,e5)))
| ~ equal(op(op(e0,e2),e0),op(e0,op(e2,e0)))
| ~ equal(op(op(e0,e2),e1),op(e0,op(e2,e1)))
| ~ equal(op(op(e0,e2),e2),op(e0,op(e2,e2)))
| ~ equal(op(op(e0,e2),e3),op(e0,op(e2,e3)))
| ~ equal(op(op(e0,e2),e4),op(e0,op(e2,e4)))
| ~ equal(op(op(e0,e2),e5),op(e0,op(e2,e5)))
| ~ equal(op(op(e0,e3),e0),op(e0,op(e3,e0)))
| ~ equal(op(op(e0,e3),e1),op(e0,op(e3,e1)))
| ~ equal(op(op(e0,e3),e2),op(e0,op(e3,e2)))
| ~ equal(op(op(e0,e3),e3),op(e0,op(e3,e3)))
| ~ equal(op(op(e0,e3),e4),op(e0,op(e3,e4)))
| ~ equal(op(op(e0,e3),e5),op(e0,op(e3,e5)))
| ~ equal(op(op(e0,e4),e0),op(e0,op(e4,e0)))
| ~ equal(op(op(e0,e4),e1),op(e0,op(e4,e1)))
| ~ equal(op(op(e0,e4),e2),op(e0,op(e4,e2)))
| ~ equal(op(op(e0,e4),e3),op(e0,op(e4,e3)))
| ~ equal(op(op(e0,e4),e4),op(e0,op(e4,e4)))
| ~ equal(op(op(e0,e4),e5),op(e0,op(e4,e5)))
| ~ equal(op(op(e0,e5),e0),op(e0,op(e5,e0)))
| ~ equal(op(op(e0,e5),e1),op(e0,op(e5,e1)))
| ~ equal(op(op(e0,e5),e2),op(e0,op(e5,e2)))
| ~ equal(op(op(e0,e5),e3),op(e0,op(e5,e3)))
| ~ equal(op(op(e0,e5),e4),op(e0,op(e5,e4)))
| ~ equal(op(op(e0,e5),e5),op(e0,op(e5,e5)))
| ~ equal(op(op(e1,e0),e0),op(e1,op(e0,e0)))
| ~ equal(op(op(e1,e0),e1),op(e1,op(e0,e1)))
| ~ equal(op(op(e1,e0),e2),op(e1,op(e0,e2)))
| ~ equal(op(op(e1,e0),e3),op(e1,op(e0,e3)))
| ~ equal(op(op(e1,e0),e4),op(e1,op(e0,e4)))
| ~ equal(op(op(e1,e0),e5),op(e1,op(e0,e5)))
| ~ equal(op(op(e1,e1),e0),op(e1,op(e1,e0)))
| ~ equal(op(op(e1,e1),e1),op(e1,op(e1,e1)))
| ~ equal(op(op(e1,e1),e2),op(e1,op(e1,e2)))
| ~ equal(op(op(e1,e1),e3),op(e1,op(e1,e3)))
| ~ equal(op(op(e1,e1),e4),op(e1,op(e1,e4)))
| ~ equal(op(op(e1,e1),e5),op(e1,op(e1,e5)))
| ~ equal(op(op(e1,e2),e0),op(e1,op(e2,e0)))
| ~ equal(op(op(e1,e2),e1),op(e1,op(e2,e1)))
| ~ equal(op(op(e1,e2),e2),op(e1,op(e2,e2)))
| ~ equal(op(op(e1,e2),e3),op(e1,op(e2,e3)))
| ~ equal(op(op(e1,e2),e4),op(e1,op(e2,e4)))
| ~ equal(op(op(e1,e2),e5),op(e1,op(e2,e5)))
| ~ equal(op(op(e1,e3),e0),op(e1,op(e3,e0)))
| ~ equal(op(op(e1,e3),e1),op(e1,op(e3,e1)))
| ~ equal(op(op(e1,e3),e2),op(e1,op(e3,e2)))
| ~ equal(op(op(e1,e3),e3),op(e1,op(e3,e3)))
| ~ equal(op(op(e1,e3),e4),op(e1,op(e3,e4)))
| ~ equal(op(op(e1,e3),e5),op(e1,op(e3,e5)))
| ~ equal(op(op(e1,e4),e0),op(e1,op(e4,e0)))
| ~ equal(op(op(e1,e4),e1),op(e1,op(e4,e1)))
| ~ equal(op(op(e1,e4),e2),op(e1,op(e4,e2)))
| ~ equal(op(op(e1,e4),e3),op(e1,op(e4,e3)))
| ~ equal(op(op(e1,e4),e4),op(e1,op(e4,e4)))
| ~ equal(op(op(e1,e4),e5),op(e1,op(e4,e5)))
| ~ equal(op(op(e1,e5),e0),op(e1,op(e5,e0)))
| ~ equal(op(op(e1,e5),e1),op(e1,op(e5,e1)))
| ~ equal(op(op(e1,e5),e2),op(e1,op(e5,e2)))
| ~ equal(op(op(e1,e5),e3),op(e1,op(e5,e3)))
| ~ equal(op(op(e1,e5),e4),op(e1,op(e5,e4)))
| ~ equal(op(op(e1,e5),e5),op(e1,op(e5,e5)))
| ~ equal(op(op(e2,e0),e0),op(e2,op(e0,e0)))
| ~ equal(op(op(e2,e0),e1),op(e2,op(e0,e1)))
| ~ equal(op(op(e2,e0),e2),op(e2,op(e0,e2)))
| ~ equal(op(op(e2,e0),e3),op(e2,op(e0,e3)))
| ~ equal(op(op(e2,e0),e4),op(e2,op(e0,e4)))
| ~ equal(op(op(e2,e0),e5),op(e2,op(e0,e5)))
| ~ equal(op(op(e2,e1),e0),op(e2,op(e1,e0)))
| ~ equal(op(op(e2,e1),e1),op(e2,op(e1,e1)))
| ~ equal(op(op(e2,e1),e2),op(e2,op(e1,e2)))
| ~ equal(op(op(e2,e1),e3),op(e2,op(e1,e3)))
| ~ equal(op(op(e2,e1),e4),op(e2,op(e1,e4)))
| ~ equal(op(op(e2,e1),e5),op(e2,op(e1,e5)))
| ~ equal(op(op(e2,e2),e0),op(e2,op(e2,e0)))
| ~ equal(op(op(e2,e2),e1),op(e2,op(e2,e1)))
| ~ equal(op(op(e2,e2),e2),op(e2,op(e2,e2)))
| ~ equal(op(op(e2,e2),e3),op(e2,op(e2,e3)))
| ~ equal(op(op(e2,e2),e4),op(e2,op(e2,e4)))
| ~ equal(op(op(e2,e2),e5),op(e2,op(e2,e5)))
| ~ equal(op(op(e2,e3),e0),op(e2,op(e3,e0)))
| ~ equal(op(op(e2,e3),e1),op(e2,op(e3,e1)))
| ~ equal(op(op(e2,e3),e2),op(e2,op(e3,e2)))
| ~ equal(op(op(e2,e3),e3),op(e2,op(e3,e3)))
| ~ equal(op(op(e2,e3),e4),op(e2,op(e3,e4)))
| ~ equal(op(op(e2,e3),e5),op(e2,op(e3,e5)))
| ~ equal(op(op(e2,e4),e0),op(e2,op(e4,e0)))
| ~ equal(op(op(e2,e4),e1),op(e2,op(e4,e1)))
| ~ equal(op(op(e2,e4),e2),op(e2,op(e4,e2)))
| ~ equal(op(op(e2,e4),e3),op(e2,op(e4,e3)))
| ~ equal(op(op(e2,e4),e4),op(e2,op(e4,e4)))
| ~ equal(op(op(e2,e4),e5),op(e2,op(e4,e5)))
| ~ equal(op(op(e2,e5),e0),op(e2,op(e5,e0)))
| ~ equal(op(op(e2,e5),e1),op(e2,op(e5,e1)))
| ~ equal(op(op(e2,e5),e2),op(e2,op(e5,e2)))
| ~ equal(op(op(e2,e5),e3),op(e2,op(e5,e3)))
| ~ equal(op(op(e2,e5),e4),op(e2,op(e5,e4)))
| ~ equal(op(op(e2,e5),e5),op(e2,op(e5,e5)))
| ~ equal(op(op(e3,e0),e0),op(e3,op(e0,e0)))
| ~ equal(op(op(e3,e0),e1),op(e3,op(e0,e1)))
| ~ equal(op(op(e3,e0),e2),op(e3,op(e0,e2)))
| ~ equal(op(op(e3,e0),e3),op(e3,op(e0,e3)))
| ~ equal(op(op(e3,e0),e4),op(e3,op(e0,e4)))
| ~ equal(op(op(e3,e0),e5),op(e3,op(e0,e5)))
| ~ equal(op(op(e3,e1),e0),op(e3,op(e1,e0)))
| ~ equal(op(op(e3,e1),e1),op(e3,op(e1,e1)))
| ~ equal(op(op(e3,e1),e2),op(e3,op(e1,e2)))
| ~ equal(op(op(e3,e1),e3),op(e3,op(e1,e3)))
| ~ equal(op(op(e3,e1),e4),op(e3,op(e1,e4)))
| ~ equal(op(op(e3,e1),e5),op(e3,op(e1,e5)))
| ~ equal(op(op(e3,e2),e0),op(e3,op(e2,e0)))
| ~ equal(op(op(e3,e2),e1),op(e3,op(e2,e1)))
| ~ equal(op(op(e3,e2),e2),op(e3,op(e2,e2)))
| ~ equal(op(op(e3,e2),e3),op(e3,op(e2,e3)))
| ~ equal(op(op(e3,e2),e4),op(e3,op(e2,e4)))
| ~ equal(op(op(e3,e2),e5),op(e3,op(e2,e5)))
| ~ equal(op(op(e3,e3),e0),op(e3,op(e3,e0)))
| ~ equal(op(op(e3,e3),e1),op(e3,op(e3,e1)))
| ~ equal(op(op(e3,e3),e2),op(e3,op(e3,e2)))
| ~ equal(op(op(e3,e3),e3),op(e3,op(e3,e3)))
| ~ equal(op(op(e3,e3),e4),op(e3,op(e3,e4)))
| ~ equal(op(op(e3,e3),e5),op(e3,op(e3,e5)))
| ~ equal(op(op(e3,e4),e0),op(e3,op(e4,e0)))
| ~ equal(op(op(e3,e4),e1),op(e3,op(e4,e1)))
| ~ equal(op(op(e3,e4),e2),op(e3,op(e4,e2)))
| ~ equal(op(op(e3,e4),e3),op(e3,op(e4,e3)))
| ~ equal(op(op(e3,e4),e4),op(e3,op(e4,e4)))
| ~ equal(op(op(e3,e4),e5),op(e3,op(e4,e5)))
| ~ equal(op(op(e3,e5),e0),op(e3,op(e5,e0)))
| ~ equal(op(op(e3,e5),e1),op(e3,op(e5,e1)))
| ~ equal(op(op(e3,e5),e2),op(e3,op(e5,e2)))
| ~ equal(op(op(e3,e5),e3),op(e3,op(e5,e3)))
| ~ equal(op(op(e3,e5),e4),op(e3,op(e5,e4)))
| ~ equal(op(op(e3,e5),e5),op(e3,op(e5,e5)))
| ~ equal(op(op(e4,e0),e0),op(e4,op(e0,e0)))
| ~ equal(op(op(e4,e0),e1),op(e4,op(e0,e1)))
| ~ equal(op(op(e4,e0),e2),op(e4,op(e0,e2)))
| ~ equal(op(op(e4,e0),e3),op(e4,op(e0,e3)))
| ~ equal(op(op(e4,e0),e4),op(e4,op(e0,e4)))
| ~ equal(op(op(e4,e0),e5),op(e4,op(e0,e5)))
| ~ equal(op(op(e4,e1),e0),op(e4,op(e1,e0)))
| ~ equal(op(op(e4,e1),e1),op(e4,op(e1,e1)))
| ~ equal(op(op(e4,e1),e2),op(e4,op(e1,e2)))
| ~ equal(op(op(e4,e1),e3),op(e4,op(e1,e3)))
| ~ equal(op(op(e4,e1),e4),op(e4,op(e1,e4)))
| ~ equal(op(op(e4,e1),e5),op(e4,op(e1,e5)))
| ~ equal(op(op(e4,e2),e0),op(e4,op(e2,e0)))
| ~ equal(op(op(e4,e2),e1),op(e4,op(e2,e1)))
| ~ equal(op(op(e4,e2),e2),op(e4,op(e2,e2)))
| ~ equal(op(op(e4,e2),e3),op(e4,op(e2,e3)))
| ~ equal(op(op(e4,e2),e4),op(e4,op(e2,e4)))
| ~ equal(op(op(e4,e2),e5),op(e4,op(e2,e5)))
| ~ equal(op(op(e4,e3),e0),op(e4,op(e3,e0)))
| ~ equal(op(op(e4,e3),e1),op(e4,op(e3,e1)))
| ~ equal(op(op(e4,e3),e2),op(e4,op(e3,e2)))
| ~ equal(op(op(e4,e3),e3),op(e4,op(e3,e3)))
| ~ equal(op(op(e4,e3),e4),op(e4,op(e3,e4)))
| ~ equal(op(op(e4,e3),e5),op(e4,op(e3,e5)))
| ~ equal(op(op(e4,e4),e0),op(e4,op(e4,e0)))
| ~ equal(op(op(e4,e4),e1),op(e4,op(e4,e1)))
| ~ equal(op(op(e4,e4),e2),op(e4,op(e4,e2)))
| ~ equal(op(op(e4,e4),e3),op(e4,op(e4,e3)))
| ~ equal(op(op(e4,e4),e4),op(e4,op(e4,e4)))
| ~ equal(op(op(e4,e4),e5),op(e4,op(e4,e5)))
| ~ equal(op(op(e4,e5),e0),op(e4,op(e5,e0)))
| ~ equal(op(op(e4,e5),e1),op(e4,op(e5,e1)))
| ~ equal(op(op(e4,e5),e2),op(e4,op(e5,e2)))
| ~ equal(op(op(e4,e5),e3),op(e4,op(e5,e3)))
| ~ equal(op(op(e4,e5),e4),op(e4,op(e5,e4)))
| ~ equal(op(op(e4,e5),e5),op(e4,op(e5,e5)))
| ~ equal(op(op(e5,e0),e0),op(e5,op(e0,e0)))
| ~ equal(op(op(e5,e0),e1),op(e5,op(e0,e1)))
| ~ equal(op(op(e5,e0),e2),op(e5,op(e0,e2)))
| ~ equal(op(op(e5,e0),e3),op(e5,op(e0,e3)))
| ~ equal(op(op(e5,e0),e4),op(e5,op(e0,e4)))
| ~ equal(op(op(e5,e0),e5),op(e5,op(e0,e5)))
| ~ equal(op(op(e5,e1),e0),op(e5,op(e1,e0)))
| ~ equal(op(op(e5,e1),e1),op(e5,op(e1,e1)))
| ~ equal(op(op(e5,e1),e2),op(e5,op(e1,e2)))
| ~ equal(op(op(e5,e1),e3),op(e5,op(e1,e3)))
| ~ equal(op(op(e5,e1),e4),op(e5,op(e1,e4)))
| ~ equal(op(op(e5,e1),e5),op(e5,op(e1,e5)))
| ~ equal(op(op(e5,e2),e0),op(e5,op(e2,e0)))
| ~ equal(op(op(e5,e2),e1),op(e5,op(e2,e1)))
| ~ equal(op(op(e5,e2),e2),op(e5,op(e2,e2)))
| ~ equal(op(op(e5,e2),e3),op(e5,op(e2,e3)))
| ~ equal(op(op(e5,e2),e4),op(e5,op(e2,e4)))
| ~ equal(op(op(e5,e2),e5),op(e5,op(e2,e5)))
| ~ equal(op(op(e5,e3),e0),op(e5,op(e3,e0)))
| ~ equal(op(op(e5,e3),e1),op(e5,op(e3,e1)))
| ~ equal(op(op(e5,e3),e2),op(e5,op(e3,e2)))
| ~ equal(op(op(e5,e3),e3),op(e5,op(e3,e3)))
| ~ equal(op(op(e5,e3),e4),op(e5,op(e3,e4)))
| ~ equal(op(op(e5,e3),e5),op(e5,op(e3,e5)))
| ~ equal(op(op(e5,e4),e0),op(e5,op(e4,e0)))
| ~ equal(op(op(e5,e4),e1),op(e5,op(e4,e1)))
| ~ equal(op(op(e5,e4),e2),op(e5,op(e4,e2)))
| ~ equal(op(op(e5,e4),e3),op(e5,op(e4,e3)))
| ~ equal(op(op(e5,e4),e4),op(e5,op(e4,e4)))
| ~ equal(op(op(e5,e4),e5),op(e5,op(e4,e5)))
| ~ equal(op(op(e5,e5),e0),op(e5,op(e5,e0)))
| ~ equal(op(op(e5,e5),e1),op(e5,op(e5,e1)))
| ~ equal(op(op(e5,e5),e2),op(e5,op(e5,e2)))
| ~ equal(op(op(e5,e5),e3),op(e5,op(e5,e3)))
| ~ equal(op(op(e5,e5),e4),op(e5,op(e5,e4)))
| ~ equal(op(op(e5,e5),e5),op(e5,op(e5,e5)))
| ~ equal(op(unit,e0),e0)
| ~ equal(op(e0,unit),e0)
| ~ equal(op(unit,e1),e1)
| ~ equal(op(e1,unit),e1)
| ~ equal(op(unit,e2),e2)
| ~ equal(op(e2,unit),e2)
| ~ equal(op(unit,e3),e3)
| ~ equal(op(e3,unit),e3)
| ~ equal(op(unit,e4),e4)
| ~ equal(op(e4,unit),e4)
| ~ equal(op(unit,e5),e5)
| ~ equal(op(e5,unit),e5)
| ~ skC36
| ~ equal(op(e0,inv(e0)),unit)
| ~ equal(op(inv(e0),e0),unit)
| ~ equal(op(e1,inv(e1)),unit)
| ~ equal(op(inv(e1),e1),unit)
| ~ equal(op(e2,inv(e2)),unit)
| ~ equal(op(inv(e2),e2),unit)
| ~ equal(op(e3,inv(e3)),unit)
| ~ equal(op(inv(e3),e3),unit)
| ~ equal(op(e4,inv(e4)),unit)
| ~ equal(op(inv(e4),e4),unit)
| ~ equal(op(e5,inv(e5)),unit)
| ~ equal(op(inv(e5),e5),unit)
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41 ),
file('ALG032+1.p',unknown),
[] ).
cnf(317,plain,
equal(inv(unit),unit),
inference(rew,[status(thm),theory(equality)],[1,17]),
[iquote('0:Rew:1.0,17.0')] ).
cnf(323,plain,
equal(op(e5,e4),unit),
inference(rew,[status(thm),theory(equality)],[1,63]),
[iquote('0:Rew:1.0,63.0')] ).
cnf(324,plain,
equal(op(e5,unit),e5),
inference(rew,[status(thm),theory(equality)],[1,59]),
[iquote('0:Rew:1.0,59.0')] ).
cnf(325,plain,
equal(op(e4,e5),unit),
inference(rew,[status(thm),theory(equality)],[1,58]),
[iquote('0:Rew:1.0,58.0')] ).
cnf(326,plain,
equal(op(e4,unit),e4),
inference(rew,[status(thm),theory(equality)],[1,53]),
[iquote('0:Rew:1.0,53.0')] ).
cnf(327,plain,
equal(op(e3,e2),unit),
inference(rew,[status(thm),theory(equality)],[1,49]),
[iquote('0:Rew:1.0,49.0')] ).
cnf(328,plain,
equal(op(e3,unit),e3),
inference(rew,[status(thm),theory(equality)],[1,47]),
[iquote('0:Rew:1.0,47.0')] ).
cnf(329,plain,
equal(op(e2,e3),unit),
inference(rew,[status(thm),theory(equality)],[1,44]),
[iquote('0:Rew:1.0,44.0')] ).
cnf(330,plain,
equal(op(e2,unit),e2),
inference(rew,[status(thm),theory(equality)],[1,41]),
[iquote('0:Rew:1.0,41.0')] ).
cnf(331,plain,
equal(op(e1,e1),unit),
inference(rew,[status(thm),theory(equality)],[1,36]),
[iquote('0:Rew:1.0,36.0')] ).
cnf(332,plain,
equal(op(e1,unit),e1),
inference(rew,[status(thm),theory(equality)],[1,35]),
[iquote('0:Rew:1.0,35.0')] ).
cnf(333,plain,
equal(op(unit,e5),e5),
inference(rew,[status(thm),theory(equality)],[1,34]),
[iquote('0:Rew:1.0,34.0')] ).
cnf(334,plain,
equal(op(unit,e4),e4),
inference(rew,[status(thm),theory(equality)],[1,33]),
[iquote('0:Rew:1.0,33.0')] ).
cnf(335,plain,
equal(op(unit,e3),e3),
inference(rew,[status(thm),theory(equality)],[1,32]),
[iquote('0:Rew:1.0,32.0')] ).
cnf(336,plain,
equal(op(unit,e2),e2),
inference(rew,[status(thm),theory(equality)],[1,31]),
[iquote('0:Rew:1.0,31.0')] ).
cnf(337,plain,
equal(op(unit,e1),e1),
inference(rew,[status(thm),theory(equality)],[1,30]),
[iquote('0:Rew:1.0,30.0')] ).
cnf(338,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[1,29]),
[iquote('0:Rew:1.0,29.0')] ).
cnf(339,plain,
( ~ equal(unit,unit)
| skC36 ),
inference(rew,[status(thm),theory(equality)],[1,23]),
[iquote('0:Rew:1.0,23.0')] ).
cnf(340,plain,
skC36,
inference(obv,[status(thm),theory(equality)],[339]),
[iquote('0:Obv:339.0')] ).
cnf(341,plain,
( ~ equal(e5,e5)
| skC41 ),
inference(rew,[status(thm),theory(equality)],[21,94]),
[iquote('0:Rew:21.0,94.0')] ).
cnf(342,plain,
skC41,
inference(obv,[status(thm),theory(equality)],[341]),
[iquote('0:Obv:341.0')] ).
cnf(346,plain,
( ~ equal(e2,e2)
| skC40 ),
inference(rew,[status(thm),theory(equality)],[20,85]),
[iquote('0:Rew:20.0,85.0')] ).
cnf(347,plain,
skC40,
inference(obv,[status(thm),theory(equality)],[346]),
[iquote('0:Obv:346.0')] ).
cnf(350,plain,
( ~ equal(e3,e3)
| skC39 ),
inference(rew,[status(thm),theory(equality)],[19,80]),
[iquote('0:Rew:19.0,80.0')] ).
cnf(351,plain,
skC39,
inference(obv,[status(thm),theory(equality)],[350]),
[iquote('0:Obv:350.0')] ).
cnf(356,plain,
( ~ equal(e1,e1)
| skC38 ),
inference(rew,[status(thm),theory(equality)],[18,72]),
[iquote('0:Rew:18.0,72.0')] ).
cnf(357,plain,
skC38,
inference(obv,[status(thm),theory(equality)],[356]),
[iquote('0:Obv:356.0')] ).
cnf(363,plain,
( ~ equal(unit,unit)
| skC37 ),
inference(rew,[status(thm),theory(equality)],[317,65,1]),
[iquote('0:Rew:317.0,65.0,1.0,65.0')] ).
cnf(364,plain,
skC37,
inference(obv,[status(thm),theory(equality)],[363]),
[iquote('0:Obv:363.0')] ).
cnf(368,plain,
( ~ equal(e2,e2)
| skC35 ),
inference(rew,[status(thm),theory(equality)],[64,307]),
[iquote('0:Rew:64.0,307.0')] ).
cnf(369,plain,
skC35,
inference(obv,[status(thm),theory(equality)],[368]),
[iquote('0:Obv:368.0')] ).
cnf(375,plain,
( ~ equal(unit,unit)
| skC34 ),
inference(rew,[status(thm),theory(equality)],[323,299,1]),
[iquote('0:Rew:323.0,299.0,1.0,299.0')] ).
cnf(376,plain,
skC34,
inference(obv,[status(thm),theory(equality)],[375]),
[iquote('0:Obv:375.0')] ).
cnf(378,plain,
( ~ equal(e4,e4)
| skC33 ),
inference(rew,[status(thm),theory(equality)],[62,297]),
[iquote('0:Rew:62.0,297.0')] ).
cnf(379,plain,
skC33,
inference(obv,[status(thm),theory(equality)],[378]),
[iquote('0:Obv:378.0')] ).
cnf(384,plain,
( ~ equal(e1,e1)
| skC32 ),
inference(rew,[status(thm),theory(equality)],[61,288]),
[iquote('0:Rew:61.0,288.0')] ).
cnf(385,plain,
skC32,
inference(obv,[status(thm),theory(equality)],[384]),
[iquote('0:Obv:384.0')] ).
cnf(388,plain,
( ~ equal(e3,e3)
| skC31 ),
inference(rew,[status(thm),theory(equality)],[60,284]),
[iquote('0:Rew:60.0,284.0')] ).
cnf(389,plain,
skC31,
inference(obv,[status(thm),theory(equality)],[388]),
[iquote('0:Obv:388.0')] ).
cnf(390,plain,
( ~ equal(e5,e5)
| skC30 ),
inference(rew,[status(thm),theory(equality)],[324,280,1]),
[iquote('0:Rew:324.0,280.0,1.0,280.0')] ).
cnf(391,plain,
skC30,
inference(obv,[status(thm),theory(equality)],[390]),
[iquote('0:Obv:390.0')] ).
cnf(397,plain,
( ~ equal(unit,unit)
| skC29 ),
inference(rew,[status(thm),theory(equality)],[325,269,1]),
[iquote('0:Rew:325.0,269.0,1.0,269.0')] ).
cnf(398,plain,
skC29,
inference(obv,[status(thm),theory(equality)],[397]),
[iquote('0:Obv:397.0')] ).
cnf(401,plain,
( ~ equal(e3,e3)
| skC28 ),
inference(rew,[status(thm),theory(equality)],[57,266]),
[iquote('0:Rew:57.0,266.0')] ).
cnf(402,plain,
skC28,
inference(obv,[status(thm),theory(equality)],[401]),
[iquote('0:Obv:401.0')] ).
cnf(407,plain,
( ~ equal(e1,e1)
| skC27 ),
inference(rew,[status(thm),theory(equality)],[56,258]),
[iquote('0:Rew:56.0,258.0')] ).
cnf(408,plain,
skC27,
inference(obv,[status(thm),theory(equality)],[407]),
[iquote('0:Obv:407.0')] ).
cnf(409,plain,
( ~ equal(e5,e5)
| skC26 ),
inference(rew,[status(thm),theory(equality)],[55,256]),
[iquote('0:Rew:55.0,256.0')] ).
cnf(410,plain,
skC26,
inference(obv,[status(thm),theory(equality)],[409]),
[iquote('0:Obv:409.0')] ).
cnf(414,plain,
( ~ equal(e2,e2)
| skC25 ),
inference(rew,[status(thm),theory(equality)],[54,247]),
[iquote('0:Rew:54.0,247.0')] ).
cnf(415,plain,
skC25,
inference(obv,[status(thm),theory(equality)],[414]),
[iquote('0:Obv:414.0')] ).
cnf(417,plain,
( ~ equal(e4,e4)
| skC24 ),
inference(rew,[status(thm),theory(equality)],[326,243,1]),
[iquote('0:Rew:326.0,243.0,1.0,243.0')] ).
cnf(418,plain,
skC24,
inference(obv,[status(thm),theory(equality)],[417]),
[iquote('0:Obv:417.0')] ).
cnf(420,plain,
( ~ equal(e4,e4)
| skC23 ),
inference(rew,[status(thm),theory(equality)],[52,237]),
[iquote('0:Rew:52.0,237.0')] ).
cnf(421,plain,
skC23,
inference(obv,[status(thm),theory(equality)],[420]),
[iquote('0:Obv:420.0')] ).
cnf(426,plain,
( ~ equal(e1,e1)
| skC22 ),
inference(rew,[status(thm),theory(equality)],[51,228]),
[iquote('0:Rew:51.0,228.0')] ).
cnf(427,plain,
skC22,
inference(obv,[status(thm),theory(equality)],[426]),
[iquote('0:Obv:426.0')] ).
cnf(431,plain,
( ~ equal(e2,e2)
| skC21 ),
inference(rew,[status(thm),theory(equality)],[50,223]),
[iquote('0:Rew:50.0,223.0')] ).
cnf(432,plain,
skC21,
inference(obv,[status(thm),theory(equality)],[431]),
[iquote('0:Obv:431.0')] ).
cnf(438,plain,
( ~ equal(unit,unit)
| skC20 ),
inference(rew,[status(thm),theory(equality)],[327,215,1]),
[iquote('0:Rew:327.0,215.0,1.0,215.0')] ).
cnf(439,plain,
skC20,
inference(obv,[status(thm),theory(equality)],[438]),
[iquote('0:Obv:438.0')] ).
cnf(440,plain,
( ~ equal(e5,e5)
| skC19 ),
inference(rew,[status(thm),theory(equality)],[48,214]),
[iquote('0:Rew:48.0,214.0')] ).
cnf(441,plain,
skC19,
inference(obv,[status(thm),theory(equality)],[440]),
[iquote('0:Obv:440.0')] ).
cnf(444,plain,
( ~ equal(e3,e3)
| skC18 ),
inference(rew,[status(thm),theory(equality)],[328,206,1]),
[iquote('0:Rew:328.0,206.0,1.0,206.0')] ).
cnf(445,plain,
skC18,
inference(obv,[status(thm),theory(equality)],[444]),
[iquote('0:Obv:444.0')] ).
cnf(450,plain,
( ~ equal(e1,e1)
| skC17 ),
inference(rew,[status(thm),theory(equality)],[46,198]),
[iquote('0:Rew:46.0,198.0')] ).
cnf(451,plain,
skC17,
inference(obv,[status(thm),theory(equality)],[450]),
[iquote('0:Obv:450.0')] ).
cnf(452,plain,
( ~ equal(e5,e5)
| skC16 ),
inference(rew,[status(thm),theory(equality)],[45,196]),
[iquote('0:Rew:45.0,196.0')] ).
cnf(453,plain,
skC16,
inference(obv,[status(thm),theory(equality)],[452]),
[iquote('0:Obv:452.0')] ).
cnf(459,plain,
( ~ equal(unit,unit)
| skC15 ),
inference(rew,[status(thm),theory(equality)],[329,185,1]),
[iquote('0:Rew:329.0,185.0,1.0,185.0')] ).
cnf(460,plain,
skC15,
inference(obv,[status(thm),theory(equality)],[459]),
[iquote('0:Obv:459.0')] ).
cnf(463,plain,
( ~ equal(e3,e3)
| skC14 ),
inference(rew,[status(thm),theory(equality)],[43,182]),
[iquote('0:Rew:43.0,182.0')] ).
cnf(464,plain,
skC14,
inference(obv,[status(thm),theory(equality)],[463]),
[iquote('0:Obv:463.0')] ).
cnf(466,plain,
( ~ equal(e4,e4)
| skC13 ),
inference(rew,[status(thm),theory(equality)],[42,177]),
[iquote('0:Rew:42.0,177.0')] ).
cnf(467,plain,
skC13,
inference(obv,[status(thm),theory(equality)],[466]),
[iquote('0:Obv:466.0')] ).
cnf(471,plain,
( ~ equal(e2,e2)
| skC12 ),
inference(rew,[status(thm),theory(equality)],[330,169,1]),
[iquote('0:Rew:330.0,169.0,1.0,169.0')] ).
cnf(472,plain,
skC12,
inference(obv,[status(thm),theory(equality)],[471]),
[iquote('0:Obv:471.0')] ).
cnf(475,plain,
( ~ equal(e3,e3)
| skC11 ),
inference(rew,[status(thm),theory(equality)],[40,164]),
[iquote('0:Rew:40.0,164.0')] ).
cnf(476,plain,
skC11,
inference(obv,[status(thm),theory(equality)],[475]),
[iquote('0:Obv:475.0')] ).
cnf(480,plain,
( ~ equal(e2,e2)
| skC10 ),
inference(rew,[status(thm),theory(equality)],[39,157]),
[iquote('0:Rew:39.0,157.0')] ).
cnf(481,plain,
skC10,
inference(obv,[status(thm),theory(equality)],[480]),
[iquote('0:Obv:480.0')] ).
cnf(482,plain,
( ~ equal(e5,e5)
| skC9 ),
inference(rew,[status(thm),theory(equality)],[38,154]),
[iquote('0:Rew:38.0,154.0')] ).
cnf(483,plain,
skC9,
inference(obv,[status(thm),theory(equality)],[482]),
[iquote('0:Obv:482.0')] ).
cnf(485,plain,
( ~ equal(e4,e4)
| skC8 ),
inference(rew,[status(thm),theory(equality)],[37,147]),
[iquote('0:Rew:37.0,147.0')] ).
cnf(486,plain,
skC8,
inference(obv,[status(thm),theory(equality)],[485]),
[iquote('0:Obv:485.0')] ).
cnf(492,plain,
( ~ equal(unit,unit)
| skC7 ),
inference(rew,[status(thm),theory(equality)],[331,137,1]),
[iquote('0:Rew:331.0,137.0,1.0,137.0')] ).
cnf(493,plain,
skC7,
inference(obv,[status(thm),theory(equality)],[492]),
[iquote('0:Obv:492.0')] ).
cnf(498,plain,
( ~ equal(e1,e1)
| skC6 ),
inference(rew,[status(thm),theory(equality)],[332,132,1]),
[iquote('0:Rew:332.0,132.0,1.0,132.0')] ).
cnf(499,plain,
skC6,
inference(obv,[status(thm),theory(equality)],[498]),
[iquote('0:Obv:498.0')] ).
cnf(500,plain,
( ~ equal(e5,e5)
| skC5 ),
inference(rew,[status(thm),theory(equality)],[333,130,1]),
[iquote('0:Rew:333.0,130.0,1.0,130.0')] ).
cnf(501,plain,
skC5,
inference(obv,[status(thm),theory(equality)],[500]),
[iquote('0:Obv:500.0')] ).
cnf(503,plain,
( ~ equal(e4,e4)
| skC4 ),
inference(rew,[status(thm),theory(equality)],[334,123,1]),
[iquote('0:Rew:334.0,123.0,1.0,123.0')] ).
cnf(504,plain,
skC4,
inference(obv,[status(thm),theory(equality)],[503]),
[iquote('0:Obv:503.0')] ).
cnf(507,plain,
( ~ equal(e3,e3)
| skC3 ),
inference(rew,[status(thm),theory(equality)],[335,116,1]),
[iquote('0:Rew:335.0,116.0,1.0,116.0')] ).
cnf(508,plain,
skC3,
inference(obv,[status(thm),theory(equality)],[507]),
[iquote('0:Obv:507.0')] ).
cnf(512,plain,
( ~ equal(e2,e2)
| skC2 ),
inference(rew,[status(thm),theory(equality)],[336,109,1]),
[iquote('0:Rew:336.0,109.0,1.0,109.0')] ).
cnf(513,plain,
skC2,
inference(obv,[status(thm),theory(equality)],[512]),
[iquote('0:Obv:512.0')] ).
cnf(518,plain,
( ~ equal(e1,e1)
| skC1 ),
inference(rew,[status(thm),theory(equality)],[337,102,1]),
[iquote('0:Rew:337.0,102.0,1.0,102.0')] ).
cnf(519,plain,
skC1,
inference(obv,[status(thm),theory(equality)],[518]),
[iquote('0:Obv:518.0')] ).
cnf(525,plain,
( ~ equal(unit,unit)
| skC0 ),
inference(rew,[status(thm),theory(equality)],[338,95,1]),
[iquote('0:Rew:338.0,95.0,1.0,95.0')] ).
cnf(526,plain,
skC0,
inference(obv,[status(thm),theory(equality)],[525]),
[iquote('0:Obv:525.0')] ).
cnf(530,plain,
( ~ equal(inv(e5),e4)
| ~ equal(op(e0,e1),op(e1,e0))
| ~ equal(op(e2,e0),op(e0,e2))
| ~ equal(op(e3,e0),op(e0,e3))
| ~ equal(op(e4,e0),op(e0,e4))
| ~ equal(op(e5,e0),op(e0,e5))
| ~ equal(op(e2,e1),op(e1,e2))
| ~ equal(op(e3,e1),op(e1,e3))
| ~ equal(op(e4,e1),op(e1,e4))
| ~ equal(op(e5,e1),op(e1,e5))
| ~ equal(op(e2,e3),op(e3,e2))
| ~ equal(op(e4,e2),op(e2,e4))
| ~ equal(op(e5,e2),op(e2,e5))
| ~ equal(op(e4,e3),op(e3,e4))
| ~ equal(op(e5,e3),op(e3,e5))
| ~ equal(op(e4,e5),op(e5,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
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ equal(op(op(e0,e0),e0),op(e0,op(e0,e0)))
| ~ equal(op(op(e0,e0),e1),op(e0,op(e0,e1)))
| ~ equal(op(op(e0,e0),e2),op(e0,op(e0,e2)))
| ~ equal(op(op(e0,e0),e3),op(e0,op(e0,e3)))
| ~ equal(op(op(e0,e0),e4),op(e0,op(e0,e4)))
| ~ equal(op(op(e0,e0),e5),op(e0,op(e0,e5)))
| ~ equal(op(op(e0,e1),e0),op(e0,op(e1,e0)))
| ~ equal(op(op(e0,e1),e1),op(e0,op(e1,e1)))
| ~ equal(op(op(e0,e1),e2),op(e0,op(e1,e2)))
| ~ equal(op(op(e0,e1),e3),op(e0,op(e1,e3)))
| ~ equal(op(op(e0,e1),e4),op(e0,op(e1,e4)))
| ~ equal(op(op(e0,e1),e5),op(e0,op(e1,e5)))
| ~ equal(op(op(e0,e2),e0),op(e0,op(e2,e0)))
| ~ equal(op(op(e0,e2),e1),op(e0,op(e2,e1)))
| ~ equal(op(op(e0,e2),e2),op(e0,op(e2,e2)))
| ~ equal(op(op(e0,e2),e3),op(e0,op(e2,e3)))
| ~ equal(op(op(e0,e2),e4),op(e0,op(e2,e4)))
| ~ equal(op(op(e0,e2),e5),op(e0,op(e2,e5)))
| ~ equal(op(op(e0,e3),e0),op(e0,op(e3,e0)))
| ~ equal(op(op(e0,e3),e1),op(e0,op(e3,e1)))
| ~ equal(op(op(e0,e3),e2),op(e0,op(e3,e2)))
| ~ equal(op(op(e0,e3),e3),op(e0,op(e3,e3)))
| ~ equal(op(op(e0,e3),e4),op(e0,op(e3,e4)))
| ~ equal(op(op(e0,e3),e5),op(e0,op(e3,e5)))
| ~ equal(op(op(e0,e4),e0),op(e0,op(e4,e0)))
| ~ equal(op(op(e0,e4),e1),op(e0,op(e4,e1)))
| ~ equal(op(op(e0,e4),e2),op(e0,op(e4,e2)))
| ~ equal(op(op(e0,e4),e3),op(e0,op(e4,e3)))
| ~ equal(op(op(e0,e4),e4),op(e0,op(e4,e4)))
| ~ equal(op(op(e0,e4),e5),op(e0,op(e4,e5)))
| ~ equal(op(op(e0,e5),e0),op(e0,op(e5,e0)))
| ~ equal(op(op(e0,e5),e1),op(e0,op(e5,e1)))
| ~ equal(op(op(e0,e5),e2),op(e0,op(e5,e2)))
| ~ equal(op(op(e0,e5),e3),op(e0,op(e5,e3)))
| ~ equal(op(op(e0,e5),e4),op(e0,op(e5,e4)))
| ~ equal(op(op(e0,e5),e5),op(e0,op(e5,e5)))
| ~ equal(op(op(e1,e0),e0),op(e1,op(e0,e0)))
| ~ equal(op(op(e1,e0),e1),op(e1,op(e0,e1)))
| ~ equal(op(op(e1,e0),e2),op(e1,op(e0,e2)))
| ~ equal(op(op(e1,e0),e3),op(e1,op(e0,e3)))
| ~ equal(op(op(e1,e0),e4),op(e1,op(e0,e4)))
| ~ equal(op(op(e1,e0),e5),op(e1,op(e0,e5)))
| ~ equal(op(op(e1,e1),e0),op(e1,op(e1,e0)))
| ~ equal(op(op(e1,e1),e1),op(e1,op(e1,e1)))
| ~ equal(op(op(e1,e1),e2),op(e1,op(e1,e2)))
| ~ equal(op(op(e1,e1),e3),op(e1,op(e1,e3)))
| ~ equal(op(op(e1,e1),e4),op(e1,op(e1,e4)))
| ~ equal(op(op(e1,e1),e5),op(e1,op(e1,e5)))
| ~ equal(op(op(e1,e2),e0),op(e1,op(e2,e0)))
| ~ equal(op(op(e1,e2),e1),op(e1,op(e2,e1)))
| ~ equal(op(op(e1,e2),e2),op(e1,op(e2,e2)))
| ~ equal(op(op(e1,e2),e3),op(e1,op(e2,e3)))
| ~ equal(op(op(e1,e2),e4),op(e1,op(e2,e4)))
| ~ equal(op(op(e1,e2),e5),op(e1,op(e2,e5)))
| ~ equal(op(op(e1,e3),e0),op(e1,op(e3,e0)))
| ~ equal(op(op(e1,e3),e1),op(e1,op(e3,e1)))
| ~ equal(op(op(e1,e3),e2),op(e1,op(e3,e2)))
| ~ equal(op(op(e1,e3),e3),op(e1,op(e3,e3)))
| ~ equal(op(op(e1,e3),e4),op(e1,op(e3,e4)))
| ~ equal(op(op(e1,e3),e5),op(e1,op(e3,e5)))
| ~ equal(op(op(e1,e4),e0),op(e1,op(e4,e0)))
| ~ equal(op(op(e1,e4),e1),op(e1,op(e4,e1)))
| ~ equal(op(op(e1,e4),e2),op(e1,op(e4,e2)))
| ~ equal(op(op(e1,e4),e3),op(e1,op(e4,e3)))
| ~ equal(op(op(e1,e4),e4),op(e1,op(e4,e4)))
| ~ equal(op(op(e1,e4),e5),op(e1,op(e4,e5)))
| ~ equal(op(op(e1,e5),e0),op(e1,op(e5,e0)))
| ~ equal(op(op(e1,e5),e1),op(e1,op(e5,e1)))
| ~ equal(op(op(e1,e5),e2),op(e1,op(e5,e2)))
| ~ equal(op(op(e1,e5),e3),op(e1,op(e5,e3)))
| ~ equal(op(op(e1,e5),e4),op(e1,op(e5,e4)))
| ~ equal(op(op(e1,e5),e5),op(e1,op(e5,e5)))
| ~ equal(op(op(e2,e0),e0),op(e2,op(e0,e0)))
| ~ equal(op(op(e2,e0),e1),op(e2,op(e0,e1)))
| ~ equal(op(op(e2,e0),e2),op(e2,op(e0,e2)))
| ~ equal(op(op(e2,e0),e3),op(e2,op(e0,e3)))
| ~ equal(op(op(e2,e0),e4),op(e2,op(e0,e4)))
| ~ equal(op(op(e2,e0),e5),op(e2,op(e0,e5)))
| ~ equal(op(op(e2,e1),e0),op(e2,op(e1,e0)))
| ~ equal(op(op(e2,e1),e1),op(e2,op(e1,e1)))
| ~ equal(op(op(e2,e1),e2),op(e2,op(e1,e2)))
| ~ equal(op(op(e2,e1),e3),op(e2,op(e1,e3)))
| ~ equal(op(op(e2,e1),e4),op(e2,op(e1,e4)))
| ~ equal(op(op(e2,e1),e5),op(e2,op(e1,e5)))
| ~ equal(op(op(e2,e2),e0),op(e2,op(e2,e0)))
| ~ equal(op(op(e2,e2),e1),op(e2,op(e2,e1)))
| ~ equal(op(op(e2,e2),e2),op(e2,op(e2,e2)))
| ~ equal(op(op(e2,e2),e3),op(e2,op(e2,e3)))
| ~ equal(op(op(e2,e2),e4),op(e2,op(e2,e4)))
| ~ equal(op(op(e2,e2),e5),op(e2,op(e2,e5)))
| ~ equal(op(op(e2,e3),e0),op(e2,op(e3,e0)))
| ~ equal(op(op(e2,e3),e1),op(e2,op(e3,e1)))
| ~ equal(op(op(e2,e3),e2),op(e2,op(e3,e2)))
| ~ equal(op(op(e2,e3),e3),op(e2,op(e3,e3)))
| ~ equal(op(op(e2,e3),e4),op(e2,op(e3,e4)))
| ~ equal(op(op(e2,e3),e5),op(e2,op(e3,e5)))
| ~ equal(op(op(e2,e4),e0),op(e2,op(e4,e0)))
| ~ equal(op(op(e2,e4),e1),op(e2,op(e4,e1)))
| ~ equal(op(op(e2,e4),e2),op(e2,op(e4,e2)))
| ~ equal(op(op(e2,e4),e3),op(e2,op(e4,e3)))
| ~ equal(op(op(e2,e4),e4),op(e2,op(e4,e4)))
| ~ equal(op(op(e2,e4),e5),op(e2,op(e4,e5)))
| ~ equal(op(op(e2,e5),e0),op(e2,op(e5,e0)))
| ~ equal(op(op(e2,e5),e1),op(e2,op(e5,e1)))
| ~ equal(op(op(e2,e5),e2),op(e2,op(e5,e2)))
| ~ equal(op(op(e2,e5),e3),op(e2,op(e5,e3)))
| ~ equal(op(op(e2,e5),e4),op(e2,op(e5,e4)))
| ~ equal(op(op(e2,e5),e5),op(e2,op(e5,e5)))
| ~ equal(op(op(e3,e0),e0),op(e3,op(e0,e0)))
| ~ equal(op(op(e3,e0),e1),op(e3,op(e0,e1)))
| ~ equal(op(op(e3,e0),e2),op(e3,op(e0,e2)))
| ~ equal(op(op(e3,e0),e3),op(e3,op(e0,e3)))
| ~ equal(op(op(e3,e0),e4),op(e3,op(e0,e4)))
| ~ equal(op(op(e3,e0),e5),op(e3,op(e0,e5)))
| ~ equal(op(op(e3,e1),e0),op(e3,op(e1,e0)))
| ~ equal(op(op(e3,e1),e1),op(e3,op(e1,e1)))
| ~ equal(op(op(e3,e1),e2),op(e3,op(e1,e2)))
| ~ equal(op(op(e3,e1),e3),op(e3,op(e1,e3)))
| ~ equal(op(op(e3,e1),e4),op(e3,op(e1,e4)))
| ~ equal(op(op(e3,e1),e5),op(e3,op(e1,e5)))
| ~ equal(op(op(e3,e2),e0),op(e3,op(e2,e0)))
| ~ equal(op(op(e3,e2),e1),op(e3,op(e2,e1)))
| ~ equal(op(op(e3,e2),e2),op(e3,op(e2,e2)))
| ~ equal(op(op(e3,e2),e3),op(e3,op(e2,e3)))
| ~ equal(op(op(e3,e2),e4),op(e3,op(e2,e4)))
| ~ equal(op(op(e3,e2),e5),op(e3,op(e2,e5)))
| ~ equal(op(op(e3,e3),e0),op(e3,op(e3,e0)))
| ~ equal(op(op(e3,e3),e1),op(e3,op(e3,e1)))
| ~ equal(op(op(e3,e3),e2),op(e3,op(e3,e2)))
| ~ equal(op(op(e3,e3),e3),op(e3,op(e3,e3)))
| ~ equal(op(op(e3,e3),e4),op(e3,op(e3,e4)))
| ~ equal(op(op(e3,e3),e5),op(e3,op(e3,e5)))
| ~ equal(op(op(e3,e4),e0),op(e3,op(e4,e0)))
| ~ equal(op(op(e3,e4),e1),op(e3,op(e4,e1)))
| ~ equal(op(op(e3,e4),e2),op(e3,op(e4,e2)))
| ~ equal(op(op(e3,e4),e3),op(e3,op(e4,e3)))
| ~ equal(op(op(e3,e4),e4),op(e3,op(e4,e4)))
| ~ equal(op(op(e3,e4),e5),op(e3,op(e4,e5)))
| ~ equal(op(op(e3,e5),e0),op(e3,op(e5,e0)))
| ~ equal(op(op(e3,e5),e1),op(e3,op(e5,e1)))
| ~ equal(op(op(e3,e5),e2),op(e3,op(e5,e2)))
| ~ equal(op(op(e3,e5),e3),op(e3,op(e5,e3)))
| ~ equal(op(op(e3,e5),e4),op(e3,op(e5,e4)))
| ~ equal(op(op(e3,e5),e5),op(e3,op(e5,e5)))
| ~ equal(op(op(e4,e0),e0),op(e4,op(e0,e0)))
| ~ equal(op(op(e4,e0),e1),op(e4,op(e0,e1)))
| ~ equal(op(op(e4,e0),e2),op(e4,op(e0,e2)))
| ~ equal(op(op(e4,e0),e3),op(e4,op(e0,e3)))
| ~ equal(op(op(e4,e0),e4),op(e4,op(e0,e4)))
| ~ equal(op(op(e4,e0),e5),op(e4,op(e0,e5)))
| ~ equal(op(op(e4,e1),e0),op(e4,op(e1,e0)))
| ~ equal(op(op(e4,e1),e1),op(e4,op(e1,e1)))
| ~ equal(op(op(e4,e1),e2),op(e4,op(e1,e2)))
| ~ equal(op(op(e4,e1),e3),op(e4,op(e1,e3)))
| ~ equal(op(op(e4,e1),e4),op(e4,op(e1,e4)))
| ~ equal(op(op(e4,e1),e5),op(e4,op(e1,e5)))
| ~ equal(op(op(e4,e2),e0),op(e4,op(e2,e0)))
| ~ equal(op(op(e4,e2),e1),op(e4,op(e2,e1)))
| ~ equal(op(op(e4,e2),e2),op(e4,op(e2,e2)))
| ~ equal(op(op(e4,e2),e3),op(e4,op(e2,e3)))
| ~ equal(op(op(e4,e2),e4),op(e4,op(e2,e4)))
| ~ equal(op(op(e4,e2),e5),op(e4,op(e2,e5)))
| ~ equal(op(op(e4,e3),e0),op(e4,op(e3,e0)))
| ~ equal(op(op(e4,e3),e1),op(e4,op(e3,e1)))
| ~ equal(op(op(e4,e3),e2),op(e4,op(e3,e2)))
| ~ equal(op(op(e4,e3),e3),op(e4,op(e3,e3)))
| ~ equal(op(op(e4,e3),e4),op(e4,op(e3,e4)))
| ~ equal(op(op(e4,e3),e5),op(e4,op(e3,e5)))
| ~ equal(op(op(e4,e4),e0),op(e4,op(e4,e0)))
| ~ equal(op(op(e4,e4),e1),op(e4,op(e4,e1)))
| ~ equal(op(op(e4,e4),e2),op(e4,op(e4,e2)))
| ~ equal(op(op(e4,e4),e3),op(e4,op(e4,e3)))
| ~ equal(op(op(e4,e4),e4),op(e4,op(e4,e4)))
| ~ equal(op(op(e4,e4),e5),op(e4,op(e4,e5)))
| ~ equal(op(op(e4,e5),e0),op(e4,op(e5,e0)))
| ~ equal(op(op(e4,e5),e1),op(e4,op(e5,e1)))
| ~ equal(op(op(e4,e5),e2),op(e4,op(e5,e2)))
| ~ equal(op(op(e4,e5),e3),op(e4,op(e5,e3)))
| ~ equal(op(op(e4,e5),e4),op(e4,op(e5,e4)))
| ~ equal(op(op(e4,e5),e5),op(e4,op(e5,e5)))
| ~ equal(op(op(e5,e0),e0),op(e5,op(e0,e0)))
| ~ equal(op(op(e5,e0),e1),op(e5,op(e0,e1)))
| ~ equal(op(op(e5,e0),e2),op(e5,op(e0,e2)))
| ~ equal(op(op(e5,e0),e3),op(e5,op(e0,e3)))
| ~ equal(op(op(e5,e0),e4),op(e5,op(e0,e4)))
| ~ equal(op(op(e5,e0),e5),op(e5,op(e0,e5)))
| ~ equal(op(op(e5,e1),e0),op(e5,op(e1,e0)))
| ~ equal(op(op(e5,e1),e1),op(e5,op(e1,e1)))
| ~ equal(op(op(e5,e1),e2),op(e5,op(e1,e2)))
| ~ equal(op(op(e5,e1),e3),op(e5,op(e1,e3)))
| ~ equal(op(op(e5,e1),e4),op(e5,op(e1,e4)))
| ~ equal(op(op(e5,e1),e5),op(e5,op(e1,e5)))
| ~ equal(op(op(e5,e2),e0),op(e5,op(e2,e0)))
| ~ equal(op(op(e5,e2),e1),op(e5,op(e2,e1)))
| ~ equal(op(op(e5,e2),e2),op(e5,op(e2,e2)))
| ~ equal(op(op(e5,e2),e3),op(e5,op(e2,e3)))
| ~ equal(op(op(e5,e2),e4),op(e5,op(e2,e4)))
| ~ equal(op(op(e5,e2),e5),op(e5,op(e2,e5)))
| ~ equal(op(op(e5,e3),e0),op(e5,op(e3,e0)))
| ~ equal(op(op(e5,e3),e1),op(e5,op(e3,e1)))
| ~ equal(op(op(e5,e3),e2),op(e5,op(e3,e2)))
| ~ equal(op(op(e5,e3),e3),op(e5,op(e3,e3)))
| ~ equal(op(op(e5,e3),e4),op(e5,op(e3,e4)))
| ~ equal(op(op(e5,e3),e5),op(e5,op(e3,e5)))
| ~ equal(op(op(e5,e4),e0),op(e5,op(e4,e0)))
| ~ equal(op(op(e5,e4),e1),op(e5,op(e4,e1)))
| ~ equal(op(op(e5,e4),e2),op(e5,op(e4,e2)))
| ~ equal(op(op(e5,e4),e3),op(e5,op(e4,e3)))
| ~ equal(op(op(e5,e4),e4),op(e5,op(e4,e4)))
| ~ equal(op(op(e5,e4),e5),op(e5,op(e4,e5)))
| ~ equal(op(op(e5,e5),e0),op(e5,op(e5,e0)))
| ~ equal(op(op(e5,e5),e1),op(e5,op(e5,e1)))
| ~ equal(op(op(e5,e5),e2),op(e5,op(e5,e2)))
| ~ equal(op(op(e5,e5),e3),op(e5,op(e5,e3)))
| ~ equal(op(op(e5,e5),e4),op(e5,op(e5,e4)))
| ~ equal(op(op(e5,e5),e5),op(e5,op(e5,e5)))
| ~ equal(op(unit,e0),e0)
| ~ equal(op(e0,unit),e0)
| ~ equal(op(unit,e1),e1)
| ~ equal(op(e1,unit),e1)
| ~ equal(op(unit,e2),e2)
| ~ equal(op(e2,unit),e2)
| ~ equal(op(unit,e3),e3)
| ~ equal(op(e3,unit),e3)
| ~ equal(op(unit,e4),e4)
| ~ equal(op(e4,unit),e4)
| ~ equal(op(unit,e5),e5)
| ~ equal(op(e5,unit),e5)
| ~ skC36
| ~ equal(op(e0,inv(e0)),unit)
| ~ equal(op(inv(e0),e0),unit)
| ~ equal(op(e1,inv(e1)),unit)
| ~ equal(op(inv(e1),e1),unit)
| ~ equal(op(e2,inv(e2)),unit)
| ~ equal(op(inv(e2),e2),unit)
| ~ equal(op(e3,inv(e3)),unit)
| ~ equal(op(inv(e3),e3),unit)
| ~ equal(op(e4,inv(e4)),unit)
| ~ equal(op(inv(e4),e4),unit)
| ~ equal(op(e5,inv(e5)),unit)
| ~ equal(op(inv(e5),e5),unit)
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41 ),
inference(obv,[status(thm),theory(equality)],[312]),
[iquote('0:Obv:312.21')] ).
cnf(531,plain,
( ~ equal(e4,e4)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e5,e5)
| ~ skC36
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41 ),
inference(rew,[status(thm),theory(equality)],[325,530,22,323,21,329,20,327,19,331,18,338,317,1,324,333,326,334,328,335,330,336,332,337,46,61,64,45,62,43,60,42,57,56,55,54,52,51,50,48,40,39,38,37]),
[iquote('0:Rew:325.0,530.292,22.0,530.292,323.0,530.291,22.0,530.291,323.0,530.290,21.0,530.290,325.0,530.289,21.0,530.289,329.0,530.288,20.0,530.288,327.0,530.287,20.0,530.287,327.0,530.286,19.0,530.286,329.0,530.285,19.0,530.285,331.0,530.284,18.0,530.284,331.0,530.283,18.0,530.283,338.0,530.282,317.0,530.282,1.0,530.282,338.0,530.281,317.0,530.281,1.0,530.281,324.0,530.279,333.0,530.278,326.0,530.277,334.0,530.276,328.0,530.275,335.0,530.274,330.0,530.273,336.0,530.272,332.0,530.271,337.0,530.270,338.0,530.269,1.0,530.269,338.0,530.268,1.0,530.268,46.0,530.267,61.0,530.267,64.0,530.267,45.0,530.266,64.0,530.266,324.0,530.266,323.0,530.266,329.0,530.265,64.0,530.265,323.0,530.265,62.0,530.265,43.0,530.264,64.0,530.264,60.0,530.264,61.0,530.264,42.0,530.263,64.0,530.263,62.0,530.263,60.0,530.263,330.0,530.262,64.0,530.262,324.0,530.262,1.0,530.262,333.0,530.261,323.0,530.261,324.0,530.261,325.0,530.261,334.0,530.260,323.0,530.260,62.0,530.260,57.0,530.260,335.0,530.259,323.0,530.259,60.0,530.259,56.0,530.259,336.0,530.258,323.0,530.258,64.0,530.258,55.0,530.258,337.0,530.257,323.0,530.257,61.0,530.257,54.0,530.257,338.0,530.256,323.0,530.256,326.0,530.256,1.0,530.256,325.0,530.255,62.0,530.255,323.0,530.255,52.0,530.255,57.0,530.254,62.0,530.254,60.0,530.254,51.0,530.254,56.0,530.253,62.0,530.253,61.0,530.253,50.0,530.253,55.0,530.252,62.0,530.252,324.0,530.252,327.0,530.252,54.0,530.251,62.0,530.251,64.0,530.251,48.0,530.251,326.0,530.250,62.0,530.250,328.0,530.250,1.0,530.250,40.0,530.249,61.0,530.249,60.0,530.249,46.0,530.249,39.0,530.248,61.0,530.248,64.0,530.248,45.0,530.248,38.0,530.247,61.0,530.247,324.0,530.247,329.0,530.247,37.0,530.246,61.0,530.246,62.0,530.246,43.0,530.246,331.0,530.245,61.0,530.245,323.0,530.245,42.0,530.245,332.0,530.244,61.0,530.244,330.0,530.244,1.0,530.244,52.0,530.243,60.0,530.243,62.0,530.243,40.0,530.243,51.0,530.242,60.0,530.242,61.0,530.242,39.0,530.242,50.0,530.241,60.0,530.241,64.0,530.241,38.0,530.241,327.0,530.240,60.0,530.240,323.0,530.240,37.0,530.240,48.0,530.239,60.0,530.239,324.0,530.239,331.0,530.239,328.0,530.238,60.0,530.238,332.0,530.238,1.0,530.238,64.0,530.237,324.0,530.237,64.0,530.237,333.0,530.237,1.0,530.237,323.0,530.236,324.0,530.236,323.0,530.236,334.0,530.236,1.0,530.236,62.0,530.235,324.0,530.235,62.0,530.235,335.0,530.235,1.0,530.235,61.0,530.234,324.0,530.234,61.0,530.234,336.0,530.234,1.0,530.234,60.0,530.233,324.0,530.233,60.0,530.233,337.0,530.233,1.0,530.233,324.0,530.232,324.0,530.232,338.0,530.232,1.0,530.232,333.0,530.231,325.0,530.231,55.0,530.231,64.0,530.231,334.0,530.230,325.0,530.230,326.0,530.230,323.0,530.230,335.0,530.229,325.0,530.229,57.0,530.229,62.0,530.229,336.0,530.228,325.0,530.228,54.0,530.228,61.0,530.228,337.0,530.227,325.0,530.227,56.0,530.227,60.0,530.227,338.0,530.226,325.0,530.226,324.0,530.226,1.0,530.226,52.0,530.225,57.0,530.225,326.0,530.225,325.0,530.225,51.0,530.224,56.0,530.224,57.0,530.224,50.0,530.223,57.0,530.223,54.0,530.223,56.0,530.223,327.0,530.222,57.0,530.222,325.0,530.222,55.0,530.222,48.0,530.221,57.0,530.221,55.0,530.221,54.0,530.221,328.0,530.220,57.0,530.220,326.0,530.220,1.0,530.220,40.0,530.219,56.0,530.219,57.0,530.219,52.0,530.219,39.0,530.218,56.0,530.218,54.0,530.218,51.0,530.218,38.0,530.217,56.0,530.217,55.0,530.217,50.0,530.217,37.0,530.216,56.0,530.216,326.0,530.216,327.0,530.216,331.0,530.215,56.0,530.215,325.0,530.215,48.0,530.215,332.0,530.214,56.0,530.214,328.0,530.214,1.0,530.214,64.0,530.213,55.0,530.213,54.0,530.213,46.0,530.213,323.0,530.212,55.0,530.212,325.0,530.212,45.0,530.212,62.0,530.211,55.0,530.211,326.0,530.211,329.0,530.211,61.0,530.210,55.0,530.210,56.0,530.210,43.0,530.210,60.0,530.209,55.0,530.209,57.0,530.209,42.0,530.209,324.0,530.208,55.0,530.208,330.0,530.208,1.0,530.208,46.0,530.207,54.0,530.207,56.0,530.207,40.0,530.207,45.0,530.206,54.0,530.206,55.0,530.206,39.0,530.206,329.0,530.205,54.0,530.205,325.0,530.205,38.0,530.205,43.0,530.204,54.0,530.204,57.0,530.204,37.0,530.204,42.0,530.203,54.0,530.203,326.0,530.203,331.0,530.203,330.0,530.202,54.0,530.202,332.0,530.202,1.0,530.202,325.0,530.201,326.0,530.201,325.0,530.201,333.0,530.201,1.0,530.201,57.0,530.200,326.0,530.200,57.0,530.200,334.0,530.200,1.0,530.200,56.0,530.199,326.0,530.199,56.0,530.199,335.0,530.199,1.0,530.199,55.0,530.198,326.0,530.198,55.0,530.198,336.0,530.198,1.0,530.198,54.0,530.197,326.0,530.197,54.0,530.197,337.0,530.197,1.0,530.197,326.0,530.196,326.0,530.196,338.0,530.196,1.0,530.196,325.0,530.195,52.0,530.195,327.0,530.195,64.0,530.195,57.0,530.194,52.0,530.194,328.0,530.194,323.0,530.194,56.0,530.193,52.0,530.193,51.0,530.193,62.0,530.193,55.0,530.192,52.0,530.192,48.0,530.192,61.0,530.192,54.0,530.191,52.0,530.191,50.0,530.191,60.0,530.191,326.0,530.190,52.0,530.190,324.0,530.190,1.0,530.190,40.0,530.189,51.0,530.189,328.0,530.189,325.0,530.189,39.0,530.188,51.0,530.188,50.0,530.188,57.0,530.188,38.0,530.187,51.0,530.187,48.0,530.187,56.0,530.187,37.0,530.186,51.0,530.186,52.0,530.186,55.0,530.186,331.0,530.185,51.0,530.185,327.0,530.185,54.0,530.185,332.0,530.184,51.0,530.184,326.0,530.184,1.0,530.184,46.0,530.183,50.0,530.183,51.0,530.183,52.0,530.183,45.0,530.182,50.0,530.182,48.0,530.182,51.0,530.182,329.0,530.181,327.0,530.181,50.0,530.181,43.0,530.180,50.0,530.180,328.0,530.180,327.0,530.180,42.0,530.179,50.0,530.179,52.0,530.179,48.0,530.179,330.0,530.178,50.0,530.178,328.0,530.178,1.0,530.178,333.0,530.177,327.0,530.177,48.0,530.177,46.0,530.177,334.0,530.176,327.0,530.176,52.0,530.176,45.0,530.176,335.0,530.175,327.0,530.175,328.0,530.175,329.0,530.175,336.0,530.174,327.0,530.174,50.0,530.174,43.0,530.174,337.0,530.173,327.0,530.173,51.0,530.173,42.0,530.173,338.0,530.172,327.0,530.172,330.0,530.172,1.0,530.172,64.0,530.171,48.0,530.171,50.0,530.171,40.0,530.171,323.0,530.170,48.0,530.170,327.0,530.170,39.0,530.170,62.0,530.169,48.0,530.169,52.0,530.169,38.0,530.169,61.0,530.168,48.0,530.168,51.0,530.168,37.0,530.168,60.0,530.167,48.0,530.167,328.0,530.167,331.0,530.167,324.0,530.166,48.0,530.166,332.0,530.166,1.0,530.166,52.0,530.165,328.0,530.165,52.0,530.165,333.0,530.165,1.0,530.165,51.0,530.164,328.0,530.164,51.0,530.164,334.0,530.164,1.0,530.164,50.0,530.163,328.0,530.163,50.0,530.163,335.0,530.163,1.0,530.163,327.0,530.162,328.0,530.162,327.0,530.162,336.0,530.162,1.0,530.162,48.0,530.161,328.0,530.161,48.0,530.161,337.0,530.161,1.0,530.161,328.0,530.160,328.0,530.160,338.0,530.160,1.0,530.160,40.0,530.159,46.0,530.159,43.0,530.159,64.0,530.159,39.0,530.158,46.0,530.158,330.0,530.158,323.0,530.158,38.0,530.157,46.0,530.157,45.0,530.157,62.0,530.157,37.0,530.156,46.0,530.156,42.0,530.156,61.0,530.156,331.0,530.155,46.0,530.155,329.0,530.155,60.0,530.155,332.0,530.154,46.0,530.154,324.0,530.154,1.0,530.154,64.0,530.153,45.0,530.153,330.0,530.153,325.0,530.153,323.0,530.152,45.0,530.152,329.0,530.152,57.0,530.152,62.0,530.151,45.0,530.151,42.0,530.151,56.0,530.151,61.0,530.150,45.0,530.150,46.0,530.150,55.0,530.150,60.0,530.149,45.0,530.149,43.0,530.149,54.0,530.149,324.0,530.148,45.0,530.148,326.0,530.148,1.0,530.148,333.0,530.147,329.0,530.147,45.0,530.147,52.0,530.147,334.0,530.146,329.0,530.146,42.0,530.146,51.0,530.146,335.0,530.145,329.0,530.145,43.0,530.145,50.0,530.145,336.0,530.144,329.0,530.144,330.0,530.144,327.0,530.144,337.0,530.143,329.0,530.143,46.0,530.143,48.0,530.143,338.0,530.142,329.0,530.142,328.0,530.142,1.0,530.142,52.0,530.141,43.0,530.141,42.0,530.141,46.0,530.141,51.0,530.140,43.0,530.140,46.0,530.140,45.0,530.140,50.0,530.139,43.0,530.139,330.0,530.139,329.0,530.139,327.0,530.138,329.0,530.138,43.0,530.138,48.0,530.137,43.0,530.137,45.0,530.137,42.0,530.137,328.0,530.136,43.0,530.136,330.0,530.136,1.0,530.136,325.0,530.135,42.0,530.135,329.0,530.135,40.0,530.135,57.0,530.134,42.0,530.134,43.0,530.134,39.0,530.134,56.0,530.133,42.0,530.133,46.0,530.133,38.0,530.133,55.0,530.132,42.0,530.132,45.0,530.132,37.0,530.132,54.0,530.131,42.0,530.131,330.0,530.131,331.0,530.131,326.0,530.130,42.0,530.130,332.0,530.130,1.0,530.130,46.0,530.129,330.0,530.129,46.0,530.129,333.0,530.129,1.0,530.129,45.0,530.128,330.0,530.128,45.0,530.128,334.0,530.128,1.0,530.128,329.0,530.127,330.0,530.127,329.0,530.127,335.0,530.127,1.0,530.127,43.0,530.126,330.0,530.126,43.0,530.126,336.0,530.126,1.0,530.126,42.0,530.125,330.0,530.125,42.0,530.125,337.0,530.125,1.0,530.125,330.0,530.124,330.0,530.124,338.0,530.124,1.0,530.124,52.0,530.123,40.0,530.123,37.0,530.123,64.0,530.123,51.0,530.122,40.0,530.122,332.0,530.122,323.0,530.122,50.0,530.121,40.0,530.121,39.0,530.121,62.0,530.121,327.0,530.120,40.0,530.120,331.0,530.120,61.0,530.120,48.0,530.119,40.0,530.119,38.0,530.119,60.0,530.119,328.0,530.118,40.0,530.118,324.0,530.118,1.0,530.118,46.0,530.117,39.0,530.117,332.0,530.117,325.0,530.117,45.0,530.116,39.0,530.116,38.0,530.116,57.0,530.116,329.0,530.115,39.0,530.115,331.0,530.115,56.0,530.115,43.0,530.114,39.0,530.114,40.0,530.114,55.0,530.114,42.0,530.113,39.0,530.113,37.0,530.113,54.0,530.113,330.0,530.112,39.0,530.112,326.0,530.112,1.0,530.112,64.0,530.111,38.0,530.111,39.0,530.111,52.0,530.111,323.0,530.110,38.0,530.110,331.0,530.110,51.0,530.110,62.0,530.109,38.0,530.109,37.0,530.109,50.0,530.109,61.0,530.108,38.0,530.108,332.0,530.108,327.0,530.108,60.0,530.107,38.0,530.107,40.0,530.107,48.0,530.107,324.0,530.106,38.0,530.106,328.0,530.106,1.0,530.106,325.0,530.105,37.0,530.105,331.0,530.105,46.0,530.105,57.0,530.104,37.0,530.104,40.0,530.104,45.0,530.104,56.0,530.103,37.0,530.103,332.0,530.103,329.0,530.103,55.0,530.102,37.0,530.102,38.0,530.102,43.0,530.102,54.0,530.101,37.0,530.101,39.0,530.101,42.0,530.101,326.0,530.100,37.0,530.100,330.0,530.100,1.0,530.100,333.0,530.99,331.0,530.99,38.0,530.99,40.0,530.99,334.0,530.98,331.0,530.98,37.0,530.98,39.0,530.98,335.0,530.97,331.0,530.97,40.0,530.97,38.0,530.97,336.0,530.96,331.0,530.96,39.0,530.96,37.0,530.96,337.0,530.95,332.0,530.95,331.0,530.95,338.0,530.94,331.0,530.94,332.0,530.94,1.0,530.94,40.0,530.93,332.0,530.93,40.0,530.93,333.0,530.93,1.0,530.93,39.0,530.92,332.0,530.92,39.0,530.92,334.0,530.92,1.0,530.92,38.0,530.91,332.0,530.91,38.0,530.91,335.0,530.91,1.0,530.91,37.0,530.90,332.0,530.90,37.0,530.90,336.0,530.90,1.0,530.90,331.0,530.89,332.0,530.89,331.0,530.89,337.0,530.89,1.0,530.89,332.0,530.88,332.0,530.88,338.0,530.88,1.0,530.88,64.0,530.87,333.0,530.87,336.0,530.87,1.0,530.87,64.0,530.87,323.0,530.86,333.0,530.86,338.0,530.86,1.0,530.86,323.0,530.86,62.0,530.85,333.0,530.85,334.0,530.85,1.0,530.85,62.0,530.85,61.0,530.84,333.0,530.84,337.0,530.84,1.0,530.84,61.0,530.84,60.0,530.83,333.0,530.83,335.0,530.83,1.0,530.83,60.0,530.83,324.0,530.82,333.0,530.82,324.0,530.82,1.0,530.82,325.0,530.81,334.0,530.81,338.0,530.81,1.0,530.81,325.0,530.81,57.0,530.80,334.0,530.80,335.0,530.80,1.0,530.80,57.0,530.80,56.0,530.79,334.0,530.79,337.0,530.79,1.0,530.79,56.0,530.79,55.0,530.78,334.0,530.78,333.0,530.78,1.0,530.78,55.0,530.78,54.0,530.77,334.0,530.77,336.0,530.77,1.0,530.77,54.0,530.77,326.0,530.76,334.0,530.76,326.0,530.76,1.0,530.76,52.0,530.75,335.0,530.75,334.0,530.75,1.0,530.75,52.0,530.75,51.0,530.74,335.0,530.74,337.0,530.74,1.0,530.74,51.0,530.74,50.0,530.73,335.0,530.73,336.0,530.73,1.0,530.73,50.0,530.73,327.0,530.72,335.0,530.72,338.0,530.72,1.0,530.72,327.0,530.72,48.0,530.71,335.0,530.71,333.0,530.71,1.0,530.71,48.0,530.71,328.0,530.70,335.0,530.70,328.0,530.70,1.0,530.70,46.0,530.69,336.0,530.69,337.0,530.69,1.0,530.69,46.0,530.69,45.0,530.68,336.0,530.68,333.0,530.68,1.0,530.68,45.0,530.68,329.0,530.67,336.0,530.67,338.0,530.67,1.0,530.67,329.0,530.67,43.0,530.66,336.0,530.66,335.0,530.66,1.0,530.66,43.0,530.66,42.0,530.65,336.0,530.65,334.0,530.65,1.0,530.65,42.0,530.65,330.0,530.64,336.0,530.64,330.0,530.64,1.0,530.64,40.0,530.63,337.0,530.63,335.0,530.63,1.0,530.63,40.0,530.63,39.0,530.62,337.0,530.62,336.0,530.62,1.0,530.62,39.0,530.62,38.0,530.61,337.0,530.61,333.0,530.61,1.0,530.61,38.0,530.61,37.0,530.60,337.0,530.60,334.0,530.60,1.0,530.60,37.0,530.60,331.0,530.59,337.0,530.59,338.0,530.59,1.0,530.59,331.0,530.59,332.0,530.58,337.0,530.58,332.0,530.58,1.0,530.58,333.0,530.57,338.0,530.57,333.0,530.57,333.0,530.57,1.0,530.57,334.0,530.56,338.0,530.56,334.0,530.56,334.0,530.56,1.0,530.56,335.0,530.55,338.0,530.55,335.0,530.55,335.0,530.55,1.0,530.55,336.0,530.54,338.0,530.54,336.0,530.54,336.0,530.54,1.0,530.54,337.0,530.53,338.0,530.53,337.0,530.53,337.0,530.53,1.0,530.53,338.0,530.52,338.0,530.52,1.0,530.52,325.0,530.15,323.0,530.15,62.0,530.14,52.0,530.14,56.0,530.13,51.0,530.13,61.0,530.12,46.0,530.12,55.0,530.11,45.0,530.11,329.0,530.10,327.0,530.10,60.0,530.9,40.0,530.9,54.0,530.8,39.0,530.8,48.0,530.7,38.0,530.7,42.0,530.6,37.0,530.6,324.0,530.5,333.0,530.5,1.0,530.5,326.0,530.4,334.0,530.4,1.0,530.4,328.0,530.3,335.0,530.3,1.0,530.3,330.0,530.2,336.0,530.2,1.0,530.2,337.0,530.1,332.0,530.1,1.0,530.1,22.0,530.0')] ).
cnf(532,plain,
( ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ skC36
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41 ),
inference(obv,[status(thm),theory(equality)],[531]),
[iquote('0:Obv:531.292')] ).
cnf(533,plain,
$false,
inference(mrr,[status(thm)],[532,526,519,513,508,504,501,499,493,486,483,481,476,472,467,464,460,453,451,445,441,439,432,427,421,418,415,410,408,402,398,391,389,385,379,376,369,340,364,357,351,347,342]),
[iquote('0:MRR:532.0,532.1,532.2,532.3,532.4,532.5,532.6,532.7,532.8,532.9,532.10,532.11,532.12,532.13,532.14,532.15,532.16,532.17,532.18,532.19,532.20,532.21,532.22,532.23,532.24,532.25,532.26,532.27,532.28,532.29,532.30,532.31,532.32,532.33,532.34,532.35,532.36,532.37,532.38,532.39,532.40,532.41,526.0,519.0,513.0,508.0,504.0,501.0,499.0,493.0,486.0,483.0,481.0,476.0,472.0,467.0,464.0,460.0,453.0,451.0,445.0,441.0,439.0,432.0,427.0,421.0,418.0,415.0,410.0,408.0,402.0,398.0,391.0,389.0,385.0,379.0,376.0,369.0,340.0,364.0,357.0,351.0,347.0,342.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.08 % Problem : ALG032+1 : TPTP v8.1.0. Released v2.7.0.
% 0.04/0.09 % Command : run_spass %d %s
% 0.09/0.28 % Computer : n029.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 600
% 0.09/0.28 % DateTime : Wed Jun 8 08:42:06 EDT 2022
% 0.09/0.28 % CPUTime :
% 2.37/2.57
% 2.37/2.57 SPASS V 3.9
% 2.37/2.57 SPASS beiseite: Proof found.
% 2.37/2.57 % SZS status Theorem
% 2.37/2.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.37/2.57 SPASS derived 0 clauses, backtracked 0 clauses, performed 0 splits and kept 101 clauses.
% 2.37/2.57 SPASS allocated 96758 KBytes.
% 2.37/2.57 SPASS spent 0:00:02.28 on the problem.
% 2.37/2.57 0:00:00.03 for the input.
% 2.37/2.57 0:00:01.83 for the FLOTTER CNF translation.
% 2.37/2.57 0:00:00.00 for inferences.
% 2.37/2.57 0:00:00.00 for the backtracking.
% 2.37/2.57 0:00:00.33 for the reduction.
% 2.37/2.57
% 2.37/2.57
% 2.37/2.57 Here is a proof with depth 0, length 191 :
% 2.37/2.57 % SZS output start Refutation
% See solution above
% 2.37/2.59 Formulae used in the proof : ax3 ax4 co1 ax2
% 2.37/2.59
%------------------------------------------------------------------------------