%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG067+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 : n020.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.12s 10.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG067+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/10.37 % Computer : n020.cluster.edu
% 0.09/10.37 % Model : x86_64 x86_64
% 0.09/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.37 % Memory : 8046.5625MB
% 0.09/10.37 % OS : Linux 6.8.0-71-generic
% 0.09/10.37 % CPULimit : 300
% 0.09/10.37 % WCLimit : 300
% 0.09/10.37 % DateTime : Mon Sep 21 12:56:13 UTC 2026
% 0.09/10.37 % CPUTime :
% 0.09/10.39 % Drodi V4.1.1
% 0.12/10.44 % Refutation found
% 0.12/10.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/10.44 % SZS output start CNFRefutation for theBenchmark
% 0.12/10.44 fof(f2,axiom,(
% 0.12/10.44 ( 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.12/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.44 fof(f4,axiom,(
% 0.12/10.44 ( 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.12/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.44 fof(f5,axiom,(
% 0.12/10.44 ( e0 != e1& e0 != e2& e0 != e3& e0 != e4& e1 != e2& e1 != e3& e1 != e4& e2 != e3& e2 != e4& e3 != e4 ) ),
% 0.12/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.44 fof(f6,axiom,(
% 0.12/10.44 ( e0 = op(op(e4,e2),op(e4,e2))& e1 = op(e4,e2)& e3 = op(e2,e4) ) ),
% 0.12/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.44 fof(f7,conjecture,(
% 0.12/10.44 ~ ( ( op(e0,e0) != e0| op(e0,e0) = e0 )& ( op(e0,e0) != e1| op(e0,e1) = e0 )& ( op(e0,e0) != e2| op(e0,e2) = e0 )& ( op(e0,e0) != e3| op(e0,e3) = e0 )& ( op(e0,e0) != e4| op(e0,e4) = e0 )& ( op(e1,e1) != e0| op(e1,e0) = e1 )& ( op(e1,e1) != e1| op(e1,e1) = e1 )& ( op(e1,e1) != e2| op(e1,e2) = e1 )& ( op(e1,e1) != e3| op(e1,e3) = e1 )& ( op(e1,e1) != e4| op(e1,e4) = e1 )& ( op(e2,e2) != e0| op(e2,e0) = e2 )& ( op(e2,e2) != e1| op(e2,e1) = e2 )& ( op(e2,e2) != e2| op(e2,e2) = e2 )& ( op(e2,e2) != e3| op(e2,e3) = e2 )& ( op(e2,e2) != e4| op(e2,e4) = e2 )& ( op(e3,e3) != e0| op(e3,e0) = e3 )& ( op(e3,e3) != e1| op(e3,e1) = e3 )& ( op(e3,e3) != e2| op(e3,e2) = e3 )& ( op(e3,e3) != e3| op(e3,e3) = e3 )& ( op(e3,e3) != e4| op(e3,e4) = e3 )& ( op(e4,e4) != e0| op(e4,e0) = e4 )& ( op(e4,e4) != e1| op(e4,e1) = e4 )& ( op(e4,e4) != e2| op(e4,e2) = e4 )& ( op(e4,e4) != e3| op(e4,e3) = e4 )& ( op(e4,e4) != e4| op(e4,e4) = e4 )& ( ( op(e0,e0) = 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.12/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.44 fof(f8,negated_conjecture,(
% 0.12/10.44 ~(~ ( ( op(e0,e0) != e0| op(e0,e0) = e0 )& ( op(e0,e0) != e1| op(e0,e1) = e0 )& ( op(e0,e0) != e2| op(e0,e2) = e0 )& ( op(e0,e0) != e3| op(e0,e3) = e0 )& ( op(e0,e0) != e4| op(e0,e4) = e0 )& ( op(e1,e1) != e0| op(e1,e0) = e1 )& ( op(e1,e1) != e1| op(e1,e1) = e1 )& ( op(e1,e1) != e2| op(e1,e2) = e1 )& ( op(e1,e1) != e3| op(e1,e3) = e1 )& ( op(e1,e1) != e4| op(e1,e4) = e1 )& ( op(e2,e2) != e0| op(e2,e0) = e2 )& ( op(e2,e2) != e1| op(e2,e1) = e2 )& ( op(e2,e2) != e2| op(e2,e2) = e2 )& ( op(e2,e2) != e3| op(e2,e3) = e2 )& ( op(e2,e2) != e4| op(e2,e4) = e2 )& ( op(e3,e3) != e0| op(e3,e0) = e3 )& ( op(e3,e3) != e1| op(e3,e1) = e3 )& ( op(e3,e3) != e2| op(e3,e2) = e3 )& ( op(e3,e3) != e3| op(e3,e3) = e3 )& ( op(e3,e3) != e4| op(e3,e4) = e3 )& ( op(e4,e4) != e0| op(e4,e0) = e4 )& ( op(e4,e4) != e1| op(e4,e1) = e4 )& ( op(e4,e4) != e2| op(e4,e2) = e4 )& ( op(e4,e4) != e3| op(e4,e3) = e4 )& ( op(e4,e4) != e4| op(e4,e4) = e4 )& ( ( op(e0,e0) = 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.12/10.44 inference(negated_conjecture,[status(cth)],[f7])).
% 0.12/10.44 fof(f35,plain,(
% 0.12/10.44 op(e0,unit)=e0),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/10.44 fof(f37,plain,(
% 0.12/10.44 op(e1,unit)=e1),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/10.44 fof(f39,plain,(
% 0.12/10.44 op(e2,unit)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/10.44 fof(f41,plain,(
% 0.12/10.44 op(e3,unit)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/10.44 fof(f43,plain,(
% 0.12/10.44 op(e4,unit)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/10.44 fof(f44,plain,(
% 0.12/10.44 unit=e0|unit=e1|unit=e2|unit=e3|unit=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/10.44 fof(f95,plain,(
% 0.12/10.44 ~op(e0,e0)=op(e1,e0)),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/10.44 fof(f142,plain,(
% 0.12/10.44 ~op(e2,e4)=op(e3,e4)),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/10.44 fof(f143,plain,(
% 0.12/10.44 ~op(e2,e4)=op(e4,e4)),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/10.44 fof(f157,plain,(
% 0.12/10.44 ~op(e1,e0)=op(e1,e3)),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/10.44 fof(f173,plain,(
% 0.12/10.44 ~op(e2,e2)=op(e2,e4)),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/10.44 fof(f195,plain,(
% 0.12/10.44 ~e0=e1),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/10.44 fof(f196,plain,(
% 0.12/10.44 ~e0=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/10.44 fof(f197,plain,(
% 0.12/10.44 ~e0=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/10.44 fof(f198,plain,(
% 0.12/10.44 ~e0=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/10.44 fof(f201,plain,(
% 0.12/10.44 ~e1=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/10.44 fof(f202,plain,(
% 0.12/10.44 ~e2=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/10.44 fof(f205,plain,(
% 0.12/10.44 e0=op(op(e4,e2),op(e4,e2))),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/10.44 fof(f206,plain,(
% 0.12/10.44 e1=op(e4,e2)),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/10.44 fof(f207,plain,(
% 0.12/10.44 e3=op(e2,e4)),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/10.44 fof(f208,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/10.44 fof(f209,plain,(
% 0.12/10.44 (((((((((((((((((((((((((~op(e0,e0)=e0|op(e0,e0)=e0)&(~op(e0,e0)=e1|op(e0,e1)=e0))&(~op(e0,e0)=e2|op(e0,e2)=e0))&(~op(e0,e0)=e3|op(e0,e3)=e0))&(~op(e0,e0)=e4|op(e0,e4)=e0))&(~op(e1,e1)=e0|op(e1,e0)=e1))&(~op(e1,e1)=e1|op(e1,e1)=e1))&(~op(e1,e1)=e2|op(e1,e2)=e1))&(~op(e1,e1)=e3|op(e1,e3)=e1))&(~op(e1,e1)=e4|op(e1,e4)=e1))&(~op(e2,e2)=e0|op(e2,e0)=e2))&(~op(e2,e2)=e1|op(e2,e1)=e2))&(~op(e2,e2)=e2|op(e2,e2)=e2))&(~op(e2,e2)=e3|op(e2,e3)=e2))&(~op(e2,e2)=e4|op(e2,e4)=e2))&(~op(e3,e3)=e0|op(e3,e0)=e3))&(~op(e3,e3)=e1|op(e3,e1)=e3))&(~op(e3,e3)=e2|op(e3,e2)=e3))&(~op(e3,e3)=e3|op(e3,e3)=e3))&(~op(e3,e3)=e4|op(e3,e4)=e3))&(~op(e4,e4)=e0|op(e4,e0)=e4))&(~op(e4,e4)=e1|op(e4,e1)=e4))&(~op(e4,e4)=e2|op(e4,e2)=e4))&(~op(e4,e4)=e3|op(e4,e3)=e4))&(~op(e4,e4)=e4|op(e4,e4)=e4))&(sP0_prd|((op(e4,e4)=e4&op(e4,e4)=e4)&~op(e4,e4)=e4))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f8,f208])).
% 0.12/10.44 fof(f215,plain,(
% 0.12/10.44 ~op(e1,e1)=e0|op(e1,e0)=e1),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f209])).
% 0.12/10.44 fof(f224,plain,(
% 0.12/10.44 ~op(e2,e2)=e4|op(e2,e4)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f209])).
% 0.12/10.44 fof(f232,plain,(
% 0.12/10.44 ~op(e4,e4)=e2|op(e4,e2)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f209])).
% 0.12/10.44 fof(f235,plain,(
% 0.12/10.44 sP0_prd|op(e4,e4)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f209])).
% 0.12/10.44 fof(f237,plain,(
% 0.12/10.44 sP0_prd|~op(e4,e4)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f209])).
% 0.12/10.44 fof(f238,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.12/10.44 fof(f239,plain,(
% 0.12/10.44 sP0_prd<=>(sP1_prd|((op(e4,e4)=e3&op(e3,e3)=e4)&~op(e4,e3)=e4))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f208,f238])).
% 0.12/10.44 fof(f240,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f239])).
% 0.12/10.44 fof(f241,plain,(
% 0.12/10.44 ~sP0_prd|sP1_prd|op(e4,e4)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f240])).
% 0.12/10.44 fof(f246,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.12/10.44 fof(f247,plain,(
% 0.12/10.44 sP1_prd<=>(sP2_prd|((op(e4,e4)=e2&op(e2,e2)=e4)&~op(e4,e2)=e4))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f238,f246])).
% 0.12/10.44 fof(f248,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f247])).
% 0.12/10.44 fof(f249,plain,(
% 0.12/10.44 ~sP1_prd|sP2_prd|op(e4,e4)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f248])).
% 0.12/10.44 fof(f254,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.12/10.44 fof(f255,plain,(
% 0.12/10.44 sP2_prd<=>(sP3_prd|((op(e4,e4)=e1&op(e1,e1)=e4)&~op(e4,e1)=e4))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f246,f254])).
% 0.12/10.44 fof(f256,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f255])).
% 0.12/10.44 fof(f258,plain,(
% 0.12/10.44 ~sP2_prd|sP3_prd|op(e1,e1)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f256])).
% 0.12/10.44 fof(f262,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.12/10.44 fof(f263,plain,(
% 0.12/10.44 sP3_prd<=>(sP4_prd|((op(e4,e4)=e0&op(e0,e0)=e4)&~op(e4,e0)=e4))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f254,f262])).
% 0.12/10.44 fof(f264,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f263])).
% 0.12/10.44 fof(f267,plain,(
% 0.12/10.44 ~sP3_prd|sP4_prd|~op(e4,e0)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f264])).
% 0.12/10.44 fof(f270,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.12/10.44 fof(f271,plain,(
% 0.12/10.44 sP4_prd<=>(sP5_prd|((op(e3,e3)=e4&op(e4,e4)=e3)&~op(e3,e4)=e3))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f262,f270])).
% 0.12/10.44 fof(f272,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f271])).
% 0.12/10.44 fof(f274,plain,(
% 0.12/10.44 ~sP4_prd|sP5_prd|op(e4,e4)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f272])).
% 0.12/10.44 fof(f278,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.12/10.44 fof(f279,plain,(
% 0.12/10.44 sP5_prd<=>(sP6_prd|((op(e3,e3)=e3&op(e3,e3)=e3)&~op(e3,e3)=e3))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f270,f278])).
% 0.12/10.44 fof(f280,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f279])).
% 0.12/10.44 fof(f281,plain,(
% 0.12/10.44 ~sP5_prd|sP6_prd|op(e3,e3)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f280])).
% 0.12/10.44 fof(f283,plain,(
% 0.12/10.44 ~sP5_prd|sP6_prd|~op(e3,e3)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f280])).
% 0.12/10.44 fof(f286,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.12/10.44 fof(f287,plain,(
% 0.12/10.44 sP6_prd<=>(sP7_prd|((op(e3,e3)=e2&op(e2,e2)=e3)&~op(e3,e2)=e3))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f278,f286])).
% 0.12/10.44 fof(f288,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f287])).
% 0.12/10.44 fof(f290,plain,(
% 0.12/10.44 ~sP6_prd|sP7_prd|op(e2,e2)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f288])).
% 0.12/10.44 fof(f294,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.12/10.44 fof(f295,plain,(
% 0.12/10.44 sP7_prd<=>(sP8_prd|((op(e3,e3)=e1&op(e1,e1)=e3)&~op(e3,e1)=e3))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f286,f294])).
% 0.12/10.44 fof(f296,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f295])).
% 0.12/10.44 fof(f298,plain,(
% 0.12/10.44 ~sP7_prd|sP8_prd|op(e1,e1)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f296])).
% 0.12/10.44 fof(f302,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.12/10.44 fof(f303,plain,(
% 0.12/10.44 sP8_prd<=>(sP9_prd|((op(e3,e3)=e0&op(e0,e0)=e3)&~op(e3,e0)=e3))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f294,f302])).
% 0.12/10.44 fof(f304,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f303])).
% 0.12/10.44 fof(f307,plain,(
% 0.12/10.44 ~sP8_prd|sP9_prd|~op(e3,e0)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f304])).
% 0.12/10.44 fof(f310,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.12/10.44 fof(f311,plain,(
% 0.12/10.44 sP9_prd<=>(sP10_prd|((op(e2,e2)=e4&op(e4,e4)=e2)&~op(e2,e4)=e2))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f302,f310])).
% 0.12/10.44 fof(f312,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f311])).
% 0.12/10.44 fof(f313,plain,(
% 0.12/10.44 ~sP9_prd|sP10_prd|op(e2,e2)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f312])).
% 0.12/10.44 fof(f318,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.12/10.44 fof(f319,plain,(
% 0.12/10.44 sP10_prd<=>(sP11_prd|((op(e2,e2)=e3&op(e3,e3)=e2)&~op(e2,e3)=e2))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f310,f318])).
% 0.12/10.44 fof(f320,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f319])).
% 0.12/10.44 fof(f321,plain,(
% 0.12/10.44 ~sP10_prd|sP11_prd|op(e2,e2)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f320])).
% 0.12/10.44 fof(f326,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.12/10.44 fof(f327,plain,(
% 0.12/10.44 sP11_prd<=>(sP12_prd|((op(e2,e2)=e2&op(e2,e2)=e2)&~op(e2,e2)=e2))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f318,f326])).
% 0.12/10.44 fof(f328,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f327])).
% 0.12/10.44 fof(f329,plain,(
% 0.12/10.44 ~sP11_prd|sP12_prd|op(e2,e2)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f328])).
% 0.12/10.44 fof(f331,plain,(
% 0.12/10.44 ~sP11_prd|sP12_prd|~op(e2,e2)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f328])).
% 0.12/10.44 fof(f334,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.12/10.44 fof(f335,plain,(
% 0.12/10.44 sP12_prd<=>(sP13_prd|((op(e2,e2)=e1&op(e1,e1)=e2)&~op(e2,e1)=e2))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f326,f334])).
% 0.12/10.44 fof(f336,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f335])).
% 0.12/10.44 fof(f338,plain,(
% 0.12/10.44 ~sP12_prd|sP13_prd|op(e1,e1)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f336])).
% 0.12/10.44 fof(f342,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.12/10.44 fof(f343,plain,(
% 0.12/10.44 sP13_prd<=>(sP14_prd|((op(e2,e2)=e0&op(e0,e0)=e2)&~op(e2,e0)=e2))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f334,f342])).
% 0.12/10.44 fof(f344,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f343])).
% 0.12/10.44 fof(f347,plain,(
% 0.12/10.44 ~sP13_prd|sP14_prd|~op(e2,e0)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f344])).
% 0.12/10.44 fof(f350,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.12/10.44 fof(f351,plain,(
% 0.12/10.44 sP14_prd<=>(sP15_prd|((op(e1,e1)=e4&op(e4,e4)=e1)&~op(e1,e4)=e1))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f342,f350])).
% 0.12/10.44 fof(f352,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f351])).
% 0.12/10.44 fof(f353,plain,(
% 0.12/10.44 ~sP14_prd|sP15_prd|op(e1,e1)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f352])).
% 0.12/10.44 fof(f358,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 0.12/10.44 fof(f359,plain,(
% 0.12/10.44 sP15_prd<=>(sP16_prd|((op(e1,e1)=e3&op(e3,e3)=e1)&~op(e1,e3)=e1))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f350,f358])).
% 0.12/10.44 fof(f360,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f359])).
% 0.12/10.44 fof(f361,plain,(
% 0.12/10.44 ~sP15_prd|sP16_prd|op(e1,e1)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f360])).
% 0.12/10.44 fof(f366,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP17_prd])],[])).
% 0.12/10.44 fof(f367,plain,(
% 0.12/10.44 sP16_prd<=>(sP17_prd|((op(e1,e1)=e2&op(e2,e2)=e1)&~op(e1,e2)=e1))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f358,f366])).
% 0.12/10.44 fof(f368,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f367])).
% 0.12/10.44 fof(f369,plain,(
% 0.12/10.44 ~sP16_prd|sP17_prd|op(e1,e1)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f368])).
% 0.12/10.44 fof(f374,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.12/10.44 fof(f375,plain,(
% 0.12/10.44 sP17_prd<=>(sP18_prd|((op(e1,e1)=e1&op(e1,e1)=e1)&~op(e1,e1)=e1))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f366,f374])).
% 0.12/10.44 fof(f376,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f375])).
% 0.12/10.44 fof(f377,plain,(
% 0.12/10.44 ~sP17_prd|sP18_prd|op(e1,e1)=e1),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f376])).
% 0.12/10.44 fof(f379,plain,(
% 0.12/10.44 ~sP17_prd|sP18_prd|~op(e1,e1)=e1),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f376])).
% 0.12/10.44 fof(f382,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.12/10.44 fof(f383,plain,(
% 0.12/10.44 sP18_prd<=>(sP19_prd|((op(e1,e1)=e0&op(e0,e0)=e1)&~op(e1,e0)=e1))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f374,f382])).
% 0.12/10.44 fof(f384,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f383])).
% 0.12/10.44 fof(f387,plain,(
% 0.12/10.44 ~sP18_prd|sP19_prd|~op(e1,e0)=e1),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f384])).
% 0.12/10.44 fof(f390,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.12/10.44 fof(f391,plain,(
% 0.12/10.44 sP19_prd<=>(sP20_prd|((op(e0,e0)=e4&op(e4,e4)=e0)&~op(e0,e4)=e0))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f382,f390])).
% 0.12/10.44 fof(f392,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f391])).
% 0.12/10.44 fof(f393,plain,(
% 0.12/10.44 ~sP19_prd|sP20_prd|op(e0,e0)=e4),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f392])).
% 0.12/10.44 fof(f398,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP21_prd])],[])).
% 0.12/10.44 fof(f399,plain,(
% 0.12/10.44 sP20_prd<=>(sP21_prd|((op(e0,e0)=e3&op(e3,e3)=e0)&~op(e0,e3)=e0))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f390,f398])).
% 0.12/10.44 fof(f400,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f399])).
% 0.12/10.44 fof(f401,plain,(
% 0.12/10.44 ~sP20_prd|sP21_prd|op(e0,e0)=e3),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f400])).
% 0.12/10.44 fof(f406,definition,(
% 0.12/10.44 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.12/10.44 introduced(definition,[new_symbols(definition,[sP22_prd])],[])).
% 0.12/10.44 fof(f407,plain,(
% 0.12/10.44 sP21_prd<=>(sP22_prd|((op(e0,e0)=e2&op(e2,e2)=e0)&~op(e0,e2)=e0))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f398,f406])).
% 0.12/10.44 fof(f408,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f407])).
% 0.12/10.44 fof(f409,plain,(
% 0.12/10.44 ~sP21_prd|sP22_prd|op(e0,e0)=e2),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f408])).
% 0.12/10.44 fof(f414,definition,(
% 0.12/10.44 sP23_prd<=>((op(e0,e0)=e0&op(e0,e0)=e0)&~op(e0,e0)=e0)),
% 0.12/10.44 introduced(definition,[new_symbols(definition,[sP23_prd])],[])).
% 0.12/10.44 fof(f415,plain,(
% 0.12/10.44 sP22_prd<=>(sP23_prd|((op(e0,e0)=e1&op(e1,e1)=e0)&~op(e0,e1)=e0))),
% 0.12/10.44 inference(formula_renaming,[status(thm)],[f406,f414])).
% 0.12/10.44 fof(f416,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f415])).
% 0.12/10.44 fof(f417,plain,(
% 0.12/10.44 ~sP22_prd|sP23_prd|op(e0,e0)=e1),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f416])).
% 0.12/10.44 fof(f422,plain,(
% 0.12/10.44 (~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.12/10.44 inference(NNF_transformation,[status(thm)],[f414])).
% 0.12/10.44 fof(f423,plain,(
% 0.12/10.44 ~sP23_prd|op(e0,e0)=e0),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f422])).
% 0.12/10.44 fof(f425,plain,(
% 0.12/10.44 ~sP23_prd|~op(e0,e0)=e0),
% 0.12/10.44 inference(cnf_transformation,[status(thm)],[f422])).
% 0.12/10.44 fof(f427,plain,(
% 0.12/10.44 e0=op(op(e4,e2),e1)),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f206,f205])).
% 0.12/10.44 fof(f448,plain,(
% 0.12/10.44 ~op(e2,e2)=e3),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f207,f173])).
% 0.12/10.44 fof(f451,plain,(
% 0.12/10.44 ~e3=op(e4,e4)),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f207,f143])).
% 0.12/10.44 fof(f452,plain,(
% 0.12/10.44 ~e3=op(e3,e4)),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f207,f142])).
% 0.12/10.44 fof(f466,plain,(
% 0.12/10.44 ~op(e2,e2)=e4|e3=e2),
% 0.12/10.44 inference(forward_demodulation,[status(thm)],[f207,f224])).
% 0.12/10.44 fof(f468,plain,(
% 0.12/10.44 ~op(e2,e2)=e4),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f466,f202])).
% 0.12/10.44 fof(f469,plain,(
% 0.12/10.44 ~op(e4,e4)=e2|e1=e4),
% 0.12/10.44 inference(forward_demodulation,[status(thm)],[f206,f232])).
% 0.12/10.44 fof(f471,plain,(
% 0.12/10.44 ~op(e4,e4)=e2),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f469,f201])).
% 0.12/10.44 fof(f472,plain,(
% 0.12/10.44 sP0_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f237,f235])).
% 0.12/10.44 fof(f473,plain,(
% 0.12/10.44 sP1_prd|op(e4,e4)=e3),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f241,f472])).
% 0.12/10.44 fof(f476,plain,(
% 0.12/10.44 ~sP1_prd|sP2_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f249,f471])).
% 0.12/10.44 fof(f479,plain,(
% 0.12/10.44 ~sP5_prd|sP6_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f283,f281])).
% 0.12/10.44 fof(f480,plain,(
% 0.12/10.44 ~sP9_prd|sP10_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f313,f468])).
% 0.12/10.44 fof(f483,plain,(
% 0.12/10.44 ~sP11_prd|sP12_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f331,f329])).
% 0.12/10.44 fof(f484,plain,(
% 0.12/10.44 ~sP17_prd|sP18_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f379,f377])).
% 0.12/10.44 fof(f487,plain,(
% 0.12/10.44 ~sP22_prd|op(e0,e0)=e1),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f417,f488])).
% 0.12/10.44 fof(f488,plain,(
% 0.12/10.44 ~sP23_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f425,f423])).
% 0.12/10.44 fof(f490,plain,(
% 0.12/10.44 ~sP16_prd|sP17_prd|e0=e2),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f519,f369])).
% 0.12/10.44 fof(f491,plain,(
% 0.12/10.44 ~sP15_prd|sP16_prd|e0=e3),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f519,f361])).
% 0.12/10.44 fof(f492,plain,(
% 0.12/10.44 ~sP14_prd|sP15_prd|e0=e4),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f519,f353])).
% 0.12/10.44 fof(f493,plain,(
% 0.12/10.44 ~sP12_prd|sP13_prd|e0=e2),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f519,f338])).
% 0.12/10.44 fof(f494,plain,(
% 0.12/10.44 ~sP7_prd|sP8_prd|e0=e3),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f519,f298])).
% 0.12/10.44 fof(f495,plain,(
% 0.12/10.44 ~sP2_prd|sP3_prd|e0=e4),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f519,f258])).
% 0.12/10.44 fof(f499,plain,(
% 0.12/10.44 ~e0=e0|op(e1,e0)=e1),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f519,f215])).
% 0.12/10.44 fof(f519,plain,(
% 0.12/10.44 e0=op(e1,e1)),
% 0.12/10.44 inference(forward_demodulation,[status(thm)],[f206,f427])).
% 0.12/10.44 fof(f546,plain,(
% 0.12/10.44 ~sP10_prd|sP11_prd),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f321,f448])).
% 0.12/10.44 fof(f547,plain,(
% 0.12/10.44 ~sP6_prd|sP7_prd),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f290,f448])).
% 0.12/10.44 fof(f552,plain,(
% 0.12/10.44 ~sP4_prd|sP5_prd),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f274,f451])).
% 0.12/10.44 fof(f553,plain,(
% 0.12/10.44 sP1_prd),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f473,f451])).
% 0.12/10.44 fof(f573,plain,(
% 0.12/10.44 ~sP16_prd|sP17_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f490,f196])).
% 0.12/10.44 fof(f574,plain,(
% 0.12/10.44 ~sP15_prd|sP16_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f491,f197])).
% 0.12/10.44 fof(f575,plain,(
% 0.12/10.44 ~sP14_prd|sP15_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f492,f198])).
% 0.12/10.44 fof(f576,plain,(
% 0.12/10.44 ~sP12_prd|sP13_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f493,f196])).
% 0.12/10.44 fof(f577,plain,(
% 0.12/10.44 ~sP7_prd|sP8_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f494,f197])).
% 0.12/10.44 fof(f578,plain,(
% 0.12/10.44 ~sP2_prd|sP3_prd),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f495,f198])).
% 0.12/10.44 fof(f579,plain,(
% 0.12/10.44 ~sP18_prd|sP19_prd|~e1=e1),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f591,f387])).
% 0.12/10.44 fof(f581,plain,(
% 0.12/10.44 ~e1=op(e1,e3)),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f591,f157])).
% 0.12/10.44 fof(f586,plain,(
% 0.12/10.44 ~op(e0,e0)=e1),
% 0.12/10.44 inference(backward_demodulation,[status(thm)],[f591,f95])).
% 0.12/10.44 fof(f591,plain,(
% 0.12/10.44 op(e1,e0)=e1),
% 0.12/10.44 inference(trivial_equality_resolution,[status(thm)],[f499])).
% 0.12/10.44 fof(f619,plain,(
% 0.12/10.44 sP2_prd),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f476,f553])).
% 0.12/10.44 fof(f624,plain,(
% 0.12/10.44 ~sP18_prd|sP19_prd),
% 0.12/10.44 inference(trivial_equality_resolution,[status(thm)],[f579])).
% 0.12/10.44 fof(f633,plain,(
% 0.12/10.44 ~sP22_prd),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f487,f586])).
% 0.12/10.44 fof(f640,plain,(
% 0.12/10.44 sP3_prd),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f578,f619])).
% 0.12/10.44 fof(f645,plain,(
% 0.12/10.44 ~sP21_prd|op(e0,e0)=e2),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f409,f633])).
% 0.12/10.44 fof(f646,plain,(
% 0.12/10.44 sP4_prd|~op(e4,e0)=e4),
% 0.12/10.44 inference(backward_subsumption_resolution,[status(thm)],[f267,f640])).
% 0.12/10.44 fof(f662,plain,(
% 0.12/10.44 sP7_prd|~sP5_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f547,f479])).
% 0.12/10.44 fof(f666,plain,(
% 0.12/10.44 op(e3,e4)=e3|unit=e0|unit=e1|unit=e2|unit=e3),
% 0.12/10.44 inference(paramodulation,[status(thm)],[f44,f41])).
% 0.12/10.44 fof(f678,plain,(
% 0.12/10.44 unit=e0|unit=e1|unit=e2|unit=e3),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f666,f452])).
% 0.12/10.44 fof(f685,plain,(
% 0.12/10.44 ~op(e4,e0)=e4|sP5_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f646,f552])).
% 0.12/10.44 fof(f688,plain,(
% 0.12/10.44 ~op(e4,e0)=e4|sP7_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f685,f662])).
% 0.12/10.44 fof(f695,plain,(
% 0.12/10.44 ~op(e4,e0)=e4|sP8_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f688,f577])).
% 0.12/10.44 fof(f731,plain,(
% 0.12/10.44 sP14_prd|~op(e2,e0)=e2|~sP12_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f347,f576])).
% 0.12/10.44 fof(f777,plain,(
% 0.12/10.44 sP14_prd|~op(e2,e0)=e2|~sP11_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f731,f483])).
% 0.12/10.44 fof(f780,plain,(
% 0.12/10.44 sP14_prd|~op(e2,e0)=e2|~sP10_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f777,f546])).
% 0.12/10.44 fof(f820,plain,(
% 0.12/10.44 sP14_prd|~op(e2,e0)=e2|~sP9_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f780,f480])).
% 0.12/10.44 fof(f825,plain,(
% 0.12/10.44 ~op(e2,e0)=e2|~sP9_prd|sP15_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f820,f575])).
% 0.12/10.44 fof(f862,plain,(
% 0.12/10.44 ~op(e2,e0)=e2|~sP9_prd|sP16_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f825,f574])).
% 0.12/10.44 fof(f918,plain,(
% 0.12/10.44 ~op(e2,e0)=e2|~sP9_prd|sP17_prd),
% 0.12/10.44 inference(resolution,[status(thm)],[f862,f573])).
% 0.12/10.44 fof(f981,plain,(
% 0.12/10.44 op(e1,e3)=e1|unit=e0|unit=e1|unit=e2),
% 0.12/10.44 inference(paramodulation,[status(thm)],[f678,f37])).
% 0.12/10.44 fof(f988,plain,(
% 0.12/10.44 unit=e0|unit=e1|unit=e2),
% 0.12/10.44 inference(forward_subsumption_resolution,[status(thm)],[f981,f581])).
% 0.12/10.45 fof(f989,plain,(
% 0.12/10.45 op(e4,e2)=e4|unit=e0|unit=e1),
% 0.12/10.45 inference(paramodulation,[status(thm)],[f988,f43])).
% 0.12/10.45 fof(f1001,plain,(
% 0.12/10.45 e1=e4|unit=e0|unit=e1),
% 0.12/10.45 inference(forward_demodulation,[status(thm)],[f206,f989])).
% 0.12/10.45 fof(f1002,plain,(
% 0.12/10.45 unit=e0|unit=e1),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1001,f201])).
% 0.12/10.45 fof(f1010,plain,(
% 0.12/10.45 op(e1,e1)=e1|unit=e0),
% 0.12/10.45 inference(paramodulation,[status(thm)],[f1002,f37])).
% 0.12/10.45 fof(f1015,plain,(
% 0.12/10.45 e0=e1|unit=e0),
% 0.12/10.45 inference(forward_demodulation,[status(thm)],[f519,f1010])).
% 0.12/10.45 fof(f1017,plain,(
% 0.12/10.45 op(e4,e0)=e4),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1033,f43])).
% 0.12/10.45 fof(f1019,plain,(
% 0.12/10.45 op(e3,e0)=e3),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1033,f41])).
% 0.12/10.45 fof(f1021,plain,(
% 0.12/10.45 op(e2,e0)=e2),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1033,f39])).
% 0.12/10.45 fof(f1025,plain,(
% 0.12/10.45 op(e0,e0)=e0),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1033,f35])).
% 0.12/10.45 fof(f1033,plain,(
% 0.12/10.45 unit=e0),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1015,f195])).
% 0.12/10.45 fof(f1041,plain,(
% 0.12/10.45 ~e4=e4|sP8_prd),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1017,f695])).
% 0.12/10.45 fof(f1101,plain,(
% 0.12/10.45 ~sP8_prd|sP9_prd|~e3=e3),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1019,f307])).
% 0.12/10.45 fof(f1143,plain,(
% 0.12/10.45 ~e2=e2|~sP9_prd|sP17_prd),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1021,f918])).
% 0.12/10.45 fof(f1205,plain,(
% 0.12/10.45 ~sP20_prd|sP21_prd|e0=e3),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1025,f401])).
% 0.12/10.45 fof(f1206,plain,(
% 0.12/10.45 ~sP19_prd|sP20_prd|e0=e4),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1025,f393])).
% 0.12/10.45 fof(f1214,plain,(
% 0.12/10.45 ~sP21_prd|e0=e2),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1025,f645])).
% 0.12/10.45 fof(f1232,plain,(
% 0.12/10.45 sP8_prd),
% 0.12/10.45 inference(trivial_equality_resolution,[status(thm)],[f1041])).
% 0.12/10.45 fof(f1304,plain,(
% 0.12/10.45 ~sP8_prd|sP9_prd),
% 0.12/10.45 inference(trivial_equality_resolution,[status(thm)],[f1101])).
% 0.12/10.45 fof(f1311,plain,(
% 0.12/10.45 sP9_prd),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1304,f1232])).
% 0.12/10.45 fof(f1354,plain,(
% 0.12/10.45 ~sP9_prd|sP17_prd),
% 0.12/10.45 inference(trivial_equality_resolution,[status(thm)],[f1143])).
% 0.12/10.45 fof(f1355,plain,(
% 0.12/10.45 sP18_prd),
% 0.12/10.45 inference(backward_subsumption_resolution,[status(thm)],[f484,f1357])).
% 0.12/10.45 fof(f1357,plain,(
% 0.12/10.45 sP17_prd),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1354,f1311])).
% 0.12/10.45 fof(f1400,plain,(
% 0.12/10.45 ~sP20_prd|sP21_prd),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1205,f197])).
% 0.12/10.45 fof(f1401,plain,(
% 0.12/10.45 ~sP19_prd|sP20_prd),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1206,f198])).
% 0.12/10.45 fof(f1402,plain,(
% 0.12/10.45 ~sP20_prd),
% 0.12/10.45 inference(backward_subsumption_resolution,[status(thm)],[f1400,f1403])).
% 0.12/10.45 fof(f1403,plain,(
% 0.12/10.45 ~sP21_prd),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1214,f196])).
% 0.12/10.45 fof(f1451,plain,(
% 0.12/10.45 sP19_prd),
% 0.12/10.45 inference(backward_subsumption_resolution,[status(thm)],[f624,f1355])).
% 0.12/10.45 fof(f1481,plain,(
% 0.12/10.45 ~sP19_prd),
% 0.12/10.45 inference(backward_subsumption_resolution,[status(thm)],[f1401,f1402])).
% 0.12/10.45 fof(f1520,plain,(
% 0.12/10.45 $false),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1481,f1451])).
% 0.12/10.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/10.46 % Elapsed time: 0.079847 seconds
% 0.12/10.46 % CPU time: 0.320932 seconds
% 0.12/10.46 % Total memory used: 97.375 MB
% 0.12/10.46 % Net memory used: 97.284 MB
%------------------------------------------------------------------------------