%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ALG105+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n025.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:53 EDT 2022
% Result : Theorem 3.71s 3.91s
% Output : Refutation 3.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 102
% Syntax : Number of clauses : 267 ( 187 unt; 68 nHn; 267 RR)
% Number of literals : 569 ( 568 equ; 266 neg)
% Maximal clause size : 20 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(4,axiom,
( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(5,axiom,
( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(12,axiom,
( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
cnf(18,axiom,
( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10
| op1(e13,e10) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(24,axiom,
( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e12,e10) = e13
| op1(e13,e10) = e13 ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(33,axiom,
( op1(e12,e10) = e10
| op1(e12,e11) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(40,axiom,
( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e12,e12) = e13
| op1(e13,e12) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(45,axiom,
( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(60,axiom,
( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
cnf(66,axiom,
( op2(e20,e20) = e20
| op2(e21,e20) = e20
| op2(e22,e20) = e20
| op2(e23,e20) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(67,axiom,
( op2(e20,e20) = e21
| op2(e20,e21) = e21
| op2(e20,e22) = e21
| op2(e20,e23) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(68,axiom,
( op2(e20,e20) = e21
| op2(e21,e20) = e21
| op2(e22,e20) = e21
| op2(e23,e20) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(69,axiom,
( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(70,axiom,
( op2(e20,e20) = e22
| op2(e21,e20) = e22
| op2(e22,e20) = e22
| op2(e23,e20) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(72,axiom,
( op2(e20,e20) = e23
| op2(e21,e20) = e23
| op2(e22,e20) = e23
| op2(e23,e20) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(97,axiom,
op1(e10,e10) != op1(e11,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(98,axiom,
op1(e10,e10) != op1(e12,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(110,axiom,
op1(e10,e12) != op1(e12,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(111,axiom,
op1(e10,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(115,axiom,
op1(e10,e13) != op1(e11,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(116,axiom,
op1(e10,e13) != op1(e12,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(117,axiom,
op1(e10,e13) != op1(e13,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(118,axiom,
op1(e11,e13) != op1(e12,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(119,axiom,
op1(e11,e13) != op1(e13,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(120,axiom,
op1(e12,e13) != op1(e13,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(123,axiom,
op1(e10,e10) != op1(e10,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(126,axiom,
op1(e10,e12) != op1(e10,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(127,axiom,
op1(e11,e10) != op1(e11,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(128,axiom,
op1(e11,e10) != op1(e11,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(129,axiom,
op1(e11,e10) != op1(e11,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(133,axiom,
op1(e12,e10) != op1(e12,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(136,axiom,
op1(e12,e11) != op1(e12,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(137,axiom,
op1(e12,e11) != op1(e12,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(142,axiom,
op1(e13,e11) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(153,axiom,
op2(e20,e21) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(159,axiom,
op2(e20,e22) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(163,axiom,
op2(e20,e23) != op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(164,axiom,
op2(e20,e23) != op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(165,axiom,
op2(e20,e23) != op2(e23,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(166,axiom,
op2(e21,e23) != op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(168,axiom,
op2(e22,e23) != op2(e23,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(169,axiom,
op2(e20,e20) != op2(e20,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(170,axiom,
op2(e20,e20) != op2(e20,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(171,axiom,
op2(e20,e20) != op2(e20,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(176,axiom,
op2(e21,e20) != op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(177,axiom,
op2(e21,e20) != op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(181,axiom,
op2(e22,e20) != op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(183,axiom,
op2(e22,e20) != op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(185,axiom,
op2(e22,e21) != op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(187,axiom,
op2(e23,e20) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(188,axiom,
op2(e23,e20) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(193,axiom,
e10 != e11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(194,axiom,
e10 != e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(195,axiom,
e10 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(196,axiom,
e11 != e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(197,axiom,
e11 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(198,axiom,
e12 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(199,axiom,
e20 != e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(200,axiom,
e20 != e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(201,axiom,
e20 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(202,axiom,
e21 != e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(203,axiom,
e21 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(204,axiom,
e22 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(223,axiom,
op1(op1(e10,e12),e10) = e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(230,axiom,
op1(op1(e12,e11),e12) = e11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(235,axiom,
op1(op1(e13,e12),e13) = e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(346,axiom,
( op1(e10,op1(e11,e10)) = op1(e11,e10)
| op1(e11,op1(e12,e11)) = op1(e12,e11)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| op1(e13,op1(e11,e13)) = op1(e11,e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(410,axiom,
( op1(e10,op1(e12,e10)) = op1(e12,e10)
| op1(e11,op1(e12,e11)) = op1(e12,e11)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| op1(e13,op1(e11,e13)) = op1(e11,e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(497,axiom,
op2(op2(e21,e20),e21) = e20,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(498,axiom,
op2(op2(e21,e21),e21) = e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(499,axiom,
op2(op2(e21,e22),e21) = e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(501,axiom,
op2(op2(e22,e20),e22) = e20,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(502,axiom,
op2(op2(e22,e21),e22) = e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(504,axiom,
op2(op2(e22,e23),e22) = e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(507,axiom,
op2(op2(e23,e22),e23) = e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(554,axiom,
( op2(e20,op2(e20,e20)) = op2(e20,e20)
| op2(e21,op2(e22,e21)) = op2(e22,e21)
| op2(e22,op2(e23,e22)) = op2(e23,e22)
| op2(e23,op2(e21,e23)) = op2(e21,e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(765,axiom,
e10 = op1(op1(e12,e11),op1(e12,e11)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(766,axiom,
op1(e12,e11) = e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(767,axiom,
e20 = op2(op2(e22,e21),op2(e22,e21)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(768,axiom,
op2(e22,e21) = e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(772,axiom,
h1(e13) = op2(e21,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(776,axiom,
h2(e13) = op2(e22,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
cnf(780,axiom,
h3(e13) = op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
cnf(784,axiom,
h4(e13) = op2(e20,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
cnf(787,axiom,
h5(e10) = op2(op2(e22,e21),op2(e22,e21)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
cnf(788,plain,
h5(e10) = op2(e23,e23),
inference('REWRITE',[status(thm)],[787,768,theory(equality)]) ).
cnf(794,axiom,
h6(e13) = op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
cnf(798,axiom,
h7(e13) = op2(e20,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
cnf(802,axiom,
h8(e13) = op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
cnf(805,axiom,
h9(e10) = op2(op2(e23,e22),op2(e23,e22)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
cnf(806,axiom,
h9(e13) = op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
cnf(810,axiom,
h10(e13) = op2(e20,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
cnf(813,axiom,
h11(e10) = op2(op2(e21,e23),op2(e21,e23)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
cnf(814,axiom,
h11(e13) = op2(e21,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
cnf(815,axiom,
h12(e11) = e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
cnf(816,axiom,
h12(e12) = e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
cnf(817,axiom,
h12(e10) = op2(op2(e22,e23),op2(e22,e23)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
cnf(818,axiom,
h12(e13) = op2(e22,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
cnf(1375,negated_conjecture,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| h12(e10) != e20
| h12(e13) != e21
| h12(e12) != e22
| h12(e11) != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
cnf(1376,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != h5(e10)
| h12(op1(e11,e12)) != h9(e13)
| h12(op1(e11,e13)) != op2(e23,h12(e13))
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != op2(e22,e22)
| h12(op1(e12,e13)) != op2(e22,h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),e23)
| h12(op1(e13,e12)) != op2(h12(e13),e22)
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| h12(e10) != e20
| h12(e13) != e21 ),
inference('REWRITE',[status(thm)],[1375,818,766,806,788,816,815,theory(equality)]) ).
cnf(1407,plain,
( h12(e13) = e20
| h12(e13) = e21
| h12(e13) = e22
| h12(e13) = e23 ),
inference('REWRITE',[status(thm)],[60,818,theory(equality)]) ).
cnf(1409,plain,
op2(h12(e13),e22) = e23,
inference('REWRITE',[status(thm)],[504,818,theory(equality)]) ).
cnf(1411,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != h5(e10)
| h12(op1(e11,e12)) != h9(e13)
| h12(op1(e11,e13)) != op2(e23,h12(e13))
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != op2(e22,e22)
| h12(op1(e12,e13)) != op2(e22,h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),e23)
| h12(op1(e13,e12)) != e23
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| h12(e10) != e20
| h12(e13) != e21 ),
inference('REWRITE',[status(thm)],[1376,1409,theory(equality)]) ).
cnf(1415,plain,
h12(e10) = op2(h12(e13),h12(e13)),
inference('REWRITE',[status(thm)],[817,818,theory(equality)]) ).
cnf(1417,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != h5(e10)
| h12(op1(e11,e12)) != h9(e13)
| h12(op1(e11,e13)) != op2(e23,h12(e13))
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != op2(e22,e22)
| h12(op1(e12,e13)) != op2(e22,h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),e23)
| h12(op1(e13,e12)) != e23
| h12(op1(e13,e13)) != h12(e10)
| h12(e10) != e20
| h12(e13) != e21 ),
inference('REWRITE',[status(thm)],[1411,1415,theory(equality)]) ).
cnf(1421,plain,
h11(e13) != h12(e13),
inference('REWRITE',[status(thm)],[166,818,814,theory(equality)]) ).
cnf(1429,plain,
h11(e10) = op2(h11(e13),h11(e13)),
inference('REWRITE',[status(thm)],[813,814,theory(equality)]) ).
cnf(1434,plain,
( h10(e13) = e20
| h10(e13) = e21
| h10(e13) = e22
| h10(e13) = e23 ),
inference('REWRITE',[status(thm)],[52,810,theory(equality)]) ).
cnf(1435,plain,
h10(e13) != h11(e13),
inference('REWRITE',[status(thm)],[163,814,810,theory(equality)]) ).
cnf(1436,plain,
h10(e13) != h12(e13),
inference('REWRITE',[status(thm)],[164,818,810,theory(equality)]) ).
cnf(1437,plain,
op2(e20,e20) != h10(e13),
inference('REWRITE',[status(thm)],[171,810,theory(equality)]) ).
cnf(1451,plain,
op2(h9(e13),e23) = e22,
inference('REWRITE',[status(thm)],[507,806,theory(equality)]) ).
cnf(1459,plain,
h9(e10) = op2(h9(e13),h9(e13)),
inference('REWRITE',[status(thm)],[805,806,theory(equality)]) ).
cnf(1469,plain,
op2(h8(e13),e21) = e22,
inference('REWRITE',[status(thm)],[499,802,theory(equality)]) ).
cnf(1489,plain,
h7(e13) != h9(e13),
inference('REWRITE',[status(thm)],[159,806,798,theory(equality)]) ).
cnf(1490,plain,
op2(e20,e20) != h7(e13),
inference('REWRITE',[status(thm)],[170,798,theory(equality)]) ).
cnf(1535,plain,
h10(e13) != h5(e10),
inference('REWRITE',[status(thm)],[165,810,788,theory(equality)]) ).
cnf(1537,plain,
h12(e13) != h5(e10),
inference('REWRITE',[status(thm)],[168,818,788,theory(equality)]) ).
cnf(1552,plain,
( op2(e20,e20) = e21
| h4(e13) = e21
| h7(e13) = e21
| h10(e13) = e21 ),
inference('REWRITE',[status(thm)],[67,810,798,784,theory(equality)]) ).
cnf(1553,plain,
( op2(e20,e20) = e22
| h4(e13) = e22
| h7(e13) = e22
| h10(e13) = e22 ),
inference('REWRITE',[status(thm)],[69,810,798,784,theory(equality)]) ).
cnf(1556,plain,
h4(e13) != h6(e13),
inference('REWRITE',[status(thm)],[153,794,784,theory(equality)]) ).
cnf(1557,plain,
op2(e20,e20) != h4(e13),
inference('REWRITE',[status(thm)],[169,784,theory(equality)]) ).
cnf(1592,plain,
h3(e13) != h6(e13),
inference('REWRITE',[status(thm)],[187,794,780,theory(equality)]) ).
cnf(1593,plain,
h3(e13) != h9(e13),
inference('REWRITE',[status(thm)],[188,806,780,theory(equality)]) ).
cnf(1657,plain,
h2(e13) != h12(e13),
inference('REWRITE',[status(thm)],[183,818,776,theory(equality)]) ).
cnf(1658,plain,
op2(h2(e13),e22) = e20,
inference('REWRITE',[status(thm)],[501,776,theory(equality)]) ).
cnf(1717,plain,
( op2(e20,e20) = e20
| h1(e13) = e20
| h2(e13) = e20
| h3(e13) = e20 ),
inference('REWRITE',[status(thm)],[66,780,776,772,theory(equality)]) ).
cnf(1718,plain,
( op2(e20,e20) = e21
| h1(e13) = e21
| h2(e13) = e21
| h3(e13) = e21 ),
inference('REWRITE',[status(thm)],[68,780,776,772,theory(equality)]) ).
cnf(1719,plain,
( op2(e20,e20) = e22
| h1(e13) = e22
| h2(e13) = e22
| h3(e13) = e22 ),
inference('REWRITE',[status(thm)],[70,780,776,772,theory(equality)]) ).
cnf(1720,plain,
( op2(e20,e20) = e23
| h1(e13) = e23
| h2(e13) = e23
| h3(e13) = e23 ),
inference('REWRITE',[status(thm)],[72,780,776,772,theory(equality)]) ).
cnf(1729,plain,
h1(e13) != h8(e13),
inference('REWRITE',[status(thm)],[176,802,772,theory(equality)]) ).
cnf(1730,plain,
h1(e13) != h11(e13),
inference('REWRITE',[status(thm)],[177,814,772,theory(equality)]) ).
cnf(1731,plain,
op2(h1(e13),e21) = e20,
inference('REWRITE',[status(thm)],[497,772,theory(equality)]) ).
cnf(1804,plain,
h2(e13) != e23,
inference('REWRITE',[status(thm)],[181,776,768,theory(equality)]) ).
cnf(1806,plain,
( op2(e20,e20) = e23
| h1(e13) = e23
| h3(e13) = e23 ),
inference('REWRITE',[status(thm)],[1720,1804]) ).
cnf(1810,plain,
h12(e13) != e23,
inference('REWRITE',[status(thm)],[185,818,768,theory(equality)]) ).
cnf(1811,plain,
( h12(e13) = e20
| h12(e13) = e21
| h12(e13) = e22 ),
inference('REWRITE',[status(thm)],[1407,1810]) ).
cnf(1813,plain,
h9(e13) = e21,
inference('REWRITE',[status(thm)],[502,806,768,theory(equality)]) ).
cnf(1814,plain,
op2(e23,e22) = e21,
inference('REWRITE',[status(thm)],[806,1813,theory(equality)]) ).
cnf(1816,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != h5(e10)
| h12(op1(e11,e12)) != e21
| h12(op1(e11,e13)) != op2(e23,h12(e13))
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != op2(e22,e22)
| h12(op1(e12,e13)) != op2(e22,h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),e23)
| h12(op1(e13,e12)) != e23
| h12(op1(e13,e13)) != h12(e10)
| h12(e10) != e20
| h12(e13) != e21 ),
inference('REWRITE',[status(thm)],[1417,1813,theory(equality)]) ).
cnf(1822,plain,
h11(e13) = e22,
inference('REWRITE',[status(thm)],[1451,814,1813,theory(equality)]) ).
cnf(1823,plain,
op2(e21,e23) = e22,
inference('REWRITE',[status(thm)],[814,1822,theory(equality)]) ).
cnf(1824,plain,
h12(e13) != e22,
inference('REWRITE',[status(thm)],[1421,1822,theory(equality)]) ).
cnf(1826,plain,
( h12(e13) = e20
| h12(e13) = e21 ),
inference('REWRITE',[status(thm)],[1811,1824]) ).
cnf(1831,plain,
h11(e10) = op2(e22,e22),
inference('REWRITE',[status(thm)],[1429,1822,theory(equality)]) ).
cnf(1883,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != h5(e10)
| h12(op1(e11,e12)) != e21
| h12(op1(e11,e13)) != op2(e23,h12(e13))
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != h11(e10)
| h12(op1(e12,e13)) != op2(e22,h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),e23)
| h12(op1(e13,e12)) != e23
| h12(op1(e13,e13)) != h12(e10)
| h12(e10) != e20
| h12(e13) != e21 ),
inference('REWRITE',[status(thm)],[1816,1831,theory(equality)]) ).
cnf(1892,plain,
h10(e13) != e22,
inference('REWRITE',[status(thm)],[1435,1822,theory(equality)]) ).
cnf(1893,plain,
( h10(e13) = e20
| h10(e13) = e21
| h10(e13) = e23 ),
inference('REWRITE',[status(thm)],[1434,1892]) ).
cnf(1894,plain,
( op2(e20,e20) = e22
| h4(e13) = e22
| h7(e13) = e22 ),
inference('REWRITE',[status(thm)],[1553,1892]) ).
cnf(1933,plain,
h1(e13) != e22,
inference('REWRITE',[status(thm)],[1730,1822,theory(equality)]) ).
cnf(1935,plain,
( op2(e20,e20) = e22
| h2(e13) = e22
| h3(e13) = e22 ),
inference('REWRITE',[status(thm)],[1719,1933]) ).
cnf(1949,plain,
h9(e10) = op2(e21,e21),
inference('REWRITE',[status(thm)],[1459,1813,theory(equality)]) ).
cnf(1950,plain,
op2(h9(e10),e21) = e21,
inference('REWRITE',[status(thm)],[498,1949,theory(equality)]) ).
cnf(1992,plain,
h7(e13) != e21,
inference('REWRITE',[status(thm)],[1489,1813,theory(equality)]) ).
cnf(1994,plain,
( op2(e20,e20) = e21
| h4(e13) = e21
| h10(e13) = e21 ),
inference('REWRITE',[status(thm)],[1552,1992]) ).
cnf(2008,plain,
h3(e13) != e21,
inference('REWRITE',[status(thm)],[1593,1813,theory(equality)]) ).
cnf(2010,plain,
( op2(e20,e20) = e21
| h1(e13) = e21
| h2(e13) = e21 ),
inference('REWRITE',[status(thm)],[1718,2008]) ).
cnf(2038,plain,
op2(e20,op2(e20,e20)) = op2(e20,e20),
inference('REWRITE',[status(thm)],[554,202,203,1814,204,1823,768,theory(equality)]) ).
cnf(2069,plain,
h5(e10) = e20,
inference('REWRITE',[status(thm)],[767,788,768,theory(equality)]) ).
cnf(2073,plain,
h10(e13) != e20,
inference('REWRITE',[status(thm)],[1535,2069,theory(equality)]) ).
cnf(2075,plain,
( h10(e13) = e21
| h10(e13) = e23 ),
inference('REWRITE',[status(thm)],[1893,2073]) ).
cnf(2076,plain,
h12(e13) != e20,
inference('REWRITE',[status(thm)],[1537,2069,theory(equality)]) ).
cnf(2077,plain,
h12(e13) = e21,
inference('REWRITE',[status(thm)],[1826,2076]) ).
cnf(2079,plain,
h8(e13) = e23,
inference('REWRITE',[status(thm)],[1409,802,2077,theory(equality)]) ).
cnf(2081,plain,
h6(e13) = e22,
inference('REWRITE',[status(thm)],[1469,794,2079,theory(equality)]) ).
cnf(2082,plain,
op2(e23,e21) = e22,
inference('REWRITE',[status(thm)],[794,2081,theory(equality)]) ).
cnf(2084,plain,
h4(e13) != e22,
inference('REWRITE',[status(thm)],[1556,2081,theory(equality)]) ).
cnf(2086,plain,
( op2(e20,e20) = e22
| h7(e13) = e22 ),
inference('REWRITE',[status(thm)],[1894,2084]) ).
cnf(2087,plain,
h3(e13) != e22,
inference('REWRITE',[status(thm)],[1592,2081,theory(equality)]) ).
cnf(2088,plain,
( op2(e20,e20) = e22
| h2(e13) = e22 ),
inference('REWRITE',[status(thm)],[1935,2087]) ).
cnf(2095,plain,
h1(e13) != e23,
inference('REWRITE',[status(thm)],[1729,2079,theory(equality)]) ).
cnf(2096,plain,
( op2(e20,e20) = e23
| h3(e13) = e23 ),
inference('REWRITE',[status(thm)],[1806,2095]) ).
cnf(2101,plain,
h12(e10) = h9(e10),
inference('REWRITE',[status(thm)],[1415,1949,2077,theory(equality)]) ).
cnf(2102,plain,
h12(e10) = op2(e21,e21),
inference('REWRITE',[status(thm)],[1949,2101,theory(equality)]) ).
cnf(2103,plain,
op2(h12(e10),e21) = e21,
inference('REWRITE',[status(thm)],[1950,2101,theory(equality)]) ).
cnf(2116,plain,
h10(e13) != e21,
inference('REWRITE',[status(thm)],[1436,2077,theory(equality)]) ).
cnf(2117,plain,
( op2(e20,e20) = e21
| h4(e13) = e21 ),
inference('REWRITE',[status(thm)],[1994,2116]) ).
cnf(2118,plain,
h10(e13) = e23,
inference('REWRITE',[status(thm)],[2075,2116]) ).
cnf(2119,plain,
op2(e20,e23) = e23,
inference('REWRITE',[status(thm)],[810,2118,theory(equality)]) ).
cnf(2120,plain,
op2(e20,e20) != e23,
inference('REWRITE',[status(thm)],[1437,2118,theory(equality)]) ).
cnf(2122,plain,
h3(e13) = e23,
inference('REWRITE',[status(thm)],[2096,2120]) ).
cnf(2123,plain,
op2(e23,e20) = e23,
inference('REWRITE',[status(thm)],[780,2122,theory(equality)]) ).
cnf(2125,plain,
( op2(e20,e20) = e20
| h1(e13) = e20
| h2(e13) = e20 ),
inference('REWRITE',[status(thm)],[1717,201,2122,theory(equality)]) ).
cnf(2128,plain,
h2(e13) != e21,
inference('REWRITE',[status(thm)],[1657,2077,theory(equality)]) ).
cnf(2130,plain,
( op2(e20,e20) = e21
| h1(e13) = e21 ),
inference('REWRITE',[status(thm)],[2010,2128]) ).
cnf(2133,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e10,e13)) != e21
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != e20
| h12(op1(e11,e12)) != e21
| h12(op1(e11,e13)) != e22
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != h11(e10)
| h12(op1(e12,e13)) != e23
| h12(op1(e13,e10)) != op2(e21,h12(e10))
| h12(op1(e13,e11)) != e22
| h12(op1(e13,e12)) != e23
| h12(op1(e13,e13)) != h12(e10)
| h12(e10) != e20 ),
inference('REWRITE',[status(thm)],[1883,1823,768,2082,2103,2077,2069,theory(equality)]) ).
cnf(2139,plain,
( op1(e10,e11) = e10
| op1(e11,e11) = e10
| op1(e13,e11) = e10 ),
inference('REWRITE',[status(thm)],[26,195,766,theory(equality)]) ).
cnf(2140,plain,
( op1(e10,e11) = e11
| op1(e11,e11) = e11
| op1(e13,e11) = e11 ),
inference('REWRITE',[status(thm)],[28,197,766,theory(equality)]) ).
cnf(2142,plain,
( op1(e12,e10) = e10
| op1(e12,e12) = e10
| op1(e12,e13) = e10 ),
inference('REWRITE',[status(thm)],[33,195,766,theory(equality)]) ).
cnf(2154,plain,
op1(e12,e10) != e13,
inference('REWRITE',[status(thm)],[133,766,theory(equality)]) ).
cnf(2156,plain,
( op1(e10,e10) = e13
| op1(e11,e10) = e13
| op1(e13,e10) = e13 ),
inference('REWRITE',[status(thm)],[24,2154]) ).
cnf(2157,plain,
op1(e12,e12) != e13,
inference('REWRITE',[status(thm)],[136,766,theory(equality)]) ).
cnf(2159,plain,
( op1(e10,e12) = e13
| op1(e11,e12) = e13
| op1(e13,e12) = e13 ),
inference('REWRITE',[status(thm)],[40,2157]) ).
cnf(2160,plain,
op1(e12,e13) != e13,
inference('REWRITE',[status(thm)],[137,766,theory(equality)]) ).
cnf(2161,plain,
( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12 ),
inference('REWRITE',[status(thm)],[12,2160]) ).
cnf(2163,plain,
op1(e13,e12) = e11,
inference('REWRITE',[status(thm)],[230,766,theory(equality)]) ).
cnf(2167,plain,
( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e13) = e12 ),
inference('REWRITE',[status(thm)],[45,196,2163,theory(equality)]) ).
cnf(2168,plain,
op1(e10,e12) != e11,
inference('REWRITE',[status(thm)],[111,2163,theory(equality)]) ).
cnf(2169,plain,
( op1(e10,e12) = e10
| op1(e10,e12) = e12
| op1(e10,e12) = e13 ),
inference('REWRITE',[status(thm)],[3,2168]) ).
cnf(2180,plain,
op1(e13,e11) != e11,
inference('REWRITE',[status(thm)],[142,2163,theory(equality)]) ).
cnf(2181,plain,
( op1(e10,e11) = e11
| op1(e11,e11) = e11 ),
inference('REWRITE',[status(thm)],[2140,2180]) ).
cnf(2186,plain,
op1(e11,e13) = e12,
inference('REWRITE',[status(thm)],[235,2163,theory(equality)]) ).
cnf(2189,plain,
op1(e10,e13) != e12,
inference('REWRITE',[status(thm)],[115,2186,theory(equality)]) ).
cnf(2190,plain,
( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e13 ),
inference('REWRITE',[status(thm)],[4,2189]) ).
cnf(2192,plain,
op1(e12,e13) != e12,
inference('REWRITE',[status(thm)],[118,2186,theory(equality)]) ).
cnf(2194,plain,
( op1(e12,e13) = e10
| op1(e12,e13) = e11 ),
inference('REWRITE',[status(thm)],[2161,2192]) ).
cnf(2195,plain,
op1(e13,e13) != e12,
inference('REWRITE',[status(thm)],[119,2186,theory(equality)]) ).
cnf(2196,plain,
( op1(e13,e10) = e12
| op1(e13,e11) = e12 ),
inference('REWRITE',[status(thm)],[2167,2195]) ).
cnf(2198,plain,
op1(e11,e10) != e12,
inference('REWRITE',[status(thm)],[129,2186,theory(equality)]) ).
cnf(2199,plain,
( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e13 ),
inference('REWRITE',[status(thm)],[5,2198]) ).
cnf(2276,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e10,e13)) != e21
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != e20
| h12(op1(e11,e12)) != e21
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != h11(e10)
| h12(op1(e12,e13)) != e23
| h12(op1(e13,e10)) != op2(e21,h12(e10))
| h12(op1(e13,e11)) != e22
| h12(op1(e13,e13)) != h12(e10)
| h12(e10) != e20 ),
inference('REWRITE',[status(thm)],[2133,815,816,2186,2163,theory(equality)]) ).
cnf(2282,plain,
( op1(e10,e12) = e13
| op1(e11,e12) = e13 ),
inference('REWRITE',[status(thm)],[2159,197,2163,theory(equality)]) ).
cnf(2298,plain,
op1(e10,op1(e11,e10)) = op1(e11,e10),
inference('REWRITE',[status(thm)],[346,196,197,2163,198,2186,766,theory(equality)]) ).
cnf(2306,plain,
op1(e10,op1(e12,e10)) = op1(e12,e10),
inference('REWRITE',[status(thm)],[410,196,197,2163,198,2186,766,theory(equality)]) ).
cnf(2315,plain,
op1(e13,e13) = e10,
inference('REWRITE',[status(thm)],[765,766,theory(equality)]) ).
cnf(2316,plain,
op1(e10,e13) != e10,
inference('REWRITE',[status(thm)],[117,2315,theory(equality)]) ).
cnf(2318,plain,
( op1(e10,e13) = e11
| op1(e10,e13) = e13 ),
inference('REWRITE',[status(thm)],[2190,2316]) ).
cnf(2319,plain,
op1(e12,e13) != e10,
inference('REWRITE',[status(thm)],[120,2315,theory(equality)]) ).
cnf(2320,plain,
( op1(e12,e10) = e10
| op1(e12,e12) = e10 ),
inference('REWRITE',[status(thm)],[2142,2319]) ).
cnf(2321,plain,
op1(e12,e13) = e11,
inference('REWRITE',[status(thm)],[2194,2319]) ).
cnf(2322,plain,
op1(e10,e13) != e11,
inference('REWRITE',[status(thm)],[116,2321,theory(equality)]) ).
cnf(2324,plain,
op1(e10,e13) = e13,
inference('REWRITE',[status(thm)],[2318,2322]) ).
cnf(2325,plain,
op1(e10,e10) != e13,
inference('REWRITE',[status(thm)],[123,2324,theory(equality)]) ).
cnf(2327,plain,
( op1(e11,e10) = e13
| op1(e13,e10) = e13 ),
inference('REWRITE',[status(thm)],[2156,2325]) ).
cnf(2328,plain,
op1(e10,e12) != e13,
inference('REWRITE',[status(thm)],[126,2324,theory(equality)]) ).
cnf(2329,plain,
( op1(e10,e12) = e10
| op1(e10,e12) = e12 ),
inference('REWRITE',[status(thm)],[2169,2328]) ).
cnf(2330,plain,
op1(e11,e12) = e13,
inference('REWRITE',[status(thm)],[2282,2328]) ).
cnf(2331,plain,
op1(e11,e10) != e13,
inference('REWRITE',[status(thm)],[128,2330,theory(equality)]) ).
cnf(2332,plain,
( op1(e11,e10) = e10
| op1(e11,e10) = e11 ),
inference('REWRITE',[status(thm)],[2199,2331]) ).
cnf(2333,plain,
op1(e13,e10) = e13,
inference('REWRITE',[status(thm)],[2327,2331]) ).
cnf(2334,plain,
( op1(e10,e10) = e10
| op1(e11,e10) = e10
| op1(e12,e10) = e10 ),
inference('REWRITE',[status(thm)],[18,195,2333,theory(equality)]) ).
cnf(2335,plain,
op1(e13,e11) = e12,
inference('REWRITE',[status(thm)],[2196,198,2333,theory(equality)]) ).
cnf(2339,plain,
( op1(e10,e11) = e10
| op1(e11,e11) = e10 ),
inference('REWRITE',[status(thm)],[2139,194,2335,theory(equality)]) ).
cnf(2351,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != e20
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != h11(e10)
| e21 != op2(e21,h12(e10))
| h12(e10) != e20 ),
inference('REWRITE',[status(thm)],[2276,816,2335,2333,815,2321,2330,2077,2324,2315,theory(equality)]) ).
cnf(2395,plain,
h7(e13) = e22,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[2038,2086,theory(equality)]),798,theory(equality)]) ).
cnf(2396,plain,
op2(e20,e22) = e22,
inference('REWRITE',[status(thm)],[798,2395,theory(equality)]) ).
cnf(2397,plain,
op2(e20,e20) != e22,
inference('REWRITE',[status(thm)],[1490,2395,theory(equality)]) ).
cnf(2398,plain,
h2(e13) = e22,
inference('REWRITE',[status(thm)],[2088,2397]) ).
cnf(2399,plain,
op2(e22,e20) = e22,
inference('REWRITE',[status(thm)],[776,2398,theory(equality)]) ).
cnf(2400,plain,
h11(e10) = e20,
inference('REWRITE',[status(thm)],[1658,1831,2398,theory(equality)]) ).
cnf(2403,plain,
( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),e23)
| h12(op1(e10,e12)) != op2(h12(e10),e22)
| h12(op1(e11,e10)) != op2(e23,h12(e10))
| h12(op1(e11,e11)) != e20
| h12(op1(e12,e10)) != op2(e22,h12(e10))
| h12(op1(e12,e12)) != e20
| e21 != op2(e21,h12(e10))
| h12(e10) != e20 ),
inference('REWRITE',[status(thm)],[2351,2400,theory(equality)]) ).
cnf(2409,plain,
( op2(e20,e20) = e20
| h1(e13) = e20 ),
inference('REWRITE',[status(thm)],[2125,200,2398,theory(equality)]) ).
cnf(2415,plain,
h4(e13) = e21,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[2038,2117,theory(equality)]),784,theory(equality)]) ).
cnf(2417,plain,
op2(e20,e20) != e21,
inference('REWRITE',[status(thm)],[1557,2415,theory(equality)]) ).
cnf(2418,plain,
h1(e13) = e21,
inference('REWRITE',[status(thm)],[2130,2417]) ).
cnf(2419,plain,
op2(e21,e20) = e21,
inference('REWRITE',[status(thm)],[772,2418,theory(equality)]) ).
cnf(2420,plain,
h12(e10) = e20,
inference('REWRITE',[status(thm)],[1731,2102,2418,theory(equality)]) ).
cnf(2424,plain,
( h12(op1(e10,e10)) != op2(e20,e20)
| h12(op1(e10,e11)) != e23
| h12(op1(e10,e12)) != e22
| h12(op1(e11,e10)) != e23
| h12(op1(e11,e11)) != e20
| h12(op1(e12,e10)) != e22
| h12(op1(e12,e12)) != e20 ),
inference('REWRITE',[status(thm)],[2403,2419,2399,2123,2396,2119,2420,theory(equality)]) ).
cnf(2427,plain,
op2(e20,e20) = e20,
inference('REWRITE',[status(thm)],[2409,199,2418,theory(equality)]) ).
cnf(2428,plain,
( h12(op1(e10,e10)) != e20
| h12(op1(e10,e11)) != e23
| h12(op1(e10,e12)) != e22
| h12(op1(e11,e10)) != e23
| h12(op1(e11,e11)) != e20
| h12(op1(e12,e10)) != e22
| h12(op1(e12,e12)) != e20 ),
inference('REWRITE',[status(thm)],[2424,2427,theory(equality)]) ).
cnf(2468,plain,
( op1(e10,e10) = e10
| op1(e11,e10) = e10 ),
inference('PARAMODULATE',[status(thm)],[2306,2334,theory(equality)]) ).
cnf(2583,plain,
op1(e10,e10) = e10,
inference('PARAMODULATE',[status(thm)],[2298,2468,theory(equality)]) ).
cnf(2584,plain,
op1(e11,e10) != e10,
inference('REWRITE',[status(thm)],[97,2583,theory(equality)]) ).
cnf(2585,plain,
op1(e11,e10) = e11,
inference('REWRITE',[status(thm)],[2332,2584]) ).
cnf(2586,plain,
op1(e11,e11) != e11,
inference('REWRITE',[status(thm)],[127,2585,theory(equality)]) ).
cnf(2587,plain,
op1(e10,e11) = e11,
inference('REWRITE',[status(thm)],[2181,2586]) ).
cnf(2588,plain,
op1(e11,e11) = e10,
inference('REWRITE',[status(thm)],[2339,193,2587,theory(equality)]) ).
cnf(2589,plain,
op1(e12,e10) != e10,
inference('REWRITE',[status(thm)],[98,2583,theory(equality)]) ).
cnf(2590,plain,
op1(e12,e12) = e10,
inference('REWRITE',[status(thm)],[2320,2589]) ).
cnf(2591,plain,
op1(e10,e12) != e10,
inference('REWRITE',[status(thm)],[110,2590,theory(equality)]) ).
cnf(2592,plain,
op1(e10,e12) = e12,
inference('REWRITE',[status(thm)],[2329,2591]) ).
cnf(2593,plain,
op1(e12,e10) = e12,
inference('REWRITE',[status(thm)],[223,2592,theory(equality)]) ).
cnf(2594,plain,
$false,
inference('REWRITE',[status(thm)],[2428,2590,2593,2588,2585,816,2592,815,2587,2420,2583,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : ALG105+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jun 9 06:41:05 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.18/0.45 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.46 *
% 0.18/0.46 *
% 0.18/0.46 #<PACKAGE "SNARK-USER">
% 0.18/0.46 *
% 0.18/0.46 SNARK-TPTP-OPTIONS
% 0.18/0.46 *
% 0.18/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.18/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.18/0.46 (USE-FACTORING :POS)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.18/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.18/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.18/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.18/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.18/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.18/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.18/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.18/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.18/0.46 *
% 0.18/0.46 "."
% 0.18/0.46 *
% 0.18/0.46 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-09T06:41:05
% 0.18/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n025.cluster.edu at 2022-06-09T06:41:05
% 3.71/3.91
% 3.71/3.91
% 3.71/3.91 #||
% 3.71/3.91 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.71/3.91 % SZS output start Refutation
% See solution above
% 3.76/3.93 ||#
% 3.76/3.93
% 3.76/3.93 ; Summary of computation:
% 3.76/3.93 ; 6615 formulas have been input or derived (from 253 formulas).
% 3.76/3.93 ; 2594 (39%) were retained. Of these,
% 3.76/3.93 ; 2485 (96%) were simplified or subsumed later,
% 3.76/3.93 ; 109 ( 4%) are still being kept.
% 3.76/3.93 ;
% 3.76/3.93 ; Run time in seconds excluding printing time:
% 3.76/3.93 ; 0.070 2% Read assertion file (1 call)
% 3.76/3.93 ; 1.182 34% Assert (26 calls)
% 3.76/3.93 ; 0.298 9% Process new row (6,052 calls)
% 3.76/3.93 ; 0.008 0% Resolution (504 calls)
% 3.76/3.93 ; 0.007 0% Paramodulation (252 calls)
% 3.76/3.93 ; 0.000 0% Factoring (44 calls)
% 3.76/3.93 ; 0.009 0% Condensing (2,238 calls)
% 3.76/3.93 ; 0.184 5% Forward subsumption (2,238 calls)
% 3.76/3.93 ; 0.153 4% Backward subsumption (1,770 calls)
% 3.76/3.93 ; 0.092 3% Clause clause subsumption (7,313 calls)
% 3.76/3.93 ; 1.274 37% Forward simplification (6,043 calls)
% 3.76/3.93 ; 0.119 3% Backward simplification (2,188 calls)
% 3.76/3.93 ; 0.002 0% Ordering (2,442 calls)
% 3.76/3.93 ; 0.000 0% Sortal reasoning (32 calls)
% 3.76/3.93 ; 0.011 0% Purity testing (1 call)
% 3.76/3.93 ; 0.032 1% Other
% 3.76/3.93 ; 3.441 Total
% 3.76/3.93 ; 3.466 Real time
% 3.76/3.93 ;
% 3.76/3.93 ; Term-hash-array has 1,407 terms in all.
% 3.76/3.93 ; Feature-vector-row-index has 0 entries (608 at peak, 1,770 added, 1,770 deleted).
% 3.76/3.93 ; Feature-vector-row-index has 1 node (3,236 at peak, 14,677 added, 14,676 deleted).
% 3.76/3.93 ; Retrieved 4,205 possibly forward subsuming rows in 2,238 calls.
% 3.76/3.93 ; Retrieved 3,754 possibly backward subsumed rows in 1,770 calls.
% 3.76/3.93 ; Path-index has 196 entries (987 at peak, 4,964 added, 4,768 deleted).
% 3.76/3.93 ; Path-index has 326 nodes (666 at peak, 2,660 added, 2,334 deleted).
% 3.76/3.93 ; Trie-index has 196 entries (987 at peak, 4,964 added, 4,768 deleted).
% 3.76/3.93 ; Trie-index has 329 nodes (2,347 at peak, 12,596 added, 12,267 deleted).
% 3.76/3.93 ; Retrieved 71,962 generalization terms in 345,933 calls.
% 3.76/3.93 ; Retrieved 417 instance terms in 417 calls.
% 3.76/3.93 ; Retrieved 475 unifiable terms in 1,536 calls.
% 3.76/3.93 ;
% 3.76/3.93 ; The agenda of backward simplifiable rows to process has 134 entries:
% 3.76/3.93 ; 134 with value 0
% 3.76/3.93 ; The agenda of rows to process has 18 entries:
% 3.76/3.93 ; 3 with value 13 1 with value 17 6 with value 69
% 3.76/3.93 ; 3 with value 16 5 with value 20
% 3.76/3.93 ; The agenda of input rows to give has 6 entries:
% 3.76/3.93 ; 6 with value 7
% 3.76/3.93 ; The agenda of rows to give has 1 entry:
% 3.76/3.93 ; 1 with value (4 9)
% 3.76/3.93 Evaluation took:
% 3.76/3.93 3.466 seconds of real time
% 3.76/3.93 3.404378 seconds of user run time
% 3.76/3.93 0.060958 seconds of system run time
% 3.76/3.93 [Run times include 0.087 seconds GC run time.]
% 3.76/3.93 0 calls to %EVAL
% 3.76/3.93 0 page faults and
% 3.76/3.93 229,452,304 bytes consed.
% 3.76/3.93 :PROOF-FOUND
% 3.76/3.93 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-09T06:41:09
% 3.76/3.93 :PROOF-FOUND
% 3.76/3.93 *
%------------------------------------------------------------------------------