%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : ALG142+1 : TPTP v5.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art07.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 04:01:41 EST 2010
% Result : Unsatisfiable 4.18s
% Output : CNFRefutation 4.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 110
% Number of leaves : 11
% Syntax : Number of formulae : 647 ( 61 unt; 0 def)
% Number of atoms : 3075 (3068 equ)
% Maximal formula atoms : 256 ( 4 avg)
% Number of connectives : 2902 ( 474 ~;2236 |; 192 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 68 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(7,axiom,
~ ( e2 = op(e0,op(e0,e0))
& e1 = op(op(e0,e0),e0)
& e3 = op(e0,e0) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax21) ).
fof(11,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax2) ).
fof(12,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax3) ).
fof(13,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax1) ).
fof(16,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax4) ).
fof(17,axiom,
( ( ( op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e1,e1) = e0
& op(e1,e0) != e1 )
| ( op(e2,e2) = e0
& op(e2,e0) != e2 )
| ( op(e3,e3) = e0
& op(e3,e0) != e3 ) )
& ( ( op(e0,e0) = e1
& op(e0,e1) != e0 )
| ( op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e2,e2) = e1
& op(e2,e1) != e2 )
| ( op(e3,e3) = e1
& op(e3,e1) != e3 ) )
& ( ( op(e0,e0) = e2
& op(e0,e2) != e0 )
| ( op(e1,e1) = e2
& op(e1,e2) != e1 )
| ( op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e3,e3) = e2
& op(e3,e2) != e3 ) )
& ( ( op(e0,e0) = e3
& op(e0,e3) != e0 )
| ( op(e1,e1) = e3
& op(e1,e3) != e1 )
| ( op(e2,e2) = e3
& op(e2,e3) != e2 )
| ( op(e3,e3) = e3
& op(e3,e3) != e3 ) ) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax5) ).
fof(18,axiom,
~ ( e0 = op(e3,op(e3,e3))
& e2 = op(op(e3,e3),e3)
& e1 = op(e3,e3) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax8) ).
fof(21,axiom,
~ ( e1 = op(e0,op(e0,e0))
& e2 = op(op(e0,e0),e0)
& e3 = op(e0,e0) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax15) ).
fof(26,axiom,
~ ( e1 = op(e3,op(e3,e3))
& e0 = op(op(e3,e3),e3)
& e2 = op(e3,e3) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax12) ).
fof(27,axiom,
~ ( e1 = op(e2,op(e2,e2))
& e0 = op(op(e2,e2),e2)
& e3 = op(e2,e2) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax13) ).
fof(28,axiom,
~ ( e2 = op(e3,op(e3,e3))
& e0 = op(op(e3,e3),e3)
& e1 = op(e3,e3) ),
file('/tmp/tmpRvTI-8/sel_ALG142+1.p_1',ax18) ).
fof(42,plain,
( e2 != op(e0,op(e0,e0))
| e1 != op(op(e0,e0),e0)
| e3 != op(e0,e0) ),
inference(fof_nnf,[status(thm)],[7]) ).
cnf(43,plain,
( e3 != op(e0,e0)
| e1 != op(op(e0,e0),e0)
| e2 != op(e0,op(e0,e0)) ),
inference(split_conjunct,[status(thm)],[42]) ).
cnf(50,plain,
( op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(52,plain,
( op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(53,plain,
( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(54,plain,
( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(55,plain,
( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(56,plain,
( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(57,plain,
( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(60,plain,
( op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(61,plain,
( op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(62,plain,
( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(63,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(65,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(67,plain,
( op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(68,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(69,plain,
( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(70,plain,
( op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(71,plain,
( op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(72,plain,
( op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(73,plain,
( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(74,plain,
( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(76,plain,
( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(77,plain,
( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(78,plain,
( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(80,plain,
( op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(81,plain,
( op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(82,plain,
op(e3,e2) != op(e3,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(83,plain,
op(e3,e1) != op(e3,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(84,plain,
op(e3,e1) != op(e3,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(85,plain,
op(e3,e0) != op(e3,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(86,plain,
op(e3,e0) != op(e3,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(87,plain,
op(e3,e0) != op(e3,e1),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(88,plain,
op(e2,e2) != op(e2,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(90,plain,
op(e2,e1) != op(e2,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(91,plain,
op(e2,e0) != op(e2,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(92,plain,
op(e2,e0) != op(e2,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(94,plain,
op(e1,e2) != op(e1,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(95,plain,
op(e1,e1) != op(e1,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(96,plain,
op(e1,e1) != op(e1,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(97,plain,
op(e1,e0) != op(e1,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(99,plain,
op(e1,e0) != op(e1,e1),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(100,plain,
op(e0,e2) != op(e0,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(101,plain,
op(e0,e1) != op(e0,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(103,plain,
op(e0,e0) != op(e0,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(104,plain,
op(e0,e0) != op(e0,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(105,plain,
op(e0,e0) != op(e0,e1),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(106,plain,
op(e2,e3) != op(e3,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(107,plain,
op(e1,e3) != op(e3,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(108,plain,
op(e1,e3) != op(e2,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(109,plain,
op(e0,e3) != op(e3,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(110,plain,
op(e0,e3) != op(e2,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(111,plain,
op(e0,e3) != op(e1,e3),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(112,plain,
op(e2,e2) != op(e3,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(113,plain,
op(e1,e2) != op(e3,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(114,plain,
op(e1,e2) != op(e2,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(115,plain,
op(e0,e2) != op(e3,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(116,plain,
op(e0,e2) != op(e2,e2),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(118,plain,
op(e2,e1) != op(e3,e1),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(119,plain,
op(e1,e1) != op(e3,e1),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(120,plain,
op(e1,e1) != op(e2,e1),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(123,plain,
op(e0,e1) != op(e1,e1),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(124,plain,
op(e2,e0) != op(e3,e0),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(125,plain,
op(e1,e0) != op(e3,e0),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(126,plain,
op(e1,e0) != op(e2,e0),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(127,plain,
op(e0,e0) != op(e3,e0),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(128,plain,
op(e0,e0) != op(e2,e0),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(129,plain,
op(e0,e0) != op(e1,e0),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(131,plain,
( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(132,plain,
( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(133,plain,
( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(134,plain,
( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(135,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(137,plain,
( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(138,plain,
( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(139,plain,
( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(141,plain,
( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(142,plain,
( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(143,plain,
( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(145,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(150,plain,
e2 != e3,
inference(split_conjunct,[status(thm)],[16]) ).
cnf(151,plain,
e1 != e3,
inference(split_conjunct,[status(thm)],[16]) ).
cnf(152,plain,
e1 != e2,
inference(split_conjunct,[status(thm)],[16]) ).
cnf(153,plain,
e0 != e3,
inference(split_conjunct,[status(thm)],[16]) ).
cnf(154,plain,
e0 != e2,
inference(split_conjunct,[status(thm)],[16]) ).
cnf(155,plain,
e0 != e1,
inference(split_conjunct,[status(thm)],[16]) ).
fof(156,plain,
( ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 )
& ( op(e3,e0) != e3
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) = e0 )
& ( op(e3,e3) = e0
| op(e2,e0) != e2
| op(e1,e1) = e0
| op(e0,e0) = e0 )
& ( op(e3,e0) != e3
| op(e2,e0) != e2
| op(e1,e1) = e0
| op(e0,e0) = e0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e0) != e1
| op(e0,e0) = e0 )
& ( op(e3,e0) != e3
| op(e2,e2) = e0
| op(e1,e0) != e1
| op(e0,e0) = e0 )
& ( op(e3,e3) = e0
| op(e2,e0) != e2
| op(e1,e0) != e1
| op(e0,e0) = e0 )
& ( op(e3,e0) != e3
| op(e2,e0) != e2
| op(e1,e0) != e1
| op(e0,e0) = e0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) != e0 )
& ( op(e3,e0) != e3
| op(e2,e2) = e0
| op(e1,e1) = e0
| op(e0,e0) != e0 )
& ( op(e3,e3) = e0
| op(e2,e0) != e2
| op(e1,e1) = e0
| op(e0,e0) != e0 )
& ( op(e3,e0) != e3
| op(e2,e0) != e2
| op(e1,e1) = e0
| op(e0,e0) != e0 )
& ( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e0) != e1
| op(e0,e0) != e0 )
& ( op(e3,e0) != e3
| op(e2,e2) = e0
| op(e1,e0) != e1
| op(e0,e0) != e0 )
& ( op(e3,e3) = e0
| op(e2,e0) != e2
| op(e1,e0) != e1
| op(e0,e0) != e0 )
& ( op(e3,e0) != e3
| op(e2,e0) != e2
| op(e1,e0) != e1
| op(e0,e0) != e0 )
& ( op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e1) != e3
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e3) = e1
| op(e2,e1) != e2
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e1) != e3
| op(e2,e1) != e2
| op(e1,e1) = e1
| op(e0,e0) = e1 )
& ( op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) != e1
| op(e0,e0) = e1 )
& ( op(e3,e1) != e3
| op(e2,e2) = e1
| op(e1,e1) != e1
| op(e0,e0) = e1 )
& ( op(e3,e3) = e1
| op(e2,e1) != e2
| op(e1,e1) != e1
| op(e0,e0) = e1 )
& ( op(e3,e1) != e3
| op(e2,e1) != e2
| op(e1,e1) != e1
| op(e0,e0) = e1 )
& ( op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e1) != e0 )
& ( op(e3,e1) != e3
| op(e2,e2) = e1
| op(e1,e1) = e1
| op(e0,e1) != e0 )
& ( op(e3,e3) = e1
| op(e2,e1) != e2
| op(e1,e1) = e1
| op(e0,e1) != e0 )
& ( op(e3,e1) != e3
| op(e2,e1) != e2
| op(e1,e1) = e1
| op(e0,e1) != e0 )
& ( op(e3,e3) = e1
| op(e2,e2) = e1
| op(e1,e1) != e1
| op(e0,e1) != e0 )
& ( op(e3,e1) != e3
| op(e2,e2) = e1
| op(e1,e1) != e1
| op(e0,e1) != e0 )
& ( op(e3,e3) = e1
| op(e2,e1) != e2
| op(e1,e1) != e1
| op(e0,e1) != e0 )
& ( op(e3,e1) != e3
| op(e2,e1) != e2
| op(e1,e1) != e1
| op(e0,e1) != e0 )
& ( op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e2) != e3
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e3) = e2
| op(e2,e2) != e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e2) != e3
| op(e2,e2) != e2
| op(e1,e1) = e2
| op(e0,e0) = e2 )
& ( op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e2) != e1
| op(e0,e0) = e2 )
& ( op(e3,e2) != e3
| op(e2,e2) = e2
| op(e1,e2) != e1
| op(e0,e0) = e2 )
& ( op(e3,e3) = e2
| op(e2,e2) != e2
| op(e1,e2) != e1
| op(e0,e0) = e2 )
& ( op(e3,e2) != e3
| op(e2,e2) != e2
| op(e1,e2) != e1
| op(e0,e0) = e2 )
& ( op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e2) != e0 )
& ( op(e3,e2) != e3
| op(e2,e2) = e2
| op(e1,e1) = e2
| op(e0,e2) != e0 )
& ( op(e3,e3) = e2
| op(e2,e2) != e2
| op(e1,e1) = e2
| op(e0,e2) != e0 )
& ( op(e3,e2) != e3
| op(e2,e2) != e2
| op(e1,e1) = e2
| op(e0,e2) != e0 )
& ( op(e3,e3) = e2
| op(e2,e2) = e2
| op(e1,e2) != e1
| op(e0,e2) != e0 )
& ( op(e3,e2) != e3
| op(e2,e2) = e2
| op(e1,e2) != e1
| op(e0,e2) != e0 )
& ( op(e3,e3) = e2
| op(e2,e2) != e2
| op(e1,e2) != e1
| op(e0,e2) != e0 )
& ( op(e3,e2) != e3
| op(e2,e2) != e2
| op(e1,e2) != e1
| op(e0,e2) != e0 )
& ( op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e3) != e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e3) = e3
| op(e2,e3) != e2
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e3) != e3
| op(e2,e3) != e2
| op(e1,e1) = e3
| op(e0,e0) = e3 )
& ( op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e3) != e1
| op(e0,e0) = e3 )
& ( op(e3,e3) != e3
| op(e2,e2) = e3
| op(e1,e3) != e1
| op(e0,e0) = e3 )
& ( op(e3,e3) = e3
| op(e2,e3) != e2
| op(e1,e3) != e1
| op(e0,e0) = e3 )
& ( op(e3,e3) != e3
| op(e2,e3) != e2
| op(e1,e3) != e1
| op(e0,e0) = e3 )
& ( op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e3) != e0 )
& ( op(e3,e3) != e3
| op(e2,e2) = e3
| op(e1,e1) = e3
| op(e0,e3) != e0 )
& ( op(e3,e3) = e3
| op(e2,e3) != e2
| op(e1,e1) = e3
| op(e0,e3) != e0 )
& ( op(e3,e3) != e3
| op(e2,e3) != e2
| op(e1,e1) = e3
| op(e0,e3) != e0 )
& ( op(e3,e3) = e3
| op(e2,e2) = e3
| op(e1,e3) != e1
| op(e0,e3) != e0 )
& ( op(e3,e3) != e3
| op(e2,e2) = e3
| op(e1,e3) != e1
| op(e0,e3) != e0 )
& ( op(e3,e3) = e3
| op(e2,e3) != e2
| op(e1,e3) != e1
| op(e0,e3) != e0 )
& ( op(e3,e3) != e3
| op(e2,e3) != e2
| op(e1,e3) != e1
| op(e0,e3) != e0 ) ),
inference(distribute,[status(thm)],[17]) ).
cnf(163,plain,
( op(e1,e1) = e3
| op(e2,e2) = e3
| op(e0,e3) != e0
| op(e3,e3) != e3 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(164,plain,
( op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e0,e3) != e0 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(167,plain,
( op(e0,e0) = e3
| op(e2,e2) = e3
| op(e1,e3) != e1
| op(e3,e3) != e3 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(168,plain,
( op(e0,e0) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3
| op(e1,e3) != e1 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(169,plain,
( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e3) != e2
| op(e3,e3) != e3 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(170,plain,
( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e3,e3) = e3
| op(e2,e3) != e2 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(171,plain,
( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) != e3 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(172,plain,
( op(e0,e0) = e3
| op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e3 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(182,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e1,e2) != e1
| op(e2,e2) != e2 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(184,plain,
( op(e0,e0) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2
| op(e1,e2) != e1 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(186,plain,
( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e3,e3) = e2
| op(e2,e2) != e2 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(188,plain,
( op(e0,e0) = e2
| op(e1,e1) = e2
| op(e2,e2) = e2
| op(e3,e3) = e2 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(192,plain,
( op(e2,e2) = e1
| op(e3,e3) = e1
| op(e0,e1) != e0
| op(e1,e1) != e1 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(196,plain,
( op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e0,e1) != e0 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(198,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e1,e1) != e1
| op(e2,e1) != e2 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(199,plain,
( op(e0,e0) = e1
| op(e2,e2) = e1
| op(e1,e1) != e1
| op(e3,e1) != e3 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(200,plain,
( op(e0,e0) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1
| op(e1,e1) != e1 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(202,plain,
( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e3,e3) = e1
| op(e2,e1) != e2 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(203,plain,
( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e1) != e3 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(204,plain,
( op(e0,e0) = e1
| op(e1,e1) = e1
| op(e2,e2) = e1
| op(e3,e3) = e1 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(208,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e0,e0) != e0
| op(e1,e0) != e1 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(210,plain,
( op(e1,e1) = e0
| op(e3,e3) = e0
| op(e0,e0) != e0
| op(e2,e0) != e2 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(212,plain,
( op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e0,e0) != e0 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(216,plain,
( op(e0,e0) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e0) != e1 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(218,plain,
( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e3,e3) = e0
| op(e2,e0) != e2 ),
inference(split_conjunct,[status(thm)],[156]) ).
cnf(220,plain,
( op(e0,e0) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0
| op(e3,e3) = e0 ),
inference(split_conjunct,[status(thm)],[156]) ).
fof(221,plain,
( e0 != op(e3,op(e3,e3))
| e2 != op(op(e3,e3),e3)
| e1 != op(e3,e3) ),
inference(fof_nnf,[status(thm)],[18]) ).
cnf(222,plain,
( e1 != op(e3,e3)
| e2 != op(op(e3,e3),e3)
| e0 != op(e3,op(e3,e3)) ),
inference(split_conjunct,[status(thm)],[221]) ).
fof(227,plain,
( e1 != op(e0,op(e0,e0))
| e2 != op(op(e0,e0),e0)
| e3 != op(e0,e0) ),
inference(fof_nnf,[status(thm)],[21]) ).
cnf(228,plain,
( e3 != op(e0,e0)
| e2 != op(op(e0,e0),e0)
| e1 != op(e0,op(e0,e0)) ),
inference(split_conjunct,[status(thm)],[227]) ).
fof(237,plain,
( e1 != op(e3,op(e3,e3))
| e0 != op(op(e3,e3),e3)
| e2 != op(e3,e3) ),
inference(fof_nnf,[status(thm)],[26]) ).
cnf(238,plain,
( e2 != op(e3,e3)
| e0 != op(op(e3,e3),e3)
| e1 != op(e3,op(e3,e3)) ),
inference(split_conjunct,[status(thm)],[237]) ).
fof(239,plain,
( e1 != op(e2,op(e2,e2))
| e0 != op(op(e2,e2),e2)
| e3 != op(e2,e2) ),
inference(fof_nnf,[status(thm)],[27]) ).
cnf(240,plain,
( e3 != op(e2,e2)
| e0 != op(op(e2,e2),e2)
| e1 != op(e2,op(e2,e2)) ),
inference(split_conjunct,[status(thm)],[239]) ).
fof(241,plain,
( e2 != op(e3,op(e3,e3))
| e0 != op(op(e3,e3),e3)
| e1 != op(e3,e3) ),
inference(fof_nnf,[status(thm)],[28]) ).
cnf(242,plain,
( e1 != op(e3,e3)
| e0 != op(op(e3,e3),e3)
| e2 != op(e3,op(e3,e3)) ),
inference(split_conjunct,[status(thm)],[241]) ).
cnf(251,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e3) != e1 ),
inference(csr,[status(thm)],[168,167]) ).
cnf(252,plain,
( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e0) != e1 ),
inference(csr,[status(thm)],[216,208]) ).
cnf(257,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e1,e2) != e1 ),
inference(csr,[status(thm)],[184,182]) ).
cnf(310,plain,
( op(e1,e1) = e3
| op(e0,e0) = e3
| op(e2,e3) != e2 ),
inference(csr,[status(thm)],[170,169]) ).
cnf(311,plain,
( op(e1,e1) = e3
| op(e2,e2) = e3
| op(e0,e3) != e0 ),
inference(csr,[status(thm)],[164,163]) ).
cnf(312,plain,
( op(e3,e3) = e0
| op(e1,e1) = e0
| op(e2,e0) != e2 ),
inference(csr,[status(thm)],[218,210]) ).
cnf(314,plain,
( op(e3,e3) = e0
| op(e1,e1) = e0
| op(e2,e2) = e0 ),
inference(csr,[status(thm)],[220,212]) ).
cnf(315,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| e0 != op(e3,e1) ),
inference(spm,[status(thm)],[119,314,theory(equality)]) ).
cnf(316,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| e0 != op(e0,e1) ),
inference(spm,[status(thm)],[123,314,theory(equality)]) ).
cnf(317,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| e0 != op(e2,e1) ),
inference(spm,[status(thm)],[120,314,theory(equality)]) ).
cnf(318,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| e0 != op(e1,e3) ),
inference(spm,[status(thm)],[95,314,theory(equality)]) ).
cnf(319,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| e0 != op(e1,e0) ),
inference(spm,[status(thm)],[99,314,theory(equality)]) ).
cnf(343,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e1,e1) = e2 ),
inference(csr,[status(thm)],[188,186]) ).
cnf(345,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| e2 != op(e0,e1) ),
inference(spm,[status(thm)],[123,343,theory(equality)]) ).
cnf(346,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| e2 != op(e2,e1) ),
inference(spm,[status(thm)],[120,343,theory(equality)]) ).
cnf(347,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| e2 != op(e1,e3) ),
inference(spm,[status(thm)],[95,343,theory(equality)]) ).
cnf(348,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| e2 != op(e1,e0) ),
inference(spm,[status(thm)],[99,343,theory(equality)]) ).
cnf(349,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| e2 != op(e1,e2) ),
inference(spm,[status(thm)],[96,343,theory(equality)]) ).
cnf(352,plain,
( e2 = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[314,343,theory(equality)]) ).
cnf(354,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[352,154,theory(equality)]) ).
cnf(371,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e2,e3) = e1
| op(e0,e3) = e1
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[251,54,theory(equality)]) ).
cnf(384,plain,
( op(e3,e3) = e1
| op(e0,e0) = e1
| op(e2,e1) != e2 ),
inference(csr,[status(thm)],[202,198]) ).
cnf(385,plain,
( op(e3,e3) = e1
| op(e2,e2) = e1
| op(e0,e1) != e0 ),
inference(csr,[status(thm)],[196,192]) ).
cnf(386,plain,
( op(e0,e0) = e3
| op(e2,e2) = e3
| op(e1,e1) = e3 ),
inference(csr,[status(thm)],[171,172]) ).
cnf(390,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| e3 != op(e1,e3) ),
inference(spm,[status(thm)],[95,386,theory(equality)]) ).
cnf(391,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| e3 != op(e1,e0) ),
inference(spm,[status(thm)],[99,386,theory(equality)]) ).
cnf(394,plain,
( e3 = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e2,e2) = e3
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[314,386,theory(equality)]) ).
cnf(395,plain,
( e3 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e2) = e3
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[343,386,theory(equality)]) ).
cnf(398,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e2,e2) = e3
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[394,153,theory(equality)]) ).
cnf(399,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e2) = e3
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[395,150,theory(equality)]) ).
cnf(402,plain,
( op(e0,e0) = e1
| op(e2,e2) = e1
| op(e3,e1) != e3 ),
inference(csr,[status(thm)],[203,199]) ).
cnf(407,plain,
( op(e3,e3) = e1
| op(e0,e0) = e1
| op(e2,e2) = e1 ),
inference(csr,[status(thm)],[204,200]) ).
cnf(408,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| e1 != op(e3,e2) ),
inference(spm,[status(thm)],[112,407,theory(equality)]) ).
cnf(409,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| e1 != op(e0,e2) ),
inference(spm,[status(thm)],[116,407,theory(equality)]) ).
cnf(410,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| e1 != op(e2,e3) ),
inference(spm,[status(thm)],[88,407,theory(equality)]) ).
cnf(411,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| e1 != op(e2,e0) ),
inference(spm,[status(thm)],[92,407,theory(equality)]) ).
cnf(421,plain,
( op(e3,e0) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[85,133,theory(equality)]) ).
cnf(429,plain,
( op(e2,e0) = e3
| op(e0,e0) = e3
| op(e3,e0) = e3
| e3 != op(e1,e3) ),
inference(spm,[status(thm)],[97,74,theory(equality)]) ).
cnf(434,plain,
( op(e2,e0) = e0
| op(e0,e0) = e0
| op(e3,e0) = e0
| e0 != op(e1,e3) ),
inference(spm,[status(thm)],[97,80,theory(equality)]) ).
cnf(450,plain,
( op(e2,e0) = e1
| op(e0,e0) = e1
| op(e3,e0) = e1
| e1 != op(e1,e3) ),
inference(spm,[status(thm)],[97,78,theory(equality)]) ).
cnf(451,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e2,e0) = e1
| op(e0,e0) = e1
| op(e3,e0) = e1 ),
inference(spm,[status(thm)],[252,78,theory(equality)]) ).
cnf(461,plain,
( op(e3,e2) = e2
| op(e3,e2) = e0
| op(e3,e2) = e3
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[82,131,theory(equality)]) ).
cnf(508,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e2) = e1
| op(e0,e2) = e1
| op(e3,e2) = e1 ),
inference(spm,[status(thm)],[257,62,theory(equality)]) ).
cnf(518,plain,
( op(e3,e1) = e2
| op(e3,e1) = e0
| op(e3,e1) = e3
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[83,132,theory(equality)]) ).
cnf(553,plain,
( e0 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e1) = e0
| op(e0,e1) = e0
| op(e3,e1) = e0 ),
inference(spm,[status(thm)],[343,72,theory(equality)]) ).
cnf(562,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e1) = e0
| op(e0,e1) = e0
| op(e3,e1) = e0 ),
inference(sr,[status(thm)],[553,154,theory(equality)]) ).
cnf(574,plain,
( e2 = e3
| op(e2,e2) = e3
| op(e0,e0) = e3
| op(e2,e1) = e2
| op(e0,e1) = e2
| op(e3,e1) = e2 ),
inference(spm,[status(thm)],[386,68,theory(equality)]) ).
cnf(582,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e2,e1) = e2
| op(e0,e1) = e2
| op(e3,e1) = e2 ),
inference(sr,[status(thm)],[574,150,theory(equality)]) ).
cnf(595,plain,
( e1 = e3
| op(e2,e2) = e3
| op(e0,e0) = e3
| op(e2,e1) = e1
| op(e0,e1) = e1
| op(e3,e1) = e1 ),
inference(spm,[status(thm)],[386,70,theory(equality)]) ).
cnf(605,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e2,e1) = e1
| op(e0,e1) = e1
| op(e3,e1) = e1 ),
inference(sr,[status(thm)],[595,151,theory(equality)]) ).
cnf(612,plain,
( op(e0,e3) = e2
| op(e0,e3) = e0
| op(e0,e3) = e3
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[109,142,theory(equality)]) ).
cnf(628,plain,
( op(e2,e2) = e1
| op(e3,e3) = e1
| op(e0,e2) = e0
| op(e0,e0) = e0
| op(e0,e3) = e0 ),
inference(spm,[status(thm)],[385,81,theory(equality)]) ).
cnf(669,plain,
( op(e0,e2) = e2
| op(e0,e2) = e0
| op(e0,e2) = e3
| e1 != op(e0,e0) ),
inference(spm,[status(thm)],[104,143,theory(equality)]) ).
cnf(690,plain,
( op(e2,e3) = e2
| op(e2,e3) = e0
| op(e2,e3) = e3
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[106,134,theory(equality)]) ).
cnf(713,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e2,e2) = e2
| op(e2,e0) = e2
| op(e2,e3) = e2 ),
inference(spm,[status(thm)],[384,61,theory(equality)]) ).
cnf(718,plain,
( op(e2,e2) = e1
| op(e2,e0) = e1
| op(e2,e3) = e1
| e1 != op(e3,e1) ),
inference(spm,[status(thm)],[118,63,theory(equality)]) ).
cnf(734,plain,
( op(e2,e0) = e2
| op(e2,e0) = e0
| op(e2,e0) = e3
| e1 != op(e0,e0) ),
inference(spm,[status(thm)],[128,137,theory(equality)]) ).
cnf(769,plain,
( op(e1,e3) = e2
| op(e1,e3) = e0
| op(e1,e3) = e3
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[107,138,theory(equality)]) ).
cnf(772,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e3) = e2
| op(e1,e3) = e0
| op(e1,e3) = e3 ),
inference(spm,[status(thm)],[251,138,theory(equality)]) ).
cnf(785,plain,
( e3 = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e2) = e3
| op(e1,e0) = e3
| op(e1,e3) = e3 ),
inference(spm,[status(thm)],[314,67,theory(equality)]) ).
cnf(796,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e2) = e3
| op(e1,e0) = e3
| op(e1,e3) = e3 ),
inference(sr,[status(thm)],[785,153,theory(equality)]) ).
cnf(810,plain,
( e0 = e3
| op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e2) = e0
| op(e1,e0) = e0
| op(e1,e3) = e0 ),
inference(spm,[status(thm)],[386,73,theory(equality)]) ).
cnf(820,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e2) = e0
| op(e1,e0) = e0
| op(e1,e3) = e0 ),
inference(sr,[status(thm)],[810,153,theory(equality)]) ).
cnf(831,plain,
( e2 = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e2) = e2
| op(e1,e0) = e2
| op(e1,e3) = e2 ),
inference(spm,[status(thm)],[314,69,theory(equality)]) ).
cnf(844,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e2) = e2
| op(e1,e0) = e2
| op(e1,e3) = e2 ),
inference(sr,[status(thm)],[831,154,theory(equality)]) ).
cnf(857,plain,
( e1 = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e2) = e1
| op(e1,e0) = e1
| op(e1,e3) = e1 ),
inference(spm,[status(thm)],[314,71,theory(equality)]) ).
cnf(858,plain,
( e1 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e1,e2) = e1
| op(e1,e0) = e1
| op(e1,e3) = e1 ),
inference(spm,[status(thm)],[343,71,theory(equality)]) ).
cnf(861,plain,
( e1 = e3
| op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e2) = e1
| op(e1,e0) = e1
| op(e1,e3) = e1 ),
inference(spm,[status(thm)],[386,71,theory(equality)]) ).
cnf(872,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e2) = e1
| op(e1,e0) = e1
| op(e1,e3) = e1 ),
inference(sr,[status(thm)],[857,155,theory(equality)]) ).
cnf(873,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e1,e2) = e1
| op(e1,e0) = e1
| op(e1,e3) = e1 ),
inference(sr,[status(thm)],[858,152,theory(equality)]) ).
cnf(874,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e2) = e1
| op(e1,e0) = e1
| op(e1,e3) = e1 ),
inference(sr,[status(thm)],[861,151,theory(equality)]) ).
cnf(888,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e0) = e2
| op(e1,e0) = e0
| op(e1,e0) = e3 ),
inference(spm,[status(thm)],[252,141,theory(equality)]) ).
cnf(903,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e1,e2) = e2
| op(e1,e2) = e0
| op(e1,e2) = e3 ),
inference(spm,[status(thm)],[257,139,theory(equality)]) ).
cnf(944,plain,
( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[315,57,theory(equality)]) ).
cnf(949,plain,
( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e0,e2) = e0
| op(e0,e0) = e0
| op(e0,e3) = e0 ),
inference(spm,[status(thm)],[316,81,theory(equality)]) ).
cnf(954,plain,
( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e2,e0) = e0
| op(e2,e3) = e0 ),
inference(spm,[status(thm)],[317,65,theory(equality)]) ).
cnf(959,plain,
( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e0,e3) = e0 ),
inference(spm,[status(thm)],[318,56,theory(equality)]) ).
cnf(964,plain,
( op(e3,e3) = e0
| op(e2,e2) = e0
| op(e2,e0) = e0
| op(e0,e0) = e0
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[319,80,theory(equality)]) ).
cnf(980,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 ),
inference(spm,[status(thm)],[345,77,theory(equality)]) ).
cnf(985,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e2) = e2
| op(e2,e0) = e2
| op(e2,e3) = e2 ),
inference(spm,[status(thm)],[346,61,theory(equality)]) ).
cnf(990,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e3) = e2
| op(e0,e3) = e2 ),
inference(spm,[status(thm)],[347,52,theory(equality)]) ).
cnf(995,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 ),
inference(spm,[status(thm)],[348,76,theory(equality)]) ).
cnf(1000,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e2) = e2
| op(e0,e2) = e2
| op(e3,e2) = e2 ),
inference(spm,[status(thm)],[349,60,theory(equality)]) ).
cnf(1028,plain,
( e0 = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[407,354,theory(equality)]) ).
cnf(1029,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[1028,155,theory(equality)]) ).
cnf(1041,plain,
( e0 = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e0,e0) = e3
| op(e2,e2) = e3
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[407,398,theory(equality)]) ).
cnf(1042,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e0,e0) = e3
| op(e2,e2) = e3
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[1041,155,theory(equality)]) ).
cnf(1043,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e2
| e3 != op(e3,e2) ),
inference(spm,[status(thm)],[112,399,theory(equality)]) ).
cnf(1045,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e2
| e3 != op(e2,e3) ),
inference(spm,[status(thm)],[88,399,theory(equality)]) ).
cnf(1054,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e0
| e3 = e0
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[354,399,theory(equality)]) ).
cnf(1056,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e0
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[1054,153,theory(equality)]) ).
cnf(1057,plain,
( op(e0,e0) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e0,e3) = e3
| op(e3,e3) = e3 ),
inference(spm,[status(thm)],[390,50,theory(equality)]) ).
cnf(1062,plain,
( op(e0,e0) = e3
| op(e2,e2) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 ),
inference(spm,[status(thm)],[391,74,theory(equality)]) ).
cnf(1072,plain,
( op(e3,e3) = e1
| op(e0,e0) = e1
| op(e3,e2) = e2
| op(e3,e2) = e0
| op(e3,e2) = e3 ),
inference(spm,[status(thm)],[408,131,theory(equality)]) ).
cnf(1073,plain,
( op(e3,e3) = e1
| op(e0,e0) = e1
| op(e0,e2) = e2
| op(e0,e2) = e0
| op(e0,e2) = e3 ),
inference(spm,[status(thm)],[409,143,theory(equality)]) ).
cnf(1172,plain,
( e0 = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e2,e3) = e0
| op(e2,e0) = e0
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[407,954,theory(equality)]) ).
cnf(1174,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e2,e3) = e0
| op(e2,e0) = e0
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[1172,155,theory(equality)]) ).
cnf(1177,plain,
( op(e0,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| e0 != op(e0,e2) ),
inference(spm,[status(thm)],[116,959,theory(equality)]) ).
cnf(1179,plain,
( op(e0,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| e0 != op(e2,e0) ),
inference(spm,[status(thm)],[92,959,theory(equality)]) ).
cnf(1221,plain,
( op(e1,e1) = e3
| op(e0,e0) = e3
| op(e0,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[310,990,theory(equality)]) ).
cnf(1226,plain,
( op(e3,e0) = e3
| op(e0,e0) = e3
| op(e2,e0) = e3
| op(e2,e3) = e3
| op(e0,e3) = e3
| op(e3,e3) = e3 ),
inference(spm,[status(thm)],[429,50,theory(equality)]) ).
cnf(1232,plain,
( op(e3,e0) = e0
| op(e0,e0) = e0
| op(e2,e0) = e0
| op(e2,e3) = e0
| op(e0,e3) = e0
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[434,56,theory(equality)]) ).
cnf(1244,plain,
( op(e3,e0) = e1
| op(e0,e0) = e1
| op(e2,e0) = e1
| op(e2,e3) = e1
| op(e0,e3) = e1
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[450,54,theory(equality)]) ).
cnf(1280,plain,
( op(e3,e0) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| e2 != op(e2,e3) ),
inference(spm,[status(thm)],[91,995,theory(equality)]) ).
cnf(1282,plain,
( op(e1,e1) = e0
| op(e3,e3) = e0
| op(e3,e0) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[312,995,theory(equality)]) ).
cnf(1329,plain,
( op(e0,e0) = e3
| op(e3,e3) = e0
| op(e3,e3) = e2
| e2 != op(e3,e0) ),
inference(spm,[status(thm)],[127,1056,theory(equality)]) ).
cnf(1330,plain,
( op(e0,e0) = e3
| op(e3,e3) = e0
| op(e3,e3) = e2
| e2 != op(e0,e3) ),
inference(spm,[status(thm)],[103,1056,theory(equality)]) ).
cnf(1337,plain,
( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e0,e0) = e3
| e3 != op(e3,e2) ),
inference(spm,[status(thm)],[112,1062,theory(equality)]) ).
cnf(1339,plain,
( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e0,e0) = e3
| e3 != op(e2,e3) ),
inference(spm,[status(thm)],[88,1062,theory(equality)]) ).
cnf(1391,plain,
( e3 = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e0,e3) = e1
| op(e2,e3) = e1
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[407,371,theory(equality)]) ).
cnf(1397,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e0,e3) = e1
| op(e2,e3) = e1
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[1391,151,theory(equality)]) ).
cnf(1448,plain,
( e0 = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[407,451,theory(equality)]) ).
cnf(1456,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[1448,155,theory(equality)]) ).
cnf(1539,plain,
( op(e0,e0) = e3
| e1 = e3
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e2) = e1
| op(e0,e2) = e1 ),
inference(spm,[status(thm)],[399,508,theory(equality)]) ).
cnf(1553,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e2) = e1
| op(e0,e2) = e1 ),
inference(sr,[status(thm)],[1539,151,theory(equality)]) ).
cnf(1604,plain,
( op(e3,e1) = e0
| op(e0,e1) = e0
| op(e3,e3) = e2
| op(e0,e0) = e2
| e0 != op(e2,e2) ),
inference(spm,[status(thm)],[90,562,theory(equality)]) ).
cnf(1675,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e1) = e2
| op(e0,e1) = e2
| op(e0,e0) = e3
| op(e2,e2) = e3 ),
inference(spm,[status(thm)],[384,582,theory(equality)]) ).
cnf(1760,plain,
( op(e3,e1) = e1
| op(e0,e1) = e1
| op(e0,e0) = e3
| op(e2,e2) = e3
| e1 != op(e2,e2) ),
inference(spm,[status(thm)],[90,605,theory(equality)]) ).
cnf(1890,plain,
( e2 = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e2,e3) = e2
| op(e2,e0) = e2 ),
inference(spm,[status(thm)],[407,713,theory(equality)]) ).
cnf(1907,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e2,e3) = e2
| op(e2,e0) = e2 ),
inference(sr,[status(thm)],[1890,152,theory(equality)]) ).
cnf(1931,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e3) = e2
| op(e1,e3) = e0 ),
inference(csr,[status(thm)],[772,390]) ).
cnf(1933,plain,
( op(e1,e3) = e0
| op(e0,e0) = e3
| op(e2,e2) = e3
| e2 != op(e3,e3) ),
inference(spm,[status(thm)],[107,1931,theory(equality)]) ).
cnf(1962,plain,
( op(e1,e3) = e3
| op(e1,e0) = e3
| op(e3,e3) = e0
| op(e2,e2) = e0
| e3 != op(e2,e2) ),
inference(spm,[status(thm)],[114,796,theory(equality)]) ).
cnf(2039,plain,
( op(e2,e3) = e1
| op(e2,e0) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e3,e0) = e1
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[718,55,theory(equality)]) ).
cnf(2081,plain,
( op(e1,e3) = e0
| op(e1,e0) = e0
| op(e0,e0) = e3
| op(e2,e2) = e3
| e0 != op(e2,e2) ),
inference(spm,[status(thm)],[114,820,theory(equality)]) ).
cnf(2162,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e2) = e1
| op(e1,e3) = e1 ),
inference(csr,[status(thm)],[872,252]) ).
cnf(2163,plain,
( op(e1,e3) = e1
| op(e3,e3) = e0
| op(e2,e2) = e0
| e1 != op(e3,e2) ),
inference(spm,[status(thm)],[113,2162,theory(equality)]) ).
cnf(2165,plain,
( op(e1,e3) = e1
| op(e3,e3) = e0
| op(e2,e2) = e0
| e1 != op(e2,e2) ),
inference(spm,[status(thm)],[114,2162,theory(equality)]) ).
cnf(2181,plain,
( op(e1,e3) = e3
| op(e1,e0) = e3
| e1 = e3
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e3) = e1 ),
inference(spm,[status(thm)],[796,2162,theory(equality)]) ).
cnf(2185,plain,
( op(e1,e3) = e2
| op(e1,e0) = e2
| e1 = e2
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e3) = e1 ),
inference(spm,[status(thm)],[844,2162,theory(equality)]) ).
cnf(2190,plain,
( op(e1,e3) = e3
| op(e1,e0) = e3
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e3) = e1 ),
inference(sr,[status(thm)],[2181,151,theory(equality)]) ).
cnf(2194,plain,
( op(e1,e3) = e2
| op(e1,e0) = e2
| op(e3,e3) = e0
| op(e2,e2) = e0
| op(e1,e3) = e1 ),
inference(sr,[status(thm)],[2185,152,theory(equality)]) ).
cnf(2196,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e1,e3) = e1
| op(e1,e0) = e1 ),
inference(csr,[status(thm)],[873,257]) ).
cnf(2198,plain,
( op(e1,e3) = e1
| op(e3,e3) = e2
| op(e0,e0) = e2
| e1 != op(e0,e0) ),
inference(spm,[status(thm)],[129,2196,theory(equality)]) ).
cnf(2221,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e2) = e1
| op(e1,e0) = e1 ),
inference(csr,[status(thm)],[874,251]) ).
cnf(2243,plain,
( op(e1,e3) = e0
| op(e1,e0) = e0
| e1 = e0
| op(e0,e0) = e3
| op(e2,e2) = e3
| op(e1,e0) = e1 ),
inference(spm,[status(thm)],[820,2221,theory(equality)]) ).
cnf(2252,plain,
( op(e1,e3) = e0
| op(e1,e0) = e0
| op(e0,e0) = e3
| op(e2,e2) = e3
| op(e1,e0) = e1 ),
inference(sr,[status(thm)],[2243,155,theory(equality)]) ).
cnf(2340,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e0) = e2
| op(e1,e0) = e3 ),
inference(csr,[status(thm)],[888,319]) ).
cnf(2342,plain,
( op(e1,e0) = e3
| op(e3,e3) = e0
| op(e2,e2) = e0
| e2 != op(e3,e0) ),
inference(spm,[status(thm)],[125,2340,theory(equality)]) ).
cnf(2343,plain,
( op(e1,e0) = e3
| op(e3,e3) = e0
| op(e2,e2) = e0
| e2 != op(e0,e0) ),
inference(spm,[status(thm)],[129,2340,theory(equality)]) ).
cnf(2368,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e1,e2) = e3
| op(e1,e2) = e0 ),
inference(csr,[status(thm)],[903,349]) ).
cnf(2372,plain,
( op(e1,e2) = e3
| op(e3,e3) = e2
| op(e0,e0) = e2
| e0 != op(e2,e2) ),
inference(spm,[status(thm)],[114,2368,theory(equality)]) ).
cnf(2530,plain,
( op(e0,e3) = e0
| op(e0,e0) = e0
| op(e0,e2) = e0
| op(e3,e3) = e1
| e0 = e1
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[628,949,theory(equality)]) ).
cnf(2542,plain,
( op(e0,e3) = e0
| op(e0,e0) = e0
| op(e0,e2) = e0
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[2530,155,theory(equality)]) ).
cnf(2545,plain,
( op(e3,e0) = e0
| op(e0,e0) = e0
| op(e2,e0) = e0
| op(e3,e3) = e0
| e0 != op(e2,e3) ),
inference(spm,[status(thm)],[88,964,theory(equality)]) ).
cnf(2586,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e0
| e2 = e0
| op(e2,e3) = e2
| op(e2,e0) = e2 ),
inference(spm,[status(thm)],[354,985,theory(equality)]) ).
cnf(2607,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e0
| op(e2,e3) = e2
| op(e2,e0) = e2 ),
inference(sr,[status(thm)],[2586,154,theory(equality)]) ).
cnf(2639,plain,
( op(e0,e0) = e3
| e2 = e3
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e2) = e2
| op(e0,e2) = e2 ),
inference(spm,[status(thm)],[399,1000,theory(equality)]) ).
cnf(2661,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e2) = e2
| op(e0,e2) = e2 ),
inference(sr,[status(thm)],[2639,150,theory(equality)]) ).
cnf(2727,plain,
( e1 = e3
| op(e3,e3) = e0
| e1 = e2
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[1056,1029,theory(equality)]) ).
cnf(2733,plain,
( op(e3,e3) = e0
| e1 = e2
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[2727,151,theory(equality)]) ).
cnf(2734,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[2733,152,theory(equality)]) ).
cnf(2757,plain,
( e3 = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e3) = e0
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[407,1042,theory(equality)]) ).
cnf(2773,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e3) = e0
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[2757,151,theory(equality)]) ).
cnf(2797,plain,
( e1 = e3
| op(e3,e3) = e0
| e1 = e2
| op(e3,e3) = e2
| op(e0,e0) = e3
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[1056,2773,theory(equality)]) ).
cnf(2804,plain,
( op(e3,e3) = e0
| e1 = e2
| op(e3,e3) = e2
| op(e0,e0) = e3
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[2797,151,theory(equality)]) ).
cnf(2805,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e0,e0) = e3
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[2804,152,theory(equality)]) ).
cnf(2898,plain,
( op(e3,e3) = e1
| e3 = e2
| op(e3,e3) = e2
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[2734,2805,theory(equality)]) ).
cnf(2900,plain,
( op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[2898,150,theory(equality)]) ).
cnf(2907,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e3,e1) != e0
| op(e1,e3) != e2 ),
inference(spm,[status(thm)],[222,2900,theory(equality)]) ).
cnf(2909,plain,
( op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e0) = e2
| op(e3,e3) = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[421,2900,theory(equality)]) ).
cnf(2912,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| op(e0,e3) = e2
| op(e3,e3) = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[612,2900,theory(equality)]) ).
cnf(2914,plain,
( op(e1,e3) = e3
| op(e1,e3) = e0
| op(e1,e3) = e2
| op(e3,e3) = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[769,2900,theory(equality)]) ).
cnf(2937,plain,
( op(e3,e3) = e3
| op(e0,e3) = e3
| op(e2,e3) = e3
| op(e0,e0) = e3
| e3 != op(e2,e0) ),
inference(spm,[status(thm)],[92,1057,theory(equality)]) ).
cnf(2974,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e2) = e2
| op(e0,e0) = e1 ),
inference(csr,[status(thm)],[1072,461]) ).
cnf(2992,plain,
( op(e3,e3) = e1
| op(e0,e2) = e3
| op(e0,e2) = e0
| op(e0,e2) = e2 ),
inference(csr,[status(thm)],[1073,669]) ).
cnf(3007,plain,
( op(e3,e3) = e2
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e0) = e0
| op(e1,e3) != e2 ),
inference(spm,[status(thm)],[2907,57,theory(equality)]) ).
cnf(3106,plain,
( e0 = e2
| op(e2,e3) = e2
| op(e3,e3) = e1
| op(e0,e0) = e1
| op(e3,e3) = e0
| op(e2,e3) = e0 ),
inference(spm,[status(thm)],[1907,1174,theory(equality)]) ).
cnf(3115,plain,
( op(e2,e3) = e2
| op(e3,e3) = e1
| op(e0,e0) = e1
| op(e3,e3) = e0
| op(e2,e3) = e0 ),
inference(sr,[status(thm)],[3106,154,theory(equality)]) ).
cnf(3179,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e0) = e2
| op(e0,e3) = e2 ),
inference(spm,[status(thm)],[1280,990,theory(equality)]) ).
cnf(3225,plain,
( e3 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e3) = e2
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[343,1221,theory(equality)]) ).
cnf(3239,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e3) = e2
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[3225,150,theory(equality)]) ).
cnf(3272,plain,
( e0 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e3,e0) = e2
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[343,1282,theory(equality)]) ).
cnf(3286,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e3,e0) = e2
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[3272,154,theory(equality)]) ).
cnf(3454,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e0,e3) = e1
| op(e0,e0) = e3 ),
inference(csr,[status(thm)],[1397,410]) ).
cnf(3480,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e0) = e1
| op(e3,e3) = e0 ),
inference(csr,[status(thm)],[1456,411]) ).
cnf(3547,plain,
( e1 = e3
| e1 = e0
| e1 = e2
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[2992,1553,theory(equality)]) ).
cnf(3558,plain,
( e1 = e0
| e1 = e2
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[3547,151,theory(equality)]) ).
cnf(3559,plain,
( e1 = e2
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[3558,155,theory(equality)]) ).
cnf(3560,plain,
( op(e3,e3) = e1
| op(e3,e2) = e1
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[3559,152,theory(equality)]) ).
cnf(3574,plain,
( e1 = e0
| op(e3,e3) = e0
| op(e1,e3) = e1
| op(e2,e2) = e2
| op(e2,e2) = e0
| op(e2,e2) = e3 ),
inference(spm,[status(thm)],[2165,135,theory(equality)]) ).
cnf(3589,plain,
( op(e3,e3) = e0
| op(e1,e3) = e1
| op(e2,e2) = e2
| op(e2,e2) = e0
| op(e2,e2) = e3 ),
inference(sr,[status(thm)],[3574,155,theory(equality)]) ).
cnf(3605,plain,
( e1 = e2
| op(e3,e3) = e2
| op(e1,e3) = e1
| op(e0,e0) = e2
| op(e0,e0) = e0
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[2198,145,theory(equality)]) ).
cnf(3612,plain,
( op(e3,e3) = e2
| op(e1,e3) = e1
| op(e0,e0) = e2
| op(e0,e0) = e0
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[3605,152,theory(equality)]) ).
cnf(3679,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e0) = e3
| op(e3,e0) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[2343,3286,theory(equality)]) ).
cnf(3804,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e1,e2) = e3
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[2372,354,theory(equality)]) ).
cnf(3892,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e0,e0) = e2
| e3 != op(e2,e2) ),
inference(spm,[status(thm)],[114,3804,theory(equality)]) ).
cnf(3893,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e0,e0) = e2
| e3 != op(e1,e3) ),
inference(spm,[status(thm)],[94,3804,theory(equality)]) ).
cnf(4059,plain,
( op(e1,e3) = e1
| op(e2,e2) = e0
| op(e3,e3) = e0
| e2 = e3
| op(e1,e3) = e3
| op(e1,e3) = e2 ),
inference(spm,[status(thm)],[2190,2194,theory(equality)]) ).
cnf(4065,plain,
( op(e1,e3) = e1
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e3) = e3
| op(e1,e3) = e2 ),
inference(sr,[status(thm)],[4059,150,theory(equality)]) ).
cnf(4144,plain,
( op(e2,e2) = e3
| op(e0,e0) = e3
| op(e1,e0) = e0
| op(e1,e3) = e0
| e1 != op(e0,e0) ),
inference(spm,[status(thm)],[129,2252,theory(equality)]) ).
cnf(4380,plain,
( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e0,e3) = e0
| op(e3,e3) = e1
| op(e0,e0) = e0 ),
inference(spm,[status(thm)],[1177,2542,theory(equality)]) ).
cnf(4400,plain,
( op(e1,e1) = e0
| op(e3,e3) = e0
| op(e2,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[312,2607,theory(equality)]) ).
cnf(4482,plain,
( op(e3,e2) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3
| e2 != op(e0,e3) ),
inference(spm,[status(thm)],[100,2661,theory(equality)]) ).
cnf(4556,plain,
( op(e3,e3) = e2
| op(e3,e3) = e0
| op(e0,e0) = e3
| op(e3,e0) = e0
| op(e3,e0) = e3 ),
inference(spm,[status(thm)],[1329,2909,theory(equality)]) ).
cnf(4645,plain,
( op(e3,e3) = e2
| op(e3,e3) = e0
| op(e0,e0) = e3
| op(e0,e3) = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[1330,2912,theory(equality)]) ).
cnf(4769,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e0
| op(e1,e3) = e0
| op(e1,e3) = e3 ),
inference(spm,[status(thm)],[347,2914,theory(equality)]) ).
cnf(4893,plain,
( op(e2,e3) = e0
| op(e3,e3) = e0
| op(e0,e0) = e1
| op(e3,e3) = e1
| e2 != op(e3,e3) ),
inference(spm,[status(thm)],[106,3115,theory(equality)]) ).
cnf(5237,plain,
( e2 = e3
| op(e0,e3) = e1
| op(e3,e3) = e1
| e2 = e1
| op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e2) = e1 ),
inference(spm,[status(thm)],[3454,3560,theory(equality)]) ).
cnf(5249,plain,
( op(e0,e3) = e1
| op(e3,e3) = e1
| e1 = e2
| op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e2) = e1 ),
inference(sr,[status(thm)],[5237,150,theory(equality)]) ).
cnf(5250,plain,
( op(e0,e3) = e1
| op(e3,e3) = e1
| op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e2) = e1 ),
inference(sr,[status(thm)],[5249,152,theory(equality)]) ).
cnf(5255,plain,
( op(e2,e2) = e3
| op(e2,e2) = e0
| op(e2,e2) = e2
| op(e3,e3) = e0
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[107,3589,theory(equality)]) ).
cnf(5298,plain,
( op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e0) = e2
| op(e3,e3) = e2
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[107,3612,theory(equality)]) ).
cnf(5724,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e0) = e3
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[3679,2342]) ).
cnf(5725,plain,
( op(e3,e3) = e2
| op(e3,e3) = e0
| op(e2,e2) = e0
| e3 != op(e3,e0) ),
inference(spm,[status(thm)],[125,5724,theory(equality)]) ).
cnf(5726,plain,
( op(e3,e3) = e2
| op(e3,e3) = e0
| op(e2,e2) = e0
| e3 != op(e0,e0) ),
inference(spm,[status(thm)],[129,5724,theory(equality)]) ).
cnf(5727,plain,
( op(e3,e3) = e2
| op(e3,e3) = e0
| op(e2,e2) = e0
| e3 != op(e2,e0) ),
inference(spm,[status(thm)],[126,5724,theory(equality)]) ).
cnf(6029,plain,
( op(e1,e3) = e2
| op(e1,e3) = e3
| op(e3,e3) = e0
| op(e2,e2) = e0
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[107,4065,theory(equality)]) ).
cnf(6320,plain,
( e0 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[343,4400,theory(equality)]) ).
cnf(6335,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[6320,154,theory(equality)]) ).
cnf(6345,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e0,e0) = e2
| e2 != op(e0,e3) ),
inference(spm,[status(thm)],[110,6335,theory(equality)]) ).
cnf(6445,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e3,e3) = e0
| op(e0,e3) = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[6345,2912,theory(equality)]) ).
cnf(6592,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e3,e3) = e2
| op(e3,e0) = e3
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[5726,4556,theory(equality)]) ).
cnf(6809,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e3) = e0
| op(e1,e3) = e0 ),
inference(csr,[status(thm)],[4769,3893]) ).
cnf(6811,plain,
( op(e3,e3) = e0
| op(e0,e0) = e2
| op(e3,e3) = e2
| e0 != op(e0,e3) ),
inference(spm,[status(thm)],[111,6809,theory(equality)]) ).
cnf(7145,plain,
( op(e3,e2) = e1
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e3) = e1
| op(e0,e3) != e2
| op(e3,e0) != e1 ),
inference(spm,[status(thm)],[43,5250,theory(equality)]) ).
cnf(7775,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e3,e3) = e0
| op(e0,e3) = e3 ),
inference(csr,[status(thm)],[6445,6811]) ).
cnf(7801,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| e2 = e3
| op(e3,e3) = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[4645,7775,theory(equality)]) ).
cnf(7815,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| op(e3,e3) = e0
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[7801,150,theory(equality)]) ).
cnf(7823,plain,
( op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e3) = e2
| op(e3,e3) = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[311,7815,theory(equality)]) ).
cnf(7845,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e3,e3) = e2
| op(e3,e0) = e0 ),
inference(csr,[status(thm)],[6592,5725]) ).
cnf(7846,plain,
( op(e3,e0) = e0
| op(e3,e3) = e2
| op(e3,e3) = e0
| e0 != op(e3,e2) ),
inference(spm,[status(thm)],[112,7845,theory(equality)]) ).
cnf(7849,plain,
( op(e3,e0) = e0
| op(e3,e3) = e2
| op(e3,e3) = e0
| e0 != op(e2,e0) ),
inference(spm,[status(thm)],[92,7845,theory(equality)]) ).
cnf(8182,plain,
( op(e0,e3) = e3
| op(e3,e3) = e0
| op(e3,e3) = e2
| op(e2,e2) = e3
| e3 != op(e1,e3) ),
inference(spm,[status(thm)],[95,7823,theory(equality)]) ).
cnf(10901,plain,
( e1 = e3
| op(e0,e0) = e3
| op(e0,e1) = e1
| op(e3,e1) = e1
| op(e0,e0) = e1
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[1760,407,theory(equality)]) ).
cnf(10928,plain,
( op(e0,e0) = e3
| op(e0,e1) = e1
| op(e3,e1) = e1
| op(e0,e0) = e1
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[10901,151,theory(equality)]) ).
cnf(11214,plain,
( op(e3,e3) = e1
| op(e0,e0) = e1
| op(e3,e1) = e1
| op(e0,e0) = e3
| e1 != op(e0,e3) ),
inference(spm,[status(thm)],[101,10928,theory(equality)]) ).
cnf(11954,plain,
( e0 = e3
| op(e0,e0) = e3
| op(e1,e0) = e0
| op(e1,e3) = e0
| op(e2,e2) = e3
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[2081,398,theory(equality)]) ).
cnf(11986,plain,
( op(e0,e0) = e3
| op(e1,e0) = e0
| op(e1,e3) = e0
| op(e2,e2) = e3
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[11954,153,theory(equality)]) ).
cnf(12076,plain,
( op(e3,e3) = e0
| op(e2,e2) = e3
| op(e1,e3) = e0
| op(e0,e0) = e3
| e0 != op(e3,e0) ),
inference(spm,[status(thm)],[125,11986,theory(equality)]) ).
cnf(12607,plain,
( op(e3,e3) = e2
| op(e3,e3) = e0
| op(e3,e0) = e0
| op(e1,e3) != e2 ),
inference(csr,[status(thm)],[3007,7846]) ).
cnf(12615,plain,
( op(e3,e0) = e0
| op(e3,e3) = e0
| op(e3,e3) = e2
| op(e1,e3) = e0
| op(e1,e3) = e3 ),
inference(spm,[status(thm)],[12607,2914,theory(equality)]) ).
cnf(12734,plain,
( op(e1,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e0
| op(e3,e0) = e0
| e0 != op(e0,e3) ),
inference(spm,[status(thm)],[111,12615,theory(equality)]) ).
cnf(14560,plain,
( op(e3,e2) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3 ),
inference(csr,[status(thm)],[4482,3239]) ).
cnf(14575,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e2) = e2
| e2 = e1
| op(e0,e0) = e3
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[2974,14560,theory(equality)]) ).
cnf(14596,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e2) = e2
| op(e0,e0) = e3
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[14575,152,theory(equality)]) ).
cnf(14628,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e2) = e2
| e3 = e1
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[2974,14596,theory(equality)]) ).
cnf(14649,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e2) = e2
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[14628,151,theory(equality)]) ).
cnf(14666,plain,
( op(e3,e3) = e2
| op(e3,e2) = e0
| op(e3,e2) = e3
| e2 != op(e3,e0) ),
inference(spm,[status(thm)],[86,14649,theory(equality)]) ).
cnf(15307,plain,
( op(e2,e3) = e0
| op(e3,e3) = e0
| op(e0,e0) = e1
| op(e3,e3) = e1 ),
inference(csr,[status(thm)],[4893,2900]) ).
cnf(15309,plain,
( op(e3,e3) = e1
| op(e0,e0) = e1
| op(e3,e3) = e0
| e0 != op(e0,e3) ),
inference(spm,[status(thm)],[110,15307,theory(equality)]) ).
cnf(16674,plain,
( op(e3,e3) = e1
| op(e0,e0) = e1
| op(e3,e1) = e1
| op(e0,e0) = e3 ),
inference(csr,[status(thm)],[11214,3454]) ).
cnf(16691,plain,
( e1 = e3
| op(e0,e3) = e2
| op(e3,e3) = e2
| e1 = e2
| op(e0,e0) = e3
| op(e3,e1) = e1
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[3239,16674,theory(equality)]) ).
cnf(16721,plain,
( op(e0,e3) = e2
| op(e3,e3) = e2
| e1 = e2
| op(e0,e0) = e3
| op(e3,e1) = e1
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[16691,151,theory(equality)]) ).
cnf(16722,plain,
( op(e0,e3) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3
| op(e3,e1) = e1
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[16721,152,theory(equality)]) ).
cnf(16767,plain,
( op(e0,e3) = e2
| op(e3,e0) = e2
| e3 = e2
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e1) = e1 ),
inference(spm,[status(thm)],[3179,16722,theory(equality)]) ).
cnf(16789,plain,
( op(e0,e3) = e2
| op(e3,e0) = e2
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e1) = e1 ),
inference(sr,[status(thm)],[16767,150,theory(equality)]) ).
cnf(17354,plain,
( op(e3,e0) = e0
| op(e3,e3) = e0
| op(e3,e3) = e2
| op(e1,e3) = e3
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[12734,7815,theory(equality)]) ).
cnf(17540,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e3,e3) = e0
| op(e0,e3) = e3
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[8182,17354,theory(equality)]) ).
cnf(17784,plain,
( op(e3,e0) = e0
| op(e3,e3) = e2
| op(e3,e3) = e0
| e3 = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[7845,17540,theory(equality)]) ).
cnf(17818,plain,
( op(e3,e0) = e0
| op(e3,e3) = e2
| op(e3,e3) = e0
| op(e0,e3) = e3 ),
inference(sr,[status(thm)],[17784,153,theory(equality)]) ).
cnf(18178,plain,
( op(e3,e0) = e3
| op(e0,e0) = e3
| op(e2,e0) = e3
| op(e3,e3) = e3
| op(e0,e3) = e3 ),
inference(csr,[status(thm)],[1226,1339]) ).
cnf(18181,plain,
( op(e3,e3) = e3
| op(e0,e3) = e3
| op(e0,e0) = e3
| op(e3,e0) = e3
| e3 != op(e2,e3) ),
inference(spm,[status(thm)],[91,18178,theory(equality)]) ).
cnf(18238,plain,
( op(e0,e0) = e3
| op(e2,e3) = e3
| op(e0,e3) = e3
| op(e3,e3) = e3
| op(e3,e0) = e3 ),
inference(spm,[status(thm)],[2937,18178,theory(equality)]) ).
cnf(18486,plain,
( op(e3,e3) = e3
| op(e0,e3) = e3
| op(e0,e0) = e3
| op(e3,e0) = e3 ),
inference(csr,[status(thm)],[18181,18238]) ).
cnf(18666,plain,
( op(e3,e0) = e0
| op(e0,e0) = e0
| op(e2,e0) = e0
| op(e3,e3) = e0
| op(e0,e3) = e0 ),
inference(csr,[status(thm)],[1232,2545]) ).
cnf(18669,plain,
( op(e3,e3) = e0
| op(e0,e3) = e0
| op(e0,e0) = e0
| op(e3,e0) = e0
| e0 != op(e2,e3) ),
inference(spm,[status(thm)],[91,18666,theory(equality)]) ).
cnf(18682,plain,
( op(e3,e3) = e0
| op(e2,e3) = e0
| op(e0,e3) = e0
| op(e0,e0) = e0
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[1179,18666,theory(equality)]) ).
cnf(18703,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e3,e0) = e0
| op(e0,e3) = e0
| op(e0,e0) = e0 ),
inference(spm,[status(thm)],[7849,18666,theory(equality)]) ).
cnf(18961,plain,
( e0 = e3
| op(e3,e3) = e0
| e0 = e2
| op(e3,e3) = e2
| op(e0,e3) = e0
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[1056,18703,theory(equality)]) ).
cnf(19009,plain,
( op(e3,e3) = e0
| e2 = e0
| op(e3,e3) = e2
| op(e0,e3) = e0
| op(e3,e0) = e0 ),
inference(sr,[status(thm)],[18961,153,theory(equality)]) ).
cnf(19010,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e0,e3) = e0
| op(e3,e0) = e0 ),
inference(sr,[status(thm)],[19009,154,theory(equality)]) ).
cnf(19109,plain,
( e0 = e3
| op(e3,e3) = e0
| op(e3,e3) = e2
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[17818,19010,theory(equality)]) ).
cnf(19124,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| op(e3,e0) = e0 ),
inference(sr,[status(thm)],[19109,153,theory(equality)]) ).
cnf(19168,plain,
( op(e0,e0) = e3
| op(e1,e3) = e0
| op(e2,e2) = e3
| op(e3,e3) = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[12076,19124,theory(equality)]) ).
cnf(19264,plain,
( op(e3,e3) = e0
| op(e0,e3) = e0
| op(e0,e0) = e0
| op(e3,e0) = e0 ),
inference(csr,[status(thm)],[18669,18682]) ).
cnf(19279,plain,
( e0 = e3
| op(e3,e3) = e0
| op(e3,e3) = e1
| e0 = e1
| op(e3,e0) = e0
| op(e0,e3) = e0 ),
inference(spm,[status(thm)],[2773,19264,theory(equality)]) ).
cnf(19324,plain,
( op(e3,e3) = e0
| op(e3,e3) = e1
| e1 = e0
| op(e3,e0) = e0
| op(e0,e3) = e0 ),
inference(sr,[status(thm)],[19279,153,theory(equality)]) ).
cnf(19325,plain,
( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e0) = e0
| op(e0,e3) = e0 ),
inference(sr,[status(thm)],[19324,155,theory(equality)]) ).
cnf(19374,plain,
( op(e1,e1) = e3
| op(e2,e2) = e3
| op(e3,e0) = e0
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[311,19325,theory(equality)]) ).
cnf(19404,plain,
( op(e3,e3) = e0
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[15309,19325,theory(equality)]) ).
cnf(19439,plain,
( op(e3,e0) = e0
| op(e3,e3) = e1
| op(e3,e3) = e0
| e1 != op(e3,e0) ),
inference(spm,[status(thm)],[127,19404,theory(equality)]) ).
cnf(19440,plain,
( op(e3,e0) = e0
| op(e3,e3) = e1
| op(e3,e3) = e0
| e1 != op(e0,e3) ),
inference(spm,[status(thm)],[103,19404,theory(equality)]) ).
cnf(19524,plain,
( op(e0,e0) = e3
| op(e1,e3) = e0
| op(e2,e2) = e3
| op(e3,e3) = e0 ),
inference(csr,[status(thm)],[19168,1933]) ).
cnf(19526,plain,
( op(e3,e3) = e0
| op(e2,e2) = e3
| op(e0,e0) = e3
| e0 != op(e0,e3) ),
inference(spm,[status(thm)],[111,19524,theory(equality)]) ).
cnf(19608,plain,
( op(e3,e3) = e0
| op(e3,e3) = e1
| e1 = e0
| op(e3,e0) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3 ),
inference(spm,[status(thm)],[19439,133,theory(equality)]) ).
cnf(19609,plain,
( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e0) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3 ),
inference(sr,[status(thm)],[19608,155,theory(equality)]) ).
cnf(19621,plain,
( op(e0,e0) = e3
| op(e2,e2) = e3
| op(e3,e3) = e0
| op(e3,e0) = e0
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[19526,19325,theory(equality)]) ).
cnf(19656,plain,
( e3 = e0
| op(e2,e2) = e0
| op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e0) = e0
| op(e2,e2) = e3 ),
inference(spm,[status(thm)],[314,19374,theory(equality)]) ).
cnf(19673,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e0) = e0
| op(e2,e2) = e3 ),
inference(sr,[status(thm)],[19656,153,theory(equality)]) ).
cnf(20023,plain,
( op(e3,e3) = e0
| op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e0) = e2 ),
inference(csr,[status(thm)],[19609,421]) ).
cnf(20026,plain,
( op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e3) = e0
| e2 != op(e3,e3) ),
inference(spm,[status(thm)],[85,20023,theory(equality)]) ).
cnf(20171,plain,
( op(e3,e0) = e0
| op(e3,e2) = e0
| e3 = e0
| op(e3,e3) = e0
| op(e3,e3) = e1
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[944,19621,theory(equality)]) ).
cnf(20210,plain,
( op(e3,e0) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e3) = e1
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[20171,153,theory(equality)]) ).
cnf(20242,plain,
( op(e2,e2) = e3
| op(e3,e0) = e0
| op(e3,e3) = e1
| op(e3,e3) = e0
| e0 != op(e3,e2) ),
inference(spm,[status(thm)],[112,19673,theory(equality)]) ).
cnf(20347,plain,
( op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e3) = e0 ),
inference(csr,[status(thm)],[20026,19124]) ).
cnf(20481,plain,
( op(e3,e0) = e0
| op(e3,e3) = e1
| e3 = e1
| op(e3,e3) = e0
| op(e3,e2) = e0 ),
inference(spm,[status(thm)],[19404,20210,theory(equality)]) ).
cnf(20498,plain,
( op(e3,e0) = e0
| op(e3,e3) = e1
| op(e3,e3) = e0
| op(e3,e2) = e0 ),
inference(sr,[status(thm)],[20481,151,theory(equality)]) ).
cnf(20854,plain,
( op(e2,e2) = e3
| op(e3,e0) = e0
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(csr,[status(thm)],[20242,20498]) ).
cnf(20860,plain,
( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e0) = e0
| op(e2,e3) != e1
| op(e3,e2) != e0 ),
inference(spm,[status(thm)],[240,20854,theory(equality)]) ).
cnf(20899,plain,
( e3 = e0
| op(e3,e3) = e0
| op(e1,e0) = e3
| op(e1,e3) = e3
| op(e3,e3) = e1
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[1962,20854,theory(equality)]) ).
cnf(20935,plain,
( op(e3,e3) = e0
| op(e1,e0) = e3
| op(e1,e3) = e3
| op(e3,e3) = e1
| op(e3,e0) = e0 ),
inference(sr,[status(thm)],[20899,153,theory(equality)]) ).
cnf(21013,plain,
( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e0) = e0
| op(e2,e3) != e1 ),
inference(csr,[status(thm)],[20860,20498]) ).
cnf(21164,plain,
( op(e3,e0) = e0
| op(e3,e3) = e1
| op(e1,e3) = e3
| op(e3,e3) = e0
| e3 != op(e3,e0) ),
inference(spm,[status(thm)],[125,20935,theory(equality)]) ).
cnf(21242,plain,
( op(e3,e0) = e1
| op(e0,e0) = e1
| op(e2,e0) = e1
| op(e3,e3) = e1
| op(e0,e3) = e1 ),
inference(csr,[status(thm)],[1244,410]) ).
cnf(21243,plain,
( op(e3,e0) = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e0,e3) = e1 ),
inference(csr,[status(thm)],[21242,411]) ).
cnf(21267,plain,
( e1 = e3
| op(e3,e3) = e2
| e1 = e2
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e0,e3) = e1
| op(e3,e0) = e1 ),
inference(spm,[status(thm)],[3560,21243,theory(equality)]) ).
cnf(21302,plain,
( op(e3,e3) = e2
| e1 = e2
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e0,e3) = e1
| op(e3,e0) = e1 ),
inference(sr,[status(thm)],[21267,151,theory(equality)]) ).
cnf(21303,plain,
( op(e3,e3) = e2
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e0,e3) = e1
| op(e3,e0) = e1 ),
inference(sr,[status(thm)],[21302,152,theory(equality)]) ).
cnf(21534,plain,
( op(e3,e0) = e0
| op(e3,e3) = e1
| op(e1,e3) = e3
| op(e3,e3) = e0 ),
inference(csr,[status(thm)],[21164,20347]) ).
cnf(21541,plain,
( e3 = e1
| op(e2,e3) = e1
| op(e0,e3) = e1
| op(e3,e3) = e1
| op(e3,e3) = e0
| op(e3,e0) = e0 ),
inference(spm,[status(thm)],[54,21534,theory(equality)]) ).
cnf(21601,plain,
( op(e2,e3) = e1
| op(e0,e3) = e1
| op(e3,e3) = e1
| op(e3,e3) = e0
| op(e3,e0) = e0 ),
inference(sr,[status(thm)],[21541,151,theory(equality)]) ).
cnf(21860,plain,
( op(e2,e3) = e1
| op(e3,e0) = e0
| op(e3,e3) = e0
| op(e3,e3) = e1 ),
inference(csr,[status(thm)],[21601,19440]) ).
cnf(21861,plain,
( op(e3,e0) = e0
| op(e3,e3) = e0
| op(e3,e3) = e1 ),
inference(csr,[status(thm)],[21860,21013]) ).
cnf(26271,plain,
( e3 = e1
| op(e0,e0) = e1
| op(e3,e3) = e1
| op(e0,e0) = e3
| op(e0,e1) = e2
| op(e3,e1) = e2 ),
inference(spm,[status(thm)],[407,1675,theory(equality)]) ).
cnf(26316,plain,
( op(e0,e0) = e1
| op(e3,e3) = e1
| op(e0,e0) = e3
| op(e0,e1) = e2
| op(e3,e1) = e2 ),
inference(sr,[status(thm)],[26271,151,theory(equality)]) ).
cnf(26357,plain,
( op(e3,e1) = e2
| op(e0,e0) = e3
| op(e3,e3) = e1
| op(e0,e0) = e1
| e2 != op(e0,e0) ),
inference(spm,[status(thm)],[105,26316,theory(equality)]) ).
cnf(26631,plain,
( e2 = e1
| op(e3,e3) = e1
| e2 = e3
| op(e3,e1) = e2
| op(e0,e3) = e2
| op(e3,e0) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[26357,3179,theory(equality)]) ).
cnf(26647,plain,
( op(e3,e3) = e1
| e2 = e3
| op(e3,e1) = e2
| op(e0,e3) = e2
| op(e3,e0) = e2
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[26631,152,theory(equality)]) ).
cnf(26648,plain,
( op(e3,e3) = e1
| op(e3,e1) = e2
| op(e0,e3) = e2
| op(e3,e0) = e2
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[26647,150,theory(equality)]) ).
cnf(31176,plain,
( op(e3,e2) = e1
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e3) = e1
| op(e0,e3) != e2 ),
inference(csr,[status(thm)],[7145,21303]) ).
cnf(31178,plain,
( e2 = e1
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e2 ),
inference(spm,[status(thm)],[31176,16789,theory(equality)]) ).
cnf(31180,plain,
( e2 = e1
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e2) = e1
| op(e3,e0) = e2
| op(e3,e1) = e2 ),
inference(spm,[status(thm)],[31176,26648,theory(equality)]) ).
cnf(31182,plain,
( op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e2 ),
inference(sr,[status(thm)],[31178,152,theory(equality)]) ).
cnf(31184,plain,
( op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e2) = e1
| op(e3,e0) = e2
| op(e3,e1) = e2 ),
inference(sr,[status(thm)],[31180,152,theory(equality)]) ).
cnf(31322,plain,
( op(e3,e0) = e2
| e2 = e1
| op(e3,e2) = e1
| op(e3,e3) = e2
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[31182,31184,theory(equality)]) ).
cnf(31326,plain,
( op(e3,e0) = e2
| op(e3,e2) = e1
| op(e3,e3) = e2
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[31322,152,theory(equality)]) ).
cnf(31370,plain,
( op(e3,e3) = e2
| e1 = e2
| e1 = e0
| e1 = e3
| op(e3,e3) = e1
| op(e3,e0) = e2 ),
inference(spm,[status(thm)],[14649,31326,theory(equality)]) ).
cnf(31385,plain,
( op(e3,e3) = e2
| e1 = e0
| e1 = e3
| op(e3,e3) = e1
| op(e3,e0) = e2 ),
inference(sr,[status(thm)],[31370,152,theory(equality)]) ).
cnf(31386,plain,
( op(e3,e3) = e2
| e1 = e3
| op(e3,e3) = e1
| op(e3,e0) = e2 ),
inference(sr,[status(thm)],[31385,155,theory(equality)]) ).
cnf(31387,plain,
( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e0) = e2 ),
inference(sr,[status(thm)],[31386,151,theory(equality)]) ).
cnf(31421,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e3) = e2
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[14666,31387,theory(equality)]) ).
cnf(31759,plain,
( op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e2) = e3
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[82,31421,theory(equality)]) ).
cnf(32119,plain,
( op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e2) = e3 ),
inference(csr,[status(thm)],[31759,2900]) ).
cnf(32133,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[1043,32119,theory(equality)]) ).
cnf(32191,plain,
( op(e3,e3) = e1
| op(e0,e0) = e3
| op(e3,e3) = e2
| e2 != op(e3,e0) ),
inference(spm,[status(thm)],[127,32133,theory(equality)]) ).
cnf(32463,plain,
( op(e3,e3) = e1
| op(e0,e0) = e3
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[32191,31387]) ).
cnf(32467,plain,
( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e3) != e1
| op(e3,e0) != e2 ),
inference(spm,[status(thm)],[228,32463,theory(equality)]) ).
cnf(32498,plain,
( op(e3,e3) = e1
| op(e0,e3) = e1
| e3 = e1
| op(e3,e0) = e1
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[21243,32463,theory(equality)]) ).
cnf(32518,plain,
( op(e3,e3) = e1
| op(e0,e3) = e1
| op(e3,e0) = e1
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[32498,151,theory(equality)]) ).
cnf(32533,plain,
( op(e3,e3) = e2
| op(e3,e3) = e1
| op(e0,e3) != e1 ),
inference(csr,[status(thm)],[32467,31387]) ).
cnf(32555,plain,
( op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e0) = e1 ),
inference(csr,[status(thm)],[32518,32533]) ).
cnf(32597,plain,
( e1 = e2
| op(e3,e3) = e1
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[31387,32555,theory(equality)]) ).
cnf(32605,plain,
( op(e3,e3) = e1
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[32597,152,theory(equality)]) ).
cnf(32612,plain,
( op(e3,e3) = e2
| op(e3,e1) != e2
| op(e1,e3) != e0 ),
inference(spm,[status(thm)],[242,32605,theory(equality)]) ).
cnf(32613,plain,
( op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e0) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[421,32605,theory(equality)]) ).
cnf(32615,plain,
( op(e3,e1) = e3
| op(e3,e1) = e0
| op(e3,e1) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[518,32605,theory(equality)]) ).
cnf(32616,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| op(e0,e3) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[612,32605,theory(equality)]) ).
cnf(32617,plain,
( op(e2,e3) = e3
| op(e2,e3) = e0
| op(e2,e3) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[690,32605,theory(equality)]) ).
cnf(32618,plain,
( op(e1,e3) = e3
| op(e1,e3) = e0
| op(e1,e3) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[769,32605,theory(equality)]) ).
cnf(32621,plain,
( e1 = e0
| op(e2,e2) = e2
| op(e2,e2) = e0
| op(e2,e2) = e3
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[5255,32605,theory(equality)]) ).
cnf(32622,plain,
( e1 = e2
| op(e0,e0) = e2
| op(e0,e0) = e0
| op(e0,e0) = e3
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[5298,32605,theory(equality)]) ).
cnf(32623,plain,
( op(e2,e2) = e0
| e1 = e0
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[6029,32605,theory(equality)]) ).
cnf(32625,plain,
( op(e2,e2) = e2
| op(e2,e2) = e0
| op(e2,e2) = e3
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[32621,155,theory(equality)]) ).
cnf(32626,plain,
( op(e0,e0) = e2
| op(e0,e0) = e0
| op(e0,e0) = e3
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[32622,152,theory(equality)]) ).
cnf(32627,plain,
( op(e2,e2) = e0
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[32623,155,theory(equality)]) ).
cnf(32659,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e3) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3 ),
inference(spm,[status(thm)],[14666,32613,theory(equality)]) ).
cnf(32680,plain,
( op(e3,e3) = e2
| op(e3,e1) = e0
| op(e3,e1) = e3
| e2 != op(e3,e0) ),
inference(spm,[status(thm)],[87,32615,theory(equality)]) ).
cnf(32681,plain,
( op(e3,e3) = e2
| op(e3,e1) = e0
| op(e3,e1) = e3
| e2 != op(e3,e2) ),
inference(spm,[status(thm)],[84,32615,theory(equality)]) ).
cnf(32791,plain,
( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e0) = e2
| op(e1,e3) != e0 ),
inference(spm,[status(thm)],[32612,53,theory(equality)]) ).
cnf(32800,plain,
( op(e3,e3) = e2
| op(e2,e3) = e0
| op(e2,e3) = e3
| e2 != op(e0,e3) ),
inference(spm,[status(thm)],[110,32617,theory(equality)]) ).
cnf(32802,plain,
( op(e1,e1) = e3
| op(e0,e0) = e3
| op(e3,e3) = e2
| op(e2,e3) = e0
| op(e2,e3) = e3 ),
inference(spm,[status(thm)],[310,32617,theory(equality)]) ).
cnf(32814,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e0) = e2
| op(e2,e3) = e0
| op(e2,e3) = e3 ),
inference(spm,[status(thm)],[1280,32617,theory(equality)]) ).
cnf(32899,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e1,e3) = e0
| op(e1,e3) = e3 ),
inference(spm,[status(thm)],[347,32618,theory(equality)]) ).
cnf(33120,plain,
( op(e3,e3) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| e2 != op(e0,e3) ),
inference(spm,[status(thm)],[103,32626,theory(equality)]) ).
cnf(33185,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e1,e3) = e3
| op(e2,e2) = e0 ),
inference(spm,[status(thm)],[347,32627,theory(equality)]) ).
cnf(33386,plain,
( op(e3,e1) = e3
| op(e3,e1) = e0
| op(e3,e3) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3 ),
inference(spm,[status(thm)],[32680,32613,theory(equality)]) ).
cnf(33390,plain,
( op(e3,e1) = e3
| op(e3,e1) = e0
| op(e3,e3) = e2
| op(e3,e2) = e0
| op(e3,e2) = e3 ),
inference(spm,[status(thm)],[32681,14649,theory(equality)]) ).
cnf(33435,plain,
( op(e2,e3) = e3
| op(e2,e3) = e0
| op(e3,e3) = e2
| op(e0,e3) = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[32800,32616,theory(equality)]) ).
cnf(33460,plain,
( op(e1,e3) = e3
| op(e0,e0) = e2
| op(e3,e3) = e2
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[107,32899,theory(equality)]) ).
cnf(33461,plain,
( op(e1,e3) = e3
| op(e0,e0) = e2
| op(e3,e3) = e2
| e0 != op(e0,e3) ),
inference(spm,[status(thm)],[111,32899,theory(equality)]) ).
cnf(33535,plain,
( op(e2,e2) = e0
| op(e0,e0) = e2
| op(e3,e3) = e2
| e3 != op(e0,e3) ),
inference(spm,[status(thm)],[111,33185,theory(equality)]) ).
cnf(33763,plain,
( op(e0,e0) = e0
| op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e3) = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[33120,32616,theory(equality)]) ).
cnf(33875,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e1,e3) = e3
| op(e3,e3) = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[33461,7815,theory(equality)]) ).
cnf(34071,plain,
( op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e3) = e2
| op(e3,e2) = e3
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[82,32659,theory(equality)]) ).
cnf(34359,plain,
( e3 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e0
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[343,32802,theory(equality)]) ).
cnf(34375,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e0
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[34359,150,theory(equality)]) ).
cnf(34385,plain,
( op(e2,e3) = e3
| op(e3,e0) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[106,32814,theory(equality)]) ).
cnf(34796,plain,
( op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e3) = e2
| op(e3,e1) = e3
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[83,33386,theory(equality)]) ).
cnf(34841,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e3) = e2
| op(e3,e1) = e3
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[83,33390,theory(equality)]) ).
cnf(34842,plain,
( op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e3) = e2
| op(e3,e1) = e3
| e0 != op(e3,e0) ),
inference(spm,[status(thm)],[87,33390,theory(equality)]) ).
cnf(34910,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| op(e3,e3) = e2
| op(e2,e3) = e3
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[106,33435,theory(equality)]) ).
cnf(36108,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e1,e3) = e3
| op(e0,e3) = e3 ),
inference(csr,[status(thm)],[33875,33460]) ).
cnf(36111,plain,
( op(e0,e3) = e3
| op(e0,e0) = e2
| op(e3,e3) = e2
| e3 != op(e2,e3) ),
inference(spm,[status(thm)],[108,36108,theory(equality)]) ).
cnf(36209,plain,
( op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e3) = e2
| op(e3,e2) = e3 ),
inference(csr,[status(thm)],[34071,20347]) ).
cnf(36336,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3
| op(e2,e3) = e0 ),
inference(csr,[status(thm)],[34375,1045]) ).
cnf(36337,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e2
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[106,36336,theory(equality)]) ).
cnf(36429,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e0,e0) = e2 ),
inference(csr,[status(thm)],[36337,1056]) ).
cnf(36468,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| op(e3,e3) = e2
| e2 = e3
| e2 = e0
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[33763,36429,theory(equality)]) ).
cnf(36493,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| op(e3,e3) = e2
| e2 = e0
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[36468,150,theory(equality)]) ).
cnf(36494,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| op(e3,e3) = e2
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[36493,154,theory(equality)]) ).
cnf(36910,plain,
( op(e2,e3) = e3
| op(e3,e0) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[34385,3286]) ).
cnf(36912,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e0) = e2
| e3 != op(e0,e3) ),
inference(spm,[status(thm)],[110,36910,theory(equality)]) ).
cnf(36982,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e0,e3) = e3
| op(e3,e0) = e2 ),
inference(spm,[status(thm)],[36111,36910,theory(equality)]) ).
cnf(37120,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e3,e0) = e2 ),
inference(csr,[status(thm)],[36982,36912]) ).
cnf(37479,plain,
( op(e3,e0) = e3
| op(e3,e0) = e0
| op(e3,e3) = e2
| op(e3,e1) = e3 ),
inference(csr,[status(thm)],[34796,20347]) ).
cnf(37482,plain,
( op(e3,e3) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3
| e3 != op(e3,e2) ),
inference(spm,[status(thm)],[84,37479,theory(equality)]) ).
cnf(37525,plain,
( op(e3,e3) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3 ),
inference(csr,[status(thm)],[37482,36209]) ).
cnf(37642,plain,
( op(e3,e1) = e3
| op(e3,e3) = e2
| op(e3,e2) = e0
| op(e3,e2) = e3
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[34842,19124,theory(equality)]) ).
cnf(37673,plain,
( op(e0,e3) = e3
| op(e0,e3) = e0
| op(e3,e3) = e2
| op(e2,e3) = e3 ),
inference(csr,[status(thm)],[34910,7815]) ).
cnf(37744,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e0,e3) = e3
| op(e0,e3) = e0 ),
inference(spm,[status(thm)],[36111,37673,theory(equality)]) ).
cnf(37796,plain,
( e2 = e3
| op(e3,e3) = e2
| op(e0,e3) = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[36494,37744,theory(equality)]) ).
cnf(37820,plain,
( op(e3,e3) = e2
| op(e0,e3) = e0
| op(e0,e3) = e3 ),
inference(sr,[status(thm)],[37796,150,theory(equality)]) ).
cnf(37824,plain,
( op(e0,e3) = e3
| op(e3,e3) = e2
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[109,37820,theory(equality)]) ).
cnf(37828,plain,
( op(e1,e1) = e3
| op(e2,e2) = e3
| op(e0,e3) = e3
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[311,37820,theory(equality)]) ).
cnf(37867,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e2) = e0
| op(e0,e3) = e3
| e0 != e3 ),
inference(spm,[status(thm)],[33535,37820,theory(equality)]) ).
cnf(37881,plain,
( e3 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e3) = e3
| op(e2,e2) = e3 ),
inference(spm,[status(thm)],[343,37828,theory(equality)]) ).
cnf(37897,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e3) = e3
| op(e2,e2) = e3 ),
inference(sr,[status(thm)],[37881,150,theory(equality)]) ).
cnf(37934,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e3,e3) = e0
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[3892,37897,theory(equality)]) ).
cnf(38274,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e3) = e3 ),
inference(csr,[status(thm)],[37934,37824]) ).
cnf(38644,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e2) = e0
| op(e0,e3) = e3 ),
inference(csr,[status(thm)],[37867,38274]) ).
cnf(38645,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e2) = e0 ),
inference(csr,[status(thm)],[38644,33535]) ).
cnf(38646,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| e0 != op(e3,e2) ),
inference(spm,[status(thm)],[112,38645,theory(equality)]) ).
cnf(38667,plain,
( op(e2,e3) = e2
| op(e2,e0) = e2
| e0 = e2
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[985,38645,theory(equality)]) ).
cnf(38672,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e1,e2) = e3 ),
inference(spm,[status(thm)],[2372,38645,theory(equality)]) ).
cnf(38680,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e0,e1) = e0
| op(e3,e1) = e0 ),
inference(spm,[status(thm)],[1604,38645,theory(equality)]) ).
cnf(38720,plain,
( op(e2,e3) = e2
| op(e2,e0) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[38667,154,theory(equality)]) ).
cnf(38829,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| e3 != op(e3,e2) ),
inference(spm,[status(thm)],[113,38672,theory(equality)]) ).
cnf(39009,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e3) = e2
| e2 != op(e3,e0) ),
inference(spm,[status(thm)],[124,38720,theory(equality)]) ).
cnf(39205,plain,
( e0 = e2
| op(e0,e2) = e2
| op(e0,e0) = e2
| op(e0,e3) = e2
| op(e3,e1) = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[77,38680,theory(equality)]) ).
cnf(39258,plain,
( op(e0,e2) = e2
| op(e0,e0) = e2
| op(e0,e3) = e2
| op(e3,e1) = e0
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[39205,154,theory(equality)]) ).
cnf(39863,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| op(e2,e3) = e2 ),
inference(csr,[status(thm)],[39009,37120]) ).
cnf(39865,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| e2 != op(e0,e3) ),
inference(spm,[status(thm)],[110,39863,theory(equality)]) ).
cnf(40000,plain,
( op(e3,e1) = e3
| op(e3,e3) = e2
| op(e3,e2) = e0
| op(e3,e2) = e3 ),
inference(csr,[status(thm)],[37642,34841]) ).
cnf(40010,plain,
( op(e2,e2) = e1
| op(e0,e0) = e1
| op(e3,e2) = e3
| op(e3,e2) = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[402,40000,theory(equality)]) ).
cnf(41119,plain,
( op(e0,e2) = e2
| op(e0,e0) = e2
| op(e0,e3) = e2
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[39258,980]) ).
cnf(41120,plain,
( op(e0,e2) = e2
| op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[41119,39865]) ).
cnf(41121,plain,
( op(e3,e3) = e2
| op(e0,e0) = e2
| e2 != op(e3,e2) ),
inference(spm,[status(thm)],[115,41120,theory(equality)]) ).
cnf(41275,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e3,e2) = e0
| op(e3,e2) = e3 ),
inference(spm,[status(thm)],[41121,14649,theory(equality)]) ).
cnf(41331,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2
| op(e3,e2) = e0 ),
inference(csr,[status(thm)],[41275,38829]) ).
cnf(41332,plain,
( op(e0,e0) = e2
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[41331,38646]) ).
cnf(41333,plain,
( op(e3,e3) = e2
| e2 != op(e3,e0) ),
inference(spm,[status(thm)],[127,41332,theory(equality)]) ).
cnf(41398,plain,
( op(e3,e3) = e2
| op(e3,e0) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3
| e1 != e2 ),
inference(spm,[status(thm)],[41333,133,theory(equality)]) ).
cnf(41571,plain,
( op(e3,e3) = e2
| e1 = e3
| e1 = e0
| e1 = e2
| op(e3,e2) = e0
| op(e3,e2) = e3
| op(e0,e0) = e1 ),
inference(spm,[status(thm)],[32625,40010,theory(equality)]) ).
cnf(41642,plain,
( op(e3,e3) = e2
| e1 = e0
| e1 = e2
| op(e3,e2) = e0
| op(e3,e2) = e3
| op(e0,e0) = e1 ),
inference(sr,[status(thm)],[41571,151,theory(equality)]) ).
cnf(41643,plain,
( op(e3,e3) = e2
| e1 = e2
| op(e3,e2) = e0
| op(e3,e2) = e3
| op(e0,e0) = e1 ),
inference(sr,[status(thm)],[41642,155,theory(equality)]) ).
cnf(41644,plain,
( op(e3,e3) = e2
| op(e3,e2) = e0
| op(e3,e2) = e3
| op(e0,e0) = e1 ),
inference(sr,[status(thm)],[41643,152,theory(equality)]) ).
cnf(41681,plain,
( op(e3,e3) = e2
| e1 = e2
| op(e3,e2) = e3
| op(e3,e2) = e0 ),
inference(spm,[status(thm)],[41332,41644,theory(equality)]) ).
cnf(41693,plain,
( op(e3,e3) = e2
| op(e3,e2) = e3
| op(e3,e2) = e0 ),
inference(sr,[status(thm)],[41681,152,theory(equality)]) ).
cnf(41695,plain,
( op(e3,e2) = e3
| op(e3,e3) = e2
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[82,41693,theory(equality)]) ).
cnf(41696,plain,
( op(e3,e2) = e3
| op(e3,e3) = e2
| e0 != op(e3,e0) ),
inference(spm,[status(thm)],[86,41693,theory(equality)]) ).
cnf(41745,plain,
( op(e3,e3) = e2
| op(e3,e2) = e3
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[41696,19124,theory(equality)]) ).
cnf(41758,plain,
( op(e3,e3) = e2
| op(e3,e2) = e3 ),
inference(csr,[status(thm)],[41745,41695]) ).
cnf(41760,plain,
( op(e3,e3) = e2
| e3 != op(e3,e0) ),
inference(spm,[status(thm)],[86,41758,theory(equality)]) ).
cnf(41775,plain,
( op(e0,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[1337,41758,theory(equality)]) ).
cnf(41776,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e3) = e1
| op(e3,e3) = e2
| e3 != e1 ),
inference(spm,[status(thm)],[2163,41758,theory(equality)]) ).
cnf(41955,plain,
( op(e0,e0) = e3
| op(e2,e0) = e3
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[41775,41760]) ).
cnf(41974,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e3,e3) = e2
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[5727,41955,theory(equality)]) ).
cnf(42054,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[41974,5726]) ).
cnf(42240,plain,
( op(e3,e3) = e2
| op(e3,e0) = e2
| op(e3,e0) = e0
| op(e3,e0) = e3 ),
inference(csr,[status(thm)],[41398,37525]) ).
cnf(42241,plain,
( op(e3,e3) = e2
| op(e3,e0) = e2
| op(e3,e0) = e0 ),
inference(csr,[status(thm)],[42240,41760]) ).
cnf(42242,plain,
( op(e3,e3) = e2
| op(e3,e0) = e0 ),
inference(csr,[status(thm)],[42241,41333]) ).
cnf(42243,plain,
( op(e3,e3) = e2
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[85,42242,theory(equality)]) ).
cnf(42316,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e1,e3) = e1
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[41776,42054]) ).
cnf(42317,plain,
( op(e2,e2) = e0
| op(e3,e3) = e0
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[42316,42054]) ).
cnf(42318,plain,
( op(e2,e2) = e0
| op(e3,e3) = e2 ),
inference(csr,[status(thm)],[42317,42243]) ).
cnf(42354,plain,
( e0 = e3
| op(e0,e0) = e3
| op(e1,e0) = e0
| op(e1,e3) = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[2081,42318,theory(equality)]) ).
cnf(42400,plain,
( op(e0,e0) = e3
| op(e1,e0) = e0
| op(e1,e3) = e0
| op(e3,e3) = e2 ),
inference(sr,[status(thm)],[42354,153,theory(equality)]) ).
cnf(42527,plain,
( op(e3,e3) = e2
| op(e1,e3) = e0
| op(e0,e0) = e3
| e0 != op(e3,e0) ),
inference(spm,[status(thm)],[125,42400,theory(equality)]) ).
cnf(42621,plain,
( op(e3,e3) = e2
| op(e1,e3) = e0
| op(e0,e0) = e3 ),
inference(csr,[status(thm)],[42527,42242]) ).
cnf(42670,plain,
( op(e3,e0) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[32791,42621,theory(equality)]) ).
cnf(42797,plain,
( op(e0,e0) = e3
| op(e3,e3) = e2
| op(e3,e2) = e2 ),
inference(csr,[status(thm)],[42670,41333]) ).
cnf(42823,plain,
( op(e3,e3) = e2
| e3 = e2
| op(e3,e2) = e2 ),
inference(spm,[status(thm)],[41332,42797,theory(equality)]) ).
cnf(42832,plain,
( op(e3,e3) = e2
| op(e3,e2) = e2 ),
inference(sr,[status(thm)],[42823,150,theory(equality)]) ).
cnf(42870,plain,
( e2 = e3
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[41758,42832,theory(equality)]) ).
cnf(42875,plain,
op(e3,e3) = e2,
inference(sr,[status(thm)],[42870,150,theory(equality)]) ).
cnf(42937,plain,
( e2 = e1
| op(e3,e0) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e2,e0) = e1
| op(e2,e3) = e1 ),
inference(rw,[status(thm)],[2039,42875,theory(equality)]) ).
cnf(42938,plain,
( op(e3,e0) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e2,e0) = e1
| op(e2,e3) = e1 ),
inference(sr,[status(thm)],[42937,152,theory(equality)]) ).
cnf(43076,plain,
( op(e3,e0) = e0
| e2 = e0
| op(e3,e3) = e1 ),
inference(rw,[status(thm)],[21861,42875,theory(equality)]) ).
cnf(43077,plain,
( op(e3,e0) = e0
| e2 = e0
| e2 = e1 ),
inference(rw,[status(thm)],[43076,42875,theory(equality)]) ).
cnf(43078,plain,
( op(e3,e0) = e0
| e1 = e2 ),
inference(sr,[status(thm)],[43077,154,theory(equality)]) ).
cnf(43079,plain,
op(e3,e0) = e0,
inference(sr,[status(thm)],[43078,152,theory(equality)]) ).
cnf(43108,plain,
( op(e3,e0) = e3
| op(e0,e0) = e3
| op(e0,e3) = e3
| e2 = e3 ),
inference(rw,[status(thm)],[18486,42875,theory(equality)]) ).
cnf(43109,plain,
( op(e3,e0) = e3
| op(e0,e0) = e3
| op(e0,e3) = e3 ),
inference(sr,[status(thm)],[43108,150,theory(equality)]) ).
cnf(43430,plain,
( op(e0,e0) = e0
| e2 = e1
| op(e0,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 ),
inference(rw,[status(thm)],[4380,42875,theory(equality)]) ).
cnf(43431,plain,
( op(e0,e0) = e0
| e2 = e1
| op(e0,e3) = e0
| op(e2,e3) = e0
| e2 = e0 ),
inference(rw,[status(thm)],[43430,42875,theory(equality)]) ).
cnf(43432,plain,
( op(e0,e0) = e0
| op(e0,e3) = e0
| op(e2,e3) = e0
| e2 = e0 ),
inference(sr,[status(thm)],[43431,152,theory(equality)]) ).
cnf(43433,plain,
( op(e0,e0) = e0
| op(e0,e3) = e0
| op(e2,e3) = e0 ),
inference(sr,[status(thm)],[43432,154,theory(equality)]) ).
cnf(43566,plain,
( e2 = e0
| op(e3,e0) = e1
| op(e3,e3) = e1
| op(e0,e0) = e1 ),
inference(rw,[status(thm)],[3480,42875,theory(equality)]) ).
cnf(43567,plain,
( e2 = e0
| op(e3,e0) = e1
| e2 = e1
| op(e0,e0) = e1 ),
inference(rw,[status(thm)],[43566,42875,theory(equality)]) ).
cnf(43568,plain,
( op(e3,e0) = e1
| e1 = e2
| op(e0,e0) = e1 ),
inference(sr,[status(thm)],[43567,154,theory(equality)]) ).
cnf(43569,plain,
( op(e3,e0) = e1
| op(e0,e0) = e1 ),
inference(sr,[status(thm)],[43568,152,theory(equality)]) ).
cnf(43735,plain,
( op(e3,e2) != e1
| op(op(e3,e3),e3) != e0
| op(e3,e3) != e2 ),
inference(rw,[status(thm)],[238,42875,theory(equality)]) ).
cnf(43736,plain,
( op(e3,e2) != e1
| op(e2,e3) != e0
| op(e3,e3) != e2 ),
inference(rw,[status(thm)],[43735,42875,theory(equality)]) ).
cnf(43737,plain,
( op(e3,e2) != e1
| op(e2,e3) != e0
| $false ),
inference(rw,[status(thm)],[43736,42875,theory(equality)]) ).
cnf(43738,plain,
( op(e3,e2) != e1
| op(e2,e3) != e0 ),
inference(cn,[status(thm)],[43737,theory(equality)]) ).
cnf(43924,plain,
op(e1,e0) != e0,
inference(rw,[status(thm)],[125,43079,theory(equality)]) ).
cnf(43925,plain,
op(e2,e0) != e0,
inference(rw,[status(thm)],[124,43079,theory(equality)]) ).
cnf(44109,plain,
( e0 = e1
| op(e0,e0) = e1 ),
inference(rw,[status(thm)],[43569,43079,theory(equality)]) ).
cnf(44110,plain,
op(e0,e0) = e1,
inference(sr,[status(thm)],[44109,155,theory(equality)]) ).
cnf(44147,plain,
( op(e1,e3) = e0
| op(e1,e0) = e0
| e1 = e3
| op(e2,e2) = e3
| op(e0,e0) != e1 ),
inference(rw,[status(thm)],[4144,44110,theory(equality)]) ).
cnf(44148,plain,
( op(e1,e3) = e0
| op(e1,e0) = e0
| e1 = e3
| op(e2,e2) = e3
| $false ),
inference(rw,[status(thm)],[44147,44110,theory(equality)]) ).
cnf(44149,plain,
( op(e1,e3) = e0
| op(e1,e0) = e0
| e1 = e3
| op(e2,e2) = e3 ),
inference(cn,[status(thm)],[44148,theory(equality)]) ).
cnf(44150,plain,
( op(e1,e3) = e0
| e1 = e3
| op(e2,e2) = e3 ),
inference(sr,[status(thm)],[44149,43924,theory(equality)]) ).
cnf(44151,plain,
( op(e1,e3) = e0
| op(e2,e2) = e3 ),
inference(sr,[status(thm)],[44150,151,theory(equality)]) ).
cnf(44239,plain,
( op(e2,e0) = e3
| op(e2,e0) = e0
| op(e2,e0) = e2
| $false ),
inference(rw,[status(thm)],[734,44110,theory(equality)]) ).
cnf(44240,plain,
( op(e2,e0) = e3
| op(e2,e0) = e0
| op(e2,e0) = e2 ),
inference(cn,[status(thm)],[44239,theory(equality)]) ).
cnf(44241,plain,
( op(e2,e0) = e3
| op(e2,e0) = e2 ),
inference(sr,[status(thm)],[44240,43925,theory(equality)]) ).
cnf(44391,plain,
( op(e2,e2) = e3
| e0 != op(e2,e3) ),
inference(spm,[status(thm)],[108,44151,theory(equality)]) ).
cnf(44513,plain,
( e0 = e3
| op(e0,e0) = e3
| op(e0,e3) = e3 ),
inference(rw,[status(thm)],[43109,43079,theory(equality)]) ).
cnf(44514,plain,
( e0 = e3
| e1 = e3
| op(e0,e3) = e3 ),
inference(rw,[status(thm)],[44513,44110,theory(equality)]) ).
cnf(44515,plain,
( e1 = e3
| op(e0,e3) = e3 ),
inference(sr,[status(thm)],[44514,153,theory(equality)]) ).
cnf(44516,plain,
op(e0,e3) = e3,
inference(sr,[status(thm)],[44515,151,theory(equality)]) ).
cnf(44578,plain,
( e1 = e0
| op(e0,e3) = e0
| op(e2,e3) = e0 ),
inference(rw,[status(thm)],[43433,44110,theory(equality)]) ).
cnf(44579,plain,
( e1 = e0
| e3 = e0
| op(e2,e3) = e0 ),
inference(rw,[status(thm)],[44578,44516,theory(equality)]) ).
cnf(44580,plain,
( e0 = e3
| op(e2,e3) = e0 ),
inference(sr,[status(thm)],[44579,155,theory(equality)]) ).
cnf(44581,plain,
op(e2,e3) = e0,
inference(sr,[status(thm)],[44580,153,theory(equality)]) ).
cnf(44588,plain,
( op(e2,e2) = e3
| $false ),
inference(rw,[status(thm)],[44391,44581,theory(equality)]) ).
cnf(44589,plain,
op(e2,e2) = e3,
inference(cn,[status(thm)],[44588,theory(equality)]) ).
cnf(44591,plain,
( op(e3,e2) != e1
| $false ),
inference(rw,[status(thm)],[43738,44581,theory(equality)]) ).
cnf(44592,plain,
op(e3,e2) != e1,
inference(cn,[status(thm)],[44591,theory(equality)]) ).
cnf(44626,plain,
e3 != op(e2,e0),
inference(rw,[status(thm)],[92,44589,theory(equality)]) ).
cnf(44745,plain,
op(e2,e0) = e2,
inference(sr,[status(thm)],[44241,44626,theory(equality)]) ).
cnf(45021,plain,
( e0 = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e2,e0) = e1
| op(e2,e3) = e1 ),
inference(rw,[status(thm)],[42938,43079,theory(equality)]) ).
cnf(45022,plain,
( e0 = e1
| op(e3,e2) = e1
| e3 = e1
| op(e2,e0) = e1
| op(e2,e3) = e1 ),
inference(rw,[status(thm)],[45021,44589,theory(equality)]) ).
cnf(45023,plain,
( e0 = e1
| op(e3,e2) = e1
| e3 = e1
| e2 = e1
| op(e2,e3) = e1 ),
inference(rw,[status(thm)],[45022,44745,theory(equality)]) ).
cnf(45024,plain,
( e0 = e1
| op(e3,e2) = e1
| e3 = e1
| e2 = e1
| e0 = e1 ),
inference(rw,[status(thm)],[45023,44581,theory(equality)]) ).
cnf(45025,plain,
( e0 = e1
| op(e3,e2) = e1
| e3 = e1
| e2 = e1 ),
inference(cn,[status(thm)],[45024,theory(equality)]) ).
cnf(45026,plain,
( op(e3,e2) = e1
| e1 = e3
| e1 = e2 ),
inference(sr,[status(thm)],[45025,155,theory(equality)]) ).
cnf(45027,plain,
( e1 = e3
| e1 = e2 ),
inference(sr,[status(thm)],[45026,44592,theory(equality)]) ).
cnf(45028,plain,
e1 = e2,
inference(sr,[status(thm)],[45027,151,theory(equality)]) ).
cnf(45029,plain,
$false,
inference(sr,[status(thm)],[45028,152,theory(equality)]) ).
cnf(45030,plain,
$false,
45029,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/ALG/ALG142+1.p
% --creating new selector for []
% -running prover on /tmp/tmpRvTI-8/sel_ALG142+1.p_1 with time limit 29
% -prover status Unsatisfiable
% Problem ALG142+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/ALG/ALG142+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/ALG/ALG142+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Unsatisfiable
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------