%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ALG124+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n022.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:57 EDT 2022
% Result : Theorem 186.72s 186.98s
% Output : Refutation 186.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 126
% Syntax : Number of clauses : 365 ( 188 unt; 151 nHn; 365 RR)
% Number of literals : 927 ( 926 equ; 425 neg)
% Maximal clause size : 20 ( 2 avg)
% Maximal term depth : 4 ( 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(4,axiom,
( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(6,axiom,
( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(11,axiom,
( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(12,axiom,
( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(16,axiom,
( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(17,axiom,
( op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(26,axiom,
( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(27,axiom,
( op1(e11,e10) = e11
| op1(e11,e11) = e11
| op1(e11,e12) = e11
| op1(e11,e13) = e11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(28,axiom,
( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e12,e11) = e11
| op1(e13,e11) = e11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(31,axiom,
( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(36,axiom,
( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e12,e12) = e11
| op1(e13,e12) = e11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(37,axiom,
( op1(e12,e10) = e12
| op1(e12,e11) = e12
| op1(e12,e12) = e12
| op1(e12,e13) = e12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(38,axiom,
( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e12,e12) = e12
| op1(e13,e12) = e12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(41,axiom,
( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(43,axiom,
( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(47,axiom,
( op1(e13,e10) = e13
| op1(e13,e11) = e13
| op1(e13,e12) = e13
| op1(e13,e13) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(48,axiom,
( op1(e10,e13) = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
cnf(52,axiom,
( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(54,axiom,
( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(59,axiom,
( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(64,axiom,
( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
cnf(69,axiom,
( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(74,axiom,
( op2(e20,e21) = e20
| op2(e21,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(76,axiom,
( op2(e20,e21) = e21
| op2(e21,e21) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(85,axiom,
( op2(e22,e20) = e22
| op2(e22,e21) = e22
| op2(e22,e22) = e22
| op2(e22,e23) = e22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(87,axiom,
( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(89,axiom,
( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(94,axiom,
( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(95,axiom,
( op2(e23,e20) = e23
| op2(e23,e21) = e23
| op2(e23,e22) = e23
| op2(e23,e23) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(96,axiom,
( op2(e20,e23) = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
cnf(97,axiom,
op1(e10,e10) != op1(e11,e10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(99,axiom,
op1(e10,e10) != op1(e13,e10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(100,axiom,
op1(e11,e10) != op1(e12,e10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(101,axiom,
op1(e11,e10) != op1(e13,e10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(108,axiom,
op1(e12,e11) != op1(e13,e11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(113,axiom,
op1(e11,e12) != op1(e13,e12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(114,axiom,
op1(e12,e12) != op1(e13,e12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(116,axiom,
op1(e10,e13) != op1(e12,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(117,axiom,
op1(e10,e13) != op1(e13,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(118,axiom,
op1(e11,e13) != op1(e12,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(119,axiom,
op1(e11,e13) != op1(e13,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(121,axiom,
op1(e10,e10) != op1(e10,e11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(123,axiom,
op1(e10,e10) != op1(e10,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(126,axiom,
op1(e10,e12) != op1(e10,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(127,axiom,
op1(e11,e10) != op1(e11,e11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(131,axiom,
op1(e11,e11) != op1(e11,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(133,axiom,
op1(e12,e10) != op1(e12,e11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(134,axiom,
op1(e12,e10) != op1(e12,e12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(135,axiom,
op1(e12,e10) != op1(e12,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(136,axiom,
op1(e12,e11) != op1(e12,e12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(138,axiom,
op1(e12,e12) != op1(e12,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(139,axiom,
op1(e13,e10) != op1(e13,e11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(140,axiom,
op1(e13,e10) != op1(e13,e12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(141,axiom,
op1(e13,e10) != op1(e13,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(143,axiom,
op1(e13,e11) != op1(e13,e13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
cnf(145,axiom,
op2(e20,e20) != op2(e21,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(146,axiom,
op2(e20,e20) != op2(e22,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(147,axiom,
op2(e20,e20) != op2(e23,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(148,axiom,
op2(e21,e20) != op2(e22,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(149,axiom,
op2(e21,e20) != op2(e23,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(150,axiom,
op2(e22,e20) != op2(e23,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(151,axiom,
op2(e20,e21) != op2(e21,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(154,axiom,
op2(e21,e21) != op2(e22,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(155,axiom,
op2(e21,e21) != op2(e23,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(157,axiom,
op2(e20,e22) != op2(e21,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(162,axiom,
op2(e22,e22) != op2(e23,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(164,axiom,
op2(e20,e23) != op2(e22,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(165,axiom,
op2(e20,e23) != op2(e23,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(166,axiom,
op2(e21,e23) != op2(e22,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(171,axiom,
op2(e20,e20) != op2(e20,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(173,axiom,
op2(e20,e21) != op2(e20,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(175,axiom,
op2(e21,e20) != op2(e21,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(176,axiom,
op2(e21,e20) != op2(e21,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(179,axiom,
op2(e21,e21) != op2(e21,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(180,axiom,
op2(e21,e22) != op2(e21,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(181,axiom,
op2(e22,e20) != op2(e22,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(182,axiom,
op2(e22,e20) != op2(e22,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(183,axiom,
op2(e22,e20) != op2(e22,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(184,axiom,
op2(e22,e21) != op2(e22,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(186,axiom,
op2(e22,e22) != op2(e22,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(189,axiom,
op2(e23,e20) != op2(e23,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(191,axiom,
op2(e23,e21) != op2(e23,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
cnf(193,axiom,
e10 != e11,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
cnf(194,axiom,
e10 != e12,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
cnf(195,axiom,
e10 != e13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
cnf(196,axiom,
e11 != e12,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
cnf(197,axiom,
e11 != e13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
cnf(198,axiom,
e12 != e13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
cnf(199,axiom,
e20 != e21,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
cnf(200,axiom,
e20 != e22,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
cnf(201,axiom,
e20 != e23,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
cnf(202,axiom,
e21 != e22,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
cnf(203,axiom,
e21 != e23,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
cnf(204,axiom,
e22 != e23,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
cnf(221,axiom,
op1(e10,e10) != e10,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
cnf(222,axiom,
op1(e11,e11) != e11,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
cnf(223,axiom,
op1(e12,e12) != e12,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
cnf(224,axiom,
op1(e13,e13) != e13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
cnf(14129,axiom,
( op1(e13,e11) != e10
| op1(e13,e10) = e11
| op1(e12,e10) != e11
| op1(e12,e11) = e10
| op1(e13,e10) != e12
| op1(e13,e12) = e10
| op1(e13,e12) != e13
| op1(e13,e13) = e12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
cnf(16450,axiom,
( op1(e13,e13) != e10
| op1(e13,e10) = e13
| op1(e10,e13) != e11
| op1(e10,e11) = e13
| op1(e13,e10) != e12
| op1(e13,e12) = e10
| op1(e13,e12) != e13
| op1(e13,e13) = e12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
cnf(16906,axiom,
( op1(e13,e13) != e10
| op1(e13,e10) = e13
| op1(e12,e10) != e11
| op1(e12,e11) = e10
| op1(e12,e11) != e12
| op1(e12,e12) = e11
| op1(e10,e10) != e13
| op1(e10,e13) = e10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
cnf(17395,axiom,
( op1(e13,e13) != e10
| op1(e13,e10) = e13
| op1(e13,e12) != e11
| op1(e13,e11) = e12
| op1(e12,e11) != e12
| op1(e12,e12) = e11
| op1(e10,e10) != e13
| op1(e10,e13) = e10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
cnf(17554,axiom,
op2(e21,e21) != e21,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
cnf(17555,axiom,
op2(e22,e22) != e22,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
cnf(17556,axiom,
op2(e23,e23) != e23,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
cnf(28468,axiom,
( op2(e22,e22) != e20
| op2(e22,e20) = e22
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e22,e21) != e22
| op2(e22,e22) = e21
| op2(e23,e22) != e23
| op2(e23,e23) = e22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
cnf(31461,axiom,
( op2(e23,e21) != e20
| op2(e23,e20) = e21
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e23,e20) != e22
| op2(e23,e22) = e20
| op2(e23,e22) != e23
| op2(e23,e23) = e22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
cnf(34256,axiom,
( op2(e23,e23) != e20
| op2(e23,e20) = e23
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e22,e23) != e22
| op2(e22,e22) = e23
| op2(e22,e21) != e23
| op2(e22,e23) = e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
cnf(34885,axiom,
e11 = op1(op1(op1(e10,e10),e10),e10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
cnf(34886,axiom,
e12 = op1(op1(e10,e10),e10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
cnf(34887,axiom,
op1(e10,e10) = e13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
cnf(34888,axiom,
e21 = op2(op2(op2(e20,e20),e20),e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
cnf(34889,axiom,
e22 = op2(op2(e20,e20),e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
cnf(34890,axiom,
op2(e20,e20) = e23,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
cnf(34891,axiom,
h1(e10) = e20,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
cnf(34892,axiom,
h1(e11) = op2(op2(op2(e20,e20),e20),e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
cnf(34893,plain,
h1(e11) = op2(op2(e23,e20),e20),
inference('REWRITE',[status(thm)],[34892,34890,theory(equality)]) ).
cnf(34894,axiom,
h1(e12) = op2(op2(e20,e20),e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
cnf(34895,plain,
h1(e12) = op2(e23,e20),
inference('REWRITE',[status(thm)],[34894,34890,theory(equality)]) ).
cnf(34896,axiom,
h1(e13) = op2(e20,e20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
cnf(34897,plain,
h1(e13) = e23,
inference('REWRITE',[status(thm)],[34896,34890,theory(equality)]) ).
cnf(34900,axiom,
h2(e12) = op2(op2(e21,e21),e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
cnf(34901,axiom,
h2(e13) = op2(e21,e21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
cnf(34905,axiom,
h3(e13) = op2(e22,e22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
cnf(34909,axiom,
h4(e13) = op2(e23,e23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
cnf(34920,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(e10) != e20
| h1(e11) != e21
| h1(e12) != e22
| h1(e13) != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
cnf(34921,plain,
( h1(op1(e10,e11)) != op2(e20,h1(e11))
| h1(op1(e10,e12)) != op2(e20,h1(e12))
| h1(op1(e10,e13)) != op2(e20,e23)
| h1(op1(e11,e10)) != op2(h1(e11),e20)
| 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),e23)
| h1(op1(e12,e10)) != op2(h1(e12),e20)
| 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),e23)
| h1(op1(e13,e10)) != h1(e12)
| h1(op1(e13,e11)) != op2(e23,h1(e11))
| h1(op1(e13,e12)) != op2(e23,h1(e12))
| h1(op1(e13,e13)) != h4(e13)
| h1(e11) != e21
| h1(e12) != e22 ),
inference('REWRITE',[status(thm)],[34920,34909,34895,34890,34891,34897,34887,theory(equality)]) ).
cnf(35365,plain,
( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| h4(e13) = e22 ),
inference('REWRITE',[status(thm)],[94,34909,theory(equality)]) ).
cnf(35366,plain,
op2(e20,e23) != h4(e13),
inference('REWRITE',[status(thm)],[165,34909,theory(equality)]) ).
cnf(35369,plain,
op2(e23,e21) != h4(e13),
inference('REWRITE',[status(thm)],[191,34909,theory(equality)]) ).
cnf(35848,plain,
( op2(e22,e20) = e23
| op2(e22,e21) = e23
| h3(e13) = e23
| op2(e22,e23) = e23 ),
inference('REWRITE',[status(thm)],[87,34905,theory(equality)]) ).
cnf(35852,plain,
h3(e13) != op2(e23,e22),
inference('REWRITE',[status(thm)],[162,34905,theory(equality)]) ).
cnf(35853,plain,
op2(e22,e20) != h3(e13),
inference('REWRITE',[status(thm)],[182,34905,theory(equality)]) ).
cnf(35854,plain,
op2(e22,e21) != h3(e13),
inference('REWRITE',[status(thm)],[184,34905,theory(equality)]) ).
cnf(35855,plain,
h3(e13) != op2(e22,e23),
inference('REWRITE',[status(thm)],[186,34905,theory(equality)]) ).
cnf(36692,plain,
( h3(e13) != e20
| op2(e22,e20) = e22
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e22,e21) != e22
| h3(e13) = e21
| op2(e23,e22) != e23
| h4(e13) = e22 ),
inference('REWRITE',[status(thm)],[28468,34909,34905,theory(equality)]) ).
cnf(37236,plain,
( op2(e20,e21) = e20
| h2(e13) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 ),
inference('REWRITE',[status(thm)],[74,34901,theory(equality)]) ).
cnf(37241,plain,
op2(e20,e21) != h2(e13),
inference('REWRITE',[status(thm)],[151,34901,theory(equality)]) ).
cnf(37242,plain,
h2(e13) != op2(e22,e21),
inference('REWRITE',[status(thm)],[154,34901,theory(equality)]) ).
cnf(37243,plain,
h2(e13) != op2(e23,e21),
inference('REWRITE',[status(thm)],[155,34901,theory(equality)]) ).
cnf(37244,plain,
op2(e21,e20) != h2(e13),
inference('REWRITE',[status(thm)],[175,34901,theory(equality)]) ).
cnf(37246,plain,
h2(e13) != op2(e21,e23),
inference('REWRITE',[status(thm)],[179,34901,theory(equality)]) ).
cnf(39844,plain,
h2(e12) = op2(h2(e13),e21),
inference('REWRITE',[status(thm)],[34900,34901,theory(equality)]) ).
cnf(39901,plain,
( h1(e12) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| h4(e13) = e20 ),
inference('REWRITE',[status(thm)],[89,34909,34895,theory(equality)]) ).
cnf(39904,plain,
op2(e21,e20) != h1(e12),
inference('REWRITE',[status(thm)],[149,34895,theory(equality)]) ).
cnf(39905,plain,
op2(e22,e20) != h1(e12),
inference('REWRITE',[status(thm)],[150,34895,theory(equality)]) ).
cnf(39908,plain,
h1(e12) != h4(e13),
inference('REWRITE',[status(thm)],[189,34909,34895,theory(equality)]) ).
cnf(42333,plain,
( op2(e23,e21) != e20
| h1(e12) = e21
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| h1(e12) != e22
| op2(e23,e22) = e20
| op2(e23,e22) != e23
| h4(e13) = e22 ),
inference('REWRITE',[status(thm)],[31461,34909,34895,theory(equality)]) ).
cnf(44423,plain,
( h4(e13) != e20
| h1(e12) = e23
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e22,e23) != e22
| h3(e13) = e23
| op2(e22,e21) != e23
| op2(e22,e23) = e21 ),
inference('REWRITE',[status(thm)],[34256,34905,34909,34895,theory(equality)]) ).
cnf(44943,plain,
h1(e11) = op2(h1(e12),e20),
inference('REWRITE',[status(thm)],[34893,34895,theory(equality)]) ).
cnf(44945,plain,
( h1(op1(e10,e11)) != op2(e20,h1(e11))
| h1(op1(e10,e12)) != op2(e20,h1(e12))
| h1(op1(e10,e13)) != op2(e20,e23)
| h1(op1(e11,e10)) != op2(h1(e11),e20)
| 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),e23)
| h1(op1(e12,e10)) != h1(e11)
| 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),e23)
| h1(op1(e13,e10)) != h1(e12)
| h1(op1(e13,e11)) != op2(e23,h1(e11))
| h1(op1(e13,e12)) != op2(e23,h1(e12))
| h1(op1(e13,e13)) != h4(e13)
| h1(e11) != e21
| h1(e12) != e22 ),
inference('REWRITE',[status(thm)],[34921,44943,theory(equality)]) ).
cnf(44950,plain,
( op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 ),
inference('REWRITE',[status(thm)],[69,204,34890,theory(equality)]) ).
cnf(44952,plain,
op2(e21,e20) != e23,
inference('REWRITE',[status(thm)],[145,34890,theory(equality)]) ).
cnf(44953,plain,
( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22 ),
inference('REWRITE',[status(thm)],[53,44952]) ).
cnf(46037,plain,
op2(e22,e20) != e23,
inference('REWRITE',[status(thm)],[146,34890,theory(equality)]) ).
cnf(46207,plain,
( op2(e22,e21) = e23
| h3(e13) = e23
| op2(e22,e23) = e23 ),
inference('REWRITE',[status(thm)],[35848,46037]) ).
cnf(47005,plain,
h1(e12) != e23,
inference('REWRITE',[status(thm)],[147,34895,34890,theory(equality)]) ).
cnf(47447,plain,
( h4(e13) != e20
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e22,e23) != e22
| h3(e13) = e23
| op2(e22,e21) != e23
| op2(e22,e23) = e21 ),
inference('REWRITE',[status(thm)],[44423,47005]) ).
cnf(49046,plain,
op2(e20,e23) != e23,
inference('REWRITE',[status(thm)],[171,34890,theory(equality)]) ).
cnf(49047,plain,
( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22 ),
inference('REWRITE',[status(thm)],[52,49046]) ).
cnf(51541,plain,
h1(e12) = e22,
inference('REWRITE',[status(thm)],[34889,34895,34890,theory(equality)]) ).
cnf(51542,plain,
op2(e23,e20) = e22,
inference('REWRITE',[status(thm)],[34895,51541,theory(equality)]) ).
cnf(51543,plain,
( op2(e23,e21) = e20
| op2(e23,e22) = e20
| h4(e13) = e20 ),
inference('REWRITE',[status(thm)],[39901,200,51541,theory(equality)]) ).
cnf(51545,plain,
op2(e21,e20) != e22,
inference('REWRITE',[status(thm)],[39904,51541,theory(equality)]) ).
cnf(51904,plain,
( op2(e21,e20) = e20
| op2(e21,e20) = e21 ),
inference('REWRITE',[status(thm)],[44953,51545]) ).
cnf(52093,plain,
op2(e22,e20) != e22,
inference('REWRITE',[status(thm)],[39905,51541,theory(equality)]) ).
cnf(52129,plain,
( h3(e13) != e20
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e22,e21) != e22
| h3(e13) = e21
| op2(e23,e22) != e23
| h4(e13) = e22 ),
inference('REWRITE',[status(thm)],[36692,52093]) ).
cnf(52992,plain,
h4(e13) != e22,
inference('REWRITE',[status(thm)],[39908,51541,theory(equality)]) ).
cnf(52993,plain,
( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22 ),
inference('REWRITE',[status(thm)],[35365,52992]) ).
cnf(53395,plain,
( h3(e13) != e20
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e22,e21) != e22
| h3(e13) = e21
| op2(e23,e22) != e23 ),
inference('REWRITE',[status(thm)],[52129,52992]) ).
cnf(53838,plain,
( op2(e23,e21) != e20
| op2(e22,e20) != e21
| op2(e22,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e22) != e23 ),
inference('REWRITE',[status(thm)],[42333,52992,202,51541,theory(equality)]) ).
cnf(53957,plain,
h1(e11) = op2(e22,e20),
inference('REWRITE',[status(thm)],[44943,51541,theory(equality)]) ).
cnf(53958,plain,
op2(e21,e20) != h1(e11),
inference('REWRITE',[status(thm)],[148,53957,theory(equality)]) ).
cnf(53959,plain,
h1(e11) != op2(e22,e21),
inference('REWRITE',[status(thm)],[181,53957,theory(equality)]) ).
cnf(53960,plain,
h1(e11) != op2(e22,e23),
inference('REWRITE',[status(thm)],[183,53957,theory(equality)]) ).
cnf(53971,plain,
h1(e11) != h3(e13),
inference('REWRITE',[status(thm)],[35853,53957,theory(equality)]) ).
cnf(54186,plain,
( h4(e13) != e20
| h1(e11) != e21
| op2(e22,e21) = e20
| op2(e22,e23) != e22
| h3(e13) = e23
| op2(e22,e21) != e23
| op2(e22,e23) = e21 ),
inference('REWRITE',[status(thm)],[47447,53957,theory(equality)]) ).
cnf(54598,plain,
( h3(e13) != e20
| h1(e11) != e21
| op2(e22,e21) = e20
| op2(e22,e21) != e22
| h3(e13) = e21
| op2(e23,e22) != e23 ),
inference('REWRITE',[status(thm)],[53395,53957,theory(equality)]) ).
cnf(54704,plain,
( op2(e23,e21) != e20
| h1(e11) != e21
| op2(e22,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e22) != e23 ),
inference('REWRITE',[status(thm)],[53838,53957,theory(equality)]) ).
cnf(54705,plain,
( h1(op1(e10,e11)) != op2(e20,h1(e11))
| h1(op1(e10,e12)) != op2(e20,e22)
| h1(op1(e10,e13)) != op2(e20,e23)
| h1(op1(e11,e10)) != op2(h1(e11),e20)
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),e22)
| h1(op1(e11,e13)) != op2(h1(e11),e23)
| h1(op1(e12,e10)) != h1(e11)
| h1(op1(e12,e11)) != op2(e22,h1(e11))
| h1(op1(e12,e12)) != h3(e13)
| h1(op1(e12,e13)) != op2(e22,e23)
| h1(op1(e13,e10)) != e22
| h1(op1(e13,e11)) != op2(e23,h1(e11))
| h1(op1(e13,e12)) != op2(e23,e22)
| h1(op1(e13,e13)) != h4(e13)
| h1(e11) != e21 ),
inference('REWRITE',[status(thm)],[44945,34905,51541,theory(equality)]) ).
cnf(55262,plain,
h1(e11) = e21,
inference('REWRITE',[status(thm)],[34888,53957,34889,theory(equality)]) ).
cnf(55263,plain,
op2(e22,e20) = e21,
inference('REWRITE',[status(thm)],[53957,55262,theory(equality)]) ).
cnf(55264,plain,
op2(e21,e20) != e21,
inference('REWRITE',[status(thm)],[53958,55262,theory(equality)]) ).
cnf(55467,plain,
op2(e21,e20) = e20,
inference('REWRITE',[status(thm)],[51904,55264]) ).
cnf(55468,plain,
op2(e21,e22) != e20,
inference('REWRITE',[status(thm)],[176,55467,theory(equality)]) ).
cnf(55469,plain,
( op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 ),
inference('REWRITE',[status(thm)],[55,55468]) ).
cnf(55474,plain,
h2(e13) != e20,
inference('REWRITE',[status(thm)],[37244,55467,theory(equality)]) ).
cnf(55475,plain,
( op2(e20,e21) = e20
| op2(e22,e21) = e20
| op2(e23,e21) = e20 ),
inference('REWRITE',[status(thm)],[37236,55474]) ).
cnf(55476,plain,
op2(e22,e21) != e21,
inference('REWRITE',[status(thm)],[53959,55262,theory(equality)]) ).
cnf(55478,plain,
op2(e22,e23) != e21,
inference('REWRITE',[status(thm)],[53960,55262,theory(equality)]) ).
cnf(55758,plain,
h3(e13) != e21,
inference('REWRITE',[status(thm)],[53971,55262,theory(equality)]) ).
cnf(56044,plain,
( h4(e13) != e20
| op2(e22,e21) = e20
| op2(e22,e23) != e22
| h3(e13) = e23
| op2(e22,e21) != e23 ),
inference('REWRITE',[status(thm)],[54186,55478,55262,theory(equality)]) ).
cnf(56196,plain,
( h3(e13) != e20
| op2(e22,e21) = e20
| op2(e22,e21) != e22
| op2(e23,e22) != e23 ),
inference('REWRITE',[status(thm)],[54598,55758,55262,theory(equality)]) ).
cnf(56239,plain,
( op2(e23,e21) != e20
| op2(e22,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e22) != e23 ),
inference('REWRITE',[status(thm)],[54704,55262,theory(equality)]) ).
cnf(56240,plain,
( h1(op1(e10,e11)) != op2(e20,e21)
| h1(op1(e10,e12)) != op2(e20,e22)
| h1(op1(e10,e13)) != op2(e20,e23)
| h1(op1(e11,e10)) != e20
| h1(op1(e11,e11)) != h2(e13)
| h1(op1(e11,e12)) != op2(e21,e22)
| h1(op1(e11,e13)) != op2(e21,e23)
| h1(op1(e12,e10)) != e21
| h1(op1(e12,e11)) != op2(e22,e21)
| h1(op1(e12,e12)) != h3(e13)
| h1(op1(e12,e13)) != op2(e22,e23)
| h1(op1(e13,e10)) != e22
| h1(op1(e13,e11)) != op2(e23,e21)
| h1(op1(e13,e12)) != op2(e23,e22)
| h1(op1(e13,e13)) != h4(e13) ),
inference('REWRITE',[status(thm)],[54705,34901,55467,55262,theory(equality)]) ).
cnf(56287,plain,
op1(e11,e10) != e13,
inference('REWRITE',[status(thm)],[97,34887,theory(equality)]) ).
cnf(56288,plain,
( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12 ),
inference('REWRITE',[status(thm)],[5,56287]) ).
cnf(56289,plain,
( op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 ),
inference('REWRITE',[status(thm)],[31,56287]) ).
cnf(58340,plain,
op1(e13,e10) != e13,
inference('REWRITE',[status(thm)],[99,34887,theory(equality)]) ).
cnf(58477,plain,
( op1(e13,e13) != e10
| op1(e10,e13) != e11
| op1(e10,e11) = e13
| op1(e13,e10) != e12
| op1(e13,e12) = e10
| op1(e13,e12) != e13
| op1(e13,e13) = e12 ),
inference('REWRITE',[status(thm)],[16450,58340]) ).
cnf(59190,plain,
op1(e10,e11) != e13,
inference('REWRITE',[status(thm)],[121,34887,theory(equality)]) ).
cnf(59815,plain,
( op1(e13,e13) != e10
| op1(e10,e13) != e11
| op1(e13,e10) != e12
| op1(e13,e12) = e10
| op1(e13,e12) != e13
| op1(e13,e13) = e12 ),
inference('REWRITE',[status(thm)],[58477,59190]) ).
cnf(60381,plain,
op1(e10,e13) != e13,
inference('REWRITE',[status(thm)],[123,34887,theory(equality)]) ).
cnf(60382,plain,
( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12 ),
inference('REWRITE',[status(thm)],[4,60381]) ).
cnf(62818,plain,
( op1(e13,e13) != e10
| op1(e12,e10) != e11
| op1(e12,e11) = e10
| op1(e12,e11) != e12
| op1(e12,e12) = e11
| op1(e10,e13) = e10 ),
inference('REWRITE',[status(thm)],[16906,58340,34887,theory(equality)]) ).
cnf(62861,plain,
( op1(e13,e13) != e10
| op1(e13,e12) != e11
| op1(e13,e11) = e12
| op1(e12,e11) != e12
| op1(e12,e12) = e11
| op1(e10,e13) = e10 ),
inference('REWRITE',[status(thm)],[17395,58340,34887,theory(equality)]) ).
cnf(62876,plain,
op1(e13,e10) = e12,
inference('REWRITE',[status(thm)],[34886,34887,theory(equality)]) ).
cnf(62877,plain,
( op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 ),
inference('REWRITE',[status(thm)],[41,194,62876,theory(equality)]) ).
cnf(62878,plain,
( op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 ),
inference('REWRITE',[status(thm)],[43,196,62876,theory(equality)]) ).
cnf(62879,plain,
op1(e11,e10) != e12,
inference('REWRITE',[status(thm)],[101,62876,theory(equality)]) ).
cnf(63238,plain,
( op1(e11,e10) = e10
| op1(e11,e10) = e11 ),
inference('REWRITE',[status(thm)],[56288,62879]) ).
cnf(63907,plain,
op1(e13,e11) != e12,
inference('REWRITE',[status(thm)],[139,62876,theory(equality)]) ).
cnf(64229,plain,
( op1(e13,e13) != e10
| op1(e13,e12) != e11
| op1(e12,e11) != e12
| op1(e12,e12) = e11
| op1(e10,e13) = e10 ),
inference('REWRITE',[status(thm)],[62861,63907]) ).
cnf(64324,plain,
op1(e13,e12) != e12,
inference('REWRITE',[status(thm)],[140,62876,theory(equality)]) ).
cnf(64326,plain,
op1(e13,e13) != e12,
inference('REWRITE',[status(thm)],[141,62876,theory(equality)]) ).
cnf(65172,plain,
( op1(e13,e11) != e10
| op1(e12,e10) != e11
| op1(e12,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e12) != e13 ),
inference('REWRITE',[status(thm)],[14129,64326,196,62876,theory(equality)]) ).
cnf(65345,plain,
( h1(op1(e10,e11)) != op2(e20,e21)
| h1(op1(e10,e12)) != op2(e20,e22)
| h1(op1(e10,e13)) != op2(e20,e23)
| h1(op1(e11,e10)) != e20
| h1(op1(e11,e11)) != h2(e13)
| h1(op1(e11,e12)) != op2(e21,e22)
| h1(op1(e11,e13)) != op2(e21,e23)
| h1(op1(e12,e10)) != e21
| h1(op1(e12,e11)) != op2(e22,e21)
| h1(op1(e12,e12)) != h3(e13)
| h1(op1(e12,e13)) != op2(e22,e23)
| h1(op1(e13,e11)) != op2(e23,e21)
| h1(op1(e13,e12)) != op2(e23,e22)
| h1(op1(e13,e13)) != h4(e13) ),
inference('REWRITE',[status(thm)],[56240,51541,62876,theory(equality)]) ).
cnf(65575,plain,
( op1(e13,e13) != e10
| op1(e10,e13) != e11
| op1(e13,e12) = e10
| op1(e13,e12) != e13 ),
inference('REWRITE',[status(thm)],[59815,64326,62876,theory(equality)]) ).
cnf(65902,plain,
op1(e12,e10) = e11,
inference('REWRITE',[status(thm)],[34885,34886,theory(equality)]) ).
cnf(65904,plain,
op1(e11,e10) != e11,
inference('REWRITE',[status(thm)],[100,65902,theory(equality)]) ).
cnf(66107,plain,
op1(e11,e10) = e10,
inference('REWRITE',[status(thm)],[63238,65904]) ).
cnf(66108,plain,
op1(e11,e11) != e10,
inference('REWRITE',[status(thm)],[127,66107,theory(equality)]) ).
cnf(66109,plain,
( op1(e10,e11) = e10
| op1(e12,e11) = e10
| op1(e13,e11) = e10 ),
inference('REWRITE',[status(thm)],[26,66108]) ).
cnf(66116,plain,
op1(e12,e11) != e11,
inference('REWRITE',[status(thm)],[133,65902,theory(equality)]) ).
cnf(66118,plain,
op1(e12,e12) != e11,
inference('REWRITE',[status(thm)],[134,65902,theory(equality)]) ).
cnf(66119,plain,
( op1(e10,e12) = e11
| op1(e11,e12) = e11
| op1(e13,e12) = e11 ),
inference('REWRITE',[status(thm)],[36,66118]) ).
cnf(66308,plain,
( op1(e13,e13) != e10
| op1(e13,e12) != e11
| op1(e12,e11) != e12
| op1(e10,e13) = e10 ),
inference('REWRITE',[status(thm)],[64229,66118]) ).
cnf(66396,plain,
op1(e12,e13) != e11,
inference('REWRITE',[status(thm)],[135,65902,theory(equality)]) ).
cnf(66397,plain,
( op1(e12,e13) = e10
| op1(e12,e13) = e12
| op1(e12,e13) = e13 ),
inference('REWRITE',[status(thm)],[12,66396]) ).
cnf(66773,plain,
( op1(e13,e13) != e10
| op1(e12,e11) = e10
| op1(e12,e11) != e12
| op1(e10,e13) = e10 ),
inference('REWRITE',[status(thm)],[62818,66118,65902,theory(equality)]) ).
cnf(66878,plain,
( op1(e13,e11) != e10
| op1(e12,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e12) != e13 ),
inference('REWRITE',[status(thm)],[65172,65902,theory(equality)]) ).
cnf(66933,plain,
( h1(op1(e10,e11)) != op2(e20,e21)
| h1(op1(e10,e12)) != op2(e20,e22)
| h1(op1(e10,e13)) != op2(e20,e23)
| h1(op1(e11,e11)) != h2(e13)
| h1(op1(e11,e12)) != op2(e21,e22)
| h1(op1(e11,e13)) != op2(e21,e23)
| h1(op1(e12,e11)) != op2(e22,e21)
| h1(op1(e12,e12)) != h3(e13)
| h1(op1(e12,e13)) != op2(e22,e23)
| h1(op1(e13,e11)) != op2(e23,e21)
| h1(op1(e13,e12)) != op2(e23,e22)
| h1(op1(e13,e13)) != h4(e13) ),
inference('REWRITE',[status(thm)],[65345,55262,34891,66107,65902,theory(equality)]) ).
cnf(66976,plain,
( h4(e13) = e20
| h4(e13) = e21 ),
inference('REWRITE',[status(thm)],[64,52992,34909,17556,theory(equality)]) ).
cnf(66977,plain,
( op2(e23,e21) = e23
| op2(e23,e22) = e23 ),
inference('REWRITE',[status(thm)],[95,204,51542,17556,theory(equality)]) ).
cnf(66978,plain,
( op2(e21,e23) = e23
| op2(e22,e23) = e23 ),
inference('REWRITE',[status(thm)],[96,49046,17556]) ).
cnf(66979,plain,
( h3(e13) = e20
| h3(e13) = e23 ),
inference('REWRITE',[status(thm)],[59,55758,34905,17555,theory(equality)]) ).
cnf(66980,plain,
( op2(e22,e21) = e22
| op2(e22,e23) = e22 ),
inference('REWRITE',[status(thm)],[85,202,55263,17555,theory(equality)]) ).
cnf(66982,plain,
( h2(e13) = e22
| h2(e13) = e23 ),
inference('REWRITE',[status(thm)],[54,55474,34901,17554,theory(equality)]) ).
cnf(66984,plain,
( op2(e20,e21) = e21
| op2(e23,e21) = e21 ),
inference('REWRITE',[status(thm)],[76,55476,17554]) ).
cnf(66986,plain,
( op1(e13,e13) = e10
| op1(e13,e13) = e11 ),
inference('REWRITE',[status(thm)],[16,64326,224]) ).
cnf(66987,plain,
( op1(e13,e11) = e13
| op1(e13,e12) = e13 ),
inference('REWRITE',[status(thm)],[47,198,62876,224,theory(equality)]) ).
cnf(66988,plain,
( op1(e11,e13) = e13
| op1(e12,e13) = e13 ),
inference('REWRITE',[status(thm)],[48,60381,224]) ).
cnf(66989,plain,
( op1(e12,e12) = e10
| op1(e12,e12) = e13 ),
inference('REWRITE',[status(thm)],[11,66118,223]) ).
cnf(66990,plain,
( op1(e12,e11) = e12
| op1(e12,e13) = e12 ),
inference('REWRITE',[status(thm)],[37,196,65902,223,theory(equality)]) ).
cnf(66991,plain,
( op1(e10,e12) = e12
| op1(e11,e12) = e12 ),
inference('REWRITE',[status(thm)],[38,64324,223]) ).
cnf(66992,plain,
( op1(e11,e11) = e12
| op1(e11,e11) = e13 ),
inference('REWRITE',[status(thm)],[6,66108,222]) ).
cnf(66993,plain,
( op1(e11,e12) = e11
| op1(e11,e13) = e11 ),
inference('REWRITE',[status(thm)],[27,193,66107,222,theory(equality)]) ).
cnf(66994,plain,
( op1(e10,e11) = e11
| op1(e13,e11) = e11 ),
inference('REWRITE',[status(thm)],[28,66116,222]) ).
cnf(66995,plain,
( op1(e10,e11) = e10
| op1(e10,e12) = e10
| op1(e10,e13) = e10 ),
inference('REWRITE',[status(thm)],[17,221]) ).
cnf(66997,plain,
( h4(e13) = e20
| op2(e23,e21) != e21 ),
inference('PARAMODULATE',[status(thm)],[35369,66976,theory(equality)]) ).
cnf(67001,plain,
( h3(e13) = e20
| op2(e22,e23) != e23 ),
inference('PARAMODULATE',[status(thm)],[35855,66979,theory(equality)]) ).
cnf(67006,plain,
( h2(e13) = e22
| op2(e21,e23) != e23 ),
inference('PARAMODULATE',[status(thm)],[37246,66982,theory(equality)]) ).
cnf(67008,plain,
( h2(e13) = e22
| op2(e23,e21) != e23 ),
inference('PARAMODULATE',[status(thm)],[37243,66982,theory(equality)]) ).
cnf(67010,plain,
( h2(e13) = e22
| h2(e12) = op2(e23,e21) ),
inference('PARAMODULATE',[status(thm)],[39844,66982,theory(equality)]) ).
cnf(67017,plain,
( op2(e22,e21) = e22
| op2(e21,e23) = e23 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66978,66980,theory(equality)]),204]) ).
cnf(67026,plain,
( op1(e13,e13) = e10
| op1(e11,e13) != e11 ),
inference('PARAMODULATE',[status(thm)],[119,66986,theory(equality)]) ).
cnf(67027,plain,
( op1(e13,e13) = e10
| op1(e10,e13) != e11 ),
inference('PARAMODULATE',[status(thm)],[117,66986,theory(equality)]) ).
cnf(67028,plain,
( op1(e13,e11) = e13
| op1(e12,e12) != e13 ),
inference('PARAMODULATE',[status(thm)],[114,66987,theory(equality)]) ).
cnf(67030,plain,
( op1(e11,e13) = e13
| op1(e12,e12) != e13 ),
inference('PARAMODULATE',[status(thm)],[138,66988,theory(equality)]) ).
cnf(67038,plain,
( op1(e12,e11) = e12
| op1(e11,e13) = e13 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66988,66990,theory(equality)]),198]) ).
cnf(67052,plain,
( op2(e22,e21) = e23
| h3(e13) = e23
| op2(e22,e21) = e22 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66980,46207,theory(equality)]),204]) ).
cnf(67105,plain,
( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e21,e23) = e23 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66978,52993,theory(equality)]),204]) ).
cnf(67135,plain,
( op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e12,e13) != e13 ),
inference('PARAMODULATE',[status(thm)],[118,56289,theory(equality)]) ).
cnf(67156,plain,
( op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e10,e13) != e11 ),
inference('PARAMODULATE',[status(thm)],[117,62878,theory(equality)]) ).
cnf(67514,plain,
( op2(e23,e21) = e23
| op2(e23,e21) != e20
| op2(e22,e21) = e20 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[56239,66977,theory(equality)]),201,theory(equality)]) ).
cnf(67623,plain,
( op1(e13,e11) = e13
| op1(e13,e13) != e10
| op1(e10,e13) != e11 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[65575,66987,theory(equality)]),195,theory(equality)]) ).
cnf(67871,plain,
( op1(e13,e11) = e13
| op1(e13,e11) != e10
| op1(e12,e11) = e10 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66878,66987,theory(equality)]),195,theory(equality)]) ).
cnf(72103,plain,
( op1(e10,e11) = e10
| op1(e10,e12) = e10
| h1(op1(e10,e11)) != op2(e20,e21)
| h1(op1(e10,e12)) != op2(e20,e22)
| op2(e20,e23) != e20
| h1(op1(e11,e11)) != h2(e13)
| h1(op1(e11,e12)) != op2(e21,e22)
| h1(op1(e11,e13)) != op2(e21,e23)
| h1(op1(e12,e11)) != op2(e22,e21)
| h1(op1(e12,e12)) != h3(e13)
| h1(op1(e12,e13)) != op2(e22,e23)
| h1(op1(e13,e11)) != op2(e23,e21)
| h1(op1(e13,e12)) != op2(e23,e22)
| h1(op1(e13,e13)) != h4(e13) ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66933,66995,theory(equality)]),34891,theory(equality)]) ).
cnf(74136,plain,
( op2(e20,e21) = e21
| h4(e13) = e20 ),
inference('HYPERRESOLVE',[status(thm)],[66997,66984]) ).
cnf(74138,plain,
( op2(e21,e23) = e23
| h3(e13) = e20 ),
inference('HYPERRESOLVE',[status(thm)],[67001,66978]) ).
cnf(74357,plain,
( h2(e13) = e22
| op2(e20,e21) = e21
| h2(e12) = e21 ),
inference('PARAMODULATE',[status(thm)],[66984,67010,theory(equality)]) ).
cnf(74468,plain,
( op2(e22,e21) = e22
| h2(e13) = e22 ),
inference('HYPERRESOLVE',[status(thm)],[67006,67017]) ).
cnf(74481,plain,
( op1(e11,e12) = e11
| op1(e13,e13) = e10 ),
inference('HYPERRESOLVE',[status(thm)],[67026,66993]) ).
cnf(74484,plain,
( op1(e12,e12) = e10
| op1(e11,e13) = e13 ),
inference('HYPERRESOLVE',[status(thm)],[67030,66989]) ).
cnf(74494,plain,
( op1(e12,e11) = e12
| op1(e11,e12) = e11 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66993,67038,theory(equality)]),197]) ).
cnf(74638,plain,
( h3(e13) = e20
| h2(e13) = e22 ),
inference('HYPERRESOLVE',[status(thm)],[67006,74138]) ).
cnf(74743,plain,
( h2(e13) = e22
| h3(e13) != e20
| op2(e23,e22) != e23 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[56196,74468,theory(equality)]),200,theory(equality)]) ).
cnf(74770,plain,
( h2(e13) = e22
| op2(e22,e21) != e20 ),
inference('PARAMODULATE',[status(thm)],[35854,74638,theory(equality)]) ).
cnf(75164,plain,
( op1(e11,e12) = e11
| op1(e10,e13) != e10 ),
inference('PARAMODULATE',[status(thm)],[117,74481,theory(equality)]) ).
cnf(75555,plain,
( op1(e12,e12) = e10
| op1(e11,e12) = e11 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66993,74484,theory(equality)]),197]) ).
cnf(75615,plain,
( op1(e11,e12) = e11
| op1(e12,e11) = e10
| op1(e10,e13) = e10 ),
inference('HYPERRESOLVE',[status(thm)],[66773,74494,74481]) ).
cnf(75617,plain,
( op1(e11,e12) = e11
| op1(e10,e12) = e11
| op1(e10,e13) = e10 ),
inference('HYPERRESOLVE',[status(thm)],[66308,74494,74481,66119]) ).
cnf(76001,plain,
( op1(e11,e12) = e11
| op1(e12,e11) != e10 ),
inference('PARAMODULATE',[status(thm)],[136,75555,theory(equality)]) ).
cnf(76175,plain,
( h3(e13) = e23
| op2(e22,e21) = e22
| h4(e13) != e20
| op2(e22,e23) != e22 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[56044,67052,theory(equality)]),201,theory(equality)]) ).
cnf(76915,plain,
( op1(e12,e13) = e10
| op1(e12,e13) = e12
| op1(e11,e11) = e13
| op1(e11,e12) = e13 ),
inference('HYPERRESOLVE',[status(thm)],[67135,66397]) ).
cnf(77437,plain,
( op2(e20,e21) = e20
| op2(e22,e21) = e20 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[67514,55475,theory(equality)]),201,theory(equality)]) ).
cnf(77442,plain,
( op2(e20,e21) = e20
| h2(e13) = e22 ),
inference('HYPERRESOLVE',[status(thm)],[74770,77437]) ).
cnf(77446,plain,
( op2(e20,e21) = e20
| h3(e13) = e23 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[67052,77437,theory(equality)]),200,201]) ).
cnf(77453,plain,
( h3(e13) = e23
| h4(e13) = e20 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[74136,77446,theory(equality)]),199]) ).
cnf(77693,plain,
( h2(e13) = e22
| h2(e12) = e21 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[74357,77442,theory(equality)]),199]) ).
cnf(77736,plain,
( h2(e12) = e21
| op2(e22,e21) = h2(e12) ),
inference('PARAMODULATE',[status(thm)],[39844,77693,theory(equality)]) ).
cnf(78031,plain,
( h2(e12) = e21
| op2(e20,e21) = e20
| h2(e12) = e20 ),
inference('PARAMODULATE',[status(thm)],[77437,77736,theory(equality)]) ).
cnf(78101,plain,
( op1(e10,e11) = e10
| op1(e12,e11) = e10 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[67871,66109,theory(equality)]),195,theory(equality)]) ).
cnf(78445,plain,
( h2(e13) = e22
| op2(e23,e21) = e23 ),
inference('HYPERRESOLVE',[status(thm)],[74743,74638,66977]) ).
cnf(78447,plain,
h2(e13) = e22,
inference('HYPERRESOLVE',[status(thm)],[67008,78445]) ).
cnf(78449,plain,
op2(e20,e21) != e22,
inference('REWRITE',[status(thm)],[37241,78447,theory(equality)]) ).
cnf(78450,plain,
( op2(e20,e22) = e22
| op2(e20,e23) = e22 ),
inference('REWRITE',[status(thm)],[44950,78449]) ).
cnf(78787,plain,
op2(e22,e21) != e22,
inference('REWRITE',[status(thm)],[37242,78447,theory(equality)]) ).
cnf(78789,plain,
op2(e22,e23) = e22,
inference('REWRITE',[status(thm)],[66980,78787]) ).
cnf(78790,plain,
op2(e20,e23) != e22,
inference('REWRITE',[status(thm)],[164,78789,theory(equality)]) ).
cnf(78791,plain,
( op2(e20,e23) = e20
| op2(e20,e23) = e21 ),
inference('REWRITE',[status(thm)],[49047,78790]) ).
cnf(78792,plain,
( op2(e21,e23) = e22
| op2(e21,e23) = e23 ),
inference('REWRITE',[status(thm)],[67105,78790]) ).
cnf(78844,plain,
op2(e20,e22) = e22,
inference('REWRITE',[status(thm)],[78450,78790]) ).
cnf(78845,plain,
op2(e21,e22) != e22,
inference('REWRITE',[status(thm)],[157,78844,theory(equality)]) ).
cnf(78846,plain,
( op2(e21,e22) = e21
| op2(e21,e22) = e23 ),
inference('REWRITE',[status(thm)],[55469,78845]) ).
cnf(78896,plain,
op2(e21,e23) != e22,
inference('REWRITE',[status(thm)],[166,78789,theory(equality)]) ).
cnf(78897,plain,
op2(e21,e23) = e23,
inference('REWRITE',[status(thm)],[78792,78896]) ).
cnf(78898,plain,
op2(e21,e22) != e23,
inference('REWRITE',[status(thm)],[180,78897,theory(equality)]) ).
cnf(78918,plain,
op2(e21,e22) = e21,
inference('REWRITE',[status(thm)],[78846,78898]) ).
cnf(78975,plain,
( h3(e13) = e23
| h4(e13) != e20 ),
inference('REWRITE',[status(thm)],[76175,78789,78787,theory(equality)]) ).
cnf(78999,plain,
op2(e22,e21) = h2(e12),
inference('REWRITE',[status(thm)],[39844,78447,theory(equality)]) ).
cnf(79003,plain,
h2(e12) != e21,
inference('REWRITE',[status(thm)],[55476,78999,theory(equality)]) ).
cnf(79008,plain,
( op2(e20,e21) = e20
| h2(e12) = e20 ),
inference('REWRITE',[status(thm)],[78031,79003]) ).
cnf(79056,plain,
( op1(e10,e11) = e10
| op1(e10,e12) = e10
| h1(op1(e10,e11)) != op2(e20,e21)
| h1(op1(e10,e12)) != e22
| op2(e20,e23) != e20
| h1(op1(e11,e11)) != e22
| h1(op1(e11,e12)) != e21
| h1(op1(e11,e13)) != e23
| h1(op1(e12,e11)) != h2(e12)
| h1(op1(e12,e12)) != h3(e13)
| h1(op1(e12,e13)) != e22
| h1(op1(e13,e11)) != op2(e23,e21)
| h1(op1(e13,e12)) != op2(e23,e22)
| h1(op1(e13,e13)) != h4(e13) ),
inference('REWRITE',[status(thm)],[72103,78789,78999,78897,78918,78844,78447,theory(equality)]) ).
cnf(79473,plain,
h3(e13) = e23,
inference('HYPERRESOLVE',[status(thm)],[78975,77453]) ).
cnf(79475,plain,
op2(e23,e22) != e23,
inference('REWRITE',[status(thm)],[35852,79473,theory(equality)]) ).
cnf(79476,plain,
op2(e23,e21) = e23,
inference('REWRITE',[status(thm)],[66977,79475]) ).
cnf(79477,plain,
( op2(e23,e22) = e20
| h4(e13) = e20 ),
inference('REWRITE',[status(thm)],[51543,201,79476,theory(equality)]) ).
cnf(79478,plain,
op2(e20,e21) = e21,
inference('REWRITE',[status(thm)],[66984,203,79476,theory(equality)]) ).
cnf(79479,plain,
op2(e20,e23) != e21,
inference('REWRITE',[status(thm)],[173,79478,theory(equality)]) ).
cnf(79480,plain,
op2(e20,e23) = e20,
inference('REWRITE',[status(thm)],[78791,79479]) ).
cnf(79481,plain,
h4(e13) != e20,
inference('REWRITE',[status(thm)],[35366,79480,theory(equality)]) ).
cnf(79482,plain,
h4(e13) = e21,
inference('REWRITE',[status(thm)],[66976,79481]) ).
cnf(79486,plain,
op2(e23,e22) = e20,
inference('REWRITE',[status(thm)],[79477,79481]) ).
cnf(79487,plain,
h2(e12) = e20,
inference('REWRITE',[status(thm)],[79008,199,79478,theory(equality)]) ).
cnf(79495,plain,
( op1(e10,e11) = e10
| op1(e10,e12) = e10
| h1(op1(e10,e11)) != e21
| h1(op1(e10,e12)) != e22
| h1(op1(e11,e11)) != e22
| h1(op1(e11,e12)) != e21
| h1(op1(e11,e13)) != e23
| h1(op1(e12,e11)) != e20
| h1(op1(e12,e12)) != e23
| h1(op1(e12,e13)) != e22
| h1(op1(e13,e11)) != e23
| h1(op1(e13,e12)) != e20
| h1(op1(e13,e13)) != e21 ),
inference('REWRITE',[status(thm)],[79056,79482,79486,79476,79487,79480,79478,79473,theory(equality)]) ).
cnf(79798,plain,
( op1(e11,e12) = e11
| op1(e12,e11) = e10 ),
inference('HYPERRESOLVE',[status(thm)],[75164,75615]) ).
cnf(79802,plain,
( op1(e12,e11) = e10
| op1(e10,e12) = e12 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66991,79798,theory(equality)]),196]) ).
cnf(79805,plain,
( op1(e10,e12) = e12
| op1(e11,e12) = e11 ),
inference('HYPERRESOLVE',[status(thm)],[76001,79802]) ).
cnf(79813,plain,
op1(e10,e12) = e12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[66991,79805,theory(equality)]),196]) ).
cnf(79867,plain,
op1(e10,e13) != e12,
inference('REWRITE',[status(thm)],[126,79813,theory(equality)]) ).
cnf(79868,plain,
( op1(e10,e13) = e10
| op1(e10,e13) = e11 ),
inference('REWRITE',[status(thm)],[60382,79867]) ).
cnf(79953,plain,
( op1(e11,e12) = e11
| op1(e10,e13) = e10 ),
inference('REWRITE',[status(thm)],[75617,196,79813,theory(equality)]) ).
cnf(79968,plain,
( op1(e10,e11) = e10
| h1(op1(e10,e11)) != e21
| h1(op1(e11,e11)) != e22
| h1(op1(e11,e12)) != e21
| h1(op1(e11,e13)) != e23
| h1(op1(e12,e11)) != e20
| h1(op1(e12,e12)) != e23
| h1(op1(e12,e13)) != e22
| h1(op1(e13,e11)) != e23
| h1(op1(e13,e12)) != e20
| h1(op1(e13,e13)) != e21 ),
inference('REWRITE',[status(thm)],[79495,51541,194,79813,theory(equality)]) ).
cnf(79992,plain,
( op1(e10,e13) = e10
| op1(e13,e13) = e10 ),
inference('HYPERRESOLVE',[status(thm)],[67027,79868]) ).
cnf(79995,plain,
( op1(e10,e13) = e10
| op1(e13,e11) = e11
| op1(e13,e12) = e11 ),
inference('HYPERRESOLVE',[status(thm)],[67156,79868]) ).
cnf(80022,plain,
( op1(e10,e13) = e10
| op1(e13,e11) = e13 ),
inference('HYPERRESOLVE',[status(thm)],[67623,79992,79868]) ).
cnf(80078,plain,
op1(e11,e12) = e11,
inference('HYPERRESOLVE',[status(thm)],[75164,79953]) ).
cnf(80079,plain,
op1(e13,e12) != e11,
inference('REWRITE',[status(thm)],[113,80078,theory(equality)]) ).
cnf(80112,plain,
( op1(e10,e13) = e10
| op1(e13,e11) = e11 ),
inference('REWRITE',[status(thm)],[79995,80079]) ).
cnf(80253,plain,
( op1(e12,e13) = e10
| op1(e12,e13) = e12
| op1(e11,e11) = e13 ),
inference('REWRITE',[status(thm)],[76915,197,80078,theory(equality)]) ).
cnf(80266,plain,
( op1(e10,e11) = e10
| h1(op1(e10,e11)) != e21
| h1(op1(e11,e11)) != e22
| h1(op1(e11,e13)) != e23
| h1(op1(e12,e11)) != e20
| h1(op1(e12,e12)) != e23
| h1(op1(e12,e13)) != e22
| h1(op1(e13,e11)) != e23
| h1(op1(e13,e12)) != e20
| h1(op1(e13,e13)) != e21 ),
inference('REWRITE',[status(thm)],[79968,55262,80078,theory(equality)]) ).
cnf(80299,plain,
op1(e10,e13) = e10,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[80112,80022,theory(equality)]),197]) ).
cnf(80300,plain,
op1(e12,e13) != e10,
inference('REWRITE',[status(thm)],[116,80299,theory(equality)]) ).
cnf(80308,plain,
( op1(e12,e13) = e12
| op1(e11,e11) = e13 ),
inference('REWRITE',[status(thm)],[80253,80300]) ).
cnf(80309,plain,
op1(e13,e13) != e10,
inference('REWRITE',[status(thm)],[117,80299,theory(equality)]) ).
cnf(80310,plain,
( op1(e13,e11) = e10
| op1(e13,e12) = e10 ),
inference('REWRITE',[status(thm)],[62877,80309]) ).
cnf(80311,plain,
op1(e13,e13) = e11,
inference('REWRITE',[status(thm)],[66986,80309]) ).
cnf(80312,plain,
op1(e13,e11) != e11,
inference('REWRITE',[status(thm)],[143,80311,theory(equality)]) ).
cnf(80314,plain,
op1(e10,e11) = e11,
inference('REWRITE',[status(thm)],[66994,80312]) ).
cnf(80315,plain,
op1(e12,e11) = e10,
inference('REWRITE',[status(thm)],[78101,193,80314,theory(equality)]) ).
cnf(80316,plain,
op1(e13,e11) != e10,
inference('REWRITE',[status(thm)],[108,80315,theory(equality)]) ).
cnf(80317,plain,
op1(e13,e12) = e10,
inference('REWRITE',[status(thm)],[80310,80316]) ).
cnf(80318,plain,
op1(e12,e12) != e10,
inference('REWRITE',[status(thm)],[114,80317,theory(equality)]) ).
cnf(80319,plain,
op1(e12,e12) = e13,
inference('REWRITE',[status(thm)],[66989,80318]) ).
cnf(80320,plain,
op1(e12,e13) != e13,
inference('REWRITE',[status(thm)],[138,80319,theory(equality)]) ).
cnf(80321,plain,
op1(e11,e13) = e13,
inference('REWRITE',[status(thm)],[66988,80320]) ).
cnf(80322,plain,
op1(e11,e11) != e13,
inference('REWRITE',[status(thm)],[131,80321,theory(equality)]) ).
cnf(80323,plain,
op1(e11,e11) = e12,
inference('REWRITE',[status(thm)],[66992,80322]) ).
cnf(80324,plain,
op1(e12,e13) = e12,
inference('REWRITE',[status(thm)],[80308,80322]) ).
cnf(80325,plain,
op1(e13,e11) = e13,
inference('REWRITE',[status(thm)],[67028,80319,theory(equality)]) ).
cnf(80326,plain,
$false,
inference('REWRITE',[status(thm)],[80266,80317,80325,80324,80319,34891,80315,34897,80321,51541,80323,55262,193,80314,80311,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ALG124+1 : TPTP v8.1.0. Released v2.7.0.
% 0.11/0.13 % Command : run-snark %s %d
% 0.12/0.34 % Computer : n022.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 : 600
% 0.12/0.34 % DateTime : Wed Jun 8 20:48:05 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 *
% 0.19/0.46 *
% 0.19/0.47 #<PACKAGE "SNARK-USER">
% 0.19/0.47 *
% 0.19/0.47 SNARK-TPTP-OPTIONS
% 0.19/0.47 *
% 0.19/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.47 (USE-FACTORING :POS)
% 0.19/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.47 *
% 0.19/0.47 "."
% 0.19/0.47 *
% 0.19/0.47 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-08T20:48:05
% 0.19/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n022.cluster.edu at 2022-06-08T20:48:05
% 186.72/186.98
% 186.72/186.98
% 186.72/186.98 #||
% 186.72/186.98 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 186.72/186.98 % SZS output start Refutation
% See solution above
% 186.77/187.03 ||#
% 186.77/187.03
% 186.77/187.03 ; Summary of computation:
% 186.77/187.03 ; 195723 formulas have been input or derived (from 3751 formulas).
% 186.77/187.03 ; 80326 (41%) were retained. Of these,
% 186.77/187.03 ; 80249 (100%) were simplified or subsumed later,
% 186.77/187.03 ; 77 ( 0%) are still being kept.
% 186.77/187.03 ;
% 186.77/187.03 ; Run time in seconds excluding printing time:
% 186.77/187.03 ; 0.060 0% Read assertion file (1 call)
% 186.77/187.03 ; 1.646 1% Assert (18 calls)
% 186.77/187.03 ; 11.837 6% Process new row (194,220 calls)
% 186.77/187.03 ; 2.503 1% Resolution (7,500 calls)
% 186.77/187.03 ; 2.535 1% Paramodulation (3,750 calls)
% 186.77/187.03 ; 0.001 0% Factoring (217 calls)
% 186.77/187.03 ; 0.282 0% Condensing (125,903 calls)
% 186.77/187.03 ; 88.894 48% Forward subsumption (125,903 calls)
% 186.77/187.03 ; 32.074 17% Backward subsumption (79,663 calls)
% 186.77/187.03 ; 22.999 12% Clause clause subsumption (6,471,876 calls)
% 186.77/187.03 ; 11.867 6% Forward simplification (184,829 calls)
% 186.77/187.03 ; 10.324 6% Backward simplification (79,963 calls)
% 186.77/187.03 ; 0.526 0% Ordering (317,754 calls)
% 186.77/187.03 ; 0.000 0% Sortal reasoning (32 calls)
% 186.77/187.03 ; 0.059 0% Purity testing (1 call)
% 186.77/187.03 ; 0.862 0% Other
% 186.77/187.03 ; 186.469 Total
% 186.77/187.03 ; 186.563 Real time
% 186.77/187.03 ;
% 186.77/187.03 ; Term-hash-array has 867 terms in all.
% 186.77/187.03 ; Feature-vector-row-index has 0 entries (34,728 at peak, 79,663 added, 79,663 deleted).
% 186.77/187.03 ; Feature-vector-row-index has 1 node (122,778 at peak, 496,310 added, 496,309 deleted).
% 186.77/187.03 ; Retrieved 4,701,322 possibly forward subsuming rows in 125,903 calls.
% 186.77/187.03 ; Retrieved 3,138,265 possibly backward subsumed rows in 79,663 calls.
% 186.77/187.03 ; Path-index has 132 entries (650 at peak, 1,930 added, 1,798 deleted).
% 186.77/187.03 ; Path-index has 166 nodes (274 at peak, 860 added, 694 deleted).
% 186.77/187.03 ; Trie-index has 132 entries (650 at peak, 1,930 added, 1,798 deleted).
% 186.77/187.03 ; Trie-index has 217 nodes (1,245 at peak, 4,376 added, 4,159 deleted).
% 186.77/187.03 ; Retrieved 173,905 generalization terms in 2,499,884 calls.
% 186.77/187.03 ; Retrieved 299 instance terms in 299 calls.
% 186.77/187.03 ; Retrieved 58,782 unifiable terms in 75,545 calls.
% 186.77/187.03 ;
% 186.77/187.03 ; The agenda of backward simplifiable rows to process has 196 entries:
% 186.77/187.03 ; 196 with value 0
% 186.77/187.03 ; The agenda of rows to process has 74 entries:
% 186.77/187.03 ; 2 with value 15 5 with value 26 4 with value 39
% 186.77/187.03 ; 8 with value 18 3 with value 29 2 with value 40
% 186.77/187.03 ; 10 with value 22 12 with value 32 10 with value 43
% 186.77/187.03 ; 1 with value 23 8 with value 36 3 with value 46
% 186.77/187.03 ; 6 with value 25
% 186.77/187.03 ; The agenda of input rows to give has 6 entries:
% 186.77/187.03 ; 6 with value 7
% 186.77/187.03 ; The agenda of rows to give has 4 entries:
% 186.77/187.03 ; 1 with value (4 8) 2 with value (4 9) 1 with value (4 11)
% 186.77/187.03 Evaluation took:
% 186.77/187.03 186.563 seconds of real time
% 186.77/187.03 174.65584 seconds of user run time
% 186.77/187.03 11.869111 seconds of system run time
% 186.77/187.03 [Run times include 22.099 seconds GC run time.]
% 186.77/187.03 0 calls to %EVAL
% 186.77/187.03 0 page faults and
% 186.77/187.03 20,378,135,264 bytes consed.
% 186.77/187.03 :PROOF-FOUND
% 186.77/187.03 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-08T20:51:11
% 186.77/187.03 :PROOF-FOUND
% 186.77/187.03 *
%------------------------------------------------------------------------------