%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ALG117+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n026.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 17:59:56 EDT 2022
% Result : Theorem 1.99s 2.22s
% Output : Refutation 1.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 106
% Syntax : Number of clauses : 285 ( 199 unt; 76 nHn; 285 RR)
% Number of literals : 534 ( 533 equ; 247 neg)
% Maximal clause size : 20 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(3,axiom,
( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(4,axiom,
( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(5,axiom,
( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(7,axiom,
( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(8,axiom,
( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(13,axiom,
( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(14,axiom,
( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(18,axiom,
( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(30,axiom,
( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12
| op1(e13,e11) = e12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(50,axiom,
( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(51,axiom,
( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(52,axiom,
( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(53,axiom,
( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(55,axiom,
( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(56,axiom,
( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(58,axiom,
( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(61,axiom,
( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(62,axiom,
( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(66,axiom,
( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(99,axiom,
op1(e10,e10) != op1(e13,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(101,axiom,
op1(e11,e10) != op1(e13,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(103,axiom,
op1(e10,e11) != op1(e11,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(105,axiom,
op1(e10,e11) != op1(e13,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(107,axiom,
op1(e11,e11) != op1(e13,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(109,axiom,
op1(e10,e12) != op1(e11,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(110,axiom,
op1(e10,e12) != op1(e12,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(111,axiom,
op1(e10,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(112,axiom,
op1(e11,e12) != op1(e12,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(113,axiom,
op1(e11,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(114,axiom,
op1(e12,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(115,axiom,
op1(e10,e13) != op1(e11,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(116,axiom,
op1(e10,e13) != op1(e12,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(117,axiom,
op1(e10,e13) != op1(e13,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(118,axiom,
op1(e11,e13) != op1(e12,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(119,axiom,
op1(e11,e13) != op1(e13,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(123,axiom,
op1(e10,e10) != op1(e10,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(124,axiom,
op1(e10,e11) != op1(e10,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(127,axiom,
op1(e11,e10) != op1(e11,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(128,axiom,
op1(e11,e10) != op1(e11,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(131,axiom,
op1(e11,e11) != op1(e11,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(139,axiom,
op1(e13,e10) != op1(e13,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(140,axiom,
op1(e13,e10) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(141,axiom,
op1(e13,e10) != op1(e13,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(143,axiom,
op1(e13,e11) != op1(e13,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(147,axiom,
op2(e20,e20) != op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(149,axiom,
op2(e21,e20) != op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(151,axiom,
op2(e20,e21) != op2(e21,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(152,axiom,
op2(e20,e21) != op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(153,axiom,
op2(e20,e21) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(154,axiom,
op2(e21,e21) != op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(156,axiom,
op2(e22,e21) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(157,axiom,
op2(e20,e22) != op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(158,axiom,
op2(e20,e22) != op2(e22,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(159,axiom,
op2(e20,e22) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(160,axiom,
op2(e21,e22) != op2(e22,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(161,axiom,
op2(e21,e22) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(162,axiom,
op2(e22,e22) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(163,axiom,
op2(e20,e23) != op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(164,axiom,
op2(e20,e23) != op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(165,axiom,
op2(e20,e23) != op2(e23,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(166,axiom,
op2(e21,e23) != op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(167,axiom,
op2(e21,e23) != op2(e23,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(171,axiom,
op2(e20,e20) != op2(e20,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(175,axiom,
op2(e21,e20) != op2(e21,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(176,axiom,
op2(e21,e20) != op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(179,axiom,
op2(e21,e21) != op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(184,axiom,
op2(e22,e21) != op2(e22,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(187,axiom,
op2(e23,e20) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(188,axiom,
op2(e23,e20) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(189,axiom,
op2(e23,e20) != op2(e23,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(190,axiom,
op2(e23,e21) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(191,axiom,
op2(e23,e21) != op2(e23,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(194,axiom,
e10 != e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(195,axiom,
e10 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(196,axiom,
e11 != e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(197,axiom,
e11 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(200,axiom,
e20 != e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(201,axiom,
e20 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(202,axiom,
e21 != e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(203,axiom,
e21 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(221,axiom,
( op1(e11,e11) = e10
| op1(e12,e12) = e10
| op1(e13,e13) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(225,axiom,
( op1(e11,e10) != e11
| op1(e12,e12) = e10
| op1(e13,e13) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(229,axiom,
( op1(e10,e10) = e11
| op1(e12,e12) = e11
| op1(e13,e13) = e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(249,axiom,
( op1(e10,e13) != e10
| op1(e11,e11) = e13
| op1(e12,e12) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(253,axiom,
( op2(e21,e21) = e20
| op2(e22,e22) = e20
| op2(e23,e23) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(257,axiom,
( op2(e21,e20) != e21
| op2(e22,e22) = e20
| op2(e23,e23) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(261,axiom,
( op2(e20,e20) = e21
| op2(e22,e22) = e21
| op2(e23,e23) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(281,axiom,
( op2(e20,e23) != e20
| op2(e21,e21) = e23
| op2(e22,e22) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(285,axiom,
e10 = op1(e13,op1(e13,e13)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(286,axiom,
e11 = op1(op1(e13,e13),e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(287,axiom,
op1(e13,e13) = e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(288,axiom,
e20 = op2(e23,op2(e23,e23)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(289,axiom,
e21 = op2(op2(e23,e23),e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(290,axiom,
op2(e23,e23) = e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(291,axiom,
h1(e13) = e20,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(292,axiom,
h1(e10) = op2(e20,op2(e20,e20)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(293,axiom,
h1(e11) = op2(op2(e20,e20),e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(294,axiom,
h1(e12) = op2(e20,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(296,axiom,
h2(e10) = op2(e21,op2(e21,e21)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
cnf(297,axiom,
h2(e11) = op2(op2(e21,e21),e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
cnf(298,axiom,
h2(e12) = op2(e21,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
cnf(302,axiom,
h3(e12) = op2(e22,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
cnf(304,axiom,
h4(e10) = op2(e23,op2(e23,e23)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
cnf(305,plain,
h4(e10) = op2(e23,e22),
inference('REWRITE',[status(thm)],[304,290,theory(equality)]) ).
cnf(306,axiom,
h4(e11) = op2(op2(e23,e23),e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
cnf(307,plain,
h4(e11) = op2(e22,e23),
inference('REWRITE',[status(thm)],[306,290,theory(equality)]) ).
cnf(514,negated_conjecture,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(e13) != e20
| h1(e12) != e21
| h1(e11) != e22
| h1(e10) != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
cnf(515,plain,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),e20)
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),e20)
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),e20)
| h1(op1(e13,e10)) != op2(e20,h1(e10))
| h1(op1(e13,e11)) != op2(e20,h1(e11))
| h1(op1(e13,e12)) != op2(e20,h1(e12))
| h1(e12) != e21
| h1(e11) != e22
| h1(e10) != e23 ),
inference('REWRITE',[status(thm)],[514,294,287,291,theory(equality)]) ).
cnf(1031,plain,
op2(e20,e23) != h4(e11),
inference('REWRITE',[status(thm)],[164,307,theory(equality)]) ).
cnf(1032,plain,
op2(e21,e23) != h4(e11),
inference('REWRITE',[status(thm)],[166,307,theory(equality)]) ).
cnf(1037,plain,
op2(e20,e22) != h4(e10),
inference('REWRITE',[status(thm)],[159,305,theory(equality)]) ).
cnf(1038,plain,
op2(e21,e22) != h4(e10),
inference('REWRITE',[status(thm)],[161,305,theory(equality)]) ).
cnf(1039,plain,
op2(e23,e20) != h4(e10),
inference('REWRITE',[status(thm)],[188,305,theory(equality)]) ).
cnf(1040,plain,
op2(e23,e21) != h4(e10),
inference('REWRITE',[status(thm)],[190,305,theory(equality)]) ).
cnf(1051,plain,
op2(e20,e22) != h3(e12),
inference('REWRITE',[status(thm)],[158,302,theory(equality)]) ).
cnf(1052,plain,
op2(e21,e22) != h3(e12),
inference('REWRITE',[status(thm)],[160,302,theory(equality)]) ).
cnf(1053,plain,
h3(e12) != h4(e10),
inference('REWRITE',[status(thm)],[162,305,302,theory(equality)]) ).
cnf(1055,plain,
op2(e22,e21) != h3(e12),
inference('REWRITE',[status(thm)],[184,302,theory(equality)]) ).
cnf(1125,plain,
op2(e20,e21) != h2(e12),
inference('REWRITE',[status(thm)],[151,298,theory(equality)]) ).
cnf(1126,plain,
h2(e12) != op2(e22,e21),
inference('REWRITE',[status(thm)],[154,298,theory(equality)]) ).
cnf(1128,plain,
op2(e21,e20) != h2(e12),
inference('REWRITE',[status(thm)],[175,298,theory(equality)]) ).
cnf(1130,plain,
h2(e12) != op2(e21,e23),
inference('REWRITE',[status(thm)],[179,298,theory(equality)]) ).
cnf(1134,plain,
( op2(e20,e23) != e20
| h2(e12) = e23
| h3(e12) = e23 ),
inference('REWRITE',[status(thm)],[281,302,298,theory(equality)]) ).
cnf(1136,plain,
h2(e10) = op2(e21,h2(e12)),
inference('REWRITE',[status(thm)],[296,298,theory(equality)]) ).
cnf(1164,plain,
h2(e11) = op2(h2(e12),e21),
inference('REWRITE',[status(thm)],[297,298,theory(equality)]) ).
cnf(1194,plain,
( h1(e12) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 ),
inference('REWRITE',[status(thm)],[66,294,theory(equality)]) ).
cnf(1203,plain,
h1(e12) != op2(e23,e20),
inference('REWRITE',[status(thm)],[147,294,theory(equality)]) ).
cnf(1206,plain,
h1(e12) != op2(e20,e23),
inference('REWRITE',[status(thm)],[171,294,theory(equality)]) ).
cnf(1215,plain,
h1(e10) = op2(e20,h1(e12)),
inference('REWRITE',[status(thm)],[292,294,theory(equality)]) ).
cnf(1237,plain,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),e20)
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),e20)
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),e20)
| h1(op1(e13,e10)) != op2(e20,h1(e10))
| h1(op1(e13,e11)) != op2(e20,h1(e11))
| h1(op1(e13,e12)) != h1(e10)
| h1(e12) != e21
| h1(e11) != e22
| h1(e10) != e23 ),
inference('REWRITE',[status(thm)],[515,1215,theory(equality)]) ).
cnf(1243,plain,
h1(e11) = op2(h1(e12),e20),
inference('REWRITE',[status(thm)],[293,294,theory(equality)]) ).
cnf(1265,plain,
( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),e20)
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),e20)
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != h1(e11)
| h1(op1(e13,e10)) != op2(e20,h1(e10))
| h1(op1(e13,e11)) != op2(e20,h1(e11))
| h1(op1(e13,e12)) != h1(e10)
| h1(e12) != e21
| h1(e11) != e22
| h1(e10) != e23 ),
inference('REWRITE',[status(thm)],[1237,1243,theory(equality)]) ).
cnf(1277,plain,
op2(e20,e23) != e22,
inference('REWRITE',[status(thm)],[165,290,theory(equality)]) ).
cnf(1278,plain,
( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e23 ),
inference('REWRITE',[status(thm)],[52,1277]) ).
cnf(1280,plain,
op2(e21,e23) != e22,
inference('REWRITE',[status(thm)],[167,290,theory(equality)]) ).
cnf(1281,plain,
( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e23 ),
inference('REWRITE',[status(thm)],[56,1280]) ).
cnf(1286,plain,
op2(e23,e20) != e22,
inference('REWRITE',[status(thm)],[189,290,theory(equality)]) ).
cnf(1287,plain,
( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e23 ),
inference('REWRITE',[status(thm)],[61,1286]) ).
cnf(1289,plain,
op2(e23,e21) != e22,
inference('REWRITE',[status(thm)],[191,290,theory(equality)]) ).
cnf(1290,plain,
( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e23 ),
inference('REWRITE',[status(thm)],[62,1289]) ).
cnf(1295,plain,
( h2(e12) = e20
| h3(e12) = e20 ),
inference('REWRITE',[status(thm)],[253,200,302,298,290,theory(equality)]) ).
cnf(1297,plain,
( op2(e21,e20) != e21
| h3(e12) = e20 ),
inference('REWRITE',[status(thm)],[257,200,302,290,theory(equality)]) ).
cnf(1299,plain,
( h1(e12) = e21
| h3(e12) = e21 ),
inference('REWRITE',[status(thm)],[261,202,302,294,290,theory(equality)]) ).
cnf(1303,plain,
h4(e10) = e20,
inference('REWRITE',[status(thm)],[288,305,290,theory(equality)]) ).
cnf(1304,plain,
op2(e23,e22) = e20,
inference('REWRITE',[status(thm)],[305,1303,theory(equality)]) ).
cnf(1306,plain,
op2(e20,e22) != e20,
inference('REWRITE',[status(thm)],[1037,1303,theory(equality)]) ).
cnf(1307,plain,
( op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 ),
inference('REWRITE',[status(thm)],[51,1306]) ).
cnf(1309,plain,
op2(e21,e22) != e20,
inference('REWRITE',[status(thm)],[1038,1303,theory(equality)]) ).
cnf(1310,plain,
( op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 ),
inference('REWRITE',[status(thm)],[55,1309]) ).
cnf(1312,plain,
op2(e23,e20) != e20,
inference('REWRITE',[status(thm)],[1039,1303,theory(equality)]) ).
cnf(1313,plain,
( h1(e12) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20 ),
inference('REWRITE',[status(thm)],[1194,1312]) ).
cnf(1314,plain,
( op2(e23,e20) = e21
| op2(e23,e20) = e23 ),
inference('REWRITE',[status(thm)],[1287,1312]) ).
cnf(1315,plain,
op2(e23,e21) != e20,
inference('REWRITE',[status(thm)],[1040,1303,theory(equality)]) ).
cnf(1317,plain,
( op2(e23,e21) = e21
| op2(e23,e21) = e23 ),
inference('REWRITE',[status(thm)],[1290,1315]) ).
cnf(1320,plain,
h3(e12) != e20,
inference('REWRITE',[status(thm)],[1053,1303,theory(equality)]) ).
cnf(1323,plain,
h2(e12) = e20,
inference('REWRITE',[status(thm)],[1295,1320]) ).
cnf(1324,plain,
op2(e21,e21) = e20,
inference('REWRITE',[status(thm)],[298,1323,theory(equality)]) ).
cnf(1329,plain,
op2(e20,e21) != e20,
inference('REWRITE',[status(thm)],[1125,1323,theory(equality)]) ).
cnf(1330,plain,
( op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 ),
inference('REWRITE',[status(thm)],[50,1329]) ).
cnf(1332,plain,
op2(e22,e21) != e20,
inference('REWRITE',[status(thm)],[1126,1323,theory(equality)]) ).
cnf(1333,plain,
( op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 ),
inference('REWRITE',[status(thm)],[58,1332]) ).
cnf(1335,plain,
op2(e21,e20) != e20,
inference('REWRITE',[status(thm)],[1128,1323,theory(equality)]) ).
cnf(1336,plain,
( op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 ),
inference('REWRITE',[status(thm)],[53,1335]) ).
cnf(1337,plain,
( h1(e12) = e20
| op2(e22,e20) = e20 ),
inference('REWRITE',[status(thm)],[1313,1335]) ).
cnf(1338,plain,
op2(e21,e23) != e20,
inference('REWRITE',[status(thm)],[1130,1323,theory(equality)]) ).
cnf(1340,plain,
( op2(e21,e23) = e21
| op2(e21,e23) = e23 ),
inference('REWRITE',[status(thm)],[1281,1338]) ).
cnf(1341,plain,
( op2(e20,e23) != e20
| h3(e12) = e23 ),
inference('REWRITE',[status(thm)],[1134,201,1323,theory(equality)]) ).
cnf(1342,plain,
h2(e10) = op2(e21,e20),
inference('REWRITE',[status(thm)],[1136,1323,theory(equality)]) ).
cnf(1344,plain,
h2(e10) != op2(e23,e20),
inference('REWRITE',[status(thm)],[149,1342,theory(equality)]) ).
cnf(1345,plain,
h2(e10) != op2(e21,e22),
inference('REWRITE',[status(thm)],[176,1342,theory(equality)]) ).
cnf(1355,plain,
( h2(e10) = e21
| h2(e10) = e22
| h2(e10) = e23 ),
inference('REWRITE',[status(thm)],[1336,1342,theory(equality)]) ).
cnf(1356,plain,
h2(e11) = op2(e20,e21),
inference('REWRITE',[status(thm)],[1164,1323,theory(equality)]) ).
cnf(1357,plain,
h2(e11) != op2(e22,e21),
inference('REWRITE',[status(thm)],[152,1356,theory(equality)]) ).
cnf(1358,plain,
h2(e11) != op2(e23,e21),
inference('REWRITE',[status(thm)],[153,1356,theory(equality)]) ).
cnf(1368,plain,
( h2(e11) = e21
| h2(e11) = e22
| h2(e11) = e23 ),
inference('REWRITE',[status(thm)],[1330,1356,theory(equality)]) ).
cnf(1376,plain,
h2(e10) != e21,
inference('REWRITE',[status(thm)],[1297,1342,1320,theory(equality)]) ).
cnf(1379,plain,
( h2(e10) = e22
| h2(e10) = e23 ),
inference('REWRITE',[status(thm)],[1355,1376]) ).
cnf(1382,plain,
h4(e11) = e21,
inference('REWRITE',[status(thm)],[289,307,290,theory(equality)]) ).
cnf(1383,plain,
op2(e22,e23) = e21,
inference('REWRITE',[status(thm)],[307,1382,theory(equality)]) ).
cnf(1384,plain,
op2(e20,e23) != e21,
inference('REWRITE',[status(thm)],[1031,1382,theory(equality)]) ).
cnf(1385,plain,
( op2(e20,e23) = e20
| op2(e20,e23) = e23 ),
inference('REWRITE',[status(thm)],[1278,1384]) ).
cnf(1387,plain,
op2(e21,e23) != e21,
inference('REWRITE',[status(thm)],[1032,1382,theory(equality)]) ).
cnf(1388,plain,
op2(e21,e23) = e23,
inference('REWRITE',[status(thm)],[1340,1387]) ).
cnf(1389,plain,
op2(e20,e23) != e23,
inference('REWRITE',[status(thm)],[163,1388,theory(equality)]) ).
cnf(1391,plain,
op2(e20,e23) = e20,
inference('REWRITE',[status(thm)],[1385,1389]) ).
cnf(1392,plain,
h1(e12) != e20,
inference('REWRITE',[status(thm)],[1206,1391,theory(equality)]) ).
cnf(1394,plain,
op2(e22,e20) = e20,
inference('REWRITE',[status(thm)],[1337,1392]) ).
cnf(1399,plain,
h3(e12) = e23,
inference('REWRITE',[status(thm)],[1341,1391,theory(equality)]) ).
cnf(1400,plain,
op2(e22,e22) = e23,
inference('REWRITE',[status(thm)],[302,1399,theory(equality)]) ).
cnf(1401,plain,
op2(e20,e22) != e23,
inference('REWRITE',[status(thm)],[1051,1399,theory(equality)]) ).
cnf(1402,plain,
( op2(e20,e22) = e21
| op2(e20,e22) = e22 ),
inference('REWRITE',[status(thm)],[1307,1401]) ).
cnf(1404,plain,
op2(e21,e22) != e23,
inference('REWRITE',[status(thm)],[1052,1399,theory(equality)]) ).
cnf(1405,plain,
( op2(e21,e22) = e21
| op2(e21,e22) = e22 ),
inference('REWRITE',[status(thm)],[1310,1404]) ).
cnf(1406,plain,
op2(e22,e21) != e23,
inference('REWRITE',[status(thm)],[1055,1399,theory(equality)]) ).
cnf(1407,plain,
( op2(e22,e21) = e21
| op2(e22,e21) = e22 ),
inference('REWRITE',[status(thm)],[1333,1406]) ).
cnf(1413,plain,
h1(e12) = e21,
inference('REWRITE',[status(thm)],[1299,203,1399,theory(equality)]) ).
cnf(1415,plain,
op2(e23,e20) != e21,
inference('REWRITE',[status(thm)],[1203,1413,theory(equality)]) ).
cnf(1416,plain,
op2(e23,e20) = e23,
inference('REWRITE',[status(thm)],[1314,1415]) ).
cnf(1417,plain,
op2(e23,e21) != e23,
inference('REWRITE',[status(thm)],[187,1416,theory(equality)]) ).
cnf(1418,plain,
op2(e23,e21) = e21,
inference('REWRITE',[status(thm)],[1317,1417]) ).
cnf(1419,plain,
op2(e22,e21) != e21,
inference('REWRITE',[status(thm)],[156,1418,theory(equality)]) ).
cnf(1420,plain,
op2(e22,e21) = e22,
inference('REWRITE',[status(thm)],[1407,1419]) ).
cnf(1421,plain,
h2(e11) != e22,
inference('REWRITE',[status(thm)],[1357,1420,theory(equality)]) ).
cnf(1422,plain,
( h2(e11) = e21
| h2(e11) = e23 ),
inference('REWRITE',[status(thm)],[1368,1421]) ).
cnf(1423,plain,
h2(e11) != e21,
inference('REWRITE',[status(thm)],[1358,1418,theory(equality)]) ).
cnf(1424,plain,
h2(e11) = e23,
inference('REWRITE',[status(thm)],[1422,1423]) ).
cnf(1425,plain,
op2(e20,e21) = e23,
inference('REWRITE',[status(thm)],[1356,1424,theory(equality)]) ).
cnf(1426,plain,
h2(e10) != e23,
inference('REWRITE',[status(thm)],[1344,1416,theory(equality)]) ).
cnf(1427,plain,
h2(e10) = e22,
inference('REWRITE',[status(thm)],[1379,1426]) ).
cnf(1428,plain,
op2(e21,e20) = e22,
inference('REWRITE',[status(thm)],[1342,1427,theory(equality)]) ).
cnf(1429,plain,
op2(e21,e22) != e22,
inference('REWRITE',[status(thm)],[1345,1427,theory(equality)]) ).
cnf(1430,plain,
op2(e21,e22) = e21,
inference('REWRITE',[status(thm)],[1405,1429]) ).
cnf(1431,plain,
op2(e20,e22) != e21,
inference('REWRITE',[status(thm)],[157,1430,theory(equality)]) ).
cnf(1432,plain,
op2(e20,e22) = e22,
inference('REWRITE',[status(thm)],[1402,1431]) ).
cnf(1433,plain,
h1(e10) = e23,
inference('REWRITE',[status(thm)],[1215,1425,1413,theory(equality)]) ).
cnf(1434,plain,
h1(e11) = e22,
inference('REWRITE',[status(thm)],[1243,1428,1413,theory(equality)]) ).
cnf(1435,plain,
( h1(op1(e10,e10)) != e22
| h1(op1(e10,e11)) != e20
| h1(op1(e10,e12)) != e21
| h1(op1(e10,e13)) != e23
| h1(op1(e11,e10)) != e21
| h1(op1(e11,e11)) != e23
| h1(op1(e11,e12)) != e22
| h1(op1(e11,e13)) != e20
| h1(op1(e12,e10)) != e23
| h1(op1(e12,e11)) != e21
| h1(op1(e12,e12)) != e20
| h1(op1(e12,e13)) != e22
| h1(op1(e13,e10)) != e20
| h1(op1(e13,e11)) != e22
| h1(op1(e13,e12)) != e23 ),
inference('REWRITE',[status(thm)],[1265,1432,1391,1324,1430,1388,1394,1420,1400,1383,1416,1418,1304,1434,290,1433,1413,theory(equality)]) ).
cnf(1445,plain,
op1(e10,e13) != e12,
inference('REWRITE',[status(thm)],[117,287,theory(equality)]) ).
cnf(1446,plain,
( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e13 ),
inference('REWRITE',[status(thm)],[4,1445]) ).
cnf(1448,plain,
op1(e11,e13) != e12,
inference('REWRITE',[status(thm)],[119,287,theory(equality)]) ).
cnf(1449,plain,
( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e13 ),
inference('REWRITE',[status(thm)],[8,1448]) ).
cnf(1454,plain,
op1(e13,e10) != e12,
inference('REWRITE',[status(thm)],[141,287,theory(equality)]) ).
cnf(1455,plain,
( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e13 ),
inference('REWRITE',[status(thm)],[13,1454]) ).
cnf(1457,plain,
op1(e13,e11) != e12,
inference('REWRITE',[status(thm)],[143,287,theory(equality)]) ).
cnf(1458,plain,
( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e13 ),
inference('REWRITE',[status(thm)],[14,1457]) ).
cnf(1459,plain,
( op1(e10,e11) = e12
| op1(e11,e11) = e12
| op1(e12,e11) = e12 ),
inference('REWRITE',[status(thm)],[30,1457]) ).
cnf(1463,plain,
( op1(e11,e11) = e10
| op1(e12,e12) = e10 ),
inference('REWRITE',[status(thm)],[221,194,287,theory(equality)]) ).
cnf(1465,plain,
( op1(e11,e10) != e11
| op1(e12,e12) = e10 ),
inference('REWRITE',[status(thm)],[225,194,287,theory(equality)]) ).
cnf(1467,plain,
( op1(e10,e10) = e11
| op1(e12,e12) = e11 ),
inference('REWRITE',[status(thm)],[229,196,287,theory(equality)]) ).
cnf(1471,plain,
op1(e13,e12) = e10,
inference('REWRITE',[status(thm)],[285,287,theory(equality)]) ).
cnf(1474,plain,
op1(e10,e12) != e10,
inference('REWRITE',[status(thm)],[111,1471,theory(equality)]) ).
cnf(1475,plain,
( op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 ),
inference('REWRITE',[status(thm)],[3,1474]) ).
cnf(1477,plain,
op1(e11,e12) != e10,
inference('REWRITE',[status(thm)],[113,1471,theory(equality)]) ).
cnf(1478,plain,
( op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 ),
inference('REWRITE',[status(thm)],[7,1477]) ).
cnf(1480,plain,
op1(e12,e12) != e10,
inference('REWRITE',[status(thm)],[114,1471,theory(equality)]) ).
cnf(1483,plain,
op1(e11,e11) = e10,
inference('REWRITE',[status(thm)],[1463,1480]) ).
cnf(1488,plain,
op1(e10,e11) != e10,
inference('REWRITE',[status(thm)],[103,1483,theory(equality)]) ).
cnf(1489,plain,
( op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 ),
inference('REWRITE',[status(thm)],[2,1488]) ).
cnf(1494,plain,
op1(e13,e11) != e10,
inference('REWRITE',[status(thm)],[107,1483,theory(equality)]) ).
cnf(1495,plain,
( op1(e13,e11) = e11
| op1(e13,e11) = e13 ),
inference('REWRITE',[status(thm)],[1458,1494]) ).
cnf(1496,plain,
op1(e11,e10) != e10,
inference('REWRITE',[status(thm)],[127,1483,theory(equality)]) ).
cnf(1497,plain,
( op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 ),
inference('REWRITE',[status(thm)],[5,1496]) ).
cnf(1498,plain,
( op1(e10,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 ),
inference('REWRITE',[status(thm)],[18,1496]) ).
cnf(1499,plain,
op1(e11,e13) != e10,
inference('REWRITE',[status(thm)],[131,1483,theory(equality)]) ).
cnf(1501,plain,
( op1(e11,e13) = e11
| op1(e11,e13) = e13 ),
inference('REWRITE',[status(thm)],[1449,1499]) ).
cnf(1503,plain,
( op1(e10,e13) != e10
| op1(e12,e12) = e13 ),
inference('REWRITE',[status(thm)],[249,195,1483,theory(equality)]) ).
cnf(1505,plain,
( op1(e10,e11) = e12
| op1(e12,e11) = e12 ),
inference('REWRITE',[status(thm)],[1459,194,1483,theory(equality)]) ).
cnf(1506,plain,
op1(e11,e10) != e11,
inference('REWRITE',[status(thm)],[1465,1480]) ).
cnf(1509,plain,
( op1(e11,e10) = e12
| op1(e11,e10) = e13 ),
inference('REWRITE',[status(thm)],[1497,1506]) ).
cnf(1510,plain,
op1(e13,e10) != e10,
inference('REWRITE',[status(thm)],[140,1471,theory(equality)]) ).
cnf(1511,plain,
( op1(e13,e10) = e11
| op1(e13,e10) = e13 ),
inference('REWRITE',[status(thm)],[1455,1510]) ).
cnf(1512,plain,
( op1(e10,e10) = e10
| op1(e12,e10) = e10 ),
inference('REWRITE',[status(thm)],[1498,1510]) ).
cnf(1513,plain,
( h1(op1(e10,e10)) != e22
| h1(op1(e10,e11)) != e20
| h1(op1(e10,e12)) != e21
| h1(op1(e10,e13)) != e23
| h1(op1(e11,e10)) != e21
| h1(op1(e11,e12)) != e22
| h1(op1(e11,e13)) != e20
| h1(op1(e12,e10)) != e23
| h1(op1(e12,e11)) != e21
| h1(op1(e12,e12)) != e20
| h1(op1(e12,e13)) != e22
| h1(op1(e13,e10)) != e20
| h1(op1(e13,e11)) != e22 ),
inference('REWRITE',[status(thm)],[1435,1433,1483,1471,theory(equality)]) ).
cnf(1519,plain,
op1(e12,e13) = e11,
inference('REWRITE',[status(thm)],[286,287,theory(equality)]) ).
cnf(1521,plain,
op1(e10,e13) != e11,
inference('REWRITE',[status(thm)],[116,1519,theory(equality)]) ).
cnf(1523,plain,
( op1(e10,e13) = e10
| op1(e10,e13) = e13 ),
inference('REWRITE',[status(thm)],[1446,1521]) ).
cnf(1524,plain,
op1(e11,e13) != e11,
inference('REWRITE',[status(thm)],[118,1519,theory(equality)]) ).
cnf(1525,plain,
op1(e11,e13) = e13,
inference('REWRITE',[status(thm)],[1501,1524]) ).
cnf(1526,plain,
op1(e10,e13) != e13,
inference('REWRITE',[status(thm)],[115,1525,theory(equality)]) ).
cnf(1528,plain,
op1(e10,e13) = e10,
inference('REWRITE',[status(thm)],[1523,1526]) ).
cnf(1529,plain,
op1(e10,e10) != e10,
inference('REWRITE',[status(thm)],[123,1528,theory(equality)]) ).
cnf(1531,plain,
op1(e12,e10) = e10,
inference('REWRITE',[status(thm)],[1512,1529]) ).
cnf(1537,plain,
op1(e12,e12) = e13,
inference('REWRITE',[status(thm)],[1503,1528,theory(equality)]) ).
cnf(1538,plain,
op1(e10,e12) != e13,
inference('REWRITE',[status(thm)],[110,1537,theory(equality)]) ).
cnf(1539,plain,
( op1(e10,e12) = e11
| op1(e10,e12) = e12 ),
inference('REWRITE',[status(thm)],[1475,1538]) ).
cnf(1541,plain,
op1(e11,e12) != e13,
inference('REWRITE',[status(thm)],[112,1537,theory(equality)]) ).
cnf(1542,plain,
( op1(e11,e12) = e11
| op1(e11,e12) = e12 ),
inference('REWRITE',[status(thm)],[1478,1541]) ).
cnf(1547,plain,
op1(e10,e10) = e11,
inference('REWRITE',[status(thm)],[1467,197,1537,theory(equality)]) ).
cnf(1548,plain,
op1(e13,e10) != e11,
inference('REWRITE',[status(thm)],[99,1547,theory(equality)]) ).
cnf(1549,plain,
op1(e13,e10) = e13,
inference('REWRITE',[status(thm)],[1511,1548]) ).
cnf(1550,plain,
op1(e11,e10) != e13,
inference('REWRITE',[status(thm)],[101,1549,theory(equality)]) ).
cnf(1551,plain,
op1(e11,e10) = e12,
inference('REWRITE',[status(thm)],[1509,1550]) ).
cnf(1552,plain,
op1(e11,e12) != e12,
inference('REWRITE',[status(thm)],[128,1551,theory(equality)]) ).
cnf(1553,plain,
op1(e11,e12) = e11,
inference('REWRITE',[status(thm)],[1542,1552]) ).
cnf(1554,plain,
op1(e10,e12) != e11,
inference('REWRITE',[status(thm)],[109,1553,theory(equality)]) ).
cnf(1555,plain,
op1(e10,e12) = e12,
inference('REWRITE',[status(thm)],[1539,1554]) ).
cnf(1556,plain,
op1(e10,e11) != e12,
inference('REWRITE',[status(thm)],[124,1555,theory(equality)]) ).
cnf(1557,plain,
( op1(e10,e11) = e11
| op1(e10,e11) = e13 ),
inference('REWRITE',[status(thm)],[1489,1556]) ).
cnf(1558,plain,
op1(e12,e11) = e12,
inference('REWRITE',[status(thm)],[1505,1556]) ).
cnf(1560,plain,
op1(e13,e11) != e13,
inference('REWRITE',[status(thm)],[139,1549,theory(equality)]) ).
cnf(1561,plain,
op1(e13,e11) = e11,
inference('REWRITE',[status(thm)],[1495,1560]) ).
cnf(1562,plain,
op1(e10,e11) != e11,
inference('REWRITE',[status(thm)],[105,1561,theory(equality)]) ).
cnf(1563,plain,
op1(e10,e11) = e13,
inference('REWRITE',[status(thm)],[1557,1562]) ).
cnf(1564,plain,
$false,
inference('REWRITE',[status(thm)],[1513,1561,1549,1537,1558,1531,1525,1553,1551,1433,1528,1413,1555,291,1563,1434,1547,1519,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : ALG117+1 : TPTP v8.1.0. Released v2.7.0.
% 0.07/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 8 15:34:02 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.44 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 *
% 0.18/0.45 *
% 0.18/0.46 #<PACKAGE "SNARK-USER">
% 0.18/0.46 *
% 0.18/0.46 SNARK-TPTP-OPTIONS
% 0.18/0.46 *
% 0.18/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.18/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.18/0.46 (USE-FACTORING :POS)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.18/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.18/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.18/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.18/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.18/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.18/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.18/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.18/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.18/0.46 *
% 0.18/0.46 "."
% 0.18/0.46 *
% 0.18/0.46 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-08T15:34:02
% 0.18/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n026.cluster.edu at 2022-06-08T15:34:02
% 1.99/2.22
% 1.99/2.22
% 1.99/2.22 #||
% 1.99/2.22 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.99/2.22 % SZS output start Refutation
% See solution above
% 1.99/2.24 ||#
% 1.99/2.24
% 1.99/2.24 ; Summary of computation:
% 1.99/2.24 ; 2499 formulas have been input or derived (from 1 formulas).
% 1.99/2.24 ; 1564 (63%) were retained. Of these,
% 1.99/2.24 ; 1487 (95%) were simplified or subsumed later,
% 1.99/2.24 ; 77 ( 5%) are still being kept.
% 1.99/2.24 ;
% 1.99/2.24 ; Run time in seconds excluding printing time:
% 1.99/2.24 ; 0.047 3% Read assertion file (1 call)
% 1.99/2.24 ; 0.458 26% Assert (18 calls)
% 1.99/2.24 ; 0.222 13% Process new row (2,132 calls)
% 1.99/2.24 ; 0.006 0% Condensing (907 calls)
% 1.99/2.24 ; 0.100 6% Forward subsumption (907 calls)
% 1.99/2.24 ; 0.145 8% Backward subsumption (906 calls)
% 1.99/2.24 ; 0.221 13% Clause clause subsumption (2,793 calls)
% 1.99/2.24 ; 0.471 27% Forward simplification (2,132 calls)
% 1.99/2.24 ; 0.070 4% Backward simplification (1,201 calls)
% 1.99/2.24 ; 0.000 0% Ordering (71 calls)
% 1.99/2.24 ; 0.000 0% Sortal reasoning (32 calls)
% 1.99/2.24 ; 0.003 0% Purity testing (1 call)
% 1.99/2.24 ; 0.024 1% Other
% 1.99/2.24 ; 1.767 Total
% 1.99/2.24 ; 1.785 Real time
% 1.99/2.24 ;
% 1.99/2.24 ; Term-hash-array has 687 terms in all.
% 1.99/2.24 ; Feature-vector-row-index has 0 entries (209 at peak, 906 added, 906 deleted).
% 1.99/2.24 ; Feature-vector-row-index has 1 node (1,652 at peak, 7,505 added, 7,504 deleted).
% 1.99/2.24 ; Retrieved 1,252 possibly forward subsuming rows in 907 calls.
% 1.99/2.24 ; Retrieved 1,541 possibly backward subsumed rows in 906 calls.
% 1.99/2.24 ; Path-index has 132 entries (501 at peak, 1,452 added, 1,320 deleted).
% 1.99/2.24 ; Path-index has 166 nodes (274 at peak, 730 added, 564 deleted).
% 1.99/2.24 ; Trie-index has 132 entries (501 at peak, 1,452 added, 1,320 deleted).
% 1.99/2.24 ; Trie-index has 217 nodes (1,022 at peak, 3,130 added, 2,913 deleted).
% 1.99/2.24 ; Retrieved 16,360 generalization terms in 121,586 calls.
% 1.99/2.24 ; Retrieved 294 instance terms in 294 calls.
% 1.99/2.24 ;
% 1.99/2.24 ; The agenda of backward simplifiable rows to process has 3 entries:
% 1.99/2.24 ; 3 with value 0
% 1.99/2.24 ; The agenda of input rows to give has 76 entries:
% 1.99/2.24 ; 28 with value 4 16 with value 6 32 with value 7
% 1.99/2.24 Evaluation took:
% 1.99/2.24 1.785 seconds of real time
% 1.99/2.24 1.753049 seconds of user run time
% 1.99/2.24 0.032179 seconds of system run time
% 1.99/2.24 [Run times include 0.037 seconds GC run time.]
% 1.99/2.24 0 calls to %EVAL
% 1.99/2.24 0 page faults and
% 1.99/2.24 159,483,192 bytes consed.
% 1.99/2.24 :PROOF-FOUND
% 1.99/2.24 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-08T15:34:04
% 1.99/2.24 :PROOF-FOUND
% 1.99/2.24 *
%------------------------------------------------------------------------------