%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG028+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 : n019.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:29 AM UTC 2026
% Result : Theorem 0.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG028+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n019.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:53:51 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f11,axiom,(
% 0.13/0.40 ( e0 = op(op(op(op(e4,e4),e4),e4),op(e4,e4))& e1 = op(op(e4,e4),e4)& e2 = op(op(op(e4,e4),e4),e4)& e3 = op(e4,e4)& e5 = op(op(op(op(e4,e4),e4),e4),e4) ) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f12,conjecture,(
% 0.13/0.40 ~ ( op(e0,e0) = op(e0,e0)& op(e0,e1) = op(e1,e0)& op(e0,e2) = op(e2,e0)& op(e0,e3) = op(e3,e0)& op(e0,e4) = op(e4,e0)& op(e0,e5) = op(e5,e0)& op(e1,e0) = op(e0,e1)& op(e1,e1) = op(e1,e1)& op(e1,e2) = op(e2,e1)& op(e1,e3) = op(e3,e1)& op(e1,e4) = op(e4,e1)& op(e1,e5) = op(e5,e1)& op(e2,e0) = op(e0,e2)& op(e2,e1) = op(e1,e2)& op(e2,e2) = op(e2,e2)& op(e2,e3) = op(e3,e2)& op(e2,e4) = op(e4,e2)& op(e2,e5) = op(e5,e2)& op(e3,e0) = op(e0,e3)& op(e3,e1) = op(e1,e3)& op(e3,e2) = op(e2,e3)& op(e3,e3) = op(e3,e3)& op(e3,e4) = op(e4,e3)& op(e3,e5) = op(e5,e3)& op(e4,e0) = op(e0,e4)& op(e4,e1) = op(e1,e4)& op(e4,e2) = op(e2,e4)& op(e4,e3) = op(e3,e4)& op(e4,e4) = op(e4,e4)& op(e4,e5) = op(e5,e4)& op(e5,e0) = op(e0,e5)& op(e5,e1) = op(e1,e5)& op(e5,e2) = op(e2,e5)& op(e5,e3) = op(e3,e5)& op(e5,e4) = op(e4,e5)& op(e5,e5) = op(e5,e5)& ~ ( op(e0,e0) = op(e0,e0)& op(e0,e1) = op(e1,e0)& op(e0,e2) = op(e2,e0)& op(e0,e3) = op(e3,e0)& op(e0,e4) = op(e4,e0)& op(e0,e5) = op(e5,e0)& op(e1,e0) = op(e0,e1)& op(e1,e1) = op(e1,e1)& op(e1,e2) = op(e2,e1)& op(e1,e3) = op(e3,e1)& op(e1,e4) = op(e4,e1)& op(e1,e5) = op(e5,e1)& op(e2,e0) = op(e0,e2)& op(e2,e1) = op(e1,e2)& op(e2,e2) = op(e2,e2)& op(e2,e3) = op(e3,e2)& op(e2,e4) = op(e4,e2)& op(e2,e5) = op(e5,e2)& op(e3,e0) = op(e0,e3)& op(e3,e1) = op(e1,e3)& op(e3,e2) = op(e2,e3)& op(e3,e3) = op(e3,e3)& op(e3,e4) = op(e4,e3)& op(e3,e5) = op(e5,e3)& op(e4,e0) = op(e0,e4)& op(e4,e1) = op(e1,e4)& op(e4,e2) = op(e2,e4)& op(e4,e3) = op(e3,e4)& op(e4,e4) = op(e4,e4)& op(e4,e5) = op(e5,e4)& op(e5,e0) = op(e0,e5)& op(e5,e1) = op(e1,e5)& op(e5,e2) = op(e2,e5)& op(e5,e3) = op(e3,e5)& op(e5,e4) = op(e4,e5)& op(e5,e5) = op(e5,e5) ) ) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f13,negated_conjecture,(
% 0.13/0.40 ~(~ ( op(e0,e0) = op(e0,e0)& op(e0,e1) = op(e1,e0)& op(e0,e2) = op(e2,e0)& op(e0,e3) = op(e3,e0)& op(e0,e4) = op(e4,e0)& op(e0,e5) = op(e5,e0)& op(e1,e0) = op(e0,e1)& op(e1,e1) = op(e1,e1)& op(e1,e2) = op(e2,e1)& op(e1,e3) = op(e3,e1)& op(e1,e4) = op(e4,e1)& op(e1,e5) = op(e5,e1)& op(e2,e0) = op(e0,e2)& op(e2,e1) = op(e1,e2)& op(e2,e2) = op(e2,e2)& op(e2,e3) = op(e3,e2)& op(e2,e4) = op(e4,e2)& op(e2,e5) = op(e5,e2)& op(e3,e0) = op(e0,e3)& op(e3,e1) = op(e1,e3)& op(e3,e2) = op(e2,e3)& op(e3,e3) = op(e3,e3)& op(e3,e4) = op(e4,e3)& op(e3,e5) = op(e5,e3)& op(e4,e0) = op(e0,e4)& op(e4,e1) = op(e1,e4)& op(e4,e2) = op(e2,e4)& op(e4,e3) = op(e3,e4)& op(e4,e4) = op(e4,e4)& op(e4,e5) = op(e5,e4)& op(e5,e0) = op(e0,e5)& op(e5,e1) = op(e1,e5)& op(e5,e2) = op(e2,e5)& op(e5,e3) = op(e3,e5)& op(e5,e4) = op(e4,e5)& op(e5,e5) = op(e5,e5)& ~ ( op(e0,e0) = op(e0,e0)& op(e0,e1) = op(e1,e0)& op(e0,e2) = op(e2,e0)& op(e0,e3) = op(e3,e0)& op(e0,e4) = op(e4,e0)& op(e0,e5) = op(e5,e0)& op(e1,e0) = op(e0,e1)& op(e1,e1) = op(e1,e1)& op(e1,e2) = op(e2,e1)& op(e1,e3) = op(e3,e1)& op(e1,e4) = op(e4,e1)& op(e1,e5) = op(e5,e1)& op(e2,e0) = op(e0,e2)& op(e2,e1) = op(e1,e2)& op(e2,e2) = op(e2,e2)& op(e2,e3) = op(e3,e2)& op(e2,e4) = op(e4,e2)& op(e2,e5) = op(e5,e2)& op(e3,e0) = op(e0,e3)& op(e3,e1) = op(e1,e3)& op(e3,e2) = op(e2,e3)& op(e3,e3) = op(e3,e3)& op(e3,e4) = op(e4,e3)& op(e3,e5) = op(e5,e3)& op(e4,e0) = op(e0,e4)& op(e4,e1) = op(e1,e4)& op(e4,e2) = op(e2,e4)& op(e4,e3) = op(e3,e4)& op(e4,e4) = op(e4,e4)& op(e4,e5) = op(e5,e4)& op(e5,e0) = op(e0,e5)& op(e5,e1) = op(e1,e5)& op(e5,e2) = op(e2,e5)& op(e5,e3) = op(e3,e5)& op(e5,e4) = op(e4,e5)& op(e5,e5) = op(e5,e5) ) ) )),
% 0.13/0.40 inference(negated_conjecture,[status(cth)],[f12])).
% 0.13/0.40 fof(f552,plain,(
% 0.13/0.40 e1=op(op(e4,e4),e4)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.40 fof(f553,plain,(
% 0.13/0.40 e2=op(op(op(e4,e4),e4),e4)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.40 fof(f554,plain,(
% 0.13/0.40 e3=op(e4,e4)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.40 fof(f555,plain,(
% 0.13/0.40 e5=op(op(op(op(e4,e4),e4),e4),e4)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.40 fof(f556,plain,(
% 0.13/0.40 (((((((((((((((((((((((((((((((((((op(e0,e0)=op(e0,e0)&op(e0,e1)=op(e1,e0))&op(e0,e2)=op(e2,e0))&op(e0,e3)=op(e3,e0))&op(e0,e4)=op(e4,e0))&op(e0,e5)=op(e5,e0))&op(e1,e0)=op(e0,e1))&op(e1,e1)=op(e1,e1))&op(e1,e2)=op(e2,e1))&op(e1,e3)=op(e3,e1))&op(e1,e4)=op(e4,e1))&op(e1,e5)=op(e5,e1))&op(e2,e0)=op(e0,e2))&op(e2,e1)=op(e1,e2))&op(e2,e2)=op(e2,e2))&op(e2,e3)=op(e3,e2))&op(e2,e4)=op(e4,e2))&op(e2,e5)=op(e5,e2))&op(e3,e0)=op(e0,e3))&op(e3,e1)=op(e1,e3))&op(e3,e2)=op(e2,e3))&op(e3,e3)=op(e3,e3))&op(e3,e4)=op(e4,e3))&op(e3,e5)=op(e5,e3))&op(e4,e0)=op(e0,e4))&op(e4,e1)=op(e1,e4))&op(e4,e2)=op(e2,e4))&op(e4,e3)=op(e3,e4))&op(e4,e4)=op(e4,e4))&op(e4,e5)=op(e5,e4))&op(e5,e0)=op(e0,e5))&op(e5,e1)=op(e1,e5))&op(e5,e2)=op(e2,e5))&op(e5,e3)=op(e3,e5))&op(e5,e4)=op(e4,e5))&op(e5,e5)=op(e5,e5))&(((((((((((((((((((((((((((((((((((~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e1,e0))|~op(e0,e2)=op(e2,e0))|~op(e0,e3)=op(e3,e0))|~op(e0,e4)=op(e4,e0))|~op(e0,e5)=op(e5,e0))|~op(e1,e0)=op(e0,e1))|~op(e1,e1)=op(e1,e1))|~op(e1,e2)=op(e2,e1))|~op(e1,e3)=op(e3,e1))|~op(e1,e4)=op(e4,e1))|~op(e1,e5)=op(e5,e1))|~op(e2,e0)=op(e0,e2))|~op(e2,e1)=op(e1,e2))|~op(e2,e2)=op(e2,e2))|~op(e2,e3)=op(e3,e2))|~op(e2,e4)=op(e4,e2))|~op(e2,e5)=op(e5,e2))|~op(e3,e0)=op(e0,e3))|~op(e3,e1)=op(e1,e3))|~op(e3,e2)=op(e2,e3))|~op(e3,e3)=op(e3,e3))|~op(e3,e4)=op(e4,e3))|~op(e3,e5)=op(e5,e3))|~op(e4,e0)=op(e0,e4))|~op(e4,e1)=op(e1,e4))|~op(e4,e2)=op(e2,e4))|~op(e4,e3)=op(e3,e4))|~op(e4,e4)=op(e4,e4))|~op(e4,e5)=op(e5,e4))|~op(e5,e0)=op(e0,e5))|~op(e5,e1)=op(e1,e5))|~op(e5,e2)=op(e2,e5))|~op(e5,e3)=op(e3,e5))|~op(e5,e4)=op(e4,e5))|~op(e5,e5)=op(e5,e5))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.13/0.40 fof(f558,plain,(
% 0.13/0.40 op(e0,e1)=op(e1,e0)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f559,plain,(
% 0.13/0.40 op(e0,e2)=op(e2,e0)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f560,plain,(
% 0.13/0.40 op(e0,e3)=op(e3,e0)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f561,plain,(
% 0.13/0.40 op(e0,e4)=op(e4,e0)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f562,plain,(
% 0.13/0.40 op(e0,e5)=op(e5,e0)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f565,plain,(
% 0.13/0.40 op(e1,e2)=op(e2,e1)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f566,plain,(
% 0.13/0.40 op(e1,e3)=op(e3,e1)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f567,plain,(
% 0.13/0.40 op(e1,e4)=op(e4,e1)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f568,plain,(
% 0.13/0.40 op(e1,e5)=op(e5,e1)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f572,plain,(
% 0.13/0.40 op(e2,e3)=op(e3,e2)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f573,plain,(
% 0.13/0.40 op(e2,e4)=op(e4,e2)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f574,plain,(
% 0.13/0.40 op(e2,e5)=op(e5,e2)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f579,plain,(
% 0.13/0.40 op(e3,e4)=op(e4,e3)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f580,plain,(
% 0.13/0.40 op(e3,e5)=op(e5,e3)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f586,plain,(
% 0.13/0.40 op(e4,e5)=op(e5,e4)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f593,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e1,e0)|~op(e0,e2)=op(e2,e0)|~op(e0,e3)=op(e3,e0)|~op(e0,e4)=op(e4,e0)|~op(e0,e5)=op(e5,e0)|~op(e1,e0)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e2,e1)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f556])).
% 0.13/0.40 fof(f619,plain,(
% 0.13/0.40 e2=op(e1,e4)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f552,f553])).
% 0.13/0.40 fof(f641,plain,(
% 0.13/0.40 e5=op(op(e1,e4),e4)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f552,f555])).
% 0.13/0.40 fof(f662,plain,(
% 0.13/0.40 e5=op(e2,e4)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f619,f641])).
% 0.13/0.40 fof(f814,plain,(
% 0.13/0.40 e2=op(e4,e1)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f619,f567])).
% 0.13/0.40 fof(f863,plain,(
% 0.13/0.40 e5=op(e4,e2)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f662,f573])).
% 0.13/0.40 fof(f922,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e2,e0)|~op(e0,e3)=op(e3,e0)|~op(e0,e4)=op(e4,e0)|~op(e0,e5)=op(e5,e0)|~op(e1,e0)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e2,e1)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f558,f593])).
% 0.13/0.40 fof(f923,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e3,e0)|~op(e0,e4)=op(e4,e0)|~op(e0,e5)=op(e5,e0)|~op(e1,e0)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e2,e1)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f559,f922])).
% 0.13/0.40 fof(f924,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e4,e0)|~op(e0,e5)=op(e5,e0)|~op(e1,e0)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e2,e1)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f560,f923])).
% 0.13/0.40 fof(f925,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e5,e0)|~op(e1,e0)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e2,e1)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f561,f924])).
% 0.13/0.40 fof(f926,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e1,e0)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e2,e1)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f562,f925])).
% 0.13/0.40 fof(f927,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e2,e1)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f558,f926])).
% 0.13/0.40 fof(f928,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e3,e1)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f565,f927])).
% 0.13/0.40 fof(f929,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~op(e1,e4)=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f566,f928])).
% 0.13/0.40 fof(f930,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=op(e4,e1)|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f619,f929])).
% 0.13/0.40 fof(f931,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e5,e1)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f814,f930])).
% 0.13/0.40 fof(f932,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e2,e0)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f568,f931])).
% 0.13/0.40 fof(f933,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e2,e1)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f559,f932])).
% 0.13/0.40 fof(f934,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e3,e2)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f565,f933])).
% 0.13/0.40 fof(f935,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~op(e2,e4)=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f572,f934])).
% 0.13/0.40 fof(f936,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=op(e4,e2)|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f662,f935])).
% 0.13/0.40 fof(f937,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e5,e2)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f863,f936])).
% 0.13/0.40 fof(f938,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e3,e0)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f574,f937])).
% 0.13/0.40 fof(f939,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e3,e1)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f560,f938])).
% 0.13/0.40 fof(f940,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e3,e2)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f566,f939])).
% 0.13/0.40 fof(f941,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e4,e3)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f572,f940])).
% 0.13/0.40 fof(f942,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e5,e3)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f579,f941])).
% 0.13/0.40 fof(f943,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e4,e0)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f580,f942])).
% 0.13/0.40 fof(f944,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~op(e4,e1)=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f561,f943])).
% 0.13/0.40 fof(f945,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=op(e1,e4)|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f814,f944])).
% 0.13/0.40 fof(f946,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~op(e4,e2)=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f619,f945])).
% 0.13/0.40 fof(f947,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=op(e2,e4)|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f863,f946])).
% 0.13/0.40 fof(f948,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e4,e3)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f662,f947])).
% 0.13/0.40 fof(f949,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~op(e4,e4)=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f579,f948])).
% 0.13/0.40 fof(f950,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~e3=op(e4,e4)|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f554,f949])).
% 0.13/0.40 fof(f951,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~e3=e3|~op(e4,e5)=op(e5,e4)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f554,f950])).
% 0.13/0.40 fof(f952,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~e3=e3|~op(e4,e5)=op(e4,e5)|~op(e5,e0)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f586,f951])).
% 0.13/0.40 fof(f953,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~e3=e3|~op(e4,e5)=op(e4,e5)|~op(e0,e5)=op(e0,e5)|~op(e5,e1)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f562,f952])).
% 0.13/0.40 fof(f954,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~e3=e3|~op(e4,e5)=op(e4,e5)|~op(e0,e5)=op(e0,e5)|~op(e1,e5)=op(e1,e5)|~op(e5,e2)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f568,f953])).
% 0.13/0.40 fof(f955,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~e3=e3|~op(e4,e5)=op(e4,e5)|~op(e0,e5)=op(e0,e5)|~op(e1,e5)=op(e1,e5)|~op(e2,e5)=op(e2,e5)|~op(e5,e3)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f574,f954])).
% 0.13/0.40 fof(f956,plain,(
% 0.13/0.40 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~e3=e3|~op(e4,e5)=op(e4,e5)|~op(e0,e5)=op(e0,e5)|~op(e1,e5)=op(e1,e5)|~op(e2,e5)=op(e2,e5)|~op(e3,e5)=op(e3,e5)|~op(e5,e4)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f580,f955])).
% 0.13/0.41 fof(f957,plain,(
% 0.13/0.41 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e0,e1)=op(e0,e1)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e0,e2)=op(e0,e2)|~op(e1,e2)=op(e1,e2)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e0,e3)=op(e0,e3)|~op(e1,e3)=op(e1,e3)|~op(e2,e3)=op(e2,e3)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~op(e0,e4)=op(e0,e4)|~e2=e2|~e5=e5|~op(e3,e4)=op(e3,e4)|~e3=e3|~op(e4,e5)=op(e4,e5)|~op(e0,e5)=op(e0,e5)|~op(e1,e5)=op(e1,e5)|~op(e2,e5)=op(e2,e5)|~op(e3,e5)=op(e3,e5)|~op(e4,e5)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f586,f956])).
% 0.13/0.41 fof(f958,plain,(
% 0.13/0.41 ~op(e0,e0)=op(e0,e0)|~op(e0,e1)=op(e0,e1)|~op(e0,e2)=op(e0,e2)|~op(e0,e3)=op(e0,e3)|~op(e0,e4)=op(e0,e4)|~op(e0,e5)=op(e0,e5)|~op(e1,e1)=op(e1,e1)|~op(e1,e2)=op(e1,e2)|~op(e1,e3)=op(e1,e3)|~e2=e2|~op(e1,e5)=op(e1,e5)|~op(e2,e2)=op(e2,e2)|~op(e2,e3)=op(e2,e3)|~e5=e5|~op(e2,e5)=op(e2,e5)|~op(e3,e3)=op(e3,e3)|~op(e3,e4)=op(e3,e4)|~op(e3,e5)=op(e3,e5)|~e3=e3|~op(e4,e5)=op(e4,e5)|~op(e5,e5)=op(e5,e5)),
% 0.13/0.41 inference(duplicate_literals_removal,[status(thm)],[f957])).
% 0.13/0.41 fof(f959,plain,(
% 0.13/0.41 $false),
% 0.13/0.41 inference(trivial_equality_resolution,[status(thm)],[f958])).
% 0.13/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.43 % Elapsed time: 0.070080 seconds
% 0.13/0.43 % CPU time: 0.210497 seconds
% 0.13/0.43 % Total memory used: 114.722 MB
% 0.13/0.43 % Net memory used: 114.579 MB
%------------------------------------------------------------------------------