Drodi-SAT---4.1.1.UNS-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : ALG130+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n016.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:40 AM UTC 2026

% Result   : Unsatisfiable 0.02s 0.48s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ALG130+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37  % Computer : n016.cluster.edu
% 0.09/0.37  % Model    : x86_64 x86_64
% 0.09/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37  % Memory   : 8046.5625MB
% 0.09/0.37  % OS       : Linux 6.8.0-71-generic
% 0.09/0.37  % CPULimit : 300
% 0.09/0.37  % WCLimit  : 300
% 0.09/0.37  % DateTime : Mon Sep 21 13:02:53 UTC 2026
% 0.02/0.38  % CPUTime  : 
% 0.02/0.38  % Drodi V4.1.1
% 0.02/0.48  % Refutation found
% 0.02/0.48  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.02/0.48  % SZS output start CNFRefutation for theBenchmark
% 0.02/0.48  fof(f1,axiom,(
% 0.02/0.48    ( ( 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.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f2,axiom,(
% 0.02/0.48    ( ( op(e0,e0) = e0| op(e0,e1) = e0| op(e0,e2) = e0| op(e0,e3) = e0 )& ( op(e0,e0) = e0| op(e1,e0) = e0| op(e2,e0) = e0| op(e3,e0) = e0 )& ( op(e0,e0) = e1| op(e0,e1) = e1| op(e0,e2) = e1| op(e0,e3) = e1 )& ( op(e0,e0) = e1| op(e1,e0) = e1| op(e2,e0) = e1| op(e3,e0) = e1 )& ( op(e0,e0) = e2| op(e0,e1) = e2| op(e0,e2) = e2| op(e0,e3) = e2 )& ( op(e0,e0) = e2| op(e1,e0) = e2| op(e2,e0) = e2| op(e3,e0) = e2 )& ( op(e0,e0) = e3| op(e0,e1) = e3| op(e0,e2) = e3| op(e0,e3) = e3 )& ( op(e0,e0) = e3| op(e1,e0) = e3| op(e2,e0) = e3| op(e3,e0) = e3 )& ( op(e1,e0) = e0| op(e1,e1) = e0| op(e1,e2) = e0| op(e1,e3) = e0 )& ( op(e0,e1) = e0| op(e1,e1) = e0| op(e2,e1) = e0| op(e3,e1) = e0 )& ( op(e1,e0) = e1| op(e1,e1) = e1| op(e1,e2) = e1| op(e1,e3) = e1 )& ( op(e0,e1) = e1| op(e1,e1) = e1| op(e2,e1) = e1| op(e3,e1) = e1 )& ( op(e1,e0) = e2| op(e1,e1) = e2| op(e1,e2) = e2| op(e1,e3) = e2 )& ( op(e0,e1) = e2| op(e1,e1) = e2| op(e2,e1) = e2| op(e3,e1) = e2 )& ( op(e1,e0) = e3| op(e1,e1) = e3| op(e1,e2) = e3| op(e1,e3) = e3 )& ( op(e0,e1) = e3| op(e1,e1) = e3| op(e2,e1) = e3| op(e3,e1) = e3 )& ( op(e2,e0) = e0| op(e2,e1) = e0| op(e2,e2) = e0| op(e2,e3) = e0 )& ( op(e0,e2) = e0| op(e1,e2) = e0| op(e2,e2) = e0| op(e3,e2) = e0 )& ( op(e2,e0) = e1| op(e2,e1) = e1| op(e2,e2) = e1| op(e2,e3) = e1 )& ( op(e0,e2) = e1| op(e1,e2) = e1| op(e2,e2) = e1| op(e3,e2) = e1 )& ( op(e2,e0) = e2| op(e2,e1) = e2| op(e2,e2) = e2| op(e2,e3) = e2 )& ( op(e0,e2) = e2| op(e1,e2) = e2| op(e2,e2) = e2| op(e3,e2) = e2 )& ( op(e2,e0) = e3| op(e2,e1) = e3| op(e2,e2) = e3| op(e2,e3) = e3 )& ( op(e0,e2) = e3| op(e1,e2) = e3| op(e2,e2) = e3| op(e3,e2) = e3 )& ( op(e3,e0) = e0| op(e3,e1) = e0| op(e3,e2) = e0| op(e3,e3) = e0 )& ( op(e0,e3) = e0| op(e1,e3) = e0| op(e2,e3) = e0| op(e3,e3) = e0 )& ( op(e3,e0) = e1| op(e3,e1) = e1| op(e3,e2) = e1| op(e3,e3) = e1 )& ( op(e0,e3) = e1| op(e1,e3) = e1| op(e2,e3) = e1| op(e3,e3) = e1 )& ( op(e3,e0) = e2| op(e3,e1) = e2| op(e3,e2) = e2| op(e3,e3) = e2 )& ( op(e0,e3) = e2| op(e1,e3) = e2| op(e2,e3) = e2| op(e3,e3) = e2 )& ( op(e3,e0) = e3| op(e3,e1) = e3| op(e3,e2) = e3| op(e3,e3) = e3 )& ( op(e0,e3) = e3| op(e1,e3) = e3| op(e2,e3) = e3| op(e3,e3) = e3 ) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f3,axiom,(
% 0.02/0.48    ( 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.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f4,axiom,(
% 0.02/0.48    ( e0 != e1& e0 != e2& e0 != e3& e1 != e2& e1 != e3& e2 != e3 ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f5,axiom,(
% 0.02/0.48    ( op(op(e0,e0),e0) = e0& op(op(e0,e1),e0) = e1& op(op(e0,e2),e0) = e2& op(op(e0,e3),e0) = e3& op(op(e1,e0),e1) = e0& op(op(e1,e1),e1) = e1& op(op(e1,e2),e1) = e2& op(op(e1,e3),e1) = e3& op(op(e2,e0),e2) = e0& op(op(e2,e1),e2) = e1& op(op(e2,e2),e2) = e2& op(op(e2,e3),e2) = e3& op(op(e3,e0),e3) = e0& op(op(e3,e1),e3) = e1& op(op(e3,e2),e3) = e2& op(op(e3,e3),e3) = e3& ( ( op(e0,op(e0,e0)) = op(e0,e0)& op(e0,op(e1,e0)) = op(e1,e0)& op(e0,op(e2,e0)) = op(e2,e0)& op(e0,op(e3,e0)) = op(e3,e0) )| ( op(e1,op(e0,e1)) = op(e0,e1)& op(e1,op(e1,e1)) = op(e1,e1)& op(e1,op(e2,e1)) = op(e2,e1)& op(e1,op(e3,e1)) = op(e3,e1) )| ( op(e2,op(e0,e2)) = op(e0,e2)& op(e2,op(e1,e2)) = op(e1,e2)& op(e2,op(e2,e2)) = op(e2,e2)& op(e2,op(e3,e2)) = op(e3,e2) )| ( op(e3,op(e0,e3)) = op(e0,e3)& op(e3,op(e1,e3)) = op(e1,e3)& op(e3,op(e2,e3)) = op(e2,e3)& op(e3,op(e3,e3)) = op(e3,e3) ) ) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f6,axiom,(
% 0.02/0.48    ~ ( e0 = op(op(e2,e1),op(e2,e1))& e3 = op(e2,e1) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f8,axiom,(
% 0.02/0.48    ~ ( e0 = op(op(e1,e2),op(e1,e2))& e3 = op(e1,e2) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f9,axiom,(
% 0.02/0.48    ~ ( e0 = op(op(e3,e2),op(e3,e2))& e1 = op(e3,e2) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f11,axiom,(
% 0.02/0.48    ~ ( e0 = op(op(e2,e3),op(e2,e3))& e1 = op(e2,e3) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f13,axiom,(
% 0.02/0.48    ~ ( e1 = op(op(e3,e0),op(e3,e0))& e2 = op(e3,e0) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f15,axiom,(
% 0.02/0.48    ~ ( e1 = op(op(e3,e2),op(e3,e2))& e0 = op(e3,e2) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f17,axiom,(
% 0.02/0.48    ~ ( e1 = op(op(e2,e3),op(e2,e3))& e0 = op(e2,e3) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f20,axiom,(
% 0.02/0.48    ~ ( e2 = op(op(e0,e1),op(e0,e1))& e3 = op(e0,e1) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f23,axiom,(
% 0.02/0.48    ~ ( e2 = op(op(e1,e3),op(e1,e3))& e0 = op(e1,e3) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f26,axiom,(
% 0.02/0.48    ~ ( e3 = op(op(e0,e1),op(e0,e1))& e2 = op(e0,e1) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f28,axiom,(
% 0.02/0.48    ~ ( e3 = op(op(e0,e2),op(e0,e2))& e1 = op(e0,e2) ) ),
% 0.02/0.48    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.48  fof(f30,plain,(
% 0.02/0.48    op(e0,e0)=e0|op(e0,e0)=e1|op(e0,e0)=e2|op(e0,e0)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f31,plain,(
% 0.02/0.48    op(e0,e1)=e0|op(e0,e1)=e1|op(e0,e1)=e2|op(e0,e1)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f32,plain,(
% 0.02/0.48    op(e0,e2)=e0|op(e0,e2)=e1|op(e0,e2)=e2|op(e0,e2)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f35,plain,(
% 0.02/0.48    op(e1,e1)=e0|op(e1,e1)=e1|op(e1,e1)=e2|op(e1,e1)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f37,plain,(
% 0.02/0.48    op(e1,e3)=e0|op(e1,e3)=e1|op(e1,e3)=e2|op(e1,e3)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f38,plain,(
% 0.02/0.48    op(e2,e0)=e0|op(e2,e0)=e1|op(e2,e0)=e2|op(e2,e0)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f39,plain,(
% 0.02/0.48    op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f41,plain,(
% 0.02/0.48    op(e2,e3)=e0|op(e2,e3)=e1|op(e2,e3)=e2|op(e2,e3)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f42,plain,(
% 0.02/0.48    op(e3,e0)=e0|op(e3,e0)=e1|op(e3,e0)=e2|op(e3,e0)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f43,plain,(
% 0.02/0.48    op(e3,e1)=e0|op(e3,e1)=e1|op(e3,e1)=e2|op(e3,e1)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f44,plain,(
% 0.02/0.48    op(e3,e2)=e0|op(e3,e2)=e1|op(e3,e2)=e2|op(e3,e2)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f45,plain,(
% 0.02/0.48    op(e3,e3)=e0|op(e3,e3)=e1|op(e3,e3)=e2|op(e3,e3)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.48  fof(f46,plain,(
% 0.02/0.48    op(e0,e0)=e0|op(e0,e1)=e0|op(e0,e2)=e0|op(e0,e3)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f48,plain,(
% 0.02/0.48    op(e0,e0)=e1|op(e0,e1)=e1|op(e0,e2)=e1|op(e0,e3)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f49,plain,(
% 0.02/0.48    op(e0,e0)=e1|op(e1,e0)=e1|op(e2,e0)=e1|op(e3,e0)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f54,plain,(
% 0.02/0.48    op(e1,e0)=e0|op(e1,e1)=e0|op(e1,e2)=e0|op(e1,e3)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f55,plain,(
% 0.02/0.48    op(e0,e1)=e0|op(e1,e1)=e0|op(e2,e1)=e0|op(e3,e1)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f57,plain,(
% 0.02/0.48    op(e0,e1)=e1|op(e1,e1)=e1|op(e2,e1)=e1|op(e3,e1)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f61,plain,(
% 0.02/0.48    op(e0,e1)=e3|op(e1,e1)=e3|op(e2,e1)=e3|op(e3,e1)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f62,plain,(
% 0.02/0.48    op(e2,e0)=e0|op(e2,e1)=e0|op(e2,e2)=e0|op(e2,e3)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f63,plain,(
% 0.02/0.48    op(e0,e2)=e0|op(e1,e2)=e0|op(e2,e2)=e0|op(e3,e2)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f64,plain,(
% 0.02/0.48    op(e2,e0)=e1|op(e2,e1)=e1|op(e2,e2)=e1|op(e2,e3)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f65,plain,(
% 0.02/0.48    op(e0,e2)=e1|op(e1,e2)=e1|op(e2,e2)=e1|op(e3,e2)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f67,plain,(
% 0.02/0.48    op(e0,e2)=e2|op(e1,e2)=e2|op(e2,e2)=e2|op(e3,e2)=e2),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f68,plain,(
% 0.02/0.48    op(e2,e0)=e3|op(e2,e1)=e3|op(e2,e2)=e3|op(e2,e3)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f70,plain,(
% 0.02/0.48    op(e3,e0)=e0|op(e3,e1)=e0|op(e3,e2)=e0|op(e3,e3)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f71,plain,(
% 0.02/0.48    op(e0,e3)=e0|op(e1,e3)=e0|op(e2,e3)=e0|op(e3,e3)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f74,plain,(
% 0.02/0.48    op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f77,plain,(
% 0.02/0.48    op(e0,e3)=e3|op(e1,e3)=e3|op(e2,e3)=e3|op(e3,e3)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.48  fof(f78,plain,(
% 0.02/0.48    ~op(e0,e0)=op(e1,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f79,plain,(
% 0.02/0.48    ~op(e0,e0)=op(e2,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f80,plain,(
% 0.02/0.48    ~op(e0,e0)=op(e3,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f81,plain,(
% 0.02/0.48    ~op(e1,e0)=op(e2,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f82,plain,(
% 0.02/0.48    ~op(e1,e0)=op(e3,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f83,plain,(
% 0.02/0.48    ~op(e2,e0)=op(e3,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f84,plain,(
% 0.02/0.48    ~op(e0,e1)=op(e1,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f85,plain,(
% 0.02/0.48    ~op(e0,e1)=op(e2,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f86,plain,(
% 0.02/0.48    ~op(e0,e1)=op(e3,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f87,plain,(
% 0.02/0.48    ~op(e1,e1)=op(e2,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f88,plain,(
% 0.02/0.48    ~op(e1,e1)=op(e3,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f89,plain,(
% 0.02/0.48    ~op(e2,e1)=op(e3,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f90,plain,(
% 0.02/0.48    ~op(e0,e2)=op(e1,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f91,plain,(
% 0.02/0.48    ~op(e0,e2)=op(e2,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f92,plain,(
% 0.02/0.48    ~op(e0,e2)=op(e3,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f93,plain,(
% 0.02/0.48    ~op(e1,e2)=op(e2,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f94,plain,(
% 0.02/0.48    ~op(e1,e2)=op(e3,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f95,plain,(
% 0.02/0.48    ~op(e2,e2)=op(e3,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f96,plain,(
% 0.02/0.48    ~op(e0,e3)=op(e1,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f97,plain,(
% 0.02/0.48    ~op(e0,e3)=op(e2,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f98,plain,(
% 0.02/0.48    ~op(e0,e3)=op(e3,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f99,plain,(
% 0.02/0.48    ~op(e1,e3)=op(e2,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f100,plain,(
% 0.02/0.48    ~op(e1,e3)=op(e3,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f101,plain,(
% 0.02/0.48    ~op(e2,e3)=op(e3,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f102,plain,(
% 0.02/0.48    ~op(e0,e0)=op(e0,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f103,plain,(
% 0.02/0.48    ~op(e0,e0)=op(e0,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f105,plain,(
% 0.02/0.48    ~op(e0,e1)=op(e0,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f107,plain,(
% 0.02/0.48    ~op(e0,e2)=op(e0,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f110,plain,(
% 0.02/0.48    ~op(e1,e0)=op(e1,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f111,plain,(
% 0.02/0.48    ~op(e1,e1)=op(e1,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f112,plain,(
% 0.02/0.48    ~op(e1,e1)=op(e1,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f113,plain,(
% 0.02/0.48    ~op(e1,e2)=op(e1,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f114,plain,(
% 0.02/0.48    ~op(e2,e0)=op(e2,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f115,plain,(
% 0.02/0.48    ~op(e2,e0)=op(e2,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f116,plain,(
% 0.02/0.48    ~op(e2,e0)=op(e2,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f117,plain,(
% 0.02/0.48    ~op(e2,e1)=op(e2,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f118,plain,(
% 0.02/0.48    ~op(e2,e1)=op(e2,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f119,plain,(
% 0.02/0.48    ~op(e2,e2)=op(e2,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f120,plain,(
% 0.02/0.48    ~op(e3,e0)=op(e3,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f121,plain,(
% 0.02/0.48    ~op(e3,e0)=op(e3,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f122,plain,(
% 0.02/0.48    ~op(e3,e0)=op(e3,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f123,plain,(
% 0.02/0.48    ~op(e3,e1)=op(e3,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f124,plain,(
% 0.02/0.48    ~op(e3,e1)=op(e3,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.48  fof(f126,plain,(
% 0.02/0.48    ~e0=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f4])).
% 0.02/0.48  fof(f127,plain,(
% 0.02/0.48    ~e0=e2),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f4])).
% 0.02/0.48  fof(f128,plain,(
% 0.02/0.48    ~e0=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f4])).
% 0.02/0.48  fof(f129,plain,(
% 0.02/0.48    ~e1=e2),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f4])).
% 0.02/0.48  fof(f130,plain,(
% 0.02/0.48    ~e1=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f4])).
% 0.02/0.48  fof(f131,plain,(
% 0.02/0.48    ~e2=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f4])).
% 0.02/0.48  fof(f132,definition,(
% 0.02/0.48    sP0_prd<=>(((((op(e0,op(e0,e0))=op(e0,e0)&op(e0,op(e1,e0))=op(e1,e0))&op(e0,op(e2,e0))=op(e2,e0))&op(e0,op(e3,e0))=op(e3,e0))|(((op(e1,op(e0,e1))=op(e0,e1)&op(e1,op(e1,e1))=op(e1,e1))&op(e1,op(e2,e1))=op(e2,e1))&op(e1,op(e3,e1))=op(e3,e1)))|(((op(e2,op(e0,e2))=op(e0,e2)&op(e2,op(e1,e2))=op(e1,e2))&op(e2,op(e2,e2))=op(e2,e2))&op(e2,op(e3,e2))=op(e3,e2)))),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.02/0.48  fof(f133,plain,(
% 0.02/0.48    (((((((((((((((op(op(e0,e0),e0)=e0&op(op(e0,e1),e0)=e1)&op(op(e0,e2),e0)=e2)&op(op(e0,e3),e0)=e3)&op(op(e1,e0),e1)=e0)&op(op(e1,e1),e1)=e1)&op(op(e1,e2),e1)=e2)&op(op(e1,e3),e1)=e3)&op(op(e2,e0),e2)=e0)&op(op(e2,e1),e2)=e1)&op(op(e2,e2),e2)=e2)&op(op(e2,e3),e2)=e3)&op(op(e3,e0),e3)=e0)&op(op(e3,e1),e3)=e1)&op(op(e3,e2),e3)=e2)&op(op(e3,e3),e3)=e3)&(sP0_prd|(((op(e3,op(e0,e3))=op(e0,e3)&op(e3,op(e1,e3))=op(e1,e3))&op(e3,op(e2,e3))=op(e2,e3))&op(e3,op(e3,e3))=op(e3,e3)))),
% 0.02/0.48    inference(formula_renaming,[status(thm)],[f5,f132])).
% 0.02/0.48  fof(f134,plain,(
% 0.02/0.48    op(op(e0,e0),e0)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f135,plain,(
% 0.02/0.48    op(op(e0,e1),e0)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f136,plain,(
% 0.02/0.48    op(op(e0,e2),e0)=e2),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f137,plain,(
% 0.02/0.48    op(op(e0,e3),e0)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f138,plain,(
% 0.02/0.48    op(op(e1,e0),e1)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f139,plain,(
% 0.02/0.48    op(op(e1,e1),e1)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f140,plain,(
% 0.02/0.48    op(op(e1,e2),e1)=e2),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f141,plain,(
% 0.02/0.48    op(op(e1,e3),e1)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f142,plain,(
% 0.02/0.48    op(op(e2,e0),e2)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f143,plain,(
% 0.02/0.48    op(op(e2,e1),e2)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f144,plain,(
% 0.02/0.48    op(op(e2,e2),e2)=e2),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f145,plain,(
% 0.02/0.48    op(op(e2,e3),e2)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f146,plain,(
% 0.02/0.48    op(op(e3,e0),e3)=e0),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f147,plain,(
% 0.02/0.48    op(op(e3,e1),e3)=e1),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f148,plain,(
% 0.02/0.48    op(op(e3,e2),e3)=e2),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f149,plain,(
% 0.02/0.48    op(op(e3,e3),e3)=e3),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f150,plain,(
% 0.02/0.48    sP0_prd|op(e3,op(e0,e3))=op(e0,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f151,plain,(
% 0.02/0.48    sP0_prd|op(e3,op(e1,e3))=op(e1,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f152,plain,(
% 0.02/0.48    sP0_prd|op(e3,op(e2,e3))=op(e2,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f153,plain,(
% 0.02/0.48    sP0_prd|op(e3,op(e3,e3))=op(e3,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f133])).
% 0.02/0.48  fof(f154,plain,(
% 0.02/0.48    (~e0=op(op(e2,e1),op(e2,e1))|~e3=op(e2,e1))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.02/0.48  fof(f155,plain,(
% 0.02/0.48    ~e0=op(op(e2,e1),op(e2,e1))|~e3=op(e2,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f154])).
% 0.02/0.48  fof(f158,plain,(
% 0.02/0.48    (~e0=op(op(e1,e2),op(e1,e2))|~e3=op(e1,e2))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.02/0.48  fof(f159,plain,(
% 0.02/0.48    ~e0=op(op(e1,e2),op(e1,e2))|~e3=op(e1,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f158])).
% 0.02/0.48  fof(f160,plain,(
% 0.02/0.48    (~e0=op(op(e3,e2),op(e3,e2))|~e1=op(e3,e2))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.02/0.48  fof(f161,plain,(
% 0.02/0.48    ~e0=op(op(e3,e2),op(e3,e2))|~e1=op(e3,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f160])).
% 0.02/0.48  fof(f164,plain,(
% 0.02/0.48    (~e0=op(op(e2,e3),op(e2,e3))|~e1=op(e2,e3))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.02/0.48  fof(f165,plain,(
% 0.02/0.48    ~e0=op(op(e2,e3),op(e2,e3))|~e1=op(e2,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f164])).
% 0.02/0.48  fof(f168,plain,(
% 0.02/0.48    (~e1=op(op(e3,e0),op(e3,e0))|~e2=op(e3,e0))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.02/0.48  fof(f169,plain,(
% 0.02/0.48    ~e1=op(op(e3,e0),op(e3,e0))|~e2=op(e3,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f168])).
% 0.02/0.48  fof(f172,plain,(
% 0.02/0.48    (~e1=op(op(e3,e2),op(e3,e2))|~e0=op(e3,e2))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.02/0.48  fof(f173,plain,(
% 0.02/0.48    ~e1=op(op(e3,e2),op(e3,e2))|~e0=op(e3,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f172])).
% 0.02/0.48  fof(f176,plain,(
% 0.02/0.48    (~e1=op(op(e2,e3),op(e2,e3))|~e0=op(e2,e3))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.02/0.48  fof(f177,plain,(
% 0.02/0.48    ~e1=op(op(e2,e3),op(e2,e3))|~e0=op(e2,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f176])).
% 0.02/0.48  fof(f182,plain,(
% 0.02/0.48    (~e2=op(op(e0,e1),op(e0,e1))|~e3=op(e0,e1))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.02/0.48  fof(f183,plain,(
% 0.02/0.48    ~e2=op(op(e0,e1),op(e0,e1))|~e3=op(e0,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f182])).
% 0.02/0.48  fof(f188,plain,(
% 0.02/0.48    (~e2=op(op(e1,e3),op(e1,e3))|~e0=op(e1,e3))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.02/0.48  fof(f189,plain,(
% 0.02/0.48    ~e2=op(op(e1,e3),op(e1,e3))|~e0=op(e1,e3)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f188])).
% 0.02/0.48  fof(f194,plain,(
% 0.02/0.48    (~e3=op(op(e0,e1),op(e0,e1))|~e2=op(e0,e1))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.02/0.48  fof(f195,plain,(
% 0.02/0.48    ~e3=op(op(e0,e1),op(e0,e1))|~e2=op(e0,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f194])).
% 0.02/0.48  fof(f198,plain,(
% 0.02/0.48    (~e3=op(op(e0,e2),op(e0,e2))|~e1=op(e0,e2))),
% 0.02/0.48    inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.02/0.48  fof(f199,plain,(
% 0.02/0.48    ~e3=op(op(e0,e2),op(e0,e2))|~e1=op(e0,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f198])).
% 0.02/0.48  fof(f202,definition,(
% 0.02/0.48    sP1_prd<=>((((op(e0,op(e0,e0))=op(e0,e0)&op(e0,op(e1,e0))=op(e1,e0))&op(e0,op(e2,e0))=op(e2,e0))&op(e0,op(e3,e0))=op(e3,e0))|(((op(e1,op(e0,e1))=op(e0,e1)&op(e1,op(e1,e1))=op(e1,e1))&op(e1,op(e2,e1))=op(e2,e1))&op(e1,op(e3,e1))=op(e3,e1)))),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.02/0.48  fof(f203,plain,(
% 0.02/0.48    sP0_prd<=>(sP1_prd|(((op(e2,op(e0,e2))=op(e0,e2)&op(e2,op(e1,e2))=op(e1,e2))&op(e2,op(e2,e2))=op(e2,e2))&op(e2,op(e3,e2))=op(e3,e2)))),
% 0.02/0.48    inference(formula_renaming,[status(thm)],[f132,f202])).
% 0.02/0.48  fof(f204,plain,(
% 0.02/0.48    (~sP0_prd|(sP1_prd|(((op(e2,op(e0,e2))=op(e0,e2)&op(e2,op(e1,e2))=op(e1,e2))&op(e2,op(e2,e2))=op(e2,e2))&op(e2,op(e3,e2))=op(e3,e2))))&(sP0_prd|(~sP1_prd&(((~op(e2,op(e0,e2))=op(e0,e2)|~op(e2,op(e1,e2))=op(e1,e2))|~op(e2,op(e2,e2))=op(e2,e2))|~op(e2,op(e3,e2))=op(e3,e2))))),
% 0.02/0.48    inference(NNF_transformation,[status(thm)],[f203])).
% 0.02/0.48  fof(f205,plain,(
% 0.02/0.48    ~sP0_prd|sP1_prd|op(e2,op(e0,e2))=op(e0,e2)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f204])).
% 0.02/0.48  fof(f209,plain,(
% 0.02/0.48    sP0_prd|~sP1_prd),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f204])).
% 0.02/0.48  fof(f211,definition,(
% 0.02/0.48    sP2_prd<=>(((op(e0,op(e0,e0))=op(e0,e0)&op(e0,op(e1,e0))=op(e1,e0))&op(e0,op(e2,e0))=op(e2,e0))&op(e0,op(e3,e0))=op(e3,e0))),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.02/0.48  fof(f212,plain,(
% 0.02/0.48    sP1_prd<=>(sP2_prd|(((op(e1,op(e0,e1))=op(e0,e1)&op(e1,op(e1,e1))=op(e1,e1))&op(e1,op(e2,e1))=op(e2,e1))&op(e1,op(e3,e1))=op(e3,e1)))),
% 0.02/0.48    inference(formula_renaming,[status(thm)],[f202,f211])).
% 0.02/0.48  fof(f213,plain,(
% 0.02/0.48    (~sP1_prd|(sP2_prd|(((op(e1,op(e0,e1))=op(e0,e1)&op(e1,op(e1,e1))=op(e1,e1))&op(e1,op(e2,e1))=op(e2,e1))&op(e1,op(e3,e1))=op(e3,e1))))&(sP1_prd|(~sP2_prd&(((~op(e1,op(e0,e1))=op(e0,e1)|~op(e1,op(e1,e1))=op(e1,e1))|~op(e1,op(e2,e1))=op(e2,e1))|~op(e1,op(e3,e1))=op(e3,e1))))),
% 0.02/0.48    inference(NNF_transformation,[status(thm)],[f212])).
% 0.02/0.48  fof(f214,plain,(
% 0.02/0.48    ~sP1_prd|sP2_prd|op(e1,op(e0,e1))=op(e0,e1)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f213])).
% 0.02/0.48  fof(f218,plain,(
% 0.02/0.48    sP1_prd|~sP2_prd),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f213])).
% 0.02/0.48  fof(f220,plain,(
% 0.02/0.48    (~sP2_prd|(((op(e0,op(e0,e0))=op(e0,e0)&op(e0,op(e1,e0))=op(e1,e0))&op(e0,op(e2,e0))=op(e2,e0))&op(e0,op(e3,e0))=op(e3,e0)))&(sP2_prd|(((~op(e0,op(e0,e0))=op(e0,e0)|~op(e0,op(e1,e0))=op(e1,e0))|~op(e0,op(e2,e0))=op(e2,e0))|~op(e0,op(e3,e0))=op(e3,e0)))),
% 0.02/0.48    inference(NNF_transformation,[status(thm)],[f211])).
% 0.02/0.48  fof(f221,plain,(
% 0.02/0.48    ~sP2_prd|op(e0,op(e0,e0))=op(e0,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f220])).
% 0.02/0.48  fof(f222,plain,(
% 0.02/0.48    ~sP2_prd|op(e0,op(e1,e0))=op(e1,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f220])).
% 0.02/0.48  fof(f223,plain,(
% 0.02/0.48    ~sP2_prd|op(e0,op(e2,e0))=op(e2,e0)),
% 0.02/0.48    inference(cnf_transformation,[status(thm)],[f220])).
% 0.02/0.48  fof(f226,definition,(
% 0.02/0.48    sQ0_spl <=> (op(e0,e0)=e0)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f227,plain,(
% 0.02/0.48    op(e0,e0)=e0|~sQ0_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f226])).
% 0.02/0.48  fof(f229,definition,(
% 0.02/0.48    sQ1_spl <=> (op(e0,e0)=e1)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f230,plain,(
% 0.02/0.48    op(e0,e0)=e1|~sQ1_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f229])).
% 0.02/0.48  fof(f232,definition,(
% 0.02/0.48    sQ2_spl <=> (op(e0,e0)=e2)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f233,plain,(
% 0.02/0.48    op(e0,e0)=e2|~sQ2_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f232])).
% 0.02/0.48  fof(f235,definition,(
% 0.02/0.48    sQ3_spl <=> (op(e0,e0)=e3)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f236,plain,(
% 0.02/0.48    op(e0,e0)=e3|~sQ3_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f235])).
% 0.02/0.48  fof(f238,plain,(
% 0.02/0.48    sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl),
% 0.02/0.48    inference(split_clause,[status(thm)],[f30,f226,f229,f232,f235])).
% 0.02/0.48  fof(f239,definition,(
% 0.02/0.48    sQ4_spl <=> (op(e0,e1)=e0)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f240,plain,(
% 0.02/0.48    op(e0,e1)=e0|~sQ4_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f239])).
% 0.02/0.48  fof(f242,definition,(
% 0.02/0.48    sQ5_spl <=> (op(e0,e1)=e1)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f243,plain,(
% 0.02/0.48    op(e0,e1)=e1|~sQ5_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f242])).
% 0.02/0.48  fof(f245,definition,(
% 0.02/0.48    sQ6_spl <=> (op(e0,e1)=e2)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f246,plain,(
% 0.02/0.48    op(e0,e1)=e2|~sQ6_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f245])).
% 0.02/0.48  fof(f248,definition,(
% 0.02/0.48    sQ7_spl <=> (op(e0,e1)=e3)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f251,plain,(
% 0.02/0.48    sQ4_spl|sQ5_spl|sQ6_spl|sQ7_spl),
% 0.02/0.48    inference(split_clause,[status(thm)],[f31,f239,f242,f245,f248])).
% 0.02/0.48  fof(f252,definition,(
% 0.02/0.48    sQ8_spl <=> (op(e0,e2)=e0)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f253,plain,(
% 0.02/0.48    op(e0,e2)=e0|~sQ8_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f252])).
% 0.02/0.48  fof(f255,definition,(
% 0.02/0.48    sQ9_spl <=> (op(e0,e2)=e1)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.02/0.48  fof(f256,plain,(
% 0.02/0.48    op(e0,e2)=e1|~sQ9_spl),
% 0.02/0.48    inference(component_clause,[status(thm)],[f255])).
% 0.02/0.48  fof(f258,definition,(
% 0.02/0.48    sQ10_spl <=> (op(e0,e2)=e2)),
% 0.02/0.48    introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f259,plain,(
% 0.02/0.49    op(e0,e2)=e2|~sQ10_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f258])).
% 0.02/0.49  fof(f260,plain,(
% 0.02/0.49    ~op(e0,e2)=e2|sQ10_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f258])).
% 0.02/0.49  fof(f261,definition,(
% 0.02/0.49    sQ11_spl <=> (op(e0,e2)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f264,plain,(
% 0.02/0.49    sQ8_spl|sQ9_spl|sQ10_spl|sQ11_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f32,f252,f255,f258,f261])).
% 0.02/0.49  fof(f265,definition,(
% 0.02/0.49    sQ12_spl <=> (op(e0,e3)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f266,plain,(
% 0.02/0.49    op(e0,e3)=e0|~sQ12_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f265])).
% 0.02/0.49  fof(f268,definition,(
% 0.02/0.49    sQ13_spl <=> (op(e0,e3)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f269,plain,(
% 0.02/0.49    op(e0,e3)=e1|~sQ13_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f268])).
% 0.02/0.49  fof(f271,definition,(
% 0.02/0.49    sQ14_spl <=> (op(e0,e3)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f274,definition,(
% 0.02/0.49    sQ15_spl <=> (op(e0,e3)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f275,plain,(
% 0.02/0.49    op(e0,e3)=e3|~sQ15_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f274])).
% 0.02/0.49  fof(f278,definition,(
% 0.02/0.49    sQ16_spl <=> (op(e1,e0)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f279,plain,(
% 0.02/0.49    op(e1,e0)=e0|~sQ16_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f278])).
% 0.02/0.49  fof(f281,definition,(
% 0.02/0.49    sQ17_spl <=> (op(e1,e0)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f284,definition,(
% 0.02/0.49    sQ18_spl <=> (op(e1,e0)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f287,definition,(
% 0.02/0.49    sQ19_spl <=> (op(e1,e0)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f291,definition,(
% 0.02/0.49    sQ20_spl <=> (op(e1,e1)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f292,plain,(
% 0.02/0.49    op(e1,e1)=e0|~sQ20_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f291])).
% 0.02/0.49  fof(f294,definition,(
% 0.02/0.49    sQ21_spl <=> (op(e1,e1)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f297,definition,(
% 0.02/0.49    sQ22_spl <=> (op(e1,e1)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f298,plain,(
% 0.02/0.49    op(e1,e1)=e2|~sQ22_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f297])).
% 0.02/0.49  fof(f300,definition,(
% 0.02/0.49    sQ23_spl <=> (op(e1,e1)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f301,plain,(
% 0.02/0.49    op(e1,e1)=e3|~sQ23_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f300])).
% 0.02/0.49  fof(f303,plain,(
% 0.02/0.49    sQ20_spl|sQ21_spl|sQ22_spl|sQ23_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f35,f291,f294,f297,f300])).
% 0.02/0.49  fof(f304,definition,(
% 0.02/0.49    sQ24_spl <=> (op(e1,e2)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f307,definition,(
% 0.02/0.49    sQ25_spl <=> (op(e1,e2)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f308,plain,(
% 0.02/0.49    op(e1,e2)=e1|~sQ25_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f307])).
% 0.02/0.49  fof(f310,definition,(
% 0.02/0.49    sQ26_spl <=> (op(e1,e2)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f311,plain,(
% 0.02/0.49    op(e1,e2)=e2|~sQ26_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f310])).
% 0.02/0.49  fof(f312,plain,(
% 0.02/0.49    ~op(e1,e2)=e2|sQ26_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f310])).
% 0.02/0.49  fof(f313,definition,(
% 0.02/0.49    sQ27_spl <=> (op(e1,e2)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f317,definition,(
% 0.02/0.49    sQ28_spl <=> (op(e1,e3)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f318,plain,(
% 0.02/0.49    op(e1,e3)=e0|~sQ28_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f317])).
% 0.02/0.49  fof(f320,definition,(
% 0.02/0.49    sQ29_spl <=> (op(e1,e3)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f321,plain,(
% 0.02/0.49    op(e1,e3)=e1|~sQ29_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f320])).
% 0.02/0.49  fof(f323,definition,(
% 0.02/0.49    sQ30_spl <=> (op(e1,e3)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f324,plain,(
% 0.02/0.49    op(e1,e3)=e2|~sQ30_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f323])).
% 0.02/0.49  fof(f326,definition,(
% 0.02/0.49    sQ31_spl <=> (op(e1,e3)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f327,plain,(
% 0.02/0.49    op(e1,e3)=e3|~sQ31_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f326])).
% 0.02/0.49  fof(f329,plain,(
% 0.02/0.49    sQ28_spl|sQ29_spl|sQ30_spl|sQ31_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f37,f317,f320,f323,f326])).
% 0.02/0.49  fof(f330,definition,(
% 0.02/0.49    sQ32_spl <=> (op(e2,e0)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f331,plain,(
% 0.02/0.49    op(e2,e0)=e0|~sQ32_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f330])).
% 0.02/0.49  fof(f333,definition,(
% 0.02/0.49    sQ33_spl <=> (op(e2,e0)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f334,plain,(
% 0.02/0.49    op(e2,e0)=e1|~sQ33_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f333])).
% 0.02/0.49  fof(f336,definition,(
% 0.02/0.49    sQ34_spl <=> (op(e2,e0)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f337,plain,(
% 0.02/0.49    op(e2,e0)=e2|~sQ34_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f336])).
% 0.02/0.49  fof(f339,definition,(
% 0.02/0.49    sQ35_spl <=> (op(e2,e0)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f340,plain,(
% 0.02/0.49    op(e2,e0)=e3|~sQ35_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f339])).
% 0.02/0.49  fof(f342,plain,(
% 0.02/0.49    sQ32_spl|sQ33_spl|sQ34_spl|sQ35_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f38,f330,f333,f336,f339])).
% 0.02/0.49  fof(f343,definition,(
% 0.02/0.49    sQ36_spl <=> (op(e2,e1)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f344,plain,(
% 0.02/0.49    op(e2,e1)=e0|~sQ36_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f343])).
% 0.02/0.49  fof(f346,definition,(
% 0.02/0.49    sQ37_spl <=> (op(e2,e1)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f347,plain,(
% 0.02/0.49    op(e2,e1)=e1|~sQ37_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f346])).
% 0.02/0.49  fof(f349,definition,(
% 0.02/0.49    sQ38_spl <=> (op(e2,e1)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f350,plain,(
% 0.02/0.49    op(e2,e1)=e2|~sQ38_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f349])).
% 0.02/0.49  fof(f352,definition,(
% 0.02/0.49    sQ39_spl <=> (op(e2,e1)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f353,plain,(
% 0.02/0.49    op(e2,e1)=e3|~sQ39_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f352])).
% 0.02/0.49  fof(f355,plain,(
% 0.02/0.49    sQ36_spl|sQ37_spl|sQ38_spl|sQ39_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f39,f343,f346,f349,f352])).
% 0.02/0.49  fof(f356,definition,(
% 0.02/0.49    sQ40_spl <=> (op(e2,e2)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f357,plain,(
% 0.02/0.49    op(e2,e2)=e0|~sQ40_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f356])).
% 0.02/0.49  fof(f359,definition,(
% 0.02/0.49    sQ41_spl <=> (op(e2,e2)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f360,plain,(
% 0.02/0.49    op(e2,e2)=e1|~sQ41_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f359])).
% 0.02/0.49  fof(f362,definition,(
% 0.02/0.49    sQ42_spl <=> (op(e2,e2)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f365,definition,(
% 0.02/0.49    sQ43_spl <=> (op(e2,e2)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f366,plain,(
% 0.02/0.49    op(e2,e2)=e3|~sQ43_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f365])).
% 0.02/0.49  fof(f369,definition,(
% 0.02/0.49    sQ44_spl <=> (op(e2,e3)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f370,plain,(
% 0.02/0.49    op(e2,e3)=e0|~sQ44_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f369])).
% 0.02/0.49  fof(f372,definition,(
% 0.02/0.49    sQ45_spl <=> (op(e2,e3)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f373,plain,(
% 0.02/0.49    op(e2,e3)=e1|~sQ45_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f372])).
% 0.02/0.49  fof(f375,definition,(
% 0.02/0.49    sQ46_spl <=> (op(e2,e3)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f376,plain,(
% 0.02/0.49    op(e2,e3)=e2|~sQ46_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f375])).
% 0.02/0.49  fof(f378,definition,(
% 0.02/0.49    sQ47_spl <=> (op(e2,e3)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f379,plain,(
% 0.02/0.49    op(e2,e3)=e3|~sQ47_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f378])).
% 0.02/0.49  fof(f381,plain,(
% 0.02/0.49    sQ44_spl|sQ45_spl|sQ46_spl|sQ47_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f41,f369,f372,f375,f378])).
% 0.02/0.49  fof(f382,definition,(
% 0.02/0.49    sQ48_spl <=> (op(e3,e0)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f383,plain,(
% 0.02/0.49    op(e3,e0)=e0|~sQ48_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f382])).
% 0.02/0.49  fof(f385,definition,(
% 0.02/0.49    sQ49_spl <=> (op(e3,e0)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f388,definition,(
% 0.02/0.49    sQ50_spl <=> (op(e3,e0)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f389,plain,(
% 0.02/0.49    op(e3,e0)=e2|~sQ50_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f388])).
% 0.02/0.49  fof(f391,definition,(
% 0.02/0.49    sQ51_spl <=> (op(e3,e0)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f392,plain,(
% 0.02/0.49    op(e3,e0)=e3|~sQ51_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f391])).
% 0.02/0.49  fof(f394,plain,(
% 0.02/0.49    sQ48_spl|sQ49_spl|sQ50_spl|sQ51_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f42,f382,f385,f388,f391])).
% 0.02/0.49  fof(f395,definition,(
% 0.02/0.49    sQ52_spl <=> (op(e3,e1)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f396,plain,(
% 0.02/0.49    op(e3,e1)=e0|~sQ52_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f395])).
% 0.02/0.49  fof(f398,definition,(
% 0.02/0.49    sQ53_spl <=> (op(e3,e1)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f399,plain,(
% 0.02/0.49    op(e3,e1)=e1|~sQ53_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f398])).
% 0.02/0.49  fof(f401,definition,(
% 0.02/0.49    sQ54_spl <=> (op(e3,e1)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f404,definition,(
% 0.02/0.49    sQ55_spl <=> (op(e3,e1)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f405,plain,(
% 0.02/0.49    op(e3,e1)=e3|~sQ55_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f404])).
% 0.02/0.49  fof(f407,plain,(
% 0.02/0.49    sQ52_spl|sQ53_spl|sQ54_spl|sQ55_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f43,f395,f398,f401,f404])).
% 0.02/0.49  fof(f408,definition,(
% 0.02/0.49    sQ56_spl <=> (op(e3,e2)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f409,plain,(
% 0.02/0.49    op(e3,e2)=e0|~sQ56_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f408])).
% 0.02/0.49  fof(f411,definition,(
% 0.02/0.49    sQ57_spl <=> (op(e3,e2)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f412,plain,(
% 0.02/0.49    op(e3,e2)=e1|~sQ57_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f411])).
% 0.02/0.49  fof(f414,definition,(
% 0.02/0.49    sQ58_spl <=> (op(e3,e2)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f415,plain,(
% 0.02/0.49    op(e3,e2)=e2|~sQ58_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f414])).
% 0.02/0.49  fof(f417,definition,(
% 0.02/0.49    sQ59_spl <=> (op(e3,e2)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f418,plain,(
% 0.02/0.49    op(e3,e2)=e3|~sQ59_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f417])).
% 0.02/0.49  fof(f420,plain,(
% 0.02/0.49    sQ56_spl|sQ57_spl|sQ58_spl|sQ59_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f44,f408,f411,f414,f417])).
% 0.02/0.49  fof(f421,definition,(
% 0.02/0.49    sQ60_spl <=> (op(e3,e3)=e0)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f422,plain,(
% 0.02/0.49    op(e3,e3)=e0|~sQ60_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f421])).
% 0.02/0.49  fof(f424,definition,(
% 0.02/0.49    sQ61_spl <=> (op(e3,e3)=e1)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f425,plain,(
% 0.02/0.49    op(e3,e3)=e1|~sQ61_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f424])).
% 0.02/0.49  fof(f427,definition,(
% 0.02/0.49    sQ62_spl <=> (op(e3,e3)=e2)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f428,plain,(
% 0.02/0.49    op(e3,e3)=e2|~sQ62_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f427])).
% 0.02/0.49  fof(f430,definition,(
% 0.02/0.49    sQ63_spl <=> (op(e3,e3)=e3)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f431,plain,(
% 0.02/0.49    op(e3,e3)=e3|~sQ63_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f430])).
% 0.02/0.49  fof(f433,plain,(
% 0.02/0.49    sQ60_spl|sQ61_spl|sQ62_spl|sQ63_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f45,f421,f424,f427,f430])).
% 0.02/0.49  fof(f434,plain,(
% 0.02/0.49    sQ0_spl|sQ4_spl|sQ8_spl|sQ12_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f46,f226,f239,f252,f265])).
% 0.02/0.49  fof(f436,plain,(
% 0.02/0.49    sQ1_spl|sQ5_spl|sQ9_spl|sQ13_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f48,f229,f242,f255,f268])).
% 0.02/0.49  fof(f437,plain,(
% 0.02/0.49    sQ1_spl|sQ17_spl|sQ33_spl|sQ49_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f49,f229,f281,f333,f385])).
% 0.02/0.49  fof(f442,plain,(
% 0.02/0.49    sQ16_spl|sQ20_spl|sQ24_spl|sQ28_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f54,f278,f291,f304,f317])).
% 0.02/0.49  fof(f443,plain,(
% 0.02/0.49    sQ4_spl|sQ20_spl|sQ36_spl|sQ52_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f55,f239,f291,f343,f395])).
% 0.02/0.49  fof(f445,plain,(
% 0.02/0.49    sQ5_spl|sQ21_spl|sQ37_spl|sQ53_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f57,f242,f294,f346,f398])).
% 0.02/0.49  fof(f449,plain,(
% 0.02/0.49    sQ7_spl|sQ23_spl|sQ39_spl|sQ55_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f61,f248,f300,f352,f404])).
% 0.02/0.49  fof(f450,plain,(
% 0.02/0.49    sQ32_spl|sQ36_spl|sQ40_spl|sQ44_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f62,f330,f343,f356,f369])).
% 0.02/0.49  fof(f451,plain,(
% 0.02/0.49    sQ8_spl|sQ24_spl|sQ40_spl|sQ56_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f63,f252,f304,f356,f408])).
% 0.02/0.49  fof(f452,plain,(
% 0.02/0.49    sQ33_spl|sQ37_spl|sQ41_spl|sQ45_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f64,f333,f346,f359,f372])).
% 0.02/0.49  fof(f453,plain,(
% 0.02/0.49    sQ9_spl|sQ25_spl|sQ41_spl|sQ57_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f65,f255,f307,f359,f411])).
% 0.02/0.49  fof(f455,plain,(
% 0.02/0.49    sQ10_spl|sQ26_spl|sQ42_spl|sQ58_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f67,f258,f310,f362,f414])).
% 0.02/0.49  fof(f456,plain,(
% 0.02/0.49    sQ35_spl|sQ39_spl|sQ43_spl|sQ47_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f68,f339,f352,f365,f378])).
% 0.02/0.49  fof(f458,plain,(
% 0.02/0.49    sQ48_spl|sQ52_spl|sQ56_spl|sQ60_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f70,f382,f395,f408,f421])).
% 0.02/0.49  fof(f459,plain,(
% 0.02/0.49    sQ12_spl|sQ28_spl|sQ44_spl|sQ60_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f71,f265,f317,f369,f421])).
% 0.02/0.49  fof(f462,plain,(
% 0.02/0.49    sQ50_spl|sQ54_spl|sQ58_spl|sQ62_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f74,f388,f401,f414,f427])).
% 0.02/0.49  fof(f465,plain,(
% 0.02/0.49    sQ15_spl|sQ31_spl|sQ47_spl|sQ63_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f77,f274,f326,f378,f430])).
% 0.02/0.49  fof(f466,definition,(
% 0.02/0.49    sQ64_spl <=> (sP0_prd)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f469,definition,(
% 0.02/0.49    sQ65_spl <=> (op(e3,op(e0,e3))=op(e0,e3))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f472,plain,(
% 0.02/0.49    sQ64_spl|sQ65_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f150,f466,f469])).
% 0.02/0.49  fof(f473,definition,(
% 0.02/0.49    sQ66_spl <=> (op(e3,op(e1,e3))=op(e1,e3))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f474,plain,(
% 0.02/0.49    op(e3,op(e1,e3))=op(e1,e3)|~sQ66_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f473])).
% 0.02/0.49  fof(f476,plain,(
% 0.02/0.49    sQ64_spl|sQ66_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f151,f466,f473])).
% 0.02/0.49  fof(f477,definition,(
% 0.02/0.49    sQ67_spl <=> (op(e3,op(e2,e3))=op(e2,e3))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f480,plain,(
% 0.02/0.49    sQ64_spl|sQ67_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f152,f466,f477])).
% 0.02/0.49  fof(f481,definition,(
% 0.02/0.49    sQ68_spl <=> (op(e3,op(e3,e3))=op(e3,e3))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f484,plain,(
% 0.02/0.49    sQ64_spl|sQ68_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f153,f466,f481])).
% 0.02/0.49  fof(f485,definition,(
% 0.02/0.49    sQ69_spl <=> (e0=op(op(e2,e1),op(e2,e1)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f487,plain,(
% 0.02/0.49    ~e0=op(op(e2,e1),op(e2,e1))|sQ69_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f485])).
% 0.02/0.49  fof(f488,plain,(
% 0.02/0.49    ~sQ69_spl|~sQ39_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f155,f485,f352])).
% 0.02/0.49  fof(f493,definition,(
% 0.02/0.49    sQ71_spl <=> (e0=op(op(e1,e2),op(e1,e2)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f496,plain,(
% 0.02/0.49    ~sQ71_spl|~sQ27_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f159,f493,f313])).
% 0.02/0.49  fof(f497,definition,(
% 0.02/0.49    sQ72_spl <=> (e0=op(op(e3,e2),op(e3,e2)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f499,plain,(
% 0.02/0.49    ~e0=op(op(e3,e2),op(e3,e2))|sQ72_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f497])).
% 0.02/0.49  fof(f500,plain,(
% 0.02/0.49    ~sQ72_spl|~sQ57_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f161,f497,f411])).
% 0.02/0.49  fof(f505,definition,(
% 0.02/0.49    sQ74_spl <=> (e0=op(op(e2,e3),op(e2,e3)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f508,plain,(
% 0.02/0.49    ~sQ74_spl|~sQ45_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f165,f505,f372])).
% 0.02/0.49  fof(f513,definition,(
% 0.02/0.49    sQ76_spl <=> (e1=op(op(e3,e0),op(e3,e0)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f515,plain,(
% 0.02/0.49    ~e1=op(op(e3,e0),op(e3,e0))|sQ76_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f513])).
% 0.02/0.49  fof(f516,plain,(
% 0.02/0.49    ~sQ76_spl|~sQ50_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f169,f513,f388])).
% 0.02/0.49  fof(f521,definition,(
% 0.02/0.49    sQ78_spl <=> (e1=op(op(e3,e2),op(e3,e2)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f524,plain,(
% 0.02/0.49    ~sQ78_spl|~sQ56_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f173,f521,f408])).
% 0.02/0.49  fof(f529,definition,(
% 0.02/0.49    sQ80_spl <=> (e1=op(op(e2,e3),op(e2,e3)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f531,plain,(
% 0.02/0.49    ~e1=op(op(e2,e3),op(e2,e3))|sQ80_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f529])).
% 0.02/0.49  fof(f532,plain,(
% 0.02/0.49    ~sQ80_spl|~sQ44_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f177,f529,f369])).
% 0.02/0.49  fof(f541,definition,(
% 0.02/0.49    sQ83_spl <=> (e2=op(op(e0,e1),op(e0,e1)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f543,plain,(
% 0.02/0.49    ~e2=op(op(e0,e1),op(e0,e1))|sQ83_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f541])).
% 0.02/0.49  fof(f544,plain,(
% 0.02/0.49    ~sQ83_spl|~sQ7_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f183,f541,f248])).
% 0.02/0.49  fof(f553,definition,(
% 0.02/0.49    sQ86_spl <=> (e2=op(op(e1,e3),op(e1,e3)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f555,plain,(
% 0.02/0.49    ~e2=op(op(e1,e3),op(e1,e3))|sQ86_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f553])).
% 0.02/0.49  fof(f556,plain,(
% 0.02/0.49    ~sQ86_spl|~sQ28_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f189,f553,f317])).
% 0.02/0.49  fof(f565,definition,(
% 0.02/0.49    sQ89_spl <=> (e3=op(op(e0,e1),op(e0,e1)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f567,plain,(
% 0.02/0.49    ~e3=op(op(e0,e1),op(e0,e1))|sQ89_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f565])).
% 0.02/0.49  fof(f568,plain,(
% 0.02/0.49    ~sQ89_spl|~sQ6_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f195,f565,f245])).
% 0.02/0.49  fof(f573,definition,(
% 0.02/0.49    sQ91_spl <=> (e3=op(op(e0,e2),op(e0,e2)))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f575,plain,(
% 0.02/0.49    ~e3=op(op(e0,e2),op(e0,e2))|sQ91_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f573])).
% 0.02/0.49  fof(f576,plain,(
% 0.02/0.49    ~sQ91_spl|~sQ9_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f199,f573,f255])).
% 0.02/0.49  fof(f581,definition,(
% 0.02/0.49    sQ93_spl <=> (sP1_prd)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f584,definition,(
% 0.02/0.49    sQ94_spl <=> (op(e2,op(e0,e2))=op(e0,e2))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f585,plain,(
% 0.02/0.49    op(e2,op(e0,e2))=op(e0,e2)|~sQ94_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f584])).
% 0.02/0.49  fof(f587,plain,(
% 0.02/0.49    ~sQ64_spl|sQ93_spl|sQ94_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f205,f466,f581,f584])).
% 0.02/0.49  fof(f600,plain,(
% 0.02/0.49    sQ64_spl|~sQ93_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f209,f466,f581])).
% 0.02/0.49  fof(f602,definition,(
% 0.02/0.49    sQ98_spl <=> (sP2_prd)),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f605,definition,(
% 0.02/0.49    sQ99_spl <=> (op(e1,op(e0,e1))=op(e0,e1))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f606,plain,(
% 0.02/0.49    op(e1,op(e0,e1))=op(e0,e1)|~sQ99_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f605])).
% 0.02/0.49  fof(f608,plain,(
% 0.02/0.49    ~sQ93_spl|sQ98_spl|sQ99_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f214,f581,f602,f605])).
% 0.02/0.49  fof(f621,plain,(
% 0.02/0.49    sQ93_spl|~sQ98_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f218,f581,f602])).
% 0.02/0.49  fof(f623,definition,(
% 0.02/0.49    sQ103_spl <=> (op(e0,op(e0,e0))=op(e0,e0))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f624,plain,(
% 0.02/0.49    op(e0,op(e0,e0))=op(e0,e0)|~sQ103_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f623])).
% 0.02/0.49  fof(f626,plain,(
% 0.02/0.49    ~sQ98_spl|sQ103_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f221,f602,f623])).
% 0.02/0.49  fof(f627,definition,(
% 0.02/0.49    sQ104_spl <=> (op(e0,op(e1,e0))=op(e1,e0))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f628,plain,(
% 0.02/0.49    op(e0,op(e1,e0))=op(e1,e0)|~sQ104_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f627])).
% 0.02/0.49  fof(f630,plain,(
% 0.02/0.49    ~sQ98_spl|sQ104_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f222,f602,f627])).
% 0.02/0.49  fof(f631,definition,(
% 0.02/0.49    sQ105_spl <=> (op(e0,op(e2,e0))=op(e2,e0))),
% 0.02/0.49    introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.02/0.49  fof(f632,plain,(
% 0.02/0.49    op(e0,op(e2,e0))=op(e2,e0)|~sQ105_spl),
% 0.02/0.49    inference(component_clause,[status(thm)],[f631])).
% 0.02/0.49  fof(f634,plain,(
% 0.02/0.49    ~sQ98_spl|sQ105_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f223,f602,f631])).
% 0.02/0.49  fof(f640,plain,(
% 0.02/0.49    ~e0=op(e3,e0)|~sQ16_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f279,f82])).
% 0.02/0.49  fof(f641,plain,(
% 0.02/0.49    ~e0=op(e2,e0)|~sQ16_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f279,f81])).
% 0.02/0.49  fof(f642,plain,(
% 0.02/0.49    ~op(e0,e0)=e0|~sQ16_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f279,f78])).
% 0.02/0.49  fof(f643,plain,(
% 0.02/0.49    ~e1=op(e3,e0)|~sQ1_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f230,f80])).
% 0.02/0.49  fof(f646,plain,(
% 0.02/0.49    ~e0=op(e2,e1)|~sQ4_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f240,f85])).
% 0.02/0.49  fof(f648,plain,(
% 0.02/0.49    ~e0=op(e3,e0)|~sQ32_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f331,f83])).
% 0.02/0.49  fof(f652,plain,(
% 0.02/0.49    ~op(e0,e0)=e0|~sQ32_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f331,f79])).
% 0.02/0.49  fof(f653,plain,(
% 0.02/0.49    ~e0=op(e3,e2)|~sQ8_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f253,f92])).
% 0.02/0.49  fof(f655,plain,(
% 0.02/0.49    ~e0=op(e1,e2)|~sQ8_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f253,f90])).
% 0.02/0.49  fof(f657,plain,(
% 0.02/0.49    ~e0=op(e2,e3)|~sQ12_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f266,f97])).
% 0.02/0.49  fof(f660,plain,(
% 0.02/0.49    ~op(e1,e3)=e2|~sQ46_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f376,f99])).
% 0.02/0.49  fof(f666,plain,(
% 0.02/0.49    ~e2=op(e3,e3)|~sQ46_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f376,f101])).
% 0.02/0.49  fof(f667,plain,(
% 0.02/0.49    ~e2=op(e3,e1)|~sQ22_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f298,f88])).
% 0.02/0.49  fof(f668,plain,(
% 0.02/0.49    ~e3=op(e0,e1)|~sQ3_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f236,f102])).
% 0.02/0.49  fof(f671,plain,(
% 0.02/0.49    ~op(e1,e2)=e2|~sQ58_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f415,f94])).
% 0.02/0.49  fof(f672,plain,(
% 0.02/0.49    ~e3=op(e0,e2)|~sQ3_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f236,f103])).
% 0.02/0.49  fof(f681,plain,(
% 0.02/0.49    e2=e0|~sQ22_spl|~sQ20_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f298,f292])).
% 0.02/0.49  fof(f682,plain,(
% 0.02/0.49    $false|~sQ22_spl|~sQ20_spl),
% 0.02/0.49    inference(forward_subsumption_resolution,[status(thm)],[f681,f127])).
% 0.02/0.49  fof(f683,plain,(
% 0.02/0.49    ~sQ22_spl|~sQ20_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f682])).
% 0.02/0.49  fof(f686,plain,(
% 0.02/0.49    ~op(e0,e1)=e1|~sQ53_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f399,f86])).
% 0.02/0.49  fof(f710,plain,(
% 0.02/0.49    ~e0=op(e1,e3)|~sQ16_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f279,f110])).
% 0.02/0.49  fof(f713,plain,(
% 0.02/0.49    ~e3=op(e1,e2)|~sQ23_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f301,f111])).
% 0.02/0.49  fof(f722,plain,(
% 0.02/0.49    ~op(e1,e0)=e1|~sQ29_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f321,f110])).
% 0.02/0.49  fof(f730,plain,(
% 0.02/0.49    ~e0=e0|~sQ48_spl|~sQ16_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f383,f640])).
% 0.02/0.49  fof(f731,plain,(
% 0.02/0.49    $false|~sQ48_spl|~sQ16_spl),
% 0.02/0.49    inference(trivial_equality_resolution,[status(thm)],[f730])).
% 0.02/0.49  fof(f732,plain,(
% 0.02/0.49    ~sQ48_spl|~sQ16_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f731])).
% 0.02/0.49  fof(f733,plain,(
% 0.02/0.49    ~op(e1,e1)=e1|~sQ29_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f321,f112])).
% 0.02/0.49  fof(f735,plain,(
% 0.02/0.49    ~e1=op(e1,e3)|~sQ25_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f308,f113])).
% 0.02/0.49  fof(f736,plain,(
% 0.02/0.49    ~e1=e1|~sQ29_spl|~sQ25_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f321,f735])).
% 0.02/0.49  fof(f737,plain,(
% 0.02/0.49    $false|~sQ29_spl|~sQ25_spl),
% 0.02/0.49    inference(trivial_equality_resolution,[status(thm)],[f736])).
% 0.02/0.49  fof(f738,plain,(
% 0.02/0.49    ~sQ29_spl|~sQ25_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f737])).
% 0.02/0.49  fof(f739,plain,(
% 0.02/0.49    e3=e1|~sQ43_spl|~sQ41_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f366,f360])).
% 0.02/0.49  fof(f740,plain,(
% 0.02/0.49    $false|~sQ43_spl|~sQ41_spl),
% 0.02/0.49    inference(forward_subsumption_resolution,[status(thm)],[f739,f130])).
% 0.02/0.49  fof(f741,plain,(
% 0.02/0.49    ~sQ43_spl|~sQ41_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f740])).
% 0.02/0.49  fof(f747,plain,(
% 0.02/0.49    ~op(e2,e0)=e2|~sQ46_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f376,f116])).
% 0.02/0.49  fof(f749,plain,(
% 0.02/0.49    ~e1=op(e2,e3)|~sQ37_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f347,f118])).
% 0.02/0.49  fof(f752,plain,(
% 0.02/0.49    ~op(e2,e2)=e2|~sQ46_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f376,f119])).
% 0.02/0.49  fof(f754,plain,(
% 0.02/0.49    ~op(e3,e0)=e1|~sQ53_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f399,f120])).
% 0.02/0.49  fof(f755,plain,(
% 0.02/0.49    ~op(e3,e0)=e2|~sQ58_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f415,f121])).
% 0.02/0.49  fof(f757,plain,(
% 0.02/0.49    ~e1=op(e3,e2)|~sQ53_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f399,f123])).
% 0.02/0.49  fof(f764,plain,(
% 0.02/0.49    op(e2,e0)=e2|~sQ10_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f259,f136])).
% 0.02/0.49  fof(f765,plain,(
% 0.02/0.49    $false|~sQ46_spl|~sQ10_spl),
% 0.02/0.49    inference(forward_subsumption_resolution,[status(thm)],[f764,f747])).
% 0.02/0.49  fof(f766,plain,(
% 0.02/0.49    ~sQ46_spl|~sQ10_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f765])).
% 0.02/0.49  fof(f768,plain,(
% 0.02/0.49    sQ34_spl|~sQ10_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f764,f336,f258])).
% 0.02/0.49  fof(f783,plain,(
% 0.02/0.49    ~sQ11_spl|~sQ3_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f672,f261,f235])).
% 0.02/0.49  fof(f784,plain,(
% 0.02/0.49    ~sQ7_spl|~sQ3_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f668,f248,f235])).
% 0.02/0.49  fof(f785,plain,(
% 0.02/0.49    op(e3,e0)=e0|~sQ12_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f786,f134])).
% 0.02/0.49  fof(f786,plain,(
% 0.02/0.49    op(e0,e0)=e3|~sQ12_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f266,f137])).
% 0.02/0.49  fof(f787,plain,(
% 0.02/0.49    sQ48_spl|~sQ12_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f785,f382,f265])).
% 0.02/0.49  fof(f789,plain,(
% 0.02/0.49    op(e1,e1)=e2|~sQ37_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f791,f140])).
% 0.02/0.49  fof(f791,plain,(
% 0.02/0.49    op(e1,e2)=e1|~sQ37_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f347,f143])).
% 0.02/0.49  fof(f792,plain,(
% 0.02/0.49    sQ22_spl|~sQ37_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f789,f297,f346])).
% 0.02/0.49  fof(f793,plain,(
% 0.02/0.49    ~sQ5_spl|~sQ53_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f686,f242,f398])).
% 0.02/0.49  fof(f794,plain,(
% 0.02/0.49    e1=e0|~sQ37_spl|~sQ36_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f347,f344])).
% 0.02/0.49  fof(f795,plain,(
% 0.02/0.49    $false|~sQ37_spl|~sQ36_spl),
% 0.02/0.49    inference(forward_subsumption_resolution,[status(thm)],[f794,f126])).
% 0.02/0.49  fof(f796,plain,(
% 0.02/0.49    ~sQ37_spl|~sQ36_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f795])).
% 0.02/0.49  fof(f798,plain,(
% 0.02/0.49    ~e3=op(e3,e3)|~sQ51_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f392,f122])).
% 0.02/0.49  fof(f799,plain,(
% 0.02/0.49    op(e3,e3)=e0|~sQ51_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f392,f146])).
% 0.02/0.49  fof(f800,plain,(
% 0.02/0.49    e1=e0|~sQ1_spl|~sQ0_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f230,f227])).
% 0.02/0.49  fof(f801,plain,(
% 0.02/0.49    $false|~sQ1_spl|~sQ0_spl),
% 0.02/0.49    inference(forward_subsumption_resolution,[status(thm)],[f800,f126])).
% 0.02/0.49  fof(f802,plain,(
% 0.02/0.49    ~sQ1_spl|~sQ0_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f801])).
% 0.02/0.49  fof(f806,plain,(
% 0.02/0.49    op(e0,e3)=e3|~sQ51_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f799,f149])).
% 0.02/0.49  fof(f807,plain,(
% 0.02/0.49    op(e3,e1)=e3|~sQ31_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f327,f141])).
% 0.02/0.49  fof(f812,plain,(
% 0.02/0.49    e1=e0|~sQ61_spl|~sQ51_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f425,f799])).
% 0.02/0.49  fof(f813,plain,(
% 0.02/0.49    $false|~sQ61_spl|~sQ51_spl),
% 0.02/0.49    inference(forward_subsumption_resolution,[status(thm)],[f812,f126])).
% 0.02/0.49  fof(f814,plain,(
% 0.02/0.49    ~sQ61_spl|~sQ51_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f813])).
% 0.02/0.49  fof(f818,plain,(
% 0.02/0.49    ~sQ49_spl|~sQ1_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f643,f385,f229])).
% 0.02/0.49  fof(f822,plain,(
% 0.02/0.49    ~sQ50_spl|~sQ58_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f755,f388,f414])).
% 0.02/0.49  fof(f825,plain,(
% 0.02/0.49    op(e3,e3)=op(e1,e3)|~sQ31_spl|~sQ66_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f327,f474])).
% 0.02/0.49  fof(f826,plain,(
% 0.02/0.49    op(e3,e3)=e3|~sQ31_spl|~sQ66_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f327,f825])).
% 0.02/0.49  fof(f840,plain,(
% 0.02/0.49    ~sQ24_spl|~sQ8_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f655,f304,f252])).
% 0.02/0.49  fof(f841,plain,(
% 0.02/0.49    ~sQ49_spl|~sQ53_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f754,f385,f398])).
% 0.02/0.49  fof(f843,plain,(
% 0.02/0.49    ~sQ30_spl|~sQ46_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f660,f323,f375])).
% 0.02/0.49  fof(f847,plain,(
% 0.02/0.49    op(e3,e3)=e2|~sQ59_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f418,f148])).
% 0.02/0.49  fof(f848,plain,(
% 0.02/0.49    op(e3,e2)=e3|~sQ47_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f379,f145])).
% 0.02/0.49  fof(f853,plain,(
% 0.02/0.49    ~op(e0,e2)=e1|~sQ41_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f360,f91])).
% 0.02/0.49  fof(f854,plain,(
% 0.02/0.49    op(e1,e2)=e2|~sQ41_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f360,f144])).
% 0.02/0.49  fof(f855,plain,(
% 0.02/0.49    ~op(e2,e0)=e1|~sQ41_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f360,f115])).
% 0.02/0.49  fof(f858,plain,(
% 0.02/0.49    ~e2=op(e1,e3)|~sQ26_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f311,f113])).
% 0.02/0.49  fof(f860,plain,(
% 0.02/0.49    ~op(e1,e1)=e2|~sQ26_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f311,f111])).
% 0.02/0.49  fof(f861,plain,(
% 0.02/0.49    e3=e1|~sQ15_spl|~sQ13_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f275,f269])).
% 0.02/0.49  fof(f862,plain,(
% 0.02/0.49    $false|~sQ15_spl|~sQ13_spl),
% 0.02/0.49    inference(forward_subsumption_resolution,[status(thm)],[f861,f130])).
% 0.02/0.49  fof(f863,plain,(
% 0.02/0.49    ~sQ15_spl|~sQ13_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f862])).
% 0.02/0.49  fof(f865,plain,(
% 0.02/0.49    e2=e1|~sQ62_spl|~sQ61_spl),
% 0.02/0.49    inference(forward_demodulation,[status(thm)],[f428,f425])).
% 0.02/0.49  fof(f866,plain,(
% 0.02/0.49    $false|~sQ62_spl|~sQ61_spl),
% 0.02/0.49    inference(forward_subsumption_resolution,[status(thm)],[f865,f129])).
% 0.02/0.49  fof(f867,plain,(
% 0.02/0.49    ~sQ62_spl|~sQ61_spl),
% 0.02/0.49    inference(contradiction_clause,[status(thm)],[f866])).
% 0.02/0.49  fof(f868,plain,(
% 0.02/0.49    ~sQ54_spl|~sQ22_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f667,f401,f297])).
% 0.02/0.49  fof(f873,plain,(
% 0.02/0.49    ~sQ21_spl|~sQ29_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f733,f294,f320])).
% 0.02/0.49  fof(f891,plain,(
% 0.02/0.49    ~sQ27_spl|~sQ23_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f713,f313,f300])).
% 0.02/0.49  fof(f895,plain,(
% 0.02/0.49    ~op(e1,e2)=e0|~sQ40_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f357,f93])).
% 0.02/0.49  fof(f896,plain,(
% 0.02/0.49    ~sQ24_spl|~sQ40_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f895,f304,f356])).
% 0.02/0.49  fof(f897,plain,(
% 0.02/0.49    ~op(e1,e0)=e2|~sQ34_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f337,f81])).
% 0.02/0.49  fof(f899,plain,(
% 0.02/0.49    op(e2,e2)=e0|~sQ34_spl),
% 0.02/0.49    inference(backward_demodulation,[status(thm)],[f337,f142])).
% 0.02/0.49  fof(f900,plain,(
% 0.02/0.49    ~sQ18_spl|~sQ34_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f897,f284,f336])).
% 0.02/0.49  fof(f902,plain,(
% 0.02/0.49    sQ40_spl|~sQ34_spl),
% 0.02/0.49    inference(split_clause,[status(thm)],[f899,f356,f336])).
% 0.02/0.50  fof(f903,plain,(
% 0.02/0.50    sQ59_spl|~sQ47_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f848,f417,f378])).
% 0.02/0.50  fof(f904,plain,(
% 0.02/0.50    ~sQ9_spl|~sQ41_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f853,f255,f359])).
% 0.02/0.50  fof(f906,plain,(
% 0.02/0.50    sQ26_spl|~sQ41_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f854,f310,f359])).
% 0.02/0.50  fof(f907,plain,(
% 0.02/0.50    op(e0,e3)=e1|~sQ52_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f396,f147])).
% 0.02/0.50  fof(f911,plain,(
% 0.02/0.50    ~e1=op(e1,e1)|~sQ5_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f243,f84])).
% 0.02/0.50  fof(f912,plain,(
% 0.02/0.50    ~e1=op(e0,e2)|~sQ5_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f243,f105])).
% 0.02/0.50  fof(f913,plain,(
% 0.02/0.50    op(e1,e0)=e1|~sQ5_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f243,f135])).
% 0.02/0.50  fof(f914,plain,(
% 0.02/0.50    ~sQ21_spl|~sQ5_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f911,f294,f242])).
% 0.02/0.50  fof(f915,plain,(
% 0.02/0.50    sQ17_spl|~sQ5_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f913,f281,f242])).
% 0.02/0.50  fof(f917,plain,(
% 0.02/0.50    ~sQ57_spl|~sQ53_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f757,f411,f398])).
% 0.02/0.50  fof(f925,plain,(
% 0.02/0.50    ~op(e2,e2)=e1|~sQ57_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f412,f95])).
% 0.02/0.50  fof(f931,plain,(
% 0.02/0.50    ~e0=op(e3,e2)|~sQ52_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f396,f123])).
% 0.02/0.50  fof(f933,plain,(
% 0.02/0.50    ~op(e3,e0)=e0|~sQ52_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f396,f120])).
% 0.02/0.50  fof(f934,plain,(
% 0.02/0.50    ~op(e1,e1)=e0|~sQ52_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f396,f88])).
% 0.02/0.50  fof(f936,plain,(
% 0.02/0.50    ~e0=op(e2,e3)|~sQ28_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f318,f99])).
% 0.02/0.50  fof(f938,plain,(
% 0.02/0.50    ~op(e1,e1)=e0|~sQ28_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f318,f112])).
% 0.02/0.50  fof(f941,plain,(
% 0.02/0.50    ~op(e2,e3)=e3|~sQ63_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f431,f101])).
% 0.02/0.50  fof(f945,plain,(
% 0.02/0.50    ~op(e2,e2)=e1|~sQ45_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f373,f119])).
% 0.02/0.50  fof(f952,plain,(
% 0.02/0.50    op(e0,e0)=e2|~sQ8_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f253,f136])).
% 0.02/0.50  fof(f953,plain,(
% 0.02/0.50    sQ2_spl|~sQ8_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f952,f232,f252])).
% 0.02/0.50  fof(f954,plain,(
% 0.02/0.50    e3=e0|~sQ63_spl|~sQ60_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f431,f422])).
% 0.02/0.50  fof(f955,plain,(
% 0.02/0.50    $false|~sQ63_spl|~sQ60_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f954,f128])).
% 0.02/0.50  fof(f956,plain,(
% 0.02/0.50    ~sQ63_spl|~sQ60_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f955])).
% 0.02/0.50  fof(f961,plain,(
% 0.02/0.50    ~sQ56_spl|~sQ52_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f931,f408,f395])).
% 0.02/0.50  fof(f962,plain,(
% 0.02/0.50    sQ63_spl|~sQ31_spl|~sQ66_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f826,f430,f326,f473])).
% 0.02/0.50  fof(f963,plain,(
% 0.02/0.50    ~sQ0_spl|~sQ16_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f642,f226,f278])).
% 0.02/0.50  fof(f968,plain,(
% 0.02/0.50    ~sQ26_spl|~sQ58_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f671,f310,f414])).
% 0.02/0.50  fof(f969,plain,(
% 0.02/0.50    ~sQ9_spl|~sQ5_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f912,f255,f242])).
% 0.02/0.50  fof(f970,plain,(
% 0.02/0.50    sQ13_spl|~sQ52_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f907,f268,f395])).
% 0.02/0.50  fof(f971,plain,(
% 0.02/0.50    ~sQ48_spl|~sQ52_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f933,f382,f395])).
% 0.02/0.50  fof(f973,plain,(
% 0.02/0.50    ~sQ47_spl|~sQ63_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f941,f378,f430])).
% 0.02/0.50  fof(f974,plain,(
% 0.02/0.50    ~sQ63_spl|~sQ51_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f798,f430,f391])).
% 0.02/0.50  fof(f975,plain,(
% 0.02/0.50    sQ15_spl|~sQ51_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f806,f274,f391])).
% 0.02/0.50  fof(f976,plain,(
% 0.02/0.50    sQ60_spl|~sQ51_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f799,f421,f391])).
% 0.02/0.50  fof(f980,plain,(
% 0.02/0.50    ~sQ22_spl|~sQ26_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f860,f297,f310])).
% 0.02/0.50  fof(f985,plain,(
% 0.02/0.50    ~op(e0,e3)=e1|~sQ45_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f373,f97])).
% 0.02/0.50  fof(f989,plain,(
% 0.02/0.50    ~sQ42_spl|~sQ46_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f752,f362,f375])).
% 0.02/0.50  fof(f991,plain,(
% 0.02/0.50    sQ62_spl|~sQ59_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f847,f427,f417])).
% 0.02/0.50  fof(f997,plain,(
% 0.02/0.50    e2=e1|~sQ6_spl|~sQ5_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f246,f243])).
% 0.02/0.50  fof(f998,plain,(
% 0.02/0.50    $false|~sQ6_spl|~sQ5_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f997,f129])).
% 0.02/0.50  fof(f999,plain,(
% 0.02/0.50    ~sQ6_spl|~sQ5_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f998])).
% 0.02/0.50  fof(f1000,plain,(
% 0.02/0.50    ~sQ48_spl|~sQ32_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f648,f382,f330])).
% 0.02/0.50  fof(f1006,plain,(
% 0.02/0.50    ~e3=op(e2,e1)|~sQ35_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f340,f114])).
% 0.02/0.50  fof(f1013,plain,(
% 0.02/0.50    ~op(e1,e3)=e0|~sQ60_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f422,f100])).
% 0.02/0.50  fof(f1014,plain,(
% 0.02/0.50    ~op(e3,e0)=e0|~sQ60_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f422,f122])).
% 0.02/0.50  fof(f1015,plain,(
% 0.02/0.50    op(e0,e3)=e3|~sQ60_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f422,f149])).
% 0.02/0.50  fof(f1017,plain,(
% 0.02/0.50    ~op(e1,e0)=e3|~sQ35_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f340,f81])).
% 0.02/0.50  fof(f1021,plain,(
% 0.02/0.50    op(e3,e0)=e3|~sQ15_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f275,f137])).
% 0.02/0.50  fof(f1022,plain,(
% 0.02/0.50    op(e0,e3)=op(e2,e0)|~sQ35_spl|~sQ105_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f340,f632])).
% 0.02/0.50  fof(f1025,plain,(
% 0.02/0.50    op(e0,e3)=e2|~sQ35_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f1027,f148])).
% 0.02/0.50  fof(f1027,plain,(
% 0.02/0.50    op(e3,e2)=e0|~sQ35_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f340,f142])).
% 0.02/0.50  fof(f1028,plain,(
% 0.02/0.50    e3=e2|~sQ15_spl|~sQ35_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f275,f1025])).
% 0.02/0.50  fof(f1029,plain,(
% 0.02/0.50    $false|~sQ15_spl|~sQ35_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1028,f131])).
% 0.02/0.50  fof(f1030,plain,(
% 0.02/0.50    ~sQ15_spl|~sQ35_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1029])).
% 0.02/0.50  fof(f1031,plain,(
% 0.02/0.50    op(e0,e3)=e3|~sQ35_spl|~sQ105_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f340,f1022])).
% 0.02/0.50  fof(f1034,plain,(
% 0.02/0.50    op(e1,e0)=e0|~sQ1_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f230,f134])).
% 0.02/0.50  fof(f1040,plain,(
% 0.02/0.50    op(e1,e2)=e3|~sQ45_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f373,f145])).
% 0.02/0.50  fof(f1042,plain,(
% 0.02/0.50    sQ27_spl|~sQ45_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1040,f313,f372])).
% 0.02/0.50  fof(f1045,plain,(
% 0.02/0.50    e1=e0|~sQ45_spl|~sQ44_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f373,f370])).
% 0.02/0.50  fof(f1046,plain,(
% 0.02/0.50    $false|~sQ45_spl|~sQ44_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1045,f126])).
% 0.02/0.50  fof(f1047,plain,(
% 0.02/0.50    ~sQ45_spl|~sQ44_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1046])).
% 0.02/0.50  fof(f1054,plain,(
% 0.02/0.50    ~sQ28_spl|~sQ60_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1013,f317,f421])).
% 0.02/0.50  fof(f1055,plain,(
% 0.02/0.50    ~sQ48_spl|~sQ60_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1014,f382,f421])).
% 0.02/0.50  fof(f1056,plain,(
% 0.02/0.50    sQ15_spl|~sQ60_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1015,f274,f421])).
% 0.02/0.50  fof(f1058,plain,(
% 0.02/0.50    ~sQ39_spl|~sQ35_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1006,f352,f339])).
% 0.02/0.50  fof(f1059,plain,(
% 0.02/0.50    sQ14_spl|~sQ35_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1025,f271,f339])).
% 0.02/0.50  fof(f1060,plain,(
% 0.02/0.50    ~sQ19_spl|~sQ35_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1017,f287,f339])).
% 0.02/0.50  fof(f1064,plain,(
% 0.02/0.50    sQ3_spl|~sQ12_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f786,f235,f265])).
% 0.02/0.50  fof(f1066,plain,(
% 0.02/0.50    ~sQ17_spl|~sQ29_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f722,f281,f320])).
% 0.02/0.50  fof(f1067,plain,(
% 0.02/0.50    ~sQ62_spl|~sQ46_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f666,f427,f375])).
% 0.02/0.50  fof(f1068,plain,(
% 0.02/0.50    ~sQ34_spl|~sQ46_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f747,f336,f375])).
% 0.02/0.50  fof(f1069,plain,(
% 0.02/0.50    sQ51_spl|~sQ15_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1021,f391,f274])).
% 0.02/0.50  fof(f1071,plain,(
% 0.02/0.50    ~sQ41_spl|~sQ57_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f925,f359,f411])).
% 0.02/0.50  fof(f1074,plain,(
% 0.02/0.50    ~op(e1,e2)=e0|~sQ28_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f318,f113])).
% 0.02/0.50  fof(f1075,plain,(
% 0.02/0.50    op(e0,e1)=e3|~sQ28_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f318,f141])).
% 0.02/0.50  fof(f1076,plain,(
% 0.02/0.50    sQ7_spl|~sQ28_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1075,f248,f317])).
% 0.02/0.50  fof(f1077,plain,(
% 0.02/0.50    sQ15_spl|~sQ35_spl|~sQ105_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1031,f274,f339,f631])).
% 0.02/0.50  fof(f1079,plain,(
% 0.02/0.50    ~sQ0_spl|~sQ32_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f652,f226,f330])).
% 0.02/0.50  fof(f1081,plain,(
% 0.02/0.50    ~sQ45_spl|~sQ37_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f749,f372,f346])).
% 0.02/0.50  fof(f1083,plain,(
% 0.02/0.50    ~sQ44_spl|~sQ12_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f657,f369,f265])).
% 0.02/0.50  fof(f1084,plain,(
% 0.02/0.50    ~sQ56_spl|~sQ8_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f653,f408,f252])).
% 0.02/0.50  fof(f1085,plain,(
% 0.02/0.50    ~sQ20_spl|~sQ28_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f938,f291,f317])).
% 0.02/0.50  fof(f1086,plain,(
% 0.02/0.50    op(e1,e3)=e1|~sQ53_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f399,f147])).
% 0.02/0.50  fof(f1096,plain,(
% 0.02/0.50    op(e1,e0)=e2|~sQ9_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f256,f136])).
% 0.02/0.50  fof(f1099,plain,(
% 0.02/0.50    ~e1=op(e0,e3)|~sQ9_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f256,f107])).
% 0.02/0.50  fof(f1105,plain,(
% 0.02/0.50    op(e2,e0)=e1|~sQ6_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f246,f135])).
% 0.02/0.50  fof(f1106,plain,(
% 0.02/0.50    ~e2=op(e1,e1)|~sQ6_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f246,f84])).
% 0.02/0.50  fof(f1113,plain,(
% 0.02/0.50    ~e0=op(e1,e2)|~sQ20_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f292,f111])).
% 0.02/0.50  fof(f1114,plain,(
% 0.02/0.50    op(e0,e1)=e1|~sQ20_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f292,f139])).
% 0.02/0.50  fof(f1115,plain,(
% 0.02/0.50    ~e0=op(e2,e1)|~sQ20_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f292,f87])).
% 0.02/0.50  fof(f1117,plain,(
% 0.02/0.50    ~sQ24_spl|~sQ20_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1113,f304,f291])).
% 0.02/0.50  fof(f1118,plain,(
% 0.02/0.50    sQ5_spl|~sQ20_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1114,f242,f291])).
% 0.02/0.50  fof(f1119,plain,(
% 0.02/0.50    ~sQ36_spl|~sQ20_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1115,f343,f291])).
% 0.02/0.50  fof(f1122,plain,(
% 0.02/0.50    e1=e0|~sQ9_spl|~sQ8_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f256,f253])).
% 0.02/0.50  fof(f1123,plain,(
% 0.02/0.50    $false|~sQ9_spl|~sQ8_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1122,f126])).
% 0.02/0.50  fof(f1124,plain,(
% 0.02/0.50    ~sQ9_spl|~sQ8_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1123])).
% 0.02/0.50  fof(f1132,plain,(
% 0.02/0.50    ~e0=op(e3,e2)|~sQ33_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f1136,f94])).
% 0.02/0.50  fof(f1134,plain,(
% 0.02/0.50    op(e0,e1)=e2|~sQ33_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f1136,f140])).
% 0.02/0.50  fof(f1136,plain,(
% 0.02/0.50    op(e1,e2)=e0|~sQ33_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f334,f142])).
% 0.02/0.50  fof(f1140,plain,(
% 0.02/0.50    ~e0=e0|~sQ33_spl|~sQ28_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1136,f1074])).
% 0.02/0.50  fof(f1141,plain,(
% 0.02/0.50    $false|~sQ33_spl|~sQ28_spl),
% 0.02/0.50    inference(trivial_equality_resolution,[status(thm)],[f1140])).
% 0.02/0.50  fof(f1142,plain,(
% 0.02/0.50    ~sQ33_spl|~sQ28_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1141])).
% 0.02/0.50  fof(f1145,plain,(
% 0.02/0.50    op(e2,e0)=e0|~sQ2_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f233,f134])).
% 0.02/0.50  fof(f1149,plain,(
% 0.02/0.50    ~sQ20_spl|~sQ52_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f934,f291,f395])).
% 0.02/0.50  fof(f1155,plain,(
% 0.02/0.50    sQ56_spl|~sQ35_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1027,f408,f339])).
% 0.02/0.50  fof(f1157,plain,(
% 0.02/0.50    ~sQ41_spl|~sQ45_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f945,f359,f372])).
% 0.02/0.50  fof(f1158,plain,(
% 0.02/0.50    ~sQ13_spl|~sQ45_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f985,f268,f372])).
% 0.02/0.50  fof(f1162,plain,(
% 0.02/0.50    ~sQ56_spl|~sQ33_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1132,f408,f333])).
% 0.02/0.50  fof(f1163,plain,(
% 0.02/0.50    sQ6_spl|~sQ33_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1134,f245,f333])).
% 0.02/0.50  fof(f1165,plain,(
% 0.02/0.50    op(e0,e2)=op(e0,e0)|~sQ2_spl|~sQ103_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f233,f624])).
% 0.02/0.50  fof(f1166,plain,(
% 0.02/0.50    op(e0,e2)=e2|~sQ2_spl|~sQ103_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f233,f1165])).
% 0.02/0.50  fof(f1167,plain,(
% 0.02/0.50    $false|sQ10_spl|~sQ2_spl|~sQ103_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1166,f260])).
% 0.02/0.50  fof(f1168,plain,(
% 0.02/0.50    sQ10_spl|~sQ2_spl|~sQ103_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1167])).
% 0.02/0.50  fof(f1171,plain,(
% 0.02/0.50    ~op(e2,e0)=e2|~sQ38_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f350,f114])).
% 0.02/0.50  fof(f1173,plain,(
% 0.02/0.50    ~e2=op(e2,e3)|~sQ38_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f350,f118])).
% 0.02/0.50  fof(f1175,plain,(
% 0.02/0.50    op(e2,e2)=e1|~sQ38_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f350,f143])).
% 0.02/0.50  fof(f1178,plain,(
% 0.02/0.50    ~e1=op(e3,e3)|~sQ13_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f269,f98])).
% 0.02/0.50  fof(f1179,plain,(
% 0.02/0.50    op(e1,e0)=e3|~sQ13_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f269,f137])).
% 0.02/0.50  fof(f1180,plain,(
% 0.02/0.50    ~e1=op(e1,e3)|~sQ13_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f269,f96])).
% 0.02/0.50  fof(f1182,plain,(
% 0.02/0.50    sQ19_spl|~sQ13_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1179,f287,f268])).
% 0.02/0.50  fof(f1183,plain,(
% 0.02/0.50    ~sQ28_spl|~sQ16_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f710,f317,f278])).
% 0.02/0.50  fof(f1184,plain,(
% 0.02/0.50    ~sQ34_spl|~sQ38_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1171,f336,f349])).
% 0.02/0.50  fof(f1185,plain,(
% 0.02/0.50    sQ41_spl|~sQ38_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1175,f359,f349])).
% 0.02/0.50  fof(f1186,plain,(
% 0.02/0.50    ~sQ33_spl|~sQ41_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f855,f333,f359])).
% 0.02/0.50  fof(f1190,plain,(
% 0.02/0.50    sQ16_spl|~sQ1_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1034,f278,f229])).
% 0.02/0.50  fof(f1192,plain,(
% 0.02/0.50    ~sQ36_spl|~sQ4_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f646,f343,f239])).
% 0.02/0.50  fof(f1193,plain,(
% 0.02/0.50    ~sQ13_spl|~sQ9_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1099,f268,f255])).
% 0.02/0.50  fof(f1195,plain,(
% 0.02/0.50    sQ25_spl|~sQ37_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f791,f307,f346])).
% 0.02/0.50  fof(f1196,plain,(
% 0.02/0.50    ~sQ29_spl|~sQ13_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1180,f320,f268])).
% 0.02/0.50  fof(f1197,plain,(
% 0.02/0.50    ~sQ22_spl|~sQ6_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1106,f297,f245])).
% 0.02/0.50  fof(f1202,plain,(
% 0.02/0.50    ~e3=op(e3,e3)|~sQ55_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f405,f124])).
% 0.02/0.50  fof(f1203,plain,(
% 0.02/0.50    op(e3,e3)=e1|~sQ55_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f405,f147])).
% 0.02/0.50  fof(f1204,plain,(
% 0.02/0.50    ~sQ63_spl|~sQ55_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1202,f430,f404])).
% 0.02/0.50  fof(f1205,plain,(
% 0.02/0.50    sQ29_spl|~sQ53_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1086,f320,f398])).
% 0.02/0.50  fof(f1208,plain,(
% 0.02/0.50    sQ61_spl|~sQ55_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1203,f424,f404])).
% 0.02/0.50  fof(f1214,plain,(
% 0.02/0.50    ~e1=op(e3,e3)|~sQ45_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f373,f101])).
% 0.02/0.50  fof(f1216,plain,(
% 0.02/0.50    ~sQ61_spl|~sQ45_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1214,f424,f372])).
% 0.02/0.50  fof(f1217,plain,(
% 0.02/0.50    sQ33_spl|~sQ6_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1105,f333,f245])).
% 0.02/0.50  fof(f1218,plain,(
% 0.02/0.50    op(e3,e2)=e1|~sQ39_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f353,f143])).
% 0.02/0.50  fof(f1227,plain,(
% 0.02/0.50    sQ57_spl|~sQ39_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1218,f411,f352])).
% 0.02/0.50  fof(f1232,plain,(
% 0.02/0.50    sQ55_spl|~sQ31_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f807,f404,f326])).
% 0.02/0.50  fof(f1233,plain,(
% 0.02/0.50    ~sQ46_spl|~sQ38_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1173,f375,f349])).
% 0.02/0.50  fof(f1238,plain,(
% 0.02/0.50    ~e0=op(e3,e0)|~sQ0_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f227,f80])).
% 0.02/0.50  fof(f1244,plain,(
% 0.02/0.50    ~e1=op(op(e3,e0),e2)|~sQ50_spl|sQ76_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f389,f515])).
% 0.02/0.50  fof(f1250,plain,(
% 0.02/0.50    ~e1=op(e2,e2)|~sQ50_spl|sQ76_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f389,f1244])).
% 0.02/0.50  fof(f1253,plain,(
% 0.02/0.50    ~sQ44_spl|~sQ28_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f936,f369,f317])).
% 0.02/0.50  fof(f1269,plain,(
% 0.02/0.50    op(e0,e3)=e1|~sQ52_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f396,f147])).
% 0.02/0.50  fof(f1284,plain,(
% 0.02/0.50    op(e1,e3)=e2|~sQ57_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f412,f148])).
% 0.02/0.50  fof(f1297,plain,(
% 0.02/0.50    ~e0=op(e1,op(e3,e2))|~sQ57_spl|sQ72_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f412,f499])).
% 0.02/0.50  fof(f1298,plain,(
% 0.02/0.50    ~e0=op(e1,e1)|~sQ57_spl|sQ72_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f412,f1297])).
% 0.02/0.50  fof(f1306,plain,(
% 0.02/0.50    op(e2,e1)=e3|~sQ30_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f324,f141])).
% 0.02/0.50  fof(f1321,plain,(
% 0.02/0.50    ~e0=op(e3,op(e2,e1))|~sQ39_spl|sQ69_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f353,f487])).
% 0.02/0.50  fof(f1322,plain,(
% 0.02/0.50    ~e0=op(e3,e3)|~sQ39_spl|sQ69_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f353,f1321])).
% 0.02/0.50  fof(f1354,plain,(
% 0.02/0.50    op(e0,e0)=e1|~sQ4_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f240,f135])).
% 0.02/0.50  fof(f1359,plain,(
% 0.02/0.50    $false|~sQ39_spl|sQ69_spl|~sQ60_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f422,f1322])).
% 0.02/0.50  fof(f1360,plain,(
% 0.02/0.50    ~sQ39_spl|sQ69_spl|~sQ60_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1359])).
% 0.02/0.50  fof(f1362,plain,(
% 0.02/0.50    ~sQ20_spl|~sQ57_spl|sQ72_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1298,f291,f411,f497])).
% 0.02/0.50  fof(f1367,plain,(
% 0.02/0.50    ~sQ48_spl|~sQ0_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1238,f382,f226])).
% 0.02/0.50  fof(f1368,plain,(
% 0.02/0.50    e3=e0|~sQ39_spl|~sQ36_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f353,f344])).
% 0.02/0.50  fof(f1369,plain,(
% 0.02/0.50    $false|~sQ39_spl|~sQ36_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1368,f128])).
% 0.02/0.50  fof(f1370,plain,(
% 0.02/0.50    ~sQ39_spl|~sQ36_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1369])).
% 0.02/0.50  fof(f1377,plain,(
% 0.02/0.50    op(e1,e0)=e2|~sQ9_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f256,f136])).
% 0.02/0.50  fof(f1383,plain,(
% 0.02/0.50    op(e2,e1)=e0|~sQ9_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f1096,f138])).
% 0.02/0.50  fof(f1397,plain,(
% 0.02/0.50    ~e0=op(e2,e2)|~sQ36_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f344,f117])).
% 0.02/0.50  fof(f1419,plain,(
% 0.02/0.50    ~e0=op(e2,e3)|~sQ36_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f344,f118])).
% 0.02/0.50  fof(f1426,plain,(
% 0.02/0.50    op(e0,e2)=e1|~sQ36_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f344,f143])).
% 0.02/0.50  fof(f1444,plain,(
% 0.02/0.50    ~e3=op(e1,op(e0,e2))|~sQ9_spl|sQ91_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f256,f575])).
% 0.02/0.50  fof(f1445,plain,(
% 0.02/0.50    ~e3=op(e1,e1)|~sQ9_spl|sQ91_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f256,f1444])).
% 0.02/0.50  fof(f1450,plain,(
% 0.02/0.50    ~e3=op(e2,op(e0,e1))|~sQ6_spl|sQ89_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f246,f567])).
% 0.02/0.50  fof(f1451,plain,(
% 0.02/0.50    ~e3=op(e2,e2)|~sQ6_spl|sQ89_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f246,f1450])).
% 0.02/0.50  fof(f1458,plain,(
% 0.02/0.50    ~e3=op(e2,e3)|~sQ15_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f275,f97])).
% 0.02/0.50  fof(f1465,plain,(
% 0.02/0.50    op(e2,e2)=e3|~sQ46_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f376,f145])).
% 0.02/0.50  fof(f1469,plain,(
% 0.02/0.50    $false|~sQ6_spl|sQ89_spl|~sQ46_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1465,f1451])).
% 0.02/0.50  fof(f1470,plain,(
% 0.02/0.50    ~sQ6_spl|sQ89_spl|~sQ46_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1469])).
% 0.02/0.50  fof(f1471,plain,(
% 0.02/0.50    ~sQ44_spl|~sQ36_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1419,f369,f343])).
% 0.02/0.50  fof(f1475,plain,(
% 0.02/0.50    ~sQ47_spl|~sQ15_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1458,f378,f274])).
% 0.02/0.50  fof(f1479,plain,(
% 0.02/0.50    ~sQ41_spl|~sQ50_spl|sQ76_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1250,f359,f388,f513])).
% 0.02/0.50  fof(f1486,plain,(
% 0.02/0.50    ~op(e2,e2)=e0|~sQ44_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f370,f119])).
% 0.02/0.50  fof(f1487,plain,(
% 0.02/0.50    op(e0,e2)=e3|~sQ44_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f370,f145])).
% 0.02/0.50  fof(f1491,plain,(
% 0.02/0.50    ~e1=op(e0,op(e2,e3))|~sQ44_spl|sQ80_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f370,f531])).
% 0.02/0.50  fof(f1492,plain,(
% 0.02/0.50    ~e1=op(e0,e0)|~sQ44_spl|sQ80_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f370,f1491])).
% 0.02/0.50  fof(f1510,plain,(
% 0.02/0.50    ~e2=op(e3,e1)|~sQ38_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f350,f89])).
% 0.02/0.50  fof(f1516,plain,(
% 0.02/0.50    ~sQ54_spl|~sQ38_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1510,f401,f349])).
% 0.02/0.50  fof(f1517,plain,(
% 0.02/0.50    sQ1_spl|~sQ4_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1354,f229,f239])).
% 0.02/0.50  fof(f1518,plain,(
% 0.02/0.50    ~sQ61_spl|~sQ13_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1178,f424,f268])).
% 0.02/0.50  fof(f1520,plain,(
% 0.02/0.50    sQ32_spl|~sQ2_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1145,f330,f232])).
% 0.02/0.50  fof(f1522,plain,(
% 0.02/0.50    ~sQ40_spl|~sQ44_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1486,f356,f369])).
% 0.02/0.50  fof(f1523,plain,(
% 0.02/0.50    ~sQ23_spl|~sQ9_spl|sQ91_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1445,f300,f255,f573])).
% 0.02/0.50  fof(f1543,plain,(
% 0.02/0.50    ~op(e0,e3)=e2|~sQ62_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f428,f98])).
% 0.02/0.50  fof(f1560,plain,(
% 0.02/0.50    op(e0,e3)=e1|~sQ52_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f396,f147])).
% 0.02/0.50  fof(f1568,plain,(
% 0.02/0.50    op(e1,e0)=e3|~sQ52_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f1269,f137])).
% 0.02/0.50  fof(f1581,plain,(
% 0.02/0.50    ~e2=op(e0,op(e1,e3))|~sQ28_spl|sQ86_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f318,f555])).
% 0.02/0.50  fof(f1582,plain,(
% 0.02/0.50    ~e2=op(e0,e0)|~sQ28_spl|sQ86_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f318,f1581])).
% 0.02/0.50  fof(f1592,plain,(
% 0.02/0.50    $false|~sQ28_spl|sQ86_spl|~sQ2_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f233,f1582])).
% 0.02/0.50  fof(f1593,plain,(
% 0.02/0.50    ~sQ28_spl|sQ86_spl|~sQ2_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1592])).
% 0.02/0.50  fof(f1594,plain,(
% 0.02/0.50    ~sQ40_spl|~sQ36_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1397,f356,f343])).
% 0.02/0.50  fof(f1595,plain,(
% 0.02/0.50    sQ9_spl|~sQ36_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1426,f255,f343])).
% 0.02/0.50  fof(f1600,plain,(
% 0.02/0.50    ~sQ14_spl|~sQ62_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1543,f271,f427])).
% 0.02/0.50  fof(f1601,plain,(
% 0.02/0.50    e3=e0|~sQ59_spl|~sQ56_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f418,f409])).
% 0.02/0.50  fof(f1602,plain,(
% 0.02/0.50    $false|~sQ59_spl|~sQ56_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1601,f128])).
% 0.02/0.50  fof(f1603,plain,(
% 0.02/0.50    ~sQ59_spl|~sQ56_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1602])).
% 0.02/0.50  fof(f1604,plain,(
% 0.02/0.50    ~sQ1_spl|~sQ44_spl|sQ80_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1492,f229,f369,f529])).
% 0.02/0.50  fof(f1605,plain,(
% 0.02/0.50    ~sQ32_spl|~sQ16_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f641,f330,f278])).
% 0.02/0.50  fof(f1606,plain,(
% 0.02/0.50    sQ18_spl|~sQ9_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1377,f284,f255])).
% 0.02/0.50  fof(f1614,plain,(
% 0.02/0.50    ~sQ30_spl|~sQ26_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f858,f323,f310])).
% 0.02/0.50  fof(f1617,plain,(
% 0.02/0.50    sQ39_spl|~sQ30_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1306,f352,f323])).
% 0.02/0.50  fof(f1633,plain,(
% 0.02/0.50    op(e0,e1)=e3|~sQ28_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f318,f141])).
% 0.02/0.50  fof(f1649,plain,(
% 0.02/0.50    ~e2=op(e3,op(e0,e1))|~sQ28_spl|sQ83_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1633,f543])).
% 0.02/0.50  fof(f1650,plain,(
% 0.02/0.50    ~e2=op(e3,e3)|~sQ28_spl|sQ83_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1633,f1649])).
% 0.02/0.50  fof(f1680,plain,(
% 0.02/0.50    op(e3,e0)=op(e1,e3)|~sQ28_spl|~sQ66_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f318,f474])).
% 0.02/0.50  fof(f1681,plain,(
% 0.02/0.50    op(e3,e0)=e0|~sQ28_spl|~sQ66_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f318,f1680])).
% 0.02/0.50  fof(f1682,plain,(
% 0.02/0.50    op(e1,e3)=op(e0,e1)|~sQ28_spl|~sQ99_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1633,f606])).
% 0.02/0.50  fof(f1683,plain,(
% 0.02/0.50    e0=op(e0,e1)|~sQ28_spl|~sQ99_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f318,f1682])).
% 0.02/0.50  fof(f1684,plain,(
% 0.02/0.50    e0=e3|~sQ28_spl|~sQ99_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1633,f1683])).
% 0.02/0.50  fof(f1685,plain,(
% 0.02/0.50    $false|~sQ28_spl|~sQ99_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1684,f128])).
% 0.02/0.50  fof(f1686,plain,(
% 0.02/0.50    ~sQ28_spl|~sQ99_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1685])).
% 0.02/0.50  fof(f1725,plain,(
% 0.02/0.50    op(e1,op(e0,e1))=e2|~sQ6_spl|~sQ99_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f246,f606])).
% 0.02/0.50  fof(f1726,plain,(
% 0.02/0.50    op(e1,e2)=e2|~sQ6_spl|~sQ99_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f246,f1725])).
% 0.02/0.50  fof(f1727,plain,(
% 0.02/0.50    $false|sQ26_spl|~sQ6_spl|~sQ99_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1726,f312])).
% 0.02/0.50  fof(f1728,plain,(
% 0.02/0.50    sQ26_spl|~sQ6_spl|~sQ99_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1727])).
% 0.02/0.50  fof(f1737,plain,(
% 0.02/0.50    ~sQ62_spl|~sQ28_spl|sQ83_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1650,f427,f317,f541])).
% 0.02/0.50  fof(f1742,plain,(
% 0.02/0.50    sQ48_spl|~sQ28_spl|~sQ66_spl),
% 0.02/0.50    inference(split_clause,[status(thm)],[f1681,f382,f317,f473])).
% 0.02/0.50  fof(f1783,plain,(
% 0.02/0.50    op(e2,op(e0,e2))=e1|~sQ9_spl|~sQ94_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f256,f585])).
% 0.02/0.50  fof(f1790,plain,(
% 0.02/0.50    op(e2,e1)=e1|~sQ9_spl|~sQ94_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f256,f1783])).
% 0.02/0.50  fof(f1922,plain,(
% 0.02/0.50    e1=e0|~sQ94_spl|~sQ9_spl),
% 0.02/0.50    inference(backward_demodulation,[status(thm)],[f1790,f1383])).
% 0.02/0.50  fof(f1923,plain,(
% 0.02/0.50    $false|~sQ94_spl|~sQ9_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f1922,f126])).
% 0.02/0.50  fof(f1924,plain,(
% 0.02/0.50    ~sQ94_spl|~sQ9_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f1923])).
% 0.02/0.50  fof(f2069,plain,(
% 0.02/0.50    op(e3,e2)=op(e1,e3)|~sQ57_spl|~sQ66_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1284,f474])).
% 0.02/0.50  fof(f2070,plain,(
% 0.02/0.50    e1=op(e1,e3)|~sQ57_spl|~sQ66_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f412,f2069])).
% 0.02/0.50  fof(f2071,plain,(
% 0.02/0.50    e1=e2|~sQ57_spl|~sQ66_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1284,f2070])).
% 0.02/0.50  fof(f2072,plain,(
% 0.02/0.50    $false|~sQ57_spl|~sQ66_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f2071,f129])).
% 0.02/0.50  fof(f2073,plain,(
% 0.02/0.50    ~sQ57_spl|~sQ66_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f2072])).
% 0.02/0.50  fof(f2081,plain,(
% 0.02/0.50    op(e0,e3)=op(e1,e0)|~sQ52_spl|~sQ104_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1568,f628])).
% 0.02/0.50  fof(f2082,plain,(
% 0.02/0.50    e1=op(e1,e0)|~sQ52_spl|~sQ104_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1560,f2081])).
% 0.02/0.50  fof(f2083,plain,(
% 0.02/0.50    e1=e3|~sQ52_spl|~sQ104_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1568,f2082])).
% 0.02/0.50  fof(f2084,plain,(
% 0.02/0.50    $false|~sQ52_spl|~sQ104_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f2083,f130])).
% 0.02/0.50  fof(f2085,plain,(
% 0.02/0.50    ~sQ52_spl|~sQ104_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f2084])).
% 0.02/0.50  fof(f2089,plain,(
% 0.02/0.50    op(e2,e3)=op(e0,e2)|~sQ44_spl|~sQ94_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1487,f585])).
% 0.02/0.50  fof(f2090,plain,(
% 0.02/0.50    e0=op(e0,e2)|~sQ44_spl|~sQ94_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f370,f2089])).
% 0.02/0.50  fof(f2091,plain,(
% 0.02/0.50    e0=e3|~sQ44_spl|~sQ94_spl),
% 0.02/0.50    inference(forward_demodulation,[status(thm)],[f1487,f2090])).
% 0.02/0.50  fof(f2092,plain,(
% 0.02/0.50    $false|~sQ44_spl|~sQ94_spl),
% 0.02/0.50    inference(forward_subsumption_resolution,[status(thm)],[f2091,f128])).
% 0.02/0.50  fof(f2093,plain,(
% 0.02/0.50    ~sQ44_spl|~sQ94_spl),
% 0.02/0.50    inference(contradiction_clause,[status(thm)],[f2092])).
% 0.02/0.50  fof(f2094,plain,(
% 0.02/0.50    $false),
% 0.02/0.50    inference(sat_refutation,[status(thm)],[f238,f251,f264,f303,f329,f342,f355,f381,f394,f407,f420,f433,f434,f436,f437,f442,f443,f445,f449,f450,f451,f452,f453,f455,f456,f458,f459,f462,f465,f472,f476,f480,f484,f488,f496,f500,f508,f516,f524,f532,f544,f556,f568,f576,f587,f600,f608,f621,f626,f630,f634,f683,f732,f738,f741,f766,f768,f783,f784,f787,f792,f793,f796,f802,f814,f818,f822,f840,f841,f843,f863,f867,f868,f873,f891,f896,f900,f902,f903,f904,f906,f914,f915,f917,f953,f956,f961,f962,f963,f968,f969,f970,f971,f973,f974,f975,f976,f980,f989,f991,f999,f1000,f1030,f1042,f1047,f1054,f1055,f1056,f1058,f1059,f1060,f1064,f1066,f1067,f1068,f1069,f1071,f1076,f1077,f1079,f1081,f1083,f1084,f1085,f1117,f1118,f1119,f1124,f1142,f1149,f1155,f1157,f1158,f1162,f1163,f1168,f1182,f1183,f1184,f1185,f1186,f1190,f1192,f1193,f1195,f1196,f1197,f1204,f1205,f1208,f1216,f1217,f1227,f1232,f1233,f1253,f1360,f1362,f1367,f1370,f1470,f1471,f1475,f1479,f1516,f1517,f1518,f1520,f1522,f1523,f1593,f1594,f1595,f1600,f1603,f1604,f1605,f1606,f1614,f1617,f1686,f1728,f1737,f1742,f1924,f2073,f2085,f2093])).
% 0.02/0.50  % SZS output end CNFRefutation for theBenchmark.p
% 0.02/0.50  % Elapsed time: 0.123365 seconds
% 0.02/0.50  % CPU time: 0.740078 seconds
% 0.02/0.50  % Total memory used: 20.868 MB
% 0.02/0.50  % Net memory used: 20.574 MB
%------------------------------------------------------------------------------