%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ALG049+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:44 EDT 2022
% Result : Theorem 266.88s 267.07s
% Output : Refutation 266.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 215
% Syntax : Number of clauses : 596 ( 389 unt; 177 nHn; 596 RR)
% Number of literals : 1455 (1454 equ; 656 neg)
% Maximal clause size : 30 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 12 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
| op1(e10,e13) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(8,axiom,
( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13
| op1(e11,e12) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(9,axiom,
( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13
| op1(e11,e13) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(10,axiom,
( op1(e11,e14) = e10
| op1(e11,e14) = e11
| op1(e11,e14) = e12
| op1(e11,e14) = e13
| op1(e11,e14) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(12,axiom,
( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13
| op1(e12,e11) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(16,axiom,
( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13
| op1(e13,e10) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(27,axiom,
op1(e10,unit1) = e10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(28,axiom,
op1(unit1,e11) = e11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(29,axiom,
op1(e11,unit1) = e11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(30,axiom,
op1(unit1,e12) = e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(33,axiom,
op1(e13,unit1) = e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(35,axiom,
op1(e14,unit1) = e14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(36,axiom,
( unit1 = e10
| unit1 = e11
| unit1 = e12
| unit1 = e13
| unit1 = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(45,axiom,
( op1(e10,e10) = e14
| op1(e10,e11) = e14
| op1(e10,e12) = e14
| op1(e10,e13) = e14
| op1(e10,e14) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(57,axiom,
( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10
| op1(e12,e14) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(59,axiom,
( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11
| op1(e12,e14) = e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(67,axiom,
( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10
| op1(e13,e14) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(69,axiom,
( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11
| op1(e13,e14) = e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(71,axiom,
( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12
| op1(e13,e14) = e12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(72,axiom,
( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12
| op1(e14,e13) = e12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(75,axiom,
( op1(e13,e10) = e14
| op1(e13,e11) = e14
| op1(e13,e12) = e14
| op1(e13,e13) = e14
| op1(e13,e14) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(77,axiom,
( op1(e14,e10) = e10
| op1(e14,e11) = e10
| op1(e14,e12) = e10
| op1(e14,e13) = e10
| op1(e14,e14) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(80,axiom,
( op1(e10,e14) = e11
| op1(e11,e14) = e11
| op1(e12,e14) = e11
| op1(e13,e14) = e11
| op1(e14,e14) = e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(81,axiom,
( op1(e14,e10) = e12
| op1(e14,e11) = e12
| op1(e14,e12) = e12
| op1(e14,e13) = e12
| op1(e14,e14) = e12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(83,axiom,
( op1(e14,e10) = e13
| op1(e14,e11) = e13
| op1(e14,e12) = e13
| op1(e14,e13) = e13
| op1(e14,e14) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(90,axiom,
( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23
| op2(e20,e23) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(91,axiom,
( op2(e20,e24) = e20
| op2(e20,e24) = e21
| op2(e20,e24) = e22
| op2(e20,e24) = e23
| op2(e20,e24) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(94,axiom,
( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23
| op2(e21,e22) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(95,axiom,
( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23
| op2(e21,e23) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(96,axiom,
( op2(e21,e24) = e20
| op2(e21,e24) = e21
| op2(e21,e24) = e22
| op2(e21,e24) = e23
| op2(e21,e24) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(98,axiom,
( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23
| op2(e22,e21) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(102,axiom,
( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23
| op2(e23,e20) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(105,axiom,
( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23
| op2(e23,e23) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(111,axiom,
( op2(e24,e24) = e20
| op2(e24,e24) = e21
| op2(e24,e24) = e22
| op2(e24,e24) = e23
| op2(e24,e24) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(113,axiom,
op2(e20,unit2) = e20,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(114,axiom,
op2(unit2,e21) = e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(115,axiom,
op2(e21,unit2) = e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(116,axiom,
op2(unit2,e22) = e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(119,axiom,
op2(e23,unit2) = e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(121,axiom,
op2(e24,unit2) = e24,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(122,axiom,
( unit2 = e20
| unit2 = e21
| unit2 = e22
| unit2 = e23
| unit2 = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(123,axiom,
( op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e22) = e20
| op2(e20,e23) = e20
| op2(e20,e24) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(143,axiom,
( op2(e22,e20) = e20
| op2(e22,e21) = e20
| op2(e22,e22) = e20
| op2(e22,e23) = e20
| op2(e22,e24) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(144,axiom,
( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e22,e22) = e20
| op2(e23,e22) = e20
| op2(e24,e22) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(145,axiom,
( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21
| op2(e22,e24) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(155,axiom,
( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21
| op2(e23,e24) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(157,axiom,
( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22
| op2(e23,e24) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(161,axiom,
( op2(e23,e20) = e24
| op2(e23,e21) = e24
| op2(e23,e22) = e24
| op2(e23,e23) = e24
| op2(e23,e24) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(163,axiom,
( op2(e24,e20) = e20
| op2(e24,e21) = e20
| op2(e24,e22) = e20
| op2(e24,e23) = e20
| op2(e24,e24) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(164,axiom,
( op2(e20,e24) = e20
| op2(e21,e24) = e20
| op2(e22,e24) = e20
| op2(e23,e24) = e20
| op2(e24,e24) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(167,axiom,
( op2(e24,e20) = e22
| op2(e24,e21) = e22
| op2(e24,e22) = e22
| op2(e24,e23) = e22
| op2(e24,e24) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(169,axiom,
( op2(e24,e20) = e23
| op2(e24,e21) = e23
| op2(e24,e22) = e23
| op2(e24,e23) = e23
| op2(e24,e24) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(174,axiom,
op1(e10,e10) != op1(e12,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(175,axiom,
op1(e10,e10) != op1(e13,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(176,axiom,
op1(e10,e10) != op1(e14,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(177,axiom,
op1(e11,e10) != op1(e12,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(178,axiom,
op1(e11,e10) != op1(e13,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(180,axiom,
op1(e12,e10) != op1(e13,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(181,axiom,
op1(e12,e10) != op1(e14,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(182,axiom,
op1(e13,e10) != op1(e14,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(184,axiom,
op1(e10,e11) != op1(e12,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(185,axiom,
op1(e10,e11) != op1(e13,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(187,axiom,
op1(e11,e11) != op1(e12,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(188,axiom,
op1(e11,e11) != op1(e13,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(189,axiom,
op1(e11,e11) != op1(e14,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(190,axiom,
op1(e12,e11) != op1(e13,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(192,axiom,
op1(e13,e11) != op1(e14,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(193,axiom,
op1(e10,e12) != op1(e11,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(195,axiom,
op1(e10,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(198,axiom,
op1(e11,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(199,axiom,
op1(e11,e12) != op1(e14,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(200,axiom,
op1(e12,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(201,axiom,
op1(e12,e12) != op1(e14,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(202,axiom,
op1(e13,e12) != op1(e14,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(203,axiom,
op1(e10,e13) != op1(e11,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(204,axiom,
op1(e10,e13) != op1(e12,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(206,axiom,
op1(e10,e13) != op1(e14,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(209,axiom,
op1(e11,e13) != op1(e14,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(210,axiom,
op1(e12,e13) != op1(e13,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(212,axiom,
op1(e13,e13) != op1(e14,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(213,axiom,
op1(e10,e14) != op1(e11,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(215,axiom,
op1(e10,e14) != op1(e13,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(217,axiom,
op1(e11,e14) != op1(e12,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(220,axiom,
op1(e12,e14) != op1(e13,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(221,axiom,
op1(e12,e14) != op1(e14,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(225,axiom,
op1(e10,e10) != op1(e10,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(235,axiom,
op1(e11,e10) != op1(e11,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(236,axiom,
op1(e11,e10) != op1(e11,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(237,axiom,
op1(e11,e11) != op1(e11,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(238,axiom,
op1(e11,e11) != op1(e11,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(239,axiom,
op1(e11,e11) != op1(e11,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(240,axiom,
op1(e11,e12) != op1(e11,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(243,axiom,
op1(e12,e10) != op1(e12,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(249,axiom,
op1(e12,e11) != op1(e12,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(271,axiom,
op1(e14,e12) != op1(e14,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(274,axiom,
op2(e20,e20) != op2(e22,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(275,axiom,
op2(e20,e20) != op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(276,axiom,
op2(e20,e20) != op2(e24,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(277,axiom,
op2(e21,e20) != op2(e22,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(278,axiom,
op2(e21,e20) != op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(280,axiom,
op2(e22,e20) != op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(281,axiom,
op2(e22,e20) != op2(e24,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(282,axiom,
op2(e23,e20) != op2(e24,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(283,axiom,
op2(e20,e21) != op2(e21,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(284,axiom,
op2(e20,e21) != op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(285,axiom,
op2(e20,e21) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(287,axiom,
op2(e21,e21) != op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(289,axiom,
op2(e21,e21) != op2(e24,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(290,axiom,
op2(e22,e21) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(292,axiom,
op2(e23,e21) != op2(e24,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(293,axiom,
op2(e20,e22) != op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(298,axiom,
op2(e21,e22) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(299,axiom,
op2(e21,e22) != op2(e24,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(300,axiom,
op2(e22,e22) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(301,axiom,
op2(e22,e22) != op2(e24,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(302,axiom,
op2(e23,e22) != op2(e24,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(304,axiom,
op2(e20,e23) != op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(306,axiom,
op2(e20,e23) != op2(e24,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(309,axiom,
op2(e21,e23) != op2(e24,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(310,axiom,
op2(e22,e23) != op2(e23,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(312,axiom,
op2(e23,e23) != op2(e24,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(313,axiom,
op2(e20,e24) != op2(e21,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(314,axiom,
op2(e20,e24) != op2(e22,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(315,axiom,
op2(e20,e24) != op2(e23,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(317,axiom,
op2(e21,e24) != op2(e22,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(319,axiom,
op2(e21,e24) != op2(e24,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(320,axiom,
op2(e22,e24) != op2(e23,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(321,axiom,
op2(e22,e24) != op2(e24,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(324,axiom,
op2(e20,e20) != op2(e20,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(325,axiom,
op2(e20,e20) != op2(e20,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(326,axiom,
op2(e20,e20) != op2(e20,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(332,axiom,
op2(e20,e23) != op2(e20,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(335,axiom,
op2(e21,e20) != op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(336,axiom,
op2(e21,e20) != op2(e21,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(337,axiom,
op2(e21,e21) != op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(338,axiom,
op2(e21,e21) != op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(339,axiom,
op2(e21,e21) != op2(e21,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(340,axiom,
op2(e21,e22) != op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(342,axiom,
op2(e21,e23) != op2(e21,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(343,axiom,
op2(e22,e20) != op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(349,axiom,
op2(e22,e21) != op2(e22,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(354,axiom,
op2(e23,e20) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(355,axiom,
op2(e23,e20) != op2(e23,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(371,axiom,
op2(e24,e22) != op2(e24,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(373,axiom,
e10 != e11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(374,axiom,
e10 != e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(375,axiom,
e10 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(376,axiom,
e10 != e14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(377,axiom,
e11 != e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(378,axiom,
e11 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(379,axiom,
e11 != e14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(380,axiom,
e12 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(381,axiom,
e12 != e14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(382,axiom,
e13 != e14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
cnf(383,axiom,
e20 != e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(384,axiom,
e20 != e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(385,axiom,
e20 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(387,axiom,
e21 != e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(388,axiom,
e21 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(389,axiom,
e21 != e24,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(390,axiom,
e22 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(391,axiom,
e22 != e24,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(392,axiom,
e23 != e24,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(422,axiom,
( op1(e11,e11) != e10
| op1(e11,e10) = e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(426,axiom,
( op1(e12,e12) != e10
| op1(e12,e10) = e12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(433,axiom,
( op1(e13,e13) != e14
| op1(e13,e14) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(434,axiom,
( op1(e14,e14) != e10
| op1(e14,e10) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(436,axiom,
( op1(e14,e14) != e12
| op1(e14,e12) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(442,axiom,
( op2(e21,e21) != e20
| op2(e21,e20) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(446,axiom,
( op2(e22,e22) != e20
| op2(e22,e20) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(452,axiom,
( op2(e23,e23) != e22
| op2(e23,e22) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(453,axiom,
( op2(e23,e23) != e24
| op2(e23,e24) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(454,axiom,
( op2(e24,e24) != e20
| op2(e24,e20) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(456,axiom,
( op2(e24,e24) != e22
| op2(e24,e22) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(458,axiom,
e10 = op1(op1(e14,e12),op1(e14,e12)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(459,axiom,
op1(e14,e12) = e11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(460,axiom,
op1(e12,e14) = e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(461,axiom,
e20 = op2(op2(e24,e22),op2(e24,e22)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
cnf(462,axiom,
op2(e24,e22) = e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
cnf(463,axiom,
op2(e22,e24) = e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
cnf(467,axiom,
h1(e11) = op2(e21,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
cnf(468,axiom,
h1(e13) = op2(e20,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
cnf(472,axiom,
h2(e11) = op2(e22,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
cnf(473,axiom,
h2(e13) = op2(e20,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
cnf(477,axiom,
h3(e11) = op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
cnf(478,axiom,
h3(e13) = op2(e20,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
cnf(482,axiom,
h4(e11) = op2(e24,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
cnf(483,axiom,
h4(e13) = op2(e20,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
cnf(495,axiom,
h6(e11) = op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
cnf(496,axiom,
h6(e13) = op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
cnf(500,axiom,
h7(e11) = op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
cnf(501,axiom,
h7(e13) = op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
cnf(502,axiom,
h8(e12) = e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
cnf(503,axiom,
h8(e14) = e24,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
cnf(504,axiom,
h8(e10) = op2(op2(e24,e21),op2(e24,e21)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
cnf(505,axiom,
h8(e11) = op2(e24,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
cnf(506,axiom,
h8(e13) = op2(e21,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
cnf(519,axiom,
h10(e11) = op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
cnf(520,plain,
h10(e11) = h6(e13),
inference('REWRITE',[status(thm)],[519,496,theory(equality)]) ).
cnf(521,axiom,
h10(e13) = op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
cnf(522,plain,
h10(e13) = h6(e11),
inference('REWRITE',[status(thm)],[521,495,theory(equality)]) ).
cnf(526,axiom,
h11(e11) = op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
cnf(527,axiom,
h11(e13) = op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
cnf(530,axiom,
h12(e10) = op2(op2(e24,e22),op2(e24,e22)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax27) ).
cnf(531,plain,
h12(e10) = op2(e21,e21),
inference('REWRITE',[status(thm)],[530,462,theory(equality)]) ).
cnf(540,axiom,
h13(e11) = op2(e20,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
cnf(541,plain,
h13(e11) = h3(e13),
inference('REWRITE',[status(thm)],[540,478,theory(equality)]) ).
cnf(542,axiom,
h13(e13) = op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
cnf(543,plain,
h13(e13) = h3(e11),
inference('REWRITE',[status(thm)],[542,477,theory(equality)]) ).
cnf(548,axiom,
h14(e11) = op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
cnf(549,plain,
h14(e11) = h7(e13),
inference('REWRITE',[status(thm)],[548,501,theory(equality)]) ).
cnf(550,axiom,
h14(e13) = op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
cnf(551,plain,
h14(e13) = h7(e11),
inference('REWRITE',[status(thm)],[550,500,theory(equality)]) ).
cnf(563,axiom,
h16(e11) = op2(e24,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax31) ).
cnf(564,axiom,
h16(e13) = op2(e23,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax31) ).
cnf(569,axiom,
h17(e11) = op2(e20,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax32) ).
cnf(570,plain,
h17(e11) = h4(e13),
inference('REWRITE',[status(thm)],[569,483,theory(equality)]) ).
cnf(571,axiom,
h17(e13) = op2(e24,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax32) ).
cnf(572,plain,
h17(e13) = h4(e11),
inference('REWRITE',[status(thm)],[571,482,theory(equality)]) ).
cnf(575,axiom,
h18(e10) = op2(op2(e21,e24),op2(e21,e24)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax33) ).
cnf(576,plain,
h18(e10) = op2(h8(e13),h8(e13)),
inference('REWRITE',[status(thm)],[575,506,theory(equality)]) ).
cnf(577,axiom,
h18(e11) = op2(e21,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax33) ).
cnf(578,plain,
h18(e11) = h8(e13),
inference('REWRITE',[status(thm)],[577,506,theory(equality)]) ).
cnf(579,axiom,
h18(e13) = op2(e24,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax33) ).
cnf(580,plain,
h18(e13) = h8(e11),
inference('REWRITE',[status(thm)],[579,505,theory(equality)]) ).
cnf(583,axiom,
h19(e10) = op2(op2(e22,e24),op2(e22,e24)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax34) ).
cnf(584,plain,
h19(e10) = op2(e23,e23),
inference('REWRITE',[status(thm)],[583,463,theory(equality)]) ).
cnf(6095,negated_conjecture,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e14)) != op2(h8(e10),h8(e14))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e14)) != op2(h8(e11),h8(e14))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e14)) != op2(h8(e12),h8(e14))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e14)) != op2(h8(e13),h8(e14))
| h8(op1(e14,e10)) != op2(h8(e14),h8(e10))
| h8(op1(e14,e11)) != op2(h8(e14),h8(e11))
| h8(op1(e14,e12)) != op2(h8(e14),h8(e12))
| h8(op1(e14,e13)) != op2(h8(e14),h8(e13))
| h8(op1(e14,e14)) != op2(h8(e14),h8(e14))
| h8(e10) != e20
| h8(e12) != e21
| h8(e13) != e22
| h8(e11) != e23
| h8(e14) != e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
cnf(6096,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h8(op1(e11,e10)) != op2(h18(e13),h8(e10))
| h8(op1(e11,e11)) != op2(h18(e13),h18(e13))
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h18(e11) != op2(e21,e24)
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != op2(h18(e11),h18(e11))
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h18(e13) != op2(e24,e21)
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != op2(e24,e24)
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[6095,459,460,531,503,578,502,580,theory(equality)]) ).
cnf(14269,plain,
( h19(e10) = e20
| h19(e10) = e21
| h19(e10) = e22
| h19(e10) = e23
| h19(e10) = e24 ),
inference('REWRITE',[status(thm)],[105,584,theory(equality)]) ).
cnf(14270,plain,
h18(e13) = op2(e24,e21),
inference('REWRITE',[status(thm)],[505,580,theory(equality)]) ).
cnf(14278,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h8(op1(e11,e10)) != op2(h18(e13),h8(e10))
| h8(op1(e11,e11)) != op2(h18(e13),h18(e13))
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h18(e11) != op2(e21,e24)
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != op2(h18(e11),h18(e11))
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != op2(e24,e24)
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[6096,14270,theory(equality)]) ).
cnf(14327,plain,
h18(e11) = op2(e21,e24),
inference('REWRITE',[status(thm)],[506,578,theory(equality)]) ).
cnf(14335,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h8(op1(e11,e10)) != op2(h18(e13),h8(e10))
| h8(op1(e11,e11)) != op2(h18(e13),h18(e13))
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != op2(h18(e11),h18(e11))
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != op2(e24,e24)
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[14278,14327,theory(equality)]) ).
cnf(14384,plain,
h18(e10) = op2(h18(e11),h18(e11)),
inference('REWRITE',[status(thm)],[576,578,theory(equality)]) ).
cnf(14392,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h8(op1(e11,e10)) != op2(h18(e13),h8(e10))
| h8(op1(e11,e11)) != op2(h18(e13),h18(e13))
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != h18(e10)
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != op2(e24,e24)
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[14335,14384,theory(equality)]) ).
cnf(14439,plain,
h17(e13) = op2(e24,e20),
inference('REWRITE',[status(thm)],[482,572,theory(equality)]) ).
cnf(14494,plain,
h17(e11) = op2(e20,e24),
inference('REWRITE',[status(thm)],[483,570,theory(equality)]) ).
cnf(14607,plain,
( h19(e10) != e24
| h16(e13) = e23 ),
inference('REWRITE',[status(thm)],[453,584,564,theory(equality)]) ).
cnf(14609,plain,
h19(e10) != h16(e11),
inference('REWRITE',[status(thm)],[312,584,563,theory(equality)]) ).
cnf(14667,plain,
h14(e13) = op2(e23,e21),
inference('REWRITE',[status(thm)],[500,551,theory(equality)]) ).
cnf(14724,plain,
h14(e11) = op2(e21,e23),
inference('REWRITE',[status(thm)],[501,549,theory(equality)]) ).
cnf(14836,plain,
h13(e13) = op2(e23,e20),
inference('REWRITE',[status(thm)],[477,543,theory(equality)]) ).
cnf(14891,plain,
h13(e11) = op2(e20,e23),
inference('REWRITE',[status(thm)],[478,541,theory(equality)]) ).
cnf(15003,plain,
h11(e13) != h19(e10),
inference('REWRITE',[status(thm)],[310,584,527,theory(equality)]) ).
cnf(15008,plain,
op2(e22,e22) != h11(e11),
inference('REWRITE',[status(thm)],[300,526,theory(equality)]) ).
cnf(15011,plain,
( h19(e10) != e22
| h11(e11) = e23 ),
inference('REWRITE',[status(thm)],[452,584,526,theory(equality)]) ).
cnf(15067,plain,
h10(e13) = op2(e22,e21),
inference('REWRITE',[status(thm)],[495,522,theory(equality)]) ).
cnf(15124,plain,
h10(e11) = op2(e21,e22),
inference('REWRITE',[status(thm)],[496,520,theory(equality)]) ).
cnf(15236,plain,
( h18(e11) = e20
| h18(e11) = e21
| h18(e11) = e22
| h18(e11) = e23
| h18(e11) = e24 ),
inference('REWRITE',[status(thm)],[96,578,506,theory(equality)]) ).
cnf(15238,plain,
h18(e11) != op2(e24,e24),
inference('REWRITE',[status(thm)],[319,578,506,theory(equality)]) ).
cnf(15239,plain,
h12(e10) != h18(e11),
inference('REWRITE',[status(thm)],[339,578,531,506,theory(equality)]) ).
cnf(15242,plain,
h12(e10) != h18(e13),
inference('REWRITE',[status(thm)],[289,580,531,505,theory(equality)]) ).
cnf(15246,plain,
h8(e10) = op2(h18(e13),h18(e13)),
inference('REWRITE',[status(thm)],[504,580,505,theory(equality)]) ).
cnf(15254,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h8(op1(e11,e10)) != op2(h18(e13),h8(e10))
| h8(op1(e11,e11)) != h8(e10)
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != h18(e10)
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != op2(e24,e24)
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[14392,15246,theory(equality)]) ).
cnf(15301,plain,
( h14(e11) = e20
| h14(e11) = e21
| h14(e11) = e22
| h14(e11) = e23
| h14(e11) = e24 ),
inference('REWRITE',[status(thm)],[95,549,501,theory(equality)]) ).
cnf(15304,plain,
h14(e11) != h16(e11),
inference('REWRITE',[status(thm)],[309,563,549,501,theory(equality)]) ).
cnf(15305,plain,
h12(e10) != h14(e11),
inference('REWRITE',[status(thm)],[338,549,531,501,theory(equality)]) ).
cnf(15306,plain,
h14(e11) != h18(e11),
inference('REWRITE',[status(thm)],[342,14327,549,501,theory(equality)]) ).
cnf(15310,plain,
h14(e13) != h18(e13),
inference('REWRITE',[status(thm)],[292,14270,551,500,theory(equality)]) ).
cnf(15370,plain,
( h10(e11) = e20
| h10(e11) = e21
| h10(e11) = e22
| h10(e11) = e23
| h10(e11) = e24 ),
inference('REWRITE',[status(thm)],[94,520,496,theory(equality)]) ).
cnf(15372,plain,
h10(e11) != h11(e11),
inference('REWRITE',[status(thm)],[298,526,520,496,theory(equality)]) ).
cnf(15373,plain,
h12(e10) != h10(e11),
inference('REWRITE',[status(thm)],[337,520,531,496,theory(equality)]) ).
cnf(15374,plain,
h10(e11) != h14(e11),
inference('REWRITE',[status(thm)],[340,14724,520,496,theory(equality)]) ).
cnf(15377,plain,
( h10(e13) = e20
| h10(e13) = e21
| h10(e13) = e22
| h10(e13) = e23
| h10(e13) = e24 ),
inference('REWRITE',[status(thm)],[98,522,495,theory(equality)]) ).
cnf(15378,plain,
h12(e10) != h10(e13),
inference('REWRITE',[status(thm)],[287,522,531,495,theory(equality)]) ).
cnf(15379,plain,
h10(e13) != h14(e13),
inference('REWRITE',[status(thm)],[290,14667,522,495,theory(equality)]) ).
cnf(15439,plain,
( h17(e11) = e20
| h17(e11) = e21
| h17(e11) = e22
| h17(e11) = e23
| h17(e11) = e24 ),
inference('REWRITE',[status(thm)],[91,570,483,theory(equality)]) ).
cnf(15440,plain,
h17(e11) != h18(e11),
inference('REWRITE',[status(thm)],[313,14327,570,483,theory(equality)]) ).
cnf(15441,plain,
h17(e11) != h16(e13),
inference('REWRITE',[status(thm)],[315,564,570,483,theory(equality)]) ).
cnf(15443,plain,
op2(e20,e20) != h17(e11),
inference('REWRITE',[status(thm)],[326,570,483,theory(equality)]) ).
cnf(15446,plain,
op2(e20,e20) != h17(e13),
inference('REWRITE',[status(thm)],[276,572,482,theory(equality)]) ).
cnf(15450,plain,
( op2(e24,e24) != e20
| h17(e13) = e24 ),
inference('REWRITE',[status(thm)],[454,572,482,theory(equality)]) ).
cnf(15506,plain,
( h13(e11) = e20
| h13(e11) = e21
| h13(e11) = e22
| h13(e11) = e23
| h13(e11) = e24 ),
inference('REWRITE',[status(thm)],[90,541,478,theory(equality)]) ).
cnf(15513,plain,
h13(e11) != h11(e13),
inference('REWRITE',[status(thm)],[304,527,541,478,theory(equality)]) ).
cnf(15515,plain,
h13(e11) != h16(e11),
inference('REWRITE',[status(thm)],[306,563,541,478,theory(equality)]) ).
cnf(15516,plain,
op2(e20,e20) != h13(e11),
inference('REWRITE',[status(thm)],[325,541,478,theory(equality)]) ).
cnf(15517,plain,
h13(e11) != h17(e11),
inference('REWRITE',[status(thm)],[332,14494,541,478,theory(equality)]) ).
cnf(15519,plain,
( h13(e13) = e20
| h13(e13) = e21
| h13(e13) = e22
| h13(e13) = e23
| h13(e13) = e24 ),
inference('REWRITE',[status(thm)],[102,543,477,theory(equality)]) ).
cnf(15521,plain,
( h13(e13) = e21
| h14(e13) = e21
| h11(e11) = e21
| h19(e10) = e21
| h16(e13) = e21 ),
inference('REWRITE',[status(thm)],[155,564,584,526,14667,543,477,theory(equality)]) ).
cnf(15522,plain,
( h13(e13) = e22
| h14(e13) = e22
| h11(e11) = e22
| h19(e10) = e22
| h16(e13) = e22 ),
inference('REWRITE',[status(thm)],[157,564,584,526,14667,543,477,theory(equality)]) ).
cnf(15524,plain,
( h13(e13) = e24
| h14(e13) = e24
| h11(e11) = e24
| h19(e10) = e24
| h16(e13) = e24 ),
inference('REWRITE',[status(thm)],[161,564,584,526,14667,543,477,theory(equality)]) ).
cnf(15525,plain,
op2(e20,e20) != h13(e13),
inference('REWRITE',[status(thm)],[275,543,477,theory(equality)]) ).
cnf(15526,plain,
h13(e13) != h17(e13),
inference('REWRITE',[status(thm)],[282,14439,543,477,theory(equality)]) ).
cnf(15528,plain,
h13(e13) != h11(e11),
inference('REWRITE',[status(thm)],[354,526,543,477,theory(equality)]) ).
cnf(15529,plain,
h13(e13) != h19(e10),
inference('REWRITE',[status(thm)],[355,584,543,477,theory(equality)]) ).
cnf(15588,plain,
h2(e13) != h10(e11),
inference('REWRITE',[status(thm)],[293,15124,473,theory(equality)]) ).
cnf(15591,plain,
op2(e20,e20) != h2(e13),
inference('REWRITE',[status(thm)],[324,473,theory(equality)]) ).
cnf(15596,plain,
op2(e20,e20) != h2(e11),
inference('REWRITE',[status(thm)],[274,472,theory(equality)]) ).
cnf(15597,plain,
h2(e11) != h13(e13),
inference('REWRITE',[status(thm)],[280,14836,472,theory(equality)]) ).
cnf(15598,plain,
h2(e11) != h17(e13),
inference('REWRITE',[status(thm)],[281,14439,472,theory(equality)]) ).
cnf(15599,plain,
h2(e11) != h10(e13),
inference('REWRITE',[status(thm)],[343,15067,472,theory(equality)]) ).
cnf(15602,plain,
( op2(e22,e22) != e20
| h2(e11) = e22 ),
inference('REWRITE',[status(thm)],[446,472,theory(equality)]) ).
cnf(15659,plain,
( op2(e20,e20) = e20
| h1(e13) = e20
| h2(e13) = e20
| h13(e11) = e20
| h17(e11) = e20 ),
inference('REWRITE',[status(thm)],[123,14494,14891,473,468,theory(equality)]) ).
cnf(15669,plain,
h1(e13) != h12(e10),
inference('REWRITE',[status(thm)],[283,531,468,theory(equality)]) ).
cnf(15670,plain,
h1(e13) != h10(e13),
inference('REWRITE',[status(thm)],[284,15067,468,theory(equality)]) ).
cnf(15671,plain,
h1(e13) != h14(e13),
inference('REWRITE',[status(thm)],[285,14667,468,theory(equality)]) ).
cnf(15690,plain,
h1(e11) != h2(e11),
inference('REWRITE',[status(thm)],[277,472,467,theory(equality)]) ).
cnf(15691,plain,
h1(e11) != h13(e13),
inference('REWRITE',[status(thm)],[278,14836,467,theory(equality)]) ).
cnf(15695,plain,
h1(e11) != h14(e11),
inference('REWRITE',[status(thm)],[335,14724,467,theory(equality)]) ).
cnf(15696,plain,
h1(e11) != h18(e11),
inference('REWRITE',[status(thm)],[336,14327,467,theory(equality)]) ).
cnf(15697,plain,
( h12(e10) != e20
| h1(e11) = e21 ),
inference('REWRITE',[status(thm)],[442,531,467,theory(equality)]) ).
cnf(15753,plain,
( h2(e11) = e20
| h10(e13) = e20
| op2(e22,e22) = e20
| h11(e13) = e20 ),
inference('REWRITE',[status(thm)],[143,385,527,15067,472,463,theory(equality)]) ).
cnf(15754,plain,
( h2(e11) = e21
| h10(e13) = e21
| op2(e22,e22) = e21
| h11(e13) = e21 ),
inference('REWRITE',[status(thm)],[145,388,527,15067,472,463,theory(equality)]) ).
cnf(15757,plain,
( h17(e11) = e20
| h18(e11) = e20
| h16(e13) = e20
| op2(e24,e24) = e20 ),
inference('REWRITE',[status(thm)],[164,564,385,14327,14494,463,theory(equality)]) ).
cnf(15761,plain,
h17(e11) != e23,
inference('REWRITE',[status(thm)],[314,14494,463,theory(equality)]) ).
cnf(15762,plain,
( h17(e11) = e20
| h17(e11) = e21
| h17(e11) = e22
| h17(e11) = e24 ),
inference('REWRITE',[status(thm)],[15439,15761]) ).
cnf(15764,plain,
h18(e11) != e23,
inference('REWRITE',[status(thm)],[317,14327,463,theory(equality)]) ).
cnf(15765,plain,
( h18(e11) = e20
| h18(e11) = e21
| h18(e11) = e22
| h18(e11) = e24 ),
inference('REWRITE',[status(thm)],[15236,15764]) ).
cnf(15767,plain,
h16(e13) != e23,
inference('REWRITE',[status(thm)],[320,564,463,theory(equality)]) ).
cnf(15769,plain,
h19(e10) != e24,
inference('REWRITE',[status(thm)],[14607,15767]) ).
cnf(15770,plain,
( h19(e10) = e20
| h19(e10) = e21
| h19(e10) = e22
| h19(e10) = e23 ),
inference('REWRITE',[status(thm)],[14269,15769]) ).
cnf(15772,plain,
( h13(e13) = e24
| h14(e13) = e24
| h11(e11) = e24
| h16(e13) = e24 ),
inference('REWRITE',[status(thm)],[15524,15769]) ).
cnf(15774,plain,
op2(e24,e24) != e23,
inference('REWRITE',[status(thm)],[321,463,theory(equality)]) ).
cnf(15775,plain,
( op2(e24,e24) = e20
| op2(e24,e24) = e21
| op2(e24,e24) = e22
| op2(e24,e24) = e24 ),
inference('REWRITE',[status(thm)],[111,15774]) ).
cnf(15779,plain,
h10(e13) != e23,
inference('REWRITE',[status(thm)],[349,15067,463,theory(equality)]) ).
cnf(15780,plain,
( h10(e13) = e20
| h10(e13) = e21
| h10(e13) = e22
| h10(e13) = e24 ),
inference('REWRITE',[status(thm)],[15377,15779]) ).
cnf(15790,plain,
( h2(e13) = e20
| h10(e11) = e20
| op2(e22,e22) = e20
| h11(e11) = e20 ),
inference('REWRITE',[status(thm)],[144,383,526,15124,473,462,theory(equality)]) ).
cnf(15794,plain,
( h17(e13) = e20
| h18(e13) = e20
| h16(e11) = e20
| op2(e24,e24) = e20 ),
inference('REWRITE',[status(thm)],[163,563,383,14270,14439,462,theory(equality)]) ).
cnf(15795,plain,
( h17(e13) = e22
| h18(e13) = e22
| h16(e11) = e22
| op2(e24,e24) = e22 ),
inference('REWRITE',[status(thm)],[167,563,387,14270,14439,462,theory(equality)]) ).
cnf(15796,plain,
( h17(e13) = e23
| h18(e13) = e23
| h16(e11) = e23 ),
inference('REWRITE',[status(thm)],[169,15774,563,388,14270,14439,462,theory(equality)]) ).
cnf(15801,plain,
h10(e11) != e21,
inference('REWRITE',[status(thm)],[299,15124,462,theory(equality)]) ).
cnf(15802,plain,
( h10(e11) = e20
| h10(e11) = e22
| h10(e11) = e23
| h10(e11) = e24 ),
inference('REWRITE',[status(thm)],[15370,15801]) ).
cnf(15808,plain,
op2(e22,e22) != e21,
inference('REWRITE',[status(thm)],[301,462,theory(equality)]) ).
cnf(15809,plain,
( h2(e11) = e21
| h10(e13) = e21
| h11(e13) = e21 ),
inference('REWRITE',[status(thm)],[15754,15808]) ).
cnf(15811,plain,
h11(e11) != e21,
inference('REWRITE',[status(thm)],[302,526,462,theory(equality)]) ).
cnf(15813,plain,
( h13(e13) = e21
| h14(e13) = e21
| h19(e10) = e21
| h16(e13) = e21 ),
inference('REWRITE',[status(thm)],[15521,15811]) ).
cnf(15823,plain,
op2(e24,e24) != e21,
inference('REWRITE',[status(thm)],[371,462,theory(equality)]) ).
cnf(15825,plain,
( op2(e24,e24) = e20
| op2(e24,e24) = e22
| op2(e24,e24) = e24 ),
inference('REWRITE',[status(thm)],[15775,15823]) ).
cnf(15826,plain,
op2(e24,e24) != e22,
inference('REWRITE',[status(thm)],[456,389,462,theory(equality)]) ).
cnf(15828,plain,
( h17(e13) = e22
| h18(e13) = e22
| h16(e11) = e22 ),
inference('REWRITE',[status(thm)],[15795,15826]) ).
cnf(15829,plain,
( op2(e24,e24) = e20
| op2(e24,e24) = e24 ),
inference('REWRITE',[status(thm)],[15825,15826]) ).
cnf(15830,plain,
h12(e10) = e20,
inference('REWRITE',[status(thm)],[461,531,462,theory(equality)]) ).
cnf(15831,plain,
op2(e21,e21) = e20,
inference('REWRITE',[status(thm)],[531,15830,theory(equality)]) ).
cnf(15834,plain,
h18(e11) != e20,
inference('REWRITE',[status(thm)],[15239,15830,theory(equality)]) ).
cnf(15835,plain,
( h17(e11) = e20
| h16(e13) = e20
| op2(e24,e24) = e20 ),
inference('REWRITE',[status(thm)],[15757,15834]) ).
cnf(15836,plain,
( h18(e11) = e21
| h18(e11) = e22
| h18(e11) = e24 ),
inference('REWRITE',[status(thm)],[15765,15834]) ).
cnf(15837,plain,
h18(e13) != e20,
inference('REWRITE',[status(thm)],[15242,15830,theory(equality)]) ).
cnf(15838,plain,
( h17(e13) = e20
| h16(e11) = e20
| op2(e24,e24) = e20 ),
inference('REWRITE',[status(thm)],[15794,15837]) ).
cnf(15845,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h8(op1(e11,e10)) != op2(h18(e13),h8(e10))
| h8(op1(e11,e11)) != h8(e10)
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != e20
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != h18(e10)
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != op2(e24,e24)
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[15254,15830,theory(equality)]) ).
cnf(15852,plain,
h14(e11) != e20,
inference('REWRITE',[status(thm)],[15305,15830,theory(equality)]) ).
cnf(15853,plain,
( h14(e11) = e21
| h14(e11) = e22
| h14(e11) = e23
| h14(e11) = e24 ),
inference('REWRITE',[status(thm)],[15301,15852]) ).
cnf(15876,plain,
h10(e11) != e20,
inference('REWRITE',[status(thm)],[15373,15830,theory(equality)]) ).
cnf(15877,plain,
( h2(e13) = e20
| op2(e22,e22) = e20
| h11(e11) = e20 ),
inference('REWRITE',[status(thm)],[15790,15876]) ).
cnf(15878,plain,
( h10(e11) = e22
| h10(e11) = e23
| h10(e11) = e24 ),
inference('REWRITE',[status(thm)],[15802,15876]) ).
cnf(15879,plain,
h10(e13) != e20,
inference('REWRITE',[status(thm)],[15378,15830,theory(equality)]) ).
cnf(15880,plain,
( h2(e11) = e20
| op2(e22,e22) = e20
| h11(e13) = e20 ),
inference('REWRITE',[status(thm)],[15753,15879]) ).
cnf(15881,plain,
( h10(e13) = e21
| h10(e13) = e22
| h10(e13) = e24 ),
inference('REWRITE',[status(thm)],[15780,15879]) ).
cnf(15895,plain,
h1(e13) != e20,
inference('REWRITE',[status(thm)],[15669,15830,theory(equality)]) ).
cnf(15897,plain,
( op2(e20,e20) = e20
| h2(e13) = e20
| h13(e11) = e20
| h17(e11) = e20 ),
inference('REWRITE',[status(thm)],[15659,15895]) ).
cnf(15906,plain,
h1(e11) = e21,
inference('REWRITE',[status(thm)],[15697,15830,theory(equality)]) ).
cnf(15907,plain,
op2(e21,e20) = e21,
inference('REWRITE',[status(thm)],[467,15906,theory(equality)]) ).
cnf(15911,plain,
h2(e11) != e21,
inference('REWRITE',[status(thm)],[15690,15906,theory(equality)]) ).
cnf(15913,plain,
( h10(e13) = e21
| h11(e13) = e21 ),
inference('REWRITE',[status(thm)],[15809,15911]) ).
cnf(15914,plain,
h13(e13) != e21,
inference('REWRITE',[status(thm)],[15691,15906,theory(equality)]) ).
cnf(15915,plain,
( h13(e13) = e20
| h13(e13) = e22
| h13(e13) = e23
| h13(e13) = e24 ),
inference('REWRITE',[status(thm)],[15519,15914]) ).
cnf(15916,plain,
( h14(e13) = e21
| h19(e10) = e21
| h16(e13) = e21 ),
inference('REWRITE',[status(thm)],[15813,15914]) ).
cnf(15917,plain,
h14(e11) != e21,
inference('REWRITE',[status(thm)],[15695,15906,theory(equality)]) ).
cnf(15919,plain,
( h14(e11) = e22
| h14(e11) = e23
| h14(e11) = e24 ),
inference('REWRITE',[status(thm)],[15853,15917]) ).
cnf(15920,plain,
h18(e11) != e21,
inference('REWRITE',[status(thm)],[15696,15906,theory(equality)]) ).
cnf(15922,plain,
( h18(e11) = e22
| h18(e11) = e24 ),
inference('REWRITE',[status(thm)],[15836,15920]) ).
cnf(15940,plain,
( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 ),
inference('REWRITE',[status(thm)],[57,375,460,theory(equality)]) ).
cnf(15941,plain,
( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 ),
inference('REWRITE',[status(thm)],[59,378,460,theory(equality)]) ).
cnf(15945,plain,
( op1(e10,e14) = e11
| op1(e11,e14) = e11
| op1(e13,e14) = e11
| op1(e14,e14) = e11 ),
inference('REWRITE',[status(thm)],[80,378,460,theory(equality)]) ).
cnf(15951,plain,
op1(e11,e14) != e13,
inference('REWRITE',[status(thm)],[217,460,theory(equality)]) ).
cnf(15952,plain,
( op1(e11,e14) = e10
| op1(e11,e14) = e11
| op1(e11,e14) = e12
| op1(e11,e14) = e14 ),
inference('REWRITE',[status(thm)],[10,15951]) ).
cnf(15954,plain,
op1(e13,e14) != e13,
inference('REWRITE',[status(thm)],[220,460,theory(equality)]) ).
cnf(15957,plain,
op1(e13,e13) != e14,
inference('REWRITE',[status(thm)],[433,15954]) ).
cnf(15959,plain,
( op1(e13,e10) = e14
| op1(e13,e11) = e14
| op1(e13,e12) = e14
| op1(e13,e14) = e14 ),
inference('REWRITE',[status(thm)],[75,15957]) ).
cnf(15961,plain,
op1(e14,e14) != e13,
inference('REWRITE',[status(thm)],[221,460,theory(equality)]) ).
cnf(15966,plain,
op1(e12,e11) != e13,
inference('REWRITE',[status(thm)],[249,460,theory(equality)]) ).
cnf(15967,plain,
( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e14 ),
inference('REWRITE',[status(thm)],[12,15966]) ).
cnf(15981,plain,
( op1(e14,e10) = e10
| op1(e14,e11) = e10
| op1(e14,e13) = e10
| op1(e14,e14) = e10 ),
inference('REWRITE',[status(thm)],[77,373,459,theory(equality)]) ).
cnf(15982,plain,
( op1(e14,e10) = e12
| op1(e14,e11) = e12
| op1(e14,e13) = e12
| op1(e14,e14) = e12 ),
inference('REWRITE',[status(thm)],[81,377,459,theory(equality)]) ).
cnf(15983,plain,
( op1(e14,e10) = e13
| op1(e14,e11) = e13
| op1(e14,e13) = e13 ),
inference('REWRITE',[status(thm)],[83,15961,378,459,theory(equality)]) ).
cnf(15988,plain,
op1(e11,e12) != e11,
inference('REWRITE',[status(thm)],[199,459,theory(equality)]) ).
cnf(15989,plain,
( op1(e11,e12) = e10
| op1(e11,e12) = e12
| op1(e11,e12) = e13
| op1(e11,e12) = e14 ),
inference('REWRITE',[status(thm)],[8,15988]) ).
cnf(15995,plain,
op1(e12,e12) != e11,
inference('REWRITE',[status(thm)],[201,459,theory(equality)]) ).
cnf(15996,plain,
( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e13) = e11 ),
inference('REWRITE',[status(thm)],[15941,15995]) ).
cnf(15998,plain,
op1(e13,e12) != e11,
inference('REWRITE',[status(thm)],[202,459,theory(equality)]) ).
cnf(16000,plain,
( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e13) = e11
| op1(e13,e14) = e11 ),
inference('REWRITE',[status(thm)],[69,15998]) ).
cnf(16010,plain,
op1(e14,e14) != e11,
inference('REWRITE',[status(thm)],[271,459,theory(equality)]) ).
cnf(16011,plain,
( op1(e10,e14) = e11
| op1(e11,e14) = e11
| op1(e13,e14) = e11 ),
inference('REWRITE',[status(thm)],[15945,16010]) ).
cnf(16013,plain,
op1(e14,e14) != e12,
inference('REWRITE',[status(thm)],[436,379,459,theory(equality)]) ).
cnf(16015,plain,
( op1(e14,e10) = e12
| op1(e14,e11) = e12
| op1(e14,e13) = e12 ),
inference('REWRITE',[status(thm)],[15982,16013]) ).
cnf(16017,plain,
op1(e11,e11) = e10,
inference('REWRITE',[status(thm)],[458,459,theory(equality)]) ).
cnf(16027,plain,
op1(e12,e11) != e10,
inference('REWRITE',[status(thm)],[187,16017,theory(equality)]) ).
cnf(16028,plain,
( op1(e12,e10) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 ),
inference('REWRITE',[status(thm)],[15940,16027]) ).
cnf(16029,plain,
( op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e14 ),
inference('REWRITE',[status(thm)],[15967,16027]) ).
cnf(16030,plain,
op1(e13,e11) != e10,
inference('REWRITE',[status(thm)],[188,16017,theory(equality)]) ).
cnf(16032,plain,
( op1(e13,e10) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10
| op1(e13,e14) = e10 ),
inference('REWRITE',[status(thm)],[67,16030]) ).
cnf(16033,plain,
op1(e14,e11) != e10,
inference('REWRITE',[status(thm)],[189,16017,theory(equality)]) ).
cnf(16034,plain,
( op1(e14,e10) = e10
| op1(e14,e13) = e10
| op1(e14,e14) = e10 ),
inference('REWRITE',[status(thm)],[15981,16033]) ).
cnf(16039,plain,
op1(e11,e12) != e10,
inference('REWRITE',[status(thm)],[237,16017,theory(equality)]) ).
cnf(16041,plain,
( op1(e11,e12) = e12
| op1(e11,e12) = e13
| op1(e11,e12) = e14 ),
inference('REWRITE',[status(thm)],[15989,16039]) ).
cnf(16042,plain,
op1(e11,e13) != e10,
inference('REWRITE',[status(thm)],[238,16017,theory(equality)]) ).
cnf(16043,plain,
( op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13
| op1(e11,e13) = e14 ),
inference('REWRITE',[status(thm)],[9,16042]) ).
cnf(16045,plain,
op1(e11,e14) != e10,
inference('REWRITE',[status(thm)],[239,16017,theory(equality)]) ).
cnf(16047,plain,
( op1(e11,e14) = e11
| op1(e11,e14) = e12
| op1(e11,e14) = e14 ),
inference('REWRITE',[status(thm)],[15952,16045]) ).
cnf(16048,plain,
op1(e11,e10) = e11,
inference('REWRITE',[status(thm)],[422,16017,theory(equality)]) ).
cnf(16051,plain,
op1(e12,e10) != e11,
inference('REWRITE',[status(thm)],[177,16048,theory(equality)]) ).
cnf(16053,plain,
( op1(e12,e11) = e11
| op1(e12,e13) = e11 ),
inference('REWRITE',[status(thm)],[15996,16051]) ).
cnf(16054,plain,
op1(e13,e10) != e11,
inference('REWRITE',[status(thm)],[178,16048,theory(equality)]) ).
cnf(16055,plain,
( op1(e13,e10) = e10
| op1(e13,e10) = e12
| op1(e13,e10) = e13
| op1(e13,e10) = e14 ),
inference('REWRITE',[status(thm)],[16,16054]) ).
cnf(16056,plain,
( op1(e13,e11) = e11
| op1(e13,e13) = e11
| op1(e13,e14) = e11 ),
inference('REWRITE',[status(thm)],[16000,16054]) ).
cnf(16057,plain,
op1(e11,e13) != e11,
inference('REWRITE',[status(thm)],[235,16048,theory(equality)]) ).
cnf(16059,plain,
( op1(e11,e13) = e12
| op1(e11,e13) = e13
| op1(e11,e13) = e14 ),
inference('REWRITE',[status(thm)],[16043,16057]) ).
cnf(16060,plain,
op1(e11,e14) != e11,
inference('REWRITE',[status(thm)],[236,16048,theory(equality)]) ).
cnf(16061,plain,
( op1(e10,e14) = e11
| op1(e13,e14) = e11 ),
inference('REWRITE',[status(thm)],[16011,16060]) ).
cnf(16062,plain,
( op1(e11,e14) = e12
| op1(e11,e14) = e14 ),
inference('REWRITE',[status(thm)],[16047,16060]) ).
cnf(16216,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h18(e13) != op2(h18(e13),h8(e10))
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != e20
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != h18(e10)
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != op2(e24,e24)
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[15845,580,16048,16017,theory(equality)]) ).
cnf(16276,plain,
( h18(e11) = e22
| op2(e24,e24) != e24 ),
inference('PARAMODULATE',[status(thm)],[15238,15922,theory(equality)]) ).
cnf(16277,plain,
( h18(e11) = e22
| h18(e10) = op2(e24,e24) ),
inference('PARAMODULATE',[status(thm)],[14384,15922,theory(equality)]) ).
cnf(16394,plain,
( h17(e11) = e20
| h16(e13) = e20
| h17(e13) = e24 ),
inference('HYPERRESOLVE',[status(thm)],[15450,15835]) ).
cnf(16400,plain,
( h2(e13) = e20
| h11(e11) = e20
| h2(e11) = e22 ),
inference('HYPERRESOLVE',[status(thm)],[15602,15877]) ).
cnf(16411,plain,
( unit1 = e10
| unit1 = e11
| unit1 = e12
| unit1 = e13 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[33,36,theory(equality)]),15954]) ).
cnf(16413,plain,
( unit2 = e20
| unit2 = e21
| unit2 = e22
| unit2 = e23 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[119,122,theory(equality)]),15767,564,theory(equality)]) ).
cnf(16632,plain,
( h2(e13) = e20
| h13(e11) = e20
| h17(e11) = e20
| h2(e11) != e20 ),
inference('PARAMODULATE',[status(thm)],[15596,15897,theory(equality)]) ).
cnf(16703,plain,
( op1(e13,e10) = e14
| op1(e13,e11) = e14
| op1(e13,e12) = e14
| op1(e10,e14) = e11 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[16061,15959,theory(equality)]),379]) ).
cnf(16786,plain,
( op1(e13,e10) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10
| op1(e10,e14) = e11 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[16061,16032,theory(equality)]),373]) ).
cnf(16879,plain,
( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12
| op1(e10,e14) = e11 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[16061,71,theory(equality)]),377]) ).
cnf(16885,plain,
( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12
| op1(e14,e10) = e13
| op1(e14,e11) = e13 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[15983,72,theory(equality)]),380]) ).
cnf(19262,plain,
( h17(e13) = e20
| h16(e11) = e20
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h18(e13) != op2(h18(e13),h8(e10))
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != e20
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != h18(e10)
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != e20
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('PARAMODULATE',[status(thm)],[16216,15838,theory(equality)]) ).
cnf(31430,plain,
( op2(e24,e24) = e20
| h18(e11) = e22 ),
inference('HYPERRESOLVE',[status(thm)],[16276,15829]) ).
cnf(31693,plain,
( h18(e11) = e22
| h18(e10) = e20 ),
inference('PARAMODULATE',[status(thm)],[16277,31430,theory(equality)]) ).
cnf(31758,plain,
( h18(e10) = e20
| h18(e10) = op2(e22,e22) ),
inference('PARAMODULATE',[status(thm)],[14384,31693,theory(equality)]) ).
cnf(31971,plain,
( unit1 = e10
| unit1 = e11
| unit1 = e12 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[29,16411,theory(equality)]),16057]) ).
cnf(31972,plain,
( unit1 = e10
| unit1 = e11 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[35,31971,theory(equality)]),379,459,theory(equality)]) ).
cnf(31979,plain,
unit1 = e10,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[29,31972,theory(equality)]),373,16017,theory(equality)]) ).
cnf(31980,plain,
op1(e10,e10) = e10,
inference('REWRITE',[status(thm)],[27,31979,theory(equality)]) ).
cnf(31982,plain,
( op1(e10,e11) = e14
| op1(e10,e12) = e14
| op1(e10,e13) = e14
| op1(e10,e14) = e14 ),
inference('REWRITE',[status(thm)],[45,376,31980,theory(equality)]) ).
cnf(31983,plain,
op1(e12,e10) != e10,
inference('REWRITE',[status(thm)],[174,31980,theory(equality)]) ).
cnf(31984,plain,
( op1(e12,e12) = e10
| op1(e12,e13) = e10 ),
inference('REWRITE',[status(thm)],[16028,31983]) ).
cnf(31995,plain,
op1(e13,e10) != e10,
inference('REWRITE',[status(thm)],[175,31980,theory(equality)]) ).
cnf(31997,plain,
( op1(e13,e10) = e12
| op1(e13,e10) = e13
| op1(e13,e10) = e14 ),
inference('REWRITE',[status(thm)],[16055,31995]) ).
cnf(32000,plain,
( op1(e13,e12) = e10
| op1(e13,e13) = e10
| op1(e10,e14) = e11 ),
inference('REWRITE',[status(thm)],[16786,31995]) ).
cnf(32010,plain,
op1(e14,e10) != e10,
inference('REWRITE',[status(thm)],[176,31980,theory(equality)]) ).
cnf(32012,plain,
( op1(e14,e13) = e10
| op1(e14,e14) = e10 ),
inference('REWRITE',[status(thm)],[16034,32010]) ).
cnf(32034,plain,
op1(e10,e13) != e10,
inference('REWRITE',[status(thm)],[225,31980,theory(equality)]) ).
cnf(32035,plain,
( op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13
| op1(e10,e13) = e14 ),
inference('REWRITE',[status(thm)],[4,32034]) ).
cnf(34521,plain,
( h17(e13) = e20
| h16(e11) = e20
| h8(e10) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h18(e13) != op2(h18(e13),h8(e10))
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e12,e11)) != op2(e21,h18(e13))
| h8(op1(e12,e12)) != e20
| h8(op1(e12,e13)) != op2(e21,h18(e11))
| h8(op1(e13,e10)) != op2(h18(e11),h8(e10))
| h8(op1(e13,e11)) != op2(h18(e11),h18(e13))
| h8(op1(e13,e12)) != op2(h18(e11),e21)
| h8(op1(e13,e13)) != h18(e10)
| h8(op1(e13,e14)) != op2(h18(e11),e24)
| h8(op1(e14,e10)) != op2(e24,h8(e10))
| h8(op1(e14,e11)) != op2(e24,h18(e13))
| h8(op1(e14,e13)) != op2(e24,h18(e11))
| h8(op1(e14,e14)) != e20
| h8(e10) != e20
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[19262,31980,theory(equality)]) ).
cnf(46480,plain,
op1(e10,e11) = e11,
inference('REWRITE',[status(thm)],[28,31979,theory(equality)]) ).
cnf(46481,plain,
op1(e12,e11) != e11,
inference('REWRITE',[status(thm)],[184,46480,theory(equality)]) ).
cnf(46482,plain,
( op1(e12,e11) = e12
| op1(e12,e11) = e14 ),
inference('REWRITE',[status(thm)],[16029,46481]) ).
cnf(46483,plain,
op1(e12,e13) = e11,
inference('REWRITE',[status(thm)],[16053,46481]) ).
cnf(46485,plain,
op1(e10,e13) != e11,
inference('REWRITE',[status(thm)],[204,46483,theory(equality)]) ).
cnf(46486,plain,
( op1(e10,e13) = e12
| op1(e10,e13) = e13
| op1(e10,e13) = e14 ),
inference('REWRITE',[status(thm)],[32035,46485]) ).
cnf(46491,plain,
op1(e13,e13) != e11,
inference('REWRITE',[status(thm)],[210,46483,theory(equality)]) ).
cnf(46493,plain,
( op1(e13,e11) = e11
| op1(e13,e14) = e11 ),
inference('REWRITE',[status(thm)],[16056,46491]) ).
cnf(46517,plain,
( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e13,e13) = e12
| op1(e14,e10) = e13
| op1(e14,e11) = e13 ),
inference('REWRITE',[status(thm)],[16885,377,46483,theory(equality)]) ).
cnf(46521,plain,
op1(e12,e12) = e10,
inference('REWRITE',[status(thm)],[31984,373,46483,theory(equality)]) ).
cnf(46522,plain,
op1(e13,e12) != e10,
inference('REWRITE',[status(thm)],[200,46521,theory(equality)]) ).
cnf(46531,plain,
( op1(e13,e13) = e10
| op1(e10,e14) = e11 ),
inference('REWRITE',[status(thm)],[32000,46522]) ).
cnf(46536,plain,
op1(e12,e10) = e12,
inference('REWRITE',[status(thm)],[426,46521,theory(equality)]) ).
cnf(46537,plain,
op1(e13,e10) != e12,
inference('REWRITE',[status(thm)],[180,46536,theory(equality)]) ).
cnf(46541,plain,
( op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12
| op1(e10,e14) = e11 ),
inference('REWRITE',[status(thm)],[16879,46537]) ).
cnf(46543,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e14 ),
inference('REWRITE',[status(thm)],[31997,46537]) ).
cnf(46550,plain,
op1(e14,e10) != e12,
inference('REWRITE',[status(thm)],[181,46536,theory(equality)]) ).
cnf(46551,plain,
( op1(e14,e11) = e12
| op1(e14,e13) = e12 ),
inference('REWRITE',[status(thm)],[16015,46550]) ).
cnf(46564,plain,
op1(e12,e11) != e12,
inference('REWRITE',[status(thm)],[243,46536,theory(equality)]) ).
cnf(46565,plain,
op1(e12,e11) = e14,
inference('REWRITE',[status(thm)],[46482,46564]) ).
cnf(46566,plain,
op1(e13,e11) != e14,
inference('REWRITE',[status(thm)],[190,46565,theory(equality)]) ).
cnf(46572,plain,
( op1(e13,e10) = e14
| op1(e13,e12) = e14
| op1(e10,e14) = e11 ),
inference('REWRITE',[status(thm)],[16703,46566]) ).
cnf(46600,plain,
op1(e13,e11) != e11,
inference('REWRITE',[status(thm)],[185,46480,theory(equality)]) ).
cnf(46601,plain,
op1(e13,e14) = e11,
inference('REWRITE',[status(thm)],[46493,46600]) ).
cnf(46602,plain,
op1(e10,e14) != e11,
inference('REWRITE',[status(thm)],[215,46601,theory(equality)]) ).
cnf(46610,plain,
op1(e13,e13) = e10,
inference('REWRITE',[status(thm)],[46531,46602]) ).
cnf(46611,plain,
op1(e14,e13) != e10,
inference('REWRITE',[status(thm)],[212,46610,theory(equality)]) ).
cnf(46617,plain,
op1(e14,e14) = e10,
inference('REWRITE',[status(thm)],[32012,46611]) ).
cnf(46618,plain,
op1(e14,e10) = e14,
inference('REWRITE',[status(thm)],[434,46617,theory(equality)]) ).
cnf(46619,plain,
op1(e13,e10) != e14,
inference('REWRITE',[status(thm)],[182,46618,theory(equality)]) ).
cnf(46620,plain,
op1(e13,e10) = e13,
inference('REWRITE',[status(thm)],[46543,46619]) ).
cnf(46641,plain,
( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e14,e11) = e13 ),
inference('REWRITE',[status(thm)],[46517,382,46618,374,46610,theory(equality)]) ).
cnf(46646,plain,
( op1(e13,e11) = e12
| op1(e13,e12) = e12 ),
inference('REWRITE',[status(thm)],[46541,374,46610,46602,theory(equality)]) ).
cnf(46647,plain,
op1(e13,e12) = e14,
inference('REWRITE',[status(thm)],[46572,382,46620,46602,theory(equality)]) ).
cnf(46648,plain,
op1(e10,e12) != e14,
inference('REWRITE',[status(thm)],[195,46647,theory(equality)]) ).
cnf(46651,plain,
op1(e11,e12) != e14,
inference('REWRITE',[status(thm)],[198,46647,theory(equality)]) ).
cnf(46652,plain,
( op1(e11,e12) = e12
| op1(e11,e12) = e13 ),
inference('REWRITE',[status(thm)],[16041,46651]) ).
cnf(46657,plain,
op1(e13,e11) = e12,
inference('REWRITE',[status(thm)],[46646,381,46647,theory(equality)]) ).
cnf(46658,plain,
op1(e14,e11) != e12,
inference('REWRITE',[status(thm)],[192,46657,theory(equality)]) ).
cnf(46659,plain,
op1(e14,e13) = e12,
inference('REWRITE',[status(thm)],[46551,46658]) ).
cnf(46660,plain,
op1(e10,e13) != e12,
inference('REWRITE',[status(thm)],[206,46659,theory(equality)]) ).
cnf(46661,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e14 ),
inference('REWRITE',[status(thm)],[46486,46660]) ).
cnf(46664,plain,
( op1(e11,e13) = e12
| op1(e14,e11) = e13 ),
inference('REWRITE',[status(thm)],[46641,46660]) ).
cnf(46666,plain,
op1(e11,e13) != e12,
inference('REWRITE',[status(thm)],[209,46659,theory(equality)]) ).
cnf(46667,plain,
( op1(e11,e13) = e13
| op1(e11,e13) = e14 ),
inference('REWRITE',[status(thm)],[16059,46666]) ).
cnf(46674,plain,
op1(e14,e11) = e13,
inference('REWRITE',[status(thm)],[46664,46666]) ).
cnf(46678,plain,
( op1(e10,e13) = e14
| op1(e10,e14) = e14 ),
inference('REWRITE',[status(thm)],[31982,46648,379,46480,theory(equality)]) ).
cnf(47345,plain,
( h17(e13) = e20
| h16(e11) = e20
| h8(e10) != op2(h8(e10),h8(e10))
| h18(e13) != op2(h8(e10),h18(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e13)) != op2(h8(e10),h18(e11))
| h8(op1(e10,e14)) != op2(h8(e10),e24)
| h18(e13) != op2(h18(e13),h8(e10))
| h8(op1(e11,e12)) != op2(h18(e13),e21)
| h8(op1(e11,e13)) != op2(h18(e13),h18(e11))
| h8(op1(e11,e14)) != op2(h18(e13),e24)
| e21 != op2(e21,h8(e10))
| e24 != op2(e21,h18(e13))
| h8(e10) != e20
| h18(e13) != op2(e21,h18(e11))
| h18(e11) != op2(h18(e11),h8(e10))
| e21 != op2(h18(e11),h18(e13))
| e24 != op2(h18(e11),e21)
| h8(e10) != h18(e10)
| h18(e13) != op2(h18(e11),e24)
| e24 != op2(e24,h8(e10))
| h18(e11) != op2(e24,h18(e13))
| e21 != op2(e24,h18(e11))
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[34521,46617,46659,46674,46618,46601,46610,46647,46657,578,46620,46483,46521,503,46565,502,46536,580,46480,theory(equality)]) ).
cnf(50882,plain,
op1(e10,e12) = e12,
inference('REWRITE',[status(thm)],[30,31979,theory(equality)]) ).
cnf(50883,plain,
op1(e11,e12) != e12,
inference('REWRITE',[status(thm)],[193,50882,theory(equality)]) ).
cnf(50884,plain,
op1(e11,e12) = e13,
inference('REWRITE',[status(thm)],[46652,50883]) ).
cnf(50885,plain,
op1(e11,e13) != e13,
inference('REWRITE',[status(thm)],[240,50884,theory(equality)]) ).
cnf(50886,plain,
op1(e11,e13) = e14,
inference('REWRITE',[status(thm)],[46667,50885]) ).
cnf(50887,plain,
op1(e10,e13) != e14,
inference('REWRITE',[status(thm)],[203,50886,theory(equality)]) ).
cnf(50888,plain,
op1(e10,e13) = e13,
inference('REWRITE',[status(thm)],[46661,50887]) ).
cnf(50889,plain,
op1(e10,e14) = e14,
inference('REWRITE',[status(thm)],[46678,50887]) ).
cnf(50890,plain,
op1(e11,e14) != e14,
inference('REWRITE',[status(thm)],[213,50889,theory(equality)]) ).
cnf(50891,plain,
op1(e11,e14) = e12,
inference('REWRITE',[status(thm)],[16062,50890]) ).
cnf(51289,plain,
( h17(e13) = e20
| h16(e11) = e20
| h8(e10) != op2(h8(e10),h8(e10))
| h18(e13) != op2(h8(e10),h18(e13))
| e21 != op2(h8(e10),e21)
| h18(e11) != op2(h8(e10),h18(e11))
| e24 != op2(h8(e10),e24)
| h18(e13) != op2(h18(e13),h8(e10))
| h18(e11) != op2(h18(e13),e21)
| e24 != op2(h18(e13),h18(e11))
| e21 != op2(h18(e13),e24)
| e21 != op2(e21,h8(e10))
| e24 != op2(e21,h18(e13))
| h8(e10) != e20
| h18(e13) != op2(e21,h18(e11))
| h18(e11) != op2(h18(e11),h8(e10))
| e21 != op2(h18(e11),h18(e13))
| e24 != op2(h18(e11),e21)
| h8(e10) != h18(e10)
| h18(e13) != op2(h18(e11),e24)
| e24 != op2(e24,h8(e10))
| h18(e11) != op2(e24,h18(e13))
| e21 != op2(e24,h18(e11))
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[47345,50891,50886,50884,503,50889,578,50888,502,50882,theory(equality)]) ).
cnf(53290,plain,
( unit2 = e20
| unit2 = e21
| unit2 = e22 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[115,16413,theory(equality)]),15917,14724,theory(equality)]) ).
cnf(53291,plain,
( unit2 = e20
| unit2 = e21 ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[121,53290,theory(equality)]),389,462,theory(equality)]) ).
cnf(53298,plain,
unit2 = e20,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[115,53291,theory(equality)]),383,15831,theory(equality)]) ).
cnf(53299,plain,
op2(e20,e20) = e20,
inference('REWRITE',[status(thm)],[113,53298,theory(equality)]) ).
cnf(53300,plain,
h17(e11) != e20,
inference('REWRITE',[status(thm)],[15443,53299,theory(equality)]) ).
cnf(53301,plain,
( h17(e11) = e21
| h17(e11) = e22
| h17(e11) = e24 ),
inference('REWRITE',[status(thm)],[15762,53300]) ).
cnf(53303,plain,
( h16(e13) = e20
| h17(e13) = e24 ),
inference('REWRITE',[status(thm)],[16394,53300]) ).
cnf(53314,plain,
( h2(e13) = e20
| h13(e11) = e20
| h2(e11) != e20 ),
inference('REWRITE',[status(thm)],[16632,53300]) ).
cnf(53419,plain,
h17(e13) != e20,
inference('REWRITE',[status(thm)],[15446,53299,theory(equality)]) ).
cnf(53445,plain,
( h16(e11) = e20
| h8(e10) != op2(h8(e10),h8(e10))
| h18(e13) != op2(h8(e10),h18(e13))
| e21 != op2(h8(e10),e21)
| h18(e11) != op2(h8(e10),h18(e11))
| e24 != op2(h8(e10),e24)
| h18(e13) != op2(h18(e13),h8(e10))
| h18(e11) != op2(h18(e13),e21)
| e24 != op2(h18(e13),h18(e11))
| e21 != op2(h18(e13),e24)
| e21 != op2(e21,h8(e10))
| e24 != op2(e21,h18(e13))
| h8(e10) != e20
| h18(e13) != op2(e21,h18(e11))
| h18(e11) != op2(h18(e11),h8(e10))
| e21 != op2(h18(e11),h18(e13))
| e24 != op2(h18(e11),e21)
| h8(e10) != h18(e10)
| h18(e13) != op2(h18(e11),e24)
| e24 != op2(e24,h8(e10))
| h18(e11) != op2(e24,h18(e13))
| e21 != op2(e24,h18(e11))
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[51289,53419]) ).
cnf(53536,plain,
h13(e11) != e20,
inference('REWRITE',[status(thm)],[15516,53299,theory(equality)]) ).
cnf(53537,plain,
( h13(e11) = e21
| h13(e11) = e22
| h13(e11) = e23
| h13(e11) = e24 ),
inference('REWRITE',[status(thm)],[15506,53536]) ).
cnf(53599,plain,
( h2(e13) = e20
| h2(e11) != e20 ),
inference('REWRITE',[status(thm)],[53314,53536]) ).
cnf(53674,plain,
h13(e13) != e20,
inference('REWRITE',[status(thm)],[15525,53299,theory(equality)]) ).
cnf(53676,plain,
( h13(e13) = e22
| h13(e13) = e23
| h13(e13) = e24 ),
inference('REWRITE',[status(thm)],[15915,53674]) ).
cnf(53809,plain,
h2(e13) != e20,
inference('REWRITE',[status(thm)],[15591,53299,theory(equality)]) ).
cnf(53812,plain,
( h11(e11) = e20
| h2(e11) = e22 ),
inference('REWRITE',[status(thm)],[16400,53809]) ).
cnf(53848,plain,
h2(e11) != e20,
inference('REWRITE',[status(thm)],[53599,53809]) ).
cnf(53849,plain,
( op2(e22,e22) = e20
| h11(e13) = e20 ),
inference('REWRITE',[status(thm)],[15880,53848]) ).
cnf(54508,plain,
h1(e13) = e21,
inference('REWRITE',[status(thm)],[114,468,53298,theory(equality)]) ).
cnf(54509,plain,
op2(e20,e21) = e21,
inference('REWRITE',[status(thm)],[468,54508,theory(equality)]) ).
cnf(54512,plain,
h10(e13) != e21,
inference('REWRITE',[status(thm)],[15670,54508,theory(equality)]) ).
cnf(54513,plain,
( h10(e13) = e22
| h10(e13) = e24 ),
inference('REWRITE',[status(thm)],[15881,54512]) ).
cnf(54514,plain,
h11(e13) = e21,
inference('REWRITE',[status(thm)],[15913,54512]) ).
cnf(54515,plain,
op2(e22,e23) = e21,
inference('REWRITE',[status(thm)],[527,54514,theory(equality)]) ).
cnf(54518,plain,
h19(e10) != e21,
inference('REWRITE',[status(thm)],[15003,54514,theory(equality)]) ).
cnf(54519,plain,
( h19(e10) = e20
| h19(e10) = e22
| h19(e10) = e23 ),
inference('REWRITE',[status(thm)],[15770,54518]) ).
cnf(54520,plain,
( h14(e13) = e21
| h16(e13) = e21 ),
inference('REWRITE',[status(thm)],[15916,54518]) ).
cnf(54619,plain,
h13(e11) != e21,
inference('REWRITE',[status(thm)],[15513,54514,theory(equality)]) ).
cnf(54620,plain,
( h13(e11) = e22
| h13(e11) = e23
| h13(e11) = e24 ),
inference('REWRITE',[status(thm)],[53537,54619]) ).
cnf(54780,plain,
op2(e22,e22) = e20,
inference('REWRITE',[status(thm)],[53849,383,54514,theory(equality)]) ).
cnf(54781,plain,
h11(e11) != e20,
inference('REWRITE',[status(thm)],[15008,54780,theory(equality)]) ).
cnf(54824,plain,
h2(e11) = e22,
inference('REWRITE',[status(thm)],[53812,54781]) ).
cnf(54825,plain,
op2(e22,e20) = e22,
inference('REWRITE',[status(thm)],[472,54824,theory(equality)]) ).
cnf(54827,plain,
h13(e13) != e22,
inference('REWRITE',[status(thm)],[15597,54824,theory(equality)]) ).
cnf(54828,plain,
( h14(e13) = e22
| h11(e11) = e22
| h19(e10) = e22
| h16(e13) = e22 ),
inference('REWRITE',[status(thm)],[15522,54827]) ).
cnf(54853,plain,
( h13(e13) = e23
| h13(e13) = e24 ),
inference('REWRITE',[status(thm)],[53676,54827]) ).
cnf(54867,plain,
h17(e13) != e22,
inference('REWRITE',[status(thm)],[15598,54824,theory(equality)]) ).
cnf(54868,plain,
( h18(e13) = e22
| h16(e11) = e22 ),
inference('REWRITE',[status(thm)],[15828,54867]) ).
cnf(54879,plain,
h10(e13) != e22,
inference('REWRITE',[status(thm)],[15599,54824,theory(equality)]) ).
cnf(54880,plain,
h10(e13) = e24,
inference('REWRITE',[status(thm)],[54513,54879]) ).
cnf(54882,plain,
op2(e22,e21) = e24,
inference('REWRITE',[status(thm)],[15067,54880,theory(equality)]) ).
cnf(54883,plain,
h14(e13) != e24,
inference('REWRITE',[status(thm)],[15379,54880,theory(equality)]) ).
cnf(54884,plain,
( h13(e13) = e24
| h11(e11) = e24
| h16(e13) = e24 ),
inference('REWRITE',[status(thm)],[15772,54883]) ).
cnf(55385,plain,
h18(e10) = e20,
inference('REWRITE',[status(thm)],[31758,54780,theory(equality)]) ).
cnf(55410,plain,
( h16(e11) = e20
| h8(e10) != op2(h8(e10),h8(e10))
| h18(e13) != op2(h8(e10),h18(e13))
| e21 != op2(h8(e10),e21)
| h18(e11) != op2(h8(e10),h18(e11))
| e24 != op2(h8(e10),e24)
| h18(e13) != op2(h18(e13),h8(e10))
| h18(e11) != op2(h18(e13),e21)
| e24 != op2(h18(e13),h18(e11))
| e21 != op2(h18(e13),e24)
| e21 != op2(e21,h8(e10))
| e24 != op2(e21,h18(e13))
| h8(e10) != e20
| h18(e13) != op2(e21,h18(e11))
| h18(e11) != op2(h18(e11),h8(e10))
| e21 != op2(h18(e11),h18(e13))
| e24 != op2(h18(e11),e21)
| h18(e13) != op2(h18(e11),e24)
| e24 != op2(e24,h8(e10))
| h18(e11) != op2(e24,h18(e13))
| e21 != op2(e24,h18(e11))
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[53445,55385,theory(equality)]) ).
cnf(55489,plain,
h14(e13) != e21,
inference('REWRITE',[status(thm)],[15671,54508,theory(equality)]) ).
cnf(55490,plain,
h16(e13) = e21,
inference('REWRITE',[status(thm)],[54520,55489]) ).
cnf(55491,plain,
op2(e23,e24) = e21,
inference('REWRITE',[status(thm)],[564,55490,theory(equality)]) ).
cnf(55494,plain,
h17(e11) != e21,
inference('REWRITE',[status(thm)],[15441,55490,theory(equality)]) ).
cnf(55495,plain,
( h17(e11) = e22
| h17(e11) = e24 ),
inference('REWRITE',[status(thm)],[53301,55494]) ).
cnf(55520,plain,
h17(e13) = e24,
inference('REWRITE',[status(thm)],[53303,383,55490,theory(equality)]) ).
cnf(55522,plain,
op2(e24,e20) = e24,
inference('REWRITE',[status(thm)],[14439,55520,theory(equality)]) ).
cnf(55571,plain,
h13(e13) != e24,
inference('REWRITE',[status(thm)],[15526,55520,theory(equality)]) ).
cnf(55572,plain,
h13(e13) = e23,
inference('REWRITE',[status(thm)],[54853,55571]) ).
cnf(55574,plain,
op2(e23,e20) = e23,
inference('REWRITE',[status(thm)],[14836,55572,theory(equality)]) ).
cnf(55576,plain,
h11(e11) != e23,
inference('REWRITE',[status(thm)],[15528,55572,theory(equality)]) ).
cnf(55577,plain,
h19(e10) != e22,
inference('REWRITE',[status(thm)],[15011,55576]) ).
cnf(55578,plain,
( h19(e10) = e20
| h19(e10) = e23 ),
inference('REWRITE',[status(thm)],[54519,55577]) ).
cnf(55605,plain,
h19(e10) != e23,
inference('REWRITE',[status(thm)],[15529,55572,theory(equality)]) ).
cnf(55607,plain,
h19(e10) = e20,
inference('REWRITE',[status(thm)],[55578,55605]) ).
cnf(55608,plain,
op2(e23,e23) = e20,
inference('REWRITE',[status(thm)],[584,55607,theory(equality)]) ).
cnf(55609,plain,
h16(e11) != e20,
inference('REWRITE',[status(thm)],[14609,55607,theory(equality)]) ).
cnf(55628,plain,
( h8(e10) != op2(h8(e10),h8(e10))
| h18(e13) != op2(h8(e10),h18(e13))
| e21 != op2(h8(e10),e21)
| h18(e11) != op2(h8(e10),h18(e11))
| e24 != op2(h8(e10),e24)
| h18(e13) != op2(h18(e13),h8(e10))
| h18(e11) != op2(h18(e13),e21)
| e24 != op2(h18(e13),h18(e11))
| e21 != op2(h18(e13),e24)
| e21 != op2(e21,h8(e10))
| e24 != op2(e21,h18(e13))
| h8(e10) != e20
| h18(e13) != op2(e21,h18(e11))
| h18(e11) != op2(h18(e11),h8(e10))
| e21 != op2(h18(e11),h18(e13))
| e24 != op2(h18(e11),e21)
| h18(e13) != op2(h18(e11),e24)
| e24 != op2(e24,h8(e10))
| h18(e11) != op2(e24,h18(e13))
| e21 != op2(e24,h18(e11))
| h18(e11) != e22
| h18(e13) != e23 ),
inference('REWRITE',[status(thm)],[55410,55609]) ).
cnf(55661,plain,
( h18(e13) = e23
| h16(e11) = e23 ),
inference('REWRITE',[status(thm)],[15796,392,55520,theory(equality)]) ).
cnf(55673,plain,
( h14(e13) = e22
| h11(e11) = e22 ),
inference('REWRITE',[status(thm)],[54828,387,384,55607,55490,theory(equality)]) ).
cnf(55674,plain,
h11(e11) = e24,
inference('REWRITE',[status(thm)],[54884,389,392,55572,55490,theory(equality)]) ).
cnf(55675,plain,
op2(e23,e22) = e24,
inference('REWRITE',[status(thm)],[526,55674,theory(equality)]) ).
cnf(55678,plain,
h10(e11) != e24,
inference('REWRITE',[status(thm)],[15372,55674,theory(equality)]) ).
cnf(55679,plain,
( h10(e11) = e22
| h10(e11) = e23 ),
inference('REWRITE',[status(thm)],[15878,55678]) ).
cnf(55688,plain,
h14(e13) = e22,
inference('REWRITE',[status(thm)],[55673,391,55674,theory(equality)]) ).
cnf(55690,plain,
op2(e23,e21) = e22,
inference('REWRITE',[status(thm)],[14667,55688,theory(equality)]) ).
cnf(55691,plain,
h18(e13) != e22,
inference('REWRITE',[status(thm)],[15310,55688,theory(equality)]) ).
cnf(55692,plain,
h16(e11) = e22,
inference('REWRITE',[status(thm)],[54868,55691]) ).
cnf(55693,plain,
op2(e24,e23) = e22,
inference('REWRITE',[status(thm)],[563,55692,theory(equality)]) ).
cnf(55696,plain,
h14(e11) != e22,
inference('REWRITE',[status(thm)],[15304,55692,theory(equality)]) ).
cnf(55697,plain,
( h14(e11) = e23
| h14(e11) = e24 ),
inference('REWRITE',[status(thm)],[15919,55696]) ).
cnf(55709,plain,
h13(e11) != e22,
inference('REWRITE',[status(thm)],[15515,55692,theory(equality)]) ).
cnf(55710,plain,
( h13(e11) = e23
| h13(e11) = e24 ),
inference('REWRITE',[status(thm)],[54620,55709]) ).
cnf(55715,plain,
h18(e13) = e23,
inference('REWRITE',[status(thm)],[55661,390,55692,theory(equality)]) ).
cnf(55718,plain,
h8(e10) = e20,
inference('REWRITE',[status(thm)],[15246,55608,55715,theory(equality)]) ).
cnf(55719,plain,
( h13(e11) != e23
| h18(e11) != op2(e20,h18(e11))
| h17(e11) != e24
| h18(e11) != e22
| e24 != op2(e23,h18(e11))
| h14(e11) != e24
| e23 != op2(e21,h18(e11))
| h18(e11) != op2(h18(e11),e20)
| e21 != op2(h18(e11),e23)
| e24 != op2(h18(e11),e21)
| e23 != op2(h18(e11),e24)
| e21 != op2(e24,h18(e11)) ),
inference('REWRITE',[status(thm)],[55628,55693,55522,14724,15907,55491,55690,55574,14494,54509,14891,53299,55718,55715,theory(equality)]) ).
cnf(55744,plain,
h2(e13) = e22,
inference('REWRITE',[status(thm)],[116,473,53298,theory(equality)]) ).
cnf(55745,plain,
op2(e20,e22) = e22,
inference('REWRITE',[status(thm)],[473,55744,theory(equality)]) ).
cnf(55748,plain,
h10(e11) != e22,
inference('REWRITE',[status(thm)],[15588,55744,theory(equality)]) ).
cnf(55749,plain,
h10(e11) = e23,
inference('REWRITE',[status(thm)],[55679,55748]) ).
cnf(55751,plain,
op2(e21,e22) = e23,
inference('REWRITE',[status(thm)],[15124,55749,theory(equality)]) ).
cnf(55753,plain,
h14(e11) != e23,
inference('REWRITE',[status(thm)],[15374,55749,theory(equality)]) ).
cnf(55754,plain,
h14(e11) = e24,
inference('REWRITE',[status(thm)],[55697,55753]) ).
cnf(55758,plain,
h18(e11) != e24,
inference('REWRITE',[status(thm)],[15306,55754,theory(equality)]) ).
cnf(55759,plain,
h18(e11) = e22,
inference('REWRITE',[status(thm)],[15922,55758]) ).
cnf(55762,plain,
h17(e11) != e22,
inference('REWRITE',[status(thm)],[15440,55759,theory(equality)]) ).
cnf(55763,plain,
h17(e11) = e24,
inference('REWRITE',[status(thm)],[55495,55762]) ).
cnf(55767,plain,
h13(e11) != e24,
inference('REWRITE',[status(thm)],[15517,55763,theory(equality)]) ).
cnf(55768,plain,
h13(e11) = e23,
inference('REWRITE',[status(thm)],[55710,55767]) ).
cnf(55772,plain,
$false,
inference('REWRITE',[status(thm)],[55719,462,463,54882,54515,54825,55751,55675,55763,55745,55759,55768,55754,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : ALG049+1 : TPTP v8.1.0. Released v2.7.0.
% 0.07/0.07 % Command : run-snark %s %d
% 0.07/0.26 % Computer : n026.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % WCLimit : 600
% 0.07/0.26 % DateTime : Wed Jun 8 18:33:17 EDT 2022
% 0.07/0.26 % CPUTime :
% 0.10/0.32 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.33 *
% 0.10/0.33 *
% 0.10/0.33 #<PACKAGE "SNARK-USER">
% 0.10/0.33 *
% 0.10/0.33 SNARK-TPTP-OPTIONS
% 0.10/0.33 *
% 0.10/0.33 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.10/0.33 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.10/0.33 (USE-FACTORING :POS)
% 0.10/0.33 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.10/0.33 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.10/0.33 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.10/0.33 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.10/0.33 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.10/0.33 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.10/0.33 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.10/0.33 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.10/0.33 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.10/0.33 (DECLARE-TPTP-SYMBOLS2))
% 0.10/0.33 *
% 0.10/0.33 "."
% 0.10/0.33 *
% 0.10/0.33 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-08T18:33:17
% 0.10/0.33 ; 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-08T18:33:17
% 266.88/267.07
% 266.88/267.07
% 266.88/267.07 #||
% 266.88/267.07 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 266.88/267.07 % SZS output start Refutation
% See solution above
% 266.94/267.14 ||#
% 266.94/267.14
% 266.94/267.14 ; Summary of computation:
% 266.94/267.14 ; 132939 formulas have been input or derived (from 1019 formulas).
% 266.94/267.14 ; 55772 (42%) were retained. Of these,
% 266.94/267.14 ; 55574 (100%) were simplified or subsumed later,
% 266.94/267.14 ; 198 ( 0%) are still being kept.
% 266.94/267.14 ;
% 266.94/267.14 ; Run time in seconds excluding printing time:
% 266.94/267.14 ; 0.069 0% Read assertion file (1 call)
% 266.94/267.14 ; 44.750 17% Assert (36 calls)
% 266.94/267.14 ; 28.409 11% Process new row (125,025 calls)
% 266.94/267.14 ; 1.595 1% Resolution (2,036 calls)
% 266.94/267.14 ; 2.022 1% Paramodulation (1,018 calls)
% 266.94/267.14 ; 0.003 0% Factoring (142 calls)
% 266.94/267.14 ; 0.312 0% Condensing (57,725 calls)
% 266.94/267.14 ; 65.625 25% Forward subsumption (57,725 calls)
% 266.94/267.14 ; 14.716 6% Backward subsumption (47,196 calls)
% 266.94/267.14 ; 22.037 8% Clause clause subsumption (157,263 calls)
% 266.94/267.14 ; 69.500 26% Forward simplification (124,980 calls)
% 266.94/267.14 ; 16.542 6% Backward simplification (47,931 calls)
% 266.94/267.14 ; 0.315 0% Ordering (216,547 calls)
% 266.94/267.14 ; 0.000 0% Sortal reasoning (32 calls)
% 266.94/267.14 ; 0.326 0% Purity testing (1 call)
% 266.94/267.14 ; 0.517 0% Other
% 266.94/267.14 ; 266.738 Total
% 266.94/267.14 ; 266.812 Real time
% 266.94/267.14 ;
% 266.94/267.14 ; Term-hash-array has 4,064 terms in all.
% 266.94/267.14 ; Feature-vector-row-index has 0 entries (15,849 at peak, 47,196 added, 47,196 deleted).
% 266.94/267.14 ; Feature-vector-row-index has 1 node (202,746 at peak, 597,921 added, 597,920 deleted).
% 266.94/267.14 ; Retrieved 153,182 possibly forward subsuming rows in 57,725 calls.
% 266.94/267.14 ; Retrieved 59,857 possibly backward subsumed rows in 47,196 calls.
% 266.94/267.14 ; Path-index has 359 entries (3,218 at peak, 18,549 added, 18,190 deleted).
% 266.94/267.14 ; Path-index has 542 nodes (1,102 at peak, 4,974 added, 4,432 deleted).
% 266.94/267.14 ; Trie-index has 359 entries (3,218 at peak, 18,549 added, 18,190 deleted).
% 266.94/267.14 ; Trie-index has 585 nodes (6,697 at peak, 40,197 added, 39,612 deleted).
% 266.94/267.14 ; Retrieved 2,845,291 generalization terms in 14,746,003 calls.
% 266.94/267.14 ; Retrieved 734 instance terms in 734 calls.
% 266.94/267.14 ; Retrieved 6,875 unifiable terms in 26,108 calls.
% 266.94/267.14 ;
% 266.94/267.14 ; The agenda of backward simplifiable rows to process has 59 entries:
% 266.94/267.14 ; 59 with value 0
% 266.94/267.14 ; The agenda of rows to process has 3 entries:
% 266.94/267.14 ; 2 with value 15 1 with value 16
% 266.94/267.14 ; The agenda of input rows to give has 70 entries:
% 266.94/267.14 ; 49 with value 6 21 with value 7
% 266.94/267.14 ; The agenda of rows to give has 4 entries:
% 266.94/267.14 ; 2 with value (4 7) 1 with value (4 8) 1 with value (4 10)
% 266.94/267.14 Evaluation took:
% 266.94/267.14 266.812 seconds of real time
% 266.94/267.14 261.1698 seconds of user run time
% 266.94/267.14 5.64278 seconds of system run time
% 266.94/267.14 [Run times include 25.767 seconds GC run time.]
% 266.94/267.14 0 calls to %EVAL
% 266.94/267.14 0 page faults and
% 266.94/267.14 21,431,616,560 bytes consed.
% 266.94/267.14 :PROOF-FOUND
% 266.94/267.14 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-08T18:37:44
% 266.94/267.14 :PROOF-FOUND
% 266.94/267.14 *
%------------------------------------------------------------------------------