%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG015+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n021.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:01:57 EDT 2022
% Result : Theorem 0.73s 0.89s
% Output : Refutation 0.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 141
% Syntax : Number of clauses : 403 ( 320 unt; 51 nHn; 403 RR)
% Number of literals : 624 ( 0 equ; 221 neg)
% Maximal clause size : 20 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 10 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
~ equal(e11,e10),
file('ALG015+1.p',unknown),
[] ).
cnf(4,axiom,
~ equal(e12,e10),
file('ALG015+1.p',unknown),
[] ).
cnf(5,axiom,
~ equal(e13,e10),
file('ALG015+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e12,e11),
file('ALG015+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(e13,e11),
file('ALG015+1.p',unknown),
[] ).
cnf(8,axiom,
~ equal(e13,e12),
file('ALG015+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(e21,e20),
file('ALG015+1.p',unknown),
[] ).
cnf(10,axiom,
~ equal(e22,e20),
file('ALG015+1.p',unknown),
[] ).
cnf(11,axiom,
~ equal(e23,e20),
file('ALG015+1.p',unknown),
[] ).
cnf(14,axiom,
~ equal(e22,e23),
file('ALG015+1.p',unknown),
[] ).
cnf(53,axiom,
equal(h12(e12),e23),
file('ALG015+1.p',unknown),
[] ).
cnf(54,axiom,
equal(h12(e13),e22),
file('ALG015+1.p',unknown),
[] ).
cnf(57,axiom,
equal(op1(unit1,e11),e11),
file('ALG015+1.p',unknown),
[] ).
cnf(58,axiom,
equal(op1(e11,unit1),e11),
file('ALG015+1.p',unknown),
[] ).
cnf(59,axiom,
equal(op1(unit1,e12),e12),
file('ALG015+1.p',unknown),
[] ).
cnf(60,axiom,
equal(op1(e12,unit1),e12),
file('ALG015+1.p',unknown),
[] ).
cnf(61,axiom,
equal(op1(unit1,e13),e13),
file('ALG015+1.p',unknown),
[] ).
cnf(62,axiom,
equal(op1(e13,unit1),e13),
file('ALG015+1.p',unknown),
[] ).
cnf(65,axiom,
equal(op2(unit2,e21),e21),
file('ALG015+1.p',unknown),
[] ).
cnf(66,axiom,
equal(op2(e21,unit2),e21),
file('ALG015+1.p',unknown),
[] ).
cnf(67,axiom,
equal(op2(unit2,e22),e22),
file('ALG015+1.p',unknown),
[] ).
cnf(68,axiom,
equal(op2(e22,unit2),e22),
file('ALG015+1.p',unknown),
[] ).
cnf(70,axiom,
equal(op2(e23,unit2),e23),
file('ALG015+1.p',unknown),
[] ).
cnf(79,axiom,
equal(op1(e13,e13),e10),
file('ALG015+1.p',unknown),
[] ).
cnf(80,axiom,
equal(op1(e12,e13),e11),
file('ALG015+1.p',unknown),
[] ).
cnf(81,axiom,
equal(op2(e23,e23),e20),
file('ALG015+1.p',unknown),
[] ).
cnf(82,axiom,
equal(op2(e22,e23),e21),
file('ALG015+1.p',unknown),
[] ).
cnf(215,axiom,
( ~ equal(h12(e10),e20)
| skC39 ),
file('ALG015+1.p',unknown),
[] ).
cnf(220,axiom,
( ~ equal(h12(e11),e21)
| skC40 ),
file('ALG015+1.p',unknown),
[] ).
cnf(226,axiom,
( ~ equal(h12(e13),e22)
| skC41 ),
file('ALG015+1.p',unknown),
[] ).
cnf(255,axiom,
equal(op2(e21,e21),h1(e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(256,axiom,
equal(op2(e20,e21),h1(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(257,axiom,
equal(op2(e22,e22),h2(e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(258,axiom,
equal(op2(e20,e22),h2(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(260,axiom,
equal(op2(e20,e23),h3(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(261,axiom,
equal(op2(e20,e20),h4(e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(262,axiom,
equal(op2(e21,e20),h4(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(263,axiom,
equal(op2(e22,e22),h5(e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(264,axiom,
equal(op2(e21,e22),h5(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(266,axiom,
equal(op2(e21,e23),h6(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(268,axiom,
equal(op2(e22,e20),h7(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(270,axiom,
equal(op2(e22,e21),h8(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(274,axiom,
equal(op2(e23,e20),h10(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(276,axiom,
equal(op2(e23,e21),h11(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(277,axiom,
equal(op2(e22,e22),h12(e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(278,axiom,
equal(op2(e23,e22),h12(e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(279,axiom,
( ~ skC0
| equal(op1(e10,e10),e10) ),
file('ALG015+1.p',unknown),
[] ).
cnf(280,axiom,
( ~ skC0
| equal(op1(e11,e11),e10) ),
file('ALG015+1.p',unknown),
[] ).
cnf(281,axiom,
( ~ skC0
| equal(op1(e12,e12),e10) ),
file('ALG015+1.p',unknown),
[] ).
cnf(286,axiom,
( ~ skC1
| equal(op1(e13,e13),e11) ),
file('ALG015+1.p',unknown),
[] ).
cnf(290,axiom,
( ~ skC2
| equal(op1(e13,e13),e12) ),
file('ALG015+1.p',unknown),
[] ).
cnf(291,axiom,
( ~ skC3
| equal(op2(e20,e20),e20) ),
file('ALG015+1.p',unknown),
[] ).
cnf(292,axiom,
( ~ skC3
| equal(op2(e21,e21),e20) ),
file('ALG015+1.p',unknown),
[] ).
cnf(293,axiom,
( ~ skC3
| equal(op2(e22,e22),e20) ),
file('ALG015+1.p',unknown),
[] ).
cnf(298,axiom,
( ~ skC4
| equal(op2(e23,e23),e21) ),
file('ALG015+1.p',unknown),
[] ).
cnf(302,axiom,
( ~ skC5
| equal(op2(e23,e23),e22) ),
file('ALG015+1.p',unknown),
[] ).
cnf(311,axiom,
~ equal(op1(e13,e11),op1(e10,e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(315,axiom,
~ equal(op1(e11,e12),op1(e10,e12)),
file('ALG015+1.p',unknown),
[] ).
cnf(317,axiom,
~ equal(op1(e13,e12),op1(e10,e12)),
file('ALG015+1.p',unknown),
[] ).
cnf(319,axiom,
~ equal(op1(e13,e12),op1(e11,e12)),
file('ALG015+1.p',unknown),
[] ).
cnf(322,axiom,
~ equal(op1(e12,e13),op1(e10,e13)),
file('ALG015+1.p',unknown),
[] ).
cnf(324,axiom,
~ equal(op1(e12,e13),op1(e11,e13)),
file('ALG015+1.p',unknown),
[] ).
cnf(327,axiom,
~ equal(op1(e10,e11),op1(e10,e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(328,axiom,
~ equal(op1(e10,e12),op1(e10,e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(329,axiom,
~ equal(op1(e10,e13),op1(e10,e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(330,axiom,
~ equal(op1(e10,e12),op1(e10,e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(331,axiom,
~ equal(op1(e10,e13),op1(e10,e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(334,axiom,
~ equal(op1(e11,e12),op1(e11,e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(336,axiom,
~ equal(op1(e11,e12),op1(e11,e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(345,axiom,
~ equal(op1(e13,e11),op1(e13,e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(346,axiom,
~ equal(op1(e13,e12),op1(e13,e10)),
file('ALG015+1.p',unknown),
[] ).
cnf(348,axiom,
~ equal(op1(e13,e12),op1(e13,e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(349,axiom,
~ equal(op1(e13,e13),op1(e13,e11)),
file('ALG015+1.p',unknown),
[] ).
cnf(350,axiom,
~ equal(op1(e13,e13),op1(e13,e12)),
file('ALG015+1.p',unknown),
[] ).
cnf(359,axiom,
~ equal(op2(e23,e21),op2(e20,e21)),
file('ALG015+1.p',unknown),
[] ).
cnf(363,axiom,
~ equal(op2(e21,e22),op2(e20,e22)),
file('ALG015+1.p',unknown),
[] ).
cnf(365,axiom,
~ equal(op2(e23,e22),op2(e20,e22)),
file('ALG015+1.p',unknown),
[] ).
cnf(367,axiom,
~ equal(op2(e23,e22),op2(e21,e22)),
file('ALG015+1.p',unknown),
[] ).
cnf(370,axiom,
~ equal(op2(e22,e23),op2(e20,e23)),
file('ALG015+1.p',unknown),
[] ).
cnf(372,axiom,
~ equal(op2(e22,e23),op2(e21,e23)),
file('ALG015+1.p',unknown),
[] ).
cnf(375,axiom,
~ equal(op2(e20,e21),op2(e20,e20)),
file('ALG015+1.p',unknown),
[] ).
cnf(376,axiom,
~ equal(op2(e20,e22),op2(e20,e20)),
file('ALG015+1.p',unknown),
[] ).
cnf(377,axiom,
~ equal(op2(e20,e23),op2(e20,e20)),
file('ALG015+1.p',unknown),
[] ).
cnf(378,axiom,
~ equal(op2(e20,e22),op2(e20,e21)),
file('ALG015+1.p',unknown),
[] ).
cnf(380,axiom,
~ equal(op2(e20,e22),op2(e20,e23)),
file('ALG015+1.p',unknown),
[] ).
cnf(384,axiom,
~ equal(op2(e21,e22),op2(e21,e21)),
file('ALG015+1.p',unknown),
[] ).
cnf(394,axiom,
~ equal(op2(e23,e22),op2(e23,e20)),
file('ALG015+1.p',unknown),
[] ).
cnf(396,axiom,
~ equal(op2(e23,e22),op2(e23,e21)),
file('ALG015+1.p',unknown),
[] ).
cnf(398,axiom,
~ equal(op2(e23,e22),op2(e23,e23)),
file('ALG015+1.p',unknown),
[] ).
cnf(402,axiom,
( equal(op1(e13,e13),e13)
| skC0
| skC1
| skC2 ),
file('ALG015+1.p',unknown),
[] ).
cnf(406,axiom,
( equal(op2(e23,e23),e23)
| skC3
| skC4
| skC5 ),
file('ALG015+1.p',unknown),
[] ).
cnf(449,axiom,
equal(op1(op1(e11,e10),e12),op1(e11,op1(e10,e12))),
file('ALG015+1.p',unknown),
[] ).
cnf(454,axiom,
equal(op1(op1(e11,e11),e13),op1(e11,op1(e11,e13))),
file('ALG015+1.p',unknown),
[] ).
cnf(456,axiom,
equal(op1(op1(e11,e12),e11),op1(e11,op1(e12,e11))),
file('ALG015+1.p',unknown),
[] ).
cnf(457,axiom,
equal(op1(op1(e11,e12),e12),op1(e11,op1(e12,e12))),
file('ALG015+1.p',unknown),
[] ).
cnf(459,axiom,
equal(op1(op1(e11,e13),e10),op1(e11,op1(e13,e10))),
file('ALG015+1.p',unknown),
[] ).
cnf(463,axiom,
equal(op1(op1(e12,e10),e10),op1(e12,op1(e10,e10))),
file('ALG015+1.p',unknown),
[] ).
cnf(472,axiom,
equal(op1(op1(e12,e12),e11),op1(e12,op1(e12,e11))),
file('ALG015+1.p',unknown),
[] ).
cnf(473,axiom,
equal(op1(op1(e12,e12),e12),op1(e12,op1(e12,e12))),
file('ALG015+1.p',unknown),
[] ).
cnf(474,axiom,
equal(op1(op1(e12,e12),e13),op1(e12,op1(e12,e13))),
file('ALG015+1.p',unknown),
[] ).
cnf(475,axiom,
equal(op1(op1(e12,e13),e10),op1(e12,op1(e13,e10))),
file('ALG015+1.p',unknown),
[] ).
cnf(478,axiom,
equal(op1(op1(e12,e13),e13),op1(e12,op1(e13,e13))),
file('ALG015+1.p',unknown),
[] ).
cnf(479,axiom,
equal(op1(op1(e13,e10),e10),op1(e13,op1(e10,e10))),
file('ALG015+1.p',unknown),
[] ).
cnf(492,axiom,
equal(op1(op1(e13,e13),e11),op1(e13,op1(e13,e11))),
file('ALG015+1.p',unknown),
[] ).
cnf(493,axiom,
equal(op1(op1(e13,e13),e12),op1(e13,op1(e13,e12))),
file('ALG015+1.p',unknown),
[] ).
cnf(494,axiom,
equal(op1(op1(e13,e13),e13),op1(e13,op1(e13,e13))),
file('ALG015+1.p',unknown),
[] ).
cnf(501,axiom,
equal(op2(op2(e20,e21),e22),op2(e20,op2(e21,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(509,axiom,
equal(op2(op2(e20,e23),e22),op2(e20,op2(e23,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(513,axiom,
equal(op2(op2(e21,e20),e22),op2(e21,op2(e20,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(518,axiom,
equal(op2(op2(e21,e21),e23),op2(e21,op2(e21,e23))),
file('ALG015+1.p',unknown),
[] ).
cnf(521,axiom,
equal(op2(op2(e21,e22),e22),op2(e21,op2(e22,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(532,axiom,
equal(op2(op2(e22,e21),e21),op2(e22,op2(e21,e21))),
file('ALG015+1.p',unknown),
[] ).
cnf(533,axiom,
equal(op2(op2(e22,e21),e22),op2(e22,op2(e21,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(536,axiom,
equal(op2(op2(e22,e22),e21),op2(e22,op2(e22,e21))),
file('ALG015+1.p',unknown),
[] ).
cnf(537,axiom,
equal(op2(op2(e22,e22),e22),op2(e22,op2(e22,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(538,axiom,
equal(op2(op2(e22,e22),e23),op2(e22,op2(e22,e23))),
file('ALG015+1.p',unknown),
[] ).
cnf(539,axiom,
equal(op2(op2(e22,e23),e20),op2(e22,op2(e23,e20))),
file('ALG015+1.p',unknown),
[] ).
cnf(541,axiom,
equal(op2(op2(e22,e23),e22),op2(e22,op2(e23,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(542,axiom,
equal(op2(op2(e22,e23),e23),op2(e22,op2(e23,e23))),
file('ALG015+1.p',unknown),
[] ).
cnf(543,axiom,
equal(op2(op2(e23,e20),e20),op2(e23,op2(e20,e20))),
file('ALG015+1.p',unknown),
[] ).
cnf(544,axiom,
equal(op2(op2(e23,e20),e21),op2(e23,op2(e20,e21))),
file('ALG015+1.p',unknown),
[] ).
cnf(545,axiom,
equal(op2(op2(e23,e20),e22),op2(e23,op2(e20,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(551,axiom,
equal(op2(op2(e23,e22),e20),op2(e23,op2(e22,e20))),
file('ALG015+1.p',unknown),
[] ).
cnf(553,axiom,
equal(op2(op2(e23,e22),e22),op2(e23,op2(e22,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(554,axiom,
equal(op2(op2(e23,e22),e23),op2(e23,op2(e22,e23))),
file('ALG015+1.p',unknown),
[] ).
cnf(557,axiom,
equal(op2(op2(e23,e23),e22),op2(e23,op2(e23,e22))),
file('ALG015+1.p',unknown),
[] ).
cnf(558,axiom,
equal(op2(op2(e23,e23),e23),op2(e23,op2(e23,e23))),
file('ALG015+1.p',unknown),
[] ).
cnf(559,axiom,
( equal(e13,unit1)
| equal(e12,unit1)
| equal(e11,unit1)
| equal(e10,unit1) ),
file('ALG015+1.p',unknown),
[] ).
cnf(560,axiom,
( equal(e23,unit2)
| equal(e22,unit2)
| equal(e21,unit2)
| equal(e20,unit2) ),
file('ALG015+1.p',unknown),
[] ).
cnf(570,axiom,
( equal(op2(e23,e22),e20)
| equal(op2(e23,e22),e21)
| equal(op2(e23,e22),e22)
| equal(op2(e23,e22),e23) ),
file('ALG015+1.p',unknown),
[] ).
cnf(572,axiom,
( equal(op2(e23,e20),e20)
| equal(op2(e23,e20),e21)
| equal(op2(e23,e20),e22)
| equal(op2(e23,e20),e23) ),
file('ALG015+1.p',unknown),
[] ).
cnf(576,axiom,
( equal(op2(e22,e20),e20)
| equal(op2(e22,e20),e21)
| equal(op2(e22,e20),e22)
| equal(op2(e22,e20),e23) ),
file('ALG015+1.p',unknown),
[] ).
cnf(578,axiom,
( equal(op2(e21,e22),e20)
| equal(op2(e21,e22),e21)
| equal(op2(e21,e22),e22)
| equal(op2(e21,e22),e23) ),
file('ALG015+1.p',unknown),
[] ).
cnf(580,axiom,
( equal(op2(e21,e20),e20)
| equal(op2(e21,e20),e21)
| equal(op2(e21,e20),e22)
| equal(op2(e21,e20),e23) ),
file('ALG015+1.p',unknown),
[] ).
cnf(586,axiom,
( equal(op1(e13,e12),e10)
| equal(op1(e13,e12),e11)
| equal(op1(e13,e12),e12)
| equal(op1(e13,e12),e13) ),
file('ALG015+1.p',unknown),
[] ).
cnf(587,axiom,
( equal(op1(e13,e11),e10)
| equal(op1(e13,e11),e11)
| equal(op1(e13,e11),e12)
| equal(op1(e13,e11),e13) ),
file('ALG015+1.p',unknown),
[] ).
cnf(588,axiom,
( equal(op1(e13,e10),e10)
| equal(op1(e13,e10),e11)
| equal(op1(e13,e10),e12)
| equal(op1(e13,e10),e13) ),
file('ALG015+1.p',unknown),
[] ).
cnf(592,axiom,
( equal(op1(e12,e10),e10)
| equal(op1(e12,e10),e11)
| equal(op1(e12,e10),e12)
| equal(op1(e12,e10),e13) ),
file('ALG015+1.p',unknown),
[] ).
cnf(594,axiom,
( equal(op1(e11,e12),e10)
| equal(op1(e11,e12),e11)
| equal(op1(e11,e12),e12)
| equal(op1(e11,e12),e13) ),
file('ALG015+1.p',unknown),
[] ).
cnf(596,axiom,
( equal(op1(e11,e10),e10)
| equal(op1(e11,e10),e11)
| equal(op1(e11,e10),e12)
| equal(op1(e11,e10),e13) ),
file('ALG015+1.p',unknown),
[] ).
cnf(602,axiom,
( ~ equal(h12(e12),e23)
| ~ equal(op2(h12(e10),h12(e10)),h12(op1(e10,e10)))
| ~ equal(op2(h12(e10),h12(e11)),h12(op1(e10,e11)))
| ~ equal(op2(h12(e10),h12(e12)),h12(op1(e10,e12)))
| ~ equal(op2(h12(e10),h12(e13)),h12(op1(e10,e13)))
| ~ equal(op2(h12(e11),h12(e10)),h12(op1(e11,e10)))
| ~ equal(op2(h12(e11),h12(e11)),h12(op1(e11,e11)))
| ~ equal(op2(h12(e11),h12(e12)),h12(op1(e11,e12)))
| ~ equal(op2(h12(e11),h12(e13)),h12(op1(e11,e13)))
| ~ equal(op2(h12(e12),h12(e10)),h12(op1(e12,e10)))
| ~ equal(op2(h12(e12),h12(e11)),h12(op1(e12,e11)))
| ~ equal(op2(h12(e12),h12(e12)),h12(op1(e12,e12)))
| ~ equal(op2(h12(e12),h12(e13)),h12(op1(e12,e13)))
| ~ equal(op2(h12(e13),h12(e10)),h12(op1(e13,e10)))
| ~ equal(op2(h12(e13),h12(e11)),h12(op1(e13,e11)))
| ~ equal(op2(h12(e13),h12(e12)),h12(op1(e13,e12)))
| ~ equal(op2(h12(e13),h12(e13)),h12(op1(e13,e13)))
| ~ skC39
| ~ skC40
| ~ skC41 ),
file('ALG015+1.p',unknown),
[] ).
cnf(656,plain,
equal(h12(e10),h5(e10)),
inference(rew,[status(thm),theory(equality)],[277,263]),
[iquote('0:Rew:277.0,263.0')] ).
cnf(657,plain,
equal(op2(e22,e22),h5(e10)),
inference(rew,[status(thm),theory(equality)],[656,277]),
[iquote('0:Rew:656.0,277.0')] ).
cnf(659,plain,
( ~ equal(e22,e22)
| skC41 ),
inference(rew,[status(thm),theory(equality)],[54,226]),
[iquote('0:Rew:54.0,226.0')] ).
cnf(660,plain,
skC41,
inference(obv,[status(thm),theory(equality)],[659]),
[iquote('0:Obv:659.0')] ).
cnf(666,plain,
( ~ equal(h5(e10),e20)
| skC39 ),
inference(rew,[status(thm),theory(equality)],[656,215]),
[iquote('0:Rew:656.0,215.0')] ).
cnf(766,plain,
equal(h5(e10),h2(e10)),
inference(rew,[status(thm),theory(equality)],[257,657]),
[iquote('0:Rew:257.0,657.0')] ).
cnf(767,plain,
equal(h12(e10),h2(e10)),
inference(rew,[status(thm),theory(equality)],[766,656]),
[iquote('0:Rew:766.0,656.0')] ).
cnf(770,plain,
( ~ equal(h2(e10),e20)
| skC39 ),
inference(rew,[status(thm),theory(equality)],[766,666]),
[iquote('0:Rew:766.0,666.0')] ).
cnf(771,plain,
( ~ skC5
| equal(e22,e20) ),
inference(rew,[status(thm),theory(equality)],[81,302]),
[iquote('0:Rew:81.0,302.1')] ).
cnf(772,plain,
~ skC5,
inference(mrr,[status(thm)],[771,10]),
[iquote('0:MRR:771.1,10.0')] ).
cnf(773,plain,
( ~ skC4
| equal(e21,e20) ),
inference(rew,[status(thm),theory(equality)],[81,298]),
[iquote('0:Rew:81.0,298.1')] ).
cnf(774,plain,
~ skC4,
inference(mrr,[status(thm)],[773,9]),
[iquote('0:MRR:773.1,9.0')] ).
cnf(775,plain,
( ~ skC3
| equal(h2(e10),e20) ),
inference(rew,[status(thm),theory(equality)],[257,293]),
[iquote('0:Rew:257.0,293.1')] ).
cnf(776,plain,
( ~ skC3
| equal(h1(e10),e20) ),
inference(rew,[status(thm),theory(equality)],[255,292]),
[iquote('0:Rew:255.0,292.1')] ).
cnf(777,plain,
( ~ skC3
| equal(h4(e10),e20) ),
inference(rew,[status(thm),theory(equality)],[261,291]),
[iquote('0:Rew:261.0,291.1')] ).
cnf(778,plain,
( ~ skC2
| equal(e12,e10) ),
inference(rew,[status(thm),theory(equality)],[79,290]),
[iquote('0:Rew:79.0,290.1')] ).
cnf(779,plain,
~ skC2,
inference(mrr,[status(thm)],[778,4]),
[iquote('0:MRR:778.1,4.0')] ).
cnf(780,plain,
( ~ skC1
| equal(e11,e10) ),
inference(rew,[status(thm),theory(equality)],[79,286]),
[iquote('0:Rew:79.0,286.1')] ).
cnf(781,plain,
~ skC1,
inference(mrr,[status(thm)],[780,3]),
[iquote('0:MRR:780.1,3.0')] ).
cnf(782,plain,
( equal(e23,e20)
| skC3
| skC4
| skC5 ),
inference(rew,[status(thm),theory(equality)],[81,406]),
[iquote('0:Rew:81.0,406.0')] ).
cnf(783,plain,
skC3,
inference(mrr,[status(thm)],[782,11,774,772]),
[iquote('0:MRR:782.0,782.2,782.3,11.0,774.0,772.0')] ).
cnf(784,plain,
equal(h2(e10),e20),
inference(mrr,[status(thm)],[775,783]),
[iquote('0:MRR:775.0,783.0')] ).
cnf(785,plain,
equal(h1(e10),e20),
inference(mrr,[status(thm)],[776,783]),
[iquote('0:MRR:776.0,783.0')] ).
cnf(786,plain,
equal(h4(e10),e20),
inference(mrr,[status(thm)],[777,783]),
[iquote('0:MRR:777.0,783.0')] ).
cnf(787,plain,
equal(op2(e22,e22),e20),
inference(rew,[status(thm),theory(equality)],[784,257]),
[iquote('0:Rew:784.0,257.0')] ).
cnf(791,plain,
equal(h12(e10),e20),
inference(rew,[status(thm),theory(equality)],[784,767]),
[iquote('0:Rew:784.0,767.0')] ).
cnf(792,plain,
( ~ equal(e20,e20)
| skC39 ),
inference(rew,[status(thm),theory(equality)],[784,770]),
[iquote('0:Rew:784.0,770.0')] ).
cnf(794,plain,
equal(op2(e21,e21),e20),
inference(rew,[status(thm),theory(equality)],[785,255]),
[iquote('0:Rew:785.0,255.0')] ).
cnf(801,plain,
equal(op2(e20,e20),e20),
inference(rew,[status(thm),theory(equality)],[786,261]),
[iquote('0:Rew:786.0,261.0')] ).
cnf(808,plain,
skC39,
inference(obv,[status(thm),theory(equality)],[792]),
[iquote('0:Obv:792.0')] ).
cnf(812,plain,
( equal(e13,e10)
| skC0
| skC1
| skC2 ),
inference(rew,[status(thm),theory(equality)],[79,402]),
[iquote('0:Rew:79.0,402.0')] ).
cnf(813,plain,
skC0,
inference(mrr,[status(thm)],[812,5,781,779]),
[iquote('0:MRR:812.0,812.2,812.3,5.0,781.0,779.0')] ).
cnf(814,plain,
equal(op1(e12,e12),e10),
inference(mrr,[status(thm)],[281,813]),
[iquote('0:MRR:281.0,813.0')] ).
cnf(815,plain,
equal(op1(e11,e11),e10),
inference(mrr,[status(thm)],[280,813]),
[iquote('0:MRR:280.0,813.0')] ).
cnf(816,plain,
equal(op1(e10,e10),e10),
inference(mrr,[status(thm)],[279,813]),
[iquote('0:MRR:279.0,813.0')] ).
cnf(817,plain,
~ equal(h12(e11),e20),
inference(rew,[status(thm),theory(equality)],[278,398,81]),
[iquote('0:Rew:278.0,398.0,81.0,398.0')] ).
cnf(819,plain,
~ equal(h12(e11),h11(e11)),
inference(rew,[status(thm),theory(equality)],[278,396,276]),
[iquote('0:Rew:278.0,396.0,276.0,396.0')] ).
cnf(821,plain,
~ equal(h12(e11),h10(e11)),
inference(rew,[status(thm),theory(equality)],[278,394,274]),
[iquote('0:Rew:278.0,394.0,274.0,394.0')] ).
cnf(831,plain,
~ equal(h5(e11),e20),
inference(rew,[status(thm),theory(equality)],[264,384,794]),
[iquote('0:Rew:264.0,384.0,794.0,384.0')] ).
cnf(835,plain,
~ equal(h3(e11),h2(e11)),
inference(rew,[status(thm),theory(equality)],[258,380,260]),
[iquote('0:Rew:258.0,380.0,260.0,380.0')] ).
cnf(837,plain,
~ equal(h2(e11),h1(e11)),
inference(rew,[status(thm),theory(equality)],[258,378,256]),
[iquote('0:Rew:258.0,378.0,256.0,378.0')] ).
cnf(838,plain,
~ equal(h3(e11),e20),
inference(rew,[status(thm),theory(equality)],[260,377,801]),
[iquote('0:Rew:260.0,377.0,801.0,377.0')] ).
cnf(839,plain,
~ equal(h2(e11),e20),
inference(rew,[status(thm),theory(equality)],[258,376,801]),
[iquote('0:Rew:258.0,376.0,801.0,376.0')] ).
cnf(840,plain,
~ equal(h1(e11),e20),
inference(rew,[status(thm),theory(equality)],[256,375,801]),
[iquote('0:Rew:256.0,375.0,801.0,375.0')] ).
cnf(843,plain,
~ equal(h6(e11),e21),
inference(rew,[status(thm),theory(equality)],[82,372,266]),
[iquote('0:Rew:82.0,372.0,266.0,372.0')] ).
cnf(845,plain,
~ equal(h3(e11),e21),
inference(rew,[status(thm),theory(equality)],[82,370,260]),
[iquote('0:Rew:82.0,370.0,260.0,370.0')] ).
cnf(848,plain,
~ equal(h12(e11),h5(e11)),
inference(rew,[status(thm),theory(equality)],[278,367,264]),
[iquote('0:Rew:278.0,367.0,264.0,367.0')] ).
cnf(850,plain,
~ equal(h12(e11),h2(e11)),
inference(rew,[status(thm),theory(equality)],[278,365,258]),
[iquote('0:Rew:278.0,365.0,258.0,365.0')] ).
cnf(852,plain,
~ equal(h5(e11),h2(e11)),
inference(rew,[status(thm),theory(equality)],[264,363,258]),
[iquote('0:Rew:264.0,363.0,258.0,363.0')] ).
cnf(856,plain,
~ equal(h11(e11),h1(e11)),
inference(rew,[status(thm),theory(equality)],[276,359,256]),
[iquote('0:Rew:276.0,359.0,256.0,359.0')] ).
cnf(865,plain,
~ equal(op1(e13,e12),e10),
inference(rew,[status(thm),theory(equality)],[79,350]),
[iquote('0:Rew:79.0,350.0')] ).
cnf(866,plain,
~ equal(op1(e13,e11),e10),
inference(rew,[status(thm),theory(equality)],[79,349]),
[iquote('0:Rew:79.0,349.0')] ).
cnf(874,plain,
~ equal(op1(e11,e12),e10),
inference(rew,[status(thm),theory(equality)],[815,336]),
[iquote('0:Rew:815.0,336.0')] ).
cnf(876,plain,
~ equal(op1(e10,e13),e10),
inference(rew,[status(thm),theory(equality)],[816,329]),
[iquote('0:Rew:816.0,329.0')] ).
cnf(877,plain,
~ equal(op1(e10,e12),e10),
inference(rew,[status(thm),theory(equality)],[816,328]),
[iquote('0:Rew:816.0,328.0')] ).
cnf(878,plain,
~ equal(op1(e10,e11),e10),
inference(rew,[status(thm),theory(equality)],[816,327]),
[iquote('0:Rew:816.0,327.0')] ).
cnf(881,plain,
~ equal(op1(e11,e13),e11),
inference(rew,[status(thm),theory(equality)],[80,324]),
[iquote('0:Rew:80.0,324.0')] ).
cnf(883,plain,
~ equal(op1(e10,e13),e11),
inference(rew,[status(thm),theory(equality)],[80,322]),
[iquote('0:Rew:80.0,322.0')] ).
cnf(893,plain,
equal(h10(e11),h3(e11)),
inference(rew,[status(thm),theory(equality)],[260,558,274,81]),
[iquote('0:Rew:260.0,558.0,274.0,558.0,81.0,558.0')] ).
cnf(894,plain,
equal(op2(e23,e20),h3(e11)),
inference(rew,[status(thm),theory(equality)],[893,274]),
[iquote('0:Rew:893.0,274.0')] ).
cnf(898,plain,
~ equal(h12(e11),h3(e11)),
inference(rew,[status(thm),theory(equality)],[893,821]),
[iquote('0:Rew:893.0,821.0')] ).
cnf(902,plain,
equal(op2(e23,h12(e11)),h2(e11)),
inference(rew,[status(thm),theory(equality)],[258,557,81,278]),
[iquote('0:Rew:258.0,557.0,81.0,557.0,278.0,557.0')] ).
cnf(905,plain,
equal(op2(h12(e11),e23),h11(e11)),
inference(rew,[status(thm),theory(equality)],[278,554,276,82]),
[iquote('0:Rew:278.0,554.0,276.0,554.0,82.0,554.0')] ).
cnf(906,plain,
equal(op2(h12(e11),e22),h3(e11)),
inference(rew,[status(thm),theory(equality)],[278,553,894,787]),
[iquote('0:Rew:278.0,553.0,894.0,553.0,787.0,553.0')] ).
cnf(908,plain,
equal(op2(h12(e11),e20),op2(e23,h7(e11))),
inference(rew,[status(thm),theory(equality)],[278,551,268]),
[iquote('0:Rew:278.0,551.0,268.0,551.0')] ).
cnf(914,plain,
equal(op2(h3(e11),e22),op2(e23,h2(e11))),
inference(rew,[status(thm),theory(equality)],[894,545,258]),
[iquote('0:Rew:894.0,545.0,258.0,545.0')] ).
cnf(915,plain,
equal(op2(h3(e11),e21),op2(e23,h1(e11))),
inference(rew,[status(thm),theory(equality)],[894,544,256]),
[iquote('0:Rew:894.0,544.0,256.0,544.0')] ).
cnf(916,plain,
equal(op2(h3(e11),e20),h3(e11)),
inference(rew,[status(thm),theory(equality)],[894,543,801]),
[iquote('0:Rew:894.0,543.0,801.0,543.0')] ).
cnf(917,plain,
equal(h7(e11),h6(e11)),
inference(rew,[status(thm),theory(equality)],[266,542,82,268,81]),
[iquote('0:Rew:266.0,542.0,82.0,542.0,268.0,542.0,81.0,542.0')] ).
cnf(918,plain,
equal(op2(e22,e20),h6(e11)),
inference(rew,[status(thm),theory(equality)],[917,268]),
[iquote('0:Rew:917.0,268.0')] ).
cnf(924,plain,
equal(op2(h12(e11),e20),op2(e23,h6(e11))),
inference(rew,[status(thm),theory(equality)],[917,908]),
[iquote('0:Rew:917.0,908.0')] ).
cnf(925,plain,
equal(op2(e22,h12(e11)),h5(e11)),
inference(rew,[status(thm),theory(equality)],[264,541,82,278]),
[iquote('0:Rew:264.0,541.0,82.0,541.0,278.0,541.0')] ).
cnf(927,plain,
equal(op2(e22,h3(e11)),h4(e11)),
inference(rew,[status(thm),theory(equality)],[262,539,82,894]),
[iquote('0:Rew:262.0,539.0,82.0,539.0,894.0,539.0')] ).
cnf(928,plain,
equal(h8(e11),h3(e11)),
inference(rew,[status(thm),theory(equality)],[260,538,787,270,82]),
[iquote('0:Rew:260.0,538.0,787.0,538.0,270.0,538.0,82.0,538.0')] ).
cnf(929,plain,
equal(op2(e22,e21),h3(e11)),
inference(rew,[status(thm),theory(equality)],[928,270]),
[iquote('0:Rew:928.0,270.0')] ).
cnf(937,plain,
equal(h6(e11),h2(e11)),
inference(rew,[status(thm),theory(equality)],[258,537,918,787]),
[iquote('0:Rew:258.0,537.0,918.0,537.0,787.0,537.0')] ).
cnf(938,plain,
equal(op2(e21,e23),h2(e11)),
inference(rew,[status(thm),theory(equality)],[937,266]),
[iquote('0:Rew:937.0,266.0')] ).
cnf(943,plain,
~ equal(h2(e11),e21),
inference(rew,[status(thm),theory(equality)],[937,843]),
[iquote('0:Rew:937.0,843.0')] ).
cnf(946,plain,
equal(op2(h12(e11),e20),op2(e23,h2(e11))),
inference(rew,[status(thm),theory(equality)],[937,924]),
[iquote('0:Rew:937.0,924.0')] ).
cnf(948,plain,
equal(op2(e22,e20),h2(e11)),
inference(rew,[status(thm),theory(equality)],[937,918]),
[iquote('0:Rew:937.0,918.0')] ).
cnf(949,plain,
equal(h4(e11),h1(e11)),
inference(rew,[status(thm),theory(equality)],[256,536,787,927,929]),
[iquote('0:Rew:256.0,536.0,787.0,536.0,927.0,536.0,929.0,536.0')] ).
cnf(950,plain,
equal(op2(e21,e20),h1(e11)),
inference(rew,[status(thm),theory(equality)],[949,262]),
[iquote('0:Rew:949.0,262.0')] ).
cnf(960,plain,
equal(op2(e22,h5(e11)),op2(e23,h2(e11))),
inference(rew,[status(thm),theory(equality)],[914,533,929,264]),
[iquote('0:Rew:914.0,533.0,929.0,533.0,264.0,533.0')] ).
cnf(961,plain,
equal(op2(e23,h1(e11)),h2(e11)),
inference(rew,[status(thm),theory(equality)],[915,532,929,948,794]),
[iquote('0:Rew:915.0,532.0,929.0,532.0,948.0,532.0,794.0,532.0')] ).
cnf(974,plain,
equal(op2(h5(e11),e22),h1(e11)),
inference(rew,[status(thm),theory(equality)],[264,521,950,787]),
[iquote('0:Rew:264.0,521.0,950.0,521.0,787.0,521.0')] ).
cnf(977,plain,
equal(op2(e21,h2(e11)),h3(e11)),
inference(rew,[status(thm),theory(equality)],[260,518,794,938]),
[iquote('0:Rew:260.0,518.0,794.0,518.0,938.0,518.0')] ).
cnf(983,plain,
equal(op2(h1(e11),e22),h3(e11)),
inference(rew,[status(thm),theory(equality)],[950,513,977,258]),
[iquote('0:Rew:950.0,513.0,977.0,513.0,258.0,513.0')] ).
cnf(987,plain,
equal(op2(e23,h2(e11)),op2(e20,h12(e11))),
inference(rew,[status(thm),theory(equality)],[914,509,260,278]),
[iquote('0:Rew:914.0,509.0,260.0,509.0,278.0,509.0')] ).
cnf(990,plain,
equal(op2(h12(e11),e20),op2(e20,h12(e11))),
inference(rew,[status(thm),theory(equality)],[987,946]),
[iquote('0:Rew:987.0,946.0')] ).
cnf(991,plain,
equal(op2(e22,h5(e11)),op2(e20,h12(e11))),
inference(rew,[status(thm),theory(equality)],[987,960]),
[iquote('0:Rew:987.0,960.0')] ).
cnf(999,plain,
equal(op2(e20,h5(e11)),h3(e11)),
inference(rew,[status(thm),theory(equality)],[983,501,256,264]),
[iquote('0:Rew:983.0,501.0,256.0,501.0,264.0,501.0')] ).
cnf(1006,plain,
equal(op1(e13,e10),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[79,494]),
[iquote('0:Rew:79.0,494.0')] ).
cnf(1008,plain,
~ equal(op1(e13,e12),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[1006,346]),
[iquote('0:Rew:1006.0,346.0')] ).
cnf(1009,plain,
~ equal(op1(e13,e11),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[1006,345]),
[iquote('0:Rew:1006.0,345.0')] ).
cnf(1012,plain,
equal(op1(e13,op1(e13,e12)),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[79,493]),
[iquote('0:Rew:79.0,493.0')] ).
cnf(1013,plain,
equal(op1(e13,op1(e13,e11)),op1(e10,e11)),
inference(rew,[status(thm),theory(equality)],[79,492]),
[iquote('0:Rew:79.0,492.0')] ).
cnf(1021,plain,
equal(op1(op1(e10,e13),e10),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[1006,479,816]),
[iquote('0:Rew:1006.0,479.0,816.0,479.0')] ).
cnf(1022,plain,
equal(op1(e12,e10),op1(e11,e13)),
inference(rew,[status(thm),theory(equality)],[80,478,79]),
[iquote('0:Rew:80.0,478.0,79.0,478.0')] ).
cnf(1031,plain,
equal(op1(e12,op1(e10,e13)),op1(e11,e10)),
inference(rew,[status(thm),theory(equality)],[80,475,1006]),
[iquote('0:Rew:80.0,475.0,1006.0,475.0')] ).
cnf(1032,plain,
equal(op1(e12,e11),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[814,474,80]),
[iquote('0:Rew:814.0,474.0,80.0,474.0')] ).
cnf(1039,plain,
equal(op1(e11,e13),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[1022,473,814]),
[iquote('0:Rew:1022.0,473.0,814.0,473.0')] ).
cnf(1043,plain,
~ equal(op1(e10,e12),e11),
inference(rew,[status(thm),theory(equality)],[1039,881]),
[iquote('0:Rew:1039.0,881.0')] ).
cnf(1046,plain,
equal(op1(e12,e10),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[1039,1022]),
[iquote('0:Rew:1039.0,1022.0')] ).
cnf(1047,plain,
equal(op1(e11,e10),op1(e10,e11)),
inference(rew,[status(thm),theory(equality)],[814,472,1031,1032]),
[iquote('0:Rew:814.0,472.0,1031.0,472.0,1032.0,472.0')] ).
cnf(1048,plain,
~ equal(op1(e11,e12),op1(e10,e11)),
inference(rew,[status(thm),theory(equality)],[1047,334]),
[iquote('0:Rew:1047.0,334.0')] ).
cnf(1064,plain,
equal(op1(op1(e10,e12),e10),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[1046,463,816]),
[iquote('0:Rew:1046.0,463.0,816.0,463.0')] ).
cnf(1068,plain,
equal(op1(e11,op1(e10,e13)),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[1064,459,1039,1006]),
[iquote('0:Rew:1064.0,459.0,1039.0,459.0,1006.0,459.0')] ).
cnf(1070,plain,
equal(op1(op1(e11,e12),e12),op1(e10,e11)),
inference(rew,[status(thm),theory(equality)],[1047,457,814]),
[iquote('0:Rew:1047.0,457.0,814.0,457.0')] ).
cnf(1071,plain,
equal(op1(op1(e11,e12),e11),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[1068,456,1032]),
[iquote('0:Rew:1068.0,456.0,1032.0,456.0')] ).
cnf(1073,plain,
equal(op1(e11,op1(e10,e12)),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[815,454,1039]),
[iquote('0:Rew:815.0,454.0,1039.0,454.0')] ).
cnf(1079,plain,
equal(op1(op1(e10,e11),e12),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[1047,449,1073]),
[iquote('0:Rew:1047.0,449.0,1073.0,449.0')] ).
cnf(1105,plain,
( equal(h12(e11),e20)
| equal(h12(e11),e21)
| equal(h12(e11),e22)
| equal(h12(e11),e23) ),
inference(rew,[status(thm),theory(equality)],[278,570]),
[iquote('0:Rew:278.0,570.3,278.0,570.2,278.0,570.1,278.0,570.0')] ).
cnf(1106,plain,
( equal(h12(e11),e23)
| equal(h12(e11),e22)
| equal(h12(e11),e21) ),
inference(mrr,[status(thm)],[1105,817]),
[iquote('0:MRR:1105.0,817.0')] ).
cnf(1109,plain,
( equal(h3(e11),e20)
| equal(h3(e11),e21)
| equal(h3(e11),e22)
| equal(h3(e11),e23) ),
inference(rew,[status(thm),theory(equality)],[894,572]),
[iquote('0:Rew:894.0,572.3,894.0,572.2,894.0,572.1,894.0,572.0')] ).
cnf(1110,plain,
( equal(h3(e11),e23)
| equal(h3(e11),e22) ),
inference(mrr,[status(thm)],[1109,838,845]),
[iquote('0:MRR:1109.0,1109.1,838.0,845.0')] ).
cnf(1112,plain,
( equal(h2(e11),e20)
| equal(h2(e11),e21)
| equal(h2(e11),e22)
| equal(h2(e11),e23) ),
inference(rew,[status(thm),theory(equality)],[948,576]),
[iquote('0:Rew:948.0,576.3,948.0,576.2,948.0,576.1,948.0,576.0')] ).
cnf(1113,plain,
( equal(h2(e11),e23)
| equal(h2(e11),e22) ),
inference(mrr,[status(thm)],[1112,839,943]),
[iquote('0:MRR:1112.0,1112.1,839.0,943.0')] ).
cnf(1115,plain,
( equal(h5(e11),e20)
| equal(h5(e11),e21)
| equal(h5(e11),e22)
| equal(h5(e11),e23) ),
inference(rew,[status(thm),theory(equality)],[264,578]),
[iquote('0:Rew:264.0,578.3,264.0,578.2,264.0,578.1,264.0,578.0')] ).
cnf(1116,plain,
( equal(h5(e11),e23)
| equal(h5(e11),e22)
| equal(h5(e11),e21) ),
inference(mrr,[status(thm)],[1115,831]),
[iquote('0:MRR:1115.0,831.0')] ).
cnf(1117,plain,
( equal(h1(e11),e20)
| equal(h1(e11),e21)
| equal(h1(e11),e22)
| equal(h1(e11),e23) ),
inference(rew,[status(thm),theory(equality)],[950,580]),
[iquote('0:Rew:950.0,580.3,950.0,580.2,950.0,580.1,950.0,580.0')] ).
cnf(1118,plain,
( equal(h1(e11),e23)
| equal(h1(e11),e22)
| equal(h1(e11),e21) ),
inference(mrr,[status(thm)],[1117,840]),
[iquote('0:MRR:1117.0,840.0')] ).
cnf(1122,plain,
( equal(op1(e13,e12),e13)
| equal(op1(e13,e12),e12)
| equal(op1(e13,e12),e11) ),
inference(mrr,[status(thm)],[586,865]),
[iquote('0:MRR:586.0,865.0')] ).
cnf(1123,plain,
( equal(op1(e13,e11),e13)
| equal(op1(e13,e11),e11)
| equal(op1(e13,e11),e12) ),
inference(mrr,[status(thm)],[587,866]),
[iquote('0:MRR:587.0,866.0')] ).
cnf(1124,plain,
( equal(op1(e10,e13),e10)
| equal(op1(e10,e13),e11)
| equal(op1(e10,e13),e12)
| equal(op1(e10,e13),e13) ),
inference(rew,[status(thm),theory(equality)],[1006,588]),
[iquote('0:Rew:1006.0,588.3,1006.0,588.2,1006.0,588.1,1006.0,588.0')] ).
cnf(1125,plain,
( equal(op1(e10,e13),e13)
| equal(op1(e10,e13),e12) ),
inference(mrr,[status(thm)],[1124,876,883]),
[iquote('0:MRR:1124.0,1124.1,876.0,883.0')] ).
cnf(1127,plain,
( equal(op1(e10,e12),e10)
| equal(op1(e10,e12),e11)
| equal(op1(e10,e12),e12)
| equal(op1(e10,e12),e13) ),
inference(rew,[status(thm),theory(equality)],[1046,592]),
[iquote('0:Rew:1046.0,592.3,1046.0,592.2,1046.0,592.1,1046.0,592.0')] ).
cnf(1128,plain,
( equal(op1(e10,e12),e12)
| equal(op1(e10,e12),e13) ),
inference(mrr,[status(thm)],[1127,877,1043]),
[iquote('0:MRR:1127.0,1127.1,877.0,1043.0')] ).
cnf(1130,plain,
( equal(op1(e11,e12),e12)
| equal(op1(e11,e12),e11)
| equal(op1(e11,e12),e13) ),
inference(mrr,[status(thm)],[594,874]),
[iquote('0:MRR:594.0,874.0')] ).
cnf(1131,plain,
( equal(op1(e10,e11),e10)
| equal(op1(e10,e11),e11)
| equal(op1(e10,e11),e12)
| equal(op1(e10,e11),e13) ),
inference(rew,[status(thm),theory(equality)],[1047,596]),
[iquote('0:Rew:1047.0,596.3,1047.0,596.2,1047.0,596.1,1047.0,596.0')] ).
cnf(1132,plain,
( equal(op1(e10,e11),e11)
| equal(op1(e10,e11),e13)
| equal(op1(e10,e11),e12) ),
inference(mrr,[status(thm)],[1131,878]),
[iquote('0:MRR:1131.0,878.0')] ).
cnf(1135,plain,
( ~ equal(e23,e23)
| ~ equal(e20,e20)
| ~ equal(op2(e20,h12(e11)),h12(op1(e10,e11)))
| ~ equal(h12(op1(e10,e12)),h3(e11))
| ~ equal(h12(op1(e10,e13)),h2(e11))
| ~ equal(op2(e20,h12(e11)),h12(op1(e10,e11)))
| ~ equal(op2(h12(e11),h12(e11)),e20)
| ~ equal(h12(op1(e11,e12)),h11(e11))
| ~ equal(h12(op1(e10,e12)),h3(e11))
| ~ equal(h12(op1(e10,e12)),h3(e11))
| ~ equal(h12(op1(e10,e13)),h2(e11))
| ~ equal(e20,e20)
| ~ equal(h12(e11),h12(e11))
| ~ equal(h12(op1(e10,e13)),h2(e11))
| ~ equal(h12(op1(e13,e11)),h5(e11))
| ~ equal(h12(op1(e13,e12)),e21)
| ~ equal(e20,e20)
| ~ skC39
| ~ skC40
| ~ skC41 ),
inference(rew,[status(thm),theory(equality)],[787,602,54,791,79,82,53,925,948,1006,278,80,81,814,902,1032,894,1046,906,1039,905,815,990,1047,258,260,801,816]),
[iquote('0:Rew:787.0,602.16,54.0,602.16,791.0,602.16,79.0,602.16,82.0,602.15,54.0,602.15,53.0,602.15,925.0,602.14,54.0,602.14,948.0,602.13,54.0,602.13,791.0,602.13,1006.0,602.13,278.0,602.12,53.0,602.12,54.0,602.12,80.0,602.12,81.0,602.11,53.0,602.11,791.0,602.11,814.0,602.11,902.0,602.10,53.0,602.10,1032.0,602.10,894.0,602.9,53.0,602.9,791.0,602.9,1046.0,602.9,906.0,602.8,54.0,602.8,1039.0,602.8,905.0,602.7,53.0,602.7,791.0,602.6,815.0,602.6,990.0,602.5,791.0,602.5,1047.0,602.5,258.0,602.4,791.0,602.4,54.0,602.4,260.0,602.3,791.0,602.3,53.0,602.3,791.0,602.2,801.0,602.1,791.0,602.1,816.0,602.1,53.0,602.0')] ).
cnf(1136,plain,
( ~ equal(op2(e20,h12(e11)),h12(op1(e10,e11)))
| ~ equal(op2(h12(e11),h12(e11)),e20)
| ~ equal(h12(op1(e11,e12)),h11(e11))
| ~ equal(h12(op1(e10,e12)),h3(e11))
| ~ equal(h12(op1(e10,e13)),h2(e11))
| ~ equal(h12(op1(e13,e11)),h5(e11))
| ~ equal(h12(op1(e13,e12)),e21)
| ~ skC39
| ~ skC40
| ~ skC41 ),
inference(obv,[status(thm),theory(equality)],[1135]),
[iquote('0:Obv:1135.16')] ).
cnf(1137,plain,
( ~ skC40
| ~ equal(h12(op1(e13,e12)),e21)
| ~ equal(h12(op1(e13,e11)),h5(e11))
| ~ equal(h12(op1(e11,e12)),h11(e11))
| ~ equal(h12(op1(e10,e13)),h2(e11))
| ~ equal(h12(op1(e10,e12)),h3(e11))
| ~ equal(op2(e20,h12(e11)),h12(op1(e10,e11)))
| ~ equal(op2(h12(e11),h12(e11)),e20) ),
inference(mrr,[status(thm)],[1136,808,660]),
[iquote('0:MRR:1136.7,1136.9,808.0,660.0')] ).
cnf(1241,plain,
equal(e11,unit1),
inference(spt,[spt(split,[position(s1)])],[559]),
[iquote('1:Spt:559.2')] ).
cnf(1355,plain,
~ equal(op1(e13,e12),op1(e13,unit1)),
inference(rew,[status(thm),theory(equality)],[1241,348]),
[iquote('1:Rew:1241.0,348.0')] ).
cnf(1413,plain,
equal(op1(e12,unit1),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[1241,1032]),
[iquote('1:Rew:1241.0,1032.0')] ).
cnf(1428,plain,
( equal(op1(e13,e12),e13)
| equal(op1(e13,e12),e12)
| equal(op1(e13,e12),unit1) ),
inference(rew,[status(thm),theory(equality)],[1241,1122]),
[iquote('1:Rew:1241.0,1122.2')] ).
cnf(1445,plain,
equal(op1(e10,e13),e12),
inference(rew,[status(thm),theory(equality)],[60,1413]),
[iquote('1:Rew:60.0,1413.0')] ).
cnf(1451,plain,
~ equal(op1(e13,e12),e12),
inference(rew,[status(thm),theory(equality)],[1445,1008]),
[iquote('1:Rew:1445.0,1008.0')] ).
cnf(1453,plain,
equal(op1(e12,e10),e12),
inference(rew,[status(thm),theory(equality)],[1445,1021]),
[iquote('1:Rew:1445.0,1021.0')] ).
cnf(1460,plain,
equal(op1(e10,e12),e12),
inference(rew,[status(thm),theory(equality)],[1046,1453]),
[iquote('1:Rew:1046.0,1453.0')] ).
cnf(1466,plain,
equal(op1(e13,op1(e13,e12)),e12),
inference(rew,[status(thm),theory(equality)],[1460,1012]),
[iquote('1:Rew:1460.0,1012.0')] ).
cnf(1480,plain,
~ equal(op1(e13,e12),e13),
inference(rew,[status(thm),theory(equality)],[62,1355]),
[iquote('1:Rew:62.0,1355.0')] ).
cnf(1535,plain,
equal(op1(e13,e12),unit1),
inference(mrr,[status(thm)],[1428,1480,1451]),
[iquote('1:MRR:1428.0,1428.1,1480.0,1451.0')] ).
cnf(1541,plain,
equal(op1(e13,unit1),e12),
inference(rew,[status(thm),theory(equality)],[1535,1466]),
[iquote('1:Rew:1535.0,1466.0')] ).
cnf(1551,plain,
equal(e13,e12),
inference(rew,[status(thm),theory(equality)],[62,1541]),
[iquote('1:Rew:62.0,1541.0')] ).
cnf(1552,plain,
$false,
inference(mrr,[status(thm)],[1551,8]),
[iquote('1:MRR:1551.0,8.0')] ).
cnf(1578,plain,
~ equal(e11,unit1),
inference(spt,[spt(split,[position(sa)])],[1552,1241]),
[iquote('1:Spt:1552.0,559.2,1241.0')] ).
cnf(1579,plain,
( equal(e13,unit1)
| equal(e12,unit1)
| equal(e10,unit1) ),
inference(spt,[spt(split,[position(s2)])],[559]),
[iquote('1:Spt:1552.0,559.0,559.1,559.3')] ).
cnf(1580,plain,
equal(e13,unit1),
inference(spt,[spt(split,[position(s2s1)])],[1579]),
[iquote('2:Spt:1579.0')] ).
cnf(1650,plain,
~ equal(op1(e10,e11),op1(unit1,e11)),
inference(rew,[status(thm),theory(equality)],[1580,311]),
[iquote('2:Rew:1580.0,311.0')] ).
cnf(1660,plain,
~ equal(op1(e11,e12),op1(unit1,e12)),
inference(rew,[status(thm),theory(equality)],[1580,319]),
[iquote('2:Rew:1580.0,319.0')] ).
cnf(1663,plain,
~ equal(op1(e10,e12),op1(unit1,e12)),
inference(rew,[status(thm),theory(equality)],[1580,317]),
[iquote('2:Rew:1580.0,317.0')] ).
cnf(1682,plain,
( equal(op1(e10,e12),e12)
| equal(op1(e10,e12),unit1) ),
inference(rew,[status(thm),theory(equality)],[1580,1128]),
[iquote('2:Rew:1580.0,1128.1')] ).
cnf(1686,plain,
( equal(op1(e10,e11),e11)
| equal(op1(e10,e11),unit1)
| equal(op1(e10,e11),e12) ),
inference(rew,[status(thm),theory(equality)],[1580,1132]),
[iquote('2:Rew:1580.0,1132.1')] ).
cnf(1687,plain,
( equal(op1(e11,e12),e12)
| equal(op1(e11,e12),e11)
| equal(op1(e11,e12),unit1) ),
inference(rew,[status(thm),theory(equality)],[1580,1130]),
[iquote('2:Rew:1580.0,1130.2')] ).
cnf(1719,plain,
~ equal(op1(e10,e11),e11),
inference(rew,[status(thm),theory(equality)],[57,1650]),
[iquote('2:Rew:57.0,1650.0')] ).
cnf(1721,plain,
~ equal(op1(e11,e12),e12),
inference(rew,[status(thm),theory(equality)],[59,1660]),
[iquote('2:Rew:59.0,1660.0')] ).
cnf(1724,plain,
~ equal(op1(e10,e12),e12),
inference(rew,[status(thm),theory(equality)],[59,1663]),
[iquote('2:Rew:59.0,1663.0')] ).
cnf(1762,plain,
equal(op1(e10,e12),unit1),
inference(mrr,[status(thm)],[1682,1724]),
[iquote('2:MRR:1682.0,1724.0')] ).
cnf(1768,plain,
~ equal(op1(e10,e11),unit1),
inference(rew,[status(thm),theory(equality)],[1762,330]),
[iquote('2:Rew:1762.0,330.0')] ).
cnf(1769,plain,
~ equal(op1(e11,e12),unit1),
inference(rew,[status(thm),theory(equality)],[1762,315]),
[iquote('2:Rew:1762.0,315.0')] ).
cnf(1802,plain,
equal(op1(e10,e11),e12),
inference(mrr,[status(thm)],[1686,1719,1768]),
[iquote('2:MRR:1686.0,1686.1,1719.0,1768.0')] ).
cnf(1810,plain,
equal(op1(op1(e11,e12),e12),e12),
inference(rew,[status(thm),theory(equality)],[1802,1070]),
[iquote('2:Rew:1802.0,1070.0')] ).
cnf(1826,plain,
equal(op1(e11,e12),e11),
inference(mrr,[status(thm)],[1687,1721,1769]),
[iquote('2:MRR:1687.0,1687.2,1721.0,1769.0')] ).
cnf(1837,plain,
equal(op1(e11,e12),e12),
inference(rew,[status(thm),theory(equality)],[1826,1810]),
[iquote('2:Rew:1826.0,1810.0')] ).
cnf(1850,plain,
equal(e12,e11),
inference(rew,[status(thm),theory(equality)],[1826,1837]),
[iquote('2:Rew:1826.0,1837.0')] ).
cnf(1851,plain,
$false,
inference(mrr,[status(thm)],[1850,6]),
[iquote('2:MRR:1850.0,6.0')] ).
cnf(1876,plain,
~ equal(e13,unit1),
inference(spt,[spt(split,[position(s2sa)])],[1851,1580]),
[iquote('2:Spt:1851.0,1579.0,1580.0')] ).
cnf(1877,plain,
( equal(e12,unit1)
| equal(e10,unit1) ),
inference(spt,[spt(split,[position(s2s2)])],[1579]),
[iquote('2:Spt:1851.0,1579.1,1579.2')] ).
cnf(1878,plain,
equal(e12,unit1),
inference(spt,[spt(split,[position(s2s2s1)])],[1877]),
[iquote('3:Spt:1877.0')] ).
cnf(1920,plain,
~ equal(op1(e13,unit1),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[1878,1008]),
[iquote('3:Rew:1878.0,1008.0')] ).
cnf(1921,plain,
~ equal(op1(e13,e11),op1(e13,unit1)),
inference(rew,[status(thm),theory(equality)],[1878,348]),
[iquote('3:Rew:1878.0,348.0')] ).
cnf(1962,plain,
~ equal(op1(e11,unit1),op1(e10,e11)),
inference(rew,[status(thm),theory(equality)],[1878,1048]),
[iquote('3:Rew:1878.0,1048.0')] ).
cnf(1980,plain,
( equal(op1(e10,e13),e13)
| equal(op1(e10,e13),unit1) ),
inference(rew,[status(thm),theory(equality)],[1878,1125]),
[iquote('3:Rew:1878.0,1125.1')] ).
cnf(1984,plain,
( equal(op1(e10,e11),e11)
| equal(op1(e10,e11),e13)
| equal(op1(e10,e11),unit1) ),
inference(rew,[status(thm),theory(equality)],[1878,1132]),
[iquote('3:Rew:1878.0,1132.2')] ).
cnf(1985,plain,
( equal(op1(e13,e11),e13)
| equal(op1(e13,e11),e11)
| equal(op1(e13,e11),unit1) ),
inference(rew,[status(thm),theory(equality)],[1878,1123]),
[iquote('3:Rew:1878.0,1123.2')] ).
cnf(2011,plain,
~ equal(op1(e10,e13),e13),
inference(rew,[status(thm),theory(equality)],[62,1920]),
[iquote('3:Rew:62.0,1920.0')] ).
cnf(2012,plain,
~ equal(op1(e13,e11),e13),
inference(rew,[status(thm),theory(equality)],[62,1921]),
[iquote('3:Rew:62.0,1921.0')] ).
cnf(2018,plain,
~ equal(op1(e10,e11),e11),
inference(rew,[status(thm),theory(equality)],[58,1962]),
[iquote('3:Rew:58.0,1962.0')] ).
cnf(2056,plain,
equal(op1(e10,e13),unit1),
inference(mrr,[status(thm)],[1980,2011]),
[iquote('3:MRR:1980.0,2011.0')] ).
cnf(2062,plain,
~ equal(op1(e13,e11),unit1),
inference(rew,[status(thm),theory(equality)],[2056,1009]),
[iquote('3:Rew:2056.0,1009.0')] ).
cnf(2063,plain,
~ equal(op1(e10,e11),unit1),
inference(rew,[status(thm),theory(equality)],[2056,331]),
[iquote('3:Rew:2056.0,331.0')] ).
cnf(2095,plain,
equal(op1(e10,e11),e13),
inference(mrr,[status(thm)],[1984,2018,2063]),
[iquote('3:MRR:1984.0,1984.2,2018.0,2063.0')] ).
cnf(2101,plain,
equal(op1(e13,op1(e13,e11)),e13),
inference(rew,[status(thm),theory(equality)],[2095,1013]),
[iquote('3:Rew:2095.0,1013.0')] ).
cnf(2119,plain,
equal(op1(e13,e11),e11),
inference(mrr,[status(thm)],[1985,2012,2062]),
[iquote('3:MRR:1985.0,1985.2,2012.0,2062.0')] ).
cnf(2130,plain,
equal(op1(e13,e11),e13),
inference(rew,[status(thm),theory(equality)],[2119,2101]),
[iquote('3:Rew:2119.0,2101.0')] ).
cnf(2143,plain,
equal(e13,e11),
inference(rew,[status(thm),theory(equality)],[2119,2130]),
[iquote('3:Rew:2119.0,2130.0')] ).
cnf(2144,plain,
$false,
inference(mrr,[status(thm)],[2143,7]),
[iquote('3:MRR:2143.0,7.0')] ).
cnf(2169,plain,
~ equal(e12,unit1),
inference(spt,[spt(split,[position(s2s2sa)])],[2144,1878]),
[iquote('3:Spt:2144.0,1877.0,1878.0')] ).
cnf(2170,plain,
equal(e10,unit1),
inference(spt,[spt(split,[position(s2s2s2)])],[1877]),
[iquote('3:Spt:2144.0,1877.1')] ).
cnf(2243,plain,
equal(op1(op1(e11,e12),e12),e11),
inference(rew,[status(thm),theory(equality)],[57,1070,2170]),
[iquote('3:Rew:57.0,1070.0,2170.0,1070.0')] ).
cnf(2244,plain,
equal(op1(e11,e12),e13),
inference(rew,[status(thm),theory(equality)],[57,1079,61,2170]),
[iquote('3:Rew:57.0,1079.0,61.0,1079.0,2170.0,1079.0')] ).
cnf(2250,plain,
equal(op1(e13,e12),e11),
inference(rew,[status(thm),theory(equality)],[2244,2243]),
[iquote('3:Rew:2244.0,2243.0')] ).
cnf(2263,plain,
equal(op1(e13,e11),e12),
inference(rew,[status(thm),theory(equality)],[2244,1071,59,2170]),
[iquote('3:Rew:2244.0,1071.0,59.0,1071.0,2170.0,1071.0')] ).
cnf(2317,plain,
( ~ skC40
| ~ equal(h12(e11),e21)
| ~ equal(h5(e11),e23)
| ~ equal(h11(e11),e22)
| ~ equal(h2(e11),e22)
| ~ equal(h3(e11),e23)
| ~ equal(op2(e20,h12(e11)),h12(e11))
| ~ equal(op2(h12(e11),h12(e11)),e20) ),
inference(rew,[status(thm),theory(equality)],[57,1137,2170,53,59,54,61,2244,2263,2250]),
[iquote('3:Rew:57.0,1137.6,2170.0,1137.6,53.0,1137.5,59.0,1137.5,2170.0,1137.5,54.0,1137.4,61.0,1137.4,2170.0,1137.4,54.0,1137.3,2244.0,1137.3,53.0,1137.2,2263.0,1137.2,2250.0,1137.1')] ).
cnf(2318,plain,
( ~ equal(h12(e11),e21)
| ~ equal(h5(e11),e23)
| ~ equal(h11(e11),e22)
| ~ equal(h2(e11),e22)
| ~ equal(h3(e11),e23)
| ~ equal(op2(e20,h12(e11)),h12(e11))
| ~ equal(op2(h12(e11),h12(e11)),e20) ),
inference(mrr,[status(thm)],[2317,220]),
[iquote('3:MRR:2317.0,220.1')] ).
cnf(2336,plain,
equal(e20,unit2),
inference(spt,[spt(split,[position(s2s2s2s1)])],[560]),
[iquote('4:Spt:560.3')] ).
cnf(2358,plain,
equal(op2(e21,e21),unit2),
inference(rew,[status(thm),theory(equality)],[2336,794]),
[iquote('4:Rew:2336.0,794.0')] ).
cnf(2371,plain,
equal(op2(e21,unit2),h1(e11)),
inference(rew,[status(thm),theory(equality)],[2336,950]),
[iquote('4:Rew:2336.0,950.0')] ).
cnf(2375,plain,
equal(op2(e22,unit2),h2(e11)),
inference(rew,[status(thm),theory(equality)],[2336,948]),
[iquote('4:Rew:2336.0,948.0')] ).
cnf(2399,plain,
( ~ equal(h12(e11),e21)
| ~ equal(h5(e11),e23)
| ~ equal(h11(e11),e22)
| ~ equal(h2(e11),e22)
| ~ equal(h3(e11),e23)
| ~ equal(op2(unit2,h12(e11)),h12(e11))
| ~ equal(op2(h12(e11),h12(e11)),e20) ),
inference(rew,[status(thm),theory(equality)],[2336,2318]),
[iquote('4:Rew:2336.0,2318.5')] ).
cnf(2438,plain,
equal(h1(e11),e21),
inference(rew,[status(thm),theory(equality)],[66,2371]),
[iquote('4:Rew:66.0,2371.0')] ).
cnf(2446,plain,
equal(op2(e21,e22),h3(e11)),
inference(rew,[status(thm),theory(equality)],[2438,983]),
[iquote('4:Rew:2438.0,983.0')] ).
cnf(2448,plain,
equal(op2(h5(e11),e22),e21),
inference(rew,[status(thm),theory(equality)],[2438,974]),
[iquote('4:Rew:2438.0,974.0')] ).
cnf(2451,plain,
equal(op2(e23,e21),h2(e11)),
inference(rew,[status(thm),theory(equality)],[2438,961]),
[iquote('4:Rew:2438.0,961.0')] ).
cnf(2461,plain,
equal(h2(e11),e22),
inference(rew,[status(thm),theory(equality)],[68,2375]),
[iquote('4:Rew:68.0,2375.0')] ).
cnf(2468,plain,
~ equal(h3(e11),e22),
inference(rew,[status(thm),theory(equality)],[2461,835]),
[iquote('4:Rew:2461.0,835.0')] ).
cnf(2481,plain,
equal(h3(e11),e23),
inference(mrr,[status(thm)],[1110,2468]),
[iquote('4:MRR:1110.1,2468.0')] ).
cnf(2499,plain,
equal(h5(e11),e23),
inference(rew,[status(thm),theory(equality)],[264,2446,2481]),
[iquote('4:Rew:264.0,2446.0,2481.0,2446.0')] ).
cnf(2509,plain,
equal(h12(e11),e21),
inference(rew,[status(thm),theory(equality)],[278,2448,2499]),
[iquote('4:Rew:278.0,2448.0,2499.0,2448.0')] ).
cnf(2522,plain,
equal(h11(e11),e22),
inference(rew,[status(thm),theory(equality)],[276,2451,2461]),
[iquote('4:Rew:276.0,2451.0,2461.0,2451.0')] ).
cnf(2595,plain,
( ~ equal(e21,e21)
| ~ equal(e23,e23)
| ~ equal(e22,e22)
| ~ equal(e22,e22)
| ~ equal(e23,e23)
| ~ equal(e21,e21)
| ~ equal(unit2,unit2) ),
inference(rew,[status(thm),theory(equality)],[2358,2399,2509,2336,65,2481,2461,2522,2499]),
[iquote('4:Rew:2358.0,2399.6,2509.0,2399.6,2336.0,2399.6,65.0,2399.5,2509.0,2399.5,2481.0,2399.4,2461.0,2399.3,2522.0,2399.2,2499.0,2399.1,2509.0,2399.0')] ).
cnf(2596,plain,
$false,
inference(obv,[status(thm),theory(equality)],[2595]),
[iquote('4:Obv:2595.6')] ).
cnf(2597,plain,
~ equal(e20,unit2),
inference(spt,[spt(split,[position(s2s2s2sa)])],[2596,2336]),
[iquote('4:Spt:2596.0,560.3,2336.0')] ).
cnf(2598,plain,
( equal(e23,unit2)
| equal(e22,unit2)
| equal(e21,unit2) ),
inference(spt,[spt(split,[position(s2s2s2s2)])],[560]),
[iquote('4:Spt:2596.0,560.0,560.1,560.2')] ).
cnf(2599,plain,
equal(e23,unit2),
inference(spt,[spt(split,[position(s2s2s2s2s1)])],[2598]),
[iquote('5:Spt:2598.0')] ).
cnf(2638,plain,
equal(op2(unit2,e22),h12(e11)),
inference(rew,[status(thm),theory(equality)],[2599,278]),
[iquote('5:Rew:2599.0,278.0')] ).
cnf(2639,plain,
equal(op2(unit2,e21),h11(e11)),
inference(rew,[status(thm),theory(equality)],[2599,276]),
[iquote('5:Rew:2599.0,276.0')] ).
cnf(2648,plain,
( equal(h2(e11),unit2)
| equal(h2(e11),e22) ),
inference(rew,[status(thm),theory(equality)],[2599,1113]),
[iquote('5:Rew:2599.0,1113.0')] ).
cnf(2663,plain,
( equal(h1(e11),unit2)
| equal(h1(e11),e22)
| equal(h1(e11),e21) ),
inference(rew,[status(thm),theory(equality)],[2599,1118]),
[iquote('5:Rew:2599.0,1118.0')] ).
cnf(2665,plain,
( equal(h5(e11),unit2)
| equal(h5(e11),e22)
| equal(h5(e11),e21) ),
inference(rew,[status(thm),theory(equality)],[2599,1116]),
[iquote('5:Rew:2599.0,1116.0')] ).
cnf(2684,plain,
equal(h12(e11),e22),
inference(rew,[status(thm),theory(equality)],[67,2638]),
[iquote('5:Rew:67.0,2638.0')] ).
cnf(2688,plain,
~ equal(h2(e11),e22),
inference(rew,[status(thm),theory(equality)],[2684,850]),
[iquote('5:Rew:2684.0,850.0')] ).
cnf(2689,plain,
~ equal(h3(e11),e22),
inference(rew,[status(thm),theory(equality)],[2684,898]),
[iquote('5:Rew:2684.0,898.0')] ).
cnf(2690,plain,
~ equal(h5(e11),e22),
inference(rew,[status(thm),theory(equality)],[2684,848]),
[iquote('5:Rew:2684.0,848.0')] ).
cnf(2702,plain,
equal(h11(e11),e21),
inference(rew,[status(thm),theory(equality)],[65,2639]),
[iquote('5:Rew:65.0,2639.0')] ).
cnf(2705,plain,
~ equal(h1(e11),e21),
inference(rew,[status(thm),theory(equality)],[2702,856]),
[iquote('5:Rew:2702.0,856.0')] ).
cnf(2733,plain,
equal(h2(e11),unit2),
inference(mrr,[status(thm)],[2648,2688]),
[iquote('5:MRR:2648.1,2688.0')] ).
cnf(2742,plain,
~ equal(h1(e11),unit2),
inference(rew,[status(thm),theory(equality)],[2733,837]),
[iquote('5:Rew:2733.0,837.0')] ).
cnf(2744,plain,
~ equal(h5(e11),unit2),
inference(rew,[status(thm),theory(equality)],[2733,852]),
[iquote('5:Rew:2733.0,852.0')] ).
cnf(2784,plain,
equal(h1(e11),e22),
inference(mrr,[status(thm)],[2663,2742,2705]),
[iquote('5:MRR:2663.0,2663.2,2742.0,2705.0')] ).
cnf(2787,plain,
equal(op2(e20,e21),e22),
inference(rew,[status(thm),theory(equality)],[2784,256]),
[iquote('5:Rew:2784.0,256.0')] ).
cnf(2823,plain,
equal(h5(e11),e21),
inference(mrr,[status(thm)],[2665,2744,2690]),
[iquote('5:MRR:2665.0,2665.1,2744.0,2690.0')] ).
cnf(2827,plain,
equal(op2(e20,e21),h3(e11)),
inference(rew,[status(thm),theory(equality)],[2823,999]),
[iquote('5:Rew:2823.0,999.0')] ).
cnf(2848,plain,
equal(h3(e11),e22),
inference(rew,[status(thm),theory(equality)],[2787,2827]),
[iquote('5:Rew:2787.0,2827.0')] ).
cnf(2849,plain,
$false,
inference(mrr,[status(thm)],[2848,2689]),
[iquote('5:MRR:2848.0,2689.0')] ).
cnf(2864,plain,
~ equal(e23,unit2),
inference(spt,[spt(split,[position(s2s2s2s2sa)])],[2849,2599]),
[iquote('5:Spt:2849.0,2598.0,2599.0')] ).
cnf(2865,plain,
( equal(e22,unit2)
| equal(e21,unit2) ),
inference(spt,[spt(split,[position(s2s2s2s2s2)])],[2598]),
[iquote('5:Spt:2849.0,2598.1,2598.2')] ).
cnf(2866,plain,
equal(e22,unit2),
inference(spt,[spt(split,[position(s2s2s2s2s2s1)])],[2865]),
[iquote('6:Spt:2865.0')] ).
cnf(2900,plain,
equal(op2(e23,unit2),h12(e11)),
inference(rew,[status(thm),theory(equality)],[2866,278]),
[iquote('6:Rew:2866.0,278.0')] ).
cnf(2922,plain,
equal(op2(e21,unit2),h5(e11)),
inference(rew,[status(thm),theory(equality)],[2866,264]),
[iquote('6:Rew:2866.0,264.0')] ).
cnf(2932,plain,
equal(op2(e20,h12(e11)),op2(unit2,h5(e11))),
inference(rew,[status(thm),theory(equality)],[2866,991]),
[iquote('6:Rew:2866.0,991.0')] ).
cnf(2947,plain,
equal(h12(e11),e23),
inference(rew,[status(thm),theory(equality)],[70,2900]),
[iquote('6:Rew:70.0,2900.0')] ).
cnf(2971,plain,
equal(h5(e11),e21),
inference(rew,[status(thm),theory(equality)],[66,2922]),
[iquote('6:Rew:66.0,2922.0')] ).
cnf(3084,plain,
equal(h3(e11),e21),
inference(rew,[status(thm),theory(equality)],[260,2932,2947,65,2971]),
[iquote('6:Rew:260.0,2932.0,2947.0,2932.0,65.0,2932.0,2971.0,2932.0')] ).
cnf(3085,plain,
$false,
inference(mrr,[status(thm)],[3084,845]),
[iquote('6:MRR:3084.0,845.0')] ).
cnf(3097,plain,
~ equal(e22,unit2),
inference(spt,[spt(split,[position(s2s2s2s2s2sa)])],[3085,2866]),
[iquote('6:Spt:3085.0,2865.0,2866.0')] ).
cnf(3098,plain,
equal(e21,unit2),
inference(spt,[spt(split,[position(s2s2s2s2s2s2)])],[2865]),
[iquote('6:Spt:3085.0,2865.1')] ).
cnf(3125,plain,
equal(op2(e23,unit2),h11(e11)),
inference(rew,[status(thm),theory(equality)],[3098,276]),
[iquote('6:Rew:3098.0,276.0')] ).
cnf(3136,plain,
equal(h3(e11),e22),
inference(rew,[status(thm),theory(equality)],[68,929,3098]),
[iquote('6:Rew:68.0,929.0,3098.0,929.0')] ).
cnf(3140,plain,
equal(op2(e22,e20),e22),
inference(rew,[status(thm),theory(equality)],[3136,916]),
[iquote('6:Rew:3136.0,916.0')] ).
cnf(3150,plain,
equal(h2(e11),e22),
inference(rew,[status(thm),theory(equality)],[948,3140]),
[iquote('6:Rew:948.0,3140.0')] ).
cnf(3170,plain,
~ equal(h12(e11),e22),
inference(rew,[status(thm),theory(equality)],[3150,850]),
[iquote('6:Rew:3150.0,850.0')] ).
cnf(3195,plain,
equal(h11(e11),e23),
inference(rew,[status(thm),theory(equality)],[70,3125]),
[iquote('6:Rew:70.0,3125.0')] ).
cnf(3199,plain,
~ equal(h12(e11),e23),
inference(rew,[status(thm),theory(equality)],[3195,819]),
[iquote('6:Rew:3195.0,819.0')] ).
cnf(3211,plain,
equal(op2(e23,h12(e11)),e22),
inference(rew,[status(thm),theory(equality)],[3150,902]),
[iquote('6:Rew:3150.0,902.0')] ).
cnf(3267,plain,
( equal(h12(e11),e23)
| equal(h12(e11),e22)
| equal(h12(e11),unit2) ),
inference(rew,[status(thm),theory(equality)],[3098,1106]),
[iquote('6:Rew:3098.0,1106.2')] ).
cnf(3268,plain,
equal(h12(e11),unit2),
inference(mrr,[status(thm)],[3267,3199,3170]),
[iquote('6:MRR:3267.0,3267.1,3199.0,3170.0')] ).
cnf(3278,plain,
equal(op2(e23,unit2),e22),
inference(rew,[status(thm),theory(equality)],[3268,3211]),
[iquote('6:Rew:3268.0,3211.0')] ).
cnf(3287,plain,
equal(e22,e23),
inference(rew,[status(thm),theory(equality)],[70,3278]),
[iquote('6:Rew:70.0,3278.0')] ).
cnf(3288,plain,
$false,
inference(mrr,[status(thm)],[3287,14]),
[iquote('6:MRR:3287.0,14.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ALG015+1 : TPTP v8.1.0. Released v2.7.0.
% 0.07/0.14 % Command : run_spass %d %s
% 0.15/0.35 % Computer : n021.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 600
% 0.15/0.35 % DateTime : Wed Jun 8 10:11:52 EDT 2022
% 0.15/0.35 % CPUTime :
% 0.73/0.89
% 0.73/0.89 SPASS V 3.9
% 0.73/0.89 SPASS beiseite: Proof found.
% 0.73/0.89 % SZS status Theorem
% 0.73/0.89 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.73/0.89 SPASS derived 1224 clauses, backtracked 885 clauses, performed 6 splits and kept 1969 clauses.
% 0.73/0.89 SPASS allocated 88350 KBytes.
% 0.73/0.89 SPASS spent 0:00:00.53 on the problem.
% 0.73/0.89 0:00:00.04 for the input.
% 0.73/0.89 0:00:00.17 for the FLOTTER CNF translation.
% 0.73/0.89 0:00:00.00 for inferences.
% 0.73/0.89 0:00:00.01 for the backtracking.
% 0.73/0.89 0:00:00.27 for the reduction.
% 0.73/0.89
% 0.73/0.89
% 0.73/0.89 Here is a proof with depth 3, length 403 :
% 0.73/0.89 % SZS output start Refutation
% See solution above
% 0.73/0.91 Formulae used in the proof : ax19 ax20 ax37 ax3 ax7 ax24 ax25 co1 ax26 ax27 ax28 ax29 ax30 ax31 ax32 ax33 ax35 ax36 ax22 ax23 ax17 ax18 ax2 ax6 ax5 ax1
% 0.73/0.91
%------------------------------------------------------------------------------