%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG055+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n024.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:09 EDT 2022
% Result : Theorem 0.46s 0.64s
% Output : Refutation 0.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 92
% Syntax : Number of clauses : 287 ( 167 unt; 62 nHn; 287 RR)
% Number of literals : 543 ( 0 equ; 218 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 9 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('ALG055+1.p',unknown),
[] ).
cnf(2,axiom,
~ equal(e2,e0),
file('ALG055+1.p',unknown),
[] ).
cnf(4,axiom,
~ equal(e4,e0),
file('ALG055+1.p',unknown),
[] ).
cnf(5,axiom,
~ equal(e2,e1),
file('ALG055+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e3,e1),
file('ALG055+1.p',unknown),
[] ).
cnf(7,axiom,
~ equal(e4,e1),
file('ALG055+1.p',unknown),
[] ).
cnf(8,axiom,
~ equal(e3,e2),
file('ALG055+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(e4,e2),
file('ALG055+1.p',unknown),
[] ).
cnf(10,axiom,
~ equal(e4,e3),
file('ALG055+1.p',unknown),
[] ).
cnf(11,axiom,
equal(op(unit,e0),e0),
file('ALG055+1.p',unknown),
[] ).
cnf(12,axiom,
equal(op(e0,unit),e0),
file('ALG055+1.p',unknown),
[] ).
cnf(13,axiom,
equal(op(unit,e1),e1),
file('ALG055+1.p',unknown),
[] ).
cnf(14,axiom,
equal(op(e1,unit),e1),
file('ALG055+1.p',unknown),
[] ).
cnf(15,axiom,
equal(op(unit,e2),e2),
file('ALG055+1.p',unknown),
[] ).
cnf(16,axiom,
equal(op(e2,unit),e2),
file('ALG055+1.p',unknown),
[] ).
cnf(17,axiom,
equal(op(unit,e3),e3),
file('ALG055+1.p',unknown),
[] ).
cnf(18,axiom,
equal(op(e3,unit),e3),
file('ALG055+1.p',unknown),
[] ).
cnf(19,axiom,
equal(op(unit,e4),e4),
file('ALG055+1.p',unknown),
[] ).
cnf(20,axiom,
equal(op(e4,unit),e4),
file('ALG055+1.p',unknown),
[] ).
cnf(21,axiom,
equal(op(e2,e2),e4),
file('ALG055+1.p',unknown),
[] ).
cnf(22,axiom,
equal(op(e2,op(e2,e2)),e3),
file('ALG055+1.p',unknown),
[] ).
cnf(37,axiom,
~ equal(op(e2,e1),op(e1,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(38,axiom,
~ equal(op(e3,e1),op(e1,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(39,axiom,
~ equal(op(e4,e1),op(e1,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(40,axiom,
~ equal(op(e3,e1),op(e2,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(44,axiom,
~ equal(op(e2,e2),op(e0,e2)),
file('ALG055+1.p',unknown),
[] ).
cnf(53,axiom,
~ equal(op(e1,e3),op(e0,e3)),
file('ALG055+1.p',unknown),
[] ).
cnf(56,axiom,
~ equal(op(e4,e3),op(e0,e3)),
file('ALG055+1.p',unknown),
[] ).
cnf(64,axiom,
~ equal(op(e2,e4),op(e0,e4)),
file('ALG055+1.p',unknown),
[] ).
cnf(65,axiom,
~ equal(op(e3,e4),op(e0,e4)),
file('ALG055+1.p',unknown),
[] ).
cnf(66,axiom,
~ equal(op(e4,e4),op(e0,e4)),
file('ALG055+1.p',unknown),
[] ).
cnf(67,axiom,
~ equal(op(e2,e4),op(e1,e4)),
file('ALG055+1.p',unknown),
[] ).
cnf(68,axiom,
~ equal(op(e3,e4),op(e1,e4)),
file('ALG055+1.p',unknown),
[] ).
cnf(69,axiom,
~ equal(op(e4,e4),op(e1,e4)),
file('ALG055+1.p',unknown),
[] ).
cnf(74,axiom,
~ equal(op(e0,e2),op(e0,e0)),
file('ALG055+1.p',unknown),
[] ).
cnf(78,axiom,
~ equal(op(e0,e3),op(e0,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(80,axiom,
~ equal(op(e0,e3),op(e0,e2)),
file('ALG055+1.p',unknown),
[] ).
cnf(82,axiom,
~ equal(op(e0,e4),op(e0,e3)),
file('ALG055+1.p',unknown),
[] ).
cnf(83,axiom,
~ equal(op(e1,e1),op(e1,e0)),
file('ALG055+1.p',unknown),
[] ).
cnf(84,axiom,
~ equal(op(e1,e2),op(e1,e0)),
file('ALG055+1.p',unknown),
[] ).
cnf(86,axiom,
~ equal(op(e1,e4),op(e1,e0)),
file('ALG055+1.p',unknown),
[] ).
cnf(89,axiom,
~ equal(op(e1,e4),op(e1,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(91,axiom,
~ equal(op(e1,e4),op(e1,e2)),
file('ALG055+1.p',unknown),
[] ).
cnf(92,axiom,
~ equal(op(e1,e4),op(e1,e3)),
file('ALG055+1.p',unknown),
[] ).
cnf(95,axiom,
~ equal(op(e2,e3),op(e2,e0)),
file('ALG055+1.p',unknown),
[] ).
cnf(97,axiom,
~ equal(op(e2,e2),op(e2,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(98,axiom,
~ equal(op(e2,e3),op(e2,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(99,axiom,
~ equal(op(e2,e4),op(e2,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(100,axiom,
~ equal(op(e2,e3),op(e2,e2)),
file('ALG055+1.p',unknown),
[] ).
cnf(106,axiom,
~ equal(op(e3,e4),op(e3,e0)),
file('ALG055+1.p',unknown),
[] ).
cnf(111,axiom,
~ equal(op(e3,e4),op(e3,e2)),
file('ALG055+1.p',unknown),
[] ).
cnf(112,axiom,
~ equal(op(e3,e4),op(e3,e3)),
file('ALG055+1.p',unknown),
[] ).
cnf(113,axiom,
~ equal(op(e4,e1),op(e4,e0)),
file('ALG055+1.p',unknown),
[] ).
cnf(115,axiom,
~ equal(op(e4,e3),op(e4,e0)),
file('ALG055+1.p',unknown),
[] ).
cnf(118,axiom,
~ equal(op(e4,e3),op(e4,e1)),
file('ALG055+1.p',unknown),
[] ).
cnf(120,axiom,
~ equal(op(e4,e3),op(e4,e2)),
file('ALG055+1.p',unknown),
[] ).
cnf(121,axiom,
~ equal(op(e4,e4),op(e4,e2)),
file('ALG055+1.p',unknown),
[] ).
cnf(122,axiom,
~ equal(op(e4,e4),op(e4,e3)),
file('ALG055+1.p',unknown),
[] ).
cnf(139,axiom,
( ~ skC16
| equal(op(e4,op(e0,e4)),e0) ),
file('ALG055+1.p',unknown),
[] ).
cnf(140,axiom,
( ~ skC17
| equal(op(e4,op(e1,e4)),e1) ),
file('ALG055+1.p',unknown),
[] ).
cnf(141,axiom,
( ~ skC18
| equal(op(e4,op(e2,e4)),e2) ),
file('ALG055+1.p',unknown),
[] ).
cnf(142,axiom,
( ~ skC19
| equal(op(e4,op(e3,e4)),e3) ),
file('ALG055+1.p',unknown),
[] ).
cnf(143,axiom,
equal(op(op(e2,e2),op(e2,e2)),e0),
file('ALG055+1.p',unknown),
[] ).
cnf(160,axiom,
( ~ skC16
| ~ equal(op(e0,op(e0,e4)),e4) ),
file('ALG055+1.p',unknown),
[] ).
cnf(168,axiom,
( equal(op(e4,op(e4,e4)),e4)
| skC16
| skC17
| skC18
| skC19 ),
file('ALG055+1.p',unknown),
[] ).
cnf(169,axiom,
equal(op(op(e2,op(e2,e2)),op(e2,e2)),e1),
file('ALG055+1.p',unknown),
[] ).
cnf(174,axiom,
( ~ equal(op(e4,op(e4,e4)),e4)
| skC16
| skC17
| skC18
| skC19 ),
file('ALG055+1.p',unknown),
[] ).
cnf(199,axiom,
( ~ equal(e0,unit)
| ~ equal(op(e4,e4),e0)
| ~ skC20 ),
file('ALG055+1.p',unknown),
[] ).
cnf(219,axiom,
( ~ equal(e1,unit)
| ~ equal(op(e3,e4),e1)
| ~ skC21 ),
file('ALG055+1.p',unknown),
[] ).
cnf(280,axiom,
( ~ skC20
| ~ equal(op(e1,e2),e0)
| equal(op(e1,e0),e2) ),
file('ALG055+1.p',unknown),
[] ).
cnf(294,axiom,
( ~ equal(op(e4,e4),e0)
| ~ skC20
| equal(op(e4,e0),e4) ),
file('ALG055+1.p',unknown),
[] ).
cnf(310,axiom,
( ~ equal(op(e3,e4),e1)
| ~ skC21
| equal(op(e3,e1),e4) ),
file('ALG055+1.p',unknown),
[] ).
cnf(312,axiom,
( ~ skC21
| ~ equal(op(e4,e2),e1)
| equal(op(e4,e1),e2) ),
file('ALG055+1.p',unknown),
[] ).
cnf(318,axiom,
( ~ equal(op(e0,e4),e2)
| ~ skC22
| equal(op(e0,e2),e4) ),
file('ALG055+1.p',unknown),
[] ).
cnf(323,axiom,
( ~ equal(op(e2,e0),e2)
| ~ skC22
| equal(op(e2,e2),e0) ),
file('ALG055+1.p',unknown),
[] ).
cnf(325,axiom,
( ~ equal(op(e2,e3),e2)
| ~ skC22
| equal(op(e2,e2),e3) ),
file('ALG055+1.p',unknown),
[] ).
cnf(333,axiom,
( ~ skC22
| ~ equal(op(e4,e3),e2)
| equal(op(e4,e2),e3) ),
file('ALG055+1.p',unknown),
[] ).
cnf(346,axiom,
( ~ equal(op(e2,e4),e3)
| ~ skC23
| equal(op(e2,e3),e4) ),
file('ALG055+1.p',unknown),
[] ).
cnf(390,axiom,
( ~ equal(op(e2,e2),e4)
| equal(op(e2,e4),e2)
| skC20
| skC21
| skC22
| skC23 ),
file('ALG055+1.p',unknown),
[] ).
cnf(400,axiom,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e1,unit)
| equal(e0,unit) ),
file('ALG055+1.p',unknown),
[] ).
cnf(405,axiom,
( equal(op(e0,e4),e2)
| equal(op(e1,e4),e2)
| equal(op(e2,e4),e2)
| equal(op(e3,e4),e2)
| equal(op(e4,e4),e2) ),
file('ALG055+1.p',unknown),
[] ).
cnf(417,axiom,
( equal(op(e0,e3),e1)
| equal(op(e1,e3),e1)
| equal(op(e2,e3),e1)
| equal(op(e3,e3),e1)
| equal(op(e4,e3),e1) ),
file('ALG055+1.p',unknown),
[] ).
cnf(425,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('ALG055+1.p',unknown),
[] ).
cnf(427,axiom,
( equal(op(e0,e2),e1)
| equal(op(e1,e2),e1)
| equal(op(e2,e2),e1)
| equal(op(e3,e2),e1)
| equal(op(e4,e2),e1) ),
file('ALG055+1.p',unknown),
[] ).
cnf(429,axiom,
( equal(op(e0,e2),e0)
| equal(op(e1,e2),e0)
| equal(op(e2,e2),e0)
| equal(op(e3,e2),e0)
| equal(op(e4,e2),e0) ),
file('ALG055+1.p',unknown),
[] ).
cnf(447,axiom,
( equal(op(e0,e0),e1)
| equal(op(e1,e0),e1)
| equal(op(e2,e0),e1)
| equal(op(e3,e0),e1)
| equal(op(e4,e0),e1) ),
file('ALG055+1.p',unknown),
[] ).
cnf(452,axiom,
( equal(op(e4,e3),e0)
| equal(op(e4,e3),e1)
| equal(op(e4,e3),e2)
| equal(op(e4,e3),e3)
| equal(op(e4,e3),e4) ),
file('ALG055+1.p',unknown),
[] ).
cnf(464,axiom,
( equal(op(e2,e1),e0)
| equal(op(e2,e1),e1)
| equal(op(e2,e1),e2)
| equal(op(e2,e1),e3)
| equal(op(e2,e1),e4) ),
file('ALG055+1.p',unknown),
[] ).
cnf(466,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('ALG055+1.p',unknown),
[] ).
cnf(469,axiom,
( equal(op(e1,e1),e1)
| equal(op(e1,e1),e4)
| equal(op(e1,e1),e3)
| equal(op(e1,e1),e2)
| equal(op(e1,e1),e0) ),
file('ALG055+1.p',unknown),
[] ).
cnf(471,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('ALG055+1.p',unknown),
[] ).
cnf(472,axiom,
( equal(op(e0,e3),e3)
| equal(op(e0,e3),e0)
| equal(op(e0,e3),e4)
| equal(op(e0,e3),e2)
| equal(op(e0,e3),e1) ),
file('ALG055+1.p',unknown),
[] ).
cnf(476,plain,
equal(op(e2,e4),e3),
inference(rew,[status(thm),theory(equality)],[21,22]),
[iquote('0:Rew:21.0,22.0')] ).
cnf(479,plain,
~ equal(op(e2,e3),e4),
inference(rew,[status(thm),theory(equality)],[21,100]),
[iquote('0:Rew:21.0,100.0')] ).
cnf(480,plain,
~ equal(op(e2,e1),e3),
inference(rew,[status(thm),theory(equality)],[476,99]),
[iquote('0:Rew:476.0,99.0')] ).
cnf(481,plain,
~ equal(op(e2,e1),e4),
inference(rew,[status(thm),theory(equality)],[21,97]),
[iquote('0:Rew:21.0,97.0')] ).
cnf(486,plain,
~ equal(op(e1,e4),e3),
inference(rew,[status(thm),theory(equality)],[476,67]),
[iquote('0:Rew:476.0,67.0')] ).
cnf(487,plain,
~ equal(op(e0,e4),e3),
inference(rew,[status(thm),theory(equality)],[476,64]),
[iquote('0:Rew:476.0,64.0')] ).
cnf(491,plain,
~ equal(op(e0,e2),e4),
inference(rew,[status(thm),theory(equality)],[21,44]),
[iquote('0:Rew:21.0,44.0')] ).
cnf(492,plain,
equal(op(e4,e4),e0),
inference(rew,[status(thm),theory(equality)],[21,143]),
[iquote('0:Rew:21.0,143.0')] ).
cnf(493,plain,
~ equal(op(e4,e3),e0),
inference(rew,[status(thm),theory(equality)],[492,122]),
[iquote('0:Rew:492.0,122.0')] ).
cnf(494,plain,
~ equal(op(e4,e2),e0),
inference(rew,[status(thm),theory(equality)],[492,121]),
[iquote('0:Rew:492.0,121.0')] ).
cnf(499,plain,
~ equal(op(e1,e4),e0),
inference(rew,[status(thm),theory(equality)],[492,69]),
[iquote('0:Rew:492.0,69.0')] ).
cnf(500,plain,
~ equal(op(e0,e4),e0),
inference(rew,[status(thm),theory(equality)],[492,66]),
[iquote('0:Rew:492.0,66.0')] ).
cnf(501,plain,
( ~ skC18
| equal(op(e4,e3),e2) ),
inference(rew,[status(thm),theory(equality)],[476,141]),
[iquote('0:Rew:476.0,141.1')] ).
cnf(511,plain,
equal(op(e3,e4),e1),
inference(rew,[status(thm),theory(equality)],[476,169,21]),
[iquote('0:Rew:476.0,169.0,21.0,169.0')] ).
cnf(512,plain,
~ equal(op(e3,e3),e1),
inference(rew,[status(thm),theory(equality)],[511,112]),
[iquote('0:Rew:511.0,112.0')] ).
cnf(513,plain,
~ equal(op(e3,e2),e1),
inference(rew,[status(thm),theory(equality)],[511,111]),
[iquote('0:Rew:511.0,111.0')] ).
cnf(515,plain,
~ equal(op(e3,e0),e1),
inference(rew,[status(thm),theory(equality)],[511,106]),
[iquote('0:Rew:511.0,106.0')] ).
cnf(517,plain,
~ equal(op(e1,e4),e1),
inference(rew,[status(thm),theory(equality)],[511,68]),
[iquote('0:Rew:511.0,68.0')] ).
cnf(518,plain,
~ equal(op(e0,e4),e1),
inference(rew,[status(thm),theory(equality)],[511,65]),
[iquote('0:Rew:511.0,65.0')] ).
cnf(520,plain,
( ~ skC19
| equal(op(e4,e1),e3) ),
inference(rew,[status(thm),theory(equality)],[511,142]),
[iquote('0:Rew:511.0,142.1')] ).
cnf(522,plain,
( equal(op(e4,e0),e4)
| skC16
| skC17
| skC18
| skC19 ),
inference(rew,[status(thm),theory(equality)],[492,168]),
[iquote('0:Rew:492.0,168.0')] ).
cnf(536,plain,
( ~ equal(e1,unit)
| ~ equal(e1,e1)
| ~ skC21 ),
inference(rew,[status(thm),theory(equality)],[511,219]),
[iquote('0:Rew:511.0,219.1')] ).
cnf(537,plain,
( ~ skC21
| ~ equal(e1,unit) ),
inference(obv,[status(thm),theory(equality)],[536]),
[iquote('0:Obv:536.1')] ).
cnf(538,plain,
( ~ equal(e0,unit)
| ~ equal(e0,e0)
| ~ skC20 ),
inference(rew,[status(thm),theory(equality)],[492,199]),
[iquote('0:Rew:492.0,199.1')] ).
cnf(539,plain,
( ~ skC20
| ~ equal(e0,unit) ),
inference(obv,[status(thm),theory(equality)],[538]),
[iquote('0:Obv:538.1')] ).
cnf(540,plain,
( ~ equal(e4,e4)
| skC16
| skC17
| skC18
| skC19 ),
inference(rew,[status(thm),theory(equality)],[522,174,492]),
[iquote('0:Rew:522.0,174.0,492.0,174.0')] ).
cnf(541,plain,
( skC19
| skC18
| skC17
| skC16 ),
inference(obv,[status(thm),theory(equality)],[540]),
[iquote('0:Obv:540.0')] ).
cnf(550,plain,
( ~ equal(e3,e3)
| ~ skC23
| equal(op(e2,e3),e4) ),
inference(rew,[status(thm),theory(equality)],[476,346]),
[iquote('0:Rew:476.0,346.0')] ).
cnf(551,plain,
( ~ skC23
| equal(op(e2,e3),e4) ),
inference(obv,[status(thm),theory(equality)],[550]),
[iquote('0:Obv:550.0')] ).
cnf(552,plain,
~ skC23,
inference(mrr,[status(thm)],[551,479]),
[iquote('0:MRR:551.1,479.0')] ).
cnf(557,plain,
( ~ equal(op(e2,e3),e2)
| ~ skC22
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[21,325]),
[iquote('0:Rew:21.0,325.2')] ).
cnf(558,plain,
( ~ skC22
| ~ equal(op(e2,e3),e2) ),
inference(mrr,[status(thm)],[557,10]),
[iquote('0:MRR:557.2,10.0')] ).
cnf(561,plain,
( ~ equal(op(e2,e0),e2)
| ~ skC22
| equal(e4,e0) ),
inference(rew,[status(thm),theory(equality)],[21,323]),
[iquote('0:Rew:21.0,323.2')] ).
cnf(562,plain,
( ~ skC22
| ~ equal(op(e2,e0),e2) ),
inference(mrr,[status(thm)],[561,4]),
[iquote('0:MRR:561.2,4.0')] ).
cnf(564,plain,
( ~ skC22
| ~ equal(op(e0,e4),e2) ),
inference(mrr,[status(thm)],[318,491]),
[iquote('0:MRR:318.2,491.0')] ).
cnf(567,plain,
( ~ equal(e1,e1)
| ~ skC21
| equal(op(e3,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[511,310]),
[iquote('0:Rew:511.0,310.0')] ).
cnf(568,plain,
( ~ skC21
| equal(op(e3,e1),e4) ),
inference(obv,[status(thm),theory(equality)],[567]),
[iquote('0:Obv:567.0')] ).
cnf(572,plain,
( ~ equal(e0,e0)
| ~ skC20
| equal(op(e4,e0),e4) ),
inference(rew,[status(thm),theory(equality)],[492,294]),
[iquote('0:Rew:492.0,294.0')] ).
cnf(573,plain,
( ~ skC20
| equal(op(e4,e0),e4) ),
inference(obv,[status(thm),theory(equality)],[572]),
[iquote('0:Obv:572.0')] ).
cnf(599,plain,
( ~ equal(e4,e4)
| equal(e3,e2)
| skC20
| skC21
| skC22
| skC23 ),
inference(rew,[status(thm),theory(equality)],[476,390,21]),
[iquote('0:Rew:476.0,390.1,21.0,390.0')] ).
cnf(600,plain,
( equal(e3,e2)
| skC20
| skC21
| skC22
| skC23 ),
inference(obv,[status(thm),theory(equality)],[599]),
[iquote('0:Obv:599.0')] ).
cnf(601,plain,
( skC22
| skC21
| skC20 ),
inference(mrr,[status(thm)],[600,8,552]),
[iquote('0:MRR:600.0,600.4,8.0,552.0')] ).
cnf(608,plain,
( equal(op(e0,e4),e2)
| equal(op(e1,e4),e2)
| equal(e3,e2)
| equal(e2,e1)
| equal(e2,e0) ),
inference(rew,[status(thm),theory(equality)],[492,405,511,476]),
[iquote('0:Rew:492.0,405.4,511.0,405.3,476.0,405.2')] ).
cnf(609,plain,
( equal(op(e1,e4),e2)
| equal(op(e0,e4),e2) ),
inference(mrr,[status(thm)],[608,8,5,2]),
[iquote('0:MRR:608.2,608.3,608.4,8.0,5.0,2.0')] ).
cnf(622,plain,
( equal(op(e1,e3),e1)
| equal(op(e4,e3),e1)
| equal(op(e2,e3),e1)
| equal(op(e0,e3),e1) ),
inference(mrr,[status(thm)],[417,512]),
[iquote('0:MRR:417.3,512.0')] ).
cnf(628,plain,
( equal(op(e0,e2),e2)
| equal(op(e1,e2),e2)
| equal(e4,e2)
| equal(op(e3,e2),e2)
| equal(op(e4,e2),e2) ),
inference(rew,[status(thm),theory(equality)],[21,425]),
[iquote('0:Rew:21.0,425.2')] ).
cnf(629,plain,
( equal(op(e4,e2),e2)
| equal(op(e3,e2),e2)
| equal(op(e1,e2),e2)
| equal(op(e0,e2),e2) ),
inference(mrr,[status(thm)],[628,9]),
[iquote('0:MRR:628.2,9.0')] ).
cnf(632,plain,
( equal(op(e0,e2),e1)
| equal(op(e1,e2),e1)
| equal(e4,e1)
| equal(op(e3,e2),e1)
| equal(op(e4,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[21,427]),
[iquote('0:Rew:21.0,427.2')] ).
cnf(633,plain,
( equal(op(e1,e2),e1)
| equal(op(e4,e2),e1)
| equal(op(e0,e2),e1) ),
inference(mrr,[status(thm)],[632,7,513]),
[iquote('0:MRR:632.2,632.3,7.0,513.0')] ).
cnf(636,plain,
( equal(op(e0,e2),e0)
| equal(op(e1,e2),e0)
| equal(e4,e0)
| equal(op(e3,e2),e0)
| equal(op(e4,e2),e0) ),
inference(rew,[status(thm),theory(equality)],[21,429]),
[iquote('0:Rew:21.0,429.2')] ).
cnf(637,plain,
( equal(op(e0,e2),e0)
| equal(op(e3,e2),e0)
| equal(op(e1,e2),e0) ),
inference(mrr,[status(thm)],[636,4,494]),
[iquote('0:MRR:636.2,636.4,4.0,494.0')] ).
cnf(652,plain,
( equal(op(e1,e0),e1)
| equal(op(e0,e0),e1)
| equal(op(e4,e0),e1)
| equal(op(e2,e0),e1) ),
inference(mrr,[status(thm)],[447,515]),
[iquote('0:MRR:447.3,515.0')] ).
cnf(656,plain,
( equal(op(e4,e3),e4)
| equal(op(e4,e3),e3)
| equal(op(e4,e3),e2)
| equal(op(e4,e3),e1) ),
inference(mrr,[status(thm)],[452,493]),
[iquote('0:MRR:452.0,493.0')] ).
cnf(665,plain,
( equal(op(e2,e1),e2)
| equal(op(e2,e1),e1)
| equal(op(e2,e1),e0) ),
inference(mrr,[status(thm)],[464,480,481]),
[iquote('0:MRR:464.3,464.4,480.0,481.0')] ).
cnf(667,plain,
( equal(op(e1,e4),e4)
| equal(op(e1,e4),e2) ),
inference(mrr,[status(thm)],[466,499,517,486]),
[iquote('0:MRR:466.0,466.1,466.3,499.0,517.0,486.0')] ).
cnf(669,plain,
( equal(op(e0,e4),e4)
| equal(op(e0,e4),e2) ),
inference(mrr,[status(thm)],[471,500,518,487]),
[iquote('0:MRR:471.0,471.1,471.3,500.0,518.0,487.0')] ).
cnf(671,plain,
equal(e1,unit),
inference(spt,[spt(split,[position(s1)])],[400]),
[iquote('1:Spt:400.3')] ).
cnf(676,plain,
( ~ skC19
| equal(op(e4,unit),e3) ),
inference(rew,[status(thm),theory(equality)],[671,520]),
[iquote('1:Rew:671.0,520.1')] ).
cnf(687,plain,
~ equal(op(e4,e0),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[671,113]),
[iquote('1:Rew:671.0,113.0')] ).
cnf(729,plain,
~ equal(op(e0,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[671,53]),
[iquote('1:Rew:671.0,53.0')] ).
cnf(790,plain,
~ equal(op(e0,e3),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[671,78]),
[iquote('1:Rew:671.0,78.0')] ).
cnf(797,plain,
( ~ skC21
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[671,537]),
[iquote('1:Rew:671.0,537.1')] ).
cnf(800,plain,
( equal(op(e1,e2),e1)
| equal(op(e4,e2),unit)
| equal(op(e0,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[671,633]),
[iquote('1:Rew:671.0,633.1')] ).
cnf(813,plain,
( equal(op(e0,e3),e3)
| equal(op(e0,e3),e0)
| equal(op(e0,e3),e4)
| equal(op(e0,e3),e2)
| equal(op(e0,e3),unit) ),
inference(rew,[status(thm),theory(equality)],[671,472]),
[iquote('1:Rew:671.0,472.4')] ).
cnf(817,plain,
~ equal(e3,unit),
inference(rew,[status(thm),theory(equality)],[671,6]),
[iquote('1:Rew:671.0,6.0')] ).
cnf(818,plain,
~ equal(e2,unit),
inference(rew,[status(thm),theory(equality)],[671,5]),
[iquote('1:Rew:671.0,5.0')] ).
cnf(819,plain,
~ equal(e0,unit),
inference(rew,[status(thm),theory(equality)],[671,1]),
[iquote('1:Rew:671.0,1.0')] ).
cnf(829,plain,
( ~ skC17
| equal(op(e4,op(unit,e4)),unit) ),
inference(rew,[status(thm),theory(equality)],[671,140]),
[iquote('1:Rew:671.0,140.1')] ).
cnf(851,plain,
~ skC21,
inference(obv,[status(thm),theory(equality)],[797]),
[iquote('1:Obv:797.1')] ).
cnf(852,plain,
( skC22
| skC20 ),
inference(mrr,[status(thm)],[601,851]),
[iquote('1:MRR:601.1,851.0')] ).
cnf(855,plain,
( ~ skC19
| equal(e4,e3) ),
inference(rew,[status(thm),theory(equality)],[20,676]),
[iquote('1:Rew:20.0,676.1')] ).
cnf(856,plain,
~ skC19,
inference(mrr,[status(thm)],[855,10]),
[iquote('1:MRR:855.1,10.0')] ).
cnf(857,plain,
( skC18
| skC17
| skC16 ),
inference(mrr,[status(thm)],[541,856]),
[iquote('1:MRR:541.0,856.0')] ).
cnf(860,plain,
~ equal(op(e4,e0),e4),
inference(rew,[status(thm),theory(equality)],[20,687]),
[iquote('1:Rew:20.0,687.0')] ).
cnf(861,plain,
~ skC20,
inference(mrr,[status(thm)],[573,860]),
[iquote('1:MRR:573.1,860.0')] ).
cnf(862,plain,
skC22,
inference(mrr,[status(thm)],[852,861]),
[iquote('1:MRR:852.1,861.0')] ).
cnf(866,plain,
~ equal(op(e0,e4),e2),
inference(mrr,[status(thm)],[564,862]),
[iquote('1:MRR:564.0,862.0')] ).
cnf(867,plain,
( ~ equal(op(e4,e3),e2)
| equal(op(e4,e2),e3) ),
inference(mrr,[status(thm)],[333,862]),
[iquote('1:MRR:333.0,862.0')] ).
cnf(872,plain,
equal(op(e0,e4),e4),
inference(mrr,[status(thm)],[669,866]),
[iquote('1:MRR:669.1,866.0')] ).
cnf(875,plain,
~ equal(op(e0,e3),e4),
inference(rew,[status(thm),theory(equality)],[872,82]),
[iquote('1:Rew:872.0,82.0')] ).
cnf(879,plain,
( ~ skC16
| ~ equal(op(e0,e4),e4) ),
inference(rew,[status(thm),theory(equality)],[872,160]),
[iquote('1:Rew:872.0,160.1')] ).
cnf(900,plain,
~ equal(op(e0,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,729]),
[iquote('1:Rew:17.0,729.0')] ).
cnf(925,plain,
~ equal(op(e0,e3),e0),
inference(rew,[status(thm),theory(equality)],[12,790]),
[iquote('1:Rew:12.0,790.0')] ).
cnf(932,plain,
( ~ skC16
| ~ equal(e4,e4) ),
inference(rew,[status(thm),theory(equality)],[872,879]),
[iquote('1:Rew:872.0,879.1')] ).
cnf(933,plain,
~ skC16,
inference(obv,[status(thm),theory(equality)],[932]),
[iquote('1:Obv:932.1')] ).
cnf(934,plain,
( skC18
| skC17 ),
inference(mrr,[status(thm)],[857,933]),
[iquote('1:MRR:857.2,933.0')] ).
cnf(935,plain,
( ~ skC17
| equal(e0,unit) ),
inference(rew,[status(thm),theory(equality)],[492,829,19]),
[iquote('1:Rew:492.0,829.1,19.0,829.1')] ).
cnf(936,plain,
~ skC17,
inference(mrr,[status(thm)],[935,819]),
[iquote('1:MRR:935.1,819.0')] ).
cnf(937,plain,
skC18,
inference(mrr,[status(thm)],[934,936]),
[iquote('1:MRR:934.1,936.0')] ).
cnf(938,plain,
equal(op(e4,e3),e2),
inference(mrr,[status(thm)],[501,937]),
[iquote('1:MRR:501.0,937.0')] ).
cnf(944,plain,
~ equal(op(e0,e3),e2),
inference(rew,[status(thm),theory(equality)],[938,56]),
[iquote('1:Rew:938.0,56.0')] ).
cnf(988,plain,
( ~ equal(e2,e2)
| equal(op(e4,e2),e3) ),
inference(rew,[status(thm),theory(equality)],[938,867]),
[iquote('1:Rew:938.0,867.0')] ).
cnf(989,plain,
equal(op(e4,e2),e3),
inference(obv,[status(thm),theory(equality)],[988]),
[iquote('1:Obv:988.0')] ).
cnf(1018,plain,
( equal(e2,unit)
| equal(e3,unit)
| equal(op(e0,e2),unit) ),
inference(rew,[status(thm),theory(equality)],[671,800,989,15]),
[iquote('1:Rew:671.0,800.2,989.0,800.1,15.0,800.0,671.0,800.0')] ).
cnf(1019,plain,
equal(op(e0,e2),unit),
inference(mrr,[status(thm)],[1018,818,817]),
[iquote('1:MRR:1018.0,1018.1,818.0,817.0')] ).
cnf(1021,plain,
~ equal(op(e0,e3),unit),
inference(rew,[status(thm),theory(equality)],[1019,80]),
[iquote('1:Rew:1019.0,80.0')] ).
cnf(1098,plain,
$false,
inference(mrr,[status(thm)],[813,900,925,875,944,1021]),
[iquote('1:MRR:813.0,813.1,813.2,813.3,813.4,900.0,925.0,875.0,944.0,1021.0')] ).
cnf(1099,plain,
~ equal(e1,unit),
inference(spt,[spt(split,[position(sa)])],[1098,671]),
[iquote('1:Spt:1098.0,400.3,671.0')] ).
cnf(1100,plain,
( equal(e4,unit)
| equal(e3,unit)
| equal(e2,unit)
| equal(e0,unit) ),
inference(spt,[spt(split,[position(s2)])],[400]),
[iquote('1:Spt:1098.0,400.0,400.1,400.2,400.4')] ).
cnf(1101,plain,
equal(e4,unit),
inference(spt,[spt(split,[position(s2s1)])],[1100]),
[iquote('2:Spt:1100.0')] ).
cnf(1104,plain,
( equal(op(e1,e0),e1)
| equal(op(e0,e0),e1)
| equal(op(unit,e0),e1)
| equal(op(e2,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[1101,652]),
[iquote('2:Rew:1101.0,652.2')] ).
cnf(1140,plain,
~ equal(op(e1,e0),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[1101,86]),
[iquote('2:Rew:1101.0,86.0')] ).
cnf(1142,plain,
~ equal(op(e1,e2),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[1101,91]),
[iquote('2:Rew:1101.0,91.0')] ).
cnf(1144,plain,
~ equal(op(e1,e3),op(e1,unit)),
inference(rew,[status(thm),theory(equality)],[1101,92]),
[iquote('2:Rew:1101.0,92.0')] ).
cnf(1177,plain,
( equal(op(e1,e3),e1)
| equal(op(unit,e3),e1)
| equal(op(e2,e3),e1)
| equal(op(e0,e3),e1) ),
inference(rew,[status(thm),theory(equality)],[1101,622]),
[iquote('2:Rew:1101.0,622.1')] ).
cnf(1190,plain,
( equal(op(e1,e2),e1)
| equal(op(unit,e2),e1)
| equal(op(e0,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[1101,633]),
[iquote('2:Rew:1101.0,633.1')] ).
cnf(1280,plain,
~ equal(op(e1,e0),e1),
inference(rew,[status(thm),theory(equality)],[14,1140]),
[iquote('2:Rew:14.0,1140.0')] ).
cnf(1283,plain,
~ equal(op(e1,e2),e1),
inference(rew,[status(thm),theory(equality)],[14,1142]),
[iquote('2:Rew:14.0,1142.0')] ).
cnf(1287,plain,
~ equal(op(e1,e3),e1),
inference(rew,[status(thm),theory(equality)],[14,1144]),
[iquote('2:Rew:14.0,1144.0')] ).
cnf(1342,plain,
( equal(op(e1,e2),e1)
| equal(e2,e1)
| equal(op(e0,e2),e1) ),
inference(rew,[status(thm),theory(equality)],[15,1190]),
[iquote('2:Rew:15.0,1190.1')] ).
cnf(1343,plain,
equal(op(e0,e2),e1),
inference(mrr,[status(thm)],[1342,1283,5]),
[iquote('2:MRR:1342.0,1342.1,1283.0,5.0')] ).
cnf(1347,plain,
~ equal(op(e0,e0),e1),
inference(rew,[status(thm),theory(equality)],[1343,74]),
[iquote('2:Rew:1343.0,74.0')] ).
cnf(1348,plain,
~ equal(op(e0,e3),e1),
inference(rew,[status(thm),theory(equality)],[1343,80]),
[iquote('2:Rew:1343.0,80.0')] ).
cnf(1370,plain,
( equal(op(e1,e0),e1)
| equal(op(e0,e0),e1)
| equal(e1,e0)
| equal(op(e2,e0),e1) ),
inference(rew,[status(thm),theory(equality)],[11,1104]),
[iquote('2:Rew:11.0,1104.2')] ).
cnf(1371,plain,
equal(op(e2,e0),e1),
inference(mrr,[status(thm)],[1370,1280,1347,1]),
[iquote('2:MRR:1370.0,1370.1,1370.2,1280.0,1347.0,1.0')] ).
cnf(1377,plain,
~ equal(op(e2,e3),e1),
inference(rew,[status(thm),theory(equality)],[1371,95]),
[iquote('2:Rew:1371.0,95.0')] ).
cnf(1397,plain,
( equal(op(e1,e3),e1)
| equal(e3,e1)
| equal(op(e2,e3),e1)
| equal(op(e0,e3),e1) ),
inference(rew,[status(thm),theory(equality)],[17,1177]),
[iquote('2:Rew:17.0,1177.1')] ).
cnf(1398,plain,
$false,
inference(mrr,[status(thm)],[1397,1287,6,1377,1348]),
[iquote('2:MRR:1397.0,1397.1,1397.2,1397.3,1287.0,6.0,1377.0,1348.0')] ).
cnf(1429,plain,
~ equal(e4,unit),
inference(spt,[spt(split,[position(s2sa)])],[1398,1101]),
[iquote('2:Spt:1398.0,1100.0,1101.0')] ).
cnf(1430,plain,
( equal(e3,unit)
| equal(e2,unit)
| equal(e0,unit) ),
inference(spt,[spt(split,[position(s2s2)])],[1100]),
[iquote('2:Spt:1398.0,1100.1,1100.2,1100.3')] ).
cnf(1431,plain,
equal(e3,unit),
inference(spt,[spt(split,[position(s2s2s1)])],[1430]),
[iquote('3:Spt:1430.0')] ).
cnf(1435,plain,
~ equal(op(e0,e2),op(e0,unit)),
inference(rew,[status(thm),theory(equality)],[1431,80]),
[iquote('3:Rew:1431.0,80.0')] ).
cnf(1473,plain,
~ equal(op(e1,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[1431,38]),
[iquote('3:Rew:1431.0,38.0')] ).
cnf(1474,plain,
~ equal(op(e2,e1),op(unit,e1)),
inference(rew,[status(thm),theory(equality)],[1431,40]),
[iquote('3:Rew:1431.0,40.0')] ).
cnf(1481,plain,
( ~ skC21
| equal(op(unit,e1),e4) ),
inference(rew,[status(thm),theory(equality)],[1431,568]),
[iquote('3:Rew:1431.0,568.1')] ).
cnf(1490,plain,
( equal(op(e0,e2),e0)
| equal(op(unit,e2),e0)
| equal(op(e1,e2),e0) ),
inference(rew,[status(thm),theory(equality)],[1431,637]),
[iquote('3:Rew:1431.0,637.1')] ).
cnf(1506,plain,
~ equal(op(e2,e1),op(e2,unit)),
inference(rew,[status(thm),theory(equality)],[1431,98]),
[iquote('3:Rew:1431.0,98.0')] ).
cnf(1509,plain,
( ~ skC22
| ~ equal(op(e2,unit),e2) ),
inference(rew,[status(thm),theory(equality)],[1431,558]),
[iquote('3:Rew:1431.0,558.1')] ).
cnf(1557,plain,
( ~ skC18
| equal(op(e4,unit),e2) ),
inference(rew,[status(thm),theory(equality)],[1431,501]),
[iquote('3:Rew:1431.0,501.1')] ).
cnf(1574,plain,
( ~ skC19
| equal(op(e4,e1),unit) ),
inference(rew,[status(thm),theory(equality)],[1431,520]),
[iquote('3:Rew:1431.0,520.1')] ).
cnf(1582,plain,
( equal(op(e1,e1),e1)
| equal(op(e1,e1),e4)
| equal(op(e1,e1),unit)
| equal(op(e1,e1),e2)
| equal(op(e1,e1),e0) ),
inference(rew,[status(thm),theory(equality)],[1431,469]),
[iquote('3:Rew:1431.0,469.2')] ).
cnf(1598,plain,
( ~ skC21
| equal(e4,e1) ),
inference(rew,[status(thm),theory(equality)],[13,1481]),
[iquote('3:Rew:13.0,1481.1')] ).
cnf(1599,plain,
~ skC21,
inference(mrr,[status(thm)],[1598,7]),
[iquote('3:MRR:1598.1,7.0')] ).
cnf(1600,plain,
( skC22
| skC20 ),
inference(mrr,[status(thm)],[601,1599]),
[iquote('3:MRR:601.1,1599.0')] ).
cnf(1601,plain,
( ~ skC18
| equal(e4,e2) ),
inference(rew,[status(thm),theory(equality)],[20,1557]),
[iquote('3:Rew:20.0,1557.1')] ).
cnf(1602,plain,
~ skC18,
inference(mrr,[status(thm)],[1601,9]),
[iquote('3:MRR:1601.1,9.0')] ).
cnf(1603,plain,
( skC19
| skC17
| skC16 ),
inference(mrr,[status(thm)],[541,1602]),
[iquote('3:MRR:541.1,1602.0')] ).
cnf(1607,plain,
~ equal(op(e0,e2),e0),
inference(rew,[status(thm),theory(equality)],[12,1435]),
[iquote('3:Rew:12.0,1435.0')] ).
cnf(1616,plain,
~ equal(op(e1,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1473]),
[iquote('3:Rew:13.0,1473.0')] ).
cnf(1617,plain,
~ equal(op(e2,e1),e1),
inference(rew,[status(thm),theory(equality)],[13,1474]),
[iquote('3:Rew:13.0,1474.0')] ).
cnf(1618,plain,
( equal(op(e2,e1),e2)
| equal(op(e2,e1),e0) ),
inference(mrr,[status(thm)],[665,1617]),
[iquote('3:MRR:665.1,1617.0')] ).
cnf(1633,plain,
~ equal(op(e2,e1),e2),
inference(rew,[status(thm),theory(equality)],[16,1506]),
[iquote('3:Rew:16.0,1506.0')] ).
cnf(1634,plain,
( ~ skC22
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[16,1509]),
[iquote('3:Rew:16.0,1509.1')] ).
cnf(1635,plain,
~ skC22,
inference(obv,[status(thm),theory(equality)],[1634]),
[iquote('3:Obv:1634.1')] ).
cnf(1636,plain,
skC20,
inference(mrr,[status(thm)],[1600,1635]),
[iquote('3:MRR:1600.0,1635.0')] ).
cnf(1639,plain,
( ~ equal(op(e1,e2),e0)
| equal(op(e1,e0),e2) ),
inference(mrr,[status(thm)],[280,1636]),
[iquote('3:MRR:280.0,1636.0')] ).
cnf(1702,plain,
equal(op(e2,e1),e0),
inference(mrr,[status(thm)],[1618,1633]),
[iquote('3:MRR:1618.0,1633.0')] ).
cnf(1704,plain,
~ equal(op(e1,e1),e0),
inference(rew,[status(thm),theory(equality)],[1702,37]),
[iquote('3:Rew:1702.0,37.0')] ).
cnf(1740,plain,
( equal(op(e0,e2),e0)
| equal(e2,e0)
| equal(op(e1,e2),e0) ),
inference(rew,[status(thm),theory(equality)],[15,1490]),
[iquote('3:Rew:15.0,1490.1')] ).
cnf(1741,plain,
equal(op(e1,e2),e0),
inference(mrr,[status(thm)],[1740,1607,2]),
[iquote('3:MRR:1740.0,1740.1,1607.0,2.0')] ).
cnf(1752,plain,
( ~ equal(e0,e0)
| equal(op(e1,e0),e2) ),
inference(rew,[status(thm),theory(equality)],[1741,1639]),
[iquote('3:Rew:1741.0,1639.0')] ).
cnf(1753,plain,
equal(op(e1,e0),e2),
inference(obv,[status(thm),theory(equality)],[1752]),
[iquote('3:Obv:1752.0')] ).
cnf(1754,plain,
~ equal(op(e1,e1),e2),
inference(rew,[status(thm),theory(equality)],[1753,83]),
[iquote('3:Rew:1753.0,83.0')] ).
cnf(1755,plain,
~ equal(op(e1,e4),e2),
inference(rew,[status(thm),theory(equality)],[1753,86]),
[iquote('3:Rew:1753.0,86.0')] ).
cnf(1772,plain,
equal(op(e1,e4),e4),
inference(mrr,[status(thm)],[667,1755]),
[iquote('3:MRR:667.1,1755.0')] ).
cnf(1773,plain,
equal(op(e0,e4),e2),
inference(mrr,[status(thm)],[609,1755]),
[iquote('3:MRR:609.0,1755.0')] ).
cnf(1777,plain,
~ equal(op(e1,e1),e4),
inference(rew,[status(thm),theory(equality)],[1772,89]),
[iquote('3:Rew:1772.0,89.0')] ).
cnf(1778,plain,
( ~ skC17
| equal(op(e4,e4),e1) ),
inference(rew,[status(thm),theory(equality)],[1772,140]),
[iquote('3:Rew:1772.0,140.1')] ).
cnf(1785,plain,
( ~ skC16
| equal(op(e4,e2),e0) ),
inference(rew,[status(thm),theory(equality)],[1773,139]),
[iquote('3:Rew:1773.0,139.1')] ).
cnf(1795,plain,
( ~ skC17
| equal(e1,e0) ),
inference(rew,[status(thm),theory(equality)],[492,1778]),
[iquote('3:Rew:492.0,1778.1')] ).
cnf(1796,plain,
~ skC17,
inference(mrr,[status(thm)],[1795,1]),
[iquote('3:MRR:1795.1,1.0')] ).
cnf(1797,plain,
( skC19
| skC16 ),
inference(mrr,[status(thm)],[1603,1796]),
[iquote('3:MRR:1603.1,1796.0')] ).
cnf(1798,plain,
~ skC16,
inference(mrr,[status(thm)],[1785,494]),
[iquote('3:MRR:1785.1,494.0')] ).
cnf(1799,plain,
skC19,
inference(mrr,[status(thm)],[1797,1798]),
[iquote('3:MRR:1797.1,1798.0')] ).
cnf(1800,plain,
equal(op(e4,e1),unit),
inference(mrr,[status(thm)],[1574,1799]),
[iquote('3:MRR:1574.0,1799.0')] ).
cnf(1803,plain,
~ equal(op(e1,e1),unit),
inference(rew,[status(thm),theory(equality)],[1800,39]),
[iquote('3:Rew:1800.0,39.0')] ).
cnf(1853,plain,
$false,
inference(mrr,[status(thm)],[1582,1616,1777,1803,1754,1704]),
[iquote('3:MRR:1582.0,1582.1,1582.2,1582.3,1582.4,1616.0,1777.0,1803.0,1754.0,1704.0')] ).
cnf(1854,plain,
~ equal(e3,unit),
inference(spt,[spt(split,[position(s2s2sa)])],[1853,1431]),
[iquote('3:Spt:1853.0,1430.0,1431.0')] ).
cnf(1855,plain,
( equal(e2,unit)
| equal(e0,unit) ),
inference(spt,[spt(split,[position(s2s2s2)])],[1430]),
[iquote('3:Spt:1853.0,1430.1,1430.2')] ).
cnf(1856,plain,
equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2s1)])],[1855]),
[iquote('4:Spt:1855.0')] ).
cnf(1857,plain,
~ equal(e0,unit),
inference(rew,[status(thm),theory(equality)],[1856,2]),
[iquote('4:Rew:1856.0,2.0')] ).
cnf(2012,plain,
( equal(op(e4,e2),e2)
| equal(op(e3,unit),unit)
| equal(op(e1,e2),e2)
| equal(op(e0,e2),e2) ),
inference(rew,[status(thm),theory(equality)],[1856,629]),
[iquote('4:Rew:1856.0,629.1')] ).
cnf(2197,plain,
( equal(e4,unit)
| equal(e3,unit)
| equal(e1,unit)
| equal(e0,unit) ),
inference(rew,[status(thm),theory(equality)],[12,2012,1856,14,18,20]),
[iquote('4:Rew:12.0,2012.3,1856.0,2012.3,14.0,2012.2,1856.0,2012.2,18.0,2012.1,20.0,2012.0,1856.0,2012.0')] ).
cnf(2198,plain,
$false,
inference(mrr,[status(thm)],[2197,1429,1854,1099,1857]),
[iquote('4:MRR:2197.0,2197.1,2197.2,2197.3,1429.0,1854.0,1099.0,1857.0')] ).
cnf(2217,plain,
~ equal(e2,unit),
inference(spt,[spt(split,[position(s2s2s2sa)])],[2198,1856]),
[iquote('4:Spt:2198.0,1855.0,1856.0')] ).
cnf(2218,plain,
equal(e0,unit),
inference(spt,[spt(split,[position(s2s2s2s2)])],[1855]),
[iquote('4:Spt:2198.0,1855.1')] ).
cnf(2235,plain,
~ equal(op(e4,e3),op(e4,unit)),
inference(rew,[status(thm),theory(equality)],[2218,115]),
[iquote('4:Rew:2218.0,115.0')] ).
cnf(2243,plain,
~ equal(op(e4,e3),op(unit,e3)),
inference(rew,[status(thm),theory(equality)],[2218,56]),
[iquote('4:Rew:2218.0,56.0')] ).
cnf(2280,plain,
( ~ skC20
| ~ equal(unit,unit) ),
inference(rew,[status(thm),theory(equality)],[2218,539]),
[iquote('4:Rew:2218.0,539.1')] ).
cnf(2281,plain,
~ skC20,
inference(obv,[status(thm),theory(equality)],[2280]),
[iquote('4:Obv:2280.1')] ).
cnf(2282,plain,
( skC22
| skC21 ),
inference(mrr,[status(thm)],[601,2281]),
[iquote('4:MRR:601.2,2281.0')] ).
cnf(2288,plain,
( ~ skC22
| ~ equal(e2,e2) ),
inference(rew,[status(thm),theory(equality)],[16,562,2218]),
[iquote('4:Rew:16.0,562.1,2218.0,562.1')] ).
cnf(2289,plain,
~ skC22,
inference(obv,[status(thm),theory(equality)],[2288]),
[iquote('4:Obv:2288.1')] ).
cnf(2290,plain,
skC21,
inference(mrr,[status(thm)],[2282,2289]),
[iquote('4:MRR:2282.0,2289.0')] ).
cnf(2310,plain,
~ equal(op(e1,e2),e1),
inference(rew,[status(thm),theory(equality)],[14,84,2218]),
[iquote('4:Rew:14.0,84.0,2218.0,84.0')] ).
cnf(2327,plain,
~ equal(op(e4,e3),e4),
inference(rew,[status(thm),theory(equality)],[20,2235]),
[iquote('4:Rew:20.0,2235.0')] ).
cnf(2331,plain,
~ equal(op(e4,e3),e3),
inference(rew,[status(thm),theory(equality)],[17,2243]),
[iquote('4:Rew:17.0,2243.0')] ).
cnf(2393,plain,
( ~ equal(op(e4,e2),e1)
| equal(op(e4,e1),e2) ),
inference(mrr,[status(thm)],[312,2290]),
[iquote('4:MRR:312.0,2290.0')] ).
cnf(2448,plain,
( equal(op(e1,e2),e1)
| equal(op(e4,e2),e1)
| equal(e2,e1) ),
inference(rew,[status(thm),theory(equality)],[15,633,2218]),
[iquote('4:Rew:15.0,633.2,2218.0,633.2')] ).
cnf(2449,plain,
equal(op(e4,e2),e1),
inference(mrr,[status(thm)],[2448,2310,5]),
[iquote('4:MRR:2448.0,2448.2,2310.0,5.0')] ).
cnf(2455,plain,
~ equal(op(e4,e3),e1),
inference(rew,[status(thm),theory(equality)],[2449,120]),
[iquote('4:Rew:2449.0,120.0')] ).
cnf(2456,plain,
( ~ equal(e1,e1)
| equal(op(e4,e1),e2) ),
inference(rew,[status(thm),theory(equality)],[2449,2393]),
[iquote('4:Rew:2449.0,2393.0')] ).
cnf(2462,plain,
equal(op(e4,e1),e2),
inference(obv,[status(thm),theory(equality)],[2456]),
[iquote('4:Obv:2456.0')] ).
cnf(2463,plain,
~ equal(op(e4,e3),e2),
inference(rew,[status(thm),theory(equality)],[2462,118]),
[iquote('4:Rew:2462.0,118.0')] ).
cnf(2521,plain,
$false,
inference(mrr,[status(thm)],[656,2327,2331,2463,2455]),
[iquote('4:MRR:656.0,656.1,656.2,656.3,2327.0,2331.0,2463.0,2455.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : ALG055+1 : TPTP v8.1.0. Released v2.7.0.
% 0.04/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n024.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 8 19:45:34 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.46/0.64
% 0.46/0.64 SPASS V 3.9
% 0.46/0.64 SPASS beiseite: Proof found.
% 0.46/0.64 % SZS status Theorem
% 0.46/0.64 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.46/0.64 SPASS derived 1098 clauses, backtracked 920 clauses, performed 4 splits and kept 1640 clauses.
% 0.46/0.64 SPASS allocated 86603 KBytes.
% 0.46/0.64 SPASS spent 0:00:00.28 on the problem.
% 0.46/0.64 0:00:00.04 for the input.
% 0.46/0.64 0:00:00.08 for the FLOTTER CNF translation.
% 0.46/0.64 0:00:00.00 for inferences.
% 0.46/0.64 0:00:00.00 for the backtracking.
% 0.46/0.64 0:00:00.13 for the reduction.
% 0.46/0.64
% 0.46/0.64
% 0.46/0.64 Here is a proof with depth 4, length 287 :
% 0.46/0.64 % SZS output start Refutation
% See solution above
% 0.46/0.64 Formulae used in the proof : ax5 ax2 ax6 ax4 co1 ax3 ax1
% 0.46/0.64
%------------------------------------------------------------------------------