%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG064+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 : n003.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.15s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG064+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n003.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 12:56:47 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 0.15/0.41 % Refutation found
% 0.15/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.41 fof(f1,axiom,(
% 0.15/0.41 ( ( 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.15/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f2,axiom,(
% 0.15/0.41 ( 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.15/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f3,axiom,(
% 0.15/0.41 ( ( 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.15/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f4,axiom,(
% 0.15/0.41 ( 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.15/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f5,axiom,(
% 0.15/0.41 ( e0 != e1& e0 != e2& e0 != e3& e0 != e4& e1 != e2& e1 != e3& e1 != e4& e2 != e3& e2 != e4& e3 != e4 ) ),
% 0.15/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f6,axiom,(
% 0.15/0.41 ( e0 = op(e1,op(op(e1,e1),op(e1,e1)))& e2 = op(op(e1,e1),op(e1,e1))& e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))& e4 = op(e1,e1) ) ),
% 0.15/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f7,conjecture,(
% 0.15/0.41 ~ ( ( op(e0,e0) = e0| op(e1,e1) = e0| op(e2,e2) = e0| op(e3,e3) = e0| op(e4,e4) = e0 )& ( op(e0,e0) = e1| op(e1,e1) = e1| op(e2,e2) = e1| op(e3,e3) = e1| op(e4,e4) = e1 )& ( op(e0,e0) = e2| op(e1,e1) = e2| op(e2,e2) = e2| op(e3,e3) = e2| op(e4,e4) = e2 )& ( op(e0,e0) = e3| op(e1,e1) = e3| op(e2,e2) = e3| op(e3,e3) = e3| op(e4,e4) = e3 )& ( op(e0,e0) = e4| op(e1,e1) = e4| op(e2,e2) = e4| op(e3,e3) = e4| op(e4,e4) = e4 )& ( ( op(e0,e0) != op(e0,e0)& op(op(e0,e0),e0) = e0& op(op(e0,e0),e0) != e0 )| ( op(e1,e0) != op(e0,e1)& op(op(e0,e1),e1) = e0& op(op(e0,e1),e0) != e1 )| ( op(e2,e0) != op(e0,e2)& op(op(e0,e2),e2) = e0& op(op(e0,e2),e0) != e2 )| ( op(e3,e0) != op(e0,e3)& op(op(e0,e3),e3) = e0& op(op(e0,e3),e0) != e3 )| ( op(e4,e0) != op(e0,e4)& op(op(e0,e4),e4) = e0& op(op(e0,e4),e0) != e4 )| ( op(e0,e1) != op(e1,e0)& op(op(e1,e0),e0) = e1& op(op(e1,e0),e1) != e0 )| ( op(e1,e1) != op(e1,e1)& op(op(e1,e1),e1) = e1& op(op(e1,e1),e1) != e1 )| ( op(e2,e1) != op(e1,e2)& op(op(e1,e2),e2) = e1& op(op(e1,e2),e1) != e2 )| ( op(e3,e1) != op(e1,e3)& op(op(e1,e3),e3) = e1& op(op(e1,e3),e1) != e3 )| ( op(e4,e1) != op(e1,e4)& op(op(e1,e4),e4) = e1& op(op(e1,e4),e1) != e4 )| ( op(e0,e2) != op(e2,e0)& op(op(e2,e0),e0) = e2& op(op(e2,e0),e2) != e0 )| ( op(e1,e2) != op(e2,e1)& op(op(e2,e1),e1) = e2& op(op(e2,e1),e2) != e1 )| ( op(e2,e2) != op(e2,e2)& op(op(e2,e2),e2) = e2& op(op(e2,e2),e2) != e2 )| ( op(e3,e2) != op(e2,e3)& op(op(e2,e3),e3) = e2& op(op(e2,e3),e2) != e3 )| ( op(e4,e2) != op(e2,e4)& op(op(e2,e4),e4) = e2& op(op(e2,e4),e2) != e4 )| ( op(e0,e3) != op(e3,e0)& op(op(e3,e0),e0) = e3& op(op(e3,e0),e3) != e0 )| ( op(e1,e3) != op(e3,e1)& op(op(e3,e1),e1) = e3& op(op(e3,e1),e3) != e1 )| ( op(e2,e3) != op(e3,e2)& op(op(e3,e2),e2) = e3& op(op(e3,e2),e3) != e2 )| ( op(e3,e3) != op(e3,e3)& op(op(e3,e3),e3) = e3& op(op(e3,e3),e3) != e3 )| ( op(e4,e3) != op(e3,e4)& op(op(e3,e4),e4) = e3& op(op(e3,e4),e3) != e4 )| ( op(e0,e4) != op(e4,e0)& op(op(e4,e0),e0) = e4& op(op(e4,e0),e4) != e0 )| ( op(e1,e4) != op(e4,e1)& op(op(e4,e1),e1) = e4& op(op(e4,e1),e4) != e1 )| ( op(e2,e4) != op(e4,e2)& op(op(e4,e2),e2) = e4& op(op(e4,e2),e4) != e2 )| ( op(e3,e4) != op(e4,e3)& op(op(e4,e3),e3) = e4& op(op(e4,e3),e4) != e3 )| ( op(e4,e4) != op(e4,e4)& op(op(e4,e4),e4) = e4& op(op(e4,e4),e4) != e4 ) ) ) ),
% 0.15/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.41 fof(f8,negated_conjecture,(
% 0.15/0.41 ~(~ ( ( op(e0,e0) = e0| op(e1,e1) = e0| op(e2,e2) = e0| op(e3,e3) = e0| op(e4,e4) = e0 )& ( op(e0,e0) = e1| op(e1,e1) = e1| op(e2,e2) = e1| op(e3,e3) = e1| op(e4,e4) = e1 )& ( op(e0,e0) = e2| op(e1,e1) = e2| op(e2,e2) = e2| op(e3,e3) = e2| op(e4,e4) = e2 )& ( op(e0,e0) = e3| op(e1,e1) = e3| op(e2,e2) = e3| op(e3,e3) = e3| op(e4,e4) = e3 )& ( op(e0,e0) = e4| op(e1,e1) = e4| op(e2,e2) = e4| op(e3,e3) = e4| op(e4,e4) = e4 )& ( ( op(e0,e0) != op(e0,e0)& op(op(e0,e0),e0) = e0& op(op(e0,e0),e0) != e0 )| ( op(e1,e0) != op(e0,e1)& op(op(e0,e1),e1) = e0& op(op(e0,e1),e0) != e1 )| ( op(e2,e0) != op(e0,e2)& op(op(e0,e2),e2) = e0& op(op(e0,e2),e0) != e2 )| ( op(e3,e0) != op(e0,e3)& op(op(e0,e3),e3) = e0& op(op(e0,e3),e0) != e3 )| ( op(e4,e0) != op(e0,e4)& op(op(e0,e4),e4) = e0& op(op(e0,e4),e0) != e4 )| ( op(e0,e1) != op(e1,e0)& op(op(e1,e0),e0) = e1& op(op(e1,e0),e1) != e0 )| ( op(e1,e1) != op(e1,e1)& op(op(e1,e1),e1) = e1& op(op(e1,e1),e1) != e1 )| ( op(e2,e1) != op(e1,e2)& op(op(e1,e2),e2) = e1& op(op(e1,e2),e1) != e2 )| ( op(e3,e1) != op(e1,e3)& op(op(e1,e3),e3) = e1& op(op(e1,e3),e1) != e3 )| ( op(e4,e1) != op(e1,e4)& op(op(e1,e4),e4) = e1& op(op(e1,e4),e1) != e4 )| ( op(e0,e2) != op(e2,e0)& op(op(e2,e0),e0) = e2& op(op(e2,e0),e2) != e0 )| ( op(e1,e2) != op(e2,e1)& op(op(e2,e1),e1) = e2& op(op(e2,e1),e2) != e1 )| ( op(e2,e2) != op(e2,e2)& op(op(e2,e2),e2) = e2& op(op(e2,e2),e2) != e2 )| ( op(e3,e2) != op(e2,e3)& op(op(e2,e3),e3) = e2& op(op(e2,e3),e2) != e3 )| ( op(e4,e2) != op(e2,e4)& op(op(e2,e4),e4) = e2& op(op(e2,e4),e2) != e4 )| ( op(e0,e3) != op(e3,e0)& op(op(e3,e0),e0) = e3& op(op(e3,e0),e3) != e0 )| ( op(e1,e3) != op(e3,e1)& op(op(e3,e1),e1) = e3& op(op(e3,e1),e3) != e1 )| ( op(e2,e3) != op(e3,e2)& op(op(e3,e2),e2) = e3& op(op(e3,e2),e3) != e2 )| ( op(e3,e3) != op(e3,e3)& op(op(e3,e3),e3) = e3& op(op(e3,e3),e3) != e3 )| ( op(e4,e3) != op(e3,e4)& op(op(e3,e4),e4) = e3& op(op(e3,e4),e3) != e4 )| ( op(e0,e4) != op(e4,e0)& op(op(e4,e0),e0) = e4& op(op(e4,e0),e4) != e0 )| ( op(e1,e4) != op(e4,e1)& op(op(e4,e1),e1) = e4& op(op(e4,e1),e4) != e1 )| ( op(e2,e4) != op(e4,e2)& op(op(e4,e2),e2) = e4& op(op(e4,e2),e4) != e2 )| ( op(e3,e4) != op(e4,e3)& op(op(e4,e3),e3) = e4& op(op(e4,e3),e4) != e3 )| ( op(e4,e4) != op(e4,e4)& op(op(e4,e4),e4) = e4& op(op(e4,e4),e4) != e4 ) ) ) )),
% 0.15/0.41 inference(negated_conjecture,[status(cth)],[f7])).
% 0.15/0.41 fof(f20,plain,(
% 0.15/0.41 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e3|op(e2,e1)=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f1])).
% 0.15/0.41 fof(f31,plain,(
% 0.15/0.41 op(e4,e2)=e0|op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e3|op(e4,e2)=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f1])).
% 0.15/0.41 fof(f35,plain,(
% 0.15/0.41 op(e0,unit)=e0),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f36,plain,(
% 0.15/0.41 op(unit,e1)=e1),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f37,plain,(
% 0.15/0.41 op(e1,unit)=e1),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f38,plain,(
% 0.15/0.41 op(unit,e2)=e2),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f39,plain,(
% 0.15/0.41 op(e2,unit)=e2),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f40,plain,(
% 0.15/0.41 op(unit,e3)=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f41,plain,(
% 0.15/0.41 op(e3,unit)=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f42,plain,(
% 0.15/0.41 op(unit,e4)=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f43,plain,(
% 0.15/0.41 op(e4,unit)=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f44,plain,(
% 0.15/0.41 unit=e0|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.41 fof(f59,plain,(
% 0.15/0.41 op(e1,e0)=e2|op(e1,e1)=e2|op(e1,e2)=e2|op(e1,e3)=e2|op(e1,e4)=e2),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f60,plain,(
% 0.15/0.41 op(e0,e1)=e2|op(e1,e1)=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f67,plain,(
% 0.15/0.41 op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e2)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f74,plain,(
% 0.15/0.41 op(e0,e2)=e4|op(e1,e2)=e4|op(e2,e2)=e4|op(e3,e2)=e4|op(e4,e2)=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f75,plain,(
% 0.15/0.41 op(e3,e0)=e0|op(e3,e1)=e0|op(e3,e2)=e0|op(e3,e3)=e0|op(e3,e4)=e0),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f76,plain,(
% 0.15/0.41 op(e0,e3)=e0|op(e1,e3)=e0|op(e2,e3)=e0|op(e3,e3)=e0|op(e4,e3)=e0),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f77,plain,(
% 0.15/0.41 op(e3,e0)=e1|op(e3,e1)=e1|op(e3,e2)=e1|op(e3,e3)=e1|op(e3,e4)=e1),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f84,plain,(
% 0.15/0.41 op(e0,e3)=e4|op(e1,e3)=e4|op(e2,e3)=e4|op(e3,e3)=e4|op(e4,e3)=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f91,plain,(
% 0.15/0.41 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e2)=e3|op(e4,e3)=e3|op(e4,e4)=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f92,plain,(
% 0.15/0.41 op(e0,e4)=e3|op(e1,e4)=e3|op(e2,e4)=e3|op(e3,e4)=e3|op(e4,e4)=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.41 fof(f106,plain,(
% 0.15/0.41 ~op(e0,e1)=op(e2,e1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f107,plain,(
% 0.15/0.41 ~op(e0,e1)=op(e3,e1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f109,plain,(
% 0.15/0.41 ~op(e1,e1)=op(e2,e1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f110,plain,(
% 0.15/0.41 ~op(e1,e1)=op(e3,e1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f111,plain,(
% 0.15/0.41 ~op(e1,e1)=op(e4,e1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f112,plain,(
% 0.15/0.41 ~op(e2,e1)=op(e3,e1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f120,plain,(
% 0.15/0.41 ~op(e1,e2)=op(e3,e2)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f121,plain,(
% 0.15/0.41 ~op(e1,e2)=op(e4,e2)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f122,plain,(
% 0.15/0.41 ~op(e2,e2)=op(e3,e2)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f123,plain,(
% 0.15/0.41 ~op(e2,e2)=op(e4,e2)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f127,plain,(
% 0.15/0.41 ~op(e0,e3)=op(e3,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f128,plain,(
% 0.15/0.41 ~op(e0,e3)=op(e4,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f132,plain,(
% 0.15/0.41 ~op(e2,e3)=op(e3,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f141,plain,(
% 0.15/0.41 ~op(e1,e4)=op(e4,e4)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f142,plain,(
% 0.15/0.41 ~op(e2,e4)=op(e3,e4)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f147,plain,(
% 0.15/0.41 ~op(e0,e0)=op(e0,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f160,plain,(
% 0.15/0.41 ~op(e1,e1)=op(e1,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f162,plain,(
% 0.15/0.41 ~op(e1,e2)=op(e1,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f165,plain,(
% 0.15/0.41 ~op(e2,e0)=op(e2,e1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f169,plain,(
% 0.15/0.41 ~op(e2,e1)=op(e2,e2)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f173,plain,(
% 0.15/0.41 ~op(e2,e2)=op(e2,e4)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f178,plain,(
% 0.15/0.41 ~op(e3,e0)=op(e3,e4)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f182,plain,(
% 0.15/0.41 ~op(e3,e2)=op(e3,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f186,plain,(
% 0.15/0.41 ~op(e4,e0)=op(e4,e2)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f187,plain,(
% 0.15/0.41 ~op(e4,e0)=op(e4,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f191,plain,(
% 0.15/0.41 ~op(e4,e1)=op(e4,e4)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f193,plain,(
% 0.15/0.41 ~op(e4,e2)=op(e4,e4)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f194,plain,(
% 0.15/0.41 ~op(e4,e3)=op(e4,e4)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.41 fof(f195,plain,(
% 0.15/0.41 ~e0=e1),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f196,plain,(
% 0.15/0.41 ~e0=e2),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f197,plain,(
% 0.15/0.41 ~e0=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f198,plain,(
% 0.15/0.41 ~e0=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f199,plain,(
% 0.15/0.41 ~e1=e2),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f200,plain,(
% 0.15/0.41 ~e1=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f201,plain,(
% 0.15/0.41 ~e1=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f202,plain,(
% 0.15/0.41 ~e2=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f203,plain,(
% 0.15/0.41 ~e2=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f204,plain,(
% 0.15/0.41 ~e3=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.41 fof(f205,plain,(
% 0.15/0.41 e0=op(e1,op(op(e1,e1),op(e1,e1)))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f6])).
% 0.15/0.41 fof(f206,plain,(
% 0.15/0.41 e2=op(op(e1,e1),op(e1,e1))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f6])).
% 0.15/0.41 fof(f207,plain,(
% 0.15/0.41 e3=op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f6])).
% 0.15/0.41 fof(f208,plain,(
% 0.15/0.41 e4=op(e1,e1)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f6])).
% 0.15/0.41 fof(f209,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.15/0.41 fof(f210,plain,(
% 0.15/0.41 ((((((((op(e0,e0)=e0|op(e1,e1)=e0)|op(e2,e2)=e0)|op(e3,e3)=e0)|op(e4,e4)=e0)&((((op(e0,e0)=e1|op(e1,e1)=e1)|op(e2,e2)=e1)|op(e3,e3)=e1)|op(e4,e4)=e1))&((((op(e0,e0)=e2|op(e1,e1)=e2)|op(e2,e2)=e2)|op(e3,e3)=e2)|op(e4,e4)=e2))&((((op(e0,e0)=e3|op(e1,e1)=e3)|op(e2,e2)=e3)|op(e3,e3)=e3)|op(e4,e4)=e3))&((((op(e0,e0)=e4|op(e1,e1)=e4)|op(e2,e2)=e4)|op(e3,e3)=e4)|op(e4,e4)=e4))&(sP0_prd|((~op(e4,e4)=op(e4,e4)&op(op(e4,e4),e4)=e4)&~op(op(e4,e4),e4)=e4))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f8,f209])).
% 0.15/0.41 fof(f211,plain,(
% 0.15/0.41 op(e0,e0)=e0|op(e1,e1)=e0|op(e2,e2)=e0|op(e3,e3)=e0|op(e4,e4)=e0),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f210])).
% 0.15/0.41 fof(f212,plain,(
% 0.15/0.41 op(e0,e0)=e1|op(e1,e1)=e1|op(e2,e2)=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f210])).
% 0.15/0.41 fof(f216,plain,(
% 0.15/0.41 sP0_prd|~op(e4,e4)=op(e4,e4)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f210])).
% 0.15/0.41 fof(f219,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.15/0.41 fof(f220,plain,(
% 0.15/0.41 sP0_prd<=>(sP1_prd|((~op(e3,e4)=op(e4,e3)&op(op(e4,e3),e3)=e4)&~op(op(e4,e3),e4)=e3))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f209,f219])).
% 0.15/0.41 fof(f221,plain,(
% 0.15/0.41 (~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.15/0.41 inference(NNF_transformation,[status(thm)],[f220])).
% 0.15/0.41 fof(f222,plain,(
% 0.15/0.41 ~sP0_prd|sP1_prd|~op(e3,e4)=op(e4,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f221])).
% 0.15/0.41 fof(f227,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.15/0.41 fof(f228,plain,(
% 0.15/0.41 sP1_prd<=>(sP2_prd|((~op(e2,e4)=op(e4,e2)&op(op(e4,e2),e2)=e4)&~op(op(e4,e2),e4)=e2))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f219,f227])).
% 0.15/0.41 fof(f229,plain,(
% 0.15/0.41 (~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.15/0.41 inference(NNF_transformation,[status(thm)],[f228])).
% 0.15/0.41 fof(f231,plain,(
% 0.15/0.41 ~sP1_prd|sP2_prd|op(op(e4,e2),e2)=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f229])).
% 0.15/0.41 fof(f235,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.15/0.41 fof(f236,plain,(
% 0.15/0.41 sP2_prd<=>(sP3_prd|((~op(e1,e4)=op(e4,e1)&op(op(e4,e1),e1)=e4)&~op(op(e4,e1),e4)=e1))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f227,f235])).
% 0.15/0.41 fof(f237,plain,(
% 0.15/0.41 (~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.15/0.41 inference(NNF_transformation,[status(thm)],[f236])).
% 0.15/0.41 fof(f239,plain,(
% 0.15/0.41 ~sP2_prd|sP3_prd|op(op(e4,e1),e1)=e4),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f237])).
% 0.15/0.41 fof(f243,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.15/0.41 fof(f244,plain,(
% 0.15/0.41 sP3_prd<=>(sP4_prd|((~op(e0,e4)=op(e4,e0)&op(op(e4,e0),e0)=e4)&~op(op(e4,e0),e4)=e0))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f235,f243])).
% 0.15/0.41 fof(f245,plain,(
% 0.15/0.41 (~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.15/0.41 inference(NNF_transformation,[status(thm)],[f244])).
% 0.15/0.41 fof(f246,plain,(
% 0.15/0.41 ~sP3_prd|sP4_prd|~op(e0,e4)=op(e4,e0)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f245])).
% 0.15/0.41 fof(f251,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.15/0.41 fof(f252,plain,(
% 0.15/0.41 sP4_prd<=>(sP5_prd|((~op(e4,e3)=op(e3,e4)&op(op(e3,e4),e4)=e3)&~op(op(e3,e4),e3)=e4))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f243,f251])).
% 0.15/0.41 fof(f253,plain,(
% 0.15/0.41 (~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.15/0.41 inference(NNF_transformation,[status(thm)],[f252])).
% 0.15/0.41 fof(f255,plain,(
% 0.15/0.41 ~sP4_prd|sP5_prd|op(op(e3,e4),e4)=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f253])).
% 0.15/0.41 fof(f259,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.15/0.41 fof(f260,plain,(
% 0.15/0.41 sP5_prd<=>(sP6_prd|((~op(e3,e3)=op(e3,e3)&op(op(e3,e3),e3)=e3)&~op(op(e3,e3),e3)=e3))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f251,f259])).
% 0.15/0.41 fof(f261,plain,(
% 0.15/0.41 (~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.15/0.41 inference(NNF_transformation,[status(thm)],[f260])).
% 0.15/0.41 fof(f262,plain,(
% 0.15/0.41 ~sP5_prd|sP6_prd|~op(e3,e3)=op(e3,e3)),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f261])).
% 0.15/0.41 fof(f267,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.15/0.41 fof(f268,plain,(
% 0.15/0.41 sP6_prd<=>(sP7_prd|((~op(e2,e3)=op(e3,e2)&op(op(e3,e2),e2)=e3)&~op(op(e3,e2),e3)=e2))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f259,f267])).
% 0.15/0.41 fof(f269,plain,(
% 0.15/0.41 (~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.15/0.41 inference(NNF_transformation,[status(thm)],[f268])).
% 0.15/0.41 fof(f271,plain,(
% 0.15/0.41 ~sP6_prd|sP7_prd|op(op(e3,e2),e2)=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f269])).
% 0.15/0.41 fof(f275,definition,(
% 0.15/0.41 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.15/0.41 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.15/0.41 fof(f276,plain,(
% 0.15/0.41 sP7_prd<=>(sP8_prd|((~op(e1,e3)=op(e3,e1)&op(op(e3,e1),e1)=e3)&~op(op(e3,e1),e3)=e1))),
% 0.15/0.41 inference(formula_renaming,[status(thm)],[f267,f275])).
% 0.15/0.41 fof(f277,plain,(
% 0.15/0.41 (~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.15/0.41 inference(NNF_transformation,[status(thm)],[f276])).
% 0.15/0.41 fof(f279,plain,(
% 0.15/0.41 ~sP7_prd|sP8_prd|op(op(e3,e1),e1)=e3),
% 0.15/0.41 inference(cnf_transformation,[status(thm)],[f277])).
% 0.15/0.41 fof(f283,definition,(
% 0.15/0.41 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.15/0.42 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.15/0.42 fof(f284,plain,(
% 0.15/0.42 sP8_prd<=>(sP9_prd|((~op(e0,e3)=op(e3,e0)&op(op(e3,e0),e0)=e3)&~op(op(e3,e0),e3)=e0))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f275,f283])).
% 0.15/0.42 fof(f285,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f284])).
% 0.15/0.42 fof(f286,plain,(
% 0.15/0.42 ~sP8_prd|sP9_prd|~op(e0,e3)=op(e3,e0)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f285])).
% 0.15/0.42 fof(f291,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.15/0.42 fof(f292,plain,(
% 0.15/0.42 sP9_prd<=>(sP10_prd|((~op(e4,e2)=op(e2,e4)&op(op(e2,e4),e4)=e2)&~op(op(e2,e4),e2)=e4))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f283,f291])).
% 0.15/0.42 fof(f293,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f292])).
% 0.15/0.42 fof(f295,plain,(
% 0.15/0.42 ~sP9_prd|sP10_prd|op(op(e2,e4),e4)=e2),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f293])).
% 0.15/0.42 fof(f299,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.15/0.42 fof(f300,plain,(
% 0.15/0.42 sP10_prd<=>(sP11_prd|((~op(e3,e2)=op(e2,e3)&op(op(e2,e3),e3)=e2)&~op(op(e2,e3),e2)=e3))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f291,f299])).
% 0.15/0.42 fof(f301,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f300])).
% 0.15/0.42 fof(f303,plain,(
% 0.15/0.42 ~sP10_prd|sP11_prd|op(op(e2,e3),e3)=e2),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f301])).
% 0.15/0.42 fof(f307,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.15/0.42 fof(f308,plain,(
% 0.15/0.42 sP11_prd<=>(sP12_prd|((~op(e2,e2)=op(e2,e2)&op(op(e2,e2),e2)=e2)&~op(op(e2,e2),e2)=e2))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f299,f307])).
% 0.15/0.42 fof(f309,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f308])).
% 0.15/0.42 fof(f310,plain,(
% 0.15/0.42 ~sP11_prd|sP12_prd|~op(e2,e2)=op(e2,e2)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f309])).
% 0.15/0.42 fof(f315,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.15/0.42 fof(f316,plain,(
% 0.15/0.42 sP12_prd<=>(sP13_prd|((~op(e1,e2)=op(e2,e1)&op(op(e2,e1),e1)=e2)&~op(op(e2,e1),e2)=e1))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f307,f315])).
% 0.15/0.42 fof(f317,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f316])).
% 0.15/0.42 fof(f319,plain,(
% 0.15/0.42 ~sP12_prd|sP13_prd|op(op(e2,e1),e1)=e2),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f317])).
% 0.15/0.42 fof(f323,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.15/0.42 fof(f324,plain,(
% 0.15/0.42 sP13_prd<=>(sP14_prd|((~op(e0,e2)=op(e2,e0)&op(op(e2,e0),e0)=e2)&~op(op(e2,e0),e2)=e0))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f315,f323])).
% 0.15/0.42 fof(f325,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f324])).
% 0.15/0.42 fof(f326,plain,(
% 0.15/0.42 ~sP13_prd|sP14_prd|~op(e0,e2)=op(e2,e0)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f325])).
% 0.15/0.42 fof(f331,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.15/0.42 fof(f332,plain,(
% 0.15/0.42 sP14_prd<=>(sP15_prd|((~op(e4,e1)=op(e1,e4)&op(op(e1,e4),e4)=e1)&~op(op(e1,e4),e1)=e4))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f323,f331])).
% 0.15/0.42 fof(f333,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f332])).
% 0.15/0.42 fof(f334,plain,(
% 0.15/0.42 ~sP14_prd|sP15_prd|~op(e4,e1)=op(e1,e4)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f333])).
% 0.15/0.42 fof(f339,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 0.15/0.42 fof(f340,plain,(
% 0.15/0.42 sP15_prd<=>(sP16_prd|((~op(e3,e1)=op(e1,e3)&op(op(e1,e3),e3)=e1)&~op(op(e1,e3),e1)=e3))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f331,f339])).
% 0.15/0.42 fof(f341,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f340])).
% 0.15/0.42 fof(f343,plain,(
% 0.15/0.42 ~sP15_prd|sP16_prd|op(op(e1,e3),e3)=e1),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f341])).
% 0.15/0.42 fof(f347,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP17_prd])],[])).
% 0.15/0.42 fof(f348,plain,(
% 0.15/0.42 sP16_prd<=>(sP17_prd|((~op(e2,e1)=op(e1,e2)&op(op(e1,e2),e2)=e1)&~op(op(e1,e2),e1)=e2))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f339,f347])).
% 0.15/0.42 fof(f349,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f348])).
% 0.15/0.42 fof(f351,plain,(
% 0.15/0.42 ~sP16_prd|sP17_prd|op(op(e1,e2),e2)=e1),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f349])).
% 0.15/0.42 fof(f355,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.15/0.42 fof(f356,plain,(
% 0.15/0.42 sP17_prd<=>(sP18_prd|((~op(e1,e1)=op(e1,e1)&op(op(e1,e1),e1)=e1)&~op(op(e1,e1),e1)=e1))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f347,f355])).
% 0.15/0.42 fof(f357,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f356])).
% 0.15/0.42 fof(f358,plain,(
% 0.15/0.42 ~sP17_prd|sP18_prd|~op(e1,e1)=op(e1,e1)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f357])).
% 0.15/0.42 fof(f363,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.15/0.42 fof(f364,plain,(
% 0.15/0.42 sP18_prd<=>(sP19_prd|((~op(e0,e1)=op(e1,e0)&op(op(e1,e0),e0)=e1)&~op(op(e1,e0),e1)=e0))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f355,f363])).
% 0.15/0.42 fof(f365,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f364])).
% 0.15/0.42 fof(f366,plain,(
% 0.15/0.42 ~sP18_prd|sP19_prd|~op(e0,e1)=op(e1,e0)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f365])).
% 0.15/0.42 fof(f371,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.15/0.42 fof(f372,plain,(
% 0.15/0.42 sP19_prd<=>(sP20_prd|((~op(e4,e0)=op(e0,e4)&op(op(e0,e4),e4)=e0)&~op(op(e0,e4),e0)=e4))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f363,f371])).
% 0.15/0.42 fof(f373,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f372])).
% 0.15/0.42 fof(f374,plain,(
% 0.15/0.42 ~sP19_prd|sP20_prd|~op(e4,e0)=op(e0,e4)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f373])).
% 0.15/0.42 fof(f379,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP21_prd])],[])).
% 0.15/0.42 fof(f380,plain,(
% 0.15/0.42 sP20_prd<=>(sP21_prd|((~op(e3,e0)=op(e0,e3)&op(op(e0,e3),e3)=e0)&~op(op(e0,e3),e0)=e3))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f371,f379])).
% 0.15/0.42 fof(f381,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f380])).
% 0.15/0.42 fof(f382,plain,(
% 0.15/0.42 ~sP20_prd|sP21_prd|~op(e3,e0)=op(e0,e3)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f381])).
% 0.15/0.42 fof(f387,definition,(
% 0.15/0.42 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.15/0.42 introduced(definition,[new_symbols(definition,[sP22_prd])],[])).
% 0.15/0.42 fof(f388,plain,(
% 0.15/0.42 sP21_prd<=>(sP22_prd|((~op(e2,e0)=op(e0,e2)&op(op(e0,e2),e2)=e0)&~op(op(e0,e2),e0)=e2))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f379,f387])).
% 0.15/0.42 fof(f389,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f388])).
% 0.15/0.42 fof(f392,plain,(
% 0.15/0.42 ~sP21_prd|sP22_prd|~op(op(e0,e2),e0)=e2),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f389])).
% 0.15/0.42 fof(f395,definition,(
% 0.15/0.42 sP23_prd<=>((~op(e0,e0)=op(e0,e0)&op(op(e0,e0),e0)=e0)&~op(op(e0,e0),e0)=e0)),
% 0.15/0.42 introduced(definition,[new_symbols(definition,[sP23_prd])],[])).
% 0.15/0.42 fof(f396,plain,(
% 0.15/0.42 sP22_prd<=>(sP23_prd|((~op(e1,e0)=op(e0,e1)&op(op(e0,e1),e1)=e0)&~op(op(e0,e1),e0)=e1))),
% 0.15/0.42 inference(formula_renaming,[status(thm)],[f387,f395])).
% 0.15/0.42 fof(f397,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f396])).
% 0.15/0.42 fof(f398,plain,(
% 0.15/0.42 ~sP22_prd|sP23_prd|~op(e1,e0)=op(e0,e1)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f397])).
% 0.15/0.42 fof(f403,plain,(
% 0.15/0.42 (~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.15/0.42 inference(NNF_transformation,[status(thm)],[f395])).
% 0.15/0.42 fof(f404,plain,(
% 0.15/0.42 ~sP23_prd|~op(e0,e0)=op(e0,e0)),
% 0.15/0.42 inference(cnf_transformation,[status(thm)],[f403])).
% 0.15/0.42 fof(f408,plain,(
% 0.15/0.42 e0=op(e1,e2)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f206,f205])).
% 0.15/0.42 fof(f409,plain,(
% 0.15/0.42 e3=op(e2,op(op(e1,e1),op(e1,e1)))),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f206,f207])).
% 0.15/0.42 fof(f410,plain,(
% 0.15/0.42 ~e3=op(e2,e4)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f429,f173])).
% 0.15/0.42 fof(f412,plain,(
% 0.15/0.42 ~op(e2,e1)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f429,f169])).
% 0.15/0.42 fof(f414,plain,(
% 0.15/0.42 ~e3=op(e4,e2)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f429,f123])).
% 0.15/0.42 fof(f415,plain,(
% 0.15/0.42 ~e3=op(e3,e2)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f429,f122])).
% 0.15/0.42 fof(f418,plain,(
% 0.15/0.42 op(e0,e2)=e4|op(e1,e2)=e4|e3=e4|op(e3,e2)=e4|op(e4,e2)=e4),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f429,f74])).
% 0.15/0.42 fof(f425,plain,(
% 0.15/0.42 op(e2,e0)=e1|op(e2,e1)=e1|e3=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f429,f67])).
% 0.15/0.42 fof(f429,plain,(
% 0.15/0.42 e3=op(e2,e2)),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f206,f409])).
% 0.15/0.42 fof(f430,plain,(
% 0.15/0.42 e2=op(op(e1,e1),e4)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f208,f206])).
% 0.15/0.42 fof(f432,plain,(
% 0.15/0.42 ~e4=op(e1,e3)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f208,f160])).
% 0.15/0.42 fof(f435,plain,(
% 0.15/0.42 ~e4=op(e4,e1)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f208,f111])).
% 0.15/0.42 fof(f436,plain,(
% 0.15/0.42 ~e4=op(e3,e1)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f208,f110])).
% 0.15/0.42 fof(f437,plain,(
% 0.15/0.42 ~e4=op(e2,e1)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f208,f109])).
% 0.15/0.42 fof(f443,plain,(
% 0.15/0.42 op(e0,e1)=e2|e4=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f208,f60])).
% 0.15/0.42 fof(f444,plain,(
% 0.15/0.42 op(e1,e0)=e2|e4=e2|op(e1,e2)=e2|op(e1,e3)=e2|op(e1,e4)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f208,f59])).
% 0.15/0.42 fof(f450,plain,(
% 0.15/0.42 op(e0,e0)=e0|e4=e0|op(e2,e2)=e0|op(e3,e3)=e0|op(e4,e4)=e0),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f208,f211])).
% 0.15/0.42 fof(f451,plain,(
% 0.15/0.42 op(e0,e0)=e0|e4=e0|e3=e0|op(e3,e3)=e0|op(e4,e4)=e0),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f429,f450])).
% 0.15/0.42 fof(f452,plain,(
% 0.15/0.42 op(e0,e0)=e0|e3=e0|op(e3,e3)=e0|op(e4,e4)=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f451,f198])).
% 0.15/0.42 fof(f453,plain,(
% 0.15/0.42 op(e0,e0)=e1|e4=e1|op(e2,e2)=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f208,f212])).
% 0.15/0.42 fof(f454,plain,(
% 0.15/0.42 op(e0,e0)=e1|e4=e1|e3=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f429,f453])).
% 0.15/0.42 fof(f455,plain,(
% 0.15/0.42 op(e0,e0)=e1|e3=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f454,f201])).
% 0.15/0.42 fof(f460,plain,(
% 0.15/0.42 sP0_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f216])).
% 0.15/0.42 fof(f461,plain,(
% 0.15/0.42 sP1_prd|~op(e3,e4)=op(e4,e3)),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f222,f460])).
% 0.15/0.42 fof(f464,plain,(
% 0.15/0.42 ~sP5_prd|sP6_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f262])).
% 0.15/0.42 fof(f465,plain,(
% 0.15/0.42 ~sP11_prd|sP12_prd|~e3=op(e2,e2)),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f429,f310])).
% 0.15/0.42 fof(f466,plain,(
% 0.15/0.42 ~sP11_prd|sP12_prd|~e3=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f429,f465])).
% 0.15/0.42 fof(f467,plain,(
% 0.15/0.42 ~sP11_prd|sP12_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f466])).
% 0.15/0.42 fof(f470,plain,(
% 0.15/0.42 ~sP17_prd|sP18_prd|~e4=op(e1,e1)),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f208,f358])).
% 0.15/0.42 fof(f471,plain,(
% 0.15/0.42 ~sP17_prd|sP18_prd|~e4=e4),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f208,f470])).
% 0.15/0.42 fof(f472,plain,(
% 0.15/0.42 ~sP17_prd|sP18_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f471])).
% 0.15/0.42 fof(f477,plain,(
% 0.15/0.42 ~sP22_prd|~op(e1,e0)=op(e0,e1)),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f398,f478])).
% 0.15/0.42 fof(f478,plain,(
% 0.15/0.42 ~sP23_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f404])).
% 0.15/0.42 fof(f481,plain,(
% 0.15/0.42 ~sP16_prd|sP17_prd|op(e0,e2)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f408,f351])).
% 0.15/0.42 fof(f486,plain,(
% 0.15/0.42 ~e0=op(e1,e3)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f408,f162])).
% 0.15/0.42 fof(f488,plain,(
% 0.15/0.42 ~e0=op(e4,e2)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f408,f121])).
% 0.15/0.42 fof(f489,plain,(
% 0.15/0.42 ~e0=op(e3,e2)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f408,f120])).
% 0.15/0.42 fof(f492,plain,(
% 0.15/0.42 op(e0,e4)=e3|op(e1,e4)=e3|op(e3,e4)=e3|op(e4,e4)=e3),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f92,f410])).
% 0.15/0.42 fof(f496,plain,(
% 0.15/0.42 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e4),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f20,f412])).
% 0.15/0.42 fof(f499,plain,(
% 0.15/0.42 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3|op(e4,e4)=e3),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f91,f414])).
% 0.15/0.42 fof(f500,plain,(
% 0.15/0.42 op(e4,e2)=e0|op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e4),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f31,f414])).
% 0.15/0.42 fof(f506,plain,(
% 0.15/0.42 op(e0,e2)=e4|e0=e4|e3=e4|op(e3,e2)=e4|op(e4,e2)=e4),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f408,f418])).
% 0.15/0.42 fof(f507,plain,(
% 0.15/0.42 op(e0,e2)=e4|e3=e4|op(e3,e2)=e4|op(e4,e2)=e4),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f506,f198])).
% 0.15/0.42 fof(f514,plain,(
% 0.15/0.42 op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f425,f200])).
% 0.15/0.42 fof(f520,plain,(
% 0.15/0.42 op(e0,e0)=e1|e3=e1|op(e3,e3)=e1|e2=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f539,f455])).
% 0.15/0.42 fof(f521,plain,(
% 0.15/0.42 op(e0,e0)=e0|e3=e0|op(e3,e3)=e0|e2=e0),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f539,f452])).
% 0.15/0.42 fof(f522,plain,(
% 0.15/0.42 ~op(e4,e3)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f539,f194])).
% 0.15/0.42 fof(f523,plain,(
% 0.15/0.42 ~op(e4,e2)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f539,f193])).
% 0.15/0.42 fof(f524,plain,(
% 0.15/0.42 ~op(e4,e1)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f539,f191])).
% 0.15/0.42 fof(f528,plain,(
% 0.15/0.42 ~op(e1,e4)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f539,f141])).
% 0.15/0.42 fof(f539,plain,(
% 0.15/0.42 e2=op(e4,e4)),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f208,f430])).
% 0.15/0.42 fof(f541,plain,(
% 0.15/0.42 op(e0,e3)=e4|op(e2,e3)=e4|op(e3,e3)=e4|op(e4,e3)=e4),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f84,f432])).
% 0.15/0.42 fof(f555,plain,(
% 0.15/0.42 op(e0,e1)=e2|op(e2,e1)=e2|op(e3,e1)=e2|op(e4,e1)=e2),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f443,f203])).
% 0.15/0.42 fof(f556,plain,(
% 0.15/0.42 op(e1,e0)=e2|e4=e2|e0=e2|op(e1,e3)=e2|op(e1,e4)=e2),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f408,f444])).
% 0.15/0.42 fof(f557,plain,(
% 0.15/0.42 op(e1,e0)=e2|e0=e2|op(e1,e3)=e2|op(e1,e4)=e2),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f556,f203])).
% 0.15/0.42 fof(f564,plain,(
% 0.15/0.42 op(e0,e3)=e0|op(e2,e3)=e0|op(e3,e3)=e0|op(e4,e3)=e0),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f76,f486])).
% 0.15/0.42 fof(f566,plain,(
% 0.15/0.42 op(e3,e0)=e0|op(e3,e1)=e0|op(e3,e3)=e0|op(e3,e4)=e0),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f75,f489])).
% 0.15/0.42 fof(f568,plain,(
% 0.15/0.42 op(e0,e4)=e3|op(e1,e4)=e3|op(e3,e4)=e3|e2=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f539,f492])).
% 0.15/0.42 fof(f569,plain,(
% 0.15/0.42 op(e0,e4)=e3|op(e1,e4)=e3|op(e3,e4)=e3),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f568,f202])).
% 0.15/0.42 fof(f570,plain,(
% 0.15/0.42 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f496,f437])).
% 0.15/0.42 fof(f571,plain,(
% 0.15/0.42 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3|e2=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f539,f499])).
% 0.15/0.42 fof(f572,plain,(
% 0.15/0.42 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e3)=e3),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f571,f202])).
% 0.15/0.42 fof(f573,plain,(
% 0.15/0.42 op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e4),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f500,f488])).
% 0.15/0.42 fof(f576,plain,(
% 0.15/0.42 op(e0,e0)=e1|op(e3,e3)=e1|e2=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f520,f200])).
% 0.15/0.42 fof(f577,plain,(
% 0.15/0.42 op(e0,e0)=e0|op(e3,e3)=e0|e2=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f521,f197])).
% 0.15/0.42 fof(f580,plain,(
% 0.15/0.42 op(e4,e2)=e1|op(e4,e2)=e4),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f573,f523])).
% 0.15/0.42 fof(f582,plain,(
% 0.15/0.42 op(e0,e1)=e2|op(e2,e1)=e2|op(e3,e1)=e2),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f555,f524])).
% 0.15/0.42 fof(f589,plain,(
% 0.15/0.42 op(e1,e0)=e2|e0=e2|op(e1,e3)=e2),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f557,f528])).
% 0.15/0.42 fof(f605,plain,(
% 0.15/0.42 op(e1,e0)=e2|op(e1,e3)=e2),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f589,f196])).
% 0.15/0.42 fof(f625,plain,(
% 0.15/0.42 op(e4,e4)=e4|unit=e0|unit=e1|unit=e2|unit=e3),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f44,f43])).
% 0.15/0.42 fof(f639,plain,(
% 0.15/0.42 e2=e4|unit=e0|unit=e1|unit=e2|unit=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f539,f625])).
% 0.15/0.42 fof(f640,plain,(
% 0.15/0.42 unit=e0|unit=e1|unit=e2|unit=e3),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f639,f203])).
% 0.15/0.42 fof(f669,plain,(
% 0.15/0.42 ~op(e2,e4)=e1|op(e3,e0)=e1|op(e3,e1)=e1|op(e3,e2)=e1|op(e3,e3)=e1),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f77,f142])).
% 0.15/0.42 fof(f728,plain,(
% 0.15/0.42 sP16_prd|op(op(e1,e3),e3)=e1|~sP14_prd|~op(e4,e1)=op(e1,e4)),
% 0.15/0.42 inference(resolution,[status(thm)],[f343,f334])).
% 0.15/0.42 fof(f757,plain,(
% 0.15/0.42 sP22_prd|~op(op(e0,e2),e0)=e2|~sP20_prd|~op(e3,e0)=op(e0,e3)),
% 0.15/0.42 inference(resolution,[status(thm)],[f392,f382])).
% 0.15/0.42 fof(f771,plain,(
% 0.15/0.42 ~op(e2,e3)=e1|op(e0,e0)=e1|e2=e1),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f576,f132])).
% 0.15/0.42 fof(f779,plain,(
% 0.15/0.42 ~op(e2,e3)=e1|op(e0,e0)=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f771,f199])).
% 0.15/0.42 fof(f788,plain,(
% 0.15/0.42 ~op(e4,e0)=e4|op(e4,e2)=e1),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f580,f186])).
% 0.15/0.42 fof(f814,plain,(
% 0.15/0.42 op(e0,e3)=e0|unit=e0|unit=e1|unit=e2),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f640,f35])).
% 0.15/0.42 fof(f822,plain,(
% 0.15/0.42 ~op(e4,e0)=e4|op(e0,e2)=e4|e3=e4|op(e3,e2)=e4),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f507,f186])).
% 0.15/0.42 fof(f829,plain,(
% 0.15/0.42 ~op(e4,e0)=e4|op(e0,e2)=e4|op(e3,e2)=e4),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f822,f204])).
% 0.15/0.42 fof(f885,plain,(
% 0.15/0.42 ~op(e0,e3)=e0|op(e0,e0)=e0|e2=e0),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f577,f127])).
% 0.15/0.42 fof(f893,plain,(
% 0.15/0.42 ~op(e0,e3)=e0|op(e0,e0)=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f885,f196])).
% 0.15/0.42 fof(f957,plain,(
% 0.15/0.42 ~op(e3,e0)=e3|op(e0,e4)=e3|op(e1,e4)=e3),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f569,f178])).
% 0.15/0.42 fof(f1068,plain,(
% 0.15/0.42 unit=e0|unit=e1|unit=e2|op(e0,e0)=e0),
% 0.15/0.42 inference(resolution,[status(thm)],[f814,f893])).
% 0.15/0.42 fof(f1074,plain,(
% 0.15/0.42 ~op(e0,e0)=e0|unit=e0|unit=e1|unit=e2),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f814,f147])).
% 0.15/0.42 fof(f1077,plain,(
% 0.15/0.42 unit=e0|unit=e1|unit=e2),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1074,f1068])).
% 0.15/0.42 fof(f1080,plain,(
% 0.15/0.42 op(e3,e2)=e3|unit=e0|unit=e1),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f1077,f41])).
% 0.15/0.42 fof(f1090,plain,(
% 0.15/0.42 unit=e0|unit=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1080,f415])).
% 0.15/0.42 fof(f1094,plain,(
% 0.15/0.42 op(e4,e1)=e4|unit=e0),
% 0.15/0.42 inference(paramodulation,[status(thm)],[f1090,f43])).
% 0.15/0.42 fof(f1106,plain,(
% 0.15/0.42 op(e4,e0)=e4),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f43])).
% 0.15/0.42 fof(f1107,plain,(
% 0.15/0.42 op(e0,e4)=e4),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f42])).
% 0.15/0.42 fof(f1108,plain,(
% 0.15/0.42 op(e3,e0)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f41])).
% 0.15/0.42 fof(f1109,plain,(
% 0.15/0.42 op(e0,e3)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f40])).
% 0.15/0.42 fof(f1110,plain,(
% 0.15/0.42 op(e2,e0)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f39])).
% 0.15/0.42 fof(f1111,plain,(
% 0.15/0.42 op(e0,e2)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f38])).
% 0.15/0.42 fof(f1112,plain,(
% 0.15/0.42 op(e1,e0)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f37])).
% 0.15/0.42 fof(f1113,plain,(
% 0.15/0.42 op(e0,e1)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f36])).
% 0.15/0.42 fof(f1114,plain,(
% 0.15/0.42 op(e0,e0)=e0),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1116,f35])).
% 0.15/0.42 fof(f1116,plain,(
% 0.15/0.42 unit=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1094,f435])).
% 0.15/0.42 fof(f1122,plain,(
% 0.15/0.42 ~e4=e4|op(e4,e2)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1106,f788])).
% 0.15/0.42 fof(f1124,plain,(
% 0.15/0.42 ~sP19_prd|sP20_prd|~e4=op(e0,e4)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1106,f374])).
% 0.15/0.42 fof(f1125,plain,(
% 0.15/0.42 ~e4=op(e4,e3)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1106,f187])).
% 0.15/0.42 fof(f1131,plain,(
% 0.15/0.42 ~sP3_prd|sP4_prd|~op(e0,e4)=e4),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1106,f246])).
% 0.15/0.42 fof(f1142,plain,(
% 0.15/0.42 ~e4=e4|op(e0,e2)=e4|op(e3,e2)=e4),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1106,f829])).
% 0.15/0.42 fof(f1151,plain,(
% 0.15/0.42 e4=e3|op(e4,e1)=e3|op(e4,e3)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1106,f572])).
% 0.15/0.42 fof(f1164,plain,(
% 0.15/0.42 ~op(e3,e0)=e3|e4=e3|op(e1,e4)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1107,f957])).
% 0.15/0.42 fof(f1189,plain,(
% 0.15/0.42 ~sP8_prd|sP9_prd|~op(e0,e3)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1108,f286])).
% 0.15/0.42 fof(f1200,plain,(
% 0.15/0.42 sP22_prd|~op(op(e0,e2),e0)=e2|~sP20_prd|~e3=op(e0,e3)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1108,f757])).
% 0.15/0.42 fof(f1205,plain,(
% 0.15/0.42 ~op(e2,e4)=e1|e3=e1|op(e3,e1)=e1|op(e3,e2)=e1|op(e3,e3)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1108,f669])).
% 0.15/0.42 fof(f1211,plain,(
% 0.15/0.42 e3=e0|op(e3,e1)=e0|op(e3,e3)=e0|op(e3,e4)=e0),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1108,f566])).
% 0.15/0.42 fof(f1223,plain,(
% 0.15/0.42 ~e3=op(e4,e3)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1109,f128])).
% 0.15/0.42 fof(f1245,plain,(
% 0.15/0.42 e3=e0|op(e2,e3)=e0|op(e3,e3)=e0|op(e4,e3)=e0),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1109,f564])).
% 0.15/0.42 fof(f1246,plain,(
% 0.15/0.42 e3=e4|op(e2,e3)=e4|op(e3,e3)=e4|op(e4,e3)=e4),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1109,f541])).
% 0.15/0.42 fof(f1248,plain,(
% 0.15/0.42 e2=e1|op(e2,e1)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1110,f514])).
% 0.15/0.42 fof(f1254,plain,(
% 0.15/0.42 ~sP13_prd|sP14_prd|~op(e0,e2)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1110,f326])).
% 0.15/0.42 fof(f1257,plain,(
% 0.15/0.42 ~e2=op(e2,e1)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1110,f165])).
% 0.15/0.42 fof(f1284,plain,(
% 0.15/0.42 ~sP16_prd|sP17_prd|e2=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1111,f481])).
% 0.15/0.42 fof(f1293,plain,(
% 0.15/0.42 e1=e2|op(e1,e3)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1112,f605])).
% 0.15/0.42 fof(f1298,plain,(
% 0.15/0.42 ~sP18_prd|sP19_prd|~op(e0,e1)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1112,f366])).
% 0.15/0.42 fof(f1301,plain,(
% 0.15/0.42 ~sP22_prd|~e1=op(e0,e1)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1112,f477])).
% 0.15/0.42 fof(f1314,plain,(
% 0.15/0.42 ~e1=op(e3,e1)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1113,f107])).
% 0.15/0.42 fof(f1315,plain,(
% 0.15/0.42 ~e1=op(e2,e1)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1113,f106])).
% 0.15/0.42 fof(f1323,plain,(
% 0.15/0.42 e1=e2|op(e2,e1)=e2|op(e3,e1)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1113,f582])).
% 0.15/0.42 fof(f1330,plain,(
% 0.15/0.42 ~op(e2,e3)=e1|e0=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1114,f779])).
% 0.15/0.42 fof(f1349,plain,(
% 0.15/0.42 ~sP1_prd|sP2_prd|op(e1,e2)=e4),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1352,f231])).
% 0.15/0.42 fof(f1352,plain,(
% 0.15/0.42 op(e4,e2)=e1),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1122])).
% 0.15/0.42 fof(f1353,plain,(
% 0.15/0.42 ~sP19_prd|sP20_prd|~e4=e4),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1107,f1124])).
% 0.15/0.42 fof(f1354,plain,(
% 0.15/0.42 ~sP19_prd|sP20_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1353])).
% 0.15/0.42 fof(f1359,plain,(
% 0.15/0.42 ~sP3_prd|sP4_prd|~e4=e4),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1107,f1131])).
% 0.15/0.42 fof(f1360,plain,(
% 0.15/0.42 ~sP3_prd|sP4_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1359])).
% 0.15/0.42 fof(f1368,plain,(
% 0.15/0.42 ~e4=e4|e2=e4|op(e3,e2)=e4),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1111,f1142])).
% 0.15/0.42 fof(f1369,plain,(
% 0.15/0.42 e2=e4|op(e3,e2)=e4),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1368])).
% 0.15/0.42 fof(f1374,plain,(
% 0.15/0.42 ~sP6_prd|sP7_prd|op(e4,e2)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1385,f271])).
% 0.15/0.42 fof(f1377,plain,(
% 0.15/0.42 ~e4=op(e3,e3)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1385,f182])).
% 0.15/0.42 fof(f1385,plain,(
% 0.15/0.42 op(e3,e2)=e4),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1369,f203])).
% 0.15/0.42 fof(f1389,plain,(
% 0.15/0.42 op(e4,e1)=e3|op(e4,e3)=e3),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1151,f204])).
% 0.15/0.42 fof(f1402,plain,(
% 0.15/0.42 ~e3=e3|e4=e3|op(e1,e4)=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1108,f1164])).
% 0.15/0.42 fof(f1403,plain,(
% 0.15/0.42 e4=e3|op(e1,e4)=e3),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1402])).
% 0.15/0.42 fof(f1421,plain,(
% 0.15/0.42 sP16_prd|op(op(e1,e3),e3)=e1|~sP14_prd|~op(e4,e1)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1429,f728])).
% 0.15/0.42 fof(f1429,plain,(
% 0.15/0.42 op(e1,e4)=e3),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1403,f204])).
% 0.15/0.42 fof(f1444,plain,(
% 0.15/0.42 ~sP8_prd|sP9_prd|~e3=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1109,f1189])).
% 0.15/0.42 fof(f1445,plain,(
% 0.15/0.42 ~sP8_prd|sP9_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1444])).
% 0.15/0.42 fof(f1458,plain,(
% 0.15/0.42 sP22_prd|~op(e2,e0)=e2|~sP20_prd|~e3=op(e0,e3)),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1111,f1200])).
% 0.15/0.42 fof(f1459,plain,(
% 0.15/0.42 sP22_prd|~e2=e2|~sP20_prd|~e3=op(e0,e3)),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1110,f1458])).
% 0.15/0.42 fof(f1460,plain,(
% 0.15/0.42 sP22_prd|~e2=e2|~sP20_prd|~e3=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1109,f1459])).
% 0.15/0.42 fof(f1461,plain,(
% 0.15/0.42 sP22_prd|~sP20_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1460])).
% 0.15/0.42 fof(f1471,plain,(
% 0.15/0.42 ~op(e2,e4)=e1|e3=e1|op(e3,e1)=e1|e4=e1|op(e3,e3)=e1),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1385,f1205])).
% 0.15/0.42 fof(f1472,plain,(
% 0.15/0.42 ~op(e2,e4)=e1|op(e3,e1)=e1|e4=e1|op(e3,e3)=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1471,f200])).
% 0.15/0.42 fof(f1477,plain,(
% 0.15/0.42 op(e3,e1)=e0|op(e3,e3)=e0|op(e3,e4)=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1211,f197])).
% 0.15/0.42 fof(f1485,plain,(
% 0.15/0.42 op(e4,e1)=e3),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1389,f1223])).
% 0.15/0.42 fof(f1517,plain,(
% 0.15/0.42 op(e2,e3)=e0|op(e3,e3)=e0|op(e4,e3)=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1245,f197])).
% 0.15/0.42 fof(f1518,plain,(
% 0.15/0.42 op(e2,e3)=e4|op(e3,e3)=e4|op(e4,e3)=e4),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1246,f204])).
% 0.15/0.42 fof(f1520,plain,(
% 0.15/0.42 op(e2,e1)=e1|op(e2,e3)=e1|op(e2,e4)=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1248,f199])).
% 0.15/0.42 fof(f1525,plain,(
% 0.15/0.42 ~sP13_prd|sP14_prd|~e2=e2),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1111,f1254])).
% 0.15/0.42 fof(f1526,plain,(
% 0.15/0.42 ~sP13_prd|sP14_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1525])).
% 0.15/0.42 fof(f1529,plain,(
% 0.15/0.42 op(e2,e1)=e0|op(e2,e1)=e1),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f570,f1257])).
% 0.15/0.42 fof(f1548,plain,(
% 0.15/0.42 ~sP16_prd|sP17_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1284,f199])).
% 0.15/0.42 fof(f1571,plain,(
% 0.15/0.42 op(e1,e3)=e2),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1293,f199])).
% 0.15/0.42 fof(f1574,plain,(
% 0.15/0.42 ~sP18_prd|sP19_prd|~e1=e1),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1113,f1298])).
% 0.15/0.42 fof(f1575,plain,(
% 0.15/0.42 ~sP18_prd|sP19_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1574])).
% 0.15/0.42 fof(f1578,plain,(
% 0.15/0.42 ~sP22_prd|~e1=e1),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1113,f1301])).
% 0.15/0.42 fof(f1580,plain,(
% 0.15/0.42 ~sP20_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1461,f1581])).
% 0.15/0.42 fof(f1581,plain,(
% 0.15/0.42 ~sP22_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1578])).
% 0.15/0.42 fof(f1588,plain,(
% 0.15/0.42 ~op(e2,e4)=e1|e4=e1|op(e3,e3)=e1),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1472,f1314])).
% 0.15/0.42 fof(f1591,plain,(
% 0.15/0.42 op(e2,e3)=e1|op(e2,e4)=e1),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1520,f1315])).
% 0.15/0.42 fof(f1597,plain,(
% 0.15/0.42 op(e2,e1)=e2|op(e3,e1)=e2),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1323,f199])).
% 0.15/0.42 fof(f1600,plain,(
% 0.15/0.42 ~op(e2,e3)=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1330,f195])).
% 0.15/0.42 fof(f1609,plain,(
% 0.15/0.42 ~sP1_prd|sP2_prd|e0=e4),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f408,f1349])).
% 0.15/0.42 fof(f1610,plain,(
% 0.15/0.42 ~sP1_prd|sP2_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1609,f198])).
% 0.15/0.42 fof(f1615,plain,(
% 0.15/0.42 ~sP6_prd|sP7_prd|e1=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1352,f1374])).
% 0.15/0.42 fof(f1616,plain,(
% 0.15/0.42 ~sP6_prd|sP7_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1615,f200])).
% 0.15/0.42 fof(f1617,plain,(
% 0.15/0.42 op(e2,e3)=e4|op(e4,e3)=e4),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1518,f1377])).
% 0.15/0.42 fof(f1634,plain,(
% 0.15/0.42 sP16_prd|op(e2,e3)=e1|~sP14_prd|~op(e4,e1)=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1571,f1421])).
% 0.15/0.42 fof(f1635,plain,(
% 0.15/0.42 sP16_prd|~sP14_prd|~op(e4,e1)=e3),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1634,f1600])).
% 0.15/0.42 fof(f1645,plain,(
% 0.15/0.42 ~sP2_prd|sP3_prd|op(e3,e1)=e4),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1485,f239])).
% 0.15/0.42 fof(f1651,plain,(
% 0.15/0.42 sP16_prd|~sP14_prd|~e3=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1485,f1635])).
% 0.15/0.42 fof(f1665,plain,(
% 0.15/0.42 ~sP12_prd|sP13_prd|op(e0,e1)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1678,f319])).
% 0.15/0.42 fof(f1668,plain,(
% 0.15/0.42 ~e0=op(e3,e1)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1678,f112])).
% 0.15/0.42 fof(f1672,plain,(
% 0.15/0.42 e0=e2|op(e3,e1)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1678,f1597])).
% 0.15/0.42 fof(f1678,plain,(
% 0.15/0.42 op(e2,e1)=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1529,f1315])).
% 0.15/0.42 fof(f1690,plain,(
% 0.15/0.42 ~sP19_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1354,f1580])).
% 0.15/0.42 fof(f1692,plain,(
% 0.15/0.42 ~op(e2,e4)=e1|op(e3,e3)=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1588,f201])).
% 0.15/0.42 fof(f1695,plain,(
% 0.15/0.42 ~sP9_prd|sP10_prd|op(e1,e4)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1709,f295])).
% 0.15/0.42 fof(f1700,plain,(
% 0.15/0.42 ~e1=e1|op(e3,e3)=e1),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1709,f1692])).
% 0.15/0.42 fof(f1709,plain,(
% 0.15/0.42 op(e2,e4)=e1),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1591,f1600])).
% 0.15/0.42 fof(f1711,plain,(
% 0.15/0.42 ~sP10_prd|sP11_prd|op(e4,e3)=e2),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1722,f303])).
% 0.15/0.42 fof(f1721,plain,(
% 0.15/0.42 e4=e0|op(e3,e3)=e0|op(e4,e3)=e0),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1722,f1517])).
% 0.15/0.42 fof(f1722,plain,(
% 0.15/0.42 op(e2,e3)=e4),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1617,f1125])).
% 0.15/0.42 fof(f1723,plain,(
% 0.15/0.42 ~sP2_prd|sP3_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1645,f436])).
% 0.15/0.42 fof(f1725,plain,(
% 0.15/0.42 sP16_prd|~sP14_prd),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1651])).
% 0.15/0.42 fof(f1730,plain,(
% 0.15/0.42 ~sP12_prd|sP13_prd|e1=e2),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1113,f1665])).
% 0.15/0.42 fof(f1731,plain,(
% 0.15/0.42 ~sP12_prd|sP13_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1730,f199])).
% 0.15/0.42 fof(f1735,plain,(
% 0.15/0.42 op(e3,e3)=e0|op(e3,e4)=e0),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1477,f1668])).
% 0.15/0.42 fof(f1738,plain,(
% 0.15/0.42 ~sP7_prd|sP8_prd|op(e2,e1)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1748,f279])).
% 0.15/0.42 fof(f1748,plain,(
% 0.15/0.42 op(e3,e1)=e2),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1672,f196])).
% 0.15/0.42 fof(f1749,plain,(
% 0.15/0.42 ~sP18_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1575,f1690])).
% 0.15/0.42 fof(f1751,plain,(
% 0.15/0.42 ~sP9_prd|sP10_prd|e3=e2),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1429,f1695])).
% 0.15/0.42 fof(f1752,plain,(
% 0.15/0.42 ~sP9_prd|sP10_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1751,f202])).
% 0.15/0.42 fof(f1763,plain,(
% 0.15/0.42 op(e3,e3)=e1),
% 0.15/0.42 inference(trivial_equality_resolution,[status(thm)],[f1700])).
% 0.15/0.42 fof(f1767,plain,(
% 0.15/0.42 ~sP10_prd|sP11_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1711,f522])).
% 0.15/0.42 fof(f1770,plain,(
% 0.15/0.42 e4=e0|e1=e0|op(e4,e3)=e0),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1763,f1721])).
% 0.15/0.42 fof(f1771,plain,(
% 0.15/0.42 e1=e0|op(e4,e3)=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1770,f198])).
% 0.15/0.42 fof(f1772,plain,(
% 0.15/0.42 e1=e0|op(e3,e4)=e0),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1763,f1735])).
% 0.15/0.42 fof(f1775,plain,(
% 0.15/0.42 ~sP4_prd|sP5_prd|op(e0,e4)=e3),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1784,f255])).
% 0.15/0.42 fof(f1778,plain,(
% 0.15/0.42 sP1_prd|~e0=op(e4,e3)),
% 0.15/0.42 inference(backward_demodulation,[status(thm)],[f1784,f461])).
% 0.15/0.42 fof(f1784,plain,(
% 0.15/0.42 op(e3,e4)=e0),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1772,f195])).
% 0.15/0.42 fof(f1786,plain,(
% 0.15/0.42 ~sP7_prd|sP8_prd|e0=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1678,f1738])).
% 0.15/0.42 fof(f1787,plain,(
% 0.15/0.42 ~sP7_prd|sP8_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1786,f197])).
% 0.15/0.42 fof(f1791,plain,(
% 0.15/0.42 ~sP17_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f472,f1749])).
% 0.15/0.42 fof(f1797,plain,(
% 0.15/0.42 ~sP4_prd|sP5_prd|e4=e3),
% 0.15/0.42 inference(forward_demodulation,[status(thm)],[f1107,f1775])).
% 0.15/0.42 fof(f1798,plain,(
% 0.15/0.42 ~sP4_prd|sP5_prd),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1797,f204])).
% 0.15/0.42 fof(f1802,plain,(
% 0.15/0.42 ~sP16_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1548,f1791])).
% 0.15/0.42 fof(f1803,plain,(
% 0.15/0.42 ~sP14_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1725,f1802])).
% 0.15/0.42 fof(f1806,plain,(
% 0.15/0.42 ~sP13_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1526,f1803])).
% 0.15/0.42 fof(f1807,plain,(
% 0.15/0.42 ~sP12_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1731,f1806])).
% 0.15/0.42 fof(f1808,plain,(
% 0.15/0.42 ~sP11_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f467,f1807])).
% 0.15/0.42 fof(f1809,plain,(
% 0.15/0.42 ~sP10_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1767,f1808])).
% 0.15/0.42 fof(f1810,plain,(
% 0.15/0.42 ~sP9_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1752,f1809])).
% 0.15/0.42 fof(f1811,plain,(
% 0.15/0.42 ~sP8_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1445,f1810])).
% 0.15/0.42 fof(f1812,plain,(
% 0.15/0.42 ~sP7_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1787,f1811])).
% 0.15/0.42 fof(f1813,plain,(
% 0.15/0.42 ~sP6_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1616,f1812])).
% 0.15/0.42 fof(f1814,plain,(
% 0.15/0.42 ~sP5_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f464,f1813])).
% 0.15/0.42 fof(f1815,plain,(
% 0.15/0.42 ~sP4_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1798,f1814])).
% 0.15/0.42 fof(f1816,plain,(
% 0.15/0.42 ~sP3_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1360,f1815])).
% 0.15/0.42 fof(f1817,plain,(
% 0.15/0.42 ~sP2_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1723,f1816])).
% 0.15/0.42 fof(f1818,plain,(
% 0.15/0.42 ~sP1_prd),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1610,f1817])).
% 0.15/0.42 fof(f1821,plain,(
% 0.15/0.42 ~e0=op(e4,e3)),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1778,f1818])).
% 0.15/0.42 fof(f1822,plain,(
% 0.15/0.42 e1=e0),
% 0.15/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1771,f1821])).
% 0.15/0.42 fof(f1825,plain,(
% 0.15/0.42 $false),
% 0.15/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1822,f195])).
% 0.15/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.46 % Elapsed time: 0.082751 seconds
% 0.15/0.46 % CPU time: 0.247593 seconds
% 0.15/0.46 % Total memory used: 43.510 MB
% 0.15/0.46 % Net memory used: 43.466 MB
%------------------------------------------------------------------------------