%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : SWV558-1.007 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n015.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 : 300s
% DateTime : Wed Jul 27 13:21:11 EDT 2022
% Result : Unsatisfiable 1.96s 2.16s
% Output : Refutation 1.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 33
% Syntax : Number of clauses : 133 ( 133 unt; 0 nHn; 110 RR)
% Number of literals : 133 ( 132 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 39 ( 39 usr; 37 con; 0-3 aty)
% Number of variables : 29 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
a1 != a2,
file('SWV558-1.007.p',unknown),
[] ).
cnf(2,plain,
a2 != a1,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[1])]),
[iquote('copy,1,flip.1')] ).
cnf(4,axiom,
select(store(A,B,C),B) = C,
file('SWV558-1.007.p',unknown),
[] ).
cnf(7,axiom,
store(A,B,select(A,B)) = A,
file('SWV558-1.007.p',unknown),
[] ).
cnf(9,axiom,
store(store(A,B,C),B,D) = store(A,B,D),
file('SWV558-1.007.p',unknown),
[] ).
cnf(12,axiom,
a_29 = store(a1,i1,e_28),
file('SWV558-1.007.p',unknown),
[] ).
cnf(14,plain,
store(a1,i1,e_28) = a_29,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[12])]),
[iquote('copy,12,flip.1')] ).
cnf(15,axiom,
a_31 = store(a2,i1,e_30),
file('SWV558-1.007.p',unknown),
[] ).
cnf(16,plain,
store(a2,i1,e_30) = a_31,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[15])]),
[iquote('copy,15,flip.1')] ).
cnf(18,axiom,
a_33 = store(a_29,i2,e_32),
file('SWV558-1.007.p',unknown),
[] ).
cnf(20,plain,
store(a_29,i2,e_32) = a_33,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[18])]),
[iquote('copy,18,flip.1')] ).
cnf(21,axiom,
a_35 = store(a_31,i2,e_34),
file('SWV558-1.007.p',unknown),
[] ).
cnf(22,plain,
store(a_31,i2,e_34) = a_35,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[21])]),
[iquote('copy,21,flip.1')] ).
cnf(24,axiom,
a_37 = store(a_33,i3,e_36),
file('SWV558-1.007.p',unknown),
[] ).
cnf(26,plain,
store(a_33,i3,e_36) = a_37,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[24])]),
[iquote('copy,24,flip.1')] ).
cnf(27,axiom,
a_39 = store(a_35,i3,e_38),
file('SWV558-1.007.p',unknown),
[] ).
cnf(28,plain,
store(a_35,i3,e_38) = a_39,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[27])]),
[iquote('copy,27,flip.1')] ).
cnf(30,axiom,
a_41 = store(a_37,i4,e_40),
file('SWV558-1.007.p',unknown),
[] ).
cnf(32,plain,
store(a_37,i4,e_40) = a_41,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[30])]),
[iquote('copy,30,flip.1')] ).
cnf(33,axiom,
a_43 = store(a_39,i4,e_42),
file('SWV558-1.007.p',unknown),
[] ).
cnf(34,plain,
store(a_39,i4,e_42) = a_43,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[33])]),
[iquote('copy,33,flip.1')] ).
cnf(36,axiom,
a_45 = store(a_41,i5,e_44),
file('SWV558-1.007.p',unknown),
[] ).
cnf(38,plain,
store(a_41,i5,e_44) = a_45,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[36])]),
[iquote('copy,36,flip.1')] ).
cnf(39,axiom,
a_47 = store(a_43,i5,e_46),
file('SWV558-1.007.p',unknown),
[] ).
cnf(40,plain,
store(a_43,i5,e_46) = a_47,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[39])]),
[iquote('copy,39,flip.1')] ).
cnf(42,axiom,
a_49 = store(a_45,i6,e_48),
file('SWV558-1.007.p',unknown),
[] ).
cnf(44,plain,
store(a_45,i6,e_48) = a_49,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[42])]),
[iquote('copy,42,flip.1')] ).
cnf(45,axiom,
a_51 = store(a_47,i6,e_50),
file('SWV558-1.007.p',unknown),
[] ).
cnf(46,plain,
store(a_47,i6,e_50) = a_51,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[45])]),
[iquote('copy,45,flip.1')] ).
cnf(48,axiom,
a_53 = store(a_49,i7,e_52),
file('SWV558-1.007.p',unknown),
[] ).
cnf(50,plain,
store(a_49,i7,e_52) = a_53,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[48])]),
[iquote('copy,48,flip.1')] ).
cnf(51,axiom,
a_55 = store(a_51,i7,e_54),
file('SWV558-1.007.p',unknown),
[] ).
cnf(52,plain,
store(a_51,i7,e_54) = a_55,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[51])]),
[iquote('copy,51,flip.1')] ).
cnf(54,axiom,
e_28 = select(a2,i1),
file('SWV558-1.007.p',unknown),
[] ).
cnf(55,plain,
select(a2,i1) = e_28,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[54])]),
[iquote('copy,54,flip.1')] ).
cnf(57,axiom,
e_30 = select(a1,i1),
file('SWV558-1.007.p',unknown),
[] ).
cnf(58,plain,
select(a1,i1) = e_30,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[57])]),
[iquote('copy,57,flip.1')] ).
cnf(60,axiom,
e_32 = select(a_31,i2),
file('SWV558-1.007.p',unknown),
[] ).
cnf(61,plain,
select(a_31,i2) = e_32,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[60])]),
[iquote('copy,60,flip.1')] ).
cnf(63,axiom,
e_34 = select(a_29,i2),
file('SWV558-1.007.p',unknown),
[] ).
cnf(64,plain,
select(a_29,i2) = e_34,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[63])]),
[iquote('copy,63,flip.1')] ).
cnf(66,axiom,
e_36 = select(a_35,i3),
file('SWV558-1.007.p',unknown),
[] ).
cnf(67,plain,
select(a_35,i3) = e_36,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[66])]),
[iquote('copy,66,flip.1')] ).
cnf(69,axiom,
e_38 = select(a_33,i3),
file('SWV558-1.007.p',unknown),
[] ).
cnf(70,plain,
select(a_33,i3) = e_38,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[69])]),
[iquote('copy,69,flip.1')] ).
cnf(72,axiom,
e_40 = select(a_39,i4),
file('SWV558-1.007.p',unknown),
[] ).
cnf(73,plain,
select(a_39,i4) = e_40,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[72])]),
[iquote('copy,72,flip.1')] ).
cnf(75,axiom,
e_42 = select(a_37,i4),
file('SWV558-1.007.p',unknown),
[] ).
cnf(76,plain,
select(a_37,i4) = e_42,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[75])]),
[iquote('copy,75,flip.1')] ).
cnf(78,axiom,
e_44 = select(a_43,i5),
file('SWV558-1.007.p',unknown),
[] ).
cnf(79,plain,
select(a_43,i5) = e_44,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[78])]),
[iquote('copy,78,flip.1')] ).
cnf(81,axiom,
e_46 = select(a_41,i5),
file('SWV558-1.007.p',unknown),
[] ).
cnf(82,plain,
select(a_41,i5) = e_46,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[81])]),
[iquote('copy,81,flip.1')] ).
cnf(84,axiom,
e_48 = select(a_47,i6),
file('SWV558-1.007.p',unknown),
[] ).
cnf(85,plain,
select(a_47,i6) = e_48,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[84])]),
[iquote('copy,84,flip.1')] ).
cnf(87,axiom,
e_50 = select(a_45,i6),
file('SWV558-1.007.p',unknown),
[] ).
cnf(88,plain,
select(a_45,i6) = e_50,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[87])]),
[iquote('copy,87,flip.1')] ).
cnf(90,axiom,
e_52 = select(a_51,i7),
file('SWV558-1.007.p',unknown),
[] ).
cnf(91,plain,
select(a_51,i7) = e_52,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[90])]),
[iquote('copy,90,flip.1')] ).
cnf(93,axiom,
e_54 = select(a_49,i7),
file('SWV558-1.007.p',unknown),
[] ).
cnf(94,plain,
select(a_49,i7) = e_54,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[93])]),
[iquote('copy,93,flip.1')] ).
cnf(96,axiom,
a_53 = a_55,
file('SWV558-1.007.p',unknown),
[] ).
cnf(98,plain,
a_55 = a_53,
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[96])]),
[iquote('copy,96,flip.1')] ).
cnf(99,plain,
store(a_51,i7,e_54) = a_53,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[52]),98]),
[iquote('back_demod,52,demod,98')] ).
cnf(139,plain,
store(a_47,i6,e_48) = a_47,
inference(para_into,[status(thm),theory(equality)],[7,85]),
[iquote('para_into,7.1.1.3,85.1.1')] ).
cnf(141,plain,
store(a_41,i5,e_46) = a_41,
inference(para_into,[status(thm),theory(equality)],[7,82]),
[iquote('para_into,7.1.1.3,82.1.1')] ).
cnf(143,plain,
store(a_43,i5,e_44) = a_43,
inference(para_into,[status(thm),theory(equality)],[7,79]),
[iquote('para_into,7.1.1.3,79.1.1')] ).
cnf(145,plain,
store(a_37,i4,e_42) = a_37,
inference(para_into,[status(thm),theory(equality)],[7,76]),
[iquote('para_into,7.1.1.3,76.1.1')] ).
cnf(147,plain,
store(a_39,i4,e_40) = a_39,
inference(para_into,[status(thm),theory(equality)],[7,73]),
[iquote('para_into,7.1.1.3,73.1.1')] ).
cnf(149,plain,
store(a_33,i3,e_38) = a_33,
inference(para_into,[status(thm),theory(equality)],[7,70]),
[iquote('para_into,7.1.1.3,70.1.1')] ).
cnf(151,plain,
store(a_35,i3,e_36) = a_35,
inference(para_into,[status(thm),theory(equality)],[7,67]),
[iquote('para_into,7.1.1.3,67.1.1')] ).
cnf(153,plain,
store(a_29,i2,e_34) = a_29,
inference(para_into,[status(thm),theory(equality)],[7,64]),
[iquote('para_into,7.1.1.3,64.1.1')] ).
cnf(155,plain,
store(a_31,i2,e_32) = a_31,
inference(para_into,[status(thm),theory(equality)],[7,61]),
[iquote('para_into,7.1.1.3,61.1.1')] ).
cnf(157,plain,
store(a1,i1,e_30) = a1,
inference(para_into,[status(thm),theory(equality)],[7,58]),
[iquote('para_into,7.1.1.3,58.1.1')] ).
cnf(159,plain,
store(a2,i1,e_28) = a2,
inference(para_into,[status(thm),theory(equality)],[7,55]),
[iquote('para_into,7.1.1.3,55.1.1')] ).
cnf(165,plain,
store(a_45,i6,e_50) = a_45,
inference(para_from,[status(thm),theory(equality)],[88,7]),
[iquote('para_from,88.1.1,7.1.1.3')] ).
cnf(169,plain,
store(a_51,i7,e_52) = a_51,
inference(para_from,[status(thm),theory(equality)],[91,7]),
[iquote('para_from,91.1.1,7.1.1.3')] ).
cnf(173,plain,
store(a_49,i7,e_54) = a_49,
inference(para_from,[status(thm),theory(equality)],[94,7]),
[iquote('para_from,94.1.1,7.1.1.3')] ).
cnf(180,plain,
select(a_29,i1) = e_28,
inference(para_from,[status(thm),theory(equality)],[14,4]),
[iquote('para_from,13.1.1,4.1.1.1')] ).
cnf(182,plain,
store(a_29,i1,A) = store(a1,i1,A),
inference(para_into,[status(thm),theory(equality)],[9,14]),
[iquote('para_into,9.1.1.1,13.1.1')] ).
cnf(191,plain,
store(a_31,i1,A) = store(a2,i1,A),
inference(para_from,[status(thm),theory(equality)],[16,9]),
[iquote('para_from,16.1.1,9.1.1.1')] ).
cnf(193,plain,
select(a_31,i1) = e_30,
inference(para_from,[status(thm),theory(equality)],[16,4]),
[iquote('para_from,16.1.1,4.1.1.1')] ).
cnf(202,plain,
store(a_33,i2,A) = store(a_29,i2,A),
inference(para_from,[status(thm),theory(equality)],[20,9]),
[iquote('para_from,19.1.1,9.1.1.1')] ).
cnf(204,plain,
select(a_33,i2) = e_32,
inference(para_from,[status(thm),theory(equality)],[20,4]),
[iquote('para_from,19.1.1,4.1.1.1')] ).
cnf(300,plain,
store(a_35,i2,A) = store(a_31,i2,A),
inference(para_from,[status(thm),theory(equality)],[22,9]),
[iquote('para_from,22.1.1,9.1.1.1')] ).
cnf(302,plain,
select(a_35,i2) = e_34,
inference(para_from,[status(thm),theory(equality)],[22,4]),
[iquote('para_from,22.1.1,4.1.1.1')] ).
cnf(317,plain,
store(a_37,i3,A) = store(a_33,i3,A),
inference(para_from,[status(thm),theory(equality)],[26,9]),
[iquote('para_from,25.1.1,9.1.1.1')] ).
cnf(319,plain,
select(a_37,i3) = e_36,
inference(para_from,[status(thm),theory(equality)],[26,4]),
[iquote('para_from,25.1.1,4.1.1.1')] ).
cnf(328,plain,
store(a_39,i3,A) = store(a_35,i3,A),
inference(para_from,[status(thm),theory(equality)],[28,9]),
[iquote('para_from,28.1.1,9.1.1.1')] ).
cnf(330,plain,
select(a_39,i3) = e_38,
inference(para_from,[status(thm),theory(equality)],[28,4]),
[iquote('para_from,28.1.1,4.1.1.1')] ).
cnf(349,plain,
store(a_41,i4,A) = store(a_37,i4,A),
inference(para_from,[status(thm),theory(equality)],[32,9]),
[iquote('para_from,31.1.1,9.1.1.1')] ).
cnf(351,plain,
select(a_41,i4) = e_40,
inference(para_from,[status(thm),theory(equality)],[32,4]),
[iquote('para_from,31.1.1,4.1.1.1')] ).
cnf(364,plain,
store(a_43,i4,A) = store(a_39,i4,A),
inference(para_from,[status(thm),theory(equality)],[34,9]),
[iquote('para_from,34.1.1,9.1.1.1')] ).
cnf(366,plain,
select(a_43,i4) = e_42,
inference(para_from,[status(thm),theory(equality)],[34,4]),
[iquote('para_from,34.1.1,4.1.1.1')] ).
cnf(381,plain,
store(a_45,i5,A) = store(a_41,i5,A),
inference(para_from,[status(thm),theory(equality)],[38,9]),
[iquote('para_from,37.1.1,9.1.1.1')] ).
cnf(383,plain,
select(a_45,i5) = e_44,
inference(para_from,[status(thm),theory(equality)],[38,4]),
[iquote('para_from,37.1.1,4.1.1.1')] ).
cnf(396,plain,
store(a_47,i5,A) = store(a_43,i5,A),
inference(para_from,[status(thm),theory(equality)],[40,9]),
[iquote('para_from,40.1.1,9.1.1.1')] ).
cnf(398,plain,
select(a_47,i5) = e_46,
inference(para_from,[status(thm),theory(equality)],[40,4]),
[iquote('para_from,40.1.1,4.1.1.1')] ).
cnf(409,plain,
store(a_49,i6,A) = store(a_45,i6,A),
inference(para_from,[status(thm),theory(equality)],[44,9]),
[iquote('para_from,43.1.1,9.1.1.1')] ).
cnf(411,plain,
select(a_49,i6) = e_48,
inference(para_from,[status(thm),theory(equality)],[44,4]),
[iquote('para_from,43.1.1,4.1.1.1')] ).
cnf(428,plain,
store(a_51,i6,A) = store(a_47,i6,A),
inference(para_from,[status(thm),theory(equality)],[46,9]),
[iquote('para_from,46.1.1,9.1.1.1')] ).
cnf(430,plain,
select(a_51,i6) = e_50,
inference(para_from,[status(thm),theory(equality)],[46,4]),
[iquote('para_from,46.1.1,4.1.1.1')] ).
cnf(445,plain,
store(a_53,i7,A) = store(a_49,i7,A),
inference(para_from,[status(thm),theory(equality)],[50,9]),
[iquote('para_from,49.1.1,9.1.1.1')] ).
cnf(447,plain,
select(a_53,i7) = e_52,
inference(para_from,[status(thm),theory(equality)],[50,4]),
[iquote('para_from,49.1.1,4.1.1.1')] ).
cnf(461,plain,
store(a_51,i7,A) = store(a_49,i7,A),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[99,9]),445])]),
[iquote('para_from,99.1.1,9.1.1.1,demod,445,flip.1')] ).
cnf(463,plain,
e_54 = e_52,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[99,4]),447])]),
[iquote('para_from,99.1.1,4.1.1.1,demod,447,flip.1')] ).
cnf(465,plain,
a_53 = a_51,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[169]),461,50]),
[iquote('back_demod,169,demod,461,50')] ).
cnf(474,plain,
a_51 = a_49,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[173]),463,50,465]),
[iquote('back_demod,173,demod,463,50,465')] ).
cnf(497,plain,
e_50 = e_48,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[430]),474,411])]),
[iquote('back_demod,430,demod,474,411,flip.1')] ).
cnf(499,plain,
store(a_47,i6,A) = store(a_45,i6,A),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[428]),474,409])]),
[iquote('back_demod,428,demod,474,409,flip.1')] ).
cnf(509,plain,
a_49 = a_45,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[165]),497,44]),
[iquote('back_demod,165,demod,497,44')] ).
cnf(515,plain,
a_47 = a_45,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[139]),499,44,509])]),
[iquote('back_demod,139,demod,499,44,509,flip.1')] ).
cnf(551,plain,
e_46 = e_44,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[398]),515,383])]),
[iquote('back_demod,398,demod,515,383,flip.1')] ).
cnf(553,plain,
store(a_43,i5,A) = store(a_41,i5,A),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[396]),515,381])]),
[iquote('back_demod,396,demod,515,381,flip.1')] ).
cnf(563,plain,
a_45 = a_41,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[141]),551,38]),
[iquote('back_demod,141,demod,551,38')] ).
cnf(569,plain,
a_43 = a_41,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[143]),553,38,563])]),
[iquote('back_demod,143,demod,553,38,563,flip.1')] ).
cnf(624,plain,
e_42 = e_40,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[366]),569,351])]),
[iquote('back_demod,366,demod,569,351,flip.1')] ).
cnf(626,plain,
store(a_39,i4,A) = store(a_37,i4,A),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[364]),569,349])]),
[iquote('back_demod,364,demod,569,349,flip.1')] ).
cnf(636,plain,
a_41 = a_37,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[145]),624,32]),
[iquote('back_demod,145,demod,624,32')] ).
cnf(642,plain,
a_39 = a_37,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[147]),626,32,636])]),
[iquote('back_demod,147,demod,626,32,636,flip.1')] ).
cnf(716,plain,
e_38 = e_36,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[330]),642,319])]),
[iquote('back_demod,330,demod,642,319,flip.1')] ).
cnf(718,plain,
store(a_35,i3,A) = store(a_33,i3,A),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[328]),642,317])]),
[iquote('back_demod,328,demod,642,317,flip.1')] ).
cnf(728,plain,
a_37 = a_33,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[149]),716,26]),
[iquote('back_demod,149,demod,716,26')] ).
cnf(734,plain,
a_35 = a_33,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[151]),718,26,728])]),
[iquote('back_demod,151,demod,718,26,728,flip.1')] ).
cnf(827,plain,
e_34 = e_32,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[302]),734,204])]),
[iquote('back_demod,302,demod,734,204,flip.1')] ).
cnf(829,plain,
store(a_31,i2,A) = store(a_29,i2,A),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[300]),734,202])]),
[iquote('back_demod,300,demod,734,202,flip.1')] ).
cnf(839,plain,
a_33 = a_29,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[153]),827,20]),
[iquote('back_demod,153,demod,827,20')] ).
cnf(845,plain,
a_31 = a_29,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[155]),829,20,839])]),
[iquote('back_demod,155,demod,829,20,839,flip.1')] ).
cnf(961,plain,
e_30 = e_28,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[193]),845,180])]),
[iquote('back_demod,193,demod,845,180,flip.1')] ).
cnf(963,plain,
store(a2,i1,A) = store(a1,i1,A),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[191]),845,182])]),
[iquote('back_demod,191,demod,845,182,flip.1')] ).
cnf(973,plain,
a_29 = a1,
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[157]),961,14]),
[iquote('back_demod,157,demod,961,14')] ).
cnf(978,plain,
a2 = a1,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[159]),963,14,973])]),
[iquote('back_demod,159,demod,963,14,973,flip.1')] ).
cnf(980,plain,
$false,
inference(binary,[status(thm)],[978,2]),
[iquote('binary,978.1,2.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV558-1.007 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : otter-tptp-script %s
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jul 27 05:56:26 EDT 2022
% 0.12/0.34 % CPUTime :
% 1.96/2.13 ----- Otter 3.3f, August 2004 -----
% 1.96/2.13 The process was started by sandbox on n015.cluster.edu,
% 1.96/2.13 Wed Jul 27 05:56:26 2022
% 1.96/2.13 The command was "./otter". The process ID is 1216.
% 1.96/2.13
% 1.96/2.13 set(prolog_style_variables).
% 1.96/2.13 set(auto).
% 1.96/2.13 dependent: set(auto1).
% 1.96/2.13 dependent: set(process_input).
% 1.96/2.13 dependent: clear(print_kept).
% 1.96/2.13 dependent: clear(print_new_demod).
% 1.96/2.13 dependent: clear(print_back_demod).
% 1.96/2.13 dependent: clear(print_back_sub).
% 1.96/2.13 dependent: set(control_memory).
% 1.96/2.13 dependent: assign(max_mem, 12000).
% 1.96/2.13 dependent: assign(pick_given_ratio, 4).
% 1.96/2.13 dependent: assign(stats_level, 1).
% 1.96/2.13 dependent: assign(max_seconds, 10800).
% 1.96/2.13 clear(print_given).
% 1.96/2.13
% 1.96/2.13 list(usable).
% 1.96/2.13 0 [] A=A.
% 1.96/2.13 0 [] select(store(A,I,E),I)=E.
% 1.96/2.13 0 [] I=J|select(store(A,I,E),J)=select(A,J).
% 1.96/2.13 0 [] store(A,I,select(A,I))=A.
% 1.96/2.13 0 [] store(store(A,I,E),I,F)=store(A,I,F).
% 1.96/2.13 0 [] I=J|store(store(A,I,E),J,F)=store(store(A,J,F),I,E).
% 1.96/2.13 0 [] a_29=store(a1,i1,e_28).
% 1.96/2.13 0 [] a_31=store(a2,i1,e_30).
% 1.96/2.13 0 [] a_33=store(a_29,i2,e_32).
% 1.96/2.13 0 [] a_35=store(a_31,i2,e_34).
% 1.96/2.13 0 [] a_37=store(a_33,i3,e_36).
% 1.96/2.13 0 [] a_39=store(a_35,i3,e_38).
% 1.96/2.13 0 [] a_41=store(a_37,i4,e_40).
% 1.96/2.13 0 [] a_43=store(a_39,i4,e_42).
% 1.96/2.13 0 [] a_45=store(a_41,i5,e_44).
% 1.96/2.13 0 [] a_47=store(a_43,i5,e_46).
% 1.96/2.13 0 [] a_49=store(a_45,i6,e_48).
% 1.96/2.13 0 [] a_51=store(a_47,i6,e_50).
% 1.96/2.13 0 [] a_53=store(a_49,i7,e_52).
% 1.96/2.13 0 [] a_55=store(a_51,i7,e_54).
% 1.96/2.13 0 [] e_28=select(a2,i1).
% 1.96/2.13 0 [] e_30=select(a1,i1).
% 1.96/2.13 0 [] e_32=select(a_31,i2).
% 1.96/2.13 0 [] e_34=select(a_29,i2).
% 1.96/2.13 0 [] e_36=select(a_35,i3).
% 1.96/2.13 0 [] e_38=select(a_33,i3).
% 1.96/2.13 0 [] e_40=select(a_39,i4).
% 1.96/2.13 0 [] e_42=select(a_37,i4).
% 1.96/2.13 0 [] e_44=select(a_43,i5).
% 1.96/2.13 0 [] e_46=select(a_41,i5).
% 1.96/2.13 0 [] e_48=select(a_47,i6).
% 1.96/2.13 0 [] e_50=select(a_45,i6).
% 1.96/2.13 0 [] e_52=select(a_51,i7).
% 1.96/2.13 0 [] e_54=select(a_49,i7).
% 1.96/2.13 0 [] a_53=a_55.
% 1.96/2.13 0 [] a1!=a2.
% 1.96/2.13 end_of_list.
% 1.96/2.13
% 1.96/2.13 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2.
% 1.96/2.13
% 1.96/2.13 This ia a non-Horn set with equality. The strategy will be
% 1.96/2.13 Knuth-Bendix, ordered hyper_res, factoring, and unit
% 1.96/2.13 deletion, with positive clauses in sos and nonpositive
% 1.96/2.13 clauses in usable.
% 1.96/2.13
% 1.96/2.13 dependent: set(knuth_bendix).
% 1.96/2.13 dependent: set(anl_eq).
% 1.96/2.13 dependent: set(para_from).
% 1.96/2.13 dependent: set(para_into).
% 1.96/2.13 dependent: clear(para_from_right).
% 1.96/2.13 dependent: clear(para_into_right).
% 1.96/2.13 dependent: set(para_from_vars).
% 1.96/2.13 dependent: set(eq_units_both_ways).
% 1.96/2.13 dependent: set(dynamic_demod_all).
% 1.96/2.13 dependent: set(dynamic_demod).
% 1.96/2.13 dependent: set(order_eq).
% 1.96/2.13 dependent: set(back_demod).
% 1.96/2.13 dependent: set(lrpo).
% 1.96/2.13 dependent: set(hyper_res).
% 1.96/2.13 dependent: set(unit_deletion).
% 1.96/2.13 dependent: set(factor).
% 1.96/2.13
% 1.96/2.13 ------------> process usable:
% 1.96/2.13 ** KEPT (pick-wt=3): 2 [copy,1,flip.1] a2!=a1.
% 1.96/2.13
% 1.96/2.13 ------------> process sos:
% 1.96/2.13 ** KEPT (pick-wt=3): 3 [] A=A.
% 1.96/2.13 ** KEPT (pick-wt=8): 4 [] select(store(A,B,C),B)=C.
% 1.96/2.13 ---> New Demodulator: 5 [new_demod,4] select(store(A,B,C),B)=C.
% 1.96/2.13 ** KEPT (pick-wt=13): 6 [] A=B|select(store(C,A,D),B)=select(C,B).
% 1.96/2.13 ** KEPT (pick-wt=8): 7 [] store(A,B,select(A,B))=A.
% 1.96/2.13 ---> New Demodulator: 8 [new_demod,7] store(A,B,select(A,B))=A.
% 1.96/2.13 ** KEPT (pick-wt=12): 9 [] store(store(A,B,C),B,D)=store(A,B,D).
% 1.96/2.13 ---> New Demodulator: 10 [new_demod,9] store(store(A,B,C),B,D)=store(A,B,D).
% 1.96/2.13 ** KEPT (pick-wt=18): 11 [] A=B|store(store(C,A,D),B,E)=store(store(C,B,E),A,D).
% 1.96/2.13 ** KEPT (pick-wt=6): 13 [copy,12,flip.1] store(a1,i1,e_28)=a_29.
% 1.96/2.13 ---> New Demodulator: 14 [new_demod,13] store(a1,i1,e_28)=a_29.
% 1.96/2.13 ** KEPT (pick-wt=6): 16 [copy,15,flip.1] store(a2,i1,e_30)=a_31.
% 1.96/2.13 ---> New Demodulator: 17 [new_demod,16] store(a2,i1,e_30)=a_31.
% 1.96/2.13 ** KEPT (pick-wt=6): 19 [copy,18,flip.1] store(a_29,i2,e_32)=a_33.
% 1.96/2.13 ---> New Demodulator: 20 [new_demod,19] store(a_29,i2,e_32)=a_33.
% 1.96/2.13 ** KEPT (pick-wt=6): 22 [copy,21,flip.1] store(a_31,i2,e_34)=a_35.
% 1.96/2.13 ---> New Demodulator: 23 [new_demod,22] store(a_31,i2,e_34)=a_35.
% 1.96/2.13 ** KEPT (pick-wt=6): 25 [copy,24,flip.1] store(a_33,i3,e_36)=a_37.
% 1.96/2.13 ---> New Demodulator: 26 [new_demod,25] store(a_33,i3,e_36)=a_37.
% 1.96/2.13 ** KEPT (pick-wt=6): 28 [copy,27,flip.1] store(a_35,i3,e_38)=a_39.
% 1.96/2.13 ---> New Demodulator: 29 [new_demod,28] store(a_35,i3,e_38)=a_39.
% 1.96/2.13 ** KEPT (pick-wt=6): 31 [copy,30,flip.1] store(a_37,i4,e_40)=a_41.
% 1.96/2.13 ---> New Demodulator: 32 [new_demod,31] store(a_37,i4,e_40)=a_41.
% 1.96/2.13 ** KEPT (pick-wt=6): 34 [copy,33,flip.1] store(a_39,i4,e_42)=a_43.
% 1.96/2.13 ---> New Demodulator: 35 [new_demod,34] store(a_39,i4,e_42)=a_43.
% 1.96/2.13 ** KEPT (pick-wt=6): 37 [copy,36,flip.1] store(a_41,i5,e_44)=a_45.
% 1.96/2.13 ---> New Demodulator: 38 [new_demod,37] store(a_41,i5,e_44)=a_45.
% 1.96/2.13 ** KEPT (pick-wt=6): 40 [copy,39,flip.1] store(a_43,i5,e_46)=a_47.
% 1.96/2.13 ---> New Demodulator: 41 [new_demod,40] store(a_43,i5,e_46)=a_47.
% 1.96/2.13 ** KEPT (pick-wt=6): 43 [copy,42,flip.1] store(a_45,i6,e_48)=a_49.
% 1.96/2.13 ---> New Demodulator: 44 [new_demod,43] store(a_45,i6,e_48)=a_49.
% 1.96/2.13 ** KEPT (pick-wt=6): 46 [copy,45,flip.1] store(a_47,i6,e_50)=a_51.
% 1.96/2.13 ---> New Demodulator: 47 [new_demod,46] store(a_47,i6,e_50)=a_51.
% 1.96/2.13 ** KEPT (pick-wt=6): 49 [copy,48,flip.1] store(a_49,i7,e_52)=a_53.
% 1.96/2.13 ---> New Demodulator: 50 [new_demod,49] store(a_49,i7,e_52)=a_53.
% 1.96/2.13 ** KEPT (pick-wt=6): 52 [copy,51,flip.1] store(a_51,i7,e_54)=a_55.
% 1.96/2.13 ---> New Demodulator: 53 [new_demod,52] store(a_51,i7,e_54)=a_55.
% 1.96/2.13 ** KEPT (pick-wt=5): 55 [copy,54,flip.1] select(a2,i1)=e_28.
% 1.96/2.13 ---> New Demodulator: 56 [new_demod,55] select(a2,i1)=e_28.
% 1.96/2.13 ** KEPT (pick-wt=5): 58 [copy,57,flip.1] select(a1,i1)=e_30.
% 1.96/2.13 ---> New Demodulator: 59 [new_demod,58] select(a1,i1)=e_30.
% 1.96/2.13 ** KEPT (pick-wt=5): 61 [copy,60,flip.1] select(a_31,i2)=e_32.
% 1.96/2.13 ---> New Demodulator: 62 [new_demod,61] select(a_31,i2)=e_32.
% 1.96/2.13 ** KEPT (pick-wt=5): 64 [copy,63,flip.1] select(a_29,i2)=e_34.
% 1.96/2.13 ---> New Demodulator: 65 [new_demod,64] select(a_29,i2)=e_34.
% 1.96/2.13 ** KEPT (pick-wt=5): 67 [copy,66,flip.1] select(a_35,i3)=e_36.
% 1.96/2.13 ---> New Demodulator: 68 [new_demod,67] select(a_35,i3)=e_36.
% 1.96/2.13 ** KEPT (pick-wt=5): 70 [copy,69,flip.1] select(a_33,i3)=e_38.
% 1.96/2.13 ---> New Demodulator: 71 [new_demod,70] select(a_33,i3)=e_38.
% 1.96/2.13 ** KEPT (pick-wt=5): 73 [copy,72,flip.1] select(a_39,i4)=e_40.
% 1.96/2.13 ---> New Demodulator: 74 [new_demod,73] select(a_39,i4)=e_40.
% 1.96/2.13 ** KEPT (pick-wt=5): 76 [copy,75,flip.1] select(a_37,i4)=e_42.
% 1.96/2.13 ---> New Demodulator: 77 [new_demod,76] select(a_37,i4)=e_42.
% 1.96/2.13 ** KEPT (pick-wt=5): 79 [copy,78,flip.1] select(a_43,i5)=e_44.
% 1.96/2.13 ---> New Demodulator: 80 [new_demod,79] select(a_43,i5)=e_44.
% 1.96/2.13 ** KEPT (pick-wt=5): 82 [copy,81,flip.1] select(a_41,i5)=e_46.
% 1.96/2.13 ---> New Demodulator: 83 [new_demod,82] select(a_41,i5)=e_46.
% 1.96/2.13 ** KEPT (pick-wt=5): 85 [copy,84,flip.1] select(a_47,i6)=e_48.
% 1.96/2.13 ---> New Demodulator: 86 [new_demod,85] select(a_47,i6)=e_48.
% 1.96/2.13 ** KEPT (pick-wt=5): 88 [copy,87,flip.1] select(a_45,i6)=e_50.
% 1.96/2.13 ---> New Demodulator: 89 [new_demod,88] select(a_45,i6)=e_50.
% 1.96/2.13 ** KEPT (pick-wt=5): 91 [copy,90,flip.1] select(a_51,i7)=e_52.
% 1.96/2.13 ---> New Demodulator: 92 [new_demod,91] select(a_51,i7)=e_52.
% 1.96/2.13 ** KEPT (pick-wt=5): 94 [copy,93,flip.1] select(a_49,i7)=e_54.
% 1.96/2.13 ---> New Demodulator: 95 [new_demod,94] select(a_49,i7)=e_54.
% 1.96/2.13 ** KEPT (pick-wt=3): 97 [copy,96,flip.1] a_55=a_53.
% 1.96/2.13 ---> New Demodulator: 98 [new_demod,97] a_55=a_53.
% 1.96/2.13 Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] A=A.
% 1.96/2.13 >>>> Starting back demodulation with 5.
% 1.96/2.13 >>>> Starting back demodulation with 8.
% 1.96/2.13 >>>> Starting back demodulation with 10.
% 1.96/2.13 >>>> Starting back demodulation with 14.
% 1.96/2.13 >>>> Starting back demodulation with 17.
% 1.96/2.13 >>>> Starting back demodulation with 20.
% 1.96/2.13 >>>> Starting back demodulation with 23.
% 1.96/2.13 >>>> Starting back demodulation with 26.
% 1.96/2.13 >>>> Starting back demodulation with 29.
% 1.96/2.13 >>>> Starting back demodulation with 32.
% 1.96/2.13 >>>> Starting back demodulation with 35.
% 1.96/2.13 >>>> Starting back demodulation with 38.
% 1.96/2.13 >>>> Starting back demodulation with 41.
% 1.96/2.13 >>>> Starting back demodulation with 44.
% 1.96/2.13 >>>> Starting back demodulation with 47.
% 1.96/2.13 >>>> Starting back demodulation with 50.
% 1.96/2.13 >>>> Starting back demodulation with 53.
% 1.96/2.13 >>>> Starting back demodulation with 56.
% 1.96/2.13 >>>> Starting back demodulation with 59.
% 1.96/2.13 >>>> Starting back demodulation with 62.
% 1.96/2.13 >>>> Starting back demodulation with 65.
% 1.96/2.13 >>>> Starting back demodulation with 68.
% 1.96/2.13 >>>> Starting back demodulation with 71.
% 1.96/2.13 >>>> Starting back demodulation with 74.
% 1.96/2.13 >>>> Starting back demodulation with 77.
% 1.96/2.13 >>>> Starting back demodulation with 80.
% 1.96/2.13 >>>> Starting back demodulation with 83.
% 1.96/2.13 >>>> Starting back demodulation with 86.
% 1.96/2.13 >>>> Starting back demodulation with 89.
% 1.96/2.13 >>>> Starting back demodulation with 92.
% 1.96/2.13 >>>> Starting back demodulation with 95.
% 1.96/2.16 >>>> Starting back demodulation with 98.
% 1.96/2.16 >> back demodulating 52 with 98.
% 1.96/2.16 >>>> Starting back demodulation with 100.
% 1.96/2.16
% 1.96/2.16 ======= end of input processing =======
% 1.96/2.16
% 1.96/2.16 =========== start of search ===========
% 1.96/2.16
% 1.96/2.16 -------- PROOF --------
% 1.96/2.16
% 1.96/2.16 ----> UNIT CONFLICT at 0.03 sec ----> 980 [binary,978.1,2.1] $F.
% 1.96/2.16
% 1.96/2.16 Length of proof is 99. Level of proof is 23.
% 1.96/2.16
% 1.96/2.16 ---------------- PROOF ----------------
% 1.96/2.16 % SZS status Unsatisfiable
% 1.96/2.16 % SZS output start Refutation
% See solution above
% 1.96/2.16 ------------ end of proof -------------
% 1.96/2.16
% 1.96/2.16
% 1.96/2.16 Search stopped by max_proofs option.
% 1.96/2.16
% 1.96/2.16
% 1.96/2.16 Search stopped by max_proofs option.
% 1.96/2.16
% 1.96/2.16 ============ end of search ============
% 1.96/2.16
% 1.96/2.16 -------------- statistics -------------
% 1.96/2.16 clauses given 48
% 1.96/2.16 clauses generated 508
% 1.96/2.16 clauses kept 767
% 1.96/2.16 clauses forward subsumed 350
% 1.96/2.16 clauses back subsumed 27
% 1.96/2.16 Kbytes malloced 2929
% 1.96/2.16
% 1.96/2.16 ----------- times (seconds) -----------
% 1.96/2.16 user CPU time 0.03 (0 hr, 0 min, 0 sec)
% 1.96/2.16 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.96/2.16 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 1.96/2.16
% 1.96/2.16 That finishes the proof of the theorem.
% 1.96/2.16
% 1.96/2.16 Process 1216 finished Wed Jul 27 05:56:28 2022
% 1.96/2.16 Otter interrupted
% 1.96/2.16 PROOF FOUND
%------------------------------------------------------------------------------