Drodi-SAT---4.1.1.THM-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : ALG121+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 : n004.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:39 AM UTC 2026

% Result   : Theorem 0.12s 0.51s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ALG121+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.35  % Computer : n004.cluster.edu
% 0.09/0.35  % Model    : x86_64 x86_64
% 0.09/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35  % Memory   : 8046.5625MB
% 0.09/0.35  % OS       : Linux 6.8.0-71-generic
% 0.09/0.35  % CPULimit : 300
% 0.09/0.35  % WCLimit  : 300
% 0.09/0.35  % DateTime : Mon Sep 21 12:57:35 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.12/0.38  % Drodi V4.1.1
% 0.12/0.51  % Refutation found
% 0.12/0.51  % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.51  % SZS output start CNFRefutation for theBenchmark
% 0.12/0.51  fof(f1,axiom,(
% 0.12/0.51    ( ( op1(e10,e10) = e10| op1(e10,e10) = e11| op1(e10,e10) = e12| op1(e10,e10) = e13 )& ( op1(e10,e11) = e10| op1(e10,e11) = e11| op1(e10,e11) = e12| op1(e10,e11) = e13 )& ( op1(e10,e12) = e10| op1(e10,e12) = e11| op1(e10,e12) = e12| op1(e10,e12) = e13 )& ( op1(e10,e13) = e10| op1(e10,e13) = e11| op1(e10,e13) = e12| op1(e10,e13) = e13 )& ( op1(e11,e10) = e10| op1(e11,e10) = e11| op1(e11,e10) = e12| op1(e11,e10) = e13 )& ( op1(e11,e11) = e10| op1(e11,e11) = e11| op1(e11,e11) = e12| op1(e11,e11) = e13 )& ( op1(e11,e12) = e10| op1(e11,e12) = e11| op1(e11,e12) = e12| op1(e11,e12) = e13 )& ( op1(e11,e13) = e10| op1(e11,e13) = e11| op1(e11,e13) = e12| op1(e11,e13) = e13 )& ( op1(e12,e10) = e10| op1(e12,e10) = e11| op1(e12,e10) = e12| op1(e12,e10) = e13 )& ( op1(e12,e11) = e10| op1(e12,e11) = e11| op1(e12,e11) = e12| op1(e12,e11) = e13 )& ( op1(e12,e12) = e10| op1(e12,e12) = e11| op1(e12,e12) = e12| op1(e12,e12) = e13 )& ( op1(e12,e13) = e10| op1(e12,e13) = e11| op1(e12,e13) = e12| op1(e12,e13) = e13 )& ( op1(e13,e10) = e10| op1(e13,e10) = e11| op1(e13,e10) = e12| op1(e13,e10) = e13 )& ( op1(e13,e11) = e10| op1(e13,e11) = e11| op1(e13,e11) = e12| op1(e13,e11) = e13 )& ( op1(e13,e12) = e10| op1(e13,e12) = e11| op1(e13,e12) = e12| op1(e13,e12) = e13 )& ( op1(e13,e13) = e10| op1(e13,e13) = e11| op1(e13,e13) = e12| op1(e13,e13) = e13 ) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f2,axiom,(
% 0.12/0.51    ( ( op1(e10,e10) = e10| op1(e10,e11) = e10| op1(e10,e12) = e10| op1(e10,e13) = e10 )& ( op1(e10,e10) = e10| op1(e11,e10) = e10| op1(e12,e10) = e10| op1(e13,e10) = e10 )& ( op1(e10,e10) = e11| op1(e10,e11) = e11| op1(e10,e12) = e11| op1(e10,e13) = e11 )& ( op1(e10,e10) = e11| op1(e11,e10) = e11| op1(e12,e10) = e11| op1(e13,e10) = e11 )& ( op1(e10,e10) = e12| op1(e10,e11) = e12| op1(e10,e12) = e12| op1(e10,e13) = e12 )& ( op1(e10,e10) = e12| op1(e11,e10) = e12| op1(e12,e10) = e12| op1(e13,e10) = e12 )& ( op1(e10,e10) = e13| op1(e10,e11) = e13| op1(e10,e12) = e13| op1(e10,e13) = e13 )& ( op1(e10,e10) = e13| op1(e11,e10) = e13| op1(e12,e10) = e13| op1(e13,e10) = e13 )& ( op1(e11,e10) = e10| op1(e11,e11) = e10| op1(e11,e12) = e10| op1(e11,e13) = e10 )& ( op1(e10,e11) = e10| op1(e11,e11) = e10| op1(e12,e11) = e10| op1(e13,e11) = e10 )& ( op1(e11,e10) = e11| op1(e11,e11) = e11| op1(e11,e12) = e11| op1(e11,e13) = e11 )& ( op1(e10,e11) = e11| op1(e11,e11) = e11| op1(e12,e11) = e11| op1(e13,e11) = e11 )& ( op1(e11,e10) = e12| op1(e11,e11) = e12| op1(e11,e12) = e12| op1(e11,e13) = e12 )& ( op1(e10,e11) = e12| op1(e11,e11) = e12| op1(e12,e11) = e12| op1(e13,e11) = e12 )& ( op1(e11,e10) = e13| op1(e11,e11) = e13| op1(e11,e12) = e13| op1(e11,e13) = e13 )& ( op1(e10,e11) = e13| op1(e11,e11) = e13| op1(e12,e11) = e13| op1(e13,e11) = e13 )& ( op1(e12,e10) = e10| op1(e12,e11) = e10| op1(e12,e12) = e10| op1(e12,e13) = e10 )& ( op1(e10,e12) = e10| op1(e11,e12) = e10| op1(e12,e12) = e10| op1(e13,e12) = e10 )& ( op1(e12,e10) = e11| op1(e12,e11) = e11| op1(e12,e12) = e11| op1(e12,e13) = e11 )& ( op1(e10,e12) = e11| op1(e11,e12) = e11| op1(e12,e12) = e11| op1(e13,e12) = e11 )& ( op1(e12,e10) = e12| op1(e12,e11) = e12| op1(e12,e12) = e12| op1(e12,e13) = e12 )& ( op1(e10,e12) = e12| op1(e11,e12) = e12| op1(e12,e12) = e12| op1(e13,e12) = e12 )& ( op1(e12,e10) = e13| op1(e12,e11) = e13| op1(e12,e12) = e13| op1(e12,e13) = e13 )& ( op1(e10,e12) = e13| op1(e11,e12) = e13| op1(e12,e12) = e13| op1(e13,e12) = e13 )& ( op1(e13,e10) = e10| op1(e13,e11) = e10| op1(e13,e12) = e10| op1(e13,e13) = e10 )& ( op1(e10,e13) = e10| op1(e11,e13) = e10| op1(e12,e13) = e10| op1(e13,e13) = e10 )& ( op1(e13,e10) = e11| op1(e13,e11) = e11| op1(e13,e12) = e11| op1(e13,e13) = e11 )& ( op1(e10,e13) = e11| op1(e11,e13) = e11| op1(e12,e13) = e11| op1(e13,e13) = e11 )& ( op1(e13,e10) = e12| op1(e13,e11) = e12| op1(e13,e12) = e12| op1(e13,e13) = e12 )& ( op1(e10,e13) = e12| op1(e11,e13) = e12| op1(e12,e13) = e12| op1(e13,e13) = e12 )& ( op1(e13,e10) = e13| op1(e13,e11) = e13| op1(e13,e12) = e13| op1(e13,e13) = e13 )& ( op1(e10,e13) = e13| op1(e11,e13) = e13| op1(e12,e13) = e13| op1(e13,e13) = e13 ) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f3,axiom,(
% 0.12/0.51    ( ( op2(e20,e20) = e20| op2(e20,e20) = e21| op2(e20,e20) = e22| op2(e20,e20) = e23 )& ( op2(e20,e21) = e20| op2(e20,e21) = e21| op2(e20,e21) = e22| op2(e20,e21) = e23 )& ( op2(e20,e22) = e20| op2(e20,e22) = e21| op2(e20,e22) = e22| op2(e20,e22) = e23 )& ( op2(e20,e23) = e20| op2(e20,e23) = e21| op2(e20,e23) = e22| op2(e20,e23) = e23 )& ( op2(e21,e20) = e20| op2(e21,e20) = e21| op2(e21,e20) = e22| op2(e21,e20) = e23 )& ( op2(e21,e21) = e20| op2(e21,e21) = e21| op2(e21,e21) = e22| op2(e21,e21) = e23 )& ( op2(e21,e22) = e20| op2(e21,e22) = e21| op2(e21,e22) = e22| op2(e21,e22) = e23 )& ( op2(e21,e23) = e20| op2(e21,e23) = e21| op2(e21,e23) = e22| op2(e21,e23) = e23 )& ( op2(e22,e20) = e20| op2(e22,e20) = e21| op2(e22,e20) = e22| op2(e22,e20) = e23 )& ( op2(e22,e21) = e20| op2(e22,e21) = e21| op2(e22,e21) = e22| op2(e22,e21) = e23 )& ( op2(e22,e22) = e20| op2(e22,e22) = e21| op2(e22,e22) = e22| op2(e22,e22) = e23 )& ( op2(e22,e23) = e20| op2(e22,e23) = e21| op2(e22,e23) = e22| op2(e22,e23) = e23 )& ( op2(e23,e20) = e20| op2(e23,e20) = e21| op2(e23,e20) = e22| op2(e23,e20) = e23 )& ( op2(e23,e21) = e20| op2(e23,e21) = e21| op2(e23,e21) = e22| op2(e23,e21) = e23 )& ( op2(e23,e22) = e20| op2(e23,e22) = e21| op2(e23,e22) = e22| op2(e23,e22) = e23 )& ( op2(e23,e23) = e20| op2(e23,e23) = e21| op2(e23,e23) = e22| op2(e23,e23) = e23 ) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f4,axiom,(
% 0.12/0.51    ( ( op2(e20,e20) = e20| op2(e20,e21) = e20| op2(e20,e22) = e20| op2(e20,e23) = e20 )& ( op2(e20,e20) = e20| op2(e21,e20) = e20| op2(e22,e20) = e20| op2(e23,e20) = e20 )& ( op2(e20,e20) = e21| op2(e20,e21) = e21| op2(e20,e22) = e21| op2(e20,e23) = e21 )& ( op2(e20,e20) = e21| op2(e21,e20) = e21| op2(e22,e20) = e21| op2(e23,e20) = e21 )& ( op2(e20,e20) = e22| op2(e20,e21) = e22| op2(e20,e22) = e22| op2(e20,e23) = e22 )& ( op2(e20,e20) = e22| op2(e21,e20) = e22| op2(e22,e20) = e22| op2(e23,e20) = e22 )& ( op2(e20,e20) = e23| op2(e20,e21) = e23| op2(e20,e22) = e23| op2(e20,e23) = e23 )& ( op2(e20,e20) = e23| op2(e21,e20) = e23| op2(e22,e20) = e23| op2(e23,e20) = e23 )& ( op2(e21,e20) = e20| op2(e21,e21) = e20| op2(e21,e22) = e20| op2(e21,e23) = e20 )& ( op2(e20,e21) = e20| op2(e21,e21) = e20| op2(e22,e21) = e20| op2(e23,e21) = e20 )& ( op2(e21,e20) = e21| op2(e21,e21) = e21| op2(e21,e22) = e21| op2(e21,e23) = e21 )& ( op2(e20,e21) = e21| op2(e21,e21) = e21| op2(e22,e21) = e21| op2(e23,e21) = e21 )& ( op2(e21,e20) = e22| op2(e21,e21) = e22| op2(e21,e22) = e22| op2(e21,e23) = e22 )& ( op2(e20,e21) = e22| op2(e21,e21) = e22| op2(e22,e21) = e22| op2(e23,e21) = e22 )& ( op2(e21,e20) = e23| op2(e21,e21) = e23| op2(e21,e22) = e23| op2(e21,e23) = e23 )& ( op2(e20,e21) = e23| op2(e21,e21) = e23| op2(e22,e21) = e23| op2(e23,e21) = e23 )& ( op2(e22,e20) = e20| op2(e22,e21) = e20| op2(e22,e22) = e20| op2(e22,e23) = e20 )& ( op2(e20,e22) = e20| op2(e21,e22) = e20| op2(e22,e22) = e20| op2(e23,e22) = e20 )& ( op2(e22,e20) = e21| op2(e22,e21) = e21| op2(e22,e22) = e21| op2(e22,e23) = e21 )& ( op2(e20,e22) = e21| op2(e21,e22) = e21| op2(e22,e22) = e21| op2(e23,e22) = e21 )& ( op2(e22,e20) = e22| op2(e22,e21) = e22| op2(e22,e22) = e22| op2(e22,e23) = e22 )& ( op2(e20,e22) = e22| op2(e21,e22) = e22| op2(e22,e22) = e22| op2(e23,e22) = e22 )& ( op2(e22,e20) = e23| op2(e22,e21) = e23| op2(e22,e22) = e23| op2(e22,e23) = e23 )& ( op2(e20,e22) = e23| op2(e21,e22) = e23| op2(e22,e22) = e23| op2(e23,e22) = e23 )& ( op2(e23,e20) = e20| op2(e23,e21) = e20| op2(e23,e22) = e20| op2(e23,e23) = e20 )& ( op2(e20,e23) = e20| op2(e21,e23) = e20| op2(e22,e23) = e20| op2(e23,e23) = e20 )& ( op2(e23,e20) = e21| op2(e23,e21) = e21| op2(e23,e22) = e21| op2(e23,e23) = e21 )& ( op2(e20,e23) = e21| op2(e21,e23) = e21| op2(e22,e23) = e21| op2(e23,e23) = e21 )& ( op2(e23,e20) = e22| op2(e23,e21) = e22| op2(e23,e22) = e22| op2(e23,e23) = e22 )& ( op2(e20,e23) = e22| op2(e21,e23) = e22| op2(e22,e23) = e22| op2(e23,e23) = e22 )& ( op2(e23,e20) = e23| op2(e23,e21) = e23| op2(e23,e22) = e23| op2(e23,e23) = e23 )& ( op2(e20,e23) = e23| op2(e21,e23) = e23| op2(e22,e23) = e23| op2(e23,e23) = e23 ) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f5,axiom,(
% 0.12/0.51    ( op1(e10,e10) != op1(e11,e10)& op1(e10,e10) != op1(e12,e10)& op1(e10,e10) != op1(e13,e10)& op1(e11,e10) != op1(e12,e10)& op1(e11,e10) != op1(e13,e10)& op1(e12,e10) != op1(e13,e10)& op1(e10,e11) != op1(e11,e11)& op1(e10,e11) != op1(e12,e11)& op1(e10,e11) != op1(e13,e11)& op1(e11,e11) != op1(e12,e11)& op1(e11,e11) != op1(e13,e11)& op1(e12,e11) != op1(e13,e11)& op1(e10,e12) != op1(e11,e12)& op1(e10,e12) != op1(e12,e12)& op1(e10,e12) != op1(e13,e12)& op1(e11,e12) != op1(e12,e12)& op1(e11,e12) != op1(e13,e12)& op1(e12,e12) != op1(e13,e12)& op1(e10,e13) != op1(e11,e13)& op1(e10,e13) != op1(e12,e13)& op1(e10,e13) != op1(e13,e13)& op1(e11,e13) != op1(e12,e13)& op1(e11,e13) != op1(e13,e13)& op1(e12,e13) != op1(e13,e13)& op1(e10,e10) != op1(e10,e11)& op1(e10,e10) != op1(e10,e12)& op1(e10,e10) != op1(e10,e13)& op1(e10,e11) != op1(e10,e12)& op1(e10,e11) != op1(e10,e13)& op1(e10,e12) != op1(e10,e13)& op1(e11,e10) != op1(e11,e11)& op1(e11,e10) != op1(e11,e12)& op1(e11,e10) != op1(e11,e13)& op1(e11,e11) != op1(e11,e12)& op1(e11,e11) != op1(e11,e13)& op1(e11,e12) != op1(e11,e13)& op1(e12,e10) != op1(e12,e11)& op1(e12,e10) != op1(e12,e12)& op1(e12,e10) != op1(e12,e13)& op1(e12,e11) != op1(e12,e12)& op1(e12,e11) != op1(e12,e13)& op1(e12,e12) != op1(e12,e13)& op1(e13,e10) != op1(e13,e11)& op1(e13,e10) != op1(e13,e12)& op1(e13,e10) != op1(e13,e13)& op1(e13,e11) != op1(e13,e12)& op1(e13,e11) != op1(e13,e13)& op1(e13,e12) != op1(e13,e13) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f6,axiom,(
% 0.12/0.51    ( op2(e20,e20) != op2(e21,e20)& op2(e20,e20) != op2(e22,e20)& op2(e20,e20) != op2(e23,e20)& op2(e21,e20) != op2(e22,e20)& op2(e21,e20) != op2(e23,e20)& op2(e22,e20) != op2(e23,e20)& op2(e20,e21) != op2(e21,e21)& op2(e20,e21) != op2(e22,e21)& op2(e20,e21) != op2(e23,e21)& op2(e21,e21) != op2(e22,e21)& op2(e21,e21) != op2(e23,e21)& op2(e22,e21) != op2(e23,e21)& op2(e20,e22) != op2(e21,e22)& op2(e20,e22) != op2(e22,e22)& op2(e20,e22) != op2(e23,e22)& op2(e21,e22) != op2(e22,e22)& op2(e21,e22) != op2(e23,e22)& op2(e22,e22) != op2(e23,e22)& op2(e20,e23) != op2(e21,e23)& op2(e20,e23) != op2(e22,e23)& op2(e20,e23) != op2(e23,e23)& op2(e21,e23) != op2(e22,e23)& op2(e21,e23) != op2(e23,e23)& op2(e22,e23) != op2(e23,e23)& op2(e20,e20) != op2(e20,e21)& op2(e20,e20) != op2(e20,e22)& op2(e20,e20) != op2(e20,e23)& op2(e20,e21) != op2(e20,e22)& op2(e20,e21) != op2(e20,e23)& op2(e20,e22) != op2(e20,e23)& op2(e21,e20) != op2(e21,e21)& op2(e21,e20) != op2(e21,e22)& op2(e21,e20) != op2(e21,e23)& op2(e21,e21) != op2(e21,e22)& op2(e21,e21) != op2(e21,e23)& op2(e21,e22) != op2(e21,e23)& op2(e22,e20) != op2(e22,e21)& op2(e22,e20) != op2(e22,e22)& op2(e22,e20) != op2(e22,e23)& op2(e22,e21) != op2(e22,e22)& op2(e22,e21) != op2(e22,e23)& op2(e22,e22) != op2(e22,e23)& op2(e23,e20) != op2(e23,e21)& op2(e23,e20) != op2(e23,e22)& op2(e23,e20) != op2(e23,e23)& op2(e23,e21) != op2(e23,e22)& op2(e23,e21) != op2(e23,e23)& op2(e23,e22) != op2(e23,e23) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f7,axiom,(
% 0.12/0.51    ( e10 != e11& e10 != e12& e10 != e13& e11 != e12& e11 != e13& e12 != e13 ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f8,axiom,(
% 0.12/0.51    ( e20 != e21& e20 != e22& e20 != e23& e21 != e22& e21 != e23& e22 != e23 ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f10,axiom,(
% 0.12/0.51    ( ( op1(e10,e10) = e10| op1(e11,e11) = e11| op1(e12,e12) = e12| op1(e13,e13) = e13 )& ( op1(e10,e10) != e10| op1(e10,e10) = e10 )& ( op1(e10,e10) != e11| op1(e10,e11) = e10 )& ( op1(e10,e10) != e12| op1(e10,e12) = e10 )& ( op1(e10,e10) != e13| op1(e10,e13) = e10 )& ( op1(e11,e11) != e10| op1(e11,e10) = e11 )& ( op1(e11,e11) != e11| op1(e11,e11) = e11 )& ( op1(e11,e11) != e12| op1(e11,e12) = e11 )& ( op1(e11,e11) != e13| op1(e11,e13) = e11 )& ( op1(e12,e12) != e10| op1(e12,e10) = e12 )& ( op1(e12,e12) != e11| op1(e12,e11) = e12 )& ( op1(e12,e12) != e12| op1(e12,e12) = e12 )& ( op1(e12,e12) != e13| op1(e12,e13) = e12 )& ( op1(e13,e13) != e10| op1(e13,e10) = e13 )& ( op1(e13,e13) != e11| op1(e13,e11) = e13 )& ( op1(e13,e13) != e12| op1(e13,e12) = e13 )& ( op1(e13,e13) != e13| op1(e13,e13) = e13 )& ( ( op1(e10,e10) = e10& op1(e10,e10) = e10& op1(e10,e10) != e10 )| ( op1(e10,e11) = e10& op1(e11,e10) = e10& op1(e11,e11) != e11 )| ( op1(e10,e12) = e10& op1(e12,e10) = e10& op1(e12,e12) != e12 )| ( op1(e10,e13) = e10& op1(e13,e10) = e10& op1(e13,e13) != e13 )| ( op1(e11,e10) = e11& op1(e10,e11) = e11& op1(e10,e10) != e10 )| ( op1(e11,e11) = e11& op1(e11,e11) = e11& op1(e11,e11) != e11 )| ( op1(e11,e12) = e11& op1(e12,e11) = e11& op1(e12,e12) != e12 )| ( op1(e11,e13) = e11& op1(e13,e11) = e11& op1(e13,e13) != e13 )| ( op1(e12,e10) = e12& op1(e10,e12) = e12& op1(e10,e10) != e10 )| ( op1(e12,e11) = e12& op1(e11,e12) = e12& op1(e11,e11) != e11 )| ( op1(e12,e12) = e12& op1(e12,e12) = e12& op1(e12,e12) != e12 )| ( op1(e12,e13) = e12& op1(e13,e12) = e12& op1(e13,e13) != e13 )| ( op1(e13,e10) = e13& op1(e10,e13) = e13& op1(e10,e10) != e10 )| ( op1(e13,e11) = e13& op1(e11,e13) = e13& op1(e11,e11) != e11 )| ( op1(e13,e12) = e13& op1(e12,e13) = e13& op1(e12,e12) != e12 )| ( op1(e13,e13) = e13& op1(e13,e13) = e13& op1(e13,e13) != e13 ) ) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f11,axiom,(
% 0.12/0.51    ( ( op2(e20,e20) = e20| op2(e21,e21) = e21| op2(e22,e22) = e22| op2(e23,e23) = e23 )& ( op2(e20,e20) != e20| op2(e20,e20) = e20 )& ( op2(e20,e20) != e21| op2(e20,e21) = e20 )& ( op2(e20,e20) != e22| op2(e20,e22) = e20 )& ( op2(e20,e20) != e23| op2(e20,e23) = e20 )& ( op2(e21,e21) != e20| op2(e21,e20) = e21 )& ( op2(e21,e21) != e21| op2(e21,e21) = e21 )& ( op2(e21,e21) != e22| op2(e21,e22) = e21 )& ( op2(e21,e21) != e23| op2(e21,e23) = e21 )& ( op2(e22,e22) != e20| op2(e22,e20) = e22 )& ( op2(e22,e22) != e21| op2(e22,e21) = e22 )& ( op2(e22,e22) != e22| op2(e22,e22) = e22 )& ( op2(e22,e22) != e23| op2(e22,e23) = e22 )& ( op2(e23,e23) != e20| op2(e23,e20) = e23 )& ( op2(e23,e23) != e21| op2(e23,e21) = e23 )& ( op2(e23,e23) != e22| op2(e23,e22) = e23 )& ( op2(e23,e23) != e23| op2(e23,e23) = e23 )& ( ( op2(e20,e20) = e20& op2(e20,e20) = e20& op2(e20,e20) != e20 )| ( op2(e20,e21) = e20& op2(e21,e20) = e20& op2(e21,e21) != e21 )| ( op2(e20,e22) = e20& op2(e22,e20) = e20& op2(e22,e22) != e22 )| ( op2(e20,e23) = e20& op2(e23,e20) = e20& op2(e23,e23) != e23 )| ( op2(e21,e20) = e21& op2(e20,e21) = e21& op2(e20,e20) != e20 )| ( op2(e21,e21) = e21& op2(e21,e21) = e21& op2(e21,e21) != e21 )| ( op2(e21,e22) = e21& op2(e22,e21) = e21& op2(e22,e22) != e22 )| ( op2(e21,e23) = e21& op2(e23,e21) = e21& op2(e23,e23) != e23 )| ( op2(e22,e20) = e22& op2(e20,e22) = e22& op2(e20,e20) != e20 )| ( op2(e22,e21) = e22& op2(e21,e22) = e22& op2(e21,e21) != e21 )| ( op2(e22,e22) = e22& op2(e22,e22) = e22& op2(e22,e22) != e22 )| ( op2(e22,e23) = e22& op2(e23,e22) = e22& op2(e23,e23) != e23 )| ( op2(e23,e20) = e23& op2(e20,e23) = e23& op2(e20,e20) != e20 )| ( op2(e23,e21) = e23& op2(e21,e23) = e23& op2(e21,e21) != e21 )| ( op2(e23,e22) = e23& op2(e22,e23) = e23& op2(e22,e22) != e22 )| ( op2(e23,e23) = e23& op2(e23,e23) = e23& op2(e23,e23) != e23 ) ) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f12,axiom,(
% 0.12/0.51    ( e10 = op1(e13,e13)& e11 = op1(op1(e13,e13),op1(e13,e13))& e12 = op1(op1(op1(e13,e13),op1(e13,e13)),e13) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f13,axiom,(
% 0.12/0.51    ( e20 = op2(e23,e23)& e21 = op2(op2(e23,e23),op2(e23,e23))& e22 = op2(op2(op2(e23,e23),op2(e23,e23)),e23) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f14,axiom,(
% 0.12/0.51    ( h1(e13) = e20& h1(e10) = op2(e20,e20)& h1(e11) = op2(op2(e20,e20),op2(e20,e20))& h1(e12) = op2(op2(op2(e20,e20),op2(e20,e20)),e20) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f16,axiom,(
% 0.12/0.51    ( h3(e13) = e22& h3(e10) = op2(e22,e22)& h3(e11) = op2(op2(e22,e22),op2(e22,e22))& h3(e12) = op2(op2(op2(e22,e22),op2(e22,e22)),e22) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f17,axiom,(
% 0.12/0.51    ( h4(e13) = e23& h4(e10) = op2(e23,e23)& h4(e11) = op2(op2(e23,e23),op2(e23,e23))& h4(e12) = op2(op2(op2(e23,e23),op2(e23,e23)),e23) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f18,conjecture,(
% 0.12/0.51    ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))& ( h1(e10) = e20| h1(e11) = e20| h1(e12) = e20| h1(e13) = e20 )& ( h1(e10) = e21| h1(e11) = e21| h1(e12) = e21| h1(e13) = e21 )& ( h1(e10) = e22| h1(e11) = e22| h1(e12) = e22| h1(e13) = e22 )& ( h1(e10) = e23| h1(e11) = e23| h1(e12) = e23| h1(e13) = e23 ) )| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))& ( h2(e10) = e20| h2(e11) = e20| h2(e12) = e20| h2(e13) = e20 )& ( h2(e10) = e21| h2(e11) = e21| h2(e12) = e21| h2(e13) = e21 )& ( h2(e10) = e22| h2(e11) = e22| h2(e12) = e22| h2(e13) = e22 )& ( h2(e10) = e23| h2(e11) = e23| h2(e12) = e23| h2(e13) = e23 ) )| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))& ( h3(e10) = e20| h3(e11) = e20| h3(e12) = e20| h3(e13) = e20 )& ( h3(e10) = e21| h3(e11) = e21| h3(e12) = e21| h3(e13) = e21 )& ( h3(e10) = e22| h3(e11) = e22| h3(e12) = e22| h3(e13) = e22 )& ( h3(e10) = e23| h3(e11) = e23| h3(e12) = e23| h3(e13) = e23 ) )| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))& ( h4(e10) = e20| h4(e11) = e20| h4(e12) = e20| h4(e13) = e20 )& ( h4(e10) = e21| h4(e11) = e21| h4(e12) = e21| h4(e13) = e21 )& ( h4(e10) = e22| h4(e11) = e22| h4(e12) = e22| h4(e13) = e22 )& ( h4(e10) = e23| h4(e11) = e23| h4(e12) = e23| h4(e13) = e23 ) ) ) ),
% 0.12/0.51    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51  fof(f19,negated_conjecture,(
% 0.12/0.51    ~(( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))& ( h1(e10) = e20| h1(e11) = e20| h1(e12) = e20| h1(e13) = e20 )& ( h1(e10) = e21| h1(e11) = e21| h1(e12) = e21| h1(e13) = e21 )& ( h1(e10) = e22| h1(e11) = e22| h1(e12) = e22| h1(e13) = e22 )& ( h1(e10) = e23| h1(e11) = e23| h1(e12) = e23| h1(e13) = e23 ) )| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))& ( h2(e10) = e20| h2(e11) = e20| h2(e12) = e20| h2(e13) = e20 )& ( h2(e10) = e21| h2(e11) = e21| h2(e12) = e21| h2(e13) = e21 )& ( h2(e10) = e22| h2(e11) = e22| h2(e12) = e22| h2(e13) = e22 )& ( h2(e10) = e23| h2(e11) = e23| h2(e12) = e23| h2(e13) = e23 ) )| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))& ( h3(e10) = e20| h3(e11) = e20| h3(e12) = e20| h3(e13) = e20 )& ( h3(e10) = e21| h3(e11) = e21| h3(e12) = e21| h3(e13) = e21 )& ( h3(e10) = e22| h3(e11) = e22| h3(e12) = e22| h3(e13) = e22 )& ( h3(e10) = e23| h3(e11) = e23| h3(e12) = e23| h3(e13) = e23 ) )| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))& ( h4(e10) = e20| h4(e11) = e20| h4(e12) = e20| h4(e13) = e20 )& ( h4(e10) = e21| h4(e11) = e21| h4(e12) = e21| h4(e13) = e21 )& ( h4(e10) = e22| h4(e11) = e22| h4(e12) = e22| h4(e13) = e22 )& ( h4(e10) = e23| h4(e11) = e23| h4(e12) = e23| h4(e13) = e23 ) ) ) )),
% 0.12/0.51    inference(negated_conjecture,[status(cth)],[f18])).
% 0.12/0.51  fof(f23,plain,(
% 0.12/0.51    op1(e10,e13)=e10|op1(e10,e13)=e11|op1(e10,e13)=e12|op1(e10,e13)=e13),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.51  fof(f25,plain,(
% 0.12/0.51    op1(e11,e11)=e10|op1(e11,e11)=e11|op1(e11,e11)=e12|op1(e11,e11)=e13),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.51  fof(f29,plain,(
% 0.12/0.51    op1(e12,e11)=e10|op1(e12,e11)=e11|op1(e12,e11)=e12|op1(e12,e11)=e13),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.51  fof(f34,plain,(
% 0.12/0.51    op1(e13,e12)=e10|op1(e13,e12)=e11|op1(e13,e12)=e12|op1(e13,e12)=e13),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.51  fof(f40,plain,(
% 0.12/0.51    op1(e10,e10)=e12|op1(e10,e11)=e12|op1(e10,e12)=e12|op1(e10,e13)=e12),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.51  fof(f41,plain,(
% 0.12/0.51    op1(e10,e10)=e12|op1(e11,e10)=e12|op1(e12,e10)=e12|op1(e13,e10)=e12),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.51  fof(f44,plain,(
% 0.12/0.51    op1(e11,e10)=e10|op1(e11,e11)=e10|op1(e11,e12)=e10|op1(e11,e13)=e10),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.51  fof(f49,plain,(
% 0.12/0.51    op1(e10,e11)=e12|op1(e11,e11)=e12|op1(e12,e11)=e12|op1(e13,e11)=e12),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.51  fof(f50,plain,(
% 0.12/0.51    op1(e11,e10)=e13|op1(e11,e11)=e13|op1(e11,e12)=e13|op1(e11,e13)=e13),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.51  fof(f53,plain,(
% 0.12/0.51    op1(e10,e12)=e10|op1(e11,e12)=e10|op1(e12,e12)=e10|op1(e13,e12)=e10),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.51  fof(f63,plain,(
% 0.12/0.51    op1(e10,e13)=e11|op1(e11,e13)=e11|op1(e12,e13)=e11|op1(e13,e13)=e11),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.51  fof(f71,plain,(
% 0.12/0.51    op2(e20,e23)=e20|op2(e20,e23)=e21|op2(e20,e23)=e22|op2(e20,e23)=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.51  fof(f82,plain,(
% 0.12/0.51    op2(e23,e22)=e20|op2(e23,e22)=e21|op2(e23,e22)=e22|op2(e23,e22)=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.51  fof(f85,plain,(
% 0.12/0.51    op2(e20,e20)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f88,plain,(
% 0.12/0.51    op2(e20,e20)=e22|op2(e20,e21)=e22|op2(e20,e22)=e22|op2(e20,e23)=e22),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f89,plain,(
% 0.12/0.51    op2(e20,e20)=e22|op2(e21,e20)=e22|op2(e22,e20)=e22|op2(e23,e20)=e22),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f94,plain,(
% 0.12/0.51    op2(e21,e20)=e21|op2(e21,e21)=e21|op2(e21,e22)=e21|op2(e21,e23)=e21),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f99,plain,(
% 0.12/0.51    op2(e20,e21)=e23|op2(e21,e21)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f101,plain,(
% 0.12/0.51    op2(e20,e22)=e20|op2(e21,e22)=e20|op2(e22,e22)=e20|op2(e23,e22)=e20),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f107,plain,(
% 0.12/0.51    op2(e20,e22)=e23|op2(e21,e22)=e23|op2(e22,e22)=e23|op2(e23,e22)=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f111,plain,(
% 0.12/0.51    op2(e20,e23)=e21|op2(e21,e23)=e21|op2(e22,e23)=e21|op2(e23,e23)=e21),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f112,plain,(
% 0.12/0.51    op2(e23,e20)=e22|op2(e23,e21)=e22|op2(e23,e22)=e22|op2(e23,e23)=e22),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.51  fof(f120,plain,(
% 0.12/0.51    ~op1(e11,e10)=op1(e13,e10)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f122,plain,(
% 0.12/0.51    ~op1(e10,e11)=op1(e11,e11)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f123,plain,(
% 0.12/0.51    ~op1(e10,e11)=op1(e12,e11)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f130,plain,(
% 0.12/0.51    ~op1(e10,e12)=op1(e13,e12)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f134,plain,(
% 0.12/0.51    ~op1(e10,e13)=op1(e11,e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f136,plain,(
% 0.12/0.51    ~op1(e10,e13)=op1(e13,e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f142,plain,(
% 0.12/0.51    ~op1(e10,e10)=op1(e10,e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f143,plain,(
% 0.12/0.51    ~op1(e10,e11)=op1(e10,e12)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f148,plain,(
% 0.12/0.51    ~op1(e11,e10)=op1(e11,e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f150,plain,(
% 0.12/0.51    ~op1(e11,e11)=op1(e11,e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f152,plain,(
% 0.12/0.51    ~op1(e12,e10)=op1(e12,e11)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f156,plain,(
% 0.12/0.51    ~op1(e12,e11)=op1(e12,e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f159,plain,(
% 0.12/0.51    ~op1(e13,e10)=op1(e13,e12)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f163,plain,(
% 0.12/0.51    ~op1(e13,e12)=op1(e13,e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.51  fof(f164,plain,(
% 0.12/0.51    ~op2(e20,e20)=op2(e21,e20)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f178,plain,(
% 0.12/0.51    ~op2(e20,e22)=op2(e23,e22)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f182,plain,(
% 0.12/0.51    ~op2(e20,e23)=op2(e21,e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f184,plain,(
% 0.12/0.51    ~op2(e20,e23)=op2(e23,e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f185,plain,(
% 0.12/0.51    ~op2(e21,e23)=op2(e22,e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f190,plain,(
% 0.12/0.51    ~op2(e20,e20)=op2(e20,e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f191,plain,(
% 0.12/0.51    ~op2(e20,e21)=op2(e20,e22)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f196,plain,(
% 0.12/0.51    ~op2(e21,e20)=op2(e21,e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f206,plain,(
% 0.12/0.51    ~op2(e23,e20)=op2(e23,e21)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f207,plain,(
% 0.12/0.51    ~op2(e23,e20)=op2(e23,e22)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f211,plain,(
% 0.12/0.51    ~op2(e23,e22)=op2(e23,e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51  fof(f212,plain,(
% 0.12/0.51    ~e10=e11),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.51  fof(f213,plain,(
% 0.12/0.51    ~e10=e12),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.51  fof(f214,plain,(
% 0.12/0.51    ~e10=e13),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.51  fof(f215,plain,(
% 0.12/0.51    ~e11=e12),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.51  fof(f217,plain,(
% 0.12/0.51    ~e12=e13),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.51  fof(f218,plain,(
% 0.12/0.51    ~e20=e21),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.51  fof(f219,plain,(
% 0.12/0.51    ~e20=e22),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.51  fof(f220,plain,(
% 0.12/0.51    ~e20=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.51  fof(f221,plain,(
% 0.12/0.51    ~e21=e22),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.51  fof(f222,plain,(
% 0.12/0.51    ~e21=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.51  fof(f223,plain,(
% 0.12/0.51    ~e22=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.51  fof(f240,definition,(
% 0.12/0.51    sP0_prd<=>((((((((((((((((op1(e10,e10)=e10&op1(e10,e10)=e10)&~op1(e10,e10)=e10)|((op1(e10,e11)=e10&op1(e11,e10)=e10)&~op1(e11,e11)=e11))|((op1(e10,e12)=e10&op1(e12,e10)=e10)&~op1(e12,e12)=e12))|((op1(e10,e13)=e10&op1(e13,e10)=e10)&~op1(e13,e13)=e13))|((op1(e11,e10)=e11&op1(e10,e11)=e11)&~op1(e10,e10)=e10))|((op1(e11,e11)=e11&op1(e11,e11)=e11)&~op1(e11,e11)=e11))|((op1(e11,e12)=e11&op1(e12,e11)=e11)&~op1(e12,e12)=e12))|((op1(e11,e13)=e11&op1(e13,e11)=e11)&~op1(e13,e13)=e13))|((op1(e12,e10)=e12&op1(e10,e12)=e12)&~op1(e10,e10)=e10))|((op1(e12,e11)=e12&op1(e11,e12)=e12)&~op1(e11,e11)=e11))|((op1(e12,e12)=e12&op1(e12,e12)=e12)&~op1(e12,e12)=e12))|((op1(e12,e13)=e12&op1(e13,e12)=e12)&~op1(e13,e13)=e13))|((op1(e13,e10)=e13&op1(e10,e13)=e13)&~op1(e10,e10)=e10))|((op1(e13,e11)=e13&op1(e11,e13)=e13)&~op1(e11,e11)=e11))|((op1(e13,e12)=e13&op1(e12,e13)=e13)&~op1(e12,e12)=e12))),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/0.51  fof(f241,plain,(
% 0.12/0.51    (((((((((((((((((((op1(e10,e10)=e10|op1(e11,e11)=e11)|op1(e12,e12)=e12)|op1(e13,e13)=e13)&(~op1(e10,e10)=e10|op1(e10,e10)=e10))&(~op1(e10,e10)=e11|op1(e10,e11)=e10))&(~op1(e10,e10)=e12|op1(e10,e12)=e10))&(~op1(e10,e10)=e13|op1(e10,e13)=e10))&(~op1(e11,e11)=e10|op1(e11,e10)=e11))&(~op1(e11,e11)=e11|op1(e11,e11)=e11))&(~op1(e11,e11)=e12|op1(e11,e12)=e11))&(~op1(e11,e11)=e13|op1(e11,e13)=e11))&(~op1(e12,e12)=e10|op1(e12,e10)=e12))&(~op1(e12,e12)=e11|op1(e12,e11)=e12))&(~op1(e12,e12)=e12|op1(e12,e12)=e12))&(~op1(e12,e12)=e13|op1(e12,e13)=e12))&(~op1(e13,e13)=e10|op1(e13,e10)=e13))&(~op1(e13,e13)=e11|op1(e13,e11)=e13))&(~op1(e13,e13)=e12|op1(e13,e12)=e13))&(~op1(e13,e13)=e13|op1(e13,e13)=e13))&(sP0_prd|((op1(e13,e13)=e13&op1(e13,e13)=e13)&~op1(e13,e13)=e13))),
% 0.12/0.51    inference(formula_renaming,[status(thm)],[f10,f240])).
% 0.12/0.51  fof(f244,plain,(
% 0.12/0.51    ~op1(e10,e10)=e11|op1(e10,e11)=e10),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f241])).
% 0.12/0.51  fof(f250,plain,(
% 0.12/0.51    ~op1(e11,e11)=e13|op1(e11,e13)=e11),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f241])).
% 0.12/0.51  fof(f255,plain,(
% 0.12/0.51    ~op1(e13,e13)=e10|op1(e13,e10)=e13),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f241])).
% 0.12/0.51  fof(f262,definition,(
% 0.12/0.51    sP1_prd<=>((((((((((((((((op2(e20,e20)=e20&op2(e20,e20)=e20)&~op2(e20,e20)=e20)|((op2(e20,e21)=e20&op2(e21,e20)=e20)&~op2(e21,e21)=e21))|((op2(e20,e22)=e20&op2(e22,e20)=e20)&~op2(e22,e22)=e22))|((op2(e20,e23)=e20&op2(e23,e20)=e20)&~op2(e23,e23)=e23))|((op2(e21,e20)=e21&op2(e20,e21)=e21)&~op2(e20,e20)=e20))|((op2(e21,e21)=e21&op2(e21,e21)=e21)&~op2(e21,e21)=e21))|((op2(e21,e22)=e21&op2(e22,e21)=e21)&~op2(e22,e22)=e22))|((op2(e21,e23)=e21&op2(e23,e21)=e21)&~op2(e23,e23)=e23))|((op2(e22,e20)=e22&op2(e20,e22)=e22)&~op2(e20,e20)=e20))|((op2(e22,e21)=e22&op2(e21,e22)=e22)&~op2(e21,e21)=e21))|((op2(e22,e22)=e22&op2(e22,e22)=e22)&~op2(e22,e22)=e22))|((op2(e22,e23)=e22&op2(e23,e22)=e22)&~op2(e23,e23)=e23))|((op2(e23,e20)=e23&op2(e20,e23)=e23)&~op2(e20,e20)=e20))|((op2(e23,e21)=e23&op2(e21,e23)=e23)&~op2(e21,e21)=e21))|((op2(e23,e22)=e23&op2(e22,e23)=e23)&~op2(e22,e22)=e22))),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.12/0.51  fof(f263,plain,(
% 0.12/0.51    (((((((((((((((((((op2(e20,e20)=e20|op2(e21,e21)=e21)|op2(e22,e22)=e22)|op2(e23,e23)=e23)&(~op2(e20,e20)=e20|op2(e20,e20)=e20))&(~op2(e20,e20)=e21|op2(e20,e21)=e20))&(~op2(e20,e20)=e22|op2(e20,e22)=e20))&(~op2(e20,e20)=e23|op2(e20,e23)=e20))&(~op2(e21,e21)=e20|op2(e21,e20)=e21))&(~op2(e21,e21)=e21|op2(e21,e21)=e21))&(~op2(e21,e21)=e22|op2(e21,e22)=e21))&(~op2(e21,e21)=e23|op2(e21,e23)=e21))&(~op2(e22,e22)=e20|op2(e22,e20)=e22))&(~op2(e22,e22)=e21|op2(e22,e21)=e22))&(~op2(e22,e22)=e22|op2(e22,e22)=e22))&(~op2(e22,e22)=e23|op2(e22,e23)=e22))&(~op2(e23,e23)=e20|op2(e23,e20)=e23))&(~op2(e23,e23)=e21|op2(e23,e21)=e23))&(~op2(e23,e23)=e22|op2(e23,e22)=e23))&(~op2(e23,e23)=e23|op2(e23,e23)=e23))&(sP1_prd|((op2(e23,e23)=e23&op2(e23,e23)=e23)&~op2(e23,e23)=e23))),
% 0.12/0.51    inference(formula_renaming,[status(thm)],[f11,f262])).
% 0.12/0.51  fof(f264,plain,(
% 0.12/0.51    op2(e20,e20)=e20|op2(e21,e21)=e21|op2(e22,e22)=e22|op2(e23,e23)=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f263])).
% 0.12/0.51  fof(f266,plain,(
% 0.12/0.51    ~op2(e20,e20)=e21|op2(e20,e21)=e20),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f263])).
% 0.12/0.51  fof(f272,plain,(
% 0.12/0.51    ~op2(e21,e21)=e23|op2(e21,e23)=e21),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f263])).
% 0.12/0.51  fof(f276,plain,(
% 0.12/0.51    ~op2(e22,e22)=e23|op2(e22,e23)=e22),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f263])).
% 0.12/0.51  fof(f277,plain,(
% 0.12/0.51    ~op2(e23,e23)=e20|op2(e23,e20)=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f263])).
% 0.12/0.51  fof(f284,plain,(
% 0.12/0.51    e10=op1(e13,e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.51  fof(f285,plain,(
% 0.12/0.51    e11=op1(op1(e13,e13),op1(e13,e13))),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.51  fof(f286,plain,(
% 0.12/0.51    e12=op1(op1(op1(e13,e13),op1(e13,e13)),e13)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.51  fof(f287,plain,(
% 0.12/0.51    e20=op2(e23,e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f13])).
% 0.12/0.51  fof(f288,plain,(
% 0.12/0.51    e21=op2(op2(e23,e23),op2(e23,e23))),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f13])).
% 0.12/0.51  fof(f289,plain,(
% 0.12/0.51    e22=op2(op2(op2(e23,e23),op2(e23,e23)),e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f13])).
% 0.12/0.51  fof(f292,plain,(
% 0.12/0.51    h1(e11)=op2(op2(e20,e20),op2(e20,e20))),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f14])).
% 0.12/0.51  fof(f293,plain,(
% 0.12/0.51    h1(e12)=op2(op2(op2(e20,e20),op2(e20,e20)),e20)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f14])).
% 0.12/0.51  fof(f299,plain,(
% 0.12/0.51    h3(e10)=op2(e22,e22)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f16])).
% 0.12/0.51  fof(f302,plain,(
% 0.12/0.51    h4(e13)=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.51  fof(f303,plain,(
% 0.12/0.51    h4(e10)=op2(e23,e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.51  fof(f304,plain,(
% 0.12/0.51    h4(e11)=op2(op2(e23,e23),op2(e23,e23))),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.51  fof(f305,plain,(
% 0.12/0.51    h4(e12)=op2(op2(op2(e23,e23),op2(e23,e23)),e23)),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.51  fof(f306,plain,(
% 0.12/0.51    ((((((((((((((((((((((~h1(op1(e10,e10))=op2(h1(e10),h1(e10))|~h1(op1(e10,e11))=op2(h1(e10),h1(e11)))|~h1(op1(e10,e12))=op2(h1(e10),h1(e12)))|~h1(op1(e10,e13))=op2(h1(e10),h1(e13)))|~h1(op1(e11,e10))=op2(h1(e11),h1(e10)))|~h1(op1(e11,e11))=op2(h1(e11),h1(e11)))|~h1(op1(e11,e12))=op2(h1(e11),h1(e12)))|~h1(op1(e11,e13))=op2(h1(e11),h1(e13)))|~h1(op1(e12,e10))=op2(h1(e12),h1(e10)))|~h1(op1(e12,e11))=op2(h1(e12),h1(e11)))|~h1(op1(e12,e12))=op2(h1(e12),h1(e12)))|~h1(op1(e12,e13))=op2(h1(e12),h1(e13)))|~h1(op1(e13,e10))=op2(h1(e13),h1(e10)))|~h1(op1(e13,e11))=op2(h1(e13),h1(e11)))|~h1(op1(e13,e12))=op2(h1(e13),h1(e12)))|~h1(op1(e13,e13))=op2(h1(e13),h1(e13)))|(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20))|(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21))|(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22))|(((~h1(e10)=e23&~h1(e11)=e23)&~h1(e12)=e23)&~h1(e13)=e23))&(((((((((((((((((((~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11)))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12)))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13)))|~h2(op1(e11,e10))=op2(h2(e11),h2(e10)))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11)))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12)))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13)))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10)))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11)))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12)))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13)))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10)))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11)))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12)))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13)))|(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20))|(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21))|(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22))|(((~h2(e10)=e23&~h2(e11)=e23)&~h2(e12)=e23)&~h2(e13)=e23)))&(((((((((((((((((((~h3(op1(e10,e10))=op2(h3(e10),h3(e10))|~h3(op1(e10,e11))=op2(h3(e10),h3(e11)))|~h3(op1(e10,e12))=op2(h3(e10),h3(e12)))|~h3(op1(e10,e13))=op2(h3(e10),h3(e13)))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10)))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11)))|~h3(op1(e11,e12))=op2(h3(e11),h3(e12)))|~h3(op1(e11,e13))=op2(h3(e11),h3(e13)))|~h3(op1(e12,e10))=op2(h3(e12),h3(e10)))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11)))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12)))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13)))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10)))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11)))|~h3(op1(e13,e12))=op2(h3(e13),h3(e12)))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13)))|(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20))|(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21))|(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22))|(((~h3(e10)=e23&~h3(e11)=e23)&~h3(e12)=e23)&~h3(e13)=e23)))&(((((((((((((((((((~h4(op1(e10,e10))=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11)))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12)))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13)))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10)))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11)))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12)))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13)))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10)))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11)))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12)))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13)))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10)))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11)))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12)))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13)))|(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20))|(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21))|(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22))|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23)))),
% 0.12/0.51    inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.12/0.51  fof(f307,definition,(
% 0.12/0.51    sP2_prd<=>(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.12/0.51  fof(f308,definition,(
% 0.12/0.51    sP3_prd<=>(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.12/0.51  fof(f309,definition,(
% 0.12/0.51    sP4_prd<=>(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.12/0.51  fof(f310,definition,(
% 0.12/0.51    sP5_prd<=>(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.12/0.51  fof(f311,definition,(
% 0.12/0.51    sP6_prd<=>(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.12/0.51  fof(f312,definition,(
% 0.12/0.51    sP7_prd<=>(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.12/0.51  fof(f313,definition,(
% 0.12/0.51    sP8_prd<=>(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.12/0.51  fof(f314,definition,(
% 0.12/0.51    sP9_prd<=>(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.12/0.51  fof(f315,definition,(
% 0.12/0.51    sP10_prd<=>(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.12/0.51  fof(f316,definition,(
% 0.12/0.51    sP11_prd<=>(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.12/0.51  fof(f317,definition,(
% 0.12/0.51    sP12_prd<=>(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.12/0.51  fof(f318,definition,(
% 0.12/0.51    sP13_prd<=>(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22)),
% 0.12/0.51    introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.12/0.51  fof(f319,plain,(
% 0.12/0.51    (((((((((((((((((((((~h1(op1(e10,e10))=op2(h1(e10),h1(e10))|~h1(op1(e10,e11))=op2(h1(e10),h1(e11)))|~h1(op1(e10,e12))=op2(h1(e10),h1(e12)))|~h1(op1(e10,e13))=op2(h1(e10),h1(e13)))|~h1(op1(e11,e10))=op2(h1(e11),h1(e10)))|~h1(op1(e11,e11))=op2(h1(e11),h1(e11)))|~h1(op1(e11,e12))=op2(h1(e11),h1(e12)))|~h1(op1(e11,e13))=op2(h1(e11),h1(e13)))|~h1(op1(e12,e10))=op2(h1(e12),h1(e10)))|~h1(op1(e12,e11))=op2(h1(e12),h1(e11)))|~h1(op1(e12,e12))=op2(h1(e12),h1(e12)))|~h1(op1(e12,e13))=op2(h1(e12),h1(e13)))|~h1(op1(e13,e10))=op2(h1(e13),h1(e10)))|~h1(op1(e13,e11))=op2(h1(e13),h1(e11)))|~h1(op1(e13,e12))=op2(h1(e13),h1(e12)))|~h1(op1(e13,e13))=op2(h1(e13),h1(e13)))|sP2_prd)|sP3_prd)|sP4_prd)|(((~h1(e10)=e23&~h1(e11)=e23)&~h1(e12)=e23)&~h1(e13)=e23))&(((((((((((((((((((~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11)))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12)))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13)))|~h2(op1(e11,e10))=op2(h2(e11),h2(e10)))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11)))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12)))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13)))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10)))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11)))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12)))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13)))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10)))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11)))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12)))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13)))|sP5_prd)|sP6_prd)|sP7_prd)|(((~h2(e10)=e23&~h2(e11)=e23)&~h2(e12)=e23)&~h2(e13)=e23)))&(((((((((((((((((((~h3(op1(e10,e10))=op2(h3(e10),h3(e10))|~h3(op1(e10,e11))=op2(h3(e10),h3(e11)))|~h3(op1(e10,e12))=op2(h3(e10),h3(e12)))|~h3(op1(e10,e13))=op2(h3(e10),h3(e13)))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10)))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11)))|~h3(op1(e11,e12))=op2(h3(e11),h3(e12)))|~h3(op1(e11,e13))=op2(h3(e11),h3(e13)))|~h3(op1(e12,e10))=op2(h3(e12),h3(e10)))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11)))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12)))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13)))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10)))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11)))|~h3(op1(e13,e12))=op2(h3(e13),h3(e12)))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13)))|sP8_prd)|sP9_prd)|sP10_prd)|(((~h3(e10)=e23&~h3(e11)=e23)&~h3(e12)=e23)&~h3(e13)=e23)))&(((((((((((((((((((~h4(op1(e10,e10))=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11)))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12)))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13)))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10)))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11)))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12)))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13)))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10)))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11)))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12)))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13)))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10)))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11)))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12)))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13)))|sP11_prd)|sP12_prd)|sP13_prd)|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23))),
% 0.12/0.51    inference(formula_renaming,[status(thm)],[f306,f318,f317,f316,f315,f314,f313,f312,f311,f310,f309,f308,f307])).
% 0.12/0.51  fof(f335,plain,(
% 0.12/0.51    ~h4(op1(e10,e10))=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f319])).
% 0.12/0.51  fof(f406,plain,(
% 0.12/0.51    (~sP11_prd|(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20))&(sP11_prd|(((h4(e10)=e20|h4(e11)=e20)|h4(e12)=e20)|h4(e13)=e20))),
% 0.12/0.51    inference(NNF_transformation,[status(thm)],[f316])).
% 0.12/0.51  fof(f407,plain,(
% 0.12/0.51    ~sP11_prd|~h4(e10)=e20),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f406])).
% 0.12/0.51  fof(f412,plain,(
% 0.12/0.51    (~sP12_prd|(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21))&(sP12_prd|(((h4(e10)=e21|h4(e11)=e21)|h4(e12)=e21)|h4(e13)=e21))),
% 0.12/0.51    inference(NNF_transformation,[status(thm)],[f317])).
% 0.12/0.51  fof(f414,plain,(
% 0.12/0.51    ~sP12_prd|~h4(e11)=e21),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f412])).
% 0.12/0.51  fof(f418,plain,(
% 0.12/0.51    (~sP13_prd|(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22))&(sP13_prd|(((h4(e10)=e22|h4(e11)=e22)|h4(e12)=e22)|h4(e13)=e22))),
% 0.12/0.51    inference(NNF_transformation,[status(thm)],[f318])).
% 0.12/0.51  fof(f421,plain,(
% 0.12/0.51    ~sP13_prd|~h4(e12)=e22),
% 0.12/0.51    inference(cnf_transformation,[status(thm)],[f418])).
% 0.12/0.51  fof(f646,plain,(
% 0.12/0.51    ~e10=e10|op1(e13,e10)=e13),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f284,f255])).
% 0.12/0.51  fof(f648,plain,(
% 0.12/0.51    ~op1(e13,e12)=e10),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f284,f163])).
% 0.12/0.51  fof(f653,plain,(
% 0.12/0.51    ~op1(e10,e13)=e10),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f284,f136])).
% 0.12/0.51  fof(f658,plain,(
% 0.12/0.51    op1(e10,e13)=e11|op1(e11,e13)=e11|op1(e12,e13)=e11|e10=e11),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f284,f63])).
% 0.12/0.51  fof(f663,plain,(
% 0.12/0.51    e11=op1(e10,op1(e13,e13))),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f284,f285])).
% 0.12/0.51  fof(f666,plain,(
% 0.12/0.51    ~e11=e11|op1(e10,e11)=e10),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f682,f244])).
% 0.12/0.51  fof(f667,plain,(
% 0.12/0.51    ~e11=op1(e10,e13)),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f682,f142])).
% 0.12/0.51  fof(f675,plain,(
% 0.12/0.51    e11=e12|op1(e11,e10)=e12|op1(e12,e10)=e12|op1(e13,e10)=e12),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f682,f41])).
% 0.12/0.51  fof(f676,plain,(
% 0.12/0.51    e11=e12|op1(e10,e11)=e12|op1(e10,e12)=e12|op1(e10,e13)=e12),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f682,f40])).
% 0.12/0.51  fof(f682,plain,(
% 0.12/0.51    e11=op1(e10,e10)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f284,f663])).
% 0.12/0.51  fof(f683,plain,(
% 0.12/0.51    e12=op1(op1(e10,op1(e13,e13)),e13)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f284,f286])).
% 0.12/0.51  fof(f684,plain,(
% 0.12/0.51    e12=op1(op1(e10,e10),e13)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f284,f683])).
% 0.12/0.51  fof(f685,plain,(
% 0.12/0.51    ~op1(e11,e11)=e13|e12=e11),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f696,f250])).
% 0.12/0.51  fof(f687,plain,(
% 0.12/0.51    ~op1(e11,e11)=e12),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f696,f150])).
% 0.12/0.51  fof(f688,plain,(
% 0.12/0.51    ~op1(e11,e10)=e12),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f696,f148])).
% 0.12/0.51  fof(f690,plain,(
% 0.12/0.51    ~op1(e10,e13)=e12),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f696,f134])).
% 0.12/0.51  fof(f691,plain,(
% 0.12/0.51    op1(e11,e10)=e13|op1(e11,e11)=e13|op1(e11,e12)=e13|e12=e13),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f696,f50])).
% 0.12/0.51  fof(f694,plain,(
% 0.12/0.51    op1(e11,e10)=e10|op1(e11,e11)=e10|op1(e11,e12)=e10|e12=e10),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f696,f44])).
% 0.12/0.51  fof(f696,plain,(
% 0.12/0.51    e12=op1(e11,e13)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f682,f684])).
% 0.12/0.51  fof(f699,plain,(
% 0.12/0.51    ~e20=e20|op2(e23,e20)=e23),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f287,f277])).
% 0.12/0.51  fof(f700,plain,(
% 0.12/0.51    op2(e20,e20)=e20|op2(e21,e21)=e21|op2(e22,e22)=e22|e20=e23),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f287,f264])).
% 0.12/0.51  fof(f701,plain,(
% 0.12/0.51    ~op2(e23,e22)=e20),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f287,f211])).
% 0.12/0.51  fof(f706,plain,(
% 0.12/0.51    ~op2(e20,e23)=e20),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f287,f184])).
% 0.12/0.51  fof(f710,plain,(
% 0.12/0.51    op2(e23,e20)=e22|op2(e23,e21)=e22|op2(e23,e22)=e22|e20=e22),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f287,f112])).
% 0.12/0.51  fof(f711,plain,(
% 0.12/0.51    op2(e20,e23)=e21|op2(e21,e23)=e21|op2(e22,e23)=e21|e20=e21),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f287,f111])).
% 0.12/0.51  fof(f716,plain,(
% 0.12/0.51    e21=op2(e20,op2(e23,e23))),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f288])).
% 0.12/0.51  fof(f719,plain,(
% 0.12/0.51    ~e21=e21|op2(e20,e21)=e20),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f735,f266])).
% 0.12/0.51  fof(f720,plain,(
% 0.12/0.51    ~e21=op2(e20,e23)),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f735,f190])).
% 0.12/0.51  fof(f725,plain,(
% 0.12/0.51    ~e21=op2(e21,e20)),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f735,f164])).
% 0.12/0.51  fof(f728,plain,(
% 0.12/0.51    e21=e22|op2(e21,e20)=e22|op2(e22,e20)=e22|op2(e23,e20)=e22),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f735,f89])).
% 0.12/0.51  fof(f729,plain,(
% 0.12/0.51    e21=e22|op2(e20,e21)=e22|op2(e20,e22)=e22|op2(e20,e23)=e22),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f735,f88])).
% 0.12/0.51  fof(f732,plain,(
% 0.12/0.51    e21=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f735,f85])).
% 0.12/0.51  fof(f735,plain,(
% 0.12/0.51    e21=op2(e20,e20)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f716])).
% 0.12/0.51  fof(f736,plain,(
% 0.12/0.51    e22=op2(op2(e20,op2(e23,e23)),e23)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f289])).
% 0.12/0.51  fof(f737,plain,(
% 0.12/0.51    e22=op2(op2(e20,e20),e23)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f736])).
% 0.12/0.51  fof(f738,plain,(
% 0.12/0.51    ~op2(e21,e21)=e23|e22=e21),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f749,f272])).
% 0.12/0.51  fof(f741,plain,(
% 0.12/0.51    ~op2(e21,e20)=e22),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f749,f196])).
% 0.12/0.51  fof(f742,plain,(
% 0.12/0.51    ~e22=op2(e22,e23)),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f749,f185])).
% 0.12/0.51  fof(f743,plain,(
% 0.12/0.51    ~op2(e20,e23)=e22),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f749,f182])).
% 0.12/0.51  fof(f746,plain,(
% 0.12/0.51    op2(e21,e20)=e21|op2(e21,e21)=e21|op2(e21,e22)=e21|e22=e21),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f749,f94])).
% 0.12/0.51  fof(f749,plain,(
% 0.12/0.51    e22=op2(e21,e23)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f735,f737])).
% 0.12/0.51  fof(f751,plain,(
% 0.12/0.51    h1(e11)=op2(e21,op2(e20,e20))),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f735,f292])).
% 0.12/0.51  fof(f759,plain,(
% 0.12/0.51    op2(e20,e21)=e23|h1(e11)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f764,f99])).
% 0.12/0.51  fof(f764,plain,(
% 0.12/0.51    h1(e11)=op2(e21,e21)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f735,f751])).
% 0.12/0.51  fof(f765,plain,(
% 0.12/0.51    h1(e12)=op2(op2(e21,op2(e20,e20)),e20)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f735,f293])).
% 0.12/0.51  fof(f766,plain,(
% 0.12/0.51    h1(e12)=op2(op2(e21,e21),e20)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f735,f765])).
% 0.12/0.51  fof(f767,plain,(
% 0.12/0.51    h1(e12)=op2(h1(e11),e20)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f764,f766])).
% 0.12/0.51  fof(f774,plain,(
% 0.12/0.51    ~h3(e10)=e23|op2(e22,e23)=e22),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f299,f276])).
% 0.12/0.51  fof(f783,plain,(
% 0.12/0.51    op2(e20,e22)=e23|op2(e21,e22)=e23|h3(e10)=e23|op2(e23,e22)=e23),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f299,f107])).
% 0.12/0.51  fof(f789,plain,(
% 0.12/0.51    op2(e20,e22)=e20|op2(e21,e22)=e20|h3(e10)=e20|op2(e23,e22)=e20),
% 0.12/0.51    inference(backward_demodulation,[status(thm)],[f299,f101])).
% 0.12/0.51  fof(f797,plain,(
% 0.12/0.51    h4(e10)=e20),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f303])).
% 0.12/0.51  fof(f798,plain,(
% 0.12/0.51    h4(e11)=op2(e20,op2(e23,e23))),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f304])).
% 0.12/0.51  fof(f799,plain,(
% 0.12/0.51    h4(e11)=op2(e20,e20)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f798])).
% 0.12/0.51  fof(f800,plain,(
% 0.12/0.51    h4(e11)=e21),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f735,f799])).
% 0.12/0.51  fof(f801,plain,(
% 0.12/0.51    h4(e12)=op2(op2(e20,op2(e23,e23)),e23)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f305])).
% 0.12/0.51  fof(f802,plain,(
% 0.12/0.51    h4(e12)=op2(op2(e20,e20),e23)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f287,f801])).
% 0.12/0.51  fof(f803,plain,(
% 0.12/0.51    h4(e12)=op2(e21,e23)),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f735,f802])).
% 0.12/0.51  fof(f804,plain,(
% 0.12/0.51    h4(e12)=e22),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f749,f803])).
% 0.12/0.51  fof(f1201,plain,(
% 0.12/0.51    ~h4(e11)=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f682,f335])).
% 0.12/0.51  fof(f1202,plain,(
% 0.12/0.51    ~e21=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f800,f1201])).
% 0.12/0.51  fof(f1203,plain,(
% 0.12/0.51    ~e21=op2(e20,h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f797,f1202])).
% 0.12/0.51  fof(f1204,plain,(
% 0.12/0.51    ~e21=op2(e20,e20)|~h4(op1(e10,e11))=op2(h4(e10),h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f797,f1203])).
% 0.12/0.51  fof(f1205,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(h4(e10),h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f735,f1204])).
% 0.12/0.51  fof(f1206,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f797,f1205])).
% 0.12/0.51  fof(f1207,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f800,f1206])).
% 0.12/0.51  fof(f1208,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f797,f1207])).
% 0.12/0.51  fof(f1209,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f804,f1208])).
% 0.12/0.51  fof(f1210,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f797,f1209])).
% 0.12/0.51  fof(f1211,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f302,f1210])).
% 0.12/0.51  fof(f1212,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f800,f1211])).
% 0.12/0.51  fof(f1213,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f797,f1212])).
% 0.12/0.51  fof(f1214,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=op2(e21,h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f800,f1213])).
% 0.12/0.51  fof(f1215,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=op2(e21,e21)|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f800,f1214])).
% 0.12/0.51  fof(f1216,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.51    inference(forward_demodulation,[status(thm)],[f764,f1215])).
% 0.12/0.51  fof(f1217,plain,(
% 0.12/0.51    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f800,f1216])).
% 0.12/0.52  fof(f1218,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1217])).
% 0.12/0.52  fof(f1219,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(e12)=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f696,f1218])).
% 0.12/0.52  fof(f1220,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1219])).
% 0.12/0.52  fof(f1221,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=op2(e21,h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f800,f1220])).
% 0.12/0.52  fof(f1222,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=op2(e21,e23)|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1221])).
% 0.12/0.52  fof(f1223,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f749,f1222])).
% 0.12/0.52  fof(f1224,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1223])).
% 0.12/0.52  fof(f1225,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f797,f1224])).
% 0.12/0.52  fof(f1226,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1225])).
% 0.12/0.52  fof(f1227,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f800,f1226])).
% 0.12/0.52  fof(f1228,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=op2(e22,h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1227])).
% 0.12/0.52  fof(f1229,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=op2(e22,e22)|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1228])).
% 0.12/0.52  fof(f1230,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f299,f1229])).
% 0.12/0.52  fof(f1231,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1230])).
% 0.12/0.52  fof(f1232,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1231])).
% 0.12/0.52  fof(f1233,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1232])).
% 0.12/0.52  fof(f1234,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f797,f1233])).
% 0.12/0.52  fof(f1235,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1234])).
% 0.12/0.52  fof(f1236,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f800,f1235])).
% 0.12/0.52  fof(f1237,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1236])).
% 0.12/0.52  fof(f1238,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1237])).
% 0.12/0.52  fof(f1239,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~h4(e10)=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f284,f1238])).
% 0.12/0.52  fof(f1240,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e20=op2(h4(e13),h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f797,f1239])).
% 0.12/0.52  fof(f1241,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e20=op2(e23,h4(e13))|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1240])).
% 0.12/0.52  fof(f1242,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e20=op2(e23,e23)|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1241])).
% 0.12/0.52  fof(f1243,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e20=e20|sP11_prd|sP12_prd|sP13_prd|~h4(e13)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f287,f1242])).
% 0.12/0.52  fof(f1244,plain,(
% 0.12/0.52    ~e21=e21|~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=e22|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e20=e20|sP11_prd|sP12_prd|sP13_prd|~e23=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1243])).
% 0.12/0.52  fof(f1245,plain,(
% 0.12/0.52    ~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd|sP12_prd|sP13_prd),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f1244])).
% 0.12/0.52  fof(f1296,plain,(
% 0.12/0.52    ~sP11_prd|~e20=e20),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f797,f407])).
% 0.12/0.52  fof(f1297,plain,(
% 0.12/0.52    ~h4(op1(e10,e11))=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP12_prd|sP13_prd),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1245,f1298])).
% 0.12/0.52  fof(f1298,plain,(
% 0.12/0.52    ~sP11_prd),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f1296])).
% 0.12/0.52  fof(f1303,plain,(
% 0.12/0.52    ~sP12_prd|~e21=e21),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f800,f414])).
% 0.12/0.52  fof(f1304,plain,(
% 0.12/0.52    ~sP12_prd),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f1303])).
% 0.12/0.52  fof(f1310,plain,(
% 0.12/0.52    ~sP13_prd|~e22=e22),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f421])).
% 0.12/0.52  fof(f1311,plain,(
% 0.12/0.52    ~sP13_prd),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f1310])).
% 0.12/0.52  fof(f1399,plain,(
% 0.12/0.52    ~e13=op1(e13,e12)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1404,f159])).
% 0.12/0.52  fof(f1402,plain,(
% 0.12/0.52    ~op1(e11,e10)=e13),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1404,f120])).
% 0.12/0.52  fof(f1404,plain,(
% 0.12/0.52    op1(e13,e10)=e13),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f646])).
% 0.12/0.52  fof(f1407,plain,(
% 0.12/0.52    op1(e10,e12)=e10|op1(e11,e12)=e10|op1(e12,e12)=e10),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f53,f648])).
% 0.12/0.52  fof(f1408,plain,(
% 0.12/0.52    op1(e13,e12)=e11|op1(e13,e12)=e12|op1(e13,e12)=e13),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f34,f648])).
% 0.12/0.52  fof(f1416,plain,(
% 0.12/0.52    op1(e10,e13)=e11|op1(e10,e13)=e12|op1(e10,e13)=e13),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f23,f653])).
% 0.12/0.52  fof(f1421,plain,(
% 0.12/0.52    op1(e10,e13)=e11|e12=e11|op1(e12,e13)=e11|e10=e11),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f696,f658])).
% 0.12/0.52  fof(f1422,plain,(
% 0.12/0.52    op1(e10,e13)=e11|op1(e12,e13)=e11|e10=e11),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1421,f215])).
% 0.12/0.52  fof(f1429,plain,(
% 0.12/0.52    ~e10=op1(e10,e12)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1437,f143])).
% 0.12/0.52  fof(f1431,plain,(
% 0.12/0.52    ~e10=op1(e12,e11)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1437,f123])).
% 0.12/0.52  fof(f1432,plain,(
% 0.12/0.52    ~e10=op1(e11,e11)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1437,f122])).
% 0.12/0.52  fof(f1434,plain,(
% 0.12/0.52    e10=e12|op1(e11,e11)=e12|op1(e12,e11)=e12|op1(e13,e11)=e12),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1437,f49])).
% 0.12/0.52  fof(f1437,plain,(
% 0.12/0.52    op1(e10,e11)=e10),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f666])).
% 0.12/0.52  fof(f1438,plain,(
% 0.12/0.52    op1(e12,e13)=e11|e10=e11),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1422,f667])).
% 0.12/0.52  fof(f1450,plain,(
% 0.12/0.52    e11=e12|op1(e11,e10)=e12|op1(e12,e10)=e12|e13=e12),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1404,f675])).
% 0.12/0.52  fof(f1451,plain,(
% 0.12/0.52    op1(e11,e10)=e12|op1(e12,e10)=e12|e13=e12),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1450,f215])).
% 0.12/0.52  fof(f1452,plain,(
% 0.12/0.52    e11=e12|e10=e12|op1(e10,e12)=e12|op1(e10,e13)=e12),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1437,f676])).
% 0.12/0.52  fof(f1453,plain,(
% 0.12/0.52    e10=e12|op1(e10,e12)=e12|op1(e10,e13)=e12),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1452,f215])).
% 0.12/0.52  fof(f1457,plain,(
% 0.12/0.52    op1(e11,e11)=e10|op1(e11,e11)=e11|op1(e11,e11)=e12),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f25,f1458])).
% 0.12/0.52  fof(f1458,plain,(
% 0.12/0.52    ~op1(e11,e11)=e13),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f685,f215])).
% 0.12/0.52  fof(f1462,plain,(
% 0.12/0.52    op1(e12,e10)=e12|e13=e12),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1451,f688])).
% 0.12/0.52  fof(f1466,plain,(
% 0.12/0.52    e10=e12|op1(e10,e12)=e12),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1453,f690])).
% 0.12/0.52  fof(f1467,plain,(
% 0.12/0.52    op1(e11,e10)=e13|op1(e11,e12)=e13|e12=e13),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f691,f1458])).
% 0.12/0.52  fof(f1469,plain,(
% 0.12/0.52    op1(e11,e10)=e10|op1(e11,e11)=e10|op1(e11,e12)=e10),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f694,f213])).
% 0.12/0.52  fof(f1476,plain,(
% 0.12/0.52    ~e23=op2(e23,e22)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1481,f207])).
% 0.12/0.52  fof(f1477,plain,(
% 0.12/0.52    ~e23=op2(e23,e21)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1481,f206])).
% 0.12/0.52  fof(f1481,plain,(
% 0.12/0.52    op2(e23,e20)=e23),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f699])).
% 0.12/0.52  fof(f1482,plain,(
% 0.12/0.52    e21=e20|op2(e21,e21)=e21|op2(e22,e22)=e22|e20=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f735,f700])).
% 0.12/0.52  fof(f1483,plain,(
% 0.12/0.52    e21=e20|h1(e11)=e21|op2(e22,e22)=e22|e20=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f764,f1482])).
% 0.12/0.52  fof(f1484,plain,(
% 0.12/0.52    e21=e20|h1(e11)=e21|h3(e10)=e22|e20=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f299,f1483])).
% 0.12/0.52  fof(f1485,plain,(
% 0.12/0.52    h1(e11)=e21|h3(e10)=e22|e20=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1484,f218])).
% 0.12/0.52  fof(f1486,plain,(
% 0.12/0.52    op2(e23,e22)=e21|op2(e23,e22)=e22|op2(e23,e22)=e23),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f82,f701])).
% 0.12/0.52  fof(f1492,plain,(
% 0.12/0.52    op2(e20,e23)=e21|op2(e20,e23)=e22|op2(e20,e23)=e23),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f71,f706])).
% 0.12/0.52  fof(f1495,plain,(
% 0.12/0.52    e23=e22|op2(e23,e21)=e22|op2(e23,e22)=e22|e20=e22),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1481,f710])).
% 0.12/0.52  fof(f1496,plain,(
% 0.12/0.52    op2(e23,e21)=e22|op2(e23,e22)=e22|e20=e22),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1495,f223])).
% 0.12/0.52  fof(f1497,plain,(
% 0.12/0.52    op2(e20,e23)=e21|e22=e21|op2(e22,e23)=e21|e20=e21),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f749,f711])).
% 0.12/0.52  fof(f1498,plain,(
% 0.12/0.52    op2(e20,e23)=e21|op2(e22,e23)=e21|e20=e21),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1497,f221])).
% 0.12/0.52  fof(f1505,plain,(
% 0.12/0.52    ~e20=op2(e20,e22)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1509,f191])).
% 0.12/0.52  fof(f1509,plain,(
% 0.12/0.52    op2(e20,e21)=e20),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f719])).
% 0.12/0.52  fof(f1510,plain,(
% 0.12/0.52    op2(e22,e23)=e21|e20=e21),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1498,f720])).
% 0.12/0.52  fof(f1519,plain,(
% 0.12/0.52    e21=e22|op2(e21,e20)=e22|op2(e22,e20)=e22|e23=e22),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1481,f728])).
% 0.12/0.52  fof(f1520,plain,(
% 0.12/0.52    op2(e21,e20)=e22|op2(e22,e20)=e22|e23=e22),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1519,f221])).
% 0.12/0.52  fof(f1521,plain,(
% 0.12/0.52    e21=e22|e20=e22|op2(e20,e22)=e22|op2(e20,e23)=e22),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1509,f729])).
% 0.12/0.52  fof(f1522,plain,(
% 0.12/0.52    e20=e22|op2(e20,e22)=e22|op2(e20,e23)=e22),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1521,f221])).
% 0.12/0.52  fof(f1523,plain,(
% 0.12/0.52    e21=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|e23=e20),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1481,f732])).
% 0.12/0.52  fof(f1524,plain,(
% 0.12/0.52    op2(e21,e20)=e20|op2(e22,e20)=e20|e23=e20),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1523,f218])).
% 0.12/0.52  fof(f1526,plain,(
% 0.12/0.52    ~h1(e11)=e23|e22=e21),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f764,f738])).
% 0.12/0.52  fof(f1527,plain,(
% 0.12/0.52    ~h1(e11)=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1526,f221])).
% 0.12/0.52  fof(f1533,plain,(
% 0.12/0.52    op2(e22,e20)=e22|e23=e22),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1520,f741])).
% 0.12/0.52  fof(f1535,plain,(
% 0.12/0.52    e20=e22|op2(e20,e22)=e22),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1522,f743])).
% 0.12/0.52  fof(f1538,plain,(
% 0.12/0.52    op2(e21,e20)=e21|h1(e11)=e21|op2(e21,e22)=e21|e22=e21),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f764,f746])).
% 0.12/0.52  fof(f1539,plain,(
% 0.12/0.52    h1(e11)=e21|op2(e21,e22)=e21|e22=e21),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1538,f725])).
% 0.12/0.52  fof(f1548,plain,(
% 0.12/0.52    e20=e23|h1(e11)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1509,f759])).
% 0.12/0.52  fof(f1549,plain,(
% 0.12/0.52    h1(e11)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1548,f220])).
% 0.12/0.52  fof(f1558,plain,(
% 0.12/0.52    ~h3(e10)=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f774,f742])).
% 0.12/0.52  fof(f1559,plain,(
% 0.12/0.52    op2(e20,e22)=e23|op2(e21,e22)=e23|op2(e23,e22)=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f783,f1558])).
% 0.12/0.52  fof(f1565,plain,(
% 0.12/0.52    op2(e20,e22)=e20|op2(e21,e22)=e20|h3(e10)=e20),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f789,f701])).
% 0.12/0.52  fof(f1605,plain,(
% 0.12/0.52    ~h4(e10)=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP12_prd|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1437,f1297])).
% 0.12/0.52  fof(f1606,plain,(
% 0.12/0.52    ~e20=op2(e20,e21)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP12_prd|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f797,f1605])).
% 0.12/0.52  fof(f1607,plain,(
% 0.12/0.52    ~e20=e20|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP12_prd|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1509,f1606])).
% 0.12/0.52  fof(f1608,plain,(
% 0.12/0.52    ~e20=e20|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(e13)=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP12_prd|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1404,f1607])).
% 0.12/0.52  fof(f1609,plain,(
% 0.12/0.52    ~e20=e20|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP12_prd|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1608])).
% 0.12/0.52  fof(f1610,plain,(
% 0.12/0.52    ~e20=e20|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~e23=e23|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP12_prd|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1481,f1609])).
% 0.12/0.52  fof(f1611,plain,(
% 0.12/0.52    ~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP12_prd|sP13_prd),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f1610])).
% 0.12/0.52  fof(f1612,plain,(
% 0.12/0.52    ~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1611,f1304])).
% 0.12/0.52  fof(f1618,plain,(
% 0.12/0.52    op1(e11,e12)=e13|e12=e13),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1467,f1402])).
% 0.12/0.52  fof(f1619,plain,(
% 0.12/0.52    op1(e13,e12)=e11|op1(e13,e12)=e12),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1408,f1399])).
% 0.12/0.52  fof(f1622,plain,(
% 0.12/0.52    op1(e10,e13)=e12|op1(e10,e13)=e13),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1416,f667])).
% 0.12/0.52  fof(f1625,plain,(
% 0.12/0.52    op1(e11,e12)=e10|op1(e12,e12)=e10),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1407,f1429])).
% 0.12/0.52  fof(f1628,plain,(
% 0.12/0.52    op1(e12,e11)=e11|op1(e12,e11)=e12|op1(e12,e11)=e13),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f29,f1431])).
% 0.12/0.52  fof(f1629,plain,(
% 0.12/0.52    op1(e11,e10)=e10|op1(e11,e12)=e10),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1469,f1432])).
% 0.12/0.52  fof(f1631,plain,(
% 0.12/0.52    op1(e11,e11)=e12|op1(e12,e11)=e12|op1(e13,e11)=e12),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1434,f213])).
% 0.12/0.52  fof(f1634,plain,(
% 0.12/0.52    ~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1648,f1612])).
% 0.12/0.52  fof(f1645,plain,(
% 0.12/0.52    ~op1(e12,e11)=e11),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1648,f156])).
% 0.12/0.52  fof(f1648,plain,(
% 0.12/0.52    op1(e12,e13)=e11),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1438,f212])).
% 0.12/0.52  fof(f1652,plain,(
% 0.12/0.52    op1(e11,e11)=e11|op1(e11,e11)=e12),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1457,f1432])).
% 0.12/0.52  fof(f1662,plain,(
% 0.12/0.52    ~e12=op1(e12,e11)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1664,f152])).
% 0.12/0.52  fof(f1664,plain,(
% 0.12/0.52    op1(e12,e10)=e12),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1462,f217])).
% 0.12/0.52  fof(f1673,plain,(
% 0.12/0.52    ~e12=op1(e13,e12)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1676,f130])).
% 0.12/0.52  fof(f1676,plain,(
% 0.12/0.52    op1(e10,e12)=e12),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1466,f213])).
% 0.12/0.52  fof(f1679,plain,(
% 0.12/0.52    op2(e20,e22)=e23|op2(e21,e22)=e23),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1559,f1476])).
% 0.12/0.52  fof(f1681,plain,(
% 0.12/0.52    h1(e11)=e23|op2(e22,e21)=e23),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1549,f1477])).
% 0.12/0.52  fof(f1684,plain,(
% 0.12/0.52    op2(e23,e22)=e21|op2(e23,e22)=e22),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1486,f1476])).
% 0.12/0.52  fof(f1687,plain,(
% 0.12/0.52    op2(e20,e23)=e22|op2(e20,e23)=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1492,f720])).
% 0.12/0.52  fof(f1690,plain,(
% 0.12/0.52    op2(e21,e22)=e20|h3(e10)=e20),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1565,f1505])).
% 0.12/0.52  fof(f1704,plain,(
% 0.12/0.52    op2(e22,e23)=e21),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1510,f218])).
% 0.12/0.52  fof(f1714,plain,(
% 0.12/0.52    op2(e21,e20)=e20|e22=e20|e23=e20),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1721,f1524])).
% 0.12/0.52  fof(f1721,plain,(
% 0.12/0.52    op2(e22,e20)=e22),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1533,f223])).
% 0.12/0.52  fof(f1730,plain,(
% 0.12/0.52    ~e22=op2(e23,e22)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1732,f178])).
% 0.12/0.52  fof(f1732,plain,(
% 0.12/0.52    op2(e20,e22)=e22),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1535,f219])).
% 0.12/0.52  fof(f1749,plain,(
% 0.12/0.52    op1(e11,e12)=e13),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1618,f217])).
% 0.12/0.52  fof(f1750,plain,(
% 0.12/0.52    e13=e10|op1(e12,e12)=e10),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1749,f1625])).
% 0.12/0.52  fof(f1758,plain,(
% 0.12/0.52    op1(e12,e12)=e10),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1750,f214])).
% 0.12/0.52  fof(f1760,plain,(
% 0.12/0.52    op1(e11,e10)=e10|e13=e10),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1749,f1629])).
% 0.12/0.52  fof(f1768,plain,(
% 0.12/0.52    op1(e11,e10)=e10),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1760,f214])).
% 0.12/0.52  fof(f1769,plain,(
% 0.12/0.52    ~h4(e12)=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1676,f1634])).
% 0.12/0.52  fof(f1770,plain,(
% 0.12/0.52    ~e22=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1769])).
% 0.12/0.52  fof(f1771,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1732,f1770])).
% 0.12/0.52  fof(f1772,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~h4(e10)=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1768,f1771])).
% 0.12/0.52  fof(f1773,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f797,f1772])).
% 0.12/0.52  fof(f1774,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~h4(e13)=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1749,f1773])).
% 0.12/0.52  fof(f1775,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1774])).
% 0.12/0.52  fof(f1776,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~h4(e12)=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1664,f1775])).
% 0.12/0.52  fof(f1777,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~e22=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1776])).
% 0.12/0.52  fof(f1778,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~e22=e22|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1721,f1777])).
% 0.12/0.52  fof(f1779,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~e22=e22|~h4(op1(e12,e11))=op2(e22,e21)|~h4(e10)=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1758,f1778])).
% 0.12/0.52  fof(f1780,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~e22=e22|~h4(op1(e12,e11))=op2(e22,e21)|~e20=h3(e10)|~h4(e11)=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f797,f1779])).
% 0.12/0.52  fof(f1781,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~e22=e22|~h4(op1(e12,e11))=op2(e22,e21)|~e20=h3(e10)|~e21=op2(e22,e23)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f800,f1780])).
% 0.12/0.52  fof(f1782,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~e22=e22|~h4(op1(e12,e11))=op2(e22,e21)|~e20=h3(e10)|~e21=e21|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1704,f1781])).
% 0.12/0.52  fof(f1783,plain,(
% 0.12/0.52    ~e22=e22|~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~h4(op1(e12,e11))=op2(e22,e21)|~e20=h3(e10)|~e21=e21|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(duplicate_literals_removal,[status(thm)],[f1782])).
% 0.12/0.52  fof(f1784,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~h4(op1(e12,e11))=op2(e22,e21)|~e20=h3(e10)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP13_prd),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f1783])).
% 0.12/0.52  fof(f1785,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=op2(e21,e22)|~h4(op1(e12,e11))=op2(e22,e21)|~e20=h3(e10)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1784,f1311])).
% 0.12/0.52  fof(f1824,plain,(
% 0.12/0.52    op1(e12,e11)=e12|op1(e12,e11)=e13),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1628,f1645])).
% 0.12/0.52  fof(f1833,plain,(
% 0.12/0.52    op1(e11,e11)=e12|op1(e13,e11)=e12),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1631,f1662])).
% 0.12/0.52  fof(f1835,plain,(
% 0.12/0.52    op1(e13,e12)=e11),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1619,f1673])).
% 0.12/0.52  fof(f1839,plain,(
% 0.12/0.52    e22=e23|op2(e21,e22)=e23),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1732,f1679])).
% 0.12/0.52  fof(f1840,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~h4(op1(e12,e11))=op2(e22,e21)|~e20=h3(e10)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1852,f1785])).
% 0.12/0.52  fof(f1846,plain,(
% 0.12/0.52    h1(e11)=e21|e23=e21|e22=e21),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1852,f1539])).
% 0.12/0.52  fof(f1852,plain,(
% 0.12/0.52    op2(e21,e22)=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1839,f223])).
% 0.12/0.52  fof(f1862,plain,(
% 0.12/0.52    op2(e22,e21)=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1681,f1527])).
% 0.12/0.52  fof(f1863,plain,(
% 0.12/0.52    e23=e20|h3(e10)=e20),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1852,f1690])).
% 0.12/0.52  fof(f1869,plain,(
% 0.12/0.52    h1(e11)=e21|e20=e22|e20=e23),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1878,f1485])).
% 0.12/0.52  fof(f1878,plain,(
% 0.12/0.52    h3(e10)=e20),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1863,f220])).
% 0.12/0.52  fof(f1887,plain,(
% 0.12/0.52    op2(e21,e20)=e20|e23=e20),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1714,f219])).
% 0.12/0.52  fof(f1894,plain,(
% 0.12/0.52    op2(e23,e22)=e21),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1684,f1730])).
% 0.12/0.52  fof(f1895,plain,(
% 0.12/0.52    op2(e23,e21)=e22|e20=e22),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1496,f1730])).
% 0.12/0.52  fof(f1917,plain,(
% 0.12/0.52    op1(e12,e11)=e13),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1824,f1662])).
% 0.12/0.52  fof(f1925,plain,(
% 0.12/0.52    op1(e13,e11)=e12),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1833,f687])).
% 0.12/0.52  fof(f1930,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~h4(e13)=op2(e22,e21)|~e20=h3(e10)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1917,f1840])).
% 0.12/0.52  fof(f1931,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~e23=op2(e22,e21)|~e20=h3(e10)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f1930])).
% 0.12/0.52  fof(f1932,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~e23=e23|~e20=h3(e10)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1862,f1931])).
% 0.12/0.52  fof(f1933,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~e23=e23|~e20=e20|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1878,f1932])).
% 0.12/0.52  fof(f1934,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~e23=e23|~e20=e20|~h4(e12)=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1925,f1933])).
% 0.12/0.52  fof(f1935,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~e23=e23|~e20=e20|~e22=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f804,f1934])).
% 0.12/0.52  fof(f1936,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~e23=e23|~e20=e20|~e22=op2(e23,e21)|~h4(e11)=op2(e23,e22)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f1835,f1935])).
% 0.12/0.52  fof(f1937,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~e23=e23|~e20=e20|~e22=op2(e23,e21)|~e21=op2(e23,e22)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f800,f1936])).
% 0.12/0.52  fof(f1938,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e23=e23|~e20=e20|~e22=op2(e23,e21)|~e21=op2(e23,e22)),
% 0.12/0.52    inference(duplicate_literals_removal,[status(thm)],[f1937])).
% 0.12/0.52  fof(f1939,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e22=op2(e23,e21)|~e21=op2(e23,e22)),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f1938])).
% 0.12/0.52  fof(f1943,plain,(
% 0.12/0.52    h1(e11)=e21|e22=e21),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1846,f222])).
% 0.12/0.52  fof(f1983,plain,(
% 0.12/0.52    h1(e11)=e21|e20=e23),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1869,f219])).
% 0.12/0.52  fof(f1995,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e22=op2(e23,e21)|~e21=e21),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f1894,f1939])).
% 0.12/0.52  fof(f2006,plain,(
% 0.12/0.52    op2(e23,e21)=e22),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f1895,f219])).
% 0.12/0.52  fof(f2051,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|~e22=e22|~e21=e21),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f2006,f1995])).
% 0.12/0.52  fof(f2052,plain,(
% 0.12/0.52    ~h4(op1(e10,e13))=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f2051])).
% 0.12/0.52  fof(f2082,plain,(
% 0.12/0.52    ~h4(e13)=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|op1(e10,e13)=e12),
% 0.12/0.52    inference(paramodulation,[status(thm)],[f1622,f2052])).
% 0.12/0.52  fof(f2087,plain,(
% 0.12/0.52    ~e23=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)|op1(e10,e13)=e12),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f302,f2082])).
% 0.12/0.52  fof(f2088,plain,(
% 0.12/0.52    ~e23=op2(e20,e23)|~e20=op2(e21,e20)|~h4(op1(e11,e11))=h1(e11)),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f2087,f690])).
% 0.12/0.52  fof(f2092,plain,(
% 0.12/0.52    op1(e11,e11)=e11),
% 0.12/0.52    inference(resolution,[status(thm)],[f1652,f687])).
% 0.12/0.52  fof(f2105,plain,(
% 0.12/0.52    ~e23=op2(e20,e23)|~e20=op2(e21,e20)|~h4(e11)=h1(e11)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f2092,f2088])).
% 0.12/0.52  fof(f2114,plain,(
% 0.12/0.52    ~e23=op2(e20,e23)|~e20=op2(e21,e20)|~e21=h1(e11)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f800,f2105])).
% 0.12/0.52  fof(f2155,plain,(
% 0.12/0.52    h1(e12)=op2(e21,e20)|e22=e21),
% 0.12/0.52    inference(paramodulation,[status(thm)],[f1943,f767])).
% 0.12/0.52  fof(f2171,plain,(
% 0.12/0.52    h1(e12)=e20|e23=e20),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f2181,f1887])).
% 0.12/0.52  fof(f2177,plain,(
% 0.12/0.52    ~e23=op2(e20,e23)|~e20=h1(e12)|~e21=h1(e11)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f2181,f2114])).
% 0.12/0.52  fof(f2181,plain,(
% 0.12/0.52    h1(e12)=op2(e21,e20)),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f2155,f221])).
% 0.12/0.52  fof(f2204,plain,(
% 0.12/0.52    h1(e12)=e20),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f2171,f220])).
% 0.12/0.52  fof(f2210,plain,(
% 0.12/0.52    ~e23=op2(e20,e23)|~e20=e20|~e21=h1(e11)),
% 0.12/0.52    inference(forward_demodulation,[status(thm)],[f2204,f2177])).
% 0.12/0.52  fof(f2211,plain,(
% 0.12/0.52    ~e23=op2(e20,e23)|~e21=h1(e11)),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f2210])).
% 0.12/0.52  fof(f2290,plain,(
% 0.12/0.52    op2(e20,e23)=e23),
% 0.12/0.52    inference(resolution,[status(thm)],[f743,f1687])).
% 0.12/0.52  fof(f2298,plain,(
% 0.12/0.52    ~e23=e23|~e21=h1(e11)),
% 0.12/0.52    inference(backward_demodulation,[status(thm)],[f2290,f2211])).
% 0.12/0.52  fof(f2300,plain,(
% 0.12/0.52    e20=e23),
% 0.12/0.52    inference(backward_subsumption_resolution,[status(thm)],[f1983,f2304])).
% 0.12/0.52  fof(f2304,plain,(
% 0.12/0.52    ~e21=h1(e11)),
% 0.12/0.52    inference(trivial_equality_resolution,[status(thm)],[f2298])).
% 0.12/0.52  fof(f2305,plain,(
% 0.12/0.52    $false),
% 0.12/0.52    inference(forward_subsumption_resolution,[status(thm)],[f2300,f220])).
% 0.12/0.52  % SZS output end CNFRefutation for theBenchmark.p
% 0.73/0.54  % Elapsed time: 0.169387 seconds
% 0.73/0.54  % CPU time: 1.018607 seconds
% 0.73/0.54  % Total memory used: 146.120 MB
% 0.73/0.54  % Net memory used: 144.587 MB
%------------------------------------------------------------------------------