%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG033+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 14 18:02:02 EDT 2022
% Result : Theorem 0.92s 1.13s
% Output : Refutation 0.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 88
% Syntax : Number of clauses : 194 ( 105 unt; 0 nHn; 194 RR)
% Number of literals : 888 ( 0 equ; 696 neg)
% Maximal clause size : 284 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 45 ( 44 usr; 44 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('ALG033+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(e2,e1),
file('ALG033+1.p',unknown),
[] ).
cnf(17,axiom,
equal(inv(e0),e0),
file('ALG033+1.p',unknown),
[] ).
cnf(18,axiom,
equal(inv(e1),e1),
file('ALG033+1.p',unknown),
[] ).
cnf(19,axiom,
equal(inv(e2),e2),
file('ALG033+1.p',unknown),
[] ).
cnf(20,axiom,
equal(inv(e3),e4),
file('ALG033+1.p',unknown),
[] ).
cnf(21,axiom,
equal(inv(e4),e3),
file('ALG033+1.p',unknown),
[] ).
cnf(22,axiom,
equal(inv(e5),e5),
file('ALG033+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ equal(e0,unit)
| skC36 ),
file('ALG033+1.p',unknown),
[] ).
cnf(29,axiom,
equal(op(e0,e0),e0),
file('ALG033+1.p',unknown),
[] ).
cnf(30,axiom,
equal(op(e0,e1),e1),
file('ALG033+1.p',unknown),
[] ).
cnf(31,axiom,
equal(op(e0,e2),e2),
file('ALG033+1.p',unknown),
[] ).
cnf(32,axiom,
equal(op(e0,e3),e3),
file('ALG033+1.p',unknown),
[] ).
cnf(33,axiom,
equal(op(e0,e4),e4),
file('ALG033+1.p',unknown),
[] ).
cnf(34,axiom,
equal(op(e0,e5),e5),
file('ALG033+1.p',unknown),
[] ).
cnf(35,axiom,
equal(op(e1,e0),e1),
file('ALG033+1.p',unknown),
[] ).
cnf(36,axiom,
equal(op(e1,e1),e0),
file('ALG033+1.p',unknown),
[] ).
cnf(37,axiom,
equal(op(e1,e2),e3),
file('ALG033+1.p',unknown),
[] ).
cnf(38,axiom,
equal(op(e1,e3),e2),
file('ALG033+1.p',unknown),
[] ).
cnf(39,axiom,
equal(op(e1,e4),e5),
file('ALG033+1.p',unknown),
[] ).
cnf(40,axiom,
equal(op(e1,e5),e4),
file('ALG033+1.p',unknown),
[] ).
cnf(41,axiom,
equal(op(e2,e0),e2),
file('ALG033+1.p',unknown),
[] ).
cnf(42,axiom,
equal(op(e2,e1),e4),
file('ALG033+1.p',unknown),
[] ).
cnf(43,axiom,
equal(op(e2,e2),e0),
file('ALG033+1.p',unknown),
[] ).
cnf(44,axiom,
equal(op(e2,e3),e5),
file('ALG033+1.p',unknown),
[] ).
cnf(45,axiom,
equal(op(e2,e4),e1),
file('ALG033+1.p',unknown),
[] ).
cnf(46,axiom,
equal(op(e2,e5),e3),
file('ALG033+1.p',unknown),
[] ).
cnf(47,axiom,
equal(op(e3,e0),e3),
file('ALG033+1.p',unknown),
[] ).
cnf(48,axiom,
equal(op(e3,e1),e5),
file('ALG033+1.p',unknown),
[] ).
cnf(49,axiom,
equal(op(e3,e2),e1),
file('ALG033+1.p',unknown),
[] ).
cnf(50,axiom,
equal(op(e3,e3),e4),
file('ALG033+1.p',unknown),
[] ).
cnf(51,axiom,
equal(op(e3,e4),e0),
file('ALG033+1.p',unknown),
[] ).
cnf(52,axiom,
equal(op(e3,e5),e2),
file('ALG033+1.p',unknown),
[] ).
cnf(53,axiom,
equal(op(e4,e0),e4),
file('ALG033+1.p',unknown),
[] ).
cnf(54,axiom,
equal(op(e4,e1),e2),
file('ALG033+1.p',unknown),
[] ).
cnf(55,axiom,
equal(op(e4,e2),e5),
file('ALG033+1.p',unknown),
[] ).
cnf(56,axiom,
equal(op(e4,e3),e0),
file('ALG033+1.p',unknown),
[] ).
cnf(57,axiom,
equal(op(e4,e4),e3),
file('ALG033+1.p',unknown),
[] ).
cnf(58,axiom,
equal(op(e4,e5),e1),
file('ALG033+1.p',unknown),
[] ).
cnf(59,axiom,
equal(op(e5,e0),e5),
file('ALG033+1.p',unknown),
[] ).
cnf(60,axiom,
equal(op(e5,e1),e3),
file('ALG033+1.p',unknown),
[] ).
cnf(61,axiom,
equal(op(e5,e2),e4),
file('ALG033+1.p',unknown),
[] ).
cnf(62,axiom,
equal(op(e5,e3),e1),
file('ALG033+1.p',unknown),
[] ).
cnf(63,axiom,
equal(op(e5,e4),e2),
file('ALG033+1.p',unknown),
[] ).
cnf(64,axiom,
equal(op(e5,e5),e0),
file('ALG033+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ equal(inv(e0),e0)
| skC37 ),
file('ALG033+1.p',unknown),
[] ).
cnf(72,axiom,
( ~ equal(inv(e1),e1)
| skC38 ),
file('ALG033+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ equal(inv(e2),e2)
| skC39 ),
file('ALG033+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ equal(inv(e3),e4)
| skC40 ),
file('ALG033+1.p',unknown),
[] ).
cnf(92,axiom,
( ~ equal(inv(e4),e3)
| skC41 ),
file('ALG033+1.p',unknown),
[] ).
cnf(95,axiom,
( ~ equal(op(e0,e0),e0)
| skC0 ),
file('ALG033+1.p',unknown),
[] ).
cnf(102,axiom,
( ~ equal(op(e0,e1),e1)
| skC1 ),
file('ALG033+1.p',unknown),
[] ).
cnf(109,axiom,
( ~ equal(op(e0,e2),e2)
| skC2 ),
file('ALG033+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ equal(op(e0,e3),e3)
| skC3 ),
file('ALG033+1.p',unknown),
[] ).
cnf(123,axiom,
( ~ equal(op(e0,e4),e4)
| skC4 ),
file('ALG033+1.p',unknown),
[] ).
cnf(130,axiom,
( ~ equal(op(e0,e5),e5)
| skC5 ),
file('ALG033+1.p',unknown),
[] ).
cnf(132,axiom,
( ~ equal(op(e1,e0),e1)
| skC6 ),
file('ALG033+1.p',unknown),
[] ).
cnf(137,axiom,
( ~ equal(op(e1,e1),e0)
| skC7 ),
file('ALG033+1.p',unknown),
[] ).
cnf(146,axiom,
( ~ equal(op(e1,e2),e3)
| skC8 ),
file('ALG033+1.p',unknown),
[] ).
cnf(151,axiom,
( ~ equal(op(e1,e3),e2)
| skC9 ),
file('ALG033+1.p',unknown),
[] ).
cnf(160,axiom,
( ~ equal(op(e1,e4),e5)
| skC10 ),
file('ALG033+1.p',unknown),
[] ).
cnf(165,axiom,
( ~ equal(op(e1,e5),e4)
| skC11 ),
file('ALG033+1.p',unknown),
[] ).
cnf(169,axiom,
( ~ equal(op(e2,e0),e2)
| skC12 ),
file('ALG033+1.p',unknown),
[] ).
cnf(177,axiom,
( ~ equal(op(e2,e1),e4)
| skC13 ),
file('ALG033+1.p',unknown),
[] ).
cnf(179,axiom,
( ~ equal(op(e2,e2),e0)
| skC14 ),
file('ALG033+1.p',unknown),
[] ).
cnf(190,axiom,
( ~ equal(op(e2,e3),e5)
| skC15 ),
file('ALG033+1.p',unknown),
[] ).
cnf(192,axiom,
( ~ equal(op(e2,e4),e1)
| skC16 ),
file('ALG033+1.p',unknown),
[] ).
cnf(200,axiom,
( ~ equal(op(e2,e5),e3)
| skC17 ),
file('ALG033+1.p',unknown),
[] ).
cnf(206,axiom,
( ~ equal(op(e3,e0),e3)
| skC18 ),
file('ALG033+1.p',unknown),
[] ).
cnf(214,axiom,
( ~ equal(op(e3,e1),e5)
| skC19 ),
file('ALG033+1.p',unknown),
[] ).
cnf(216,axiom,
( ~ equal(op(e3,e2),e1)
| skC20 ),
file('ALG033+1.p',unknown),
[] ).
cnf(225,axiom,
( ~ equal(op(e3,e3),e4)
| skC21 ),
file('ALG033+1.p',unknown),
[] ).
cnf(227,axiom,
( ~ equal(op(e3,e4),e0)
| skC22 ),
file('ALG033+1.p',unknown),
[] ).
cnf(235,axiom,
( ~ equal(op(e3,e5),e2)
| skC23 ),
file('ALG033+1.p',unknown),
[] ).
cnf(243,axiom,
( ~ equal(op(e4,e0),e4)
| skC24 ),
file('ALG033+1.p',unknown),
[] ).
cnf(247,axiom,
( ~ equal(op(e4,e1),e2)
| skC25 ),
file('ALG033+1.p',unknown),
[] ).
cnf(256,axiom,
( ~ equal(op(e4,e2),e5)
| skC26 ),
file('ALG033+1.p',unknown),
[] ).
cnf(257,axiom,
( ~ equal(op(e4,e3),e0)
| skC27 ),
file('ALG033+1.p',unknown),
[] ).
cnf(266,axiom,
( ~ equal(op(e4,e4),e3)
| skC28 ),
file('ALG033+1.p',unknown),
[] ).
cnf(270,axiom,
( ~ equal(op(e4,e5),e1)
| skC29 ),
file('ALG033+1.p',unknown),
[] ).
cnf(280,axiom,
( ~ equal(op(e5,e0),e5)
| skC30 ),
file('ALG033+1.p',unknown),
[] ).
cnf(284,axiom,
( ~ equal(op(e5,e1),e3)
| skC31 ),
file('ALG033+1.p',unknown),
[] ).
cnf(291,axiom,
( ~ equal(op(e5,e2),e4)
| skC32 ),
file('ALG033+1.p',unknown),
[] ).
cnf(294,axiom,
( ~ equal(op(e5,e3),e1)
| skC33 ),
file('ALG033+1.p',unknown),
[] ).
cnf(301,axiom,
( ~ equal(op(e5,e4),e2)
| skC34 ),
file('ALG033+1.p',unknown),
[] ).
cnf(305,axiom,
( ~ equal(op(e5,e5),e0)
| skC35 ),
file('ALG033+1.p',unknown),
[] ).
cnf(330,axiom,
( ~ skC42
| equal(op(e4,e5),op(e5,e4)) ),
file('ALG033+1.p',unknown),
[] ).
cnf(332,axiom,
( ~ equal(inv(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
| skC42 ),
file('ALG033+1.p',unknown),
[] ).
cnf(338,plain,
equal(inv(unit),unit),
inference(rew,[status(thm),theory(equality)],[1,17]),
[iquote('0:Rew:1.0,17.0')] ).
cnf(344,plain,
equal(op(e5,e5),unit),
inference(rew,[status(thm),theory(equality)],[1,64]),
[iquote('0:Rew:1.0,64.0')] ).
cnf(345,plain,
equal(op(e5,unit),e5),
inference(rew,[status(thm),theory(equality)],[1,59]),
[iquote('0:Rew:1.0,59.0')] ).
cnf(346,plain,
equal(op(e4,e3),unit),
inference(rew,[status(thm),theory(equality)],[1,56]),
[iquote('0:Rew:1.0,56.0')] ).
cnf(347,plain,
equal(op(e4,unit),e4),
inference(rew,[status(thm),theory(equality)],[1,53]),
[iquote('0:Rew:1.0,53.0')] ).
cnf(348,plain,
equal(op(e3,e4),unit),
inference(rew,[status(thm),theory(equality)],[1,51]),
[iquote('0:Rew:1.0,51.0')] ).
cnf(349,plain,
equal(op(e3,unit),e3),
inference(rew,[status(thm),theory(equality)],[1,47]),
[iquote('0:Rew:1.0,47.0')] ).
cnf(350,plain,
equal(op(e2,e2),unit),
inference(rew,[status(thm),theory(equality)],[1,43]),
[iquote('0:Rew:1.0,43.0')] ).
cnf(351,plain,
equal(op(e2,unit),e2),
inference(rew,[status(thm),theory(equality)],[1,41]),
[iquote('0:Rew:1.0,41.0')] ).
cnf(352,plain,
equal(op(e1,e1),unit),
inference(rew,[status(thm),theory(equality)],[1,36]),
[iquote('0:Rew:1.0,36.0')] ).
cnf(353,plain,
equal(op(e1,unit),e1),
inference(rew,[status(thm),theory(equality)],[1,35]),
[iquote('0:Rew:1.0,35.0')] ).
cnf(354,plain,
equal(op(unit,e5),e5),
inference(rew,[status(thm),theory(equality)],[1,34]),
[iquote('0:Rew:1.0,34.0')] ).
cnf(355,plain,
equal(op(unit,e4),e4),
inference(rew,[status(thm),theory(equality)],[1,33]),
[iquote('0:Rew:1.0,33.0')] ).
cnf(356,plain,
equal(op(unit,e3),e3),
inference(rew,[status(thm),theory(equality)],[1,32]),
[iquote('0:Rew:1.0,32.0')] ).
cnf(357,plain,
equal(op(unit,e2),e2),
inference(rew,[status(thm),theory(equality)],[1,31]),
[iquote('0:Rew:1.0,31.0')] ).
cnf(358,plain,
equal(op(unit,e1),e1),
inference(rew,[status(thm),theory(equality)],[1,30]),
[iquote('0:Rew:1.0,30.0')] ).
cnf(359,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[1,29]),
[iquote('0:Rew:1.0,29.0')] ).
cnf(360,plain,
( ~ equal(unit,unit)
| skC36 ),
inference(rew,[status(thm),theory(equality)],[1,23]),
[iquote('0:Rew:1.0,23.0')] ).
cnf(361,plain,
skC36,
inference(obv,[status(thm),theory(equality)],[360]),
[iquote('0:Obv:360.0')] ).
cnf(364,plain,
( ~ equal(e3,e3)
| skC41 ),
inference(rew,[status(thm),theory(equality)],[21,92]),
[iquote('0:Rew:21.0,92.0')] ).
cnf(365,plain,
skC41,
inference(obv,[status(thm),theory(equality)],[364]),
[iquote('0:Obv:364.0')] ).
cnf(367,plain,
( ~ equal(e4,e4)
| skC40 ),
inference(rew,[status(thm),theory(equality)],[20,87]),
[iquote('0:Rew:20.0,87.0')] ).
cnf(368,plain,
skC40,
inference(obv,[status(thm),theory(equality)],[367]),
[iquote('0:Obv:367.0')] ).
cnf(372,plain,
( ~ equal(e2,e2)
| skC39 ),
inference(rew,[status(thm),theory(equality)],[19,79]),
[iquote('0:Rew:19.0,79.0')] ).
cnf(373,plain,
skC39,
inference(obv,[status(thm),theory(equality)],[372]),
[iquote('0:Obv:372.0')] ).
cnf(378,plain,
( ~ equal(e1,e1)
| skC38 ),
inference(rew,[status(thm),theory(equality)],[18,72]),
[iquote('0:Rew:18.0,72.0')] ).
cnf(379,plain,
skC38,
inference(obv,[status(thm),theory(equality)],[378]),
[iquote('0:Obv:378.0')] ).
cnf(385,plain,
( ~ equal(unit,unit)
| skC37 ),
inference(rew,[status(thm),theory(equality)],[338,65,1]),
[iquote('0:Rew:338.0,65.0,1.0,65.0')] ).
cnf(386,plain,
skC37,
inference(obv,[status(thm),theory(equality)],[385]),
[iquote('0:Obv:385.0')] ).
cnf(392,plain,
( ~ equal(unit,unit)
| skC35 ),
inference(rew,[status(thm),theory(equality)],[344,305,1]),
[iquote('0:Rew:344.0,305.0,1.0,305.0')] ).
cnf(393,plain,
skC35,
inference(obv,[status(thm),theory(equality)],[392]),
[iquote('0:Obv:392.0')] ).
cnf(397,plain,
( ~ equal(e2,e2)
| skC34 ),
inference(rew,[status(thm),theory(equality)],[63,301]),
[iquote('0:Rew:63.0,301.0')] ).
cnf(398,plain,
skC34,
inference(obv,[status(thm),theory(equality)],[397]),
[iquote('0:Obv:397.0')] ).
cnf(403,plain,
( ~ equal(e1,e1)
| skC33 ),
inference(rew,[status(thm),theory(equality)],[62,294]),
[iquote('0:Rew:62.0,294.0')] ).
cnf(404,plain,
skC33,
inference(obv,[status(thm),theory(equality)],[403]),
[iquote('0:Obv:403.0')] ).
cnf(406,plain,
( ~ equal(e4,e4)
| skC32 ),
inference(rew,[status(thm),theory(equality)],[61,291]),
[iquote('0:Rew:61.0,291.0')] ).
cnf(407,plain,
skC32,
inference(obv,[status(thm),theory(equality)],[406]),
[iquote('0:Obv:406.0')] ).
cnf(410,plain,
( ~ equal(e3,e3)
| skC31 ),
inference(rew,[status(thm),theory(equality)],[60,284]),
[iquote('0:Rew:60.0,284.0')] ).
cnf(411,plain,
skC31,
inference(obv,[status(thm),theory(equality)],[410]),
[iquote('0:Obv:410.0')] ).
cnf(412,plain,
( ~ equal(e5,e5)
| skC30 ),
inference(rew,[status(thm),theory(equality)],[345,280,1]),
[iquote('0:Rew:345.0,280.0,1.0,280.0')] ).
cnf(413,plain,
skC30,
inference(obv,[status(thm),theory(equality)],[412]),
[iquote('0:Obv:412.0')] ).
cnf(418,plain,
( ~ equal(e1,e1)
| skC29 ),
inference(rew,[status(thm),theory(equality)],[58,270]),
[iquote('0:Rew:58.0,270.0')] ).
cnf(419,plain,
skC29,
inference(obv,[status(thm),theory(equality)],[418]),
[iquote('0:Obv:418.0')] ).
cnf(422,plain,
( ~ equal(e3,e3)
| skC28 ),
inference(rew,[status(thm),theory(equality)],[57,266]),
[iquote('0:Rew:57.0,266.0')] ).
cnf(423,plain,
skC28,
inference(obv,[status(thm),theory(equality)],[422]),
[iquote('0:Obv:422.0')] ).
cnf(429,plain,
( ~ equal(unit,unit)
| skC27 ),
inference(rew,[status(thm),theory(equality)],[346,257,1]),
[iquote('0:Rew:346.0,257.0,1.0,257.0')] ).
cnf(430,plain,
skC27,
inference(obv,[status(thm),theory(equality)],[429]),
[iquote('0:Obv:429.0')] ).
cnf(431,plain,
( ~ equal(e5,e5)
| skC26 ),
inference(rew,[status(thm),theory(equality)],[55,256]),
[iquote('0:Rew:55.0,256.0')] ).
cnf(432,plain,
skC26,
inference(obv,[status(thm),theory(equality)],[431]),
[iquote('0:Obv:431.0')] ).
cnf(436,plain,
( ~ equal(e2,e2)
| skC25 ),
inference(rew,[status(thm),theory(equality)],[54,247]),
[iquote('0:Rew:54.0,247.0')] ).
cnf(437,plain,
skC25,
inference(obv,[status(thm),theory(equality)],[436]),
[iquote('0:Obv:436.0')] ).
cnf(439,plain,
( ~ equal(e4,e4)
| skC24 ),
inference(rew,[status(thm),theory(equality)],[347,243,1]),
[iquote('0:Rew:347.0,243.0,1.0,243.0')] ).
cnf(440,plain,
skC24,
inference(obv,[status(thm),theory(equality)],[439]),
[iquote('0:Obv:439.0')] ).
cnf(444,plain,
( ~ equal(e2,e2)
| skC23 ),
inference(rew,[status(thm),theory(equality)],[52,235]),
[iquote('0:Rew:52.0,235.0')] ).
cnf(445,plain,
skC23,
inference(obv,[status(thm),theory(equality)],[444]),
[iquote('0:Obv:444.0')] ).
cnf(451,plain,
( ~ equal(unit,unit)
| skC22 ),
inference(rew,[status(thm),theory(equality)],[348,227,1]),
[iquote('0:Rew:348.0,227.0,1.0,227.0')] ).
cnf(452,plain,
skC22,
inference(obv,[status(thm),theory(equality)],[451]),
[iquote('0:Obv:451.0')] ).
cnf(454,plain,
( ~ equal(e4,e4)
| skC21 ),
inference(rew,[status(thm),theory(equality)],[50,225]),
[iquote('0:Rew:50.0,225.0')] ).
cnf(455,plain,
skC21,
inference(obv,[status(thm),theory(equality)],[454]),
[iquote('0:Obv:454.0')] ).
cnf(460,plain,
( ~ equal(e1,e1)
| skC20 ),
inference(rew,[status(thm),theory(equality)],[49,216]),
[iquote('0:Rew:49.0,216.0')] ).
cnf(461,plain,
skC20,
inference(obv,[status(thm),theory(equality)],[460]),
[iquote('0:Obv:460.0')] ).
cnf(462,plain,
( ~ equal(e5,e5)
| skC19 ),
inference(rew,[status(thm),theory(equality)],[48,214]),
[iquote('0:Rew:48.0,214.0')] ).
cnf(463,plain,
skC19,
inference(obv,[status(thm),theory(equality)],[462]),
[iquote('0:Obv:462.0')] ).
cnf(466,plain,
( ~ equal(e3,e3)
| skC18 ),
inference(rew,[status(thm),theory(equality)],[349,206,1]),
[iquote('0:Rew:349.0,206.0,1.0,206.0')] ).
cnf(467,plain,
skC18,
inference(obv,[status(thm),theory(equality)],[466]),
[iquote('0:Obv:466.0')] ).
cnf(470,plain,
( ~ equal(e3,e3)
| skC17 ),
inference(rew,[status(thm),theory(equality)],[46,200]),
[iquote('0:Rew:46.0,200.0')] ).
cnf(471,plain,
skC17,
inference(obv,[status(thm),theory(equality)],[470]),
[iquote('0:Obv:470.0')] ).
cnf(476,plain,
( ~ equal(e1,e1)
| skC16 ),
inference(rew,[status(thm),theory(equality)],[45,192]),
[iquote('0:Rew:45.0,192.0')] ).
cnf(477,plain,
skC16,
inference(obv,[status(thm),theory(equality)],[476]),
[iquote('0:Obv:476.0')] ).
cnf(478,plain,
( ~ equal(e5,e5)
| skC15 ),
inference(rew,[status(thm),theory(equality)],[44,190]),
[iquote('0:Rew:44.0,190.0')] ).
cnf(479,plain,
skC15,
inference(obv,[status(thm),theory(equality)],[478]),
[iquote('0:Obv:478.0')] ).
cnf(485,plain,
( ~ equal(unit,unit)
| skC14 ),
inference(rew,[status(thm),theory(equality)],[350,179,1]),
[iquote('0:Rew:350.0,179.0,1.0,179.0')] ).
cnf(486,plain,
skC14,
inference(obv,[status(thm),theory(equality)],[485]),
[iquote('0:Obv:485.0')] ).
cnf(488,plain,
( ~ equal(e4,e4)
| skC13 ),
inference(rew,[status(thm),theory(equality)],[42,177]),
[iquote('0:Rew:42.0,177.0')] ).
cnf(489,plain,
skC13,
inference(obv,[status(thm),theory(equality)],[488]),
[iquote('0:Obv:488.0')] ).
cnf(493,plain,
( ~ equal(e2,e2)
| skC12 ),
inference(rew,[status(thm),theory(equality)],[351,169,1]),
[iquote('0:Rew:351.0,169.0,1.0,169.0')] ).
cnf(494,plain,
skC12,
inference(obv,[status(thm),theory(equality)],[493]),
[iquote('0:Obv:493.0')] ).
cnf(496,plain,
( ~ equal(e4,e4)
| skC11 ),
inference(rew,[status(thm),theory(equality)],[40,165]),
[iquote('0:Rew:40.0,165.0')] ).
cnf(497,plain,
skC11,
inference(obv,[status(thm),theory(equality)],[496]),
[iquote('0:Obv:496.0')] ).
cnf(498,plain,
( ~ equal(e5,e5)
| skC10 ),
inference(rew,[status(thm),theory(equality)],[39,160]),
[iquote('0:Rew:39.0,160.0')] ).
cnf(499,plain,
skC10,
inference(obv,[status(thm),theory(equality)],[498]),
[iquote('0:Obv:498.0')] ).
cnf(503,plain,
( ~ equal(e2,e2)
| skC9 ),
inference(rew,[status(thm),theory(equality)],[38,151]),
[iquote('0:Rew:38.0,151.0')] ).
cnf(504,plain,
skC9,
inference(obv,[status(thm),theory(equality)],[503]),
[iquote('0:Obv:503.0')] ).
cnf(507,plain,
( ~ equal(e3,e3)
| skC8 ),
inference(rew,[status(thm),theory(equality)],[37,146]),
[iquote('0:Rew:37.0,146.0')] ).
cnf(508,plain,
skC8,
inference(obv,[status(thm),theory(equality)],[507]),
[iquote('0:Obv:507.0')] ).
cnf(514,plain,
( ~ equal(unit,unit)
| skC7 ),
inference(rew,[status(thm),theory(equality)],[352,137,1]),
[iquote('0:Rew:352.0,137.0,1.0,137.0')] ).
cnf(515,plain,
skC7,
inference(obv,[status(thm),theory(equality)],[514]),
[iquote('0:Obv:514.0')] ).
cnf(520,plain,
( ~ equal(e1,e1)
| skC6 ),
inference(rew,[status(thm),theory(equality)],[353,132,1]),
[iquote('0:Rew:353.0,132.0,1.0,132.0')] ).
cnf(521,plain,
skC6,
inference(obv,[status(thm),theory(equality)],[520]),
[iquote('0:Obv:520.0')] ).
cnf(522,plain,
( ~ equal(e5,e5)
| skC5 ),
inference(rew,[status(thm),theory(equality)],[354,130,1]),
[iquote('0:Rew:354.0,130.0,1.0,130.0')] ).
cnf(523,plain,
skC5,
inference(obv,[status(thm),theory(equality)],[522]),
[iquote('0:Obv:522.0')] ).
cnf(525,plain,
( ~ equal(e4,e4)
| skC4 ),
inference(rew,[status(thm),theory(equality)],[355,123,1]),
[iquote('0:Rew:355.0,123.0,1.0,123.0')] ).
cnf(526,plain,
skC4,
inference(obv,[status(thm),theory(equality)],[525]),
[iquote('0:Obv:525.0')] ).
cnf(529,plain,
( ~ equal(e3,e3)
| skC3 ),
inference(rew,[status(thm),theory(equality)],[356,116,1]),
[iquote('0:Rew:356.0,116.0,1.0,116.0')] ).
cnf(530,plain,
skC3,
inference(obv,[status(thm),theory(equality)],[529]),
[iquote('0:Obv:529.0')] ).
cnf(534,plain,
( ~ equal(e2,e2)
| skC2 ),
inference(rew,[status(thm),theory(equality)],[357,109,1]),
[iquote('0:Rew:357.0,109.0,1.0,109.0')] ).
cnf(535,plain,
skC2,
inference(obv,[status(thm),theory(equality)],[534]),
[iquote('0:Obv:534.0')] ).
cnf(540,plain,
( ~ equal(e1,e1)
| skC1 ),
inference(rew,[status(thm),theory(equality)],[358,102,1]),
[iquote('0:Rew:358.0,102.0,1.0,102.0')] ).
cnf(541,plain,
skC1,
inference(obv,[status(thm),theory(equality)],[540]),
[iquote('0:Obv:540.0')] ).
cnf(547,plain,
( ~ equal(unit,unit)
| skC0 ),
inference(rew,[status(thm),theory(equality)],[359,95,1]),
[iquote('0:Rew:359.0,95.0,1.0,95.0')] ).
cnf(548,plain,
skC0,
inference(obv,[status(thm),theory(equality)],[547]),
[iquote('0:Obv:547.0')] ).
cnf(549,plain,
( ~ skC42
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[58,330,63]),
[iquote('0:Rew:58.0,330.1,63.0,330.1')] ).
cnf(550,plain,
~ skC42,
inference(mrr,[status(thm)],[549,7]),
[iquote('0:MRR:549.1,7.0')] ).
cnf(551,plain,
( ~ equal(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(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(unit,unit)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ 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(e4,e4)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e4,e4)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ 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(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(unit,unit)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(unit,unit)
| ~ equal(e3,e3)
| ~ equal(e2,e2)
| ~ equal(e5,e5)
| ~ equal(e4,e4)
| ~ equal(e2,e2)
| ~ equal(e4,e4)
| ~ equal(unit,unit)
| ~ equal(e5,e5)
| ~ equal(e1,e1)
| ~ equal(e3,e3)
| ~ equal(unit,unit)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e5,e5)
| ~ 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
| skC42 ),
inference(rew,[status(thm),theory(equality)],[344,332,22,348,21,346,20,350,19,352,18,359,338,1,345,354,347,355,349,356,351,357,353,358,61,63,60,62,46,58,45,57,44,55,42,54,40,52,39,38,50,37,49,48]),
[iquote('0:Rew:344.0,332.277,22.0,332.277,344.0,332.276,22.0,332.276,348.0,332.275,21.0,332.275,346.0,332.274,21.0,332.274,346.0,332.273,20.0,332.273,348.0,332.272,20.0,332.272,350.0,332.271,19.0,332.271,350.0,332.270,19.0,332.270,352.0,332.269,18.0,332.269,352.0,332.268,18.0,332.268,359.0,332.267,338.0,332.267,1.0,332.267,359.0,332.266,338.0,332.266,1.0,332.266,345.0,332.264,354.0,332.263,347.0,332.262,355.0,332.261,349.0,332.260,356.0,332.259,351.0,332.258,357.0,332.257,353.0,332.256,358.0,332.255,359.0,332.254,1.0,332.254,359.0,332.253,1.0,332.253,354.0,332.252,345.0,332.252,344.0,332.252,355.0,332.251,344.0,332.251,61.0,332.251,63.0,332.251,356.0,332.250,344.0,332.250,60.0,332.250,62.0,332.250,357.0,332.249,344.0,332.249,63.0,332.249,61.0,332.249,358.0,332.248,344.0,332.248,62.0,332.248,60.0,332.248,359.0,332.247,344.0,332.247,345.0,332.247,1.0,332.247,46.0,332.246,63.0,332.246,60.0,332.246,58.0,332.246,45.0,332.245,63.0,332.245,62.0,332.245,57.0,332.245,44.0,332.244,63.0,332.244,345.0,332.244,346.0,332.244,350.0,332.243,63.0,332.243,344.0,332.243,55.0,332.243,42.0,332.242,63.0,332.242,61.0,332.242,54.0,332.242,351.0,332.241,63.0,332.241,347.0,332.241,1.0,332.241,40.0,332.240,62.0,332.240,61.0,332.240,52.0,332.240,39.0,332.239,62.0,332.239,345.0,332.239,348.0,332.239,38.0,332.238,62.0,332.238,63.0,332.238,50.0,332.238,37.0,332.237,62.0,332.237,60.0,332.237,49.0,332.237,352.0,332.236,62.0,332.236,344.0,332.236,48.0,332.236,353.0,332.235,62.0,332.235,349.0,332.235,1.0,332.235,58.0,332.234,61.0,332.234,62.0,332.234,46.0,332.234,57.0,332.233,61.0,332.233,60.0,332.233,45.0,332.233,346.0,332.232,61.0,332.232,344.0,332.232,44.0,332.232,55.0,332.231,61.0,332.231,345.0,332.231,350.0,332.231,54.0,332.230,61.0,332.230,63.0,332.230,42.0,332.230,347.0,332.229,61.0,332.229,351.0,332.229,1.0,332.229,52.0,332.228,60.0,332.228,63.0,332.228,40.0,332.228,348.0,332.227,60.0,332.227,344.0,332.227,39.0,332.227,50.0,332.226,60.0,332.226,61.0,332.226,38.0,332.226,49.0,332.225,60.0,332.225,62.0,332.225,37.0,332.225,48.0,332.224,60.0,332.224,345.0,332.224,352.0,332.224,349.0,332.223,60.0,332.223,353.0,332.223,1.0,332.223,344.0,332.222,345.0,332.222,344.0,332.222,354.0,332.222,1.0,332.222,63.0,332.221,345.0,332.221,63.0,332.221,355.0,332.221,1.0,332.221,62.0,332.220,345.0,332.220,62.0,332.220,356.0,332.220,1.0,332.220,61.0,332.219,345.0,332.219,61.0,332.219,357.0,332.219,1.0,332.219,60.0,332.218,345.0,332.218,60.0,332.218,358.0,332.218,1.0,332.218,345.0,332.217,345.0,332.217,359.0,332.217,1.0,332.217,40.0,332.216,58.0,332.216,347.0,332.216,344.0,332.216,39.0,332.215,58.0,332.215,55.0,332.215,63.0,332.215,38.0,332.214,58.0,332.214,54.0,332.214,62.0,332.214,37.0,332.213,58.0,332.213,57.0,332.213,61.0,332.213,352.0,332.212,58.0,332.212,346.0,332.212,60.0,332.212,353.0,332.211,58.0,332.211,345.0,332.211,1.0,332.211,52.0,332.210,57.0,332.210,54.0,332.210,58.0,332.210,348.0,332.209,346.0,332.209,57.0,332.209,50.0,332.208,57.0,332.208,347.0,332.208,346.0,332.208,49.0,332.207,57.0,332.207,58.0,332.207,55.0,332.207,48.0,332.206,57.0,332.206,55.0,332.206,54.0,332.206,349.0,332.205,57.0,332.205,347.0,332.205,1.0,332.205,354.0,332.204,346.0,332.204,55.0,332.204,52.0,332.204,355.0,332.203,346.0,332.203,347.0,332.203,348.0,332.203,356.0,332.202,346.0,332.202,57.0,332.202,50.0,332.202,357.0,332.201,346.0,332.201,54.0,332.201,49.0,332.201,358.0,332.200,346.0,332.200,58.0,332.200,48.0,332.200,359.0,332.199,346.0,332.199,349.0,332.199,1.0,332.199,344.0,332.198,55.0,332.198,346.0,332.198,46.0,332.198,63.0,332.197,55.0,332.197,54.0,332.197,45.0,332.197,62.0,332.196,55.0,332.196,58.0,332.196,44.0,332.196,61.0,332.195,55.0,332.195,347.0,332.195,350.0,332.195,60.0,332.194,55.0,332.194,57.0,332.194,42.0,332.194,345.0,332.193,55.0,332.193,351.0,332.193,1.0,332.193,46.0,332.192,54.0,332.192,57.0,332.192,40.0,332.192,45.0,332.191,54.0,332.191,58.0,332.191,39.0,332.191,44.0,332.190,54.0,332.190,55.0,332.190,38.0,332.190,350.0,332.189,54.0,332.189,346.0,332.189,37.0,332.189,42.0,332.188,54.0,332.188,347.0,332.188,352.0,332.188,351.0,332.187,54.0,332.187,353.0,332.187,1.0,332.187,58.0,332.186,347.0,332.186,58.0,332.186,354.0,332.186,1.0,332.186,57.0,332.185,347.0,332.185,57.0,332.185,355.0,332.185,1.0,332.185,346.0,332.184,347.0,332.184,346.0,332.184,356.0,332.184,1.0,332.184,55.0,332.183,347.0,332.183,55.0,332.183,357.0,332.183,1.0,332.183,54.0,332.182,347.0,332.182,54.0,332.182,358.0,332.182,1.0,332.182,347.0,332.181,347.0,332.181,359.0,332.181,1.0,332.181,46.0,332.180,52.0,332.180,349.0,332.180,344.0,332.180,45.0,332.179,52.0,332.179,49.0,332.179,63.0,332.179,44.0,332.178,52.0,332.178,48.0,332.178,62.0,332.178,350.0,332.177,52.0,332.177,348.0,332.177,61.0,332.177,42.0,332.176,52.0,332.176,50.0,332.176,60.0,332.176,351.0,332.175,52.0,332.175,345.0,332.175,1.0,332.175,354.0,332.174,348.0,332.174,48.0,332.174,58.0,332.174,355.0,332.173,348.0,332.173,50.0,332.173,57.0,332.173,356.0,332.172,348.0,332.172,349.0,332.172,346.0,332.172,357.0,332.171,348.0,332.171,52.0,332.171,55.0,332.171,358.0,332.170,348.0,332.170,49.0,332.170,54.0,332.170,359.0,332.169,348.0,332.169,347.0,332.169,1.0,332.169,58.0,332.168,50.0,332.168,49.0,332.168,52.0,332.168,57.0,332.167,50.0,332.167,349.0,332.167,348.0,332.167,346.0,332.166,348.0,332.166,50.0,332.166,55.0,332.165,50.0,332.165,48.0,332.165,49.0,332.165,54.0,332.164,50.0,332.164,52.0,332.164,48.0,332.164,347.0,332.163,50.0,332.163,349.0,332.163,1.0,332.163,40.0,332.162,49.0,332.162,50.0,332.162,46.0,332.162,39.0,332.161,49.0,332.161,48.0,332.161,45.0,332.161,38.0,332.160,49.0,332.160,52.0,332.160,44.0,332.160,37.0,332.159,49.0,332.159,349.0,332.159,350.0,332.159,352.0,332.158,49.0,332.158,348.0,332.158,42.0,332.158,353.0,332.157,49.0,332.157,351.0,332.157,1.0,332.157,344.0,332.156,48.0,332.156,348.0,332.156,40.0,332.156,63.0,332.155,48.0,332.155,52.0,332.155,39.0,332.155,62.0,332.154,48.0,332.154,49.0,332.154,38.0,332.154,61.0,332.153,48.0,332.153,50.0,332.153,37.0,332.153,60.0,332.152,48.0,332.152,349.0,332.152,352.0,332.152,345.0,332.151,48.0,332.151,353.0,332.151,1.0,332.151,52.0,332.150,349.0,332.150,52.0,332.150,354.0,332.150,1.0,332.150,348.0,332.149,349.0,332.149,348.0,332.149,355.0,332.149,1.0,332.149,50.0,332.148,349.0,332.148,50.0,332.148,356.0,332.148,1.0,332.148,49.0,332.147,349.0,332.147,49.0,332.147,357.0,332.147,1.0,332.147,48.0,332.146,349.0,332.146,48.0,332.146,358.0,332.146,1.0,332.146,349.0,332.145,349.0,332.145,359.0,332.145,1.0,332.145,52.0,332.144,46.0,332.144,351.0,332.144,344.0,332.144,348.0,332.143,46.0,332.143,350.0,332.143,63.0,332.143,50.0,332.142,46.0,332.142,42.0,332.142,62.0,332.142,49.0,332.141,46.0,332.141,45.0,332.141,61.0,332.141,48.0,332.140,46.0,332.140,44.0,332.140,60.0,332.140,349.0,332.139,46.0,332.139,345.0,332.139,1.0,332.139,40.0,332.138,45.0,332.138,42.0,332.138,58.0,332.138,39.0,332.137,45.0,332.137,44.0,332.137,57.0,332.137,38.0,332.136,45.0,332.136,351.0,332.136,346.0,332.136,37.0,332.135,45.0,332.135,46.0,332.135,55.0,332.135,352.0,332.134,45.0,332.134,350.0,332.134,54.0,332.134,353.0,332.133,45.0,332.133,347.0,332.133,1.0,332.133,344.0,332.132,44.0,332.132,350.0,332.132,52.0,332.132,63.0,332.131,44.0,332.131,351.0,332.131,348.0,332.131,62.0,332.130,44.0,332.130,45.0,332.130,50.0,332.130,61.0,332.129,44.0,332.129,42.0,332.129,49.0,332.129,60.0,332.128,44.0,332.128,46.0,332.128,48.0,332.128,345.0,332.127,44.0,332.127,349.0,332.127,1.0,332.127,354.0,332.126,350.0,332.126,44.0,332.126,46.0,332.126,355.0,332.125,350.0,332.125,42.0,332.125,45.0,332.125,356.0,332.124,350.0,332.124,46.0,332.124,44.0,332.124,357.0,332.123,351.0,332.123,350.0,332.123,358.0,332.122,350.0,332.122,45.0,332.122,42.0,332.122,359.0,332.121,350.0,332.121,351.0,332.121,1.0,332.121,58.0,332.120,42.0,332.120,45.0,332.120,40.0,332.120,57.0,332.119,42.0,332.119,46.0,332.119,39.0,332.119,346.0,332.118,42.0,332.118,350.0,332.118,38.0,332.118,55.0,332.117,42.0,332.117,44.0,332.117,37.0,332.117,54.0,332.116,42.0,332.116,351.0,332.116,352.0,332.116,347.0,332.115,42.0,332.115,353.0,332.115,1.0,332.115,46.0,332.114,351.0,332.114,46.0,332.114,354.0,332.114,1.0,332.114,45.0,332.113,351.0,332.113,45.0,332.113,355.0,332.113,1.0,332.113,44.0,332.112,351.0,332.112,44.0,332.112,356.0,332.112,1.0,332.112,350.0,332.111,351.0,332.111,350.0,332.111,357.0,332.111,1.0,332.111,42.0,332.110,351.0,332.110,42.0,332.110,358.0,332.110,1.0,332.110,351.0,332.109,351.0,332.109,359.0,332.109,1.0,332.109,58.0,332.108,40.0,332.108,353.0,332.108,344.0,332.108,57.0,332.107,40.0,332.107,37.0,332.107,63.0,332.107,346.0,332.106,40.0,332.106,352.0,332.106,62.0,332.106,55.0,332.105,40.0,332.105,39.0,332.105,61.0,332.105,54.0,332.104,40.0,332.104,38.0,332.104,60.0,332.104,347.0,332.103,40.0,332.103,345.0,332.103,1.0,332.103,344.0,332.102,39.0,332.102,352.0,332.102,58.0,332.102,63.0,332.101,39.0,332.101,38.0,332.101,57.0,332.101,62.0,332.100,39.0,332.100,353.0,332.100,346.0,332.100,61.0,332.99,39.0,332.99,40.0,332.99,55.0,332.99,60.0,332.98,39.0,332.98,37.0,332.98,54.0,332.98,345.0,332.97,39.0,332.97,347.0,332.97,1.0,332.97,46.0,332.96,38.0,332.96,37.0,332.96,52.0,332.96,45.0,332.95,38.0,332.95,353.0,332.95,348.0,332.95,44.0,332.94,38.0,332.94,39.0,332.94,50.0,332.94,350.0,332.93,38.0,332.93,352.0,332.93,49.0,332.93,42.0,332.92,38.0,332.92,40.0,332.92,48.0,332.92,351.0,332.91,38.0,332.91,349.0,332.91,1.0,332.91,52.0,332.90,37.0,332.90,38.0,332.90,46.0,332.90,348.0,332.89,37.0,332.89,352.0,332.89,45.0,332.89,50.0,332.88,37.0,332.88,40.0,332.88,44.0,332.88,49.0,332.87,37.0,332.87,353.0,332.87,350.0,332.87,48.0,332.86,37.0,332.86,39.0,332.86,42.0,332.86,349.0,332.85,37.0,332.85,351.0,332.85,1.0,332.85,354.0,332.84,352.0,332.84,39.0,332.84,40.0,332.84,355.0,332.83,352.0,332.83,40.0,332.83,39.0,332.83,356.0,332.82,352.0,332.82,37.0,332.82,38.0,332.82,357.0,332.81,352.0,332.81,38.0,332.81,37.0,332.81,358.0,332.80,353.0,332.80,352.0,332.80,359.0,332.79,352.0,332.79,353.0,332.79,1.0,332.79,40.0,332.78,353.0,332.78,40.0,332.78,354.0,332.78,1.0,332.78,39.0,332.77,353.0,332.77,39.0,332.77,355.0,332.77,1.0,332.77,38.0,332.76,353.0,332.76,38.0,332.76,356.0,332.76,1.0,332.76,37.0,332.75,353.0,332.75,37.0,332.75,357.0,332.75,1.0,332.75,352.0,332.74,353.0,332.74,352.0,332.74,358.0,332.74,1.0,332.74,353.0,332.73,353.0,332.73,359.0,332.73,1.0,332.73,344.0,332.72,354.0,332.72,359.0,332.72,1.0,332.72,344.0,332.72,63.0,332.71,354.0,332.71,357.0,332.71,1.0,332.71,63.0,332.71,62.0,332.70,354.0,332.70,358.0,332.70,1.0,332.70,62.0,332.70,61.0,332.69,354.0,332.69,355.0,332.69,1.0,332.69,61.0,332.69,60.0,332.68,354.0,332.68,356.0,332.68,1.0,332.68,60.0,332.68,345.0,332.67,354.0,332.67,345.0,332.67,1.0,332.67,58.0,332.66,355.0,332.66,358.0,332.66,1.0,332.66,58.0,332.66,57.0,332.65,355.0,332.65,356.0,332.65,1.0,332.65,57.0,332.65,346.0,332.64,355.0,332.64,359.0,332.64,1.0,332.64,346.0,332.64,55.0,332.63,355.0,332.63,354.0,332.63,1.0,332.63,55.0,332.63,54.0,332.62,355.0,332.62,357.0,332.62,1.0,332.62,54.0,332.62,347.0,332.61,355.0,332.61,347.0,332.61,1.0,332.61,52.0,332.60,356.0,332.60,357.0,332.60,1.0,332.60,52.0,332.60,348.0,332.59,356.0,332.59,359.0,332.59,1.0,332.59,348.0,332.59,50.0,332.58,356.0,332.58,355.0,332.58,1.0,332.58,50.0,332.58,49.0,332.57,356.0,332.57,358.0,332.57,1.0,332.57,49.0,332.57,48.0,332.56,356.0,332.56,354.0,332.56,1.0,332.56,48.0,332.56,349.0,332.55,356.0,332.55,349.0,332.55,1.0,332.55,46.0,332.54,357.0,332.54,356.0,332.54,1.0,332.54,46.0,332.54,45.0,332.53,357.0,332.53,358.0,332.53,1.0,332.53,45.0,332.53,44.0,332.52,357.0,332.52,354.0,332.52,1.0,332.52,44.0,332.52,350.0,332.51,357.0,332.51,359.0,332.51,1.0,332.51,350.0,332.51,42.0,332.50,357.0,332.50,355.0,332.50,1.0,332.50,42.0,332.50,351.0,332.49,357.0,332.49,351.0,332.49,1.0,332.49,40.0,332.48,358.0,332.48,355.0,332.48,1.0,332.48,40.0,332.48,39.0,332.47,358.0,332.47,354.0,332.47,1.0,332.47,39.0,332.47,38.0,332.46,358.0,332.46,357.0,332.46,1.0,332.46,38.0,332.46,37.0,332.45,358.0,332.45,356.0,332.45,1.0,332.45,37.0,332.45,352.0,332.44,358.0,332.44,359.0,332.44,1.0,332.44,352.0,332.44,353.0,332.43,358.0,332.43,353.0,332.43,1.0,332.43,354.0,332.42,359.0,332.42,354.0,332.42,354.0,332.42,1.0,332.42,355.0,332.41,359.0,332.41,355.0,332.41,355.0,332.41,1.0,332.41,356.0,332.40,359.0,332.40,356.0,332.40,356.0,332.40,1.0,332.40,357.0,332.39,359.0,332.39,357.0,332.39,357.0,332.39,1.0,332.39,358.0,332.38,359.0,332.38,358.0,332.38,358.0,332.38,1.0,332.38,359.0,332.37,359.0,332.37,1.0,332.37,22.0,332.0')] ).
cnf(552,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
| skC42 ),
inference(obv,[status(thm),theory(equality)],[551]),
[iquote('0:Obv:551.277')] ).
cnf(553,plain,
$false,
inference(mrr,[status(thm)],[552,548,541,535,530,526,523,521,515,508,504,499,497,494,489,486,479,477,471,467,463,461,455,452,445,440,437,432,430,423,419,413,411,407,404,398,393,361,386,379,373,368,365,550]),
[iquote('0:MRR:552.0,552.1,552.2,552.3,552.4,552.5,552.6,552.7,552.8,552.9,552.10,552.11,552.12,552.13,552.14,552.15,552.16,552.17,552.18,552.19,552.20,552.21,552.22,552.23,552.24,552.25,552.26,552.27,552.28,552.29,552.30,552.31,552.32,552.33,552.34,552.35,552.36,552.37,552.38,552.39,552.40,552.41,552.42,548.0,541.0,535.0,530.0,526.0,523.0,521.0,515.0,508.0,504.0,499.0,497.0,494.0,489.0,486.0,479.0,477.0,471.0,467.0,463.0,461.0,455.0,452.0,445.0,440.0,437.0,432.0,430.0,423.0,419.0,413.0,411.0,407.0,404.0,398.0,393.0,361.0,386.0,379.0,373.0,368.0,365.0,550.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : ALG033+1 : TPTP v8.1.0. Released v2.7.0.
% 0.10/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Thu Jun 9 07:33:27 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.92/1.13
% 0.92/1.13 SPASS V 3.9
% 0.92/1.13 SPASS beiseite: Proof found.
% 0.92/1.13 % SZS status Theorem
% 0.92/1.13 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.92/1.13 SPASS derived 0 clauses, backtracked 0 clauses, performed 0 splits and kept 102 clauses.
% 0.92/1.13 SPASS allocated 96110 KBytes.
% 0.92/1.13 SPASS spent 0:00:00.78 on the problem.
% 0.92/1.13 0:00:00.04 for the input.
% 0.92/1.13 0:00:00.60 for the FLOTTER CNF translation.
% 0.92/1.13 0:00:00.00 for inferences.
% 0.92/1.13 0:00:00.00 for the backtracking.
% 0.92/1.13 0:00:00.09 for the reduction.
% 0.92/1.13
% 0.92/1.13
% 0.92/1.13 Here is a proof with depth 0, length 194 :
% 0.92/1.13 % SZS output start Refutation
% See solution above
% 0.92/1.14 Formulae used in the proof : ax3 ax1 ax4 co1 ax2
% 0.92/1.14
%------------------------------------------------------------------------------