%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG062+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 14 18:02:11 EDT 2022
% Result : Theorem 0.39s 0.58s
% Output : Refutation 0.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 105
% Syntax : Number of clauses : 334 ( 207 unt; 91 nHn; 334 RR)
% Number of literals : 649 ( 0 equ; 232 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 5 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ equal(e1,e0),
file('ALG062+1.p',unknown),
[] ).
cnf(2,axiom,
~ equal(e2,e0),
file('ALG062+1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(e3,e0),
file('ALG062+1.p',unknown),
[] ).
cnf(4,axiom,
~ equal(e4,e0),
file('ALG062+1.p',unknown),
[] ).
cnf(5,axiom,
~ equal(e2,e1),
file('ALG062+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e3,e1),
file('ALG062+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(e4,e1),
file('ALG062+1.p',unknown),
[] ).
cnf(8,axiom,
~ equal(e3,e2),
file('ALG062+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(e4,e2),
file('ALG062+1.p',unknown),
[] ).
cnf(10,axiom,
~ equal(e4,e3),
file('ALG062+1.p',unknown),
[] ).
cnf(11,axiom,
equal(op(unit,e0),e0),
file('ALG062+1.p',unknown),
[] ).
cnf(12,axiom,
equal(op(e0,unit),e0),
file('ALG062+1.p',unknown),
[] ).
cnf(13,axiom,
equal(op(unit,e1),e1),
file('ALG062+1.p',unknown),
[] ).
cnf(14,axiom,
equal(op(e1,unit),e1),
file('ALG062+1.p',unknown),
[] ).
cnf(15,axiom,
equal(op(unit,e2),e2),
file('ALG062+1.p',unknown),
[] ).
cnf(16,axiom,
equal(op(e2,unit),e2),
file('ALG062+1.p',unknown),
[] ).
cnf(17,axiom,
equal(op(unit,e3),e3),
file('ALG062+1.p',unknown),
[] ).
cnf(18,axiom,
equal(op(e3,unit),e3),
file('ALG062+1.p',unknown),
[] ).
cnf(19,axiom,
equal(op(unit,e4),e4),
file('ALG062+1.p',unknown),
[] ).
cnf(20,axiom,
equal(op(e4,unit),e4),
file('ALG062+1.p',unknown),
[] ).
cnf(21,axiom,
equal(op(e1,e1),e4),
file('ALG062+1.p',unknown),
[] ).
cnf(23,axiom,
~ equal(op(e2,e0),op(e0,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(24,axiom,
~ equal(op(e3,e0),op(e0,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(25,axiom,
~ equal(op(e4,e0),op(e0,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(26,axiom,
~ equal(op(e2,e0),op(e1,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(29,axiom,
~ equal(op(e3,e0),op(e2,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(30,axiom,
~ equal(op(e4,e0),op(e2,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(36,axiom,
~ equal(op(e2,e1),op(e1,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(37,axiom,
~ equal(op(e3,e1),op(e1,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(40,axiom,
~ equal(op(e4,e1),op(e2,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(45,axiom,
~ equal(op(e4,e2),op(e0,e2)),
file('ALG062+1.p',unknown),
[] ).
cnf(48,axiom,
~ equal(op(e4,e2),op(e1,e2)),
file('ALG062+1.p',unknown),
[] ).
cnf(50,axiom,
~ equal(op(e4,e2),op(e2,e2)),
file('ALG062+1.p',unknown),
[] ).
cnf(55,axiom,
~ equal(op(e4,e3),op(e0,e3)),
file('ALG062+1.p',unknown),
[] ).
cnf(59,axiom,
~ equal(op(e3,e3),op(e2,e3)),
file('ALG062+1.p',unknown),
[] ).
cnf(60,axiom,
~ equal(op(e4,e3),op(e2,e3)),
file('ALG062+1.p',unknown),
[] ).
cnf(61,axiom,
~ equal(op(e4,e3),op(e3,e3)),
file('ALG062+1.p',unknown),
[] ).
cnf(62,axiom,
~ equal(op(e1,e4),op(e0,e4)),
file('ALG062+1.p',unknown),
[] ).
cnf(64,axiom,
~ equal(op(e3,e4),op(e0,e4)),
file('ALG062+1.p',unknown),
[] ).
cnf(65,axiom,
~ equal(op(e4,e4),op(e0,e4)),
file('ALG062+1.p',unknown),
[] ).
cnf(68,axiom,
~ equal(op(e4,e4),op(e1,e4)),
file('ALG062+1.p',unknown),
[] ).
cnf(72,axiom,
~ equal(op(e0,e1),op(e0,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(75,axiom,
~ equal(op(e0,e4),op(e0,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(76,axiom,
~ equal(op(e0,e2),op(e0,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(79,axiom,
~ equal(op(e0,e3),op(e0,e2)),
file('ALG062+1.p',unknown),
[] ).
cnf(81,axiom,
~ equal(op(e0,e4),op(e0,e3)),
file('ALG062+1.p',unknown),
[] ).
cnf(87,axiom,
~ equal(op(e1,e3),op(e1,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(88,axiom,
~ equal(op(e1,e4),op(e1,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(90,axiom,
~ equal(op(e1,e4),op(e1,e2)),
file('ALG062+1.p',unknown),
[] ).
cnf(91,axiom,
~ equal(op(e1,e4),op(e1,e3)),
file('ALG062+1.p',unknown),
[] ).
cnf(92,axiom,
~ equal(op(e2,e1),op(e2,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(93,axiom,
~ equal(op(e2,e2),op(e2,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(94,axiom,
~ equal(op(e2,e3),op(e2,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(96,axiom,
~ equal(op(e2,e2),op(e2,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(97,axiom,
~ equal(op(e2,e3),op(e2,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(99,axiom,
~ equal(op(e2,e3),op(e2,e2)),
file('ALG062+1.p',unknown),
[] ).
cnf(100,axiom,
~ equal(op(e2,e4),op(e2,e2)),
file('ALG062+1.p',unknown),
[] ).
cnf(102,axiom,
~ equal(op(e3,e1),op(e3,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(103,axiom,
~ equal(op(e3,e2),op(e3,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(104,axiom,
~ equal(op(e3,e3),op(e3,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(105,axiom,
~ equal(op(e3,e4),op(e3,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(106,axiom,
~ equal(op(e3,e2),op(e3,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(111,axiom,
~ equal(op(e3,e4),op(e3,e3)),
file('ALG062+1.p',unknown),
[] ).
cnf(113,axiom,
~ equal(op(e4,e2),op(e4,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(115,axiom,
~ equal(op(e4,e4),op(e4,e0)),
file('ALG062+1.p',unknown),
[] ).
cnf(116,axiom,
~ equal(op(e4,e2),op(e4,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(117,axiom,
~ equal(op(e4,e3),op(e4,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(118,axiom,
~ equal(op(e4,e4),op(e4,e1)),
file('ALG062+1.p',unknown),
[] ).
cnf(120,axiom,
~ equal(op(e4,e4),op(e4,e2)),
file('ALG062+1.p',unknown),
[] ).
cnf(122,axiom,
equal(op(op(e1,e1),op(e1,e1)),e2),
file('ALG062+1.p',unknown),
[] ).
cnf(123,axiom,
equal(op(e1,op(op(e1,e1),op(e1,e1))),e0),
file('ALG062+1.p',unknown),
[] ).
cnf(131,axiom,
( ~ equal(e0,unit)
| ~ equal(op(e1,e2),e0)
| ~ skC0 ),
file('ALG062+1.p',unknown),
[] ).
cnf(198,axiom,
( ~ equal(e2,unit)
| ~ equal(op(e4,e4),e2)
| ~ skC2 ),
file('ALG062+1.p',unknown),
[] ).
cnf(229,axiom,
( ~ equal(op(e1,e2),e0)
| ~ skC0
| equal(op(e1,e0),e2) ),
file('ALG062+1.p',unknown),
[] ).
cnf(240,axiom,
( ~ skC0
| ~ equal(op(e4,e1),e0)
| equal(op(e4,e0),e1) ),
file('ALG062+1.p',unknown),
[] ).
cnf(244,axiom,
( ~ skC1
| ~ equal(op(e0,e0),e1)
| equal(op(e0,e1),e0) ),
file('ALG062+1.p',unknown),
[] ).
cnf(259,axiom,
( ~ equal(op(e3,e4),e1)
| ~ skC1
| equal(op(e3,e1),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(261,axiom,
( ~ equal(op(e4,e2),e1)
| ~ skC1
| equal(op(e4,e1),e2) ),
file('ALG062+1.p',unknown),
[] ).
cnf(273,axiom,
( ~ equal(op(e2,e1),e2)
| ~ skC2
| equal(op(e2,e2),e1) ),
file('ALG062+1.p',unknown),
[] ).
cnf(283,axiom,
( ~ equal(op(e4,e4),e2)
| ~ skC2
| equal(op(e4,e2),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(294,axiom,
( ~ equal(op(e2,e2),e3)
| ~ skC3
| equal(op(e2,e3),e2) ),
file('ALG062+1.p',unknown),
[] ).
cnf(334,axiom,
( ~ equal(op(e1,e1),e4)
| equal(op(e1,e4),e1)
| skC0
| skC1
| skC2
| skC3 ),
file('ALG062+1.p',unknown),
[] ).
cnf(340,axiom,
( ~ equal(op(e2,e3),e4)
| equal(op(e2,e4),e3)
| skC0
| skC1
| skC2
| skC3 ),
file('ALG062+1.p',unknown),
[] ).
cnf(341,axiom,
( ~ equal(op(e3,e0),e4)
| skC3
| skC2
| skC1
| skC0
| equal(op(e3,e4),e0) ),
file('ALG062+1.p',unknown),
[] ).
cnf(349,axiom,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit)
| equal(e0,unit) ),
file('ALG062+1.p',unknown),
[] ).
cnf(350,axiom,
equal(op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))),e3),
file('ALG062+1.p',unknown),
[] ).
cnf(354,axiom,
( equal(op(e4,e0),e3)
| equal(op(e4,e1),e3)
| equal(op(e4,e2),e3)
| equal(op(e4,e3),e3)
| equal(op(e4,e4),e3) ),
file('ALG062+1.p',unknown),
[] ).
cnf(360,axiom,
( equal(op(e4,e0),e0)
| equal(op(e4,e1),e0)
| equal(op(e4,e2),e0)
| equal(op(e4,e3),e0)
| equal(op(e4,e4),e0) ),
file('ALG062+1.p',unknown),
[] ).
cnf(361,axiom,
( equal(op(e0,e3),e4)
| equal(op(e1,e3),e4)
| equal(op(e2,e3),e4)
| equal(op(e3,e3),e4)
| equal(op(e4,e3),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(368,axiom,
( equal(op(e3,e3),e1)
| equal(op(e3,e1),e1)
| equal(op(e3,e4),e1)
| equal(op(e3,e2),e1)
| equal(op(e3,e0),e1) ),
file('ALG062+1.p',unknown),
[] ).
cnf(371,axiom,
( equal(op(e0,e2),e4)
| equal(op(e1,e2),e4)
| equal(op(e2,e2),e4)
| equal(op(e3,e2),e4)
| equal(op(e4,e2),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(372,axiom,
( equal(op(e2,e0),e4)
| equal(op(e2,e1),e4)
| equal(op(e2,e2),e4)
| equal(op(e2,e3),e4)
| equal(op(e2,e4),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(375,axiom,
( equal(op(e0,e2),e2)
| equal(op(e1,e2),e2)
| equal(op(e2,e2),e2)
| equal(op(e3,e2),e2)
| equal(op(e4,e2),e2) ),
file('ALG062+1.p',unknown),
[] ).
cnf(378,axiom,
( equal(op(e2,e0),e1)
| equal(op(e2,e1),e1)
| equal(op(e2,e2),e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e4),e1) ),
file('ALG062+1.p',unknown),
[] ).
cnf(383,axiom,
( equal(op(e0,e1),e3)
| equal(op(e1,e1),e3)
| equal(op(e2,e1),e3)
| equal(op(e3,e1),e3)
| equal(op(e4,e1),e3) ),
file('ALG062+1.p',unknown),
[] ).
cnf(385,axiom,
( equal(op(e0,e1),e2)
| equal(op(e1,e1),e2)
| equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(e4,e1),e2) ),
file('ALG062+1.p',unknown),
[] ).
cnf(395,axiom,
( equal(op(e0,e0),e2)
| equal(op(e1,e0),e2)
| equal(op(e2,e0),e2)
| equal(op(e3,e0),e2)
| equal(op(e4,e0),e2) ),
file('ALG062+1.p',unknown),
[] ).
cnf(403,axiom,
( equal(op(e4,e2),e0)
| equal(op(e4,e2),e1)
| equal(op(e4,e2),e2)
| equal(op(e4,e2),e3)
| equal(op(e4,e2),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(410,axiom,
( equal(op(e3,e0),e3)
| equal(op(e3,e0),e0)
| equal(op(e3,e0),e4)
| equal(op(e3,e0),e2)
| equal(op(e3,e0),e1) ),
file('ALG062+1.p',unknown),
[] ).
cnf(412,axiom,
( equal(op(e2,e3),e0)
| equal(op(e2,e3),e1)
| equal(op(e2,e3),e2)
| equal(op(e2,e3),e3)
| equal(op(e2,e3),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(415,axiom,
( equal(op(e2,e0),e0)
| equal(op(e2,e0),e1)
| equal(op(e2,e0),e2)
| equal(op(e2,e0),e3)
| equal(op(e2,e0),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(416,axiom,
( equal(op(e1,e4),e0)
| equal(op(e1,e4),e1)
| equal(op(e1,e4),e2)
| equal(op(e1,e4),e3)
| equal(op(e1,e4),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(421,axiom,
( equal(op(e0,e4),e0)
| equal(op(e0,e4),e1)
| equal(op(e0,e4),e2)
| equal(op(e0,e4),e3)
| equal(op(e0,e4),e4) ),
file('ALG062+1.p',unknown),
[] ).
cnf(429,axiom,
( equal(op(e0,e0),e1)
| equal(op(e1,e1),e1)
| equal(op(e2,e2),e1)
| equal(op(e3,e3),e1)
| equal(op(e4,e4),e1) ),
file('ALG062+1.p',unknown),
[] ).
cnf(430,axiom,
( equal(op(e0,e0),e0)
| equal(op(e1,e1),e0)
| equal(op(e2,e2),e0)
| equal(op(e3,e3),e0)
| equal(op(e4,e4),e0) ),
file('ALG062+1.p',unknown),
[] ).
cnf(431,plain,
~ equal(op(e1,e4),e4),
inference(rew,[status(thm),theory(equality)],[21,88]),
[iquote('0:Rew:21.0,88.0')] ).
cnf(432,plain,
~ equal(op(e1,e3),e4),
inference(rew,[status(thm),theory(equality)],[21,87]),
[iquote('0:Rew:21.0,87.0')] ).
cnf(436,plain,
~ equal(op(e3,e1),e4),
inference(rew,[status(thm),theory(equality)],[21,37]),
[iquote('0:Rew:21.0,37.0')] ).
cnf(437,plain,
~ equal(op(e2,e1),e4),
inference(rew,[status(thm),theory(equality)],[21,36]),
[iquote('0:Rew:21.0,36.0')] ).
cnf(439,plain,
equal(op(e4,e4),e2),
inference(rew,[status(thm),theory(equality)],[21,122]),
[iquote('0:Rew:21.0,122.0')] ).
cnf(441,plain,
~ equal(op(e4,e2),e2),
inference(rew,[status(thm),theory(equality)],[439,120]),
[iquote('0:Rew:439.0,120.0')] ).
cnf(442,plain,
~ equal(op(e4,e1),e2),
inference(rew,[status(thm),theory(equality)],[439,118]),
[iquote('0:Rew:439.0,118.0')] ).
cnf(443,plain,
~ equal(op(e4,e0),e2),
inference(rew,[status(thm),theory(equality)],[439,115]),
[iquote('0:Rew:439.0,115.0')] ).
cnf(446,plain,
~ equal(op(e1,e4),e2),
inference(rew,[status(thm),theory(equality)],[439,68]),
[iquote('0:Rew:439.0,68.0')] ).
cnf(447,plain,
~ equal(op(e0,e4),e2),
inference(rew,[status(thm),theory(equality)],[439,65]),
[iquote('0:Rew:439.0,65.0')] ).
cnf(448,plain,
equal(op(e1,e2),e0),
inference(rew,[status(thm),theory(equality)],[439,123,21]),
[iquote('0:Rew:439.0,123.0,21.0,123.0')] ).
cnf(449,plain,
~ equal(op(e1,e4),e0),
inference(rew,[status(thm),theory(equality)],[448,90]),
[iquote('0:Rew:448.0,90.0')] ).
cnf(453,plain,
~ equal(op(e4,e2),e0),
inference(rew,[status(thm),theory(equality)],[448,48]),
[iquote('0:Rew:448.0,48.0')] ).
cnf(460,plain,
( ~ equal(e2,unit)
| ~ equal(e2,e2)
| ~ skC2 ),
inference(rew,[status(thm),theory(equality)],[439,198]),
[iquote('0:Rew:439.0,198.1')] ).
cnf(461,plain,
( ~ skC2
| ~ equal(e2,unit) ),
inference(obv,[status(thm),theory(equality)],[460]),
[iquote('0:Obv:460.1')] ).
cnf(466,plain,
( ~ equal(e0,unit)
| ~ equal(e0,e0)
| ~ skC0 ),
inference(rew,[status(thm),theory(equality)],[448,131]),
[iquote('0:Rew:448.0,131.1')] ).
cnf(467,plain,
( ~ skC0
| ~ equal(e0,unit) ),
inference(obv,[status(thm),theory(equality)],[466]),
[iquote('0:Obv:466.1')] ).
cnf(474,plain,
( ~ equal(e2,e2)
| ~ skC2
| equal(op(e4,e2),e4) ),
inference(rew,[status(thm),theory(equality)],[439,283]),
[iquote('0:Rew:439.0,283.0')] ).
cnf(475,plain,
( ~ skC2
| equal(op(e4,e2),e4) ),
inference(obv,[status(thm),theory(equality)],[474]),
[iquote('0:Obv:474.0')] ).
cnf(483,plain,
( ~ skC1
| ~ equal(op(e4,e2),e1) ),
inference(mrr,[status(thm)],[261,442]),
[iquote('0:MRR:261.2,442.0')] ).
cnf(484,plain,
( ~ skC1
| ~ equal(op(e3,e4),e1) ),
inference(mrr,[status(thm)],[259,436]),
[iquote('0:MRR:259.2,436.0')] ).
cnf(493,plain,
( ~ equal(e0,e0)
| ~ skC0
| equal(op(e1,e0),e2) ),
inference(rew,[status(thm),theory(equality)],[448,229]),
[iquote('0:Rew:448.0,229.0')] ).
cnf(494,plain,
( ~ skC0
| equal(op(e1,e0),e2) ),
inference(obv,[status(thm),theory(equality)],[493]),
[iquote('0:Obv:493.0')] ).
cnf(507,plain,
( ~ equal(e4,e4)
| equal(op(e1,e4),e1)
| skC0
| skC1
| skC2
| skC3 ),
inference(rew,[status(thm),theory(equality)],[21,334]),
[iquote('0:Rew:21.0,334.0')] ).
cnf(508,plain,
( skC3
| skC2
| skC1
| skC0
| equal(op(e1,e4),e1) ),
inference(obv,[status(thm),theory(equality)],[507]),
[iquote('0:Obv:507.0')] ).
cnf(510,plain,
equal(op(e2,e2),e3),
inference(rew,[status(thm),theory(equality)],[439,350,21]),
[iquote('0:Rew:439.0,350.0,21.0,350.0')] ).
cnf(511,plain,
~ equal(op(e2,e4),e3),
inference(rew,[status(thm),theory(equality)],[510,100]),
[iquote('0:Rew:510.0,100.0')] ).
cnf(512,plain,
~ equal(op(e2,e3),e3),
inference(rew,[status(thm),theory(equality)],[510,99]),
[iquote('0:Rew:510.0,99.0')] ).
cnf(513,plain,
~ equal(op(e2,e1),e3),
inference(rew,[status(thm),theory(equality)],[510,96]),
[iquote('0:Rew:510.0,96.0')] ).
cnf(514,plain,
~ equal(op(e2,e0),e3),
inference(rew,[status(thm),theory(equality)],[510,93]),
[iquote('0:Rew:510.0,93.0')] ).
cnf(515,plain,
~ equal(op(e4,e2),e3),
inference(rew,[status(thm),theory(equality)],[510,50]),
[iquote('0:Rew:510.0,50.0')] ).
cnf(519,plain,
( ~ equal(e3,e3)
| ~ skC3
| equal(op(e2,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[510,294]),
[iquote('0:Rew:510.0,294.0')] ).
cnf(522,plain,
( ~ equal(op(e2,e1),e2)
| ~ skC2
| equal(e3,e1) ),
inference(rew,[status(thm),theory(equality)],[510,273]),
[iquote('0:Rew:510.0,273.2')] ).
cnf(525,plain,
( ~ equal(op(e2,e3),e4)
| skC3
| skC2
| skC1
| skC0 ),
inference(mrr,[status(thm)],[340,511]),
[iquote('0:MRR:340.1,511.0')] ).
cnf(531,plain,
( ~ skC3
| equal(op(e2,e3),e2) ),
inference(obv,[status(thm),theory(equality)],[519]),
[iquote('0:Obv:519.0')] ).
cnf(532,plain,
( ~ skC2
| ~ equal(op(e2,e1),e2) ),
inference(mrr,[status(thm)],[522,6]),
[iquote('0:MRR:522.2,6.0')] ).
cnf(539,plain,
( equal(op(e4,e0),e3)
| equal(op(e4,e1),e3)
| equal(op(e4,e2),e3)
| equal(op(e4,e3),e3)
| equal(e3,e2) ),
inference(rew,[status(thm),theory(equality)],[439,354]),
[iquote('0:Rew:439.0,354.4')] ).
cnf(540,plain,
( equal(op(e4,e3),e3)
| equal(op(e4,e1),e3)
| equal(op(e4,e0),e3) ),
inference(mrr,[status(thm)],[539,515,8]),
[iquote('0:MRR:539.2,539.4,515.0,8.0')] ).
cnf(547,plain,
( equal(op(e4,e0),e0)
| equal(op(e4,e1),e0)
| equal(op(e4,e2),e0)
| equal(op(e4,e3),e0)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[439,360]),
[iquote('0:Rew:439.0,360.4')] ).
cnf(548,plain,
( equal(op(e4,e0),e0)
| equal(op(e4,e3),e0)
| equal(op(e4,e1),e0) ),
inference(mrr,[status(thm)],[547,453,2]),
[iquote('0:MRR:547.2,547.4,453.0,2.0')] ).
cnf(549,plain,
( equal(op(e4,e3),e4)
| equal(op(e3,e3),e4)
| equal(op(e2,e3),e4)
| equal(op(e0,e3),e4) ),
inference(mrr,[status(thm)],[361,432]),
[iquote('0:MRR:361.1,432.0')] ).
cnf(557,plain,
( equal(op(e0,e2),e4)
| equal(e4,e0)
| equal(e4,e3)
| equal(op(e3,e2),e4)
| equal(op(e4,e2),e4) ),
inference(rew,[status(thm),theory(equality)],[510,371,448]),
[iquote('0:Rew:510.0,371.2,448.0,371.1')] ).
cnf(558,plain,
( equal(op(e4,e2),e4)
| equal(op(e3,e2),e4)
| equal(op(e0,e2),e4) ),
inference(mrr,[status(thm)],[557,4,10]),
[iquote('0:MRR:557.1,557.2,4.0,10.0')] ).
cnf(559,plain,
( equal(op(e2,e0),e4)
| equal(op(e2,e1),e4)
| equal(e4,e3)
| equal(op(e2,e3),e4)
| equal(op(e2,e4),e4) ),
inference(rew,[status(thm),theory(equality)],[510,372]),
[iquote('0:Rew:510.0,372.2')] ).
cnf(560,plain,
( equal(op(e2,e4),e4)
| equal(op(e2,e3),e4)
| equal(op(e2,e0),e4) ),
inference(mrr,[status(thm)],[559,437,10]),
[iquote('0:MRR:559.1,559.2,437.0,10.0')] ).
cnf(561,plain,
( equal(op(e0,e2),e2)
| equal(e2,e0)
| equal(e3,e2)
| equal(op(e3,e2),e2)
| equal(op(e4,e2),e2) ),
inference(rew,[status(thm),theory(equality)],[510,375,448]),
[iquote('0:Rew:510.0,375.2,448.0,375.1')] ).
cnf(562,plain,
( equal(op(e3,e2),e2)
| equal(op(e0,e2),e2) ),
inference(mrr,[status(thm)],[561,2,8,441]),
[iquote('0:MRR:561.1,561.2,561.4,2.0,8.0,441.0')] ).
cnf(567,plain,
( equal(op(e2,e0),e1)
| equal(op(e2,e1),e1)
| equal(e3,e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[510,378]),
[iquote('0:Rew:510.0,378.2')] ).
cnf(568,plain,
( equal(op(e2,e1),e1)
| equal(op(e2,e4),e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[567,6]),
[iquote('0:MRR:567.2,6.0')] ).
cnf(571,plain,
( equal(op(e0,e1),e3)
| equal(e4,e3)
| equal(op(e2,e1),e3)
| equal(op(e3,e1),e3)
| equal(op(e4,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[21,383]),
[iquote('0:Rew:21.0,383.1')] ).
cnf(572,plain,
( equal(op(e3,e1),e3)
| equal(op(e4,e1),e3)
| equal(op(e0,e1),e3) ),
inference(mrr,[status(thm)],[571,10,513]),
[iquote('0:MRR:571.1,571.2,10.0,513.0')] ).
cnf(575,plain,
( equal(op(e0,e1),e2)
| equal(e4,e2)
| equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(e4,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[21,385]),
[iquote('0:Rew:21.0,385.1')] ).
cnf(576,plain,
( equal(op(e2,e1),e2)
| equal(op(e3,e1),e2)
| equal(op(e0,e1),e2) ),
inference(mrr,[status(thm)],[575,9,442]),
[iquote('0:MRR:575.1,575.4,9.0,442.0')] ).
cnf(589,plain,
( equal(op(e2,e0),e2)
| equal(op(e0,e0),e2)
| equal(op(e3,e0),e2)
| equal(op(e1,e0),e2) ),
inference(mrr,[status(thm)],[395,443]),
[iquote('0:MRR:395.4,443.0')] ).
cnf(594,plain,
( equal(op(e4,e2),e4)
| equal(op(e4,e2),e1) ),
inference(mrr,[status(thm)],[403,453,441,515]),
[iquote('0:MRR:403.0,403.2,403.3,453.0,441.0,515.0')] ).
cnf(601,plain,
( equal(op(e2,e3),e2)
| equal(op(e2,e3),e4)
| equal(op(e2,e3),e1)
| equal(op(e2,e3),e0) ),
inference(mrr,[status(thm)],[412,512]),
[iquote('0:MRR:412.3,512.0')] ).
cnf(603,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e0)
| equal(op(e2,e0),e4)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[415,514]),
[iquote('0:MRR:415.3,514.0')] ).
cnf(604,plain,
( equal(op(e1,e4),e1)
| equal(op(e1,e4),e3) ),
inference(mrr,[status(thm)],[416,449,446,431]),
[iquote('0:MRR:416.0,416.2,416.4,449.0,446.0,431.0')] ).
cnf(607,plain,
( equal(op(e0,e4),e4)
| equal(op(e0,e4),e0)
| equal(op(e0,e4),e3)
| equal(op(e0,e4),e1) ),
inference(mrr,[status(thm)],[421,447]),
[iquote('0:MRR:421.2,447.0')] ).
cnf(610,plain,
( equal(op(e0,e0),e1)
| equal(e4,e1)
| equal(e3,e1)
| equal(op(e3,e3),e1)
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[439,429,510,21]),
[iquote('0:Rew:439.0,429.4,510.0,429.2,21.0,429.1')] ).
cnf(611,plain,
( equal(op(e3,e3),e1)
| equal(op(e0,e0),e1) ),
inference(mrr,[status(thm)],[610,7,6,5]),
[iquote('0:MRR:610.1,610.2,610.4,7.0,6.0,5.0')] ).
cnf(612,plain,
( equal(op(e0,e0),e0)
| equal(e4,e0)
| equal(e3,e0)
| equal(op(e3,e3),e0)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[439,430,510,21]),
[iquote('0:Rew:439.0,430.4,510.0,430.2,21.0,430.1')] ).
cnf(613,plain,
( equal(op(e0,e0),e0)
| equal(op(e3,e3),e0) ),
inference(mrr,[status(thm)],[612,4,3,2]),
[iquote('0:MRR:612.1,612.2,612.4,4.0,3.0,2.0')] ).
cnf(614,plain,
equal(e0,unit),
inference(spt,[spt(split,[position(s1)])],[349]),
[iquote('1:Spt:349.4')] ).
cnf(617,plain,
( equal(op(e4,e3),e3)
| equal(op(e4,e1),e3)
| equal(op(e4,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[614,540]),
[iquote('1:Rew:614.0,540.2')] ).
cnf(630,plain,
~ equal(op(e4,e2),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[614,113]),
[iquote('1:Rew:614.0,113.0')] ).
cnf(663,plain,
~ equal(op(e2,e3),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[614,94]),
[iquote('1:Rew:614.0,94.0')] ).
cnf(695,plain,
~ equal(op(e4,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[614,55]),
[iquote('1:Rew:614.0,55.0')] ).
cnf(740,plain,
( equal(op(e3,e3),e1)
| equal(op(unit,unit),e1) ),
inference(rew,[status(thm),theory(equality)],[614,611]),
[iquote('1:Rew:614.0,611.1')] ).
cnf(752,plain,
( ~ skC0
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[614,467]),
[iquote('1:Rew:614.0,467.1')] ).
cnf(755,plain,
( equal(op(e4,e0),e0)
| equal(op(e4,e3),unit)
| equal(op(e4,e1),e0) ),
inference(rew,[status(thm),theory(equality)],[614,548]),
[iquote('1:Rew:614.0,548.1')] ).
cnf(768,plain,
( equal(op(e2,e3),e2)
| equal(op(e2,e3),e4)
| equal(op(e2,e3),e1)
| equal(op(e2,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[614,601]),
[iquote('1:Rew:614.0,601.3')] ).
cnf(771,plain,
~ equal(e4,unit),
inference(rew,[status(thm),theory(equality)],[614,4]),
[iquote('1:Rew:614.0,4.0')] ).
cnf(772,plain,
~ equal(e3,unit),
inference(rew,[status(thm),theory(equality)],[614,3]),
[iquote('1:Rew:614.0,3.0')] ).
cnf(774,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[614,1]),
[iquote('1:Rew:614.0,1.0')] ).
cnf(775,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[614,12]),
[iquote('1:Rew:614.0,12.0')] ).
cnf(790,plain,
~ skC0,
inference(obv,[status(thm),theory(equality)],[752]),
[iquote('1:Obv:752.1')] ).
cnf(794,plain,
( ~ equal(op(e2,e3),e4)
| skC3
| skC2
| skC1 ),
inference(mrr,[status(thm)],[525,790]),
[iquote('1:MRR:525.4,790.0')] ).
cnf(799,plain,
~ equal(op(e4,e2),e4),
inference(rew,[status(thm),theory(equality)],[20,630]),
[iquote('1:Rew:20.0,630.0')] ).
cnf(800,plain,
~ skC2,
inference(mrr,[status(thm)],[475,799]),
[iquote('1:MRR:475.1,799.0')] ).
cnf(801,plain,
equal(op(e4,e2),e1),
inference(mrr,[status(thm)],[594,799]),
[iquote('1:MRR:594.0,799.0')] ).
cnf(802,plain,
( ~ skC1
| ~ equal(e1,e1) ),
inference(rew,[status(thm),theory(equality)],[801,483]),
[iquote('1:Rew:801.0,483.1')] ).
cnf(810,plain,
~ skC1,
inference(obv,[status(thm),theory(equality)],[802]),
[iquote('1:Obv:802.1')] ).
cnf(820,plain,
~ equal(op(e2,e3),e2),
inference(rew,[status(thm),theory(equality)],[16,663]),
[iquote('1:Rew:16.0,663.0')] ).
cnf(821,plain,
~ skC3,
inference(mrr,[status(thm)],[531,820]),
[iquote('1:MRR:531.1,820.0')] ).
cnf(839,plain,
~ equal(op(e4,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,695]),
[iquote('1:Rew:17.0,695.0')] ).
cnf(868,plain,
~ equal(op(e2,e3),e4),
inference(mrr,[status(thm)],[794,821,800,810]),
[iquote('1:MRR:794.1,794.2,794.3,821.0,800.0,810.0')] ).
cnf(882,plain,
( equal(op(e3,e3),e1)
| equal(e1,unit) ),
inference(rew,[status(thm),theory(equality)],[775,740]),
[iquote('1:Rew:775.0,740.1')] ).
cnf(883,plain,
equal(op(e3,e3),e1),
inference(mrr,[status(thm)],[882,774]),
[iquote('1:MRR:882.1,774.0')] ).
cnf(888,plain,
~ equal(op(e2,e3),e1),
inference(rew,[status(thm),theory(equality)],[883,59]),
[iquote('1:Rew:883.0,59.0')] ).
cnf(894,plain,
( equal(op(e4,e3),e3)
| equal(op(e4,e1),e3)
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[20,617]),
[iquote('1:Rew:20.0,617.2')] ).
cnf(895,plain,
equal(op(e4,e1),e3),
inference(mrr,[status(thm)],[894,839,10]),
[iquote('1:MRR:894.0,894.2,839.0,10.0')] ).
cnf(920,plain,
( equal(e4,unit)
| equal(op(e4,e3),unit)
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[895,755,614,20]),
[iquote('1:Rew:895.0,755.2,614.0,755.2,20.0,755.0,614.0,755.0')] ).
cnf(921,plain,
equal(op(e4,e3),unit),
inference(mrr,[status(thm)],[920,771,772]),
[iquote('1:MRR:920.0,920.2,771.0,772.0')] ).
cnf(923,plain,
~ equal(op(e2,e3),unit),
inference(rew,[status(thm),theory(equality)],[921,60]),
[iquote('1:Rew:921.0,60.0')] ).
cnf(963,plain,
$false,
inference(mrr,[status(thm)],[768,820,868,888,923]),
[iquote('1:MRR:768.0,768.1,768.2,768.3,820.0,868.0,888.0,923.0')] ).
cnf(969,plain,
~ equal(e0,unit),
inference(spt,[spt(split,[position(sa)])],[963,614]),
[iquote('1:Spt:963.0,349.4,614.0')] ).
cnf(970,plain,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2)])],[349]),
[iquote('1:Spt:963.0,349.0,349.1,349.2,349.3')] ).
cnf(971,plain,
equal(e4,unit),
inference(spt,[spt(split,[position(s2s1)])],[970]),
[iquote('2:Spt:970.0')] ).
cnf(973,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[971,9]),
[iquote('2:Rew:971.0,9.0')] ).
cnf(974,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[971,7]),
[iquote('2:Rew:971.0,7.0')] ).
cnf(983,plain,
~ equal(op(e0,e2),op(unit,e2)),
inference(rew,[status(thm),theory(equality)],[971,45]),
[iquote('2:Rew:971.0,45.0')] ).
cnf(1003,plain,
~ equal(op(e0,e0),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[971,75]),
[iquote('2:Rew:971.0,75.0')] ).
cnf(1042,plain,
~ equal(op(e2,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[971,40]),
[iquote('2:Rew:971.0,40.0')] ).
cnf(1069,plain,
~ equal(op(e3,e0),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[971,105]),
[iquote('2:Rew:971.0,105.0')] ).
cnf(1087,plain,
( equal(op(e2,e1),e1)
| equal(op(e2,unit),e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[971,568]),
[iquote('2:Rew:971.0,568.1')] ).
cnf(1108,plain,
( equal(op(e2,e4),e4)
| equal(op(e2,e3),unit)
| equal(op(e2,e0),e4) ),
inference(rew,[status(thm),theory(equality)],[971,560]),
[iquote('2:Rew:971.0,560.1')] ).
cnf(1117,plain,
( equal(op(e3,e0),e3)
| equal(op(e3,e0),e0)
| equal(op(e3,e0),unit)
| equal(op(e3,e0),e2)
| equal(op(e3,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[971,410]),
[iquote('2:Rew:971.0,410.2')] ).
cnf(1140,plain,
~ equal(op(e0,e2),e2),
inference(rew,[status(thm),theory(equality)],[15,983]),
[iquote('2:Rew:15.0,983.0')] ).
cnf(1141,plain,
equal(op(e3,e2),e2),
inference(mrr,[status(thm)],[562,1140]),
[iquote('2:MRR:562.1,1140.0')] ).
cnf(1146,plain,
~ equal(op(e3,e0),e2),
inference(rew,[status(thm),theory(equality)],[1141,103]),
[iquote('2:Rew:1141.0,103.0')] ).
cnf(1162,plain,
~ equal(op(e0,e0),e0),
inference(rew,[status(thm),theory(equality)],[12,1003]),
[iquote('2:Rew:12.0,1003.0')] ).
cnf(1163,plain,
equal(op(e3,e3),e0),
inference(mrr,[status(thm)],[613,1162]),
[iquote('2:MRR:613.0,1162.0')] ).
cnf(1165,plain,
~ equal(op(e3,e0),e0),
inference(rew,[status(thm),theory(equality)],[1163,104]),
[iquote('2:Rew:1163.0,104.0')] ).
cnf(1172,plain,
( equal(e1,e0)
| equal(op(e0,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1163,611]),
[iquote('2:Rew:1163.0,611.0')] ).
cnf(1191,plain,
~ equal(op(e2,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1042]),
[iquote('2:Rew:13.0,1042.0')] ).
cnf(1202,plain,
~ equal(op(e3,e0),e3),
inference(rew,[status(thm),theory(equality)],[18,1069]),
[iquote('2:Rew:18.0,1069.0')] ).
cnf(1219,plain,
equal(op(e0,e0),e1),
inference(mrr,[status(thm)],[1172,1]),
[iquote('2:MRR:1172.0,1.0')] ).
cnf(1221,plain,
~ equal(op(e2,e0),e1),
inference(rew,[status(thm),theory(equality)],[1219,23]),
[iquote('2:Rew:1219.0,23.0')] ).
cnf(1222,plain,
~ equal(op(e3,e0),e1),
inference(rew,[status(thm),theory(equality)],[1219,24]),
[iquote('2:Rew:1219.0,24.0')] ).
cnf(1283,plain,
( equal(e2,unit)
| equal(op(e2,e3),unit)
| equal(op(e2,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[971,1108,16]),
[iquote('2:Rew:971.0,1108.2,16.0,1108.0,971.0,1108.0')] ).
cnf(1284,plain,
( equal(op(e2,e3),unit)
| equal(op(e2,e0),unit) ),
inference(mrr,[status(thm)],[1283,973]),
[iquote('2:MRR:1283.0,973.0')] ).
cnf(1300,plain,
( equal(op(e2,e1),e1)
| equal(e2,e1)
| equal(op(e2,e3),e1)
| equal(op(e2,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[16,1087]),
[iquote('2:Rew:16.0,1087.1')] ).
cnf(1301,plain,
equal(op(e2,e3),e1),
inference(mrr,[status(thm)],[1300,1191,5,1221]),
[iquote('2:MRR:1300.0,1300.1,1300.3,1191.0,5.0,1221.0')] ).
cnf(1309,plain,
( equal(e1,unit)
| equal(op(e2,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[1301,1284]),
[iquote('2:Rew:1301.0,1284.0')] ).
cnf(1310,plain,
equal(op(e2,e0),unit),
inference(mrr,[status(thm)],[1309,974]),
[iquote('2:MRR:1309.0,974.0')] ).
cnf(1312,plain,
~ equal(op(e3,e0),unit),
inference(rew,[status(thm),theory(equality)],[1310,29]),
[iquote('2:Rew:1310.0,29.0')] ).
cnf(1327,plain,
$false,
inference(mrr,[status(thm)],[1117,1202,1165,1312,1146,1222]),
[iquote('2:MRR:1117.0,1117.1,1117.2,1117.3,1117.4,1202.0,1165.0,1312.0,1146.0,1222.0')] ).
cnf(1328,plain,
~ equal(e4,unit),
inference(spt,[spt(split,[position(s2sa)])],[1327,971]),
[iquote('2:Spt:1327.0,970.0,971.0')] ).
cnf(1329,plain,
( equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2s2)])],[970]),
[iquote('2:Spt:1327.0,970.1,970.2,970.3')] ).
cnf(1330,plain,
equal(e3,unit),
inference(spt,[spt(split,[position(s2s2s1)])],[1329]),
[iquote('3:Spt:1329.0')] ).
cnf(1332,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[1330,6]),
[iquote('3:Rew:1330.0,6.0')] ).
cnf(1333,plain,
equal(op(unit,unit),unit),
inference(rew,[status(thm),theory(equality)],[1330,18]),
[iquote('3:Rew:1330.0,18.0')] ).
cnf(1339,plain,
~ equal(op(e1,e4),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[1330,91]),
[iquote('3:Rew:1330.0,91.0')] ).
cnf(1381,plain,
~ equal(op(e0,e4),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[1330,81]),
[iquote('3:Rew:1330.0,81.0')] ).
cnf(1410,plain,
~ equal(op(e0,e4),op(unit,e4)),
inference(rew,[status(thm),theory(equality)],[1330,64]),
[iquote('3:Rew:1330.0,64.0')] ).
cnf(1478,plain,
( equal(op(unit,unit),e1)
| equal(op(e0,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1330,611]),
[iquote('3:Rew:1330.0,611.0')] ).
cnf(1483,plain,
( equal(op(e1,e4),e1)
| equal(op(e1,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[1330,604]),
[iquote('3:Rew:1330.0,604.1')] ).
cnf(1494,plain,
( equal(op(e0,e4),e4)
| equal(op(e0,e4),e0)
| equal(op(e0,e4),unit)
| equal(op(e0,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[1330,607]),
[iquote('3:Rew:1330.0,607.2')] ).
cnf(1512,plain,
~ equal(op(e1,e4),e1),
inference(rew,[status(thm),theory(equality)],[14,1339]),
[iquote('3:Rew:14.0,1339.0')] ).
cnf(1529,plain,
~ equal(op(e0,e4),e0),
inference(rew,[status(thm),theory(equality)],[12,1381]),
[iquote('3:Rew:12.0,1381.0')] ).
cnf(1539,plain,
~ equal(op(e0,e4),e4),
inference(rew,[status(thm),theory(equality)],[19,1410]),
[iquote('3:Rew:19.0,1410.0')] ).
cnf(1590,plain,
( equal(e1,unit)
| equal(op(e0,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1333,1478]),
[iquote('3:Rew:1333.0,1478.0')] ).
cnf(1591,plain,
equal(op(e0,e0),e1),
inference(mrr,[status(thm)],[1590,1332]),
[iquote('3:MRR:1590.0,1332.0')] ).
cnf(1593,plain,
~ equal(op(e0,e4),e1),
inference(rew,[status(thm),theory(equality)],[1591,75]),
[iquote('3:Rew:1591.0,75.0')] ).
cnf(1599,plain,
equal(op(e1,e4),unit),
inference(mrr,[status(thm)],[1483,1512]),
[iquote('3:MRR:1483.0,1512.0')] ).
cnf(1604,plain,
~ equal(op(e0,e4),unit),
inference(rew,[status(thm),theory(equality)],[1599,62]),
[iquote('3:Rew:1599.0,62.0')] ).
cnf(1680,plain,
$false,
inference(mrr,[status(thm)],[1494,1539,1529,1604,1593]),
[iquote('3:MRR:1494.0,1494.1,1494.2,1494.3,1539.0,1529.0,1604.0,1593.0')] ).
cnf(1685,plain,
~ equal(e3,unit),
inference(spt,[spt(split,[position(s2s2sa)])],[1680,1330]),
[iquote('3:Spt:1680.0,1329.0,1330.0')] ).
cnf(1686,plain,
( equal(e2,unit)
| equal(e1,unit) ),
inference(spt,[spt(split,[position(s2s2s2)])],[1329]),
[iquote('3:Spt:1680.0,1329.1,1329.2')] ).
cnf(1687,plain,
equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2s1)])],[1686]),
[iquote('4:Spt:1686.0')] ).
cnf(1688,plain,
~ equal(e1,unit),
inference(rew,[status(thm),theory(equality)],[1687,5]),
[iquote('4:Rew:1687.0,5.0')] ).
cnf(1700,plain,
~ equal(op(e3,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1687,29]),
[iquote('4:Rew:1687.0,29.0')] ).
cnf(1702,plain,
~ equal(op(e0,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1687,23]),
[iquote('4:Rew:1687.0,23.0')] ).
cnf(1703,plain,
~ equal(op(e4,e0),op(unit,e0)),
inference(rew,[status(thm),theory(equality)],[1687,30]),
[iquote('4:Rew:1687.0,30.0')] ).
cnf(1733,plain,
~ equal(op(e0,e1),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[1687,76]),
[iquote('4:Rew:1687.0,76.0')] ).
cnf(1748,plain,
~ equal(op(e3,e0),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[1687,103]),
[iquote('4:Rew:1687.0,103.0')] ).
cnf(1749,plain,
~ equal(op(e3,e1),op(e3,unit)),
inference(rew,[status(thm),theory(equality)],[1687,106]),
[iquote('4:Rew:1687.0,106.0')] ).
cnf(1795,plain,
( ~ skC2
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[1687,461]),
[iquote('4:Rew:1687.0,461.1')] ).
cnf(1802,plain,
( ~ skC3
| equal(op(unit,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[1687,531]),
[iquote('4:Rew:1687.0,531.1')] ).
cnf(1813,plain,
( equal(op(e3,e0),e3)
| equal(op(e3,e0),e0)
| equal(op(e3,e0),e4)
| equal(op(e3,e0),unit)
| equal(op(e3,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1687,410]),
[iquote('4:Rew:1687.0,410.3')] ).
cnf(1820,plain,
( equal(op(unit,e1),unit)
| equal(op(e3,e1),e2)
| equal(op(e0,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[1687,576]),
[iquote('4:Rew:1687.0,576.0')] ).
cnf(1843,plain,
~ skC2,
inference(obv,[status(thm),theory(equality)],[1795]),
[iquote('4:Obv:1795.1')] ).
cnf(1849,plain,
( ~ equal(op(e3,e0),e4)
| skC3
| skC1
| skC0
| equal(op(e3,e4),e0) ),
inference(mrr,[status(thm)],[341,1843]),
[iquote('4:MRR:341.2,1843.0')] ).
cnf(1853,plain,
( ~ skC3
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[17,1802]),
[iquote('4:Rew:17.0,1802.1')] ).
cnf(1854,plain,
~ skC3,
inference(mrr,[status(thm)],[1853,1685]),
[iquote('4:MRR:1853.1,1685.0')] ).
cnf(1855,plain,
~ equal(op(e3,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1700]),
[iquote('4:Rew:11.0,1700.0')] ).
cnf(1858,plain,
~ equal(op(e0,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1702]),
[iquote('4:Rew:11.0,1702.0')] ).
cnf(1859,plain,
equal(op(e3,e3),e0),
inference(mrr,[status(thm)],[613,1858]),
[iquote('4:MRR:613.0,1858.0')] ).
cnf(1865,plain,
~ equal(op(e4,e3),e0),
inference(rew,[status(thm),theory(equality)],[1859,61]),
[iquote('4:Rew:1859.0,61.0')] ).
cnf(1866,plain,
~ equal(op(e3,e4),e0),
inference(rew,[status(thm),theory(equality)],[1859,111]),
[iquote('4:Rew:1859.0,111.0')] ).
cnf(1868,plain,
( equal(e1,e0)
| equal(op(e0,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1859,611]),
[iquote('4:Rew:1859.0,611.0')] ).
cnf(1873,plain,
( equal(op(e4,e0),e0)
| equal(op(e4,e1),e0) ),
inference(mrr,[status(thm)],[548,1865]),
[iquote('4:MRR:548.1,1865.0')] ).
cnf(1876,plain,
~ equal(op(e4,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,1703]),
[iquote('4:Rew:11.0,1703.0')] ).
cnf(1890,plain,
~ equal(op(e0,e1),e0),
inference(rew,[status(thm),theory(equality)],[12,1733]),
[iquote('4:Rew:12.0,1733.0')] ).
cnf(1891,plain,
( ~ skC1
| ~ equal(op(e0,e0),e1) ),
inference(mrr,[status(thm)],[244,1890]),
[iquote('4:MRR:244.2,1890.0')] ).
cnf(1896,plain,
~ equal(op(e3,e0),e3),
inference(rew,[status(thm),theory(equality)],[18,1748]),
[iquote('4:Rew:18.0,1748.0')] ).
cnf(1898,plain,
~ equal(op(e3,e1),e3),
inference(rew,[status(thm),theory(equality)],[18,1749]),
[iquote('4:Rew:18.0,1749.0')] ).
cnf(1899,plain,
( equal(op(e4,e1),e3)
| equal(op(e0,e1),e3) ),
inference(mrr,[status(thm)],[572,1898]),
[iquote('4:MRR:572.0,1898.0')] ).
cnf(1922,plain,
equal(op(e0,e0),e1),
inference(mrr,[status(thm)],[1868,1]),
[iquote('4:MRR:1868.0,1.0')] ).
cnf(1924,plain,
~ equal(op(e3,e0),e1),
inference(rew,[status(thm),theory(equality)],[1922,24]),
[iquote('4:Rew:1922.0,24.0')] ).
cnf(1928,plain,
~ equal(op(e4,e0),e1),
inference(rew,[status(thm),theory(equality)],[1922,25]),
[iquote('4:Rew:1922.0,25.0')] ).
cnf(1931,plain,
( ~ skC0
| ~ equal(op(e4,e1),e0) ),
inference(mrr,[status(thm)],[240,1928]),
[iquote('4:MRR:240.2,1928.0')] ).
cnf(1932,plain,
( ~ skC1
| ~ equal(e1,e1) ),
inference(rew,[status(thm),theory(equality)],[1922,1891]),
[iquote('4:Rew:1922.0,1891.1')] ).
cnf(1933,plain,
~ skC1,
inference(obv,[status(thm),theory(equality)],[1932]),
[iquote('4:Obv:1932.1')] ).
cnf(1941,plain,
equal(op(e4,e1),e0),
inference(mrr,[status(thm)],[1873,1876]),
[iquote('4:MRR:1873.0,1876.0')] ).
cnf(1949,plain,
( ~ skC0
| ~ equal(e0,e0) ),
inference(rew,[status(thm),theory(equality)],[1941,1931]),
[iquote('4:Rew:1941.0,1931.1')] ).
cnf(1950,plain,
~ skC0,
inference(obv,[status(thm),theory(equality)],[1949]),
[iquote('4:Obv:1949.1')] ).
cnf(1977,plain,
( equal(e3,e0)
| equal(op(e0,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[1941,1899]),
[iquote('4:Rew:1941.0,1899.0')] ).
cnf(1978,plain,
equal(op(e0,e1),e3),
inference(mrr,[status(thm)],[1977,3]),
[iquote('4:MRR:1977.0,3.0')] ).
cnf(1990,plain,
~ equal(op(e3,e0),e4),
inference(mrr,[status(thm)],[1849,1854,1933,1950,1866]),
[iquote('4:MRR:1849.1,1849.2,1849.3,1849.4,1854.0,1933.0,1950.0,1866.0')] ).
cnf(2006,plain,
( equal(e1,unit)
| equal(op(e3,e1),unit)
| equal(e3,unit) ),
inference(rew,[status(thm),theory(equality)],[1978,1820,1687,13]),
[iquote('4:Rew:1978.0,1820.2,1687.0,1820.2,1687.0,1820.1,13.0,1820.0')] ).
cnf(2007,plain,
equal(op(e3,e1),unit),
inference(mrr,[status(thm)],[2006,1688,1685]),
[iquote('4:MRR:2006.0,2006.2,1688.0,1685.0')] ).
cnf(2010,plain,
~ equal(op(e3,e0),unit),
inference(rew,[status(thm),theory(equality)],[2007,102]),
[iquote('4:Rew:2007.0,102.0')] ).
cnf(2051,plain,
$false,
inference(mrr,[status(thm)],[1813,1896,1855,1990,2010,1924]),
[iquote('4:MRR:1813.0,1813.1,1813.2,1813.3,1813.4,1896.0,1855.0,1990.0,2010.0,1924.0')] ).
cnf(2052,plain,
~ equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2sa)])],[2051,1687]),
[iquote('4:Spt:2051.0,1686.0,1687.0')] ).
cnf(2053,plain,
equal(e1,unit),
inference(spt,[spt(split,[position(s2s2s2s2)])],[1686]),
[iquote('4:Spt:2051.0,1686.1')] ).
cnf(2060,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[2053,5]),
[iquote('4:Rew:2053.0,5.0')] ).
cnf(2082,plain,
( ~ skC0
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[11,494,2053]),
[iquote('4:Rew:11.0,494.1,2053.0,494.1')] ).
cnf(2083,plain,
~ skC0,
inference(mrr,[status(thm)],[2082,2]),
[iquote('4:MRR:2082.1,2.0')] ).
cnf(2084,plain,
( ~ skC2
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[16,532,2053]),
[iquote('4:Rew:16.0,532.1,2053.0,532.1')] ).
cnf(2085,plain,
~ skC2,
inference(obv,[status(thm),theory(equality)],[2084]),
[iquote('4:Obv:2084.1')] ).
cnf(2089,plain,
~ equal(op(e2,e0),e2),
inference(rew,[status(thm),theory(equality)],[16,92,2053]),
[iquote('4:Rew:16.0,92.0,2053.0,92.0')] ).
cnf(2091,plain,
~ equal(op(e2,e3),e2),
inference(rew,[status(thm),theory(equality)],[16,97,2053]),
[iquote('4:Rew:16.0,97.0,2053.0,97.0')] ).
cnf(2092,plain,
~ skC3,
inference(mrr,[status(thm)],[531,2091]),
[iquote('4:MRR:531.1,2091.0')] ).
cnf(2095,plain,
~ equal(op(e4,e2),e4),
inference(rew,[status(thm),theory(equality)],[20,116,2053]),
[iquote('4:Rew:20.0,116.0,2053.0,116.0')] ).
cnf(2101,plain,
~ equal(op(e2,e0),e0),
inference(rew,[status(thm),theory(equality)],[11,26,2053]),
[iquote('4:Rew:11.0,26.0,2053.0,26.0')] ).
cnf(2104,plain,
~ equal(op(e0,e0),e0),
inference(rew,[status(thm),theory(equality)],[12,72,2053]),
[iquote('4:Rew:12.0,72.0,2053.0,72.0')] ).
cnf(2108,plain,
( ~ skC1
| ~ equal(op(e3,e4),unit) ),
inference(rew,[status(thm),theory(equality)],[2053,484]),
[iquote('4:Rew:2053.0,484.1')] ).
cnf(2113,plain,
~ equal(op(e4,e3),e4),
inference(rew,[status(thm),theory(equality)],[20,117,2053]),
[iquote('4:Rew:20.0,117.0,2053.0,117.0')] ).
cnf(2128,plain,
( skC3
| skC2
| skC1
| skC0
| equal(e4,unit) ),
inference(rew,[status(thm),theory(equality)],[19,508,2053]),
[iquote('4:Rew:19.0,508.4,2053.0,508.4')] ).
cnf(2129,plain,
skC1,
inference(mrr,[status(thm)],[2128,2092,2085,2083,1328]),
[iquote('4:MRR:2128.0,2128.1,2128.3,2128.4,2092.0,2085.0,2083.0,1328.0')] ).
cnf(2134,plain,
~ equal(op(e3,e4),unit),
inference(mrr,[status(thm)],[2108,2129]),
[iquote('4:MRR:2108.0,2129.0')] ).
cnf(2139,plain,
equal(op(e3,e3),e0),
inference(mrr,[status(thm)],[613,2104]),
[iquote('4:MRR:613.0,2104.0')] ).
cnf(2147,plain,
( equal(e0,unit)
| equal(op(e0,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[2053,611,2139]),
[iquote('4:Rew:2053.0,611.1,2139.0,611.0,2053.0,611.0')] ).
cnf(2148,plain,
equal(op(e0,e0),unit),
inference(mrr,[status(thm)],[2147,969]),
[iquote('4:MRR:2147.0,969.0')] ).
cnf(2150,plain,
~ equal(op(e2,e0),unit),
inference(rew,[status(thm),theory(equality)],[2148,23]),
[iquote('4:Rew:2148.0,23.0')] ).
cnf(2219,plain,
( equal(op(e3,e2),e4)
| equal(op(e0,e2),e4) ),
inference(mrr,[status(thm)],[558,2095]),
[iquote('4:MRR:558.0,2095.0')] ).
cnf(2260,plain,
( equal(op(e2,e0),e2)
| equal(op(e2,e0),e0)
| equal(op(e2,e0),e4)
| equal(op(e2,e0),unit) ),
inference(rew,[status(thm),theory(equality)],[2053,603]),
[iquote('4:Rew:2053.0,603.3')] ).
cnf(2261,plain,
equal(op(e2,e0),e4),
inference(mrr,[status(thm)],[2260,2089,2101,2150]),
[iquote('4:MRR:2260.0,2260.1,2260.3,2089.0,2101.0,2150.0')] ).
cnf(2264,plain,
~ equal(op(e2,e3),e4),
inference(rew,[status(thm),theory(equality)],[2261,94]),
[iquote('4:Rew:2261.0,94.0')] ).
cnf(2272,plain,
( equal(op(e4,e3),e4)
| equal(e4,e0)
| equal(op(e2,e3),e4)
| equal(op(e0,e3),e4) ),
inference(rew,[status(thm),theory(equality)],[2139,549]),
[iquote('4:Rew:2139.0,549.1')] ).
cnf(2273,plain,
equal(op(e0,e3),e4),
inference(mrr,[status(thm)],[2272,2113,4,2264]),
[iquote('4:MRR:2272.0,2272.1,2272.2,2113.0,4.0,2264.0')] ).
cnf(2274,plain,
~ equal(op(e0,e2),e4),
inference(rew,[status(thm),theory(equality)],[2273,79]),
[iquote('4:Rew:2273.0,79.0')] ).
cnf(2280,plain,
equal(op(e3,e2),e4),
inference(mrr,[status(thm)],[2219,2274]),
[iquote('4:MRR:2219.1,2274.0')] ).
cnf(2305,plain,
( equal(e4,e2)
| equal(e2,unit)
| equal(op(e3,e0),e2)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[11,589,2053,2148,2261]),
[iquote('4:Rew:11.0,589.3,2053.0,589.3,2148.0,589.1,2261.0,589.0')] ).
cnf(2306,plain,
equal(op(e3,e0),e2),
inference(mrr,[status(thm)],[2305,9,2060,2]),
[iquote('4:MRR:2305.0,2305.1,2305.3,9.0,2060.0,2.0')] ).
cnf(2318,plain,
( equal(e0,unit)
| equal(e3,unit)
| equal(op(e3,e4),unit)
| equal(e4,unit)
| equal(e2,unit) ),
inference(rew,[status(thm),theory(equality)],[2306,368,2053,2280,18,2139]),
[iquote('4:Rew:2306.0,368.4,2053.0,368.4,2280.0,368.3,2053.0,368.3,2053.0,368.2,18.0,368.1,2053.0,368.1,2139.0,368.0,2053.0,368.0')] ).
cnf(2319,plain,
$false,
inference(mrr,[status(thm)],[2318,969,1685,2134,1328,2060]),
[iquote('4:MRR:2318.0,2318.1,2318.2,2318.3,2318.4,969.0,1685.0,2134.0,1328.0,2060.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : ALG062+1 : TPTP v8.1.0. Released v2.7.0.
% 0.04/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 8 07:39:10 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.39/0.58
% 0.39/0.58 SPASS V 3.9
% 0.39/0.58 SPASS beiseite: Proof found.
% 0.39/0.58 % SZS status Theorem
% 0.39/0.58 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.58 SPASS derived 1060 clauses, backtracked 984 clauses, performed 4 splits and kept 1536 clauses.
% 0.39/0.58 SPASS allocated 86446 KBytes.
% 0.39/0.58 SPASS spent 0:00:00.24 on the problem.
% 0.39/0.58 0:00:00.04 for the input.
% 0.39/0.58 0:00:00.07 for the FLOTTER CNF translation.
% 0.39/0.58 0:00:00.00 for inferences.
% 0.39/0.58 0:00:00.00 for the backtracking.
% 0.39/0.58 0:00:00.09 for the reduction.
% 0.39/0.58
% 0.39/0.58
% 0.39/0.58 Here is a proof with depth 4, length 334 :
% 0.39/0.58 % SZS output start Refutation
% See solution above
% 0.39/0.59 Formulae used in the proof : ax5 ax2 ax6 ax4 co1 ax3 ax1
% 0.39/0.59
%------------------------------------------------------------------------------