%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG187+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:51 EDT 2022
% Result : Theorem 0.36s 0.55s
% Output : Refutation 0.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 106
% Syntax : Number of clauses : 259 ( 106 unt; 2 nHn; 259 RR)
% Number of literals : 691 ( 0 equ; 430 neg)
% Maximal clause size : 101 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 77 ( 76 usr; 76 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
~ equal(e2,e0),
file('ALG187+1.p',unknown),
[] ).
cnf(4,axiom,
~ equal(e4,e0),
file('ALG187+1.p',unknown),
[] ).
cnf(5,axiom,
~ equal(e2,e1),
file('ALG187+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e3,e1),
file('ALG187+1.p',unknown),
[] ).
cnf(10,axiom,
~ equal(e4,e3),
file('ALG187+1.p',unknown),
[] ).
cnf(11,axiom,
equal(op(e0,e0),e4),
file('ALG187+1.p',unknown),
[] ).
cnf(12,axiom,
equal(op(e0,e1),e2),
file('ALG187+1.p',unknown),
[] ).
cnf(13,axiom,
equal(op(e0,e2),e0),
file('ALG187+1.p',unknown),
[] ).
cnf(14,axiom,
equal(op(e0,e3),e1),
file('ALG187+1.p',unknown),
[] ).
cnf(15,axiom,
equal(op(e0,e4),e3),
file('ALG187+1.p',unknown),
[] ).
cnf(16,axiom,
equal(op(e1,e0),e0),
file('ALG187+1.p',unknown),
[] ).
cnf(17,axiom,
equal(op(e1,e1),e1),
file('ALG187+1.p',unknown),
[] ).
cnf(18,axiom,
equal(op(e1,e2),e2),
file('ALG187+1.p',unknown),
[] ).
cnf(19,axiom,
equal(op(e1,e3),e3),
file('ALG187+1.p',unknown),
[] ).
cnf(20,axiom,
equal(op(e1,e4),e4),
file('ALG187+1.p',unknown),
[] ).
cnf(21,axiom,
equal(op(e2,e0),e1),
file('ALG187+1.p',unknown),
[] ).
cnf(22,axiom,
equal(op(e2,e1),e4),
file('ALG187+1.p',unknown),
[] ).
cnf(23,axiom,
equal(op(e2,e2),e3),
file('ALG187+1.p',unknown),
[] ).
cnf(24,axiom,
equal(op(e2,e3),e0),
file('ALG187+1.p',unknown),
[] ).
cnf(25,axiom,
equal(op(e2,e4),e2),
file('ALG187+1.p',unknown),
[] ).
cnf(26,axiom,
equal(op(e3,e0),e3),
file('ALG187+1.p',unknown),
[] ).
cnf(27,axiom,
equal(op(e3,e1),e0),
file('ALG187+1.p',unknown),
[] ).
cnf(28,axiom,
equal(op(e3,e2),e4),
file('ALG187+1.p',unknown),
[] ).
cnf(29,axiom,
equal(op(e3,e3),e2),
file('ALG187+1.p',unknown),
[] ).
cnf(30,axiom,
equal(op(e3,e4),e1),
file('ALG187+1.p',unknown),
[] ).
cnf(31,axiom,
equal(op(e4,e0),e2),
file('ALG187+1.p',unknown),
[] ).
cnf(32,axiom,
equal(op(e4,e1),e3),
file('ALG187+1.p',unknown),
[] ).
cnf(33,axiom,
equal(op(e4,e2),e1),
file('ALG187+1.p',unknown),
[] ).
cnf(34,axiom,
equal(op(e4,e3),e4),
file('ALG187+1.p',unknown),
[] ).
cnf(35,axiom,
equal(op(e4,e4),e0),
file('ALG187+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ equal(op(e0,e0),e4)
| skC1 ),
file('ALG187+1.p',unknown),
[] ).
cnf(43,axiom,
( ~ equal(op(e0,e1),e2)
| skC2 ),
file('ALG187+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ equal(op(e0,e2),e0)
| skC3 ),
file('ALG187+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ equal(op(e0,e3),e1)
| skC4 ),
file('ALG187+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ equal(op(e0,e4),e3)
| skC5 ),
file('ALG187+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ equal(op(e1,e0),e0)
| skC6 ),
file('ALG187+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ equal(op(e1,e1),e1)
| skC7 ),
file('ALG187+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ equal(op(e1,e2),e2)
| skC8 ),
file('ALG187+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ equal(op(e1,e3),e3)
| skC9 ),
file('ALG187+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ equal(op(e1,e4),e4)
| skC10 ),
file('ALG187+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ equal(op(e2,e0),e1)
| skC11 ),
file('ALG187+1.p',unknown),
[] ).
cnf(95,axiom,
( ~ equal(op(e2,e1),e4)
| skC12 ),
file('ALG187+1.p',unknown),
[] ).
cnf(99,axiom,
( ~ equal(op(e2,e2),e3)
| skC13 ),
file('ALG187+1.p',unknown),
[] ).
cnf(101,axiom,
( ~ equal(op(e2,e3),e0)
| skC14 ),
file('ALG187+1.p',unknown),
[] ).
cnf(108,axiom,
( ~ equal(op(e2,e4),e2)
| skC15 ),
file('ALG187+1.p',unknown),
[] ).
cnf(114,axiom,
( ~ equal(op(e3,e0),e3)
| skC16 ),
file('ALG187+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ equal(op(e3,e1),e0)
| skC17 ),
file('ALG187+1.p',unknown),
[] ).
cnf(125,axiom,
( ~ equal(op(e3,e2),e4)
| skC18 ),
file('ALG187+1.p',unknown),
[] ).
cnf(128,axiom,
( ~ equal(op(e3,e3),e2)
| skC19 ),
file('ALG187+1.p',unknown),
[] ).
cnf(132,axiom,
( ~ equal(op(e3,e4),e1)
| skC20 ),
file('ALG187+1.p',unknown),
[] ).
cnf(138,axiom,
( ~ equal(op(e4,e0),e2)
| skC21 ),
file('ALG187+1.p',unknown),
[] ).
cnf(144,axiom,
( ~ equal(op(e4,e1),e3)
| skC22 ),
file('ALG187+1.p',unknown),
[] ).
cnf(147,axiom,
( ~ equal(op(e4,e2),e1)
| skC23 ),
file('ALG187+1.p',unknown),
[] ).
cnf(155,axiom,
( ~ equal(op(e4,e3),e4)
| skC24 ),
file('ALG187+1.p',unknown),
[] ).
cnf(156,axiom,
( ~ equal(op(e4,e4),e0)
| skC25 ),
file('ALG187+1.p',unknown),
[] ).
cnf(163,axiom,
( ~ equal(op(e0,e2),e0)
| skC26 ),
file('ALG187+1.p',unknown),
[] ).
cnf(167,axiom,
( ~ equal(op(e1,e0),e0)
| skC27 ),
file('ALG187+1.p',unknown),
[] ).
cnf(174,axiom,
( ~ equal(op(e0,e3),e1)
| skC28 ),
file('ALG187+1.p',unknown),
[] ).
cnf(178,axiom,
( ~ equal(op(e2,e0),e1)
| skC29 ),
file('ALG187+1.p',unknown),
[] ).
cnf(182,axiom,
( ~ equal(op(e0,e1),e2)
| skC30 ),
file('ALG187+1.p',unknown),
[] ).
cnf(190,axiom,
( ~ equal(op(e4,e0),e2)
| skC31 ),
file('ALG187+1.p',unknown),
[] ).
cnf(195,axiom,
( ~ equal(op(e0,e4),e3)
| skC32 ),
file('ALG187+1.p',unknown),
[] ).
cnf(199,axiom,
( ~ equal(op(e3,e0),e3)
| skC33 ),
file('ALG187+1.p',unknown),
[] ).
cnf(201,axiom,
( ~ equal(op(e0,e0),e4)
| skC34 ),
file('ALG187+1.p',unknown),
[] ).
cnf(206,axiom,
( ~ equal(op(e0,e0),e4)
| skC35 ),
file('ALG187+1.p',unknown),
[] ).
cnf(211,axiom,
( ~ equal(op(e1,e0),e0)
| skC36 ),
file('ALG187+1.p',unknown),
[] ).
cnf(219,axiom,
( ~ equal(op(e3,e1),e0)
| skC37 ),
file('ALG187+1.p',unknown),
[] ).
cnf(222,axiom,
( ~ equal(op(e1,e1),e1)
| skC38 ),
file('ALG187+1.p',unknown),
[] ).
cnf(227,axiom,
( ~ equal(op(e1,e1),e1)
| skC39 ),
file('ALG187+1.p',unknown),
[] ).
cnf(233,axiom,
( ~ equal(op(e1,e2),e2)
| skC40 ),
file('ALG187+1.p',unknown),
[] ).
cnf(236,axiom,
( ~ equal(op(e0,e1),e2)
| skC41 ),
file('ALG187+1.p',unknown),
[] ).
cnf(244,axiom,
( ~ equal(op(e1,e3),e3)
| skC42 ),
file('ALG187+1.p',unknown),
[] ).
cnf(250,axiom,
( ~ equal(op(e4,e1),e3)
| skC43 ),
file('ALG187+1.p',unknown),
[] ).
cnf(255,axiom,
( ~ equal(op(e1,e4),e4)
| skC44 ),
file('ALG187+1.p',unknown),
[] ).
cnf(258,axiom,
( ~ equal(op(e2,e1),e4)
| skC45 ),
file('ALG187+1.p',unknown),
[] ).
cnf(264,axiom,
( ~ equal(op(e2,e3),e0)
| skC46 ),
file('ALG187+1.p',unknown),
[] ).
cnf(266,axiom,
( ~ equal(op(e0,e2),e0)
| skC47 ),
file('ALG187+1.p',unknown),
[] ).
cnf(271,axiom,
( ~ equal(op(e2,e0),e1)
| skC48 ),
file('ALG187+1.p',unknown),
[] ).
cnf(280,axiom,
( ~ equal(op(e4,e2),e1)
| skC49 ),
file('ALG187+1.p',unknown),
[] ).
cnf(285,axiom,
( ~ equal(op(e2,e4),e2)
| skC50 ),
file('ALG187+1.p',unknown),
[] ).
cnf(287,axiom,
( ~ equal(op(e1,e2),e2)
| skC51 ),
file('ALG187+1.p',unknown),
[] ).
cnf(293,axiom,
( ~ equal(op(e2,e2),e3)
| skC52 ),
file('ALG187+1.p',unknown),
[] ).
cnf(298,axiom,
( ~ equal(op(e2,e2),e3)
| skC53 ),
file('ALG187+1.p',unknown),
[] ).
cnf(302,axiom,
( ~ equal(op(e2,e1),e4)
| skC54 ),
file('ALG187+1.p',unknown),
[] ).
cnf(309,axiom,
( ~ equal(op(e3,e2),e4)
| skC55 ),
file('ALG187+1.p',unknown),
[] ).
cnf(312,axiom,
( ~ equal(op(e3,e1),e0)
| skC56 ),
file('ALG187+1.p',unknown),
[] ).
cnf(318,axiom,
( ~ equal(op(e2,e3),e0)
| skC57 ),
file('ALG187+1.p',unknown),
[] ).
cnf(325,axiom,
( ~ equal(op(e3,e4),e1)
| skC58 ),
file('ALG187+1.p',unknown),
[] ).
cnf(326,axiom,
( ~ equal(op(e0,e3),e1)
| skC59 ),
file('ALG187+1.p',unknown),
[] ).
cnf(334,axiom,
( ~ equal(op(e3,e3),e2)
| skC60 ),
file('ALG187+1.p',unknown),
[] ).
cnf(339,axiom,
( ~ equal(op(e3,e3),e2)
| skC61 ),
file('ALG187+1.p',unknown),
[] ).
cnf(341,axiom,
( ~ equal(op(e3,e0),e3)
| skC62 ),
file('ALG187+1.p',unknown),
[] ).
cnf(347,axiom,
( ~ equal(op(e1,e3),e3)
| skC63 ),
file('ALG187+1.p',unknown),
[] ).
cnf(353,axiom,
( ~ equal(op(e3,e2),e4)
| skC64 ),
file('ALG187+1.p',unknown),
[] ).
cnf(360,axiom,
( ~ equal(op(e4,e3),e4)
| skC65 ),
file('ALG187+1.p',unknown),
[] ).
cnf(365,axiom,
( ~ equal(op(e4,e4),e0)
| skC66 ),
file('ALG187+1.p',unknown),
[] ).
cnf(370,axiom,
( ~ equal(op(e4,e4),e0)
| skC67 ),
file('ALG187+1.p',unknown),
[] ).
cnf(373,axiom,
( ~ equal(op(e4,e2),e1)
| skC68 ),
file('ALG187+1.p',unknown),
[] ).
cnf(379,axiom,
( ~ equal(op(e3,e4),e1)
| skC69 ),
file('ALG187+1.p',unknown),
[] ).
cnf(381,axiom,
( ~ equal(op(e4,e0),e2)
| skC70 ),
file('ALG187+1.p',unknown),
[] ).
cnf(388,axiom,
( ~ equal(op(e2,e4),e2)
| skC71 ),
file('ALG187+1.p',unknown),
[] ).
cnf(392,axiom,
( ~ equal(op(e4,e1),e3)
| skC72 ),
file('ALG187+1.p',unknown),
[] ).
cnf(396,axiom,
( ~ equal(op(e0,e4),e3)
| skC73 ),
file('ALG187+1.p',unknown),
[] ).
cnf(404,axiom,
( ~ equal(op(e4,e3),e4)
| skC74 ),
file('ALG187+1.p',unknown),
[] ).
cnf(406,axiom,
( equal(op(e4,e0),e0)
| equal(op(e4,e1),e1)
| equal(op(e4,e2),e2)
| equal(op(e4,e3),e3)
| equal(op(e4,e4),e4)
| skC0 ),
file('ALG187+1.p',unknown),
[] ).
cnf(414,axiom,
( ~ equal(op(e1,e4),e4)
| ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ skC36
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41
| ~ skC42
| ~ skC43
| ~ skC44
| ~ skC45
| ~ skC46
| ~ skC47
| ~ skC48
| ~ skC49
| ~ skC50
| ~ skC51
| ~ skC52
| ~ skC53
| ~ skC54
| ~ skC55
| ~ skC56
| ~ skC57
| ~ skC58
| ~ skC59
| ~ skC60
| ~ skC61
| ~ skC62
| ~ skC63
| ~ skC64
| ~ skC65
| ~ skC66
| ~ skC67
| ~ skC68
| ~ skC69
| ~ skC70
| ~ skC71
| ~ skC72
| ~ skC73
| ~ skC74
| ~ equal(op(op(e0,e0),op(e0,e0)),e0)
| ~ equal(op(op(e1,e0),op(e0,e1)),e0)
| ~ equal(op(op(e2,e0),op(e0,e2)),e0)
| ~ equal(op(op(e3,e0),op(e0,e3)),e0)
| ~ equal(op(op(e4,e0),op(e0,e4)),e0)
| ~ equal(op(op(e0,e1),op(e1,e0)),e1)
| ~ equal(op(op(e1,e1),op(e1,e1)),e1)
| ~ equal(op(op(e2,e1),op(e1,e2)),e1)
| ~ equal(op(op(e3,e1),op(e1,e3)),e1)
| ~ equal(op(op(e4,e1),op(e1,e4)),e1)
| ~ equal(op(op(e0,e2),op(e2,e0)),e2)
| ~ equal(op(op(e1,e2),op(e2,e1)),e2)
| ~ equal(op(op(e2,e2),op(e2,e2)),e2)
| ~ equal(op(op(e3,e2),op(e2,e3)),e2)
| ~ equal(op(op(e4,e2),op(e2,e4)),e2)
| ~ equal(op(op(e0,e3),op(e3,e0)),e3)
| ~ equal(op(op(e1,e3),op(e3,e1)),e3)
| ~ equal(op(op(e2,e3),op(e3,e2)),e3)
| ~ equal(op(op(e3,e3),op(e3,e3)),e3)
| ~ equal(op(op(e4,e3),op(e3,e4)),e3)
| ~ equal(op(op(e0,e4),op(e4,e0)),e4)
| ~ equal(op(op(e1,e4),op(e4,e1)),e4)
| ~ equal(op(op(e2,e4),op(e4,e2)),e4)
| ~ equal(op(op(e3,e4),op(e4,e3)),e4)
| ~ equal(op(op(e4,e4),op(e4,e4)),e4) ),
file('ALG187+1.p',unknown),
[] ).
cnf(417,plain,
( ~ equal(e4,e4)
| skC74 ),
inference(rew,[status(thm),theory(equality)],[34,404]),
[iquote('0:Rew:34.0,404.0')] ).
cnf(418,plain,
skC74,
inference(obv,[status(thm),theory(equality)],[417]),
[iquote('0:Obv:417.0')] ).
cnf(423,plain,
( ~ equal(e3,e3)
| skC73 ),
inference(rew,[status(thm),theory(equality)],[15,396]),
[iquote('0:Rew:15.0,396.0')] ).
cnf(424,plain,
skC73,
inference(obv,[status(thm),theory(equality)],[423]),
[iquote('0:Obv:423.0')] ).
cnf(428,plain,
( ~ equal(e3,e3)
| skC72 ),
inference(rew,[status(thm),theory(equality)],[32,392]),
[iquote('0:Rew:32.0,392.0')] ).
cnf(429,plain,
skC72,
inference(obv,[status(thm),theory(equality)],[428]),
[iquote('0:Obv:428.0')] ).
cnf(432,plain,
( ~ equal(e2,e2)
| skC71 ),
inference(rew,[status(thm),theory(equality)],[25,388]),
[iquote('0:Rew:25.0,388.0')] ).
cnf(433,plain,
skC71,
inference(obv,[status(thm),theory(equality)],[432]),
[iquote('0:Obv:432.0')] ).
cnf(438,plain,
( ~ equal(e2,e2)
| skC70 ),
inference(rew,[status(thm),theory(equality)],[31,381]),
[iquote('0:Rew:31.0,381.0')] ).
cnf(439,plain,
skC70,
inference(obv,[status(thm),theory(equality)],[438]),
[iquote('0:Obv:438.0')] ).
cnf(441,plain,
( ~ equal(e1,e1)
| skC69 ),
inference(rew,[status(thm),theory(equality)],[30,379]),
[iquote('0:Rew:30.0,379.0')] ).
cnf(442,plain,
skC69,
inference(obv,[status(thm),theory(equality)],[441]),
[iquote('0:Obv:441.0')] ).
cnf(445,plain,
( ~ equal(e1,e1)
| skC68 ),
inference(rew,[status(thm),theory(equality)],[33,373]),
[iquote('0:Rew:33.0,373.0')] ).
cnf(446,plain,
skC68,
inference(obv,[status(thm),theory(equality)],[445]),
[iquote('0:Obv:445.0')] ).
cnf(447,plain,
( ~ equal(e0,e0)
| skC67 ),
inference(rew,[status(thm),theory(equality)],[35,370]),
[iquote('0:Rew:35.0,370.0')] ).
cnf(448,plain,
skC67,
inference(obv,[status(thm),theory(equality)],[447]),
[iquote('0:Obv:447.0')] ).
cnf(449,plain,
( ~ equal(e0,e0)
| skC66 ),
inference(rew,[status(thm),theory(equality)],[35,365]),
[iquote('0:Rew:35.0,365.0')] ).
cnf(450,plain,
skC66,
inference(obv,[status(thm),theory(equality)],[449]),
[iquote('0:Obv:449.0')] ).
cnf(451,plain,
( ~ equal(e4,e4)
| skC65 ),
inference(rew,[status(thm),theory(equality)],[34,360]),
[iquote('0:Rew:34.0,360.0')] ).
cnf(452,plain,
skC65,
inference(obv,[status(thm),theory(equality)],[451]),
[iquote('0:Obv:451.0')] ).
cnf(455,plain,
( ~ equal(e4,e4)
| skC64 ),
inference(rew,[status(thm),theory(equality)],[28,353]),
[iquote('0:Rew:28.0,353.0')] ).
cnf(456,plain,
skC64,
inference(obv,[status(thm),theory(equality)],[455]),
[iquote('0:Obv:455.0')] ).
cnf(460,plain,
( ~ equal(e3,e3)
| skC63 ),
inference(rew,[status(thm),theory(equality)],[19,347]),
[iquote('0:Rew:19.0,347.0')] ).
cnf(461,plain,
skC63,
inference(obv,[status(thm),theory(equality)],[460]),
[iquote('0:Obv:460.0')] ).
cnf(466,plain,
( ~ equal(e3,e3)
| skC62 ),
inference(rew,[status(thm),theory(equality)],[26,341]),
[iquote('0:Rew:26.0,341.0')] ).
cnf(467,plain,
skC62,
inference(obv,[status(thm),theory(equality)],[466]),
[iquote('0:Obv:466.0')] ).
cnf(469,plain,
( ~ equal(e2,e2)
| skC61 ),
inference(rew,[status(thm),theory(equality)],[29,339]),
[iquote('0:Rew:29.0,339.0')] ).
cnf(470,plain,
skC61,
inference(obv,[status(thm),theory(equality)],[469]),
[iquote('0:Obv:469.0')] ).
cnf(472,plain,
( ~ equal(e2,e2)
| skC60 ),
inference(rew,[status(thm),theory(equality)],[29,334]),
[iquote('0:Rew:29.0,334.0')] ).
cnf(473,plain,
skC60,
inference(obv,[status(thm),theory(equality)],[472]),
[iquote('0:Obv:472.0')] ).
cnf(478,plain,
( ~ equal(e1,e1)
| skC59 ),
inference(rew,[status(thm),theory(equality)],[14,326]),
[iquote('0:Rew:14.0,326.0')] ).
cnf(479,plain,
skC59,
inference(obv,[status(thm),theory(equality)],[478]),
[iquote('0:Obv:478.0')] ).
cnf(480,plain,
( ~ equal(e1,e1)
| skC58 ),
inference(rew,[status(thm),theory(equality)],[30,325]),
[iquote('0:Rew:30.0,325.0')] ).
cnf(481,plain,
skC58,
inference(obv,[status(thm),theory(equality)],[480]),
[iquote('0:Obv:480.0')] ).
cnf(484,plain,
( ~ equal(e0,e0)
| skC57 ),
inference(rew,[status(thm),theory(equality)],[24,318]),
[iquote('0:Rew:24.0,318.0')] ).
cnf(485,plain,
skC57,
inference(obv,[status(thm),theory(equality)],[484]),
[iquote('0:Obv:484.0')] ).
cnf(489,plain,
( ~ equal(e0,e0)
| skC56 ),
inference(rew,[status(thm),theory(equality)],[27,312]),
[iquote('0:Rew:27.0,312.0')] ).
cnf(490,plain,
skC56,
inference(obv,[status(thm),theory(equality)],[489]),
[iquote('0:Obv:489.0')] ).
cnf(492,plain,
( ~ equal(e4,e4)
| skC55 ),
inference(rew,[status(thm),theory(equality)],[28,309]),
[iquote('0:Rew:28.0,309.0')] ).
cnf(493,plain,
skC55,
inference(obv,[status(thm),theory(equality)],[492]),
[iquote('0:Obv:492.0')] ).
cnf(497,plain,
( ~ equal(e4,e4)
| skC54 ),
inference(rew,[status(thm),theory(equality)],[22,302]),
[iquote('0:Rew:22.0,302.0')] ).
cnf(498,plain,
skC54,
inference(obv,[status(thm),theory(equality)],[497]),
[iquote('0:Obv:497.0')] ).
cnf(501,plain,
( ~ equal(e3,e3)
| skC53 ),
inference(rew,[status(thm),theory(equality)],[23,298]),
[iquote('0:Rew:23.0,298.0')] ).
cnf(502,plain,
skC53,
inference(obv,[status(thm),theory(equality)],[501]),
[iquote('0:Obv:501.0')] ).
cnf(505,plain,
( ~ equal(e3,e3)
| skC52 ),
inference(rew,[status(thm),theory(equality)],[23,293]),
[iquote('0:Rew:23.0,293.0')] ).
cnf(506,plain,
skC52,
inference(obv,[status(thm),theory(equality)],[505]),
[iquote('0:Obv:505.0')] ).
cnf(510,plain,
( ~ equal(e2,e2)
| skC51 ),
inference(rew,[status(thm),theory(equality)],[18,287]),
[iquote('0:Rew:18.0,287.0')] ).
cnf(511,plain,
skC51,
inference(obv,[status(thm),theory(equality)],[510]),
[iquote('0:Obv:510.0')] ).
cnf(512,plain,
( ~ equal(e2,e2)
| skC50 ),
inference(rew,[status(thm),theory(equality)],[25,285]),
[iquote('0:Rew:25.0,285.0')] ).
cnf(513,plain,
skC50,
inference(obv,[status(thm),theory(equality)],[512]),
[iquote('0:Obv:512.0')] ).
cnf(514,plain,
( ~ equal(e1,e1)
| skC49 ),
inference(rew,[status(thm),theory(equality)],[33,280]),
[iquote('0:Rew:33.0,280.0')] ).
cnf(515,plain,
skC49,
inference(obv,[status(thm),theory(equality)],[514]),
[iquote('0:Obv:514.0')] ).
cnf(520,plain,
( ~ equal(e1,e1)
| skC48 ),
inference(rew,[status(thm),theory(equality)],[21,271]),
[iquote('0:Rew:21.0,271.0')] ).
cnf(521,plain,
skC48,
inference(obv,[status(thm),theory(equality)],[520]),
[iquote('0:Obv:520.0')] ).
cnf(526,plain,
( ~ equal(e0,e0)
| skC47 ),
inference(rew,[status(thm),theory(equality)],[13,266]),
[iquote('0:Rew:13.0,266.0')] ).
cnf(527,plain,
skC47,
inference(obv,[status(thm),theory(equality)],[526]),
[iquote('0:Obv:526.0')] ).
cnf(529,plain,
( ~ equal(e0,e0)
| skC46 ),
inference(rew,[status(thm),theory(equality)],[24,264]),
[iquote('0:Rew:24.0,264.0')] ).
cnf(530,plain,
skC46,
inference(obv,[status(thm),theory(equality)],[529]),
[iquote('0:Obv:529.0')] ).
cnf(533,plain,
( ~ equal(e4,e4)
| skC45 ),
inference(rew,[status(thm),theory(equality)],[22,258]),
[iquote('0:Rew:22.0,258.0')] ).
cnf(534,plain,
skC45,
inference(obv,[status(thm),theory(equality)],[533]),
[iquote('0:Obv:533.0')] ).
cnf(535,plain,
( ~ equal(e4,e4)
| skC44 ),
inference(rew,[status(thm),theory(equality)],[20,255]),
[iquote('0:Rew:20.0,255.0')] ).
cnf(536,plain,
skC44,
inference(obv,[status(thm),theory(equality)],[535]),
[iquote('0:Obv:535.0')] ).
cnf(537,plain,
( ~ equal(e3,e3)
| skC43 ),
inference(rew,[status(thm),theory(equality)],[32,250]),
[iquote('0:Rew:32.0,250.0')] ).
cnf(538,plain,
skC43,
inference(obv,[status(thm),theory(equality)],[537]),
[iquote('0:Obv:537.0')] ).
cnf(540,plain,
( ~ equal(e3,e3)
| skC42 ),
inference(rew,[status(thm),theory(equality)],[19,244]),
[iquote('0:Rew:19.0,244.0')] ).
cnf(541,plain,
skC42,
inference(obv,[status(thm),theory(equality)],[540]),
[iquote('0:Obv:540.0')] ).
cnf(546,plain,
( ~ equal(e2,e2)
| skC41 ),
inference(rew,[status(thm),theory(equality)],[12,236]),
[iquote('0:Rew:12.0,236.0')] ).
cnf(547,plain,
skC41,
inference(obv,[status(thm),theory(equality)],[546]),
[iquote('0:Obv:546.0')] ).
cnf(550,plain,
( ~ equal(e2,e2)
| skC40 ),
inference(rew,[status(thm),theory(equality)],[18,233]),
[iquote('0:Rew:18.0,233.0')] ).
cnf(551,plain,
skC40,
inference(obv,[status(thm),theory(equality)],[550]),
[iquote('0:Obv:550.0')] ).
cnf(555,plain,
( ~ equal(e1,e1)
| skC39 ),
inference(rew,[status(thm),theory(equality)],[17,227]),
[iquote('0:Rew:17.0,227.0')] ).
cnf(556,plain,
skC39,
inference(obv,[status(thm),theory(equality)],[555]),
[iquote('0:Obv:555.0')] ).
cnf(560,plain,
( ~ equal(e1,e1)
| skC38 ),
inference(rew,[status(thm),theory(equality)],[17,222]),
[iquote('0:Rew:17.0,222.0')] ).
cnf(561,plain,
skC38,
inference(obv,[status(thm),theory(equality)],[560]),
[iquote('0:Obv:560.0')] ).
cnf(563,plain,
( ~ equal(e0,e0)
| skC37 ),
inference(rew,[status(thm),theory(equality)],[27,219]),
[iquote('0:Rew:27.0,219.0')] ).
cnf(564,plain,
skC37,
inference(obv,[status(thm),theory(equality)],[563]),
[iquote('0:Obv:563.0')] ).
cnf(569,plain,
( ~ equal(e0,e0)
| skC36 ),
inference(rew,[status(thm),theory(equality)],[16,211]),
[iquote('0:Rew:16.0,211.0')] ).
cnf(570,plain,
skC36,
inference(obv,[status(thm),theory(equality)],[569]),
[iquote('0:Obv:569.0')] ).
cnf(575,plain,
( ~ equal(e4,e4)
| skC35 ),
inference(rew,[status(thm),theory(equality)],[11,206]),
[iquote('0:Rew:11.0,206.0')] ).
cnf(576,plain,
skC35,
inference(obv,[status(thm),theory(equality)],[575]),
[iquote('0:Obv:575.0')] ).
cnf(581,plain,
( ~ equal(e4,e4)
| skC34 ),
inference(rew,[status(thm),theory(equality)],[11,201]),
[iquote('0:Rew:11.0,201.0')] ).
cnf(582,plain,
skC34,
inference(obv,[status(thm),theory(equality)],[581]),
[iquote('0:Obv:581.0')] ).
cnf(584,plain,
( ~ equal(e3,e3)
| skC33 ),
inference(rew,[status(thm),theory(equality)],[26,199]),
[iquote('0:Rew:26.0,199.0')] ).
cnf(585,plain,
skC33,
inference(obv,[status(thm),theory(equality)],[584]),
[iquote('0:Obv:584.0')] ).
cnf(586,plain,
( ~ equal(e3,e3)
| skC32 ),
inference(rew,[status(thm),theory(equality)],[15,195]),
[iquote('0:Rew:15.0,195.0')] ).
cnf(587,plain,
skC32,
inference(obv,[status(thm),theory(equality)],[586]),
[iquote('0:Obv:586.0')] ).
cnf(588,plain,
( ~ equal(e2,e2)
| skC31 ),
inference(rew,[status(thm),theory(equality)],[31,190]),
[iquote('0:Rew:31.0,190.0')] ).
cnf(589,plain,
skC31,
inference(obv,[status(thm),theory(equality)],[588]),
[iquote('0:Obv:588.0')] ).
cnf(593,plain,
( ~ equal(e2,e2)
| skC30 ),
inference(rew,[status(thm),theory(equality)],[12,182]),
[iquote('0:Rew:12.0,182.0')] ).
cnf(594,plain,
skC30,
inference(obv,[status(thm),theory(equality)],[593]),
[iquote('0:Obv:593.0')] ).
cnf(597,plain,
( ~ equal(e1,e1)
| skC29 ),
inference(rew,[status(thm),theory(equality)],[21,178]),
[iquote('0:Rew:21.0,178.0')] ).
cnf(598,plain,
skC29,
inference(obv,[status(thm),theory(equality)],[597]),
[iquote('0:Obv:597.0')] ).
cnf(600,plain,
( ~ equal(e1,e1)
| skC28 ),
inference(rew,[status(thm),theory(equality)],[14,174]),
[iquote('0:Rew:14.0,174.0')] ).
cnf(601,plain,
skC28,
inference(obv,[status(thm),theory(equality)],[600]),
[iquote('0:Obv:600.0')] ).
cnf(605,plain,
( ~ equal(e0,e0)
| skC27 ),
inference(rew,[status(thm),theory(equality)],[16,167]),
[iquote('0:Rew:16.0,167.0')] ).
cnf(606,plain,
skC27,
inference(obv,[status(thm),theory(equality)],[605]),
[iquote('0:Obv:605.0')] ).
cnf(609,plain,
( ~ equal(e0,e0)
| skC26 ),
inference(rew,[status(thm),theory(equality)],[13,163]),
[iquote('0:Rew:13.0,163.0')] ).
cnf(610,plain,
skC26,
inference(obv,[status(thm),theory(equality)],[609]),
[iquote('0:Obv:609.0')] ).
cnf(615,plain,
( ~ equal(e0,e0)
| skC25 ),
inference(rew,[status(thm),theory(equality)],[35,156]),
[iquote('0:Rew:35.0,156.0')] ).
cnf(616,plain,
skC25,
inference(obv,[status(thm),theory(equality)],[615]),
[iquote('0:Obv:615.0')] ).
cnf(617,plain,
( ~ equal(e4,e4)
| skC24 ),
inference(rew,[status(thm),theory(equality)],[34,155]),
[iquote('0:Rew:34.0,155.0')] ).
cnf(618,plain,
skC24,
inference(obv,[status(thm),theory(equality)],[617]),
[iquote('0:Obv:617.0')] ).
cnf(622,plain,
( ~ equal(e1,e1)
| skC23 ),
inference(rew,[status(thm),theory(equality)],[33,147]),
[iquote('0:Rew:33.0,147.0')] ).
cnf(623,plain,
skC23,
inference(obv,[status(thm),theory(equality)],[622]),
[iquote('0:Obv:622.0')] ).
cnf(625,plain,
( ~ equal(e3,e3)
| skC22 ),
inference(rew,[status(thm),theory(equality)],[32,144]),
[iquote('0:Rew:32.0,144.0')] ).
cnf(626,plain,
skC22,
inference(obv,[status(thm),theory(equality)],[625]),
[iquote('0:Obv:625.0')] ).
cnf(629,plain,
( ~ equal(e2,e2)
| skC21 ),
inference(rew,[status(thm),theory(equality)],[31,138]),
[iquote('0:Rew:31.0,138.0')] ).
cnf(630,plain,
skC21,
inference(obv,[status(thm),theory(equality)],[629]),
[iquote('0:Obv:629.0')] ).
cnf(634,plain,
( ~ equal(e1,e1)
| skC20 ),
inference(rew,[status(thm),theory(equality)],[30,132]),
[iquote('0:Rew:30.0,132.0')] ).
cnf(635,plain,
skC20,
inference(obv,[status(thm),theory(equality)],[634]),
[iquote('0:Obv:634.0')] ).
cnf(638,plain,
( ~ equal(e2,e2)
| skC19 ),
inference(rew,[status(thm),theory(equality)],[29,128]),
[iquote('0:Rew:29.0,128.0')] ).
cnf(639,plain,
skC19,
inference(obv,[status(thm),theory(equality)],[638]),
[iquote('0:Obv:638.0')] ).
cnf(640,plain,
( ~ equal(e4,e4)
| skC18 ),
inference(rew,[status(thm),theory(equality)],[28,125]),
[iquote('0:Rew:28.0,125.0')] ).
cnf(641,plain,
skC18,
inference(obv,[status(thm),theory(equality)],[640]),
[iquote('0:Obv:640.0')] ).
cnf(646,plain,
( ~ equal(e0,e0)
| skC17 ),
inference(rew,[status(thm),theory(equality)],[27,116]),
[iquote('0:Rew:27.0,116.0')] ).
cnf(647,plain,
skC17,
inference(obv,[status(thm),theory(equality)],[646]),
[iquote('0:Obv:646.0')] ).
cnf(649,plain,
( ~ equal(e3,e3)
| skC16 ),
inference(rew,[status(thm),theory(equality)],[26,114]),
[iquote('0:Rew:26.0,114.0')] ).
cnf(650,plain,
skC16,
inference(obv,[status(thm),theory(equality)],[649]),
[iquote('0:Obv:649.0')] ).
cnf(653,plain,
( ~ equal(e2,e2)
| skC15 ),
inference(rew,[status(thm),theory(equality)],[25,108]),
[iquote('0:Rew:25.0,108.0')] ).
cnf(654,plain,
skC15,
inference(obv,[status(thm),theory(equality)],[653]),
[iquote('0:Obv:653.0')] ).
cnf(659,plain,
( ~ equal(e0,e0)
| skC14 ),
inference(rew,[status(thm),theory(equality)],[24,101]),
[iquote('0:Rew:24.0,101.0')] ).
cnf(660,plain,
skC14,
inference(obv,[status(thm),theory(equality)],[659]),
[iquote('0:Obv:659.0')] ).
cnf(662,plain,
( ~ equal(e3,e3)
| skC13 ),
inference(rew,[status(thm),theory(equality)],[23,99]),
[iquote('0:Rew:23.0,99.0')] ).
cnf(663,plain,
skC13,
inference(obv,[status(thm),theory(equality)],[662]),
[iquote('0:Obv:662.0')] ).
cnf(664,plain,
( ~ equal(e4,e4)
| skC12 ),
inference(rew,[status(thm),theory(equality)],[22,95]),
[iquote('0:Rew:22.0,95.0')] ).
cnf(665,plain,
skC12,
inference(obv,[status(thm),theory(equality)],[664]),
[iquote('0:Obv:664.0')] ).
cnf(669,plain,
( ~ equal(e1,e1)
| skC11 ),
inference(rew,[status(thm),theory(equality)],[21,87]),
[iquote('0:Rew:21.0,87.0')] ).
cnf(670,plain,
skC11,
inference(obv,[status(thm),theory(equality)],[669]),
[iquote('0:Obv:669.0')] ).
cnf(671,plain,
( ~ equal(e4,e4)
| skC10 ),
inference(rew,[status(thm),theory(equality)],[20,85]),
[iquote('0:Rew:20.0,85.0')] ).
cnf(672,plain,
skC10,
inference(obv,[status(thm),theory(equality)],[671]),
[iquote('0:Obv:671.0')] ).
cnf(674,plain,
( ~ equal(e3,e3)
| skC9 ),
inference(rew,[status(thm),theory(equality)],[19,79]),
[iquote('0:Rew:19.0,79.0')] ).
cnf(675,plain,
skC9,
inference(obv,[status(thm),theory(equality)],[674]),
[iquote('0:Obv:674.0')] ).
cnf(678,plain,
( ~ equal(e2,e2)
| skC8 ),
inference(rew,[status(thm),theory(equality)],[18,73]),
[iquote('0:Rew:18.0,73.0')] ).
cnf(679,plain,
skC8,
inference(obv,[status(thm),theory(equality)],[678]),
[iquote('0:Obv:678.0')] ).
cnf(683,plain,
( ~ equal(e1,e1)
| skC7 ),
inference(rew,[status(thm),theory(equality)],[17,67]),
[iquote('0:Rew:17.0,67.0')] ).
cnf(684,plain,
skC7,
inference(obv,[status(thm),theory(equality)],[683]),
[iquote('0:Obv:683.0')] ).
cnf(689,plain,
( ~ equal(e0,e0)
| skC6 ),
inference(rew,[status(thm),theory(equality)],[16,61]),
[iquote('0:Rew:16.0,61.0')] ).
cnf(690,plain,
skC6,
inference(obv,[status(thm),theory(equality)],[689]),
[iquote('0:Obv:689.0')] ).
cnf(692,plain,
( ~ equal(e3,e3)
| skC5 ),
inference(rew,[status(thm),theory(equality)],[15,59]),
[iquote('0:Rew:15.0,59.0')] ).
cnf(693,plain,
skC5,
inference(obv,[status(thm),theory(equality)],[692]),
[iquote('0:Obv:692.0')] ).
cnf(697,plain,
( ~ equal(e1,e1)
| skC4 ),
inference(rew,[status(thm),theory(equality)],[14,52]),
[iquote('0:Rew:14.0,52.0')] ).
cnf(698,plain,
skC4,
inference(obv,[status(thm),theory(equality)],[697]),
[iquote('0:Obv:697.0')] ).
cnf(703,plain,
( ~ equal(e0,e0)
| skC3 ),
inference(rew,[status(thm),theory(equality)],[13,46]),
[iquote('0:Rew:13.0,46.0')] ).
cnf(704,plain,
skC3,
inference(obv,[status(thm),theory(equality)],[703]),
[iquote('0:Obv:703.0')] ).
cnf(707,plain,
( ~ equal(e2,e2)
| skC2 ),
inference(rew,[status(thm),theory(equality)],[12,43]),
[iquote('0:Rew:12.0,43.0')] ).
cnf(708,plain,
skC2,
inference(obv,[status(thm),theory(equality)],[707]),
[iquote('0:Obv:707.0')] ).
cnf(709,plain,
( ~ equal(e4,e4)
| skC1 ),
inference(rew,[status(thm),theory(equality)],[11,40]),
[iquote('0:Rew:11.0,40.0')] ).
cnf(710,plain,
skC1,
inference(obv,[status(thm),theory(equality)],[709]),
[iquote('0:Obv:709.0')] ).
cnf(711,plain,
( equal(e2,e0)
| equal(e3,e1)
| equal(e2,e1)
| equal(e4,e3)
| equal(e4,e0)
| skC0 ),
inference(rew,[status(thm),theory(equality)],[35,406,34,33,32,31]),
[iquote('0:Rew:35.0,406.4,34.0,406.3,33.0,406.2,32.0,406.1,31.0,406.0')] ).
cnf(712,plain,
skC0,
inference(mrr,[status(thm)],[711,2,6,5,10,4]),
[iquote('0:MRR:711.0,711.1,711.2,711.3,711.4,2.0,6.0,5.0,10.0,4.0')] ).
cnf(719,plain,
( ~ equal(e4,e4)
| ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ skC36
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41
| ~ skC42
| ~ skC43
| ~ skC44
| ~ skC45
| ~ skC46
| ~ skC47
| ~ skC48
| ~ skC49
| ~ skC50
| ~ skC51
| ~ skC52
| ~ skC53
| ~ skC54
| ~ skC55
| ~ skC56
| ~ skC57
| ~ skC58
| ~ skC59
| ~ skC60
| ~ skC61
| ~ skC62
| ~ skC63
| ~ skC64
| ~ skC65
| ~ skC66
| ~ skC67
| ~ skC68
| ~ skC69
| ~ skC70
| ~ skC71
| ~ skC72
| ~ skC73
| ~ skC74
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e0,e0)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e1,e1)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e2,e2)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e3,e3)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e4,e4)
| ~ equal(e4,e4) ),
inference(rew,[status(thm),theory(equality)],[11,414,35,20,30,34,22,25,33,32,28,15,31,23,29,24,26,19,27,14,18,12,13,21,17,16]),
[iquote('0:Rew:11.0,414.100,35.0,414.100,20.0,414.99,30.0,414.99,34.0,414.99,22.0,414.98,25.0,414.98,33.0,414.98,34.0,414.97,20.0,414.97,32.0,414.97,28.0,414.96,15.0,414.96,31.0,414.96,32.0,414.95,34.0,414.95,30.0,414.95,23.0,414.94,29.0,414.94,15.0,414.93,24.0,414.93,28.0,414.93,26.0,414.92,19.0,414.92,27.0,414.92,19.0,414.91,14.0,414.91,26.0,414.91,18.0,414.90,33.0,414.90,25.0,414.90,31.0,414.89,28.0,414.89,24.0,414.89,29.0,414.88,23.0,414.88,25.0,414.87,18.0,414.87,22.0,414.87,12.0,414.86,13.0,414.86,21.0,414.86,30.0,414.85,32.0,414.85,20.0,414.85,14.0,414.84,27.0,414.84,19.0,414.84,33.0,414.83,22.0,414.83,18.0,414.83,17.0,414.82,17.0,414.82,21.0,414.81,12.0,414.81,16.0,414.81,24.0,414.80,31.0,414.80,15.0,414.80,27.0,414.79,26.0,414.79,14.0,414.79,16.0,414.78,21.0,414.78,13.0,414.78,13.0,414.77,16.0,414.77,12.0,414.77,35.0,414.76,11.0,414.76,20.0,414.0')] ).
cnf(720,plain,
( ~ skC0
| ~ skC1
| ~ skC2
| ~ skC3
| ~ skC4
| ~ skC5
| ~ skC6
| ~ skC7
| ~ skC8
| ~ skC9
| ~ skC10
| ~ skC11
| ~ skC12
| ~ skC13
| ~ skC14
| ~ skC15
| ~ skC16
| ~ skC17
| ~ skC18
| ~ skC19
| ~ skC20
| ~ skC21
| ~ skC22
| ~ skC23
| ~ skC24
| ~ skC25
| ~ skC26
| ~ skC27
| ~ skC28
| ~ skC29
| ~ skC30
| ~ skC31
| ~ skC32
| ~ skC33
| ~ skC34
| ~ skC35
| ~ skC36
| ~ skC37
| ~ skC38
| ~ skC39
| ~ skC40
| ~ skC41
| ~ skC42
| ~ skC43
| ~ skC44
| ~ skC45
| ~ skC46
| ~ skC47
| ~ skC48
| ~ skC49
| ~ skC50
| ~ skC51
| ~ skC52
| ~ skC53
| ~ skC54
| ~ skC55
| ~ skC56
| ~ skC57
| ~ skC58
| ~ skC59
| ~ skC60
| ~ skC61
| ~ skC62
| ~ skC63
| ~ skC64
| ~ skC65
| ~ skC66
| ~ skC67
| ~ skC68
| ~ skC69
| ~ skC70
| ~ skC71
| ~ skC72
| ~ skC73
| ~ skC74 ),
inference(obv,[status(thm),theory(equality)],[719]),
[iquote('0:Obv:719.100')] ).
cnf(721,plain,
$false,
inference(mrr,[status(thm)],[720,712,710,708,704,698,693,690,684,679,675,672,670,665,663,660,654,650,647,641,639,635,630,626,623,618,616,610,606,601,598,594,589,587,585,582,576,570,564,561,556,551,547,541,538,536,534,530,527,521,515,513,511,506,502,498,493,490,485,481,479,473,470,467,461,456,452,450,448,446,442,439,433,429,424,418]),
[iquote('0:MRR:720.0,720.1,720.2,720.3,720.4,720.5,720.6,720.7,720.8,720.9,720.10,720.11,720.12,720.13,720.14,720.15,720.16,720.17,720.18,720.19,720.20,720.21,720.22,720.23,720.24,720.25,720.26,720.27,720.28,720.29,720.30,720.31,720.32,720.33,720.34,720.35,720.36,720.37,720.38,720.39,720.40,720.41,720.42,720.43,720.44,720.45,720.46,720.47,720.48,720.49,720.50,720.51,720.52,720.53,720.54,720.55,720.56,720.57,720.58,720.59,720.60,720.61,720.62,720.63,720.64,720.65,720.66,720.67,720.68,720.69,720.70,720.71,720.72,720.73,720.74,712.0,710.0,708.0,704.0,698.0,693.0,690.0,684.0,679.0,675.0,672.0,670.0,665.0,663.0,660.0,654.0,650.0,647.0,641.0,639.0,635.0,630.0,626.0,623.0,618.0,616.0,610.0,606.0,601.0,598.0,594.0,589.0,587.0,585.0,582.0,576.0,570.0,564.0,561.0,556.0,551.0,547.0,541.0,538.0,536.0,534.0,530.0,527.0,521.0,515.0,513.0,511.0,506.0,502.0,498.0,493.0,490.0,485.0,481.0,479.0,473.0,470.0,467.0,461.0,456.0,452.0,450.0,448.0,446.0,442.0,439.0,433.0,429.0,424.0,418.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ALG187+1 : TPTP v8.1.0. Released v2.7.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n024.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:26:49 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.36/0.55
% 0.36/0.55 SPASS V 3.9
% 0.36/0.55 SPASS beiseite: Proof found.
% 0.36/0.55 % SZS status Theorem
% 0.36/0.55 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.55 SPASS derived 0 clauses, backtracked 0 clauses, performed 0 splits and kept 111 clauses.
% 0.36/0.55 SPASS allocated 86597 KBytes.
% 0.36/0.55 SPASS spent 0:00:00.21 on the problem.
% 0.36/0.55 0:00:00.04 for the input.
% 0.36/0.55 0:00:00.12 for the FLOTTER CNF translation.
% 0.36/0.55 0:00:00.00 for inferences.
% 0.36/0.55 0:00:00.00 for the backtracking.
% 0.36/0.55 0:00:00.02 for the reduction.
% 0.36/0.55
% 0.36/0.55
% 0.36/0.55 Here is a proof with depth 0, length 259 :
% 0.36/0.55 % SZS output start Refutation
% See solution above
% 0.36/0.56 Formulae used in the proof : ax1 ax2 co1
% 0.36/0.56
%------------------------------------------------------------------------------