%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG068+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:49:33 AM UTC 2026
% Result : Theorem 0.20s 15.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG068+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/15.44 % Computer : n006.cluster.edu
% 0.15/15.44 % Model : x86_64 x86_64
% 0.15/15.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/15.44 % Memory : 8046.5625MB
% 0.15/15.44 % OS : Linux 6.8.0-71-generic
% 0.15/15.44 % CPULimit : 300
% 0.15/15.44 % WCLimit : 300
% 0.15/15.44 % DateTime : Mon Sep 21 12:55:12 UTC 2026
% 0.15/15.45 % CPUTime :
% 0.15/15.47 % Drodi V4.1.1
% 0.20/15.53 % Refutation found
% 0.20/15.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/15.53 % SZS output start CNFRefutation for theBenchmark
% 0.20/15.53 fof(f1,axiom,(
% 0.20/15.53 ( ( 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 ) ) ),
% 0.20/15.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.53 fof(f2,axiom,(
% 0.20/15.53 ( 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 ) ) ),
% 0.20/15.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.53 fof(f3,axiom,(
% 0.20/15.53 ( ( 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 ) ) ),
% 0.20/15.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.53 fof(f4,axiom,(
% 0.20/15.53 ( 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) ) ),
% 0.20/15.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.53 fof(f5,axiom,(
% 0.20/15.53 ( e0 != e1& e0 != e2& e0 != e3& e0 != e4& e1 != e2& e1 != e3& e1 != e4& e2 != e3& e2 != e4& e3 != e4 ) ),
% 0.20/15.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.53 fof(f6,axiom,(
% 0.20/15.53 ( e0 = op(op(e4,e2),op(e4,e2))& e1 = op(e4,e2)& e3 = op(e2,e4) ) ),
% 0.20/15.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.53 fof(f7,conjecture,(
% 0.20/15.53 ~ ( ( op(e0,e0) != e0| op(e0,e0) = e0 )& ( op(e0,e0) != e1| op(e0,e1) = e0 )& ( op(e0,e0) != e2| op(e0,e2) = e0 )& ( op(e0,e0) != e3| op(e0,e3) = e0 )& ( op(e0,e0) != e4| op(e0,e4) = e0 )& ( op(e1,e1) != e0| op(e1,e0) = e1 )& ( op(e1,e1) != e1| op(e1,e1) = e1 )& ( op(e1,e1) != e2| op(e1,e2) = e1 )& ( op(e1,e1) != e3| op(e1,e3) = e1 )& ( op(e1,e1) != e4| op(e1,e4) = e1 )& ( op(e2,e2) != e0| op(e2,e0) = e2 )& ( op(e2,e2) != e1| op(e2,e1) = e2 )& ( op(e2,e2) != e2| op(e2,e2) = e2 )& ( op(e2,e2) != e3| op(e2,e3) = e2 )& ( op(e2,e2) != e4| op(e2,e4) = e2 )& ( op(e3,e3) != e0| op(e3,e0) = e3 )& ( op(e3,e3) != e1| op(e3,e1) = e3 )& ( op(e3,e3) != e2| op(e3,e2) = e3 )& ( op(e3,e3) != e3| op(e3,e3) = e3 )& ( op(e3,e3) != e4| op(e3,e4) = e3 )& ( op(e4,e4) != e0| op(e4,e0) = e4 )& ( op(e4,e4) != e1| op(e4,e1) = e4 )& ( op(e4,e4) != e2| op(e4,e2) = e4 )& ( op(e4,e4) != e3| op(e4,e3) = e4 )& ( op(e4,e4) != e4| op(e4,e4) = e4 )& ( ( op(e0,e0) != op(e0,e0)& op(op(e0,e0),e0) = e0& op(op(e0,e0),e0) != e0 )| ( op(e1,e0) != op(e0,e1)& op(op(e0,e1),e1) = e0& op(op(e0,e1),e0) != e1 )| ( op(e2,e0) != op(e0,e2)& op(op(e0,e2),e2) = e0& op(op(e0,e2),e0) != e2 )| ( op(e3,e0) != op(e0,e3)& op(op(e0,e3),e3) = e0& op(op(e0,e3),e0) != e3 )| ( op(e4,e0) != op(e0,e4)& op(op(e0,e4),e4) = e0& op(op(e0,e4),e0) != e4 )| ( op(e0,e1) != op(e1,e0)& op(op(e1,e0),e0) = e1& op(op(e1,e0),e1) != e0 )| ( op(e1,e1) != op(e1,e1)& op(op(e1,e1),e1) = e1& op(op(e1,e1),e1) != e1 )| ( op(e2,e1) != op(e1,e2)& op(op(e1,e2),e2) = e1& op(op(e1,e2),e1) != e2 )| ( op(e3,e1) != op(e1,e3)& op(op(e1,e3),e3) = e1& op(op(e1,e3),e1) != e3 )| ( op(e4,e1) != op(e1,e4)& op(op(e1,e4),e4) = e1& op(op(e1,e4),e1) != e4 )| ( op(e0,e2) != op(e2,e0)& op(op(e2,e0),e0) = e2& op(op(e2,e0),e2) != e0 )| ( op(e1,e2) != op(e2,e1)& op(op(e2,e1),e1) = e2& op(op(e2,e1),e2) != e1 )| ( op(e2,e2) != op(e2,e2)& op(op(e2,e2),e2) = e2& op(op(e2,e2),e2) != e2 )| ( op(e3,e2) != op(e2,e3)& op(op(e2,e3),e3) = e2& op(op(e2,e3),e2) != e3 )| ( op(e4,e2) != op(e2,e4)& op(op(e2,e4),e4) = e2& op(op(e2,e4),e2) != e4 )| ( op(e0,e3) != op(e3,e0)& op(op(e3,e0),e0) = e3& op(op(e3,e0),e3) != e0 )| ( op(e1,e3) != op(e3,e1)& op(op(e3,e1),e1) = e3& op(op(e3,e1),e3) != e1 )| ( op(e2,e3) != op(e3,e2)& op(op(e3,e2),e2) = e3& op(op(e3,e2),e3) != e2 )| ( op(e3,e3) != op(e3,e3)& op(op(e3,e3),e3) = e3& op(op(e3,e3),e3) != e3 )| ( op(e4,e3) != op(e3,e4)& op(op(e3,e4),e4) = e3& op(op(e3,e4),e3) != e4 )| ( op(e0,e4) != op(e4,e0)& op(op(e4,e0),e0) = e4& op(op(e4,e0),e4) != e0 )| ( op(e1,e4) != op(e4,e1)& op(op(e4,e1),e1) = e4& op(op(e4,e1),e4) != e1 )| ( op(e2,e4) != op(e4,e2)& op(op(e4,e2),e2) = e4& op(op(e4,e2),e4) != e2 )| ( op(e3,e4) != op(e4,e3)& op(op(e4,e3),e3) = e4& op(op(e4,e3),e4) != e3 )| ( op(e4,e4) != op(e4,e4)& op(op(e4,e4),e4) = e4& op(op(e4,e4),e4) != e4 ) ) ) ),
% 0.20/15.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.53 fof(f8,negated_conjecture,(
% 0.20/15.53 ~(~ ( ( op(e0,e0) != e0| op(e0,e0) = e0 )& ( op(e0,e0) != e1| op(e0,e1) = e0 )& ( op(e0,e0) != e2| op(e0,e2) = e0 )& ( op(e0,e0) != e3| op(e0,e3) = e0 )& ( op(e0,e0) != e4| op(e0,e4) = e0 )& ( op(e1,e1) != e0| op(e1,e0) = e1 )& ( op(e1,e1) != e1| op(e1,e1) = e1 )& ( op(e1,e1) != e2| op(e1,e2) = e1 )& ( op(e1,e1) != e3| op(e1,e3) = e1 )& ( op(e1,e1) != e4| op(e1,e4) = e1 )& ( op(e2,e2) != e0| op(e2,e0) = e2 )& ( op(e2,e2) != e1| op(e2,e1) = e2 )& ( op(e2,e2) != e2| op(e2,e2) = e2 )& ( op(e2,e2) != e3| op(e2,e3) = e2 )& ( op(e2,e2) != e4| op(e2,e4) = e2 )& ( op(e3,e3) != e0| op(e3,e0) = e3 )& ( op(e3,e3) != e1| op(e3,e1) = e3 )& ( op(e3,e3) != e2| op(e3,e2) = e3 )& ( op(e3,e3) != e3| op(e3,e3) = e3 )& ( op(e3,e3) != e4| op(e3,e4) = e3 )& ( op(e4,e4) != e0| op(e4,e0) = e4 )& ( op(e4,e4) != e1| op(e4,e1) = e4 )& ( op(e4,e4) != e2| op(e4,e2) = e4 )& ( op(e4,e4) != e3| op(e4,e3) = e4 )& ( op(e4,e4) != e4| op(e4,e4) = e4 )& ( ( op(e0,e0) != op(e0,e0)& op(op(e0,e0),e0) = e0& op(op(e0,e0),e0) != e0 )| ( op(e1,e0) != op(e0,e1)& op(op(e0,e1),e1) = e0& op(op(e0,e1),e0) != e1 )| ( op(e2,e0) != op(e0,e2)& op(op(e0,e2),e2) = e0& op(op(e0,e2),e0) != e2 )| ( op(e3,e0) != op(e0,e3)& op(op(e0,e3),e3) = e0& op(op(e0,e3),e0) != e3 )| ( op(e4,e0) != op(e0,e4)& op(op(e0,e4),e4) = e0& op(op(e0,e4),e0) != e4 )| ( op(e0,e1) != op(e1,e0)& op(op(e1,e0),e0) = e1& op(op(e1,e0),e1) != e0 )| ( op(e1,e1) != op(e1,e1)& op(op(e1,e1),e1) = e1& op(op(e1,e1),e1) != e1 )| ( op(e2,e1) != op(e1,e2)& op(op(e1,e2),e2) = e1& op(op(e1,e2),e1) != e2 )| ( op(e3,e1) != op(e1,e3)& op(op(e1,e3),e3) = e1& op(op(e1,e3),e1) != e3 )| ( op(e4,e1) != op(e1,e4)& op(op(e1,e4),e4) = e1& op(op(e1,e4),e1) != e4 )| ( op(e0,e2) != op(e2,e0)& op(op(e2,e0),e0) = e2& op(op(e2,e0),e2) != e0 )| ( op(e1,e2) != op(e2,e1)& op(op(e2,e1),e1) = e2& op(op(e2,e1),e2) != e1 )| ( op(e2,e2) != op(e2,e2)& op(op(e2,e2),e2) = e2& op(op(e2,e2),e2) != e2 )| ( op(e3,e2) != op(e2,e3)& op(op(e2,e3),e3) = e2& op(op(e2,e3),e2) != e3 )| ( op(e4,e2) != op(e2,e4)& op(op(e2,e4),e4) = e2& op(op(e2,e4),e2) != e4 )| ( op(e0,e3) != op(e3,e0)& op(op(e3,e0),e0) = e3& op(op(e3,e0),e3) != e0 )| ( op(e1,e3) != op(e3,e1)& op(op(e3,e1),e1) = e3& op(op(e3,e1),e3) != e1 )| ( op(e2,e3) != op(e3,e2)& op(op(e3,e2),e2) = e3& op(op(e3,e2),e3) != e2 )| ( op(e3,e3) != op(e3,e3)& op(op(e3,e3),e3) = e3& op(op(e3,e3),e3) != e3 )| ( op(e4,e3) != op(e3,e4)& op(op(e3,e4),e4) = e3& op(op(e3,e4),e3) != e4 )| ( op(e0,e4) != op(e4,e0)& op(op(e4,e0),e0) = e4& op(op(e4,e0),e4) != e0 )| ( op(e1,e4) != op(e4,e1)& op(op(e4,e1),e1) = e4& op(op(e4,e1),e4) != e1 )| ( op(e2,e4) != op(e4,e2)& op(op(e4,e2),e2) = e4& op(op(e4,e2),e4) != e2 )| ( op(e3,e4) != op(e4,e3)& op(op(e4,e3),e3) = e4& op(op(e4,e3),e4) != e3 )| ( op(e4,e4) != op(e4,e4)& op(op(e4,e4),e4) = e4& op(op(e4,e4),e4) != e4 ) ) ) )),
% 0.20/15.53 inference(negated_conjecture,[status(cth)],[f7])).
% 0.20/15.53 fof(f16,plain,(
% 0.20/15.53 op(e1,e2)=e0|op(e1,e2)=e1|op(e1,e2)=e2|op(e1,e2)=e3|op(e1,e2)=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f1])).
% 0.20/15.53 fof(f17,plain,(
% 0.20/15.53 op(e1,e3)=e0|op(e1,e3)=e1|op(e1,e3)=e2|op(e1,e3)=e3|op(e1,e3)=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f1])).
% 0.20/15.53 fof(f18,plain,(
% 0.20/15.53 op(e1,e4)=e0|op(e1,e4)=e1|op(e1,e4)=e2|op(e1,e4)=e3|op(e1,e4)=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f1])).
% 0.20/15.53 fof(f20,plain,(
% 0.20/15.53 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e3|op(e2,e1)=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f1])).
% 0.20/15.53 fof(f27,plain,(
% 0.20/15.53 op(e3,e3)=e0|op(e3,e3)=e1|op(e3,e3)=e2|op(e3,e3)=e3|op(e3,e3)=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f1])).
% 0.20/15.53 fof(f36,plain,(
% 0.20/15.53 op(unit,e1)=e1),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f37,plain,(
% 0.20/15.53 op(e1,unit)=e1),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f38,plain,(
% 0.20/15.53 op(unit,e2)=e2),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f39,plain,(
% 0.20/15.53 op(e2,unit)=e2),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f40,plain,(
% 0.20/15.53 op(unit,e3)=e3),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f41,plain,(
% 0.20/15.53 op(e3,unit)=e3),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f42,plain,(
% 0.20/15.53 op(unit,e4)=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f43,plain,(
% 0.20/15.53 op(e4,unit)=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f44,plain,(
% 0.20/15.53 unit=e0|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.20/15.53 fof(f67,plain,(
% 0.20/15.53 op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e2)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f3])).
% 0.20/15.53 fof(f74,plain,(
% 0.20/15.53 op(e0,e2)=e4|op(e1,e2)=e4|op(e2,e2)=e4|op(e3,e2)=e4|op(e4,e2)=e4),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f3])).
% 0.20/15.53 fof(f79,plain,(
% 0.20/15.53 op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2|op(e3,e4)=e2),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f3])).
% 0.20/15.53 fof(f88,plain,(
% 0.20/15.53 op(e0,e4)=e1|op(e1,e4)=e1|op(e2,e4)=e1|op(e3,e4)=e1|op(e4,e4)=e1),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f3])).
% 0.20/15.53 fof(f89,plain,(
% 0.20/15.53 op(e4,e0)=e2|op(e4,e1)=e2|op(e4,e2)=e2|op(e4,e3)=e2|op(e4,e4)=e2),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f3])).
% 0.20/15.53 fof(f91,plain,(
% 0.20/15.53 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e2)=e3|op(e4,e3)=e3|op(e4,e4)=e3),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f3])).
% 0.20/15.53 fof(f99,plain,(
% 0.20/15.53 ~op(e1,e0)=op(e2,e0)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f106,plain,(
% 0.20/15.53 ~op(e0,e1)=op(e2,e1)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f109,plain,(
% 0.20/15.53 ~op(e1,e1)=op(e2,e1)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f115,plain,(
% 0.20/15.53 ~op(e0,e2)=op(e1,e2)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f117,plain,(
% 0.20/15.53 ~op(e0,e2)=op(e3,e2)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f121,plain,(
% 0.20/15.53 ~op(e1,e2)=op(e4,e2)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f123,plain,(
% 0.20/15.53 ~op(e2,e2)=op(e4,e2)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f125,plain,(
% 0.20/15.53 ~op(e0,e3)=op(e1,e3)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f128,plain,(
% 0.20/15.53 ~op(e0,e3)=op(e4,e3)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f135,plain,(
% 0.20/15.53 ~op(e0,e4)=op(e1,e4)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f139,plain,(
% 0.20/15.53 ~op(e1,e4)=op(e2,e4)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f142,plain,(
% 0.20/15.53 ~op(e2,e4)=op(e3,e4)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f143,plain,(
% 0.20/15.53 ~op(e2,e4)=op(e4,e4)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f157,plain,(
% 0.20/15.53 ~op(e1,e0)=op(e1,e3)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f158,plain,(
% 0.20/15.53 ~op(e1,e0)=op(e1,e4)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f159,plain,(
% 0.20/15.53 ~op(e1,e1)=op(e1,e2)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.53 fof(f160,plain,(
% 0.20/15.53 ~op(e1,e1)=op(e1,e3)),
% 0.20/15.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f161,plain,(
% 0.20/15.54 ~op(e1,e1)=op(e1,e4)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f162,plain,(
% 0.20/15.54 ~op(e1,e2)=op(e1,e3)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f164,plain,(
% 0.20/15.54 ~op(e1,e3)=op(e1,e4)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f165,plain,(
% 0.20/15.54 ~op(e2,e0)=op(e2,e1)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f171,plain,(
% 0.20/15.54 ~op(e2,e1)=op(e2,e4)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f176,plain,(
% 0.20/15.54 ~op(e3,e0)=op(e3,e2)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f177,plain,(
% 0.20/15.54 ~op(e3,e0)=op(e3,e3)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f184,plain,(
% 0.20/15.54 ~op(e3,e3)=op(e3,e4)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f193,plain,(
% 0.20/15.54 ~op(e4,e2)=op(e4,e4)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.20/15.54 fof(f195,plain,(
% 0.20/15.54 ~e0=e1),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.20/15.54 fof(f196,plain,(
% 0.20/15.54 ~e0=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.20/15.54 fof(f199,plain,(
% 0.20/15.54 ~e1=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.20/15.54 fof(f200,plain,(
% 0.20/15.54 ~e1=e3),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.20/15.54 fof(f201,plain,(
% 0.20/15.54 ~e1=e4),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.20/15.54 fof(f202,plain,(
% 0.20/15.54 ~e2=e3),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.20/15.54 fof(f203,plain,(
% 0.20/15.54 ~e2=e4),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.20/15.54 fof(f204,plain,(
% 0.20/15.54 ~e3=e4),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.20/15.54 fof(f205,plain,(
% 0.20/15.54 e0=op(op(e4,e2),op(e4,e2))),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.20/15.54 fof(f206,plain,(
% 0.20/15.54 e1=op(e4,e2)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.20/15.54 fof(f207,plain,(
% 0.20/15.54 e3=op(e2,e4)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.20/15.54 fof(f208,definition,(
% 0.20/15.54 sP0_prd<=>(((((((((((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3))|((~op(e4,e3)=op(e3,e4)&op(op(e3,e4),e4)=e3)&~op(op(e3,e4),e3)=e4))|((~op(e0,e4)=op(e4,e0)&op(op(e4,e0),e0)=e4)&~op(op(e4,e0),e4)=e0))|((~op(e1,e4)=op(e4,e1)&op(op(e4,e1),e1)=e4)&~op(op(e4,e1),e4)=e1))|((~op(e2,e4)=op(e4,e2)&op(op(e4,e2),e2)=e4)&~op(op(e4,e2),e4)=e2))|((~op(e3,e4)=op(e4,e3)&op(op(e4,e3),e3)=e4)&~op(op(e4,e3),e4)=e3))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.20/15.54 fof(f209,plain,(
% 0.20/15.54 (((((((((((((((((((((((((~op(e0,e0)=e0|op(e0,e0)=e0)&(~op(e0,e0)=e1|op(e0,e1)=e0))&(~op(e0,e0)=e2|op(e0,e2)=e0))&(~op(e0,e0)=e3|op(e0,e3)=e0))&(~op(e0,e0)=e4|op(e0,e4)=e0))&(~op(e1,e1)=e0|op(e1,e0)=e1))&(~op(e1,e1)=e1|op(e1,e1)=e1))&(~op(e1,e1)=e2|op(e1,e2)=e1))&(~op(e1,e1)=e3|op(e1,e3)=e1))&(~op(e1,e1)=e4|op(e1,e4)=e1))&(~op(e2,e2)=e0|op(e2,e0)=e2))&(~op(e2,e2)=e1|op(e2,e1)=e2))&(~op(e2,e2)=e2|op(e2,e2)=e2))&(~op(e2,e2)=e3|op(e2,e3)=e2))&(~op(e2,e2)=e4|op(e2,e4)=e2))&(~op(e3,e3)=e0|op(e3,e0)=e3))&(~op(e3,e3)=e1|op(e3,e1)=e3))&(~op(e3,e3)=e2|op(e3,e2)=e3))&(~op(e3,e3)=e3|op(e3,e3)=e3))&(~op(e3,e3)=e4|op(e3,e4)=e3))&(~op(e4,e4)=e0|op(e4,e0)=e4))&(~op(e4,e4)=e1|op(e4,e1)=e4))&(~op(e4,e4)=e2|op(e4,e2)=e4))&(~op(e4,e4)=e3|op(e4,e3)=e4))&(~op(e4,e4)=e4|op(e4,e4)=e4))&(sP0_prd|((~op(e4,e4)=op(e4,e4)&op(op(e4,e4),e4)=e4)&~op(op(e4,e4),e4)=e4))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f8,f208])).
% 0.20/15.54 fof(f215,plain,(
% 0.20/15.54 ~op(e1,e1)=e0|op(e1,e0)=e1),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f209])).
% 0.20/15.54 fof(f224,plain,(
% 0.20/15.54 ~op(e2,e2)=e4|op(e2,e4)=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f209])).
% 0.20/15.54 fof(f227,plain,(
% 0.20/15.54 ~op(e3,e3)=e2|op(e3,e2)=e3),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f209])).
% 0.20/15.54 fof(f229,plain,(
% 0.20/15.54 ~op(e3,e3)=e4|op(e3,e4)=e3),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f209])).
% 0.20/15.54 fof(f232,plain,(
% 0.20/15.54 ~op(e4,e4)=e2|op(e4,e2)=e4),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f209])).
% 0.20/15.54 fof(f235,plain,(
% 0.20/15.54 sP0_prd|~op(e4,e4)=op(e4,e4)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f209])).
% 0.20/15.54 fof(f238,definition,(
% 0.20/15.54 sP1_prd<=>((((((((((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3))|((~op(e4,e3)=op(e3,e4)&op(op(e3,e4),e4)=e3)&~op(op(e3,e4),e3)=e4))|((~op(e0,e4)=op(e4,e0)&op(op(e4,e0),e0)=e4)&~op(op(e4,e0),e4)=e0))|((~op(e1,e4)=op(e4,e1)&op(op(e4,e1),e1)=e4)&~op(op(e4,e1),e4)=e1))|((~op(e2,e4)=op(e4,e2)&op(op(e4,e2),e2)=e4)&~op(op(e4,e2),e4)=e2))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.20/15.54 fof(f239,plain,(
% 0.20/15.54 sP0_prd<=>(sP1_prd|((~op(e3,e4)=op(e4,e3)&op(op(e4,e3),e3)=e4)&~op(op(e4,e3),e4)=e3))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f208,f238])).
% 0.20/15.54 fof(f240,plain,(
% 0.20/15.54 (~sP0_prd|(sP1_prd|((~op(e3,e4)=op(e4,e3)&op(op(e4,e3),e3)=e4)&~op(op(e4,e3),e4)=e3)))&(sP0_prd|(~sP1_prd&((op(e3,e4)=op(e4,e3)|~op(op(e4,e3),e3)=e4)|op(op(e4,e3),e4)=e3)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f239])).
% 0.20/15.54 fof(f242,plain,(
% 0.20/15.54 ~sP0_prd|sP1_prd|op(op(e4,e3),e3)=e4),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f240])).
% 0.20/15.54 fof(f246,definition,(
% 0.20/15.54 sP2_prd<=>(((((((((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3))|((~op(e4,e3)=op(e3,e4)&op(op(e3,e4),e4)=e3)&~op(op(e3,e4),e3)=e4))|((~op(e0,e4)=op(e4,e0)&op(op(e4,e0),e0)=e4)&~op(op(e4,e0),e4)=e0))|((~op(e1,e4)=op(e4,e1)&op(op(e4,e1),e1)=e4)&~op(op(e4,e1),e4)=e1))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.20/15.54 fof(f247,plain,(
% 0.20/15.54 sP1_prd<=>(sP2_prd|((~op(e2,e4)=op(e4,e2)&op(op(e4,e2),e2)=e4)&~op(op(e4,e2),e4)=e2))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f238,f246])).
% 0.20/15.54 fof(f248,plain,(
% 0.20/15.54 (~sP1_prd|(sP2_prd|((~op(e2,e4)=op(e4,e2)&op(op(e4,e2),e2)=e4)&~op(op(e4,e2),e4)=e2)))&(sP1_prd|(~sP2_prd&((op(e2,e4)=op(e4,e2)|~op(op(e4,e2),e2)=e4)|op(op(e4,e2),e4)=e2)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f247])).
% 0.20/15.54 fof(f251,plain,(
% 0.20/15.54 ~sP1_prd|sP2_prd|~op(op(e4,e2),e4)=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f248])).
% 0.20/15.54 fof(f254,definition,(
% 0.20/15.54 sP3_prd<=>((((((((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3))|((~op(e4,e3)=op(e3,e4)&op(op(e3,e4),e4)=e3)&~op(op(e3,e4),e3)=e4))|((~op(e0,e4)=op(e4,e0)&op(op(e4,e0),e0)=e4)&~op(op(e4,e0),e4)=e0))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.20/15.54 fof(f255,plain,(
% 0.20/15.54 sP2_prd<=>(sP3_prd|((~op(e1,e4)=op(e4,e1)&op(op(e4,e1),e1)=e4)&~op(op(e4,e1),e4)=e1))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f246,f254])).
% 0.20/15.54 fof(f256,plain,(
% 0.20/15.54 (~sP2_prd|(sP3_prd|((~op(e1,e4)=op(e4,e1)&op(op(e4,e1),e1)=e4)&~op(op(e4,e1),e4)=e1)))&(sP2_prd|(~sP3_prd&((op(e1,e4)=op(e4,e1)|~op(op(e4,e1),e1)=e4)|op(op(e4,e1),e4)=e1)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f255])).
% 0.20/15.54 fof(f259,plain,(
% 0.20/15.54 ~sP2_prd|sP3_prd|~op(op(e4,e1),e4)=e1),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f256])).
% 0.20/15.54 fof(f262,definition,(
% 0.20/15.54 sP4_prd<=>(((((((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3))|((~op(e4,e3)=op(e3,e4)&op(op(e3,e4),e4)=e3)&~op(op(e3,e4),e3)=e4))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.20/15.54 fof(f263,plain,(
% 0.20/15.54 sP3_prd<=>(sP4_prd|((~op(e0,e4)=op(e4,e0)&op(op(e4,e0),e0)=e4)&~op(op(e4,e0),e4)=e0))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f254,f262])).
% 0.20/15.54 fof(f264,plain,(
% 0.20/15.54 (~sP3_prd|(sP4_prd|((~op(e0,e4)=op(e4,e0)&op(op(e4,e0),e0)=e4)&~op(op(e4,e0),e4)=e0)))&(sP3_prd|(~sP4_prd&((op(e0,e4)=op(e4,e0)|~op(op(e4,e0),e0)=e4)|op(op(e4,e0),e4)=e0)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f263])).
% 0.20/15.54 fof(f265,plain,(
% 0.20/15.54 ~sP3_prd|sP4_prd|~op(e0,e4)=op(e4,e0)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f264])).
% 0.20/15.54 fof(f270,definition,(
% 0.20/15.54 sP5_prd<=>((((((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.20/15.54 fof(f271,plain,(
% 0.20/15.54 sP4_prd<=>(sP5_prd|((~op(e4,e3)=op(e3,e4)&op(op(e3,e4),e4)=e3)&~op(op(e3,e4),e3)=e4))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f262,f270])).
% 0.20/15.54 fof(f272,plain,(
% 0.20/15.54 (~sP4_prd|(sP5_prd|((~op(e4,e3)=op(e3,e4)&op(op(e3,e4),e4)=e3)&~op(op(e3,e4),e3)=e4)))&(sP4_prd|(~sP5_prd&((op(e4,e3)=op(e3,e4)|~op(op(e3,e4),e4)=e3)|op(op(e3,e4),e3)=e4)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f271])).
% 0.20/15.54 fof(f274,plain,(
% 0.20/15.54 ~sP4_prd|sP5_prd|op(op(e3,e4),e4)=e3),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f272])).
% 0.20/15.54 fof(f278,definition,(
% 0.20/15.54 sP6_prd<=>(((((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.20/15.54 fof(f279,plain,(
% 0.20/15.54 sP5_prd<=>(sP6_prd|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f270,f278])).
% 0.20/15.54 fof(f280,plain,(
% 0.20/15.54 (~sP5_prd|(sP6_prd|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3)))&(sP5_prd|(~sP6_prd&((op(e3,e3)=op(e3,e3)|~op(op(e3,e3),e3)=e3)|op(op(e3,e3),e3)=e3)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f279])).
% 0.20/15.54 fof(f281,plain,(
% 0.20/15.54 ~sP5_prd|sP6_prd|~op(e3,e3)=op(e3,e3)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f280])).
% 0.20/15.54 fof(f286,definition,(
% 0.20/15.54 sP7_prd<=>((((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.20/15.54 fof(f287,plain,(
% 0.20/15.54 sP6_prd<=>(sP7_prd|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f278,f286])).
% 0.20/15.54 fof(f288,plain,(
% 0.20/15.54 (~sP6_prd|(sP7_prd|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2)))&(sP6_prd|(~sP7_prd&((op(e2,e3)=op(e3,e2)|~op(op(e3,e2),e2)=e3)|op(op(e3,e2),e3)=e2)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f287])).
% 0.20/15.54 fof(f291,plain,(
% 0.20/15.54 ~sP6_prd|sP7_prd|~op(op(e3,e2),e3)=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f288])).
% 0.20/15.54 fof(f294,definition,(
% 0.20/15.54 sP8_prd<=>(((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.20/15.54 fof(f295,plain,(
% 0.20/15.54 sP7_prd<=>(sP8_prd|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f286,f294])).
% 0.20/15.54 fof(f296,plain,(
% 0.20/15.54 (~sP7_prd|(sP8_prd|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1)))&(sP7_prd|(~sP8_prd&((op(e1,e3)=op(e3,e1)|~op(op(e3,e1),e1)=e3)|op(op(e3,e1),e3)=e1)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f295])).
% 0.20/15.54 fof(f299,plain,(
% 0.20/15.54 ~sP7_prd|sP8_prd|~op(op(e3,e1),e3)=e1),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f296])).
% 0.20/15.54 fof(f302,definition,(
% 0.20/15.54 sP9_prd<=>((((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.20/15.54 fof(f303,plain,(
% 0.20/15.54 sP8_prd<=>(sP9_prd|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f294,f302])).
% 0.20/15.54 fof(f304,plain,(
% 0.20/15.54 (~sP8_prd|(sP9_prd|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0)))&(sP8_prd|(~sP9_prd&((op(e0,e3)=op(e3,e0)|~op(op(e3,e0),e0)=e3)|op(op(e3,e0),e3)=e0)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f303])).
% 0.20/15.54 fof(f305,plain,(
% 0.20/15.54 ~sP8_prd|sP9_prd|~op(e0,e3)=op(e3,e0)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f304])).
% 0.20/15.54 fof(f310,definition,(
% 0.20/15.54 sP10_prd<=>(((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.20/15.54 fof(f311,plain,(
% 0.20/15.54 sP9_prd<=>(sP10_prd|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f302,f310])).
% 0.20/15.54 fof(f312,plain,(
% 0.20/15.54 (~sP9_prd|(sP10_prd|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4)))&(sP9_prd|(~sP10_prd&((op(e4,e2)=op(e2,e4)|~op(op(e2,e4),e4)=e2)|op(op(e2,e4),e2)=e4)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f311])).
% 0.20/15.54 fof(f314,plain,(
% 0.20/15.54 ~sP9_prd|sP10_prd|op(op(e2,e4),e4)=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f312])).
% 0.20/15.54 fof(f318,definition,(
% 0.20/15.54 sP11_prd<=>((((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.20/15.54 fof(f319,plain,(
% 0.20/15.54 sP10_prd<=>(sP11_prd|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f310,f318])).
% 0.20/15.54 fof(f320,plain,(
% 0.20/15.54 (~sP10_prd|(sP11_prd|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3)))&(sP10_prd|(~sP11_prd&((op(e3,e2)=op(e2,e3)|~op(op(e2,e3),e3)=e2)|op(op(e2,e3),e2)=e3)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f319])).
% 0.20/15.54 fof(f322,plain,(
% 0.20/15.54 ~sP10_prd|sP11_prd|op(op(e2,e3),e3)=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f320])).
% 0.20/15.54 fof(f326,definition,(
% 0.20/15.54 sP12_prd<=>(((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.20/15.54 fof(f327,plain,(
% 0.20/15.54 sP11_prd<=>(sP12_prd|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f318,f326])).
% 0.20/15.54 fof(f328,plain,(
% 0.20/15.54 (~sP11_prd|(sP12_prd|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2)))&(sP11_prd|(~sP12_prd&((op(e2,e2)=op(e2,e2)|~op(op(e2,e2),e2)=e2)|op(op(e2,e2),e2)=e2)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f327])).
% 0.20/15.54 fof(f329,plain,(
% 0.20/15.54 ~sP11_prd|sP12_prd|~op(e2,e2)=op(e2,e2)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f328])).
% 0.20/15.54 fof(f334,definition,(
% 0.20/15.54 sP13_prd<=>((((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.20/15.54 fof(f335,plain,(
% 0.20/15.54 sP12_prd<=>(sP13_prd|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f326,f334])).
% 0.20/15.54 fof(f336,plain,(
% 0.20/15.54 (~sP12_prd|(sP13_prd|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1)))&(sP12_prd|(~sP13_prd&((op(e1,e2)=op(e2,e1)|~op(op(e2,e1),e1)=e2)|op(op(e2,e1),e2)=e1)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f335])).
% 0.20/15.54 fof(f339,plain,(
% 0.20/15.54 ~sP12_prd|sP13_prd|~op(op(e2,e1),e2)=e1),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f336])).
% 0.20/15.54 fof(f342,definition,(
% 0.20/15.54 sP14_prd<=>(((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.20/15.54 fof(f343,plain,(
% 0.20/15.54 sP13_prd<=>(sP14_prd|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f334,f342])).
% 0.20/15.54 fof(f344,plain,(
% 0.20/15.54 (~sP13_prd|(sP14_prd|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0)))&(sP13_prd|(~sP14_prd&((op(e0,e2)=op(e2,e0)|~op(op(e2,e0),e0)=e2)|op(op(e2,e0),e2)=e0)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f343])).
% 0.20/15.54 fof(f345,plain,(
% 0.20/15.54 ~sP13_prd|sP14_prd|~op(e0,e2)=op(e2,e0)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f344])).
% 0.20/15.54 fof(f350,definition,(
% 0.20/15.54 sP15_prd<=>((((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.20/15.54 fof(f351,plain,(
% 0.20/15.54 sP14_prd<=>(sP15_prd|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f342,f350])).
% 0.20/15.54 fof(f352,plain,(
% 0.20/15.54 (~sP14_prd|(sP15_prd|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4)))&(sP14_prd|(~sP15_prd&((op(e4,e1)=op(e1,e4)|~op(op(e1,e4),e4)=e1)|op(op(e1,e4),e1)=e4)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f351])).
% 0.20/15.54 fof(f354,plain,(
% 0.20/15.54 ~sP14_prd|sP15_prd|op(op(e1,e4),e4)=e1),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f352])).
% 0.20/15.54 fof(f358,definition,(
% 0.20/15.54 sP16_prd<=>(((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 0.20/15.54 fof(f359,plain,(
% 0.20/15.54 sP15_prd<=>(sP16_prd|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f350,f358])).
% 0.20/15.54 fof(f360,plain,(
% 0.20/15.54 (~sP15_prd|(sP16_prd|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3)))&(sP15_prd|(~sP16_prd&((op(e3,e1)=op(e1,e3)|~op(op(e1,e3),e3)=e1)|op(op(e1,e3),e1)=e3)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f359])).
% 0.20/15.54 fof(f363,plain,(
% 0.20/15.54 ~sP15_prd|sP16_prd|~op(op(e1,e3),e1)=e3),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f360])).
% 0.20/15.54 fof(f366,definition,(
% 0.20/15.54 sP17_prd<=>((((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP17_prd])],[])).
% 0.20/15.54 fof(f367,plain,(
% 0.20/15.54 sP16_prd<=>(sP17_prd|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f358,f366])).
% 0.20/15.54 fof(f368,plain,(
% 0.20/15.54 (~sP16_prd|(sP17_prd|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2)))&(sP16_prd|(~sP17_prd&((op(e2,e1)=op(e1,e2)|~op(op(e1,e2),e2)=e1)|op(op(e1,e2),e1)=e2)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f367])).
% 0.20/15.54 fof(f371,plain,(
% 0.20/15.54 ~sP16_prd|sP17_prd|~op(op(e1,e2),e1)=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f368])).
% 0.20/15.54 fof(f374,definition,(
% 0.20/15.54 sP18_prd<=>(((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.20/15.54 fof(f375,plain,(
% 0.20/15.54 sP17_prd<=>(sP18_prd|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f366,f374])).
% 0.20/15.54 fof(f376,plain,(
% 0.20/15.54 (~sP17_prd|(sP18_prd|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1)))&(sP17_prd|(~sP18_prd&((op(e1,e1)=op(e1,e1)|~op(op(e1,e1),e1)=e1)|op(op(e1,e1),e1)=e1)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f375])).
% 0.20/15.54 fof(f377,plain,(
% 0.20/15.54 ~sP17_prd|sP18_prd|~op(e1,e1)=op(e1,e1)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f376])).
% 0.20/15.54 fof(f382,definition,(
% 0.20/15.54 sP19_prd<=>((((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.20/15.54 fof(f383,plain,(
% 0.20/15.54 sP18_prd<=>(sP19_prd|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f374,f382])).
% 0.20/15.54 fof(f384,plain,(
% 0.20/15.54 (~sP18_prd|(sP19_prd|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0)))&(sP18_prd|(~sP19_prd&((op(e0,e1)=op(e1,e0)|~op(op(e1,e0),e0)=e1)|op(op(e1,e0),e1)=e0)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f383])).
% 0.20/15.54 fof(f387,plain,(
% 0.20/15.54 ~sP18_prd|sP19_prd|~op(op(e1,e0),e1)=e0),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f384])).
% 0.20/15.54 fof(f390,definition,(
% 0.20/15.54 sP20_prd<=>(((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.20/15.54 fof(f391,plain,(
% 0.20/15.54 sP19_prd<=>(sP20_prd|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f382,f390])).
% 0.20/15.54 fof(f392,plain,(
% 0.20/15.54 (~sP19_prd|(sP20_prd|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4)))&(sP19_prd|(~sP20_prd&((op(e4,e0)=op(e0,e4)|~op(op(e0,e4),e4)=e0)|op(op(e0,e4),e0)=e4)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f391])).
% 0.20/15.54 fof(f393,plain,(
% 0.20/15.54 ~sP19_prd|sP20_prd|~op(e4,e0)=op(e0,e4)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f392])).
% 0.20/15.54 fof(f398,definition,(
% 0.20/15.54 sP21_prd<=>((((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP21_prd])],[])).
% 0.20/15.54 fof(f399,plain,(
% 0.20/15.54 sP20_prd<=>(sP21_prd|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f390,f398])).
% 0.20/15.54 fof(f400,plain,(
% 0.20/15.54 (~sP20_prd|(sP21_prd|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3)))&(sP20_prd|(~sP21_prd&((op(e3,e0)=op(e0,e3)|~op(op(e0,e3),e3)=e0)|op(op(e0,e3),e0)=e3)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f399])).
% 0.20/15.54 fof(f401,plain,(
% 0.20/15.54 ~sP20_prd|sP21_prd|~op(e3,e0)=op(e0,e3)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f400])).
% 0.20/15.54 fof(f406,definition,(
% 0.20/15.54 sP22_prd<=>(((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP22_prd])],[])).
% 0.20/15.54 fof(f407,plain,(
% 0.20/15.54 sP21_prd<=>(sP22_prd|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f398,f406])).
% 0.20/15.54 fof(f408,plain,(
% 0.20/15.54 (~sP21_prd|(sP22_prd|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2)))&(sP21_prd|(~sP22_prd&((op(e2,e0)=op(e0,e2)|~op(op(e0,e2),e2)=e0)|op(op(e0,e2),e0)=e2)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f407])).
% 0.20/15.54 fof(f411,plain,(
% 0.20/15.54 ~sP21_prd|sP22_prd|~op(op(e0,e2),e0)=e2),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f408])).
% 0.20/15.54 fof(f414,definition,(
% 0.20/15.54 sP23_prd<=>((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)),
% 0.20/15.54 introduced(definition,[new_symbols(definition,[sP23_prd])],[])).
% 0.20/15.54 fof(f415,plain,(
% 0.20/15.54 sP22_prd<=>(sP23_prd|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))),
% 0.20/15.54 inference(formula_renaming,[status(thm)],[f406,f414])).
% 0.20/15.54 fof(f416,plain,(
% 0.20/15.54 (~sP22_prd|(sP23_prd|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1)))&(sP22_prd|(~sP23_prd&((op(e1,e0)=op(e0,e1)|~op(op(e0,e1),e1)=e0)|op(op(e0,e1),e0)=e1)))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f415])).
% 0.20/15.54 fof(f419,plain,(
% 0.20/15.54 ~sP22_prd|sP23_prd|~op(op(e0,e1),e0)=e1),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f416])).
% 0.20/15.54 fof(f422,plain,(
% 0.20/15.54 (~sP23_prd|((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0))&(sP23_prd|((op(e0,e0)=op(e0,e0)|~op(op(e0,e0),e0)=e0)|op(op(e0,e0),e0)=e0))),
% 0.20/15.54 inference(NNF_transformation,[status(thm)],[f414])).
% 0.20/15.54 fof(f423,plain,(
% 0.20/15.54 ~sP23_prd|~op(e0,e0)=op(e0,e0)),
% 0.20/15.54 inference(cnf_transformation,[status(thm)],[f422])).
% 0.20/15.54 fof(f427,plain,(
% 0.20/15.54 e0=op(op(e4,e2),e1)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f206,f205])).
% 0.20/15.54 fof(f428,plain,(
% 0.20/15.54 ~e1=op(e4,e4)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f206,f193])).
% 0.20/15.54 fof(f433,plain,(
% 0.20/15.54 ~op(e2,e2)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f206,f123])).
% 0.20/15.54 fof(f434,plain,(
% 0.20/15.54 ~op(e1,e2)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f206,f121])).
% 0.20/15.54 fof(f437,plain,(
% 0.20/15.54 op(e4,e0)=e3|op(e4,e1)=e3|e1=e3|op(e4,e3)=e3|op(e4,e4)=e3),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f206,f91])).
% 0.20/15.54 fof(f438,plain,(
% 0.20/15.54 op(e4,e0)=e2|op(e4,e1)=e2|e1=e2|op(e4,e3)=e2|op(e4,e4)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f206,f89])).
% 0.20/15.54 fof(f441,plain,(
% 0.20/15.54 op(e0,e2)=e4|op(e1,e2)=e4|op(e2,e2)=e4|op(e3,e2)=e4|e1=e4),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f206,f74])).
% 0.20/15.54 fof(f449,plain,(
% 0.20/15.54 ~op(e2,e1)=e3),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f207,f171])).
% 0.20/15.54 fof(f451,plain,(
% 0.20/15.54 ~e3=op(e4,e4)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f207,f143])).
% 0.20/15.54 fof(f452,plain,(
% 0.20/15.54 ~e3=op(e3,e4)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f207,f142])).
% 0.20/15.54 fof(f453,plain,(
% 0.20/15.54 ~op(e1,e4)=e3),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f207,f139])).
% 0.20/15.54 fof(f458,plain,(
% 0.20/15.54 op(e0,e4)=e1|op(e1,e4)=e1|e3=e1|op(e3,e4)=e1|op(e4,e4)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f207,f88])).
% 0.20/15.54 fof(f463,plain,(
% 0.20/15.54 op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e2)=e1|op(e2,e3)=e1|e3=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f207,f67])).
% 0.20/15.54 fof(f466,plain,(
% 0.20/15.54 ~op(e2,e2)=e4|e3=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f207,f224])).
% 0.20/15.54 fof(f468,plain,(
% 0.20/15.54 ~op(e2,e2)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f466,f202])).
% 0.20/15.54 fof(f469,plain,(
% 0.20/15.54 ~op(e4,e4)=e2|e1=e4),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f206,f232])).
% 0.20/15.54 fof(f471,plain,(
% 0.20/15.54 ~op(e4,e4)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f469,f201])).
% 0.20/15.54 fof(f472,plain,(
% 0.20/15.54 sP0_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f235])).
% 0.20/15.54 fof(f474,plain,(
% 0.20/15.54 sP1_prd|op(op(e4,e3),e3)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f242,f472])).
% 0.20/15.54 fof(f479,plain,(
% 0.20/15.54 ~sP1_prd|sP2_prd|~op(e1,e4)=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f206,f251])).
% 0.20/15.54 fof(f485,plain,(
% 0.20/15.54 ~sP5_prd|sP6_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f281])).
% 0.20/15.54 fof(f488,plain,(
% 0.20/15.54 ~sP9_prd|sP10_prd|op(e3,e4)=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f207,f314])).
% 0.20/15.54 fof(f495,plain,(
% 0.20/15.54 ~sP11_prd|sP12_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f329])).
% 0.20/15.54 fof(f496,plain,(
% 0.20/15.54 ~sP17_prd|sP18_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f377])).
% 0.20/15.54 fof(f497,plain,(
% 0.20/15.54 ~sP22_prd|~op(op(e0,e1),e0)=e1),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f419,f500])).
% 0.20/15.54 fof(f500,plain,(
% 0.20/15.54 ~sP23_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f423])).
% 0.20/15.54 fof(f504,plain,(
% 0.20/15.54 ~e0=e0|op(e1,e0)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f524,f215])).
% 0.20/15.54 fof(f505,plain,(
% 0.20/15.54 ~e0=op(e1,e4)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f524,f161])).
% 0.20/15.54 fof(f506,plain,(
% 0.20/15.54 ~e0=op(e1,e3)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f524,f160])).
% 0.20/15.54 fof(f507,plain,(
% 0.20/15.54 ~e0=op(e1,e2)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f524,f159])).
% 0.20/15.54 fof(f511,plain,(
% 0.20/15.54 ~e0=op(e2,e1)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f524,f109])).
% 0.20/15.54 fof(f524,plain,(
% 0.20/15.54 e0=op(e1,e1)),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f206,f427])).
% 0.20/15.54 fof(f532,plain,(
% 0.20/15.54 op(e1,e2)=e0|op(e1,e2)=e2|op(e1,e2)=e3|op(e1,e2)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f16,f434])).
% 0.20/15.54 fof(f536,plain,(
% 0.20/15.54 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3|op(e4,e4)=e3),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f437,f200])).
% 0.20/15.54 fof(f537,plain,(
% 0.20/15.54 op(e4,e0)=e2|op(e4,e1)=e2|op(e4,e3)=e2|op(e4,e4)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f438,f199])).
% 0.20/15.54 fof(f539,plain,(
% 0.20/15.54 op(e0,e2)=e4|op(e1,e2)=e4|op(e3,e2)=e4|e1=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f441,f468])).
% 0.20/15.54 fof(f547,plain,(
% 0.20/15.54 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f20,f449])).
% 0.20/15.54 fof(f550,plain,(
% 0.20/15.54 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f536,f451])).
% 0.20/15.54 fof(f551,plain,(
% 0.20/15.54 ~op(e3,e3)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f229,f452])).
% 0.20/15.54 fof(f554,plain,(
% 0.20/15.54 op(e1,e4)=e0|op(e1,e4)=e1|op(e1,e4)=e2|op(e1,e4)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f18,f453])).
% 0.20/15.54 fof(f559,plain,(
% 0.20/15.54 op(e0,e4)=e1|op(e1,e4)=e1|op(e3,e4)=e1|op(e4,e4)=e1),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f458,f200])).
% 0.20/15.54 fof(f563,plain,(
% 0.20/15.54 op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e3)=e1|e3=e1),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f463,f433])).
% 0.20/15.54 fof(f573,plain,(
% 0.20/15.54 ~sP18_prd|sP19_prd|~op(e1,e1)=e0),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f587,f387])).
% 0.20/15.54 fof(f576,plain,(
% 0.20/15.54 ~e1=op(e1,e4)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f587,f158])).
% 0.20/15.54 fof(f577,plain,(
% 0.20/15.54 ~e1=op(e1,e3)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f587,f157])).
% 0.20/15.54 fof(f581,plain,(
% 0.20/15.54 ~e1=op(e2,e0)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f587,f99])).
% 0.20/15.54 fof(f587,plain,(
% 0.20/15.54 op(e1,e0)=e1),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f504])).
% 0.20/15.54 fof(f590,plain,(
% 0.20/15.54 op(e1,e3)=e1|op(e1,e3)=e2|op(e1,e3)=e3|op(e1,e3)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f17,f506])).
% 0.20/15.54 fof(f611,plain,(
% 0.20/15.54 op(e1,e2)=e2|op(e1,e2)=e3|op(e1,e2)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f532,f507])).
% 0.20/15.54 fof(f612,plain,(
% 0.20/15.54 op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f547,f511])).
% 0.20/15.54 fof(f617,plain,(
% 0.20/15.54 op(e3,e3)=e0|op(e3,e3)=e1|op(e3,e3)=e2|op(e3,e3)=e3),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f27,f551])).
% 0.20/15.54 fof(f618,plain,(
% 0.20/15.54 op(e1,e4)=e1|op(e1,e4)=e2|op(e1,e4)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f554,f505])).
% 0.20/15.54 fof(f622,plain,(
% 0.20/15.54 ~sP18_prd|sP19_prd|~e0=e0),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f524,f573])).
% 0.20/15.54 fof(f623,plain,(
% 0.20/15.54 ~sP18_prd|sP19_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f622])).
% 0.20/15.54 fof(f624,plain,(
% 0.20/15.54 op(e1,e4)=e2|op(e1,e4)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f618,f576])).
% 0.20/15.54 fof(f625,plain,(
% 0.20/15.54 op(e0,e4)=e1|op(e3,e4)=e1|op(e4,e4)=e1),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f559,f576])).
% 0.20/15.54 fof(f630,plain,(
% 0.20/15.54 op(e2,e1)=e1|op(e2,e3)=e1|e3=e1),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f563,f581])).
% 0.20/15.54 fof(f637,plain,(
% 0.20/15.54 op(e1,e3)=e2|op(e1,e3)=e3|op(e1,e3)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f590,f577])).
% 0.20/15.54 fof(f638,plain,(
% 0.20/15.54 op(e0,e4)=e1|op(e3,e4)=e1),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f625,f428])).
% 0.20/15.54 fof(f639,plain,(
% 0.20/15.54 op(e2,e1)=e1|op(e2,e3)=e1),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f630,f200])).
% 0.20/15.54 fof(f654,plain,(
% 0.20/15.54 op(e3,e4)=e3|unit=e0|unit=e1|unit=e2|unit=e3),
% 0.20/15.54 inference(paramodulation,[status(thm)],[f44,f41])).
% 0.20/15.54 fof(f666,plain,(
% 0.20/15.54 unit=e0|unit=e1|unit=e2|unit=e3),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f654,f452])).
% 0.20/15.54 fof(f693,plain,(
% 0.20/15.54 op(op(e4,e3),e3)=e4|sP2_prd|~op(e1,e4)=e2),
% 0.20/15.54 inference(resolution,[status(thm)],[f474,f479])).
% 0.20/15.54 fof(f722,plain,(
% 0.20/15.54 ~sP8_prd|~op(e0,e3)=op(e3,e0)|sP10_prd|op(e3,e4)=e2),
% 0.20/15.54 inference(resolution,[status(thm)],[f305,f488])).
% 0.20/15.54 fof(f776,plain,(
% 0.20/15.54 sP22_prd|~op(op(e0,e2),e0)=e2|~sP20_prd|~op(e3,e0)=op(e0,e3)),
% 0.20/15.54 inference(resolution,[status(thm)],[f411,f401])).
% 0.20/15.54 fof(f783,plain,(
% 0.20/15.54 ~op(e0,e4)=e4|op(e1,e4)=e2),
% 0.20/15.54 inference(paramodulation,[status(thm)],[f624,f135])).
% 0.20/15.54 fof(f788,plain,(
% 0.20/15.54 op(e0,e4)=e1|e2=e1|op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2),
% 0.20/15.54 inference(paramodulation,[status(thm)],[f79,f638])).
% 0.20/15.54 fof(f789,plain,(
% 0.20/15.54 ~op(e3,e3)=e1|op(e0,e4)=e1),
% 0.20/15.54 inference(paramodulation,[status(thm)],[f638,f184])).
% 0.20/15.54 fof(f797,plain,(
% 0.20/15.54 op(e0,e4)=e1|op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f788,f199])).
% 0.20/15.54 fof(f810,plain,(
% 0.20/15.54 op(e1,e3)=e1|unit=e0|unit=e1|unit=e2),
% 0.20/15.54 inference(paramodulation,[status(thm)],[f666,f37])).
% 0.20/15.54 fof(f817,plain,(
% 0.20/15.54 unit=e0|unit=e1|unit=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f810,f577])).
% 0.20/15.54 fof(f829,plain,(
% 0.20/15.54 op(e4,e0)=e2|op(e4,e1)=e2|op(e4,e3)=e2),
% 0.20/15.54 inference(resolution,[status(thm)],[f537,f471])).
% 0.20/15.54 fof(f843,plain,(
% 0.20/15.54 op(e4,e2)=e4|unit=e0|unit=e1),
% 0.20/15.54 inference(paramodulation,[status(thm)],[f817,f43])).
% 0.20/15.54 fof(f855,plain,(
% 0.20/15.54 e1=e4|unit=e0|unit=e1),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f206,f843])).
% 0.20/15.54 fof(f856,plain,(
% 0.20/15.54 unit=e0|unit=e1),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f855,f201])).
% 0.20/15.54 fof(f864,plain,(
% 0.20/15.54 op(e1,e1)=e1|unit=e0),
% 0.20/15.54 inference(paramodulation,[status(thm)],[f856,f37])).
% 0.20/15.54 fof(f869,plain,(
% 0.20/15.54 e0=e1|unit=e0),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f524,f864])).
% 0.20/15.54 fof(f871,plain,(
% 0.20/15.54 op(e4,e0)=e4),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f887,f43])).
% 0.20/15.54 fof(f872,plain,(
% 0.20/15.54 op(e0,e4)=e4),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f887,f42])).
% 0.20/15.54 fof(f873,plain,(
% 0.20/15.54 op(e3,e0)=e3),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f887,f41])).
% 0.20/15.54 fof(f874,plain,(
% 0.20/15.54 op(e0,e3)=e3),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f887,f40])).
% 0.20/15.54 fof(f875,plain,(
% 0.20/15.54 op(e2,e0)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f887,f39])).
% 0.20/15.54 fof(f876,plain,(
% 0.20/15.54 op(e0,e2)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f887,f38])).
% 0.20/15.54 fof(f878,plain,(
% 0.20/15.54 op(e0,e1)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f887,f36])).
% 0.20/15.54 fof(f887,plain,(
% 0.20/15.54 unit=e0),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f869,f195])).
% 0.20/15.54 fof(f892,plain,(
% 0.20/15.54 ~sP19_prd|sP20_prd|~e4=op(e0,e4)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f871,f393])).
% 0.20/15.54 fof(f896,plain,(
% 0.20/15.54 ~sP3_prd|sP4_prd|~op(e0,e4)=e4),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f871,f265])).
% 0.20/15.54 fof(f905,plain,(
% 0.20/15.54 e4=e2|op(e4,e1)=e2|op(e4,e3)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f871,f829])).
% 0.20/15.54 fof(f916,plain,(
% 0.20/15.54 e4=e3|op(e4,e1)=e3|op(e4,e3)=e3),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f871,f550])).
% 0.20/15.54 fof(f919,plain,(
% 0.20/15.54 e4=e1|op(e3,e4)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f872,f638])).
% 0.20/15.54 fof(f934,plain,(
% 0.20/15.54 ~op(e3,e3)=e1|e4=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f872,f789])).
% 0.20/15.54 fof(f935,plain,(
% 0.20/15.54 e4=e1|op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f872,f797])).
% 0.20/15.54 fof(f936,plain,(
% 0.20/15.54 ~e4=e4|op(e1,e4)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f872,f783])).
% 0.20/15.54 fof(f951,plain,(
% 0.20/15.54 ~e3=op(e3,e3)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f873,f177])).
% 0.20/15.54 fof(f952,plain,(
% 0.20/15.54 ~e3=op(e3,e2)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f873,f176])).
% 0.20/15.54 fof(f959,plain,(
% 0.20/15.54 sP22_prd|~op(op(e0,e2),e0)=e2|~sP20_prd|~e3=op(e0,e3)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f873,f776])).
% 0.20/15.54 fof(f968,plain,(
% 0.20/15.54 ~sP8_prd|~op(e0,e3)=e3|sP10_prd|op(e3,e4)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f873,f722])).
% 0.20/15.54 fof(f980,plain,(
% 0.20/15.54 ~e3=op(e4,e3)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f874,f128])).
% 0.20/15.54 fof(f983,plain,(
% 0.20/15.54 ~e3=op(e1,e3)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f874,f125])).
% 0.20/15.54 fof(f1009,plain,(
% 0.20/15.54 ~sP13_prd|sP14_prd|~op(e0,e2)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f875,f345])).
% 0.20/15.54 fof(f1012,plain,(
% 0.20/15.54 ~e2=op(e2,e1)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f875,f165])).
% 0.20/15.54 fof(f1027,plain,(
% 0.20/15.54 ~e2=op(e3,e2)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f876,f117])).
% 0.20/15.54 fof(f1029,plain,(
% 0.20/15.54 ~e2=op(e1,e2)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f876,f115])).
% 0.20/15.54 fof(f1036,plain,(
% 0.20/15.54 e2=e4|op(e1,e2)=e4|op(e3,e2)=e4|e1=e4),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f876,f539])).
% 0.20/15.54 fof(f1038,plain,(
% 0.20/15.54 ~sP22_prd|~op(e1,e0)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f878,f497])).
% 0.20/15.54 fof(f1044,plain,(
% 0.20/15.54 ~e1=op(e2,e1)),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f878,f106])).
% 0.20/15.54 fof(f1053,plain,(
% 0.20/15.54 ~sP19_prd|sP20_prd|~e4=e4),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f872,f892])).
% 0.20/15.54 fof(f1054,plain,(
% 0.20/15.54 ~sP19_prd|sP20_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1053])).
% 0.20/15.54 fof(f1056,plain,(
% 0.20/15.54 ~sP3_prd|sP4_prd|~e4=e4),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f872,f896])).
% 0.20/15.54 fof(f1057,plain,(
% 0.20/15.54 ~sP3_prd|sP4_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1056])).
% 0.20/15.54 fof(f1064,plain,(
% 0.20/15.54 op(e4,e1)=e2|op(e4,e3)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f905,f203])).
% 0.20/15.54 fof(f1069,plain,(
% 0.20/15.54 op(e4,e1)=e3|op(e4,e3)=e3),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f916,f204])).
% 0.20/15.54 fof(f1074,plain,(
% 0.20/15.54 ~sP4_prd|sP5_prd|op(e1,e4)=e3),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1090,f274])).
% 0.20/15.54 fof(f1090,plain,(
% 0.20/15.54 op(e3,e4)=e1),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f919,f201])).
% 0.20/15.54 fof(f1104,plain,(
% 0.20/15.54 op(e3,e3)=e0|op(e3,e3)=e2|op(e3,e3)=e3),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f617,f1105])).
% 0.20/15.54 fof(f1105,plain,(
% 0.20/15.54 ~op(e3,e3)=e1),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f934,f201])).
% 0.20/15.54 fof(f1106,plain,(
% 0.20/15.54 e4=e1|e3=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f873,f935])).
% 0.20/15.54 fof(f1107,plain,(
% 0.20/15.54 e3=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1106,f201])).
% 0.20/15.54 fof(f1110,plain,(
% 0.20/15.54 ~sP14_prd|sP15_prd|op(e2,e4)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1130,f354])).
% 0.20/15.54 fof(f1114,plain,(
% 0.20/15.54 ~op(e1,e3)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1130,f164])).
% 0.20/15.54 fof(f1127,plain,(
% 0.20/15.54 op(op(e4,e3),e3)=e4|sP2_prd|~e2=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1130,f693])).
% 0.20/15.54 fof(f1130,plain,(
% 0.20/15.54 op(e1,e4)=e2),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f936])).
% 0.20/15.54 fof(f1140,plain,(
% 0.20/15.54 ~op(e3,e3)=e2),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f227,f952])).
% 0.20/15.54 fof(f1145,plain,(
% 0.20/15.54 sP22_prd|~op(e2,e0)=e2|~sP20_prd|~e3=op(e0,e3)),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f876,f959])).
% 0.20/15.54 fof(f1146,plain,(
% 0.20/15.54 sP22_prd|~e2=e2|~sP20_prd|~e3=op(e0,e3)),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f875,f1145])).
% 0.20/15.54 fof(f1147,plain,(
% 0.20/15.54 sP22_prd|~e2=e2|~sP20_prd|~e3=e3),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f874,f1146])).
% 0.20/15.54 fof(f1148,plain,(
% 0.20/15.54 sP22_prd|~sP20_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1147])).
% 0.20/15.54 fof(f1159,plain,(
% 0.20/15.54 ~sP8_prd|~e3=e3|sP10_prd|op(e3,e4)=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f874,f968])).
% 0.20/15.54 fof(f1160,plain,(
% 0.20/15.54 ~sP8_prd|~e3=e3|sP10_prd|e1=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1090,f1159])).
% 0.20/15.54 fof(f1161,plain,(
% 0.20/15.54 ~sP8_prd|sP10_prd|e1=e2),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1160])).
% 0.20/15.54 fof(f1162,plain,(
% 0.20/15.54 ~sP8_prd|sP10_prd),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1161,f199])).
% 0.20/15.54 fof(f1178,plain,(
% 0.20/15.54 op(e4,e1)=e3),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1069,f980])).
% 0.20/15.54 fof(f1179,plain,(
% 0.20/15.54 op(e1,e3)=e2|op(e1,e3)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f637,f983])).
% 0.20/15.54 fof(f1215,plain,(
% 0.20/15.54 ~sP13_prd|sP14_prd|~e2=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f876,f1009])).
% 0.20/15.54 fof(f1216,plain,(
% 0.20/15.54 ~sP13_prd|sP14_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1215])).
% 0.20/15.54 fof(f1221,plain,(
% 0.20/15.54 op(e2,e1)=e1|op(e2,e1)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f612,f1012])).
% 0.20/15.54 fof(f1231,plain,(
% 0.20/15.54 e3=e2|op(e3,e1)=e2|op(e3,e3)=e2),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1107,f1027])).
% 0.20/15.54 fof(f1232,plain,(
% 0.20/15.54 op(e1,e2)=e3|op(e1,e2)=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f611,f1029])).
% 0.20/15.54 fof(f1236,plain,(
% 0.20/15.54 op(e1,e2)=e4|op(e3,e2)=e4|e1=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1036,f203])).
% 0.20/15.54 fof(f1237,plain,(
% 0.20/15.54 ~sP22_prd|~e1=e1),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f587,f1038])).
% 0.20/15.54 fof(f1239,plain,(
% 0.20/15.54 ~sP20_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1148,f1240])).
% 0.20/15.54 fof(f1240,plain,(
% 0.20/15.54 ~sP22_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1237])).
% 0.20/15.54 fof(f1243,plain,(
% 0.20/15.54 op(e2,e3)=e1),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f639,f1044])).
% 0.20/15.54 fof(f1260,plain,(
% 0.20/15.54 ~sP4_prd|sP5_prd|e2=e3),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1130,f1074])).
% 0.20/15.54 fof(f1261,plain,(
% 0.20/15.54 ~sP4_prd|sP5_prd),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1260,f202])).
% 0.20/15.54 fof(f1273,plain,(
% 0.20/15.54 op(e3,e3)=e0|op(e3,e3)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1104,f951])).
% 0.20/15.54 fof(f1277,plain,(
% 0.20/15.54 ~sP14_prd|sP15_prd|e3=e1),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f207,f1110])).
% 0.20/15.54 fof(f1278,plain,(
% 0.20/15.54 ~sP14_prd|sP15_prd),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1277,f200])).
% 0.20/15.54 fof(f1285,plain,(
% 0.20/15.54 op(op(e4,e3),e3)=e4|sP2_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1127])).
% 0.20/15.54 fof(f1287,plain,(
% 0.20/15.54 op(e3,e3)=e0),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1273,f1140])).
% 0.20/15.54 fof(f1289,plain,(
% 0.20/15.54 ~sP2_prd|sP3_prd|~op(e3,e4)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1178,f259])).
% 0.20/15.54 fof(f1303,plain,(
% 0.20/15.54 e3=e2|op(e4,e3)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1178,f1064])).
% 0.20/15.54 fof(f1306,plain,(
% 0.20/15.54 ~sP15_prd|sP16_prd|~op(e4,e1)=e3),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1324,f363])).
% 0.20/15.54 fof(f1311,plain,(
% 0.20/15.54 ~op(e1,e2)=e4),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1324,f162])).
% 0.20/15.54 fof(f1324,plain,(
% 0.20/15.54 op(e1,e3)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1179,f1114])).
% 0.20/15.54 fof(f1343,plain,(
% 0.20/15.54 ~sP12_prd|sP13_prd|~op(e4,e2)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1355,f339])).
% 0.20/15.54 fof(f1355,plain,(
% 0.20/15.54 op(e2,e1)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1221,f1044])).
% 0.20/15.54 fof(f1356,plain,(
% 0.20/15.54 op(e3,e1)=e2|op(e3,e3)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1231,f202])).
% 0.20/15.54 fof(f1358,plain,(
% 0.20/15.54 ~sP19_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1054,f1239])).
% 0.20/15.54 fof(f1361,plain,(
% 0.20/15.54 ~sP10_prd|sP11_prd|op(e1,e3)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1243,f322])).
% 0.20/15.54 fof(f1380,plain,(
% 0.20/15.54 op(e3,e1)=e2|e0=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1287,f1356])).
% 0.20/15.54 fof(f1386,plain,(
% 0.20/15.54 ~sP2_prd|sP3_prd|~e1=e1),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1090,f1289])).
% 0.20/15.54 fof(f1387,plain,(
% 0.20/15.54 ~sP2_prd|sP3_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1386])).
% 0.20/15.54 fof(f1399,plain,(
% 0.20/15.54 op(e2,e3)=e4|sP2_prd),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1403,f1285])).
% 0.20/15.54 fof(f1403,plain,(
% 0.20/15.54 op(e4,e3)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1303,f202])).
% 0.20/15.54 fof(f1407,plain,(
% 0.20/15.54 ~sP15_prd|sP16_prd|~e3=e3),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1178,f1306])).
% 0.20/15.54 fof(f1408,plain,(
% 0.20/15.54 ~sP15_prd|sP16_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1407])).
% 0.20/15.54 fof(f1410,plain,(
% 0.20/15.54 op(e1,e2)=e3),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1232,f1311])).
% 0.20/15.54 fof(f1411,plain,(
% 0.20/15.54 op(e3,e2)=e4|e1=e4),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1236,f1311])).
% 0.20/15.54 fof(f1426,plain,(
% 0.20/15.54 ~sP12_prd|sP13_prd|~e1=e1),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f206,f1343])).
% 0.20/15.54 fof(f1427,plain,(
% 0.20/15.54 ~sP12_prd|sP13_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1426])).
% 0.20/15.54 fof(f1438,plain,(
% 0.20/15.54 ~sP18_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f623,f1358])).
% 0.20/15.54 fof(f1442,plain,(
% 0.20/15.54 ~sP10_prd|sP11_prd|e4=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1324,f1361])).
% 0.20/15.54 fof(f1443,plain,(
% 0.20/15.54 ~sP10_prd|sP11_prd),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1442,f203])).
% 0.20/15.54 fof(f1453,plain,(
% 0.20/15.54 ~sP7_prd|sP8_prd|~op(e2,e3)=e1),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1461,f299])).
% 0.20/15.54 fof(f1461,plain,(
% 0.20/15.54 op(e3,e1)=e2),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1380,f196])).
% 0.20/15.54 fof(f1466,plain,(
% 0.20/15.54 e1=e4|sP2_prd),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1243,f1399])).
% 0.20/15.54 fof(f1467,plain,(
% 0.20/15.54 sP3_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1387,f1468])).
% 0.20/15.54 fof(f1468,plain,(
% 0.20/15.54 sP2_prd),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1466,f201])).
% 0.20/15.54 fof(f1471,plain,(
% 0.20/15.54 ~sP16_prd|sP17_prd|~op(e3,e1)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1410,f371])).
% 0.20/15.54 fof(f1482,plain,(
% 0.20/15.54 ~sP6_prd|sP7_prd|~op(e4,e3)=e2),
% 0.20/15.54 inference(backward_demodulation,[status(thm)],[f1490,f291])).
% 0.20/15.54 fof(f1490,plain,(
% 0.20/15.54 op(e3,e2)=e4),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1411,f201])).
% 0.20/15.54 fof(f1497,plain,(
% 0.20/15.54 ~sP17_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f496,f1438])).
% 0.20/15.54 fof(f1498,plain,(
% 0.20/15.54 ~sP7_prd|sP8_prd|~e1=e1),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1243,f1453])).
% 0.20/15.54 fof(f1499,plain,(
% 0.20/15.54 ~sP7_prd|sP8_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1498])).
% 0.20/15.54 fof(f1502,plain,(
% 0.20/15.54 sP4_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1057,f1467])).
% 0.20/15.54 fof(f1503,plain,(
% 0.20/15.54 ~sP16_prd|sP17_prd|~e2=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1461,f1471])).
% 0.20/15.54 fof(f1504,plain,(
% 0.20/15.54 ~sP16_prd|sP17_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1503])).
% 0.20/15.54 fof(f1511,plain,(
% 0.20/15.54 ~sP6_prd|sP7_prd|~e2=e2),
% 0.20/15.54 inference(forward_demodulation,[status(thm)],[f1403,f1482])).
% 0.20/15.54 fof(f1512,plain,(
% 0.20/15.54 ~sP6_prd|sP7_prd),
% 0.20/15.54 inference(trivial_equality_resolution,[status(thm)],[f1511])).
% 0.20/15.54 fof(f1518,plain,(
% 0.20/15.54 ~sP16_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1504,f1497])).
% 0.20/15.54 fof(f1519,plain,(
% 0.20/15.54 sP5_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1261,f1502])).
% 0.20/15.54 fof(f1520,plain,(
% 0.20/15.54 ~sP15_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1408,f1518])).
% 0.20/15.54 fof(f1521,plain,(
% 0.20/15.54 sP6_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f485,f1519])).
% 0.20/15.54 fof(f1522,plain,(
% 0.20/15.54 ~sP14_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1278,f1520])).
% 0.20/15.54 fof(f1523,plain,(
% 0.20/15.54 sP7_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1512,f1521])).
% 0.20/15.54 fof(f1524,plain,(
% 0.20/15.54 ~sP13_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1216,f1522])).
% 0.20/15.54 fof(f1525,plain,(
% 0.20/15.54 sP8_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1499,f1523])).
% 0.20/15.54 fof(f1526,plain,(
% 0.20/15.54 ~sP12_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1427,f1524])).
% 0.20/15.54 fof(f1527,plain,(
% 0.20/15.54 sP10_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1162,f1525])).
% 0.20/15.54 fof(f1529,plain,(
% 0.20/15.54 ~sP11_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f495,f1526])).
% 0.20/15.54 fof(f1531,plain,(
% 0.20/15.54 sP11_prd),
% 0.20/15.54 inference(backward_subsumption_resolution,[status(thm)],[f1443,f1527])).
% 0.20/15.54 fof(f1532,plain,(
% 0.20/15.54 $false),
% 0.20/15.54 inference(forward_subsumption_resolution,[status(thm)],[f1531,f1529])).
% 0.20/15.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/15.58 % Elapsed time: 0.111904 seconds
% 0.20/15.58 % CPU time: 0.463728 seconds
% 0.20/15.58 % Total memory used: 124.330 MB
% 0.20/15.58 % Net memory used: 124.136 MB
%------------------------------------------------------------------------------