%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : ALG064+1 : TPTP v5.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art02.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 : Tue Dec 28 20:46:41 EST 2010
% Result : Theorem 1.86s
% Output : Solution 1.86s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP5934/ALG064+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP5934/ALG064+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP5934/ALG064+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 6030
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.031 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,((((((((((((((((((((((((((((op(e0,e0)=e0|op(e0,e0)=e1)|op(e0,e0)=e2)|op(e0,e0)=e3)|op(e0,e0)=e4)&((((op(e0,e1)=e0|op(e0,e1)=e1)|op(e0,e1)=e2)|op(e0,e1)=e3)|op(e0,e1)=e4))&((((op(e0,e2)=e0|op(e0,e2)=e1)|op(e0,e2)=e2)|op(e0,e2)=e3)|op(e0,e2)=e4))&((((op(e0,e3)=e0|op(e0,e3)=e1)|op(e0,e3)=e2)|op(e0,e3)=e3)|op(e0,e3)=e4))&((((op(e0,e4)=e0|op(e0,e4)=e1)|op(e0,e4)=e2)|op(e0,e4)=e3)|op(e0,e4)=e4))&((((op(e1,e0)=e0|op(e1,e0)=e1)|op(e1,e0)=e2)|op(e1,e0)=e3)|op(e1,e0)=e4))&((((op(e1,e1)=e0|op(e1,e1)=e1)|op(e1,e1)=e2)|op(e1,e1)=e3)|op(e1,e1)=e4))&((((op(e1,e2)=e0|op(e1,e2)=e1)|op(e1,e2)=e2)|op(e1,e2)=e3)|op(e1,e2)=e4))&((((op(e1,e3)=e0|op(e1,e3)=e1)|op(e1,e3)=e2)|op(e1,e3)=e3)|op(e1,e3)=e4))&((((op(e1,e4)=e0|op(e1,e4)=e1)|op(e1,e4)=e2)|op(e1,e4)=e3)|op(e1,e4)=e4))&((((op(e2,e0)=e0|op(e2,e0)=e1)|op(e2,e0)=e2)|op(e2,e0)=e3)|op(e2,e0)=e4))&((((op(e2,e1)=e0|op(e2,e1)=e1)|op(e2,e1)=e2)|op(e2,e1)=e3)|op(e2,e1)=e4))&((((op(e2,e2)=e0|op(e2,e2)=e1)|op(e2,e2)=e2)|op(e2,e2)=e3)|op(e2,e2)=e4))&((((op(e2,e3)=e0|op(e2,e3)=e1)|op(e2,e3)=e2)|op(e2,e3)=e3)|op(e2,e3)=e4))&((((op(e2,e4)=e0|op(e2,e4)=e1)|op(e2,e4)=e2)|op(e2,e4)=e3)|op(e2,e4)=e4))&((((op(e3,e0)=e0|op(e3,e0)=e1)|op(e3,e0)=e2)|op(e3,e0)=e3)|op(e3,e0)=e4))&((((op(e3,e1)=e0|op(e3,e1)=e1)|op(e3,e1)=e2)|op(e3,e1)=e3)|op(e3,e1)=e4))&((((op(e3,e2)=e0|op(e3,e2)=e1)|op(e3,e2)=e2)|op(e3,e2)=e3)|op(e3,e2)=e4))&((((op(e3,e3)=e0|op(e3,e3)=e1)|op(e3,e3)=e2)|op(e3,e3)=e3)|op(e3,e3)=e4))&((((op(e3,e4)=e0|op(e3,e4)=e1)|op(e3,e4)=e2)|op(e3,e4)=e3)|op(e3,e4)=e4))&((((op(e4,e0)=e0|op(e4,e0)=e1)|op(e4,e0)=e2)|op(e4,e0)=e3)|op(e4,e0)=e4))&((((op(e4,e1)=e0|op(e4,e1)=e1)|op(e4,e1)=e2)|op(e4,e1)=e3)|op(e4,e1)=e4))&((((op(e4,e2)=e0|op(e4,e2)=e1)|op(e4,e2)=e2)|op(e4,e2)=e3)|op(e4,e2)=e4))&((((op(e4,e3)=e0|op(e4,e3)=e1)|op(e4,e3)=e2)|op(e4,e3)=e3)|op(e4,e3)=e4))&((((op(e4,e4)=e0|op(e4,e4)=e1)|op(e4,e4)=e2)|op(e4,e4)=e3)|op(e4,e4)=e4)),file('/tmp/SRASS.s.p', ax1)).
% fof(2, axiom,(((((((((((((((((((((((((((((((((((((((((((((((((((((op(e0,e0)=e0|op(e0,e1)=e0)|op(e0,e2)=e0)|op(e0,e3)=e0)|op(e0,e4)=e0)&((((op(e0,e0)=e0|op(e1,e0)=e0)|op(e2,e0)=e0)|op(e3,e0)=e0)|op(e4,e0)=e0))&((((op(e0,e0)=e1|op(e0,e1)=e1)|op(e0,e2)=e1)|op(e0,e3)=e1)|op(e0,e4)=e1))&((((op(e0,e0)=e1|op(e1,e0)=e1)|op(e2,e0)=e1)|op(e3,e0)=e1)|op(e4,e0)=e1))&((((op(e0,e0)=e2|op(e0,e1)=e2)|op(e0,e2)=e2)|op(e0,e3)=e2)|op(e0,e4)=e2))&((((op(e0,e0)=e2|op(e1,e0)=e2)|op(e2,e0)=e2)|op(e3,e0)=e2)|op(e4,e0)=e2))&((((op(e0,e0)=e3|op(e0,e1)=e3)|op(e0,e2)=e3)|op(e0,e3)=e3)|op(e0,e4)=e3))&((((op(e0,e0)=e3|op(e1,e0)=e3)|op(e2,e0)=e3)|op(e3,e0)=e3)|op(e4,e0)=e3))&((((op(e0,e0)=e4|op(e0,e1)=e4)|op(e0,e2)=e4)|op(e0,e3)=e4)|op(e0,e4)=e4))&((((op(e0,e0)=e4|op(e1,e0)=e4)|op(e2,e0)=e4)|op(e3,e0)=e4)|op(e4,e0)=e4))&((((op(e1,e0)=e0|op(e1,e1)=e0)|op(e1,e2)=e0)|op(e1,e3)=e0)|op(e1,e4)=e0))&((((op(e0,e1)=e0|op(e1,e1)=e0)|op(e2,e1)=e0)|op(e3,e1)=e0)|op(e4,e1)=e0))&((((op(e1,e0)=e1|op(e1,e1)=e1)|op(e1,e2)=e1)|op(e1,e3)=e1)|op(e1,e4)=e1))&((((op(e0,e1)=e1|op(e1,e1)=e1)|op(e2,e1)=e1)|op(e3,e1)=e1)|op(e4,e1)=e1))&((((op(e1,e0)=e2|op(e1,e1)=e2)|op(e1,e2)=e2)|op(e1,e3)=e2)|op(e1,e4)=e2))&((((op(e0,e1)=e2|op(e1,e1)=e2)|op(e2,e1)=e2)|op(e3,e1)=e2)|op(e4,e1)=e2))&((((op(e1,e0)=e3|op(e1,e1)=e3)|op(e1,e2)=e3)|op(e1,e3)=e3)|op(e1,e4)=e3))&((((op(e0,e1)=e3|op(e1,e1)=e3)|op(e2,e1)=e3)|op(e3,e1)=e3)|op(e4,e1)=e3))&((((op(e1,e0)=e4|op(e1,e1)=e4)|op(e1,e2)=e4)|op(e1,e3)=e4)|op(e1,e4)=e4))&((((op(e0,e1)=e4|op(e1,e1)=e4)|op(e2,e1)=e4)|op(e3,e1)=e4)|op(e4,e1)=e4))&((((op(e2,e0)=e0|op(e2,e1)=e0)|op(e2,e2)=e0)|op(e2,e3)=e0)|op(e2,e4)=e0))&((((op(e0,e2)=e0|op(e1,e2)=e0)|op(e2,e2)=e0)|op(e3,e2)=e0)|op(e4,e2)=e0))&((((op(e2,e0)=e1|op(e2,e1)=e1)|op(e2,e2)=e1)|op(e2,e3)=e1)|op(e2,e4)=e1))&((((op(e0,e2)=e1|op(e1,e2)=e1)|op(e2,e2)=e1)|op(e3,e2)=e1)|op(e4,e2)=e1))&((((op(e2,e0)=e2|op(e2,e1)=e2)|op(e2,e2)=e2)|op(e2,e3)=e2)|op(e2,e4)=e2))&((((op(e0,e2)=e2|op(e1,e2)=e2)|op(e2,e2)=e2)|op(e3,e2)=e2)|op(e4,e2)=e2))&((((op(e2,e0)=e3|op(e2,e1)=e3)|op(e2,e2)=e3)|op(e2,e3)=e3)|op(e2,e4)=e3))&((((op(e0,e2)=e3|op(e1,e2)=e3)|op(e2,e2)=e3)|op(e3,e2)=e3)|op(e4,e2)=e3))&((((op(e2,e0)=e4|op(e2,e1)=e4)|op(e2,e2)=e4)|op(e2,e3)=e4)|op(e2,e4)=e4))&((((op(e0,e2)=e4|op(e1,e2)=e4)|op(e2,e2)=e4)|op(e3,e2)=e4)|op(e4,e2)=e4))&((((op(e3,e0)=e0|op(e3,e1)=e0)|op(e3,e2)=e0)|op(e3,e3)=e0)|op(e3,e4)=e0))&((((op(e0,e3)=e0|op(e1,e3)=e0)|op(e2,e3)=e0)|op(e3,e3)=e0)|op(e4,e3)=e0))&((((op(e3,e0)=e1|op(e3,e1)=e1)|op(e3,e2)=e1)|op(e3,e3)=e1)|op(e3,e4)=e1))&((((op(e0,e3)=e1|op(e1,e3)=e1)|op(e2,e3)=e1)|op(e3,e3)=e1)|op(e4,e3)=e1))&((((op(e3,e0)=e2|op(e3,e1)=e2)|op(e3,e2)=e2)|op(e3,e3)=e2)|op(e3,e4)=e2))&((((op(e0,e3)=e2|op(e1,e3)=e2)|op(e2,e3)=e2)|op(e3,e3)=e2)|op(e4,e3)=e2))&((((op(e3,e0)=e3|op(e3,e1)=e3)|op(e3,e2)=e3)|op(e3,e3)=e3)|op(e3,e4)=e3))&((((op(e0,e3)=e3|op(e1,e3)=e3)|op(e2,e3)=e3)|op(e3,e3)=e3)|op(e4,e3)=e3))&((((op(e3,e0)=e4|op(e3,e1)=e4)|op(e3,e2)=e4)|op(e3,e3)=e4)|op(e3,e4)=e4))&((((op(e0,e3)=e4|op(e1,e3)=e4)|op(e2,e3)=e4)|op(e3,e3)=e4)|op(e4,e3)=e4))&((((op(e4,e0)=e0|op(e4,e1)=e0)|op(e4,e2)=e0)|op(e4,e3)=e0)|op(e4,e4)=e0))&((((op(e0,e4)=e0|op(e1,e4)=e0)|op(e2,e4)=e0)|op(e3,e4)=e0)|op(e4,e4)=e0))&((((op(e4,e0)=e1|op(e4,e1)=e1)|op(e4,e2)=e1)|op(e4,e3)=e1)|op(e4,e4)=e1))&((((op(e0,e4)=e1|op(e1,e4)=e1)|op(e2,e4)=e1)|op(e3,e4)=e1)|op(e4,e4)=e1))&((((op(e4,e0)=e2|op(e4,e1)=e2)|op(e4,e2)=e2)|op(e4,e3)=e2)|op(e4,e4)=e2))&((((op(e0,e4)=e2|op(e1,e4)=e2)|op(e2,e4)=e2)|op(e3,e4)=e2)|op(e4,e4)=e2))&((((op(e4,e0)=e3|op(e4,e1)=e3)|op(e4,e2)=e3)|op(e4,e3)=e3)|op(e4,e4)=e3))&((((op(e0,e4)=e3|op(e1,e4)=e3)|op(e2,e4)=e3)|op(e3,e4)=e3)|op(e4,e4)=e3))&((((op(e4,e0)=e4|op(e4,e1)=e4)|op(e4,e2)=e4)|op(e4,e3)=e4)|op(e4,e4)=e4))&((((op(e0,e4)=e4|op(e1,e4)=e4)|op(e2,e4)=e4)|op(e3,e4)=e4)|op(e4,e4)=e4)),file('/tmp/SRASS.s.p', ax3)).
% fof(3, axiom,(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(op(e0,e0)=op(e1,e0))&~(op(e0,e0)=op(e2,e0)))&~(op(e0,e0)=op(e3,e0)))&~(op(e0,e0)=op(e4,e0)))&~(op(e1,e0)=op(e2,e0)))&~(op(e1,e0)=op(e3,e0)))&~(op(e1,e0)=op(e4,e0)))&~(op(e2,e0)=op(e3,e0)))&~(op(e2,e0)=op(e4,e0)))&~(op(e3,e0)=op(e4,e0)))&~(op(e0,e1)=op(e1,e1)))&~(op(e0,e1)=op(e2,e1)))&~(op(e0,e1)=op(e3,e1)))&~(op(e0,e1)=op(e4,e1)))&~(op(e1,e1)=op(e2,e1)))&~(op(e1,e1)=op(e3,e1)))&~(op(e1,e1)=op(e4,e1)))&~(op(e2,e1)=op(e3,e1)))&~(op(e2,e1)=op(e4,e1)))&~(op(e3,e1)=op(e4,e1)))&~(op(e0,e2)=op(e1,e2)))&~(op(e0,e2)=op(e2,e2)))&~(op(e0,e2)=op(e3,e2)))&~(op(e0,e2)=op(e4,e2)))&~(op(e1,e2)=op(e2,e2)))&~(op(e1,e2)=op(e3,e2)))&~(op(e1,e2)=op(e4,e2)))&~(op(e2,e2)=op(e3,e2)))&~(op(e2,e2)=op(e4,e2)))&~(op(e3,e2)=op(e4,e2)))&~(op(e0,e3)=op(e1,e3)))&~(op(e0,e3)=op(e2,e3)))&~(op(e0,e3)=op(e3,e3)))&~(op(e0,e3)=op(e4,e3)))&~(op(e1,e3)=op(e2,e3)))&~(op(e1,e3)=op(e3,e3)))&~(op(e1,e3)=op(e4,e3)))&~(op(e2,e3)=op(e3,e3)))&~(op(e2,e3)=op(e4,e3)))&~(op(e3,e3)=op(e4,e3)))&~(op(e0,e4)=op(e1,e4)))&~(op(e0,e4)=op(e2,e4)))&~(op(e0,e4)=op(e3,e4)))&~(op(e0,e4)=op(e4,e4)))&~(op(e1,e4)=op(e2,e4)))&~(op(e1,e4)=op(e3,e4)))&~(op(e1,e4)=op(e4,e4)))&~(op(e2,e4)=op(e3,e4)))&~(op(e2,e4)=op(e4,e4)))&~(op(e3,e4)=op(e4,e4)))&~(op(e0,e0)=op(e0,e1)))&~(op(e0,e0)=op(e0,e2)))&~(op(e0,e0)=op(e0,e3)))&~(op(e0,e0)=op(e0,e4)))&~(op(e0,e1)=op(e0,e2)))&~(op(e0,e1)=op(e0,e3)))&~(op(e0,e1)=op(e0,e4)))&~(op(e0,e2)=op(e0,e3)))&~(op(e0,e2)=op(e0,e4)))&~(op(e0,e3)=op(e0,e4)))&~(op(e1,e0)=op(e1,e1)))&~(op(e1,e0)=op(e1,e2)))&~(op(e1,e0)=op(e1,e3)))&~(op(e1,e0)=op(e1,e4)))&~(op(e1,e1)=op(e1,e2)))&~(op(e1,e1)=op(e1,e3)))&~(op(e1,e1)=op(e1,e4)))&~(op(e1,e2)=op(e1,e3)))&~(op(e1,e2)=op(e1,e4)))&~(op(e1,e3)=op(e1,e4)))&~(op(e2,e0)=op(e2,e1)))&~(op(e2,e0)=op(e2,e2)))&~(op(e2,e0)=op(e2,e3)))&~(op(e2,e0)=op(e2,e4)))&~(op(e2,e1)=op(e2,e2)))&~(op(e2,e1)=op(e2,e3)))&~(op(e2,e1)=op(e2,e4)))&~(op(e2,e2)=op(e2,e3)))&~(op(e2,e2)=op(e2,e4)))&~(op(e2,e3)=op(e2,e4)))&~(op(e3,e0)=op(e3,e1)))&~(op(e3,e0)=op(e3,e2)))&~(op(e3,e0)=op(e3,e3)))&~(op(e3,e0)=op(e3,e4)))&~(op(e3,e1)=op(e3,e2)))&~(op(e3,e1)=op(e3,e3)))&~(op(e3,e1)=op(e3,e4)))&~(op(e3,e2)=op(e3,e3)))&~(op(e3,e2)=op(e3,e4)))&~(op(e3,e3)=op(e3,e4)))&~(op(e4,e0)=op(e4,e1)))&~(op(e4,e0)=op(e4,e2)))&~(op(e4,e0)=op(e4,e3)))&~(op(e4,e0)=op(e4,e4)))&~(op(e4,e1)=op(e4,e2)))&~(op(e4,e1)=op(e4,e3)))&~(op(e4,e1)=op(e4,e4)))&~(op(e4,e2)=op(e4,e3)))&~(op(e4,e2)=op(e4,e4)))&~(op(e4,e3)=op(e4,e4))),file('/tmp/SRASS.s.p', ax4)).
% fof(4, axiom,(((e0=op(e1,op(op(e1,e1),op(e1,e1)))&e2=op(op(e1,e1),op(e1,e1)))&e3=op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))))&e4=op(e1,e1)),file('/tmp/SRASS.s.p', ax6)).
% fof(5, 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)&op(unit,e4)=e4)&op(e4,unit)=e4)&((((unit=e0|unit=e1)|unit=e2)|unit=e3)|unit=e4)),file('/tmp/SRASS.s.p', ax2)).
% fof(6, axiom,(((((((((~(e0=e1)&~(e0=e2))&~(e0=e3))&~(e0=e4))&~(e1=e2))&~(e1=e3))&~(e1=e4))&~(e2=e3))&~(e2=e4))&~(e3=e4)),file('/tmp/SRASS.s.p', ax5)).
% fof(7, conjecture,~((((((((((op(e0,e0)=e0|op(e1,e1)=e0)|op(e2,e2)=e0)|op(e3,e3)=e0)|op(e4,e4)=e0)&((((op(e0,e0)=e1|op(e1,e1)=e1)|op(e2,e2)=e1)|op(e3,e3)=e1)|op(e4,e4)=e1))&((((op(e0,e0)=e2|op(e1,e1)=e2)|op(e2,e2)=e2)|op(e3,e3)=e2)|op(e4,e4)=e2))&((((op(e0,e0)=e3|op(e1,e1)=e3)|op(e2,e2)=e3)|op(e3,e3)=e3)|op(e4,e4)=e3))&((((op(e0,e0)=e4|op(e1,e1)=e4)|op(e2,e2)=e4)|op(e3,e3)=e4)|op(e4,e4)=e4))&((((((((((((((((((((((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))|((~(op(e2,e2)=op(e2,e2))&op(op(e2,e2),e2)=e2)&~(op(op(e2,e2),e2)=e2)))|((~(op(e3,e2)=op(e2,e3))&op(op(e2,e3),e3)=e2)&~(op(op(e2,e3),e2)=e3)))|((~(op(e4,e2)=op(e2,e4))&op(op(e2,e4),e4)=e2)&~(op(op(e2,e4),e2)=e4)))|((~(op(e0,e3)=op(e3,e0))&op(op(e3,e0),e0)=e3)&~(op(op(e3,e0),e3)=e0)))|((~(op(e1,e3)=op(e3,e1))&op(op(e3,e1),e1)=e3)&~(op(op(e3,e1),e3)=e1)))|((~(op(e2,e3)=op(e3,e2))&op(op(e3,e2),e2)=e3)&~(op(op(e3,e2),e3)=e2)))|((~(op(e3,e3)=op(e3,e3))&op(op(e3,e3),e3)=e3)&~(op(op(e3,e3),e3)=e3)))|((~(op(e4,e3)=op(e3,e4))&op(op(e3,e4),e4)=e3)&~(op(op(e3,e4),e3)=e4)))|((~(op(e0,e4)=op(e4,e0))&op(op(e4,e0),e0)=e4)&~(op(op(e4,e0),e4)=e0)))|((~(op(e1,e4)=op(e4,e1))&op(op(e4,e1),e1)=e4)&~(op(op(e4,e1),e4)=e1)))|((~(op(e2,e4)=op(e4,e2))&op(op(e4,e2),e2)=e4)&~(op(op(e4,e2),e4)=e2)))|((~(op(e3,e4)=op(e4,e3))&op(op(e4,e3),e3)=e4)&~(op(op(e4,e3),e4)=e3)))|((~(op(e4,e4)=op(e4,e4))&op(op(e4,e4),e4)=e4)&~(op(op(e4,e4),e4)=e4))))),file('/tmp/SRASS.s.p', co1)).
% fof(8, negated_conjecture,~(~((((((((((op(e0,e0)=e0|op(e1,e1)=e0)|op(e2,e2)=e0)|op(e3,e3)=e0)|op(e4,e4)=e0)&((((op(e0,e0)=e1|op(e1,e1)=e1)|op(e2,e2)=e1)|op(e3,e3)=e1)|op(e4,e4)=e1))&((((op(e0,e0)=e2|op(e1,e1)=e2)|op(e2,e2)=e2)|op(e3,e3)=e2)|op(e4,e4)=e2))&((((op(e0,e0)=e3|op(e1,e1)=e3)|op(e2,e2)=e3)|op(e3,e3)=e3)|op(e4,e4)=e3))&((((op(e0,e0)=e4|op(e1,e1)=e4)|op(e2,e2)=e4)|op(e3,e3)=e4)|op(e4,e4)=e4))&((((((((((((((((((((((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))|((~(op(e2,e2)=op(e2,e2))&op(op(e2,e2),e2)=e2)&~(op(op(e2,e2),e2)=e2)))|((~(op(e3,e2)=op(e2,e3))&op(op(e2,e3),e3)=e2)&~(op(op(e2,e3),e2)=e3)))|((~(op(e4,e2)=op(e2,e4))&op(op(e2,e4),e4)=e2)&~(op(op(e2,e4),e2)=e4)))|((~(op(e0,e3)=op(e3,e0))&op(op(e3,e0),e0)=e3)&~(op(op(e3,e0),e3)=e0)))|((~(op(e1,e3)=op(e3,e1))&op(op(e3,e1),e1)=e3)&~(op(op(e3,e1),e3)=e1)))|((~(op(e2,e3)=op(e3,e2))&op(op(e3,e2),e2)=e3)&~(op(op(e3,e2),e3)=e2)))|((~(op(e3,e3)=op(e3,e3))&op(op(e3,e3),e3)=e3)&~(op(op(e3,e3),e3)=e3)))|((~(op(e4,e3)=op(e3,e4))&op(op(e3,e4),e4)=e3)&~(op(op(e3,e4),e3)=e4)))|((~(op(e0,e4)=op(e4,e0))&op(op(e4,e0),e0)=e4)&~(op(op(e4,e0),e4)=e0)))|((~(op(e1,e4)=op(e4,e1))&op(op(e4,e1),e1)=e4)&~(op(op(e4,e1),e4)=e1)))|((~(op(e2,e4)=op(e4,e2))&op(op(e4,e2),e2)=e4)&~(op(op(e4,e2),e4)=e2)))|((~(op(e3,e4)=op(e4,e3))&op(op(e4,e3),e3)=e4)&~(op(op(e4,e3),e4)=e3)))|((~(op(e4,e4)=op(e4,e4))&op(op(e4,e4),e4)=e4)&~(op(op(e4,e4),e4)=e4)))))),inference(assume_negation,[status(cth)],[7])).
% fof(9, plain,(epred1_0=>((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))),introduced(definition)).
% fof(10, plain,(epred2_0=>(((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))),introduced(definition)).
% fof(11, plain,(epred3_0=>((((((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))),introduced(definition)).
% fof(12, plain,(epred4_0=>(((((((((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))),introduced(definition)).
% fof(13, plain,(epred5_0=>((((((((((((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))|((~(op(e2,e2)=op(e2,e2))&op(op(e2,e2),e2)=e2)&~(op(op(e2,e2),e2)=e2)))|((~(op(e3,e2)=op(e2,e3))&op(op(e2,e3),e3)=e2)&~(op(op(e2,e3),e2)=e3)))|((~(op(e4,e2)=op(e2,e4))&op(op(e2,e4),e4)=e2)&~(op(op(e2,e4),e2)=e4)))),introduced(definition)).
% fof(14, plain,(epred6_0=>(((((((((((((((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))|((~(op(e2,e2)=op(e2,e2))&op(op(e2,e2),e2)=e2)&~(op(op(e2,e2),e2)=e2)))|((~(op(e3,e2)=op(e2,e3))&op(op(e2,e3),e3)=e2)&~(op(op(e2,e3),e2)=e3)))|((~(op(e4,e2)=op(e2,e4))&op(op(e2,e4),e4)=e2)&~(op(op(e2,e4),e2)=e4)))|((~(op(e0,e3)=op(e3,e0))&op(op(e3,e0),e0)=e3)&~(op(op(e3,e0),e3)=e0)))|((~(op(e1,e3)=op(e3,e1))&op(op(e3,e1),e1)=e3)&~(op(op(e3,e1),e3)=e1)))|((~(op(e2,e3)=op(e3,e2))&op(op(e3,e2),e2)=e3)&~(op(op(e3,e2),e3)=e2)))),introduced(definition)).
% fof(15, plain,(epred7_0=>((((((((((((((((((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))|((~(op(e2,e2)=op(e2,e2))&op(op(e2,e2),e2)=e2)&~(op(op(e2,e2),e2)=e2)))|((~(op(e3,e2)=op(e2,e3))&op(op(e2,e3),e3)=e2)&~(op(op(e2,e3),e2)=e3)))|((~(op(e4,e2)=op(e2,e4))&op(op(e2,e4),e4)=e2)&~(op(op(e2,e4),e2)=e4)))|((~(op(e0,e3)=op(e3,e0))&op(op(e3,e0),e0)=e3)&~(op(op(e3,e0),e3)=e0)))|((~(op(e1,e3)=op(e3,e1))&op(op(e3,e1),e1)=e3)&~(op(op(e3,e1),e3)=e1)))|((~(op(e2,e3)=op(e3,e2))&op(op(e3,e2),e2)=e3)&~(op(op(e3,e2),e3)=e2)))|((~(op(e3,e3)=op(e3,e3))&op(op(e3,e3),e3)=e3)&~(op(op(e3,e3),e3)=e3)))|((~(op(e4,e3)=op(e3,e4))&op(op(e3,e4),e4)=e3)&~(op(op(e3,e4),e3)=e4)))|((~(op(e0,e4)=op(e4,e0))&op(op(e4,e0),e0)=e4)&~(op(op(e4,e0),e4)=e0)))),introduced(definition)).
% fof(16, plain,(epred8_0=>(((((((((((((((((((((((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))|((~(op(e2,e2)=op(e2,e2))&op(op(e2,e2),e2)=e2)&~(op(op(e2,e2),e2)=e2)))|((~(op(e3,e2)=op(e2,e3))&op(op(e2,e3),e3)=e2)&~(op(op(e2,e3),e2)=e3)))|((~(op(e4,e2)=op(e2,e4))&op(op(e2,e4),e4)=e2)&~(op(op(e2,e4),e2)=e4)))|((~(op(e0,e3)=op(e3,e0))&op(op(e3,e0),e0)=e3)&~(op(op(e3,e0),e3)=e0)))|((~(op(e1,e3)=op(e3,e1))&op(op(e3,e1),e1)=e3)&~(op(op(e3,e1),e3)=e1)))|((~(op(e2,e3)=op(e3,e2))&op(op(e3,e2),e2)=e3)&~(op(op(e3,e2),e3)=e2)))|((~(op(e3,e3)=op(e3,e3))&op(op(e3,e3),e3)=e3)&~(op(op(e3,e3),e3)=e3)))|((~(op(e4,e3)=op(e3,e4))&op(op(e3,e4),e4)=e3)&~(op(op(e3,e4),e3)=e4)))|((~(op(e0,e4)=op(e4,e0))&op(op(e4,e0),e0)=e4)&~(op(op(e4,e0),e4)=e0)))|((~(op(e1,e4)=op(e4,e1))&op(op(e4,e1),e1)=e4)&~(op(op(e4,e1),e4)=e1)))|((~(op(e2,e4)=op(e4,e2))&op(op(e4,e2),e2)=e4)&~(op(op(e4,e2),e4)=e2)))|((~(op(e3,e4)=op(e4,e3))&op(op(e4,e3),e3)=e4)&~(op(op(e4,e3),e4)=e3)))),introduced(definition)).
% fof(17, negated_conjecture,~(~((((((((((op(e0,e0)=e0|op(e1,e1)=e0)|op(e2,e2)=e0)|op(e3,e3)=e0)|op(e4,e4)=e0)&((((op(e0,e0)=e1|op(e1,e1)=e1)|op(e2,e2)=e1)|op(e3,e3)=e1)|op(e4,e4)=e1))&((((op(e0,e0)=e2|op(e1,e1)=e2)|op(e2,e2)=e2)|op(e3,e3)=e2)|op(e4,e4)=e2))&((((op(e0,e0)=e3|op(e1,e1)=e3)|op(e2,e2)=e3)|op(e3,e3)=e3)|op(e4,e4)=e3))&((((op(e0,e0)=e4|op(e1,e1)=e4)|op(e2,e2)=e4)|op(e3,e3)=e4)|op(e4,e4)=e4))&(epred8_0|((~(op(e4,e4)=op(e4,e4))&op(op(e4,e4),e4)=e4)&~(op(op(e4,e4),e4)=e4)))))),inference(apply_def,[status(esa)],[8,16,theory(equality)])).
% fof(18, plain,(epred2_0=>(((epred1_0|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))),inference(apply_def,[status(esa)],[10,9,theory(equality)])).
% fof(19, plain,(epred3_0=>(((epred2_0|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))),inference(apply_def,[status(esa)],[11,18,theory(equality)])).
% fof(20, plain,(epred4_0=>(((epred3_0|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))),inference(apply_def,[status(esa)],[12,19,theory(equality)])).
% fof(21, plain,(epred5_0=>(((epred4_0|((~(op(e2,e2)=op(e2,e2))&op(op(e2,e2),e2)=e2)&~(op(op(e2,e2),e2)=e2)))|((~(op(e3,e2)=op(e2,e3))&op(op(e2,e3),e3)=e2)&~(op(op(e2,e3),e2)=e3)))|((~(op(e4,e2)=op(e2,e4))&op(op(e2,e4),e4)=e2)&~(op(op(e2,e4),e2)=e4)))),inference(apply_def,[status(esa)],[13,20,theory(equality)])).
% fof(22, plain,(epred6_0=>(((epred5_0|((~(op(e0,e3)=op(e3,e0))&op(op(e3,e0),e0)=e3)&~(op(op(e3,e0),e3)=e0)))|((~(op(e1,e3)=op(e3,e1))&op(op(e3,e1),e1)=e3)&~(op(op(e3,e1),e3)=e1)))|((~(op(e2,e3)=op(e3,e2))&op(op(e3,e2),e2)=e3)&~(op(op(e3,e2),e3)=e2)))),inference(apply_def,[status(esa)],[14,21,theory(equality)])).
% fof(23, plain,(epred7_0=>(((epred6_0|((~(op(e3,e3)=op(e3,e3))&op(op(e3,e3),e3)=e3)&~(op(op(e3,e3),e3)=e3)))|((~(op(e4,e3)=op(e3,e4))&op(op(e3,e4),e4)=e3)&~(op(op(e3,e4),e3)=e4)))|((~(op(e0,e4)=op(e4,e0))&op(op(e4,e0),e0)=e4)&~(op(op(e4,e0),e4)=e0)))),inference(apply_def,[status(esa)],[15,22,theory(equality)])).
% fof(24, plain,(epred8_0=>(((epred7_0|((~(op(e1,e4)=op(e4,e1))&op(op(e4,e1),e1)=e4)&~(op(op(e4,e1),e4)=e1)))|((~(op(e2,e4)=op(e4,e2))&op(op(e4,e2),e2)=e4)&~(op(op(e4,e2),e4)=e2)))|((~(op(e3,e4)=op(e4,e3))&op(op(e4,e3),e3)=e4)&~(op(op(e4,e3),e4)=e3)))),inference(apply_def,[status(esa)],[16,23,theory(equality)])).
% cnf(26,plain,(op(e4,e3)=e4|op(e4,e3)=e3|op(e4,e3)=e2|op(e4,e3)=e1|op(e4,e3)=e0),inference(split_conjunct,[status(thm)],[1])).
% cnf(27,plain,(op(e4,e2)=e4|op(e4,e2)=e3|op(e4,e2)=e2|op(e4,e2)=e1|op(e4,e2)=e0),inference(split_conjunct,[status(thm)],[1])).
% cnf(30,plain,(op(e3,e4)=e4|op(e3,e4)=e3|op(e3,e4)=e2|op(e3,e4)=e1|op(e3,e4)=e0),inference(split_conjunct,[status(thm)],[1])).
% cnf(35,plain,(op(e2,e4)=e4|op(e2,e4)=e3|op(e2,e4)=e2|op(e2,e4)=e1|op(e2,e4)=e0),inference(split_conjunct,[status(thm)],[1])).
% cnf(52,plain,(op(e4,e4)=e3|op(e3,e4)=e3|op(e2,e4)=e3|op(e1,e4)=e3|op(e0,e4)=e3),inference(split_conjunct,[status(thm)],[2])).
% cnf(53,plain,(op(e4,e4)=e3|op(e4,e3)=e3|op(e4,e2)=e3|op(e4,e1)=e3|op(e4,e0)=e3),inference(split_conjunct,[status(thm)],[2])).
% cnf(64,plain,(op(e4,e3)=e2|op(e3,e3)=e2|op(e2,e3)=e2|op(e1,e3)=e2|op(e0,e3)=e2),inference(split_conjunct,[status(thm)],[2])).
% cnf(65,plain,(op(e3,e4)=e2|op(e3,e3)=e2|op(e3,e2)=e2|op(e3,e1)=e2|op(e3,e0)=e2),inference(split_conjunct,[status(thm)],[2])).
% cnf(70,plain,(op(e4,e2)=e4|op(e3,e2)=e4|op(e2,e2)=e4|op(e1,e2)=e4|op(e0,e2)=e4),inference(split_conjunct,[status(thm)],[2])).
% cnf(71,plain,(op(e2,e4)=e4|op(e2,e3)=e4|op(e2,e2)=e4|op(e2,e1)=e4|op(e2,e0)=e4),inference(split_conjunct,[status(thm)],[2])).
% cnf(84,plain,(op(e4,e1)=e2|op(e3,e1)=e2|op(e2,e1)=e2|op(e1,e1)=e2|op(e0,e1)=e2),inference(split_conjunct,[status(thm)],[2])).
% cnf(88,plain,(op(e4,e1)=e0|op(e3,e1)=e0|op(e2,e1)=e0|op(e1,e1)=e0|op(e0,e1)=e0),inference(split_conjunct,[status(thm)],[2])).
% cnf(100,plain,(op(e4,e3)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(101,plain,(op(e4,e2)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(102,plain,(op(e4,e2)!=op(e4,e3)),inference(split_conjunct,[status(thm)],[3])).
% cnf(103,plain,(op(e4,e1)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(108,plain,(op(e4,e0)!=op(e4,e2)),inference(split_conjunct,[status(thm)],[3])).
% cnf(116,plain,(op(e3,e0)!=op(e3,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(120,plain,(op(e2,e3)!=op(e2,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(121,plain,(op(e2,e2)!=op(e2,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(123,plain,(op(e2,e1)!=op(e2,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(129,plain,(op(e2,e0)!=op(e2,e1)),inference(split_conjunct,[status(thm)],[3])).
% cnf(133,plain,(op(e1,e1)!=op(e1,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(140,plain,(op(e0,e3)!=op(e0,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(141,plain,(op(e0,e2)!=op(e0,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(145,plain,(op(e0,e1)!=op(e0,e2)),inference(split_conjunct,[status(thm)],[3])).
% cnf(149,plain,(op(e0,e0)!=op(e0,e1)),inference(split_conjunct,[status(thm)],[3])).
% cnf(150,plain,(op(e3,e4)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(151,plain,(op(e2,e4)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(152,plain,(op(e2,e4)!=op(e3,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(153,plain,(op(e1,e4)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(154,plain,(op(e1,e4)!=op(e3,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(157,plain,(op(e0,e4)!=op(e3,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(158,plain,(op(e0,e4)!=op(e2,e4)),inference(split_conjunct,[status(thm)],[3])).
% cnf(160,plain,(op(e3,e3)!=op(e4,e3)),inference(split_conjunct,[status(thm)],[3])).
% cnf(161,plain,(op(e2,e3)!=op(e4,e3)),inference(split_conjunct,[status(thm)],[3])).
% cnf(164,plain,(op(e1,e3)!=op(e3,e3)),inference(split_conjunct,[status(thm)],[3])).
% cnf(166,plain,(op(e0,e3)!=op(e4,e3)),inference(split_conjunct,[status(thm)],[3])).
% cnf(167,plain,(op(e0,e3)!=op(e3,e3)),inference(split_conjunct,[status(thm)],[3])).
% cnf(171,plain,(op(e2,e2)!=op(e4,e2)),inference(split_conjunct,[status(thm)],[3])).
% cnf(173,plain,(op(e1,e2)!=op(e4,e2)),inference(split_conjunct,[status(thm)],[3])).
% cnf(176,plain,(op(e0,e2)!=op(e4,e2)),inference(split_conjunct,[status(thm)],[3])).
% cnf(179,plain,(op(e0,e2)!=op(e1,e2)),inference(split_conjunct,[status(thm)],[3])).
% cnf(184,plain,(op(e1,e1)!=op(e3,e1)),inference(split_conjunct,[status(thm)],[3])).
% cnf(185,plain,(op(e1,e1)!=op(e2,e1)),inference(split_conjunct,[status(thm)],[3])).
% cnf(191,plain,(op(e2,e0)!=op(e4,e0)),inference(split_conjunct,[status(thm)],[3])).
% cnf(200,plain,(e4=op(e1,e1)),inference(split_conjunct,[status(thm)],[4])).
% cnf(201,plain,(e3=op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))),inference(split_conjunct,[status(thm)],[4])).
% cnf(202,plain,(e2=op(op(e1,e1),op(e1,e1))),inference(split_conjunct,[status(thm)],[4])).
% cnf(203,plain,(e0=op(e1,op(op(e1,e1),op(e1,e1)))),inference(split_conjunct,[status(thm)],[4])).
% cnf(204,plain,(unit=e4|unit=e3|unit=e2|unit=e1|unit=e0),inference(split_conjunct,[status(thm)],[5])).
% cnf(205,plain,(op(e4,unit)=e4),inference(split_conjunct,[status(thm)],[5])).
% cnf(206,plain,(op(unit,e4)=e4),inference(split_conjunct,[status(thm)],[5])).
% cnf(207,plain,(op(e3,unit)=e3),inference(split_conjunct,[status(thm)],[5])).
% cnf(208,plain,(op(unit,e3)=e3),inference(split_conjunct,[status(thm)],[5])).
% cnf(209,plain,(op(e2,unit)=e2),inference(split_conjunct,[status(thm)],[5])).
% cnf(210,plain,(op(unit,e2)=e2),inference(split_conjunct,[status(thm)],[5])).
% cnf(211,plain,(op(e1,unit)=e1),inference(split_conjunct,[status(thm)],[5])).
% cnf(212,plain,(op(unit,e1)=e1),inference(split_conjunct,[status(thm)],[5])).
% cnf(213,plain,(op(e0,unit)=e0),inference(split_conjunct,[status(thm)],[5])).
% cnf(215,plain,(e3!=e4),inference(split_conjunct,[status(thm)],[6])).
% cnf(216,plain,(e2!=e4),inference(split_conjunct,[status(thm)],[6])).
% cnf(217,plain,(e2!=e3),inference(split_conjunct,[status(thm)],[6])).
% cnf(218,plain,(e1!=e4),inference(split_conjunct,[status(thm)],[6])).
% cnf(219,plain,(e1!=e3),inference(split_conjunct,[status(thm)],[6])).
% cnf(220,plain,(e1!=e2),inference(split_conjunct,[status(thm)],[6])).
% cnf(221,plain,(e0!=e4),inference(split_conjunct,[status(thm)],[6])).
% cnf(222,plain,(e0!=e3),inference(split_conjunct,[status(thm)],[6])).
% cnf(223,plain,(e0!=e2),inference(split_conjunct,[status(thm)],[6])).
% cnf(224,plain,(e0!=e1),inference(split_conjunct,[status(thm)],[6])).
% fof(225, negated_conjecture,(((((((((op(e0,e0)=e0|op(e1,e1)=e0)|op(e2,e2)=e0)|op(e3,e3)=e0)|op(e4,e4)=e0)&((((op(e0,e0)=e1|op(e1,e1)=e1)|op(e2,e2)=e1)|op(e3,e3)=e1)|op(e4,e4)=e1))&((((op(e0,e0)=e2|op(e1,e1)=e2)|op(e2,e2)=e2)|op(e3,e3)=e2)|op(e4,e4)=e2))&((((op(e0,e0)=e3|op(e1,e1)=e3)|op(e2,e2)=e3)|op(e3,e3)=e3)|op(e4,e4)=e3))&((((op(e0,e0)=e4|op(e1,e1)=e4)|op(e2,e2)=e4)|op(e3,e3)=e4)|op(e4,e4)=e4))&(epred8_0|((~(op(e4,e4)=op(e4,e4))&op(op(e4,e4),e4)=e4)&~(op(op(e4,e4),e4)=e4)))),inference(fof_nnf,[status(thm)],[17])).
% fof(226, negated_conjecture,(((((((((op(e0,e0)=e0|op(e1,e1)=e0)|op(e2,e2)=e0)|op(e3,e3)=e0)|op(e4,e4)=e0)&((((op(e0,e0)=e1|op(e1,e1)=e1)|op(e2,e2)=e1)|op(e3,e3)=e1)|op(e4,e4)=e1))&((((op(e0,e0)=e2|op(e1,e1)=e2)|op(e2,e2)=e2)|op(e3,e3)=e2)|op(e4,e4)=e2))&((((op(e0,e0)=e3|op(e1,e1)=e3)|op(e2,e2)=e3)|op(e3,e3)=e3)|op(e4,e4)=e3))&((((op(e0,e0)=e4|op(e1,e1)=e4)|op(e2,e2)=e4)|op(e3,e3)=e4)|op(e4,e4)=e4))&(((~(op(e4,e4)=op(e4,e4))|epred8_0)&(op(op(e4,e4),e4)=e4|epred8_0))&(~(op(op(e4,e4),e4)=e4)|epred8_0))),inference(distribute,[status(thm)],[225])).
% cnf(229,negated_conjecture,(epred8_0|$false),inference(split_conjunct,[status(thm)],[226])).
% cnf(233,negated_conjecture,(op(e4,e4)=e1|op(e3,e3)=e1|op(e2,e2)=e1|op(e1,e1)=e1|op(e0,e0)=e1),inference(split_conjunct,[status(thm)],[226])).
% cnf(234,negated_conjecture,(op(e4,e4)=e0|op(e3,e3)=e0|op(e2,e2)=e0|op(e1,e1)=e0|op(e0,e0)=e0),inference(split_conjunct,[status(thm)],[226])).
% fof(235, plain,(~(epred1_0)|((((~(op(e0,e0)=op(e0,e0))&op(op(e0,e0),e0)=e0)&~(op(op(e0,e0),e0)=e0))|((~(op(e1,e0)=op(e0,e1))&op(op(e0,e1),e1)=e0)&~(op(op(e0,e1),e0)=e1)))|((~(op(e2,e0)=op(e0,e2))&op(op(e0,e2),e2)=e0)&~(op(op(e0,e2),e0)=e2)))),inference(fof_nnf,[status(thm)],[9])).
% fof(236, plain,((((((((~(op(e2,e0)=op(e0,e2))|(~(op(e1,e0)=op(e0,e1))|~(op(e0,e0)=op(e0,e0))))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(~(op(e1,e0)=op(e0,e1))|~(op(e0,e0)=op(e0,e0))))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(~(op(e1,e0)=op(e0,e1))|~(op(e0,e0)=op(e0,e0))))|~(epred1_0)))&((((~(op(e2,e0)=op(e0,e2))|(op(op(e0,e1),e1)=e0|~(op(e0,e0)=op(e0,e0))))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(op(op(e0,e1),e1)=e0|~(op(e0,e0)=op(e0,e0))))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(op(op(e0,e1),e1)=e0|~(op(e0,e0)=op(e0,e0))))|~(epred1_0))))&((((~(op(e2,e0)=op(e0,e2))|(~(op(op(e0,e1),e0)=e1)|~(op(e0,e0)=op(e0,e0))))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(~(op(op(e0,e1),e0)=e1)|~(op(e0,e0)=op(e0,e0))))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(~(op(op(e0,e1),e0)=e1)|~(op(e0,e0)=op(e0,e0))))|~(epred1_0))))&((((((~(op(e2,e0)=op(e0,e2))|(~(op(e1,e0)=op(e0,e1))|op(op(e0,e0),e0)=e0))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(~(op(e1,e0)=op(e0,e1))|op(op(e0,e0),e0)=e0))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(~(op(e1,e0)=op(e0,e1))|op(op(e0,e0),e0)=e0))|~(epred1_0)))&((((~(op(e2,e0)=op(e0,e2))|(op(op(e0,e1),e1)=e0|op(op(e0,e0),e0)=e0))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(op(op(e0,e1),e1)=e0|op(op(e0,e0),e0)=e0))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(op(op(e0,e1),e1)=e0|op(op(e0,e0),e0)=e0))|~(epred1_0))))&((((~(op(e2,e0)=op(e0,e2))|(~(op(op(e0,e1),e0)=e1)|op(op(e0,e0),e0)=e0))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(~(op(op(e0,e1),e0)=e1)|op(op(e0,e0),e0)=e0))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(~(op(op(e0,e1),e0)=e1)|op(op(e0,e0),e0)=e0))|~(epred1_0)))))&((((((~(op(e2,e0)=op(e0,e2))|(~(op(e1,e0)=op(e0,e1))|~(op(op(e0,e0),e0)=e0)))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(~(op(e1,e0)=op(e0,e1))|~(op(op(e0,e0),e0)=e0)))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(~(op(e1,e0)=op(e0,e1))|~(op(op(e0,e0),e0)=e0)))|~(epred1_0)))&((((~(op(e2,e0)=op(e0,e2))|(op(op(e0,e1),e1)=e0|~(op(op(e0,e0),e0)=e0)))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(op(op(e0,e1),e1)=e0|~(op(op(e0,e0),e0)=e0)))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(op(op(e0,e1),e1)=e0|~(op(op(e0,e0),e0)=e0)))|~(epred1_0))))&((((~(op(e2,e0)=op(e0,e2))|(~(op(op(e0,e1),e0)=e1)|~(op(op(e0,e0),e0)=e0)))|~(epred1_0))&((op(op(e0,e2),e2)=e0|(~(op(op(e0,e1),e0)=e1)|~(op(op(e0,e0),e0)=e0)))|~(epred1_0)))&((~(op(op(e0,e2),e0)=e2)|(~(op(op(e0,e1),e0)=e1)|~(op(op(e0,e0),e0)=e0)))|~(epred1_0))))),inference(distribute,[status(thm)],[235])).
% cnf(259,plain,(op(op(e0,e1),e1)=e0|op(op(e0,e2),e2)=e0|~epred1_0|$false),inference(split_conjunct,[status(thm)],[236])).
% fof(264, plain,(~(epred2_0)|(((epred1_0|((~(op(e3,e0)=op(e0,e3))&op(op(e0,e3),e3)=e0)&~(op(op(e0,e3),e0)=e3)))|((~(op(e4,e0)=op(e0,e4))&op(op(e0,e4),e4)=e0)&~(op(op(e0,e4),e0)=e4)))|((~(op(e0,e1)=op(e1,e0))&op(op(e1,e0),e0)=e1)&~(op(op(e1,e0),e1)=e0)))),inference(fof_nnf,[status(thm)],[18])).
% fof(265, plain,((((((((~(op(e0,e1)=op(e1,e0))|(~(op(e4,e0)=op(e0,e4))|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(~(op(e4,e0)=op(e0,e4))|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(~(op(e4,e0)=op(e0,e4))|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0)))&((((~(op(e0,e1)=op(e1,e0))|(op(op(e0,e4),e4)=e0|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(op(op(e0,e4),e4)=e0|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(op(op(e0,e4),e4)=e0|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0))))&((((~(op(e0,e1)=op(e1,e0))|(~(op(op(e0,e4),e0)=e4)|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(~(op(op(e0,e4),e0)=e4)|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(~(op(op(e0,e4),e0)=e4)|(~(op(e3,e0)=op(e0,e3))|epred1_0)))|~(epred2_0))))&((((((~(op(e0,e1)=op(e1,e0))|(~(op(e4,e0)=op(e0,e4))|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(~(op(e4,e0)=op(e0,e4))|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(~(op(e4,e0)=op(e0,e4))|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0)))&((((~(op(e0,e1)=op(e1,e0))|(op(op(e0,e4),e4)=e0|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(op(op(e0,e4),e4)=e0|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(op(op(e0,e4),e4)=e0|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0))))&((((~(op(e0,e1)=op(e1,e0))|(~(op(op(e0,e4),e0)=e4)|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(~(op(op(e0,e4),e0)=e4)|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(~(op(op(e0,e4),e0)=e4)|(op(op(e0,e3),e3)=e0|epred1_0)))|~(epred2_0)))))&((((((~(op(e0,e1)=op(e1,e0))|(~(op(e4,e0)=op(e0,e4))|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(~(op(e4,e0)=op(e0,e4))|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(~(op(e4,e0)=op(e0,e4))|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0)))&((((~(op(e0,e1)=op(e1,e0))|(op(op(e0,e4),e4)=e0|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(op(op(e0,e4),e4)=e0|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(op(op(e0,e4),e4)=e0|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0))))&((((~(op(e0,e1)=op(e1,e0))|(~(op(op(e0,e4),e0)=e4)|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0))&((op(op(e1,e0),e0)=e1|(~(op(op(e0,e4),e0)=e4)|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0)))&((~(op(op(e1,e0),e1)=e0)|(~(op(op(e0,e4),e0)=e4)|(~(op(op(e0,e3),e0)=e3)|epred1_0)))|~(epred2_0))))),inference(distribute,[status(thm)],[264])).
% cnf(268,plain,(epred1_0|~epred2_0|op(op(e0,e3),e0)!=e3|op(op(e0,e4),e0)!=e4|op(e0,e1)!=op(e1,e0)),inference(split_conjunct,[status(thm)],[265])).
% fof(293, plain,(~(epred3_0)|(((epred2_0|((~(op(e1,e1)=op(e1,e1))&op(op(e1,e1),e1)=e1)&~(op(op(e1,e1),e1)=e1)))|((~(op(e2,e1)=op(e1,e2))&op(op(e1,e2),e2)=e1)&~(op(op(e1,e2),e1)=e2)))|((~(op(e3,e1)=op(e1,e3))&op(op(e1,e3),e3)=e1)&~(op(op(e1,e3),e1)=e3)))),inference(fof_nnf,[status(thm)],[19])).
% fof(294, plain,((((((((~(op(e3,e1)=op(e1,e3))|(~(op(e2,e1)=op(e1,e2))|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(~(op(e2,e1)=op(e1,e2))|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(~(op(e2,e1)=op(e1,e2))|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0)))&((((~(op(e3,e1)=op(e1,e3))|(op(op(e1,e2),e2)=e1|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(op(op(e1,e2),e2)=e1|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(op(op(e1,e2),e2)=e1|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0))))&((((~(op(e3,e1)=op(e1,e3))|(~(op(op(e1,e2),e1)=e2)|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(~(op(op(e1,e2),e1)=e2)|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(~(op(op(e1,e2),e1)=e2)|(~(op(e1,e1)=op(e1,e1))|epred2_0)))|~(epred3_0))))&((((((~(op(e3,e1)=op(e1,e3))|(~(op(e2,e1)=op(e1,e2))|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(~(op(e2,e1)=op(e1,e2))|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(~(op(e2,e1)=op(e1,e2))|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0)))&((((~(op(e3,e1)=op(e1,e3))|(op(op(e1,e2),e2)=e1|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(op(op(e1,e2),e2)=e1|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(op(op(e1,e2),e2)=e1|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0))))&((((~(op(e3,e1)=op(e1,e3))|(~(op(op(e1,e2),e1)=e2)|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(~(op(op(e1,e2),e1)=e2)|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(~(op(op(e1,e2),e1)=e2)|(op(op(e1,e1),e1)=e1|epred2_0)))|~(epred3_0)))))&((((((~(op(e3,e1)=op(e1,e3))|(~(op(e2,e1)=op(e1,e2))|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(~(op(e2,e1)=op(e1,e2))|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(~(op(e2,e1)=op(e1,e2))|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0)))&((((~(op(e3,e1)=op(e1,e3))|(op(op(e1,e2),e2)=e1|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(op(op(e1,e2),e2)=e1|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(op(op(e1,e2),e2)=e1|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0))))&((((~(op(e3,e1)=op(e1,e3))|(~(op(op(e1,e2),e1)=e2)|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0))&((op(op(e1,e3),e3)=e1|(~(op(op(e1,e2),e1)=e2)|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0)))&((~(op(op(e1,e3),e1)=e3)|(~(op(op(e1,e2),e1)=e2)|(~(op(op(e1,e1),e1)=e1)|epred2_0)))|~(epred3_0))))),inference(distribute,[status(thm)],[293])).
% cnf(317,plain,(epred2_0|op(op(e1,e2),e2)=e1|op(op(e1,e3),e3)=e1|~epred3_0|$false),inference(split_conjunct,[status(thm)],[294])).
% fof(322, plain,(~(epred4_0)|(((epred3_0|((~(op(e4,e1)=op(e1,e4))&op(op(e1,e4),e4)=e1)&~(op(op(e1,e4),e1)=e4)))|((~(op(e0,e2)=op(e2,e0))&op(op(e2,e0),e0)=e2)&~(op(op(e2,e0),e2)=e0)))|((~(op(e1,e2)=op(e2,e1))&op(op(e2,e1),e1)=e2)&~(op(op(e2,e1),e2)=e1)))),inference(fof_nnf,[status(thm)],[20])).
% fof(323, plain,((((((((~(op(e1,e2)=op(e2,e1))|(~(op(e0,e2)=op(e2,e0))|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(~(op(e0,e2)=op(e2,e0))|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(~(op(e0,e2)=op(e2,e0))|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0)))&((((~(op(e1,e2)=op(e2,e1))|(op(op(e2,e0),e0)=e2|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(op(op(e2,e0),e0)=e2|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(op(op(e2,e0),e0)=e2|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0))))&((((~(op(e1,e2)=op(e2,e1))|(~(op(op(e2,e0),e2)=e0)|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(~(op(op(e2,e0),e2)=e0)|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(~(op(op(e2,e0),e2)=e0)|(~(op(e4,e1)=op(e1,e4))|epred3_0)))|~(epred4_0))))&((((((~(op(e1,e2)=op(e2,e1))|(~(op(e0,e2)=op(e2,e0))|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(~(op(e0,e2)=op(e2,e0))|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(~(op(e0,e2)=op(e2,e0))|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0)))&((((~(op(e1,e2)=op(e2,e1))|(op(op(e2,e0),e0)=e2|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(op(op(e2,e0),e0)=e2|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(op(op(e2,e0),e0)=e2|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0))))&((((~(op(e1,e2)=op(e2,e1))|(~(op(op(e2,e0),e2)=e0)|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(~(op(op(e2,e0),e2)=e0)|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(~(op(op(e2,e0),e2)=e0)|(op(op(e1,e4),e4)=e1|epred3_0)))|~(epred4_0)))))&((((((~(op(e1,e2)=op(e2,e1))|(~(op(e0,e2)=op(e2,e0))|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(~(op(e0,e2)=op(e2,e0))|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(~(op(e0,e2)=op(e2,e0))|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0)))&((((~(op(e1,e2)=op(e2,e1))|(op(op(e2,e0),e0)=e2|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(op(op(e2,e0),e0)=e2|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(op(op(e2,e0),e0)=e2|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0))))&((((~(op(e1,e2)=op(e2,e1))|(~(op(op(e2,e0),e2)=e0)|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0))&((op(op(e2,e1),e1)=e2|(~(op(op(e2,e0),e2)=e0)|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0)))&((~(op(op(e2,e1),e2)=e1)|(~(op(op(e2,e0),e2)=e0)|(~(op(op(e1,e4),e1)=e4)|epred3_0)))|~(epred4_0))))),inference(distribute,[status(thm)],[322])).
% cnf(350,plain,(epred3_0|~epred4_0|op(e4,e1)!=op(e1,e4)|op(e0,e2)!=op(e2,e0)|op(e1,e2)!=op(e2,e1)),inference(split_conjunct,[status(thm)],[323])).
% fof(351, plain,(~(epred5_0)|(((epred4_0|((~(op(e2,e2)=op(e2,e2))&op(op(e2,e2),e2)=e2)&~(op(op(e2,e2),e2)=e2)))|((~(op(e3,e2)=op(e2,e3))&op(op(e2,e3),e3)=e2)&~(op(op(e2,e3),e2)=e3)))|((~(op(e4,e2)=op(e2,e4))&op(op(e2,e4),e4)=e2)&~(op(op(e2,e4),e2)=e4)))),inference(fof_nnf,[status(thm)],[21])).
% fof(352, plain,((((((((~(op(e4,e2)=op(e2,e4))|(~(op(e3,e2)=op(e2,e3))|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(~(op(e3,e2)=op(e2,e3))|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(~(op(e3,e2)=op(e2,e3))|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0)))&((((~(op(e4,e2)=op(e2,e4))|(op(op(e2,e3),e3)=e2|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(op(op(e2,e3),e3)=e2|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(op(op(e2,e3),e3)=e2|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0))))&((((~(op(e4,e2)=op(e2,e4))|(~(op(op(e2,e3),e2)=e3)|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(~(op(op(e2,e3),e2)=e3)|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(~(op(op(e2,e3),e2)=e3)|(~(op(e2,e2)=op(e2,e2))|epred4_0)))|~(epred5_0))))&((((((~(op(e4,e2)=op(e2,e4))|(~(op(e3,e2)=op(e2,e3))|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(~(op(e3,e2)=op(e2,e3))|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(~(op(e3,e2)=op(e2,e3))|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0)))&((((~(op(e4,e2)=op(e2,e4))|(op(op(e2,e3),e3)=e2|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(op(op(e2,e3),e3)=e2|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(op(op(e2,e3),e3)=e2|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0))))&((((~(op(e4,e2)=op(e2,e4))|(~(op(op(e2,e3),e2)=e3)|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(~(op(op(e2,e3),e2)=e3)|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(~(op(op(e2,e3),e2)=e3)|(op(op(e2,e2),e2)=e2|epred4_0)))|~(epred5_0)))))&((((((~(op(e4,e2)=op(e2,e4))|(~(op(e3,e2)=op(e2,e3))|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(~(op(e3,e2)=op(e2,e3))|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(~(op(e3,e2)=op(e2,e3))|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0)))&((((~(op(e4,e2)=op(e2,e4))|(op(op(e2,e3),e3)=e2|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(op(op(e2,e3),e3)=e2|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(op(op(e2,e3),e3)=e2|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0))))&((((~(op(e4,e2)=op(e2,e4))|(~(op(op(e2,e3),e2)=e3)|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0))&((op(op(e2,e4),e4)=e2|(~(op(op(e2,e3),e2)=e3)|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0)))&((~(op(op(e2,e4),e2)=e4)|(~(op(op(e2,e3),e2)=e3)|(~(op(op(e2,e2),e2)=e2)|epred4_0)))|~(epred5_0))))),inference(distribute,[status(thm)],[351])).
% cnf(375,plain,(epred4_0|op(op(e2,e3),e3)=e2|op(op(e2,e4),e4)=e2|~epred5_0|$false),inference(split_conjunct,[status(thm)],[352])).
% fof(380, plain,(~(epred6_0)|(((epred5_0|((~(op(e0,e3)=op(e3,e0))&op(op(e3,e0),e0)=e3)&~(op(op(e3,e0),e3)=e0)))|((~(op(e1,e3)=op(e3,e1))&op(op(e3,e1),e1)=e3)&~(op(op(e3,e1),e3)=e1)))|((~(op(e2,e3)=op(e3,e2))&op(op(e3,e2),e2)=e3)&~(op(op(e3,e2),e3)=e2)))),inference(fof_nnf,[status(thm)],[22])).
% fof(381, plain,((((((((~(op(e2,e3)=op(e3,e2))|(~(op(e1,e3)=op(e3,e1))|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(~(op(e1,e3)=op(e3,e1))|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(~(op(e1,e3)=op(e3,e1))|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0)))&((((~(op(e2,e3)=op(e3,e2))|(op(op(e3,e1),e1)=e3|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(op(op(e3,e1),e1)=e3|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(op(op(e3,e1),e1)=e3|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0))))&((((~(op(e2,e3)=op(e3,e2))|(~(op(op(e3,e1),e3)=e1)|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(~(op(op(e3,e1),e3)=e1)|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(~(op(op(e3,e1),e3)=e1)|(~(op(e0,e3)=op(e3,e0))|epred5_0)))|~(epred6_0))))&((((((~(op(e2,e3)=op(e3,e2))|(~(op(e1,e3)=op(e3,e1))|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(~(op(e1,e3)=op(e3,e1))|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(~(op(e1,e3)=op(e3,e1))|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0)))&((((~(op(e2,e3)=op(e3,e2))|(op(op(e3,e1),e1)=e3|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(op(op(e3,e1),e1)=e3|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(op(op(e3,e1),e1)=e3|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0))))&((((~(op(e2,e3)=op(e3,e2))|(~(op(op(e3,e1),e3)=e1)|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(~(op(op(e3,e1),e3)=e1)|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(~(op(op(e3,e1),e3)=e1)|(op(op(e3,e0),e0)=e3|epred5_0)))|~(epred6_0)))))&((((((~(op(e2,e3)=op(e3,e2))|(~(op(e1,e3)=op(e3,e1))|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(~(op(e1,e3)=op(e3,e1))|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(~(op(e1,e3)=op(e3,e1))|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0)))&((((~(op(e2,e3)=op(e3,e2))|(op(op(e3,e1),e1)=e3|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(op(op(e3,e1),e1)=e3|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(op(op(e3,e1),e1)=e3|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0))))&((((~(op(e2,e3)=op(e3,e2))|(~(op(op(e3,e1),e3)=e1)|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0))&((op(op(e3,e2),e2)=e3|(~(op(op(e3,e1),e3)=e1)|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0)))&((~(op(op(e3,e2),e3)=e2)|(~(op(op(e3,e1),e3)=e1)|(~(op(op(e3,e0),e3)=e0)|epred5_0)))|~(epred6_0))))),inference(distribute,[status(thm)],[380])).
% cnf(408,plain,(epred5_0|~epred6_0|op(e0,e3)!=op(e3,e0)|op(e1,e3)!=op(e3,e1)|op(e2,e3)!=op(e3,e2)),inference(split_conjunct,[status(thm)],[381])).
% fof(409, plain,(~(epred7_0)|(((epred6_0|((~(op(e3,e3)=op(e3,e3))&op(op(e3,e3),e3)=e3)&~(op(op(e3,e3),e3)=e3)))|((~(op(e4,e3)=op(e3,e4))&op(op(e3,e4),e4)=e3)&~(op(op(e3,e4),e3)=e4)))|((~(op(e0,e4)=op(e4,e0))&op(op(e4,e0),e0)=e4)&~(op(op(e4,e0),e4)=e0)))),inference(fof_nnf,[status(thm)],[23])).
% fof(410, plain,((((((((~(op(e0,e4)=op(e4,e0))|(~(op(e4,e3)=op(e3,e4))|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(~(op(e4,e3)=op(e3,e4))|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(~(op(e4,e3)=op(e3,e4))|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0)))&((((~(op(e0,e4)=op(e4,e0))|(op(op(e3,e4),e4)=e3|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(op(op(e3,e4),e4)=e3|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(op(op(e3,e4),e4)=e3|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0))))&((((~(op(e0,e4)=op(e4,e0))|(~(op(op(e3,e4),e3)=e4)|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(~(op(op(e3,e4),e3)=e4)|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(~(op(op(e3,e4),e3)=e4)|(~(op(e3,e3)=op(e3,e3))|epred6_0)))|~(epred7_0))))&((((((~(op(e0,e4)=op(e4,e0))|(~(op(e4,e3)=op(e3,e4))|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(~(op(e4,e3)=op(e3,e4))|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(~(op(e4,e3)=op(e3,e4))|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0)))&((((~(op(e0,e4)=op(e4,e0))|(op(op(e3,e4),e4)=e3|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(op(op(e3,e4),e4)=e3|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(op(op(e3,e4),e4)=e3|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0))))&((((~(op(e0,e4)=op(e4,e0))|(~(op(op(e3,e4),e3)=e4)|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(~(op(op(e3,e4),e3)=e4)|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(~(op(op(e3,e4),e3)=e4)|(op(op(e3,e3),e3)=e3|epred6_0)))|~(epred7_0)))))&((((((~(op(e0,e4)=op(e4,e0))|(~(op(e4,e3)=op(e3,e4))|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(~(op(e4,e3)=op(e3,e4))|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(~(op(e4,e3)=op(e3,e4))|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0)))&((((~(op(e0,e4)=op(e4,e0))|(op(op(e3,e4),e4)=e3|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(op(op(e3,e4),e4)=e3|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(op(op(e3,e4),e4)=e3|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0))))&((((~(op(e0,e4)=op(e4,e0))|(~(op(op(e3,e4),e3)=e4)|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0))&((op(op(e4,e0),e0)=e4|(~(op(op(e3,e4),e3)=e4)|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0)))&((~(op(op(e4,e0),e4)=e0)|(~(op(op(e3,e4),e3)=e4)|(~(op(op(e3,e3),e3)=e3)|epred6_0)))|~(epred7_0))))),inference(distribute,[status(thm)],[409])).
% cnf(437,plain,(epred6_0|~epred7_0|$false|op(e4,e3)!=op(e3,e4)|op(e0,e4)!=op(e4,e0)),inference(split_conjunct,[status(thm)],[410])).
% fof(438, plain,(~(epred8_0)|(((epred7_0|((~(op(e1,e4)=op(e4,e1))&op(op(e4,e1),e1)=e4)&~(op(op(e4,e1),e4)=e1)))|((~(op(e2,e4)=op(e4,e2))&op(op(e4,e2),e2)=e4)&~(op(op(e4,e2),e4)=e2)))|((~(op(e3,e4)=op(e4,e3))&op(op(e4,e3),e3)=e4)&~(op(op(e4,e3),e4)=e3)))),inference(fof_nnf,[status(thm)],[24])).
% fof(439, plain,((((((((~(op(e3,e4)=op(e4,e3))|(~(op(e2,e4)=op(e4,e2))|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(~(op(e2,e4)=op(e4,e2))|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(~(op(e2,e4)=op(e4,e2))|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0)))&((((~(op(e3,e4)=op(e4,e3))|(op(op(e4,e2),e2)=e4|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(op(op(e4,e2),e2)=e4|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(op(op(e4,e2),e2)=e4|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0))))&((((~(op(e3,e4)=op(e4,e3))|(~(op(op(e4,e2),e4)=e2)|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(~(op(op(e4,e2),e4)=e2)|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(~(op(op(e4,e2),e4)=e2)|(~(op(e1,e4)=op(e4,e1))|epred7_0)))|~(epred8_0))))&((((((~(op(e3,e4)=op(e4,e3))|(~(op(e2,e4)=op(e4,e2))|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(~(op(e2,e4)=op(e4,e2))|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(~(op(e2,e4)=op(e4,e2))|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0)))&((((~(op(e3,e4)=op(e4,e3))|(op(op(e4,e2),e2)=e4|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(op(op(e4,e2),e2)=e4|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(op(op(e4,e2),e2)=e4|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0))))&((((~(op(e3,e4)=op(e4,e3))|(~(op(op(e4,e2),e4)=e2)|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(~(op(op(e4,e2),e4)=e2)|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(~(op(op(e4,e2),e4)=e2)|(op(op(e4,e1),e1)=e4|epred7_0)))|~(epred8_0)))))&((((((~(op(e3,e4)=op(e4,e3))|(~(op(e2,e4)=op(e4,e2))|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(~(op(e2,e4)=op(e4,e2))|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(~(op(e2,e4)=op(e4,e2))|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0)))&((((~(op(e3,e4)=op(e4,e3))|(op(op(e4,e2),e2)=e4|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(op(op(e4,e2),e2)=e4|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(op(op(e4,e2),e2)=e4|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0))))&((((~(op(e3,e4)=op(e4,e3))|(~(op(op(e4,e2),e4)=e2)|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0))&((op(op(e4,e3),e3)=e4|(~(op(op(e4,e2),e4)=e2)|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0)))&((~(op(op(e4,e3),e4)=e3)|(~(op(op(e4,e2),e4)=e2)|(~(op(op(e4,e1),e4)=e1)|epred7_0)))|~(epred8_0))))),inference(distribute,[status(thm)],[438])).
% cnf(456,plain,(epred7_0|op(op(e4,e1),e1)=e4|op(op(e4,e3),e3)=e4|~epred8_0|op(e2,e4)!=op(e4,e2)),inference(split_conjunct,[status(thm)],[439])).
% cnf(469,plain,(op(e4,e4)=e2),inference(rw,[status(thm)],[inference(rw,[status(thm)],[202,200,theory(equality)]),200,theory(equality)])).
% cnf(470,plain,(op(e1,e2)=e0),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[203,200,theory(equality)]),200,theory(equality)]),469,theory(equality)])).
% cnf(471,plain,(op(e2,e2)=e3),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[201,200,theory(equality)]),200,theory(equality)]),469,theory(equality)]),200,theory(equality)]),200,theory(equality)]),469,theory(equality)])).
% cnf(474,plain,(e0!=op(e0,e2)),inference(rw,[status(thm)],[179,470,theory(equality)])).
% cnf(480,plain,(op(e1,e4)!=e4),inference(rw,[status(thm)],[133,200,theory(equality)])).
% cnf(484,negated_conjecture,(op(e0,e0)=e0|e4=e0|op(e2,e2)=e0|op(e3,e3)=e0|op(e4,e4)=e0),inference(rw,[status(thm)],[234,200,theory(equality)])).
% cnf(485,negated_conjecture,(op(e0,e0)=e0|e4=e0|e3=e0|op(e3,e3)=e0|op(e4,e4)=e0),inference(rw,[status(thm)],[484,471,theory(equality)])).
% cnf(486,negated_conjecture,(op(e0,e0)=e0|e4=e0|e3=e0|op(e3,e3)=e0|e2=e0),inference(rw,[status(thm)],[485,469,theory(equality)])).
% cnf(487,negated_conjecture,(op(e0,e0)=e0|e3=e0|op(e3,e3)=e0|e2=e0),inference(sr,[status(thm)],[486,221,theory(equality)])).
% cnf(488,negated_conjecture,(op(e0,e0)=e0|op(e3,e3)=e0|e2=e0),inference(sr,[status(thm)],[487,222,theory(equality)])).
% cnf(489,negated_conjecture,(op(e0,e0)=e0|op(e3,e3)=e0),inference(sr,[status(thm)],[488,223,theory(equality)])).
% cnf(490,plain,(op(e2,e1)!=e4),inference(rw,[status(thm)],[185,200,theory(equality)])).
% cnf(491,negated_conjecture,(op(e0,e0)=e1|e4=e1|op(e2,e2)=e1|op(e3,e3)=e1|op(e4,e4)=e1),inference(rw,[status(thm)],[233,200,theory(equality)])).
% cnf(492,negated_conjecture,(op(e0,e0)=e1|e4=e1|e3=e1|op(e3,e3)=e1|op(e4,e4)=e1),inference(rw,[status(thm)],[491,471,theory(equality)])).
% cnf(493,negated_conjecture,(op(e0,e0)=e1|e4=e1|e3=e1|op(e3,e3)=e1|e2=e1),inference(rw,[status(thm)],[492,469,theory(equality)])).
% cnf(494,negated_conjecture,(op(e0,e0)=e1|e3=e1|op(e3,e3)=e1|e2=e1),inference(sr,[status(thm)],[493,218,theory(equality)])).
% cnf(495,negated_conjecture,(op(e0,e0)=e1|op(e3,e3)=e1|e2=e1),inference(sr,[status(thm)],[494,219,theory(equality)])).
% cnf(496,negated_conjecture,(op(e0,e0)=e1|op(e3,e3)=e1),inference(sr,[status(thm)],[495,220,theory(equality)])).
% cnf(511,plain,(op(e2,e4)!=e3),inference(rw,[status(thm)],[121,471,theory(equality)])).
% cnf(517,plain,(op(e3,e1)!=e4),inference(rw,[status(thm)],[184,200,theory(equality)])).
% cnf(520,plain,(op(e0,e1)=e0|e4=e0|op(e2,e1)=e0|op(e3,e1)=e0|op(e4,e1)=e0),inference(rw,[status(thm)],[88,200,theory(equality)])).
% cnf(521,plain,(op(e0,e1)=e0|op(e2,e1)=e0|op(e3,e1)=e0|op(e4,e1)=e0),inference(sr,[status(thm)],[520,221,theory(equality)])).
% cnf(525,plain,(op(e0,e1)=e2|e4=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2),inference(rw,[status(thm)],[84,200,theory(equality)])).
% cnf(526,plain,(op(e0,e1)=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2),inference(sr,[status(thm)],[525,216,theory(equality)])).
% cnf(545,plain,(op(e0,e2)=e4|e0=e4|op(e2,e2)=e4|op(e3,e2)=e4|op(e4,e2)=e4),inference(rw,[status(thm)],[70,470,theory(equality)])).
% cnf(546,plain,(op(e0,e2)=e4|e0=e4|e3=e4|op(e3,e2)=e4|op(e4,e2)=e4),inference(rw,[status(thm)],[545,471,theory(equality)])).
% cnf(547,plain,(op(e0,e2)=e4|e4=e3|op(e3,e2)=e4|op(e4,e2)=e4),inference(sr,[status(thm)],[546,221,theory(equality)])).
% cnf(548,plain,(op(e0,e2)=e4|op(e3,e2)=e4|op(e4,e2)=e4),inference(sr,[status(thm)],[547,215,theory(equality)])).
% cnf(551,plain,(op(e4,e2)!=e0),inference(rw,[status(thm)],[173,470,theory(equality)])).
% cnf(552,plain,(op(e4,e2)!=e3),inference(rw,[status(thm)],[171,471,theory(equality)])).
% cnf(563,plain,(e2!=op(e1,e4)),inference(rw,[status(thm)],[153,469,theory(equality)])).
% cnf(564,plain,(e2!=op(e2,e4)),inference(rw,[status(thm)],[151,469,theory(equality)])).
% cnf(565,plain,(e2!=op(e3,e4)),inference(rw,[status(thm)],[150,469,theory(equality)])).
% cnf(567,plain,(op(e0,e4)=e3|op(e1,e4)=e3|op(e2,e4)=e3|op(e3,e4)=e3|e2=e3),inference(rw,[status(thm)],[52,469,theory(equality)])).
% cnf(568,plain,(op(e0,e4)=e3|op(e1,e4)=e3|op(e3,e4)=e3|e3=e2),inference(sr,[status(thm)],[567,511,theory(equality)])).
% cnf(569,plain,(op(e0,e4)=e3|op(e1,e4)=e3|op(e3,e4)=e3),inference(sr,[status(thm)],[568,217,theory(equality)])).
% cnf(575,plain,(e2!=op(e4,e1)),inference(rw,[status(thm)],[103,469,theory(equality)])).
% cnf(576,plain,(op(e3,e1)=e2|op(e2,e1)=e2|op(e0,e1)=e2),inference(sr,[status(thm)],[526,575,theory(equality)])).
% cnf(577,plain,(e2!=op(e4,e2)),inference(rw,[status(thm)],[101,469,theory(equality)])).
% cnf(579,plain,(e2!=op(e4,e3)),inference(rw,[status(thm)],[100,469,theory(equality)])).
% cnf(580,plain,(op(e3,e3)=e2|op(e2,e3)=e2|op(e1,e3)=e2|op(e0,e3)=e2),inference(sr,[status(thm)],[64,579,theory(equality)])).
% cnf(594,plain,(op(e0,e2)=e1|op(op(e1,e3),e3)=e1|epred2_0|~epred3_0),inference(rw,[status(thm)],[317,470,theory(equality)])).
% cnf(630,plain,(op(e2,e0)=e4|op(e2,e1)=e4|e3=e4|op(e2,e3)=e4|op(e2,e4)=e4),inference(rw,[status(thm)],[71,471,theory(equality)])).
% cnf(631,plain,(op(e2,e0)=e4|e4=e3|op(e2,e3)=e4|op(e2,e4)=e4),inference(sr,[status(thm)],[630,490,theory(equality)])).
% cnf(632,plain,(op(e2,e0)=e4|op(e2,e3)=e4|op(e2,e4)=e4),inference(sr,[status(thm)],[631,215,theory(equality)])).
% cnf(642,plain,(op(e2,e4)=e0|op(e2,e4)=e1|op(e2,e4)=e3|op(e2,e4)=e4),inference(sr,[status(thm)],[35,564,theory(equality)])).
% cnf(643,plain,(op(e2,e4)=e0|op(e2,e4)=e1|op(e2,e4)=e4),inference(sr,[status(thm)],[642,511,theory(equality)])).
% cnf(646,plain,(op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2),inference(sr,[status(thm)],[65,565,theory(equality)])).
% cnf(654,plain,(op(e3,e4)=e0|op(e3,e4)=e1|op(e3,e4)=e3|op(e3,e4)=e4),inference(sr,[status(thm)],[30,565,theory(equality)])).
% cnf(662,plain,(op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e2)=e3|op(e4,e3)=e3|e2=e3),inference(rw,[status(thm)],[53,469,theory(equality)])).
% cnf(663,plain,(op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3|e3=e2),inference(sr,[status(thm)],[662,552,theory(equality)])).
% cnf(664,plain,(op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3),inference(sr,[status(thm)],[663,217,theory(equality)])).
% cnf(671,plain,(op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e3|op(e4,e2)=e4),inference(sr,[status(thm)],[27,551,theory(equality)])).
% cnf(672,plain,(op(e4,e2)=e1|op(e4,e2)=e3|op(e4,e2)=e4),inference(sr,[status(thm)],[671,577,theory(equality)])).
% cnf(673,plain,(op(e4,e2)=e1|op(e4,e2)=e4),inference(sr,[status(thm)],[672,552,theory(equality)])).
% cnf(674,plain,(op(e4,e3)=e0|op(e4,e3)=e1|op(e4,e3)=e3|op(e4,e3)=e4),inference(sr,[status(thm)],[26,579,theory(equality)])).
% cnf(703,plain,(op(op(e4,e1),e1)=e4|op(op(e4,e3),e3)=e4|epred7_0|op(e4,e2)!=op(e2,e4)|$false),inference(rw,[status(thm)],[456,229,theory(equality)])).
% cnf(704,plain,(op(op(e4,e1),e1)=e4|op(op(e4,e3),e3)=e4|epred7_0|op(e4,e2)!=op(e2,e4)),inference(cn,[status(thm)],[703,theory(equality)])).
% cnf(777,plain,(epred3_0|op(e2,e0)!=op(e0,e2)|op(e2,e1)!=e0|op(e4,e1)!=op(e1,e4)|~epred4_0),inference(rw,[status(thm)],[350,470,theory(equality)])).
% cnf(958,plain,(op(e2,e0)=e4|op(e2,e3)=e4|e4!=op(e0,e4)),inference(spm,[status(thm)],[158,632,theory(equality)])).
% cnf(959,plain,(op(e2,e4)=e0|op(e2,e4)=e1|e4!=op(e0,e4)),inference(spm,[status(thm)],[158,643,theory(equality)])).
% cnf(986,plain,(op(e2,e4)=e2|unit=e0|unit=e1|unit=e2|unit=e3),inference(spm,[status(thm)],[209,204,theory(equality)])).
% cnf(994,plain,(unit=e0|unit=e1|unit=e2|unit=e3),inference(sr,[status(thm)],[986,564,theory(equality)])).
% cnf(1013,negated_conjecture,(op(e0,e0)=e0|e0!=op(e0,e3)),inference(spm,[status(thm)],[167,489,theory(equality)])).
% cnf(1016,negated_conjecture,(op(e0,e0)=e1|e1!=op(e1,e3)),inference(spm,[status(thm)],[164,496,theory(equality)])).
% cnf(1069,plain,(op(e0,e4)=e3|op(e1,e4)=e3|e3!=op(e3,e0)),inference(spm,[status(thm)],[116,569,theory(equality)])).
% cnf(1163,plain,(op(e4,e2)=e1|e4!=op(e4,e0)),inference(spm,[status(thm)],[108,673,theory(equality)])).
% cnf(1171,plain,(op(e4,e0)=e3|op(e4,e1)=e3|e3!=op(e0,e3)),inference(spm,[status(thm)],[166,664,theory(equality)])).
% cnf(1254,plain,(op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|e2!=op(e1,e3)),inference(spm,[status(thm)],[164,646,theory(equality)])).
% cnf(1308,plain,(op(e3,e4)=e0|op(e3,e4)=e1|op(e3,e4)=e3|e4!=op(e0,e4)),inference(spm,[status(thm)],[157,654,theory(equality)])).
% cnf(1364,plain,(op(e4,e3)=e0|op(e4,e3)=e1|op(e4,e3)=e3|e4!=op(e2,e3)),inference(spm,[status(thm)],[161,674,theory(equality)])).
% cnf(1395,negated_conjecture,(op(e0,e0)=e1|e2=e1|op(e2,e3)=e2|op(e1,e3)=e2|op(e0,e3)=e2),inference(spm,[status(thm)],[496,580,theory(equality)])).
% cnf(1397,negated_conjecture,(op(e0,e0)=e1|op(e2,e3)=e2|op(e1,e3)=e2|op(e0,e3)=e2),inference(sr,[status(thm)],[1395,220,theory(equality)])).
% cnf(1705,plain,(op(e0,e3)=e0|unit=e2|unit=e1|unit=e0),inference(spm,[status(thm)],[213,994,theory(equality)])).
% cnf(1706,plain,(op(e1,e3)=e1|unit=e2|unit=e1|unit=e0),inference(spm,[status(thm)],[211,994,theory(equality)])).
% cnf(1796,negated_conjecture,(op(e0,e0)=e0|unit=e0|unit=e1|unit=e2),inference(spm,[status(thm)],[1013,1705,theory(equality)])).
% cnf(1863,negated_conjecture,(op(e0,e0)=e1|unit=e0|unit=e1|unit=e2),inference(spm,[status(thm)],[1016,1706,theory(equality)])).
% cnf(1917,negated_conjecture,(e1=e0|unit=e2|unit=e1|unit=e0),inference(spm,[status(thm)],[1796,1863,theory(equality)])).
% cnf(1919,negated_conjecture,(unit=e2|unit=e1|unit=e0),inference(sr,[status(thm)],[1917,224,theory(equality)])).
% cnf(1922,negated_conjecture,(op(e0,e2)=e0|unit=e0|unit=e1),inference(spm,[status(thm)],[213,1919,theory(equality)])).
% cnf(1932,negated_conjecture,(unit=e0|unit=e1),inference(sr,[status(thm)],[1922,474,theory(equality)])).
% cnf(1942,negated_conjecture,(op(e0,e0)=e0|unit=e1),inference(spm,[status(thm)],[213,1932,theory(equality)])).
% cnf(1943,negated_conjecture,(op(e1,e0)=e1|unit=e1),inference(spm,[status(thm)],[211,1932,theory(equality)])).
% cnf(1944,negated_conjecture,(op(e2,e0)=e2|unit=e1),inference(spm,[status(thm)],[209,1932,theory(equality)])).
% cnf(1945,negated_conjecture,(op(e3,e0)=e3|unit=e1),inference(spm,[status(thm)],[207,1932,theory(equality)])).
% cnf(1946,negated_conjecture,(op(e4,e0)=e4|unit=e1),inference(spm,[status(thm)],[205,1932,theory(equality)])).
% cnf(1948,negated_conjecture,(op(e0,e1)=e1|unit=e1),inference(spm,[status(thm)],[212,1932,theory(equality)])).
% cnf(1949,negated_conjecture,(op(e0,e2)=e2|unit=e1),inference(spm,[status(thm)],[210,1932,theory(equality)])).
% cnf(1950,negated_conjecture,(op(e0,e3)=e3|unit=e1),inference(spm,[status(thm)],[208,1932,theory(equality)])).
% cnf(1951,negated_conjecture,(op(e0,e4)=e4|unit=e1),inference(spm,[status(thm)],[206,1932,theory(equality)])).
% cnf(1977,negated_conjecture,(unit=e1|e0!=op(e0,e1)),inference(spm,[status(thm)],[149,1942,theory(equality)])).
% cnf(1986,negated_conjecture,(unit=e1|e2!=op(e2,e1)),inference(spm,[status(thm)],[129,1944,theory(equality)])).
% cnf(2002,negated_conjecture,(unit=e1|e4!=op(e2,e0)),inference(spm,[status(thm)],[191,1946,theory(equality)])).
% cnf(2010,negated_conjecture,(op(e4,e2)=e1|unit=e1),inference(spm,[status(thm)],[1163,1946,theory(equality)])).
% cnf(2016,negated_conjecture,(unit=e1|e1!=op(e0,e2)),inference(spm,[status(thm)],[176,2010,theory(equality)])).
% cnf(2025,negated_conjecture,(op(e0,e2)=e4|op(e3,e2)=e4|e1=e4|unit=e1),inference(spm,[status(thm)],[548,2010,theory(equality)])).
% cnf(2026,plain,(op(op(e4,e1),e1)=e4|op(op(e4,e3),e3)=e4|epred7_0|unit=e1|e1!=op(e2,e4)),inference(spm,[status(thm)],[704,2010,theory(equality)])).
% cnf(2036,negated_conjecture,(op(e0,e2)=e4|op(e3,e2)=e4|unit=e1),inference(sr,[status(thm)],[2025,218,theory(equality)])).
% cnf(2042,negated_conjecture,(unit=e1|e2!=op(e0,e1)),inference(spm,[status(thm)],[145,1949,theory(equality)])).
% cnf(2058,negated_conjecture,(unit=e1|e4!=op(e0,e2)),inference(spm,[status(thm)],[141,1951,theory(equality)])).
% cnf(2059,negated_conjecture,(unit=e1|e4!=op(e0,e3)),inference(spm,[status(thm)],[140,1951,theory(equality)])).
% cnf(2065,negated_conjecture,(op(e2,e4)=e1|op(e2,e4)=e0|unit=e1),inference(spm,[status(thm)],[959,1951,theory(equality)])).
% cnf(2066,negated_conjecture,(op(e2,e3)=e4|op(e2,e0)=e4|unit=e1),inference(spm,[status(thm)],[958,1951,theory(equality)])).
% cnf(2180,negated_conjecture,(op(e3,e2)=e4|unit=e1),inference(csr,[status(thm)],[2036,2058])).
% cnf(2195,negated_conjecture,(op(e2,e4)=e1|unit=e1|e0!=op(e2,e1)),inference(spm,[status(thm)],[123,2065,theory(equality)])).
% cnf(2205,negated_conjecture,(op(e2,e3)=e4|unit=e1),inference(csr,[status(thm)],[2066,2002])).
% cnf(2329,negated_conjecture,(op(e1,e4)=e3|op(e0,e4)=e3|unit=e1),inference(spm,[status(thm)],[1069,1945,theory(equality)])).
% cnf(2342,negated_conjecture,(e3=e4|unit=e1|op(e1,e4)=e3),inference(spm,[status(thm)],[1951,2329,theory(equality)])).
% cnf(2348,negated_conjecture,(unit=e1|op(e1,e4)=e3),inference(sr,[status(thm)],[2342,215,theory(equality)])).
% cnf(2480,negated_conjecture,(op(e4,e1)=e3|op(e4,e0)=e3|unit=e1),inference(spm,[status(thm)],[1171,1950,theory(equality)])).
% cnf(2490,negated_conjecture,(e3=e4|unit=e1|op(e4,e1)=e3),inference(spm,[status(thm)],[1946,2480,theory(equality)])).
% cnf(2498,negated_conjecture,(unit=e1|op(e4,e1)=e3),inference(sr,[status(thm)],[2490,215,theory(equality)])).
% cnf(2504,negated_conjecture,(op(e0,e1)=e0|op(e2,e1)=e0|op(e3,e1)=e0|e3=e0|unit=e1),inference(spm,[status(thm)],[521,2498,theory(equality)])).
% cnf(2521,negated_conjecture,(op(e0,e1)=e0|op(e2,e1)=e0|op(e3,e1)=e0|unit=e1),inference(sr,[status(thm)],[2504,222,theory(equality)])).
% cnf(2874,negated_conjecture,(op(e3,e1)=e0|op(e2,e1)=e0|unit=e1),inference(csr,[status(thm)],[2521,1977])).
% cnf(2878,negated_conjecture,(e0=e2|op(e2,e1)=e2|op(e0,e1)=e2|op(e2,e1)=e0|unit=e1),inference(spm,[status(thm)],[576,2874,theory(equality)])).
% cnf(2887,negated_conjecture,(op(e2,e1)=e2|op(e0,e1)=e2|op(e2,e1)=e0|unit=e1),inference(sr,[status(thm)],[2878,223,theory(equality)])).
% cnf(2928,negated_conjecture,(op(e2,e1)=e2|op(e2,e1)=e0|unit=e1),inference(csr,[status(thm)],[2887,2042])).
% cnf(2929,negated_conjecture,(op(e2,e1)=e0|unit=e1),inference(csr,[status(thm)],[2928,1986])).
% cnf(2934,negated_conjecture,(op(e2,e4)=e1|unit=e1),inference(spm,[status(thm)],[2195,2929,theory(equality)])).
% cnf(2943,negated_conjecture,(unit=e1|e1!=op(e2,e3)),inference(spm,[status(thm)],[120,2934,theory(equality)])).
% cnf(3275,negated_conjecture,(e2=e4|unit=e1|op(e0,e3)=e2|op(e1,e3)=e2|op(e0,e0)=e1),inference(spm,[status(thm)],[2205,1397,theory(equality)])).
% cnf(3277,negated_conjecture,(unit=e1|op(e0,e3)=e2|op(e1,e3)=e2|op(e0,e0)=e1),inference(sr,[status(thm)],[3275,216,theory(equality)])).
% cnf(3301,negated_conjecture,(e2=e3|unit=e1|op(e0,e0)=e1|op(e1,e3)=e2),inference(spm,[status(thm)],[1950,3277,theory(equality)])).
% cnf(3307,negated_conjecture,(unit=e1|op(e0,e0)=e1|op(e1,e3)=e2),inference(sr,[status(thm)],[3301,217,theory(equality)])).
% cnf(3310,negated_conjecture,(e1=e0|unit=e1|op(e1,e3)=e2),inference(spm,[status(thm)],[1942,3307,theory(equality)])).
% cnf(3317,negated_conjecture,(unit=e1|op(e1,e3)=e2),inference(sr,[status(thm)],[3310,224,theory(equality)])).
% cnf(3746,negated_conjecture,(op(e3,e2)=e2|op(e3,e1)=e2|op(e3,e0)=e2|unit=e1),inference(spm,[status(thm)],[1254,3317,theory(equality)])).
% cnf(3759,negated_conjecture,(e2=e4|unit=e1|op(e3,e0)=e2|op(e3,e1)=e2),inference(spm,[status(thm)],[2180,3746,theory(equality)])).
% cnf(3762,negated_conjecture,(unit=e1|op(e3,e0)=e2|op(e3,e1)=e2),inference(sr,[status(thm)],[3759,216,theory(equality)])).
% cnf(3767,negated_conjecture,(e2=e3|unit=e1|op(e3,e1)=e2),inference(spm,[status(thm)],[1945,3762,theory(equality)])).
% cnf(3780,negated_conjecture,(unit=e1|op(e3,e1)=e2),inference(sr,[status(thm)],[3767,217,theory(equality)])).
% cnf(4044,negated_conjecture,(op(e3,e4)=e3|op(e3,e4)=e1|op(e3,e4)=e0|unit=e1),inference(spm,[status(thm)],[1308,1951,theory(equality)])).
% cnf(4049,negated_conjecture,(op(e3,e4)=e0|op(e3,e4)=e1|unit=e1|e3!=op(e1,e4)),inference(spm,[status(thm)],[154,4044,theory(equality)])).
% cnf(4076,negated_conjecture,(op(e3,e4)=e0|op(e3,e4)=e1|unit=e1),inference(csr,[status(thm)],[4049,2348])).
% cnf(4473,negated_conjecture,(op(e4,e3)=e3|op(e4,e3)=e1|op(e4,e3)=e0|unit=e1),inference(spm,[status(thm)],[1364,2205,theory(equality)])).
% cnf(4477,negated_conjecture,(op(e4,e3)=e0|op(e4,e3)=e1|unit=e1|e3!=op(e0,e3)),inference(spm,[status(thm)],[166,4473,theory(equality)])).
% cnf(4503,negated_conjecture,(op(e4,e3)=e0|op(e4,e3)=e1|unit=e1),inference(csr,[status(thm)],[4477,1950])).
% cnf(6222,plain,(op(op(e4,e1),e1)=e4|op(op(e4,e3),e3)=e4|unit=e1|epred7_0),inference(csr,[status(thm)],[2026,2934])).
% cnf(6232,negated_conjecture,(op(e0,e3)=e4|op(op(e4,e1),e1)=e4|unit=e1|epred7_0|op(e4,e3)=e1),inference(spm,[status(thm)],[6222,4503,theory(equality)])).
% cnf(6294,negated_conjecture,(op(op(e4,e1),e1)=e4|op(e4,e3)=e1|unit=e1|epred7_0),inference(csr,[status(thm)],[6232,2059])).
% cnf(6299,negated_conjecture,(op(e3,e1)=e4|op(e4,e3)=e1|unit=e1|epred7_0),inference(spm,[status(thm)],[6294,2498,theory(equality)])).
% cnf(6304,negated_conjecture,(op(e4,e3)=e1|unit=e1|epred7_0),inference(sr,[status(thm)],[6299,517,theory(equality)])).
% cnf(6343,negated_conjecture,(unit=e1|epred7_0|e1!=op(e3,e3)),inference(spm,[status(thm)],[160,6304,theory(equality)])).
% cnf(6388,negated_conjecture,(unit=e1|epred7_0|op(e0,e0)=e1),inference(spm,[status(thm)],[6343,496,theory(equality)])).
% cnf(6450,negated_conjecture,(e1=e0|unit=e1|epred7_0),inference(spm,[status(thm)],[1942,6388,theory(equality)])).
% cnf(6465,negated_conjecture,(unit=e1|epred7_0),inference(sr,[status(thm)],[6450,224,theory(equality)])).
% cnf(6468,negated_conjecture,(op(e1,e1)=e1|epred7_0),inference(spm,[status(thm)],[211,6465,theory(equality)])).
% cnf(6477,negated_conjecture,(e4=e1|epred7_0),inference(rw,[status(thm)],[6468,200,theory(equality)])).
% cnf(6478,negated_conjecture,(epred7_0),inference(sr,[status(thm)],[6477,218,theory(equality)])).
% cnf(6526,plain,(epred6_0|op(e4,e0)!=op(e0,e4)|op(e4,e3)!=op(e3,e4)|$false),inference(rw,[status(thm)],[437,6478,theory(equality)])).
% cnf(6527,plain,(epred6_0|op(e4,e0)!=op(e0,e4)|op(e4,e3)!=op(e3,e4)),inference(cn,[status(thm)],[6526,theory(equality)])).
% cnf(6555,negated_conjecture,(epred6_0|unit=e1|e4!=op(e0,e4)|op(e4,e3)!=op(e3,e4)),inference(spm,[status(thm)],[6527,1946,theory(equality)])).
% cnf(6657,negated_conjecture,(unit=e1|epred6_0|op(e4,e3)!=op(e3,e4)),inference(csr,[status(thm)],[6555,1951])).
% cnf(6667,negated_conjecture,(unit=e1|epred6_0|op(e4,e3)=e1|e0!=op(e3,e4)),inference(spm,[status(thm)],[6657,4503,theory(equality)])).
% cnf(6678,negated_conjecture,(op(e4,e3)=e1|unit=e1|epred6_0|op(e3,e4)=e1),inference(spm,[status(thm)],[6667,4076,theory(equality)])).
% cnf(6685,negated_conjecture,(op(e3,e4)=e1|unit=e1|epred6_0|e1!=op(e4,e2)),inference(spm,[status(thm)],[102,6678,theory(equality)])).
% cnf(6805,negated_conjecture,(op(e3,e4)=e1|unit=e1|epred6_0),inference(csr,[status(thm)],[6685,2010])).
% cnf(6809,negated_conjecture,(unit=e1|epred6_0|e1!=op(e2,e4)),inference(spm,[status(thm)],[152,6805,theory(equality)])).
% cnf(6831,negated_conjecture,(unit=e1|epred6_0),inference(csr,[status(thm)],[6809,2934])).
% cnf(6833,negated_conjecture,(op(e1,e1)=e1|epred6_0),inference(spm,[status(thm)],[211,6831,theory(equality)])).
% cnf(6842,negated_conjecture,(e4=e1|epred6_0),inference(rw,[status(thm)],[6833,200,theory(equality)])).
% cnf(6843,negated_conjecture,(epred6_0),inference(sr,[status(thm)],[6842,218,theory(equality)])).
% cnf(6890,plain,(epred5_0|op(e3,e0)!=op(e0,e3)|op(e3,e1)!=op(e1,e3)|op(e3,e2)!=op(e2,e3)|$false),inference(rw,[status(thm)],[408,6843,theory(equality)])).
% cnf(6891,plain,(epred5_0|op(e3,e0)!=op(e0,e3)|op(e3,e1)!=op(e1,e3)|op(e3,e2)!=op(e2,e3)),inference(cn,[status(thm)],[6890,theory(equality)])).
% cnf(7112,negated_conjecture,(epred5_0|unit=e1|e3!=op(e0,e3)|op(e3,e1)!=op(e1,e3)|op(e3,e2)!=op(e2,e3)),inference(spm,[status(thm)],[6891,1945,theory(equality)])).
% cnf(10299,negated_conjecture,(unit=e1|epred5_0|op(e3,e1)!=op(e1,e3)|op(e3,e2)!=op(e2,e3)),inference(csr,[status(thm)],[7112,1950])).
% cnf(10307,negated_conjecture,(unit=e1|epred5_0|e2!=op(e1,e3)|op(e3,e2)!=op(e2,e3)),inference(spm,[status(thm)],[10299,3780,theory(equality)])).
% cnf(10358,negated_conjecture,(unit=e1|epred5_0|op(e3,e2)!=op(e2,e3)),inference(csr,[status(thm)],[10307,3317])).
% cnf(10365,negated_conjecture,(unit=e1|epred5_0|e4!=op(e2,e3)),inference(spm,[status(thm)],[10358,2180,theory(equality)])).
% cnf(10371,negated_conjecture,(unit=e1|epred5_0),inference(csr,[status(thm)],[10365,2205])).
% cnf(10373,negated_conjecture,(op(e1,e1)=e1|epred5_0),inference(spm,[status(thm)],[211,10371,theory(equality)])).
% cnf(10382,negated_conjecture,(e4=e1|epred5_0),inference(rw,[status(thm)],[10373,200,theory(equality)])).
% cnf(10383,negated_conjecture,(epred5_0),inference(sr,[status(thm)],[10382,218,theory(equality)])).
% cnf(10435,plain,(op(op(e2,e3),e3)=e2|op(op(e2,e4),e4)=e2|epred4_0|$false),inference(rw,[status(thm)],[375,10383,theory(equality)])).
% cnf(10436,plain,(op(op(e2,e3),e3)=e2|op(op(e2,e4),e4)=e2|epred4_0),inference(cn,[status(thm)],[10435,theory(equality)])).
% cnf(10453,negated_conjecture,(op(e1,e4)=e2|op(op(e2,e3),e3)=e2|epred4_0|unit=e1),inference(spm,[status(thm)],[10436,2934,theory(equality)])).
% cnf(10470,negated_conjecture,(op(op(e2,e3),e3)=e2|epred4_0|unit=e1),inference(sr,[status(thm)],[10453,563,theory(equality)])).
% cnf(10485,negated_conjecture,(op(e4,e3)=e2|unit=e1|epred4_0),inference(spm,[status(thm)],[10470,2205,theory(equality)])).
% cnf(10498,negated_conjecture,(unit=e1|epred4_0),inference(sr,[status(thm)],[10485,579,theory(equality)])).
% cnf(10502,negated_conjecture,(op(e1,e1)=e1|epred4_0),inference(spm,[status(thm)],[211,10498,theory(equality)])).
% cnf(10511,negated_conjecture,(e4=e1|epred4_0),inference(rw,[status(thm)],[10502,200,theory(equality)])).
% cnf(10512,negated_conjecture,(epred4_0),inference(sr,[status(thm)],[10511,218,theory(equality)])).
% cnf(10559,plain,(epred3_0|op(e2,e0)!=op(e0,e2)|op(e4,e1)!=op(e1,e4)|op(e2,e1)!=e0|$false),inference(rw,[status(thm)],[777,10512,theory(equality)])).
% cnf(10560,plain,(epred3_0|op(e2,e0)!=op(e0,e2)|op(e4,e1)!=op(e1,e4)|op(e2,e1)!=e0),inference(cn,[status(thm)],[10559,theory(equality)])).
% cnf(11267,negated_conjecture,(epred3_0|unit=e1|e2!=op(e0,e2)|op(e4,e1)!=op(e1,e4)|op(e2,e1)!=e0),inference(spm,[status(thm)],[10560,1944,theory(equality)])).
% cnf(12505,negated_conjecture,(unit=e1|epred3_0|op(e4,e1)!=op(e1,e4)|op(e0,e2)!=e2),inference(csr,[status(thm)],[11267,2929])).
% cnf(12506,negated_conjecture,(unit=e1|epred3_0|op(e4,e1)!=op(e1,e4)),inference(csr,[status(thm)],[12505,1949])).
% cnf(12513,negated_conjecture,(unit=e1|epred3_0|e3!=op(e1,e4)),inference(spm,[status(thm)],[12506,2498,theory(equality)])).
% cnf(12526,negated_conjecture,(unit=e1|epred3_0),inference(csr,[status(thm)],[12513,2348])).
% cnf(12528,negated_conjecture,(op(e1,e1)=e1|epred3_0),inference(spm,[status(thm)],[211,12526,theory(equality)])).
% cnf(12537,negated_conjecture,(e4=e1|epred3_0),inference(rw,[status(thm)],[12528,200,theory(equality)])).
% cnf(12538,negated_conjecture,(epred3_0),inference(sr,[status(thm)],[12537,218,theory(equality)])).
% cnf(12590,plain,(op(op(e1,e3),e3)=e1|op(e0,e2)=e1|epred2_0|$false),inference(rw,[status(thm)],[594,12538,theory(equality)])).
% cnf(12591,plain,(op(op(e1,e3),e3)=e1|op(e0,e2)=e1|epred2_0),inference(cn,[status(thm)],[12590,theory(equality)])).
% cnf(12595,negated_conjecture,(op(e2,e3)=e1|op(e0,e2)=e1|epred2_0|unit=e1),inference(spm,[status(thm)],[12591,3317,theory(equality)])).
% cnf(12620,negated_conjecture,(op(e2,e3)=e1|unit=e1|epred2_0),inference(csr,[status(thm)],[12595,2016])).
% cnf(12621,negated_conjecture,(unit=e1|epred2_0),inference(csr,[status(thm)],[12620,2943])).
% cnf(12623,negated_conjecture,(op(e1,e1)=e1|epred2_0),inference(spm,[status(thm)],[211,12621,theory(equality)])).
% cnf(12632,negated_conjecture,(e4=e1|epred2_0),inference(rw,[status(thm)],[12623,200,theory(equality)])).
% cnf(12633,negated_conjecture,(epred2_0),inference(sr,[status(thm)],[12632,218,theory(equality)])).
% cnf(12655,plain,(epred1_0|op(e0,e1)!=op(e1,e0)|op(op(e0,e3),e0)!=e3|op(op(e0,e4),e0)!=e4|$false),inference(rw,[status(thm)],[268,12633,theory(equality)])).
% cnf(12656,plain,(epred1_0|op(e0,e1)!=op(e1,e0)|op(op(e0,e3),e0)!=e3|op(op(e0,e4),e0)!=e4),inference(cn,[status(thm)],[12655,theory(equality)])).
% cnf(12819,negated_conjecture,(epred1_0|unit=e1|e1!=op(e1,e0)|op(op(e0,e3),e0)!=e3|op(op(e0,e4),e0)!=e4),inference(spm,[status(thm)],[12656,1948,theory(equality)])).
% cnf(14585,negated_conjecture,(unit=e1|epred1_0|op(op(e0,e3),e0)!=e3|op(op(e0,e4),e0)!=e4),inference(csr,[status(thm)],[12819,1943])).
% cnf(14593,negated_conjecture,(unit=e1|epred1_0|op(e3,e0)!=e3|op(op(e0,e4),e0)!=e4),inference(spm,[status(thm)],[14585,1950,theory(equality)])).
% cnf(14725,negated_conjecture,(unit=e1|epred1_0|op(op(e0,e4),e0)!=e4),inference(csr,[status(thm)],[14593,1945])).
% cnf(14733,negated_conjecture,(unit=e1|epred1_0|op(e4,e0)!=e4),inference(spm,[status(thm)],[14725,1951,theory(equality)])).
% cnf(14737,negated_conjecture,(unit=e1|epred1_0),inference(csr,[status(thm)],[14733,1946])).
% cnf(14739,negated_conjecture,(op(e1,e1)=e1|epred1_0),inference(spm,[status(thm)],[211,14737,theory(equality)])).
% cnf(14748,negated_conjecture,(e4=e1|epred1_0),inference(rw,[status(thm)],[14739,200,theory(equality)])).
% cnf(14749,negated_conjecture,(epred1_0),inference(sr,[status(thm)],[14748,218,theory(equality)])).
% cnf(14801,plain,(op(op(e0,e1),e1)=e0|op(op(e0,e2),e2)=e0|$false),inference(rw,[status(thm)],[259,14749,theory(equality)])).
% cnf(14802,plain,(op(op(e0,e1),e1)=e0|op(op(e0,e2),e2)=e0),inference(cn,[status(thm)],[14801,theory(equality)])).
% cnf(14804,negated_conjecture,(op(e2,e2)=e0|op(op(e0,e1),e1)=e0|unit=e1),inference(spm,[status(thm)],[14802,1949,theory(equality)])).
% cnf(14812,negated_conjecture,(e3=e0|op(op(e0,e1),e1)=e0|unit=e1),inference(rw,[status(thm)],[14804,471,theory(equality)])).
% cnf(14813,negated_conjecture,(op(op(e0,e1),e1)=e0|unit=e1),inference(sr,[status(thm)],[14812,222,theory(equality)])).
% cnf(14823,negated_conjecture,(op(e1,e1)=e0|unit=e1),inference(spm,[status(thm)],[14813,1948,theory(equality)])).
% cnf(14824,negated_conjecture,(e4=e0|unit=e1),inference(rw,[status(thm)],[14823,200,theory(equality)])).
% cnf(14825,negated_conjecture,(unit=e1),inference(sr,[status(thm)],[14824,221,theory(equality)])).
% cnf(14887,plain,(op(e1,e4)=e4),inference(rw,[status(thm)],[206,14825,theory(equality)])).
% cnf(14888,plain,($false),inference(sr,[status(thm)],[14887,480,theory(equality)])).
% cnf(14889,plain,($false),14888,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 3065
% # ...of these trivial : 28
% # ...subsumed : 1682
% # ...remaining for further processing: 1355
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 103
% # Backward-rewritten : 321
% # Generated clauses : 9651
% # ...of the previous two non-trivial : 9334
% # Contextual simplify-reflections : 1545
% # Paramodulations : 9473
% # Factorizations : 172
% # Equation resolutions : 0
% # Current number of processed clauses: 592
% # Positive orientable unit clauses: 13
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 108
% # Non-unit-clauses : 471
% # Current number of unprocessed clauses: 4097
% # ...number of literals in the above : 29296
% # Clause-clause subsumption calls (NU) : 34472
% # Rec. Clause-clause subsumption calls : 7410
% # Unit Clause-clause subsumption calls : 193
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 8
% # Indexed BW rewrite successes : 8
% # Backwards rewriting index: 42 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-from index: 35 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 40 leaves, 1.00+/-0.000 terms/leaf
% # -------------------------------------------------
% # User time : 0.568 s
% # System time : 0.014 s
% # Total time : 0.582 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.97 CPU 1.08 WC
% FINAL PrfWatch: 0.97 CPU 1.08 WC
% SZS output end Solution for /tmp/SystemOnTPTP5934/ALG064+1.tptp
%
%------------------------------------------------------------------------------