%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG079+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:14 EDT 2022
% Result : Theorem 0.20s 0.49s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 60
% Syntax : Number of clauses : 193 ( 185 unt; 8 nHn; 193 RR)
% Number of literals : 213 ( 0 equ; 14 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ equal(e11,e10),
file('ALG079+1.p',unknown),
[] ).
cnf(2,axiom,
~ equal(e12,e10),
file('ALG079+1.p',unknown),
[] ).
cnf(11,axiom,
~ equal(e21,e20),
file('ALG079+1.p',unknown),
[] ).
cnf(13,axiom,
~ equal(e23,e20),
file('ALG079+1.p',unknown),
[] ).
cnf(19,axiom,
~ equal(e24,e22),
file('ALG079+1.p',unknown),
[] ).
cnf(20,axiom,
~ equal(e24,e23),
file('ALG079+1.p',unknown),
[] ).
cnf(46,axiom,
equal(h(j(e20)),e20),
file('ALG079+1.p',unknown),
[] ).
cnf(49,axiom,
equal(h(j(e23)),e23),
file('ALG079+1.p',unknown),
[] ).
cnf(50,axiom,
equal(h(j(e24)),e24),
file('ALG079+1.p',unknown),
[] ).
cnf(51,axiom,
equal(j(h(e10)),e10),
file('ALG079+1.p',unknown),
[] ).
cnf(52,axiom,
equal(j(h(e11)),e11),
file('ALG079+1.p',unknown),
[] ).
cnf(53,axiom,
equal(j(h(e12)),e12),
file('ALG079+1.p',unknown),
[] ).
cnf(56,axiom,
equal(op1(e10,e10),e10),
file('ALG079+1.p',unknown),
[] ).
cnf(57,axiom,
equal(op1(e10,e11),e11),
file('ALG079+1.p',unknown),
[] ).
cnf(61,axiom,
equal(op1(e11,e10),e11),
file('ALG079+1.p',unknown),
[] ).
cnf(62,axiom,
equal(op1(e11,e11),e10),
file('ALG079+1.p',unknown),
[] ).
cnf(69,axiom,
equal(op1(e12,e13),e10),
file('ALG079+1.p',unknown),
[] ).
cnf(71,axiom,
equal(op1(e13,e10),e13),
file('ALG079+1.p',unknown),
[] ).
cnf(72,axiom,
equal(op1(e13,e11),e12),
file('ALG079+1.p',unknown),
[] ).
cnf(76,axiom,
equal(op1(e14,e10),e14),
file('ALG079+1.p',unknown),
[] ).
cnf(77,axiom,
equal(op1(e14,e11),e13),
file('ALG079+1.p',unknown),
[] ).
cnf(80,axiom,
equal(op1(e14,e14),e12),
file('ALG079+1.p',unknown),
[] ).
cnf(84,axiom,
equal(op2(e20,e23),e23),
file('ALG079+1.p',unknown),
[] ).
cnf(85,axiom,
equal(op2(e20,e24),e24),
file('ALG079+1.p',unknown),
[] ).
cnf(87,axiom,
equal(op2(e21,e21),e22),
file('ALG079+1.p',unknown),
[] ).
cnf(88,axiom,
equal(op2(e21,e22),e23),
file('ALG079+1.p',unknown),
[] ).
cnf(90,axiom,
equal(op2(e21,e24),e20),
file('ALG079+1.p',unknown),
[] ).
cnf(92,axiom,
equal(op2(e22,e21),e24),
file('ALG079+1.p',unknown),
[] ).
cnf(93,axiom,
equal(op2(e22,e22),e21),
file('ALG079+1.p',unknown),
[] ).
cnf(94,axiom,
equal(op2(e22,e23),e20),
file('ALG079+1.p',unknown),
[] ).
cnf(95,axiom,
equal(op2(e22,e24),e23),
file('ALG079+1.p',unknown),
[] ).
cnf(96,axiom,
equal(op2(e23,e20),e23),
file('ALG079+1.p',unknown),
[] ).
cnf(97,axiom,
equal(op2(e23,e21),e20),
file('ALG079+1.p',unknown),
[] ).
cnf(98,axiom,
equal(op2(e23,e22),e24),
file('ALG079+1.p',unknown),
[] ).
cnf(99,axiom,
equal(op2(e23,e23),e21),
file('ALG079+1.p',unknown),
[] ).
cnf(102,axiom,
equal(op2(e24,e21),e23),
file('ALG079+1.p',unknown),
[] ).
cnf(105,axiom,
equal(op2(e24,e24),e21),
file('ALG079+1.p',unknown),
[] ).
cnf(119,axiom,
equal(op2(h(e12),h(e13)),h(op1(e12,e13))),
file('ALG079+1.p',unknown),
[] ).
cnf(121,axiom,
equal(op2(h(e13),h(e10)),h(op1(e13,e10))),
file('ALG079+1.p',unknown),
[] ).
cnf(122,axiom,
equal(op2(h(e13),h(e11)),h(op1(e13,e11))),
file('ALG079+1.p',unknown),
[] ).
cnf(126,axiom,
equal(op2(h(e14),h(e10)),h(op1(e14,e10))),
file('ALG079+1.p',unknown),
[] ).
cnf(127,axiom,
equal(op2(h(e14),h(e11)),h(op1(e14,e11))),
file('ALG079+1.p',unknown),
[] ).
cnf(130,axiom,
equal(op2(h(e14),h(e14)),h(op1(e14,e14))),
file('ALG079+1.p',unknown),
[] ).
cnf(134,axiom,
equal(op1(j(e20),j(e23)),j(op2(e20,e23))),
file('ALG079+1.p',unknown),
[] ).
cnf(135,axiom,
equal(op1(j(e20),j(e24)),j(op2(e20,e24))),
file('ALG079+1.p',unknown),
[] ).
cnf(137,axiom,
equal(op1(j(e21),j(e21)),j(op2(e21,e21))),
file('ALG079+1.p',unknown),
[] ).
cnf(138,axiom,
equal(op1(j(e21),j(e22)),j(op2(e21,e22))),
file('ALG079+1.p',unknown),
[] ).
cnf(140,axiom,
equal(op1(j(e21),j(e24)),j(op2(e21,e24))),
file('ALG079+1.p',unknown),
[] ).
cnf(142,axiom,
equal(op1(j(e22),j(e21)),j(op2(e22,e21))),
file('ALG079+1.p',unknown),
[] ).
cnf(143,axiom,
equal(op1(j(e22),j(e22)),j(op2(e22,e22))),
file('ALG079+1.p',unknown),
[] ).
cnf(144,axiom,
equal(op1(j(e22),j(e23)),j(op2(e22,e23))),
file('ALG079+1.p',unknown),
[] ).
cnf(145,axiom,
equal(op1(j(e22),j(e24)),j(op2(e22,e24))),
file('ALG079+1.p',unknown),
[] ).
cnf(146,axiom,
equal(op1(j(e23),j(e20)),j(op2(e23,e20))),
file('ALG079+1.p',unknown),
[] ).
cnf(147,axiom,
equal(op1(j(e23),j(e21)),j(op2(e23,e21))),
file('ALG079+1.p',unknown),
[] ).
cnf(148,axiom,
equal(op1(j(e23),j(e22)),j(op2(e23,e22))),
file('ALG079+1.p',unknown),
[] ).
cnf(149,axiom,
equal(op1(j(e23),j(e23)),j(op2(e23,e23))),
file('ALG079+1.p',unknown),
[] ).
cnf(152,axiom,
equal(op1(j(e24),j(e21)),j(op2(e24,e21))),
file('ALG079+1.p',unknown),
[] ).
cnf(155,axiom,
equal(op1(j(e24),j(e24)),j(op2(e24,e24))),
file('ALG079+1.p',unknown),
[] ).
cnf(164,axiom,
( equal(h(e11),e24)
| equal(h(e11),e23)
| equal(h(e11),e22)
| equal(h(e11),e21)
| equal(h(e11),e20) ),
file('ALG079+1.p',unknown),
[] ).
cnf(165,axiom,
( equal(h(e10),e24)
| equal(h(e10),e23)
| equal(h(e10),e22)
| equal(h(e10),e21)
| equal(h(e10),e20) ),
file('ALG079+1.p',unknown),
[] ).
cnf(166,plain,
equal(op1(j(e24),j(e24)),j(e21)),
inference(rew,[status(thm),theory(equality)],[105,155]),
[iquote('0:Rew:105.0,155.0')] ).
cnf(169,plain,
equal(op1(j(e24),j(e21)),j(e23)),
inference(rew,[status(thm),theory(equality)],[102,152]),
[iquote('0:Rew:102.0,152.0')] ).
cnf(172,plain,
equal(op1(j(e23),j(e23)),j(e21)),
inference(rew,[status(thm),theory(equality)],[99,149]),
[iquote('0:Rew:99.0,149.0')] ).
cnf(173,plain,
equal(op1(j(e23),j(e22)),j(e24)),
inference(rew,[status(thm),theory(equality)],[98,148]),
[iquote('0:Rew:98.0,148.0')] ).
cnf(174,plain,
equal(op1(j(e23),j(e21)),j(e20)),
inference(rew,[status(thm),theory(equality)],[97,147]),
[iquote('0:Rew:97.0,147.0')] ).
cnf(175,plain,
equal(op1(j(e23),j(e20)),j(e23)),
inference(rew,[status(thm),theory(equality)],[96,146]),
[iquote('0:Rew:96.0,146.0')] ).
cnf(176,plain,
equal(op1(j(e22),j(e24)),j(e23)),
inference(rew,[status(thm),theory(equality)],[95,145]),
[iquote('0:Rew:95.0,145.0')] ).
cnf(177,plain,
equal(op1(j(e22),j(e23)),j(e20)),
inference(rew,[status(thm),theory(equality)],[94,144]),
[iquote('0:Rew:94.0,144.0')] ).
cnf(178,plain,
equal(op1(j(e22),j(e22)),j(e21)),
inference(rew,[status(thm),theory(equality)],[93,143]),
[iquote('0:Rew:93.0,143.0')] ).
cnf(179,plain,
equal(op1(j(e22),j(e21)),j(e24)),
inference(rew,[status(thm),theory(equality)],[92,142]),
[iquote('0:Rew:92.0,142.0')] ).
cnf(181,plain,
equal(op1(j(e21),j(e24)),j(e20)),
inference(rew,[status(thm),theory(equality)],[90,140]),
[iquote('0:Rew:90.0,140.0')] ).
cnf(183,plain,
equal(op1(j(e21),j(e22)),j(e23)),
inference(rew,[status(thm),theory(equality)],[88,138]),
[iquote('0:Rew:88.0,138.0')] ).
cnf(184,plain,
equal(op1(j(e21),j(e21)),j(e22)),
inference(rew,[status(thm),theory(equality)],[87,137]),
[iquote('0:Rew:87.0,137.0')] ).
cnf(186,plain,
equal(op1(j(e20),j(e24)),j(e24)),
inference(rew,[status(thm),theory(equality)],[85,135]),
[iquote('0:Rew:85.0,135.0')] ).
cnf(187,plain,
equal(op1(j(e20),j(e23)),j(e23)),
inference(rew,[status(thm),theory(equality)],[84,134]),
[iquote('0:Rew:84.0,134.0')] ).
cnf(191,plain,
equal(op2(h(e14),h(e14)),h(e12)),
inference(rew,[status(thm),theory(equality)],[80,130]),
[iquote('0:Rew:80.0,130.0')] ).
cnf(194,plain,
equal(op2(h(e14),h(e11)),h(e13)),
inference(rew,[status(thm),theory(equality)],[77,127]),
[iquote('0:Rew:77.0,127.0')] ).
cnf(195,plain,
equal(op2(h(e14),h(e10)),h(e14)),
inference(rew,[status(thm),theory(equality)],[76,126]),
[iquote('0:Rew:76.0,126.0')] ).
cnf(199,plain,
equal(op2(h(e13),h(e11)),h(e12)),
inference(rew,[status(thm),theory(equality)],[72,122]),
[iquote('0:Rew:72.0,122.0')] ).
cnf(200,plain,
equal(op2(h(e13),h(e10)),h(e13)),
inference(rew,[status(thm),theory(equality)],[71,121]),
[iquote('0:Rew:71.0,121.0')] ).
cnf(202,plain,
equal(op2(h(e12),h(e13)),h(e10)),
inference(rew,[status(thm),theory(equality)],[69,119]),
[iquote('0:Rew:69.0,119.0')] ).
cnf(216,plain,
equal(h(e10),e24),
inference(spt,[spt(split,[position(s1)])],[165]),
[iquote('1:Spt:165.0')] ).
cnf(217,plain,
equal(j(e24),e10),
inference(rew,[status(thm),theory(equality)],[216,51]),
[iquote('1:Rew:216.0,51.0')] ).
cnf(232,plain,
equal(op1(e10,e10),j(e21)),
inference(rew,[status(thm),theory(equality)],[217,166]),
[iquote('1:Rew:217.0,166.0')] ).
cnf(235,plain,
equal(op1(e10,j(e21)),j(e23)),
inference(rew,[status(thm),theory(equality)],[217,169]),
[iquote('1:Rew:217.0,169.0')] ).
cnf(246,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[56,232]),
[iquote('1:Rew:56.0,232.0')] ).
cnf(274,plain,
equal(j(e23),e10),
inference(rew,[status(thm),theory(equality)],[56,235,246]),
[iquote('1:Rew:56.0,235.0,246.0,235.0')] ).
cnf(275,plain,
equal(h(e10),e23),
inference(rew,[status(thm),theory(equality)],[274,49]),
[iquote('1:Rew:274.0,49.0')] ).
cnf(277,plain,
equal(e24,e23),
inference(rew,[status(thm),theory(equality)],[216,275]),
[iquote('1:Rew:216.0,275.0')] ).
cnf(278,plain,
$false,
inference(mrr,[status(thm)],[277,20]),
[iquote('1:MRR:277.0,20.0')] ).
cnf(292,plain,
~ equal(h(e10),e24),
inference(spt,[spt(split,[position(sa)])],[278,216]),
[iquote('1:Spt:278.0,165.0,216.0')] ).
cnf(293,plain,
( equal(h(e10),e23)
| equal(h(e10),e22)
| equal(h(e10),e21)
| equal(h(e10),e20) ),
inference(spt,[spt(split,[position(s2)])],[165]),
[iquote('1:Spt:278.0,165.1,165.2,165.3,165.4')] ).
cnf(294,plain,
equal(h(e10),e23),
inference(spt,[spt(split,[position(s2s1)])],[293]),
[iquote('2:Spt:293.0')] ).
cnf(295,plain,
equal(j(e23),e10),
inference(rew,[status(thm),theory(equality)],[294,51]),
[iquote('2:Rew:294.0,51.0')] ).
cnf(318,plain,
equal(op1(e10,j(e21)),j(e20)),
inference(rew,[status(thm),theory(equality)],[295,174]),
[iquote('2:Rew:295.0,174.0')] ).
cnf(319,plain,
equal(op1(e10,e10),j(e21)),
inference(rew,[status(thm),theory(equality)],[295,172]),
[iquote('2:Rew:295.0,172.0')] ).
cnf(325,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[56,319]),
[iquote('2:Rew:56.0,319.0')] ).
cnf(355,plain,
equal(j(e20),e10),
inference(rew,[status(thm),theory(equality)],[56,318,325]),
[iquote('2:Rew:56.0,318.0,325.0,318.0')] ).
cnf(356,plain,
equal(h(e10),e20),
inference(rew,[status(thm),theory(equality)],[355,46]),
[iquote('2:Rew:355.0,46.0')] ).
cnf(360,plain,
equal(e23,e20),
inference(rew,[status(thm),theory(equality)],[294,356]),
[iquote('2:Rew:294.0,356.0')] ).
cnf(361,plain,
$false,
inference(mrr,[status(thm)],[360,13]),
[iquote('2:MRR:360.0,13.0')] ).
cnf(368,plain,
~ equal(h(e10),e23),
inference(spt,[spt(split,[position(s2sa)])],[361,294]),
[iquote('2:Spt:361.0,293.0,294.0')] ).
cnf(369,plain,
( equal(h(e10),e22)
| equal(h(e10),e21)
| equal(h(e10),e20) ),
inference(spt,[spt(split,[position(s2s2)])],[293]),
[iquote('2:Spt:361.0,293.1,293.2,293.3')] ).
cnf(370,plain,
equal(h(e10),e22),
inference(spt,[spt(split,[position(s2s2s1)])],[369]),
[iquote('3:Spt:369.0')] ).
cnf(372,plain,
equal(j(e22),e10),
inference(rew,[status(thm),theory(equality)],[370,51]),
[iquote('3:Rew:370.0,51.0')] ).
cnf(389,plain,
equal(op1(j(e21),e10),j(e23)),
inference(rew,[status(thm),theory(equality)],[372,183]),
[iquote('3:Rew:372.0,183.0')] ).
cnf(392,plain,
equal(op1(j(e23),e10),j(e24)),
inference(rew,[status(thm),theory(equality)],[372,173]),
[iquote('3:Rew:372.0,173.0')] ).
cnf(394,plain,
equal(op1(e10,e10),j(e21)),
inference(rew,[status(thm),theory(equality)],[372,178]),
[iquote('3:Rew:372.0,178.0')] ).
cnf(402,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[56,394]),
[iquote('3:Rew:56.0,394.0')] ).
cnf(414,plain,
equal(j(e23),e10),
inference(rew,[status(thm),theory(equality)],[56,389,402]),
[iquote('3:Rew:56.0,389.0,402.0,389.0')] ).
cnf(432,plain,
equal(j(e24),e10),
inference(rew,[status(thm),theory(equality)],[56,392,414]),
[iquote('3:Rew:56.0,392.0,414.0,392.0')] ).
cnf(433,plain,
equal(h(e10),e24),
inference(rew,[status(thm),theory(equality)],[432,50]),
[iquote('3:Rew:432.0,50.0')] ).
cnf(436,plain,
equal(e24,e22),
inference(rew,[status(thm),theory(equality)],[370,433]),
[iquote('3:Rew:370.0,433.0')] ).
cnf(437,plain,
$false,
inference(mrr,[status(thm)],[436,19]),
[iquote('3:MRR:436.0,19.0')] ).
cnf(450,plain,
~ equal(h(e10),e22),
inference(spt,[spt(split,[position(s2s2sa)])],[437,370]),
[iquote('3:Spt:437.0,369.0,370.0')] ).
cnf(451,plain,
( equal(h(e10),e21)
| equal(h(e10),e20) ),
inference(spt,[spt(split,[position(s2s2s2)])],[369]),
[iquote('3:Spt:437.0,369.1,369.2')] ).
cnf(452,plain,
equal(h(e10),e21),
inference(spt,[spt(split,[position(s2s2s2s1)])],[451]),
[iquote('4:Spt:451.0')] ).
cnf(454,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[452,51]),
[iquote('4:Rew:452.0,51.0')] ).
cnf(471,plain,
equal(op1(j(e22),e10),j(e24)),
inference(rew,[status(thm),theory(equality)],[454,179]),
[iquote('4:Rew:454.0,179.0')] ).
cnf(472,plain,
equal(op1(e10,e10),j(e22)),
inference(rew,[status(thm),theory(equality)],[454,184]),
[iquote('4:Rew:454.0,184.0')] ).
cnf(475,plain,
equal(op1(e10,j(e24)),j(e20)),
inference(rew,[status(thm),theory(equality)],[454,181]),
[iquote('4:Rew:454.0,181.0')] ).
cnf(485,plain,
equal(j(e22),e10),
inference(rew,[status(thm),theory(equality)],[56,472]),
[iquote('4:Rew:56.0,472.0')] ).
cnf(497,plain,
equal(j(e24),e10),
inference(rew,[status(thm),theory(equality)],[56,471,485]),
[iquote('4:Rew:56.0,471.0,485.0,471.0')] ).
cnf(510,plain,
equal(j(e20),e10),
inference(rew,[status(thm),theory(equality)],[56,475,497]),
[iquote('4:Rew:56.0,475.0,497.0,475.0')] ).
cnf(511,plain,
equal(h(e10),e20),
inference(rew,[status(thm),theory(equality)],[510,46]),
[iquote('4:Rew:510.0,46.0')] ).
cnf(515,plain,
equal(e21,e20),
inference(rew,[status(thm),theory(equality)],[452,511]),
[iquote('4:Rew:452.0,511.0')] ).
cnf(516,plain,
$false,
inference(mrr,[status(thm)],[515,11]),
[iquote('4:MRR:515.0,11.0')] ).
cnf(528,plain,
~ equal(h(e10),e21),
inference(spt,[spt(split,[position(s2s2s2sa)])],[516,452]),
[iquote('4:Spt:516.0,451.0,452.0')] ).
cnf(529,plain,
equal(h(e10),e20),
inference(spt,[spt(split,[position(s2s2s2s2)])],[451]),
[iquote('4:Spt:516.0,451.1')] ).
cnf(532,plain,
equal(j(e20),e10),
inference(rew,[status(thm),theory(equality)],[529,51]),
[iquote('4:Rew:529.0,51.0')] ).
cnf(537,plain,
equal(op2(h(e14),e20),h(e14)),
inference(rew,[status(thm),theory(equality)],[529,195]),
[iquote('4:Rew:529.0,195.0')] ).
cnf(539,plain,
equal(op2(h(e13),e20),h(e13)),
inference(rew,[status(thm),theory(equality)],[529,200]),
[iquote('4:Rew:529.0,200.0')] ).
cnf(540,plain,
equal(op2(h(e12),h(e13)),e20),
inference(rew,[status(thm),theory(equality)],[529,202]),
[iquote('4:Rew:529.0,202.0')] ).
cnf(549,plain,
equal(op1(j(e23),j(e21)),e10),
inference(rew,[status(thm),theory(equality)],[532,174]),
[iquote('4:Rew:532.0,174.0')] ).
cnf(552,plain,
equal(op1(j(e21),j(e24)),e10),
inference(rew,[status(thm),theory(equality)],[532,181]),
[iquote('4:Rew:532.0,181.0')] ).
cnf(553,plain,
equal(op1(j(e22),j(e23)),e10),
inference(rew,[status(thm),theory(equality)],[532,177]),
[iquote('4:Rew:532.0,177.0')] ).
cnf(558,plain,
equal(op1(e10,j(e24)),j(e24)),
inference(rew,[status(thm),theory(equality)],[532,186]),
[iquote('4:Rew:532.0,186.0')] ).
cnf(559,plain,
equal(op1(j(e23),e10),j(e23)),
inference(rew,[status(thm),theory(equality)],[532,175]),
[iquote('4:Rew:532.0,175.0')] ).
cnf(560,plain,
equal(op1(e10,j(e23)),j(e23)),
inference(rew,[status(thm),theory(equality)],[532,187]),
[iquote('4:Rew:532.0,187.0')] ).
cnf(563,plain,
equal(h(e11),e24),
inference(spt,[spt(split,[position(s2s2s2s2s1)])],[164]),
[iquote('5:Spt:164.0')] ).
cnf(564,plain,
equal(j(e24),e11),
inference(rew,[status(thm),theory(equality)],[563,52]),
[iquote('5:Rew:563.0,52.0')] ).
cnf(580,plain,
equal(op1(e11,e11),j(e21)),
inference(rew,[status(thm),theory(equality)],[564,166]),
[iquote('5:Rew:564.0,166.0')] ).
cnf(586,plain,
equal(op1(j(e22),e11),j(e23)),
inference(rew,[status(thm),theory(equality)],[564,176]),
[iquote('5:Rew:564.0,176.0')] ).
cnf(592,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[62,580]),
[iquote('5:Rew:62.0,580.0')] ).
cnf(595,plain,
equal(op1(j(e23),e10),e10),
inference(rew,[status(thm),theory(equality)],[592,549]),
[iquote('5:Rew:592.0,549.0')] ).
cnf(600,plain,
equal(op1(e10,e10),j(e22)),
inference(rew,[status(thm),theory(equality)],[592,184]),
[iquote('5:Rew:592.0,184.0')] ).
cnf(605,plain,
equal(j(e23),e10),
inference(rew,[status(thm),theory(equality)],[559,595]),
[iquote('5:Rew:559.0,595.0')] ).
cnf(612,plain,
equal(j(e22),e10),
inference(rew,[status(thm),theory(equality)],[56,600]),
[iquote('5:Rew:56.0,600.0')] ).
cnf(634,plain,
equal(e11,e10),
inference(rew,[status(thm),theory(equality)],[57,586,612,605]),
[iquote('5:Rew:57.0,586.0,612.0,586.0,605.0,586.0')] ).
cnf(635,plain,
$false,
inference(mrr,[status(thm)],[634,1]),
[iquote('5:MRR:634.0,1.0')] ).
cnf(639,plain,
~ equal(h(e11),e24),
inference(spt,[spt(split,[position(s2s2s2s2sa)])],[635,563]),
[iquote('5:Spt:635.0,164.0,563.0')] ).
cnf(640,plain,
( equal(h(e11),e23)
| equal(h(e11),e22)
| equal(h(e11),e21)
| equal(h(e11),e20) ),
inference(spt,[spt(split,[position(s2s2s2s2s2)])],[164]),
[iquote('5:Spt:635.0,164.1,164.2,164.3,164.4')] ).
cnf(641,plain,
equal(h(e11),e23),
inference(spt,[spt(split,[position(s2s2s2s2s2s1)])],[640]),
[iquote('6:Spt:640.0')] ).
cnf(642,plain,
equal(j(e23),e11),
inference(rew,[status(thm),theory(equality)],[641,52]),
[iquote('6:Rew:641.0,52.0')] ).
cnf(667,plain,
equal(op1(j(e21),j(e22)),e11),
inference(rew,[status(thm),theory(equality)],[642,183]),
[iquote('6:Rew:642.0,183.0')] ).
cnf(668,plain,
equal(op1(e11,e11),j(e21)),
inference(rew,[status(thm),theory(equality)],[642,172]),
[iquote('6:Rew:642.0,172.0')] ).
cnf(671,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[62,668]),
[iquote('6:Rew:62.0,668.0')] ).
cnf(678,plain,
equal(op1(e10,e10),j(e22)),
inference(rew,[status(thm),theory(equality)],[671,184]),
[iquote('6:Rew:671.0,184.0')] ).
cnf(692,plain,
equal(j(e22),e10),
inference(rew,[status(thm),theory(equality)],[56,678]),
[iquote('6:Rew:56.0,678.0')] ).
cnf(714,plain,
equal(e11,e10),
inference(rew,[status(thm),theory(equality)],[56,667,671,692]),
[iquote('6:Rew:56.0,667.0,671.0,667.0,692.0,667.0')] ).
cnf(715,plain,
$false,
inference(mrr,[status(thm)],[714,1]),
[iquote('6:MRR:714.0,1.0')] ).
cnf(719,plain,
~ equal(h(e11),e23),
inference(spt,[spt(split,[position(s2s2s2s2s2sa)])],[715,641]),
[iquote('6:Spt:715.0,640.0,641.0')] ).
cnf(720,plain,
( equal(h(e11),e22)
| equal(h(e11),e21)
| equal(h(e11),e20) ),
inference(spt,[spt(split,[position(s2s2s2s2s2s2)])],[640]),
[iquote('6:Spt:715.0,640.1,640.2,640.3')] ).
cnf(721,plain,
equal(h(e11),e22),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s1)])],[720]),
[iquote('7:Spt:720.0')] ).
cnf(723,plain,
equal(j(e22),e11),
inference(rew,[status(thm),theory(equality)],[721,52]),
[iquote('7:Rew:721.0,52.0')] ).
cnf(747,plain,
equal(op1(e11,e11),j(e21)),
inference(rew,[status(thm),theory(equality)],[723,178]),
[iquote('7:Rew:723.0,178.0')] ).
cnf(749,plain,
equal(op1(e11,j(e21)),j(e24)),
inference(rew,[status(thm),theory(equality)],[723,179]),
[iquote('7:Rew:723.0,179.0')] ).
cnf(752,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[62,747]),
[iquote('7:Rew:62.0,747.0')] ).
cnf(757,plain,
equal(op1(e10,j(e24)),e10),
inference(rew,[status(thm),theory(equality)],[752,552]),
[iquote('7:Rew:752.0,552.0')] ).
cnf(773,plain,
equal(j(e24),e10),
inference(rew,[status(thm),theory(equality)],[558,757]),
[iquote('7:Rew:558.0,757.0')] ).
cnf(794,plain,
equal(e11,e10),
inference(rew,[status(thm),theory(equality)],[61,749,752,773]),
[iquote('7:Rew:61.0,749.0,752.0,749.0,773.0,749.0')] ).
cnf(795,plain,
$false,
inference(mrr,[status(thm)],[794,1]),
[iquote('7:MRR:794.0,1.0')] ).
cnf(800,plain,
~ equal(h(e11),e22),
inference(spt,[spt(split,[position(s2s2s2s2s2s2sa)])],[795,721]),
[iquote('7:Spt:795.0,720.0,721.0')] ).
cnf(801,plain,
( equal(h(e11),e21)
| equal(h(e11),e20) ),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2)])],[720]),
[iquote('7:Spt:795.0,720.1,720.2')] ).
cnf(802,plain,
equal(h(e11),e21),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s1)])],[801]),
[iquote('8:Spt:801.0')] ).
cnf(804,plain,
equal(j(e21),e11),
inference(rew,[status(thm),theory(equality)],[802,52]),
[iquote('8:Rew:802.0,52.0')] ).
cnf(825,plain,
equal(op1(e11,e11),j(e22)),
inference(rew,[status(thm),theory(equality)],[804,184]),
[iquote('8:Rew:804.0,184.0')] ).
cnf(831,plain,
equal(op1(j(e23),j(e23)),e11),
inference(rew,[status(thm),theory(equality)],[804,172]),
[iquote('8:Rew:804.0,172.0')] ).
cnf(834,plain,
equal(j(e22),e10),
inference(rew,[status(thm),theory(equality)],[62,825]),
[iquote('8:Rew:62.0,825.0')] ).
cnf(839,plain,
equal(op1(e10,j(e23)),e10),
inference(rew,[status(thm),theory(equality)],[834,553]),
[iquote('8:Rew:834.0,553.0')] ).
cnf(855,plain,
equal(j(e23),e10),
inference(rew,[status(thm),theory(equality)],[560,839]),
[iquote('8:Rew:560.0,839.0')] ).
cnf(876,plain,
equal(e11,e10),
inference(rew,[status(thm),theory(equality)],[56,831,855]),
[iquote('8:Rew:56.0,831.0,855.0,831.0')] ).
cnf(877,plain,
$false,
inference(mrr,[status(thm)],[876,1]),
[iquote('8:MRR:876.0,1.0')] ).
cnf(882,plain,
~ equal(h(e11),e21),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2sa)])],[877,802]),
[iquote('8:Spt:877.0,801.0,802.0')] ).
cnf(883,plain,
equal(h(e11),e20),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2)])],[801]),
[iquote('8:Spt:877.0,801.1')] ).
cnf(894,plain,
equal(h(e14),h(e13)),
inference(rew,[status(thm),theory(equality)],[537,194,883]),
[iquote('8:Rew:537.0,194.0,883.0,194.0')] ).
cnf(896,plain,
equal(op2(h(e13),h(e13)),h(e12)),
inference(rew,[status(thm),theory(equality)],[894,191]),
[iquote('8:Rew:894.0,191.0')] ).
cnf(907,plain,
equal(h(e13),h(e12)),
inference(rew,[status(thm),theory(equality)],[539,199,883]),
[iquote('8:Rew:539.0,199.0,883.0,199.0')] ).
cnf(912,plain,
equal(op2(h(e12),h(e12)),e20),
inference(rew,[status(thm),theory(equality)],[907,540]),
[iquote('8:Rew:907.0,540.0')] ).
cnf(924,plain,
equal(h(e12),e20),
inference(rew,[status(thm),theory(equality)],[912,896,907]),
[iquote('8:Rew:912.0,896.0,907.0,896.0')] ).
cnf(925,plain,
equal(j(e20),e12),
inference(rew,[status(thm),theory(equality)],[924,53]),
[iquote('8:Rew:924.0,53.0')] ).
cnf(931,plain,
equal(e12,e10),
inference(rew,[status(thm),theory(equality)],[532,925]),
[iquote('8:Rew:532.0,925.0')] ).
cnf(932,plain,
$false,
inference(mrr,[status(thm)],[931,2]),
[iquote('8:MRR:931.0,2.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : ALG079+1 : TPTP v8.1.0. Released v2.7.0.
% 0.11/0.13 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n024.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Wed Jun 8 23:09:04 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.20/0.49
% 0.20/0.49 SPASS V 3.9
% 0.20/0.49 SPASS beiseite: Proof found.
% 0.20/0.49 % SZS status Theorem
% 0.20/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.49 SPASS derived 404 clauses, backtracked 404 clauses, performed 8 splits and kept 777 clauses.
% 0.20/0.49 SPASS allocated 85568 KBytes.
% 0.20/0.49 SPASS spent 0:00:00.13 on the problem.
% 0.20/0.49 0:00:00.04 for the input.
% 0.20/0.49 0:00:00.03 for the FLOTTER CNF translation.
% 0.20/0.49 0:00:00.00 for inferences.
% 0.20/0.49 0:00:00.00 for the backtracking.
% 0.20/0.49 0:00:00.04 for the reduction.
% 0.20/0.49
% 0.20/0.49
% 0.20/0.49 Here is a proof with depth 4, length 193 :
% 0.20/0.49 % SZS output start Refutation
% See solution above
% 0.20/0.49 Formulae used in the proof : ax1 ax2 co1 ax4 ax5
% 0.20/0.49
%------------------------------------------------------------------------------