%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG016+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 14 18:01:58 EDT 2022
% Result : Theorem 0.37s 0.56s
% Output : Refutation 0.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 54
% Syntax : Number of clauses : 181 ( 168 unt; 4 nHn; 181 RR)
% Number of literals : 239 ( 0 equ; 61 neg)
% Maximal clause size : 20 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 4 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(33,axiom,
equal(h3(e12),e22),
file('ALG016+1.p',unknown),
[] ).
cnf(59,axiom,
equal(op1(e12,e12),e13),
file('ALG016+1.p',unknown),
[] ).
cnf(60,axiom,
equal(op2(e22,e22),e23),
file('ALG016+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ equal(h3(e10),e20)
| skC6 ),
file('ALG016+1.p',unknown),
[] ).
cnf(90,axiom,
( ~ equal(h3(e11),e21)
| skC7 ),
file('ALG016+1.p',unknown),
[] ).
cnf(95,axiom,
( ~ equal(h3(e12),e22)
| skC8 ),
file('ALG016+1.p',unknown),
[] ).
cnf(137,axiom,
equal(op2(e20,e20),h1(e13)),
file('ALG016+1.p',unknown),
[] ).
cnf(138,axiom,
equal(op2(e21,e21),h2(e13)),
file('ALG016+1.p',unknown),
[] ).
cnf(139,axiom,
equal(op2(e22,e22),h3(e13)),
file('ALG016+1.p',unknown),
[] ).
cnf(140,axiom,
equal(op2(e23,e23),h4(e13)),
file('ALG016+1.p',unknown),
[] ).
cnf(141,axiom,
equal(op1(e12,op1(e12,e12)),e11),
file('ALG016+1.p',unknown),
[] ).
cnf(142,axiom,
equal(op2(e22,op2(e22,e22)),e21),
file('ALG016+1.p',unknown),
[] ).
cnf(155,axiom,
~ equal(op1(e11,e12),op1(e10,e12)),
file('ALG016+1.p',unknown),
[] ).
cnf(156,axiom,
~ equal(op1(e12,e12),op1(e10,e12)),
file('ALG016+1.p',unknown),
[] ).
cnf(157,axiom,
~ equal(op1(e13,e12),op1(e10,e12)),
file('ALG016+1.p',unknown),
[] ).
cnf(203,axiom,
~ equal(op2(e21,e22),op2(e20,e22)),
file('ALG016+1.p',unknown),
[] ).
cnf(204,axiom,
~ equal(op2(e22,e22),op2(e20,e22)),
file('ALG016+1.p',unknown),
[] ).
cnf(205,axiom,
~ equal(op2(e23,e22),op2(e20,e22)),
file('ALG016+1.p',unknown),
[] ).
cnf(241,axiom,
equal(op2(e22,op2(e22,e22)),h3(e11)),
file('ALG016+1.p',unknown),
[] ).
cnf(242,axiom,
equal(op2(e23,op2(e23,e23)),h4(e11)),
file('ALG016+1.p',unknown),
[] ).
cnf(267,axiom,
equal(op1(op1(e12,op1(e12,e12)),e12),e10),
file('ALG016+1.p',unknown),
[] ).
cnf(268,axiom,
equal(op2(op2(e22,op2(e22,e22)),e22),e20),
file('ALG016+1.p',unknown),
[] ).
cnf(271,axiom,
equal(op2(op2(e22,op2(e22,e22)),e22),h3(e10)),
file('ALG016+1.p',unknown),
[] ).
cnf(306,axiom,
equal(op1(op1(e12,e10),e11),op1(e12,op1(e10,e11))),
file('ALG016+1.p',unknown),
[] ).
cnf(309,axiom,
equal(op1(op1(e12,e11),e10),op1(e12,op1(e11,e10))),
file('ALG016+1.p',unknown),
[] ).
cnf(310,axiom,
equal(op1(op1(e12,e11),e11),op1(e12,op1(e11,e11))),
file('ALG016+1.p',unknown),
[] ).
cnf(311,axiom,
equal(op1(op1(e12,e11),e12),op1(e12,op1(e11,e12))),
file('ALG016+1.p',unknown),
[] ).
cnf(312,axiom,
equal(op1(op1(e12,e11),e13),op1(e12,op1(e11,e13))),
file('ALG016+1.p',unknown),
[] ).
cnf(315,axiom,
equal(op1(op1(e12,e12),e12),op1(e12,op1(e12,e12))),
file('ALG016+1.p',unknown),
[] ).
cnf(316,axiom,
equal(op1(op1(e12,e12),e13),op1(e12,op1(e12,e13))),
file('ALG016+1.p',unknown),
[] ).
cnf(317,axiom,
equal(op1(op1(e12,e13),e10),op1(e12,op1(e13,e10))),
file('ALG016+1.p',unknown),
[] ).
cnf(318,axiom,
equal(op1(op1(e12,e13),e11),op1(e12,op1(e13,e11))),
file('ALG016+1.p',unknown),
[] ).
cnf(319,axiom,
equal(op1(op1(e12,e13),e12),op1(e12,op1(e13,e12))),
file('ALG016+1.p',unknown),
[] ).
cnf(320,axiom,
equal(op1(op1(e12,e13),e13),op1(e12,op1(e13,e13))),
file('ALG016+1.p',unknown),
[] ).
cnf(327,axiom,
equal(op1(op1(e13,e11),e12),op1(e13,op1(e11,e12))),
file('ALG016+1.p',unknown),
[] ).
cnf(329,axiom,
equal(op1(op1(e13,e12),e10),op1(e13,op1(e12,e10))),
file('ALG016+1.p',unknown),
[] ).
cnf(330,axiom,
equal(op1(op1(e13,e12),e11),op1(e13,op1(e12,e11))),
file('ALG016+1.p',unknown),
[] ).
cnf(332,axiom,
equal(op1(op1(e13,e12),e13),op1(e13,op1(e12,e13))),
file('ALG016+1.p',unknown),
[] ).
cnf(379,axiom,
equal(op2(op2(e22,e22),e22),op2(e22,op2(e22,e22))),
file('ALG016+1.p',unknown),
[] ).
cnf(380,axiom,
equal(op2(op2(e22,e22),e23),op2(e22,op2(e22,e23))),
file('ALG016+1.p',unknown),
[] ).
cnf(383,axiom,
equal(op2(op2(e22,e23),e22),op2(e22,op2(e23,e22))),
file('ALG016+1.p',unknown),
[] ).
cnf(384,axiom,
equal(op2(op2(e22,e23),e23),op2(e22,op2(e23,e23))),
file('ALG016+1.p',unknown),
[] ).
cnf(390,axiom,
equal(op2(op2(e23,e21),e21),op2(e23,op2(e21,e21))),
file('ALG016+1.p',unknown),
[] ).
cnf(391,axiom,
equal(op2(op2(e23,e21),e22),op2(e23,op2(e21,e22))),
file('ALG016+1.p',unknown),
[] ).
cnf(393,axiom,
equal(op2(op2(e23,e22),e20),op2(e23,op2(e22,e20))),
file('ALG016+1.p',unknown),
[] ).
cnf(394,axiom,
equal(op2(op2(e23,e22),e21),op2(e23,op2(e22,e21))),
file('ALG016+1.p',unknown),
[] ).
cnf(396,axiom,
equal(op2(op2(e23,e22),e23),op2(e23,op2(e22,e23))),
file('ALG016+1.p',unknown),
[] ).
cnf(397,axiom,
equal(op2(op2(e23,e23),e20),op2(e23,op2(e23,e20))),
file('ALG016+1.p',unknown),
[] ).
cnf(398,axiom,
equal(op2(op2(e23,e23),e21),op2(e23,op2(e23,e21))),
file('ALG016+1.p',unknown),
[] ).
cnf(399,axiom,
equal(op2(op2(e23,e23),e22),op2(e23,op2(e23,e22))),
file('ALG016+1.p',unknown),
[] ).
cnf(400,axiom,
equal(op2(op2(e23,e23),e23),op2(e23,op2(e23,e23))),
file('ALG016+1.p',unknown),
[] ).
cnf(413,axiom,
( equal(op2(e23,e21),e20)
| equal(op2(e23,e21),e21)
| equal(op2(e23,e21),e22)
| equal(op2(e23,e21),e23) ),
file('ALG016+1.p',unknown),
[] ).
cnf(429,axiom,
( equal(op1(e13,e11),e10)
| equal(op1(e13,e11),e11)
| equal(op1(e13,e11),e12)
| equal(op1(e13,e11),e13) ),
file('ALG016+1.p',unknown),
[] ).
cnf(455,axiom,
( ~ equal(h3(e13),e23)
| ~ equal(op2(h3(e10),h3(e10)),h3(op1(e10,e10)))
| ~ equal(op2(h3(e10),h3(e11)),h3(op1(e10,e11)))
| ~ equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12)))
| ~ equal(op2(h3(e10),h3(e13)),h3(op1(e10,e13)))
| ~ equal(op2(h3(e11),h3(e10)),h3(op1(e11,e10)))
| ~ equal(op2(h3(e11),h3(e11)),h3(op1(e11,e11)))
| ~ equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12)))
| ~ equal(op2(h3(e11),h3(e13)),h3(op1(e11,e13)))
| ~ equal(op2(h3(e12),h3(e10)),h3(op1(e12,e10)))
| ~ equal(op2(h3(e12),h3(e11)),h3(op1(e12,e11)))
| ~ equal(op2(h3(e12),h3(e12)),h3(op1(e12,e12)))
| ~ equal(op2(h3(e12),h3(e13)),h3(op1(e12,e13)))
| ~ equal(op2(h3(e13),h3(e10)),h3(op1(e13,e10)))
| ~ equal(op2(h3(e13),h3(e11)),h3(op1(e13,e11)))
| ~ equal(op2(h3(e13),h3(e12)),h3(op1(e13,e12)))
| ~ equal(op2(h3(e13),h3(e13)),h3(op1(e13,e13)))
| ~ skC6
| ~ skC7
| ~ skC8 ),
file('ALG016+1.p',unknown),
[] ).
cnf(467,plain,
equal(h3(e13),e23),
inference(rew,[status(thm),theory(equality)],[60,139]),
[iquote('0:Rew:60.0,139.0')] ).
cnf(472,plain,
( ~ equal(e22,e22)
| skC8 ),
inference(rew,[status(thm),theory(equality)],[33,95]),
[iquote('0:Rew:33.0,95.0')] ).
cnf(473,plain,
skC8,
inference(obv,[status(thm),theory(equality)],[472]),
[iquote('0:Obv:472.0')] ).
cnf(486,plain,
equal(op2(e22,e23),e21),
inference(rew,[status(thm),theory(equality)],[60,142]),
[iquote('0:Rew:60.0,142.0')] ).
cnf(487,plain,
equal(op1(e12,e13),e11),
inference(rew,[status(thm),theory(equality)],[59,141]),
[iquote('0:Rew:59.0,141.0')] ).
cnf(488,plain,
equal(op2(e23,h4(e13)),h4(e11)),
inference(rew,[status(thm),theory(equality)],[140,242]),
[iquote('0:Rew:140.0,242.0')] ).
cnf(489,plain,
equal(h3(e11),e21),
inference(rew,[status(thm),theory(equality)],[486,241,60]),
[iquote('0:Rew:486.0,241.0,60.0,241.0')] ).
cnf(490,plain,
( ~ equal(e21,e21)
| skC7 ),
inference(rew,[status(thm),theory(equality)],[489,90]),
[iquote('0:Rew:489.0,90.0')] ).
cnf(492,plain,
skC7,
inference(obv,[status(thm),theory(equality)],[490]),
[iquote('0:Obv:490.0')] ).
cnf(516,plain,
~ equal(op2(e20,e22),e23),
inference(rew,[status(thm),theory(equality)],[60,204]),
[iquote('0:Rew:60.0,204.0')] ).
cnf(533,plain,
~ equal(op1(e10,e12),e13),
inference(rew,[status(thm),theory(equality)],[59,156]),
[iquote('0:Rew:59.0,156.0')] ).
cnf(534,plain,
equal(op2(e21,e22),e20),
inference(rew,[status(thm),theory(equality)],[486,268,60]),
[iquote('0:Rew:486.0,268.0,60.0,268.0')] ).
cnf(540,plain,
~ equal(op2(e20,e22),e20),
inference(rew,[status(thm),theory(equality)],[534,203]),
[iquote('0:Rew:534.0,203.0')] ).
cnf(541,plain,
equal(op1(e11,e12),e10),
inference(rew,[status(thm),theory(equality)],[487,267,59]),
[iquote('0:Rew:487.0,267.0,59.0,267.0')] ).
cnf(547,plain,
~ equal(op1(e10,e12),e10),
inference(rew,[status(thm),theory(equality)],[541,155]),
[iquote('0:Rew:541.0,155.0')] ).
cnf(549,plain,
equal(h3(e10),e20),
inference(rew,[status(thm),theory(equality)],[534,271,486,60]),
[iquote('0:Rew:534.0,271.0,486.0,271.0,60.0,271.0')] ).
cnf(550,plain,
( ~ equal(e20,e20)
| skC6 ),
inference(rew,[status(thm),theory(equality)],[549,85]),
[iquote('0:Rew:549.0,85.0')] ).
cnf(551,plain,
skC6,
inference(obv,[status(thm),theory(equality)],[550]),
[iquote('0:Obv:550.0')] ).
cnf(554,plain,
equal(op2(h4(e13),e23),h4(e11)),
inference(rew,[status(thm),theory(equality)],[488,400,140]),
[iquote('0:Rew:488.0,400.0,140.0,400.0')] ).
cnf(555,plain,
equal(op2(e23,op2(e23,e22)),op2(h4(e13),e22)),
inference(rew,[status(thm),theory(equality)],[140,399]),
[iquote('0:Rew:140.0,399.0')] ).
cnf(556,plain,
equal(op2(e23,op2(e23,e21)),op2(h4(e13),e21)),
inference(rew,[status(thm),theory(equality)],[140,398]),
[iquote('0:Rew:140.0,398.0')] ).
cnf(557,plain,
equal(op2(e23,op2(e23,e20)),op2(h4(e13),e20)),
inference(rew,[status(thm),theory(equality)],[140,397]),
[iquote('0:Rew:140.0,397.0')] ).
cnf(558,plain,
equal(op2(op2(e23,e22),e23),op2(e23,e21)),
inference(rew,[status(thm),theory(equality)],[486,396]),
[iquote('0:Rew:486.0,396.0')] ).
cnf(560,plain,
equal(op2(op2(e23,e21),e22),op2(e23,e20)),
inference(rew,[status(thm),theory(equality)],[534,391]),
[iquote('0:Rew:534.0,391.0')] ).
cnf(561,plain,
equal(op2(op2(e23,e21),e21),op2(e23,h2(e13))),
inference(rew,[status(thm),theory(equality)],[138,390]),
[iquote('0:Rew:138.0,390.0')] ).
cnf(563,plain,
equal(op2(e22,h4(e13)),op2(e21,e23)),
inference(rew,[status(thm),theory(equality)],[486,384,140]),
[iquote('0:Rew:486.0,384.0,140.0,384.0')] ).
cnf(564,plain,
equal(op2(e22,op2(e23,e22)),e20),
inference(rew,[status(thm),theory(equality)],[534,383,486]),
[iquote('0:Rew:534.0,383.0,486.0,383.0')] ).
cnf(567,plain,
equal(op2(e22,e21),h4(e13)),
inference(rew,[status(thm),theory(equality)],[140,380,60,486]),
[iquote('0:Rew:140.0,380.0,60.0,380.0,486.0,380.0')] ).
cnf(574,plain,
equal(op2(op2(e23,e22),e21),op2(e23,h4(e13))),
inference(rew,[status(thm),theory(equality)],[567,394]),
[iquote('0:Rew:567.0,394.0')] ).
cnf(575,plain,
equal(op2(op2(e23,e22),e21),h4(e11)),
inference(rew,[status(thm),theory(equality)],[488,574]),
[iquote('0:Rew:488.0,574.0')] ).
cnf(576,plain,
equal(op2(e23,e22),e21),
inference(rew,[status(thm),theory(equality)],[486,379,60]),
[iquote('0:Rew:486.0,379.0,60.0,379.0')] ).
cnf(581,plain,
~ equal(op2(e20,e22),e21),
inference(rew,[status(thm),theory(equality)],[576,205]),
[iquote('0:Rew:576.0,205.0')] ).
cnf(583,plain,
equal(op2(h4(e13),e22),op2(e23,e21)),
inference(rew,[status(thm),theory(equality)],[576,555]),
[iquote('0:Rew:576.0,555.0')] ).
cnf(584,plain,
equal(op2(e23,e21),op2(e21,e23)),
inference(rew,[status(thm),theory(equality)],[576,558]),
[iquote('0:Rew:576.0,558.0')] ).
cnf(586,plain,
equal(op2(e23,op2(e22,e20)),op2(e21,e20)),
inference(rew,[status(thm),theory(equality)],[576,393]),
[iquote('0:Rew:576.0,393.0')] ).
cnf(587,plain,
equal(op2(e22,e21),e20),
inference(rew,[status(thm),theory(equality)],[576,564]),
[iquote('0:Rew:576.0,564.0')] ).
cnf(588,plain,
equal(op2(e21,e21),h4(e11)),
inference(rew,[status(thm),theory(equality)],[576,575]),
[iquote('0:Rew:576.0,575.0')] ).
cnf(589,plain,
equal(h4(e13),e20),
inference(rew,[status(thm),theory(equality)],[567,587]),
[iquote('0:Rew:567.0,587.0')] ).
cnf(590,plain,
equal(op2(e23,e23),e20),
inference(rew,[status(thm),theory(equality)],[589,140]),
[iquote('0:Rew:589.0,140.0')] ).
cnf(593,plain,
equal(op2(e23,e20),h4(e11)),
inference(rew,[status(thm),theory(equality)],[589,488]),
[iquote('0:Rew:589.0,488.0')] ).
cnf(599,plain,
equal(op2(e20,e23),h4(e11)),
inference(rew,[status(thm),theory(equality)],[589,554]),
[iquote('0:Rew:589.0,554.0')] ).
cnf(600,plain,
equal(op2(e23,op2(e23,e21)),op2(e20,e21)),
inference(rew,[status(thm),theory(equality)],[589,556]),
[iquote('0:Rew:589.0,556.0')] ).
cnf(601,plain,
equal(op2(e23,op2(e23,e20)),op2(e20,e20)),
inference(rew,[status(thm),theory(equality)],[589,557]),
[iquote('0:Rew:589.0,557.0')] ).
cnf(602,plain,
equal(op2(e22,e20),op2(e21,e23)),
inference(rew,[status(thm),theory(equality)],[589,563]),
[iquote('0:Rew:589.0,563.0')] ).
cnf(603,plain,
equal(op2(e22,e21),e20),
inference(rew,[status(thm),theory(equality)],[589,567]),
[iquote('0:Rew:589.0,567.0')] ).
cnf(610,plain,
equal(h4(e11),h2(e13)),
inference(rew,[status(thm),theory(equality)],[138,588]),
[iquote('0:Rew:138.0,588.0')] ).
cnf(614,plain,
equal(op2(e23,e20),h2(e13)),
inference(rew,[status(thm),theory(equality)],[610,593]),
[iquote('0:Rew:610.0,593.0')] ).
cnf(619,plain,
equal(op2(op2(e23,e21),e22),h2(e13)),
inference(rew,[status(thm),theory(equality)],[614,560]),
[iquote('0:Rew:614.0,560.0')] ).
cnf(627,plain,
equal(op2(e20,e23),h2(e13)),
inference(rew,[status(thm),theory(equality)],[610,599]),
[iquote('0:Rew:610.0,599.0')] ).
cnf(637,plain,
equal(op2(op2(e21,e23),e21),op2(e23,h2(e13))),
inference(rew,[status(thm),theory(equality)],[584,561]),
[iquote('0:Rew:584.0,561.0')] ).
cnf(649,plain,
equal(op2(e21,e23),op2(e20,e22)),
inference(rew,[status(thm),theory(equality)],[589,583,584]),
[iquote('0:Rew:589.0,583.0,584.0,583.0')] ).
cnf(654,plain,
equal(op2(e23,e21),op2(e20,e22)),
inference(rew,[status(thm),theory(equality)],[649,584]),
[iquote('0:Rew:649.0,584.0')] ).
cnf(655,plain,
equal(op2(e22,e20),op2(e20,e22)),
inference(rew,[status(thm),theory(equality)],[649,602]),
[iquote('0:Rew:649.0,602.0')] ).
cnf(658,plain,
equal(op2(op2(e20,e22),e22),h2(e13)),
inference(rew,[status(thm),theory(equality)],[654,619]),
[iquote('0:Rew:654.0,619.0')] ).
cnf(662,plain,
equal(op2(e23,op2(e20,e22)),op2(e21,e20)),
inference(rew,[status(thm),theory(equality)],[655,586]),
[iquote('0:Rew:655.0,586.0')] ).
cnf(663,plain,
equal(op2(e21,e20),op2(e20,e21)),
inference(rew,[status(thm),theory(equality)],[662,600,654]),
[iquote('0:Rew:662.0,600.0,654.0,600.0')] ).
cnf(669,plain,
equal(op2(e23,op2(e20,e22)),op2(e20,e21)),
inference(rew,[status(thm),theory(equality)],[663,662]),
[iquote('0:Rew:663.0,662.0')] ).
cnf(670,plain,
equal(op2(e23,h2(e13)),h1(e13)),
inference(rew,[status(thm),theory(equality)],[614,601,137]),
[iquote('0:Rew:614.0,601.0,137.0,601.0')] ).
cnf(676,plain,
equal(op2(op2(e20,e22),e21),h1(e13)),
inference(rew,[status(thm),theory(equality)],[649,637,670]),
[iquote('0:Rew:649.0,637.0,670.0,637.0')] ).
cnf(724,plain,
equal(op1(op1(e13,e12),e13),op1(e13,e11)),
inference(rew,[status(thm),theory(equality)],[487,332]),
[iquote('0:Rew:487.0,332.0')] ).
cnf(726,plain,
equal(op1(op1(e13,e11),e12),op1(e13,e10)),
inference(rew,[status(thm),theory(equality)],[541,327]),
[iquote('0:Rew:541.0,327.0')] ).
cnf(727,plain,
equal(op1(e12,op1(e13,e13)),op1(e11,e13)),
inference(rew,[status(thm),theory(equality)],[487,320]),
[iquote('0:Rew:487.0,320.0')] ).
cnf(728,plain,
equal(op1(e12,op1(e13,e12)),e10),
inference(rew,[status(thm),theory(equality)],[541,319,487]),
[iquote('0:Rew:541.0,319.0,487.0,319.0')] ).
cnf(729,plain,
equal(op1(e12,op1(e13,e11)),op1(e11,e11)),
inference(rew,[status(thm),theory(equality)],[487,318]),
[iquote('0:Rew:487.0,318.0')] ).
cnf(730,plain,
equal(op1(e12,op1(e13,e10)),op1(e11,e10)),
inference(rew,[status(thm),theory(equality)],[487,317]),
[iquote('0:Rew:487.0,317.0')] ).
cnf(731,plain,
equal(op1(e13,e13),op1(e12,e11)),
inference(rew,[status(thm),theory(equality)],[59,316,487]),
[iquote('0:Rew:59.0,316.0,487.0,316.0')] ).
cnf(743,plain,
equal(op1(e12,op1(e12,e11)),op1(e11,e13)),
inference(rew,[status(thm),theory(equality)],[731,727]),
[iquote('0:Rew:731.0,727.0')] ).
cnf(744,plain,
equal(op1(e13,e12),e11),
inference(rew,[status(thm),theory(equality)],[487,315,59]),
[iquote('0:Rew:487.0,315.0,59.0,315.0')] ).
cnf(748,plain,
~ equal(op1(e10,e12),e11),
inference(rew,[status(thm),theory(equality)],[744,157]),
[iquote('0:Rew:744.0,157.0')] ).
cnf(750,plain,
equal(op1(e13,e11),op1(e11,e13)),
inference(rew,[status(thm),theory(equality)],[744,724]),
[iquote('0:Rew:744.0,724.0')] ).
cnf(751,plain,
equal(op1(e13,op1(e12,e11)),op1(e11,e11)),
inference(rew,[status(thm),theory(equality)],[744,330]),
[iquote('0:Rew:744.0,330.0')] ).
cnf(752,plain,
equal(op1(e13,op1(e12,e10)),op1(e11,e10)),
inference(rew,[status(thm),theory(equality)],[744,329]),
[iquote('0:Rew:744.0,329.0')] ).
cnf(753,plain,
equal(op1(e12,e11),e10),
inference(rew,[status(thm),theory(equality)],[744,728]),
[iquote('0:Rew:744.0,728.0')] ).
cnf(762,plain,
equal(op1(e13,e13),e10),
inference(rew,[status(thm),theory(equality)],[753,731]),
[iquote('0:Rew:753.0,731.0')] ).
cnf(766,plain,
equal(op1(e12,e10),op1(e11,e13)),
inference(rew,[status(thm),theory(equality)],[753,743]),
[iquote('0:Rew:753.0,743.0')] ).
cnf(772,plain,
equal(op1(op1(e11,e13),e12),op1(e13,e10)),
inference(rew,[status(thm),theory(equality)],[750,726]),
[iquote('0:Rew:750.0,726.0')] ).
cnf(775,plain,
equal(op1(e12,op1(e11,e13)),op1(e11,e11)),
inference(rew,[status(thm),theory(equality)],[750,729]),
[iquote('0:Rew:750.0,729.0')] ).
cnf(785,plain,
equal(op1(e13,e10),op1(e11,e11)),
inference(rew,[status(thm),theory(equality)],[753,751]),
[iquote('0:Rew:753.0,751.0')] ).
cnf(792,plain,
equal(op1(e12,op1(e11,e11)),op1(e11,e10)),
inference(rew,[status(thm),theory(equality)],[785,730]),
[iquote('0:Rew:785.0,730.0')] ).
cnf(796,plain,
equal(op1(e13,op1(e11,e13)),op1(e11,e10)),
inference(rew,[status(thm),theory(equality)],[766,752]),
[iquote('0:Rew:766.0,752.0')] ).
cnf(797,plain,
equal(op1(op1(e11,e13),e12),op1(e11,e11)),
inference(rew,[status(thm),theory(equality)],[785,772]),
[iquote('0:Rew:785.0,772.0')] ).
cnf(800,plain,
equal(op1(e11,e11),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[753,312,775]),
[iquote('0:Rew:753.0,312.0,775.0,312.0')] ).
cnf(805,plain,
equal(op1(e13,e10),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[800,785]),
[iquote('0:Rew:800.0,785.0')] ).
cnf(808,plain,
equal(op1(op1(e11,e13),e12),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[800,797]),
[iquote('0:Rew:800.0,797.0')] ).
cnf(810,plain,
equal(op1(e12,op1(e10,e13)),op1(e11,e10)),
inference(rew,[status(thm),theory(equality)],[800,792]),
[iquote('0:Rew:800.0,792.0')] ).
cnf(811,plain,
equal(op1(e11,e13),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[753,311,766,541]),
[iquote('0:Rew:753.0,311.0,766.0,311.0,541.0,311.0')] ).
cnf(816,plain,
equal(op1(e13,e11),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[811,750]),
[iquote('0:Rew:811.0,750.0')] ).
cnf(817,plain,
equal(op1(e12,e10),op1(e10,e12)),
inference(rew,[status(thm),theory(equality)],[811,766]),
[iquote('0:Rew:811.0,766.0')] ).
cnf(821,plain,
equal(op1(e13,op1(e10,e12)),op1(e11,e10)),
inference(rew,[status(thm),theory(equality)],[811,796]),
[iquote('0:Rew:811.0,796.0')] ).
cnf(822,plain,
equal(op1(op1(e10,e12),e12),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[811,808]),
[iquote('0:Rew:811.0,808.0')] ).
cnf(824,plain,
equal(op1(e11,e10),op1(e10,e11)),
inference(rew,[status(thm),theory(equality)],[753,310,810,800]),
[iquote('0:Rew:753.0,310.0,810.0,310.0,800.0,310.0')] ).
cnf(830,plain,
equal(op1(e13,op1(e10,e12)),op1(e10,e11)),
inference(rew,[status(thm),theory(equality)],[824,821]),
[iquote('0:Rew:824.0,821.0')] ).
cnf(831,plain,
equal(op1(e12,op1(e10,e11)),op1(e10,e10)),
inference(rew,[status(thm),theory(equality)],[753,309,824]),
[iquote('0:Rew:753.0,309.0,824.0,309.0')] ).
cnf(834,plain,
equal(op1(op1(e10,e12),e11),op1(e10,e10)),
inference(rew,[status(thm),theory(equality)],[817,306,831]),
[iquote('0:Rew:817.0,306.0,831.0,306.0')] ).
cnf(887,plain,
( equal(op2(e20,e22),e20)
| equal(op2(e20,e22),e21)
| equal(op2(e20,e22),e22)
| equal(op2(e20,e22),e23) ),
inference(rew,[status(thm),theory(equality)],[654,413]),
[iquote('0:Rew:654.0,413.3,654.0,413.2,654.0,413.1,654.0,413.0')] ).
cnf(888,plain,
equal(op2(e20,e22),e22),
inference(mrr,[status(thm)],[887,540,581,516]),
[iquote('0:MRR:887.0,887.1,887.3,540.0,581.0,516.0')] ).
cnf(895,plain,
equal(op2(e21,e23),e22),
inference(rew,[status(thm),theory(equality)],[888,649]),
[iquote('0:Rew:888.0,649.0')] ).
cnf(896,plain,
equal(op2(e23,e21),e22),
inference(rew,[status(thm),theory(equality)],[888,654]),
[iquote('0:Rew:888.0,654.0')] ).
cnf(897,plain,
equal(op2(e22,e20),e22),
inference(rew,[status(thm),theory(equality)],[888,655]),
[iquote('0:Rew:888.0,655.0')] ).
cnf(898,plain,
equal(op2(e22,e22),h2(e13)),
inference(rew,[status(thm),theory(equality)],[888,658]),
[iquote('0:Rew:888.0,658.0')] ).
cnf(900,plain,
equal(op2(e23,e22),op2(e20,e21)),
inference(rew,[status(thm),theory(equality)],[888,669]),
[iquote('0:Rew:888.0,669.0')] ).
cnf(901,plain,
equal(op2(e22,e21),h1(e13)),
inference(rew,[status(thm),theory(equality)],[888,676]),
[iquote('0:Rew:888.0,676.0')] ).
cnf(906,plain,
equal(h2(e13),e23),
inference(rew,[status(thm),theory(equality)],[60,898]),
[iquote('0:Rew:60.0,898.0')] ).
cnf(907,plain,
equal(op2(e21,e21),e23),
inference(rew,[status(thm),theory(equality)],[906,138]),
[iquote('0:Rew:906.0,138.0')] ).
cnf(912,plain,
equal(op2(e23,e20),e23),
inference(rew,[status(thm),theory(equality)],[906,614]),
[iquote('0:Rew:906.0,614.0')] ).
cnf(914,plain,
equal(op2(e20,e23),e23),
inference(rew,[status(thm),theory(equality)],[906,627]),
[iquote('0:Rew:906.0,627.0')] ).
cnf(928,plain,
equal(h1(e13),e20),
inference(rew,[status(thm),theory(equality)],[603,901]),
[iquote('0:Rew:603.0,901.0')] ).
cnf(929,plain,
equal(op2(e20,e20),e20),
inference(rew,[status(thm),theory(equality)],[928,137]),
[iquote('0:Rew:928.0,137.0')] ).
cnf(971,plain,
equal(op2(e20,e21),e21),
inference(rew,[status(thm),theory(equality)],[576,900]),
[iquote('0:Rew:576.0,900.0')] ).
cnf(973,plain,
equal(op2(e21,e20),e21),
inference(rew,[status(thm),theory(equality)],[971,663]),
[iquote('0:Rew:971.0,663.0')] ).
cnf(991,plain,
( equal(op1(e10,e12),e10)
| equal(op1(e10,e12),e11)
| equal(op1(e10,e12),e12)
| equal(op1(e10,e12),e13) ),
inference(rew,[status(thm),theory(equality)],[816,429]),
[iquote('0:Rew:816.0,429.3,816.0,429.2,816.0,429.1,816.0,429.0')] ).
cnf(992,plain,
equal(op1(e10,e12),e12),
inference(mrr,[status(thm)],[991,547,748,533]),
[iquote('0:MRR:991.0,991.1,991.3,547.0,748.0,533.0')] ).
cnf(999,plain,
equal(op1(e11,e13),e12),
inference(rew,[status(thm),theory(equality)],[992,811]),
[iquote('0:Rew:992.0,811.0')] ).
cnf(1000,plain,
equal(op1(e13,e11),e12),
inference(rew,[status(thm),theory(equality)],[992,816]),
[iquote('0:Rew:992.0,816.0')] ).
cnf(1001,plain,
equal(op1(e12,e10),e12),
inference(rew,[status(thm),theory(equality)],[992,817]),
[iquote('0:Rew:992.0,817.0')] ).
cnf(1002,plain,
equal(op1(e12,e12),op1(e10,e13)),
inference(rew,[status(thm),theory(equality)],[992,822]),
[iquote('0:Rew:992.0,822.0')] ).
cnf(1004,plain,
equal(op1(e13,e12),op1(e10,e11)),
inference(rew,[status(thm),theory(equality)],[992,830]),
[iquote('0:Rew:992.0,830.0')] ).
cnf(1006,plain,
equal(op1(e12,e11),op1(e10,e10)),
inference(rew,[status(thm),theory(equality)],[992,834]),
[iquote('0:Rew:992.0,834.0')] ).
cnf(1015,plain,
equal(op1(e10,e13),e13),
inference(rew,[status(thm),theory(equality)],[59,1002]),
[iquote('0:Rew:59.0,1002.0')] ).
cnf(1020,plain,
equal(op1(e11,e11),e13),
inference(rew,[status(thm),theory(equality)],[1015,800]),
[iquote('0:Rew:1015.0,800.0')] ).
cnf(1021,plain,
equal(op1(e13,e10),e13),
inference(rew,[status(thm),theory(equality)],[1015,805]),
[iquote('0:Rew:1015.0,805.0')] ).
cnf(1033,plain,
equal(op1(e10,e11),e11),
inference(rew,[status(thm),theory(equality)],[744,1004]),
[iquote('0:Rew:744.0,1004.0')] ).
cnf(1036,plain,
equal(op1(e11,e10),e11),
inference(rew,[status(thm),theory(equality)],[1033,824]),
[iquote('0:Rew:1033.0,824.0')] ).
cnf(1045,plain,
equal(op1(e10,e10),e10),
inference(rew,[status(thm),theory(equality)],[753,1006]),
[iquote('0:Rew:753.0,1006.0')] ).
cnf(1093,plain,
( ~ equal(e23,e23)
| ~ equal(e20,e20)
| ~ equal(e21,e21)
| ~ equal(e22,e22)
| ~ equal(e23,e23)
| ~ equal(e21,e21)
| ~ equal(e23,e23)
| ~ equal(e20,e20)
| ~ equal(e22,e22)
| ~ equal(e22,e22)
| ~ equal(e20,e20)
| ~ equal(e23,e23)
| ~ equal(e21,e21)
| ~ equal(e23,e23)
| ~ equal(e22,e22)
| ~ equal(e21,e21)
| ~ equal(e20,e20)
| ~ skC6
| ~ skC7
| ~ skC8 ),
inference(rew,[status(thm),theory(equality)],[590,455,467,549,762,576,33,489,744,896,1000,912,1021,486,487,60,59,603,753,897,1001,895,999,534,541,907,1020,973,1036,914,1015,888,992,971,1033,929,1045]),
[iquote('0:Rew:590.0,455.16,467.0,455.16,549.0,455.16,762.0,455.16,576.0,455.15,467.0,455.15,33.0,455.15,489.0,455.15,744.0,455.15,896.0,455.14,467.0,455.14,489.0,455.14,33.0,455.14,1000.0,455.14,912.0,455.13,549.0,455.13,467.0,455.13,1021.0,455.13,486.0,455.12,33.0,455.12,467.0,455.12,489.0,455.12,487.0,455.12,60.0,455.11,33.0,455.11,467.0,455.11,59.0,455.11,603.0,455.10,33.0,455.10,489.0,455.10,549.0,455.10,753.0,455.10,897.0,455.9,549.0,455.9,33.0,455.9,1001.0,455.9,895.0,455.8,489.0,455.8,467.0,455.8,33.0,455.8,999.0,455.8,534.0,455.7,489.0,455.7,33.0,455.7,549.0,455.7,541.0,455.7,907.0,455.6,489.0,455.6,467.0,455.6,1020.0,455.6,973.0,455.5,549.0,455.5,489.0,455.5,1036.0,455.5,914.0,455.4,549.0,455.4,467.0,455.4,1015.0,455.4,888.0,455.3,549.0,455.3,33.0,455.3,992.0,455.3,971.0,455.2,549.0,455.2,489.0,455.2,1033.0,455.2,929.0,455.1,549.0,455.1,1045.0,455.1,467.0,455.0')] ).
cnf(1094,plain,
( ~ skC6
| ~ skC7
| ~ skC8 ),
inference(obv,[status(thm),theory(equality)],[1093]),
[iquote('0:Obv:1093.16')] ).
cnf(1095,plain,
$false,
inference(mrr,[status(thm)],[1094,551,492,473]),
[iquote('0:MRR:1094.0,1094.1,1094.2,551.0,492.0,473.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG016+1 : TPTP v8.1.0. Released v2.7.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n020.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 22:30:21 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.37/0.56
% 0.37/0.56 SPASS V 3.9
% 0.37/0.56 SPASS beiseite: Proof found.
% 0.37/0.56 % SZS status Theorem
% 0.37/0.56 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.56 SPASS derived 323 clauses, backtracked 0 clauses, performed 0 splits and kept 509 clauses.
% 0.37/0.56 SPASS allocated 86461 KBytes.
% 0.37/0.56 SPASS spent 0:00:00.20 on the problem.
% 0.37/0.56 0:00:00.04 for the input.
% 0.37/0.56 0:00:00.10 for the FLOTTER CNF translation.
% 0.37/0.56 0:00:00.00 for inferences.
% 0.37/0.56 0:00:00.00 for the backtracking.
% 0.37/0.56 0:00:00.03 for the reduction.
% 0.37/0.56
% 0.37/0.56
% 0.37/0.56 Here is a proof with depth 0, length 181 :
% 0.37/0.56 % SZS output start Refutation
% See solution above
% 0.37/0.57 Formulae used in the proof : ax28 ax24 ax25 co1 ax26 ax27 ax29 ax17 ax18 ax2 ax6 ax5 ax1
% 0.37/0.57
%------------------------------------------------------------------------------