%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : ALG046+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 03:41:41 EST 2010
% Result : Unsatisfiable 1.08s
% Output : CNFRefutation 1.08s
% Verified :
% SZS Type : None (MakeTreeStats ran out of CPU time)
% Syntax : Number of formulae : 509
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
~ ( e3 = op(e1,op(e1,op(e1,e1)))
& e2 = op(e1,op(e1,e1))
& e0 = op(e1,e1) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax28) ).
fof(4,axiom,
~ ( e2 = op(e3,op(e3,op(e3,e3)))
& e1 = op(e3,op(e3,e3))
& e0 = op(e3,e3) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax24) ).
fof(5,axiom,
~ ( e3 = op(e1,op(e1,op(e1,e1)))
& e0 = op(e1,op(e1,e1))
& e2 = op(e1,e1) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax27) ).
fof(6,axiom,
~ ( e3 = op(e0,op(e0,op(e0,e0)))
& e2 = op(e0,op(e0,e0))
& e1 = op(e0,e0) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax26) ).
fof(8,axiom,
~ ( e2 = op(e0,op(e0,op(e0,e0)))
& e3 = op(e0,op(e0,e0))
& e1 = op(e0,e0) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax20) ).
fof(11,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 ) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax2) ).
fof(12,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/tmpYFkbBO/sel_ALG046+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/tmpYFkbBO/sel_ALG046+1.p_1',ax1) ).
fof(14,axiom,
~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax6) ).
fof(16,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/tmpYFkbBO/sel_ALG046+1.p_1',ax4) ).
fof(17,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax5) ).
fof(19,axiom,
~ ( e0 = op(e2,op(e2,op(e2,e2)))
& e1 = op(e2,op(e2,e2))
& e3 = op(e2,e2) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax9) ).
fof(20,axiom,
~ ( e1 = op(e0,op(e0,op(e0,e0)))
& e3 = op(e0,op(e0,e0))
& e2 = op(e0,e0) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax14) ).
fof(22,axiom,
~ ( e1 = op(e2,op(e2,op(e2,e2)))
& e3 = op(e2,op(e2,e2))
& e0 = op(e2,e2) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax16) ).
fof(24,axiom,
~ ( e0 = op(e2,op(e2,op(e2,e2)))
& e3 = op(e2,op(e2,e2))
& e1 = op(e2,e2) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax10) ).
fof(25,axiom,
~ ( e0 = op(e3,op(e3,op(e3,e3)))
& e1 = op(e3,op(e3,e3))
& e2 = op(e3,e3) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax11) ).
fof(27,axiom,
~ ( e1 = op(e0,op(e0,op(e0,e0)))
& e2 = op(e0,op(e0,e0))
& e3 = op(e0,e0) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax13) ).
fof(29,axiom,
~ ( e2 = op(e0,op(e0,op(e0,e0)))
& e1 = op(e0,op(e0,e0))
& e3 = op(e0,e0) ),
file('/tmp/tmpYFkbBO/sel_ALG046+1.p_1',ax19) ).
fof(33,plain,
( e3 != op(e1,op(e1,op(e1,e1)))
| e2 != op(e1,op(e1,e1))
| e0 != op(e1,e1) ),
inference(fof_nnf,[status(thm)],[2]) ).
cnf(34,plain,
( e0 != op(e1,e1)
| e2 != op(e1,op(e1,e1))
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(split_conjunct,[status(thm)],[33]) ).
fof(37,plain,
( e2 != op(e3,op(e3,op(e3,e3)))
| e1 != op(e3,op(e3,e3))
| e0 != op(e3,e3) ),
inference(fof_nnf,[status(thm)],[4]) ).
cnf(38,plain,
( e0 != op(e3,e3)
| e1 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,op(e3,e3))) ),
inference(split_conjunct,[status(thm)],[37]) ).
fof(39,plain,
( e3 != op(e1,op(e1,op(e1,e1)))
| e0 != op(e1,op(e1,e1))
| e2 != op(e1,e1) ),
inference(fof_nnf,[status(thm)],[5]) ).
cnf(40,plain,
( e2 != op(e1,e1)
| e0 != op(e1,op(e1,e1))
| e3 != op(e1,op(e1,op(e1,e1))) ),
inference(split_conjunct,[status(thm)],[39]) ).
fof(41,plain,
( e3 != op(e0,op(e0,op(e0,e0)))
| e2 != op(e0,op(e0,e0))
| e1 != op(e0,e0) ),
inference(fof_nnf,[status(thm)],[6]) ).
cnf(42,plain,
( e1 != op(e0,e0)
| e2 != op(e0,op(e0,e0))
| e3 != op(e0,op(e0,op(e0,e0))) ),
inference(split_conjunct,[status(thm)],[41]) ).
fof(45,plain,
( e2 != op(e0,op(e0,op(e0,e0)))
| e3 != op(e0,op(e0,e0))
| e1 != op(e0,e0) ),
inference(fof_nnf,[status(thm)],[8]) ).
cnf(46,plain,
( e1 != op(e0,e0)
| e3 != op(e0,op(e0,e0))
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(split_conjunct,[status(thm)],[45]) ).
cnf(51,plain,
( unit = e3
| unit = e2
| unit = e1
| unit = e0 ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(52,plain,
op(e3,unit) = e3,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(53,plain,
op(unit,e3) = e3,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(54,plain,
op(e2,unit) = e2,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(55,plain,
op(unit,e2) = e2,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(56,plain,
op(e1,unit) = e1,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(57,plain,
op(unit,e1) = e1,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(58,plain,
op(e0,unit) = e0,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(59,plain,
op(unit,e0) = e0,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(63,plain,
( op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(64,plain,
( op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(67,plain,
( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(68,plain,
( op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(69,plain,
( op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(72,plain,
( op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(73,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(74,plain,
( op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(75,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(78,plain,
( op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(79,plain,
( op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(83,plain,
( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(84,plain,
( op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(85,plain,
( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(86,plain,
( op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(87,plain,
( op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(88,plain,
( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(89,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(92,plain,
( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(94,plain,
( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(97,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(98,plain,
( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(101,plain,
( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(102,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(103,plain,
( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(104,plain,
( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(106,plain,
( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(107,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ),
inference(split_conjunct,[status(thm)],[13]) ).
fof(108,plain,
( ( op(e0,e0) != e0
| op(e1,e1) != e0
| op(e2,e2) != e0
| op(e3,e3) != e0 )
& ( op(e0,e0) != e1
| op(e1,e1) != e1
| op(e2,e2) != e1
| op(e3,e3) != e1 )
& ( op(e0,e0) != e2
| op(e1,e1) != e2
| op(e2,e2) != e2
| op(e3,e3) != e2 )
& ( op(e0,e0) != e3
| op(e1,e1) != e3
| op(e2,e2) != e3
| op(e3,e3) != e3 ) ),
inference(fof_nnf,[status(thm)],[14]) ).
cnf(109,plain,
( op(e3,e3) != e3
| op(e2,e2) != e3
| op(e1,e1) != e3
| op(e0,e0) != e3 ),
inference(split_conjunct,[status(thm)],[108]) ).
cnf(110,plain,
( op(e3,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) != e2
| op(e0,e0) != e2 ),
inference(split_conjunct,[status(thm)],[108]) ).
cnf(111,plain,
( op(e3,e3) != e1
| op(e2,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) != e1 ),
inference(split_conjunct,[status(thm)],[108]) ).
cnf(112,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ),
inference(split_conjunct,[status(thm)],[108]) ).
cnf(115,plain,
op(e3,e2) != op(e3,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(116,plain,
op(e3,e1) != op(e3,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(117,plain,
op(e3,e1) != op(e3,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(118,plain,
op(e3,e0) != op(e3,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(120,plain,
op(e3,e0) != op(e3,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(121,plain,
op(e2,e2) != op(e2,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(122,plain,
op(e2,e1) != op(e2,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(123,plain,
op(e2,e1) != op(e2,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(124,plain,
op(e2,e0) != op(e2,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(125,plain,
op(e2,e0) != op(e2,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(126,plain,
op(e2,e0) != op(e2,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(127,plain,
op(e1,e2) != op(e1,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(129,plain,
op(e1,e1) != op(e1,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(130,plain,
op(e1,e0) != op(e1,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(131,plain,
op(e1,e0) != op(e1,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(132,plain,
op(e1,e0) != op(e1,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(133,plain,
op(e0,e2) != op(e0,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(134,plain,
op(e0,e1) != op(e0,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(135,plain,
op(e0,e1) != op(e0,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(136,plain,
op(e0,e0) != op(e0,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(138,plain,
op(e0,e0) != op(e0,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(140,plain,
op(e1,e3) != op(e3,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(141,plain,
op(e1,e3) != op(e2,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(142,plain,
op(e0,e3) != op(e3,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(143,plain,
op(e0,e3) != op(e2,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(144,plain,
op(e0,e3) != op(e1,e3),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(145,plain,
op(e2,e2) != op(e3,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(146,plain,
op(e1,e2) != op(e3,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(147,plain,
op(e1,e2) != op(e2,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(148,plain,
op(e0,e2) != op(e3,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(150,plain,
op(e0,e2) != op(e1,e2),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(151,plain,
op(e2,e1) != op(e3,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(152,plain,
op(e1,e1) != op(e3,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(153,plain,
op(e1,e1) != op(e2,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(154,plain,
op(e0,e1) != op(e3,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(155,plain,
op(e0,e1) != op(e2,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(156,plain,
op(e0,e1) != op(e1,e1),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(158,plain,
op(e1,e0) != op(e3,e0),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(159,plain,
op(e1,e0) != op(e2,e0),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(160,plain,
op(e0,e0) != op(e3,e0),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(161,plain,
op(e0,e0) != op(e2,e0),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(162,plain,
op(e0,e0) != op(e1,e0),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(163,plain,
e2 != e3,
inference(split_conjunct,[status(thm)],[17]) ).
cnf(164,plain,
e1 != e3,
inference(split_conjunct,[status(thm)],[17]) ).
cnf(165,plain,
e1 != e2,
inference(split_conjunct,[status(thm)],[17]) ).
cnf(166,plain,
e0 != e3,
inference(split_conjunct,[status(thm)],[17]) ).
cnf(167,plain,
e0 != e2,
inference(split_conjunct,[status(thm)],[17]) ).
cnf(168,plain,
e0 != e1,
inference(split_conjunct,[status(thm)],[17]) ).
fof(171,plain,
( e0 != op(e2,op(e2,op(e2,e2)))
| e1 != op(e2,op(e2,e2))
| e3 != op(e2,e2) ),
inference(fof_nnf,[status(thm)],[19]) ).
cnf(172,plain,
( e3 != op(e2,e2)
| e1 != op(e2,op(e2,e2))
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(split_conjunct,[status(thm)],[171]) ).
fof(173,plain,
( e1 != op(e0,op(e0,op(e0,e0)))
| e3 != op(e0,op(e0,e0))
| e2 != op(e0,e0) ),
inference(fof_nnf,[status(thm)],[20]) ).
cnf(174,plain,
( e2 != op(e0,e0)
| e3 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(split_conjunct,[status(thm)],[173]) ).
fof(177,plain,
( e1 != op(e2,op(e2,op(e2,e2)))
| e3 != op(e2,op(e2,e2))
| e0 != op(e2,e2) ),
inference(fof_nnf,[status(thm)],[22]) ).
cnf(178,plain,
( e0 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,op(e2,e2))) ),
inference(split_conjunct,[status(thm)],[177]) ).
fof(181,plain,
( e0 != op(e2,op(e2,op(e2,e2)))
| e3 != op(e2,op(e2,e2))
| e1 != op(e2,e2) ),
inference(fof_nnf,[status(thm)],[24]) ).
cnf(182,plain,
( e1 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e0 != op(e2,op(e2,op(e2,e2))) ),
inference(split_conjunct,[status(thm)],[181]) ).
fof(183,plain,
( e0 != op(e3,op(e3,op(e3,e3)))
| e1 != op(e3,op(e3,e3))
| e2 != op(e3,e3) ),
inference(fof_nnf,[status(thm)],[25]) ).
cnf(184,plain,
( e2 != op(e3,e3)
| e1 != op(e3,op(e3,e3))
| e0 != op(e3,op(e3,op(e3,e3))) ),
inference(split_conjunct,[status(thm)],[183]) ).
fof(187,plain,
( e1 != op(e0,op(e0,op(e0,e0)))
| e2 != op(e0,op(e0,e0))
| e3 != op(e0,e0) ),
inference(fof_nnf,[status(thm)],[27]) ).
cnf(188,plain,
( e3 != op(e0,e0)
| e2 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,op(e0,e0))) ),
inference(split_conjunct,[status(thm)],[187]) ).
fof(191,plain,
( e2 != op(e0,op(e0,op(e0,e0)))
| e1 != op(e0,op(e0,e0))
| e3 != op(e0,e0) ),
inference(fof_nnf,[status(thm)],[29]) ).
cnf(192,plain,
( e3 != op(e0,e0)
| e1 != op(e0,op(e0,e0))
| e2 != op(e0,op(e0,op(e0,e0))) ),
inference(split_conjunct,[status(thm)],[191]) ).
cnf(198,plain,
( op(e3,e1) = e3
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[52,51,theory(equality)]) ).
cnf(199,plain,
( op(e2,e1) = e2
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[54,51,theory(equality)]) ).
cnf(200,plain,
( op(e0,e1) = e0
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[58,51,theory(equality)]) ).
cnf(201,plain,
( op(e1,e1) = e1
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[56,51,theory(equality)]) ).
cnf(202,plain,
( op(e1,e3) = e3
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[53,51,theory(equality)]) ).
cnf(203,plain,
( op(e1,e2) = e2
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[55,51,theory(equality)]) ).
cnf(204,plain,
( op(e1,e0) = e0
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[59,51,theory(equality)]) ).
cnf(223,plain,
( e0 = e2
| op(e3,e0) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e0) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 ),
inference(spm,[status(thm)],[63,67,theory(equality)]) ).
cnf(225,plain,
( op(e3,e0) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e0) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 ),
inference(sr,[status(thm)],[223,167,theory(equality)]) ).
cnf(321,plain,
( op(e0,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| e1 != op(e1,e3) ),
inference(spm,[status(thm)],[130,88,theory(equality)]) ).
cnf(325,plain,
( op(e0,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| e1 != op(e1,e2) ),
inference(spm,[status(thm)],[131,88,theory(equality)]) ).
cnf(351,plain,
( op(e0,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| e2 != op(e1,e0) ),
inference(spm,[status(thm)],[132,78,theory(equality)]) ).
cnf(392,plain,
( e0 = e3
| op(e2,e0) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e0) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 ),
inference(spm,[status(thm)],[69,75,theory(equality)]) ).
cnf(394,plain,
( op(e2,e0) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e0) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 ),
inference(sr,[status(thm)],[392,166,theory(equality)]) ).
cnf(396,plain,
( op(e2,e0) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| e1 != op(e3,e1) ),
inference(spm,[status(thm)],[151,73,theory(equality)]) ).
cnf(409,plain,
( op(e2,e2) = e0
| op(e2,e2) = e2
| op(e2,e2) = e3
| e1 != op(e3,e2) ),
inference(spm,[status(thm)],[145,97,theory(equality)]) ).
cnf(456,plain,
( op(e0,e0) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| e1 != op(e3,e1) ),
inference(spm,[status(thm)],[154,89,theory(equality)]) ).
cnf(457,plain,
( op(e0,e0) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| e1 != op(e2,e1) ),
inference(spm,[status(thm)],[155,89,theory(equality)]) ).
cnf(476,plain,
( op(e0,e0) = e0
| op(e0,e0) = e2
| op(e0,e0) = e3
| e1 != op(e3,e0) ),
inference(spm,[status(thm)],[160,107,theory(equality)]) ).
cnf(477,plain,
( op(e0,e0) = e0
| op(e0,e0) = e2
| op(e0,e0) = e3
| e1 != op(e2,e0) ),
inference(spm,[status(thm)],[161,107,theory(equality)]) ).
cnf(484,plain,
( op(e0,e1) = e0
| op(e0,e1) = e2
| op(e0,e1) = e3
| e1 != op(e2,e1) ),
inference(spm,[status(thm)],[155,106,theory(equality)]) ).
cnf(539,plain,
( e0 = e2
| op(e0,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e1,e0) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 ),
inference(spm,[status(thm)],[78,83,theory(equality)]) ).
cnf(544,plain,
( op(e0,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e1,e0) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 ),
inference(sr,[status(thm)],[539,167,theory(equality)]) ).
cnf(572,plain,
( op(e1,e2) = e0
| op(e1,e2) = e2
| op(e1,e2) = e3
| e1 != op(e1,e3) ),
inference(spm,[status(thm)],[127,101,theory(equality)]) ).
cnf(585,plain,
( op(e1,e0) = e0
| op(e1,e0) = e2
| op(e1,e0) = e3
| e1 != op(e1,e3) ),
inference(spm,[status(thm)],[130,103,theory(equality)]) ).
cnf(586,plain,
( op(e1,e0) = e0
| op(e1,e0) = e2
| op(e1,e0) = e3
| e1 != op(e1,e2) ),
inference(spm,[status(thm)],[131,103,theory(equality)]) ).
cnf(596,plain,
( op(e1,e1) = e0
| op(e1,e1) = e2
| op(e1,e1) = e3
| e1 != op(e3,e1) ),
inference(spm,[status(thm)],[152,102,theory(equality)]) ).
cnf(601,plain,
( op(e1,e1) = e0
| op(e1,e1) = e2
| op(e1,e1) = e3
| e1 != op(e1,e0) ),
inference(spm,[status(thm)],[132,102,theory(equality)]) ).
cnf(664,plain,
( op(e0,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e1,op(e1,e2)) != e3
| op(e1,e2) != e0 ),
inference(spm,[status(thm)],[40,78,theory(equality)]) ).
cnf(692,plain,
( unit = e3
| unit = e2
| unit = e0
| e3 != op(e3,e0) ),
inference(spm,[status(thm)],[120,198,theory(equality)]) ).
cnf(693,plain,
( e3 = e2
| op(e3,e0) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[63,198,theory(equality)]) ).
cnf(696,plain,
( op(e3,e0) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[693,163,theory(equality)]) ).
cnf(703,plain,
( e2 = e3
| op(e2,e0) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[69,199,theory(equality)]) ).
cnf(704,plain,
( e2 = e0
| op(e2,e0) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[75,199,theory(equality)]) ).
cnf(705,plain,
( e2 = e1
| op(e2,e0) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[73,199,theory(equality)]) ).
cnf(706,plain,
( op(e2,e0) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[703,163,theory(equality)]) ).
cnf(707,plain,
( op(e2,e0) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[704,167,theory(equality)]) ).
cnf(708,plain,
( op(e2,e0) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[705,165,theory(equality)]) ).
cnf(721,plain,
( unit = e3
| unit = e2
| unit = e0
| e0 != op(e0,e2) ),
inference(spm,[status(thm)],[135,200,theory(equality)]) ).
cnf(723,plain,
( e0 = e3
| op(e0,e0) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[85,200,theory(equality)]) ).
cnf(724,plain,
( e0 = e2
| op(e0,e0) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[87,200,theory(equality)]) ).
cnf(725,plain,
( e0 = e1
| op(e0,e0) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[89,200,theory(equality)]) ).
cnf(726,plain,
( op(e0,e0) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[723,166,theory(equality)]) ).
cnf(727,plain,
( op(e0,e0) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[724,167,theory(equality)]) ).
cnf(728,plain,
( op(e0,e0) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[725,168,theory(equality)]) ).
cnf(754,plain,
( unit = e3
| unit = e2
| unit = e0
| e3 != op(e2,e3) ),
inference(spm,[status(thm)],[141,202,theory(equality)]) ).
cnf(755,plain,
( unit = e3
| unit = e2
| unit = e0
| e3 != op(e0,e3) ),
inference(spm,[status(thm)],[144,202,theory(equality)]) ).
cnf(758,plain,
( e3 = e1
| op(e0,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[64,202,theory(equality)]) ).
cnf(761,plain,
( op(e0,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[758,164,theory(equality)]) ).
cnf(762,plain,
( unit = e3
| unit = e2
| unit = e0
| e2 != op(e3,e2) ),
inference(spm,[status(thm)],[146,203,theory(equality)]) ).
cnf(764,plain,
( unit = e3
| unit = e2
| unit = e0
| e2 != op(e0,e2) ),
inference(spm,[status(thm)],[150,203,theory(equality)]) ).
cnf(767,plain,
( e2 = e0
| op(e0,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[74,203,theory(equality)]) ).
cnf(768,plain,
( e2 = e1
| op(e0,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[72,203,theory(equality)]) ).
cnf(770,plain,
( op(e0,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[767,167,theory(equality)]) ).
cnf(771,plain,
( op(e0,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[768,165,theory(equality)]) ).
cnf(782,plain,
( unit = e3
| unit = e2
| unit = e0
| e0 != op(e2,e0) ),
inference(spm,[status(thm)],[159,204,theory(equality)]) ).
cnf(786,plain,
( e0 = e3
| op(e0,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[84,204,theory(equality)]) ).
cnf(789,plain,
( op(e0,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[786,166,theory(equality)]) ).
cnf(871,plain,
( op(e3,e0) = e2
| op(e3,e3) = e2
| unit = e0
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[696,762]) ).
cnf(915,plain,
( op(e2,e0) = e3
| op(e2,e2) = e3
| unit = e0
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[706,754]) ).
cnf(931,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| unit = e0
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[707,782]) ).
cnf(936,plain,
( op(e2,e3) = e0
| unit = e0
| unit = e2
| unit = e3
| op(e2,op(e2,e0)) != e1
| op(e2,e0) != e3 ),
inference(spm,[status(thm)],[178,931,theory(equality)]) ).
cnf(959,plain,
( op(e2,e2) = e3
| e1 = e3
| unit = e0
| unit = e2
| unit = e3
| op(e2,e3) = e1
| op(e2,e2) = e1 ),
inference(spm,[status(thm)],[915,708,theory(equality)]) ).
cnf(960,plain,
( op(e2,e2) = e3
| unit = e0
| unit = e2
| unit = e3
| op(e2,e3) = e1
| op(e2,e2) = e1 ),
inference(sr,[status(thm)],[959,164,theory(equality)]) ).
cnf(978,plain,
( op(e0,e0) = e3
| op(e0,e2) = e3
| unit = e0
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[726,755]) ).
cnf(980,plain,
( op(e0,e2) = e3
| unit = e0
| unit = e2
| unit = e3
| e3 != op(e2,e0) ),
inference(spm,[status(thm)],[161,978,theory(equality)]) ).
cnf(983,plain,
( op(e0,e2) = e3
| unit = e0
| unit = e2
| unit = e3
| op(e0,op(e0,e3)) != e1
| op(e0,e3) != e2 ),
inference(spm,[status(thm)],[188,978,theory(equality)]) ).
cnf(1018,plain,
( op(e0,e0) = e2
| op(e0,e3) = e2
| unit = e0
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[727,764]) ).
cnf(1019,plain,
( op(e0,e3) = e2
| unit = e0
| unit = e2
| unit = e3
| e2 != op(e3,e0) ),
inference(spm,[status(thm)],[160,1018,theory(equality)]) ).
cnf(1025,plain,
( op(e0,e3) = e2
| unit = e0
| unit = e2
| unit = e3
| op(e0,op(e0,e2)) != e1
| op(e0,e2) != e3 ),
inference(spm,[status(thm)],[174,1018,theory(equality)]) ).
cnf(1030,plain,
( op(e0,e2) = e3
| e2 = e3
| unit = e0
| unit = e2
| unit = e3
| op(e0,e3) = e2 ),
inference(spm,[status(thm)],[978,1018,theory(equality)]) ).
cnf(1031,plain,
( op(e0,e2) = e3
| unit = e0
| unit = e2
| unit = e3
| op(e0,e3) = e2 ),
inference(sr,[status(thm)],[1030,163,theory(equality)]) ).
cnf(1055,plain,
( op(e0,e3) = e2
| unit = e3
| unit = e2
| unit = e0
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[1019,871,theory(equality)]) ).
cnf(1120,plain,
( op(e0,e3) = e2
| e1 = e2
| unit = e0
| unit = e2
| unit = e3
| op(e0,e3) = e1
| op(e0,e2) = e1 ),
inference(spm,[status(thm)],[1018,728,theory(equality)]) ).
cnf(1122,plain,
( op(e0,e3) = e2
| unit = e0
| unit = e2
| unit = e3
| op(e0,e3) = e1
| op(e0,e2) = e1 ),
inference(sr,[status(thm)],[1120,165,theory(equality)]) ).
cnf(1180,plain,
( op(e3,e2) = e0
| op(e2,e2) = e0
| unit = e0
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[770,721]) ).
cnf(1182,plain,
( op(e3,e2) = e0
| unit = e0
| unit = e2
| unit = e3
| e0 != op(e2,e3) ),
inference(spm,[status(thm)],[121,1180,theory(equality)]) ).
cnf(1212,plain,
( op(e0,e3) = e2
| e1 = e3
| unit = e3
| unit = e2
| unit = e0
| op(e3,e2) = e1
| op(e2,e2) = e1 ),
inference(spm,[status(thm)],[1031,771,theory(equality)]) ).
cnf(1216,plain,
( op(e0,e3) = e2
| unit = e3
| unit = e2
| unit = e0
| op(e3,e2) = e1
| op(e2,e2) = e1 ),
inference(sr,[status(thm)],[1212,164,theory(equality)]) ).
cnf(1237,plain,
( op(e0,e0) = e3
| op(e2,e0) = e3
| unit = e0
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[789,692]) ).
cnf(1249,plain,
( op(e0,e3) = e2
| e3 = e2
| unit = e0
| unit = e2
| unit = e3
| op(e2,e0) = e3 ),
inference(spm,[status(thm)],[1018,1237,theory(equality)]) ).
cnf(1250,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| e3 = e1
| unit = e0
| unit = e2
| unit = e3
| op(e2,e0) = e3 ),
inference(spm,[status(thm)],[728,1237,theory(equality)]) ).
cnf(1251,plain,
( op(e0,e3) = e2
| unit = e0
| unit = e2
| unit = e3
| op(e2,e0) = e3 ),
inference(sr,[status(thm)],[1249,163,theory(equality)]) ).
cnf(1252,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| unit = e0
| unit = e2
| unit = e3
| op(e2,e0) = e3 ),
inference(sr,[status(thm)],[1250,164,theory(equality)]) ).
cnf(1577,plain,
( op(e2,e3) = e0
| e1 = e0
| unit = e0
| unit = e2
| unit = e3
| op(e2,e3) = e1
| op(e2,e2) = e3 ),
inference(spm,[status(thm)],[931,960,theory(equality)]) ).
cnf(1581,plain,
( op(e2,e3) = e0
| unit = e0
| unit = e2
| unit = e3
| op(e2,e3) = e1
| op(e2,e2) = e3 ),
inference(sr,[status(thm)],[1577,168,theory(equality)]) ).
cnf(1646,plain,
( op(e0,e3) = e2
| e1 = e3
| unit = e3
| unit = e2
| unit = e0
| op(e0,e3) = e1 ),
inference(spm,[status(thm)],[1031,1122,theory(equality)]) ).
cnf(1653,plain,
( op(e0,e3) = e2
| unit = e3
| unit = e2
| unit = e0
| op(e0,e3) = e1 ),
inference(sr,[status(thm)],[1646,164,theory(equality)]) ).
cnf(1748,plain,
( op(e2,e2) = e1
| op(e3,e2) = e1
| unit = e0
| unit = e2
| unit = e3
| e2 != op(e3,e3) ),
inference(spm,[status(thm)],[142,1216,theory(equality)]) ).
cnf(2118,plain,
( op(e2,e3) = e0
| e3 = e0
| unit = e0
| unit = e2
| unit = e3
| op(e2,e3) = e1 ),
inference(spm,[status(thm)],[931,1581,theory(equality)]) ).
cnf(2123,plain,
( op(e2,e3) = e0
| unit = e0
| unit = e2
| unit = e3
| op(e2,e3) = e1 ),
inference(sr,[status(thm)],[2118,166,theory(equality)]) ).
cnf(3727,plain,
( op(e2,e3) = e0
| unit = e3
| unit = e2
| unit = e0
| op(e2,e2) = e3
| op(e2,e3) != e1 ),
inference(spm,[status(thm)],[936,915,theory(equality)]) ).
cnf(3742,plain,
( op(e2,e3) = e0
| op(e2,e2) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(csr,[status(thm)],[3727,2123]) ).
cnf(3752,plain,
( op(e2,e3) = e0
| e3 = e0
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[931,3742,theory(equality)]) ).
cnf(3769,plain,
( op(e2,e3) = e0
| unit = e0
| unit = e2
| unit = e3 ),
inference(sr,[status(thm)],[3752,166,theory(equality)]) ).
cnf(3776,plain,
( op(e3,e2) = e0
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[1182,3769,theory(equality)]) ).
cnf(3904,plain,
( op(e0,e2) = e3
| unit = e0
| unit = e2
| unit = e3
| op(e0,op(e0,e3)) != e1 ),
inference(csr,[status(thm)],[983,1031]) ).
cnf(3909,plain,
( op(e0,e2) = e3
| unit = e3
| unit = e2
| unit = e0
| op(e3,e3) = e2
| op(e0,e2) != e1 ),
inference(spm,[status(thm)],[3904,1055,theory(equality)]) ).
cnf(3914,plain,
( op(e0,e2) = e3
| unit = e3
| unit = e2
| unit = e0
| op(e2,e0) = e3
| op(e0,e2) != e1 ),
inference(spm,[status(thm)],[3904,1251,theory(equality)]) ).
cnf(3947,plain,
( op(e3,e3) = e2
| e1 = e3
| unit = e0
| unit = e2
| unit = e3
| op(e3,e2) = e1
| op(e2,e2) = e1 ),
inference(spm,[status(thm)],[3909,771,theory(equality)]) ).
cnf(3957,plain,
( op(e3,e3) = e2
| unit = e0
| unit = e2
| unit = e3
| op(e3,e2) = e1
| op(e2,e2) = e1 ),
inference(sr,[status(thm)],[3947,164,theory(equality)]) ).
cnf(3964,plain,
( op(e2,e2) = e1
| op(e3,e2) = e1
| unit = e3
| unit = e2
| unit = e0 ),
inference(csr,[status(thm)],[3957,1748]) ).
cnf(3988,plain,
( op(e0,e2) = e3
| unit = e3
| unit = e2
| unit = e0
| op(e0,e2) != e1 ),
inference(csr,[status(thm)],[3914,980]) ).
cnf(3997,plain,
( e1 = e3
| unit = e0
| unit = e2
| unit = e3
| op(e2,e0) = e3
| op(e0,e3) = e1 ),
inference(spm,[status(thm)],[3988,1252,theory(equality)]) ).
cnf(4006,plain,
( unit = e0
| unit = e2
| unit = e3
| op(e2,e0) = e3
| op(e0,e3) = e1 ),
inference(sr,[status(thm)],[3997,164,theory(equality)]) ).
cnf(4061,plain,
( op(e2,e0) = e3
| e1 = e2
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[1251,4006,theory(equality)]) ).
cnf(4077,plain,
( op(e2,e0) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(sr,[status(thm)],[4061,165,theory(equality)]) ).
cnf(4085,plain,
( op(e0,e2) = e3
| unit = e3
| unit = e2
| unit = e0 ),
inference(spm,[status(thm)],[980,4077,theory(equality)]) ).
cnf(4236,plain,
( op(e0,e3) = e2
| unit = e0
| unit = e2
| unit = e3
| op(e0,op(e0,e2)) != e1 ),
inference(csr,[status(thm)],[1025,4085]) ).
cnf(4244,plain,
( op(e0,e3) = e2
| unit = e3
| unit = e2
| unit = e0
| op(e0,e3) != e1 ),
inference(spm,[status(thm)],[4236,4085,theory(equality)]) ).
cnf(4277,plain,
( op(e0,e3) = e2
| unit = e3
| unit = e2
| unit = e0 ),
inference(csr,[status(thm)],[4244,1653]) ).
cnf(4285,plain,
( op(e3,e3) = e1
| op(e2,e3) = e1
| e2 = e1
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[761,4277,theory(equality)]) ).
cnf(4299,plain,
( op(e3,e3) = e1
| op(e2,e3) = e1
| unit = e0
| unit = e2
| unit = e3 ),
inference(sr,[status(thm)],[4285,165,theory(equality)]) ).
cnf(4364,plain,
( e1 = e0
| unit = e3
| unit = e2
| unit = e0
| op(e3,e3) = e1 ),
inference(spm,[status(thm)],[3769,4299,theory(equality)]) ).
cnf(4366,plain,
( unit = e3
| unit = e2
| unit = e0
| op(e3,e3) = e1 ),
inference(sr,[status(thm)],[4364,168,theory(equality)]) ).
cnf(4370,plain,
( unit = e0
| unit = e2
| unit = e3
| op(e2,e2) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(spm,[status(thm)],[111,4366,theory(equality)]) ).
cnf(4466,plain,
( unit = e0
| unit = e2
| unit = e3
| op(e2,e2) != e1
| op(e0,e0) != e1 ),
inference(csr,[status(thm)],[4370,201]) ).
cnf(4468,plain,
( unit = e3
| unit = e2
| unit = e0
| op(e3,e2) = e1
| op(e0,e0) != e1 ),
inference(spm,[status(thm)],[4466,3964,theory(equality)]) ).
cnf(4471,plain,
( op(e3,e2) = e1
| unit = e0
| unit = e2
| unit = e3
| op(e0,e3) = e1
| op(e0,e2) = e1 ),
inference(spm,[status(thm)],[4468,728,theory(equality)]) ).
cnf(4512,plain,
( e1 = e3
| unit = e0
| unit = e2
| unit = e3
| op(e0,e3) = e1
| op(e3,e2) = e1 ),
inference(spm,[status(thm)],[4085,4471,theory(equality)]) ).
cnf(4519,plain,
( unit = e0
| unit = e2
| unit = e3
| op(e0,e3) = e1
| op(e3,e2) = e1 ),
inference(sr,[status(thm)],[4512,164,theory(equality)]) ).
cnf(4532,plain,
( e1 = e2
| unit = e0
| unit = e2
| unit = e3
| op(e3,e2) = e1 ),
inference(spm,[status(thm)],[4277,4519,theory(equality)]) ).
cnf(4539,plain,
( unit = e0
| unit = e2
| unit = e3
| op(e3,e2) = e1 ),
inference(sr,[status(thm)],[4532,165,theory(equality)]) ).
cnf(4548,plain,
( e1 = e0
| unit = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[3776,4539,theory(equality)]) ).
cnf(4550,plain,
( unit = e0
| unit = e2
| unit = e3 ),
inference(sr,[status(thm)],[4548,168,theory(equality)]) ).
cnf(4599,plain,
( op(e3,e0) = e3
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[52,4550,theory(equality)]) ).
cnf(4600,plain,
( op(e2,e0) = e2
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[54,4550,theory(equality)]) ).
cnf(4601,plain,
( op(e0,e0) = e0
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[58,4550,theory(equality)]) ).
cnf(4602,plain,
( op(e1,e0) = e1
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[56,4550,theory(equality)]) ).
cnf(4603,plain,
( op(e0,e3) = e3
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[53,4550,theory(equality)]) ).
cnf(4604,plain,
( op(e0,e2) = e2
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[55,4550,theory(equality)]) ).
cnf(4606,plain,
( op(e0,e1) = e1
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[57,4550,theory(equality)]) ).
cnf(4609,plain,
( op(e3,e3) = e0
| op(e3,e2) = e0
| e3 = e0
| op(e3,e3) = e2
| op(e3,e2) = e2
| e3 = e2
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[225,4599,theory(equality)]) ).
cnf(4616,plain,
( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e3) = e2
| op(e3,e2) = e2
| e2 = e3
| unit = e2
| unit = e3 ),
inference(sr,[status(thm)],[4609,166,theory(equality)]) ).
cnf(4617,plain,
( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e3) = e2
| op(e3,e2) = e2
| unit = e2
| unit = e3 ),
inference(sr,[status(thm)],[4616,163,theory(equality)]) ).
cnf(4624,plain,
( unit = e2
| unit = e3
| e2 != op(e2,e2) ),
inference(spm,[status(thm)],[125,4600,theory(equality)]) ).
cnf(4625,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| e2 = e0
| op(e2,e3) = e3
| op(e2,e2) = e3
| e2 = e3
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[394,4600,theory(equality)]) ).
cnf(4631,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e3) = e3
| op(e2,e2) = e3
| e2 = e3
| unit = e2
| unit = e3 ),
inference(sr,[status(thm)],[4625,167,theory(equality)]) ).
cnf(4632,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e3) = e3
| op(e2,e2) = e3
| unit = e2
| unit = e3 ),
inference(sr,[status(thm)],[4631,163,theory(equality)]) ).
cnf(4668,plain,
( unit = e2
| unit = e3
| e1 != op(e2,e0) ),
inference(spm,[status(thm)],[159,4602,theory(equality)]) ).
cnf(4671,plain,
( unit = e2
| unit = e3
| e1 != op(e1,e2) ),
inference(spm,[status(thm)],[131,4602,theory(equality)]) ).
cnf(4679,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[601,4602,theory(equality)]) ).
cnf(4711,plain,
( unit = e2
| unit = e3
| e3 != op(e2,e3) ),
inference(spm,[status(thm)],[143,4603,theory(equality)]) ).
cnf(4768,plain,
( unit = e2
| unit = e3
| e2 != op(e3,e2) ),
inference(spm,[status(thm)],[148,4604,theory(equality)]) ).
cnf(4783,plain,
( unit = e2
| unit = e3
| e1 != op(e3,e1) ),
inference(spm,[status(thm)],[154,4606,theory(equality)]) ).
cnf(4784,plain,
( unit = e2
| unit = e3
| e1 != op(e2,e1) ),
inference(spm,[status(thm)],[155,4606,theory(equality)]) ).
cnf(4786,plain,
( unit = e2
| unit = e3
| e1 != op(e0,e2) ),
inference(spm,[status(thm)],[135,4606,theory(equality)]) ).
cnf(5021,plain,
( unit = e3
| unit = e2
| op(e0,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 ),
inference(spm,[status(thm)],[4671,72,theory(equality)]) ).
cnf(5037,plain,
( unit = e3
| unit = e2
| op(e3,e1) = e0
| op(e3,e1) = e2
| op(e3,e1) = e3 ),
inference(spm,[status(thm)],[4783,94,theory(equality)]) ).
cnf(5085,plain,
( unit = e3
| unit = e2
| op(e2,e0) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 ),
inference(spm,[status(thm)],[4784,73,theory(equality)]) ).
cnf(5086,plain,
( unit = e3
| unit = e2
| op(e2,e1) = e0
| op(e2,e1) = e2
| op(e2,e1) = e3 ),
inference(spm,[status(thm)],[4784,98,theory(equality)]) ).
cnf(5199,plain,
( op(e3,e2) = e1
| op(e2,e2) = e1
| unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[5021,4786]) ).
cnf(5206,plain,
( op(e3,e2) = e1
| unit = e2
| unit = e3
| op(e2,op(e2,e1)) != e0
| op(e2,e1) != e3 ),
inference(spm,[status(thm)],[182,5199,theory(equality)]) ).
cnf(5251,plain,
( op(e3,e1) = e3
| op(e3,e1) = e2
| unit = e2
| unit = e3
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[116,5037,theory(equality)]) ).
cnf(5278,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[5085,4668]) ).
cnf(5279,plain,
( op(e2,e3) = e1
| unit = e2
| unit = e3
| e1 != op(e3,e2) ),
inference(spm,[status(thm)],[145,5278,theory(equality)]) ).
cnf(5297,plain,
( op(e2,e1) = e3
| op(e2,e1) = e2
| unit = e2
| unit = e3
| e0 != op(e2,e3) ),
inference(spm,[status(thm)],[122,5086,theory(equality)]) ).
cnf(5298,plain,
( op(e2,e1) = e3
| op(e2,e1) = e2
| unit = e2
| unit = e3
| e0 != op(e2,e2) ),
inference(spm,[status(thm)],[123,5086,theory(equality)]) ).
cnf(5531,plain,
( op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e3) = e2
| unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[4617,4768]) ).
cnf(5570,plain,
( op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e2) = e3
| unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[4632,4711]) ).
cnf(5585,plain,
( op(e3,e2) = e1
| e0 = e1
| unit = e2
| unit = e3
| op(e2,e2) = e3
| op(e2,e3) = e0 ),
inference(spm,[status(thm)],[5199,5570,theory(equality)]) ).
cnf(5590,plain,
( op(e3,e2) = e1
| unit = e2
| unit = e3
| op(e2,e2) = e3
| op(e2,e3) = e0 ),
inference(sr,[status(thm)],[5585,168,theory(equality)]) ).
cnf(5605,plain,
( op(e3,e2) = e1
| e3 = e1
| unit = e2
| unit = e3
| op(e2,e3) = e0 ),
inference(spm,[status(thm)],[5199,5590,theory(equality)]) ).
cnf(5610,plain,
( op(e3,e2) = e1
| unit = e2
| unit = e3
| op(e2,e3) = e0 ),
inference(sr,[status(thm)],[5605,164,theory(equality)]) ).
cnf(5623,plain,
( op(e2,e1) = e2
| op(e2,e1) = e3
| unit = e3
| unit = e2
| op(e3,e2) = e1 ),
inference(spm,[status(thm)],[5297,5610,theory(equality)]) ).
cnf(5704,plain,
( op(e3,e2) = e1
| op(e2,e1) = e3
| unit = e2
| unit = e3
| e2 != op(e2,e0) ),
inference(spm,[status(thm)],[126,5623,theory(equality)]) ).
cnf(5762,plain,
( op(e3,e2) = e1
| op(e2,e1) = e3
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[5704,4600]) ).
cnf(5782,plain,
( op(e3,e2) = e1
| unit = e3
| unit = e2
| op(e2,e3) != e0 ),
inference(spm,[status(thm)],[5206,5762,theory(equality)]) ).
cnf(5808,plain,
( op(e3,e2) = e1
| unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[5782,5610]) ).
cnf(5812,plain,
( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e0
| unit = e2
| unit = e3 ),
inference(spm,[status(thm)],[409,5808,theory(equality)]) ).
cnf(5817,plain,
( op(e2,e3) = e1
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[5279,5808,theory(equality)]) ).
cnf(5820,plain,
( op(e3,e3) = e2
| e1 = e0
| op(e3,e3) = e0
| unit = e3
| unit = e2 ),
inference(spm,[status(thm)],[5531,5808,theory(equality)]) ).
cnf(5822,plain,
( op(e3,e3) = e2
| op(e3,e3) = e0
| unit = e3
| unit = e2 ),
inference(sr,[status(thm)],[5820,168,theory(equality)]) ).
cnf(5840,plain,
( op(e3,e3) = e2
| unit = e2
| unit = e3
| op(e2,e2) != e0
| op(e0,e0) != e0
| op(e1,e1) != e0 ),
inference(spm,[status(thm)],[112,5822,theory(equality)]) ).
cnf(5856,plain,
( op(e3,e1) = e2
| op(e3,e1) = e3
| unit = e3
| unit = e2
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[5251,5822,theory(equality)]) ).
cnf(5860,plain,
( op(e2,e2) = e3
| op(e2,e2) = e0
| unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[5812,4624]) ).
cnf(5876,plain,
( op(e2,e1) = e2
| op(e2,e1) = e3
| unit = e3
| unit = e2
| op(e2,e2) = e3 ),
inference(spm,[status(thm)],[5298,5860,theory(equality)]) ).
cnf(5987,plain,
( op(e2,e2) = e3
| op(e2,e1) = e3
| unit = e2
| unit = e3
| e2 != op(e2,e0) ),
inference(spm,[status(thm)],[126,5876,theory(equality)]) ).
cnf(6070,plain,
( op(e2,e2) = e3
| op(e2,e1) = e3
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[5987,4600]) ).
cnf(6071,plain,
( op(e2,e2) = e3
| unit = e3
| unit = e2
| e3 != op(e3,e1) ),
inference(spm,[status(thm)],[151,6070,theory(equality)]) ).
cnf(6463,plain,
( op(e3,e3) = e2
| unit = e2
| unit = e3
| op(e1,e1) != e0
| op(e2,e2) != e0 ),
inference(csr,[status(thm)],[5840,4601]) ).
cnf(6465,plain,
( op(e3,e3) = e2
| unit = e3
| unit = e2
| op(e2,e2) = e3
| op(e1,e1) != e0 ),
inference(spm,[status(thm)],[6463,5860,theory(equality)]) ).
cnf(6487,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| unit = e2
| unit = e3
| op(e1,e1) = e2
| op(e1,e1) = e3 ),
inference(spm,[status(thm)],[6465,4679,theory(equality)]) ).
cnf(6706,plain,
( op(e1,e1) = e3
| op(e3,e3) = e2
| op(e2,e2) = e3
| unit = e3
| unit = e2
| e2 != op(e3,e1) ),
inference(spm,[status(thm)],[152,6487,theory(equality)]) ).
cnf(7252,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e1,e1) = e3
| unit = e2
| unit = e3
| op(e3,e1) = e3 ),
inference(spm,[status(thm)],[6706,5856,theory(equality)]) ).
cnf(7253,plain,
( op(e2,e2) = e3
| op(e3,e3) = e2
| op(e1,e1) = e3
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[7252,6071]) ).
cnf(7255,plain,
( op(e3,e3) = e2
| op(e2,e2) = e3
| unit = e3
| unit = e2
| e3 != op(e2,e1) ),
inference(spm,[status(thm)],[153,7253,theory(equality)]) ).
cnf(7280,plain,
( op(e3,e3) = e2
| op(e2,e2) = e3
| unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[7255,6070]) ).
cnf(7284,plain,
( op(e3,e3) = e2
| unit = e2
| unit = e3
| op(e2,op(e2,e3)) != e0
| op(e2,e3) != e1 ),
inference(spm,[status(thm)],[172,7280,theory(equality)]) ).
cnf(7320,plain,
( op(e3,e3) = e2
| unit = e2
| unit = e3
| op(e2,op(e2,e3)) != e0 ),
inference(csr,[status(thm)],[7284,5817]) ).
cnf(7322,plain,
( op(e3,e3) = e2
| unit = e3
| unit = e2
| op(e2,e1) != e0 ),
inference(spm,[status(thm)],[7320,5817,theory(equality)]) ).
cnf(7328,plain,
( op(e3,e3) = e2
| unit = e2
| unit = e3
| op(e2,e1) = e3
| op(e2,e1) = e2 ),
inference(spm,[status(thm)],[7322,5086,theory(equality)]) ).
cnf(7338,plain,
( op(e2,e1) = e3
| op(e3,e3) = e2
| unit = e3
| unit = e2
| e2 != op(e2,e0) ),
inference(spm,[status(thm)],[126,7328,theory(equality)]) ).
cnf(7415,plain,
( op(e2,e1) = e3
| op(e3,e3) = e2
| unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[7338,4600]) ).
cnf(7418,plain,
( op(e3,e3) = e2
| unit = e2
| unit = e3
| e3 != op(e2,e2) ),
inference(spm,[status(thm)],[123,7415,theory(equality)]) ).
cnf(7455,plain,
( op(e3,e3) = e2
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[7418,7280]) ).
cnf(7461,plain,
( unit = e3
| unit = e2
| op(e3,op(e3,e2)) != e0
| op(e3,e2) != e1 ),
inference(spm,[status(thm)],[184,7455,theory(equality)]) ).
cnf(7480,plain,
( unit = e3
| unit = e2
| op(e3,op(e3,e2)) != e0 ),
inference(csr,[status(thm)],[7461,5808]) ).
cnf(7482,plain,
( unit = e2
| unit = e3
| op(e3,e1) != e0 ),
inference(spm,[status(thm)],[7480,5808,theory(equality)]) ).
cnf(7488,plain,
( unit = e3
| unit = e2
| op(e3,e1) = e3
| op(e3,e1) = e2 ),
inference(spm,[status(thm)],[7482,5037,theory(equality)]) ).
cnf(7490,plain,
( op(e3,e1) = e3
| unit = e2
| unit = e3
| e2 != op(e3,e3) ),
inference(spm,[status(thm)],[116,7488,theory(equality)]) ).
cnf(7539,plain,
( op(e3,e1) = e3
| unit = e2
| unit = e3 ),
inference(csr,[status(thm)],[7490,7455]) ).
cnf(7542,plain,
( unit = e3
| unit = e2
| e3 != op(e3,e0) ),
inference(spm,[status(thm)],[120,7539,theory(equality)]) ).
cnf(7592,plain,
( unit = e3
| unit = e2 ),
inference(csr,[status(thm)],[7542,4599]) ).
cnf(7594,plain,
( op(e3,e2) = e3
| unit = e3 ),
inference(spm,[status(thm)],[52,7592,theory(equality)]) ).
cnf(7595,plain,
( op(e2,e2) = e2
| unit = e3 ),
inference(spm,[status(thm)],[54,7592,theory(equality)]) ).
cnf(7596,plain,
( op(e0,e2) = e0
| unit = e3 ),
inference(spm,[status(thm)],[58,7592,theory(equality)]) ).
cnf(7597,plain,
( op(e1,e2) = e1
| unit = e3 ),
inference(spm,[status(thm)],[56,7592,theory(equality)]) ).
cnf(7598,plain,
( op(e2,e3) = e3
| unit = e3 ),
inference(spm,[status(thm)],[53,7592,theory(equality)]) ).
cnf(7600,plain,
( op(e2,e0) = e0
| unit = e3 ),
inference(spm,[status(thm)],[59,7592,theory(equality)]) ).
cnf(7601,plain,
( op(e2,e1) = e1
| unit = e3 ),
inference(spm,[status(thm)],[57,7592,theory(equality)]) ).
cnf(7602,plain,
( unit = e3
| e3 != op(e3,e3) ),
inference(spm,[status(thm)],[115,7594,theory(equality)]) ).
cnf(7623,plain,
( unit = e3
| e0 != op(e0,e3) ),
inference(spm,[status(thm)],[133,7596,theory(equality)]) ).
cnf(7638,plain,
( unit = e3
| e1 != op(e0,e2) ),
inference(spm,[status(thm)],[150,7597,theory(equality)]) ).
cnf(7646,plain,
( op(e3,e0) = e1
| op(e2,e0) = e1
| op(e0,e0) = e1
| unit = e3 ),
inference(spm,[status(thm)],[325,7597,theory(equality)]) ).
cnf(7651,plain,
( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e0
| unit = e3 ),
inference(spm,[status(thm)],[586,7597,theory(equality)]) ).
cnf(7685,plain,
( unit = e3
| e1 != op(e3,e1) ),
inference(spm,[status(thm)],[151,7601,theory(equality)]) ).
cnf(7688,plain,
( unit = e3
| e1 != op(e2,e0) ),
inference(spm,[status(thm)],[126,7601,theory(equality)]) ).
cnf(7695,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e0) = e1
| unit = e3 ),
inference(spm,[status(thm)],[457,7601,theory(equality)]) ).
cnf(7696,plain,
( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e0
| unit = e3 ),
inference(spm,[status(thm)],[484,7601,theory(equality)]) ).
cnf(7776,plain,
( unit = e3
| op(e3,e1) = e0
| op(e3,e1) = e2
| op(e3,e1) = e3 ),
inference(spm,[status(thm)],[7685,94,theory(equality)]) ).
cnf(7795,plain,
( op(e3,e0) = e1
| op(e0,e0) = e1
| unit = e3 ),
inference(csr,[status(thm)],[7646,7688]) ).
cnf(7798,plain,
( op(e3,e0) = e1
| unit = e3
| e1 != op(e0,e3) ),
inference(spm,[status(thm)],[136,7795,theory(equality)]) ).
cnf(7804,plain,
( op(e3,e0) = e1
| unit = e3
| op(e0,op(e0,e1)) != e2
| op(e0,e1) != e3 ),
inference(spm,[status(thm)],[46,7795,theory(equality)]) ).
cnf(7827,plain,
( op(e3,e0) = e1
| unit = e3
| op(e0,e3) = e0
| op(e0,e3) = e2
| op(e0,e3) = e3 ),
inference(spm,[status(thm)],[7798,104,theory(equality)]) ).
cnf(7872,plain,
( op(e1,e0) = e2
| op(e1,e0) = e3
| unit = e3
| e0 != op(e2,e0) ),
inference(spm,[status(thm)],[159,7651,theory(equality)]) ).
cnf(7947,plain,
( op(e0,e3) = e1
| op(e0,e0) = e1
| unit = e3 ),
inference(csr,[status(thm)],[7695,7638]) ).
cnf(7948,plain,
( op(e0,e3) = e1
| unit = e3
| e1 != op(e3,e0) ),
inference(spm,[status(thm)],[160,7947,theory(equality)]) ).
cnf(7994,plain,
( op(e0,e1) = e2
| op(e0,e1) = e3
| unit = e3
| e0 != op(e0,e2) ),
inference(spm,[status(thm)],[135,7696,theory(equality)]) ).
cnf(8125,plain,
( op(e3,e1) = e3
| op(e3,e1) = e2
| unit = e3
| e0 != op(e3,e3) ),
inference(spm,[status(thm)],[116,7776,theory(equality)]) ).
cnf(8158,plain,
( op(e1,e0) = e2
| op(e1,e0) = e3
| unit = e3 ),
inference(csr,[status(thm)],[7872,7600]) ).
cnf(8162,plain,
( op(e1,e0) = e3
| unit = e3
| e2 != op(e0,e0) ),
inference(spm,[status(thm)],[162,8158,theory(equality)]) ).
cnf(8358,plain,
( op(e0,e1) = e2
| op(e0,e1) = e3
| unit = e3 ),
inference(csr,[status(thm)],[7994,7596]) ).
cnf(8362,plain,
( op(e0,e1) = e3
| unit = e3
| e2 != op(e0,e3) ),
inference(spm,[status(thm)],[134,8358,theory(equality)]) ).
cnf(8679,plain,
( op(e3,e0) = e1
| op(e0,e3) = e3
| op(e0,e3) = e2
| unit = e3 ),
inference(csr,[status(thm)],[7827,7623]) ).
cnf(8693,plain,
( op(e0,e1) = e3
| unit = e3
| op(e0,e3) = e3
| op(e3,e0) = e1 ),
inference(spm,[status(thm)],[8362,8679,theory(equality)]) ).
cnf(8745,plain,
( op(e3,e0) = e1
| unit = e3
| op(e0,e3) = e3
| op(e0,e3) != e2 ),
inference(spm,[status(thm)],[7804,8693,theory(equality)]) ).
cnf(8818,plain,
( op(e3,e0) = e1
| op(e0,e3) = e3
| unit = e3 ),
inference(csr,[status(thm)],[8745,8679]) ).
cnf(8820,plain,
( op(e3,e0) = e1
| unit = e3
| e3 != op(e2,e3) ),
inference(spm,[status(thm)],[143,8818,theory(equality)]) ).
cnf(8847,plain,
( op(e3,e0) = e1
| unit = e3 ),
inference(csr,[status(thm)],[8820,7598]) ).
cnf(8848,plain,
( unit = e3
| e1 != op(e3,e3) ),
inference(spm,[status(thm)],[118,8847,theory(equality)]) ).
cnf(8855,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e0
| unit = e3 ),
inference(spm,[status(thm)],[476,8847,theory(equality)]) ).
cnf(8858,plain,
( op(e0,e3) = e1
| unit = e3 ),
inference(spm,[status(thm)],[7948,8847,theory(equality)]) ).
cnf(8895,plain,
( unit = e3
| op(e3,e3) = e0
| op(e3,e3) = e2
| op(e3,e3) = e3 ),
inference(spm,[status(thm)],[8848,92,theory(equality)]) ).
cnf(8901,plain,
( op(e0,e0) = e2
| op(e0,e0) = e3
| unit = e3
| e0 != op(e2,e0) ),
inference(spm,[status(thm)],[161,8855,theory(equality)]) ).
cnf(8961,plain,
( op(e3,e3) = e0
| op(e3,e3) = e2
| unit = e3 ),
inference(csr,[status(thm)],[8895,7602]) ).
cnf(8970,plain,
( op(e3,e3) = e2
| unit = e3
| op(e3,op(e3,e0)) != e2
| op(e3,e0) != e1 ),
inference(spm,[status(thm)],[38,8961,theory(equality)]) ).
cnf(8981,plain,
( op(e3,e1) = e2
| op(e3,e1) = e3
| unit = e3
| op(e3,e3) = e2 ),
inference(spm,[status(thm)],[8125,8961,theory(equality)]) ).
cnf(9156,plain,
( op(e0,e0) = e2
| op(e0,e0) = e3
| unit = e3 ),
inference(csr,[status(thm)],[8901,7600]) ).
cnf(9176,plain,
( op(e1,e0) = e3
| unit = e3
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[8162,9156,theory(equality)]) ).
cnf(9688,plain,
( op(e3,e3) = e2
| unit = e3
| op(e3,op(e3,e0)) != e2 ),
inference(csr,[status(thm)],[8970,8847]) ).
cnf(9700,plain,
( op(e3,e3) = e2
| unit = e3
| op(e3,e1) != e2 ),
inference(spm,[status(thm)],[9688,8847,theory(equality)]) ).
cnf(9716,plain,
( op(e3,e3) = e2
| unit = e3
| op(e3,e1) = e3 ),
inference(spm,[status(thm)],[9700,8981,theory(equality)]) ).
cnf(9718,plain,
( op(e3,e3) = e2
| unit = e3
| e3 != op(e3,e2) ),
inference(spm,[status(thm)],[117,9716,theory(equality)]) ).
cnf(9812,plain,
( op(e3,e3) = e2
| unit = e3 ),
inference(csr,[status(thm)],[9718,7594]) ).
cnf(9814,plain,
( unit = e3
| op(e2,e2) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(spm,[status(thm)],[110,9812,theory(equality)]) ).
cnf(9862,plain,
( unit = e3
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(csr,[status(thm)],[9814,7595]) ).
cnf(9876,plain,
( unit = e3
| op(e0,e0) = e3
| op(e1,e1) != e2 ),
inference(spm,[status(thm)],[9862,9156,theory(equality)]) ).
cnf(9882,plain,
( op(e0,e0) = e3
| unit = e3
| op(e1,e0) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 ),
inference(spm,[status(thm)],[9876,79,theory(equality)]) ).
cnf(10363,plain,
( op(e0,e0) = e3
| e2 = e3
| unit = e3
| op(e1,e3) = e2
| op(e1,e2) = e2 ),
inference(spm,[status(thm)],[9176,9882,theory(equality)]) ).
cnf(10384,plain,
( op(e0,e0) = e3
| unit = e3
| op(e1,e3) = e2
| op(e1,e2) = e2 ),
inference(sr,[status(thm)],[10363,163,theory(equality)]) ).
cnf(10405,plain,
( e2 = e1
| unit = e3
| op(e1,e3) = e2
| op(e0,e0) = e3 ),
inference(spm,[status(thm)],[7597,10384,theory(equality)]) ).
cnf(10413,plain,
( unit = e3
| op(e1,e3) = e2
| op(e0,e0) = e3 ),
inference(sr,[status(thm)],[10405,165,theory(equality)]) ).
cnf(10415,plain,
( op(e0,e0) = e3
| unit = e3
| e2 != op(e3,e3) ),
inference(spm,[status(thm)],[140,10413,theory(equality)]) ).
cnf(10449,plain,
( op(e0,e0) = e3
| unit = e3 ),
inference(csr,[status(thm)],[10415,9812]) ).
cnf(10455,plain,
( unit = e3
| op(e0,op(e0,e3)) != e2
| op(e0,e3) != e1 ),
inference(spm,[status(thm)],[192,10449,theory(equality)]) ).
cnf(10561,plain,
( unit = e3
| op(e0,op(e0,e3)) != e2 ),
inference(csr,[status(thm)],[10455,8858]) ).
cnf(10571,plain,
( unit = e3
| op(e0,e1) != e2 ),
inference(spm,[status(thm)],[10561,8858,theory(equality)]) ).
cnf(10589,plain,
( unit = e3
| op(e0,e1) = e3 ),
inference(spm,[status(thm)],[10571,8358,theory(equality)]) ).
cnf(10594,plain,
( unit = e3
| e3 != op(e0,e0) ),
inference(spm,[status(thm)],[138,10589,theory(equality)]) ).
cnf(10647,plain,
unit = e3,
inference(csr,[status(thm)],[10594,10449]) ).
cnf(10648,plain,
op(e3,e1) = e1,
inference(rw,[status(thm)],[57,10647,theory(equality)]) ).
cnf(10649,plain,
op(e3,e0) = e0,
inference(rw,[status(thm)],[59,10647,theory(equality)]) ).
cnf(10650,plain,
op(e3,e2) = e2,
inference(rw,[status(thm)],[55,10647,theory(equality)]) ).
cnf(10651,plain,
op(e3,e3) = e3,
inference(rw,[status(thm)],[53,10647,theory(equality)]) ).
cnf(10652,plain,
op(e1,e3) = e1,
inference(rw,[status(thm)],[56,10647,theory(equality)]) ).
cnf(10653,plain,
op(e0,e3) = e0,
inference(rw,[status(thm)],[58,10647,theory(equality)]) ).
cnf(10654,plain,
op(e2,e3) = e2,
inference(rw,[status(thm)],[54,10647,theory(equality)]) ).
cnf(10727,plain,
( e1 = e2
| op(e2,e1) = e2
| op(e0,e1) = e2
| op(e1,op(e1,e2)) != e3
| op(e1,e2) != e0 ),
inference(rw,[status(thm)],[664,10648,theory(equality)]) ).
cnf(10728,plain,
( op(e2,e1) = e2
| op(e0,e1) = e2
| op(e1,op(e1,e2)) != e3
| op(e1,e2) != e0 ),
inference(sr,[status(thm)],[10727,165,theory(equality)]) ).
cnf(10746,plain,
( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e0) = e0
| e1 = e2
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(rw,[status(thm)],[544,10648,theory(equality)]) ).
cnf(10747,plain,
( op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e0) = e0
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(sr,[status(thm)],[10746,165,theory(equality)]) ).
cnf(10760,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e0
| $false ),
inference(rw,[status(thm)],[596,10648,theory(equality)]) ).
cnf(10761,plain,
( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e0 ),
inference(cn,[status(thm)],[10760,theory(equality)]) ).
cnf(10769,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e0) = e1
| $false ),
inference(rw,[status(thm)],[456,10648,theory(equality)]) ).
cnf(10770,plain,
( op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e0) = e1 ),
inference(cn,[status(thm)],[10769,theory(equality)]) ).
cnf(10776,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e0) = e1
| $false ),
inference(rw,[status(thm)],[396,10648,theory(equality)]) ).
cnf(10777,plain,
( op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e0) = e1 ),
inference(cn,[status(thm)],[10776,theory(equality)]) ).
cnf(10804,plain,
( e1 = e2
| op(e2,e1) = e2
| op(e0,e1) = e2
| op(e1,e0) != e2 ),
inference(rw,[status(thm)],[351,10648,theory(equality)]) ).
cnf(10805,plain,
( op(e2,e1) = e2
| op(e0,e1) = e2
| op(e1,e0) != e2 ),
inference(sr,[status(thm)],[10804,165,theory(equality)]) ).
cnf(10859,plain,
op(e1,e0) != e0,
inference(rw,[status(thm)],[158,10649,theory(equality)]) ).
cnf(10860,plain,
op(e0,e0) != e0,
inference(rw,[status(thm)],[160,10649,theory(equality)]) ).
cnf(10884,plain,
( e0 = e1
| op(e2,e0) = e1
| op(e0,e0) = e1
| op(e1,e3) != e1 ),
inference(rw,[status(thm)],[321,10649,theory(equality)]) ).
cnf(10885,plain,
( op(e2,e0) = e1
| op(e0,e0) = e1
| op(e1,e3) != e1 ),
inference(sr,[status(thm)],[10884,168,theory(equality)]) ).
cnf(10938,plain,
( op(e1,e0) = e2
| op(e0,e0) = e2
| op(e2,e0) = e2
| e0 = e2 ),
inference(rw,[status(thm)],[86,10649,theory(equality)]) ).
cnf(10939,plain,
( op(e1,e0) = e2
| op(e0,e0) = e2
| op(e2,e0) = e2 ),
inference(sr,[status(thm)],[10938,167,theory(equality)]) ).
cnf(10940,plain,
( op(e1,e0) = e3
| op(e0,e0) = e3
| op(e2,e0) = e3
| e0 = e3 ),
inference(rw,[status(thm)],[84,10649,theory(equality)]) ).
cnf(10941,plain,
( op(e1,e0) = e3
| op(e0,e0) = e3
| op(e2,e0) = e3 ),
inference(sr,[status(thm)],[10940,166,theory(equality)]) ).
cnf(10946,plain,
op(e1,e2) != e2,
inference(rw,[status(thm)],[146,10650,theory(equality)]) ).
cnf(10992,plain,
( op(e1,e2) = e0
| op(e0,e2) = e0
| op(e2,e2) = e0
| e2 = e0 ),
inference(rw,[status(thm)],[74,10650,theory(equality)]) ).
cnf(10993,plain,
( op(e1,e2) = e0
| op(e0,e2) = e0
| op(e2,e2) = e0 ),
inference(sr,[status(thm)],[10992,167,theory(equality)]) ).
cnf(10995,plain,
( op(e1,e2) = e3
| op(e0,e2) = e3
| op(e2,e2) = e3
| e2 = e3 ),
inference(rw,[status(thm)],[68,10650,theory(equality)]) ).
cnf(10996,plain,
( op(e1,e2) = e3
| op(e0,e2) = e3
| op(e2,e2) = e3 ),
inference(sr,[status(thm)],[10995,163,theory(equality)]) ).
cnf(11079,plain,
( $false
| op(e2,e2) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(rw,[status(thm)],[109,10651,theory(equality)]) ).
cnf(11080,plain,
( op(e2,e2) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(cn,[status(thm)],[11079,theory(equality)]) ).
cnf(11133,plain,
( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e0
| $false ),
inference(rw,[status(thm)],[585,10652,theory(equality)]) ).
cnf(11134,plain,
( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e0 ),
inference(cn,[status(thm)],[11133,theory(equality)]) ).
cnf(11135,plain,
( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e0
| $false ),
inference(rw,[status(thm)],[572,10652,theory(equality)]) ).
cnf(11136,plain,
( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e0 ),
inference(cn,[status(thm)],[11135,theory(equality)]) ).
cnf(11164,plain,
( op(e1,e1) = e0
| op(e1,e0) = e0
| op(e1,e2) = e0
| e1 = e0 ),
inference(rw,[status(thm)],[83,10652,theory(equality)]) ).
cnf(11165,plain,
( op(e1,e1) = e0
| op(e1,e0) = e0
| op(e1,e2) = e0 ),
inference(sr,[status(thm)],[11164,168,theory(equality)]) ).
cnf(11179,plain,
op(e0,e2) != e0,
inference(rw,[status(thm)],[133,10653,theory(equality)]) ).
cnf(11223,plain,
op(e2,e1) != e2,
inference(rw,[status(thm)],[122,10654,theory(equality)]) ).
cnf(11224,plain,
op(e2,e0) != e2,
inference(rw,[status(thm)],[124,10654,theory(equality)]) ).
cnf(11297,plain,
( e0 = e1
| op(e0,e2) = e1
| op(e0,e0) = e1 ),
inference(rw,[status(thm)],[10770,10653,theory(equality)]) ).
cnf(11298,plain,
( op(e0,e2) = e1
| op(e0,e0) = e1 ),
inference(sr,[status(thm)],[11297,168,theory(equality)]) ).
cnf(11358,plain,
( e2 = e1
| op(e2,e2) = e1
| op(e2,e0) = e1 ),
inference(rw,[status(thm)],[10777,10654,theory(equality)]) ).
cnf(11359,plain,
( op(e2,e2) = e1
| op(e2,e0) = e1 ),
inference(sr,[status(thm)],[11358,165,theory(equality)]) ).
cnf(11363,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e0
| op(e2,e2) = e1 ),
inference(spm,[status(thm)],[477,11359,theory(equality)]) ).
cnf(11366,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e2,e2) = e1 ),
inference(sr,[status(thm)],[11363,10860,theory(equality)]) ).
cnf(11391,plain,
( op(e1,e0) = e3
| op(e1,e0) = e2 ),
inference(sr,[status(thm)],[11134,10859,theory(equality)]) ).
cnf(11406,plain,
( op(e1,e2) = e3
| op(e1,e2) = e0 ),
inference(sr,[status(thm)],[11136,10946,theory(equality)]) ).
cnf(11408,plain,
( op(e1,e2) = e3
| e0 != op(e2,e2) ),
inference(spm,[status(thm)],[147,11406,theory(equality)]) ).
cnf(11428,plain,
( op(e0,e1) = e2
| op(e1,e0) != e2 ),
inference(sr,[status(thm)],[10805,11223,theory(equality)]) ).
cnf(11429,plain,
( op(e0,e1) = e2
| op(e1,e0) = e3 ),
inference(spm,[status(thm)],[11428,11391,theory(equality)]) ).
cnf(11430,plain,
( e1 = e0
| op(e1,e2) = e0
| op(e1,e0) = e0
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(rw,[status(thm)],[10747,10652,theory(equality)]) ).
cnf(11431,plain,
( op(e1,e2) = e0
| op(e1,e0) = e0
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(sr,[status(thm)],[11430,168,theory(equality)]) ).
cnf(11432,plain,
( op(e1,e2) = e0
| op(e2,e1) = e2
| op(e0,e1) = e2 ),
inference(sr,[status(thm)],[11431,10859,theory(equality)]) ).
cnf(11433,plain,
( op(e1,e2) = e0
| op(e0,e1) = e2 ),
inference(sr,[status(thm)],[11432,11223,theory(equality)]) ).
cnf(11438,plain,
( op(e0,e1) = e2
| op(e2,e1) = e2
| op(e1,e0) != e3 ),
inference(spm,[status(thm)],[10728,11433,theory(equality)]) ).
cnf(11442,plain,
( op(e0,e1) = e2
| op(e1,e0) != e3 ),
inference(sr,[status(thm)],[11438,11223,theory(equality)]) ).
cnf(11521,plain,
op(e0,e1) = e2,
inference(csr,[status(thm)],[11442,11429]) ).
cnf(11524,plain,
op(e1,e1) != e2,
inference(rw,[status(thm)],[156,11521,theory(equality)]) ).
cnf(11525,plain,
e2 != op(e0,e0),
inference(rw,[status(thm)],[138,11521,theory(equality)]) ).
cnf(11561,plain,
( op(e1,e1) = e0
| op(e1,e1) = e3 ),
inference(sr,[status(thm)],[10761,11524,theory(equality)]) ).
cnf(11592,plain,
( op(e1,e1) = e3
| e0 != op(e1,e2) ),
inference(spm,[status(thm)],[129,11561,theory(equality)]) ).
cnf(11710,plain,
( op(e0,e0) = e3
| op(e2,e2) = e1 ),
inference(sr,[status(thm)],[11366,11525,theory(equality)]) ).
cnf(11744,plain,
( op(e2,e0) = e1
| op(e0,e0) = e1
| $false ),
inference(rw,[status(thm)],[10885,10652,theory(equality)]) ).
cnf(11745,plain,
( op(e2,e0) = e1
| op(e0,e0) = e1 ),
inference(cn,[status(thm)],[11744,theory(equality)]) ).
cnf(11755,plain,
( op(e2,e0) = e1
| op(e0,op(e0,e1)) != e3
| op(e0,e1) != e2 ),
inference(spm,[status(thm)],[42,11745,theory(equality)]) ).
cnf(11771,plain,
( op(e2,e0) = e1
| op(e0,e2) != e3
| op(e0,e1) != e2 ),
inference(rw,[status(thm)],[11755,11521,theory(equality)]) ).
cnf(11772,plain,
( op(e2,e0) = e1
| op(e0,e2) != e3
| $false ),
inference(rw,[status(thm)],[11771,11521,theory(equality)]) ).
cnf(11773,plain,
( op(e2,e0) = e1
| op(e0,e2) != e3 ),
inference(cn,[status(thm)],[11772,theory(equality)]) ).
cnf(11872,plain,
( op(e1,e0) = e2
| op(e2,e0) = e2 ),
inference(sr,[status(thm)],[10939,11525,theory(equality)]) ).
cnf(11873,plain,
op(e1,e0) = e2,
inference(sr,[status(thm)],[11872,11224,theory(equality)]) ).
cnf(11906,plain,
( e2 = e3
| op(e0,e0) = e3
| op(e2,e0) = e3 ),
inference(rw,[status(thm)],[10941,11873,theory(equality)]) ).
cnf(11907,plain,
( op(e0,e0) = e3
| op(e2,e0) = e3 ),
inference(sr,[status(thm)],[11906,163,theory(equality)]) ).
cnf(11918,plain,
( e3 = e1
| op(e0,e2) = e1
| op(e2,e0) = e3 ),
inference(spm,[status(thm)],[11298,11907,theory(equality)]) ).
cnf(11933,plain,
( op(e0,e2) = e1
| op(e2,e0) = e3 ),
inference(sr,[status(thm)],[11918,164,theory(equality)]) ).
cnf(11986,plain,
( op(e1,e2) = e0
| op(e2,e2) = e0 ),
inference(sr,[status(thm)],[10993,11179,theory(equality)]) ).
cnf(12043,plain,
( op(e2,e2) = e0
| e3 = e0
| op(e2,e2) = e3
| op(e0,e2) = e3 ),
inference(spm,[status(thm)],[11986,10996,theory(equality)]) ).
cnf(12045,plain,
( op(e2,e2) = e0
| op(e2,e2) = e3
| op(e0,e2) = e3 ),
inference(sr,[status(thm)],[12043,166,theory(equality)]) ).
cnf(12102,plain,
( op(e2,e0) = e1
| op(e2,e2) = e3
| op(e2,e2) = e0 ),
inference(spm,[status(thm)],[11773,12045,theory(equality)]) ).
cnf(12103,plain,
( op(e2,e0) = e3
| e3 = e1
| op(e2,e2) = e3
| op(e2,e2) = e0 ),
inference(spm,[status(thm)],[11933,12045,theory(equality)]) ).
cnf(12108,plain,
( op(e2,e0) = e3
| op(e2,e2) = e3
| op(e2,e2) = e0 ),
inference(sr,[status(thm)],[12103,164,theory(equality)]) ).
cnf(12203,plain,
( op(e2,e2) = e0
| op(e2,e2) = e3
| e3 = e1 ),
inference(spm,[status(thm)],[12102,12108,theory(equality)]) ).
cnf(12207,plain,
( op(e2,e2) = e0
| op(e2,e2) = e3 ),
inference(sr,[status(thm)],[12203,164,theory(equality)]) ).
cnf(12218,plain,
( op(e1,e2) = e3
| op(e2,e2) = e3 ),
inference(spm,[status(thm)],[11408,12207,theory(equality)]) ).
cnf(12265,plain,
( op(e1,e1) = e0
| e2 = e0
| op(e1,e2) = e0 ),
inference(rw,[status(thm)],[11165,11873,theory(equality)]) ).
cnf(12266,plain,
( op(e1,e1) = e0
| op(e1,e2) = e0 ),
inference(sr,[status(thm)],[12265,167,theory(equality)]) ).
cnf(12277,plain,
( op(e1,e2) = e0
| op(e1,op(e1,e0)) != e3
| op(e1,e0) != e2 ),
inference(spm,[status(thm)],[34,12266,theory(equality)]) ).
cnf(12293,plain,
( op(e1,e2) = e0
| op(e1,e2) != e3
| op(e1,e0) != e2 ),
inference(rw,[status(thm)],[12277,11873,theory(equality)]) ).
cnf(12294,plain,
( op(e1,e2) = e0
| op(e1,e2) != e3
| $false ),
inference(rw,[status(thm)],[12293,11873,theory(equality)]) ).
cnf(12295,plain,
( op(e1,e2) = e0
| op(e1,e2) != e3 ),
inference(cn,[status(thm)],[12294,theory(equality)]) ).
cnf(12308,plain,
op(e1,e2) = e0,
inference(csr,[status(thm)],[12295,11406]) ).
cnf(12315,plain,
( op(e2,e2) = e3
| e0 = e3 ),
inference(rw,[status(thm)],[12218,12308,theory(equality)]) ).
cnf(12316,plain,
op(e2,e2) = e3,
inference(sr,[status(thm)],[12315,166,theory(equality)]) ).
cnf(12324,plain,
( op(e1,e1) = e3
| $false ),
inference(rw,[status(thm)],[11592,12308,theory(equality)]) ).
cnf(12325,plain,
op(e1,e1) = e3,
inference(cn,[status(thm)],[12324,theory(equality)]) ).
cnf(12349,plain,
( $false
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(rw,[status(thm)],[11080,12316,theory(equality)]) ).
cnf(12350,plain,
( op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(cn,[status(thm)],[12349,theory(equality)]) ).
cnf(12360,plain,
( e3 = e1
| op(e0,e0) = e3 ),
inference(rw,[status(thm)],[11710,12316,theory(equality)]) ).
cnf(12361,plain,
op(e0,e0) = e3,
inference(sr,[status(thm)],[12360,164,theory(equality)]) ).
cnf(12589,plain,
( $false
| op(e1,e1) != e3 ),
inference(rw,[status(thm)],[12350,12361,theory(equality)]) ).
cnf(12590,plain,
( $false
| $false ),
inference(rw,[status(thm)],[12589,12325,theory(equality)]) ).
cnf(12591,plain,
$false,
inference(cn,[status(thm)],[12590,theory(equality)]) ).
cnf(12592,plain,
$false,
12591,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/ALG/ALG046+1.p
% --creating new selector for []
% -running prover on /tmp/tmpYFkbBO/sel_ALG046+1.p_1 with time limit 29
% -prover status Unsatisfiable
% Problem ALG046+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/ALG/ALG046+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/ALG/ALG046+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
%
%------------------------------------------------------------------------------