%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG085+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.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:17 EDT 2022
% Result : Theorem 0.20s 0.49s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 67
% Syntax : Number of clauses : 219 ( 211 unt; 8 nHn; 219 RR)
% Number of literals : 239 ( 0 equ; 16 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(3,axiom,
~ equal(e13,e10),
file('ALG085+1.p',unknown),
[] ).
cnf(6,axiom,
~ equal(e13,e11),
file('ALG085+1.p',unknown),
[] ).
cnf(9,axiom,
~ equal(e14,e12),
file('ALG085+1.p',unknown),
[] ).
cnf(11,axiom,
~ equal(e21,e20),
file('ALG085+1.p',unknown),
[] ).
cnf(13,axiom,
~ equal(e23,e20),
file('ALG085+1.p',unknown),
[] ).
cnf(14,axiom,
~ equal(e24,e20),
file('ALG085+1.p',unknown),
[] ).
cnf(17,axiom,
~ equal(e24,e21),
file('ALG085+1.p',unknown),
[] ).
cnf(19,axiom,
~ equal(e24,e22),
file('ALG085+1.p',unknown),
[] ).
cnf(46,axiom,
equal(h(j(e20)),e20),
file('ALG085+1.p',unknown),
[] ).
cnf(47,axiom,
equal(h(j(e21)),e21),
file('ALG085+1.p',unknown),
[] ).
cnf(50,axiom,
equal(h(j(e24)),e24),
file('ALG085+1.p',unknown),
[] ).
cnf(51,axiom,
equal(j(h(e10)),e10),
file('ALG085+1.p',unknown),
[] ).
cnf(52,axiom,
equal(j(h(e11)),e11),
file('ALG085+1.p',unknown),
[] ).
cnf(53,axiom,
equal(j(h(e12)),e12),
file('ALG085+1.p',unknown),
[] ).
cnf(54,axiom,
equal(j(h(e13)),e13),
file('ALG085+1.p',unknown),
[] ).
cnf(55,axiom,
equal(j(h(e14)),e14),
file('ALG085+1.p',unknown),
[] ).
cnf(56,axiom,
equal(op1(e10,e10),e10),
file('ALG085+1.p',unknown),
[] ).
cnf(58,axiom,
equal(op1(e10,e12),e12),
file('ALG085+1.p',unknown),
[] ).
cnf(59,axiom,
equal(op1(e10,e13),e13),
file('ALG085+1.p',unknown),
[] ).
cnf(62,axiom,
equal(op1(e11,e11),e14),
file('ALG085+1.p',unknown),
[] ).
cnf(64,axiom,
equal(op1(e11,e13),e12),
file('ALG085+1.p',unknown),
[] ).
cnf(65,axiom,
equal(op1(e11,e14),e13),
file('ALG085+1.p',unknown),
[] ).
cnf(66,axiom,
equal(op1(e12,e10),e12),
file('ALG085+1.p',unknown),
[] ).
cnf(67,axiom,
equal(op1(e12,e11),e10),
file('ALG085+1.p',unknown),
[] ).
cnf(76,axiom,
equal(op1(e14,e10),e14),
file('ALG085+1.p',unknown),
[] ).
cnf(78,axiom,
equal(op1(e14,e12),e11),
file('ALG085+1.p',unknown),
[] ).
cnf(79,axiom,
equal(op1(e14,e13),e10),
file('ALG085+1.p',unknown),
[] ).
cnf(80,axiom,
equal(op1(e14,e14),e12),
file('ALG085+1.p',unknown),
[] ).
cnf(81,axiom,
equal(op2(e20,e20),e20),
file('ALG085+1.p',unknown),
[] ).
cnf(87,axiom,
equal(op2(e21,e21),e22),
file('ALG085+1.p',unknown),
[] ).
cnf(88,axiom,
equal(op2(e21,e22),e24),
file('ALG085+1.p',unknown),
[] ).
cnf(89,axiom,
equal(op2(e21,e23),e20),
file('ALG085+1.p',unknown),
[] ).
cnf(91,axiom,
equal(op2(e22,e20),e22),
file('ALG085+1.p',unknown),
[] ).
cnf(93,axiom,
equal(op2(e22,e22),e23),
file('ALG085+1.p',unknown),
[] ).
cnf(94,axiom,
equal(op2(e22,e23),e24),
file('ALG085+1.p',unknown),
[] ).
cnf(95,axiom,
equal(op2(e22,e24),e21),
file('ALG085+1.p',unknown),
[] ).
cnf(96,axiom,
equal(op2(e23,e20),e23),
file('ALG085+1.p',unknown),
[] ).
cnf(97,axiom,
equal(op2(e23,e21),e24),
file('ALG085+1.p',unknown),
[] ).
cnf(99,axiom,
equal(op2(e23,e23),e21),
file('ALG085+1.p',unknown),
[] ).
cnf(100,axiom,
equal(op2(e23,e24),e22),
file('ALG085+1.p',unknown),
[] ).
cnf(101,axiom,
equal(op2(e24,e20),e24),
file('ALG085+1.p',unknown),
[] ).
cnf(103,axiom,
equal(op2(e24,e22),e21),
file('ALG085+1.p',unknown),
[] ).
cnf(105,axiom,
equal(op2(e24,e24),e20),
file('ALG085+1.p',unknown),
[] ).
cnf(109,axiom,
equal(op2(h(e10),h(e13)),h(op1(e10,e13))),
file('ALG085+1.p',unknown),
[] ).
cnf(112,axiom,
equal(op2(h(e11),h(e11)),h(op1(e11,e11))),
file('ALG085+1.p',unknown),
[] ).
cnf(114,axiom,
equal(op2(h(e11),h(e13)),h(op1(e11,e13))),
file('ALG085+1.p',unknown),
[] ).
cnf(116,axiom,
equal(op2(h(e12),h(e10)),h(op1(e12,e10))),
file('ALG085+1.p',unknown),
[] ).
cnf(117,axiom,
equal(op2(h(e12),h(e11)),h(op1(e12,e11))),
file('ALG085+1.p',unknown),
[] ).
cnf(126,axiom,
equal(op2(h(e14),h(e10)),h(op1(e14,e10))),
file('ALG085+1.p',unknown),
[] ).
cnf(128,axiom,
equal(op2(h(e14),h(e12)),h(op1(e14,e12))),
file('ALG085+1.p',unknown),
[] ).
cnf(129,axiom,
equal(op2(h(e14),h(e13)),h(op1(e14,e13))),
file('ALG085+1.p',unknown),
[] ).
cnf(130,axiom,
equal(op2(h(e14),h(e14)),h(op1(e14,e14))),
file('ALG085+1.p',unknown),
[] ).
cnf(137,axiom,
equal(op1(j(e21),j(e21)),j(op2(e21,e21))),
file('ALG085+1.p',unknown),
[] ).
cnf(138,axiom,
equal(op1(j(e21),j(e22)),j(op2(e21,e22))),
file('ALG085+1.p',unknown),
[] ).
cnf(139,axiom,
equal(op1(j(e21),j(e23)),j(op2(e21,e23))),
file('ALG085+1.p',unknown),
[] ).
cnf(141,axiom,
equal(op1(j(e22),j(e20)),j(op2(e22,e20))),
file('ALG085+1.p',unknown),
[] ).
cnf(143,axiom,
equal(op1(j(e22),j(e22)),j(op2(e22,e22))),
file('ALG085+1.p',unknown),
[] ).
cnf(144,axiom,
equal(op1(j(e22),j(e23)),j(op2(e22,e23))),
file('ALG085+1.p',unknown),
[] ).
cnf(145,axiom,
equal(op1(j(e22),j(e24)),j(op2(e22,e24))),
file('ALG085+1.p',unknown),
[] ).
cnf(146,axiom,
equal(op1(j(e23),j(e20)),j(op2(e23,e20))),
file('ALG085+1.p',unknown),
[] ).
cnf(147,axiom,
equal(op1(j(e23),j(e21)),j(op2(e23,e21))),
file('ALG085+1.p',unknown),
[] ).
cnf(149,axiom,
equal(op1(j(e23),j(e23)),j(op2(e23,e23))),
file('ALG085+1.p',unknown),
[] ).
cnf(150,axiom,
equal(op1(j(e23),j(e24)),j(op2(e23,e24))),
file('ALG085+1.p',unknown),
[] ).
cnf(153,axiom,
equal(op1(j(e24),j(e22)),j(op2(e24,e22))),
file('ALG085+1.p',unknown),
[] ).
cnf(155,axiom,
equal(op1(j(e24),j(e24)),j(op2(e24,e24))),
file('ALG085+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('ALG085+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('ALG085+1.p',unknown),
[] ).
cnf(166,plain,
equal(op1(j(e24),j(e24)),j(e20)),
inference(rew,[status(thm),theory(equality)],[105,155]),
[iquote('0:Rew:105.0,155.0')] ).
cnf(168,plain,
equal(op1(j(e24),j(e22)),j(e21)),
inference(rew,[status(thm),theory(equality)],[103,153]),
[iquote('0:Rew:103.0,153.0')] ).
cnf(171,plain,
equal(op1(j(e23),j(e24)),j(e22)),
inference(rew,[status(thm),theory(equality)],[100,150]),
[iquote('0:Rew:100.0,150.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(174,plain,
equal(op1(j(e23),j(e21)),j(e24)),
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(e21)),
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(e24)),
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(e23)),
inference(rew,[status(thm),theory(equality)],[93,143]),
[iquote('0:Rew:93.0,143.0')] ).
cnf(180,plain,
equal(op1(j(e22),j(e20)),j(e22)),
inference(rew,[status(thm),theory(equality)],[91,141]),
[iquote('0:Rew:91.0,141.0')] ).
cnf(182,plain,
equal(op1(j(e21),j(e23)),j(e20)),
inference(rew,[status(thm),theory(equality)],[89,139]),
[iquote('0:Rew:89.0,139.0')] ).
cnf(183,plain,
equal(op1(j(e21),j(e22)),j(e24)),
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(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(192,plain,
equal(op2(h(e14),h(e13)),h(e10)),
inference(rew,[status(thm),theory(equality)],[79,129]),
[iquote('0:Rew:79.0,129.0')] ).
cnf(193,plain,
equal(op2(h(e14),h(e12)),h(e11)),
inference(rew,[status(thm),theory(equality)],[78,128]),
[iquote('0:Rew:78.0,128.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(204,plain,
equal(op2(h(e12),h(e11)),h(e10)),
inference(rew,[status(thm),theory(equality)],[67,117]),
[iquote('0:Rew:67.0,117.0')] ).
cnf(205,plain,
equal(op2(h(e12),h(e10)),h(e12)),
inference(rew,[status(thm),theory(equality)],[66,116]),
[iquote('0:Rew:66.0,116.0')] ).
cnf(207,plain,
equal(op2(h(e11),h(e13)),h(e12)),
inference(rew,[status(thm),theory(equality)],[64,114]),
[iquote('0:Rew:64.0,114.0')] ).
cnf(209,plain,
equal(op2(h(e11),h(e11)),h(e14)),
inference(rew,[status(thm),theory(equality)],[62,112]),
[iquote('0:Rew:62.0,112.0')] ).
cnf(212,plain,
equal(op2(h(e10),h(e13)),h(e13)),
inference(rew,[status(thm),theory(equality)],[59,109]),
[iquote('0:Rew:59.0,109.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(e20)),
inference(rew,[status(thm),theory(equality)],[217,166]),
[iquote('1:Rew:217.0,166.0')] ).
cnf(237,plain,
equal(op1(j(e23),e10),j(e22)),
inference(rew,[status(thm),theory(equality)],[217,171]),
[iquote('1:Rew:217.0,171.0')] ).
cnf(239,plain,
equal(op1(j(e22),e10),j(e21)),
inference(rew,[status(thm),theory(equality)],[217,176]),
[iquote('1:Rew:217.0,176.0')] ).
cnf(246,plain,
equal(j(e20),e10),
inference(rew,[status(thm),theory(equality)],[56,232]),
[iquote('1:Rew:56.0,232.0')] ).
cnf(249,plain,
equal(op1(j(e23),e10),j(e23)),
inference(rew,[status(thm),theory(equality)],[246,175]),
[iquote('1:Rew:246.0,175.0')] ).
cnf(251,plain,
equal(op1(j(e22),e10),j(e22)),
inference(rew,[status(thm),theory(equality)],[246,180]),
[iquote('1:Rew:246.0,180.0')] ).
cnf(252,plain,
equal(op1(j(e21),j(e23)),e10),
inference(rew,[status(thm),theory(equality)],[246,182]),
[iquote('1:Rew:246.0,182.0')] ).
cnf(262,plain,
equal(j(e23),j(e22)),
inference(rew,[status(thm),theory(equality)],[237,249]),
[iquote('1:Rew:237.0,249.0')] ).
cnf(264,plain,
equal(op1(j(e22),j(e22)),j(e21)),
inference(rew,[status(thm),theory(equality)],[262,172]),
[iquote('1:Rew:262.0,172.0')] ).
cnf(276,plain,
equal(j(e22),j(e21)),
inference(rew,[status(thm),theory(equality)],[239,251]),
[iquote('1:Rew:239.0,251.0')] ).
cnf(283,plain,
equal(j(e23),j(e21)),
inference(rew,[status(thm),theory(equality)],[276,262]),
[iquote('1:Rew:276.0,262.0')] ).
cnf(287,plain,
equal(op1(j(e21),j(e21)),e10),
inference(rew,[status(thm),theory(equality)],[283,252]),
[iquote('1:Rew:283.0,252.0')] ).
cnf(297,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[287,264,276]),
[iquote('1:Rew:287.0,264.0,276.0,264.0')] ).
cnf(298,plain,
equal(h(e10),e21),
inference(rew,[status(thm),theory(equality)],[297,47]),
[iquote('1:Rew:297.0,47.0')] ).
cnf(304,plain,
equal(e24,e21),
inference(rew,[status(thm),theory(equality)],[216,298]),
[iquote('1:Rew:216.0,298.0')] ).
cnf(305,plain,
$false,
inference(mrr,[status(thm)],[304,17]),
[iquote('1:MRR:304.0,17.0')] ).
cnf(308,plain,
~ equal(h(e10),e24),
inference(spt,[spt(split,[position(sa)])],[305,216]),
[iquote('1:Spt:305.0,165.0,216.0')] ).
cnf(309,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:305.0,165.1,165.2,165.3,165.4')] ).
cnf(310,plain,
equal(h(e10),e23),
inference(spt,[spt(split,[position(s2s1)])],[309]),
[iquote('2:Spt:309.0')] ).
cnf(311,plain,
equal(j(e23),e10),
inference(rew,[status(thm),theory(equality)],[310,51]),
[iquote('2:Rew:310.0,51.0')] ).
cnf(328,plain,
equal(op1(j(e22),e10),j(e24)),
inference(rew,[status(thm),theory(equality)],[311,177]),
[iquote('2:Rew:311.0,177.0')] ).
cnf(338,plain,
equal(op1(e10,e10),j(e21)),
inference(rew,[status(thm),theory(equality)],[311,172]),
[iquote('2:Rew:311.0,172.0')] ).
cnf(341,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[56,338]),
[iquote('2:Rew:56.0,338.0')] ).
cnf(349,plain,
equal(op1(e10,e10),j(e22)),
inference(rew,[status(thm),theory(equality)],[341,184]),
[iquote('2:Rew:341.0,184.0')] ).
cnf(352,plain,
equal(j(e22),e10),
inference(rew,[status(thm),theory(equality)],[56,349]),
[iquote('2:Rew:56.0,349.0')] ).
cnf(359,plain,
equal(j(e24),e10),
inference(rew,[status(thm),theory(equality)],[56,328,352]),
[iquote('2:Rew:56.0,328.0,352.0,328.0')] ).
cnf(363,plain,
equal(op1(e10,e10),j(e20)),
inference(rew,[status(thm),theory(equality)],[359,166]),
[iquote('2:Rew:359.0,166.0')] ).
cnf(367,plain,
equal(j(e20),e10),
inference(rew,[status(thm),theory(equality)],[56,363]),
[iquote('2:Rew:56.0,363.0')] ).
cnf(368,plain,
equal(h(e10),e20),
inference(rew,[status(thm),theory(equality)],[367,46]),
[iquote('2:Rew:367.0,46.0')] ).
cnf(372,plain,
equal(e23,e20),
inference(rew,[status(thm),theory(equality)],[310,368]),
[iquote('2:Rew:310.0,368.0')] ).
cnf(373,plain,
$false,
inference(mrr,[status(thm)],[372,13]),
[iquote('2:MRR:372.0,13.0')] ).
cnf(385,plain,
~ equal(h(e10),e23),
inference(spt,[spt(split,[position(s2sa)])],[373,310]),
[iquote('2:Spt:373.0,309.0,310.0')] ).
cnf(386,plain,
( equal(h(e10),e22)
| equal(h(e10),e21)
| equal(h(e10),e20) ),
inference(spt,[spt(split,[position(s2s2)])],[309]),
[iquote('2:Spt:373.0,309.1,309.2,309.3')] ).
cnf(387,plain,
equal(h(e10),e22),
inference(spt,[spt(split,[position(s2s2s1)])],[386]),
[iquote('3:Spt:386.0')] ).
cnf(389,plain,
equal(j(e22),e10),
inference(rew,[status(thm),theory(equality)],[387,51]),
[iquote('3:Rew:387.0,51.0')] ).
cnf(405,plain,
equal(op1(e10,e10),j(e23)),
inference(rew,[status(thm),theory(equality)],[389,178]),
[iquote('3:Rew:389.0,178.0')] ).
cnf(409,plain,
equal(op1(e10,j(e23)),j(e24)),
inference(rew,[status(thm),theory(equality)],[389,177]),
[iquote('3:Rew:389.0,177.0')] ).
cnf(419,plain,
equal(j(e23),e10),
inference(rew,[status(thm),theory(equality)],[56,405]),
[iquote('3:Rew:56.0,405.0')] ).
cnf(448,plain,
equal(j(e24),e10),
inference(rew,[status(thm),theory(equality)],[56,409,419]),
[iquote('3:Rew:56.0,409.0,419.0,409.0')] ).
cnf(449,plain,
equal(h(e10),e24),
inference(rew,[status(thm),theory(equality)],[448,50]),
[iquote('3:Rew:448.0,50.0')] ).
cnf(452,plain,
equal(e24,e22),
inference(rew,[status(thm),theory(equality)],[387,449]),
[iquote('3:Rew:387.0,449.0')] ).
cnf(453,plain,
$false,
inference(mrr,[status(thm)],[452,19]),
[iquote('3:MRR:452.0,19.0')] ).
cnf(466,plain,
~ equal(h(e10),e22),
inference(spt,[spt(split,[position(s2s2sa)])],[453,387]),
[iquote('3:Spt:453.0,386.0,387.0')] ).
cnf(467,plain,
( equal(h(e10),e21)
| equal(h(e10),e20) ),
inference(spt,[spt(split,[position(s2s2s2)])],[386]),
[iquote('3:Spt:453.0,386.1,386.2')] ).
cnf(468,plain,
equal(h(e10),e21),
inference(spt,[spt(split,[position(s2s2s2s1)])],[467]),
[iquote('4:Spt:467.0')] ).
cnf(470,plain,
equal(j(e21),e10),
inference(rew,[status(thm),theory(equality)],[468,51]),
[iquote('4:Rew:468.0,51.0')] ).
cnf(487,plain,
equal(op1(e10,j(e22)),j(e24)),
inference(rew,[status(thm),theory(equality)],[470,183]),
[iquote('4:Rew:470.0,183.0')] ).
cnf(491,plain,
equal(op1(e10,e10),j(e22)),
inference(rew,[status(thm),theory(equality)],[470,184]),
[iquote('4:Rew:470.0,184.0')] ).
cnf(501,plain,
equal(j(e22),e10),
inference(rew,[status(thm),theory(equality)],[56,491]),
[iquote('4:Rew:56.0,491.0')] ).
cnf(518,plain,
equal(j(e24),e10),
inference(rew,[status(thm),theory(equality)],[56,487,501]),
[iquote('4:Rew:56.0,487.0,501.0,487.0')] ).
cnf(522,plain,
equal(op1(e10,e10),j(e20)),
inference(rew,[status(thm),theory(equality)],[518,166]),
[iquote('4:Rew:518.0,166.0')] ).
cnf(525,plain,
equal(j(e20),e10),
inference(rew,[status(thm),theory(equality)],[56,522]),
[iquote('4:Rew:56.0,522.0')] ).
cnf(526,plain,
equal(h(e10),e20),
inference(rew,[status(thm),theory(equality)],[525,46]),
[iquote('4:Rew:525.0,46.0')] ).
cnf(530,plain,
equal(e21,e20),
inference(rew,[status(thm),theory(equality)],[468,526]),
[iquote('4:Rew:468.0,526.0')] ).
cnf(531,plain,
$false,
inference(mrr,[status(thm)],[530,11]),
[iquote('4:MRR:530.0,11.0')] ).
cnf(544,plain,
~ equal(h(e10),e21),
inference(spt,[spt(split,[position(s2s2s2sa)])],[531,468]),
[iquote('4:Spt:531.0,467.0,468.0')] ).
cnf(545,plain,
equal(h(e10),e20),
inference(spt,[spt(split,[position(s2s2s2s2)])],[467]),
[iquote('4:Spt:531.0,467.1')] ).
cnf(548,plain,
equal(j(e20),e10),
inference(rew,[status(thm),theory(equality)],[545,51]),
[iquote('4:Rew:545.0,51.0')] ).
cnf(552,plain,
equal(op2(h(e14),h(e13)),e20),
inference(rew,[status(thm),theory(equality)],[545,192]),
[iquote('4:Rew:545.0,192.0')] ).
cnf(553,plain,
equal(op2(h(e14),e20),h(e14)),
inference(rew,[status(thm),theory(equality)],[545,195]),
[iquote('4:Rew:545.0,195.0')] ).
cnf(556,plain,
equal(op2(h(e12),h(e11)),e20),
inference(rew,[status(thm),theory(equality)],[545,204]),
[iquote('4:Rew:545.0,204.0')] ).
cnf(557,plain,
equal(op2(h(e12),e20),h(e12)),
inference(rew,[status(thm),theory(equality)],[545,205]),
[iquote('4:Rew:545.0,205.0')] ).
cnf(561,plain,
equal(op2(e20,h(e13)),h(e13)),
inference(rew,[status(thm),theory(equality)],[545,212]),
[iquote('4:Rew:545.0,212.0')] ).
cnf(579,plain,
equal(h(e11),e24),
inference(spt,[spt(split,[position(s2s2s2s2s1)])],[164]),
[iquote('5:Spt:164.0')] ).
cnf(587,plain,
equal(op2(e24,h(e13)),h(e12)),
inference(rew,[status(thm),theory(equality)],[579,207]),
[iquote('5:Rew:579.0,207.0')] ).
cnf(588,plain,
equal(op2(e24,e24),h(e14)),
inference(rew,[status(thm),theory(equality)],[579,209]),
[iquote('5:Rew:579.0,209.0')] ).
cnf(608,plain,
equal(h(e14),e20),
inference(rew,[status(thm),theory(equality)],[105,588]),
[iquote('5:Rew:105.0,588.0')] ).
cnf(610,plain,
equal(op2(e20,e20),h(e12)),
inference(rew,[status(thm),theory(equality)],[608,191]),
[iquote('5:Rew:608.0,191.0')] ).
cnf(613,plain,
equal(op2(e20,h(e13)),e20),
inference(rew,[status(thm),theory(equality)],[608,552]),
[iquote('5:Rew:608.0,552.0')] ).
cnf(619,plain,
equal(h(e12),e20),
inference(rew,[status(thm),theory(equality)],[81,610]),
[iquote('5:Rew:81.0,610.0')] ).
cnf(632,plain,
equal(h(e13),e20),
inference(rew,[status(thm),theory(equality)],[561,613]),
[iquote('5:Rew:561.0,613.0')] ).
cnf(652,plain,
equal(e24,e20),
inference(rew,[status(thm),theory(equality)],[101,587,632,619]),
[iquote('5:Rew:101.0,587.0,632.0,587.0,619.0,587.0')] ).
cnf(653,plain,
$false,
inference(mrr,[status(thm)],[652,14]),
[iquote('5:MRR:652.0,14.0')] ).
cnf(656,plain,
~ equal(h(e11),e24),
inference(spt,[spt(split,[position(s2s2s2s2sa)])],[653,579]),
[iquote('5:Spt:653.0,164.0,579.0')] ).
cnf(657,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:653.0,164.1,164.2,164.3,164.4')] ).
cnf(658,plain,
equal(h(e11),e23),
inference(spt,[spt(split,[position(s2s2s2s2s2s1)])],[657]),
[iquote('6:Spt:657.0')] ).
cnf(659,plain,
equal(j(e23),e11),
inference(rew,[status(thm),theory(equality)],[658,52]),
[iquote('6:Rew:658.0,52.0')] ).
cnf(665,plain,
equal(op2(e23,e23),h(e14)),
inference(rew,[status(thm),theory(equality)],[658,209]),
[iquote('6:Rew:658.0,209.0')] ).
cnf(680,plain,
equal(op1(j(e22),e11),j(e24)),
inference(rew,[status(thm),theory(equality)],[659,177]),
[iquote('6:Rew:659.0,177.0')] ).
cnf(686,plain,
equal(h(e14),e21),
inference(rew,[status(thm),theory(equality)],[99,665]),
[iquote('6:Rew:99.0,665.0')] ).
cnf(687,plain,
equal(j(e21),e14),
inference(rew,[status(thm),theory(equality)],[686,55]),
[iquote('6:Rew:686.0,55.0')] ).
cnf(694,plain,
equal(op2(e21,e21),h(e12)),
inference(rew,[status(thm),theory(equality)],[686,191]),
[iquote('6:Rew:686.0,191.0')] ).
cnf(702,plain,
equal(op1(j(e24),j(e22)),e14),
inference(rew,[status(thm),theory(equality)],[687,168]),
[iquote('6:Rew:687.0,168.0')] ).
cnf(706,plain,
equal(h(e12),e22),
inference(rew,[status(thm),theory(equality)],[87,694]),
[iquote('6:Rew:87.0,694.0')] ).
cnf(707,plain,
equal(j(e22),e12),
inference(rew,[status(thm),theory(equality)],[706,53]),
[iquote('6:Rew:706.0,53.0')] ).
cnf(748,plain,
equal(j(e24),e10),
inference(rew,[status(thm),theory(equality)],[67,680,707]),
[iquote('6:Rew:67.0,680.0,707.0,680.0')] ).
cnf(773,plain,
equal(e14,e12),
inference(rew,[status(thm),theory(equality)],[58,702,748,707]),
[iquote('6:Rew:58.0,702.0,748.0,702.0,707.0,702.0')] ).
cnf(774,plain,
$false,
inference(mrr,[status(thm)],[773,9]),
[iquote('6:MRR:773.0,9.0')] ).
cnf(775,plain,
~ equal(h(e11),e23),
inference(spt,[spt(split,[position(s2s2s2s2s2sa)])],[774,658]),
[iquote('6:Spt:774.0,657.0,658.0')] ).
cnf(776,plain,
( equal(h(e11),e22)
| equal(h(e11),e21)
| equal(h(e11),e20) ),
inference(spt,[spt(split,[position(s2s2s2s2s2s2)])],[657]),
[iquote('6:Spt:774.0,657.1,657.2,657.3')] ).
cnf(777,plain,
equal(h(e11),e22),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s1)])],[776]),
[iquote('7:Spt:776.0')] ).
cnf(779,plain,
equal(j(e22),e11),
inference(rew,[status(thm),theory(equality)],[777,52]),
[iquote('7:Rew:777.0,52.0')] ).
cnf(792,plain,
equal(op2(e22,e22),h(e14)),
inference(rew,[status(thm),theory(equality)],[777,209]),
[iquote('7:Rew:777.0,209.0')] ).
cnf(800,plain,
equal(op1(e11,j(e23)),j(e24)),
inference(rew,[status(thm),theory(equality)],[779,177]),
[iquote('7:Rew:779.0,177.0')] ).
cnf(806,plain,
equal(h(e14),e23),
inference(rew,[status(thm),theory(equality)],[93,792]),
[iquote('7:Rew:93.0,792.0')] ).
cnf(807,plain,
equal(j(e23),e14),
inference(rew,[status(thm),theory(equality)],[806,55]),
[iquote('7:Rew:806.0,55.0')] ).
cnf(812,plain,
equal(op2(e23,e23),h(e12)),
inference(rew,[status(thm),theory(equality)],[806,191]),
[iquote('7:Rew:806.0,191.0')] ).
cnf(820,plain,
equal(op1(e14,j(e21)),j(e24)),
inference(rew,[status(thm),theory(equality)],[807,174]),
[iquote('7:Rew:807.0,174.0')] ).
cnf(826,plain,
equal(h(e12),e21),
inference(rew,[status(thm),theory(equality)],[99,812]),
[iquote('7:Rew:99.0,812.0')] ).
cnf(827,plain,
equal(j(e21),e12),
inference(rew,[status(thm),theory(equality)],[826,53]),
[iquote('7:Rew:826.0,53.0')] ).
cnf(868,plain,
equal(j(e24),e13),
inference(rew,[status(thm),theory(equality)],[65,800,807]),
[iquote('7:Rew:65.0,800.0,807.0,800.0')] ).
cnf(894,plain,
equal(e13,e11),
inference(rew,[status(thm),theory(equality)],[78,820,827,868]),
[iquote('7:Rew:78.0,820.0,827.0,820.0,868.0,820.0')] ).
cnf(895,plain,
$false,
inference(mrr,[status(thm)],[894,6]),
[iquote('7:MRR:894.0,6.0')] ).
cnf(897,plain,
~ equal(h(e11),e22),
inference(spt,[spt(split,[position(s2s2s2s2s2s2sa)])],[895,777]),
[iquote('7:Spt:895.0,776.0,777.0')] ).
cnf(898,plain,
( equal(h(e11),e21)
| equal(h(e11),e20) ),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2)])],[776]),
[iquote('7:Spt:895.0,776.1,776.2')] ).
cnf(899,plain,
equal(h(e11),e21),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s1)])],[898]),
[iquote('8:Spt:898.0')] ).
cnf(901,plain,
equal(j(e21),e11),
inference(rew,[status(thm),theory(equality)],[899,52]),
[iquote('8:Rew:899.0,52.0')] ).
cnf(908,plain,
equal(op2(e21,e21),h(e14)),
inference(rew,[status(thm),theory(equality)],[899,209]),
[iquote('8:Rew:899.0,209.0')] ).
cnf(922,plain,
equal(op1(e11,j(e22)),j(e24)),
inference(rew,[status(thm),theory(equality)],[901,183]),
[iquote('8:Rew:901.0,183.0')] ).
cnf(929,plain,
equal(h(e14),e22),
inference(rew,[status(thm),theory(equality)],[87,908]),
[iquote('8:Rew:87.0,908.0')] ).
cnf(930,plain,
equal(j(e22),e14),
inference(rew,[status(thm),theory(equality)],[929,55]),
[iquote('8:Rew:929.0,55.0')] ).
cnf(937,plain,
equal(op2(e22,e22),h(e12)),
inference(rew,[status(thm),theory(equality)],[929,191]),
[iquote('8:Rew:929.0,191.0')] ).
cnf(943,plain,
equal(op1(e14,j(e23)),j(e24)),
inference(rew,[status(thm),theory(equality)],[930,177]),
[iquote('8:Rew:930.0,177.0')] ).
cnf(949,plain,
equal(h(e12),e23),
inference(rew,[status(thm),theory(equality)],[93,937]),
[iquote('8:Rew:93.0,937.0')] ).
cnf(950,plain,
equal(j(e23),e12),
inference(rew,[status(thm),theory(equality)],[949,53]),
[iquote('8:Rew:949.0,53.0')] ).
cnf(989,plain,
equal(j(e24),e13),
inference(rew,[status(thm),theory(equality)],[65,922,930]),
[iquote('8:Rew:65.0,922.0,930.0,922.0')] ).
cnf(1012,plain,
equal(e13,e11),
inference(rew,[status(thm),theory(equality)],[78,943,950,989]),
[iquote('8:Rew:78.0,943.0,950.0,943.0,989.0,943.0')] ).
cnf(1013,plain,
$false,
inference(mrr,[status(thm)],[1012,6]),
[iquote('8:MRR:1012.0,6.0')] ).
cnf(1016,plain,
~ equal(h(e11),e21),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2sa)])],[1013,899]),
[iquote('8:Spt:1013.0,898.0,899.0')] ).
cnf(1017,plain,
equal(h(e11),e20),
inference(spt,[spt(split,[position(s2s2s2s2s2s2s2s2)])],[898]),
[iquote('8:Spt:1013.0,898.1')] ).
cnf(1024,plain,
equal(op2(h(e12),e20),e20),
inference(rew,[status(thm),theory(equality)],[1017,556]),
[iquote('8:Rew:1017.0,556.0')] ).
cnf(1028,plain,
equal(h(e12),e20),
inference(rew,[status(thm),theory(equality)],[1024,557]),
[iquote('8:Rew:1024.0,557.0')] ).
cnf(1035,plain,
equal(h(e14),e20),
inference(rew,[status(thm),theory(equality)],[553,193,1028,1017]),
[iquote('8:Rew:553.0,193.0,1028.0,193.0,1017.0,193.0')] ).
cnf(1037,plain,
equal(op2(e20,h(e13)),e20),
inference(rew,[status(thm),theory(equality)],[1035,552]),
[iquote('8:Rew:1035.0,552.0')] ).
cnf(1043,plain,
equal(h(e13),e20),
inference(rew,[status(thm),theory(equality)],[561,1037]),
[iquote('8:Rew:561.0,1037.0')] ).
cnf(1044,plain,
equal(j(e20),e13),
inference(rew,[status(thm),theory(equality)],[1043,54]),
[iquote('8:Rew:1043.0,54.0')] ).
cnf(1047,plain,
equal(e13,e10),
inference(rew,[status(thm),theory(equality)],[548,1044]),
[iquote('8:Rew:548.0,1044.0')] ).
cnf(1048,plain,
$false,
inference(mrr,[status(thm)],[1047,3]),
[iquote('8:MRR:1047.0,3.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : ALG085+1 : TPTP v8.1.0. Released v2.7.0.
% 0.10/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n017.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Thu Jun 9 05:15:19 EDT 2022
% 0.14/0.34 % 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/sandbox2/benchmark/theBenchmark.p
% 0.20/0.49 SPASS derived 464 clauses, backtracked 458 clauses, performed 8 splits and kept 852 clauses.
% 0.20/0.49 SPASS allocated 85609 KBytes.
% 0.20/0.49 SPASS spent 0:00:00.14 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 219 :
% 0.20/0.49 % SZS output start Refutation
% See solution above
% 0.20/0.50 Formulae used in the proof : ax1 ax2 co1 ax4 ax5
% 0.20/0.50
%------------------------------------------------------------------------------