%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG170+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 : n003.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:44 AM UTC 2026
% Result : Theorem 0.13s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG170+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.56 % Computer : n003.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Mon Sep 21 13:02:18 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.58 % Drodi V4.1.1
% 0.13/0.69 % Refutation found
% 0.13/0.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.69 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.69 fof(f1,axiom,(
% 0.13/0.69 ( ( op(e0,e0) = e0| op(e0,e0) = e1| op(e0,e0) = e2| op(e0,e0) = e3| op(e0,e0) = e4 )& ( op(e0,e1) = e0| op(e0,e1) = e1| op(e0,e1) = e2| op(e0,e1) = e3| op(e0,e1) = e4 )& ( op(e0,e2) = e0| op(e0,e2) = e1| op(e0,e2) = e2| op(e0,e2) = e3| op(e0,e2) = e4 )& ( op(e0,e3) = e0| op(e0,e3) = e1| op(e0,e3) = e2| op(e0,e3) = e3| op(e0,e3) = e4 )& ( op(e0,e4) = e0| op(e0,e4) = e1| op(e0,e4) = e2| op(e0,e4) = e3| op(e0,e4) = e4 )& ( op(e1,e0) = e0| op(e1,e0) = e1| op(e1,e0) = e2| op(e1,e0) = e3| op(e1,e0) = e4 )& ( op(e1,e1) = e0| op(e1,e1) = e1| op(e1,e1) = e2| op(e1,e1) = e3| op(e1,e1) = e4 )& ( op(e1,e2) = e0| op(e1,e2) = e1| op(e1,e2) = e2| op(e1,e2) = e3| op(e1,e2) = e4 )& ( op(e1,e3) = e0| op(e1,e3) = e1| op(e1,e3) = e2| op(e1,e3) = e3| op(e1,e3) = e4 )& ( op(e1,e4) = e0| op(e1,e4) = e1| op(e1,e4) = e2| op(e1,e4) = e3| op(e1,e4) = e4 )& ( op(e2,e0) = e0| op(e2,e0) = e1| op(e2,e0) = e2| op(e2,e0) = e3| op(e2,e0) = e4 )& ( op(e2,e1) = e0| op(e2,e1) = e1| op(e2,e1) = e2| op(e2,e1) = e3| op(e2,e1) = e4 )& ( op(e2,e2) = e0| op(e2,e2) = e1| op(e2,e2) = e2| op(e2,e2) = e3| op(e2,e2) = e4 )& ( op(e2,e3) = e0| op(e2,e3) = e1| op(e2,e3) = e2| op(e2,e3) = e3| op(e2,e3) = e4 )& ( op(e2,e4) = e0| op(e2,e4) = e1| op(e2,e4) = e2| op(e2,e4) = e3| op(e2,e4) = e4 )& ( op(e3,e0) = e0| op(e3,e0) = e1| op(e3,e0) = e2| op(e3,e0) = e3| op(e3,e0) = e4 )& ( op(e3,e1) = e0| op(e3,e1) = e1| op(e3,e1) = e2| op(e3,e1) = e3| op(e3,e1) = e4 )& ( op(e3,e2) = e0| op(e3,e2) = e1| op(e3,e2) = e2| op(e3,e2) = e3| op(e3,e2) = e4 )& ( op(e3,e3) = e0| op(e3,e3) = e1| op(e3,e3) = e2| op(e3,e3) = e3| op(e3,e3) = e4 )& ( op(e3,e4) = e0| op(e3,e4) = e1| op(e3,e4) = e2| op(e3,e4) = e3| op(e3,e4) = e4 )& ( op(e4,e0) = e0| op(e4,e0) = e1| op(e4,e0) = e2| op(e4,e0) = e3| op(e4,e0) = e4 )& ( op(e4,e1) = e0| op(e4,e1) = e1| op(e4,e1) = e2| op(e4,e1) = e3| op(e4,e1) = e4 )& ( op(e4,e2) = e0| op(e4,e2) = e1| op(e4,e2) = e2| op(e4,e2) = e3| op(e4,e2) = e4 )& ( op(e4,e3) = e0| op(e4,e3) = e1| op(e4,e3) = e2| op(e4,e3) = e3| op(e4,e3) = e4 )& ( op(e4,e4) = e0| op(e4,e4) = e1| op(e4,e4) = e2| op(e4,e4) = e3| op(e4,e4) = e4 ) ) ),
% 0.13/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f2,axiom,(
% 0.13/0.69 ( ( op(e0,e0) = e0| op(e0,e1) = e0| op(e0,e2) = e0| op(e0,e3) = e0| op(e0,e4) = e0 )& ( op(e0,e0) = e0| op(e1,e0) = e0| op(e2,e0) = e0| op(e3,e0) = e0| op(e4,e0) = e0 )& ( op(e0,e0) = e1| op(e0,e1) = e1| op(e0,e2) = e1| op(e0,e3) = e1| op(e0,e4) = e1 )& ( op(e0,e0) = e1| op(e1,e0) = e1| op(e2,e0) = e1| op(e3,e0) = e1| op(e4,e0) = e1 )& ( op(e0,e0) = e2| op(e0,e1) = e2| op(e0,e2) = e2| op(e0,e3) = e2| op(e0,e4) = e2 )& ( op(e0,e0) = e2| op(e1,e0) = e2| op(e2,e0) = e2| op(e3,e0) = e2| op(e4,e0) = e2 )& ( op(e0,e0) = e3| op(e0,e1) = e3| op(e0,e2) = e3| op(e0,e3) = e3| op(e0,e4) = e3 )& ( op(e0,e0) = e3| op(e1,e0) = e3| op(e2,e0) = e3| op(e3,e0) = e3| op(e4,e0) = e3 )& ( op(e0,e0) = e4| op(e0,e1) = e4| op(e0,e2) = e4| op(e0,e3) = e4| op(e0,e4) = e4 )& ( op(e0,e0) = e4| op(e1,e0) = e4| op(e2,e0) = e4| op(e3,e0) = e4| op(e4,e0) = e4 )& ( op(e1,e0) = e0| op(e1,e1) = e0| op(e1,e2) = e0| op(e1,e3) = e0| op(e1,e4) = e0 )& ( op(e0,e1) = e0| op(e1,e1) = e0| op(e2,e1) = e0| op(e3,e1) = e0| op(e4,e1) = e0 )& ( op(e1,e0) = e1| op(e1,e1) = e1| op(e1,e2) = e1| op(e1,e3) = e1| op(e1,e4) = e1 )& ( op(e0,e1) = e1| op(e1,e1) = e1| op(e2,e1) = e1| op(e3,e1) = e1| op(e4,e1) = e1 )& ( op(e1,e0) = e2| op(e1,e1) = e2| op(e1,e2) = e2| op(e1,e3) = e2| op(e1,e4) = e2 )& ( op(e0,e1) = e2| op(e1,e1) = e2| op(e2,e1) = e2| op(e3,e1) = e2| op(e4,e1) = e2 )& ( op(e1,e0) = e3| op(e1,e1) = e3| op(e1,e2) = e3| op(e1,e3) = e3| op(e1,e4) = e3 )& ( op(e0,e1) = e3| op(e1,e1) = e3| op(e2,e1) = e3| op(e3,e1) = e3| op(e4,e1) = e3 )& ( op(e1,e0) = e4| op(e1,e1) = e4| op(e1,e2) = e4| op(e1,e3) = e4| op(e1,e4) = e4 )& ( op(e0,e1) = e4| op(e1,e1) = e4| op(e2,e1) = e4| op(e3,e1) = e4| op(e4,e1) = e4 )& ( op(e2,e0) = e0| op(e2,e1) = e0| op(e2,e2) = e0| op(e2,e3) = e0| op(e2,e4) = e0 )& ( op(e0,e2) = e0| op(e1,e2) = e0| op(e2,e2) = e0| op(e3,e2) = e0| op(e4,e2) = e0 )& ( op(e2,e0) = e1| op(e2,e1) = e1| op(e2,e2) = e1| op(e2,e3) = e1| op(e2,e4) = e1 )& ( op(e0,e2) = e1| op(e1,e2) = e1| op(e2,e2) = e1| op(e3,e2) = e1| op(e4,e2) = e1 )& ( op(e2,e0) = e2| op(e2,e1) = e2| op(e2,e2) = e2| op(e2,e3) = e2| op(e2,e4) = e2 )& ( op(e0,e2) = e2| op(e1,e2) = e2| op(e2,e2) = e2| op(e3,e2) = e2| op(e4,e2) = e2 )& ( op(e2,e0) = e3| op(e2,e1) = e3| op(e2,e2) = e3| op(e2,e3) = e3| op(e2,e4) = e3 )& ( op(e0,e2) = e3| op(e1,e2) = e3| op(e2,e2) = e3| op(e3,e2) = e3| op(e4,e2) = e3 )& ( op(e2,e0) = e4| op(e2,e1) = e4| op(e2,e2) = e4| op(e2,e3) = e4| op(e2,e4) = e4 )& ( op(e0,e2) = e4| op(e1,e2) = e4| op(e2,e2) = e4| op(e3,e2) = e4| op(e4,e2) = e4 )& ( op(e3,e0) = e0| op(e3,e1) = e0| op(e3,e2) = e0| op(e3,e3) = e0| op(e3,e4) = e0 )& ( op(e0,e3) = e0| op(e1,e3) = e0| op(e2,e3) = e0| op(e3,e3) = e0| op(e4,e3) = e0 )& ( op(e3,e0) = e1| op(e3,e1) = e1| op(e3,e2) = e1| op(e3,e3) = e1| op(e3,e4) = e1 )& ( op(e0,e3) = e1| op(e1,e3) = e1| op(e2,e3) = e1| op(e3,e3) = e1| op(e4,e3) = e1 )& ( op(e3,e0) = e2| op(e3,e1) = e2| op(e3,e2) = e2| op(e3,e3) = e2| op(e3,e4) = e2 )& ( op(e0,e3) = e2| op(e1,e3) = e2| op(e2,e3) = e2| op(e3,e3) = e2| op(e4,e3) = e2 )& ( op(e3,e0) = e3| op(e3,e1) = e3| op(e3,e2) = e3| op(e3,e3) = e3| op(e3,e4) = e3 )& ( op(e0,e3) = e3| op(e1,e3) = e3| op(e2,e3) = e3| op(e3,e3) = e3| op(e4,e3) = e3 )& ( op(e3,e0) = e4| op(e3,e1) = e4| op(e3,e2) = e4| op(e3,e3) = e4| op(e3,e4) = e4 )& ( op(e0,e3) = e4| op(e1,e3) = e4| op(e2,e3) = e4| op(e3,e3) = e4| op(e4,e3) = e4 )& ( op(e4,e0) = e0| op(e4,e1) = e0| op(e4,e2) = e0| op(e4,e3) = e0| op(e4,e4) = e0 )& ( op(e0,e4) = e0| op(e1,e4) = e0| op(e2,e4) = e0| op(e3,e4) = e0| op(e4,e4) = e0 )& ( op(e4,e0) = e1| op(e4,e1) = e1| op(e4,e2) = e1| op(e4,e3) = e1| op(e4,e4) = e1 )& ( op(e0,e4) = e1| op(e1,e4) = e1| op(e2,e4) = e1| op(e3,e4) = e1| op(e4,e4) = e1 )& ( op(e4,e0) = e2| op(e4,e1) = e2| op(e4,e2) = e2| op(e4,e3) = e2| op(e4,e4) = e2 )& ( op(e0,e4) = e2| op(e1,e4) = e2| op(e2,e4) = e2| op(e3,e4) = e2| op(e4,e4) = e2 )& ( op(e4,e0) = e3| op(e4,e1) = e3| op(e4,e2) = e3| op(e4,e3) = e3| op(e4,e4) = e3 )& ( op(e0,e4) = e3| op(e1,e4) = e3| op(e2,e4) = e3| op(e3,e4) = e3| op(e4,e4) = e3 )& ( op(e4,e0) = e4| op(e4,e1) = e4| op(e4,e2) = e4| op(e4,e3) = e4| op(e4,e4) = e4 )& ( op(e0,e4) = e4| op(e1,e4) = e4| op(e2,e4) = e4| op(e3,e4) = e4| op(e4,e4) = e4 ) ) ),
% 0.13/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f3,axiom,(
% 0.13/0.69 ( op(op(e0,e0),op(e0,e0)) = e0& op(op(e1,e0),op(e0,e1)) = e0& op(op(e2,e0),op(e0,e2)) = e0& op(op(e3,e0),op(e0,e3)) = e0& op(op(e4,e0),op(e0,e4)) = e0& op(op(e0,e1),op(e1,e0)) = e1& op(op(e1,e1),op(e1,e1)) = e1& op(op(e2,e1),op(e1,e2)) = e1& op(op(e3,e1),op(e1,e3)) = e1& op(op(e4,e1),op(e1,e4)) = e1& op(op(e0,e2),op(e2,e0)) = e2& op(op(e1,e2),op(e2,e1)) = e2& op(op(e2,e2),op(e2,e2)) = e2& op(op(e3,e2),op(e2,e3)) = e2& op(op(e4,e2),op(e2,e4)) = e2& op(op(e0,e3),op(e3,e0)) = e3& op(op(e1,e3),op(e3,e1)) = e3& op(op(e2,e3),op(e3,e2)) = e3& op(op(e3,e3),op(e3,e3)) = e3& op(op(e4,e3),op(e3,e4)) = e3& op(op(e0,e4),op(e4,e0)) = e4& op(op(e1,e4),op(e4,e1)) = e4& op(op(e2,e4),op(e4,e2)) = e4& op(op(e3,e4),op(e4,e3)) = e4& op(op(e4,e4),op(e4,e4)) = e4 ) ),
% 0.13/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f4,axiom,(
% 0.13/0.69 ( op(e0,e0) != op(e1,e0)& op(e0,e0) != op(e2,e0)& op(e0,e0) != op(e3,e0)& op(e0,e0) != op(e4,e0)& op(e1,e0) != op(e2,e0)& op(e1,e0) != op(e3,e0)& op(e1,e0) != op(e4,e0)& op(e2,e0) != op(e3,e0)& op(e2,e0) != op(e4,e0)& op(e3,e0) != op(e4,e0)& op(e0,e1) != op(e1,e1)& op(e0,e1) != op(e2,e1)& op(e0,e1) != op(e3,e1)& op(e0,e1) != op(e4,e1)& op(e1,e1) != op(e2,e1)& op(e1,e1) != op(e3,e1)& op(e1,e1) != op(e4,e1)& op(e2,e1) != op(e3,e1)& op(e2,e1) != op(e4,e1)& op(e3,e1) != op(e4,e1)& op(e0,e2) != op(e1,e2)& op(e0,e2) != op(e2,e2)& op(e0,e2) != op(e3,e2)& op(e0,e2) != op(e4,e2)& op(e1,e2) != op(e2,e2)& op(e1,e2) != op(e3,e2)& op(e1,e2) != op(e4,e2)& op(e2,e2) != op(e3,e2)& op(e2,e2) != op(e4,e2)& op(e3,e2) != op(e4,e2)& op(e0,e3) != op(e1,e3)& op(e0,e3) != op(e2,e3)& op(e0,e3) != op(e3,e3)& op(e0,e3) != op(e4,e3)& op(e1,e3) != op(e2,e3)& op(e1,e3) != op(e3,e3)& op(e1,e3) != op(e4,e3)& op(e2,e3) != op(e3,e3)& op(e2,e3) != op(e4,e3)& op(e3,e3) != op(e4,e3)& op(e0,e4) != op(e1,e4)& op(e0,e4) != op(e2,e4)& op(e0,e4) != op(e3,e4)& op(e0,e4) != op(e4,e4)& op(e1,e4) != op(e2,e4)& op(e1,e4) != op(e3,e4)& op(e1,e4) != op(e4,e4)& op(e2,e4) != op(e3,e4)& op(e2,e4) != op(e4,e4)& op(e3,e4) != op(e4,e4)& op(e0,e0) != op(e0,e1)& op(e0,e0) != op(e0,e2)& op(e0,e0) != op(e0,e3)& op(e0,e0) != op(e0,e4)& op(e0,e1) != op(e0,e2)& op(e0,e1) != op(e0,e3)& op(e0,e1) != op(e0,e4)& op(e0,e2) != op(e0,e3)& op(e0,e2) != op(e0,e4)& op(e0,e3) != op(e0,e4)& op(e1,e0) != op(e1,e1)& op(e1,e0) != op(e1,e2)& op(e1,e0) != op(e1,e3)& op(e1,e0) != op(e1,e4)& op(e1,e1) != op(e1,e2)& op(e1,e1) != op(e1,e3)& op(e1,e1) != op(e1,e4)& op(e1,e2) != op(e1,e3)& op(e1,e2) != op(e1,e4)& op(e1,e3) != op(e1,e4)& op(e2,e0) != op(e2,e1)& op(e2,e0) != op(e2,e2)& op(e2,e0) != op(e2,e3)& op(e2,e0) != op(e2,e4)& op(e2,e1) != op(e2,e2)& op(e2,e1) != op(e2,e3)& op(e2,e1) != op(e2,e4)& op(e2,e2) != op(e2,e3)& op(e2,e2) != op(e2,e4)& op(e2,e3) != op(e2,e4)& op(e3,e0) != op(e3,e1)& op(e3,e0) != op(e3,e2)& op(e3,e0) != op(e3,e3)& op(e3,e0) != op(e3,e4)& op(e3,e1) != op(e3,e2)& op(e3,e1) != op(e3,e3)& op(e3,e1) != op(e3,e4)& op(e3,e2) != op(e3,e3)& op(e3,e2) != op(e3,e4)& op(e3,e3) != op(e3,e4)& op(e4,e0) != op(e4,e1)& op(e4,e0) != op(e4,e2)& op(e4,e0) != op(e4,e3)& op(e4,e0) != op(e4,e4)& op(e4,e1) != op(e4,e2)& op(e4,e1) != op(e4,e3)& op(e4,e1) != op(e4,e4)& op(e4,e2) != op(e4,e3)& op(e4,e2) != op(e4,e4)& op(e4,e3) != op(e4,e4) ) ),
% 0.13/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f5,axiom,(
% 0.13/0.69 ( e0 != e1& e0 != e2& e0 != e3& e0 != e4& e1 != e2& e1 != e3& e1 != e4& e2 != e3& e2 != e4& e3 != e4 ) ),
% 0.13/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f6,axiom,(
% 0.13/0.69 ( e0 = op(e4,op(e4,e4))& e1 = op(e4,e4)& e2 = op(op(e4,op(e4,e4)),op(e4,e4))& e3 = op(op(e4,op(e4,e4)),op(e4,op(e4,e4))) ) ),
% 0.13/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f7,conjecture,(
% 0.13/0.69 ~ ( ( ( op(e0,e0) != e0& op(e1,e0) != e1& op(e2,e0) != e2& op(e3,e0) != e3& op(e4,e0) != e4 )| ( op(e0,e1) != e0& op(e1,e1) != e1& op(e2,e1) != e2& op(e3,e1) != e3& op(e4,e1) != e4 )| ( op(e0,e2) != e0& op(e1,e2) != e1& op(e2,e2) != e2& op(e3,e2) != e3& op(e4,e2) != e4 )| ( op(e0,e3) != e0& op(e1,e3) != e1& op(e2,e3) != e2& op(e3,e3) != e3& op(e4,e3) != e4 )| ( op(e0,e4) != e0& op(e1,e4) != e1& op(e2,e4) != e2& op(e3,e4) != e3& op(e4,e4) != e4 ) )& ( ( op(e0,e0) != e0& op(e0,e1) != e1& op(e0,e2) != e2& op(e0,e3) != e3& op(e0,e4) != e4 )| ( op(e1,e0) != e0& op(e1,e1) != e1& op(e1,e2) != e2& op(e1,e3) != e3& op(e1,e4) != e4 )| ( op(e2,e0) != e0& op(e2,e1) != e1& op(e2,e2) != e2& op(e2,e3) != e3& op(e2,e4) != e4 )| ( op(e3,e0) != e0& op(e3,e1) != e1& op(e3,e2) != e2& op(e3,e3) != e3& op(e3,e4) != e4 )| ( op(e4,e0) != e0& op(e4,e1) != e1& op(e4,e2) != e2& op(e4,e3) != e3& op(e4,e4) != e4 ) ) ) ),
% 0.13/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.69 fof(f8,negated_conjecture,(
% 0.13/0.69 ~(~ ( ( ( op(e0,e0) != e0& op(e1,e0) != e1& op(e2,e0) != e2& op(e3,e0) != e3& op(e4,e0) != e4 )| ( op(e0,e1) != e0& op(e1,e1) != e1& op(e2,e1) != e2& op(e3,e1) != e3& op(e4,e1) != e4 )| ( op(e0,e2) != e0& op(e1,e2) != e1& op(e2,e2) != e2& op(e3,e2) != e3& op(e4,e2) != e4 )| ( op(e0,e3) != e0& op(e1,e3) != e1& op(e2,e3) != e2& op(e3,e3) != e3& op(e4,e3) != e4 )| ( op(e0,e4) != e0& op(e1,e4) != e1& op(e2,e4) != e2& op(e3,e4) != e3& op(e4,e4) != e4 ) )& ( ( op(e0,e0) != e0& op(e0,e1) != e1& op(e0,e2) != e2& op(e0,e3) != e3& op(e0,e4) != e4 )| ( op(e1,e0) != e0& op(e1,e1) != e1& op(e1,e2) != e2& op(e1,e3) != e3& op(e1,e4) != e4 )| ( op(e2,e0) != e0& op(e2,e1) != e1& op(e2,e2) != e2& op(e2,e3) != e3& op(e2,e4) != e4 )| ( op(e3,e0) != e0& op(e3,e1) != e1& op(e3,e2) != e2& op(e3,e3) != e3& op(e3,e4) != e4 )| ( op(e4,e0) != e0& op(e4,e1) != e1& op(e4,e2) != e2& op(e4,e3) != e3& op(e4,e4) != e4 ) ) ) )),
% 0.13/0.69 inference(negated_conjecture,[status(cth)],[f7])).
% 0.13/0.69 fof(f11,plain,(
% 0.13/0.69 op(e0,e2)=e0|op(e0,e2)=e1|op(e0,e2)=e2|op(e0,e2)=e3|op(e0,e2)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f13,plain,(
% 0.13/0.69 op(e0,e4)=e0|op(e0,e4)=e1|op(e0,e4)=e2|op(e0,e4)=e3|op(e0,e4)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f14,plain,(
% 0.13/0.69 op(e1,e0)=e0|op(e1,e0)=e1|op(e1,e0)=e2|op(e1,e0)=e3|op(e1,e0)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f16,plain,(
% 0.13/0.69 op(e1,e2)=e0|op(e1,e2)=e1|op(e1,e2)=e2|op(e1,e2)=e3|op(e1,e2)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f17,plain,(
% 0.13/0.69 op(e1,e3)=e0|op(e1,e3)=e1|op(e1,e3)=e2|op(e1,e3)=e3|op(e1,e3)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f18,plain,(
% 0.13/0.69 op(e1,e4)=e0|op(e1,e4)=e1|op(e1,e4)=e2|op(e1,e4)=e3|op(e1,e4)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f20,plain,(
% 0.13/0.69 op(e2,e1)=e0|op(e2,e1)=e1|op(e2,e1)=e2|op(e2,e1)=e3|op(e2,e1)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f21,plain,(
% 0.13/0.69 op(e2,e2)=e0|op(e2,e2)=e1|op(e2,e2)=e2|op(e2,e2)=e3|op(e2,e2)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f24,plain,(
% 0.13/0.69 op(e3,e0)=e0|op(e3,e0)=e1|op(e3,e0)=e2|op(e3,e0)=e3|op(e3,e0)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f25,plain,(
% 0.13/0.69 op(e3,e1)=e0|op(e3,e1)=e1|op(e3,e1)=e2|op(e3,e1)=e3|op(e3,e1)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f28,plain,(
% 0.13/0.69 op(e3,e4)=e0|op(e3,e4)=e1|op(e3,e4)=e2|op(e3,e4)=e3|op(e3,e4)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f29,plain,(
% 0.13/0.69 op(e4,e0)=e0|op(e4,e0)=e1|op(e4,e0)=e2|op(e4,e0)=e3|op(e4,e0)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f31,plain,(
% 0.13/0.69 op(e4,e2)=e0|op(e4,e2)=e1|op(e4,e2)=e2|op(e4,e2)=e3|op(e4,e2)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f33,plain,(
% 0.13/0.69 op(e4,e4)=e0|op(e4,e4)=e1|op(e4,e4)=e2|op(e4,e4)=e3|op(e4,e4)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.69 fof(f34,plain,(
% 0.13/0.69 op(e0,e0)=e0|op(e0,e1)=e0|op(e0,e2)=e0|op(e0,e3)=e0|op(e0,e4)=e0),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f41,plain,(
% 0.13/0.69 op(e0,e0)=e3|op(e1,e0)=e3|op(e2,e0)=e3|op(e3,e0)=e3|op(e4,e0)=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f50,plain,(
% 0.13/0.69 op(e1,e0)=e3|op(e1,e1)=e3|op(e1,e2)=e3|op(e1,e3)=e3|op(e1,e4)=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f52,plain,(
% 0.13/0.69 op(e1,e0)=e4|op(e1,e1)=e4|op(e1,e2)=e4|op(e1,e3)=e4|op(e1,e4)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f58,plain,(
% 0.13/0.69 op(e2,e0)=e2|op(e2,e1)=e2|op(e2,e2)=e2|op(e2,e3)=e2|op(e2,e4)=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f59,plain,(
% 0.13/0.69 op(e0,e2)=e2|op(e1,e2)=e2|op(e2,e2)=e2|op(e3,e2)=e2|op(e4,e2)=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f60,plain,(
% 0.13/0.69 op(e2,e0)=e3|op(e2,e1)=e3|op(e2,e2)=e3|op(e2,e3)=e3|op(e2,e4)=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f63,plain,(
% 0.13/0.69 op(e0,e2)=e4|op(e1,e2)=e4|op(e2,e2)=e4|op(e3,e2)=e4|op(e4,e2)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f68,plain,(
% 0.13/0.69 op(e3,e0)=e2|op(e3,e1)=e2|op(e3,e2)=e2|op(e3,e3)=e2|op(e3,e4)=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f70,plain,(
% 0.13/0.69 op(e3,e0)=e3|op(e3,e1)=e3|op(e3,e2)=e3|op(e3,e3)=e3|op(e3,e4)=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f72,plain,(
% 0.13/0.69 op(e3,e0)=e4|op(e3,e1)=e4|op(e3,e2)=e4|op(e3,e3)=e4|op(e3,e4)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f75,plain,(
% 0.13/0.69 op(e0,e4)=e0|op(e1,e4)=e0|op(e2,e4)=e0|op(e3,e4)=e0|op(e4,e4)=e0),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f80,plain,(
% 0.13/0.69 op(e4,e0)=e3|op(e4,e1)=e3|op(e4,e2)=e3|op(e4,e3)=e3|op(e4,e4)=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f82,plain,(
% 0.13/0.69 op(e4,e0)=e4|op(e4,e1)=e4|op(e4,e2)=e4|op(e4,e3)=e4|op(e4,e4)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.69 fof(f84,plain,(
% 0.13/0.69 op(op(e0,e0),op(e0,e0))=e0),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f85,plain,(
% 0.13/0.69 op(op(e1,e0),op(e0,e1))=e0),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f88,plain,(
% 0.13/0.69 op(op(e4,e0),op(e0,e4))=e0),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f89,plain,(
% 0.13/0.69 op(op(e0,e1),op(e1,e0))=e1),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f93,plain,(
% 0.13/0.69 op(op(e4,e1),op(e1,e4))=e1),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f94,plain,(
% 0.13/0.69 op(op(e0,e2),op(e2,e0))=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f95,plain,(
% 0.13/0.69 op(op(e1,e2),op(e2,e1))=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f96,plain,(
% 0.13/0.69 op(op(e2,e2),op(e2,e2))=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f102,plain,(
% 0.13/0.69 op(op(e3,e3),op(e3,e3))=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f103,plain,(
% 0.13/0.69 op(op(e4,e3),op(e3,e4))=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f104,plain,(
% 0.13/0.69 op(op(e0,e4),op(e4,e0))=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f105,plain,(
% 0.13/0.69 op(op(e1,e4),op(e4,e1))=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f108,plain,(
% 0.13/0.69 op(op(e4,e4),op(e4,e4))=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.69 fof(f109,plain,(
% 0.13/0.69 ~op(e0,e0)=op(e1,e0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f110,plain,(
% 0.13/0.69 ~op(e0,e0)=op(e2,e0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f111,plain,(
% 0.13/0.69 ~op(e0,e0)=op(e3,e0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f112,plain,(
% 0.13/0.69 ~op(e0,e0)=op(e4,e0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f113,plain,(
% 0.13/0.69 ~op(e1,e0)=op(e2,e0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f114,plain,(
% 0.13/0.69 ~op(e1,e0)=op(e3,e0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f115,plain,(
% 0.13/0.69 ~op(e1,e0)=op(e4,e0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f117,plain,(
% 0.13/0.69 ~op(e2,e0)=op(e4,e0)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f119,plain,(
% 0.13/0.69 ~op(e0,e1)=op(e1,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f120,plain,(
% 0.13/0.69 ~op(e0,e1)=op(e2,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f121,plain,(
% 0.13/0.69 ~op(e0,e1)=op(e3,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f122,plain,(
% 0.13/0.69 ~op(e0,e1)=op(e4,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f123,plain,(
% 0.13/0.69 ~op(e1,e1)=op(e2,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f124,plain,(
% 0.13/0.69 ~op(e1,e1)=op(e3,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f126,plain,(
% 0.13/0.69 ~op(e2,e1)=op(e3,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f127,plain,(
% 0.13/0.69 ~op(e2,e1)=op(e4,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f129,plain,(
% 0.13/0.69 ~op(e0,e2)=op(e1,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f130,plain,(
% 0.13/0.69 ~op(e0,e2)=op(e2,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f133,plain,(
% 0.13/0.69 ~op(e1,e2)=op(e2,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f135,plain,(
% 0.13/0.69 ~op(e1,e2)=op(e4,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f137,plain,(
% 0.13/0.69 ~op(e2,e2)=op(e4,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f138,plain,(
% 0.13/0.69 ~op(e3,e2)=op(e4,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f139,plain,(
% 0.13/0.69 ~op(e0,e3)=op(e1,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f141,plain,(
% 0.13/0.69 ~op(e0,e3)=op(e3,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f143,plain,(
% 0.13/0.69 ~op(e1,e3)=op(e2,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f144,plain,(
% 0.13/0.69 ~op(e1,e3)=op(e3,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f145,plain,(
% 0.13/0.69 ~op(e1,e3)=op(e4,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f147,plain,(
% 0.13/0.69 ~op(e2,e3)=op(e4,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f148,plain,(
% 0.13/0.69 ~op(e3,e3)=op(e4,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f150,plain,(
% 0.13/0.69 ~op(e0,e4)=op(e2,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f151,plain,(
% 0.13/0.69 ~op(e0,e4)=op(e3,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f152,plain,(
% 0.13/0.69 ~op(e0,e4)=op(e4,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f154,plain,(
% 0.13/0.69 ~op(e1,e4)=op(e3,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f155,plain,(
% 0.13/0.69 ~op(e1,e4)=op(e4,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f156,plain,(
% 0.13/0.69 ~op(e2,e4)=op(e3,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f157,plain,(
% 0.13/0.69 ~op(e2,e4)=op(e4,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f158,plain,(
% 0.13/0.69 ~op(e3,e4)=op(e4,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f160,plain,(
% 0.13/0.69 ~op(e0,e0)=op(e0,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f162,plain,(
% 0.13/0.69 ~op(e0,e0)=op(e0,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f163,plain,(
% 0.13/0.69 ~op(e0,e1)=op(e0,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f164,plain,(
% 0.13/0.69 ~op(e0,e1)=op(e0,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f165,plain,(
% 0.13/0.69 ~op(e0,e1)=op(e0,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f167,plain,(
% 0.13/0.69 ~op(e0,e2)=op(e0,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f169,plain,(
% 0.13/0.69 ~op(e1,e0)=op(e1,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f170,plain,(
% 0.13/0.69 ~op(e1,e0)=op(e1,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f171,plain,(
% 0.13/0.69 ~op(e1,e0)=op(e1,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f172,plain,(
% 0.13/0.69 ~op(e1,e0)=op(e1,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f173,plain,(
% 0.13/0.69 ~op(e1,e1)=op(e1,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f174,plain,(
% 0.13/0.69 ~op(e1,e1)=op(e1,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f175,plain,(
% 0.13/0.69 ~op(e1,e1)=op(e1,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f177,plain,(
% 0.13/0.69 ~op(e1,e2)=op(e1,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f178,plain,(
% 0.13/0.69 ~op(e1,e3)=op(e1,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f181,plain,(
% 0.13/0.69 ~op(e2,e0)=op(e2,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f183,plain,(
% 0.13/0.69 ~op(e2,e1)=op(e2,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f184,plain,(
% 0.13/0.69 ~op(e2,e1)=op(e2,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f185,plain,(
% 0.13/0.69 ~op(e2,e1)=op(e2,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f187,plain,(
% 0.13/0.69 ~op(e2,e2)=op(e2,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f189,plain,(
% 0.13/0.69 ~op(e3,e0)=op(e3,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f190,plain,(
% 0.13/0.69 ~op(e3,e0)=op(e3,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f191,plain,(
% 0.13/0.69 ~op(e3,e0)=op(e3,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f192,plain,(
% 0.13/0.69 ~op(e3,e0)=op(e3,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f193,plain,(
% 0.13/0.69 ~op(e3,e1)=op(e3,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f194,plain,(
% 0.13/0.69 ~op(e3,e1)=op(e3,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f196,plain,(
% 0.13/0.69 ~op(e3,e2)=op(e3,e3)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f198,plain,(
% 0.13/0.69 ~op(e3,e3)=op(e3,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f199,plain,(
% 0.13/0.69 ~op(e4,e0)=op(e4,e1)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f200,plain,(
% 0.13/0.69 ~op(e4,e0)=op(e4,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f202,plain,(
% 0.13/0.69 ~op(e4,e0)=op(e4,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f203,plain,(
% 0.13/0.69 ~op(e4,e1)=op(e4,e2)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f207,plain,(
% 0.13/0.69 ~op(e4,e2)=op(e4,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f208,plain,(
% 0.13/0.69 ~op(e4,e3)=op(e4,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.69 fof(f209,plain,(
% 0.13/0.69 ~e0=e1),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f210,plain,(
% 0.13/0.69 ~e0=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f211,plain,(
% 0.13/0.69 ~e0=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f212,plain,(
% 0.13/0.69 ~e0=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f213,plain,(
% 0.13/0.69 ~e1=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f214,plain,(
% 0.13/0.69 ~e1=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f215,plain,(
% 0.13/0.69 ~e1=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f216,plain,(
% 0.13/0.69 ~e2=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f217,plain,(
% 0.13/0.69 ~e2=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f218,plain,(
% 0.13/0.69 ~e3=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.69 fof(f219,plain,(
% 0.13/0.69 e0=op(e4,op(e4,e4))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.69 fof(f220,plain,(
% 0.13/0.69 e1=op(e4,e4)),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.69 fof(f221,plain,(
% 0.13/0.69 e2=op(op(e4,op(e4,e4)),op(e4,e4))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.69 fof(f222,plain,(
% 0.13/0.69 e3=op(op(e4,op(e4,e4)),op(e4,op(e4,e4)))),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.69 fof(f223,definition,(
% 0.13/0.69 sP0_prd<=>(((((((~op(e0,e0)=e0&~op(e1,e0)=e1)&~op(e2,e0)=e2)&~op(e3,e0)=e3)&~op(e4,e0)=e4)|((((~op(e0,e1)=e0&~op(e1,e1)=e1)&~op(e2,e1)=e2)&~op(e3,e1)=e3)&~op(e4,e1)=e4))|((((~op(e0,e2)=e0&~op(e1,e2)=e1)&~op(e2,e2)=e2)&~op(e3,e2)=e3)&~op(e4,e2)=e4))|((((~op(e0,e3)=e0&~op(e1,e3)=e1)&~op(e2,e3)=e2)&~op(e3,e3)=e3)&~op(e4,e3)=e4))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.69 fof(f224,definition,(
% 0.13/0.69 sP1_prd<=>(((((((~op(e0,e0)=e0&~op(e0,e1)=e1)&~op(e0,e2)=e2)&~op(e0,e3)=e3)&~op(e0,e4)=e4)|((((~op(e1,e0)=e0&~op(e1,e1)=e1)&~op(e1,e2)=e2)&~op(e1,e3)=e3)&~op(e1,e4)=e4))|((((~op(e2,e0)=e0&~op(e2,e1)=e1)&~op(e2,e2)=e2)&~op(e2,e3)=e3)&~op(e2,e4)=e4))|((((~op(e3,e0)=e0&~op(e3,e1)=e1)&~op(e3,e2)=e2)&~op(e3,e3)=e3)&~op(e3,e4)=e4))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.13/0.69 fof(f225,plain,(
% 0.13/0.69 (sP0_prd|((((~op(e0,e4)=e0&~op(e1,e4)=e1)&~op(e2,e4)=e2)&~op(e3,e4)=e3)&~op(e4,e4)=e4))&(sP1_prd|((((~op(e4,e0)=e0&~op(e4,e1)=e1)&~op(e4,e2)=e2)&~op(e4,e3)=e3)&~op(e4,e4)=e4))),
% 0.13/0.69 inference(formula_renaming,[status(thm)],[f8,f224,f223])).
% 0.13/0.69 fof(f226,plain,(
% 0.13/0.69 sP0_prd|~op(e0,e4)=e0),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f225])).
% 0.13/0.69 fof(f229,plain,(
% 0.13/0.69 sP0_prd|~op(e3,e4)=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f225])).
% 0.13/0.69 fof(f234,plain,(
% 0.13/0.69 sP1_prd|~op(e4,e3)=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f225])).
% 0.13/0.69 fof(f236,definition,(
% 0.13/0.69 sP2_prd<=>((((((~op(e0,e0)=e0&~op(e1,e0)=e1)&~op(e2,e0)=e2)&~op(e3,e0)=e3)&~op(e4,e0)=e4)|((((~op(e0,e1)=e0&~op(e1,e1)=e1)&~op(e2,e1)=e2)&~op(e3,e1)=e3)&~op(e4,e1)=e4))|((((~op(e0,e2)=e0&~op(e1,e2)=e1)&~op(e2,e2)=e2)&~op(e3,e2)=e3)&~op(e4,e2)=e4))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.13/0.69 fof(f237,plain,(
% 0.13/0.69 sP0_prd<=>(sP2_prd|((((~op(e0,e3)=e0&~op(e1,e3)=e1)&~op(e2,e3)=e2)&~op(e3,e3)=e3)&~op(e4,e3)=e4))),
% 0.13/0.69 inference(formula_renaming,[status(thm)],[f223,f236])).
% 0.13/0.69 fof(f238,plain,(
% 0.13/0.69 (~sP0_prd|(sP2_prd|((((~op(e0,e3)=e0&~op(e1,e3)=e1)&~op(e2,e3)=e2)&~op(e3,e3)=e3)&~op(e4,e3)=e4)))&(sP0_prd|(~sP2_prd&((((op(e0,e3)=e0|op(e1,e3)=e1)|op(e2,e3)=e2)|op(e3,e3)=e3)|op(e4,e3)=e4)))),
% 0.13/0.69 inference(NNF_transformation,[status(thm)],[f237])).
% 0.13/0.69 fof(f240,plain,(
% 0.13/0.69 ~sP0_prd|sP2_prd|~op(e1,e3)=e1),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f238])).
% 0.13/0.69 fof(f243,plain,(
% 0.13/0.69 ~sP0_prd|sP2_prd|~op(e4,e3)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f238])).
% 0.13/0.69 fof(f244,plain,(
% 0.13/0.69 sP0_prd|~sP2_prd),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f238])).
% 0.13/0.69 fof(f246,definition,(
% 0.13/0.69 sP3_prd<=>((((((~op(e0,e0)=e0&~op(e0,e1)=e1)&~op(e0,e2)=e2)&~op(e0,e3)=e3)&~op(e0,e4)=e4)|((((~op(e1,e0)=e0&~op(e1,e1)=e1)&~op(e1,e2)=e2)&~op(e1,e3)=e3)&~op(e1,e4)=e4))|((((~op(e2,e0)=e0&~op(e2,e1)=e1)&~op(e2,e2)=e2)&~op(e2,e3)=e3)&~op(e2,e4)=e4))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.13/0.69 fof(f247,plain,(
% 0.13/0.69 sP1_prd<=>(sP3_prd|((((~op(e3,e0)=e0&~op(e3,e1)=e1)&~op(e3,e2)=e2)&~op(e3,e3)=e3)&~op(e3,e4)=e4))),
% 0.13/0.69 inference(formula_renaming,[status(thm)],[f224,f246])).
% 0.13/0.69 fof(f248,plain,(
% 0.13/0.69 (~sP1_prd|(sP3_prd|((((~op(e3,e0)=e0&~op(e3,e1)=e1)&~op(e3,e2)=e2)&~op(e3,e3)=e3)&~op(e3,e4)=e4)))&(sP1_prd|(~sP3_prd&((((op(e3,e0)=e0|op(e3,e1)=e1)|op(e3,e2)=e2)|op(e3,e3)=e3)|op(e3,e4)=e4)))),
% 0.13/0.69 inference(NNF_transformation,[status(thm)],[f247])).
% 0.13/0.69 fof(f250,plain,(
% 0.13/0.69 ~sP1_prd|sP3_prd|~op(e3,e1)=e1),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f248])).
% 0.13/0.69 fof(f251,plain,(
% 0.13/0.69 ~sP1_prd|sP3_prd|~op(e3,e2)=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f248])).
% 0.13/0.69 fof(f256,definition,(
% 0.13/0.69 sP4_prd<=>(((((~op(e0,e0)=e0&~op(e1,e0)=e1)&~op(e2,e0)=e2)&~op(e3,e0)=e3)&~op(e4,e0)=e4)|((((~op(e0,e1)=e0&~op(e1,e1)=e1)&~op(e2,e1)=e2)&~op(e3,e1)=e3)&~op(e4,e1)=e4))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.13/0.69 fof(f257,plain,(
% 0.13/0.69 sP2_prd<=>(sP4_prd|((((~op(e0,e2)=e0&~op(e1,e2)=e1)&~op(e2,e2)=e2)&~op(e3,e2)=e3)&~op(e4,e2)=e4))),
% 0.13/0.69 inference(formula_renaming,[status(thm)],[f236,f256])).
% 0.13/0.69 fof(f258,plain,(
% 0.13/0.69 (~sP2_prd|(sP4_prd|((((~op(e0,e2)=e0&~op(e1,e2)=e1)&~op(e2,e2)=e2)&~op(e3,e2)=e3)&~op(e4,e2)=e4)))&(sP2_prd|(~sP4_prd&((((op(e0,e2)=e0|op(e1,e2)=e1)|op(e2,e2)=e2)|op(e3,e2)=e3)|op(e4,e2)=e4)))),
% 0.13/0.69 inference(NNF_transformation,[status(thm)],[f257])).
% 0.13/0.69 fof(f259,plain,(
% 0.13/0.69 ~sP2_prd|sP4_prd|~op(e0,e2)=e0),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f258])).
% 0.13/0.69 fof(f261,plain,(
% 0.13/0.69 ~sP2_prd|sP4_prd|~op(e2,e2)=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f258])).
% 0.13/0.69 fof(f264,plain,(
% 0.13/0.69 sP2_prd|~sP4_prd),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f258])).
% 0.13/0.69 fof(f266,definition,(
% 0.13/0.69 sP5_prd<=>(((((~op(e0,e0)=e0&~op(e0,e1)=e1)&~op(e0,e2)=e2)&~op(e0,e3)=e3)&~op(e0,e4)=e4)|((((~op(e1,e0)=e0&~op(e1,e1)=e1)&~op(e1,e2)=e2)&~op(e1,e3)=e3)&~op(e1,e4)=e4))),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.13/0.69 fof(f267,plain,(
% 0.13/0.69 sP3_prd<=>(sP5_prd|((((~op(e2,e0)=e0&~op(e2,e1)=e1)&~op(e2,e2)=e2)&~op(e2,e3)=e3)&~op(e2,e4)=e4))),
% 0.13/0.69 inference(formula_renaming,[status(thm)],[f246,f266])).
% 0.13/0.69 fof(f268,plain,(
% 0.13/0.69 (~sP3_prd|(sP5_prd|((((~op(e2,e0)=e0&~op(e2,e1)=e1)&~op(e2,e2)=e2)&~op(e2,e3)=e3)&~op(e2,e4)=e4)))&(sP3_prd|(~sP5_prd&((((op(e2,e0)=e0|op(e2,e1)=e1)|op(e2,e2)=e2)|op(e2,e3)=e3)|op(e2,e4)=e4)))),
% 0.13/0.69 inference(NNF_transformation,[status(thm)],[f267])).
% 0.13/0.69 fof(f270,plain,(
% 0.13/0.69 ~sP3_prd|sP5_prd|~op(e2,e1)=e1),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f268])).
% 0.13/0.69 fof(f271,plain,(
% 0.13/0.69 ~sP3_prd|sP5_prd|~op(e2,e2)=e2),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f268])).
% 0.13/0.69 fof(f276,definition,(
% 0.13/0.69 sP6_prd<=>((((~op(e0,e0)=e0&~op(e1,e0)=e1)&~op(e2,e0)=e2)&~op(e3,e0)=e3)&~op(e4,e0)=e4)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.13/0.69 fof(f277,plain,(
% 0.13/0.69 sP4_prd<=>(sP6_prd|((((~op(e0,e1)=e0&~op(e1,e1)=e1)&~op(e2,e1)=e2)&~op(e3,e1)=e3)&~op(e4,e1)=e4))),
% 0.13/0.69 inference(formula_renaming,[status(thm)],[f256,f276])).
% 0.13/0.69 fof(f278,plain,(
% 0.13/0.69 (~sP4_prd|(sP6_prd|((((~op(e0,e1)=e0&~op(e1,e1)=e1)&~op(e2,e1)=e2)&~op(e3,e1)=e3)&~op(e4,e1)=e4)))&(sP4_prd|(~sP6_prd&((((op(e0,e1)=e0|op(e1,e1)=e1)|op(e2,e1)=e2)|op(e3,e1)=e3)|op(e4,e1)=e4)))),
% 0.13/0.69 inference(NNF_transformation,[status(thm)],[f277])).
% 0.13/0.69 fof(f282,plain,(
% 0.13/0.69 ~sP4_prd|sP6_prd|~op(e3,e1)=e3),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f278])).
% 0.13/0.69 fof(f285,plain,(
% 0.13/0.69 sP4_prd|op(e0,e1)=e0|op(e1,e1)=e1|op(e2,e1)=e2|op(e3,e1)=e3|op(e4,e1)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f278])).
% 0.13/0.69 fof(f286,definition,(
% 0.13/0.69 sP7_prd<=>((((~op(e0,e0)=e0&~op(e0,e1)=e1)&~op(e0,e2)=e2)&~op(e0,e3)=e3)&~op(e0,e4)=e4)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.13/0.69 fof(f287,plain,(
% 0.13/0.69 sP5_prd<=>(sP7_prd|((((~op(e1,e0)=e0&~op(e1,e1)=e1)&~op(e1,e2)=e2)&~op(e1,e3)=e3)&~op(e1,e4)=e4))),
% 0.13/0.69 inference(formula_renaming,[status(thm)],[f266,f286])).
% 0.13/0.69 fof(f288,plain,(
% 0.13/0.69 (~sP5_prd|(sP7_prd|((((~op(e1,e0)=e0&~op(e1,e1)=e1)&~op(e1,e2)=e2)&~op(e1,e3)=e3)&~op(e1,e4)=e4)))&(sP5_prd|(~sP7_prd&((((op(e1,e0)=e0|op(e1,e1)=e1)|op(e1,e2)=e2)|op(e1,e3)=e3)|op(e1,e4)=e4)))),
% 0.13/0.69 inference(NNF_transformation,[status(thm)],[f287])).
% 0.13/0.69 fof(f289,plain,(
% 0.13/0.69 ~sP5_prd|sP7_prd|~op(e1,e0)=e0),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f288])).
% 0.13/0.69 fof(f296,plain,(
% 0.13/0.69 (~sP6_prd|((((~op(e0,e0)=e0&~op(e1,e0)=e1)&~op(e2,e0)=e2)&~op(e3,e0)=e3)&~op(e4,e0)=e4))&(sP6_prd|((((op(e0,e0)=e0|op(e1,e0)=e1)|op(e2,e0)=e2)|op(e3,e0)=e3)|op(e4,e0)=e4))),
% 0.13/0.69 inference(NNF_transformation,[status(thm)],[f276])).
% 0.13/0.69 fof(f298,plain,(
% 0.13/0.69 ~sP6_prd|~op(e1,e0)=e1),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f296])).
% 0.13/0.69 fof(f301,plain,(
% 0.13/0.69 ~sP6_prd|~op(e4,e0)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f296])).
% 0.13/0.69 fof(f303,plain,(
% 0.13/0.69 (~sP7_prd|((((~op(e0,e0)=e0&~op(e0,e1)=e1)&~op(e0,e2)=e2)&~op(e0,e3)=e3)&~op(e0,e4)=e4))&(sP7_prd|((((op(e0,e0)=e0|op(e0,e1)=e1)|op(e0,e2)=e2)|op(e0,e3)=e3)|op(e0,e4)=e4))),
% 0.13/0.69 inference(NNF_transformation,[status(thm)],[f286])).
% 0.13/0.69 fof(f308,plain,(
% 0.13/0.69 ~sP7_prd|~op(e0,e4)=e4),
% 0.13/0.69 inference(cnf_transformation,[status(thm)],[f303])).
% 0.13/0.69 fof(f310,definition,(
% 0.13/0.69 sQ0_spl <=> (op(e0,e0)=e0)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f311,plain,(
% 0.13/0.69 op(e0,e0)=e0|~sQ0_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f310])).
% 0.13/0.69 fof(f316,definition,(
% 0.13/0.69 sQ2_spl <=> (op(e0,e0)=e2)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f317,plain,(
% 0.13/0.69 op(e0,e0)=e2|~sQ2_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f316])).
% 0.13/0.69 fof(f319,definition,(
% 0.13/0.69 sQ3_spl <=> (op(e0,e0)=e3)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f322,definition,(
% 0.13/0.69 sQ4_spl <=> (op(e0,e0)=e4)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f323,plain,(
% 0.13/0.69 op(e0,e0)=e4|~sQ4_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f322])).
% 0.13/0.69 fof(f326,definition,(
% 0.13/0.69 sQ5_spl <=> (op(e0,e1)=e0)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f332,definition,(
% 0.13/0.69 sQ7_spl <=> (op(e0,e1)=e2)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f333,plain,(
% 0.13/0.69 op(e0,e1)=e2|~sQ7_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f332])).
% 0.13/0.69 fof(f334,plain,(
% 0.13/0.69 ~op(e0,e1)=e2|sQ7_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f332])).
% 0.13/0.69 fof(f335,definition,(
% 0.13/0.69 sQ8_spl <=> (op(e0,e1)=e3)),
% 0.13/0.69 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.69 fof(f336,plain,(
% 0.13/0.69 op(e0,e1)=e3|~sQ8_spl),
% 0.13/0.69 inference(component_clause,[status(thm)],[f335])).
% 0.13/0.70 fof(f338,definition,(
% 0.13/0.70 sQ9_spl <=> (op(e0,e1)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f339,plain,(
% 0.13/0.70 op(e0,e1)=e4|~sQ9_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f338])).
% 0.13/0.70 fof(f342,definition,(
% 0.13/0.70 sQ10_spl <=> (op(e0,e2)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f343,plain,(
% 0.13/0.70 op(e0,e2)=e0|~sQ10_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f342])).
% 0.13/0.70 fof(f345,definition,(
% 0.13/0.70 sQ11_spl <=> (op(e0,e2)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f346,plain,(
% 0.13/0.70 op(e0,e2)=e1|~sQ11_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f345])).
% 0.13/0.70 fof(f348,definition,(
% 0.13/0.70 sQ12_spl <=> (op(e0,e2)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f349,plain,(
% 0.13/0.70 op(e0,e2)=e2|~sQ12_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f348])).
% 0.13/0.70 fof(f351,definition,(
% 0.13/0.70 sQ13_spl <=> (op(e0,e2)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f352,plain,(
% 0.13/0.70 op(e0,e2)=e3|~sQ13_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f351])).
% 0.13/0.70 fof(f354,definition,(
% 0.13/0.70 sQ14_spl <=> (op(e0,e2)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f355,plain,(
% 0.13/0.70 op(e0,e2)=e4|~sQ14_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f354])).
% 0.13/0.70 fof(f357,plain,(
% 0.13/0.70 sQ10_spl|sQ11_spl|sQ12_spl|sQ13_spl|sQ14_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f11,f342,f345,f348,f351,f354])).
% 0.13/0.70 fof(f358,definition,(
% 0.13/0.70 sQ15_spl <=> (op(e0,e3)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f359,plain,(
% 0.13/0.70 op(e0,e3)=e0|~sQ15_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f358])).
% 0.13/0.70 fof(f361,definition,(
% 0.13/0.70 sQ16_spl <=> (op(e0,e3)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f362,plain,(
% 0.13/0.70 op(e0,e3)=e1|~sQ16_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f361])).
% 0.13/0.70 fof(f364,definition,(
% 0.13/0.70 sQ17_spl <=> (op(e0,e3)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f365,plain,(
% 0.13/0.70 op(e0,e3)=e2|~sQ17_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f364])).
% 0.13/0.70 fof(f374,definition,(
% 0.13/0.70 sQ20_spl <=> (op(e0,e4)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f375,plain,(
% 0.13/0.70 op(e0,e4)=e0|~sQ20_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f374])).
% 0.13/0.70 fof(f377,definition,(
% 0.13/0.70 sQ21_spl <=> (op(e0,e4)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f378,plain,(
% 0.13/0.70 op(e0,e4)=e1|~sQ21_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f377])).
% 0.13/0.70 fof(f380,definition,(
% 0.13/0.70 sQ22_spl <=> (op(e0,e4)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f381,plain,(
% 0.13/0.70 op(e0,e4)=e2|~sQ22_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f380])).
% 0.13/0.70 fof(f383,definition,(
% 0.13/0.70 sQ23_spl <=> (op(e0,e4)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f384,plain,(
% 0.13/0.70 op(e0,e4)=e3|~sQ23_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f383])).
% 0.13/0.70 fof(f386,definition,(
% 0.13/0.70 sQ24_spl <=> (op(e0,e4)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f387,plain,(
% 0.13/0.70 op(e0,e4)=e4|~sQ24_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f386])).
% 0.13/0.70 fof(f389,plain,(
% 0.13/0.70 sQ20_spl|sQ21_spl|sQ22_spl|sQ23_spl|sQ24_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f13,f374,f377,f380,f383,f386])).
% 0.13/0.70 fof(f390,definition,(
% 0.13/0.70 sQ25_spl <=> (op(e1,e0)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f391,plain,(
% 0.13/0.70 op(e1,e0)=e0|~sQ25_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f390])).
% 0.13/0.70 fof(f393,definition,(
% 0.13/0.70 sQ26_spl <=> (op(e1,e0)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f394,plain,(
% 0.13/0.70 op(e1,e0)=e1|~sQ26_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f393])).
% 0.13/0.70 fof(f396,definition,(
% 0.13/0.70 sQ27_spl <=> (op(e1,e0)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f397,plain,(
% 0.13/0.70 op(e1,e0)=e2|~sQ27_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f396])).
% 0.13/0.70 fof(f399,definition,(
% 0.13/0.70 sQ28_spl <=> (op(e1,e0)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f400,plain,(
% 0.13/0.70 op(e1,e0)=e3|~sQ28_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f399])).
% 0.13/0.70 fof(f402,definition,(
% 0.13/0.70 sQ29_spl <=> (op(e1,e0)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f403,plain,(
% 0.13/0.70 op(e1,e0)=e4|~sQ29_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f402])).
% 0.13/0.70 fof(f405,plain,(
% 0.13/0.70 sQ25_spl|sQ26_spl|sQ27_spl|sQ28_spl|sQ29_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f14,f390,f393,f396,f399,f402])).
% 0.13/0.70 fof(f409,definition,(
% 0.13/0.70 sQ31_spl <=> (op(e1,e1)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f410,plain,(
% 0.13/0.70 op(e1,e1)=e1|~sQ31_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f409])).
% 0.13/0.70 fof(f412,definition,(
% 0.13/0.70 sQ32_spl <=> (op(e1,e1)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f413,plain,(
% 0.13/0.70 op(e1,e1)=e2|~sQ32_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f412])).
% 0.13/0.70 fof(f415,definition,(
% 0.13/0.70 sQ33_spl <=> (op(e1,e1)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f416,plain,(
% 0.13/0.70 op(e1,e1)=e3|~sQ33_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f415])).
% 0.13/0.70 fof(f418,definition,(
% 0.13/0.70 sQ34_spl <=> (op(e1,e1)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f422,definition,(
% 0.13/0.70 sQ35_spl <=> (op(e1,e2)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f423,plain,(
% 0.13/0.70 op(e1,e2)=e0|~sQ35_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f422])).
% 0.13/0.70 fof(f425,definition,(
% 0.13/0.70 sQ36_spl <=> (op(e1,e2)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f426,plain,(
% 0.13/0.70 op(e1,e2)=e1|~sQ36_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f425])).
% 0.13/0.70 fof(f428,definition,(
% 0.13/0.70 sQ37_spl <=> (op(e1,e2)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f429,plain,(
% 0.13/0.70 op(e1,e2)=e2|~sQ37_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f428])).
% 0.13/0.70 fof(f431,definition,(
% 0.13/0.70 sQ38_spl <=> (op(e1,e2)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f432,plain,(
% 0.13/0.70 op(e1,e2)=e3|~sQ38_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f431])).
% 0.13/0.70 fof(f434,definition,(
% 0.13/0.70 sQ39_spl <=> (op(e1,e2)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f435,plain,(
% 0.13/0.70 op(e1,e2)=e4|~sQ39_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f434])).
% 0.13/0.70 fof(f437,plain,(
% 0.13/0.70 sQ35_spl|sQ36_spl|sQ37_spl|sQ38_spl|sQ39_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f16,f422,f425,f428,f431,f434])).
% 0.13/0.70 fof(f438,definition,(
% 0.13/0.70 sQ40_spl <=> (op(e1,e3)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f439,plain,(
% 0.13/0.70 op(e1,e3)=e0|~sQ40_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f438])).
% 0.13/0.70 fof(f441,definition,(
% 0.13/0.70 sQ41_spl <=> (op(e1,e3)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f444,definition,(
% 0.13/0.70 sQ42_spl <=> (op(e1,e3)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f445,plain,(
% 0.13/0.70 op(e1,e3)=e2|~sQ42_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f444])).
% 0.13/0.70 fof(f447,definition,(
% 0.13/0.70 sQ43_spl <=> (op(e1,e3)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f448,plain,(
% 0.13/0.70 op(e1,e3)=e3|~sQ43_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f447])).
% 0.13/0.70 fof(f450,definition,(
% 0.13/0.70 sQ44_spl <=> (op(e1,e3)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f451,plain,(
% 0.13/0.70 op(e1,e3)=e4|~sQ44_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f450])).
% 0.13/0.70 fof(f453,plain,(
% 0.13/0.70 sQ40_spl|sQ41_spl|sQ42_spl|sQ43_spl|sQ44_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f17,f438,f441,f444,f447,f450])).
% 0.13/0.70 fof(f454,definition,(
% 0.13/0.70 sQ45_spl <=> (op(e1,e4)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f455,plain,(
% 0.13/0.70 op(e1,e4)=e0|~sQ45_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f454])).
% 0.13/0.70 fof(f457,definition,(
% 0.13/0.70 sQ46_spl <=> (op(e1,e4)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f458,plain,(
% 0.13/0.70 op(e1,e4)=e1|~sQ46_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f457])).
% 0.13/0.70 fof(f460,definition,(
% 0.13/0.70 sQ47_spl <=> (op(e1,e4)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f463,definition,(
% 0.13/0.70 sQ48_spl <=> (op(e1,e4)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f464,plain,(
% 0.13/0.70 op(e1,e4)=e3|~sQ48_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f463])).
% 0.13/0.70 fof(f466,definition,(
% 0.13/0.70 sQ49_spl <=> (op(e1,e4)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f467,plain,(
% 0.13/0.70 op(e1,e4)=e4|~sQ49_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f466])).
% 0.13/0.70 fof(f469,plain,(
% 0.13/0.70 sQ45_spl|sQ46_spl|sQ47_spl|sQ48_spl|sQ49_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f18,f454,f457,f460,f463,f466])).
% 0.13/0.70 fof(f470,definition,(
% 0.13/0.70 sQ50_spl <=> (op(e2,e0)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f471,plain,(
% 0.13/0.70 op(e2,e0)=e0|~sQ50_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f470])).
% 0.13/0.70 fof(f473,definition,(
% 0.13/0.70 sQ51_spl <=> (op(e2,e0)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f474,plain,(
% 0.13/0.70 op(e2,e0)=e1|~sQ51_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f473])).
% 0.13/0.70 fof(f476,definition,(
% 0.13/0.70 sQ52_spl <=> (op(e2,e0)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f477,plain,(
% 0.13/0.70 op(e2,e0)=e2|~sQ52_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f476])).
% 0.13/0.70 fof(f479,definition,(
% 0.13/0.70 sQ53_spl <=> (op(e2,e0)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f480,plain,(
% 0.13/0.70 op(e2,e0)=e3|~sQ53_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f479])).
% 0.13/0.70 fof(f486,definition,(
% 0.13/0.70 sQ55_spl <=> (op(e2,e1)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f489,definition,(
% 0.13/0.70 sQ56_spl <=> (op(e2,e1)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f492,definition,(
% 0.13/0.70 sQ57_spl <=> (op(e2,e1)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f493,plain,(
% 0.13/0.70 op(e2,e1)=e2|~sQ57_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f492])).
% 0.13/0.70 fof(f495,definition,(
% 0.13/0.70 sQ58_spl <=> (op(e2,e1)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f496,plain,(
% 0.13/0.70 op(e2,e1)=e3|~sQ58_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f495])).
% 0.13/0.70 fof(f498,definition,(
% 0.13/0.70 sQ59_spl <=> (op(e2,e1)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f499,plain,(
% 0.13/0.70 op(e2,e1)=e4|~sQ59_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f498])).
% 0.13/0.70 fof(f501,plain,(
% 0.13/0.70 sQ55_spl|sQ56_spl|sQ57_spl|sQ58_spl|sQ59_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f20,f486,f489,f492,f495,f498])).
% 0.13/0.70 fof(f502,definition,(
% 0.13/0.70 sQ60_spl <=> (op(e2,e2)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f505,definition,(
% 0.13/0.70 sQ61_spl <=> (op(e2,e2)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f508,definition,(
% 0.13/0.70 sQ62_spl <=> (op(e2,e2)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f511,definition,(
% 0.13/0.70 sQ63_spl <=> (op(e2,e2)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f512,plain,(
% 0.13/0.70 op(e2,e2)=e3|~sQ63_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f511])).
% 0.13/0.70 fof(f514,definition,(
% 0.13/0.70 sQ64_spl <=> (op(e2,e2)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f515,plain,(
% 0.13/0.70 op(e2,e2)=e4|~sQ64_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f514])).
% 0.13/0.70 fof(f517,plain,(
% 0.13/0.70 sQ60_spl|sQ61_spl|sQ62_spl|sQ63_spl|sQ64_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f21,f502,f505,f508,f511,f514])).
% 0.13/0.70 fof(f521,definition,(
% 0.13/0.70 sQ66_spl <=> (op(e2,e3)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f522,plain,(
% 0.13/0.70 op(e2,e3)=e1|~sQ66_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f521])).
% 0.13/0.70 fof(f524,definition,(
% 0.13/0.70 sQ67_spl <=> (op(e2,e3)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f527,definition,(
% 0.13/0.70 sQ68_spl <=> (op(e2,e3)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f528,plain,(
% 0.13/0.70 op(e2,e3)=e3|~sQ68_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f527])).
% 0.13/0.70 fof(f534,definition,(
% 0.13/0.70 sQ70_spl <=> (op(e2,e4)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f535,plain,(
% 0.13/0.70 op(e2,e4)=e0|~sQ70_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f534])).
% 0.13/0.70 fof(f537,definition,(
% 0.13/0.70 sQ71_spl <=> (op(e2,e4)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f538,plain,(
% 0.13/0.70 op(e2,e4)=e1|~sQ71_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f537])).
% 0.13/0.70 fof(f540,definition,(
% 0.13/0.70 sQ72_spl <=> (op(e2,e4)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f543,definition,(
% 0.13/0.70 sQ73_spl <=> (op(e2,e4)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f546,definition,(
% 0.13/0.70 sQ74_spl <=> (op(e2,e4)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f550,definition,(
% 0.13/0.70 sQ75_spl <=> (op(e3,e0)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f551,plain,(
% 0.13/0.70 op(e3,e0)=e0|~sQ75_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f550])).
% 0.13/0.70 fof(f553,definition,(
% 0.13/0.70 sQ76_spl <=> (op(e3,e0)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f554,plain,(
% 0.13/0.70 op(e3,e0)=e1|~sQ76_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f553])).
% 0.13/0.70 fof(f556,definition,(
% 0.13/0.70 sQ77_spl <=> (op(e3,e0)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f557,plain,(
% 0.13/0.70 op(e3,e0)=e2|~sQ77_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f556])).
% 0.13/0.70 fof(f559,definition,(
% 0.13/0.70 sQ78_spl <=> (op(e3,e0)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f560,plain,(
% 0.13/0.70 op(e3,e0)=e3|~sQ78_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f559])).
% 0.13/0.70 fof(f562,definition,(
% 0.13/0.70 sQ79_spl <=> (op(e3,e0)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f563,plain,(
% 0.13/0.70 op(e3,e0)=e4|~sQ79_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f562])).
% 0.13/0.70 fof(f565,plain,(
% 0.13/0.70 sQ75_spl|sQ76_spl|sQ77_spl|sQ78_spl|sQ79_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f24,f550,f553,f556,f559,f562])).
% 0.13/0.70 fof(f566,definition,(
% 0.13/0.70 sQ80_spl <=> (op(e3,e1)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f567,plain,(
% 0.13/0.70 op(e3,e1)=e0|~sQ80_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f566])).
% 0.13/0.70 fof(f569,definition,(
% 0.13/0.70 sQ81_spl <=> (op(e3,e1)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f570,plain,(
% 0.13/0.70 op(e3,e1)=e1|~sQ81_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f569])).
% 0.13/0.70 fof(f572,definition,(
% 0.13/0.70 sQ82_spl <=> (op(e3,e1)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f573,plain,(
% 0.13/0.70 op(e3,e1)=e2|~sQ82_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f572])).
% 0.13/0.70 fof(f575,definition,(
% 0.13/0.70 sQ83_spl <=> (op(e3,e1)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f576,plain,(
% 0.13/0.70 op(e3,e1)=e3|~sQ83_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f575])).
% 0.13/0.70 fof(f578,definition,(
% 0.13/0.70 sQ84_spl <=> (op(e3,e1)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f579,plain,(
% 0.13/0.70 op(e3,e1)=e4|~sQ84_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f578])).
% 0.13/0.70 fof(f581,plain,(
% 0.13/0.70 sQ80_spl|sQ81_spl|sQ82_spl|sQ83_spl|sQ84_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f25,f566,f569,f572,f575,f578])).
% 0.13/0.70 fof(f582,definition,(
% 0.13/0.70 sQ85_spl <=> (op(e3,e2)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f583,plain,(
% 0.13/0.70 op(e3,e2)=e0|~sQ85_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f582])).
% 0.13/0.70 fof(f588,definition,(
% 0.13/0.70 sQ87_spl <=> (op(e3,e2)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f589,plain,(
% 0.13/0.70 op(e3,e2)=e2|~sQ87_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f588])).
% 0.13/0.70 fof(f591,definition,(
% 0.13/0.70 sQ88_spl <=> (op(e3,e2)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f592,plain,(
% 0.13/0.70 op(e3,e2)=e3|~sQ88_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f591])).
% 0.13/0.70 fof(f594,definition,(
% 0.13/0.70 sQ89_spl <=> (op(e3,e2)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f595,plain,(
% 0.13/0.70 op(e3,e2)=e4|~sQ89_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f594])).
% 0.13/0.70 fof(f598,definition,(
% 0.13/0.70 sQ90_spl <=> (op(e3,e3)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f599,plain,(
% 0.13/0.70 op(e3,e3)=e0|~sQ90_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f598])).
% 0.13/0.70 fof(f600,plain,(
% 0.13/0.70 ~op(e3,e3)=e0|sQ90_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f598])).
% 0.13/0.70 fof(f601,definition,(
% 0.13/0.70 sQ91_spl <=> (op(e3,e3)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f602,plain,(
% 0.13/0.70 op(e3,e3)=e1|~sQ91_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f601])).
% 0.13/0.70 fof(f604,definition,(
% 0.13/0.70 sQ92_spl <=> (op(e3,e3)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f605,plain,(
% 0.13/0.70 op(e3,e3)=e2|~sQ92_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f604])).
% 0.13/0.70 fof(f607,definition,(
% 0.13/0.70 sQ93_spl <=> (op(e3,e3)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f608,plain,(
% 0.13/0.70 op(e3,e3)=e3|~sQ93_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f607])).
% 0.13/0.70 fof(f610,definition,(
% 0.13/0.70 sQ94_spl <=> (op(e3,e3)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f611,plain,(
% 0.13/0.70 op(e3,e3)=e4|~sQ94_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f610])).
% 0.13/0.70 fof(f614,definition,(
% 0.13/0.70 sQ95_spl <=> (op(e3,e4)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f615,plain,(
% 0.13/0.70 op(e3,e4)=e0|~sQ95_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f614])).
% 0.13/0.70 fof(f617,definition,(
% 0.13/0.70 sQ96_spl <=> (op(e3,e4)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f618,plain,(
% 0.13/0.70 op(e3,e4)=e1|~sQ96_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f617])).
% 0.13/0.70 fof(f620,definition,(
% 0.13/0.70 sQ97_spl <=> (op(e3,e4)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f621,plain,(
% 0.13/0.70 op(e3,e4)=e2|~sQ97_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f620])).
% 0.13/0.70 fof(f623,definition,(
% 0.13/0.70 sQ98_spl <=> (op(e3,e4)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f624,plain,(
% 0.13/0.70 op(e3,e4)=e3|~sQ98_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f623])).
% 0.13/0.70 fof(f626,definition,(
% 0.13/0.70 sQ99_spl <=> (op(e3,e4)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f627,plain,(
% 0.13/0.70 op(e3,e4)=e4|~sQ99_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f626])).
% 0.13/0.70 fof(f629,plain,(
% 0.13/0.70 sQ95_spl|sQ96_spl|sQ97_spl|sQ98_spl|sQ99_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f28,f614,f617,f620,f623,f626])).
% 0.13/0.70 fof(f630,definition,(
% 0.13/0.70 sQ100_spl <=> (op(e4,e0)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f631,plain,(
% 0.13/0.70 op(e4,e0)=e0|~sQ100_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f630])).
% 0.13/0.70 fof(f633,definition,(
% 0.13/0.70 sQ101_spl <=> (op(e4,e0)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f634,plain,(
% 0.13/0.70 op(e4,e0)=e1|~sQ101_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f633])).
% 0.13/0.70 fof(f636,definition,(
% 0.13/0.70 sQ102_spl <=> (op(e4,e0)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f637,plain,(
% 0.13/0.70 op(e4,e0)=e2|~sQ102_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f636])).
% 0.13/0.70 fof(f639,definition,(
% 0.13/0.70 sQ103_spl <=> (op(e4,e0)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f640,plain,(
% 0.13/0.70 op(e4,e0)=e3|~sQ103_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f639])).
% 0.13/0.70 fof(f642,definition,(
% 0.13/0.70 sQ104_spl <=> (op(e4,e0)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f643,plain,(
% 0.13/0.70 op(e4,e0)=e4|~sQ104_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f642])).
% 0.13/0.70 fof(f645,plain,(
% 0.13/0.70 sQ100_spl|sQ101_spl|sQ102_spl|sQ103_spl|sQ104_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f29,f630,f633,f636,f639,f642])).
% 0.13/0.70 fof(f646,definition,(
% 0.13/0.70 sQ105_spl <=> (op(e4,e1)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f647,plain,(
% 0.13/0.70 op(e4,e1)=e0|~sQ105_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f646])).
% 0.13/0.70 fof(f648,plain,(
% 0.13/0.70 ~op(e4,e1)=e0|sQ105_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f646])).
% 0.13/0.70 fof(f649,definition,(
% 0.13/0.70 sQ106_spl <=> (op(e4,e1)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f650,plain,(
% 0.13/0.70 op(e4,e1)=e1|~sQ106_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f649])).
% 0.13/0.70 fof(f652,definition,(
% 0.13/0.70 sQ107_spl <=> (op(e4,e1)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f653,plain,(
% 0.13/0.70 op(e4,e1)=e2|~sQ107_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f652])).
% 0.13/0.70 fof(f655,definition,(
% 0.13/0.70 sQ108_spl <=> (op(e4,e1)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f656,plain,(
% 0.13/0.70 op(e4,e1)=e3|~sQ108_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f655])).
% 0.13/0.70 fof(f658,definition,(
% 0.13/0.70 sQ109_spl <=> (op(e4,e1)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f659,plain,(
% 0.13/0.70 op(e4,e1)=e4|~sQ109_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f658])).
% 0.13/0.70 fof(f662,definition,(
% 0.13/0.70 sQ110_spl <=> (op(e4,e2)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f663,plain,(
% 0.13/0.70 op(e4,e2)=e0|~sQ110_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f662])).
% 0.13/0.70 fof(f665,definition,(
% 0.13/0.70 sQ111_spl <=> (op(e4,e2)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f666,plain,(
% 0.13/0.70 op(e4,e2)=e1|~sQ111_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f665])).
% 0.13/0.70 fof(f668,definition,(
% 0.13/0.70 sQ112_spl <=> (op(e4,e2)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f671,definition,(
% 0.13/0.70 sQ113_spl <=> (op(e4,e2)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f672,plain,(
% 0.13/0.70 op(e4,e2)=e3|~sQ113_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f671])).
% 0.13/0.70 fof(f674,definition,(
% 0.13/0.70 sQ114_spl <=> (op(e4,e2)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f675,plain,(
% 0.13/0.70 op(e4,e2)=e4|~sQ114_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f674])).
% 0.13/0.70 fof(f677,plain,(
% 0.13/0.70 sQ110_spl|sQ111_spl|sQ112_spl|sQ113_spl|sQ114_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f31,f662,f665,f668,f671,f674])).
% 0.13/0.70 fof(f678,definition,(
% 0.13/0.70 sQ115_spl <=> (op(e4,e3)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f679,plain,(
% 0.13/0.70 op(e4,e3)=e0|~sQ115_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f678])).
% 0.13/0.70 fof(f681,definition,(
% 0.13/0.70 sQ116_spl <=> (op(e4,e3)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f682,plain,(
% 0.13/0.70 op(e4,e3)=e1|~sQ116_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f681])).
% 0.13/0.70 fof(f687,definition,(
% 0.13/0.70 sQ118_spl <=> (op(e4,e3)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f688,plain,(
% 0.13/0.70 op(e4,e3)=e3|~sQ118_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f687])).
% 0.13/0.70 fof(f690,definition,(
% 0.13/0.70 sQ119_spl <=> (op(e4,e3)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f694,definition,(
% 0.13/0.70 sQ120_spl <=> (op(e4,e4)=e0)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f695,plain,(
% 0.13/0.70 op(e4,e4)=e0|~sQ120_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f694])).
% 0.13/0.70 fof(f697,definition,(
% 0.13/0.70 sQ121_spl <=> (op(e4,e4)=e1)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f700,definition,(
% 0.13/0.70 sQ122_spl <=> (op(e4,e4)=e2)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f701,plain,(
% 0.13/0.70 op(e4,e4)=e2|~sQ122_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f700])).
% 0.13/0.70 fof(f703,definition,(
% 0.13/0.70 sQ123_spl <=> (op(e4,e4)=e3)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f704,plain,(
% 0.13/0.70 op(e4,e4)=e3|~sQ123_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f703])).
% 0.13/0.70 fof(f706,definition,(
% 0.13/0.70 sQ124_spl <=> (op(e4,e4)=e4)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f707,plain,(
% 0.13/0.70 op(e4,e4)=e4|~sQ124_spl),
% 0.13/0.70 inference(component_clause,[status(thm)],[f706])).
% 0.13/0.70 fof(f709,plain,(
% 0.13/0.70 sQ120_spl|sQ121_spl|sQ122_spl|sQ123_spl|sQ124_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f33,f694,f697,f700,f703,f706])).
% 0.13/0.70 fof(f710,plain,(
% 0.13/0.70 sQ0_spl|sQ5_spl|sQ10_spl|sQ15_spl|sQ20_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f34,f310,f326,f342,f358,f374])).
% 0.13/0.70 fof(f717,plain,(
% 0.13/0.70 sQ3_spl|sQ28_spl|sQ53_spl|sQ78_spl|sQ103_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f41,f319,f399,f479,f559,f639])).
% 0.13/0.70 fof(f726,plain,(
% 0.13/0.70 sQ28_spl|sQ33_spl|sQ38_spl|sQ43_spl|sQ48_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f50,f399,f415,f431,f447,f463])).
% 0.13/0.70 fof(f728,plain,(
% 0.13/0.70 sQ29_spl|sQ34_spl|sQ39_spl|sQ44_spl|sQ49_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f52,f402,f418,f434,f450,f466])).
% 0.13/0.70 fof(f734,plain,(
% 0.13/0.70 sQ52_spl|sQ57_spl|sQ62_spl|sQ67_spl|sQ72_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f58,f476,f492,f508,f524,f540])).
% 0.13/0.70 fof(f735,plain,(
% 0.13/0.70 sQ12_spl|sQ37_spl|sQ62_spl|sQ87_spl|sQ112_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f59,f348,f428,f508,f588,f668])).
% 0.13/0.70 fof(f736,plain,(
% 0.13/0.70 sQ53_spl|sQ58_spl|sQ63_spl|sQ68_spl|sQ73_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f60,f479,f495,f511,f527,f543])).
% 0.13/0.70 fof(f739,plain,(
% 0.13/0.70 sQ14_spl|sQ39_spl|sQ64_spl|sQ89_spl|sQ114_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f63,f354,f434,f514,f594,f674])).
% 0.13/0.70 fof(f744,plain,(
% 0.13/0.70 sQ77_spl|sQ82_spl|sQ87_spl|sQ92_spl|sQ97_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f68,f556,f572,f588,f604,f620])).
% 0.13/0.70 fof(f746,plain,(
% 0.13/0.70 sQ78_spl|sQ83_spl|sQ88_spl|sQ93_spl|sQ98_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f70,f559,f575,f591,f607,f623])).
% 0.13/0.70 fof(f748,plain,(
% 0.13/0.70 sQ79_spl|sQ84_spl|sQ89_spl|sQ94_spl|sQ99_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f72,f562,f578,f594,f610,f626])).
% 0.13/0.70 fof(f751,plain,(
% 0.13/0.70 sQ20_spl|sQ45_spl|sQ70_spl|sQ95_spl|sQ120_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f75,f374,f454,f534,f614,f694])).
% 0.13/0.70 fof(f756,plain,(
% 0.13/0.70 sQ103_spl|sQ108_spl|sQ113_spl|sQ118_spl|sQ123_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f80,f639,f655,f671,f687,f703])).
% 0.13/0.70 fof(f758,plain,(
% 0.13/0.70 sQ104_spl|sQ109_spl|sQ114_spl|sQ119_spl|sQ124_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f82,f642,f658,f674,f690,f706])).
% 0.13/0.70 fof(f760,definition,(
% 0.13/0.70 sQ125_spl <=> (sP0_prd)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f763,plain,(
% 0.13/0.70 sQ125_spl|~sQ20_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f226,f760,f374])).
% 0.13/0.70 fof(f766,plain,(
% 0.13/0.70 sQ125_spl|~sQ98_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f229,f760,f623])).
% 0.13/0.70 fof(f768,definition,(
% 0.13/0.70 sQ126_spl <=> (sP1_prd)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f774,plain,(
% 0.13/0.70 sQ126_spl|~sQ118_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f234,f768,f687])).
% 0.13/0.70 fof(f776,definition,(
% 0.13/0.70 sQ127_spl <=> (sP2_prd)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f780,plain,(
% 0.13/0.70 ~sQ125_spl|sQ127_spl|~sQ41_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f240,f760,f776,f441])).
% 0.13/0.70 fof(f783,plain,(
% 0.13/0.70 ~sQ125_spl|sQ127_spl|~sQ119_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f243,f760,f776,f690])).
% 0.13/0.70 fof(f784,plain,(
% 0.13/0.70 sQ125_spl|~sQ127_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f244,f760,f776])).
% 0.13/0.70 fof(f786,definition,(
% 0.13/0.70 sQ128_spl <=> (sP3_prd)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f790,plain,(
% 0.13/0.70 ~sQ126_spl|sQ128_spl|~sQ81_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f250,f768,f786,f569])).
% 0.13/0.70 fof(f791,plain,(
% 0.13/0.70 ~sQ126_spl|sQ128_spl|~sQ87_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f251,f768,f786,f588])).
% 0.13/0.70 fof(f796,definition,(
% 0.13/0.70 sQ129_spl <=> (sP4_prd)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f799,plain,(
% 0.13/0.70 ~sQ127_spl|sQ129_spl|~sQ10_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f259,f776,f796,f342])).
% 0.13/0.70 fof(f801,plain,(
% 0.13/0.70 ~sQ127_spl|sQ129_spl|~sQ62_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f261,f776,f796,f508])).
% 0.13/0.70 fof(f804,plain,(
% 0.13/0.70 sQ127_spl|~sQ129_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f264,f776,f796])).
% 0.13/0.70 fof(f806,definition,(
% 0.13/0.70 sQ130_spl <=> (sP5_prd)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f810,plain,(
% 0.13/0.70 ~sQ128_spl|sQ130_spl|~sQ56_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f270,f786,f806,f489])).
% 0.13/0.70 fof(f811,plain,(
% 0.13/0.70 ~sQ128_spl|sQ130_spl|~sQ62_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f271,f786,f806,f508])).
% 0.13/0.70 fof(f816,definition,(
% 0.13/0.70 sQ131_spl <=> (sP6_prd)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f822,plain,(
% 0.13/0.70 ~sQ129_spl|sQ131_spl|~sQ83_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f282,f796,f816,f575])).
% 0.13/0.70 fof(f825,plain,(
% 0.13/0.70 sQ129_spl|sQ5_spl|sQ31_spl|sQ57_spl|sQ83_spl|sQ109_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f285,f796,f326,f409,f492,f575,f658])).
% 0.13/0.70 fof(f826,definition,(
% 0.13/0.70 sQ132_spl <=> (sP7_prd)),
% 0.13/0.70 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.13/0.70 fof(f829,plain,(
% 0.13/0.70 ~sQ130_spl|sQ132_spl|~sQ25_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f289,f806,f826,f390])).
% 0.13/0.70 fof(f837,plain,(
% 0.13/0.70 ~sQ131_spl|~sQ26_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f298,f816,f393])).
% 0.13/0.70 fof(f840,plain,(
% 0.13/0.70 ~sQ131_spl|~sQ104_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f301,f816,f642])).
% 0.13/0.70 fof(f846,plain,(
% 0.13/0.70 ~sQ132_spl|~sQ24_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f308,f826,f386])).
% 0.13/0.70 fof(f848,plain,(
% 0.13/0.70 e1=e3|~sQ123_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f704])).
% 0.13/0.70 fof(f849,plain,(
% 0.13/0.70 $false|~sQ123_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f848,f214])).
% 0.13/0.70 fof(f850,plain,(
% 0.13/0.70 ~sQ123_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f849])).
% 0.13/0.70 fof(f852,plain,(
% 0.13/0.70 op(e1,op(e4,e4))=e4),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f108])).
% 0.13/0.70 fof(f854,plain,(
% 0.13/0.70 op(e1,e1)=e4),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f852])).
% 0.13/0.70 fof(f858,plain,(
% 0.13/0.70 op(e3,op(e4,e1))=e4|~sQ48_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f464,f105])).
% 0.13/0.70 fof(f859,plain,(
% 0.13/0.70 op(op(e4,e1),e3)=e1|~sQ48_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f464,f93])).
% 0.13/0.70 fof(f864,plain,(
% 0.13/0.70 ~op(e0,e0)=e3|~sQ103_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f640,f112])).
% 0.13/0.70 fof(f865,plain,(
% 0.13/0.70 e1=e2|~sQ122_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f701])).
% 0.13/0.70 fof(f866,plain,(
% 0.13/0.70 $false|~sQ122_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f865,f213])).
% 0.13/0.70 fof(f867,plain,(
% 0.13/0.70 ~sQ122_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f866])).
% 0.13/0.70 fof(f885,plain,(
% 0.13/0.70 ~op(e0,e1)=e4),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f854,f119])).
% 0.13/0.70 fof(f886,plain,(
% 0.13/0.70 ~e4=op(e2,e1)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f854,f123])).
% 0.13/0.70 fof(f887,plain,(
% 0.13/0.70 ~e4=op(e3,e1)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f854,f124])).
% 0.13/0.70 fof(f890,plain,(
% 0.13/0.70 ~op(e1,e2)=e3|~sQ113_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f672,f135])).
% 0.13/0.70 fof(f891,plain,(
% 0.13/0.70 ~op(e2,e2)=e3|~sQ113_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f672,f137])).
% 0.13/0.70 fof(f892,plain,(
% 0.13/0.70 ~op(e3,e2)=e3|~sQ113_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f672,f138])).
% 0.13/0.70 fof(f908,plain,(
% 0.13/0.70 e3=e4|~sQ113_spl|~sQ114_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f672,f675])).
% 0.13/0.70 fof(f909,plain,(
% 0.13/0.70 $false|~sQ113_spl|~sQ114_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f908,f218])).
% 0.13/0.70 fof(f910,plain,(
% 0.13/0.70 ~sQ113_spl|~sQ114_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f909])).
% 0.13/0.70 fof(f915,plain,(
% 0.13/0.70 ~e1=op(e4,e4)|~sQ21_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f378,f152])).
% 0.13/0.70 fof(f916,plain,(
% 0.13/0.70 ~e1=e1|~sQ21_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f915])).
% 0.13/0.70 fof(f917,plain,(
% 0.13/0.70 $false|~sQ21_spl),
% 0.13/0.70 inference(trivial_equality_resolution,[status(thm)],[f916])).
% 0.13/0.70 fof(f918,plain,(
% 0.13/0.70 ~sQ21_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f917])).
% 0.13/0.70 fof(f923,plain,(
% 0.13/0.70 ~op(e1,e4)=e1),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f155])).
% 0.13/0.70 fof(f924,plain,(
% 0.13/0.70 ~op(e2,e4)=e1),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f157])).
% 0.13/0.70 fof(f925,plain,(
% 0.13/0.70 ~op(e3,e4)=e1),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f158])).
% 0.13/0.70 fof(f926,plain,(
% 0.13/0.70 e1=e0|~sQ120_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f695,f220])).
% 0.13/0.70 fof(f927,plain,(
% 0.13/0.70 $false|~sQ120_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f926,f209])).
% 0.13/0.70 fof(f928,plain,(
% 0.13/0.70 ~sQ120_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f927])).
% 0.13/0.70 fof(f939,plain,(
% 0.13/0.70 ~op(e2,e1)=e0|~sQ105_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f647,f127])).
% 0.13/0.70 fof(f941,plain,(
% 0.13/0.70 ~op(e0,e1)=e0|~sQ105_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f647,f122])).
% 0.13/0.70 fof(f946,plain,(
% 0.13/0.70 op(op(e3,e3),e4)=e3|~sQ94_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f611,f102])).
% 0.13/0.70 fof(f947,plain,(
% 0.13/0.70 op(e4,e4)=e3|~sQ94_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f611,f946])).
% 0.13/0.70 fof(f948,plain,(
% 0.13/0.70 ~op(e1,e0)=e4),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f854,f169])).
% 0.13/0.70 fof(f949,plain,(
% 0.13/0.70 ~op(e1,e0)=e0|~sQ45_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f455,f172])).
% 0.13/0.70 fof(f950,plain,(
% 0.13/0.70 ~e4=op(e1,e2)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f854,f173])).
% 0.13/0.70 fof(f951,plain,(
% 0.13/0.70 ~e4=op(e1,e3)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f854,f174])).
% 0.13/0.70 fof(f952,plain,(
% 0.13/0.70 ~e4=op(e1,e4)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f854,f175])).
% 0.13/0.70 fof(f954,plain,(
% 0.13/0.70 ~op(e1,e2)=e0|~sQ45_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f455,f177])).
% 0.13/0.70 fof(f960,plain,(
% 0.13/0.70 $false|~sQ44_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f451,f951])).
% 0.13/0.70 fof(f961,plain,(
% 0.13/0.70 ~sQ44_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f960])).
% 0.13/0.70 fof(f973,plain,(
% 0.13/0.70 $false|~sQ84_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f579,f887])).
% 0.13/0.70 fof(f974,plain,(
% 0.13/0.70 ~sQ84_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f973])).
% 0.13/0.70 fof(f983,plain,(
% 0.13/0.70 ~op(e3,e3)=e0|~sQ115_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f679,f148])).
% 0.13/0.70 fof(f1028,plain,(
% 0.13/0.70 e0=e2|~sQ105_spl|~sQ107_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f647,f653])).
% 0.13/0.70 fof(f1029,plain,(
% 0.13/0.70 $false|~sQ105_spl|~sQ107_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1028,f210])).
% 0.13/0.70 fof(f1030,plain,(
% 0.13/0.70 ~sQ105_spl|~sQ107_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1029])).
% 0.13/0.70 fof(f1032,plain,(
% 0.13/0.70 ~e4=op(e3,e2)|~sQ79_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f563,f190])).
% 0.13/0.70 fof(f1033,plain,(
% 0.13/0.70 ~e4=e4|~sQ89_spl|~sQ79_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f595,f1032])).
% 0.13/0.70 fof(f1034,plain,(
% 0.13/0.70 $false|~sQ89_spl|~sQ79_spl),
% 0.13/0.70 inference(trivial_equality_resolution,[status(thm)],[f1033])).
% 0.13/0.70 fof(f1035,plain,(
% 0.13/0.70 ~sQ89_spl|~sQ79_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1034])).
% 0.13/0.70 fof(f1037,plain,(
% 0.13/0.70 ~e4=op(e3,e4)|~sQ79_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f563,f192])).
% 0.13/0.70 fof(f1043,plain,(
% 0.13/0.70 ~op(e0,e1)=e2|~sQ82_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f573,f121])).
% 0.13/0.70 fof(f1046,plain,(
% 0.13/0.70 e2=e4|~sQ77_spl|~sQ79_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f557,f563])).
% 0.13/0.70 fof(f1047,plain,(
% 0.13/0.70 $false|~sQ77_spl|~sQ79_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1046,f217])).
% 0.13/0.70 fof(f1048,plain,(
% 0.13/0.70 ~sQ77_spl|~sQ79_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1047])).
% 0.13/0.70 fof(f1054,plain,(
% 0.13/0.70 ~op(e2,e1)=e1|~sQ66_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f522,f184])).
% 0.13/0.70 fof(f1055,plain,(
% 0.13/0.70 ~op(e2,e0)=e1|~sQ66_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f522,f181])).
% 0.13/0.70 fof(f1057,plain,(
% 0.13/0.70 e2=op(e0,op(e4,e4))),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f219,f221])).
% 0.13/0.70 fof(f1058,plain,(
% 0.13/0.70 e3=op(e0,op(e4,op(e4,e4)))),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f219,f222])).
% 0.13/0.70 fof(f1059,plain,(
% 0.13/0.70 ~e3=op(e0,e4)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1065,f162])).
% 0.13/0.70 fof(f1060,plain,(
% 0.13/0.70 ~e3=op(e0,e2)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1065,f160])).
% 0.13/0.70 fof(f1062,plain,(
% 0.13/0.70 ~e3=op(e2,e0)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1065,f110])).
% 0.13/0.70 fof(f1063,plain,(
% 0.13/0.70 ~e3=op(e1,e0)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1065,f109])).
% 0.13/0.70 fof(f1064,plain,(
% 0.13/0.70 op(op(e0,e0),e3)=e0),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1065,f84])).
% 0.13/0.70 fof(f1065,plain,(
% 0.13/0.70 e3=op(e0,e0)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f219,f1058])).
% 0.13/0.70 fof(f1066,plain,(
% 0.13/0.70 op(e3,e3)=e0),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1065,f1064])).
% 0.13/0.70 fof(f1067,plain,(
% 0.13/0.70 e0=e1|~sQ90_spl|~sQ91_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f599,f602])).
% 0.13/0.70 fof(f1068,plain,(
% 0.13/0.70 $false|~sQ90_spl|~sQ91_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1067,f209])).
% 0.13/0.70 fof(f1069,plain,(
% 0.13/0.70 ~sQ90_spl|~sQ91_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1068])).
% 0.13/0.70 fof(f1091,plain,(
% 0.13/0.70 op(op(e2,e2),e4)=e2|~sQ64_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f515,f96])).
% 0.13/0.70 fof(f1093,plain,(
% 0.13/0.70 op(e4,e4)=e2|~sQ64_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f515,f1091])).
% 0.13/0.70 fof(f1094,plain,(
% 0.13/0.70 $false|~sQ39_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f435,f950])).
% 0.13/0.70 fof(f1095,plain,(
% 0.13/0.70 ~sQ39_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1094])).
% 0.13/0.70 fof(f1096,plain,(
% 0.13/0.70 ~e4=op(e0,e4)|~sQ14_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f355,f167])).
% 0.13/0.70 fof(f1101,plain,(
% 0.13/0.70 ~sQ24_spl|~sQ14_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1096,f386,f354])).
% 0.13/0.70 fof(f1102,plain,(
% 0.13/0.70 $false|~sQ59_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f499,f886])).
% 0.13/0.70 fof(f1103,plain,(
% 0.13/0.70 ~sQ59_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1102])).
% 0.13/0.70 fof(f1114,plain,(
% 0.13/0.70 op(e3,op(e2,e1))=e2|~sQ38_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f432,f95])).
% 0.13/0.70 fof(f1128,plain,(
% 0.13/0.70 e0=e3|~sQ35_spl|~sQ38_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f423,f432])).
% 0.13/0.70 fof(f1129,plain,(
% 0.13/0.70 $false|~sQ35_spl|~sQ38_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1128,f211])).
% 0.13/0.70 fof(f1130,plain,(
% 0.13/0.70 ~sQ35_spl|~sQ38_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1129])).
% 0.13/0.70 fof(f1132,plain,(
% 0.13/0.70 ~e3=e3|~sQ103_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1065,f864])).
% 0.13/0.70 fof(f1133,plain,(
% 0.13/0.70 $false|~sQ103_spl),
% 0.13/0.70 inference(trivial_equality_resolution,[status(thm)],[f1132])).
% 0.13/0.70 fof(f1134,plain,(
% 0.13/0.70 ~sQ103_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1133])).
% 0.13/0.70 fof(f1143,plain,(
% 0.13/0.70 op(e1,op(e2,e0))=e2|~sQ11_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f346,f94])).
% 0.13/0.70 fof(f1144,plain,(
% 0.13/0.70 op(e1,e1)=e2|~sQ51_spl|~sQ11_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f474,f1143])).
% 0.13/0.70 fof(f1148,plain,(
% 0.13/0.70 ~sQ5_spl|~sQ105_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f941,f326,f646])).
% 0.13/0.70 fof(f1156,plain,(
% 0.13/0.70 $false|~sQ9_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f339,f885])).
% 0.13/0.70 fof(f1157,plain,(
% 0.13/0.70 ~sQ9_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1156])).
% 0.13/0.70 fof(f1158,plain,(
% 0.13/0.70 $false|~sQ29_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f403,f948])).
% 0.13/0.70 fof(f1159,plain,(
% 0.13/0.70 ~sQ29_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1158])).
% 0.13/0.70 fof(f1160,plain,(
% 0.13/0.70 e3=e4|~sQ33_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f416,f854])).
% 0.13/0.70 fof(f1161,plain,(
% 0.13/0.70 $false|~sQ33_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1160,f218])).
% 0.13/0.70 fof(f1162,plain,(
% 0.13/0.70 ~sQ33_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1161])).
% 0.13/0.70 fof(f1168,plain,(
% 0.13/0.70 e2=e3|~sQ7_spl|~sQ8_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f333,f336])).
% 0.13/0.70 fof(f1169,plain,(
% 0.13/0.70 $false|~sQ7_spl|~sQ8_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1168,f216])).
% 0.13/0.70 fof(f1170,plain,(
% 0.13/0.70 ~sQ7_spl|~sQ8_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1169])).
% 0.13/0.70 fof(f1177,plain,(
% 0.13/0.70 op(op(e0,e2),e1)=e2|~sQ51_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f474,f94])).
% 0.13/0.70 fof(f1181,plain,(
% 0.13/0.70 ~e1=op(e3,e1)|~sQ76_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f554,f189])).
% 0.13/0.70 fof(f1183,plain,(
% 0.13/0.70 ~sQ56_spl|~sQ66_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1054,f489,f521])).
% 0.13/0.70 fof(f1184,plain,(
% 0.13/0.70 ~e1=e1|~sQ51_spl|~sQ66_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f474,f1055])).
% 0.13/0.70 fof(f1185,plain,(
% 0.13/0.70 $false|~sQ51_spl|~sQ66_spl),
% 0.13/0.70 inference(trivial_equality_resolution,[status(thm)],[f1184])).
% 0.13/0.70 fof(f1186,plain,(
% 0.13/0.70 ~sQ51_spl|~sQ66_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1185])).
% 0.13/0.70 fof(f1191,plain,(
% 0.13/0.70 sQ123_spl|~sQ94_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f947,f703,f610])).
% 0.13/0.70 fof(f1193,plain,(
% 0.13/0.70 ~sQ63_spl|~sQ113_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f891,f511,f671])).
% 0.13/0.70 fof(f1203,plain,(
% 0.13/0.70 e3=e4|~sQ4_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1065,f323])).
% 0.13/0.70 fof(f1204,plain,(
% 0.13/0.70 $false|~sQ4_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1203,f218])).
% 0.13/0.70 fof(f1205,plain,(
% 0.13/0.70 ~sQ4_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1204])).
% 0.13/0.70 fof(f1207,plain,(
% 0.13/0.70 e3=e2|~sQ2_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f317,f1065])).
% 0.13/0.70 fof(f1208,plain,(
% 0.13/0.70 $false|~sQ2_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1207,f216])).
% 0.13/0.70 fof(f1209,plain,(
% 0.13/0.70 ~sQ2_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1208])).
% 0.13/0.70 fof(f1212,plain,(
% 0.13/0.70 ~e4=op(e4,e2)|~sQ104_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f643,f200])).
% 0.13/0.70 fof(f1216,plain,(
% 0.13/0.70 op(e4,op(e0,e4))=e0|~sQ104_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f643,f88])).
% 0.13/0.70 fof(f1217,plain,(
% 0.13/0.70 op(op(e0,e4),e4)=e4|~sQ104_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f643,f104])).
% 0.13/0.70 fof(f1218,plain,(
% 0.13/0.70 ~e2=op(e4,e0)|~sQ52_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f477,f117])).
% 0.13/0.70 fof(f1224,plain,(
% 0.13/0.70 e2=op(e0,e1)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f220,f1057])).
% 0.13/0.70 fof(f1225,plain,(
% 0.13/0.70 e0=op(e4,e1)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f220,f219])).
% 0.13/0.70 fof(f1226,plain,(
% 0.13/0.70 ~op(e4,e3)=e1),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f220,f208])).
% 0.13/0.70 fof(f1227,plain,(
% 0.13/0.70 ~op(e4,e2)=e1),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f220,f207])).
% 0.13/0.70 fof(f1236,plain,(
% 0.13/0.70 ~op(e1,e4)=e3|~sQ98_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f624,f154])).
% 0.13/0.70 fof(f1237,plain,(
% 0.13/0.70 ~op(e2,e4)=e3|~sQ98_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f624,f156])).
% 0.13/0.70 fof(f1245,plain,(
% 0.13/0.70 op(e0,e4)=e4|~sQ20_spl|~sQ104_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f375,f1217])).
% 0.13/0.70 fof(f1246,plain,(
% 0.13/0.70 op(e4,e0)=e0|~sQ20_spl|~sQ104_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f375,f1216])).
% 0.13/0.70 fof(f1248,plain,(
% 0.13/0.70 sQ24_spl|~sQ20_spl|~sQ104_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1245,f386,f374,f642])).
% 0.13/0.70 fof(f1249,plain,(
% 0.13/0.70 sQ100_spl|~sQ20_spl|~sQ104_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1246,f630,f374,f642])).
% 0.13/0.70 fof(f1251,plain,(
% 0.13/0.70 ~sQ35_spl|~sQ45_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f954,f422,f454])).
% 0.13/0.70 fof(f1256,plain,(
% 0.13/0.70 op(e1,op(e0,e1))=e0|~sQ26_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f394,f85])).
% 0.13/0.70 fof(f1260,plain,(
% 0.13/0.70 ~sQ99_spl|~sQ79_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1037,f626,f562])).
% 0.13/0.70 fof(f1261,plain,(
% 0.13/0.70 ~sQ102_spl|~sQ52_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1218,f636,f476])).
% 0.13/0.70 fof(f1262,plain,(
% 0.13/0.70 ~op(e4,e0)=e1),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f202])).
% 0.13/0.70 fof(f1270,plain,(
% 0.13/0.70 op(op(e0,e1),e1)=e1|~sQ26_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f394,f89])).
% 0.13/0.70 fof(f1272,plain,(
% 0.13/0.70 $false|~sQ46_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f458,f923])).
% 0.13/0.70 fof(f1273,plain,(
% 0.13/0.70 ~sQ46_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1272])).
% 0.13/0.70 fof(f1277,plain,(
% 0.13/0.70 ~sQ55_spl|~sQ105_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f939,f486,f646])).
% 0.13/0.70 fof(f1283,plain,(
% 0.13/0.70 $false|~sQ49_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f467,f952])).
% 0.13/0.70 fof(f1284,plain,(
% 0.13/0.70 ~sQ49_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1283])).
% 0.13/0.70 fof(f1286,plain,(
% 0.13/0.70 ~op(e3,e0)=e0),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1066,f191])).
% 0.13/0.70 fof(f1295,plain,(
% 0.13/0.70 $false|~sQ13_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f352,f1060])).
% 0.13/0.70 fof(f1296,plain,(
% 0.13/0.70 ~sQ13_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1295])).
% 0.13/0.70 fof(f1299,plain,(
% 0.13/0.70 ~e1=op(e3,e0)|~sQ26_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f394,f114])).
% 0.13/0.70 fof(f1300,plain,(
% 0.13/0.70 ~e0=op(e3,e4)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1066,f198])).
% 0.13/0.70 fof(f1301,plain,(
% 0.13/0.70 ~e1=op(e1,e3)|~sQ26_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f394,f171])).
% 0.13/0.70 fof(f1302,plain,(
% 0.13/0.70 ~op(e3,e1)=e0),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1066,f194])).
% 0.13/0.70 fof(f1304,plain,(
% 0.13/0.70 ~op(e3,e2)=e0),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1066,f196])).
% 0.13/0.70 fof(f1307,plain,(
% 0.13/0.70 ~e3=op(e3,e0)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1065,f111])).
% 0.13/0.70 fof(f1308,plain,(
% 0.13/0.70 ~op(e1,e3)=e0),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1066,f144])).
% 0.13/0.70 fof(f1313,plain,(
% 0.13/0.70 ~e2=op(e0,e2)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1224,f163])).
% 0.13/0.70 fof(f1316,plain,(
% 0.13/0.70 ~e2=op(e0,e3)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1224,f164])).
% 0.13/0.70 fof(f1324,plain,(
% 0.13/0.70 ~e0=op(e4,e2)),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f1225,f203])).
% 0.13/0.70 fof(f1325,plain,(
% 0.13/0.70 ~e2=op(e2,e1)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1224,f120])).
% 0.13/0.70 fof(f1330,plain,(
% 0.13/0.70 ~op(e2,e1)=e3|~sQ68_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f528,f184])).
% 0.13/0.70 fof(f1336,plain,(
% 0.13/0.70 ~op(e1,e3)=e3|~sQ68_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f528,f143])).
% 0.13/0.70 fof(f1337,plain,(
% 0.13/0.70 ~e3=op(e4,e3)|~sQ68_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f528,f147])).
% 0.13/0.70 fof(f1340,plain,(
% 0.13/0.70 ~sQ43_spl|~sQ68_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1336,f447,f527])).
% 0.13/0.70 fof(f1345,plain,(
% 0.13/0.70 $false|~sQ95_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f615,f1300])).
% 0.13/0.70 fof(f1346,plain,(
% 0.13/0.70 ~sQ95_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1345])).
% 0.13/0.70 fof(f1347,plain,(
% 0.13/0.70 op(e2,op(e1,e0))=e1),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1224,f89])).
% 0.13/0.70 fof(f1348,plain,(
% 0.13/0.70 op(op(e1,e0),e2)=e0),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1224,f85])).
% 0.13/0.70 fof(f1349,plain,(
% 0.13/0.70 e0=e3|~sQ108_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1225,f656])).
% 0.13/0.70 fof(f1350,plain,(
% 0.13/0.70 $false|~sQ108_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1349,f211])).
% 0.13/0.70 fof(f1351,plain,(
% 0.13/0.70 ~sQ108_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1350])).
% 0.13/0.70 fof(f1352,plain,(
% 0.13/0.70 ~e0=e0|sQ90_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1066,f600])).
% 0.13/0.70 fof(f1353,plain,(
% 0.13/0.70 $false|sQ90_spl),
% 0.13/0.70 inference(trivial_equality_resolution,[status(thm)],[f1352])).
% 0.13/0.70 fof(f1354,plain,(
% 0.13/0.70 sQ90_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1353])).
% 0.13/0.70 fof(f1357,plain,(
% 0.13/0.70 ~e0=e0|sQ105_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1225,f648])).
% 0.13/0.70 fof(f1358,plain,(
% 0.13/0.70 $false|sQ105_spl),
% 0.13/0.70 inference(trivial_equality_resolution,[status(thm)],[f1357])).
% 0.13/0.70 fof(f1359,plain,(
% 0.13/0.70 sQ105_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1358])).
% 0.13/0.70 fof(f1360,plain,(
% 0.13/0.70 $false|~sQ71_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f538,f924])).
% 0.13/0.70 fof(f1361,plain,(
% 0.13/0.70 ~sQ71_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1360])).
% 0.13/0.70 fof(f1364,plain,(
% 0.13/0.70 $false|~sQ40_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f439,f1308])).
% 0.13/0.70 fof(f1365,plain,(
% 0.13/0.70 ~sQ40_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1364])).
% 0.13/0.70 fof(f1368,plain,(
% 0.13/0.70 $false|~sQ57_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f493,f1325])).
% 0.13/0.70 fof(f1369,plain,(
% 0.13/0.70 ~sQ57_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1368])).
% 0.13/0.70 fof(f1371,plain,(
% 0.13/0.70 ~op(e0,e3)=e0),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1066,f141])).
% 0.13/0.70 fof(f1372,plain,(
% 0.13/0.70 ~op(e4,e0)=e0),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1225,f199])).
% 0.13/0.70 fof(f1383,plain,(
% 0.13/0.70 $false|~sQ80_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f567,f1302])).
% 0.13/0.70 fof(f1384,plain,(
% 0.13/0.70 ~sQ80_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1383])).
% 0.13/0.70 fof(f1387,plain,(
% 0.13/0.70 $false|~sQ23_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f384,f1059])).
% 0.13/0.70 fof(f1388,plain,(
% 0.13/0.70 ~sQ23_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1387])).
% 0.13/0.70 fof(f1389,plain,(
% 0.13/0.70 ~sQ25_spl|~sQ45_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f949,f390,f454])).
% 0.13/0.70 fof(f1391,plain,(
% 0.13/0.70 ~e2=e2|sQ7_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1224,f334])).
% 0.13/0.70 fof(f1392,plain,(
% 0.13/0.70 $false|sQ7_spl),
% 0.13/0.70 inference(trivial_equality_resolution,[status(thm)],[f1391])).
% 0.13/0.70 fof(f1393,plain,(
% 0.13/0.70 sQ7_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1392])).
% 0.13/0.70 fof(f1394,plain,(
% 0.13/0.70 $false|~sQ96_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f618,f925])).
% 0.13/0.70 fof(f1395,plain,(
% 0.13/0.70 ~sQ96_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1394])).
% 0.13/0.70 fof(f1396,plain,(
% 0.13/0.70 op(e3,e0)=e4|~sQ48_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1225,f858])).
% 0.13/0.70 fof(f1397,plain,(
% 0.13/0.70 op(e0,e3)=e1|~sQ48_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1225,f859])).
% 0.13/0.70 fof(f1398,plain,(
% 0.13/0.70 $false|~sQ100_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f631,f1372])).
% 0.13/0.70 fof(f1399,plain,(
% 0.13/0.70 ~sQ100_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1398])).
% 0.13/0.70 fof(f1400,plain,(
% 0.13/0.70 $false|~sQ85_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f583,f1304])).
% 0.13/0.70 fof(f1401,plain,(
% 0.13/0.70 ~sQ85_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1400])).
% 0.13/0.70 fof(f1402,plain,(
% 0.13/0.70 $false|~sQ116_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f682,f1226])).
% 0.13/0.70 fof(f1403,plain,(
% 0.13/0.70 ~sQ116_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1402])).
% 0.13/0.70 fof(f1404,plain,(
% 0.13/0.70 e0=e4|~sQ109_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1225,f659])).
% 0.13/0.70 fof(f1405,plain,(
% 0.13/0.70 $false|~sQ109_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1404,f212])).
% 0.13/0.70 fof(f1406,plain,(
% 0.13/0.70 ~sQ109_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1405])).
% 0.13/0.70 fof(f1407,plain,(
% 0.13/0.70 e0=e2|~sQ92_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1066,f605])).
% 0.13/0.70 fof(f1408,plain,(
% 0.13/0.70 $false|~sQ92_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1407,f210])).
% 0.13/0.70 fof(f1409,plain,(
% 0.13/0.70 ~sQ92_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1408])).
% 0.13/0.70 fof(f1410,plain,(
% 0.13/0.70 $false|~sQ111_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f666,f1227])).
% 0.13/0.70 fof(f1411,plain,(
% 0.13/0.70 ~sQ111_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1410])).
% 0.13/0.70 fof(f1412,plain,(
% 0.13/0.70 e0=e3|~sQ93_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1066,f608])).
% 0.13/0.70 fof(f1413,plain,(
% 0.13/0.70 $false|~sQ93_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1412,f211])).
% 0.13/0.70 fof(f1414,plain,(
% 0.13/0.70 ~sQ93_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1413])).
% 0.13/0.70 fof(f1415,plain,(
% 0.13/0.70 op(e1,e2)=e0|~sQ26_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1224,f1256])).
% 0.13/0.70 fof(f1416,plain,(
% 0.13/0.70 op(e2,e1)=e1|~sQ26_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1224,f1270])).
% 0.13/0.70 fof(f1417,plain,(
% 0.13/0.70 ~sQ76_spl|~sQ26_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1299,f553,f393])).
% 0.13/0.70 fof(f1418,plain,(
% 0.13/0.70 ~sQ41_spl|~sQ26_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1301,f441,f393])).
% 0.13/0.70 fof(f1421,plain,(
% 0.13/0.70 e0=e1|~sQ106_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1225,f650])).
% 0.13/0.70 fof(f1422,plain,(
% 0.13/0.70 $false|~sQ106_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1421,f209])).
% 0.13/0.70 fof(f1423,plain,(
% 0.13/0.70 ~sQ106_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1422])).
% 0.13/0.70 fof(f1429,plain,(
% 0.13/0.70 sQ32_spl|~sQ51_spl|~sQ11_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1144,f412,f473,f345])).
% 0.13/0.70 fof(f1438,plain,(
% 0.13/0.70 ~e4=op(e4,e2)|~sQ89_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f595,f138])).
% 0.13/0.70 fof(f1439,plain,(
% 0.13/0.70 ~sQ114_spl|~sQ89_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1438,f674,f594])).
% 0.13/0.70 fof(f1440,plain,(
% 0.13/0.70 $false|~sQ15_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f359,f1371])).
% 0.13/0.70 fof(f1441,plain,(
% 0.13/0.70 ~sQ15_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1440])).
% 0.13/0.70 fof(f1452,plain,(
% 0.13/0.70 ~sQ58_spl|~sQ68_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1330,f495,f527])).
% 0.13/0.70 fof(f1455,plain,(
% 0.13/0.70 ~sQ118_spl|~sQ68_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1337,f687,f527])).
% 0.13/0.70 fof(f1459,plain,(
% 0.13/0.70 e1=e4|~sQ124_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f220,f707])).
% 0.13/0.70 fof(f1460,plain,(
% 0.13/0.70 $false|~sQ124_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1459,f215])).
% 0.13/0.70 fof(f1461,plain,(
% 0.13/0.70 ~sQ124_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1460])).
% 0.13/0.70 fof(f1462,plain,(
% 0.13/0.70 ~sQ48_spl|~sQ98_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1236,f463,f623])).
% 0.13/0.70 fof(f1464,plain,(
% 0.13/0.70 sQ79_spl|~sQ48_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1396,f562,f463])).
% 0.13/0.70 fof(f1465,plain,(
% 0.13/0.70 sQ16_spl|~sQ48_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1397,f361,f463])).
% 0.13/0.70 fof(f1467,plain,(
% 0.13/0.70 sQ122_spl|~sQ64_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1093,f700,f514])).
% 0.13/0.70 fof(f1470,plain,(
% 0.13/0.70 ~sQ114_spl|~sQ104_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1212,f674,f642])).
% 0.13/0.70 fof(f1471,plain,(
% 0.13/0.70 ~sQ81_spl|~sQ76_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1181,f569,f553])).
% 0.13/0.70 fof(f1474,plain,(
% 0.13/0.70 ~e2=op(e0,e4)),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1224,f165])).
% 0.13/0.70 fof(f1479,plain,(
% 0.13/0.70 op(e3,op(e3,e4))=e3|~sQ118_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f688,f103])).
% 0.13/0.70 fof(f1491,plain,(
% 0.13/0.70 ~e3=op(e3,e1)|~sQ58_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f496,f126])).
% 0.13/0.70 fof(f1493,plain,(
% 0.13/0.70 op(op(e1,e2),e3)=e2|~sQ58_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f496,f95])).
% 0.13/0.70 fof(f1494,plain,(
% 0.13/0.70 ~e3=op(e2,e2)|~sQ58_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f496,f183])).
% 0.13/0.70 fof(f1495,plain,(
% 0.13/0.70 ~sQ83_spl|~sQ58_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1491,f575,f495])).
% 0.13/0.70 fof(f1496,plain,(
% 0.13/0.70 $false|~sQ12_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f349,f1313])).
% 0.13/0.70 fof(f1497,plain,(
% 0.13/0.70 ~sQ12_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1496])).
% 0.13/0.70 fof(f1500,plain,(
% 0.13/0.70 ~sQ90_spl|~sQ115_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f983,f598,f678])).
% 0.13/0.70 fof(f1501,plain,(
% 0.13/0.70 $false|~sQ17_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f365,f1316])).
% 0.13/0.70 fof(f1502,plain,(
% 0.13/0.70 ~sQ17_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1501])).
% 0.13/0.70 fof(f1503,plain,(
% 0.13/0.70 e1=e4|~sQ31_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f410,f854])).
% 0.13/0.70 fof(f1504,plain,(
% 0.13/0.70 $false|~sQ31_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1503,f215])).
% 0.13/0.70 fof(f1505,plain,(
% 0.13/0.70 ~sQ31_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1504])).
% 0.13/0.70 fof(f1522,plain,(
% 0.13/0.70 ~op(e1,e0)=e2|~sQ37_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f429,f170])).
% 0.13/0.70 fof(f1525,plain,(
% 0.13/0.70 ~e2=op(e2,e2)|~sQ37_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f429,f133])).
% 0.13/0.70 fof(f1527,plain,(
% 0.13/0.70 ~e2=op(e1,e4)|~sQ37_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f429,f177])).
% 0.13/0.70 fof(f1529,plain,(
% 0.13/0.70 ~sQ27_spl|~sQ37_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1522,f396,f428])).
% 0.13/0.70 fof(f1530,plain,(
% 0.13/0.70 ~sQ62_spl|~sQ37_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1525,f508,f428])).
% 0.13/0.70 fof(f1532,plain,(
% 0.13/0.70 ~op(e3,e0)=e2|~sQ87_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f589,f190])).
% 0.13/0.70 fof(f1550,plain,(
% 0.13/0.70 ~sQ47_spl|~sQ37_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1527,f460,f428])).
% 0.13/0.70 fof(f1561,plain,(
% 0.13/0.70 ~op(e0,e4)=e4|~sQ99_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f627,f151])).
% 0.13/0.70 fof(f1566,plain,(
% 0.13/0.70 ~e3=op(e3,e2)|~sQ83_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f576,f193])).
% 0.13/0.70 fof(f1573,plain,(
% 0.13/0.70 ~e1=op(e1,e3)|~sQ16_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f362,f139])).
% 0.13/0.70 fof(f1576,plain,(
% 0.13/0.70 ~sQ41_spl|~sQ16_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1573,f441,f361])).
% 0.13/0.70 fof(f1577,plain,(
% 0.13/0.70 sQ35_spl|~sQ26_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1415,f422,f393])).
% 0.13/0.70 fof(f1581,plain,(
% 0.13/0.70 $false|~sQ83_spl|~sQ88_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f592,f1566])).
% 0.13/0.70 fof(f1582,plain,(
% 0.13/0.70 ~sQ83_spl|~sQ88_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1581])).
% 0.13/0.70 fof(f1583,plain,(
% 0.13/0.70 sQ56_spl|~sQ26_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1416,f489,f393])).
% 0.13/0.70 fof(f1592,plain,(
% 0.13/0.70 $false|~sQ78_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f560,f1307])).
% 0.13/0.70 fof(f1593,plain,(
% 0.13/0.70 ~sQ78_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1592])).
% 0.13/0.70 fof(f1595,plain,(
% 0.13/0.70 $false|~sQ22_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f381,f1474])).
% 0.13/0.70 fof(f1596,plain,(
% 0.13/0.70 ~sQ22_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1595])).
% 0.13/0.70 fof(f1612,plain,(
% 0.13/0.70 ~op(e1,e0)=e0|~sQ50_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f471,f113])).
% 0.13/0.70 fof(f1621,plain,(
% 0.13/0.70 ~e2=op(e4,e2)|~sQ102_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f637,f200])).
% 0.13/0.70 fof(f1624,plain,(
% 0.13/0.70 e2=e4|~sQ32_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f413,f854])).
% 0.13/0.70 fof(f1625,plain,(
% 0.13/0.70 $false|~sQ32_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1624,f217])).
% 0.13/0.70 fof(f1626,plain,(
% 0.13/0.70 ~sQ32_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1625])).
% 0.13/0.70 fof(f1629,plain,(
% 0.13/0.70 ~e3=op(e4,e3)|~sQ43_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f448,f145])).
% 0.13/0.70 fof(f1632,plain,(
% 0.13/0.70 ~e3=op(e1,e4)|~sQ43_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f448,f178])).
% 0.13/0.70 fof(f1634,plain,(
% 0.13/0.70 ~sQ48_spl|~sQ43_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1632,f463,f447])).
% 0.13/0.70 fof(f1642,plain,(
% 0.13/0.70 ~op(e2,e1)=e1|~sQ81_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f570,f126])).
% 0.13/0.70 fof(f1643,plain,(
% 0.13/0.70 ~sQ56_spl|~sQ81_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1642,f489,f569])).
% 0.13/0.70 fof(f1645,plain,(
% 0.13/0.70 op(e4,e1)=e2|~sQ14_spl|~sQ51_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f355,f1177])).
% 0.13/0.70 fof(f1646,plain,(
% 0.13/0.70 e0=e2|~sQ14_spl|~sQ51_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f1225,f1645])).
% 0.13/0.70 fof(f1647,plain,(
% 0.13/0.70 $false|~sQ14_spl|~sQ51_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1646,f210])).
% 0.13/0.70 fof(f1648,plain,(
% 0.13/0.70 ~sQ14_spl|~sQ51_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1647])).
% 0.13/0.70 fof(f1649,plain,(
% 0.13/0.70 $false|~sQ75_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f551,f1286])).
% 0.13/0.70 fof(f1650,plain,(
% 0.13/0.70 ~sQ75_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1649])).
% 0.13/0.70 fof(f1651,plain,(
% 0.13/0.70 $false|~sQ110_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f663,f1324])).
% 0.13/0.70 fof(f1652,plain,(
% 0.13/0.70 ~sQ110_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1651])).
% 0.13/0.70 fof(f1653,plain,(
% 0.13/0.70 ~sQ24_spl|~sQ99_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1561,f386,f626])).
% 0.13/0.70 fof(f1656,plain,(
% 0.13/0.70 ~sQ112_spl|~sQ102_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1621,f668,f636])).
% 0.13/0.70 fof(f1659,plain,(
% 0.13/0.70 ~sQ38_spl|~sQ113_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f890,f431,f671])).
% 0.13/0.70 fof(f1660,plain,(
% 0.13/0.70 ~sQ88_spl|~sQ113_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f892,f591,f671])).
% 0.13/0.70 fof(f1665,plain,(
% 0.13/0.70 ~e3=op(e2,e4)|~sQ58_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f496,f185])).
% 0.13/0.70 fof(f1669,plain,(
% 0.13/0.70 ~sQ73_spl|~sQ58_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1665,f543,f495])).
% 0.13/0.70 fof(f1673,plain,(
% 0.13/0.70 ~sQ7_spl|~sQ82_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1043,f332,f572])).
% 0.13/0.70 fof(f1691,plain,(
% 0.13/0.70 ~e4=op(e2,e4)|~sQ24_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f387,f150])).
% 0.13/0.70 fof(f1696,plain,(
% 0.13/0.70 ~sQ74_spl|~sQ24_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1691,f546,f386])).
% 0.13/0.70 fof(f1702,plain,(
% 0.13/0.70 ~e2=op(e2,e3)|~sQ42_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f445,f143])).
% 0.13/0.70 fof(f1709,plain,(
% 0.13/0.70 ~op(e1,e0)=e2|~sQ42_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f445,f171])).
% 0.13/0.70 fof(f1710,plain,(
% 0.13/0.70 ~e2=op(e1,e4)|~sQ42_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f445,f178])).
% 0.13/0.70 fof(f1727,plain,(
% 0.13/0.70 ~e0=op(e1,e2)|~sQ10_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f343,f129])).
% 0.13/0.70 fof(f1732,plain,(
% 0.13/0.70 ~e0=op(e2,e2)|~sQ10_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f343,f130])).
% 0.13/0.70 fof(f1733,plain,(
% 0.13/0.70 ~e0=op(e0,e4)|~sQ10_spl),
% 0.13/0.70 inference(forward_demodulation,[status(thm)],[f343,f167])).
% 0.13/0.70 fof(f1748,plain,(
% 0.13/0.70 op(e3,e2)=e3|~sQ97_spl|~sQ118_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f621,f1479])).
% 0.13/0.70 fof(f1753,plain,(
% 0.13/0.70 ~op(e1,e4)=e2|~sQ97_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f621,f154])).
% 0.13/0.70 fof(f1755,plain,(
% 0.13/0.70 ~op(e2,e4)=e2|~sQ97_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f621,f156])).
% 0.13/0.70 fof(f1769,plain,(
% 0.13/0.70 ~op(e2,e2)=e0|~sQ70_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f535,f187])).
% 0.13/0.70 fof(f1790,plain,(
% 0.13/0.70 ~op(e1,e0)=e2|~sQ102_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f637,f115])).
% 0.13/0.70 fof(f1792,plain,(
% 0.13/0.70 ~sQ27_spl|~sQ102_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1790,f396,f636])).
% 0.13/0.70 fof(f1797,plain,(
% 0.13/0.70 $false|~sQ28_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f400,f1063])).
% 0.13/0.70 fof(f1798,plain,(
% 0.13/0.70 ~sQ28_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1797])).
% 0.13/0.70 fof(f1802,plain,(
% 0.13/0.70 ~sQ25_spl|~sQ50_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1612,f390,f470])).
% 0.13/0.70 fof(f1804,plain,(
% 0.13/0.70 ~sQ20_spl|~sQ10_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1733,f374,f342])).
% 0.13/0.70 fof(f1825,plain,(
% 0.13/0.70 op(e1,e3)=e2|~sQ36_spl|~sQ58_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f426,f1493])).
% 0.13/0.70 fof(f1827,plain,(
% 0.13/0.70 ~e1=op(e2,e2)|~sQ36_spl),
% 0.13/0.70 inference(backward_demodulation,[status(thm)],[f426,f133])).
% 0.13/0.70 fof(f1828,plain,(
% 0.13/0.70 ~sQ61_spl|~sQ36_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1827,f505,f425])).
% 0.13/0.70 fof(f1832,plain,(
% 0.13/0.70 ~sQ60_spl|~sQ70_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1769,f502,f534])).
% 0.13/0.70 fof(f1833,plain,(
% 0.13/0.70 ~sQ60_spl|~sQ10_spl),
% 0.13/0.70 inference(split_clause,[status(thm)],[f1732,f502,f342])).
% 0.13/0.70 fof(f1834,plain,(
% 0.13/0.70 $false|~sQ58_spl|~sQ63_spl),
% 0.13/0.70 inference(forward_subsumption_resolution,[status(thm)],[f512,f1494])).
% 0.13/0.70 fof(f1835,plain,(
% 0.13/0.70 ~sQ58_spl|~sQ63_spl),
% 0.13/0.70 inference(contradiction_clause,[status(thm)],[f1834])).
% 0.13/0.71 fof(f1841,plain,(
% 0.13/0.71 op(e3,e3)=e2|~sQ58_spl|~sQ38_spl),
% 0.13/0.71 inference(forward_demodulation,[status(thm)],[f496,f1114])).
% 0.13/0.71 fof(f1842,plain,(
% 0.13/0.71 e0=e2|~sQ58_spl|~sQ38_spl),
% 0.13/0.71 inference(forward_demodulation,[status(thm)],[f1066,f1841])).
% 0.13/0.71 fof(f1843,plain,(
% 0.13/0.71 $false|~sQ58_spl|~sQ38_spl),
% 0.13/0.71 inference(forward_subsumption_resolution,[status(thm)],[f1842,f210])).
% 0.13/0.71 fof(f1844,plain,(
% 0.13/0.71 ~sQ58_spl|~sQ38_spl),
% 0.13/0.71 inference(contradiction_clause,[status(thm)],[f1843])).
% 0.13/0.71 fof(f1851,plain,(
% 0.13/0.71 ~sQ47_spl|~sQ97_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1753,f460,f620])).
% 0.13/0.71 fof(f1852,plain,(
% 0.13/0.71 $false|~sQ53_spl),
% 0.13/0.71 inference(forward_subsumption_resolution,[status(thm)],[f480,f1062])).
% 0.13/0.71 fof(f1853,plain,(
% 0.13/0.71 ~sQ53_spl),
% 0.13/0.71 inference(contradiction_clause,[status(thm)],[f1852])).
% 0.13/0.71 fof(f1858,plain,(
% 0.13/0.71 op(e2,e0)=e1|~sQ25_spl),
% 0.13/0.71 inference(backward_demodulation,[status(thm)],[f391,f1347])).
% 0.13/0.71 fof(f1859,plain,(
% 0.13/0.71 op(e0,e2)=e0|~sQ25_spl),
% 0.13/0.71 inference(backward_demodulation,[status(thm)],[f391,f1348])).
% 0.13/0.71 fof(f1862,plain,(
% 0.13/0.71 sQ51_spl|~sQ25_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1858,f473,f390])).
% 0.13/0.71 fof(f1863,plain,(
% 0.13/0.71 sQ10_spl|~sQ25_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1859,f342,f390])).
% 0.13/0.71 fof(f1864,plain,(
% 0.13/0.71 ~sQ35_spl|~sQ10_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1727,f422,f342])).
% 0.13/0.71 fof(f1869,plain,(
% 0.13/0.71 sQ42_spl|~sQ36_spl|~sQ58_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1825,f444,f425,f495])).
% 0.13/0.71 fof(f1874,plain,(
% 0.13/0.71 ~sQ47_spl|~sQ42_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1710,f460,f444])).
% 0.13/0.71 fof(f1875,plain,(
% 0.13/0.71 $false|~sQ101_spl),
% 0.13/0.71 inference(forward_subsumption_resolution,[status(thm)],[f634,f1262])).
% 0.13/0.71 fof(f1876,plain,(
% 0.13/0.71 ~sQ101_spl),
% 0.13/0.71 inference(contradiction_clause,[status(thm)],[f1875])).
% 0.13/0.71 fof(f1878,plain,(
% 0.13/0.71 ~sQ67_spl|~sQ42_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1702,f524,f444])).
% 0.13/0.71 fof(f1879,plain,(
% 0.13/0.71 ~sQ118_spl|~sQ43_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1629,f687,f447])).
% 0.13/0.71 fof(f1883,plain,(
% 0.13/0.71 sQ88_spl|~sQ97_spl|~sQ118_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1748,f591,f620,f687])).
% 0.13/0.71 fof(f1885,plain,(
% 0.13/0.71 ~sQ77_spl|~sQ87_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1532,f556,f588])).
% 0.13/0.71 fof(f1886,plain,(
% 0.13/0.71 ~sQ73_spl|~sQ98_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1237,f543,f623])).
% 0.13/0.71 fof(f1890,plain,(
% 0.13/0.71 ~sQ27_spl|~sQ42_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1709,f396,f444])).
% 0.13/0.71 fof(f1891,plain,(
% 0.13/0.71 ~sQ72_spl|~sQ97_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1755,f540,f620])).
% 0.13/0.71 fof(f1923,plain,(
% 0.13/0.71 e3=e0|~sQ0_spl),
% 0.13/0.71 inference(backward_demodulation,[status(thm)],[f311,f1065])).
% 0.13/0.71 fof(f1924,plain,(
% 0.13/0.71 $false|~sQ0_spl),
% 0.13/0.71 inference(forward_subsumption_resolution,[status(thm)],[f1923,f211])).
% 0.13/0.71 fof(f1925,plain,(
% 0.13/0.71 ~sQ0_spl),
% 0.13/0.71 inference(contradiction_clause,[status(thm)],[f1924])).
% 0.13/0.71 fof(f1973,plain,(
% 0.13/0.71 op(e2,e2)=e0|~sQ27_spl),
% 0.13/0.71 inference(backward_demodulation,[status(thm)],[f397,f1348])).
% 0.13/0.71 fof(f1974,plain,(
% 0.13/0.71 op(e2,e2)=e1|~sQ27_spl),
% 0.13/0.71 inference(backward_demodulation,[status(thm)],[f397,f1347])).
% 0.13/0.71 fof(f1982,plain,(
% 0.13/0.71 sQ60_spl|~sQ27_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1973,f502,f396])).
% 0.13/0.71 fof(f1983,plain,(
% 0.13/0.71 sQ61_spl|~sQ27_spl),
% 0.13/0.71 inference(split_clause,[status(thm)],[f1974,f505,f396])).
% 0.13/0.71 fof(f1984,plain,(
% 0.13/0.71 $false),
% 0.13/0.71 inference(sat_refutation,[status(thm)],[f357,f389,f405,f437,f453,f469,f501,f517,f565,f581,f629,f645,f677,f709,f710,f717,f726,f728,f734,f735,f736,f739,f744,f746,f748,f751,f756,f758,f763,f766,f774,f780,f783,f784,f790,f791,f799,f801,f804,f810,f811,f822,f825,f829,f837,f840,f846,f850,f867,f910,f918,f928,f961,f974,f1030,f1035,f1048,f1069,f1095,f1101,f1103,f1130,f1134,f1148,f1157,f1159,f1162,f1170,f1183,f1186,f1191,f1193,f1205,f1209,f1248,f1249,f1251,f1260,f1261,f1273,f1277,f1284,f1296,f1340,f1346,f1351,f1354,f1359,f1361,f1365,f1369,f1384,f1388,f1389,f1393,f1395,f1399,f1401,f1403,f1406,f1409,f1411,f1414,f1417,f1418,f1423,f1429,f1439,f1441,f1452,f1455,f1461,f1462,f1464,f1465,f1467,f1470,f1471,f1495,f1497,f1500,f1502,f1505,f1529,f1530,f1550,f1576,f1577,f1582,f1583,f1593,f1596,f1626,f1634,f1643,f1648,f1650,f1652,f1653,f1656,f1659,f1660,f1669,f1673,f1696,f1792,f1798,f1802,f1804,f1828,f1832,f1833,f1835,f1844,f1851,f1853,f1862,f1863,f1864,f1869,f1874,f1876,f1878,f1879,f1883,f1885,f1886,f1890,f1891,f1925,f1982,f1983])).
% 0.13/0.71 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.71 % Elapsed time: 0.130100 seconds
% 0.13/0.71 % CPU time: 0.693037 seconds
% 0.13/0.71 % Total memory used: 124.774 MB
% 0.13/0.71 % Net memory used: 124.507 MB
%------------------------------------------------------------------------------