%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : ALG058+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 : art01.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:45:47 EST 2010
% Result : Theorem 3.62s
% Output : Solution 3.62s
% 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/SystemOnTPTP3857/ALG058+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP3857/ALG058+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP3857/ALG058+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 3953
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.045 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 1.92 CPU 2.03 WC
% # 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(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(3, 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(4, 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(5, axiom,(((e0=op(op(op(e2,e2),e2),op(op(e2,e2),e2))&e1=op(op(e2,e2),e2))&e3=op(e2,e2))&e4=op(op(e2,e2),op(e2,e2))),file('/tmp/SRASS.s.p', ax6)).
% 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(e0,e0)=e0&~(e0=unit)))&(~(op(e0,e1)=e0)|(op(e0,e0)=e1&~(e0=unit))))&(~(op(e0,e2)=e0)|(op(e0,e0)=e2&~(e0=unit))))&(~(op(e0,e3)=e0)|(op(e0,e0)=e3&~(e0=unit))))&(~(op(e0,e4)=e0)|(op(e0,e0)=e4&~(e0=unit))))&(~(op(e1,e0)=e0)|(op(e1,e0)=e0&~(e0=unit))))&(~(op(e1,e1)=e0)|(op(e1,e0)=e1&~(e0=unit))))&(~(op(e1,e2)=e0)|(op(e1,e0)=e2&~(e0=unit))))&(~(op(e1,e3)=e0)|(op(e1,e0)=e3&~(e0=unit))))&(~(op(e1,e4)=e0)|(op(e1,e0)=e4&~(e0=unit))))&(~(op(e2,e0)=e0)|(op(e2,e0)=e0&~(e0=unit))))&(~(op(e2,e1)=e0)|(op(e2,e0)=e1&~(e0=unit))))&(~(op(e2,e2)=e0)|(op(e2,e0)=e2&~(e0=unit))))&(~(op(e2,e3)=e0)|(op(e2,e0)=e3&~(e0=unit))))&(~(op(e2,e4)=e0)|(op(e2,e0)=e4&~(e0=unit))))&(~(op(e3,e0)=e0)|(op(e3,e0)=e0&~(e0=unit))))&(~(op(e3,e1)=e0)|(op(e3,e0)=e1&~(e0=unit))))&(~(op(e3,e2)=e0)|(op(e3,e0)=e2&~(e0=unit))))&(~(op(e3,e3)=e0)|(op(e3,e0)=e3&~(e0=unit))))&(~(op(e3,e4)=e0)|(op(e3,e0)=e4&~(e0=unit))))&(~(op(e4,e0)=e0)|(op(e4,e0)=e0&~(e0=unit))))&(~(op(e4,e1)=e0)|(op(e4,e0)=e1&~(e0=unit))))&(~(op(e4,e2)=e0)|(op(e4,e0)=e2&~(e0=unit))))&(~(op(e4,e3)=e0)|(op(e4,e0)=e3&~(e0=unit))))&(~(op(e4,e4)=e0)|(op(e4,e0)=e4&~(e0=unit))))|(((((((((((((((((((((((((~(op(e0,e0)=e1)|(op(e0,e1)=e0&~(e1=unit)))&(~(op(e0,e1)=e1)|(op(e0,e1)=e1&~(e1=unit))))&(~(op(e0,e2)=e1)|(op(e0,e1)=e2&~(e1=unit))))&(~(op(e0,e3)=e1)|(op(e0,e1)=e3&~(e1=unit))))&(~(op(e0,e4)=e1)|(op(e0,e1)=e4&~(e1=unit))))&(~(op(e1,e0)=e1)|(op(e1,e1)=e0&~(e1=unit))))&(~(op(e1,e1)=e1)|(op(e1,e1)=e1&~(e1=unit))))&(~(op(e1,e2)=e1)|(op(e1,e1)=e2&~(e1=unit))))&(~(op(e1,e3)=e1)|(op(e1,e1)=e3&~(e1=unit))))&(~(op(e1,e4)=e1)|(op(e1,e1)=e4&~(e1=unit))))&(~(op(e2,e0)=e1)|(op(e2,e1)=e0&~(e1=unit))))&(~(op(e2,e1)=e1)|(op(e2,e1)=e1&~(e1=unit))))&(~(op(e2,e2)=e1)|(op(e2,e1)=e2&~(e1=unit))))&(~(op(e2,e3)=e1)|(op(e2,e1)=e3&~(e1=unit))))&(~(op(e2,e4)=e1)|(op(e2,e1)=e4&~(e1=unit))))&(~(op(e3,e0)=e1)|(op(e3,e1)=e0&~(e1=unit))))&(~(op(e3,e1)=e1)|(op(e3,e1)=e1&~(e1=unit))))&(~(op(e3,e2)=e1)|(op(e3,e1)=e2&~(e1=unit))))&(~(op(e3,e3)=e1)|(op(e3,e1)=e3&~(e1=unit))))&(~(op(e3,e4)=e1)|(op(e3,e1)=e4&~(e1=unit))))&(~(op(e4,e0)=e1)|(op(e4,e1)=e0&~(e1=unit))))&(~(op(e4,e1)=e1)|(op(e4,e1)=e1&~(e1=unit))))&(~(op(e4,e2)=e1)|(op(e4,e1)=e2&~(e1=unit))))&(~(op(e4,e3)=e1)|(op(e4,e1)=e3&~(e1=unit))))&(~(op(e4,e4)=e1)|(op(e4,e1)=e4&~(e1=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e2)|(op(e0,e2)=e0&~(e2=unit)))&(~(op(e0,e1)=e2)|(op(e0,e2)=e1&~(e2=unit))))&(~(op(e0,e2)=e2)|(op(e0,e2)=e2&~(e2=unit))))&(~(op(e0,e3)=e2)|(op(e0,e2)=e3&~(e2=unit))))&(~(op(e0,e4)=e2)|(op(e0,e2)=e4&~(e2=unit))))&(~(op(e1,e0)=e2)|(op(e1,e2)=e0&~(e2=unit))))&(~(op(e1,e1)=e2)|(op(e1,e2)=e1&~(e2=unit))))&(~(op(e1,e2)=e2)|(op(e1,e2)=e2&~(e2=unit))))&(~(op(e1,e3)=e2)|(op(e1,e2)=e3&~(e2=unit))))&(~(op(e1,e4)=e2)|(op(e1,e2)=e4&~(e2=unit))))&(~(op(e2,e0)=e2)|(op(e2,e2)=e0&~(e2=unit))))&(~(op(e2,e1)=e2)|(op(e2,e2)=e1&~(e2=unit))))&(~(op(e2,e2)=e2)|(op(e2,e2)=e2&~(e2=unit))))&(~(op(e2,e3)=e2)|(op(e2,e2)=e3&~(e2=unit))))&(~(op(e2,e4)=e2)|(op(e2,e2)=e4&~(e2=unit))))&(~(op(e3,e0)=e2)|(op(e3,e2)=e0&~(e2=unit))))&(~(op(e3,e1)=e2)|(op(e3,e2)=e1&~(e2=unit))))&(~(op(e3,e2)=e2)|(op(e3,e2)=e2&~(e2=unit))))&(~(op(e3,e3)=e2)|(op(e3,e2)=e3&~(e2=unit))))&(~(op(e3,e4)=e2)|(op(e3,e2)=e4&~(e2=unit))))&(~(op(e4,e0)=e2)|(op(e4,e2)=e0&~(e2=unit))))&(~(op(e4,e1)=e2)|(op(e4,e2)=e1&~(e2=unit))))&(~(op(e4,e2)=e2)|(op(e4,e2)=e2&~(e2=unit))))&(~(op(e4,e3)=e2)|(op(e4,e2)=e3&~(e2=unit))))&(~(op(e4,e4)=e2)|(op(e4,e2)=e4&~(e2=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e3)|(op(e0,e3)=e0&~(e3=unit)))&(~(op(e0,e1)=e3)|(op(e0,e3)=e1&~(e3=unit))))&(~(op(e0,e2)=e3)|(op(e0,e3)=e2&~(e3=unit))))&(~(op(e0,e3)=e3)|(op(e0,e3)=e3&~(e3=unit))))&(~(op(e0,e4)=e3)|(op(e0,e3)=e4&~(e3=unit))))&(~(op(e1,e0)=e3)|(op(e1,e3)=e0&~(e3=unit))))&(~(op(e1,e1)=e3)|(op(e1,e3)=e1&~(e3=unit))))&(~(op(e1,e2)=e3)|(op(e1,e3)=e2&~(e3=unit))))&(~(op(e1,e3)=e3)|(op(e1,e3)=e3&~(e3=unit))))&(~(op(e1,e4)=e3)|(op(e1,e3)=e4&~(e3=unit))))&(~(op(e2,e0)=e3)|(op(e2,e3)=e0&~(e3=unit))))&(~(op(e2,e1)=e3)|(op(e2,e3)=e1&~(e3=unit))))&(~(op(e2,e2)=e3)|(op(e2,e3)=e2&~(e3=unit))))&(~(op(e2,e3)=e3)|(op(e2,e3)=e3&~(e3=unit))))&(~(op(e2,e4)=e3)|(op(e2,e3)=e4&~(e3=unit))))&(~(op(e3,e0)=e3)|(op(e3,e3)=e0&~(e3=unit))))&(~(op(e3,e1)=e3)|(op(e3,e3)=e1&~(e3=unit))))&(~(op(e3,e2)=e3)|(op(e3,e3)=e2&~(e3=unit))))&(~(op(e3,e3)=e3)|(op(e3,e3)=e3&~(e3=unit))))&(~(op(e3,e4)=e3)|(op(e3,e3)=e4&~(e3=unit))))&(~(op(e4,e0)=e3)|(op(e4,e3)=e0&~(e3=unit))))&(~(op(e4,e1)=e3)|(op(e4,e3)=e1&~(e3=unit))))&(~(op(e4,e2)=e3)|(op(e4,e3)=e2&~(e3=unit))))&(~(op(e4,e3)=e3)|(op(e4,e3)=e3&~(e3=unit))))&(~(op(e4,e4)=e3)|(op(e4,e3)=e4&~(e3=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e4)|(op(e0,e4)=e0&~(e4=unit)))&(~(op(e0,e1)=e4)|(op(e0,e4)=e1&~(e4=unit))))&(~(op(e0,e2)=e4)|(op(e0,e4)=e2&~(e4=unit))))&(~(op(e0,e3)=e4)|(op(e0,e4)=e3&~(e4=unit))))&(~(op(e0,e4)=e4)|(op(e0,e4)=e4&~(e4=unit))))&(~(op(e1,e0)=e4)|(op(e1,e4)=e0&~(e4=unit))))&(~(op(e1,e1)=e4)|(op(e1,e4)=e1&~(e4=unit))))&(~(op(e1,e2)=e4)|(op(e1,e4)=e2&~(e4=unit))))&(~(op(e1,e3)=e4)|(op(e1,e4)=e3&~(e4=unit))))&(~(op(e1,e4)=e4)|(op(e1,e4)=e4&~(e4=unit))))&(~(op(e2,e0)=e4)|(op(e2,e4)=e0&~(e4=unit))))&(~(op(e2,e1)=e4)|(op(e2,e4)=e1&~(e4=unit))))&(~(op(e2,e2)=e4)|(op(e2,e4)=e2&~(e4=unit))))&(~(op(e2,e3)=e4)|(op(e2,e4)=e3&~(e4=unit))))&(~(op(e2,e4)=e4)|(op(e2,e4)=e4&~(e4=unit))))&(~(op(e3,e0)=e4)|(op(e3,e4)=e0&~(e4=unit))))&(~(op(e3,e1)=e4)|(op(e3,e4)=e1&~(e4=unit))))&(~(op(e3,e2)=e4)|(op(e3,e4)=e2&~(e4=unit))))&(~(op(e3,e3)=e4)|(op(e3,e4)=e3&~(e4=unit))))&(~(op(e3,e4)=e4)|(op(e3,e4)=e4&~(e4=unit))))&(~(op(e4,e0)=e4)|(op(e4,e4)=e0&~(e4=unit))))&(~(op(e4,e1)=e4)|(op(e4,e4)=e1&~(e4=unit))))&(~(op(e4,e2)=e4)|(op(e4,e4)=e2&~(e4=unit))))&(~(op(e4,e3)=e4)|(op(e4,e4)=e3&~(e4=unit))))&(~(op(e4,e4)=e4)|(op(e4,e4)=e4&~(e4=unit)))))&((((((((((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|((op(e1,e1)=e1&op(e1,e1)=e1)&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))|((op(e2,e2)=e1&op(e1,e1)=e2)&~(op(e2,e1)=e2)))|((op(e2,e2)=e2&op(e2,e2)=e2)&~(op(e2,e2)=e2)))|((op(e2,e2)=e3&op(e3,e3)=e2)&~(op(e2,e3)=e2)))|((op(e2,e2)=e4&op(e4,e4)=e2)&~(op(e2,e4)=e2)))|((op(e3,e3)=e0&op(e0,e0)=e3)&~(op(e3,e0)=e3)))|((op(e3,e3)=e1&op(e1,e1)=e3)&~(op(e3,e1)=e3)))|((op(e3,e3)=e2&op(e2,e2)=e3)&~(op(e3,e2)=e3)))|((op(e3,e3)=e3&op(e3,e3)=e3)&~(op(e3,e3)=e3)))|((op(e3,e3)=e4&op(e4,e4)=e3)&~(op(e3,e4)=e3)))|((op(e4,e4)=e0&op(e0,e0)=e4)&~(op(e4,e0)=e4)))|((op(e4,e4)=e1&op(e1,e1)=e4)&~(op(e4,e1)=e4)))|((op(e4,e4)=e2&op(e2,e2)=e4)&~(op(e4,e2)=e4)))|((op(e4,e4)=e3&op(e3,e3)=e4)&~(op(e4,e3)=e4)))|((op(e4,e4)=e4&op(e4,e4)=e4)&~(op(e4,e4)=e4))))),file('/tmp/SRASS.s.p', co1)).
% fof(8, negated_conjecture,~(~(((((((((((((((((((((((((((((((~(op(e0,e0)=e0)|(op(e0,e0)=e0&~(e0=unit)))&(~(op(e0,e1)=e0)|(op(e0,e0)=e1&~(e0=unit))))&(~(op(e0,e2)=e0)|(op(e0,e0)=e2&~(e0=unit))))&(~(op(e0,e3)=e0)|(op(e0,e0)=e3&~(e0=unit))))&(~(op(e0,e4)=e0)|(op(e0,e0)=e4&~(e0=unit))))&(~(op(e1,e0)=e0)|(op(e1,e0)=e0&~(e0=unit))))&(~(op(e1,e1)=e0)|(op(e1,e0)=e1&~(e0=unit))))&(~(op(e1,e2)=e0)|(op(e1,e0)=e2&~(e0=unit))))&(~(op(e1,e3)=e0)|(op(e1,e0)=e3&~(e0=unit))))&(~(op(e1,e4)=e0)|(op(e1,e0)=e4&~(e0=unit))))&(~(op(e2,e0)=e0)|(op(e2,e0)=e0&~(e0=unit))))&(~(op(e2,e1)=e0)|(op(e2,e0)=e1&~(e0=unit))))&(~(op(e2,e2)=e0)|(op(e2,e0)=e2&~(e0=unit))))&(~(op(e2,e3)=e0)|(op(e2,e0)=e3&~(e0=unit))))&(~(op(e2,e4)=e0)|(op(e2,e0)=e4&~(e0=unit))))&(~(op(e3,e0)=e0)|(op(e3,e0)=e0&~(e0=unit))))&(~(op(e3,e1)=e0)|(op(e3,e0)=e1&~(e0=unit))))&(~(op(e3,e2)=e0)|(op(e3,e0)=e2&~(e0=unit))))&(~(op(e3,e3)=e0)|(op(e3,e0)=e3&~(e0=unit))))&(~(op(e3,e4)=e0)|(op(e3,e0)=e4&~(e0=unit))))&(~(op(e4,e0)=e0)|(op(e4,e0)=e0&~(e0=unit))))&(~(op(e4,e1)=e0)|(op(e4,e0)=e1&~(e0=unit))))&(~(op(e4,e2)=e0)|(op(e4,e0)=e2&~(e0=unit))))&(~(op(e4,e3)=e0)|(op(e4,e0)=e3&~(e0=unit))))&(~(op(e4,e4)=e0)|(op(e4,e0)=e4&~(e0=unit))))|(((((((((((((((((((((((((~(op(e0,e0)=e1)|(op(e0,e1)=e0&~(e1=unit)))&(~(op(e0,e1)=e1)|(op(e0,e1)=e1&~(e1=unit))))&(~(op(e0,e2)=e1)|(op(e0,e1)=e2&~(e1=unit))))&(~(op(e0,e3)=e1)|(op(e0,e1)=e3&~(e1=unit))))&(~(op(e0,e4)=e1)|(op(e0,e1)=e4&~(e1=unit))))&(~(op(e1,e0)=e1)|(op(e1,e1)=e0&~(e1=unit))))&(~(op(e1,e1)=e1)|(op(e1,e1)=e1&~(e1=unit))))&(~(op(e1,e2)=e1)|(op(e1,e1)=e2&~(e1=unit))))&(~(op(e1,e3)=e1)|(op(e1,e1)=e3&~(e1=unit))))&(~(op(e1,e4)=e1)|(op(e1,e1)=e4&~(e1=unit))))&(~(op(e2,e0)=e1)|(op(e2,e1)=e0&~(e1=unit))))&(~(op(e2,e1)=e1)|(op(e2,e1)=e1&~(e1=unit))))&(~(op(e2,e2)=e1)|(op(e2,e1)=e2&~(e1=unit))))&(~(op(e2,e3)=e1)|(op(e2,e1)=e3&~(e1=unit))))&(~(op(e2,e4)=e1)|(op(e2,e1)=e4&~(e1=unit))))&(~(op(e3,e0)=e1)|(op(e3,e1)=e0&~(e1=unit))))&(~(op(e3,e1)=e1)|(op(e3,e1)=e1&~(e1=unit))))&(~(op(e3,e2)=e1)|(op(e3,e1)=e2&~(e1=unit))))&(~(op(e3,e3)=e1)|(op(e3,e1)=e3&~(e1=unit))))&(~(op(e3,e4)=e1)|(op(e3,e1)=e4&~(e1=unit))))&(~(op(e4,e0)=e1)|(op(e4,e1)=e0&~(e1=unit))))&(~(op(e4,e1)=e1)|(op(e4,e1)=e1&~(e1=unit))))&(~(op(e4,e2)=e1)|(op(e4,e1)=e2&~(e1=unit))))&(~(op(e4,e3)=e1)|(op(e4,e1)=e3&~(e1=unit))))&(~(op(e4,e4)=e1)|(op(e4,e1)=e4&~(e1=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e2)|(op(e0,e2)=e0&~(e2=unit)))&(~(op(e0,e1)=e2)|(op(e0,e2)=e1&~(e2=unit))))&(~(op(e0,e2)=e2)|(op(e0,e2)=e2&~(e2=unit))))&(~(op(e0,e3)=e2)|(op(e0,e2)=e3&~(e2=unit))))&(~(op(e0,e4)=e2)|(op(e0,e2)=e4&~(e2=unit))))&(~(op(e1,e0)=e2)|(op(e1,e2)=e0&~(e2=unit))))&(~(op(e1,e1)=e2)|(op(e1,e2)=e1&~(e2=unit))))&(~(op(e1,e2)=e2)|(op(e1,e2)=e2&~(e2=unit))))&(~(op(e1,e3)=e2)|(op(e1,e2)=e3&~(e2=unit))))&(~(op(e1,e4)=e2)|(op(e1,e2)=e4&~(e2=unit))))&(~(op(e2,e0)=e2)|(op(e2,e2)=e0&~(e2=unit))))&(~(op(e2,e1)=e2)|(op(e2,e2)=e1&~(e2=unit))))&(~(op(e2,e2)=e2)|(op(e2,e2)=e2&~(e2=unit))))&(~(op(e2,e3)=e2)|(op(e2,e2)=e3&~(e2=unit))))&(~(op(e2,e4)=e2)|(op(e2,e2)=e4&~(e2=unit))))&(~(op(e3,e0)=e2)|(op(e3,e2)=e0&~(e2=unit))))&(~(op(e3,e1)=e2)|(op(e3,e2)=e1&~(e2=unit))))&(~(op(e3,e2)=e2)|(op(e3,e2)=e2&~(e2=unit))))&(~(op(e3,e3)=e2)|(op(e3,e2)=e3&~(e2=unit))))&(~(op(e3,e4)=e2)|(op(e3,e2)=e4&~(e2=unit))))&(~(op(e4,e0)=e2)|(op(e4,e2)=e0&~(e2=unit))))&(~(op(e4,e1)=e2)|(op(e4,e2)=e1&~(e2=unit))))&(~(op(e4,e2)=e2)|(op(e4,e2)=e2&~(e2=unit))))&(~(op(e4,e3)=e2)|(op(e4,e2)=e3&~(e2=unit))))&(~(op(e4,e4)=e2)|(op(e4,e2)=e4&~(e2=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e3)|(op(e0,e3)=e0&~(e3=unit)))&(~(op(e0,e1)=e3)|(op(e0,e3)=e1&~(e3=unit))))&(~(op(e0,e2)=e3)|(op(e0,e3)=e2&~(e3=unit))))&(~(op(e0,e3)=e3)|(op(e0,e3)=e3&~(e3=unit))))&(~(op(e0,e4)=e3)|(op(e0,e3)=e4&~(e3=unit))))&(~(op(e1,e0)=e3)|(op(e1,e3)=e0&~(e3=unit))))&(~(op(e1,e1)=e3)|(op(e1,e3)=e1&~(e3=unit))))&(~(op(e1,e2)=e3)|(op(e1,e3)=e2&~(e3=unit))))&(~(op(e1,e3)=e3)|(op(e1,e3)=e3&~(e3=unit))))&(~(op(e1,e4)=e3)|(op(e1,e3)=e4&~(e3=unit))))&(~(op(e2,e0)=e3)|(op(e2,e3)=e0&~(e3=unit))))&(~(op(e2,e1)=e3)|(op(e2,e3)=e1&~(e3=unit))))&(~(op(e2,e2)=e3)|(op(e2,e3)=e2&~(e3=unit))))&(~(op(e2,e3)=e3)|(op(e2,e3)=e3&~(e3=unit))))&(~(op(e2,e4)=e3)|(op(e2,e3)=e4&~(e3=unit))))&(~(op(e3,e0)=e3)|(op(e3,e3)=e0&~(e3=unit))))&(~(op(e3,e1)=e3)|(op(e3,e3)=e1&~(e3=unit))))&(~(op(e3,e2)=e3)|(op(e3,e3)=e2&~(e3=unit))))&(~(op(e3,e3)=e3)|(op(e3,e3)=e3&~(e3=unit))))&(~(op(e3,e4)=e3)|(op(e3,e3)=e4&~(e3=unit))))&(~(op(e4,e0)=e3)|(op(e4,e3)=e0&~(e3=unit))))&(~(op(e4,e1)=e3)|(op(e4,e3)=e1&~(e3=unit))))&(~(op(e4,e2)=e3)|(op(e4,e3)=e2&~(e3=unit))))&(~(op(e4,e3)=e3)|(op(e4,e3)=e3&~(e3=unit))))&(~(op(e4,e4)=e3)|(op(e4,e3)=e4&~(e3=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e4)|(op(e0,e4)=e0&~(e4=unit)))&(~(op(e0,e1)=e4)|(op(e0,e4)=e1&~(e4=unit))))&(~(op(e0,e2)=e4)|(op(e0,e4)=e2&~(e4=unit))))&(~(op(e0,e3)=e4)|(op(e0,e4)=e3&~(e4=unit))))&(~(op(e0,e4)=e4)|(op(e0,e4)=e4&~(e4=unit))))&(~(op(e1,e0)=e4)|(op(e1,e4)=e0&~(e4=unit))))&(~(op(e1,e1)=e4)|(op(e1,e4)=e1&~(e4=unit))))&(~(op(e1,e2)=e4)|(op(e1,e4)=e2&~(e4=unit))))&(~(op(e1,e3)=e4)|(op(e1,e4)=e3&~(e4=unit))))&(~(op(e1,e4)=e4)|(op(e1,e4)=e4&~(e4=unit))))&(~(op(e2,e0)=e4)|(op(e2,e4)=e0&~(e4=unit))))&(~(op(e2,e1)=e4)|(op(e2,e4)=e1&~(e4=unit))))&(~(op(e2,e2)=e4)|(op(e2,e4)=e2&~(e4=unit))))&(~(op(e2,e3)=e4)|(op(e2,e4)=e3&~(e4=unit))))&(~(op(e2,e4)=e4)|(op(e2,e4)=e4&~(e4=unit))))&(~(op(e3,e0)=e4)|(op(e3,e4)=e0&~(e4=unit))))&(~(op(e3,e1)=e4)|(op(e3,e4)=e1&~(e4=unit))))&(~(op(e3,e2)=e4)|(op(e3,e4)=e2&~(e4=unit))))&(~(op(e3,e3)=e4)|(op(e3,e4)=e3&~(e4=unit))))&(~(op(e3,e4)=e4)|(op(e3,e4)=e4&~(e4=unit))))&(~(op(e4,e0)=e4)|(op(e4,e4)=e0&~(e4=unit))))&(~(op(e4,e1)=e4)|(op(e4,e4)=e1&~(e4=unit))))&(~(op(e4,e2)=e4)|(op(e4,e4)=e2&~(e4=unit))))&(~(op(e4,e3)=e4)|(op(e4,e4)=e3&~(e4=unit))))&(~(op(e4,e4)=e4)|(op(e4,e4)=e4&~(e4=unit)))))&((((((((((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|((op(e1,e1)=e1&op(e1,e1)=e1)&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))|((op(e2,e2)=e1&op(e1,e1)=e2)&~(op(e2,e1)=e2)))|((op(e2,e2)=e2&op(e2,e2)=e2)&~(op(e2,e2)=e2)))|((op(e2,e2)=e3&op(e3,e3)=e2)&~(op(e2,e3)=e2)))|((op(e2,e2)=e4&op(e4,e4)=e2)&~(op(e2,e4)=e2)))|((op(e3,e3)=e0&op(e0,e0)=e3)&~(op(e3,e0)=e3)))|((op(e3,e3)=e1&op(e1,e1)=e3)&~(op(e3,e1)=e3)))|((op(e3,e3)=e2&op(e2,e2)=e3)&~(op(e3,e2)=e3)))|((op(e3,e3)=e3&op(e3,e3)=e3)&~(op(e3,e3)=e3)))|((op(e3,e3)=e4&op(e4,e4)=e3)&~(op(e3,e4)=e3)))|((op(e4,e4)=e0&op(e0,e0)=e4)&~(op(e4,e0)=e4)))|((op(e4,e4)=e1&op(e1,e1)=e4)&~(op(e4,e1)=e4)))|((op(e4,e4)=e2&op(e2,e2)=e4)&~(op(e4,e2)=e4)))|((op(e4,e4)=e3&op(e3,e3)=e4)&~(op(e4,e3)=e4)))|((op(e4,e4)=e4&op(e4,e4)=e4)&~(op(e4,e4)=e4)))))),inference(assume_negation,[status(cth)],[7])).
% fof(9, negated_conjecture,~(~(((((((((((((((((((((((((((((((~(op(e0,e0)=e0)|(op(e0,e0)=e0&~(e0=unit)))&(~(op(e0,e1)=e0)|(op(e0,e0)=e1&~(e0=unit))))&(~(op(e0,e2)=e0)|(op(e0,e0)=e2&~(e0=unit))))&(~(op(e0,e3)=e0)|(op(e0,e0)=e3&~(e0=unit))))&(~(op(e0,e4)=e0)|(op(e0,e0)=e4&~(e0=unit))))&(~(op(e1,e0)=e0)|(op(e1,e0)=e0&~(e0=unit))))&(~(op(e1,e1)=e0)|(op(e1,e0)=e1&~(e0=unit))))&(~(op(e1,e2)=e0)|(op(e1,e0)=e2&~(e0=unit))))&(~(op(e1,e3)=e0)|(op(e1,e0)=e3&~(e0=unit))))&(~(op(e1,e4)=e0)|(op(e1,e0)=e4&~(e0=unit))))&(~(op(e2,e0)=e0)|(op(e2,e0)=e0&~(e0=unit))))&(~(op(e2,e1)=e0)|(op(e2,e0)=e1&~(e0=unit))))&(~(op(e2,e2)=e0)|(op(e2,e0)=e2&~(e0=unit))))&(~(op(e2,e3)=e0)|(op(e2,e0)=e3&~(e0=unit))))&(~(op(e2,e4)=e0)|(op(e2,e0)=e4&~(e0=unit))))&(~(op(e3,e0)=e0)|(op(e3,e0)=e0&~(e0=unit))))&(~(op(e3,e1)=e0)|(op(e3,e0)=e1&~(e0=unit))))&(~(op(e3,e2)=e0)|(op(e3,e0)=e2&~(e0=unit))))&(~(op(e3,e3)=e0)|(op(e3,e0)=e3&~(e0=unit))))&(~(op(e3,e4)=e0)|(op(e3,e0)=e4&~(e0=unit))))&(~(op(e4,e0)=e0)|(op(e4,e0)=e0&~(e0=unit))))&(~(op(e4,e1)=e0)|(op(e4,e0)=e1&~(e0=unit))))&(~(op(e4,e2)=e0)|(op(e4,e0)=e2&~(e0=unit))))&(~(op(e4,e3)=e0)|(op(e4,e0)=e3&~(e0=unit))))&(~(op(e4,e4)=e0)|(op(e4,e0)=e4&~(e0=unit))))|(((((((((((((((((((((((((~(op(e0,e0)=e1)|(op(e0,e1)=e0&~(e1=unit)))&(~(op(e0,e1)=e1)|(op(e0,e1)=e1&~(e1=unit))))&(~(op(e0,e2)=e1)|(op(e0,e1)=e2&~(e1=unit))))&(~(op(e0,e3)=e1)|(op(e0,e1)=e3&~(e1=unit))))&(~(op(e0,e4)=e1)|(op(e0,e1)=e4&~(e1=unit))))&(~(op(e1,e0)=e1)|(op(e1,e1)=e0&~(e1=unit))))&(~(op(e1,e1)=e1)|(op(e1,e1)=e1&~(e1=unit))))&(~(op(e1,e2)=e1)|(op(e1,e1)=e2&~(e1=unit))))&(~(op(e1,e3)=e1)|(op(e1,e1)=e3&~(e1=unit))))&(~(op(e1,e4)=e1)|(op(e1,e1)=e4&~(e1=unit))))&(~(op(e2,e0)=e1)|(op(e2,e1)=e0&~(e1=unit))))&(~(op(e2,e1)=e1)|(op(e2,e1)=e1&~(e1=unit))))&(~(op(e2,e2)=e1)|(op(e2,e1)=e2&~(e1=unit))))&(~(op(e2,e3)=e1)|(op(e2,e1)=e3&~(e1=unit))))&(~(op(e2,e4)=e1)|(op(e2,e1)=e4&~(e1=unit))))&(~(op(e3,e0)=e1)|(op(e3,e1)=e0&~(e1=unit))))&(~(op(e3,e1)=e1)|(op(e3,e1)=e1&~(e1=unit))))&(~(op(e3,e2)=e1)|(op(e3,e1)=e2&~(e1=unit))))&(~(op(e3,e3)=e1)|(op(e3,e1)=e3&~(e1=unit))))&(~(op(e3,e4)=e1)|(op(e3,e1)=e4&~(e1=unit))))&(~(op(e4,e0)=e1)|(op(e4,e1)=e0&~(e1=unit))))&(~(op(e4,e1)=e1)|(op(e4,e1)=e1&~(e1=unit))))&(~(op(e4,e2)=e1)|(op(e4,e1)=e2&~(e1=unit))))&(~(op(e4,e3)=e1)|(op(e4,e1)=e3&~(e1=unit))))&(~(op(e4,e4)=e1)|(op(e4,e1)=e4&~(e1=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e2)|(op(e0,e2)=e0&~(e2=unit)))&(~(op(e0,e1)=e2)|(op(e0,e2)=e1&~(e2=unit))))&(~(op(e0,e2)=e2)|(op(e0,e2)=e2&~(e2=unit))))&(~(op(e0,e3)=e2)|(op(e0,e2)=e3&~(e2=unit))))&(~(op(e0,e4)=e2)|(op(e0,e2)=e4&~(e2=unit))))&(~(op(e1,e0)=e2)|(op(e1,e2)=e0&~(e2=unit))))&(~(op(e1,e1)=e2)|(op(e1,e2)=e1&~(e2=unit))))&(~(op(e1,e2)=e2)|(op(e1,e2)=e2&~(e2=unit))))&(~(op(e1,e3)=e2)|(op(e1,e2)=e3&~(e2=unit))))&(~(op(e1,e4)=e2)|(op(e1,e2)=e4&~(e2=unit))))&(~(op(e2,e0)=e2)|(op(e2,e2)=e0&~(e2=unit))))&(~(op(e2,e1)=e2)|(op(e2,e2)=e1&~(e2=unit))))&(~(op(e2,e2)=e2)|(op(e2,e2)=e2&~(e2=unit))))&(~(op(e2,e3)=e2)|(op(e2,e2)=e3&~(e2=unit))))&(~(op(e2,e4)=e2)|(op(e2,e2)=e4&~(e2=unit))))&(~(op(e3,e0)=e2)|(op(e3,e2)=e0&~(e2=unit))))&(~(op(e3,e1)=e2)|(op(e3,e2)=e1&~(e2=unit))))&(~(op(e3,e2)=e2)|(op(e3,e2)=e2&~(e2=unit))))&(~(op(e3,e3)=e2)|(op(e3,e2)=e3&~(e2=unit))))&(~(op(e3,e4)=e2)|(op(e3,e2)=e4&~(e2=unit))))&(~(op(e4,e0)=e2)|(op(e4,e2)=e0&~(e2=unit))))&(~(op(e4,e1)=e2)|(op(e4,e2)=e1&~(e2=unit))))&(~(op(e4,e2)=e2)|(op(e4,e2)=e2&~(e2=unit))))&(~(op(e4,e3)=e2)|(op(e4,e2)=e3&~(e2=unit))))&(~(op(e4,e4)=e2)|(op(e4,e2)=e4&~(e2=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e3)|(op(e0,e3)=e0&~(e3=unit)))&(~(op(e0,e1)=e3)|(op(e0,e3)=e1&~(e3=unit))))&(~(op(e0,e2)=e3)|(op(e0,e3)=e2&~(e3=unit))))&(~(op(e0,e3)=e3)|(op(e0,e3)=e3&~(e3=unit))))&(~(op(e0,e4)=e3)|(op(e0,e3)=e4&~(e3=unit))))&(~(op(e1,e0)=e3)|(op(e1,e3)=e0&~(e3=unit))))&(~(op(e1,e1)=e3)|(op(e1,e3)=e1&~(e3=unit))))&(~(op(e1,e2)=e3)|(op(e1,e3)=e2&~(e3=unit))))&(~(op(e1,e3)=e3)|(op(e1,e3)=e3&~(e3=unit))))&(~(op(e1,e4)=e3)|(op(e1,e3)=e4&~(e3=unit))))&(~(op(e2,e0)=e3)|(op(e2,e3)=e0&~(e3=unit))))&(~(op(e2,e1)=e3)|(op(e2,e3)=e1&~(e3=unit))))&(~(op(e2,e2)=e3)|(op(e2,e3)=e2&~(e3=unit))))&(~(op(e2,e3)=e3)|(op(e2,e3)=e3&~(e3=unit))))&(~(op(e2,e4)=e3)|(op(e2,e3)=e4&~(e3=unit))))&(~(op(e3,e0)=e3)|(op(e3,e3)=e0&~(e3=unit))))&(~(op(e3,e1)=e3)|(op(e3,e3)=e1&~(e3=unit))))&(~(op(e3,e2)=e3)|(op(e3,e3)=e2&~(e3=unit))))&(~(op(e3,e3)=e3)|(op(e3,e3)=e3&~(e3=unit))))&(~(op(e3,e4)=e3)|(op(e3,e3)=e4&~(e3=unit))))&(~(op(e4,e0)=e3)|(op(e4,e3)=e0&~(e3=unit))))&(~(op(e4,e1)=e3)|(op(e4,e3)=e1&~(e3=unit))))&(~(op(e4,e2)=e3)|(op(e4,e3)=e2&~(e3=unit))))&(~(op(e4,e3)=e3)|(op(e4,e3)=e3&~(e3=unit))))&(~(op(e4,e4)=e3)|(op(e4,e3)=e4&~(e3=unit)))))|(((((((((((((((((((((((((~(op(e0,e0)=e4)|(op(e0,e4)=e0&~(e4=unit)))&(~(op(e0,e1)=e4)|(op(e0,e4)=e1&~(e4=unit))))&(~(op(e0,e2)=e4)|(op(e0,e4)=e2&~(e4=unit))))&(~(op(e0,e3)=e4)|(op(e0,e4)=e3&~(e4=unit))))&(~(op(e0,e4)=e4)|(op(e0,e4)=e4&~(e4=unit))))&(~(op(e1,e0)=e4)|(op(e1,e4)=e0&~(e4=unit))))&(~(op(e1,e1)=e4)|(op(e1,e4)=e1&~(e4=unit))))&(~(op(e1,e2)=e4)|(op(e1,e4)=e2&~(e4=unit))))&(~(op(e1,e3)=e4)|(op(e1,e4)=e3&~(e4=unit))))&(~(op(e1,e4)=e4)|(op(e1,e4)=e4&~(e4=unit))))&(~(op(e2,e0)=e4)|(op(e2,e4)=e0&~(e4=unit))))&(~(op(e2,e1)=e4)|(op(e2,e4)=e1&~(e4=unit))))&(~(op(e2,e2)=e4)|(op(e2,e4)=e2&~(e4=unit))))&(~(op(e2,e3)=e4)|(op(e2,e4)=e3&~(e4=unit))))&(~(op(e2,e4)=e4)|(op(e2,e4)=e4&~(e4=unit))))&(~(op(e3,e0)=e4)|(op(e3,e4)=e0&~(e4=unit))))&(~(op(e3,e1)=e4)|(op(e3,e4)=e1&~(e4=unit))))&(~(op(e3,e2)=e4)|(op(e3,e4)=e2&~(e4=unit))))&(~(op(e3,e3)=e4)|(op(e3,e4)=e3&~(e4=unit))))&(~(op(e3,e4)=e4)|(op(e3,e4)=e4&~(e4=unit))))&(~(op(e4,e0)=e4)|(op(e4,e4)=e0&~(e4=unit))))&(~(op(e4,e1)=e4)|(op(e4,e4)=e1&~(e4=unit))))&(~(op(e4,e2)=e4)|(op(e4,e4)=e2&~(e4=unit))))&(~(op(e4,e3)=e4)|(op(e4,e4)=e3&~(e4=unit))))&(~(op(e4,e4)=e4)|(op(e4,e4)=e4&~(e4=unit)))))&(((((((((((((((((((((((((op(e0,e0)=e0&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|(op(e1,e1)=e1&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))|((op(e2,e2)=e1&op(e1,e1)=e2)&~(op(e2,e1)=e2)))|(op(e2,e2)=e2&~(op(e2,e2)=e2)))|((op(e2,e2)=e3&op(e3,e3)=e2)&~(op(e2,e3)=e2)))|((op(e2,e2)=e4&op(e4,e4)=e2)&~(op(e2,e4)=e2)))|((op(e3,e3)=e0&op(e0,e0)=e3)&~(op(e3,e0)=e3)))|((op(e3,e3)=e1&op(e1,e1)=e3)&~(op(e3,e1)=e3)))|((op(e3,e3)=e2&op(e2,e2)=e3)&~(op(e3,e2)=e3)))|(op(e3,e3)=e3&~(op(e3,e3)=e3)))|((op(e3,e3)=e4&op(e4,e4)=e3)&~(op(e3,e4)=e3)))|((op(e4,e4)=e0&op(e0,e0)=e4)&~(op(e4,e0)=e4)))|((op(e4,e4)=e1&op(e1,e1)=e4)&~(op(e4,e1)=e4)))|((op(e4,e4)=e2&op(e2,e2)=e4)&~(op(e4,e2)=e4)))|((op(e4,e4)=e3&op(e3,e3)=e4)&~(op(e4,e3)=e4)))|(op(e4,e4)=e4&~(op(e4,e4)=e4)))))),inference(fof_simplification,[status(thm)],[8,theory(equality)])).
% fof(10, plain,(epred1_0=>(((((((((((((((((((((((((~(op(e0,e0)=e0)|(op(e0,e0)=e0&~(e0=unit)))&(~(op(e0,e1)=e0)|(op(e0,e0)=e1&~(e0=unit))))&(~(op(e0,e2)=e0)|(op(e0,e0)=e2&~(e0=unit))))&(~(op(e0,e3)=e0)|(op(e0,e0)=e3&~(e0=unit))))&(~(op(e0,e4)=e0)|(op(e0,e0)=e4&~(e0=unit))))&(~(op(e1,e0)=e0)|(op(e1,e0)=e0&~(e0=unit))))&(~(op(e1,e1)=e0)|(op(e1,e0)=e1&~(e0=unit))))&(~(op(e1,e2)=e0)|(op(e1,e0)=e2&~(e0=unit))))&(~(op(e1,e3)=e0)|(op(e1,e0)=e3&~(e0=unit))))&(~(op(e1,e4)=e0)|(op(e1,e0)=e4&~(e0=unit))))&(~(op(e2,e0)=e0)|(op(e2,e0)=e0&~(e0=unit))))&(~(op(e2,e1)=e0)|(op(e2,e0)=e1&~(e0=unit))))&(~(op(e2,e2)=e0)|(op(e2,e0)=e2&~(e0=unit))))&(~(op(e2,e3)=e0)|(op(e2,e0)=e3&~(e0=unit))))&(~(op(e2,e4)=e0)|(op(e2,e0)=e4&~(e0=unit))))&(~(op(e3,e0)=e0)|(op(e3,e0)=e0&~(e0=unit))))&(~(op(e3,e1)=e0)|(op(e3,e0)=e1&~(e0=unit))))&(~(op(e3,e2)=e0)|(op(e3,e0)=e2&~(e0=unit))))&(~(op(e3,e3)=e0)|(op(e3,e0)=e3&~(e0=unit))))&(~(op(e3,e4)=e0)|(op(e3,e0)=e4&~(e0=unit))))&(~(op(e4,e0)=e0)|(op(e4,e0)=e0&~(e0=unit))))&(~(op(e4,e1)=e0)|(op(e4,e0)=e1&~(e0=unit))))&(~(op(e4,e2)=e0)|(op(e4,e0)=e2&~(e0=unit))))&(~(op(e4,e3)=e0)|(op(e4,e0)=e3&~(e0=unit))))&(~(op(e4,e4)=e0)|(op(e4,e0)=e4&~(e0=unit))))),introduced(definition)).
% fof(11, plain,(epred2_0=>(((((((((((((((((((((((((~(op(e0,e0)=e1)|(op(e0,e1)=e0&~(e1=unit)))&(~(op(e0,e1)=e1)|(op(e0,e1)=e1&~(e1=unit))))&(~(op(e0,e2)=e1)|(op(e0,e1)=e2&~(e1=unit))))&(~(op(e0,e3)=e1)|(op(e0,e1)=e3&~(e1=unit))))&(~(op(e0,e4)=e1)|(op(e0,e1)=e4&~(e1=unit))))&(~(op(e1,e0)=e1)|(op(e1,e1)=e0&~(e1=unit))))&(~(op(e1,e1)=e1)|(op(e1,e1)=e1&~(e1=unit))))&(~(op(e1,e2)=e1)|(op(e1,e1)=e2&~(e1=unit))))&(~(op(e1,e3)=e1)|(op(e1,e1)=e3&~(e1=unit))))&(~(op(e1,e4)=e1)|(op(e1,e1)=e4&~(e1=unit))))&(~(op(e2,e0)=e1)|(op(e2,e1)=e0&~(e1=unit))))&(~(op(e2,e1)=e1)|(op(e2,e1)=e1&~(e1=unit))))&(~(op(e2,e2)=e1)|(op(e2,e1)=e2&~(e1=unit))))&(~(op(e2,e3)=e1)|(op(e2,e1)=e3&~(e1=unit))))&(~(op(e2,e4)=e1)|(op(e2,e1)=e4&~(e1=unit))))&(~(op(e3,e0)=e1)|(op(e3,e1)=e0&~(e1=unit))))&(~(op(e3,e1)=e1)|(op(e3,e1)=e1&~(e1=unit))))&(~(op(e3,e2)=e1)|(op(e3,e1)=e2&~(e1=unit))))&(~(op(e3,e3)=e1)|(op(e3,e1)=e3&~(e1=unit))))&(~(op(e3,e4)=e1)|(op(e3,e1)=e4&~(e1=unit))))&(~(op(e4,e0)=e1)|(op(e4,e1)=e0&~(e1=unit))))&(~(op(e4,e1)=e1)|(op(e4,e1)=e1&~(e1=unit))))&(~(op(e4,e2)=e1)|(op(e4,e1)=e2&~(e1=unit))))&(~(op(e4,e3)=e1)|(op(e4,e1)=e3&~(e1=unit))))&(~(op(e4,e4)=e1)|(op(e4,e1)=e4&~(e1=unit))))),introduced(definition)).
% fof(12, plain,(epred3_0=>(((((((((((((((((((((((((~(op(e0,e0)=e2)|(op(e0,e2)=e0&~(e2=unit)))&(~(op(e0,e1)=e2)|(op(e0,e2)=e1&~(e2=unit))))&(~(op(e0,e2)=e2)|(op(e0,e2)=e2&~(e2=unit))))&(~(op(e0,e3)=e2)|(op(e0,e2)=e3&~(e2=unit))))&(~(op(e0,e4)=e2)|(op(e0,e2)=e4&~(e2=unit))))&(~(op(e1,e0)=e2)|(op(e1,e2)=e0&~(e2=unit))))&(~(op(e1,e1)=e2)|(op(e1,e2)=e1&~(e2=unit))))&(~(op(e1,e2)=e2)|(op(e1,e2)=e2&~(e2=unit))))&(~(op(e1,e3)=e2)|(op(e1,e2)=e3&~(e2=unit))))&(~(op(e1,e4)=e2)|(op(e1,e2)=e4&~(e2=unit))))&(~(op(e2,e0)=e2)|(op(e2,e2)=e0&~(e2=unit))))&(~(op(e2,e1)=e2)|(op(e2,e2)=e1&~(e2=unit))))&(~(op(e2,e2)=e2)|(op(e2,e2)=e2&~(e2=unit))))&(~(op(e2,e3)=e2)|(op(e2,e2)=e3&~(e2=unit))))&(~(op(e2,e4)=e2)|(op(e2,e2)=e4&~(e2=unit))))&(~(op(e3,e0)=e2)|(op(e3,e2)=e0&~(e2=unit))))&(~(op(e3,e1)=e2)|(op(e3,e2)=e1&~(e2=unit))))&(~(op(e3,e2)=e2)|(op(e3,e2)=e2&~(e2=unit))))&(~(op(e3,e3)=e2)|(op(e3,e2)=e3&~(e2=unit))))&(~(op(e3,e4)=e2)|(op(e3,e2)=e4&~(e2=unit))))&(~(op(e4,e0)=e2)|(op(e4,e2)=e0&~(e2=unit))))&(~(op(e4,e1)=e2)|(op(e4,e2)=e1&~(e2=unit))))&(~(op(e4,e2)=e2)|(op(e4,e2)=e2&~(e2=unit))))&(~(op(e4,e3)=e2)|(op(e4,e2)=e3&~(e2=unit))))&(~(op(e4,e4)=e2)|(op(e4,e2)=e4&~(e2=unit))))),introduced(definition)).
% fof(13, plain,(epred4_0=>(((((((((((((((((((((((((~(op(e0,e0)=e3)|(op(e0,e3)=e0&~(e3=unit)))&(~(op(e0,e1)=e3)|(op(e0,e3)=e1&~(e3=unit))))&(~(op(e0,e2)=e3)|(op(e0,e3)=e2&~(e3=unit))))&(~(op(e0,e3)=e3)|(op(e0,e3)=e3&~(e3=unit))))&(~(op(e0,e4)=e3)|(op(e0,e3)=e4&~(e3=unit))))&(~(op(e1,e0)=e3)|(op(e1,e3)=e0&~(e3=unit))))&(~(op(e1,e1)=e3)|(op(e1,e3)=e1&~(e3=unit))))&(~(op(e1,e2)=e3)|(op(e1,e3)=e2&~(e3=unit))))&(~(op(e1,e3)=e3)|(op(e1,e3)=e3&~(e3=unit))))&(~(op(e1,e4)=e3)|(op(e1,e3)=e4&~(e3=unit))))&(~(op(e2,e0)=e3)|(op(e2,e3)=e0&~(e3=unit))))&(~(op(e2,e1)=e3)|(op(e2,e3)=e1&~(e3=unit))))&(~(op(e2,e2)=e3)|(op(e2,e3)=e2&~(e3=unit))))&(~(op(e2,e3)=e3)|(op(e2,e3)=e3&~(e3=unit))))&(~(op(e2,e4)=e3)|(op(e2,e3)=e4&~(e3=unit))))&(~(op(e3,e0)=e3)|(op(e3,e3)=e0&~(e3=unit))))&(~(op(e3,e1)=e3)|(op(e3,e3)=e1&~(e3=unit))))&(~(op(e3,e2)=e3)|(op(e3,e3)=e2&~(e3=unit))))&(~(op(e3,e3)=e3)|(op(e3,e3)=e3&~(e3=unit))))&(~(op(e3,e4)=e3)|(op(e3,e3)=e4&~(e3=unit))))&(~(op(e4,e0)=e3)|(op(e4,e3)=e0&~(e3=unit))))&(~(op(e4,e1)=e3)|(op(e4,e3)=e1&~(e3=unit))))&(~(op(e4,e2)=e3)|(op(e4,e3)=e2&~(e3=unit))))&(~(op(e4,e3)=e3)|(op(e4,e3)=e3&~(e3=unit))))&(~(op(e4,e4)=e3)|(op(e4,e3)=e4&~(e3=unit))))),introduced(definition)).
% fof(14, plain,(epred5_0=>(((((((((((((((((((((((((~(op(e0,e0)=e4)|(op(e0,e4)=e0&~(e4=unit)))&(~(op(e0,e1)=e4)|(op(e0,e4)=e1&~(e4=unit))))&(~(op(e0,e2)=e4)|(op(e0,e4)=e2&~(e4=unit))))&(~(op(e0,e3)=e4)|(op(e0,e4)=e3&~(e4=unit))))&(~(op(e0,e4)=e4)|(op(e0,e4)=e4&~(e4=unit))))&(~(op(e1,e0)=e4)|(op(e1,e4)=e0&~(e4=unit))))&(~(op(e1,e1)=e4)|(op(e1,e4)=e1&~(e4=unit))))&(~(op(e1,e2)=e4)|(op(e1,e4)=e2&~(e4=unit))))&(~(op(e1,e3)=e4)|(op(e1,e4)=e3&~(e4=unit))))&(~(op(e1,e4)=e4)|(op(e1,e4)=e4&~(e4=unit))))&(~(op(e2,e0)=e4)|(op(e2,e4)=e0&~(e4=unit))))&(~(op(e2,e1)=e4)|(op(e2,e4)=e1&~(e4=unit))))&(~(op(e2,e2)=e4)|(op(e2,e4)=e2&~(e4=unit))))&(~(op(e2,e3)=e4)|(op(e2,e4)=e3&~(e4=unit))))&(~(op(e2,e4)=e4)|(op(e2,e4)=e4&~(e4=unit))))&(~(op(e3,e0)=e4)|(op(e3,e4)=e0&~(e4=unit))))&(~(op(e3,e1)=e4)|(op(e3,e4)=e1&~(e4=unit))))&(~(op(e3,e2)=e4)|(op(e3,e4)=e2&~(e4=unit))))&(~(op(e3,e3)=e4)|(op(e3,e4)=e3&~(e4=unit))))&(~(op(e3,e4)=e4)|(op(e3,e4)=e4&~(e4=unit))))&(~(op(e4,e0)=e4)|(op(e4,e4)=e0&~(e4=unit))))&(~(op(e4,e1)=e4)|(op(e4,e4)=e1&~(e4=unit))))&(~(op(e4,e2)=e4)|(op(e4,e4)=e2&~(e4=unit))))&(~(op(e4,e3)=e4)|(op(e4,e4)=e3&~(e4=unit))))&(~(op(e4,e4)=e4)|(op(e4,e4)=e4&~(e4=unit))))),introduced(definition)).
% fof(15, plain,(epred6_0=>((((op(e0,e0)=e0&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))),introduced(definition)).
% fof(16, plain,(epred7_0=>((((((((op(e0,e0)=e0&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|(op(e1,e1)=e1&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))),introduced(definition)).
% fof(17, plain,(epred8_0=>(((((((((((op(e0,e0)=e0&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|(op(e1,e1)=e1&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))),introduced(definition)).
% fof(18, plain,(epred9_0=>(((((((((((((((op(e0,e0)=e0&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|(op(e1,e1)=e1&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))|((op(e2,e2)=e1&op(e1,e1)=e2)&~(op(e2,e1)=e2)))|(op(e2,e2)=e2&~(op(e2,e2)=e2)))|((op(e2,e2)=e3&op(e3,e3)=e2)&~(op(e2,e3)=e2)))|((op(e2,e2)=e4&op(e4,e4)=e2)&~(op(e2,e4)=e2)))),introduced(definition)).
% fof(19, plain,(epred10_0=>((((((((((((((((((op(e0,e0)=e0&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|(op(e1,e1)=e1&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))|((op(e2,e2)=e1&op(e1,e1)=e2)&~(op(e2,e1)=e2)))|(op(e2,e2)=e2&~(op(e2,e2)=e2)))|((op(e2,e2)=e3&op(e3,e3)=e2)&~(op(e2,e3)=e2)))|((op(e2,e2)=e4&op(e4,e4)=e2)&~(op(e2,e4)=e2)))|((op(e3,e3)=e0&op(e0,e0)=e3)&~(op(e3,e0)=e3)))|((op(e3,e3)=e1&op(e1,e1)=e3)&~(op(e3,e1)=e3)))|((op(e3,e3)=e2&op(e2,e2)=e3)&~(op(e3,e2)=e3)))),introduced(definition)).
% fof(20, plain,(epred11_0=>((((((((((((((((((((((op(e0,e0)=e0&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|(op(e1,e1)=e1&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))|((op(e2,e2)=e1&op(e1,e1)=e2)&~(op(e2,e1)=e2)))|(op(e2,e2)=e2&~(op(e2,e2)=e2)))|((op(e2,e2)=e3&op(e3,e3)=e2)&~(op(e2,e3)=e2)))|((op(e2,e2)=e4&op(e4,e4)=e2)&~(op(e2,e4)=e2)))|((op(e3,e3)=e0&op(e0,e0)=e3)&~(op(e3,e0)=e3)))|((op(e3,e3)=e1&op(e1,e1)=e3)&~(op(e3,e1)=e3)))|((op(e3,e3)=e2&op(e2,e2)=e3)&~(op(e3,e2)=e3)))|(op(e3,e3)=e3&~(op(e3,e3)=e3)))|((op(e3,e3)=e4&op(e4,e4)=e3)&~(op(e3,e4)=e3)))|((op(e4,e4)=e0&op(e0,e0)=e4)&~(op(e4,e0)=e4)))|((op(e4,e4)=e1&op(e1,e1)=e4)&~(op(e4,e1)=e4)))),introduced(definition)).
% fof(21, negated_conjecture,~(~((((((epred1_0|epred2_0)|epred3_0)|epred4_0)|epred5_0)&(((epred11_0|((op(e4,e4)=e2&op(e2,e2)=e4)&~(op(e4,e2)=e4)))|((op(e4,e4)=e3&op(e3,e3)=e4)&~(op(e4,e3)=e4)))|(op(e4,e4)=e4&~(op(e4,e4)=e4)))))),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[9,10,theory(equality)]),11,theory(equality)]),12,theory(equality)]),13,theory(equality)]),14,theory(equality)]),20,theory(equality)])).
% fof(22, plain,(epred7_0=>((((epred6_0|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|(op(e1,e1)=e1&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))),inference(apply_def,[status(esa)],[16,15,theory(equality)])).
% fof(23, plain,(epred8_0=>(((epred7_0|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))),inference(apply_def,[status(esa)],[17,22,theory(equality)])).
% fof(24, plain,(epred9_0=>((((epred8_0|((op(e2,e2)=e1&op(e1,e1)=e2)&~(op(e2,e1)=e2)))|(op(e2,e2)=e2&~(op(e2,e2)=e2)))|((op(e2,e2)=e3&op(e3,e3)=e2)&~(op(e2,e3)=e2)))|((op(e2,e2)=e4&op(e4,e4)=e2)&~(op(e2,e4)=e2)))),inference(apply_def,[status(esa)],[18,23,theory(equality)])).
% fof(25, plain,(epred10_0=>(((epred9_0|((op(e3,e3)=e0&op(e0,e0)=e3)&~(op(e3,e0)=e3)))|((op(e3,e3)=e1&op(e1,e1)=e3)&~(op(e3,e1)=e3)))|((op(e3,e3)=e2&op(e2,e2)=e3)&~(op(e3,e2)=e3)))),inference(apply_def,[status(esa)],[19,24,theory(equality)])).
% fof(26, plain,(epred11_0=>((((epred10_0|(op(e3,e3)=e3&~(op(e3,e3)=e3)))|((op(e3,e3)=e4&op(e4,e4)=e3)&~(op(e3,e4)=e3)))|((op(e4,e4)=e0&op(e0,e0)=e4)&~(op(e4,e0)=e4)))|((op(e4,e4)=e1&op(e1,e1)=e4)&~(op(e4,e1)=e4)))),inference(apply_def,[status(esa)],[20,25,theory(equality)])).
% cnf(32,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(e3,e1)=e4|op(e3,e1)=e3|op(e3,e1)=e2|op(e3,e1)=e1|op(e3,e1)=e0),inference(split_conjunct,[status(thm)],[1])).
% cnf(52,plain,(unit=e4|unit=e3|unit=e2|unit=e1|unit=e0),inference(split_conjunct,[status(thm)],[2])).
% cnf(54,plain,(op(unit,e4)=e4),inference(split_conjunct,[status(thm)],[2])).
% cnf(55,plain,(op(e3,unit)=e3),inference(split_conjunct,[status(thm)],[2])).
% cnf(56,plain,(op(unit,e3)=e3),inference(split_conjunct,[status(thm)],[2])).
% cnf(60,plain,(op(unit,e1)=e1),inference(split_conjunct,[status(thm)],[2])).
% cnf(61,plain,(op(e0,unit)=e0),inference(split_conjunct,[status(thm)],[2])).
% cnf(62,plain,(op(unit,e0)=e0),inference(split_conjunct,[status(thm)],[2])).
% cnf(78,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)],[3])).
% cnf(82,plain,(op(e3,e4)=e0|op(e3,e3)=e0|op(e3,e2)=e0|op(e3,e1)=e0|op(e3,e0)=e0),inference(split_conjunct,[status(thm)],[3])).
% cnf(92,plain,(op(e2,e4)=e0|op(e2,e3)=e0|op(e2,e2)=e0|op(e2,e1)=e0|op(e2,e0)=e0),inference(split_conjunct,[status(thm)],[3])).
% cnf(95,plain,(op(e4,e1)=e3|op(e3,e1)=e3|op(e2,e1)=e3|op(e1,e1)=e3|op(e0,e1)=e3),inference(split_conjunct,[status(thm)],[3])).
% cnf(116,plain,(op(e4,e1)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[4])).
% cnf(123,plain,(op(e3,e3)!=op(e3,e4)),inference(split_conjunct,[status(thm)],[4])).
% cnf(124,plain,(op(e3,e2)!=op(e3,e4)),inference(split_conjunct,[status(thm)],[4])).
% cnf(126,plain,(op(e3,e1)!=op(e3,e4)),inference(split_conjunct,[status(thm)],[4])).
% cnf(127,plain,(op(e3,e1)!=op(e3,e3)),inference(split_conjunct,[status(thm)],[4])).
% cnf(128,plain,(op(e3,e1)!=op(e3,e2)),inference(split_conjunct,[status(thm)],[4])).
% cnf(130,plain,(op(e3,e0)!=op(e3,e3)),inference(split_conjunct,[status(thm)],[4])).
% cnf(132,plain,(op(e3,e0)!=op(e3,e1)),inference(split_conjunct,[status(thm)],[4])).
% cnf(135,plain,(op(e2,e2)!=op(e2,e3)),inference(split_conjunct,[status(thm)],[4])).
% cnf(138,plain,(op(e2,e1)!=op(e2,e2)),inference(split_conjunct,[status(thm)],[4])).
% cnf(163,plain,(op(e3,e4)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[4])).
% cnf(164,plain,(op(e2,e4)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[4])).
% cnf(169,plain,(op(e0,e4)!=op(e4,e4)),inference(split_conjunct,[status(thm)],[4])).
% cnf(173,plain,(op(e3,e3)!=op(e4,e3)),inference(split_conjunct,[status(thm)],[4])).
% cnf(197,plain,(op(e1,e1)!=op(e3,e1)),inference(split_conjunct,[status(thm)],[4])).
% cnf(198,plain,(op(e1,e1)!=op(e2,e1)),inference(split_conjunct,[status(thm)],[4])).
% cnf(203,plain,(op(e3,e0)!=op(e4,e0)),inference(split_conjunct,[status(thm)],[4])).
% cnf(205,plain,(op(e2,e0)!=op(e3,e0)),inference(split_conjunct,[status(thm)],[4])).
% cnf(210,plain,(op(e0,e0)!=op(e3,e0)),inference(split_conjunct,[status(thm)],[4])).
% cnf(213,plain,(e4=op(op(e2,e2),op(e2,e2))),inference(split_conjunct,[status(thm)],[5])).
% cnf(214,plain,(e3=op(e2,e2)),inference(split_conjunct,[status(thm)],[5])).
% cnf(215,plain,(e1=op(op(e2,e2),e2)),inference(split_conjunct,[status(thm)],[5])).
% cnf(216,plain,(e0=op(op(op(e2,e2),e2),op(op(e2,e2),e2))),inference(split_conjunct,[status(thm)],[5])).
% cnf(217,plain,(e3!=e4),inference(split_conjunct,[status(thm)],[6])).
% cnf(218,plain,(e2!=e4),inference(split_conjunct,[status(thm)],[6])).
% cnf(219,plain,(e2!=e3),inference(split_conjunct,[status(thm)],[6])).
% cnf(220,plain,(e1!=e4),inference(split_conjunct,[status(thm)],[6])).
% cnf(221,plain,(e1!=e3),inference(split_conjunct,[status(thm)],[6])).
% cnf(222,plain,(e1!=e2),inference(split_conjunct,[status(thm)],[6])).
% cnf(223,plain,(e0!=e4),inference(split_conjunct,[status(thm)],[6])).
% cnf(224,plain,(e0!=e3),inference(split_conjunct,[status(thm)],[6])).
% cnf(225,plain,(e0!=e2),inference(split_conjunct,[status(thm)],[6])).
% cnf(226,plain,(e0!=e1),inference(split_conjunct,[status(thm)],[6])).
% fof(227, negated_conjecture,(((((epred1_0|epred2_0)|epred3_0)|epred4_0)|epred5_0)&(((epred11_0|((op(e4,e4)=e2&op(e2,e2)=e4)&~(op(e4,e2)=e4)))|((op(e4,e4)=e3&op(e3,e3)=e4)&~(op(e4,e3)=e4)))|(op(e4,e4)=e4&~(op(e4,e4)=e4)))),inference(fof_nnf,[status(thm)],[21])).
% fof(228, negated_conjecture,(((((epred1_0|epred2_0)|epred3_0)|epred4_0)|epred5_0)&((((((op(e4,e4)=e4|(op(e4,e4)=e3|(op(e4,e4)=e2|epred11_0)))&(~(op(e4,e4)=e4)|(op(e4,e4)=e3|(op(e4,e4)=e2|epred11_0))))&((op(e4,e4)=e4|(op(e3,e3)=e4|(op(e4,e4)=e2|epred11_0)))&(~(op(e4,e4)=e4)|(op(e3,e3)=e4|(op(e4,e4)=e2|epred11_0)))))&((op(e4,e4)=e4|(~(op(e4,e3)=e4)|(op(e4,e4)=e2|epred11_0)))&(~(op(e4,e4)=e4)|(~(op(e4,e3)=e4)|(op(e4,e4)=e2|epred11_0)))))&((((op(e4,e4)=e4|(op(e4,e4)=e3|(op(e2,e2)=e4|epred11_0)))&(~(op(e4,e4)=e4)|(op(e4,e4)=e3|(op(e2,e2)=e4|epred11_0))))&((op(e4,e4)=e4|(op(e3,e3)=e4|(op(e2,e2)=e4|epred11_0)))&(~(op(e4,e4)=e4)|(op(e3,e3)=e4|(op(e2,e2)=e4|epred11_0)))))&((op(e4,e4)=e4|(~(op(e4,e3)=e4)|(op(e2,e2)=e4|epred11_0)))&(~(op(e4,e4)=e4)|(~(op(e4,e3)=e4)|(op(e2,e2)=e4|epred11_0))))))&((((op(e4,e4)=e4|(op(e4,e4)=e3|(~(op(e4,e2)=e4)|epred11_0)))&(~(op(e4,e4)=e4)|(op(e4,e4)=e3|(~(op(e4,e2)=e4)|epred11_0))))&((op(e4,e4)=e4|(op(e3,e3)=e4|(~(op(e4,e2)=e4)|epred11_0)))&(~(op(e4,e4)=e4)|(op(e3,e3)=e4|(~(op(e4,e2)=e4)|epred11_0)))))&((op(e4,e4)=e4|(~(op(e4,e3)=e4)|(~(op(e4,e2)=e4)|epred11_0)))&(~(op(e4,e4)=e4)|(~(op(e4,e3)=e4)|(~(op(e4,e2)=e4)|epred11_0))))))),inference(distribute,[status(thm)],[227])).
% cnf(239,negated_conjecture,(epred11_0|op(e2,e2)=e4|op(e4,e4)=e3|op(e4,e4)!=e4),inference(split_conjunct,[status(thm)],[228])).
% cnf(240,negated_conjecture,(epred11_0|op(e2,e2)=e4|op(e4,e4)=e3|op(e4,e4)=e4),inference(split_conjunct,[status(thm)],[228])).
% cnf(247,negated_conjecture,(epred5_0|epred4_0|epred3_0|epred2_0|epred1_0),inference(split_conjunct,[status(thm)],[228])).
% fof(248, plain,(~(epred1_0)|(((((((((((((((((((((((((~(op(e0,e0)=e0)|(op(e0,e0)=e0&~(e0=unit)))&(~(op(e0,e1)=e0)|(op(e0,e0)=e1&~(e0=unit))))&(~(op(e0,e2)=e0)|(op(e0,e0)=e2&~(e0=unit))))&(~(op(e0,e3)=e0)|(op(e0,e0)=e3&~(e0=unit))))&(~(op(e0,e4)=e0)|(op(e0,e0)=e4&~(e0=unit))))&(~(op(e1,e0)=e0)|(op(e1,e0)=e0&~(e0=unit))))&(~(op(e1,e1)=e0)|(op(e1,e0)=e1&~(e0=unit))))&(~(op(e1,e2)=e0)|(op(e1,e0)=e2&~(e0=unit))))&(~(op(e1,e3)=e0)|(op(e1,e0)=e3&~(e0=unit))))&(~(op(e1,e4)=e0)|(op(e1,e0)=e4&~(e0=unit))))&(~(op(e2,e0)=e0)|(op(e2,e0)=e0&~(e0=unit))))&(~(op(e2,e1)=e0)|(op(e2,e0)=e1&~(e0=unit))))&(~(op(e2,e2)=e0)|(op(e2,e0)=e2&~(e0=unit))))&(~(op(e2,e3)=e0)|(op(e2,e0)=e3&~(e0=unit))))&(~(op(e2,e4)=e0)|(op(e2,e0)=e4&~(e0=unit))))&(~(op(e3,e0)=e0)|(op(e3,e0)=e0&~(e0=unit))))&(~(op(e3,e1)=e0)|(op(e3,e0)=e1&~(e0=unit))))&(~(op(e3,e2)=e0)|(op(e3,e0)=e2&~(e0=unit))))&(~(op(e3,e3)=e0)|(op(e3,e0)=e3&~(e0=unit))))&(~(op(e3,e4)=e0)|(op(e3,e0)=e4&~(e0=unit))))&(~(op(e4,e0)=e0)|(op(e4,e0)=e0&~(e0=unit))))&(~(op(e4,e1)=e0)|(op(e4,e0)=e1&~(e0=unit))))&(~(op(e4,e2)=e0)|(op(e4,e0)=e2&~(e0=unit))))&(~(op(e4,e3)=e0)|(op(e4,e0)=e3&~(e0=unit))))&(~(op(e4,e4)=e0)|(op(e4,e0)=e4&~(e0=unit))))),inference(fof_nnf,[status(thm)],[10])).
% fof(249, plain,(((((((((((((((((((((((((((op(e0,e0)=e0|~(op(e0,e0)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e0,e0)=e0))|~(epred1_0)))&(((op(e0,e0)=e1|~(op(e0,e1)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e0,e1)=e0))|~(epred1_0))))&(((op(e0,e0)=e2|~(op(e0,e2)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e0,e2)=e0))|~(epred1_0))))&(((op(e0,e0)=e3|~(op(e0,e3)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e0,e3)=e0))|~(epred1_0))))&(((op(e0,e0)=e4|~(op(e0,e4)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e0,e4)=e0))|~(epred1_0))))&(((op(e1,e0)=e0|~(op(e1,e0)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e1,e0)=e0))|~(epred1_0))))&(((op(e1,e0)=e1|~(op(e1,e1)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e1,e1)=e0))|~(epred1_0))))&(((op(e1,e0)=e2|~(op(e1,e2)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e1,e2)=e0))|~(epred1_0))))&(((op(e1,e0)=e3|~(op(e1,e3)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e1,e3)=e0))|~(epred1_0))))&(((op(e1,e0)=e4|~(op(e1,e4)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e1,e4)=e0))|~(epred1_0))))&(((op(e2,e0)=e0|~(op(e2,e0)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e2,e0)=e0))|~(epred1_0))))&(((op(e2,e0)=e1|~(op(e2,e1)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e2,e1)=e0))|~(epred1_0))))&(((op(e2,e0)=e2|~(op(e2,e2)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e2,e2)=e0))|~(epred1_0))))&(((op(e2,e0)=e3|~(op(e2,e3)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e2,e3)=e0))|~(epred1_0))))&(((op(e2,e0)=e4|~(op(e2,e4)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e2,e4)=e0))|~(epred1_0))))&(((op(e3,e0)=e0|~(op(e3,e0)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e3,e0)=e0))|~(epred1_0))))&(((op(e3,e0)=e1|~(op(e3,e1)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e3,e1)=e0))|~(epred1_0))))&(((op(e3,e0)=e2|~(op(e3,e2)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e3,e2)=e0))|~(epred1_0))))&(((op(e3,e0)=e3|~(op(e3,e3)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e3,e3)=e0))|~(epred1_0))))&(((op(e3,e0)=e4|~(op(e3,e4)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e3,e4)=e0))|~(epred1_0))))&(((op(e4,e0)=e0|~(op(e4,e0)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e4,e0)=e0))|~(epred1_0))))&(((op(e4,e0)=e1|~(op(e4,e1)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e4,e1)=e0))|~(epred1_0))))&(((op(e4,e0)=e2|~(op(e4,e2)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e4,e2)=e0))|~(epred1_0))))&(((op(e4,e0)=e3|~(op(e4,e3)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e4,e3)=e0))|~(epred1_0))))&(((op(e4,e0)=e4|~(op(e4,e4)=e0))|~(epred1_0))&((~(e0=unit)|~(op(e4,e4)=e0))|~(epred1_0)))),inference(distribute,[status(thm)],[248])).
% cnf(261,plain,(op(e3,e0)=e4|~epred1_0|op(e3,e4)!=e0),inference(split_conjunct,[status(thm)],[249])).
% cnf(286,plain,(~epred1_0|op(e1,e1)!=e0|e0!=unit),inference(split_conjunct,[status(thm)],[249])).
% fof(300, plain,(~(epred2_0)|(((((((((((((((((((((((((~(op(e0,e0)=e1)|(op(e0,e1)=e0&~(e1=unit)))&(~(op(e0,e1)=e1)|(op(e0,e1)=e1&~(e1=unit))))&(~(op(e0,e2)=e1)|(op(e0,e1)=e2&~(e1=unit))))&(~(op(e0,e3)=e1)|(op(e0,e1)=e3&~(e1=unit))))&(~(op(e0,e4)=e1)|(op(e0,e1)=e4&~(e1=unit))))&(~(op(e1,e0)=e1)|(op(e1,e1)=e0&~(e1=unit))))&(~(op(e1,e1)=e1)|(op(e1,e1)=e1&~(e1=unit))))&(~(op(e1,e2)=e1)|(op(e1,e1)=e2&~(e1=unit))))&(~(op(e1,e3)=e1)|(op(e1,e1)=e3&~(e1=unit))))&(~(op(e1,e4)=e1)|(op(e1,e1)=e4&~(e1=unit))))&(~(op(e2,e0)=e1)|(op(e2,e1)=e0&~(e1=unit))))&(~(op(e2,e1)=e1)|(op(e2,e1)=e1&~(e1=unit))))&(~(op(e2,e2)=e1)|(op(e2,e1)=e2&~(e1=unit))))&(~(op(e2,e3)=e1)|(op(e2,e1)=e3&~(e1=unit))))&(~(op(e2,e4)=e1)|(op(e2,e1)=e4&~(e1=unit))))&(~(op(e3,e0)=e1)|(op(e3,e1)=e0&~(e1=unit))))&(~(op(e3,e1)=e1)|(op(e3,e1)=e1&~(e1=unit))))&(~(op(e3,e2)=e1)|(op(e3,e1)=e2&~(e1=unit))))&(~(op(e3,e3)=e1)|(op(e3,e1)=e3&~(e1=unit))))&(~(op(e3,e4)=e1)|(op(e3,e1)=e4&~(e1=unit))))&(~(op(e4,e0)=e1)|(op(e4,e1)=e0&~(e1=unit))))&(~(op(e4,e1)=e1)|(op(e4,e1)=e1&~(e1=unit))))&(~(op(e4,e2)=e1)|(op(e4,e1)=e2&~(e1=unit))))&(~(op(e4,e3)=e1)|(op(e4,e1)=e3&~(e1=unit))))&(~(op(e4,e4)=e1)|(op(e4,e1)=e4&~(e1=unit))))),inference(fof_nnf,[status(thm)],[11])).
% fof(301, plain,(((((((((((((((((((((((((((op(e0,e1)=e0|~(op(e0,e0)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e0,e0)=e1))|~(epred2_0)))&(((op(e0,e1)=e1|~(op(e0,e1)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e0,e1)=e1))|~(epred2_0))))&(((op(e0,e1)=e2|~(op(e0,e2)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e0,e2)=e1))|~(epred2_0))))&(((op(e0,e1)=e3|~(op(e0,e3)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e0,e3)=e1))|~(epred2_0))))&(((op(e0,e1)=e4|~(op(e0,e4)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e0,e4)=e1))|~(epred2_0))))&(((op(e1,e1)=e0|~(op(e1,e0)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e1,e0)=e1))|~(epred2_0))))&(((op(e1,e1)=e1|~(op(e1,e1)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e1,e1)=e1))|~(epred2_0))))&(((op(e1,e1)=e2|~(op(e1,e2)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e1,e2)=e1))|~(epred2_0))))&(((op(e1,e1)=e3|~(op(e1,e3)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e1,e3)=e1))|~(epred2_0))))&(((op(e1,e1)=e4|~(op(e1,e4)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e1,e4)=e1))|~(epred2_0))))&(((op(e2,e1)=e0|~(op(e2,e0)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e2,e0)=e1))|~(epred2_0))))&(((op(e2,e1)=e1|~(op(e2,e1)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e2,e1)=e1))|~(epred2_0))))&(((op(e2,e1)=e2|~(op(e2,e2)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e2,e2)=e1))|~(epred2_0))))&(((op(e2,e1)=e3|~(op(e2,e3)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e2,e3)=e1))|~(epred2_0))))&(((op(e2,e1)=e4|~(op(e2,e4)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e2,e4)=e1))|~(epred2_0))))&(((op(e3,e1)=e0|~(op(e3,e0)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e3,e0)=e1))|~(epred2_0))))&(((op(e3,e1)=e1|~(op(e3,e1)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e3,e1)=e1))|~(epred2_0))))&(((op(e3,e1)=e2|~(op(e3,e2)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e3,e2)=e1))|~(epred2_0))))&(((op(e3,e1)=e3|~(op(e3,e3)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e3,e3)=e1))|~(epred2_0))))&(((op(e3,e1)=e4|~(op(e3,e4)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e3,e4)=e1))|~(epred2_0))))&(((op(e4,e1)=e0|~(op(e4,e0)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e4,e0)=e1))|~(epred2_0))))&(((op(e4,e1)=e1|~(op(e4,e1)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e4,e1)=e1))|~(epred2_0))))&(((op(e4,e1)=e2|~(op(e4,e2)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e4,e2)=e1))|~(epred2_0))))&(((op(e4,e1)=e3|~(op(e4,e3)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e4,e3)=e1))|~(epred2_0))))&(((op(e4,e1)=e4|~(op(e4,e4)=e1))|~(epred2_0))&((~(e1=unit)|~(op(e4,e4)=e1))|~(epred2_0)))),inference(distribute,[status(thm)],[300])).
% cnf(317,plain,(op(e3,e1)=e2|~epred2_0|op(e3,e2)!=e1),inference(split_conjunct,[status(thm)],[301])).
% fof(352, plain,(~(epred3_0)|(((((((((((((((((((((((((~(op(e0,e0)=e2)|(op(e0,e2)=e0&~(e2=unit)))&(~(op(e0,e1)=e2)|(op(e0,e2)=e1&~(e2=unit))))&(~(op(e0,e2)=e2)|(op(e0,e2)=e2&~(e2=unit))))&(~(op(e0,e3)=e2)|(op(e0,e2)=e3&~(e2=unit))))&(~(op(e0,e4)=e2)|(op(e0,e2)=e4&~(e2=unit))))&(~(op(e1,e0)=e2)|(op(e1,e2)=e0&~(e2=unit))))&(~(op(e1,e1)=e2)|(op(e1,e2)=e1&~(e2=unit))))&(~(op(e1,e2)=e2)|(op(e1,e2)=e2&~(e2=unit))))&(~(op(e1,e3)=e2)|(op(e1,e2)=e3&~(e2=unit))))&(~(op(e1,e4)=e2)|(op(e1,e2)=e4&~(e2=unit))))&(~(op(e2,e0)=e2)|(op(e2,e2)=e0&~(e2=unit))))&(~(op(e2,e1)=e2)|(op(e2,e2)=e1&~(e2=unit))))&(~(op(e2,e2)=e2)|(op(e2,e2)=e2&~(e2=unit))))&(~(op(e2,e3)=e2)|(op(e2,e2)=e3&~(e2=unit))))&(~(op(e2,e4)=e2)|(op(e2,e2)=e4&~(e2=unit))))&(~(op(e3,e0)=e2)|(op(e3,e2)=e0&~(e2=unit))))&(~(op(e3,e1)=e2)|(op(e3,e2)=e1&~(e2=unit))))&(~(op(e3,e2)=e2)|(op(e3,e2)=e2&~(e2=unit))))&(~(op(e3,e3)=e2)|(op(e3,e2)=e3&~(e2=unit))))&(~(op(e3,e4)=e2)|(op(e3,e2)=e4&~(e2=unit))))&(~(op(e4,e0)=e2)|(op(e4,e2)=e0&~(e2=unit))))&(~(op(e4,e1)=e2)|(op(e4,e2)=e1&~(e2=unit))))&(~(op(e4,e2)=e2)|(op(e4,e2)=e2&~(e2=unit))))&(~(op(e4,e3)=e2)|(op(e4,e2)=e3&~(e2=unit))))&(~(op(e4,e4)=e2)|(op(e4,e2)=e4&~(e2=unit))))),inference(fof_nnf,[status(thm)],[12])).
% fof(353, plain,(((((((((((((((((((((((((((op(e0,e2)=e0|~(op(e0,e0)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e0,e0)=e2))|~(epred3_0)))&(((op(e0,e2)=e1|~(op(e0,e1)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e0,e1)=e2))|~(epred3_0))))&(((op(e0,e2)=e2|~(op(e0,e2)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e0,e2)=e2))|~(epred3_0))))&(((op(e0,e2)=e3|~(op(e0,e3)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e0,e3)=e2))|~(epred3_0))))&(((op(e0,e2)=e4|~(op(e0,e4)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e0,e4)=e2))|~(epred3_0))))&(((op(e1,e2)=e0|~(op(e1,e0)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e1,e0)=e2))|~(epred3_0))))&(((op(e1,e2)=e1|~(op(e1,e1)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e1,e1)=e2))|~(epred3_0))))&(((op(e1,e2)=e2|~(op(e1,e2)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e1,e2)=e2))|~(epred3_0))))&(((op(e1,e2)=e3|~(op(e1,e3)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e1,e3)=e2))|~(epred3_0))))&(((op(e1,e2)=e4|~(op(e1,e4)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e1,e4)=e2))|~(epred3_0))))&(((op(e2,e2)=e0|~(op(e2,e0)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e2,e0)=e2))|~(epred3_0))))&(((op(e2,e2)=e1|~(op(e2,e1)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e2,e1)=e2))|~(epred3_0))))&(((op(e2,e2)=e2|~(op(e2,e2)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e2,e2)=e2))|~(epred3_0))))&(((op(e2,e2)=e3|~(op(e2,e3)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e2,e3)=e2))|~(epred3_0))))&(((op(e2,e2)=e4|~(op(e2,e4)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e2,e4)=e2))|~(epred3_0))))&(((op(e3,e2)=e0|~(op(e3,e0)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e3,e0)=e2))|~(epred3_0))))&(((op(e3,e2)=e1|~(op(e3,e1)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e3,e1)=e2))|~(epred3_0))))&(((op(e3,e2)=e2|~(op(e3,e2)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e3,e2)=e2))|~(epred3_0))))&(((op(e3,e2)=e3|~(op(e3,e3)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e3,e3)=e2))|~(epred3_0))))&(((op(e3,e2)=e4|~(op(e3,e4)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e3,e4)=e2))|~(epred3_0))))&(((op(e4,e2)=e0|~(op(e4,e0)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e4,e0)=e2))|~(epred3_0))))&(((op(e4,e2)=e1|~(op(e4,e1)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e4,e1)=e2))|~(epred3_0))))&(((op(e4,e2)=e2|~(op(e4,e2)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e4,e2)=e2))|~(epred3_0))))&(((op(e4,e2)=e3|~(op(e4,e3)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e4,e3)=e2))|~(epred3_0))))&(((op(e4,e2)=e4|~(op(e4,e4)=e2))|~(epred3_0))&((~(e2=unit)|~(op(e4,e4)=e2))|~(epred3_0)))),inference(distribute,[status(thm)],[352])).
% cnf(365,plain,(op(e3,e2)=e4|~epred3_0|op(e3,e4)!=e2),inference(split_conjunct,[status(thm)],[353])).
% cnf(373,plain,(op(e3,e2)=e0|~epred3_0|op(e3,e0)!=e2),inference(split_conjunct,[status(thm)],[353])).
% fof(404, plain,(~(epred4_0)|(((((((((((((((((((((((((~(op(e0,e0)=e3)|(op(e0,e3)=e0&~(e3=unit)))&(~(op(e0,e1)=e3)|(op(e0,e3)=e1&~(e3=unit))))&(~(op(e0,e2)=e3)|(op(e0,e3)=e2&~(e3=unit))))&(~(op(e0,e3)=e3)|(op(e0,e3)=e3&~(e3=unit))))&(~(op(e0,e4)=e3)|(op(e0,e3)=e4&~(e3=unit))))&(~(op(e1,e0)=e3)|(op(e1,e3)=e0&~(e3=unit))))&(~(op(e1,e1)=e3)|(op(e1,e3)=e1&~(e3=unit))))&(~(op(e1,e2)=e3)|(op(e1,e3)=e2&~(e3=unit))))&(~(op(e1,e3)=e3)|(op(e1,e3)=e3&~(e3=unit))))&(~(op(e1,e4)=e3)|(op(e1,e3)=e4&~(e3=unit))))&(~(op(e2,e0)=e3)|(op(e2,e3)=e0&~(e3=unit))))&(~(op(e2,e1)=e3)|(op(e2,e3)=e1&~(e3=unit))))&(~(op(e2,e2)=e3)|(op(e2,e3)=e2&~(e3=unit))))&(~(op(e2,e3)=e3)|(op(e2,e3)=e3&~(e3=unit))))&(~(op(e2,e4)=e3)|(op(e2,e3)=e4&~(e3=unit))))&(~(op(e3,e0)=e3)|(op(e3,e3)=e0&~(e3=unit))))&(~(op(e3,e1)=e3)|(op(e3,e3)=e1&~(e3=unit))))&(~(op(e3,e2)=e3)|(op(e3,e3)=e2&~(e3=unit))))&(~(op(e3,e3)=e3)|(op(e3,e3)=e3&~(e3=unit))))&(~(op(e3,e4)=e3)|(op(e3,e3)=e4&~(e3=unit))))&(~(op(e4,e0)=e3)|(op(e4,e3)=e0&~(e3=unit))))&(~(op(e4,e1)=e3)|(op(e4,e3)=e1&~(e3=unit))))&(~(op(e4,e2)=e3)|(op(e4,e3)=e2&~(e3=unit))))&(~(op(e4,e3)=e3)|(op(e4,e3)=e3&~(e3=unit))))&(~(op(e4,e4)=e3)|(op(e4,e3)=e4&~(e3=unit))))),inference(fof_nnf,[status(thm)],[13])).
% fof(405, plain,(((((((((((((((((((((((((((op(e0,e3)=e0|~(op(e0,e0)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e0,e0)=e3))|~(epred4_0)))&(((op(e0,e3)=e1|~(op(e0,e1)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e0,e1)=e3))|~(epred4_0))))&(((op(e0,e3)=e2|~(op(e0,e2)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e0,e2)=e3))|~(epred4_0))))&(((op(e0,e3)=e3|~(op(e0,e3)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e0,e3)=e3))|~(epred4_0))))&(((op(e0,e3)=e4|~(op(e0,e4)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e0,e4)=e3))|~(epred4_0))))&(((op(e1,e3)=e0|~(op(e1,e0)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e1,e0)=e3))|~(epred4_0))))&(((op(e1,e3)=e1|~(op(e1,e1)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e1,e1)=e3))|~(epred4_0))))&(((op(e1,e3)=e2|~(op(e1,e2)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e1,e2)=e3))|~(epred4_0))))&(((op(e1,e3)=e3|~(op(e1,e3)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e1,e3)=e3))|~(epred4_0))))&(((op(e1,e3)=e4|~(op(e1,e4)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e1,e4)=e3))|~(epred4_0))))&(((op(e2,e3)=e0|~(op(e2,e0)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e2,e0)=e3))|~(epred4_0))))&(((op(e2,e3)=e1|~(op(e2,e1)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e2,e1)=e3))|~(epred4_0))))&(((op(e2,e3)=e2|~(op(e2,e2)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e2,e2)=e3))|~(epred4_0))))&(((op(e2,e3)=e3|~(op(e2,e3)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e2,e3)=e3))|~(epred4_0))))&(((op(e2,e3)=e4|~(op(e2,e4)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e2,e4)=e3))|~(epred4_0))))&(((op(e3,e3)=e0|~(op(e3,e0)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e3,e0)=e3))|~(epred4_0))))&(((op(e3,e3)=e1|~(op(e3,e1)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e3,e1)=e3))|~(epred4_0))))&(((op(e3,e3)=e2|~(op(e3,e2)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e3,e2)=e3))|~(epred4_0))))&(((op(e3,e3)=e3|~(op(e3,e3)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e3,e3)=e3))|~(epred4_0))))&(((op(e3,e3)=e4|~(op(e3,e4)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e3,e4)=e3))|~(epred4_0))))&(((op(e4,e3)=e0|~(op(e4,e0)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e4,e0)=e3))|~(epred4_0))))&(((op(e4,e3)=e1|~(op(e4,e1)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e4,e1)=e3))|~(epred4_0))))&(((op(e4,e3)=e2|~(op(e4,e2)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e4,e2)=e3))|~(epred4_0))))&(((op(e4,e3)=e3|~(op(e4,e3)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e4,e3)=e3))|~(epred4_0))))&(((op(e4,e3)=e4|~(op(e4,e4)=e3))|~(epred4_0))&((~(e3=unit)|~(op(e4,e4)=e3))|~(epred4_0)))),inference(distribute,[status(thm)],[404])).
% cnf(407,plain,(op(e4,e3)=e4|~epred4_0|op(e4,e4)!=e3),inference(split_conjunct,[status(thm)],[405])).
% cnf(423,plain,(op(e3,e3)=e1|~epred4_0|op(e3,e1)!=e3),inference(split_conjunct,[status(thm)],[405])).
% cnf(431,plain,(op(e2,e3)=e2|~epred4_0|op(e2,e2)!=e3),inference(split_conjunct,[status(thm)],[405])).
% fof(456, plain,(~(epred5_0)|(((((((((((((((((((((((((~(op(e0,e0)=e4)|(op(e0,e4)=e0&~(e4=unit)))&(~(op(e0,e1)=e4)|(op(e0,e4)=e1&~(e4=unit))))&(~(op(e0,e2)=e4)|(op(e0,e4)=e2&~(e4=unit))))&(~(op(e0,e3)=e4)|(op(e0,e4)=e3&~(e4=unit))))&(~(op(e0,e4)=e4)|(op(e0,e4)=e4&~(e4=unit))))&(~(op(e1,e0)=e4)|(op(e1,e4)=e0&~(e4=unit))))&(~(op(e1,e1)=e4)|(op(e1,e4)=e1&~(e4=unit))))&(~(op(e1,e2)=e4)|(op(e1,e4)=e2&~(e4=unit))))&(~(op(e1,e3)=e4)|(op(e1,e4)=e3&~(e4=unit))))&(~(op(e1,e4)=e4)|(op(e1,e4)=e4&~(e4=unit))))&(~(op(e2,e0)=e4)|(op(e2,e4)=e0&~(e4=unit))))&(~(op(e2,e1)=e4)|(op(e2,e4)=e1&~(e4=unit))))&(~(op(e2,e2)=e4)|(op(e2,e4)=e2&~(e4=unit))))&(~(op(e2,e3)=e4)|(op(e2,e4)=e3&~(e4=unit))))&(~(op(e2,e4)=e4)|(op(e2,e4)=e4&~(e4=unit))))&(~(op(e3,e0)=e4)|(op(e3,e4)=e0&~(e4=unit))))&(~(op(e3,e1)=e4)|(op(e3,e4)=e1&~(e4=unit))))&(~(op(e3,e2)=e4)|(op(e3,e4)=e2&~(e4=unit))))&(~(op(e3,e3)=e4)|(op(e3,e4)=e3&~(e4=unit))))&(~(op(e3,e4)=e4)|(op(e3,e4)=e4&~(e4=unit))))&(~(op(e4,e0)=e4)|(op(e4,e4)=e0&~(e4=unit))))&(~(op(e4,e1)=e4)|(op(e4,e4)=e1&~(e4=unit))))&(~(op(e4,e2)=e4)|(op(e4,e4)=e2&~(e4=unit))))&(~(op(e4,e3)=e4)|(op(e4,e4)=e3&~(e4=unit))))&(~(op(e4,e4)=e4)|(op(e4,e4)=e4&~(e4=unit))))),inference(fof_nnf,[status(thm)],[14])).
% fof(457, plain,(((((((((((((((((((((((((((op(e0,e4)=e0|~(op(e0,e0)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e0,e0)=e4))|~(epred5_0)))&(((op(e0,e4)=e1|~(op(e0,e1)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e0,e1)=e4))|~(epred5_0))))&(((op(e0,e4)=e2|~(op(e0,e2)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e0,e2)=e4))|~(epred5_0))))&(((op(e0,e4)=e3|~(op(e0,e3)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e0,e3)=e4))|~(epred5_0))))&(((op(e0,e4)=e4|~(op(e0,e4)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e0,e4)=e4))|~(epred5_0))))&(((op(e1,e4)=e0|~(op(e1,e0)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e1,e0)=e4))|~(epred5_0))))&(((op(e1,e4)=e1|~(op(e1,e1)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e1,e1)=e4))|~(epred5_0))))&(((op(e1,e4)=e2|~(op(e1,e2)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e1,e2)=e4))|~(epred5_0))))&(((op(e1,e4)=e3|~(op(e1,e3)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e1,e3)=e4))|~(epred5_0))))&(((op(e1,e4)=e4|~(op(e1,e4)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e1,e4)=e4))|~(epred5_0))))&(((op(e2,e4)=e0|~(op(e2,e0)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e2,e0)=e4))|~(epred5_0))))&(((op(e2,e4)=e1|~(op(e2,e1)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e2,e1)=e4))|~(epred5_0))))&(((op(e2,e4)=e2|~(op(e2,e2)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e2,e2)=e4))|~(epred5_0))))&(((op(e2,e4)=e3|~(op(e2,e3)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e2,e3)=e4))|~(epred5_0))))&(((op(e2,e4)=e4|~(op(e2,e4)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e2,e4)=e4))|~(epred5_0))))&(((op(e3,e4)=e0|~(op(e3,e0)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e3,e0)=e4))|~(epred5_0))))&(((op(e3,e4)=e1|~(op(e3,e1)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e3,e1)=e4))|~(epred5_0))))&(((op(e3,e4)=e2|~(op(e3,e2)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e3,e2)=e4))|~(epred5_0))))&(((op(e3,e4)=e3|~(op(e3,e3)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e3,e3)=e4))|~(epred5_0))))&(((op(e3,e4)=e4|~(op(e3,e4)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e3,e4)=e4))|~(epred5_0))))&(((op(e4,e4)=e0|~(op(e4,e0)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e4,e0)=e4))|~(epred5_0))))&(((op(e4,e4)=e1|~(op(e4,e1)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e4,e1)=e4))|~(epred5_0))))&(((op(e4,e4)=e2|~(op(e4,e2)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e4,e2)=e4))|~(epred5_0))))&(((op(e4,e4)=e3|~(op(e4,e3)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e4,e3)=e4))|~(epred5_0))))&(((op(e4,e4)=e4|~(op(e4,e4)=e4))|~(epred5_0))&((~(e4=unit)|~(op(e4,e4)=e4))|~(epred5_0)))),inference(distribute,[status(thm)],[456])).
% cnf(471,plain,(op(e3,e4)=e3|~epred5_0|op(e3,e3)!=e4),inference(split_conjunct,[status(thm)],[457])).
% cnf(507,plain,(op(e0,e4)=e0|~epred5_0|op(e0,e0)!=e4),inference(split_conjunct,[status(thm)],[457])).
% fof(508, plain,(~(epred6_0)|((((op(e0,e0)=e0&~(op(e0,e0)=e0))|((op(e0,e0)=e1&op(e1,e1)=e0)&~(op(e0,e1)=e0)))|((op(e0,e0)=e2&op(e2,e2)=e0)&~(op(e0,e2)=e0)))|((op(e0,e0)=e3&op(e3,e3)=e0)&~(op(e0,e3)=e0)))),inference(fof_nnf,[status(thm)],[15])).
% fof(509, plain,(((((((((op(e0,e0)=e3|(op(e0,e0)=e2|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(op(e0,e0)=e2|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e0,e0)=e2|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0)))&((((op(e0,e0)=e3|(op(e2,e2)=e0|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(op(e2,e2)=e0|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e2,e2)=e0|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0))))&((((op(e0,e0)=e3|(~(op(e0,e2)=e0)|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(~(op(e0,e2)=e0)|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(~(op(e0,e2)=e0)|(op(e0,e0)=e1|op(e0,e0)=e0)))|~(epred6_0))))&((((((op(e0,e0)=e3|(op(e0,e0)=e2|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(op(e0,e0)=e2|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e0,e0)=e2|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0)))&((((op(e0,e0)=e3|(op(e2,e2)=e0|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(op(e2,e2)=e0|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e2,e2)=e0|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0))))&((((op(e0,e0)=e3|(~(op(e0,e2)=e0)|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(~(op(e0,e2)=e0)|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(~(op(e0,e2)=e0)|(op(e1,e1)=e0|op(e0,e0)=e0)))|~(epred6_0)))))&((((((op(e0,e0)=e3|(op(e0,e0)=e2|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(op(e0,e0)=e2|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e0,e0)=e2|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0)))&((((op(e0,e0)=e3|(op(e2,e2)=e0|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(op(e2,e2)=e0|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e2,e2)=e0|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0))))&((((op(e0,e0)=e3|(~(op(e0,e2)=e0)|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0))&((op(e3,e3)=e0|(~(op(e0,e2)=e0)|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0)))&((~(op(e0,e3)=e0)|(~(op(e0,e2)=e0)|(~(op(e0,e1)=e0)|op(e0,e0)=e0)))|~(epred6_0)))))&((((((((op(e0,e0)=e3|(op(e0,e0)=e2|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(op(e0,e0)=e2|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e0,e0)=e2|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0)))&((((op(e0,e0)=e3|(op(e2,e2)=e0|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(op(e2,e2)=e0|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e2,e2)=e0|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0))))&((((op(e0,e0)=e3|(~(op(e0,e2)=e0)|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(~(op(e0,e2)=e0)|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(~(op(e0,e2)=e0)|(op(e0,e0)=e1|~(op(e0,e0)=e0))))|~(epred6_0))))&((((((op(e0,e0)=e3|(op(e0,e0)=e2|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(op(e0,e0)=e2|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e0,e0)=e2|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0)))&((((op(e0,e0)=e3|(op(e2,e2)=e0|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(op(e2,e2)=e0|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e2,e2)=e0|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0))))&((((op(e0,e0)=e3|(~(op(e0,e2)=e0)|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(~(op(e0,e2)=e0)|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(~(op(e0,e2)=e0)|(op(e1,e1)=e0|~(op(e0,e0)=e0))))|~(epred6_0)))))&((((((op(e0,e0)=e3|(op(e0,e0)=e2|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(op(e0,e0)=e2|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e0,e0)=e2|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0)))&((((op(e0,e0)=e3|(op(e2,e2)=e0|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(op(e2,e2)=e0|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(op(e2,e2)=e0|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0))))&((((op(e0,e0)=e3|(~(op(e0,e2)=e0)|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0))&((op(e3,e3)=e0|(~(op(e0,e2)=e0)|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0)))&((~(op(e0,e3)=e0)|(~(op(e0,e2)=e0)|(~(op(e0,e1)=e0)|~(op(e0,e0)=e0))))|~(epred6_0)))))),inference(distribute,[status(thm)],[508])).
% cnf(532,plain,(op(e0,e0)=e1|op(e2,e2)=e0|op(e3,e3)=e0|~epred6_0|op(e0,e0)!=e0),inference(split_conjunct,[status(thm)],[509])).
% cnf(559,plain,(op(e0,e0)=e0|op(e0,e0)=e1|op(e2,e2)=e0|op(e3,e3)=e0|~epred6_0),inference(split_conjunct,[status(thm)],[509])).
% fof(564, plain,(~(epred7_0)|((((epred6_0|((op(e0,e0)=e4&op(e4,e4)=e0)&~(op(e0,e4)=e0)))|((op(e1,e1)=e0&op(e0,e0)=e1)&~(op(e1,e0)=e1)))|(op(e1,e1)=e1&~(op(e1,e1)=e1)))|((op(e1,e1)=e2&op(e2,e2)=e1)&~(op(e1,e2)=e1)))),inference(fof_nnf,[status(thm)],[22])).
% fof(565, plain,(((((((((op(e1,e1)=e2|(op(e1,e1)=e1|(op(e1,e1)=e0|(op(e0,e0)=e4|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(op(e1,e1)=e0|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(op(e1,e1)=e0|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(op(e0,e0)=e4|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(op(e0,e0)=e4|epred6_0))))|~(epred7_0))))&(((((op(e1,e1)=e2|(op(e1,e1)=e1|(op(e0,e0)=e1|(op(e0,e0)=e4|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(op(e0,e0)=e1|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(op(e0,e0)=e1|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(op(e0,e0)=e4|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))))&(((((op(e1,e1)=e2|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(op(e0,e0)=e4|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(op(e0,e0)=e4|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(op(e0,e0)=e4|epred6_0))))|~(epred7_0)))))&(((((((op(e1,e1)=e2|(op(e1,e1)=e1|(op(e1,e1)=e0|(op(e4,e4)=e0|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(op(e1,e1)=e0|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(op(e1,e1)=e0|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(op(e4,e4)=e0|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(op(e4,e4)=e0|epred6_0))))|~(epred7_0))))&(((((op(e1,e1)=e2|(op(e1,e1)=e1|(op(e0,e0)=e1|(op(e4,e4)=e0|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(op(e0,e0)=e1|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(op(e0,e0)=e1|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(op(e4,e4)=e0|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))))&(((((op(e1,e1)=e2|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(op(e4,e4)=e0|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(op(e4,e4)=e0|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(op(e4,e4)=e0|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(op(e4,e4)=e0|epred6_0))))|~(epred7_0))))))&(((((((op(e1,e1)=e2|(op(e1,e1)=e1|(op(e1,e1)=e0|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(op(e1,e1)=e0|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(op(e1,e1)=e0|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(op(e1,e1)=e0|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0))))&(((((op(e1,e1)=e2|(op(e1,e1)=e1|(op(e0,e0)=e1|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(op(e0,e0)=e1|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(op(e0,e0)=e1|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(op(e0,e0)=e1|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))))&(((((op(e1,e1)=e2|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(op(e1,e1)=e1|(~(op(e1,e0)=e1)|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((((op(e1,e1)=e2|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0))&((op(e2,e2)=e1|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))&((~(op(e1,e2)=e1)|(~(op(e1,e1)=e1)|(~(op(e1,e0)=e1)|(~(op(e0,e4)=e0)|epred6_0))))|~(epred7_0)))))),inference(distribute,[status(thm)],[564])).
% cnf(611,plain,(epred6_0|op(e0,e0)=e4|op(e0,e0)=e1|op(e1,e1)=e1|~epred7_0|op(e1,e2)!=e1),inference(split_conjunct,[status(thm)],[565])).
% cnf(613,plain,(epred6_0|op(e0,e0)=e4|op(e0,e0)=e1|op(e1,e1)=e1|op(e1,e1)=e2|~epred7_0),inference(split_conjunct,[status(thm)],[565])).
% fof(620, plain,(~(epred8_0)|(((epred7_0|((op(e1,e1)=e3&op(e3,e3)=e1)&~(op(e1,e3)=e1)))|((op(e1,e1)=e4&op(e4,e4)=e1)&~(op(e1,e4)=e1)))|((op(e2,e2)=e0&op(e0,e0)=e2)&~(op(e2,e0)=e2)))),inference(fof_nnf,[status(thm)],[23])).
% fof(621, plain,((((((((op(e2,e2)=e0|(op(e1,e1)=e4|(op(e1,e1)=e3|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(op(e1,e1)=e4|(op(e1,e1)=e3|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(op(e1,e1)=e4|(op(e1,e1)=e3|epred7_0)))|~(epred8_0)))&((((op(e2,e2)=e0|(op(e4,e4)=e1|(op(e1,e1)=e3|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(op(e4,e4)=e1|(op(e1,e1)=e3|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(op(e4,e4)=e1|(op(e1,e1)=e3|epred7_0)))|~(epred8_0))))&((((op(e2,e2)=e0|(~(op(e1,e4)=e1)|(op(e1,e1)=e3|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(~(op(e1,e4)=e1)|(op(e1,e1)=e3|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(~(op(e1,e4)=e1)|(op(e1,e1)=e3|epred7_0)))|~(epred8_0))))&((((((op(e2,e2)=e0|(op(e1,e1)=e4|(op(e3,e3)=e1|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(op(e1,e1)=e4|(op(e3,e3)=e1|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(op(e1,e1)=e4|(op(e3,e3)=e1|epred7_0)))|~(epred8_0)))&((((op(e2,e2)=e0|(op(e4,e4)=e1|(op(e3,e3)=e1|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(op(e4,e4)=e1|(op(e3,e3)=e1|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(op(e4,e4)=e1|(op(e3,e3)=e1|epred7_0)))|~(epred8_0))))&((((op(e2,e2)=e0|(~(op(e1,e4)=e1)|(op(e3,e3)=e1|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(~(op(e1,e4)=e1)|(op(e3,e3)=e1|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(~(op(e1,e4)=e1)|(op(e3,e3)=e1|epred7_0)))|~(epred8_0)))))&((((((op(e2,e2)=e0|(op(e1,e1)=e4|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(op(e1,e1)=e4|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(op(e1,e1)=e4|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0)))&((((op(e2,e2)=e0|(op(e4,e4)=e1|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(op(e4,e4)=e1|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(op(e4,e4)=e1|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0))))&((((op(e2,e2)=e0|(~(op(e1,e4)=e1)|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0))&((op(e0,e0)=e2|(~(op(e1,e4)=e1)|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0)))&((~(op(e2,e0)=e2)|(~(op(e1,e4)=e1)|(~(op(e1,e3)=e1)|epred7_0)))|~(epred8_0))))),inference(distribute,[status(thm)],[620])).
% cnf(648,plain,(epred7_0|op(e1,e1)=e3|op(e1,e1)=e4|op(e2,e2)=e0|~epred8_0),inference(split_conjunct,[status(thm)],[621])).
% fof(649, plain,(~(epred9_0)|((((epred8_0|((op(e2,e2)=e1&op(e1,e1)=e2)&~(op(e2,e1)=e2)))|(op(e2,e2)=e2&~(op(e2,e2)=e2)))|((op(e2,e2)=e3&op(e3,e3)=e2)&~(op(e2,e3)=e2)))|((op(e2,e2)=e4&op(e4,e4)=e2)&~(op(e2,e4)=e2)))),inference(fof_nnf,[status(thm)],[24])).
% fof(650, plain,(((((((((op(e2,e2)=e4|(op(e2,e2)=e3|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e2,e2)=e3|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e2,e2)=e3|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))&((((op(e2,e2)=e4|(op(e3,e3)=e2|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e3,e3)=e2|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e3,e3)=e2|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))))&((((op(e2,e2)=e4|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))))&((((((op(e2,e2)=e4|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))&((((op(e2,e2)=e4|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))))&((((op(e2,e2)=e4|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(op(e2,e2)=e1|epred8_0))))|~(epred9_0)))))&(((((((op(e2,e2)=e4|(op(e2,e2)=e3|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e2,e2)=e3|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e2,e2)=e3|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0)))&((((op(e2,e2)=e4|(op(e3,e3)=e2|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e3,e3)=e2|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e3,e3)=e2|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))))&((((op(e2,e2)=e4|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))))&((((((op(e2,e2)=e4|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0)))&((((op(e2,e2)=e4|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))))&((((op(e2,e2)=e4|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(op(e1,e1)=e2|epred8_0))))|~(epred9_0))))))&(((((((op(e2,e2)=e4|(op(e2,e2)=e3|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e2,e2)=e3|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e2,e2)=e3|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))&((((op(e2,e2)=e4|(op(e3,e3)=e2|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e3,e3)=e2|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e3,e3)=e2|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))))&((((op(e2,e2)=e4|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(~(op(e2,e3)=e2)|(op(e2,e2)=e2|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))))&((((((op(e2,e2)=e4|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e2,e2)=e3|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))&((((op(e2,e2)=e4|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(op(e3,e3)=e2|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))))&((((op(e2,e2)=e4|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0))&((op(e4,e4)=e2|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))&((~(op(e2,e4)=e2)|(~(op(e2,e3)=e2)|(~(op(e2,e2)=e2)|(~(op(e2,e1)=e2)|epred8_0))))|~(epred9_0)))))),inference(distribute,[status(thm)],[649])).
% cnf(701,plain,(epred8_0|op(e2,e2)=e1|op(e2,e2)=e2|op(e3,e3)=e2|op(e2,e2)=e4|~epred9_0),inference(split_conjunct,[status(thm)],[650])).
% fof(705, plain,(~(epred10_0)|(((epred9_0|((op(e3,e3)=e0&op(e0,e0)=e3)&~(op(e3,e0)=e3)))|((op(e3,e3)=e1&op(e1,e1)=e3)&~(op(e3,e1)=e3)))|((op(e3,e3)=e2&op(e2,e2)=e3)&~(op(e3,e2)=e3)))),inference(fof_nnf,[status(thm)],[25])).
% fof(706, plain,((((((((op(e3,e3)=e2|(op(e3,e3)=e1|(op(e3,e3)=e0|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(op(e3,e3)=e1|(op(e3,e3)=e0|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(op(e3,e3)=e1|(op(e3,e3)=e0|epred9_0)))|~(epred10_0)))&((((op(e3,e3)=e2|(op(e1,e1)=e3|(op(e3,e3)=e0|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(op(e1,e1)=e3|(op(e3,e3)=e0|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(op(e1,e1)=e3|(op(e3,e3)=e0|epred9_0)))|~(epred10_0))))&((((op(e3,e3)=e2|(~(op(e3,e1)=e3)|(op(e3,e3)=e0|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(~(op(e3,e1)=e3)|(op(e3,e3)=e0|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(~(op(e3,e1)=e3)|(op(e3,e3)=e0|epred9_0)))|~(epred10_0))))&((((((op(e3,e3)=e2|(op(e3,e3)=e1|(op(e0,e0)=e3|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(op(e3,e3)=e1|(op(e0,e0)=e3|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(op(e3,e3)=e1|(op(e0,e0)=e3|epred9_0)))|~(epred10_0)))&((((op(e3,e3)=e2|(op(e1,e1)=e3|(op(e0,e0)=e3|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(op(e1,e1)=e3|(op(e0,e0)=e3|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(op(e1,e1)=e3|(op(e0,e0)=e3|epred9_0)))|~(epred10_0))))&((((op(e3,e3)=e2|(~(op(e3,e1)=e3)|(op(e0,e0)=e3|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(~(op(e3,e1)=e3)|(op(e0,e0)=e3|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(~(op(e3,e1)=e3)|(op(e0,e0)=e3|epred9_0)))|~(epred10_0)))))&((((((op(e3,e3)=e2|(op(e3,e3)=e1|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(op(e3,e3)=e1|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(op(e3,e3)=e1|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0)))&((((op(e3,e3)=e2|(op(e1,e1)=e3|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(op(e1,e1)=e3|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(op(e1,e1)=e3|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0))))&((((op(e3,e3)=e2|(~(op(e3,e1)=e3)|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0))&((op(e2,e2)=e3|(~(op(e3,e1)=e3)|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0)))&((~(op(e3,e2)=e3)|(~(op(e3,e1)=e3)|(~(op(e3,e0)=e3)|epred9_0)))|~(epred10_0))))),inference(distribute,[status(thm)],[705])).
% cnf(733,plain,(epred9_0|op(e3,e3)=e0|op(e3,e3)=e1|op(e3,e3)=e2|~epred10_0),inference(split_conjunct,[status(thm)],[706])).
% fof(734, plain,(~(epred11_0)|((((epred10_0|(op(e3,e3)=e3&~(op(e3,e3)=e3)))|((op(e3,e3)=e4&op(e4,e4)=e3)&~(op(e3,e4)=e3)))|((op(e4,e4)=e0&op(e0,e0)=e4)&~(op(e4,e0)=e4)))|((op(e4,e4)=e1&op(e1,e1)=e4)&~(op(e4,e1)=e4)))),inference(fof_nnf,[status(thm)],[26])).
% fof(735, plain,(((((((((op(e4,e4)=e1|(op(e4,e4)=e0|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e4,e4)=e0|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e4,e4)=e0|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((((op(e4,e4)=e1|(op(e0,e0)=e4|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e0,e0)=e4|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e0,e0)=e4|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))))&((((op(e4,e4)=e1|(~(op(e4,e0)=e4)|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(~(op(e4,e0)=e4)|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(~(op(e4,e0)=e4)|(op(e3,e3)=e4|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))))&((((((op(e4,e4)=e1|(op(e4,e4)=e0|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e4,e4)=e0|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e4,e4)=e0|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((((op(e4,e4)=e1|(op(e0,e0)=e4|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e0,e0)=e4|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e0,e0)=e4|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))))&((((op(e4,e4)=e1|(~(op(e4,e0)=e4)|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(~(op(e4,e0)=e4)|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(~(op(e4,e0)=e4)|(op(e4,e4)=e3|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))))&((((((op(e4,e4)=e1|(op(e4,e4)=e0|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e4,e4)=e0|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e4,e4)=e0|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((((op(e4,e4)=e1|(op(e0,e0)=e4|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e0,e0)=e4|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e0,e0)=e4|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))))&((((op(e4,e4)=e1|(~(op(e4,e0)=e4)|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(~(op(e4,e0)=e4)|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(~(op(e4,e0)=e4)|(~(op(e3,e4)=e3)|(op(e3,e3)=e3|epred10_0))))|~(epred11_0)))))&((((((((op(e4,e4)=e1|(op(e4,e4)=e0|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e4,e4)=e0|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e4,e4)=e0|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((((op(e4,e4)=e1|(op(e0,e0)=e4|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e0,e0)=e4|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e0,e0)=e4|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))))&((((op(e4,e4)=e1|(~(op(e4,e0)=e4)|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(~(op(e4,e0)=e4)|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(~(op(e4,e0)=e4)|(op(e3,e3)=e4|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))))&((((((op(e4,e4)=e1|(op(e4,e4)=e0|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e4,e4)=e0|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e4,e4)=e0|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((((op(e4,e4)=e1|(op(e0,e0)=e4|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e0,e0)=e4|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e0,e0)=e4|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))))&((((op(e4,e4)=e1|(~(op(e4,e0)=e4)|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(~(op(e4,e0)=e4)|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(~(op(e4,e0)=e4)|(op(e4,e4)=e3|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))))&((((((op(e4,e4)=e1|(op(e4,e4)=e0|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e4,e4)=e0|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e4,e4)=e0|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((((op(e4,e4)=e1|(op(e0,e0)=e4|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(op(e0,e0)=e4|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(op(e0,e0)=e4|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))))&((((op(e4,e4)=e1|(~(op(e4,e0)=e4)|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0))&((op(e1,e1)=e4|(~(op(e4,e0)=e4)|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))&((~(op(e4,e1)=e4)|(~(op(e4,e0)=e4)|(~(op(e3,e4)=e3)|(~(op(e3,e3)=e3)|epred10_0))))|~(epred11_0)))))),inference(distribute,[status(thm)],[734])).
% cnf(776,plain,(epred10_0|op(e3,e3)=e3|op(e4,e4)=e3|op(e0,e0)=e4|op(e1,e1)=e4|~epred11_0),inference(split_conjunct,[status(thm)],[735])).
% cnf(779,plain,(epred10_0|op(e3,e3)=e3|op(e4,e4)=e3|op(e4,e4)=e0|op(e1,e1)=e4|~epred11_0),inference(split_conjunct,[status(thm)],[735])).
% cnf(790,plain,(op(e2,e3)!=e3),inference(rw,[status(thm)],[135,214,theory(equality)])).
% cnf(792,plain,(op(e3,e2)=e1),inference(rw,[status(thm)],[215,214,theory(equality)])).
% cnf(796,plain,(op(e3,e3)=e4),inference(rw,[status(thm)],[inference(rw,[status(thm)],[213,214,theory(equality)]),214,theory(equality)])).
% cnf(802,plain,(op(e3,e4)!=e1),inference(rw,[status(thm)],[124,792,theory(equality)])).
% cnf(803,plain,(op(e3,e4)!=e4),inference(rw,[status(thm)],[123,796,theory(equality)])).
% cnf(805,plain,(op(e2,e3)=e2|$false|~epred4_0),inference(rw,[status(thm)],[431,214,theory(equality)])).
% cnf(806,plain,(op(e2,e3)=e2|~epred4_0),inference(cn,[status(thm)],[805,theory(equality)])).
% cnf(809,plain,(op(e4,e3)!=e4),inference(rw,[status(thm)],[173,796,theory(equality)])).
% cnf(814,plain,(e1=e4|op(e3,e4)!=e2|~epred3_0),inference(rw,[status(thm)],[365,792,theory(equality)])).
% cnf(815,plain,(op(e3,e4)!=e2|~epred3_0),inference(sr,[status(thm)],[814,220,theory(equality)])).
% cnf(824,plain,(e3!=op(e2,e1)),inference(rw,[status(thm)],[138,214,theory(equality)])).
% cnf(825,plain,(op(e3,e4)=e3|$false|~epred5_0),inference(rw,[status(thm)],[471,796,theory(equality)])).
% cnf(826,plain,(op(e3,e4)=e3|~epred5_0),inference(cn,[status(thm)],[825,theory(equality)])).
% cnf(828,plain,(op(e4,e4)!=e3|~epred4_0),inference(sr,[status(thm)],[407,809,theory(equality)])).
% cnf(833,plain,(e1!=op(e3,e1)),inference(rw,[status(thm)],[128,792,theory(equality)])).
% cnf(836,plain,(e4!=op(e3,e0)),inference(rw,[status(thm)],[130,796,theory(equality)])).
% cnf(837,plain,(e4!=op(e3,e1)),inference(rw,[status(thm)],[127,796,theory(equality)])).
% cnf(852,plain,(op(e3,e4)!=e0|~epred1_0),inference(sr,[status(thm)],[261,836,theory(equality)])).
% cnf(853,plain,(op(e3,e1)=e2|$false|~epred2_0),inference(rw,[status(thm)],[317,792,theory(equality)])).
% cnf(854,plain,(op(e3,e1)=e2|~epred2_0),inference(cn,[status(thm)],[853,theory(equality)])).
% cnf(858,plain,(e1=e0|op(e3,e0)!=e2|~epred3_0),inference(rw,[status(thm)],[373,792,theory(equality)])).
% cnf(859,plain,(op(e3,e0)!=e2|~epred3_0),inference(sr,[status(thm)],[858,226,theory(equality)])).
% cnf(867,plain,(e4=e1|op(e3,e1)!=e3|~epred4_0),inference(rw,[status(thm)],[423,796,theory(equality)])).
% cnf(868,plain,(op(e3,e1)!=e3|~epred4_0),inference(sr,[status(thm)],[867,220,theory(equality)])).
% cnf(929,negated_conjecture,(e3=e4|op(e4,e4)=e3|op(e4,e4)=e4|epred11_0),inference(rw,[status(thm)],[240,214,theory(equality)])).
% cnf(930,negated_conjecture,(op(e4,e4)=e3|op(e4,e4)=e4|epred11_0),inference(sr,[status(thm)],[929,217,theory(equality)])).
% cnf(947,negated_conjecture,(e3=e4|op(e4,e4)=e3|epred11_0|op(e4,e4)!=e4),inference(rw,[status(thm)],[239,214,theory(equality)])).
% cnf(948,negated_conjecture,(op(e4,e4)=e3|epred11_0|op(e4,e4)!=e4),inference(sr,[status(thm)],[947,217,theory(equality)])).
% cnf(949,negated_conjecture,(op(e4,e4)=e3|epred11_0),inference(csr,[status(thm)],[948,930])).
% cnf(973,plain,(op(e1,e1)=e0),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[216,214,theory(equality)]),792,theory(equality)]),214,theory(equality)]),792,theory(equality)])).
% cnf(975,plain,(op(e3,e1)!=e0),inference(rw,[status(thm)],[197,973,theory(equality)])).
% cnf(976,plain,(e0!=op(e2,e1)),inference(rw,[status(thm)],[198,973,theory(equality)])).
% cnf(989,plain,($false|unit!=e0|~epred1_0),inference(rw,[status(thm)],[286,973,theory(equality)])).
% cnf(990,plain,(unit!=e0|~epred1_0),inference(cn,[status(thm)],[989,theory(equality)])).
% cnf(999,plain,(e4=e0|op(e3,e3)=e1|op(e3,e3)=e2|epred9_0|~epred10_0),inference(rw,[status(thm)],[733,796,theory(equality)])).
% cnf(1000,plain,(e4=e0|e4=e1|op(e3,e3)=e2|epred9_0|~epred10_0),inference(rw,[status(thm)],[999,796,theory(equality)])).
% cnf(1001,plain,(e4=e0|e4=e1|e4=e2|epred9_0|~epred10_0),inference(rw,[status(thm)],[1000,796,theory(equality)])).
% cnf(1002,plain,(e4=e1|e4=e2|epred9_0|~epred10_0),inference(sr,[status(thm)],[1001,223,theory(equality)])).
% cnf(1003,plain,(e4=e2|epred9_0|~epred10_0),inference(sr,[status(thm)],[1002,220,theory(equality)])).
% cnf(1004,plain,(epred9_0|~epred10_0),inference(sr,[status(thm)],[1003,218,theory(equality)])).
% cnf(1095,plain,(op(e3,e0)=e2|op(e3,e1)=e2|e1=e2|op(e3,e3)=e2|op(e3,e4)=e2),inference(rw,[status(thm)],[78,792,theory(equality)])).
% cnf(1096,plain,(op(e3,e0)=e2|op(e3,e1)=e2|e1=e2|e4=e2|op(e3,e4)=e2),inference(rw,[status(thm)],[1095,796,theory(equality)])).
% cnf(1097,plain,(op(e3,e0)=e2|op(e3,e1)=e2|e4=e2|op(e3,e4)=e2),inference(sr,[status(thm)],[1096,222,theory(equality)])).
% cnf(1098,plain,(op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e4)=e2),inference(sr,[status(thm)],[1097,218,theory(equality)])).
% cnf(1122,plain,(op(e3,e4)=e0|op(e3,e4)=e2|op(e3,e4)=e3|op(e3,e4)=e4),inference(sr,[status(thm)],[32,802,theory(equality)])).
% cnf(1123,plain,(op(e3,e4)=e0|op(e3,e4)=e2|op(e3,e4)=e3),inference(sr,[status(thm)],[1122,803,theory(equality)])).
% cnf(1125,plain,(e0=e3|op(e1,e1)=e4|op(e2,e2)=e0|epred7_0|~epred8_0),inference(rw,[status(thm)],[648,973,theory(equality)])).
% cnf(1126,plain,(e0=e3|e0=e4|op(e2,e2)=e0|epred7_0|~epred8_0),inference(rw,[status(thm)],[1125,973,theory(equality)])).
% cnf(1127,plain,(e0=e3|e0=e4|e3=e0|epred7_0|~epred8_0),inference(rw,[status(thm)],[1126,214,theory(equality)])).
% cnf(1128,plain,(e0=e3|e0=e4|epred7_0|~epred8_0),inference(cn,[status(thm)],[1127,theory(equality)])).
% cnf(1129,plain,(e4=e0|epred7_0|~epred8_0),inference(sr,[status(thm)],[1128,224,theory(equality)])).
% cnf(1130,plain,(epred7_0|~epred8_0),inference(sr,[status(thm)],[1129,223,theory(equality)])).
% cnf(1251,plain,(e3=e1|op(e2,e2)=e2|op(e2,e2)=e4|op(e3,e3)=e2|epred8_0|~epred9_0),inference(rw,[status(thm)],[701,214,theory(equality)])).
% cnf(1252,plain,(e3=e1|e3=e2|op(e2,e2)=e4|op(e3,e3)=e2|epred8_0|~epred9_0),inference(rw,[status(thm)],[1251,214,theory(equality)])).
% cnf(1253,plain,(e3=e1|e3=e2|e3=e4|op(e3,e3)=e2|epred8_0|~epred9_0),inference(rw,[status(thm)],[1252,214,theory(equality)])).
% cnf(1254,plain,(e3=e1|e3=e2|e3=e4|e4=e2|epred8_0|~epred9_0),inference(rw,[status(thm)],[1253,796,theory(equality)])).
% cnf(1255,plain,(e3=e2|e4=e3|e4=e2|epred8_0|~epred9_0),inference(sr,[status(thm)],[1254,221,theory(equality)])).
% cnf(1256,plain,(e4=e3|e4=e2|epred8_0|~epred9_0),inference(sr,[status(thm)],[1255,219,theory(equality)])).
% cnf(1257,plain,(e4=e2|epred8_0|~epred9_0),inference(sr,[status(thm)],[1256,217,theory(equality)])).
% cnf(1258,plain,(epred8_0|~epred9_0),inference(sr,[status(thm)],[1257,218,theory(equality)])).
% cnf(1454,plain,(e0=e4|op(e3,e3)=e3|op(e4,e4)=e0|op(e4,e4)=e3|epred10_0|~epred11_0),inference(rw,[status(thm)],[779,973,theory(equality)])).
% cnf(1455,plain,(e0=e4|e4=e3|op(e4,e4)=e0|op(e4,e4)=e3|epred10_0|~epred11_0),inference(rw,[status(thm)],[1454,796,theory(equality)])).
% cnf(1456,plain,(e4=e3|op(e4,e4)=e0|op(e4,e4)=e3|epred10_0|~epred11_0),inference(sr,[status(thm)],[1455,223,theory(equality)])).
% cnf(1457,plain,(op(e4,e4)=e0|op(e4,e4)=e3|epred10_0|~epred11_0),inference(sr,[status(thm)],[1456,217,theory(equality)])).
% cnf(1458,plain,(op(e4,e4)=e0|op(e4,e4)=e3|epred10_0),inference(csr,[status(thm)],[1457,949])).
% cnf(1502,plain,(op(e0,e0)=e0|op(e0,e0)=e1|e3=e0|op(e3,e3)=e0|~epred6_0),inference(rw,[status(thm)],[559,214,theory(equality)])).
% cnf(1503,plain,(op(e0,e0)=e0|op(e0,e0)=e1|e3=e0|e4=e0|~epred6_0),inference(rw,[status(thm)],[1502,796,theory(equality)])).
% cnf(1504,plain,(op(e0,e0)=e0|op(e0,e0)=e1|e4=e0|~epred6_0),inference(sr,[status(thm)],[1503,224,theory(equality)])).
% cnf(1505,plain,(op(e0,e0)=e0|op(e0,e0)=e1|~epred6_0),inference(sr,[status(thm)],[1504,223,theory(equality)])).
% cnf(1644,plain,(op(e0,e0)=e1|op(e0,e0)=e4|e0=e1|op(e1,e1)=e2|epred6_0|~epred7_0),inference(rw,[status(thm)],[613,973,theory(equality)])).
% cnf(1645,plain,(op(e0,e0)=e1|op(e0,e0)=e4|e0=e1|e0=e2|epred6_0|~epred7_0),inference(rw,[status(thm)],[1644,973,theory(equality)])).
% cnf(1646,plain,(op(e0,e0)=e1|op(e0,e0)=e4|e2=e0|epred6_0|~epred7_0),inference(sr,[status(thm)],[1645,226,theory(equality)])).
% cnf(1647,plain,(op(e0,e0)=e1|op(e0,e0)=e4|epred6_0|~epred7_0),inference(sr,[status(thm)],[1646,225,theory(equality)])).
% cnf(1713,plain,(op(e0,e0)=e4|e0=e4|op(e3,e3)=e3|op(e4,e4)=e3|epred10_0|~epred11_0),inference(rw,[status(thm)],[776,973,theory(equality)])).
% cnf(1714,plain,(op(e0,e0)=e4|e0=e4|e4=e3|op(e4,e4)=e3|epred10_0|~epred11_0),inference(rw,[status(thm)],[1713,796,theory(equality)])).
% cnf(1715,plain,(op(e0,e0)=e4|e4=e3|op(e4,e4)=e3|epred10_0|~epred11_0),inference(sr,[status(thm)],[1714,223,theory(equality)])).
% cnf(1716,plain,(op(e0,e0)=e4|op(e4,e4)=e3|epred10_0|~epred11_0),inference(sr,[status(thm)],[1715,217,theory(equality)])).
% cnf(1717,plain,(op(e0,e0)=e4|op(e4,e4)=e3|epred10_0),inference(csr,[status(thm)],[1716,949])).
% cnf(1766,plain,(op(e0,e1)=e3|e0=e3|op(e2,e1)=e3|op(e3,e1)=e3|op(e4,e1)=e3),inference(rw,[status(thm)],[95,973,theory(equality)])).
% cnf(1767,plain,(op(e0,e1)=e3|op(e2,e1)=e3|op(e3,e1)=e3|op(e4,e1)=e3),inference(sr,[status(thm)],[1766,224,theory(equality)])).
% cnf(1768,plain,(op(e0,e1)=e3|op(e3,e1)=e3|op(e4,e1)=e3),inference(sr,[status(thm)],[1767,824,theory(equality)])).
% cnf(1810,plain,(op(e2,e0)=e0|op(e2,e1)=e0|e3=e0|op(e2,e3)=e0|op(e2,e4)=e0),inference(rw,[status(thm)],[92,214,theory(equality)])).
% cnf(1811,plain,(op(e2,e0)=e0|op(e2,e1)=e0|op(e2,e3)=e0|op(e2,e4)=e0),inference(sr,[status(thm)],[1810,224,theory(equality)])).
% cnf(1817,plain,(op(e3,e0)=e0|op(e3,e1)=e0|e1=e0|op(e3,e3)=e0|op(e3,e4)=e0),inference(rw,[status(thm)],[82,792,theory(equality)])).
% cnf(1818,plain,(op(e3,e0)=e0|op(e3,e1)=e0|e1=e0|e4=e0|op(e3,e4)=e0),inference(rw,[status(thm)],[1817,796,theory(equality)])).
% cnf(1819,plain,(op(e3,e0)=e0|op(e3,e1)=e0|e4=e0|op(e3,e4)=e0),inference(sr,[status(thm)],[1818,226,theory(equality)])).
% cnf(1820,plain,(op(e3,e0)=e0|op(e3,e1)=e0|op(e3,e4)=e0),inference(sr,[status(thm)],[1819,223,theory(equality)])).
% cnf(1827,plain,(op(e3,e1)=e0|op(e3,e1)=e2|op(e3,e1)=e3|op(e3,e1)=e4),inference(sr,[status(thm)],[35,833,theory(equality)])).
% cnf(1828,plain,(op(e3,e1)=e0|op(e3,e1)=e2|op(e3,e1)=e3),inference(sr,[status(thm)],[1827,837,theory(equality)])).
% cnf(1839,plain,(op(e0,e0)=e1|e3=e0|op(e3,e3)=e0|op(e0,e0)!=e0|~epred6_0),inference(rw,[status(thm)],[532,214,theory(equality)])).
% cnf(1840,plain,(op(e0,e0)=e1|e3=e0|e4=e0|op(e0,e0)!=e0|~epred6_0),inference(rw,[status(thm)],[1839,796,theory(equality)])).
% cnf(1841,plain,(op(e0,e0)=e1|e4=e0|op(e0,e0)!=e0|~epred6_0),inference(sr,[status(thm)],[1840,224,theory(equality)])).
% cnf(1842,plain,(op(e0,e0)=e1|op(e0,e0)!=e0|~epred6_0),inference(sr,[status(thm)],[1841,223,theory(equality)])).
% cnf(1843,plain,(op(e0,e0)=e1|~epred6_0),inference(csr,[status(thm)],[1842,1505])).
% cnf(1897,plain,(op(e0,e0)=e1|op(e0,e0)=e4|e0=e1|epred6_0|op(e1,e2)!=e1|~epred7_0),inference(rw,[status(thm)],[611,973,theory(equality)])).
% cnf(1898,plain,(op(e0,e0)=e1|op(e0,e0)=e4|epred6_0|op(e1,e2)!=e1|~epred7_0),inference(sr,[status(thm)],[1897,226,theory(equality)])).
% cnf(1899,plain,(op(e0,e0)=e1|op(e0,e0)=e4|epred6_0|~epred7_0),inference(csr,[status(thm)],[1898,1647])).
% cnf(1900,plain,(op(e0,e0)=e1|op(e0,e0)=e4|~epred7_0),inference(csr,[status(thm)],[1899,1843])).
% cnf(2128,plain,(op(e3,e4)=e0|op(e3,e0)=e0),inference(sr,[status(thm)],[1820,975,theory(equality)])).
% cnf(2129,plain,(op(e3,e1)=e3|op(e3,e1)=e2),inference(sr,[status(thm)],[1828,975,theory(equality)])).
% cnf(2130,plain,(op(e2,e4)=e0|op(e2,e3)=e0|op(e2,e0)=e0),inference(sr,[status(thm)],[1811,976,theory(equality)])).
% cnf(2142,negated_conjecture,(op(e3,e4)=e3|epred4_0|epred3_0|epred2_0|epred1_0),inference(spm,[status(thm)],[826,247,theory(equality)])).
% cnf(2182,plain,(op(e3,e4)=e0|op(e3,e4)=e2|e3!=op(e3,e1)),inference(spm,[status(thm)],[126,1123,theory(equality)])).
% cnf(2200,negated_conjecture,(op(e0,e4)=e0|epred4_0|epred3_0|epred2_0|epred1_0|op(e0,e0)!=e4),inference(spm,[status(thm)],[507,247,theory(equality)])).
% cnf(2211,plain,(op(e4,e4)=e0|epred10_0|e3!=op(e3,e4)),inference(spm,[status(thm)],[163,1458,theory(equality)])).
% cnf(2213,plain,(op(e4,e4)=e0|epred10_0|e3!=op(e4,e1)),inference(spm,[status(thm)],[116,1458,theory(equality)])).
% cnf(2292,plain,(op(e4,e0)=e0|unit=e0|unit=e1|unit=e2|unit=e3),inference(spm,[status(thm)],[62,52,theory(equality)])).
% cnf(2294,plain,(op(e3,e4)=e3|unit=e0|unit=e1|unit=e2|unit=e3),inference(spm,[status(thm)],[55,52,theory(equality)])).
% cnf(2913,negated_conjecture,(epred4_0|epred3_0|epred2_0|epred1_0|e3!=op(e3,e1)),inference(spm,[status(thm)],[126,2142,theory(equality)])).
% cnf(3107,negated_conjecture,(epred3_0|epred2_0|epred1_0|op(e3,e1)!=e3),inference(csr,[status(thm)],[2913,868])).
% cnf(3108,negated_conjecture,(epred3_0|epred2_0|epred1_0|op(e3,e1)=e2),inference(spm,[status(thm)],[3107,2129,theory(equality)])).
% cnf(3111,negated_conjecture,(op(e3,e1)=e2|epred3_0|epred1_0),inference(csr,[status(thm)],[3108,854])).
% cnf(3115,negated_conjecture,(epred3_0|epred1_0|e2!=op(e3,e0)),inference(spm,[status(thm)],[132,3111,theory(equality)])).
% cnf(3140,negated_conjecture,(epred1_0|op(e3,e0)!=e2),inference(csr,[status(thm)],[3115,859])).
% cnf(3239,plain,(op(e3,e4)=e2|op(e3,e4)=e0|op(e3,e1)=e2),inference(spm,[status(thm)],[2182,2129,theory(equality)])).
% cnf(3307,negated_conjecture,(op(e4,e4)=e0|epred10_0|epred4_0|epred3_0|epred2_0|epred1_0),inference(spm,[status(thm)],[2211,2142,theory(equality)])).
% cnf(3321,negated_conjecture,(epred10_0|epred4_0|epred3_0|epred2_0|epred1_0|e0!=op(e0,e4)),inference(spm,[status(thm)],[169,3307,theory(equality)])).
% cnf(3330,plain,(op(e0,e0)=e4|e0=e3|epred10_0|epred4_0|epred3_0|epred2_0|epred1_0),inference(spm,[status(thm)],[1717,3307,theory(equality)])).
% cnf(3340,plain,(op(e0,e0)=e4|epred10_0|epred4_0|epred3_0|epred2_0|epred1_0),inference(sr,[status(thm)],[3330,224,theory(equality)])).
% cnf(3487,negated_conjecture,(op(e0,e4)=e0|epred4_0|epred3_0|epred2_0|epred1_0|epred10_0),inference(spm,[status(thm)],[2200,3340,theory(equality)])).
% cnf(3527,plain,(op(e4,e4)=e0|epred10_0|op(e0,e1)=e3|op(e3,e1)=e3),inference(spm,[status(thm)],[2213,1768,theory(equality)])).
% cnf(3561,negated_conjecture,(epred10_0|epred4_0|epred3_0|epred2_0|epred1_0),inference(csr,[status(thm)],[3321,3487])).
% cnf(3567,plain,(op(e2,e3)=e2|epred10_0|epred3_0|epred2_0|epred1_0),inference(spm,[status(thm)],[806,3561,theory(equality)])).
% cnf(3572,plain,(epred10_0|epred3_0|epred2_0|epred1_0|op(e4,e4)!=e3),inference(spm,[status(thm)],[828,3561,theory(equality)])).
% cnf(3583,plain,(epred10_0|epred3_0|epred2_0|epred1_0|op(e4,e4)=e0),inference(spm,[status(thm)],[3572,1458,theory(equality)])).
% cnf(3599,plain,(epred10_0|epred3_0|epred2_0|epred1_0|e0!=op(e2,e4)),inference(spm,[status(thm)],[164,3583,theory(equality)])).
% cnf(3600,plain,(epred10_0|epred3_0|epred2_0|epred1_0|e0!=op(e3,e4)),inference(spm,[status(thm)],[163,3583,theory(equality)])).
% cnf(3643,plain,(epred10_0|epred3_0|epred2_0|epred1_0|op(e2,e3)=e0|op(e2,e0)=e0),inference(spm,[status(thm)],[3599,2130,theory(equality)])).
% cnf(3648,plain,(epred10_0|epred3_0|epred2_0|op(e3,e4)!=e0),inference(csr,[status(thm)],[3600,852])).
% cnf(3650,plain,(epred10_0|epred3_0|epred2_0|op(e3,e0)=e0),inference(spm,[status(thm)],[3648,2128,theory(equality)])).
% cnf(3661,plain,(epred10_0|epred3_0|epred2_0|e0!=op(e2,e0)),inference(spm,[status(thm)],[205,3650,theory(equality)])).
% cnf(4370,plain,(unit=e3|unit=e2|unit=e1|unit=e0|e0!=op(e3,e0)),inference(spm,[status(thm)],[203,2292,theory(equality)])).
% cnf(4460,plain,(e3=e0|op(e3,e0)=e0|unit=e3|unit=e2|unit=e1|unit=e0),inference(spm,[status(thm)],[2128,2294,theory(equality)])).
% cnf(4468,plain,(op(e3,e0)=e0|unit=e3|unit=e2|unit=e1|unit=e0),inference(sr,[status(thm)],[4460,224,theory(equality)])).
% cnf(4548,plain,(op(e2,e3)=e0|epred10_0|epred3_0|epred2_0|epred1_0),inference(csr,[status(thm)],[3643,3661])).
% cnf(4556,plain,(e0=e2|epred10_0|epred3_0|epred2_0|epred1_0),inference(spm,[status(thm)],[3567,4548,theory(equality)])).
% cnf(4558,plain,(epred10_0|epred3_0|epred2_0|epred1_0),inference(sr,[status(thm)],[4556,225,theory(equality)])).
% cnf(4570,plain,(epred10_0|epred2_0|epred1_0|op(e3,e4)!=e2),inference(spm,[status(thm)],[815,4558,theory(equality)])).
% cnf(4616,plain,(epred10_0|epred2_0|epred1_0|op(e3,e1)=e2|op(e3,e4)=e0),inference(spm,[status(thm)],[4570,3239,theory(equality)])).
% cnf(4649,plain,(op(e3,e4)=e0|op(e3,e1)=e2|epred10_0|epred1_0),inference(csr,[status(thm)],[4616,854])).
% cnf(4664,plain,(op(e3,e0)=e2|op(e3,e1)=e2|e0=e2|epred10_0|epred1_0),inference(spm,[status(thm)],[1098,4649,theory(equality)])).
% cnf(4670,plain,(op(e3,e0)=e2|op(e3,e1)=e2|epred10_0|epred1_0),inference(sr,[status(thm)],[4664,225,theory(equality)])).
% cnf(4677,plain,(op(e3,e1)=e2|epred10_0|epred1_0),inference(csr,[status(thm)],[4670,3140])).
% cnf(6703,plain,(op(e3,e1)=e3|op(e0,e1)=e3|epred10_0|e0!=op(e3,e4)),inference(spm,[status(thm)],[163,3527,theory(equality)])).
% cnf(15862,plain,(op(e0,e1)=e3|op(e3,e1)=e3|epred10_0|op(e3,e0)=e0),inference(spm,[status(thm)],[6703,2128,theory(equality)])).
% cnf(15910,plain,(e3=e2|epred10_0|epred1_0|op(e3,e0)=e0|op(e0,e1)=e3),inference(spm,[status(thm)],[4677,15862,theory(equality)])).
% cnf(15921,plain,(epred10_0|epred1_0|op(e3,e0)=e0|op(e0,e1)=e3),inference(sr,[status(thm)],[15910,219,theory(equality)])).
% cnf(15925,plain,(op(e0,e1)=e3|epred10_0|epred1_0|e0!=op(e0,e0)),inference(spm,[status(thm)],[210,15921,theory(equality)])).
% cnf(33992,plain,(unit=e3|unit=e2|unit=e1|unit=e0),inference(csr,[status(thm)],[4370,4468])).
% cnf(33996,plain,(op(e3,e4)=e4|unit=e0|unit=e1|unit=e2),inference(spm,[status(thm)],[54,33992,theory(equality)])).
% cnf(34020,plain,(unit=e0|unit=e1|unit=e2),inference(sr,[status(thm)],[33996,803,theory(equality)])).
% cnf(34034,plain,(op(e1,e1)=e1|unit=e2|unit=e0),inference(spm,[status(thm)],[60,34020,theory(equality)])).
% cnf(34055,plain,(e0=e1|unit=e2|unit=e0),inference(rw,[status(thm)],[34034,973,theory(equality)])).
% cnf(34056,plain,(unit=e2|unit=e0),inference(sr,[status(thm)],[34055,226,theory(equality)])).
% cnf(34063,plain,(op(e2,e3)=e3|unit=e0),inference(spm,[status(thm)],[56,34056,theory(equality)])).
% cnf(34086,plain,(unit=e0),inference(sr,[status(thm)],[34063,790,theory(equality)])).
% cnf(34108,plain,($false|~epred1_0),inference(rw,[status(thm)],[990,34086,theory(equality)])).
% cnf(34109,plain,(~epred1_0),inference(cn,[status(thm)],[34108,theory(equality)])).
% cnf(34110,plain,(op(e0,e0)=e0),inference(rw,[status(thm)],[61,34086,theory(equality)])).
% cnf(34116,plain,(op(e0,e1)=e1),inference(rw,[status(thm)],[60,34086,theory(equality)])).
% cnf(34488,plain,(op(e0,e1)=e3|epred10_0|epred1_0|$false),inference(rw,[status(thm)],[15925,34110,theory(equality)])).
% cnf(34489,plain,(op(e0,e1)=e3|epred10_0|epred1_0),inference(cn,[status(thm)],[34488,theory(equality)])).
% cnf(34490,plain,(op(e0,e1)=e3|epred10_0),inference(sr,[status(thm)],[34489,34109,theory(equality)])).
% cnf(34735,plain,(e0=e1|op(e0,e0)=e4|~epred7_0),inference(rw,[status(thm)],[1900,34110,theory(equality)])).
% cnf(34736,plain,(e0=e1|e0=e4|~epred7_0),inference(rw,[status(thm)],[34735,34110,theory(equality)])).
% cnf(34737,plain,(e4=e0|~epred7_0),inference(sr,[status(thm)],[34736,226,theory(equality)])).
% cnf(34738,plain,(~epred7_0),inference(sr,[status(thm)],[34737,223,theory(equality)])).
% cnf(36338,plain,(e1=e3|epred10_0),inference(rw,[status(thm)],[34490,34116,theory(equality)])).
% cnf(36339,plain,(epred10_0),inference(sr,[status(thm)],[36338,221,theory(equality)])).
% cnf(36343,plain,(epred9_0|$false),inference(rw,[status(thm)],[1004,36339,theory(equality)])).
% cnf(36344,plain,(epred9_0),inference(cn,[status(thm)],[36343,theory(equality)])).
% cnf(36346,plain,(epred8_0|$false),inference(rw,[status(thm)],[1258,36344,theory(equality)])).
% cnf(36347,plain,(epred8_0),inference(cn,[status(thm)],[36346,theory(equality)])).
% cnf(36354,plain,(epred7_0|$false),inference(rw,[status(thm)],[1130,36347,theory(equality)])).
% cnf(36355,plain,(epred7_0),inference(cn,[status(thm)],[36354,theory(equality)])).
% cnf(36356,plain,($false),inference(sr,[status(thm)],[36355,34738,theory(equality)])).
% cnf(36357,plain,($false),36356,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 6535
% # ...of these trivial : 158
% # ...subsumed : 4500
% # ...remaining for further processing: 1877
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 479
% # Backward-rewritten : 815
% # Generated clauses : 22653
% # ...of the previous two non-trivial : 22755
% # Contextual simplify-reflections : 5194
% # Paramodulations : 22249
% # Factorizations : 183
% # Equation resolutions : 0
% # Current number of processed clauses: 74
% # Positive orientable unit clauses: 26
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 38
% # Non-unit-clauses : 10
% # Current number of unprocessed clauses: 572
% # ...number of literals in the above : 2097
% # Clause-clause subsumption calls (NU) : 49675
% # Rec. Clause-clause subsumption calls : 9618
% # Unit Clause-clause subsumption calls : 1326
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 24
% # Indexed BW rewrite successes : 24
% # Backwards rewriting index: 43 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-from index: 27 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 42 leaves, 1.00+/-0.000 terms/leaf
% # -------------------------------------------------
% # User time : 1.663 s
% # System time : 0.044 s
% # Total time : 1.707 s
% # Maximum resident set size: 0 pages
% PrfWatch: 2.50 CPU 2.63 WC
% FINAL PrfWatch: 2.50 CPU 2.63 WC
% SZS output end Solution for /tmp/SystemOnTPTP3857/ALG058+1.tptp
%
%------------------------------------------------------------------------------