%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG063+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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.13s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG063+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 12:55:06 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.45 % Refutation found
% 0.13/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.45 fof(f1,axiom,(
% 0.13/0.45 ( ( 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.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f2,axiom,(
% 0.13/0.45 ( 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.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f4,axiom,(
% 0.13/0.45 ( 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.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f5,axiom,(
% 0.13/0.45 ( e0 != e1& e0 != e2& e0 != e3& e0 != e4& e1 != e2& e1 != e3& e1 != e4& e2 != e3& e2 != e4& e3 != e4 ) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f6,axiom,(
% 0.13/0.45 ( 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.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f7,conjecture,(
% 0.13/0.45 ~ ( ( 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) = e0& op(e0,e0) = e0& op(e0,e0) != e0 )| ( op(e0,e0) = e1& op(e1,e1) = e0& op(e0,e1) != e0 )| ( op(e0,e0) = e2& op(e2,e2) = e0& op(e0,e2) != e0 )| ( op(e0,e0) = e3& op(e3,e3) = e0& op(e0,e3) != e0 )| ( op(e0,e0) = e4& op(e4,e4) = e0& op(e0,e4) != e0 )| ( op(e1,e1) = e0& op(e0,e0) = e1& op(e1,e0) != e1 )| ( op(e1,e1) = e1& op(e1,e1) = e1& op(e1,e1) != e1 )| ( op(e1,e1) = e2& op(e2,e2) = e1& op(e1,e2) != e1 )| ( op(e1,e1) = e3& op(e3,e3) = e1& op(e1,e3) != e1 )| ( op(e1,e1) = e4& op(e4,e4) = e1& op(e1,e4) != e1 )| ( op(e2,e2) = e0& op(e0,e0) = e2& op(e2,e0) != e2 )| ( op(e2,e2) = e1& op(e1,e1) = e2& op(e2,e1) != e2 )| ( op(e2,e2) = e2& op(e2,e2) = e2& op(e2,e2) != e2 )| ( op(e2,e2) = e3& op(e3,e3) = e2& op(e2,e3) != e2 )| ( op(e2,e2) = e4& op(e4,e4) = e2& op(e2,e4) != e2 )| ( op(e3,e3) = e0& op(e0,e0) = e3& op(e3,e0) != e3 )| ( op(e3,e3) = e1& op(e1,e1) = e3& op(e3,e1) != e3 )| ( op(e3,e3) = e2& op(e2,e2) = e3& op(e3,e2) != e3 )| ( op(e3,e3) = e3& op(e3,e3) = e3& op(e3,e3) != e3 )| ( op(e3,e3) = e4& op(e4,e4) = e3& op(e3,e4) != e3 )| ( op(e4,e4) = e0& op(e0,e0) = e4& op(e4,e0) != e4 )| ( op(e4,e4) = e1& op(e1,e1) = e4& op(e4,e1) != e4 )| ( op(e4,e4) = e2& op(e2,e2) = e4& op(e4,e2) != e4 )| ( op(e4,e4) = e3& op(e3,e3) = e4& op(e4,e3) != e4 )| ( op(e4,e4) = e4& op(e4,e4) = e4& op(e4,e4) != e4 ) ) ) ),
% 0.13/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f8,negated_conjecture,(
% 0.13/0.45 ~(~ ( ( 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) = e0& op(e0,e0) = e0& op(e0,e0) != e0 )| ( op(e0,e0) = e1& op(e1,e1) = e0& op(e0,e1) != e0 )| ( op(e0,e0) = e2& op(e2,e2) = e0& op(e0,e2) != e0 )| ( op(e0,e0) = e3& op(e3,e3) = e0& op(e0,e3) != e0 )| ( op(e0,e0) = e4& op(e4,e4) = e0& op(e0,e4) != e0 )| ( op(e1,e1) = e0& op(e0,e0) = e1& op(e1,e0) != e1 )| ( op(e1,e1) = e1& op(e1,e1) = e1& op(e1,e1) != e1 )| ( op(e1,e1) = e2& op(e2,e2) = e1& op(e1,e2) != e1 )| ( op(e1,e1) = e3& op(e3,e3) = e1& op(e1,e3) != e1 )| ( op(e1,e1) = e4& op(e4,e4) = e1& op(e1,e4) != e1 )| ( op(e2,e2) = e0& op(e0,e0) = e2& op(e2,e0) != e2 )| ( op(e2,e2) = e1& op(e1,e1) = e2& op(e2,e1) != e2 )| ( op(e2,e2) = e2& op(e2,e2) = e2& op(e2,e2) != e2 )| ( op(e2,e2) = e3& op(e3,e3) = e2& op(e2,e3) != e2 )| ( op(e2,e2) = e4& op(e4,e4) = e2& op(e2,e4) != e2 )| ( op(e3,e3) = e0& op(e0,e0) = e3& op(e3,e0) != e3 )| ( op(e3,e3) = e1& op(e1,e1) = e3& op(e3,e1) != e3 )| ( op(e3,e3) = e2& op(e2,e2) = e3& op(e3,e2) != e3 )| ( op(e3,e3) = e3& op(e3,e3) = e3& op(e3,e3) != e3 )| ( op(e3,e3) = e4& op(e4,e4) = e3& op(e3,e4) != e3 )| ( op(e4,e4) = e0& op(e0,e0) = e4& op(e4,e0) != e4 )| ( op(e4,e4) = e1& op(e1,e1) = e4& op(e4,e1) != e4 )| ( op(e4,e4) = e2& op(e2,e2) = e4& op(e4,e2) != e4 )| ( op(e4,e4) = e3& op(e3,e3) = e4& op(e4,e3) != e4 )| ( op(e4,e4) = e4& op(e4,e4) = e4& op(e4,e4) != e4 ) ) ) )),
% 0.13/0.45 inference(negated_conjecture,[status(cth)],[f7])).
% 0.13/0.45 fof(f31,plain,(
% 0.13/0.45 op(e4,e2)=e0|op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e3|op(e4,e2)=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.45 fof(f34,plain,(
% 0.13/0.45 op(unit,e0)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.45 fof(f35,plain,(
% 0.13/0.45 op(e0,unit)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.45 fof(f36,plain,(
% 0.13/0.45 op(unit,e1)=e1),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.45 fof(f38,plain,(
% 0.13/0.45 op(unit,e2)=e2),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.45 fof(f41,plain,(
% 0.13/0.45 op(e3,unit)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.45 fof(f44,plain,(
% 0.13/0.45 unit=e0|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.45 fof(f115,plain,(
% 0.13/0.45 ~op(e0,e2)=op(e1,e2)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f121,plain,(
% 0.13/0.45 ~op(e1,e2)=op(e4,e2)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f123,plain,(
% 0.13/0.45 ~op(e2,e2)=op(e4,e2)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f145,plain,(
% 0.13/0.45 ~op(e0,e0)=op(e0,e1)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f156,plain,(
% 0.13/0.45 ~op(e1,e0)=op(e1,e2)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f182,plain,(
% 0.13/0.45 ~op(e3,e2)=op(e3,e3)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f183,plain,(
% 0.13/0.45 ~op(e3,e2)=op(e3,e4)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f193,plain,(
% 0.13/0.45 ~op(e4,e2)=op(e4,e4)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f195,plain,(
% 0.13/0.45 ~e0=e1),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f196,plain,(
% 0.13/0.45 ~e0=e2),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f197,plain,(
% 0.13/0.45 ~e0=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f198,plain,(
% 0.13/0.45 ~e0=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f199,plain,(
% 0.13/0.45 ~e1=e2),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f200,plain,(
% 0.13/0.45 ~e1=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f201,plain,(
% 0.13/0.45 ~e1=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f202,plain,(
% 0.13/0.45 ~e2=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f203,plain,(
% 0.13/0.45 ~e2=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f204,plain,(
% 0.13/0.45 ~e3=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f205,plain,(
% 0.13/0.45 e0=op(e1,op(op(e1,e1),op(e1,e1)))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.45 fof(f206,plain,(
% 0.13/0.45 e2=op(op(e1,e1),op(e1,e1))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.45 fof(f207,plain,(
% 0.13/0.45 e3=op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1)))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.45 fof(f208,plain,(
% 0.13/0.45 e4=op(e1,e1)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.45 fof(f209,definition,(
% 0.13/0.45 sP0_prd<=>(((((((((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3))|((op(e3,e3)=e4&op(e4,e4)=e3)&~op(e3,e4)=e3))|((op(e4,e4)=e0&op(e0,e0)=e4)&~op(e4,e0)=e4))|((op(e4,e4)=e1&op(e1,e1)=e4)&~op(e4,e1)=e4))|((op(e4,e4)=e2&op(e2,e2)=e4)&~op(e4,e2)=e4))|((op(e4,e4)=e3&op(e3,e3)=e4)&~op(e4,e3)=e4))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.45 fof(f210,plain,(
% 0.13/0.45 ((((((((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)=e4&op(e4,e4)=e4)&~op(e4,e4)=e4))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f8,f209])).
% 0.13/0.45 fof(f212,plain,(
% 0.13/0.45 op(e0,e0)=e1|op(e1,e1)=e1|op(e2,e2)=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f210])).
% 0.13/0.45 fof(f216,plain,(
% 0.13/0.45 sP0_prd|op(e4,e4)=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f210])).
% 0.13/0.45 fof(f218,plain,(
% 0.13/0.45 sP0_prd|~op(e4,e4)=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f210])).
% 0.13/0.45 fof(f219,definition,(
% 0.13/0.45 sP1_prd<=>((((((((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3))|((op(e3,e3)=e4&op(e4,e4)=e3)&~op(e3,e4)=e3))|((op(e4,e4)=e0&op(e0,e0)=e4)&~op(e4,e0)=e4))|((op(e4,e4)=e1&op(e1,e1)=e4)&~op(e4,e1)=e4))|((op(e4,e4)=e2&op(e2,e2)=e4)&~op(e4,e2)=e4))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.13/0.45 fof(f220,plain,(
% 0.13/0.45 sP0_prd<=>(sP1_prd|((op(e4,e4)=e3&op(e3,e3)=e4)&~op(e4,e3)=e4))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f209,f219])).
% 0.13/0.45 fof(f221,plain,(
% 0.13/0.45 (~sP0_prd|(sP1_prd|((op(e4,e4)=e3&op(e3,e3)=e4)&~op(e4,e3)=e4)))&(sP0_prd|(~sP1_prd&((~op(e4,e4)=e3|~op(e3,e3)=e4)|op(e4,e3)=e4)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f220])).
% 0.13/0.45 fof(f222,plain,(
% 0.13/0.45 ~sP0_prd|sP1_prd|op(e4,e4)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f221])).
% 0.13/0.45 fof(f227,definition,(
% 0.13/0.45 sP2_prd<=>(((((((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3))|((op(e3,e3)=e4&op(e4,e4)=e3)&~op(e3,e4)=e3))|((op(e4,e4)=e0&op(e0,e0)=e4)&~op(e4,e0)=e4))|((op(e4,e4)=e1&op(e1,e1)=e4)&~op(e4,e1)=e4))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.13/0.45 fof(f228,plain,(
% 0.13/0.45 sP1_prd<=>(sP2_prd|((op(e4,e4)=e2&op(e2,e2)=e4)&~op(e4,e2)=e4))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f219,f227])).
% 0.13/0.45 fof(f229,plain,(
% 0.13/0.45 (~sP1_prd|(sP2_prd|((op(e4,e4)=e2&op(e2,e2)=e4)&~op(e4,e2)=e4)))&(sP1_prd|(~sP2_prd&((~op(e4,e4)=e2|~op(e2,e2)=e4)|op(e4,e2)=e4)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f228])).
% 0.13/0.45 fof(f231,plain,(
% 0.13/0.45 ~sP1_prd|sP2_prd|op(e2,e2)=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f229])).
% 0.13/0.45 fof(f235,definition,(
% 0.13/0.45 sP3_prd<=>((((((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3))|((op(e3,e3)=e4&op(e4,e4)=e3)&~op(e3,e4)=e3))|((op(e4,e4)=e0&op(e0,e0)=e4)&~op(e4,e0)=e4))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.13/0.45 fof(f236,plain,(
% 0.13/0.45 sP2_prd<=>(sP3_prd|((op(e4,e4)=e1&op(e1,e1)=e4)&~op(e4,e1)=e4))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f227,f235])).
% 0.13/0.45 fof(f237,plain,(
% 0.13/0.45 (~sP2_prd|(sP3_prd|((op(e4,e4)=e1&op(e1,e1)=e4)&~op(e4,e1)=e4)))&(sP2_prd|(~sP3_prd&((~op(e4,e4)=e1|~op(e1,e1)=e4)|op(e4,e1)=e4)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f236])).
% 0.13/0.45 fof(f238,plain,(
% 0.13/0.45 ~sP2_prd|sP3_prd|op(e4,e4)=e1),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f237])).
% 0.13/0.45 fof(f243,definition,(
% 0.13/0.45 sP4_prd<=>(((((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3))|((op(e3,e3)=e4&op(e4,e4)=e3)&~op(e3,e4)=e3))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.13/0.45 fof(f244,plain,(
% 0.13/0.45 sP3_prd<=>(sP4_prd|((op(e4,e4)=e0&op(e0,e0)=e4)&~op(e4,e0)=e4))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f235,f243])).
% 0.13/0.45 fof(f245,plain,(
% 0.13/0.45 (~sP3_prd|(sP4_prd|((op(e4,e4)=e0&op(e0,e0)=e4)&~op(e4,e0)=e4)))&(sP3_prd|(~sP4_prd&((~op(e4,e4)=e0|~op(e0,e0)=e4)|op(e4,e0)=e4)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f244])).
% 0.13/0.45 fof(f246,plain,(
% 0.13/0.45 ~sP3_prd|sP4_prd|op(e4,e4)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f245])).
% 0.13/0.45 fof(f251,definition,(
% 0.13/0.45 sP5_prd<=>((((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.13/0.45 fof(f252,plain,(
% 0.13/0.45 sP4_prd<=>(sP5_prd|((op(e3,e3)=e4&op(e4,e4)=e3)&~op(e3,e4)=e3))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f243,f251])).
% 0.13/0.45 fof(f253,plain,(
% 0.13/0.45 (~sP4_prd|(sP5_prd|((op(e3,e3)=e4&op(e4,e4)=e3)&~op(e3,e4)=e3)))&(sP4_prd|(~sP5_prd&((~op(e3,e3)=e4|~op(e4,e4)=e3)|op(e3,e4)=e3)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f252])).
% 0.13/0.45 fof(f255,plain,(
% 0.13/0.45 ~sP4_prd|sP5_prd|op(e4,e4)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f253])).
% 0.13/0.45 fof(f259,definition,(
% 0.13/0.45 sP6_prd<=>(((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.13/0.45 fof(f260,plain,(
% 0.13/0.45 sP5_prd<=>(sP6_prd|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f251,f259])).
% 0.13/0.45 fof(f261,plain,(
% 0.13/0.45 (~sP5_prd|(sP6_prd|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3)))&(sP5_prd|(~sP6_prd&((~op(e3,e3)=e3|~op(e3,e3)=e3)|op(e3,e3)=e3)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f260])).
% 0.13/0.45 fof(f262,plain,(
% 0.13/0.45 ~sP5_prd|sP6_prd|op(e3,e3)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f261])).
% 0.13/0.45 fof(f264,plain,(
% 0.13/0.45 ~sP5_prd|sP6_prd|~op(e3,e3)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f261])).
% 0.13/0.45 fof(f267,definition,(
% 0.13/0.45 sP7_prd<=>((((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.13/0.45 fof(f268,plain,(
% 0.13/0.45 sP6_prd<=>(sP7_prd|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f259,f267])).
% 0.13/0.45 fof(f269,plain,(
% 0.13/0.45 (~sP6_prd|(sP7_prd|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3)))&(sP6_prd|(~sP7_prd&((~op(e3,e3)=e2|~op(e2,e2)=e3)|op(e3,e2)=e3)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f268])).
% 0.13/0.45 fof(f270,plain,(
% 0.13/0.45 ~sP6_prd|sP7_prd|op(e3,e3)=e2),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f269])).
% 0.13/0.45 fof(f275,definition,(
% 0.13/0.45 sP8_prd<=>(((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.13/0.45 fof(f276,plain,(
% 0.13/0.45 sP7_prd<=>(sP8_prd|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f267,f275])).
% 0.13/0.45 fof(f277,plain,(
% 0.13/0.45 (~sP7_prd|(sP8_prd|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3)))&(sP7_prd|(~sP8_prd&((~op(e3,e3)=e1|~op(e1,e1)=e3)|op(e3,e1)=e3)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f276])).
% 0.13/0.45 fof(f279,plain,(
% 0.13/0.45 ~sP7_prd|sP8_prd|op(e1,e1)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f277])).
% 0.13/0.45 fof(f283,definition,(
% 0.13/0.45 sP9_prd<=>((((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.13/0.45 fof(f284,plain,(
% 0.13/0.45 sP8_prd<=>(sP9_prd|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f275,f283])).
% 0.13/0.45 fof(f285,plain,(
% 0.13/0.45 (~sP8_prd|(sP9_prd|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3)))&(sP8_prd|(~sP9_prd&((~op(e3,e3)=e0|~op(e0,e0)=e3)|op(e3,e0)=e3)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f284])).
% 0.13/0.45 fof(f286,plain,(
% 0.13/0.45 ~sP8_prd|sP9_prd|op(e3,e3)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f285])).
% 0.13/0.45 fof(f287,plain,(
% 0.13/0.45 ~sP8_prd|sP9_prd|op(e0,e0)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f285])).
% 0.13/0.45 fof(f291,definition,(
% 0.13/0.45 sP10_prd<=>(((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.13/0.45 fof(f292,plain,(
% 0.13/0.45 sP9_prd<=>(sP10_prd|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f283,f291])).
% 0.13/0.45 fof(f293,plain,(
% 0.13/0.45 (~sP9_prd|(sP10_prd|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2)))&(sP9_prd|(~sP10_prd&((~op(e2,e2)=e4|~op(e4,e4)=e2)|op(e2,e4)=e2)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f292])).
% 0.13/0.45 fof(f294,plain,(
% 0.13/0.45 ~sP9_prd|sP10_prd|op(e2,e2)=e4),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f293])).
% 0.13/0.45 fof(f299,definition,(
% 0.13/0.45 sP11_prd<=>((((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.13/0.45 fof(f300,plain,(
% 0.13/0.45 sP10_prd<=>(sP11_prd|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f291,f299])).
% 0.13/0.45 fof(f301,plain,(
% 0.13/0.45 (~sP10_prd|(sP11_prd|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2)))&(sP10_prd|(~sP11_prd&((~op(e2,e2)=e3|~op(e3,e3)=e2)|op(e2,e3)=e2)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f300])).
% 0.13/0.45 fof(f303,plain,(
% 0.13/0.45 ~sP10_prd|sP11_prd|op(e3,e3)=e2),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f301])).
% 0.13/0.45 fof(f307,definition,(
% 0.13/0.45 sP12_prd<=>(((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.13/0.45 fof(f308,plain,(
% 0.13/0.45 sP11_prd<=>(sP12_prd|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f299,f307])).
% 0.13/0.45 fof(f309,plain,(
% 0.13/0.45 (~sP11_prd|(sP12_prd|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2)))&(sP11_prd|(~sP12_prd&((~op(e2,e2)=e2|~op(e2,e2)=e2)|op(e2,e2)=e2)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f308])).
% 0.13/0.45 fof(f310,plain,(
% 0.13/0.45 ~sP11_prd|sP12_prd|op(e2,e2)=e2),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f309])).
% 0.13/0.45 fof(f315,definition,(
% 0.13/0.45 sP13_prd<=>((((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.13/0.45 fof(f316,plain,(
% 0.13/0.45 sP12_prd<=>(sP13_prd|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f307,f315])).
% 0.13/0.45 fof(f317,plain,(
% 0.13/0.45 (~sP12_prd|(sP13_prd|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2)))&(sP12_prd|(~sP13_prd&((~op(e2,e2)=e1|~op(e1,e1)=e2)|op(e2,e1)=e2)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f316])).
% 0.13/0.45 fof(f318,plain,(
% 0.13/0.45 ~sP12_prd|sP13_prd|op(e2,e2)=e1),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f317])).
% 0.13/0.45 fof(f323,definition,(
% 0.13/0.45 sP14_prd<=>(((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.13/0.45 fof(f324,plain,(
% 0.13/0.45 sP13_prd<=>(sP14_prd|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f315,f323])).
% 0.13/0.45 fof(f325,plain,(
% 0.13/0.45 (~sP13_prd|(sP14_prd|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2)))&(sP13_prd|(~sP14_prd&((~op(e2,e2)=e0|~op(e0,e0)=e2)|op(e2,e0)=e2)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f324])).
% 0.13/0.45 fof(f326,plain,(
% 0.13/0.45 ~sP13_prd|sP14_prd|op(e2,e2)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f325])).
% 0.13/0.45 fof(f331,definition,(
% 0.13/0.45 sP15_prd<=>((((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.13/0.45 fof(f332,plain,(
% 0.13/0.45 sP14_prd<=>(sP15_prd|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f323,f331])).
% 0.13/0.45 fof(f333,plain,(
% 0.13/0.45 (~sP14_prd|(sP15_prd|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1)))&(sP14_prd|(~sP15_prd&((~op(e1,e1)=e4|~op(e4,e4)=e1)|op(e1,e4)=e1)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f332])).
% 0.13/0.45 fof(f335,plain,(
% 0.13/0.45 ~sP14_prd|sP15_prd|op(e4,e4)=e1),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f333])).
% 0.13/0.45 fof(f339,definition,(
% 0.13/0.45 sP16_prd<=>(((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 0.13/0.45 fof(f340,plain,(
% 0.13/0.45 sP15_prd<=>(sP16_prd|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f331,f339])).
% 0.13/0.45 fof(f341,plain,(
% 0.13/0.45 (~sP15_prd|(sP16_prd|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1)))&(sP15_prd|(~sP16_prd&((~op(e1,e1)=e3|~op(e3,e3)=e1)|op(e1,e3)=e1)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f340])).
% 0.13/0.45 fof(f342,plain,(
% 0.13/0.45 ~sP15_prd|sP16_prd|op(e1,e1)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f341])).
% 0.13/0.45 fof(f347,definition,(
% 0.13/0.45 sP17_prd<=>((((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP17_prd])],[])).
% 0.13/0.45 fof(f348,plain,(
% 0.13/0.45 sP16_prd<=>(sP17_prd|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f339,f347])).
% 0.13/0.45 fof(f349,plain,(
% 0.13/0.45 (~sP16_prd|(sP17_prd|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1)))&(sP16_prd|(~sP17_prd&((~op(e1,e1)=e2|~op(e2,e2)=e1)|op(e1,e2)=e1)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f348])).
% 0.13/0.45 fof(f350,plain,(
% 0.13/0.45 ~sP16_prd|sP17_prd|op(e1,e1)=e2),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f349])).
% 0.13/0.45 fof(f355,definition,(
% 0.13/0.45 sP18_prd<=>(((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.13/0.45 fof(f356,plain,(
% 0.13/0.45 sP17_prd<=>(sP18_prd|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f347,f355])).
% 0.13/0.45 fof(f357,plain,(
% 0.13/0.45 (~sP17_prd|(sP18_prd|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1)))&(sP17_prd|(~sP18_prd&((~op(e1,e1)=e1|~op(e1,e1)=e1)|op(e1,e1)=e1)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f356])).
% 0.13/0.45 fof(f358,plain,(
% 0.13/0.45 ~sP17_prd|sP18_prd|op(e1,e1)=e1),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f357])).
% 0.13/0.45 fof(f363,definition,(
% 0.13/0.45 sP19_prd<=>((((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.13/0.45 fof(f364,plain,(
% 0.13/0.45 sP18_prd<=>(sP19_prd|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f355,f363])).
% 0.13/0.45 fof(f365,plain,(
% 0.13/0.45 (~sP18_prd|(sP19_prd|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1)))&(sP18_prd|(~sP19_prd&((~op(e1,e1)=e0|~op(e0,e0)=e1)|op(e1,e0)=e1)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f364])).
% 0.13/0.45 fof(f366,plain,(
% 0.13/0.45 ~sP18_prd|sP19_prd|op(e1,e1)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f365])).
% 0.13/0.45 fof(f371,definition,(
% 0.13/0.45 sP20_prd<=>(((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.13/0.45 fof(f372,plain,(
% 0.13/0.45 sP19_prd<=>(sP20_prd|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f363,f371])).
% 0.13/0.45 fof(f373,plain,(
% 0.13/0.45 (~sP19_prd|(sP20_prd|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0)))&(sP19_prd|(~sP20_prd&((~op(e0,e0)=e4|~op(e4,e4)=e0)|op(e0,e4)=e0)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f372])).
% 0.13/0.45 fof(f375,plain,(
% 0.13/0.45 ~sP19_prd|sP20_prd|op(e4,e4)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f373])).
% 0.13/0.45 fof(f379,definition,(
% 0.13/0.45 sP21_prd<=>((((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP21_prd])],[])).
% 0.13/0.45 fof(f380,plain,(
% 0.13/0.45 sP20_prd<=>(sP21_prd|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f371,f379])).
% 0.13/0.45 fof(f381,plain,(
% 0.13/0.45 (~sP20_prd|(sP21_prd|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0)))&(sP20_prd|(~sP21_prd&((~op(e0,e0)=e3|~op(e3,e3)=e0)|op(e0,e3)=e0)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f380])).
% 0.13/0.45 fof(f382,plain,(
% 0.13/0.45 ~sP20_prd|sP21_prd|op(e0,e0)=e3),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f381])).
% 0.13/0.45 fof(f383,plain,(
% 0.13/0.45 ~sP20_prd|sP21_prd|op(e3,e3)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f381])).
% 0.13/0.45 fof(f387,definition,(
% 0.13/0.45 sP22_prd<=>(((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP22_prd])],[])).
% 0.13/0.45 fof(f388,plain,(
% 0.13/0.45 sP21_prd<=>(sP22_prd|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f379,f387])).
% 0.13/0.45 fof(f389,plain,(
% 0.13/0.45 (~sP21_prd|(sP22_prd|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0)))&(sP21_prd|(~sP22_prd&((~op(e0,e0)=e2|~op(e2,e2)=e0)|op(e0,e2)=e0)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f388])).
% 0.13/0.45 fof(f391,plain,(
% 0.13/0.45 ~sP21_prd|sP22_prd|op(e2,e2)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f389])).
% 0.13/0.45 fof(f395,definition,(
% 0.13/0.45 sP23_prd<=>((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)),
% 0.13/0.45 introduced(definition,[new_symbols(definition,[sP23_prd])],[])).
% 0.13/0.45 fof(f396,plain,(
% 0.13/0.45 sP22_prd<=>(sP23_prd|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))),
% 0.13/0.45 inference(formula_renaming,[status(thm)],[f387,f395])).
% 0.13/0.45 fof(f397,plain,(
% 0.13/0.45 (~sP22_prd|(sP23_prd|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0)))&(sP22_prd|(~sP23_prd&((~op(e0,e0)=e1|~op(e1,e1)=e0)|op(e0,e1)=e0)))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f396])).
% 0.13/0.45 fof(f399,plain,(
% 0.13/0.45 ~sP22_prd|sP23_prd|op(e1,e1)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f397])).
% 0.13/0.45 fof(f403,plain,(
% 0.13/0.45 (~sP23_prd|((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0))&(sP23_prd|((~op(e0,e0)=e0|~op(e0,e0)=e0)|op(e0,e0)=e0))),
% 0.13/0.45 inference(NNF_transformation,[status(thm)],[f395])).
% 0.13/0.45 fof(f404,plain,(
% 0.13/0.45 ~sP23_prd|op(e0,e0)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f403])).
% 0.13/0.45 fof(f406,plain,(
% 0.13/0.45 ~sP23_prd|~op(e0,e0)=e0),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f403])).
% 0.13/0.45 fof(f408,plain,(
% 0.13/0.45 e0=op(e1,e2)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f206,f205])).
% 0.13/0.45 fof(f409,plain,(
% 0.13/0.45 e3=op(e2,op(op(e1,e1),op(e1,e1)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f206,f207])).
% 0.13/0.45 fof(f414,plain,(
% 0.13/0.45 ~e3=op(e4,e2)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f429,f123])).
% 0.13/0.45 fof(f429,plain,(
% 0.13/0.45 e3=op(e2,e2)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f206,f409])).
% 0.13/0.45 fof(f430,plain,(
% 0.13/0.45 e2=op(op(e1,e1),e4)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f208,f206])).
% 0.13/0.45 fof(f453,plain,(
% 0.13/0.45 op(e0,e0)=e1|e4=e1|op(e2,e2)=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f208,f212])).
% 0.13/0.45 fof(f454,plain,(
% 0.13/0.45 op(e0,e0)=e1|e4=e1|e3=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f429,f453])).
% 0.13/0.45 fof(f455,plain,(
% 0.13/0.45 op(e0,e0)=e1|e3=e1|op(e3,e3)=e1|op(e4,e4)=e1),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f454,f201])).
% 0.13/0.45 fof(f460,plain,(
% 0.13/0.45 sP0_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f218,f216])).
% 0.13/0.45 fof(f461,plain,(
% 0.13/0.45 sP1_prd|op(e4,e4)=e3),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f222,f460])).
% 0.13/0.45 fof(f464,plain,(
% 0.13/0.45 ~sP1_prd|sP2_prd|e3=e4),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f429,f231])).
% 0.13/0.45 fof(f465,plain,(
% 0.13/0.45 ~sP1_prd|sP2_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f464,f204])).
% 0.13/0.45 fof(f469,plain,(
% 0.13/0.45 ~sP5_prd|sP6_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f264,f262])).
% 0.13/0.45 fof(f472,plain,(
% 0.13/0.45 ~sP7_prd|sP8_prd|e4=e3),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f208,f279])).
% 0.13/0.45 fof(f473,plain,(
% 0.13/0.45 ~sP7_prd|sP8_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f472,f204])).
% 0.13/0.45 fof(f475,plain,(
% 0.13/0.45 ~sP9_prd|sP10_prd|e3=e4),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f429,f294])).
% 0.13/0.45 fof(f476,plain,(
% 0.13/0.45 ~sP9_prd|sP10_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f475,f204])).
% 0.13/0.45 fof(f480,plain,(
% 0.13/0.45 ~sP11_prd|sP12_prd|e3=e2),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f429,f310])).
% 0.13/0.45 fof(f481,plain,(
% 0.13/0.45 ~sP11_prd|sP12_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f480,f202])).
% 0.13/0.45 fof(f484,plain,(
% 0.13/0.45 ~sP12_prd|sP13_prd|e3=e1),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f429,f318])).
% 0.13/0.45 fof(f485,plain,(
% 0.13/0.45 ~sP12_prd|sP13_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f484,f200])).
% 0.13/0.45 fof(f489,plain,(
% 0.13/0.45 ~sP13_prd|sP14_prd|e3=e0),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f429,f326])).
% 0.13/0.45 fof(f490,plain,(
% 0.13/0.45 ~sP13_prd|sP14_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f489,f197])).
% 0.13/0.45 fof(f494,plain,(
% 0.13/0.45 ~sP15_prd|sP16_prd|e4=e3),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f208,f342])).
% 0.13/0.45 fof(f495,plain,(
% 0.13/0.45 ~sP15_prd|sP16_prd),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f494,f204])).
% 0.13/0.46 fof(f497,plain,(
% 0.13/0.46 ~sP16_prd|sP17_prd|e4=e2),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f208,f350])).
% 0.13/0.46 fof(f498,plain,(
% 0.13/0.46 ~sP16_prd|sP17_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f497,f203])).
% 0.13/0.46 fof(f502,plain,(
% 0.13/0.46 ~sP17_prd|sP18_prd|e4=e1),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f208,f358])).
% 0.13/0.46 fof(f503,plain,(
% 0.13/0.46 ~sP17_prd|sP18_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f502,f201])).
% 0.13/0.46 fof(f506,plain,(
% 0.13/0.46 ~sP18_prd|sP19_prd|e4=e0),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f208,f366])).
% 0.13/0.46 fof(f507,plain,(
% 0.13/0.46 ~sP18_prd|sP19_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f506,f198])).
% 0.13/0.46 fof(f509,plain,(
% 0.13/0.46 ~sP21_prd|sP22_prd|e3=e0),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f429,f391])).
% 0.13/0.46 fof(f510,plain,(
% 0.13/0.46 ~sP21_prd|sP22_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f509,f197])).
% 0.13/0.46 fof(f512,plain,(
% 0.13/0.46 ~sP22_prd|sP23_prd|e4=e0),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f208,f399])).
% 0.13/0.46 fof(f513,plain,(
% 0.13/0.46 ~sP22_prd|sP23_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f512,f198])).
% 0.13/0.46 fof(f515,plain,(
% 0.13/0.46 ~sP22_prd),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f513,f516])).
% 0.13/0.46 fof(f516,plain,(
% 0.13/0.46 ~sP23_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f406,f404])).
% 0.13/0.46 fof(f519,plain,(
% 0.13/0.46 ~op(e1,e0)=e0),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f408,f156])).
% 0.13/0.46 fof(f520,plain,(
% 0.13/0.46 ~e0=op(e4,e2)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f408,f121])).
% 0.13/0.46 fof(f522,plain,(
% 0.13/0.46 ~op(e0,e2)=e0),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f408,f115])).
% 0.13/0.46 fof(f532,plain,(
% 0.13/0.46 op(e4,e2)=e0|op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e4),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f31,f414])).
% 0.13/0.46 fof(f553,plain,(
% 0.13/0.46 ~sP19_prd|sP20_prd|e2=e0),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f583,f375])).
% 0.13/0.46 fof(f555,plain,(
% 0.13/0.46 ~sP14_prd|sP15_prd|e2=e1),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f583,f335])).
% 0.13/0.46 fof(f557,plain,(
% 0.13/0.46 ~sP4_prd|sP5_prd|e2=e3),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f583,f255])).
% 0.13/0.46 fof(f559,plain,(
% 0.13/0.46 ~sP3_prd|sP4_prd|e2=e0),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f583,f246])).
% 0.13/0.46 fof(f561,plain,(
% 0.13/0.46 ~sP2_prd|sP3_prd|e2=e1),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f583,f238])).
% 0.13/0.46 fof(f562,plain,(
% 0.13/0.46 sP1_prd|e2=e3),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f583,f461])).
% 0.13/0.46 fof(f564,plain,(
% 0.13/0.46 op(e0,e0)=e1|e3=e1|op(e3,e3)=e1|e2=e1),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f583,f455])).
% 0.13/0.46 fof(f567,plain,(
% 0.13/0.46 ~op(e4,e2)=e2),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f583,f193])).
% 0.13/0.46 fof(f583,plain,(
% 0.13/0.46 e2=op(e4,e4)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f208,f430])).
% 0.13/0.46 fof(f606,plain,(
% 0.13/0.46 ~sP21_prd),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f510,f515])).
% 0.13/0.46 fof(f616,plain,(
% 0.13/0.46 op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e4),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f532,f520])).
% 0.13/0.46 fof(f619,plain,(
% 0.13/0.46 ~sP19_prd|sP20_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f553,f196])).
% 0.13/0.46 fof(f620,plain,(
% 0.13/0.46 ~sP14_prd|sP15_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f555,f199])).
% 0.13/0.46 fof(f621,plain,(
% 0.13/0.46 ~sP4_prd|sP5_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f557,f202])).
% 0.13/0.46 fof(f622,plain,(
% 0.13/0.46 ~sP3_prd|sP4_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f559,f196])).
% 0.13/0.46 fof(f623,plain,(
% 0.13/0.46 ~sP2_prd|sP3_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f561,f199])).
% 0.13/0.46 fof(f624,plain,(
% 0.13/0.46 sP2_prd),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f465,f625])).
% 0.13/0.46 fof(f625,plain,(
% 0.13/0.46 sP1_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f562,f202])).
% 0.13/0.46 fof(f626,plain,(
% 0.13/0.46 op(e0,e0)=e1|op(e3,e3)=e1|e2=e1),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f564,f200])).
% 0.13/0.46 fof(f630,plain,(
% 0.13/0.46 op(e4,e2)=e1|op(e4,e2)=e4),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f616,f567])).
% 0.13/0.46 fof(f655,plain,(
% 0.13/0.46 ~sP20_prd|op(e3,e3)=e0),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f383,f606])).
% 0.13/0.46 fof(f656,plain,(
% 0.13/0.46 ~sP20_prd|op(e0,e0)=e3),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f382,f606])).
% 0.13/0.46 fof(f657,plain,(
% 0.13/0.46 sP3_prd),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f623,f624])).
% 0.13/0.46 fof(f660,plain,(
% 0.13/0.46 sP4_prd),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f622,f657])).
% 0.13/0.46 fof(f661,plain,(
% 0.13/0.46 sP5_prd),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f621,f660])).
% 0.13/0.46 fof(f662,plain,(
% 0.13/0.46 sP6_prd),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f469,f661])).
% 0.13/0.46 fof(f663,plain,(
% 0.13/0.46 sP7_prd|op(e3,e3)=e2),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f270,f662])).
% 0.13/0.46 fof(f686,plain,(
% 0.13/0.46 op(e3,e3)=e2|sP8_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f663,f473])).
% 0.13/0.46 fof(f743,plain,(
% 0.13/0.46 op(e3,e3)=e2|sP9_prd|op(e0,e0)=e3),
% 0.13/0.46 inference(resolution,[status(thm)],[f686,f287])).
% 0.13/0.46 fof(f744,plain,(
% 0.13/0.46 op(e3,e3)=e2|sP9_prd|op(e3,e3)=e0),
% 0.13/0.46 inference(resolution,[status(thm)],[f686,f286])).
% 0.13/0.46 fof(f802,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e0,e0)=e3|sP10_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f743,f476])).
% 0.13/0.46 fof(f804,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e3,e3)=e0|sP10_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f744,f476])).
% 0.13/0.46 fof(f876,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e0,e0)=e3|sP11_prd|op(e3,e3)=e2),
% 0.13/0.46 inference(resolution,[status(thm)],[f802,f303])).
% 0.13/0.46 fof(f878,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e0,e0)=e3|sP11_prd),
% 0.13/0.46 inference(duplicate_literals_removal,[status(thm)],[f876])).
% 0.13/0.46 fof(f887,plain,(
% 0.13/0.46 ~e1=op(e0,e1)|op(e3,e3)=e1|e2=e1),
% 0.13/0.46 inference(paramodulation,[status(thm)],[f626,f145])).
% 0.13/0.46 fof(f902,plain,(
% 0.13/0.46 ~e1=op(e0,e1)|op(e3,e3)=e1),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f887,f199])).
% 0.13/0.46 fof(f956,plain,(
% 0.13/0.46 ~e1=op(unit,e1)|op(e3,e3)=e1|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.13/0.46 inference(paramodulation,[status(thm)],[f44,f902])).
% 0.13/0.46 fof(f957,plain,(
% 0.13/0.46 ~e1=e1|op(e3,e3)=e1|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f36,f956])).
% 0.13/0.46 fof(f958,plain,(
% 0.13/0.46 op(e3,e3)=e1|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f957])).
% 0.13/0.46 fof(f1127,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e3,e3)=e0|sP11_prd|op(e3,e3)=e2),
% 0.13/0.46 inference(resolution,[status(thm)],[f804,f303])).
% 0.13/0.46 fof(f1129,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e3,e3)=e0|sP11_prd),
% 0.13/0.46 inference(duplicate_literals_removal,[status(thm)],[f1127])).
% 0.13/0.46 fof(f1152,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e0,e0)=e3|sP12_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f878,f481])).
% 0.13/0.46 fof(f1154,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e3,e3)=e0|sP12_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f1129,f481])).
% 0.13/0.46 fof(f1198,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e0,e0)=e3|sP13_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f1152,f485])).
% 0.13/0.46 fof(f1200,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e3,e3)=e0|sP13_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f1154,f485])).
% 0.13/0.46 fof(f1204,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e0,e0)=e3|sP14_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f1198,f490])).
% 0.13/0.46 fof(f1206,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e3,e3)=e0|sP14_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f1200,f490])).
% 0.13/0.46 fof(f1210,plain,(
% 0.13/0.46 op(e3,e3)=e2|op(e0,e0)=e3|sP15_prd),
% 0.13/0.46 inference(resolution,[status(thm)],[f1204,f620])).
% 0.13/0.46 fof(f1212,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,e3)=e0|sP15_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1206,f620])).
% 0.13/0.47 fof(f1216,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e0,e0)=e3|sP16_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1210,f495])).
% 0.13/0.47 fof(f1268,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,e3)=e0|sP16_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1212,f495])).
% 0.13/0.47 fof(f1272,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e0,e0)=e3|sP17_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1216,f498])).
% 0.13/0.47 fof(f1274,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,e3)=e0|sP17_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1268,f498])).
% 0.13/0.47 fof(f1283,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e0,e0)=e3|sP18_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1272,f503])).
% 0.13/0.47 fof(f1285,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,e3)=e0|sP18_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1274,f503])).
% 0.13/0.47 fof(f1289,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e0,e0)=e3|sP19_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1283,f507])).
% 0.13/0.47 fof(f1291,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,e3)=e0|sP19_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1285,f507])).
% 0.13/0.47 fof(f1295,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e0,e0)=e3|sP20_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1289,f619])).
% 0.13/0.47 fof(f1297,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e0,e0)=e3),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1295,f656])).
% 0.13/0.47 fof(f1315,plain,(
% 0.13/0.47 op(e3,e3)=e2|e1=e3|op(e3,e3)=e1|e2=e1),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f626,f1297])).
% 0.13/0.47 fof(f1335,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,e3)=e1|e2=e1),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1315,f200])).
% 0.13/0.47 fof(f1372,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,e3)=e0|sP20_prd),
% 0.13/0.47 inference(resolution,[status(thm)],[f1291,f619])).
% 0.13/0.47 fof(f1374,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,e3)=e0),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1372,f655])).
% 0.13/0.47 fof(f1442,plain,(
% 0.13/0.47 op(e3,e3)=e2|e0=e1|e2=e1|op(e3,e3)=e2),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f1374,f1335])).
% 0.13/0.47 fof(f1452,plain,(
% 0.13/0.47 op(e3,e3)=e2|e0=e1|e2=e1),
% 0.13/0.47 inference(duplicate_literals_removal,[status(thm)],[f1442])).
% 0.13/0.47 fof(f1453,plain,(
% 0.13/0.47 op(e3,e3)=e2|e2=e1),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1452,f195])).
% 0.13/0.47 fof(f1482,plain,(
% 0.13/0.47 e2=e1|unit=e1|unit=e2|unit=e3|unit=e4|e2=e1),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f1453,f958])).
% 0.13/0.47 fof(f1491,plain,(
% 0.13/0.47 e2=e1|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.13/0.47 inference(duplicate_literals_removal,[status(thm)],[f1482])).
% 0.13/0.47 fof(f1492,plain,(
% 0.13/0.47 unit=e1|unit=e2|unit=e3|unit=e4),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1491,f199])).
% 0.13/0.47 fof(f1544,plain,(
% 0.13/0.47 ~op(unit,e0)=e0|unit=e2|unit=e3|unit=e4),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f1492,f519])).
% 0.13/0.47 fof(f1620,plain,(
% 0.13/0.47 ~e0=e0|unit=e2|unit=e3|unit=e4),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f34,f1544])).
% 0.13/0.47 fof(f1621,plain,(
% 0.13/0.47 unit=e2|unit=e3|unit=e4),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f1620])).
% 0.13/0.47 fof(f1674,plain,(
% 0.13/0.47 ~op(e0,unit)=e0|unit=e3|unit=e4),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f1621,f522])).
% 0.13/0.47 fof(f1737,plain,(
% 0.13/0.47 ~e0=e0|unit=e3|unit=e4),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f35,f1674])).
% 0.13/0.47 fof(f1738,plain,(
% 0.13/0.47 unit=e3|unit=e4),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f1737])).
% 0.13/0.47 fof(f1761,plain,(
% 0.13/0.47 op(e3,e3)=e2|op(e3,unit)=e0|unit=e4),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f1738,f1374])).
% 0.13/0.47 fof(f1781,plain,(
% 0.13/0.47 ~op(unit,e2)=op(e3,e3)|unit=e4),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f1738,f182])).
% 0.13/0.47 fof(f1829,plain,(
% 0.13/0.47 op(e3,e3)=e2|e3=e0|unit=e4),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f41,f1761])).
% 0.13/0.47 fof(f1830,plain,(
% 0.13/0.47 op(e3,e3)=e2|unit=e4),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1829,f197])).
% 0.13/0.47 fof(f1853,plain,(
% 0.13/0.47 ~e2=op(e3,e3)|unit=e4),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f38,f1781])).
% 0.13/0.47 fof(f1880,plain,(
% 0.13/0.47 op(e4,e2)=e1|op(e4,e2)=unit),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f2058,f630])).
% 0.13/0.47 fof(f1889,plain,(
% 0.13/0.47 ~op(e3,e2)=op(e3,unit)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f2058,f183])).
% 0.13/0.47 fof(f2058,plain,(
% 0.13/0.47 unit=e4),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1853,f1830])).
% 0.13/0.47 fof(f2208,plain,(
% 0.13/0.47 op(unit,e2)=e1|op(e4,e2)=unit),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2058,f1880])).
% 0.13/0.47 fof(f2209,plain,(
% 0.13/0.47 e2=e1|op(e4,e2)=unit),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f38,f2208])).
% 0.13/0.47 fof(f2210,plain,(
% 0.13/0.47 e2=e1|op(unit,e2)=unit),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2058,f2209])).
% 0.13/0.47 fof(f2211,plain,(
% 0.13/0.47 e2=e1|e2=unit),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f38,f2210])).
% 0.13/0.47 fof(f2276,plain,(
% 0.13/0.47 e2=unit),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f2211,f199])).
% 0.13/0.47 fof(f2301,plain,(
% 0.13/0.47 ~op(e3,unit)=op(e3,unit)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2276,f1889])).
% 0.13/0.47 fof(f2302,plain,(
% 0.13/0.47 ~e3=op(e3,unit)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f41,f2301])).
% 0.13/0.47 fof(f2303,plain,(
% 0.13/0.47 ~e3=e3),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f41,f2302])).
% 0.13/0.47 fof(f2304,plain,(
% 0.13/0.47 $false),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f2303])).
% 0.13/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.47 % Elapsed time: 0.109769 seconds
% 0.13/0.47 % CPU time: 0.616188 seconds
% 0.13/0.47 % Total memory used: 125.678 MB
% 0.13/0.47 % Net memory used: 125.272 MB
%------------------------------------------------------------------------------