%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG023+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:49:28 AM UTC 2026
% Result : Unsatisfiable 0.12s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG023+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.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 12:53:28 UTC 2026
% 0.12/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.51 % Refutation found
% 0.12/0.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.51 fof(f1,axiom,(
% 0.12/0.51 ( ( op(e0,e0) = e0| op(e0,e0) = e1| op(e0,e0) = e2| op(e0,e0) = e3 )& ( op(e0,e1) = e0| op(e0,e1) = e1| op(e0,e1) = e2| op(e0,e1) = e3 )& ( op(e0,e2) = e0| op(e0,e2) = e1| op(e0,e2) = e2| op(e0,e2) = e3 )& ( op(e0,e3) = e0| op(e0,e3) = e1| op(e0,e3) = e2| op(e0,e3) = e3 )& ( op(e1,e0) = e0| op(e1,e0) = e1| op(e1,e0) = e2| op(e1,e0) = e3 )& ( op(e1,e1) = e0| op(e1,e1) = e1| op(e1,e1) = e2| op(e1,e1) = e3 )& ( op(e1,e2) = e0| op(e1,e2) = e1| op(e1,e2) = e2| op(e1,e2) = e3 )& ( op(e1,e3) = e0| op(e1,e3) = e1| op(e1,e3) = e2| op(e1,e3) = e3 )& ( op(e2,e0) = e0| op(e2,e0) = e1| op(e2,e0) = e2| op(e2,e0) = e3 )& ( op(e2,e1) = e0| op(e2,e1) = e1| op(e2,e1) = e2| op(e2,e1) = e3 )& ( op(e2,e2) = e0| op(e2,e2) = e1| op(e2,e2) = e2| op(e2,e2) = e3 )& ( op(e2,e3) = e0| op(e2,e3) = e1| op(e2,e3) = e2| op(e2,e3) = e3 )& ( op(e3,e0) = e0| op(e3,e0) = e1| op(e3,e0) = e2| op(e3,e0) = e3 )& ( op(e3,e1) = e0| op(e3,e1) = e1| op(e3,e1) = e2| op(e3,e1) = e3 )& ( op(e3,e2) = e0| op(e3,e2) = e1| op(e3,e2) = e2| op(e3,e2) = e3 )& ( op(e3,e3) = e0| op(e3,e3) = e1| op(e3,e3) = e2| op(e3,e3) = e3 ) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f2,axiom,(
% 0.12/0.52 ( op(op(e0,e0),e0) = op(e0,op(e0,e0))& op(op(e0,e0),e1) = op(e0,op(e0,e1))& op(op(e0,e0),e2) = op(e0,op(e0,e2))& op(op(e0,e0),e3) = op(e0,op(e0,e3))& op(op(e0,e1),e0) = op(e0,op(e1,e0))& op(op(e0,e1),e1) = op(e0,op(e1,e1))& op(op(e0,e1),e2) = op(e0,op(e1,e2))& op(op(e0,e1),e3) = op(e0,op(e1,e3))& op(op(e0,e2),e0) = op(e0,op(e2,e0))& op(op(e0,e2),e1) = op(e0,op(e2,e1))& op(op(e0,e2),e2) = op(e0,op(e2,e2))& op(op(e0,e2),e3) = op(e0,op(e2,e3))& op(op(e0,e3),e0) = op(e0,op(e3,e0))& op(op(e0,e3),e1) = op(e0,op(e3,e1))& op(op(e0,e3),e2) = op(e0,op(e3,e2))& op(op(e0,e3),e3) = op(e0,op(e3,e3))& op(op(e1,e0),e0) = op(e1,op(e0,e0))& op(op(e1,e0),e1) = op(e1,op(e0,e1))& op(op(e1,e0),e2) = op(e1,op(e0,e2))& op(op(e1,e0),e3) = op(e1,op(e0,e3))& op(op(e1,e1),e0) = op(e1,op(e1,e0))& op(op(e1,e1),e1) = op(e1,op(e1,e1))& op(op(e1,e1),e2) = op(e1,op(e1,e2))& op(op(e1,e1),e3) = op(e1,op(e1,e3))& op(op(e1,e2),e0) = op(e1,op(e2,e0))& op(op(e1,e2),e1) = op(e1,op(e2,e1))& op(op(e1,e2),e2) = op(e1,op(e2,e2))& op(op(e1,e2),e3) = op(e1,op(e2,e3))& op(op(e1,e3),e0) = op(e1,op(e3,e0))& op(op(e1,e3),e1) = op(e1,op(e3,e1))& op(op(e1,e3),e2) = op(e1,op(e3,e2))& op(op(e1,e3),e3) = op(e1,op(e3,e3))& op(op(e2,e0),e0) = op(e2,op(e0,e0))& op(op(e2,e0),e1) = op(e2,op(e0,e1))& op(op(e2,e0),e2) = op(e2,op(e0,e2))& op(op(e2,e0),e3) = op(e2,op(e0,e3))& op(op(e2,e1),e0) = op(e2,op(e1,e0))& op(op(e2,e1),e1) = op(e2,op(e1,e1))& op(op(e2,e1),e2) = op(e2,op(e1,e2))& op(op(e2,e1),e3) = op(e2,op(e1,e3))& op(op(e2,e2),e0) = op(e2,op(e2,e0))& op(op(e2,e2),e1) = op(e2,op(e2,e1))& op(op(e2,e2),e2) = op(e2,op(e2,e2))& op(op(e2,e2),e3) = op(e2,op(e2,e3))& op(op(e2,e3),e0) = op(e2,op(e3,e0))& op(op(e2,e3),e1) = op(e2,op(e3,e1))& op(op(e2,e3),e2) = op(e2,op(e3,e2))& op(op(e2,e3),e3) = op(e2,op(e3,e3))& op(op(e3,e0),e0) = op(e3,op(e0,e0))& op(op(e3,e0),e1) = op(e3,op(e0,e1))& op(op(e3,e0),e2) = op(e3,op(e0,e2))& op(op(e3,e0),e3) = op(e3,op(e0,e3))& op(op(e3,e1),e0) = op(e3,op(e1,e0))& op(op(e3,e1),e1) = op(e3,op(e1,e1))& op(op(e3,e1),e2) = op(e3,op(e1,e2))& op(op(e3,e1),e3) = op(e3,op(e1,e3))& op(op(e3,e2),e0) = op(e3,op(e2,e0))& op(op(e3,e2),e1) = op(e3,op(e2,e1))& op(op(e3,e2),e2) = op(e3,op(e2,e2))& op(op(e3,e2),e3) = op(e3,op(e2,e3))& op(op(e3,e3),e0) = op(e3,op(e3,e0))& op(op(e3,e3),e1) = op(e3,op(e3,e1))& op(op(e3,e3),e2) = op(e3,op(e3,e2))& op(op(e3,e3),e3) = op(e3,op(e3,e3)) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f3,axiom,(
% 0.12/0.52 ( 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& ( unit = e0| unit = e1| unit = e2| unit = e3 ) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f4,axiom,(
% 0.12/0.52 ( op(e0,inv(e0)) = unit& op(inv(e0),e0) = unit& op(e1,inv(e1)) = unit& op(inv(e1),e1) = unit& op(e2,inv(e2)) = unit& op(inv(e2),e2) = unit& op(e3,inv(e3)) = unit& op(inv(e3),e3) = unit& ( inv(e0) = e0| inv(e0) = e1| inv(e0) = e2| inv(e0) = e3 )& ( inv(e1) = e0| inv(e1) = e1| inv(e1) = e2| inv(e1) = e3 )& ( inv(e2) = e0| inv(e2) = e1| inv(e2) = e2| inv(e2) = e3 )& ( inv(e3) = e0| inv(e3) = e1| inv(e3) = e2| inv(e3) = e3 ) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f5,axiom,(
% 0.12/0.52 inv(unit) = unit ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f6,axiom,(
% 0.12/0.52 ( inv(inv(e0)) = e0& inv(inv(e1)) = e1& inv(inv(e2)) = e2& inv(inv(e3)) = e3 ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f7,axiom,(
% 0.12/0.52 ( ( inv(e0) = e0=> inv(e0) = e0 )& ( inv(e0) = e1=> inv(e1) = e0 )& ( inv(e0) = e2=> inv(e2) = e0 )& ( inv(e0) = e3=> inv(e3) = e0 )& ( inv(e1) = e0=> inv(e0) = e1 )& ( inv(e1) = e1=> inv(e1) = e1 )& ( inv(e1) = e2=> inv(e2) = e1 )& ( inv(e1) = e3=> inv(e3) = e1 )& ( inv(e2) = e0=> inv(e0) = e2 )& ( inv(e2) = e1=> inv(e1) = e2 )& ( inv(e2) = e2=> inv(e2) = e2 )& ( inv(e2) = e3=> inv(e3) = e2 )& ( inv(e3) = e0=> inv(e0) = e3 )& ( inv(e3) = e1=> inv(e1) = e3 )& ( inv(e3) = e2=> inv(e2) = e3 )& ( inv(e3) = e3=> inv(e3) = e3 ) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f8,axiom,(
% 0.12/0.52 ( inv(e0) != inv(e1)& inv(e0) != inv(e2)& inv(e0) != inv(e3)& inv(e1) != inv(e2)& inv(e1) != inv(e3)& inv(e2) != inv(e3) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f9,axiom,(
% 0.12/0.52 ( op(e0,e0) != op(e1,e0)& op(e0,e0) != op(e2,e0)& op(e0,e0) != op(e3,e0)& op(e1,e0) != op(e2,e0)& op(e1,e0) != op(e3,e0)& op(e2,e0) != op(e3,e0)& op(e0,e1) != op(e1,e1)& op(e0,e1) != op(e2,e1)& op(e0,e1) != op(e3,e1)& op(e1,e1) != op(e2,e1)& op(e1,e1) != op(e3,e1)& op(e2,e1) != op(e3,e1)& op(e0,e2) != op(e1,e2)& op(e0,e2) != op(e2,e2)& op(e0,e2) != op(e3,e2)& op(e1,e2) != op(e2,e2)& op(e1,e2) != op(e3,e2)& op(e2,e2) != op(e3,e2)& op(e0,e3) != op(e1,e3)& op(e0,e3) != op(e2,e3)& op(e0,e3) != op(e3,e3)& op(e1,e3) != op(e2,e3)& op(e1,e3) != op(e3,e3)& op(e2,e3) != op(e3,e3)& op(e0,e0) != op(e0,e1)& op(e0,e0) != op(e0,e2)& op(e0,e0) != op(e0,e3)& op(e0,e1) != op(e0,e2)& op(e0,e1) != op(e0,e3)& op(e0,e2) != op(e0,e3)& op(e1,e0) != op(e1,e1)& op(e1,e0) != op(e1,e2)& op(e1,e0) != op(e1,e3)& op(e1,e1) != op(e1,e2)& op(e1,e1) != op(e1,e3)& op(e1,e2) != op(e1,e3)& op(e2,e0) != op(e2,e1)& op(e2,e0) != op(e2,e2)& op(e2,e0) != op(e2,e3)& op(e2,e1) != op(e2,e2)& op(e2,e1) != op(e2,e3)& op(e2,e2) != op(e2,e3)& op(e3,e0) != op(e3,e1)& op(e3,e0) != op(e3,e2)& op(e3,e0) != op(e3,e3)& op(e3,e1) != op(e3,e2)& op(e3,e1) != op(e3,e3)& op(e3,e2) != op(e3,e3) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f10,axiom,(
% 0.12/0.52 ( e0 != e1& e0 != e2& e0 != e3& e1 != e2& e1 != e3& e2 != e3 ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f11,axiom,(
% 0.12/0.52 ( ( op(e0,e0) = e0& op(e1,e1) = e0& op(e2,e2) = e0& op(e3,e3) = e0 )| ( op(e0,e0) = e1& op(e1,e1) = e1& op(e2,e2) = e1& op(e3,e3) = e1 )| ( op(e0,e0) = e2& op(e1,e1) = e2& op(e2,e2) = e2& op(e3,e3) = e2 )| ( op(e0,e0) = e3& op(e1,e1) = e3& op(e2,e2) = e3& op(e3,e3) = e3 ) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f16,axiom,(
% 0.12/0.52 ~ ( e0 = op(e2,e2)& e3 = op(e1,e2) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f17,axiom,(
% 0.12/0.52 ~ ( e0 = op(e1,e1)& e3 = op(e2,e1) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f19,axiom,(
% 0.12/0.52 ~ ( e1 = op(e2,e2)& e0 = op(e3,e2) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f26,axiom,(
% 0.12/0.52 ~ ( e2 = op(e3,e3)& e1 = op(e0,e3) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f30,axiom,(
% 0.12/0.52 ~ ( e3 = op(e2,e2)& e0 = op(e1,e2) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f33,axiom,(
% 0.12/0.52 ~ ( e3 = op(e0,e0)& e1 = op(e2,e0) ) ),
% 0.12/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.52 fof(f39,plain,(
% 0.12/0.52 op(e0,e3)=e0|op(e0,e3)=e1|op(e0,e3)=e2|op(e0,e3)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.52 fof(f42,plain,(
% 0.12/0.52 op(e1,e2)=e0|op(e1,e2)=e1|op(e1,e2)=e2|op(e1,e2)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.52 fof(f44,plain,(
% 0.12/0.52 op(e2,e0)=e0|op(e2,e0)=e1|op(e2,e0)=e2|op(e2,e0)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.52 fof(f45,plain,(
% 0.12/0.52 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.52 fof(f47,plain,(
% 0.12/0.52 op(e2,e3)=e0|op(e2,e3)=e1|op(e2,e3)=e2|op(e2,e3)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.52 fof(f50,plain,(
% 0.12/0.52 op(e3,e2)=e0|op(e3,e2)=e1|op(e3,e2)=e2|op(e3,e2)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.52 fof(f52,plain,(
% 0.12/0.52 op(op(e0,e0),e0)=op(e0,op(e0,e0))),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.52 fof(f54,plain,(
% 0.12/0.52 op(op(e0,e0),e2)=op(e0,op(e0,e2))),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.52 fof(f82,plain,(
% 0.12/0.52 op(op(e1,e3),e2)=op(e1,op(e3,e2))),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.52 fof(f114,plain,(
% 0.12/0.52 op(op(e3,e3),e2)=op(e3,op(e3,e2))),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.52 fof(f116,plain,(
% 0.12/0.52 op(unit,e0)=e0),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f117,plain,(
% 0.12/0.52 op(e0,unit)=e0),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f118,plain,(
% 0.12/0.52 op(unit,e1)=e1),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f119,plain,(
% 0.12/0.52 op(e1,unit)=e1),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f120,plain,(
% 0.12/0.52 op(unit,e2)=e2),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f121,plain,(
% 0.12/0.52 op(e2,unit)=e2),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f122,plain,(
% 0.12/0.52 op(unit,e3)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f123,plain,(
% 0.12/0.52 op(e3,unit)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f124,plain,(
% 0.12/0.52 unit=e0|unit=e1|unit=e2|unit=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.52 fof(f130,plain,(
% 0.12/0.52 op(inv(e2),e2)=unit),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.52 fof(f132,plain,(
% 0.12/0.52 op(inv(e3),e3)=unit),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.52 fof(f133,plain,(
% 0.12/0.52 inv(e0)=e0|inv(e0)=e1|inv(e0)=e2|inv(e0)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.52 fof(f137,plain,(
% 0.12/0.52 inv(unit)=unit),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.52 fof(f139,plain,(
% 0.12/0.52 inv(inv(e1))=e1),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.52 fof(f142,plain,(
% 0.12/0.52 (((((((((((((((~inv(e0)=e0|inv(e0)=e0)&(~inv(e0)=e1|inv(e1)=e0))&(~inv(e0)=e2|inv(e2)=e0))&(~inv(e0)=e3|inv(e3)=e0))&(~inv(e1)=e0|inv(e0)=e1))&(~inv(e1)=e1|inv(e1)=e1))&(~inv(e1)=e2|inv(e2)=e1))&(~inv(e1)=e3|inv(e3)=e1))&(~inv(e2)=e0|inv(e0)=e2))&(~inv(e2)=e1|inv(e1)=e2))&(~inv(e2)=e2|inv(e2)=e2))&(~inv(e2)=e3|inv(e3)=e2))&(~inv(e3)=e0|inv(e0)=e3))&(~inv(e3)=e1|inv(e1)=e3))&(~inv(e3)=e2|inv(e2)=e3))&(~inv(e3)=e3|inv(e3)=e3)),
% 0.12/0.52 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.12/0.52 fof(f144,plain,(
% 0.12/0.52 ~inv(e0)=e1|inv(e1)=e0),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f142])).
% 0.12/0.52 fof(f145,plain,(
% 0.12/0.52 ~inv(e0)=e2|inv(e2)=e0),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f142])).
% 0.12/0.52 fof(f146,plain,(
% 0.12/0.52 ~inv(e0)=e3|inv(e3)=e0),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f142])).
% 0.12/0.52 fof(f149,plain,(
% 0.12/0.52 ~inv(e1)=e2|inv(e2)=e1),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f142])).
% 0.12/0.52 fof(f156,plain,(
% 0.12/0.52 ~inv(e3)=e1|inv(e1)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f142])).
% 0.12/0.52 fof(f157,plain,(
% 0.12/0.52 ~inv(e3)=e2|inv(e2)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f142])).
% 0.12/0.52 fof(f160,plain,(
% 0.12/0.52 ~inv(e0)=inv(e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.52 fof(f163,plain,(
% 0.12/0.52 ~inv(e1)=inv(e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.52 fof(f165,plain,(
% 0.12/0.52 ~op(e0,e0)=op(e1,e0)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f166,plain,(
% 0.12/0.52 ~op(e0,e0)=op(e2,e0)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f168,plain,(
% 0.12/0.52 ~op(e1,e0)=op(e2,e0)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f169,plain,(
% 0.12/0.52 ~op(e1,e0)=op(e3,e0)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f170,plain,(
% 0.12/0.52 ~op(e2,e0)=op(e3,e0)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f172,plain,(
% 0.12/0.52 ~op(e0,e1)=op(e2,e1)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f173,plain,(
% 0.12/0.52 ~op(e0,e1)=op(e3,e1)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f174,plain,(
% 0.12/0.52 ~op(e1,e1)=op(e2,e1)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f176,plain,(
% 0.12/0.52 ~op(e2,e1)=op(e3,e1)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f179,plain,(
% 0.12/0.52 ~op(e0,e2)=op(e3,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f180,plain,(
% 0.12/0.52 ~op(e1,e2)=op(e2,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f181,plain,(
% 0.12/0.52 ~op(e1,e2)=op(e3,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f182,plain,(
% 0.12/0.52 ~op(e2,e2)=op(e3,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f184,plain,(
% 0.12/0.52 ~op(e0,e3)=op(e2,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f185,plain,(
% 0.12/0.52 ~op(e0,e3)=op(e3,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f186,plain,(
% 0.12/0.52 ~op(e1,e3)=op(e2,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f190,plain,(
% 0.12/0.52 ~op(e0,e0)=op(e0,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f191,plain,(
% 0.12/0.52 ~op(e0,e0)=op(e0,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f192,plain,(
% 0.12/0.52 ~op(e0,e1)=op(e0,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f193,plain,(
% 0.12/0.52 ~op(e0,e1)=op(e0,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f194,plain,(
% 0.12/0.52 ~op(e0,e2)=op(e0,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f195,plain,(
% 0.12/0.52 ~op(e1,e0)=op(e1,e1)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f196,plain,(
% 0.12/0.52 ~op(e1,e0)=op(e1,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f199,plain,(
% 0.12/0.52 ~op(e1,e1)=op(e1,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f200,plain,(
% 0.12/0.52 ~op(e1,e2)=op(e1,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f201,plain,(
% 0.12/0.52 ~op(e2,e0)=op(e2,e1)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f203,plain,(
% 0.12/0.52 ~op(e2,e0)=op(e2,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f204,plain,(
% 0.12/0.52 ~op(e2,e1)=op(e2,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f205,plain,(
% 0.12/0.52 ~op(e2,e1)=op(e2,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f206,plain,(
% 0.12/0.52 ~op(e2,e2)=op(e2,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f207,plain,(
% 0.12/0.52 ~op(e3,e0)=op(e3,e1)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f209,plain,(
% 0.12/0.52 ~op(e3,e0)=op(e3,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f210,plain,(
% 0.12/0.52 ~op(e3,e1)=op(e3,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f211,plain,(
% 0.12/0.52 ~op(e3,e1)=op(e3,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f212,plain,(
% 0.12/0.52 ~op(e3,e2)=op(e3,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.52 fof(f213,plain,(
% 0.12/0.52 ~e0=e1),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.52 fof(f214,plain,(
% 0.12/0.52 ~e0=e2),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.52 fof(f215,plain,(
% 0.12/0.52 ~e0=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.52 fof(f216,plain,(
% 0.12/0.52 ~e1=e2),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.52 fof(f217,plain,(
% 0.12/0.52 ~e1=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.52 fof(f218,plain,(
% 0.12/0.52 ~e2=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.52 fof(f219,definition,(
% 0.12/0.52 sP0_prd<=>(((((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0)|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1))|(((op(e0,e0)=e2&op(e1,e1)=e2)&op(e2,e2)=e2)&op(e3,e3)=e2))),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/0.52 fof(f220,plain,(
% 0.12/0.52 sP0_prd|(((op(e0,e0)=e3&op(e1,e1)=e3)&op(e2,e2)=e3)&op(e3,e3)=e3)),
% 0.12/0.52 inference(formula_renaming,[status(thm)],[f11,f219])).
% 0.12/0.52 fof(f221,plain,(
% 0.12/0.52 sP0_prd|op(e0,e0)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f220])).
% 0.12/0.52 fof(f222,plain,(
% 0.12/0.52 sP0_prd|op(e1,e1)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f220])).
% 0.12/0.52 fof(f223,plain,(
% 0.12/0.52 sP0_prd|op(e2,e2)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f220])).
% 0.12/0.52 fof(f224,plain,(
% 0.12/0.52 sP0_prd|op(e3,e3)=e3),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f220])).
% 0.12/0.52 fof(f233,plain,(
% 0.12/0.52 (~e0=op(e2,e2)|~e3=op(e1,e2))),
% 0.12/0.52 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.12/0.52 fof(f234,plain,(
% 0.12/0.52 ~e0=op(e2,e2)|~e3=op(e1,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f233])).
% 0.12/0.52 fof(f235,plain,(
% 0.12/0.52 (~e0=op(e1,e1)|~e3=op(e2,e1))),
% 0.12/0.52 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.12/0.52 fof(f236,plain,(
% 0.12/0.52 ~e0=op(e1,e1)|~e3=op(e2,e1)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f235])).
% 0.12/0.52 fof(f239,plain,(
% 0.12/0.52 (~e1=op(e2,e2)|~e0=op(e3,e2))),
% 0.12/0.52 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.12/0.52 fof(f240,plain,(
% 0.12/0.52 ~e1=op(e2,e2)|~e0=op(e3,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f239])).
% 0.12/0.52 fof(f253,plain,(
% 0.12/0.52 (~e2=op(e3,e3)|~e1=op(e0,e3))),
% 0.12/0.52 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.12/0.52 fof(f254,plain,(
% 0.12/0.52 ~e2=op(e3,e3)|~e1=op(e0,e3)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f253])).
% 0.12/0.52 fof(f261,plain,(
% 0.12/0.52 (~e3=op(e2,e2)|~e0=op(e1,e2))),
% 0.12/0.52 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.12/0.52 fof(f262,plain,(
% 0.12/0.52 ~e3=op(e2,e2)|~e0=op(e1,e2)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f261])).
% 0.12/0.52 fof(f267,plain,(
% 0.12/0.52 (~e3=op(e0,e0)|~e1=op(e2,e0))),
% 0.12/0.52 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.12/0.52 fof(f268,plain,(
% 0.12/0.52 ~e3=op(e0,e0)|~e1=op(e2,e0)),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f267])).
% 0.12/0.52 fof(f273,definition,(
% 0.12/0.52 sP1_prd<=>((((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0)|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1))),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.12/0.52 fof(f274,plain,(
% 0.12/0.52 sP0_prd<=>(sP1_prd|(((op(e0,e0)=e2&op(e1,e1)=e2)&op(e2,e2)=e2)&op(e3,e3)=e2))),
% 0.12/0.52 inference(formula_renaming,[status(thm)],[f219,f273])).
% 0.12/0.52 fof(f275,plain,(
% 0.12/0.52 (~sP0_prd|(sP1_prd|(((op(e0,e0)=e2&op(e1,e1)=e2)&op(e2,e2)=e2)&op(e3,e3)=e2)))&(sP0_prd|(~sP1_prd&(((~op(e0,e0)=e2|~op(e1,e1)=e2)|~op(e2,e2)=e2)|~op(e3,e3)=e2)))),
% 0.12/0.52 inference(NNF_transformation,[status(thm)],[f274])).
% 0.12/0.52 fof(f276,plain,(
% 0.12/0.52 ~sP0_prd|sP1_prd|op(e0,e0)=e2),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f275])).
% 0.12/0.52 fof(f278,plain,(
% 0.12/0.52 ~sP0_prd|sP1_prd|op(e2,e2)=e2),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f275])).
% 0.12/0.52 fof(f279,plain,(
% 0.12/0.52 ~sP0_prd|sP1_prd|op(e3,e3)=e2),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f275])).
% 0.12/0.52 fof(f282,definition,(
% 0.12/0.52 sP2_prd<=>(((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.12/0.52 fof(f283,plain,(
% 0.12/0.52 sP1_prd<=>(sP2_prd|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1))),
% 0.12/0.52 inference(formula_renaming,[status(thm)],[f273,f282])).
% 0.12/0.52 fof(f284,plain,(
% 0.12/0.52 (~sP1_prd|(sP2_prd|(((op(e0,e0)=e1&op(e1,e1)=e1)&op(e2,e2)=e1)&op(e3,e3)=e1)))&(sP1_prd|(~sP2_prd&(((~op(e0,e0)=e1|~op(e1,e1)=e1)|~op(e2,e2)=e1)|~op(e3,e3)=e1)))),
% 0.12/0.52 inference(NNF_transformation,[status(thm)],[f283])).
% 0.12/0.52 fof(f286,plain,(
% 0.12/0.52 ~sP1_prd|sP2_prd|op(e1,e1)=e1),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f284])).
% 0.12/0.52 fof(f287,plain,(
% 0.12/0.52 ~sP1_prd|sP2_prd|op(e2,e2)=e1),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f284])).
% 0.12/0.52 fof(f291,plain,(
% 0.12/0.52 (~sP2_prd|(((op(e0,e0)=e0&op(e1,e1)=e0)&op(e2,e2)=e0)&op(e3,e3)=e0))&(sP2_prd|(((~op(e0,e0)=e0|~op(e1,e1)=e0)|~op(e2,e2)=e0)|~op(e3,e3)=e0))),
% 0.12/0.52 inference(NNF_transformation,[status(thm)],[f282])).
% 0.12/0.52 fof(f292,plain,(
% 0.12/0.52 ~sP2_prd|op(e0,e0)=e0),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f291])).
% 0.12/0.52 fof(f293,plain,(
% 0.12/0.52 ~sP2_prd|op(e1,e1)=e0),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f291])).
% 0.12/0.52 fof(f294,plain,(
% 0.12/0.52 ~sP2_prd|op(e2,e2)=e0),
% 0.12/0.52 inference(cnf_transformation,[status(thm)],[f291])).
% 0.12/0.52 fof(f297,definition,(
% 0.12/0.52 sQ0_spl <=> (op(e0,e0)=e0)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f298,plain,(
% 0.12/0.52 op(e0,e0)=e0|~sQ0_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f297])).
% 0.12/0.52 fof(f303,definition,(
% 0.12/0.52 sQ2_spl <=> (op(e0,e0)=e2)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f304,plain,(
% 0.12/0.52 op(e0,e0)=e2|~sQ2_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f303])).
% 0.12/0.52 fof(f306,definition,(
% 0.12/0.52 sQ3_spl <=> (op(e0,e0)=e3)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f307,plain,(
% 0.12/0.52 op(e0,e0)=e3|~sQ3_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f306])).
% 0.12/0.52 fof(f310,definition,(
% 0.12/0.52 sQ4_spl <=> (op(e0,e1)=e0)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f311,plain,(
% 0.12/0.52 op(e0,e1)=e0|~sQ4_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f310])).
% 0.12/0.52 fof(f313,definition,(
% 0.12/0.52 sQ5_spl <=> (op(e0,e1)=e1)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f323,definition,(
% 0.12/0.52 sQ8_spl <=> (op(e0,e2)=e0)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f324,plain,(
% 0.12/0.52 op(e0,e2)=e0|~sQ8_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f323])).
% 0.12/0.52 fof(f326,definition,(
% 0.12/0.52 sQ9_spl <=> (op(e0,e2)=e1)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f327,plain,(
% 0.12/0.52 op(e0,e2)=e1|~sQ9_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f326])).
% 0.12/0.52 fof(f329,definition,(
% 0.12/0.52 sQ10_spl <=> (op(e0,e2)=e2)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f330,plain,(
% 0.12/0.52 op(e0,e2)=e2|~sQ10_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f329])).
% 0.12/0.52 fof(f336,definition,(
% 0.12/0.52 sQ12_spl <=> (op(e0,e3)=e0)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f339,definition,(
% 0.12/0.52 sQ13_spl <=> (op(e0,e3)=e1)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f342,definition,(
% 0.12/0.52 sQ14_spl <=> (op(e0,e3)=e2)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f345,definition,(
% 0.12/0.52 sQ15_spl <=> (op(e0,e3)=e3)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f348,plain,(
% 0.12/0.52 sQ12_spl|sQ13_spl|sQ14_spl|sQ15_spl),
% 0.12/0.52 inference(split_clause,[status(thm)],[f39,f336,f339,f342,f345])).
% 0.12/0.52 fof(f349,definition,(
% 0.12/0.52 sQ16_spl <=> (op(e1,e0)=e0)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f362,definition,(
% 0.12/0.52 sQ20_spl <=> (op(e1,e1)=e0)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f365,definition,(
% 0.12/0.52 sQ21_spl <=> (op(e1,e1)=e1)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f366,plain,(
% 0.12/0.52 op(e1,e1)=e1|~sQ21_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f365])).
% 0.12/0.52 fof(f371,definition,(
% 0.12/0.52 sQ23_spl <=> (op(e1,e1)=e3)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f372,plain,(
% 0.12/0.52 op(e1,e1)=e3|~sQ23_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f371])).
% 0.12/0.52 fof(f375,definition,(
% 0.12/0.52 sQ24_spl <=> (op(e1,e2)=e0)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f378,definition,(
% 0.12/0.52 sQ25_spl <=> (op(e1,e2)=e1)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f379,plain,(
% 0.12/0.52 op(e1,e2)=e1|~sQ25_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f378])).
% 0.12/0.52 fof(f381,definition,(
% 0.12/0.52 sQ26_spl <=> (op(e1,e2)=e2)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f382,plain,(
% 0.12/0.52 op(e1,e2)=e2|~sQ26_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f381])).
% 0.12/0.52 fof(f384,definition,(
% 0.12/0.52 sQ27_spl <=> (op(e1,e2)=e3)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f387,plain,(
% 0.12/0.52 sQ24_spl|sQ25_spl|sQ26_spl|sQ27_spl),
% 0.12/0.52 inference(split_clause,[status(thm)],[f42,f375,f378,f381,f384])).
% 0.12/0.52 fof(f391,definition,(
% 0.12/0.52 sQ29_spl <=> (op(e1,e3)=e1)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.52 fof(f392,plain,(
% 0.12/0.52 op(e1,e3)=e1|~sQ29_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f391])).
% 0.12/0.52 fof(f393,plain,(
% 0.12/0.52 ~op(e1,e3)=e1|sQ29_spl),
% 0.12/0.52 inference(component_clause,[status(thm)],[f391])).
% 0.12/0.52 fof(f394,definition,(
% 0.12/0.52 sQ30_spl <=> (op(e1,e3)=e2)),
% 0.12/0.52 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f397,definition,(
% 0.12/0.53 sQ31_spl <=> (op(e1,e3)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f398,plain,(
% 0.12/0.53 op(e1,e3)=e3|~sQ31_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f397])).
% 0.12/0.53 fof(f401,definition,(
% 0.12/0.53 sQ32_spl <=> (op(e2,e0)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f402,plain,(
% 0.12/0.53 op(e2,e0)=e0|~sQ32_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f401])).
% 0.12/0.53 fof(f404,definition,(
% 0.12/0.53 sQ33_spl <=> (op(e2,e0)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f407,definition,(
% 0.12/0.53 sQ34_spl <=> (op(e2,e0)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f408,plain,(
% 0.12/0.53 op(e2,e0)=e2|~sQ34_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f407])).
% 0.12/0.53 fof(f410,definition,(
% 0.12/0.53 sQ35_spl <=> (op(e2,e0)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f413,plain,(
% 0.12/0.53 sQ32_spl|sQ33_spl|sQ34_spl|sQ35_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f44,f401,f404,f407,f410])).
% 0.12/0.53 fof(f414,definition,(
% 0.12/0.53 sQ36_spl <=> (op(e2,e1)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f415,plain,(
% 0.12/0.53 op(e2,e1)=e0|~sQ36_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f414])).
% 0.12/0.53 fof(f417,definition,(
% 0.12/0.53 sQ37_spl <=> (op(e2,e1)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f418,plain,(
% 0.12/0.53 op(e2,e1)=e1|~sQ37_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f417])).
% 0.12/0.53 fof(f420,definition,(
% 0.12/0.53 sQ38_spl <=> (op(e2,e1)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f421,plain,(
% 0.12/0.53 op(e2,e1)=e2|~sQ38_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f420])).
% 0.12/0.53 fof(f423,definition,(
% 0.12/0.53 sQ39_spl <=> (op(e2,e1)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f426,plain,(
% 0.12/0.53 sQ36_spl|sQ37_spl|sQ38_spl|sQ39_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f45,f414,f417,f420,f423])).
% 0.12/0.53 fof(f427,definition,(
% 0.12/0.53 sQ40_spl <=> (op(e2,e2)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f430,definition,(
% 0.12/0.53 sQ41_spl <=> (op(e2,e2)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f433,definition,(
% 0.12/0.53 sQ42_spl <=> (op(e2,e2)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f434,plain,(
% 0.12/0.53 op(e2,e2)=e2|~sQ42_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f433])).
% 0.12/0.53 fof(f436,definition,(
% 0.12/0.53 sQ43_spl <=> (op(e2,e2)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f440,definition,(
% 0.12/0.53 sQ44_spl <=> (op(e2,e3)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f443,definition,(
% 0.12/0.53 sQ45_spl <=> (op(e2,e3)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f446,definition,(
% 0.12/0.53 sQ46_spl <=> (op(e2,e3)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f447,plain,(
% 0.12/0.53 op(e2,e3)=e2|~sQ46_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f446])).
% 0.12/0.53 fof(f449,definition,(
% 0.12/0.53 sQ47_spl <=> (op(e2,e3)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f450,plain,(
% 0.12/0.53 op(e2,e3)=e3|~sQ47_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f449])).
% 0.12/0.53 fof(f452,plain,(
% 0.12/0.53 sQ44_spl|sQ45_spl|sQ46_spl|sQ47_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f47,f440,f443,f446,f449])).
% 0.12/0.53 fof(f453,definition,(
% 0.12/0.53 sQ48_spl <=> (op(e3,e0)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f454,plain,(
% 0.12/0.53 op(e3,e0)=e0|~sQ48_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f453])).
% 0.12/0.53 fof(f455,plain,(
% 0.12/0.53 ~op(e3,e0)=e0|sQ48_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f453])).
% 0.12/0.53 fof(f456,definition,(
% 0.12/0.53 sQ49_spl <=> (op(e3,e0)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f462,definition,(
% 0.12/0.53 sQ51_spl <=> (op(e3,e0)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f469,definition,(
% 0.12/0.53 sQ53_spl <=> (op(e3,e1)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f471,plain,(
% 0.12/0.53 ~op(e3,e1)=e1|sQ53_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f469])).
% 0.12/0.53 fof(f475,definition,(
% 0.12/0.53 sQ55_spl <=> (op(e3,e1)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f479,definition,(
% 0.12/0.53 sQ56_spl <=> (op(e3,e2)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f480,plain,(
% 0.12/0.53 op(e3,e2)=e0|~sQ56_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f479])).
% 0.12/0.53 fof(f482,definition,(
% 0.12/0.53 sQ57_spl <=> (op(e3,e2)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f483,plain,(
% 0.12/0.53 op(e3,e2)=e1|~sQ57_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f482])).
% 0.12/0.53 fof(f485,definition,(
% 0.12/0.53 sQ58_spl <=> (op(e3,e2)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f488,definition,(
% 0.12/0.53 sQ59_spl <=> (op(e3,e2)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f489,plain,(
% 0.12/0.53 op(e3,e2)=e3|~sQ59_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f488])).
% 0.12/0.53 fof(f490,plain,(
% 0.12/0.53 ~op(e3,e2)=e3|sQ59_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f488])).
% 0.12/0.53 fof(f491,plain,(
% 0.12/0.53 sQ56_spl|sQ57_spl|sQ58_spl|sQ59_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f50,f479,f482,f485,f488])).
% 0.12/0.53 fof(f498,definition,(
% 0.12/0.53 sQ62_spl <=> (op(e3,e3)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f501,definition,(
% 0.12/0.53 sQ63_spl <=> (op(e3,e3)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f502,plain,(
% 0.12/0.53 op(e3,e3)=e3|~sQ63_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f501])).
% 0.12/0.53 fof(f505,definition,(
% 0.12/0.53 sQ64_spl <=> (unit=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f506,plain,(
% 0.12/0.53 unit=e0|~sQ64_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f505])).
% 0.12/0.53 fof(f508,definition,(
% 0.12/0.53 sQ65_spl <=> (unit=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f509,plain,(
% 0.12/0.53 unit=e1|~sQ65_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f508])).
% 0.12/0.53 fof(f511,definition,(
% 0.12/0.53 sQ66_spl <=> (unit=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f512,plain,(
% 0.12/0.53 unit=e2|~sQ66_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f511])).
% 0.12/0.53 fof(f514,definition,(
% 0.12/0.53 sQ67_spl <=> (unit=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f515,plain,(
% 0.12/0.53 unit=e3|~sQ67_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f514])).
% 0.12/0.53 fof(f517,plain,(
% 0.12/0.53 sQ64_spl|sQ65_spl|sQ66_spl|sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f124,f505,f508,f511,f514])).
% 0.12/0.53 fof(f518,definition,(
% 0.12/0.53 sQ68_spl <=> (inv(e0)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f519,plain,(
% 0.12/0.53 inv(e0)=e0|~sQ68_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f518])).
% 0.12/0.53 fof(f521,definition,(
% 0.12/0.53 sQ69_spl <=> (inv(e0)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f524,definition,(
% 0.12/0.53 sQ70_spl <=> (inv(e0)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f527,definition,(
% 0.12/0.53 sQ71_spl <=> (inv(e0)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f528,plain,(
% 0.12/0.53 inv(e0)=e3|~sQ71_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f527])).
% 0.12/0.53 fof(f530,plain,(
% 0.12/0.53 sQ68_spl|sQ69_spl|sQ70_spl|sQ71_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f133,f518,f521,f524,f527])).
% 0.12/0.53 fof(f531,definition,(
% 0.12/0.53 sQ72_spl <=> (inv(e1)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f532,plain,(
% 0.12/0.53 inv(e1)=e0|~sQ72_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f531])).
% 0.12/0.53 fof(f537,definition,(
% 0.12/0.53 sQ74_spl <=> (inv(e1)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f540,definition,(
% 0.12/0.53 sQ75_spl <=> (inv(e1)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f544,definition,(
% 0.12/0.53 sQ76_spl <=> (inv(e2)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f545,plain,(
% 0.12/0.53 inv(e2)=e0|~sQ76_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f544])).
% 0.12/0.53 fof(f547,definition,(
% 0.12/0.53 sQ77_spl <=> (inv(e2)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f548,plain,(
% 0.12/0.53 inv(e2)=e1|~sQ77_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f547])).
% 0.12/0.53 fof(f550,definition,(
% 0.12/0.53 sQ78_spl <=> (inv(e2)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f551,plain,(
% 0.12/0.53 inv(e2)=e2|~sQ78_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f550])).
% 0.12/0.53 fof(f553,definition,(
% 0.12/0.53 sQ79_spl <=> (inv(e2)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f554,plain,(
% 0.12/0.53 inv(e2)=e3|~sQ79_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f553])).
% 0.12/0.53 fof(f557,definition,(
% 0.12/0.53 sQ80_spl <=> (inv(e3)=e0)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f558,plain,(
% 0.12/0.53 inv(e3)=e0|~sQ80_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f557])).
% 0.12/0.53 fof(f560,definition,(
% 0.12/0.53 sQ81_spl <=> (inv(e3)=e1)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f563,definition,(
% 0.12/0.53 sQ82_spl <=> (inv(e3)=e2)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f566,definition,(
% 0.12/0.53 sQ83_spl <=> (inv(e3)=e3)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f567,plain,(
% 0.12/0.53 inv(e3)=e3|~sQ83_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f566])).
% 0.12/0.53 fof(f568,plain,(
% 0.12/0.53 ~inv(e3)=e3|sQ83_spl),
% 0.12/0.53 inference(component_clause,[status(thm)],[f566])).
% 0.12/0.53 fof(f571,plain,(
% 0.12/0.53 ~sQ69_spl|sQ72_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f144,f521,f531])).
% 0.12/0.53 fof(f572,plain,(
% 0.12/0.53 ~sQ70_spl|sQ76_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f145,f524,f544])).
% 0.12/0.53 fof(f573,plain,(
% 0.12/0.53 ~sQ71_spl|sQ80_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f146,f527,f557])).
% 0.12/0.53 fof(f576,plain,(
% 0.12/0.53 ~sQ74_spl|sQ77_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f149,f537,f547])).
% 0.12/0.53 fof(f583,plain,(
% 0.12/0.53 ~sQ81_spl|sQ75_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f156,f560,f540])).
% 0.12/0.53 fof(f584,plain,(
% 0.12/0.53 ~sQ82_spl|sQ79_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f157,f563,f553])).
% 0.12/0.53 fof(f586,definition,(
% 0.12/0.53 sQ84_spl <=> (sP0_prd)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f589,plain,(
% 0.12/0.53 sQ84_spl|sQ3_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f221,f586,f306])).
% 0.12/0.53 fof(f590,plain,(
% 0.12/0.53 sQ84_spl|sQ23_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f222,f586,f371])).
% 0.12/0.53 fof(f591,plain,(
% 0.12/0.53 sQ84_spl|sQ43_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f223,f586,f436])).
% 0.12/0.53 fof(f592,plain,(
% 0.12/0.53 sQ84_spl|sQ63_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f224,f586,f501])).
% 0.12/0.53 fof(f597,plain,(
% 0.12/0.53 ~sQ40_spl|~sQ27_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f234,f427,f384])).
% 0.12/0.53 fof(f598,plain,(
% 0.12/0.53 ~sQ20_spl|~sQ39_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f236,f362,f423])).
% 0.12/0.53 fof(f600,plain,(
% 0.12/0.53 ~sQ41_spl|~sQ56_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f240,f430,f479])).
% 0.12/0.53 fof(f607,plain,(
% 0.12/0.53 ~sQ62_spl|~sQ13_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f254,f498,f339])).
% 0.12/0.53 fof(f611,plain,(
% 0.12/0.53 ~sQ43_spl|~sQ24_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f262,f436,f375])).
% 0.12/0.53 fof(f614,plain,(
% 0.12/0.53 ~sQ3_spl|~sQ33_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f268,f306,f404])).
% 0.12/0.53 fof(f617,definition,(
% 0.12/0.53 sQ85_spl <=> (sP1_prd)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f620,plain,(
% 0.12/0.53 ~sQ84_spl|sQ85_spl|sQ2_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f276,f586,f617,f303])).
% 0.12/0.53 fof(f622,plain,(
% 0.12/0.53 ~sQ84_spl|sQ85_spl|sQ42_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f278,f586,f617,f433])).
% 0.12/0.53 fof(f623,plain,(
% 0.12/0.53 ~sQ84_spl|sQ85_spl|sQ62_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f279,f586,f617,f498])).
% 0.12/0.53 fof(f626,definition,(
% 0.12/0.53 sQ86_spl <=> (sP2_prd)),
% 0.12/0.53 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.12/0.53 fof(f630,plain,(
% 0.12/0.53 ~sQ85_spl|sQ86_spl|sQ21_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f286,f617,f626,f365])).
% 0.12/0.53 fof(f631,plain,(
% 0.12/0.53 ~sQ85_spl|sQ86_spl|sQ41_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f287,f617,f626,f430])).
% 0.12/0.53 fof(f635,plain,(
% 0.12/0.53 ~sQ86_spl|sQ0_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f292,f626,f297])).
% 0.12/0.53 fof(f636,plain,(
% 0.12/0.53 ~sQ86_spl|sQ20_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f293,f626,f362])).
% 0.12/0.53 fof(f637,plain,(
% 0.12/0.53 ~sQ86_spl|sQ40_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f294,f626,f427])).
% 0.12/0.53 fof(f640,plain,(
% 0.12/0.53 e2=e3|~sQ66_spl|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f512,f515])).
% 0.12/0.53 fof(f641,plain,(
% 0.12/0.53 $false|~sQ66_spl|~sQ67_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f640,f218])).
% 0.12/0.53 fof(f642,plain,(
% 0.12/0.53 ~sQ66_spl|~sQ67_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f641])).
% 0.12/0.53 fof(f654,plain,(
% 0.12/0.53 e0=e3|~sQ80_spl|~sQ83_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f558,f567])).
% 0.12/0.53 fof(f655,plain,(
% 0.12/0.53 $false|~sQ80_spl|~sQ83_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f654,f215])).
% 0.12/0.53 fof(f656,plain,(
% 0.12/0.53 ~sQ80_spl|~sQ83_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f655])).
% 0.12/0.53 fof(f665,plain,(
% 0.12/0.53 e0=e2|~sQ76_spl|~sQ78_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f545,f551])).
% 0.12/0.53 fof(f666,plain,(
% 0.12/0.53 $false|~sQ76_spl|~sQ78_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f665,f214])).
% 0.12/0.53 fof(f667,plain,(
% 0.12/0.53 ~sQ76_spl|~sQ78_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f666])).
% 0.12/0.53 fof(f686,plain,(
% 0.12/0.53 op(e0,e1)=e1|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f118])).
% 0.12/0.53 fof(f699,plain,(
% 0.12/0.53 op(e0,e2)=e2|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f120])).
% 0.12/0.53 fof(f711,plain,(
% 0.12/0.53 op(e0,e3)=e3|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f122])).
% 0.12/0.53 fof(f723,plain,(
% 0.12/0.53 inv(e0)=unit|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f137])).
% 0.12/0.53 fof(f724,plain,(
% 0.12/0.53 inv(e0)=e0|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f723])).
% 0.12/0.53 fof(f736,plain,(
% 0.12/0.53 inv(e0)=e1|~sQ72_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f532,f139])).
% 0.12/0.53 fof(f740,plain,(
% 0.12/0.53 e0=e1|~sQ64_spl|~sQ72_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f724,f736])).
% 0.12/0.53 fof(f741,plain,(
% 0.12/0.53 $false|~sQ64_spl|~sQ72_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f740,f213])).
% 0.12/0.53 fof(f742,plain,(
% 0.12/0.53 ~sQ64_spl|~sQ72_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f741])).
% 0.12/0.53 fof(f775,plain,(
% 0.12/0.53 inv(e2)=unit|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f137])).
% 0.12/0.53 fof(f776,plain,(
% 0.12/0.53 e1=e2|~sQ77_spl|~sQ66_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f777,f512])).
% 0.12/0.53 fof(f777,plain,(
% 0.12/0.53 e1=unit|~sQ77_spl|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f548,f775])).
% 0.12/0.53 fof(f778,plain,(
% 0.12/0.53 $false|~sQ77_spl|~sQ66_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f776,f216])).
% 0.12/0.53 fof(f779,plain,(
% 0.12/0.53 ~sQ77_spl|~sQ66_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f778])).
% 0.12/0.53 fof(f786,plain,(
% 0.12/0.53 ~op(e3,e2)=e3|~sQ63_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f502,f212])).
% 0.12/0.53 fof(f787,plain,(
% 0.12/0.53 ~op(e3,e1)=e3|~sQ63_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f502,f211])).
% 0.12/0.53 fof(f788,plain,(
% 0.12/0.53 ~op(e3,e0)=e3|~sQ63_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f502,f209])).
% 0.12/0.53 fof(f791,plain,(
% 0.12/0.53 ~op(e0,e3)=e3|~sQ63_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f502,f185])).
% 0.12/0.53 fof(f797,plain,(
% 0.12/0.53 ~e1=op(e1,e3)|~sQ25_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f379,f200])).
% 0.12/0.53 fof(f810,plain,(
% 0.12/0.53 ~e1=op(e2,e3)|~sQ37_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f418,f205])).
% 0.12/0.53 fof(f811,plain,(
% 0.12/0.53 ~e1=op(e2,e2)|~sQ37_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f418,f204])).
% 0.12/0.53 fof(f812,plain,(
% 0.12/0.53 ~op(e2,e0)=e1|~sQ37_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f418,f201])).
% 0.12/0.53 fof(f813,plain,(
% 0.12/0.53 ~e1=op(e3,e1)|~sQ37_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f418,f176])).
% 0.12/0.53 fof(f814,plain,(
% 0.12/0.53 ~op(e1,e1)=e1|~sQ37_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f418,f174])).
% 0.12/0.53 fof(f815,plain,(
% 0.12/0.53 ~op(e0,e1)=e1|~sQ37_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f418,f172])).
% 0.12/0.53 fof(f821,plain,(
% 0.12/0.53 ~op(e3,e1)=e3|~sQ59_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f489,f210])).
% 0.12/0.53 fof(f833,plain,(
% 0.12/0.53 inv(e0)=unit|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f137])).
% 0.12/0.53 fof(f834,plain,(
% 0.12/0.53 e3=unit|~sQ71_spl|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f528,f833])).
% 0.12/0.53 fof(f835,plain,(
% 0.12/0.53 e3=e0|~sQ71_spl|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f834])).
% 0.12/0.53 fof(f836,plain,(
% 0.12/0.53 $false|~sQ71_spl|~sQ64_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f835,f215])).
% 0.12/0.53 fof(f837,plain,(
% 0.12/0.53 ~sQ71_spl|~sQ64_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f836])).
% 0.12/0.53 fof(f861,plain,(
% 0.12/0.53 ~op(e1,e3)=e3|~sQ47_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f450,f186])).
% 0.12/0.53 fof(f862,plain,(
% 0.12/0.53 ~op(e0,e3)=e3|~sQ47_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f450,f184])).
% 0.12/0.53 fof(f865,plain,(
% 0.12/0.53 e2=e3|~sQ46_spl|~sQ47_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f447,f450])).
% 0.12/0.53 fof(f866,plain,(
% 0.12/0.53 $false|~sQ46_spl|~sQ47_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f865,f218])).
% 0.12/0.53 fof(f867,plain,(
% 0.12/0.53 ~sQ46_spl|~sQ47_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f866])).
% 0.12/0.53 fof(f868,plain,(
% 0.12/0.53 e1=e2|~sQ37_spl|~sQ38_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f418,f421])).
% 0.12/0.53 fof(f869,plain,(
% 0.12/0.53 $false|~sQ37_spl|~sQ38_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f868,f216])).
% 0.12/0.53 fof(f870,plain,(
% 0.12/0.53 ~sQ37_spl|~sQ38_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f869])).
% 0.12/0.53 fof(f876,plain,(
% 0.12/0.53 e0=e2|~sQ32_spl|~sQ34_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f402,f408])).
% 0.12/0.53 fof(f877,plain,(
% 0.12/0.53 $false|~sQ32_spl|~sQ34_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f876,f214])).
% 0.12/0.53 fof(f878,plain,(
% 0.12/0.53 ~sQ32_spl|~sQ34_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f877])).
% 0.12/0.53 fof(f886,plain,(
% 0.12/0.53 e1=e3|~sQ29_spl|~sQ31_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f392,f398])).
% 0.12/0.53 fof(f887,plain,(
% 0.12/0.53 $false|~sQ29_spl|~sQ31_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f886,f217])).
% 0.12/0.53 fof(f888,plain,(
% 0.12/0.53 ~sQ29_spl|~sQ31_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f887])).
% 0.12/0.53 fof(f904,plain,(
% 0.12/0.53 ~op(e0,e0)=e2|~sQ10_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f330,f190])).
% 0.12/0.53 fof(f907,plain,(
% 0.12/0.53 e0=e2|~sQ8_spl|~sQ10_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f324,f330])).
% 0.12/0.53 fof(f908,plain,(
% 0.12/0.53 $false|~sQ8_spl|~sQ10_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f907,f214])).
% 0.12/0.53 fof(f909,plain,(
% 0.12/0.53 ~sQ8_spl|~sQ10_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f908])).
% 0.12/0.53 fof(f925,plain,(
% 0.12/0.53 e3=unit|~sQ79_spl|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f554,f775])).
% 0.12/0.53 fof(f931,plain,(
% 0.12/0.53 e3=e2|~sQ79_spl|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f925])).
% 0.12/0.53 fof(f932,plain,(
% 0.12/0.53 $false|~sQ79_spl|~sQ66_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f931,f218])).
% 0.12/0.53 fof(f933,plain,(
% 0.12/0.53 ~sQ79_spl|~sQ66_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f932])).
% 0.12/0.53 fof(f962,plain,(
% 0.12/0.53 e0=e3|~sQ64_spl|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f515])).
% 0.12/0.53 fof(f963,plain,(
% 0.12/0.53 $false|~sQ64_spl|~sQ67_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f962,f215])).
% 0.12/0.53 fof(f964,plain,(
% 0.12/0.53 ~sQ64_spl|~sQ67_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f963])).
% 0.12/0.53 fof(f967,plain,(
% 0.12/0.53 op(e3,e2)=unit|~sQ79_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f554,f130])).
% 0.12/0.53 fof(f982,plain,(
% 0.12/0.53 op(e3,e1)=e3|~sQ65_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f509,f123])).
% 0.12/0.53 fof(f996,plain,(
% 0.12/0.53 op(e2,e1)=e2|~sQ65_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f509,f121])).
% 0.12/0.53 fof(f1009,plain,(
% 0.12/0.53 e1=e3|~sQ65_spl|~sQ23_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f1010,f372])).
% 0.12/0.53 fof(f1010,plain,(
% 0.12/0.53 op(e1,e1)=e1|~sQ65_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f509,f119])).
% 0.12/0.53 fof(f1011,plain,(
% 0.12/0.53 $false|~sQ65_spl|~sQ23_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f1009,f217])).
% 0.12/0.53 fof(f1012,plain,(
% 0.12/0.53 ~sQ65_spl|~sQ23_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f1011])).
% 0.12/0.53 fof(f1024,plain,(
% 0.12/0.53 op(e2,e1)=e1|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f118])).
% 0.12/0.53 fof(f1032,plain,(
% 0.12/0.53 op(e0,e2)=e0|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f117])).
% 0.12/0.53 fof(f1041,plain,(
% 0.12/0.53 op(e3,e2)=op(e0,op(e0,e2))|~sQ3_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f307,f54])).
% 0.12/0.53 fof(f1042,plain,(
% 0.12/0.53 op(e3,e2)=op(e0,e0)|~sQ66_spl|~sQ3_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f1032,f1041])).
% 0.12/0.53 fof(f1045,plain,(
% 0.12/0.53 op(e3,e2)=e3|~sQ66_spl|~sQ3_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f307,f1042])).
% 0.12/0.53 fof(f1054,plain,(
% 0.12/0.53 op(e3,e0)=op(e0,op(e0,e0))|~sQ3_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f307,f52])).
% 0.12/0.53 fof(f1061,plain,(
% 0.12/0.53 op(e3,e0)=op(e0,e3)|~sQ3_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f307,f1054])).
% 0.12/0.53 fof(f1068,plain,(
% 0.12/0.53 op(e2,e0)=e0|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f116])).
% 0.12/0.53 fof(f1071,plain,(
% 0.12/0.53 ~e3=e3|~sQ66_spl|~sQ3_spl|~sQ63_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f1045,f786])).
% 0.12/0.53 fof(f1072,plain,(
% 0.12/0.53 $false|~sQ66_spl|~sQ3_spl|~sQ63_spl),
% 0.12/0.53 inference(trivial_equality_resolution,[status(thm)],[f1071])).
% 0.12/0.53 fof(f1073,plain,(
% 0.12/0.53 ~sQ66_spl|~sQ3_spl|~sQ63_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f1072])).
% 0.12/0.53 fof(f1081,plain,(
% 0.12/0.53 e0=e1|~sQ66_spl|~sQ9_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f1032,f327])).
% 0.12/0.53 fof(f1082,plain,(
% 0.12/0.53 $false|~sQ66_spl|~sQ9_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f1081,f213])).
% 0.12/0.53 fof(f1083,plain,(
% 0.12/0.53 ~sQ66_spl|~sQ9_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f1082])).
% 0.12/0.53 fof(f1090,plain,(
% 0.12/0.53 inv(e0)=unit|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f137])).
% 0.12/0.53 fof(f1092,plain,(
% 0.12/0.53 ~e0=inv(e2)|~sQ64_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f1094,f160])).
% 0.12/0.53 fof(f1094,plain,(
% 0.12/0.53 inv(e0)=e0|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f506,f1090])).
% 0.12/0.53 fof(f1095,plain,(
% 0.12/0.53 ~sQ76_spl|~sQ64_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1092,f544,f505])).
% 0.12/0.53 fof(f1098,plain,(
% 0.12/0.53 sQ37_spl|~sQ66_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1024,f417,f511])).
% 0.12/0.53 fof(f1099,plain,(
% 0.12/0.53 sQ32_spl|~sQ66_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1068,f401,f511])).
% 0.12/0.53 fof(f1101,plain,(
% 0.12/0.53 sQ10_spl|~sQ64_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f699,f329,f505])).
% 0.12/0.53 fof(f1102,plain,(
% 0.12/0.53 $false|~sQ63_spl|~sQ64_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f711,f791])).
% 0.12/0.53 fof(f1103,plain,(
% 0.12/0.53 ~sQ63_spl|~sQ64_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f1102])).
% 0.12/0.53 fof(f1109,plain,(
% 0.12/0.53 ~e0=op(e0,e2)|~sQ4_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f311,f192])).
% 0.12/0.53 fof(f1137,plain,(
% 0.12/0.53 ~e2=op(e2,e3)|~sQ42_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f434,f206])).
% 0.12/0.53 fof(f1150,plain,(
% 0.12/0.53 ~e2=op(e2,e3)|~sQ38_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f421,f205])).
% 0.12/0.53 fof(f1156,plain,(
% 0.12/0.53 ~sQ45_spl|~sQ37_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f810,f443,f417])).
% 0.12/0.53 fof(f1157,plain,(
% 0.12/0.53 ~sQ41_spl|~sQ37_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f811,f430,f417])).
% 0.12/0.53 fof(f1158,plain,(
% 0.12/0.53 ~sQ33_spl|~sQ37_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f812,f404,f417])).
% 0.12/0.53 fof(f1159,plain,(
% 0.12/0.53 ~sQ53_spl|~sQ37_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f813,f469,f417])).
% 0.12/0.53 fof(f1160,plain,(
% 0.12/0.53 ~e1=e1|~sQ21_spl|~sQ37_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f366,f814])).
% 0.12/0.53 fof(f1161,plain,(
% 0.12/0.53 $false|~sQ21_spl|~sQ37_spl),
% 0.12/0.53 inference(trivial_equality_resolution,[status(thm)],[f1160])).
% 0.12/0.53 fof(f1162,plain,(
% 0.12/0.53 ~sQ21_spl|~sQ37_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f1161])).
% 0.12/0.53 fof(f1165,plain,(
% 0.12/0.53 ~e0=op(e1,e0)|~sQ0_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f298,f165])).
% 0.12/0.53 fof(f1167,plain,(
% 0.12/0.53 ~e0=op(e2,e0)|~sQ0_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f298,f166])).
% 0.12/0.53 fof(f1168,plain,(
% 0.12/0.53 ~e0=op(e0,e3)|~sQ4_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f311,f193])).
% 0.12/0.53 fof(f1170,plain,(
% 0.12/0.53 ~e1=op(e1,e3)|~sQ21_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f366,f199])).
% 0.12/0.53 fof(f1179,plain,(
% 0.12/0.53 ~op(e1,e2)=e2|~sQ42_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f434,f180])).
% 0.12/0.53 fof(f1192,plain,(
% 0.12/0.53 op(e1,e2)=e2|~sQ65_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f509,f120])).
% 0.12/0.53 fof(f1193,plain,(
% 0.12/0.53 $false|~sQ42_spl|~sQ65_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f1192,f1179])).
% 0.12/0.53 fof(f1194,plain,(
% 0.12/0.53 ~sQ42_spl|~sQ65_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f1193])).
% 0.12/0.53 fof(f1196,plain,(
% 0.12/0.53 e0=unit|~sQ68_spl|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f519,f833])).
% 0.12/0.53 fof(f1225,plain,(
% 0.12/0.53 ~sQ2_spl|~sQ10_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f904,f303,f329])).
% 0.12/0.53 fof(f1228,plain,(
% 0.12/0.53 ~sQ8_spl|~sQ4_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1109,f323,f310])).
% 0.12/0.53 fof(f1241,plain,(
% 0.12/0.53 op(e3,e3)=e3|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f515,f123])).
% 0.12/0.53 fof(f1243,plain,(
% 0.12/0.53 op(e2,e3)=e2|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f515,f121])).
% 0.12/0.53 fof(f1244,plain,(
% 0.12/0.53 sQ46_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1243,f446,f514])).
% 0.12/0.53 fof(f1245,plain,(
% 0.12/0.53 sQ5_spl|~sQ64_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f686,f313,f505])).
% 0.12/0.53 fof(f1255,plain,(
% 0.12/0.53 ~sQ32_spl|~sQ0_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1167,f401,f297])).
% 0.12/0.53 fof(f1256,plain,(
% 0.12/0.53 ~sQ59_spl|~sQ63_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f786,f488,f501])).
% 0.12/0.53 fof(f1257,plain,(
% 0.12/0.53 ~sQ46_spl|~sQ38_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1150,f446,f420])).
% 0.12/0.53 fof(f1260,plain,(
% 0.12/0.53 sQ38_spl|~sQ65_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f996,f420,f508])).
% 0.12/0.53 fof(f1261,plain,(
% 0.12/0.53 sQ55_spl|~sQ65_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f982,f475,f508])).
% 0.12/0.53 fof(f1266,plain,(
% 0.12/0.53 ~sQ55_spl|~sQ63_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f787,f475,f501])).
% 0.12/0.53 fof(f1269,plain,(
% 0.12/0.53 sQ8_spl|~sQ66_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1032,f323,f511])).
% 0.12/0.53 fof(f1303,plain,(
% 0.12/0.53 ~sQ5_spl|~sQ37_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f815,f313,f417])).
% 0.12/0.53 fof(f1327,plain,(
% 0.12/0.53 op(e1,e0)=e1|~sQ68_spl|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f1196,f119])).
% 0.12/0.53 fof(f1343,plain,(
% 0.12/0.53 ~e1=op(e1,e1)|~sQ68_spl|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f1327,f195])).
% 0.12/0.53 fof(f1390,plain,(
% 0.12/0.53 ~e2=op(e2,e1)|~sQ68_spl|~sQ64_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f1391,f201])).
% 0.12/0.53 fof(f1391,plain,(
% 0.12/0.53 op(e2,e0)=e2|~sQ68_spl|~sQ64_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f1196,f121])).
% 0.12/0.53 fof(f1392,plain,(
% 0.12/0.53 ~sQ38_spl|~sQ68_spl|~sQ64_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1390,f420,f518,f505])).
% 0.12/0.53 fof(f1448,plain,(
% 0.12/0.53 op(op(e1,e3),e2)=op(e1,e0)|~sQ56_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f480,f82])).
% 0.12/0.53 fof(f1456,plain,(
% 0.12/0.53 inv(e2)=unit|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f137])).
% 0.12/0.53 fof(f1457,plain,(
% 0.12/0.53 inv(e2)=e2|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f1456])).
% 0.12/0.53 fof(f1462,plain,(
% 0.12/0.53 ~op(e1,e1)=e0|~sQ36_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f415,f174])).
% 0.12/0.53 fof(f1478,plain,(
% 0.12/0.53 ~sQ21_spl|~sQ68_spl|~sQ64_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1343,f365,f518,f505])).
% 0.12/0.53 fof(f1485,plain,(
% 0.12/0.53 ~sQ16_spl|~sQ0_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1165,f349,f297])).
% 0.12/0.53 fof(f1497,plain,(
% 0.12/0.53 op(unit,e2)=op(e3,op(e3,e2))|~sQ83_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f1501,f114])).
% 0.12/0.53 fof(f1501,plain,(
% 0.12/0.53 op(e3,e3)=unit|~sQ83_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f567,f132])).
% 0.12/0.53 fof(f1518,plain,(
% 0.12/0.53 ~op(e1,e3)=e2|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f1521,f186])).
% 0.12/0.53 fof(f1521,plain,(
% 0.12/0.53 op(e2,e3)=e2|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f121])).
% 0.12/0.53 fof(f1522,plain,(
% 0.12/0.53 ~sQ30_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1518,f394,f514])).
% 0.12/0.53 fof(f1524,plain,(
% 0.12/0.53 sQ78_spl|~sQ66_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1457,f550,f511])).
% 0.12/0.53 fof(f1608,plain,(
% 0.12/0.53 op(e1,e0)=e0|~sQ65_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f509,f116])).
% 0.12/0.53 fof(f1700,plain,(
% 0.12/0.53 ~op(e2,e0)=e0|~sQ48_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f454,f170])).
% 0.12/0.53 fof(f1702,plain,(
% 0.12/0.53 ~sQ32_spl|~sQ48_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1700,f401,f453])).
% 0.12/0.53 fof(f1727,plain,(
% 0.12/0.53 ~e2=op(e0,e3)|~sQ2_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f304,f191])).
% 0.12/0.53 fof(f1739,plain,(
% 0.12/0.53 ~op(e1,e0)=e0|~sQ66_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f1747,f168])).
% 0.12/0.53 fof(f1747,plain,(
% 0.12/0.53 op(e2,e0)=e0|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f116])).
% 0.12/0.53 fof(f1753,plain,(
% 0.12/0.53 ~e0=op(e0,e3)|~sQ66_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f1754,f194])).
% 0.12/0.53 fof(f1754,plain,(
% 0.12/0.53 op(e0,e2)=e0|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f117])).
% 0.12/0.53 fof(f1755,plain,(
% 0.12/0.53 ~sQ12_spl|~sQ66_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1753,f336,f511])).
% 0.12/0.53 fof(f1757,plain,(
% 0.12/0.53 op(unit,e2)=op(e3,e1)|~sQ57_spl|~sQ83_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f483,f1497])).
% 0.12/0.53 fof(f1761,plain,(
% 0.12/0.53 ~op(e2,e2)=e1|~sQ57_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f483,f182])).
% 0.12/0.53 fof(f1789,plain,(
% 0.12/0.53 ~sQ20_spl|~sQ36_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1462,f362,f414])).
% 0.12/0.53 fof(f1796,plain,(
% 0.12/0.53 ~sQ29_spl|~sQ21_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1170,f391,f365])).
% 0.12/0.53 fof(f1798,plain,(
% 0.12/0.53 ~sQ41_spl|~sQ57_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1761,f430,f482])).
% 0.12/0.53 fof(f1799,plain,(
% 0.12/0.53 ~sQ51_spl|~sQ63_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f788,f462,f501])).
% 0.12/0.53 fof(f1801,plain,(
% 0.12/0.53 ~sQ16_spl|~sQ66_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1739,f349,f511])).
% 0.12/0.53 fof(f1802,plain,(
% 0.12/0.53 ~sQ55_spl|~sQ59_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f821,f475,f488])).
% 0.12/0.53 fof(f1818,plain,(
% 0.12/0.53 op(e1,e2)=e2|~sQ65_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f509,f120])).
% 0.12/0.53 fof(f2002,plain,(
% 0.12/0.53 ~e2=op(e3,e2)|~sQ65_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f1818,f181])).
% 0.12/0.53 fof(f2028,plain,(
% 0.12/0.53 ~sQ31_spl|~sQ47_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f861,f397,f449])).
% 0.12/0.53 fof(f2032,plain,(
% 0.12/0.53 ~inv(e1)=e3|~sQ83_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f567,f163])).
% 0.12/0.53 fof(f2036,plain,(
% 0.12/0.53 ~sQ14_spl|~sQ2_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1727,f342,f303])).
% 0.12/0.53 fof(f2037,plain,(
% 0.12/0.53 sQ63_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1241,f501,f514])).
% 0.12/0.53 fof(f2046,plain,(
% 0.12/0.53 ~sQ46_spl|~sQ42_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1137,f446,f433])).
% 0.12/0.53 fof(f2053,plain,(
% 0.12/0.53 ~op(e0,e3)=e0|~sQ3_spl|sQ48_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f1061,f455])).
% 0.12/0.53 fof(f2069,plain,(
% 0.12/0.53 ~e3=op(e2,e0)|~sQ3_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f307,f166])).
% 0.12/0.53 fof(f2131,plain,(
% 0.12/0.53 ~sQ15_spl|~sQ47_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f862,f345,f449])).
% 0.12/0.53 fof(f2132,plain,(
% 0.12/0.53 ~sQ29_spl|~sQ25_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f797,f391,f378])).
% 0.12/0.53 fof(f2172,plain,(
% 0.12/0.53 ~e0=op(e2,e3)|~sQ66_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f2173,f203])).
% 0.12/0.53 fof(f2173,plain,(
% 0.12/0.53 op(e2,e0)=e0|~sQ66_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f512,f116])).
% 0.12/0.53 fof(f2174,plain,(
% 0.12/0.53 ~sQ44_spl|~sQ66_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2172,f440,f511])).
% 0.12/0.53 fof(f2181,plain,(
% 0.12/0.53 ~sQ35_spl|~sQ3_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2069,f410,f306])).
% 0.12/0.53 fof(f2187,plain,(
% 0.12/0.53 ~sQ15_spl|~sQ63_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f791,f345,f501])).
% 0.12/0.53 fof(f2191,plain,(
% 0.12/0.53 sQ16_spl|~sQ65_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1608,f349,f508])).
% 0.12/0.53 fof(f2197,plain,(
% 0.12/0.53 ~sQ58_spl|~sQ65_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2002,f485,f508])).
% 0.12/0.53 fof(f2198,plain,(
% 0.12/0.53 ~sQ12_spl|~sQ4_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f1168,f336,f310])).
% 0.12/0.53 fof(f2199,plain,(
% 0.12/0.53 op(e0,e3)=e0|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f515,f117])).
% 0.12/0.53 fof(f2203,plain,(
% 0.12/0.53 sQ12_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2199,f336,f514])).
% 0.12/0.53 fof(f2204,plain,(
% 0.12/0.53 op(e3,e2)=e3|~sQ67_spl|~sQ79_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f967])).
% 0.12/0.53 fof(f2205,plain,(
% 0.12/0.53 $false|sQ59_spl|~sQ67_spl|~sQ79_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f2204,f490])).
% 0.12/0.53 fof(f2206,plain,(
% 0.12/0.53 sQ59_spl|~sQ67_spl|~sQ79_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f2205])).
% 0.12/0.53 fof(f2207,plain,(
% 0.12/0.53 inv(e3)=unit|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f137])).
% 0.12/0.53 fof(f2208,plain,(
% 0.12/0.53 inv(e3)=e3|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f2207])).
% 0.12/0.53 fof(f2222,plain,(
% 0.12/0.53 ~e3=e3|~sQ67_spl|sQ83_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f2208,f568])).
% 0.12/0.53 fof(f2223,plain,(
% 0.12/0.53 $false|~sQ67_spl|sQ83_spl),
% 0.12/0.53 inference(trivial_equality_resolution,[status(thm)],[f2222])).
% 0.12/0.53 fof(f2224,plain,(
% 0.12/0.53 ~sQ67_spl|sQ83_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f2223])).
% 0.12/0.53 fof(f2242,plain,(
% 0.12/0.53 ~sQ75_spl|~sQ83_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2032,f540,f566])).
% 0.12/0.53 fof(f2244,plain,(
% 0.12/0.53 op(e3,e2)=op(e3,e1)|~sQ67_spl|~sQ57_spl|~sQ83_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f1757])).
% 0.12/0.53 fof(f2245,plain,(
% 0.12/0.53 $false|~sQ67_spl|~sQ57_spl|~sQ83_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f2244,f210])).
% 0.12/0.53 fof(f2246,plain,(
% 0.12/0.53 ~sQ67_spl|~sQ57_spl|~sQ83_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f2245])).
% 0.12/0.53 fof(f2263,plain,(
% 0.12/0.53 op(e1,e3)=e1|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f119])).
% 0.12/0.53 fof(f2277,plain,(
% 0.12/0.53 ~op(e0,e2)=e2|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f2280,f179])).
% 0.12/0.53 fof(f2280,plain,(
% 0.12/0.53 op(e3,e2)=e2|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f120])).
% 0.12/0.53 fof(f2281,plain,(
% 0.12/0.53 ~sQ10_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2277,f329,f514])).
% 0.12/0.53 fof(f2282,plain,(
% 0.12/0.53 ~e1=e1|~sQ67_spl|sQ29_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f2263,f393])).
% 0.12/0.53 fof(f2283,plain,(
% 0.12/0.53 $false|~sQ67_spl|sQ29_spl),
% 0.12/0.53 inference(trivial_equality_resolution,[status(thm)],[f2282])).
% 0.12/0.53 fof(f2284,plain,(
% 0.12/0.53 ~sQ67_spl|sQ29_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f2283])).
% 0.12/0.53 fof(f2290,plain,(
% 0.12/0.53 ~op(e0,e1)=e1|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f2295,f173])).
% 0.12/0.53 fof(f2291,plain,(
% 0.12/0.53 ~op(e3,e0)=e1|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f2295,f207])).
% 0.12/0.53 fof(f2295,plain,(
% 0.12/0.53 op(e3,e1)=e1|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f118])).
% 0.12/0.53 fof(f2296,plain,(
% 0.12/0.53 ~sQ5_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2290,f313,f514])).
% 0.12/0.53 fof(f2297,plain,(
% 0.12/0.53 ~sQ49_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2291,f456,f514])).
% 0.12/0.53 fof(f2303,plain,(
% 0.12/0.53 ~e1=e1|~sQ67_spl|sQ53_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f2295,f471])).
% 0.12/0.53 fof(f2304,plain,(
% 0.12/0.53 $false|~sQ67_spl|sQ53_spl),
% 0.12/0.53 inference(trivial_equality_resolution,[status(thm)],[f2303])).
% 0.12/0.53 fof(f2305,plain,(
% 0.12/0.53 ~sQ67_spl|sQ53_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f2304])).
% 0.12/0.53 fof(f2306,plain,(
% 0.12/0.53 ~sQ12_spl|~sQ3_spl|sQ48_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2053,f336,f306,f453])).
% 0.12/0.53 fof(f2307,plain,(
% 0.12/0.53 op(e1,e2)=op(e1,e0)|~sQ67_spl|~sQ56_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f2263,f1448])).
% 0.12/0.53 fof(f2308,plain,(
% 0.12/0.53 $false|~sQ67_spl|~sQ56_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f2307,f196])).
% 0.12/0.53 fof(f2309,plain,(
% 0.12/0.53 ~sQ67_spl|~sQ56_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f2308])).
% 0.12/0.53 fof(f2363,plain,(
% 0.12/0.53 ~op(e1,e2)=e2|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f2280,f181])).
% 0.12/0.53 fof(f2378,plain,(
% 0.12/0.53 $false|~sQ67_spl|~sQ26_spl),
% 0.12/0.53 inference(forward_subsumption_resolution,[status(thm)],[f382,f2363])).
% 0.12/0.53 fof(f2379,plain,(
% 0.12/0.53 ~sQ67_spl|~sQ26_spl),
% 0.12/0.53 inference(contradiction_clause,[status(thm)],[f2378])).
% 0.12/0.53 fof(f2399,plain,(
% 0.12/0.53 ~op(e1,e0)=e0|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f2400,f169])).
% 0.12/0.53 fof(f2400,plain,(
% 0.12/0.53 op(e3,e0)=e0|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f116])).
% 0.12/0.53 fof(f2401,plain,(
% 0.12/0.53 ~sQ16_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2399,f349,f514])).
% 0.12/0.53 fof(f2411,plain,(
% 0.12/0.53 ~op(e2,e0)=e2|~sQ67_spl),
% 0.12/0.53 inference(backward_demodulation,[status(thm)],[f2417,f203])).
% 0.12/0.53 fof(f2417,plain,(
% 0.12/0.53 op(e2,e3)=e2|~sQ67_spl),
% 0.12/0.53 inference(forward_demodulation,[status(thm)],[f515,f121])).
% 0.12/0.53 fof(f2418,plain,(
% 0.12/0.53 ~sQ34_spl|~sQ67_spl),
% 0.12/0.53 inference(split_clause,[status(thm)],[f2411,f407,f514])).
% 0.12/0.53 fof(f2419,plain,(
% 0.12/0.53 $false),
% 0.12/0.53 inference(sat_refutation,[status(thm)],[f348,f387,f413,f426,f452,f491,f517,f530,f571,f572,f573,f576,f583,f584,f589,f590,f591,f592,f597,f598,f600,f607,f611,f614,f620,f622,f623,f630,f631,f635,f636,f637,f642,f656,f667,f742,f779,f837,f867,f870,f878,f888,f909,f933,f964,f1012,f1073,f1083,f1095,f1098,f1099,f1101,f1103,f1156,f1157,f1158,f1159,f1162,f1194,f1225,f1228,f1244,f1245,f1255,f1256,f1257,f1260,f1261,f1266,f1269,f1303,f1392,f1478,f1485,f1522,f1524,f1702,f1755,f1789,f1796,f1798,f1799,f1801,f1802,f2028,f2036,f2037,f2046,f2131,f2132,f2174,f2181,f2187,f2191,f2197,f2198,f2203,f2206,f2224,f2242,f2246,f2281,f2284,f2296,f2297,f2305,f2306,f2309,f2379,f2401,f2418])).
% 0.12/0.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.53 % Elapsed time: 0.173745 seconds
% 0.12/0.53 % CPU time: 1.109646 seconds
% 0.12/0.53 % Total memory used: 38.669 MB
% 0.12/0.53 % Net memory used: 38.118 MB
%------------------------------------------------------------------------------