%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG115+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:49:38 AM UTC 2026
% Result : Theorem 0.28s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG115+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n016.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 13:01:23 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.28/0.53 % Drodi V4.1.1
% 0.28/0.67 % Refutation found
% 0.28/0.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.28/0.67 % SZS output start CNFRefutation for theBenchmark
% 0.28/0.67 fof(f1,axiom,(
% 0.28/0.67 ( ( 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.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f2,axiom,(
% 0.28/0.67 ( ( 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.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f3,axiom,(
% 0.28/0.67 ( ( 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.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f4,axiom,(
% 0.28/0.67 ( ( 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.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f5,axiom,(
% 0.28/0.67 ( 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.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f6,axiom,(
% 0.28/0.67 ( 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.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f7,axiom,(
% 0.28/0.67 ( e10 != e11& e10 != e12& e10 != e13& e11 != e12& e11 != e13& e12 != e13 ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f8,axiom,(
% 0.28/0.67 ( e20 != e21& e20 != e22& e20 != e23& e21 != e22& e21 != e23& e22 != e23 ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f10,axiom,(
% 0.28/0.67 ( ( op1(e10,e10) = e10| op1(e11,e11) = e10| op1(e12,e12) = e10| op1(e13,e13) = e10 )& ( op1(e10,e10) = e11| op1(e11,e11) = e11| op1(e12,e12) = e11| op1(e13,e13) = e11 )& ( op1(e10,e10) = e12| op1(e11,e11) = e12| op1(e12,e12) = e12| op1(e13,e13) = e12 )& ( op1(e10,e10) = e13| op1(e11,e11) = e13| op1(e12,e12) = e13| op1(e13,e13) = e13 )& ( ( op1(e10,op1(e10,e10)) != e10& op1(e10,op1(e10,e11)) != e11& op1(e10,op1(e10,e12)) != e12& op1(e10,op1(e10,e13)) != e13 )| ( op1(e11,op1(e11,e10)) != e10& op1(e11,op1(e11,e11)) != e11& op1(e11,op1(e11,e12)) != e12& op1(e11,op1(e11,e13)) != e13 )| ( op1(e12,op1(e12,e10)) != e10& op1(e12,op1(e12,e11)) != e11& op1(e12,op1(e12,e12)) != e12& op1(e12,op1(e12,e13)) != e13 )| ( op1(e13,op1(e13,e10)) != e10& op1(e13,op1(e13,e11)) != e11& op1(e13,op1(e13,e12)) != e12& op1(e13,op1(e13,e13)) != e13 ) )& ( ( op1(e10,e10) = e10& op1(e10,e10) = e10& op1(e10,e10) = e10& op1(e10,e10) = e10 )| ( op1(e10,e10) = e10& op1(e10,e10) = e10& op1(e11,e10) = e10& op1(e10,e11) = e10 )| ( op1(e10,e10) = e10& op1(e10,e10) = e10& op1(e12,e10) = e10& op1(e10,e12) = e10 )| ( op1(e10,e10) = e10& op1(e10,e10) = e10& op1(e13,e10) = e10& op1(e10,e13) = e10 )| ( op1(e10,e11) = e10& op1(e11,e10) = e10& op1(e10,e11) = e11& op1(e11,e10) = e11 )| ( op1(e10,e11) = e10& op1(e11,e10) = e10& op1(e11,e11) = e11& op1(e11,e11) = e11 )| ( op1(e10,e11) = e10& op1(e11,e10) = e10& op1(e12,e11) = e11& op1(e11,e12) = e11 )| ( op1(e10,e11) = e10& op1(e11,e10) = e10& op1(e13,e11) = e11& op1(e11,e13) = e11 )| ( op1(e10,e12) = e10& op1(e12,e10) = e10& op1(e10,e12) = e12& op1(e12,e10) = e12 )| ( op1(e10,e12) = e10& op1(e12,e10) = e10& op1(e11,e12) = e12& op1(e12,e11) = e12 )| ( op1(e10,e12) = e10& op1(e12,e10) = e10& op1(e12,e12) = e12& op1(e12,e12) = e12 )| ( op1(e10,e12) = e10& op1(e12,e10) = e10& op1(e13,e12) = e12& op1(e12,e13) = e12 )| ( op1(e10,e13) = e10& op1(e13,e10) = e10& op1(e10,e13) = e13& op1(e13,e10) = e13 )| ( op1(e10,e13) = e10& op1(e13,e10) = e10& op1(e11,e13) = e13& op1(e13,e11) = e13 )| ( op1(e10,e13) = e10& op1(e13,e10) = e10& op1(e12,e13) = e13& op1(e13,e12) = e13 )| ( op1(e10,e13) = e10& op1(e13,e10) = e10& op1(e13,e13) = e13& op1(e13,e13) = e13 )| ( op1(e11,e10) = e11& op1(e10,e11) = e11& op1(e10,e10) = e10& op1(e10,e10) = e10 )| ( op1(e11,e10) = e11& op1(e10,e11) = e11& op1(e11,e10) = e10& op1(e10,e11) = e10 )| ( op1(e11,e10) = e11& op1(e10,e11) = e11& op1(e12,e10) = e10& op1(e10,e12) = e10 )| ( op1(e11,e10) = e11& op1(e10,e11) = e11& op1(e13,e10) = e10& op1(e10,e13) = e10 )| ( op1(e11,e11) = e11& op1(e11,e11) = e11& op1(e10,e11) = e11& op1(e11,e10) = e11 )| ( op1(e11,e11) = e11& op1(e11,e11) = e11& op1(e11,e11) = e11& op1(e11,e11) = e11 )| ( op1(e11,e11) = e11& op1(e11,e11) = e11& op1(e12,e11) = e11& op1(e11,e12) = e11 )| ( op1(e11,e11) = e11& op1(e11,e11) = e11& op1(e13,e11) = e11& op1(e11,e13) = e11 )| ( op1(e11,e12) = e11& op1(e12,e11) = e11& op1(e10,e12) = e12& op1(e12,e10) = e12 )| ( op1(e11,e12) = e11& op1(e12,e11) = e11& op1(e11,e12) = e12& op1(e12,e11) = e12 )| ( op1(e11,e12) = e11& op1(e12,e11) = e11& op1(e12,e12) = e12& op1(e12,e12) = e12 )| ( op1(e11,e12) = e11& op1(e12,e11) = e11& op1(e13,e12) = e12& op1(e12,e13) = e12 )| ( op1(e11,e13) = e11& op1(e13,e11) = e11& op1(e10,e13) = e13& op1(e13,e10) = e13 )| ( op1(e11,e13) = e11& op1(e13,e11) = e11& op1(e11,e13) = e13& op1(e13,e11) = e13 )| ( op1(e11,e13) = e11& op1(e13,e11) = e11& op1(e12,e13) = e13& op1(e13,e12) = e13 )| ( op1(e11,e13) = e11& op1(e13,e11) = e11& op1(e13,e13) = e13& op1(e13,e13) = e13 )| ( op1(e12,e10) = e12& op1(e10,e12) = e12& op1(e10,e10) = e10& op1(e10,e10) = e10 )| ( op1(e12,e10) = e12& op1(e10,e12) = e12& op1(e11,e10) = e10& op1(e10,e11) = e10 )| ( op1(e12,e10) = e12& op1(e10,e12) = e12& op1(e12,e10) = e10& op1(e10,e12) = e10 )| ( op1(e12,e10) = e12& op1(e10,e12) = e12& op1(e13,e10) = e10& op1(e10,e13) = e10 )| ( op1(e12,e11) = e12& op1(e11,e12) = e12& op1(e10,e11) = e11& op1(e11,e10) = e11 )| ( op1(e12,e11) = e12& op1(e11,e12) = e12& op1(e11,e11) = e11& op1(e11,e11) = e11 )| ( op1(e12,e11) = e12& op1(e11,e12) = e12& op1(e12,e11) = e11& op1(e11,e12) = e11 )| ( op1(e12,e11) = e12& op1(e11,e12) = e12& op1(e13,e11) = e11& op1(e11,e13) = e11 )| ( op1(e12,e12) = e12& op1(e12,e12) = e12& op1(e10,e12) = e12& op1(e12,e10) = e12 )| ( op1(e12,e12) = e12& op1(e12,e12) = e12& op1(e11,e12) = e12& op1(e12,e11) = e12 )| ( op1(e12,e12) = e12& op1(e12,e12) = e12& op1(e12,e12) = e12& op1(e12,e12) = e12 )| ( op1(e12,e12) = e12& op1(e12,e12) = e12& op1(e13,e12) = e12& op1(e12,e13) = e12 )| ( op1(e12,e13) = e12& op1(e13,e12) = e12& op1(e10,e13) = e13& op1(e13,e10) = e13 )| ( op1(e12,e13) = e12& op1(e13,e12) = e12& op1(e11,e13) = e13& op1(e13,e11) = e13 )| ( op1(e12,e13) = e12& op1(e13,e12) = e12& op1(e12,e13) = e13& op1(e13,e12) = e13 )| ( op1(e12,e13) = e12& op1(e13,e12) = e12& op1(e13,e13) = e13& op1(e13,e13) = e13 )| ( op1(e13,e10) = e13& op1(e10,e13) = e13& op1(e10,e10) = e10& op1(e10,e10) = e10 )| ( op1(e13,e10) = e13& op1(e10,e13) = e13& op1(e11,e10) = e10& op1(e10,e11) = e10 )| ( op1(e13,e10) = e13& op1(e10,e13) = e13& op1(e12,e10) = e10& op1(e10,e12) = e10 )| ( op1(e13,e10) = e13& op1(e10,e13) = e13& op1(e13,e10) = e10& op1(e10,e13) = e10 )| ( op1(e13,e11) = e13& op1(e11,e13) = e13& op1(e10,e11) = e11& op1(e11,e10) = e11 )| ( op1(e13,e11) = e13& op1(e11,e13) = e13& op1(e11,e11) = e11& op1(e11,e11) = e11 )| ( op1(e13,e11) = e13& op1(e11,e13) = e13& op1(e12,e11) = e11& op1(e11,e12) = e11 )| ( op1(e13,e11) = e13& op1(e11,e13) = e13& op1(e13,e11) = e11& op1(e11,e13) = e11 )| ( op1(e13,e12) = e13& op1(e12,e13) = e13& op1(e10,e12) = e12& op1(e12,e10) = e12 )| ( op1(e13,e12) = e13& op1(e12,e13) = e13& op1(e11,e12) = e12& op1(e12,e11) = e12 )| ( op1(e13,e12) = e13& op1(e12,e13) = e13& op1(e12,e12) = e12& op1(e12,e12) = e12 )| ( op1(e13,e12) = e13& op1(e12,e13) = e13& op1(e13,e12) = e12& op1(e12,e13) = e12 )| ( op1(e13,e13) = e13& op1(e13,e13) = e13& op1(e10,e13) = e13& op1(e13,e10) = e13 )| ( op1(e13,e13) = e13& op1(e13,e13) = e13& op1(e11,e13) = e13& op1(e13,e11) = e13 )| ( op1(e13,e13) = e13& op1(e13,e13) = e13& op1(e12,e13) = e13& op1(e13,e12) = e13 )| ( op1(e13,e13) = e13& op1(e13,e13) = e13& op1(e13,e13) = e13& op1(e13,e13) = e13 ) ) ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f11,axiom,(
% 0.28/0.67 ( ( op2(e20,e20) = e20| op2(e21,e21) = e20| op2(e22,e22) = e20| op2(e23,e23) = e20 )& ( op2(e20,e20) = e21| op2(e21,e21) = e21| op2(e22,e22) = e21| op2(e23,e23) = e21 )& ( op2(e20,e20) = e22| op2(e21,e21) = e22| op2(e22,e22) = e22| op2(e23,e23) = e22 )& ( op2(e20,e20) = e23| op2(e21,e21) = e23| op2(e22,e22) = e23| op2(e23,e23) = e23 )& ( ( op2(e20,op2(e20,e20)) != e20& op2(e20,op2(e20,e21)) != e21& op2(e20,op2(e20,e22)) != e22& op2(e20,op2(e20,e23)) != e23 )| ( op2(e21,op2(e21,e20)) != e20& op2(e21,op2(e21,e21)) != e21& op2(e21,op2(e21,e22)) != e22& op2(e21,op2(e21,e23)) != e23 )| ( op2(e22,op2(e22,e20)) != e20& op2(e22,op2(e22,e21)) != e21& op2(e22,op2(e22,e22)) != e22& op2(e22,op2(e22,e23)) != e23 )| ( op2(e23,op2(e23,e20)) != e20& op2(e23,op2(e23,e21)) != e21& op2(e23,op2(e23,e22)) != e22& op2(e23,op2(e23,e23)) != e23 ) )& ( ( op2(e20,e20) = e20& op2(e20,e20) = e20& op2(e20,e20) = e20& op2(e20,e20) = e20 )| ( op2(e20,e20) = e20& op2(e20,e20) = e20& op2(e21,e20) = e20& op2(e20,e21) = e20 )| ( op2(e20,e20) = e20& op2(e20,e20) = e20& op2(e22,e20) = e20& op2(e20,e22) = e20 )| ( op2(e20,e20) = e20& op2(e20,e20) = e20& op2(e23,e20) = e20& op2(e20,e23) = e20 )| ( op2(e20,e21) = e20& op2(e21,e20) = e20& op2(e20,e21) = e21& op2(e21,e20) = e21 )| ( op2(e20,e21) = e20& op2(e21,e20) = e20& op2(e21,e21) = e21& op2(e21,e21) = e21 )| ( op2(e20,e21) = e20& op2(e21,e20) = e20& op2(e22,e21) = e21& op2(e21,e22) = e21 )| ( op2(e20,e21) = e20& op2(e21,e20) = e20& op2(e23,e21) = e21& op2(e21,e23) = e21 )| ( op2(e20,e22) = e20& op2(e22,e20) = e20& op2(e20,e22) = e22& op2(e22,e20) = e22 )| ( op2(e20,e22) = e20& op2(e22,e20) = e20& op2(e21,e22) = e22& op2(e22,e21) = e22 )| ( op2(e20,e22) = e20& op2(e22,e20) = e20& op2(e22,e22) = e22& op2(e22,e22) = e22 )| ( op2(e20,e22) = e20& op2(e22,e20) = e20& op2(e23,e22) = e22& op2(e22,e23) = e22 )| ( op2(e20,e23) = e20& op2(e23,e20) = e20& op2(e20,e23) = e23& op2(e23,e20) = e23 )| ( op2(e20,e23) = e20& op2(e23,e20) = e20& op2(e21,e23) = e23& op2(e23,e21) = e23 )| ( op2(e20,e23) = e20& op2(e23,e20) = e20& op2(e22,e23) = e23& op2(e23,e22) = e23 )| ( op2(e20,e23) = e20& op2(e23,e20) = e20& op2(e23,e23) = e23& op2(e23,e23) = e23 )| ( op2(e21,e20) = e21& op2(e20,e21) = e21& op2(e20,e20) = e20& op2(e20,e20) = e20 )| ( op2(e21,e20) = e21& op2(e20,e21) = e21& op2(e21,e20) = e20& op2(e20,e21) = e20 )| ( op2(e21,e20) = e21& op2(e20,e21) = e21& op2(e22,e20) = e20& op2(e20,e22) = e20 )| ( op2(e21,e20) = e21& op2(e20,e21) = e21& op2(e23,e20) = e20& op2(e20,e23) = e20 )| ( op2(e21,e21) = e21& op2(e21,e21) = e21& op2(e20,e21) = e21& op2(e21,e20) = e21 )| ( op2(e21,e21) = e21& op2(e21,e21) = e21& op2(e21,e21) = e21& op2(e21,e21) = e21 )| ( op2(e21,e21) = e21& op2(e21,e21) = e21& op2(e22,e21) = e21& op2(e21,e22) = e21 )| ( op2(e21,e21) = e21& op2(e21,e21) = e21& op2(e23,e21) = e21& op2(e21,e23) = e21 )| ( op2(e21,e22) = e21& op2(e22,e21) = e21& op2(e20,e22) = e22& op2(e22,e20) = e22 )| ( op2(e21,e22) = e21& op2(e22,e21) = e21& op2(e21,e22) = e22& op2(e22,e21) = e22 )| ( op2(e21,e22) = e21& op2(e22,e21) = e21& op2(e22,e22) = e22& op2(e22,e22) = e22 )| ( op2(e21,e22) = e21& op2(e22,e21) = e21& op2(e23,e22) = e22& op2(e22,e23) = e22 )| ( op2(e21,e23) = e21& op2(e23,e21) = e21& op2(e20,e23) = e23& op2(e23,e20) = e23 )| ( op2(e21,e23) = e21& op2(e23,e21) = e21& op2(e21,e23) = e23& op2(e23,e21) = e23 )| ( op2(e21,e23) = e21& op2(e23,e21) = e21& op2(e22,e23) = e23& op2(e23,e22) = e23 )| ( op2(e21,e23) = e21& op2(e23,e21) = e21& op2(e23,e23) = e23& op2(e23,e23) = e23 )| ( op2(e22,e20) = e22& op2(e20,e22) = e22& op2(e20,e20) = e20& op2(e20,e20) = e20 )| ( op2(e22,e20) = e22& op2(e20,e22) = e22& op2(e21,e20) = e20& op2(e20,e21) = e20 )| ( op2(e22,e20) = e22& op2(e20,e22) = e22& op2(e22,e20) = e20& op2(e20,e22) = e20 )| ( op2(e22,e20) = e22& op2(e20,e22) = e22& op2(e23,e20) = e20& op2(e20,e23) = e20 )| ( op2(e22,e21) = e22& op2(e21,e22) = e22& op2(e20,e21) = e21& op2(e21,e20) = e21 )| ( op2(e22,e21) = e22& op2(e21,e22) = e22& op2(e21,e21) = e21& op2(e21,e21) = e21 )| ( op2(e22,e21) = e22& op2(e21,e22) = e22& op2(e22,e21) = e21& op2(e21,e22) = e21 )| ( op2(e22,e21) = e22& op2(e21,e22) = e22& op2(e23,e21) = e21& op2(e21,e23) = e21 )| ( op2(e22,e22) = e22& op2(e22,e22) = e22& op2(e20,e22) = e22& op2(e22,e20) = e22 )| ( op2(e22,e22) = e22& op2(e22,e22) = e22& op2(e21,e22) = e22& op2(e22,e21) = e22 )| ( op2(e22,e22) = e22& op2(e22,e22) = e22& op2(e22,e22) = e22& op2(e22,e22) = e22 )| ( op2(e22,e22) = e22& op2(e22,e22) = e22& op2(e23,e22) = e22& op2(e22,e23) = e22 )| ( op2(e22,e23) = e22& op2(e23,e22) = e22& op2(e20,e23) = e23& op2(e23,e20) = e23 )| ( op2(e22,e23) = e22& op2(e23,e22) = e22& op2(e21,e23) = e23& op2(e23,e21) = e23 )| ( op2(e22,e23) = e22& op2(e23,e22) = e22& op2(e22,e23) = e23& op2(e23,e22) = e23 )| ( op2(e22,e23) = e22& op2(e23,e22) = e22& op2(e23,e23) = e23& op2(e23,e23) = e23 )| ( op2(e23,e20) = e23& op2(e20,e23) = e23& op2(e20,e20) = e20& op2(e20,e20) = e20 )| ( op2(e23,e20) = e23& op2(e20,e23) = e23& op2(e21,e20) = e20& op2(e20,e21) = e20 )| ( op2(e23,e20) = e23& op2(e20,e23) = e23& op2(e22,e20) = e20& op2(e20,e22) = e20 )| ( op2(e23,e20) = e23& op2(e20,e23) = e23& op2(e23,e20) = e20& op2(e20,e23) = e20 )| ( op2(e23,e21) = e23& op2(e21,e23) = e23& op2(e20,e21) = e21& op2(e21,e20) = e21 )| ( op2(e23,e21) = e23& op2(e21,e23) = e23& op2(e21,e21) = e21& op2(e21,e21) = e21 )| ( op2(e23,e21) = e23& op2(e21,e23) = e23& op2(e22,e21) = e21& op2(e21,e22) = e21 )| ( op2(e23,e21) = e23& op2(e21,e23) = e23& op2(e23,e21) = e21& op2(e21,e23) = e21 )| ( op2(e23,e22) = e23& op2(e22,e23) = e23& op2(e20,e22) = e22& op2(e22,e20) = e22 )| ( op2(e23,e22) = e23& op2(e22,e23) = e23& op2(e21,e22) = e22& op2(e22,e21) = e22 )| ( op2(e23,e22) = e23& op2(e22,e23) = e23& op2(e22,e22) = e22& op2(e22,e22) = e22 )| ( op2(e23,e22) = e23& op2(e22,e23) = e23& op2(e23,e22) = e22& op2(e22,e23) = e22 )| ( op2(e23,e23) = e23& op2(e23,e23) = e23& op2(e20,e23) = e23& op2(e23,e20) = e23 )| ( op2(e23,e23) = e23& op2(e23,e23) = e23& op2(e21,e23) = e23& op2(e23,e21) = e23 )| ( op2(e23,e23) = e23& op2(e23,e23) = e23& op2(e22,e23) = e23& op2(e23,e22) = e23 )| ( op2(e23,e23) = e23& op2(e23,e23) = e23& op2(e23,e23) = e23& op2(e23,e23) = e23 ) ) ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f12,axiom,(
% 0.28/0.67 ( e10 = op1(op1(e13,e13),op1(op1(e13,e13),e13))& e11 = op1(e13,e13)& e12 = op1(op1(e13,e13),e13) ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f13,axiom,(
% 0.28/0.67 ( e20 = op2(op2(e23,e23),op2(op2(e23,e23),e23))& e21 = op2(e23,e23)& e22 = op2(op2(e23,e23),e23) ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f14,axiom,(
% 0.28/0.67 ( h1(e13) = e20& h1(e10) = op2(op2(e20,e20),op2(op2(e20,e20),e20))& h1(e11) = op2(e20,e20)& h1(e12) = op2(op2(e20,e20),e20) ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f15,axiom,(
% 0.28/0.67 ( h2(e13) = e21& h2(e10) = op2(op2(e21,e21),op2(op2(e21,e21),e21))& h2(e11) = op2(e21,e21)& h2(e12) = op2(op2(e21,e21),e21) ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f16,axiom,(
% 0.28/0.67 ( h3(e13) = e22& h3(e10) = op2(op2(e22,e22),op2(op2(e22,e22),e22))& h3(e11) = op2(e22,e22)& h3(e12) = op2(op2(e22,e22),e22) ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f17,axiom,(
% 0.28/0.67 ( h4(e13) = e23& h4(e10) = op2(op2(e23,e23),op2(op2(e23,e23),e23))& h4(e11) = op2(e23,e23)& h4(e12) = op2(op2(e23,e23),e23) ) ),
% 0.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f18,conjecture,(
% 0.28/0.67 ( ( 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.28/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.67 fof(f19,negated_conjecture,(
% 0.28/0.67 ~(( ( 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.28/0.67 inference(negated_conjecture,[status(cth)],[f18])).
% 0.28/0.67 fof(f23,plain,(
% 0.28/0.67 op1(e10,e13)=e10|op1(e10,e13)=e11|op1(e10,e13)=e12|op1(e10,e13)=e13),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f1])).
% 0.28/0.67 fof(f40,plain,(
% 0.28/0.67 op1(e10,e10)=e12|op1(e10,e11)=e12|op1(e10,e12)=e12|op1(e10,e13)=e12),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f41,plain,(
% 0.28/0.67 op1(e10,e10)=e12|op1(e11,e10)=e12|op1(e12,e10)=e12|op1(e13,e10)=e12),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f46,plain,(
% 0.28/0.67 op1(e11,e10)=e11|op1(e11,e11)=e11|op1(e11,e12)=e11|op1(e11,e13)=e11),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f47,plain,(
% 0.28/0.67 op1(e10,e11)=e11|op1(e11,e11)=e11|op1(e12,e11)=e11|op1(e13,e11)=e11),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f55,plain,(
% 0.28/0.67 op1(e10,e12)=e11|op1(e11,e12)=e11|op1(e12,e12)=e11|op1(e13,e12)=e11),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f58,plain,(
% 0.28/0.67 op1(e12,e10)=e13|op1(e12,e11)=e13|op1(e12,e12)=e13|op1(e12,e13)=e13),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f59,plain,(
% 0.28/0.67 op1(e10,e12)=e13|op1(e11,e12)=e13|op1(e12,e12)=e13|op1(e13,e12)=e13),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f60,plain,(
% 0.28/0.67 op1(e13,e10)=e10|op1(e13,e11)=e10|op1(e13,e12)=e10|op1(e13,e13)=e10),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f61,plain,(
% 0.28/0.67 op1(e10,e13)=e10|op1(e11,e13)=e10|op1(e12,e13)=e10|op1(e13,e13)=e10),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.67 fof(f71,plain,(
% 0.28/0.67 op2(e20,e23)=e20|op2(e20,e23)=e21|op2(e20,e23)=e22|op2(e20,e23)=e23),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f3])).
% 0.28/0.67 fof(f86,plain,(
% 0.28/0.67 op2(e20,e20)=e21|op2(e20,e21)=e21|op2(e20,e22)=e21|op2(e20,e23)=e21),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f88,plain,(
% 0.28/0.67 op2(e20,e20)=e22|op2(e20,e21)=e22|op2(e20,e22)=e22|op2(e20,e23)=e22),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f89,plain,(
% 0.28/0.67 op2(e20,e20)=e22|op2(e21,e20)=e22|op2(e22,e20)=e22|op2(e23,e20)=e22),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f94,plain,(
% 0.28/0.67 op2(e21,e20)=e21|op2(e21,e21)=e21|op2(e21,e22)=e21|op2(e21,e23)=e21),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f95,plain,(
% 0.28/0.67 op2(e20,e21)=e21|op2(e21,e21)=e21|op2(e22,e21)=e21|op2(e23,e21)=e21),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f106,plain,(
% 0.28/0.67 op2(e22,e20)=e23|op2(e22,e21)=e23|op2(e22,e22)=e23|op2(e22,e23)=e23),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f107,plain,(
% 0.28/0.67 op2(e20,e22)=e23|op2(e21,e22)=e23|op2(e22,e22)=e23|op2(e23,e22)=e23),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f108,plain,(
% 0.28/0.67 op2(e23,e20)=e20|op2(e23,e21)=e20|op2(e23,e22)=e20|op2(e23,e23)=e20),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f109,plain,(
% 0.28/0.67 op2(e20,e23)=e20|op2(e21,e23)=e20|op2(e22,e23)=e20|op2(e23,e23)=e20),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.67 fof(f118,plain,(
% 0.28/0.67 ~op1(e10,e10)=op1(e13,e10)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f125,plain,(
% 0.28/0.67 ~op1(e11,e11)=op1(e12,e11)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f131,plain,(
% 0.28/0.67 ~op1(e11,e12)=op1(e12,e12)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f132,plain,(
% 0.28/0.67 ~op1(e11,e12)=op1(e13,e12)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f134,plain,(
% 0.28/0.67 ~op1(e10,e13)=op1(e11,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f136,plain,(
% 0.28/0.67 ~op1(e10,e13)=op1(e13,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f138,plain,(
% 0.28/0.67 ~op1(e11,e13)=op1(e13,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f142,plain,(
% 0.28/0.67 ~op1(e10,e10)=op1(e10,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f148,plain,(
% 0.28/0.67 ~op1(e11,e10)=op1(e11,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f149,plain,(
% 0.28/0.67 ~op1(e11,e11)=op1(e11,e12)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f150,plain,(
% 0.28/0.67 ~op1(e11,e11)=op1(e11,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f153,plain,(
% 0.28/0.67 ~op1(e12,e10)=op1(e12,e12)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f162,plain,(
% 0.28/0.67 ~op1(e13,e11)=op1(e13,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f163,plain,(
% 0.28/0.67 ~op1(e13,e12)=op1(e13,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.67 fof(f166,plain,(
% 0.28/0.67 ~op2(e20,e20)=op2(e23,e20)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f173,plain,(
% 0.28/0.67 ~op2(e21,e21)=op2(e22,e21)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f177,plain,(
% 0.28/0.67 ~op2(e20,e22)=op2(e22,e22)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f179,plain,(
% 0.28/0.67 ~op2(e21,e22)=op2(e22,e22)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f180,plain,(
% 0.28/0.67 ~op2(e21,e22)=op2(e23,e22)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f182,plain,(
% 0.28/0.67 ~op2(e20,e23)=op2(e21,e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f184,plain,(
% 0.28/0.67 ~op2(e20,e23)=op2(e23,e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f186,plain,(
% 0.28/0.67 ~op2(e21,e23)=op2(e23,e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f190,plain,(
% 0.28/0.67 ~op2(e20,e20)=op2(e20,e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f196,plain,(
% 0.28/0.67 ~op2(e21,e20)=op2(e21,e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f197,plain,(
% 0.28/0.67 ~op2(e21,e21)=op2(e21,e22)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f198,plain,(
% 0.28/0.67 ~op2(e21,e21)=op2(e21,e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f201,plain,(
% 0.28/0.67 ~op2(e22,e20)=op2(e22,e22)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f210,plain,(
% 0.28/0.67 ~op2(e23,e21)=op2(e23,e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.28/0.67 fof(f212,plain,(
% 0.28/0.67 ~e10=e11),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f7])).
% 0.28/0.67 fof(f213,plain,(
% 0.28/0.67 ~e10=e12),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f7])).
% 0.28/0.67 fof(f214,plain,(
% 0.28/0.67 ~e10=e13),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f7])).
% 0.28/0.67 fof(f215,plain,(
% 0.28/0.67 ~e11=e12),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f7])).
% 0.28/0.67 fof(f216,plain,(
% 0.28/0.67 ~e11=e13),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f7])).
% 0.28/0.67 fof(f217,plain,(
% 0.28/0.67 ~e12=e13),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f7])).
% 0.28/0.67 fof(f218,plain,(
% 0.28/0.67 ~e20=e21),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f8])).
% 0.28/0.67 fof(f219,plain,(
% 0.28/0.67 ~e20=e22),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f8])).
% 0.28/0.67 fof(f220,plain,(
% 0.28/0.67 ~e20=e23),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f8])).
% 0.28/0.67 fof(f221,plain,(
% 0.28/0.67 ~e21=e22),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f8])).
% 0.28/0.67 fof(f222,plain,(
% 0.28/0.67 ~e21=e23),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f8])).
% 0.28/0.67 fof(f223,plain,(
% 0.28/0.67 ~e22=e23),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f8])).
% 0.28/0.67 fof(f240,definition,(
% 0.28/0.67 sP0_prd<=>(((((~op1(e10,op1(e10,e10))=e10&~op1(e10,op1(e10,e11))=e11)&~op1(e10,op1(e10,e12))=e12)&~op1(e10,op1(e10,e13))=e13)|(((~op1(e11,op1(e11,e10))=e10&~op1(e11,op1(e11,e11))=e11)&~op1(e11,op1(e11,e12))=e12)&~op1(e11,op1(e11,e13))=e13))|(((~op1(e12,op1(e12,e10))=e10&~op1(e12,op1(e12,e11))=e11)&~op1(e12,op1(e12,e12))=e12)&~op1(e12,op1(e12,e13))=e13))),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.28/0.67 fof(f241,definition,(
% 0.28/0.67 sP1_prd<=>(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((op1(e10,e10)=e10&op1(e10,e10)=e10)&op1(e10,e10)=e10)&op1(e10,e10)=e10)|(((op1(e10,e10)=e10&op1(e10,e10)=e10)&op1(e11,e10)=e10)&op1(e10,e11)=e10))|(((op1(e10,e10)=e10&op1(e10,e10)=e10)&op1(e12,e10)=e10)&op1(e10,e12)=e10))|(((op1(e10,e10)=e10&op1(e10,e10)=e10)&op1(e13,e10)=e10)&op1(e10,e13)=e10))|(((op1(e10,e11)=e10&op1(e11,e10)=e10)&op1(e10,e11)=e11)&op1(e11,e10)=e11))|(((op1(e10,e11)=e10&op1(e11,e10)=e10)&op1(e11,e11)=e11)&op1(e11,e11)=e11))|(((op1(e10,e11)=e10&op1(e11,e10)=e10)&op1(e12,e11)=e11)&op1(e11,e12)=e11))|(((op1(e10,e11)=e10&op1(e11,e10)=e10)&op1(e13,e11)=e11)&op1(e11,e13)=e11))|(((op1(e10,e12)=e10&op1(e12,e10)=e10)&op1(e10,e12)=e12)&op1(e12,e10)=e12))|(((op1(e10,e12)=e10&op1(e12,e10)=e10)&op1(e11,e12)=e12)&op1(e12,e11)=e12))|(((op1(e10,e12)=e10&op1(e12,e10)=e10)&op1(e12,e12)=e12)&op1(e12,e12)=e12))|(((op1(e10,e12)=e10&op1(e12,e10)=e10)&op1(e13,e12)=e12)&op1(e12,e13)=e12))|(((op1(e10,e13)=e10&op1(e13,e10)=e10)&op1(e10,e13)=e13)&op1(e13,e10)=e13))|(((op1(e10,e13)=e10&op1(e13,e10)=e10)&op1(e11,e13)=e13)&op1(e13,e11)=e13))|(((op1(e10,e13)=e10&op1(e13,e10)=e10)&op1(e12,e13)=e13)&op1(e13,e12)=e13))|(((op1(e10,e13)=e10&op1(e13,e10)=e10)&op1(e13,e13)=e13)&op1(e13,e13)=e13))|(((op1(e11,e10)=e11&op1(e10,e11)=e11)&op1(e10,e10)=e10)&op1(e10,e10)=e10))|(((op1(e11,e10)=e11&op1(e10,e11)=e11)&op1(e11,e10)=e10)&op1(e10,e11)=e10))|(((op1(e11,e10)=e11&op1(e10,e11)=e11)&op1(e12,e10)=e10)&op1(e10,e12)=e10))|(((op1(e11,e10)=e11&op1(e10,e11)=e11)&op1(e13,e10)=e10)&op1(e10,e13)=e10))|(((op1(e11,e11)=e11&op1(e11,e11)=e11)&op1(e10,e11)=e11)&op1(e11,e10)=e11))|(((op1(e11,e11)=e11&op1(e11,e11)=e11)&op1(e11,e11)=e11)&op1(e11,e11)=e11))|(((op1(e11,e11)=e11&op1(e11,e11)=e11)&op1(e12,e11)=e11)&op1(e11,e12)=e11))|(((op1(e11,e11)=e11&op1(e11,e11)=e11)&op1(e13,e11)=e11)&op1(e11,e13)=e11))|(((op1(e11,e12)=e11&op1(e12,e11)=e11)&op1(e10,e12)=e12)&op1(e12,e10)=e12))|(((op1(e11,e12)=e11&op1(e12,e11)=e11)&op1(e11,e12)=e12)&op1(e12,e11)=e12))|(((op1(e11,e12)=e11&op1(e12,e11)=e11)&op1(e12,e12)=e12)&op1(e12,e12)=e12))|(((op1(e11,e12)=e11&op1(e12,e11)=e11)&op1(e13,e12)=e12)&op1(e12,e13)=e12))|(((op1(e11,e13)=e11&op1(e13,e11)=e11)&op1(e10,e13)=e13)&op1(e13,e10)=e13))|(((op1(e11,e13)=e11&op1(e13,e11)=e11)&op1(e11,e13)=e13)&op1(e13,e11)=e13))|(((op1(e11,e13)=e11&op1(e13,e11)=e11)&op1(e12,e13)=e13)&op1(e13,e12)=e13))|(((op1(e11,e13)=e11&op1(e13,e11)=e11)&op1(e13,e13)=e13)&op1(e13,e13)=e13))|(((op1(e12,e10)=e12&op1(e10,e12)=e12)&op1(e10,e10)=e10)&op1(e10,e10)=e10))|(((op1(e12,e10)=e12&op1(e10,e12)=e12)&op1(e11,e10)=e10)&op1(e10,e11)=e10))|(((op1(e12,e10)=e12&op1(e10,e12)=e12)&op1(e12,e10)=e10)&op1(e10,e12)=e10))|(((op1(e12,e10)=e12&op1(e10,e12)=e12)&op1(e13,e10)=e10)&op1(e10,e13)=e10))|(((op1(e12,e11)=e12&op1(e11,e12)=e12)&op1(e10,e11)=e11)&op1(e11,e10)=e11))|(((op1(e12,e11)=e12&op1(e11,e12)=e12)&op1(e11,e11)=e11)&op1(e11,e11)=e11))|(((op1(e12,e11)=e12&op1(e11,e12)=e12)&op1(e12,e11)=e11)&op1(e11,e12)=e11))|(((op1(e12,e11)=e12&op1(e11,e12)=e12)&op1(e13,e11)=e11)&op1(e11,e13)=e11))|(((op1(e12,e12)=e12&op1(e12,e12)=e12)&op1(e10,e12)=e12)&op1(e12,e10)=e12))|(((op1(e12,e12)=e12&op1(e12,e12)=e12)&op1(e11,e12)=e12)&op1(e12,e11)=e12))|(((op1(e12,e12)=e12&op1(e12,e12)=e12)&op1(e12,e12)=e12)&op1(e12,e12)=e12))|(((op1(e12,e12)=e12&op1(e12,e12)=e12)&op1(e13,e12)=e12)&op1(e12,e13)=e12))|(((op1(e12,e13)=e12&op1(e13,e12)=e12)&op1(e10,e13)=e13)&op1(e13,e10)=e13))|(((op1(e12,e13)=e12&op1(e13,e12)=e12)&op1(e11,e13)=e13)&op1(e13,e11)=e13))|(((op1(e12,e13)=e12&op1(e13,e12)=e12)&op1(e12,e13)=e13)&op1(e13,e12)=e13))|(((op1(e12,e13)=e12&op1(e13,e12)=e12)&op1(e13,e13)=e13)&op1(e13,e13)=e13))|(((op1(e13,e10)=e13&op1(e10,e13)=e13)&op1(e10,e10)=e10)&op1(e10,e10)=e10))|(((op1(e13,e10)=e13&op1(e10,e13)=e13)&op1(e11,e10)=e10)&op1(e10,e11)=e10))|(((op1(e13,e10)=e13&op1(e10,e13)=e13)&op1(e12,e10)=e10)&op1(e10,e12)=e10))|(((op1(e13,e10)=e13&op1(e10,e13)=e13)&op1(e13,e10)=e10)&op1(e10,e13)=e10))|(((op1(e13,e11)=e13&op1(e11,e13)=e13)&op1(e10,e11)=e11)&op1(e11,e10)=e11))|(((op1(e13,e11)=e13&op1(e11,e13)=e13)&op1(e11,e11)=e11)&op1(e11,e11)=e11))|(((op1(e13,e11)=e13&op1(e11,e13)=e13)&op1(e12,e11)=e11)&op1(e11,e12)=e11))|(((op1(e13,e11)=e13&op1(e11,e13)=e13)&op1(e13,e11)=e11)&op1(e11,e13)=e11))|(((op1(e13,e12)=e13&op1(e12,e13)=e13)&op1(e10,e12)=e12)&op1(e12,e10)=e12))|(((op1(e13,e12)=e13&op1(e12,e13)=e13)&op1(e11,e12)=e12)&op1(e12,e11)=e12))|(((op1(e13,e12)=e13&op1(e12,e13)=e13)&op1(e12,e12)=e12)&op1(e12,e12)=e12))|(((op1(e13,e12)=e13&op1(e12,e13)=e13)&op1(e13,e12)=e12)&op1(e12,e13)=e12))|(((op1(e13,e13)=e13&op1(e13,e13)=e13)&op1(e10,e13)=e13)&op1(e13,e10)=e13))|(((op1(e13,e13)=e13&op1(e13,e13)=e13)&op1(e11,e13)=e13)&op1(e13,e11)=e13))|(((op1(e13,e13)=e13&op1(e13,e13)=e13)&op1(e12,e13)=e13)&op1(e13,e12)=e13))),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.28/0.67 fof(f242,plain,(
% 0.28/0.67 (((((((op1(e10,e10)=e10|op1(e11,e11)=e10)|op1(e12,e12)=e10)|op1(e13,e13)=e10)&(((op1(e10,e10)=e11|op1(e11,e11)=e11)|op1(e12,e12)=e11)|op1(e13,e13)=e11))&(((op1(e10,e10)=e12|op1(e11,e11)=e12)|op1(e12,e12)=e12)|op1(e13,e13)=e12))&(((op1(e10,e10)=e13|op1(e11,e11)=e13)|op1(e12,e12)=e13)|op1(e13,e13)=e13))&(sP0_prd|(((~op1(e13,op1(e13,e10))=e10&~op1(e13,op1(e13,e11))=e11)&~op1(e13,op1(e13,e12))=e12)&~op1(e13,op1(e13,e13))=e13)))&(sP1_prd|(((op1(e13,e13)=e13&op1(e13,e13)=e13)&op1(e13,e13)=e13)&op1(e13,e13)=e13))),
% 0.28/0.67 inference(formula_renaming,[status(thm)],[f10,f241,f240])).
% 0.28/0.67 fof(f243,plain,(
% 0.28/0.67 op1(e10,e10)=e10|op1(e11,e11)=e10|op1(e12,e12)=e10|op1(e13,e13)=e10),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f242])).
% 0.28/0.67 fof(f245,plain,(
% 0.28/0.67 op1(e10,e10)=e12|op1(e11,e11)=e12|op1(e12,e12)=e12|op1(e13,e13)=e12),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f242])).
% 0.28/0.67 fof(f246,plain,(
% 0.28/0.67 op1(e10,e10)=e13|op1(e11,e11)=e13|op1(e12,e12)=e13|op1(e13,e13)=e13),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f242])).
% 0.28/0.67 fof(f255,definition,(
% 0.28/0.67 sP2_prd<=>(((((~op2(e20,op2(e20,e20))=e20&~op2(e20,op2(e20,e21))=e21)&~op2(e20,op2(e20,e22))=e22)&~op2(e20,op2(e20,e23))=e23)|(((~op2(e21,op2(e21,e20))=e20&~op2(e21,op2(e21,e21))=e21)&~op2(e21,op2(e21,e22))=e22)&~op2(e21,op2(e21,e23))=e23))|(((~op2(e22,op2(e22,e20))=e20&~op2(e22,op2(e22,e21))=e21)&~op2(e22,op2(e22,e22))=e22)&~op2(e22,op2(e22,e23))=e23))),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.28/0.67 fof(f256,definition,(
% 0.28/0.67 sP3_prd<=>(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((op2(e20,e20)=e20&op2(e20,e20)=e20)&op2(e20,e20)=e20)&op2(e20,e20)=e20)|(((op2(e20,e20)=e20&op2(e20,e20)=e20)&op2(e21,e20)=e20)&op2(e20,e21)=e20))|(((op2(e20,e20)=e20&op2(e20,e20)=e20)&op2(e22,e20)=e20)&op2(e20,e22)=e20))|(((op2(e20,e20)=e20&op2(e20,e20)=e20)&op2(e23,e20)=e20)&op2(e20,e23)=e20))|(((op2(e20,e21)=e20&op2(e21,e20)=e20)&op2(e20,e21)=e21)&op2(e21,e20)=e21))|(((op2(e20,e21)=e20&op2(e21,e20)=e20)&op2(e21,e21)=e21)&op2(e21,e21)=e21))|(((op2(e20,e21)=e20&op2(e21,e20)=e20)&op2(e22,e21)=e21)&op2(e21,e22)=e21))|(((op2(e20,e21)=e20&op2(e21,e20)=e20)&op2(e23,e21)=e21)&op2(e21,e23)=e21))|(((op2(e20,e22)=e20&op2(e22,e20)=e20)&op2(e20,e22)=e22)&op2(e22,e20)=e22))|(((op2(e20,e22)=e20&op2(e22,e20)=e20)&op2(e21,e22)=e22)&op2(e22,e21)=e22))|(((op2(e20,e22)=e20&op2(e22,e20)=e20)&op2(e22,e22)=e22)&op2(e22,e22)=e22))|(((op2(e20,e22)=e20&op2(e22,e20)=e20)&op2(e23,e22)=e22)&op2(e22,e23)=e22))|(((op2(e20,e23)=e20&op2(e23,e20)=e20)&op2(e20,e23)=e23)&op2(e23,e20)=e23))|(((op2(e20,e23)=e20&op2(e23,e20)=e20)&op2(e21,e23)=e23)&op2(e23,e21)=e23))|(((op2(e20,e23)=e20&op2(e23,e20)=e20)&op2(e22,e23)=e23)&op2(e23,e22)=e23))|(((op2(e20,e23)=e20&op2(e23,e20)=e20)&op2(e23,e23)=e23)&op2(e23,e23)=e23))|(((op2(e21,e20)=e21&op2(e20,e21)=e21)&op2(e20,e20)=e20)&op2(e20,e20)=e20))|(((op2(e21,e20)=e21&op2(e20,e21)=e21)&op2(e21,e20)=e20)&op2(e20,e21)=e20))|(((op2(e21,e20)=e21&op2(e20,e21)=e21)&op2(e22,e20)=e20)&op2(e20,e22)=e20))|(((op2(e21,e20)=e21&op2(e20,e21)=e21)&op2(e23,e20)=e20)&op2(e20,e23)=e20))|(((op2(e21,e21)=e21&op2(e21,e21)=e21)&op2(e20,e21)=e21)&op2(e21,e20)=e21))|(((op2(e21,e21)=e21&op2(e21,e21)=e21)&op2(e21,e21)=e21)&op2(e21,e21)=e21))|(((op2(e21,e21)=e21&op2(e21,e21)=e21)&op2(e22,e21)=e21)&op2(e21,e22)=e21))|(((op2(e21,e21)=e21&op2(e21,e21)=e21)&op2(e23,e21)=e21)&op2(e21,e23)=e21))|(((op2(e21,e22)=e21&op2(e22,e21)=e21)&op2(e20,e22)=e22)&op2(e22,e20)=e22))|(((op2(e21,e22)=e21&op2(e22,e21)=e21)&op2(e21,e22)=e22)&op2(e22,e21)=e22))|(((op2(e21,e22)=e21&op2(e22,e21)=e21)&op2(e22,e22)=e22)&op2(e22,e22)=e22))|(((op2(e21,e22)=e21&op2(e22,e21)=e21)&op2(e23,e22)=e22)&op2(e22,e23)=e22))|(((op2(e21,e23)=e21&op2(e23,e21)=e21)&op2(e20,e23)=e23)&op2(e23,e20)=e23))|(((op2(e21,e23)=e21&op2(e23,e21)=e21)&op2(e21,e23)=e23)&op2(e23,e21)=e23))|(((op2(e21,e23)=e21&op2(e23,e21)=e21)&op2(e22,e23)=e23)&op2(e23,e22)=e23))|(((op2(e21,e23)=e21&op2(e23,e21)=e21)&op2(e23,e23)=e23)&op2(e23,e23)=e23))|(((op2(e22,e20)=e22&op2(e20,e22)=e22)&op2(e20,e20)=e20)&op2(e20,e20)=e20))|(((op2(e22,e20)=e22&op2(e20,e22)=e22)&op2(e21,e20)=e20)&op2(e20,e21)=e20))|(((op2(e22,e20)=e22&op2(e20,e22)=e22)&op2(e22,e20)=e20)&op2(e20,e22)=e20))|(((op2(e22,e20)=e22&op2(e20,e22)=e22)&op2(e23,e20)=e20)&op2(e20,e23)=e20))|(((op2(e22,e21)=e22&op2(e21,e22)=e22)&op2(e20,e21)=e21)&op2(e21,e20)=e21))|(((op2(e22,e21)=e22&op2(e21,e22)=e22)&op2(e21,e21)=e21)&op2(e21,e21)=e21))|(((op2(e22,e21)=e22&op2(e21,e22)=e22)&op2(e22,e21)=e21)&op2(e21,e22)=e21))|(((op2(e22,e21)=e22&op2(e21,e22)=e22)&op2(e23,e21)=e21)&op2(e21,e23)=e21))|(((op2(e22,e22)=e22&op2(e22,e22)=e22)&op2(e20,e22)=e22)&op2(e22,e20)=e22))|(((op2(e22,e22)=e22&op2(e22,e22)=e22)&op2(e21,e22)=e22)&op2(e22,e21)=e22))|(((op2(e22,e22)=e22&op2(e22,e22)=e22)&op2(e22,e22)=e22)&op2(e22,e22)=e22))|(((op2(e22,e22)=e22&op2(e22,e22)=e22)&op2(e23,e22)=e22)&op2(e22,e23)=e22))|(((op2(e22,e23)=e22&op2(e23,e22)=e22)&op2(e20,e23)=e23)&op2(e23,e20)=e23))|(((op2(e22,e23)=e22&op2(e23,e22)=e22)&op2(e21,e23)=e23)&op2(e23,e21)=e23))|(((op2(e22,e23)=e22&op2(e23,e22)=e22)&op2(e22,e23)=e23)&op2(e23,e22)=e23))|(((op2(e22,e23)=e22&op2(e23,e22)=e22)&op2(e23,e23)=e23)&op2(e23,e23)=e23))|(((op2(e23,e20)=e23&op2(e20,e23)=e23)&op2(e20,e20)=e20)&op2(e20,e20)=e20))|(((op2(e23,e20)=e23&op2(e20,e23)=e23)&op2(e21,e20)=e20)&op2(e20,e21)=e20))|(((op2(e23,e20)=e23&op2(e20,e23)=e23)&op2(e22,e20)=e20)&op2(e20,e22)=e20))|(((op2(e23,e20)=e23&op2(e20,e23)=e23)&op2(e23,e20)=e20)&op2(e20,e23)=e20))|(((op2(e23,e21)=e23&op2(e21,e23)=e23)&op2(e20,e21)=e21)&op2(e21,e20)=e21))|(((op2(e23,e21)=e23&op2(e21,e23)=e23)&op2(e21,e21)=e21)&op2(e21,e21)=e21))|(((op2(e23,e21)=e23&op2(e21,e23)=e23)&op2(e22,e21)=e21)&op2(e21,e22)=e21))|(((op2(e23,e21)=e23&op2(e21,e23)=e23)&op2(e23,e21)=e21)&op2(e21,e23)=e21))|(((op2(e23,e22)=e23&op2(e22,e23)=e23)&op2(e20,e22)=e22)&op2(e22,e20)=e22))|(((op2(e23,e22)=e23&op2(e22,e23)=e23)&op2(e21,e22)=e22)&op2(e22,e21)=e22))|(((op2(e23,e22)=e23&op2(e22,e23)=e23)&op2(e22,e22)=e22)&op2(e22,e22)=e22))|(((op2(e23,e22)=e23&op2(e22,e23)=e23)&op2(e23,e22)=e22)&op2(e22,e23)=e22))|(((op2(e23,e23)=e23&op2(e23,e23)=e23)&op2(e20,e23)=e23)&op2(e23,e20)=e23))|(((op2(e23,e23)=e23&op2(e23,e23)=e23)&op2(e21,e23)=e23)&op2(e23,e21)=e23))|(((op2(e23,e23)=e23&op2(e23,e23)=e23)&op2(e22,e23)=e23)&op2(e23,e22)=e23))),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.28/0.67 fof(f257,plain,(
% 0.28/0.67 (((((((op2(e20,e20)=e20|op2(e21,e21)=e20)|op2(e22,e22)=e20)|op2(e23,e23)=e20)&(((op2(e20,e20)=e21|op2(e21,e21)=e21)|op2(e22,e22)=e21)|op2(e23,e23)=e21))&(((op2(e20,e20)=e22|op2(e21,e21)=e22)|op2(e22,e22)=e22)|op2(e23,e23)=e22))&(((op2(e20,e20)=e23|op2(e21,e21)=e23)|op2(e22,e22)=e23)|op2(e23,e23)=e23))&(sP2_prd|(((~op2(e23,op2(e23,e20))=e20&~op2(e23,op2(e23,e21))=e21)&~op2(e23,op2(e23,e22))=e22)&~op2(e23,op2(e23,e23))=e23)))&(sP3_prd|(((op2(e23,e23)=e23&op2(e23,e23)=e23)&op2(e23,e23)=e23)&op2(e23,e23)=e23))),
% 0.28/0.67 inference(formula_renaming,[status(thm)],[f11,f256,f255])).
% 0.28/0.67 fof(f258,plain,(
% 0.28/0.67 op2(e20,e20)=e20|op2(e21,e21)=e20|op2(e22,e22)=e20|op2(e23,e23)=e20),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f257])).
% 0.28/0.67 fof(f260,plain,(
% 0.28/0.67 op2(e20,e20)=e22|op2(e21,e21)=e22|op2(e22,e22)=e22|op2(e23,e23)=e22),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f257])).
% 0.28/0.67 fof(f261,plain,(
% 0.28/0.67 op2(e20,e20)=e23|op2(e21,e21)=e23|op2(e22,e22)=e23|op2(e23,e23)=e23),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f257])).
% 0.28/0.67 fof(f270,plain,(
% 0.28/0.67 e10=op1(op1(e13,e13),op1(op1(e13,e13),e13))),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f12])).
% 0.28/0.67 fof(f271,plain,(
% 0.28/0.67 e11=op1(e13,e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f12])).
% 0.28/0.67 fof(f272,plain,(
% 0.28/0.67 e12=op1(op1(e13,e13),e13)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f12])).
% 0.28/0.67 fof(f273,plain,(
% 0.28/0.67 e20=op2(op2(e23,e23),op2(op2(e23,e23),e23))),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f13])).
% 0.28/0.67 fof(f274,plain,(
% 0.28/0.67 e21=op2(e23,e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f13])).
% 0.28/0.67 fof(f275,plain,(
% 0.28/0.67 e22=op2(op2(e23,e23),e23)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f13])).
% 0.28/0.67 fof(f278,plain,(
% 0.28/0.67 h1(e11)=op2(e20,e20)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f14])).
% 0.28/0.67 fof(f280,plain,(
% 0.28/0.67 h2(e13)=e21),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f15])).
% 0.28/0.67 fof(f281,plain,(
% 0.28/0.67 h2(e10)=op2(op2(e21,e21),op2(op2(e21,e21),e21))),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f15])).
% 0.28/0.67 fof(f282,plain,(
% 0.28/0.67 h2(e11)=op2(e21,e21)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f15])).
% 0.28/0.67 fof(f283,plain,(
% 0.28/0.67 h2(e12)=op2(op2(e21,e21),e21)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f15])).
% 0.28/0.67 fof(f286,plain,(
% 0.28/0.67 h3(e11)=op2(e22,e22)),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f16])).
% 0.28/0.67 fof(f289,plain,(
% 0.28/0.67 h4(e10)=op2(op2(e23,e23),op2(op2(e23,e23),e23))),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f17])).
% 0.28/0.67 fof(f292,plain,(
% 0.28/0.67 ((((((((((((((((((((((~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.28/0.67 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.28/0.67 fof(f293,definition,(
% 0.28/0.67 sP4_prd<=>(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.28/0.67 fof(f294,definition,(
% 0.28/0.67 sP5_prd<=>(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.28/0.67 fof(f295,definition,(
% 0.28/0.67 sP6_prd<=>(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.28/0.67 fof(f296,definition,(
% 0.28/0.67 sP7_prd<=>(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.28/0.67 fof(f297,definition,(
% 0.28/0.67 sP8_prd<=>(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.28/0.67 fof(f298,definition,(
% 0.28/0.67 sP9_prd<=>(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.28/0.67 fof(f299,definition,(
% 0.28/0.67 sP10_prd<=>(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.28/0.67 fof(f300,definition,(
% 0.28/0.67 sP11_prd<=>(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.28/0.67 fof(f301,definition,(
% 0.28/0.67 sP12_prd<=>(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.28/0.67 fof(f302,definition,(
% 0.28/0.67 sP13_prd<=>(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.28/0.67 fof(f303,definition,(
% 0.28/0.67 sP14_prd<=>(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.28/0.67 fof(f304,definition,(
% 0.28/0.67 sP15_prd<=>(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22)),
% 0.28/0.67 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.28/0.67 fof(f305,plain,(
% 0.28/0.67 (((((((((((((((((((((~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)))|sP4_prd)|sP5_prd)|sP6_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)))|sP7_prd)|sP8_prd)|sP9_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)))|sP10_prd)|sP11_prd)|sP12_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)))|sP13_prd)|sP14_prd)|sP15_prd)|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23))),
% 0.28/0.67 inference(formula_renaming,[status(thm)],[f292,f304,f303,f302,f301,f300,f299,f298,f297,f296,f295,f294,f293])).
% 0.28/0.67 fof(f311,plain,(
% 0.28/0.67 ~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))|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f305])).
% 0.28/0.67 fof(f376,plain,(
% 0.28/0.67 (~sP7_prd|(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20))&(sP7_prd|(((h2(e10)=e20|h2(e11)=e20)|h2(e12)=e20)|h2(e13)=e20))),
% 0.28/0.67 inference(NNF_transformation,[status(thm)],[f296])).
% 0.28/0.67 fof(f379,plain,(
% 0.28/0.67 ~sP7_prd|~h2(e12)=e20),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f376])).
% 0.28/0.67 fof(f382,plain,(
% 0.28/0.67 (~sP8_prd|(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21))&(sP8_prd|(((h2(e10)=e21|h2(e11)=e21)|h2(e12)=e21)|h2(e13)=e21))),
% 0.28/0.67 inference(NNF_transformation,[status(thm)],[f297])).
% 0.28/0.67 fof(f386,plain,(
% 0.28/0.67 ~sP8_prd|~h2(e13)=e21),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f382])).
% 0.28/0.67 fof(f388,plain,(
% 0.28/0.67 (~sP9_prd|(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22))&(sP9_prd|(((h2(e10)=e22|h2(e11)=e22)|h2(e12)=e22)|h2(e13)=e22))),
% 0.28/0.67 inference(NNF_transformation,[status(thm)],[f298])).
% 0.28/0.67 fof(f389,plain,(
% 0.28/0.67 ~sP9_prd|~h2(e10)=e22),
% 0.28/0.67 inference(cnf_transformation,[status(thm)],[f388])).
% 0.28/0.67 fof(f2106,plain,(
% 0.28/0.67 ~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),e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f280,f311])).
% 0.28/0.67 fof(f2123,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f280,f2106])).
% 0.28/0.67 fof(f2124,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f280,f2123])).
% 0.28/0.67 fof(f2125,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~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),e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f280,f2124])).
% 0.28/0.67 fof(f2126,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,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),e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f280,f2125])).
% 0.28/0.67 fof(f2127,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f280,f2126])).
% 0.28/0.67 fof(f2128,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f280,f2127])).
% 0.28/0.67 fof(f2129,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(op1(e13,e13))=op2(e21,e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f280,f2128])).
% 0.28/0.67 fof(f2307,plain,(
% 0.28/0.67 op1(e10,e13)=e10|op1(e11,e13)=e10|op1(e12,e13)=e10|e11=e10),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f271,f61])).
% 0.28/0.67 fof(f2308,plain,(
% 0.28/0.67 op1(e13,e10)=e10|op1(e13,e11)=e10|op1(e13,e12)=e10|e11=e10),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f271,f60])).
% 0.28/0.67 fof(f2314,plain,(
% 0.28/0.67 op1(e10,e13)=e10|op1(e11,e13)=e10|op1(e12,e13)=e10),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2307,f212])).
% 0.28/0.67 fof(f2315,plain,(
% 0.28/0.67 op1(e13,e10)=e10|op1(e13,e11)=e10|op1(e13,e12)=e10),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2308,f212])).
% 0.28/0.67 fof(f2388,plain,(
% 0.28/0.67 op2(e20,e23)=e20|op2(e21,e23)=e20|op2(e22,e23)=e20|e21=e20),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f274,f109])).
% 0.28/0.67 fof(f2389,plain,(
% 0.28/0.67 op2(e23,e20)=e20|op2(e23,e21)=e20|op2(e23,e22)=e20|e21=e20),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f274,f108])).
% 0.28/0.67 fof(f2391,plain,(
% 0.28/0.67 op2(e20,e23)=e20|op2(e21,e23)=e20|op2(e22,e23)=e20),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2388,f218])).
% 0.28/0.67 fof(f2392,plain,(
% 0.28/0.67 op2(e23,e20)=e20|op2(e23,e21)=e20|op2(e23,e22)=e20),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2389,f218])).
% 0.28/0.67 fof(f2523,plain,(
% 0.28/0.67 ~sP8_prd|~e21=e21),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f280,f386])).
% 0.28/0.67 fof(f2524,plain,(
% 0.28/0.67 ~sP8_prd),
% 0.28/0.67 inference(trivial_equality_resolution,[status(thm)],[f2523])).
% 0.28/0.67 fof(f2551,plain,(
% 0.28/0.67 op1(e10,e13)=e10|op1(e10,e13)=e12|op1(e10,e13)=e13),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f23,f2553])).
% 0.28/0.67 fof(f2553,plain,(
% 0.28/0.67 ~op1(e10,e13)=e11),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f136])).
% 0.28/0.67 fof(f2563,plain,(
% 0.28/0.67 op1(e11,e10)=e11|op1(e11,e11)=e11|op1(e11,e12)=e11),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f46,f2564])).
% 0.28/0.67 fof(f2564,plain,(
% 0.28/0.67 ~op1(e11,e13)=e11),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f138])).
% 0.28/0.67 fof(f2645,plain,(
% 0.28/0.67 op1(e10,e11)=e11|op1(e11,e11)=e11|op1(e12,e11)=e11),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f47,f2646])).
% 0.28/0.67 fof(f2646,plain,(
% 0.28/0.67 ~op1(e13,e11)=e11),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f162])).
% 0.28/0.67 fof(f2651,plain,(
% 0.28/0.67 op1(e10,e12)=e11|op1(e11,e12)=e11|op1(e12,e12)=e11),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f55,f2652])).
% 0.28/0.67 fof(f2652,plain,(
% 0.28/0.67 ~op1(e13,e12)=e11),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f163])).
% 0.28/0.67 fof(f2736,plain,(
% 0.28/0.67 op2(e20,e23)=e20|op2(e20,e23)=e22|op2(e20,e23)=e23),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f71,f2738])).
% 0.28/0.67 fof(f2737,plain,(
% 0.28/0.67 op2(e20,e20)=e21|op2(e20,e21)=e21|op2(e20,e22)=e21),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f86,f2738])).
% 0.28/0.67 fof(f2738,plain,(
% 0.28/0.67 ~op2(e20,e23)=e21),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f184])).
% 0.28/0.67 fof(f2750,plain,(
% 0.28/0.67 op2(e21,e20)=e21|op2(e21,e21)=e21|op2(e21,e22)=e21),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f94,f2751])).
% 0.28/0.67 fof(f2751,plain,(
% 0.28/0.67 ~op2(e21,e23)=e21),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f186])).
% 0.28/0.67 fof(f2799,plain,(
% 0.28/0.67 ~h1(e11)=op2(e20,e23)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f278,f190])).
% 0.28/0.67 fof(f2802,plain,(
% 0.28/0.67 ~h1(e11)=op2(e23,e20)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f278,f166])).
% 0.28/0.67 fof(f2807,plain,(
% 0.28/0.67 h1(e11)=e22|op2(e21,e20)=e22|op2(e22,e20)=e22|op2(e23,e20)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f278,f89])).
% 0.28/0.67 fof(f2808,plain,(
% 0.28/0.67 h1(e11)=e22|op2(e20,e21)=e22|op2(e20,e22)=e22|op2(e20,e23)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f278,f88])).
% 0.28/0.67 fof(f2868,plain,(
% 0.28/0.67 ~h2(e11)=op2(e21,e23)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f282,f198])).
% 0.28/0.67 fof(f2869,plain,(
% 0.28/0.67 ~h2(e11)=op2(e21,e22)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f282,f197])).
% 0.28/0.67 fof(f2872,plain,(
% 0.28/0.67 ~h2(e11)=op2(e22,e21)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f282,f173])).
% 0.28/0.67 fof(f2878,plain,(
% 0.28/0.67 op2(e20,e21)=e21|h2(e11)=e21|op2(e22,e21)=e21|op2(e23,e21)=e21),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f282,f95])).
% 0.28/0.67 fof(f2887,plain,(
% 0.28/0.67 ~op2(e22,e20)=h3(e11)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f286,f201])).
% 0.28/0.67 fof(f2889,plain,(
% 0.28/0.67 ~op2(e21,e22)=h3(e11)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f286,f179])).
% 0.28/0.67 fof(f2890,plain,(
% 0.28/0.67 ~op2(e20,e22)=h3(e11)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f286,f177])).
% 0.28/0.67 fof(f2891,plain,(
% 0.28/0.67 op2(e20,e22)=e23|op2(e21,e22)=e23|h3(e11)=e23|op2(e23,e22)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f286,f107])).
% 0.28/0.67 fof(f2892,plain,(
% 0.28/0.67 op2(e22,e20)=e23|op2(e22,e21)=e23|h3(e11)=e23|op2(e22,e23)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f286,f106])).
% 0.28/0.67 fof(f2903,plain,(
% 0.28/0.67 ~op2(e23,e21)=e21),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f210])).
% 0.28/0.67 fof(f2908,plain,(
% 0.28/0.67 op1(e10,e10)=e10|op1(e11,e11)=e10|op1(e12,e12)=e10|e11=e10),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f243])).
% 0.28/0.67 fof(f2909,plain,(
% 0.28/0.67 op1(e10,e10)=e10|op1(e11,e11)=e10|op1(e12,e12)=e10),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2908,f212])).
% 0.28/0.67 fof(f2916,plain,(
% 0.28/0.67 op1(e10,e10)=e12|op1(e11,e11)=e12|op1(e12,e12)=e12|e11=e12),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f245])).
% 0.28/0.67 fof(f2917,plain,(
% 0.28/0.67 op1(e10,e10)=e12|op1(e11,e11)=e12|op1(e12,e12)=e12),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2916,f215])).
% 0.28/0.67 fof(f2928,plain,(
% 0.28/0.67 op1(e10,e10)=e13|op1(e11,e11)=e13|op1(e12,e12)=e13|e11=e13),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f246])).
% 0.28/0.67 fof(f2929,plain,(
% 0.28/0.67 op1(e10,e10)=e13|op1(e11,e11)=e13|op1(e12,e12)=e13),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2928,f216])).
% 0.28/0.67 fof(f2977,plain,(
% 0.28/0.67 h1(e11)=e20|op2(e21,e21)=e20|op2(e22,e22)=e20|op2(e23,e23)=e20),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f278,f258])).
% 0.28/0.67 fof(f2978,plain,(
% 0.28/0.67 h1(e11)=e20|h2(e11)=e20|op2(e22,e22)=e20|op2(e23,e23)=e20),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f282,f2977])).
% 0.28/0.67 fof(f2979,plain,(
% 0.28/0.67 h1(e11)=e20|h2(e11)=e20|h3(e11)=e20|op2(e23,e23)=e20),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f286,f2978])).
% 0.28/0.67 fof(f2980,plain,(
% 0.28/0.67 h1(e11)=e20|h2(e11)=e20|h3(e11)=e20|e21=e20),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f2979])).
% 0.28/0.67 fof(f2981,plain,(
% 0.28/0.67 h1(e11)=e20|h2(e11)=e20|h3(e11)=e20),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2980,f218])).
% 0.28/0.67 fof(f2985,plain,(
% 0.28/0.67 h1(e11)=e22|op2(e21,e21)=e22|op2(e22,e22)=e22|op2(e23,e23)=e22),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f278,f260])).
% 0.28/0.67 fof(f2986,plain,(
% 0.28/0.67 h1(e11)=e22|h2(e11)=e22|op2(e22,e22)=e22|op2(e23,e23)=e22),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f282,f2985])).
% 0.28/0.67 fof(f2987,plain,(
% 0.28/0.67 h1(e11)=e22|h2(e11)=e22|h3(e11)=e22|op2(e23,e23)=e22),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f286,f2986])).
% 0.28/0.67 fof(f2988,plain,(
% 0.28/0.67 h1(e11)=e22|h2(e11)=e22|h3(e11)=e22|e21=e22),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f2987])).
% 0.28/0.67 fof(f2989,plain,(
% 0.28/0.67 h1(e11)=e22|h2(e11)=e22|h3(e11)=e22),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2988,f221])).
% 0.28/0.67 fof(f2994,plain,(
% 0.28/0.67 h1(e11)=e23|op2(e21,e21)=e23|op2(e22,e22)=e23|op2(e23,e23)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f278,f261])).
% 0.28/0.67 fof(f2995,plain,(
% 0.28/0.67 h1(e11)=e23|h2(e11)=e23|op2(e22,e22)=e23|op2(e23,e23)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f282,f2994])).
% 0.28/0.67 fof(f2996,plain,(
% 0.28/0.67 h1(e11)=e23|h2(e11)=e23|h3(e11)=e23|op2(e23,e23)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f286,f2995])).
% 0.28/0.67 fof(f2997,plain,(
% 0.28/0.67 h1(e11)=e23|h2(e11)=e23|h3(e11)=e23|e21=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f2996])).
% 0.28/0.67 fof(f2998,plain,(
% 0.28/0.67 h1(e11)=e23|h2(e11)=e23|h3(e11)=e23),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2997,f222])).
% 0.28/0.67 fof(f3014,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(e11)=op2(e21,e21)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f2129])).
% 0.28/0.67 fof(f3015,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(e11)=h2(e11)|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f282,f3014])).
% 0.28/0.67 fof(f3016,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP8_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(trivial_equality_resolution,[status(thm)],[f3015])).
% 0.28/0.67 fof(f3017,plain,(
% 0.28/0.67 ~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),e21)|~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),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3016,f2524])).
% 0.28/0.67 fof(f3023,plain,(
% 0.28/0.67 e10=op1(e11,op1(op1(e13,e13),e13))),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f270])).
% 0.28/0.67 fof(f3024,plain,(
% 0.28/0.67 e10=op1(e11,op1(e11,e13))),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f3023])).
% 0.28/0.67 fof(f3029,plain,(
% 0.28/0.67 e10=op1(e11,e12)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3045,f3024])).
% 0.28/0.67 fof(f3031,plain,(
% 0.28/0.67 ~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),e21)|~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(e12)=op2(h2(e11),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3045,f3017])).
% 0.28/0.67 fof(f3037,plain,(
% 0.28/0.67 ~op1(e11,e11)=e12),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3045,f150])).
% 0.28/0.67 fof(f3038,plain,(
% 0.28/0.67 ~op1(e11,e10)=e12),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3045,f148])).
% 0.28/0.67 fof(f3041,plain,(
% 0.28/0.67 ~op1(e10,e13)=e12),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3045,f134])).
% 0.28/0.67 fof(f3045,plain,(
% 0.28/0.67 e12=op1(e11,e13)),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f271,f272])).
% 0.28/0.67 fof(f3048,plain,(
% 0.28/0.67 e20=op2(e21,op2(op2(e23,e23),e23))),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f273])).
% 0.28/0.67 fof(f3049,plain,(
% 0.28/0.67 e20=op2(e21,op2(e21,e23))),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f3048])).
% 0.28/0.67 fof(f3050,plain,(
% 0.28/0.67 e20=op2(e21,e22)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3058,f3049])).
% 0.28/0.67 fof(f3052,plain,(
% 0.28/0.67 ~op2(e21,e20)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3058,f196])).
% 0.28/0.67 fof(f3055,plain,(
% 0.28/0.67 ~op2(e20,e23)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3058,f182])).
% 0.28/0.67 fof(f3058,plain,(
% 0.28/0.67 e22=op2(e21,e23)),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f275])).
% 0.28/0.67 fof(f3080,plain,(
% 0.28/0.67 ~op1(e11,e11)=e10),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3029,f149])).
% 0.28/0.67 fof(f3082,plain,(
% 0.28/0.67 ~e10=op1(e13,e12)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3029,f132])).
% 0.28/0.67 fof(f3083,plain,(
% 0.28/0.67 ~e10=op1(e12,e12)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3029,f131])).
% 0.28/0.67 fof(f3085,plain,(
% 0.28/0.67 op1(e10,e12)=e13|e10=e13|op1(e12,e12)=e13|op1(e13,e12)=e13),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3029,f59])).
% 0.28/0.67 fof(f3089,plain,(
% 0.28/0.67 op1(e10,e12)=e13|op1(e12,e12)=e13|op1(e13,e12)=e13),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3085,f214])).
% 0.28/0.67 fof(f3096,plain,(
% 0.28/0.67 h2(e10)=op2(h2(e11),op2(op2(e21,e21),e21))),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f282,f281])).
% 0.28/0.67 fof(f3097,plain,(
% 0.28/0.67 h2(e10)=op2(h2(e11),op2(h2(e11),e21))),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f282,f3096])).
% 0.28/0.67 fof(f3098,plain,(
% 0.28/0.67 h2(e10)=op2(h2(e11),h2(e12))),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3099,f3097])).
% 0.28/0.67 fof(f3099,plain,(
% 0.28/0.67 h2(e12)=op2(h2(e11),e21)),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f282,f283])).
% 0.28/0.67 fof(f3115,plain,(
% 0.28/0.67 h4(e10)=op2(e21,op2(op2(e23,e23),e23))),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f289])).
% 0.28/0.67 fof(f3116,plain,(
% 0.28/0.67 h4(e10)=op2(e21,op2(e21,e23))),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f3115])).
% 0.28/0.67 fof(f3118,plain,(
% 0.28/0.67 ~h4(e10)=op2(e23,e22)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3121,f180])).
% 0.28/0.67 fof(f3121,plain,(
% 0.28/0.67 h4(e10)=op2(e21,e22)),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3058,f3116])).
% 0.28/0.67 fof(f3170,plain,(
% 0.28/0.67 op1(e10,e10)=e12|op1(e12,e12)=e12),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f2917,f3037])).
% 0.28/0.67 fof(f3173,plain,(
% 0.28/0.67 op1(e10,e10)=e12|op1(e12,e10)=e12|op1(e13,e10)=e12),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f41,f3038])).
% 0.28/0.67 fof(f3288,plain,(
% 0.28/0.67 op1(e10,e10)=e12|op1(e10,e11)=e12|op1(e10,e12)=e12),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f40,f3041])).
% 0.28/0.67 fof(f3301,plain,(
% 0.28/0.67 op1(e10,e13)=e10|e12=e10|op1(e12,e13)=e10),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3045,f2314])).
% 0.28/0.67 fof(f3302,plain,(
% 0.28/0.67 op1(e10,e13)=e10|op1(e12,e13)=e10),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3301,f213])).
% 0.28/0.67 fof(f3340,plain,(
% 0.28/0.67 ~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),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(e10)=op2(h2(e11),h2(e12))|~h2(e12)=op2(h2(e11),e21)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3029,f3031])).
% 0.28/0.67 fof(f3341,plain,(
% 0.28/0.67 ~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),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(e10)=op2(h2(e11),h2(e12))|~h2(e12)=h2(e12)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3099,f3340])).
% 0.28/0.67 fof(f3342,plain,(
% 0.28/0.67 ~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),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(e10)=op2(h2(e11),h2(e12))|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(trivial_equality_resolution,[status(thm)],[f3341])).
% 0.28/0.67 fof(f3346,plain,(
% 0.28/0.67 h4(e10)=e20),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3050,f3121])).
% 0.28/0.67 fof(f3370,plain,(
% 0.28/0.67 op2(e20,e23)=e20|e22=e20|op2(e22,e23)=e20),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3058,f2391])).
% 0.28/0.67 fof(f3371,plain,(
% 0.28/0.67 op2(e20,e23)=e20|op2(e22,e23)=e20),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3370,f219])).
% 0.28/0.67 fof(f3388,plain,(
% 0.28/0.67 op1(e10,e13)=e10|op1(e10,e13)=e13),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2551,f3041])).
% 0.28/0.67 fof(f3419,plain,(
% 0.28/0.67 op1(e11,e10)=e11|op1(e11,e11)=e11|e10=e11),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3029,f2563])).
% 0.28/0.67 fof(f3420,plain,(
% 0.28/0.67 op1(e11,e10)=e11|op1(e11,e11)=e11),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3419,f212])).
% 0.28/0.67 fof(f3524,plain,(
% 0.28/0.67 op1(e10,e10)=e10|op1(e12,e12)=e10),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f2909,f3080])).
% 0.28/0.67 fof(f3543,plain,(
% 0.28/0.67 op1(e10,e12)=e11|e10=e11|op1(e12,e12)=e11),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3029,f2651])).
% 0.28/0.67 fof(f3544,plain,(
% 0.28/0.67 op1(e10,e12)=e11|op1(e12,e12)=e11),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3543,f212])).
% 0.28/0.67 fof(f3556,plain,(
% 0.28/0.67 op2(e20,e23)=e20|op2(e20,e23)=e23),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2736,f3055])).
% 0.28/0.67 fof(f3563,plain,(
% 0.28/0.67 h1(e11)=e21|op2(e20,e21)=e21|op2(e20,e22)=e21),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f278,f2737])).
% 0.28/0.67 fof(f3591,plain,(
% 0.28/0.67 op1(e13,e10)=e10|op1(e13,e11)=e10),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f2315,f3082])).
% 0.28/0.67 fof(f3600,plain,(
% 0.28/0.67 op2(e21,e20)=e21|h2(e11)=e21|op2(e21,e22)=e21),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f282,f2750])).
% 0.28/0.67 fof(f3601,plain,(
% 0.28/0.67 op2(e21,e20)=e21|h2(e11)=e21|e20=e21),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3050,f3600])).
% 0.28/0.67 fof(f3602,plain,(
% 0.28/0.67 op2(e21,e20)=e21|h2(e11)=e21),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3601,f218])).
% 0.28/0.67 fof(f3671,plain,(
% 0.28/0.67 h1(e11)=e22|h3(e11)=e22),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f2989,f3673])).
% 0.28/0.67 fof(f3673,plain,(
% 0.28/0.67 ~h2(e11)=e22),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3058,f2868])).
% 0.28/0.67 fof(f3674,plain,(
% 0.28/0.67 h1(e11)=e20|h3(e11)=e20),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f2981,f3676])).
% 0.28/0.67 fof(f3676,plain,(
% 0.28/0.67 ~h2(e11)=e20),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3050,f2869])).
% 0.28/0.67 fof(f3684,plain,(
% 0.28/0.67 h1(e11)=e22|op2(e22,e20)=e22|op2(e23,e20)=e22),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2807,f3052])).
% 0.28/0.67 fof(f3693,plain,(
% 0.28/0.67 h1(e11)=e22|op2(e20,e21)=e22|op2(e20,e22)=e22),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2808,f3055])).
% 0.28/0.67 fof(f3826,plain,(
% 0.28/0.67 op2(e20,e21)=e21|h2(e11)=e21|op2(e22,e21)=e21),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2878,f2903])).
% 0.28/0.67 fof(f3876,plain,(
% 0.28/0.67 ~e20=h3(e11)),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3050,f2889])).
% 0.28/0.67 fof(f3881,plain,(
% 0.28/0.67 op2(e20,e22)=e23|e20=e23|h3(e11)=e23|op2(e23,e22)=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3050,f2891])).
% 0.28/0.67 fof(f3882,plain,(
% 0.28/0.67 op2(e20,e22)=e23|h3(e11)=e23|op2(e23,e22)=e23),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3881,f220])).
% 0.28/0.67 fof(f3931,plain,(
% 0.28/0.67 op2(e23,e20)=e20|op2(e23,e21)=e20),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f2392,f3932])).
% 0.28/0.67 fof(f3932,plain,(
% 0.28/0.67 ~e20=op2(e23,e22)),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f3346,f3118])).
% 0.28/0.67 fof(f4100,plain,(
% 0.28/0.67 e20=e22|h3(e11)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4134,f3671])).
% 0.28/0.67 fof(f4111,plain,(
% 0.28/0.67 e20=e22|op2(e20,e21)=e22|op2(e20,e22)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4134,f3693])).
% 0.28/0.67 fof(f4112,plain,(
% 0.28/0.67 e20=e22|op2(e22,e20)=e22|op2(e23,e20)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4134,f3684])).
% 0.28/0.67 fof(f4117,plain,(
% 0.28/0.67 ~e20=op2(e23,e20)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4134,f2802])).
% 0.28/0.67 fof(f4119,plain,(
% 0.28/0.67 e20=e21|op2(e20,e21)=e21|op2(e20,e22)=e21),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4134,f3563])).
% 0.28/0.67 fof(f4127,plain,(
% 0.28/0.67 ~e20=op2(e20,e23)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4134,f2799])).
% 0.28/0.67 fof(f4128,plain,(
% 0.28/0.67 e20=e23|h2(e11)=e23|h3(e11)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4134,f2998])).
% 0.28/0.67 fof(f4129,plain,(
% 0.28/0.67 e20=op2(e20,e20)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4134,f278])).
% 0.28/0.67 fof(f4134,plain,(
% 0.28/0.67 h1(e11)=e20),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3674,f3876])).
% 0.28/0.67 fof(f4135,plain,(
% 0.28/0.67 h3(e11)=e22),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4100,f219])).
% 0.28/0.67 fof(f4166,plain,(
% 0.28/0.67 op2(e20,e21)=e22|op2(e20,e22)=e22),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4111,f219])).
% 0.28/0.67 fof(f4167,plain,(
% 0.28/0.67 op2(e22,e20)=e22|op2(e23,e20)=e22),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4112,f219])).
% 0.28/0.67 fof(f4170,plain,(
% 0.28/0.67 op2(e20,e21)=e21|op2(e20,e22)=e21),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4119,f218])).
% 0.28/0.67 fof(f4190,plain,(
% 0.28/0.67 h2(e11)=e23|h3(e11)=e23),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4128,f220])).
% 0.28/0.67 fof(f4252,plain,(
% 0.28/0.67 op2(e22,e20)=e23|op2(e22,e21)=e23|e22=e23|op2(e22,e23)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4135,f2892])).
% 0.28/0.67 fof(f4253,plain,(
% 0.28/0.67 op2(e20,e22)=e23|e22=e23|op2(e23,e22)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4135,f3882])).
% 0.28/0.67 fof(f4254,plain,(
% 0.28/0.67 ~op2(e20,e22)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4135,f2890])).
% 0.28/0.67 fof(f4257,plain,(
% 0.28/0.67 ~op2(e22,e20)=e22),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4135,f2887])).
% 0.28/0.67 fof(f4276,plain,(
% 0.28/0.67 e22=op2(e22,e22)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4135,f286])).
% 0.28/0.67 fof(f4301,plain,(
% 0.28/0.67 op2(e22,e20)=e23|op2(e22,e21)=e23|op2(e22,e23)=e23),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4252,f223])).
% 0.28/0.67 fof(f4302,plain,(
% 0.28/0.67 op2(e20,e22)=e23|op2(e23,e22)=e23),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4253,f223])).
% 0.28/0.67 fof(f4413,plain,(
% 0.28/0.67 ~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),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(e10)=h2(e10)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f3098,f3342])).
% 0.28/0.67 fof(f4424,plain,(
% 0.28/0.67 ~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),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(trivial_equality_resolution,[status(thm)],[f4413])).
% 0.28/0.67 fof(f4498,plain,(
% 0.28/0.67 op2(e20,e23)=e23),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f3556,f4127])).
% 0.28/0.67 fof(f4499,plain,(
% 0.28/0.67 op2(e22,e23)=e20),
% 0.28/0.67 inference(backward_subsumption_resolution,[status(thm)],[f3371,f4127])).
% 0.28/0.67 fof(f4572,plain,(
% 0.28/0.67 ~h2(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),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~h2(e11)=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4595,f4424])).
% 0.28/0.67 fof(f4575,plain,(
% 0.28/0.67 e10=e12|op1(e10,e11)=e12|op1(e10,e12)=e12),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4595,f3288])).
% 0.28/0.67 fof(f4576,plain,(
% 0.28/0.67 e10=e12|op1(e12,e10)=e12|op1(e13,e10)=e12),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4595,f3173])).
% 0.28/0.67 fof(f4577,plain,(
% 0.28/0.67 e10=e12|op1(e12,e12)=e12),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4595,f3170])).
% 0.28/0.67 fof(f4585,plain,(
% 0.28/0.67 e10=e13|op1(e11,e11)=e13|op1(e12,e12)=e13),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4595,f2929])).
% 0.28/0.67 fof(f4586,plain,(
% 0.28/0.67 ~e10=op1(e10,e13)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4595,f142])).
% 0.28/0.67 fof(f4589,plain,(
% 0.28/0.67 ~e10=op1(e13,e10)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4595,f118])).
% 0.28/0.67 fof(f4595,plain,(
% 0.28/0.67 op1(e10,e10)=e10),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3524,f3083])).
% 0.28/0.67 fof(f4598,plain,(
% 0.28/0.67 op1(e10,e11)=e12|op1(e10,e12)=e12),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4575,f213])).
% 0.28/0.67 fof(f4599,plain,(
% 0.28/0.67 op1(e12,e10)=e12|op1(e13,e10)=e12),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4576,f213])).
% 0.28/0.67 fof(f4600,plain,(
% 0.28/0.67 op1(e12,e12)=e12),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4577,f213])).
% 0.28/0.67 fof(f4605,plain,(
% 0.28/0.67 op1(e11,e11)=e13|op1(e12,e12)=e13),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4585,f214])).
% 0.28/0.67 fof(f4736,plain,(
% 0.28/0.67 op2(e23,e21)=e20),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3931,f4117])).
% 0.28/0.67 fof(f4808,plain,(
% 0.28/0.67 e22=e21|h2(e11)=e21|op2(e22,e21)=e21),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4812,f3826])).
% 0.28/0.67 fof(f4812,plain,(
% 0.28/0.67 op2(e20,e21)=e22),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4166,f4254])).
% 0.28/0.67 fof(f4813,plain,(
% 0.28/0.67 h2(e11)=e21|op2(e22,e21)=e21),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4808,f221])).
% 0.28/0.67 fof(f4821,plain,(
% 0.28/0.67 op2(e23,e20)=e22),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4167,f4257])).
% 0.28/0.67 fof(f4871,plain,(
% 0.28/0.67 e22=e21|op2(e20,e22)=e21),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f4812,f4170])).
% 0.28/0.67 fof(f4877,plain,(
% 0.28/0.67 op2(e20,e22)=e21),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4871,f221])).
% 0.28/0.67 fof(f4906,plain,(
% 0.28/0.67 h2(e11)=e23|e22=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f4135,f4190])).
% 0.28/0.67 fof(f4908,plain,(
% 0.28/0.67 ~h2(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),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4921,f4572])).
% 0.28/0.67 fof(f4910,plain,(
% 0.28/0.67 h2(e10)=op2(e23,h2(e12))),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4921,f3098])).
% 0.28/0.67 fof(f4913,plain,(
% 0.28/0.67 ~e23=op2(e22,e21)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4921,f2872])).
% 0.28/0.67 fof(f4917,plain,(
% 0.28/0.67 op2(e21,e20)=e21|e23=e21),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4921,f3602])).
% 0.28/0.67 fof(f4919,plain,(
% 0.28/0.67 h2(e12)=op2(e23,e21)),
% 0.28/0.67 inference(backward_demodulation,[status(thm)],[f4921,f3099])).
% 0.28/0.67 fof(f4921,plain,(
% 0.28/0.67 h2(e11)=e23),
% 0.28/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4906,f223])).
% 0.28/0.67 fof(f4929,plain,(
% 0.28/0.67 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f4921,f4908])).
% 0.28/0.67 fof(f4930,plain,(
% 0.28/0.67 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f4921,f4929])).
% 0.28/0.67 fof(f4931,plain,(
% 0.28/0.67 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=op2(e23,h2(e11))|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f4921,f4930])).
% 0.28/0.67 fof(f4932,plain,(
% 0.28/0.67 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=op2(e23,e23)|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f4921,f4931])).
% 0.28/0.67 fof(f4933,plain,(
% 0.28/0.67 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~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),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f274,f4932])).
% 0.28/0.67 fof(f4934,plain,(
% 0.28/0.67 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e23)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f4921,f4933])).
% 0.28/0.67 fof(f4935,plain,(
% 0.28/0.67 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e23)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,e23)|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.67 inference(forward_demodulation,[status(thm)],[f4921,f4934])).
% 0.28/0.67 fof(f4936,plain,(
% 0.28/0.67 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e23)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd|~e23=e23),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f3058,f4935])).
% 0.28/0.68 fof(f4937,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e23)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP7_prd|sP9_prd),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f4936])).
% 0.28/0.68 fof(f4945,plain,(
% 0.28/0.68 op2(e21,e20)=e21),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f4917,f222])).
% 0.28/0.68 fof(f4948,plain,(
% 0.28/0.68 h2(e12)=e20),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4736,f4919])).
% 0.28/0.68 fof(f4966,plain,(
% 0.28/0.68 op2(e22,e20)=e23|op2(e22,e21)=e23|e20=e23),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4499,f4301])).
% 0.28/0.68 fof(f4967,plain,(
% 0.28/0.68 op2(e22,e20)=e23|op2(e22,e21)=e23),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f4966,f220])).
% 0.28/0.68 fof(f4970,plain,(
% 0.28/0.68 e21=e23|op2(e23,e22)=e23),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4877,f4302])).
% 0.28/0.68 fof(f4975,plain,(
% 0.28/0.68 op2(e23,e22)=e23),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f4970,f222])).
% 0.28/0.68 fof(f5133,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e23)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f4948,f4937])).
% 0.28/0.68 fof(f5137,plain,(
% 0.28/0.68 ~sP7_prd|~e20=e20),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f4948,f379])).
% 0.28/0.68 fof(f5138,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e23)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f5133])).
% 0.28/0.68 fof(f5139,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e23)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f5138])).
% 0.28/0.68 fof(f5140,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,e23)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f5139])).
% 0.28/0.68 fof(f5141,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4498,f5140])).
% 0.28/0.68 fof(f5142,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e12))=op2(e20,h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f5141])).
% 0.28/0.68 fof(f5143,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e12))=op2(e20,e20)|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f5142])).
% 0.28/0.68 fof(f5144,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e12))=e20|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4129,f5143])).
% 0.28/0.68 fof(f5145,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e12))=e20|~h2(op1(e12,e13))=op2(e20,e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f5144])).
% 0.28/0.68 fof(f5146,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e12))=e20|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4812,f5145])).
% 0.28/0.68 fof(f5148,plain,(
% 0.28/0.68 ~sP7_prd),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5137])).
% 0.28/0.68 fof(f5167,plain,(
% 0.28/0.68 op1(e10,e12)=e13|e12=e13|op1(e13,e12)=e13),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f4600,f3089])).
% 0.28/0.68 fof(f5171,plain,(
% 0.28/0.68 op1(e10,e12)=e11|e12=e11),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f4600,f3544])).
% 0.28/0.68 fof(f5177,plain,(
% 0.28/0.68 ~op1(e12,e10)=e12),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f4600,f153])).
% 0.28/0.68 fof(f5180,plain,(
% 0.28/0.68 op1(e12,e10)=e13|op1(e12,e11)=e13|e12=e13|op1(e12,e13)=e13),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f4600,f58])).
% 0.28/0.68 fof(f5188,plain,(
% 0.28/0.68 op1(e10,e12)=e13|op1(e13,e12)=e13),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5167,f217])).
% 0.28/0.68 fof(f5190,plain,(
% 0.28/0.68 op1(e10,e12)=e11),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5171,f215])).
% 0.28/0.68 fof(f5194,plain,(
% 0.28/0.68 op1(e12,e10)=e13|op1(e12,e11)=e13|op1(e12,e13)=e13),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5180,f217])).
% 0.28/0.68 fof(f5210,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(e12)=e20|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4600,f5146])).
% 0.28/0.68 fof(f5211,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~e20=e20|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f5210])).
% 0.28/0.68 fof(f5212,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP7_prd|sP9_prd),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5211])).
% 0.28/0.68 fof(f5213,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e11,e11))=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP9_prd),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5212,f5148])).
% 0.28/0.68 fof(f5216,plain,(
% 0.28/0.68 op1(e10,e13)=e13),
% 0.28/0.68 inference(backward_subsumption_resolution,[status(thm)],[f3388,f4586])).
% 0.28/0.68 fof(f5217,plain,(
% 0.28/0.68 op1(e12,e13)=e10),
% 0.28/0.68 inference(backward_subsumption_resolution,[status(thm)],[f3302,f4586])).
% 0.28/0.68 fof(f5229,plain,(
% 0.28/0.68 op1(e11,e11)=e13|e12=e13),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4600,f4605])).
% 0.28/0.68 fof(f5230,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(e13)=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP9_prd),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5243,f5213])).
% 0.28/0.68 fof(f5234,plain,(
% 0.28/0.68 op1(e10,e11)=e11|e13=e11|op1(e12,e11)=e11),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5243,f2645])).
% 0.28/0.68 fof(f5236,plain,(
% 0.28/0.68 op1(e11,e10)=e11|e13=e11),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5243,f3420])).
% 0.28/0.68 fof(f5240,plain,(
% 0.28/0.68 ~e13=op1(e12,e11)),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5243,f125])).
% 0.28/0.68 fof(f5243,plain,(
% 0.28/0.68 op1(e11,e11)=e13),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5229,f217])).
% 0.28/0.68 fof(f5244,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~e21=e21|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f280,f5230])).
% 0.28/0.68 fof(f5245,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=op2(e21,e20)|sP9_prd),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5244])).
% 0.28/0.68 fof(f5246,plain,(
% 0.28/0.68 op1(e10,e11)=e11|op1(e12,e11)=e11),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5234,f216])).
% 0.28/0.68 fof(f5249,plain,(
% 0.28/0.68 op1(e11,e10)=e11),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5236,f216])).
% 0.28/0.68 fof(f5253,plain,(
% 0.28/0.68 op1(e13,e11)=e10),
% 0.28/0.68 inference(backward_subsumption_resolution,[status(thm)],[f3591,f4589])).
% 0.28/0.68 fof(f5387,plain,(
% 0.28/0.68 op2(e22,e20)=e23),
% 0.28/0.68 inference(backward_subsumption_resolution,[status(thm)],[f4967,f4913])).
% 0.28/0.68 fof(f5403,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f4945,f5245])).
% 0.28/0.68 fof(f5444,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~h2(e11)=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5190,f5403])).
% 0.28/0.68 fof(f5448,plain,(
% 0.28/0.68 op1(e10,e11)=e12|e11=e12),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5190,f4598])).
% 0.28/0.68 fof(f5456,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~e23=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4921,f5444])).
% 0.28/0.68 fof(f5460,plain,(
% 0.28/0.68 op1(e10,e11)=e12),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5448,f215])).
% 0.28/0.68 fof(f5470,plain,(
% 0.28/0.68 op1(e13,e10)=e12),
% 0.28/0.68 inference(backward_subsumption_resolution,[status(thm)],[f4599,f5177])).
% 0.28/0.68 fof(f5516,plain,(
% 0.28/0.68 e23=e21|op2(e22,e21)=e21),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4921,f4813])).
% 0.28/0.68 fof(f5524,plain,(
% 0.28/0.68 op2(e22,e21)=e21),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5516,f222])).
% 0.28/0.68 fof(f5525,plain,(
% 0.28/0.68 h2(e10)=op2(e23,e20)),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f4910])).
% 0.28/0.68 fof(f5526,plain,(
% 0.28/0.68 ~h2(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~e23=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5529,f5456])).
% 0.28/0.68 fof(f5528,plain,(
% 0.28/0.68 ~sP9_prd|~e22=e22),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5529,f389])).
% 0.28/0.68 fof(f5529,plain,(
% 0.28/0.68 h2(e10)=e22),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4821,f5525])).
% 0.28/0.68 fof(f5530,plain,(
% 0.28/0.68 ~e22=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~e23=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5526])).
% 0.28/0.68 fof(f5531,plain,(
% 0.28/0.68 ~e22=op2(e22,h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e23)|~e23=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5530])).
% 0.28/0.68 fof(f5532,plain,(
% 0.28/0.68 ~e22=op2(e22,e22)|~h2(op1(e10,e11))=op2(h2(e10),e23)|~e23=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5531])).
% 0.28/0.68 fof(f5533,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=op2(h2(e10),e23)|~e23=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4276,f5532])).
% 0.28/0.68 fof(f5534,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=op2(e22,e23)|~e23=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5533])).
% 0.28/0.68 fof(f5535,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4499,f5534])).
% 0.28/0.68 fof(f5536,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5535])).
% 0.28/0.68 fof(f5537,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=op2(e22,e21)|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5536])).
% 0.28/0.68 fof(f5538,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=e21|~h2(op1(e11,e10))=op2(e23,h2(e10))|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5524,f5537])).
% 0.28/0.68 fof(f5539,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=e21|~h2(op1(e11,e10))=op2(e23,e22)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5538])).
% 0.28/0.68 fof(f5540,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4975,f5539])).
% 0.28/0.68 fof(f5541,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=op2(e20,e22)|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5540])).
% 0.28/0.68 fof(f5542,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=op2(e21,e22)|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4877,f5541])).
% 0.28/0.68 fof(f5543,plain,(
% 0.28/0.68 ~e22=e22|~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f3050,f5542])).
% 0.28/0.68 fof(f5544,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e10,e13))=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5543])).
% 0.28/0.68 fof(f5545,plain,(
% 0.28/0.68 ~sP9_prd),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5528])).
% 0.28/0.68 fof(f5551,plain,(
% 0.28/0.68 e11=e13|op1(e13,e12)=e13),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5190,f5188])).
% 0.28/0.68 fof(f5561,plain,(
% 0.28/0.68 op1(e13,e12)=e13),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5551,f216])).
% 0.28/0.68 fof(f5591,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(e13)=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5216,f5544])).
% 0.28/0.68 fof(f5592,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~e21=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22|~h2(op1(e13,e12))=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f280,f5591])).
% 0.28/0.68 fof(f5593,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~e21=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22|~h2(e13)=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5561,f5592])).
% 0.28/0.68 fof(f5594,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~e21=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22|~e21=e21|sP9_prd),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f280,f5593])).
% 0.28/0.68 fof(f5595,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~e21=e21|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22|sP9_prd),
% 0.28/0.68 inference(duplicate_literals_removal,[status(thm)],[f5594])).
% 0.28/0.68 fof(f5596,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22|sP9_prd),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5595])).
% 0.28/0.68 fof(f5597,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e12,e13))=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5596,f5545])).
% 0.28/0.68 fof(f5642,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(e10)=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5217,f5597])).
% 0.28/0.68 fof(f5651,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~e22=e22|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5642])).
% 0.28/0.68 fof(f5652,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e11,e10))=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5651])).
% 0.28/0.68 fof(f5664,plain,(
% 0.28/0.68 op1(e12,e10)=e13|op1(e12,e11)=e13|e10=e13),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5217,f5194])).
% 0.28/0.68 fof(f5665,plain,(
% 0.28/0.68 op1(e12,e10)=e13|op1(e12,e11)=e13),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5664,f214])).
% 0.28/0.68 fof(f5709,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(e11)=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5249,f5652])).
% 0.28/0.68 fof(f5710,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~e23=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4921,f5709])).
% 0.28/0.68 fof(f5711,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20|~h2(op1(e13,e11))=e22),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5710])).
% 0.28/0.68 fof(f5765,plain,(
% 0.28/0.68 op1(e12,e10)=e13),
% 0.28/0.68 inference(backward_subsumption_resolution,[status(thm)],[f5665,f5240])).
% 0.28/0.68 fof(f5775,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20|~h2(e10)=e22),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5253,f5711])).
% 0.28/0.68 fof(f5781,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20|~e22=e22),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5529,f5775])).
% 0.28/0.68 fof(f5782,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=op2(e22,e20)|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5781])).
% 0.28/0.68 fof(f5797,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~e23=e23|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5387,f5782])).
% 0.28/0.68 fof(f5798,plain,(
% 0.28/0.68 ~h2(op1(e10,e11))=e20|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5797])).
% 0.28/0.68 fof(f5991,plain,(
% 0.28/0.68 ~h2(e12)=e20|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5460,f5798])).
% 0.28/0.68 fof(f5994,plain,(
% 0.28/0.68 e12=e11|op1(e12,e11)=e11),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5460,f5246])).
% 0.28/0.68 fof(f5997,plain,(
% 0.28/0.68 ~e20=e20|~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f5991])).
% 0.28/0.68 fof(f5998,plain,(
% 0.28/0.68 ~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(op1(e13,e10))=e20),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f5997])).
% 0.28/0.68 fof(f6001,plain,(
% 0.28/0.68 op1(e12,e11)=e11),
% 0.28/0.68 inference(forward_subsumption_resolution,[status(thm)],[f5994,f215])).
% 0.28/0.68 fof(f6031,plain,(
% 0.28/0.68 ~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~h2(e12)=e20),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f5470,f5998])).
% 0.28/0.68 fof(f6032,plain,(
% 0.28/0.68 ~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23|~e20=e20),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4948,f6031])).
% 0.28/0.68 fof(f6033,plain,(
% 0.28/0.68 ~h2(op1(e12,e10))=e21|~h2(op1(e12,e11))=e23),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f6032])).
% 0.28/0.68 fof(f6167,plain,(
% 0.28/0.68 ~h2(e13)=e21|~h2(op1(e12,e11))=e23),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f5765,f6033])).
% 0.28/0.68 fof(f6171,plain,(
% 0.28/0.68 ~e21=e21|~h2(op1(e12,e11))=e23),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f280,f6167])).
% 0.28/0.68 fof(f6172,plain,(
% 0.28/0.68 ~h2(op1(e12,e11))=e23),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f6171])).
% 0.28/0.68 fof(f6339,plain,(
% 0.28/0.68 ~h2(e11)=e23),
% 0.28/0.68 inference(backward_demodulation,[status(thm)],[f6001,f6172])).
% 0.28/0.68 fof(f6343,plain,(
% 0.28/0.68 ~e23=e23),
% 0.28/0.68 inference(forward_demodulation,[status(thm)],[f4921,f6339])).
% 0.28/0.68 fof(f6344,plain,(
% 0.28/0.68 $false),
% 0.28/0.68 inference(trivial_equality_resolution,[status(thm)],[f6343])).
% 0.28/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 0.28/0.74 % Elapsed time: 0.356307 seconds
% 0.28/0.74 % CPU time: 1.306530 seconds
% 0.28/0.74 % Total memory used: 162.308 MB
% 0.28/0.74 % Net memory used: 161.592 MB
%------------------------------------------------------------------------------