%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG114+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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.17s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG114+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.37 % Computer : n015.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Mon Sep 21 12:59:51 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.43 % Drodi V4.1.1
% 0.17/0.54 % Refutation found
% 0.17/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.54 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.54 fof(f1,axiom,(
% 0.17/0.54 ( ( 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.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f2,axiom,(
% 0.17/0.54 ( ( 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.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f3,axiom,(
% 0.17/0.54 ( ( 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.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f4,axiom,(
% 0.17/0.54 ( ( 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.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f5,axiom,(
% 0.17/0.54 ( 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.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f6,axiom,(
% 0.17/0.54 ( 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.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f7,axiom,(
% 0.17/0.54 ( e10 != e11& e10 != e12& e10 != e13& e11 != e12& e11 != e13& e12 != e13 ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f8,axiom,(
% 0.17/0.54 ( e20 != e21& e20 != e22& e20 != e23& e21 != e22& e21 != e23& e22 != e23 ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f10,axiom,(
% 0.17/0.54 ( ( ( op1(e10,e10) = e10& op1(e10,e10) != e10 )| ( op1(e11,e11) = e10& op1(e10,e10) != e11 )| ( op1(e12,e12) = e10& op1(e10,e10) != e12 )| ( op1(e13,e13) = e10& op1(e10,e10) != e13 ) )& ( ( op1(e10,e10) = e11& op1(e11,e11) != e10 )| ( op1(e11,e11) = e11& op1(e11,e11) != e11 )| ( op1(e12,e12) = e11& op1(e11,e11) != e12 )| ( op1(e13,e13) = e11& op1(e11,e11) != e13 ) )& ( ( op1(e10,e10) = e12& op1(e12,e12) != e10 )| ( op1(e11,e11) = e12& op1(e12,e12) != e11 )| ( op1(e12,e12) = e12& op1(e12,e12) != e12 )| ( op1(e13,e13) = e12& op1(e12,e12) != e13 ) )& ( ( op1(e10,e10) = e13& op1(e13,e13) != e10 )| ( op1(e11,e11) = e13& op1(e13,e13) != e11 )| ( op1(e12,e12) = e13& op1(e13,e13) != e12 )| ( op1(e13,e13) = e13& op1(e13,e13) != e13 ) ) ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f11,axiom,(
% 0.17/0.54 ( ( ( op2(e20,e20) = e20& op2(e20,e20) != e20 )| ( op2(e21,e21) = e20& op2(e20,e20) != e21 )| ( op2(e22,e22) = e20& op2(e20,e20) != e22 )| ( op2(e23,e23) = e20& op2(e20,e20) != e23 ) )& ( ( op2(e20,e20) = e21& op2(e21,e21) != e20 )| ( op2(e21,e21) = e21& op2(e21,e21) != e21 )| ( op2(e22,e22) = e21& op2(e21,e21) != e22 )| ( op2(e23,e23) = e21& op2(e21,e21) != e23 ) )& ( ( op2(e20,e20) = e22& op2(e22,e22) != e20 )| ( op2(e21,e21) = e22& op2(e22,e22) != e21 )| ( op2(e22,e22) = e22& op2(e22,e22) != e22 )| ( op2(e23,e23) = e22& op2(e22,e22) != e23 ) )& ( ( op2(e20,e20) = e23& op2(e23,e23) != e20 )| ( op2(e21,e21) = e23& op2(e23,e23) != e21 )| ( op2(e22,e22) = e23& op2(e23,e23) != e22 )| ( op2(e23,e23) = e23& op2(e23,e23) != e23 ) ) ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f12,axiom,(
% 0.17/0.54 ( e10 = op1(op1(e12,e12),e12)& e11 = op1(op1(e12,e12),op1(e12,e12))& e13 = op1(e12,e12) ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f13,axiom,(
% 0.17/0.54 ( e20 = op2(op2(e22,e22),e22)& e21 = op2(op2(e22,e22),op2(e22,e22))& e23 = op2(e22,e22) ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f14,axiom,(
% 0.17/0.54 ( h1(e12) = e20& h1(e10) = op2(op2(e20,e20),e20)& h1(e11) = op2(op2(e20,e20),op2(e20,e20))& h1(e13) = op2(e20,e20) ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f15,axiom,(
% 0.17/0.54 ( h2(e12) = e21& h2(e10) = op2(op2(e21,e21),e21)& h2(e11) = op2(op2(e21,e21),op2(e21,e21))& h2(e13) = op2(e21,e21) ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f16,axiom,(
% 0.17/0.54 ( h3(e12) = e22& h3(e10) = op2(op2(e22,e22),e22)& h3(e11) = op2(op2(e22,e22),op2(e22,e22))& h3(e13) = op2(e22,e22) ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f17,axiom,(
% 0.17/0.54 ( h4(e12) = e23& h4(e10) = op2(op2(e23,e23),e23)& h4(e11) = op2(op2(e23,e23),op2(e23,e23))& h4(e13) = op2(e23,e23) ) ),
% 0.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f18,conjecture,(
% 0.17/0.54 ( ( 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.17/0.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.54 fof(f19,negated_conjecture,(
% 0.17/0.54 ~(( ( 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.17/0.54 inference(negated_conjecture,[status(cth)],[f18])).
% 0.17/0.54 fof(f22,plain,(
% 0.17/0.54 op1(e10,e12)=e10|op1(e10,e12)=e11|op1(e10,e12)=e12|op1(e10,e12)=e13),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f1])).
% 0.17/0.54 fof(f32,plain,(
% 0.17/0.54 op1(e13,e10)=e10|op1(e13,e10)=e11|op1(e13,e10)=e12|op1(e13,e10)=e13),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f1])).
% 0.17/0.54 fof(f36,plain,(
% 0.17/0.54 op1(e10,e10)=e10|op1(e10,e11)=e10|op1(e10,e12)=e10|op1(e10,e13)=e10),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f37,plain,(
% 0.17/0.54 op1(e10,e10)=e10|op1(e11,e10)=e10|op1(e12,e10)=e10|op1(e13,e10)=e10),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f46,plain,(
% 0.17/0.54 op1(e11,e10)=e11|op1(e11,e11)=e11|op1(e11,e12)=e11|op1(e11,e13)=e11),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f47,plain,(
% 0.17/0.54 op1(e10,e11)=e11|op1(e11,e11)=e11|op1(e12,e11)=e11|op1(e13,e11)=e11),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f50,plain,(
% 0.17/0.54 op1(e11,e10)=e13|op1(e11,e11)=e13|op1(e11,e12)=e13|op1(e11,e13)=e13),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f51,plain,(
% 0.17/0.54 op1(e10,e11)=e13|op1(e11,e11)=e13|op1(e12,e11)=e13|op1(e13,e11)=e13),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f57,plain,(
% 0.17/0.54 op1(e10,e12)=e12|op1(e11,e12)=e12|op1(e12,e12)=e12|op1(e13,e12)=e12),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f64,plain,(
% 0.17/0.54 op1(e13,e10)=e12|op1(e13,e11)=e12|op1(e13,e12)=e12|op1(e13,e13)=e12),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f65,plain,(
% 0.17/0.54 op1(e10,e13)=e12|op1(e11,e13)=e12|op1(e12,e13)=e12|op1(e13,e13)=e12),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.54 fof(f70,plain,(
% 0.17/0.54 op2(e20,e22)=e20|op2(e20,e22)=e21|op2(e20,e22)=e22|op2(e20,e22)=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f3])).
% 0.17/0.54 fof(f79,plain,(
% 0.17/0.54 op2(e22,e23)=e20|op2(e22,e23)=e21|op2(e22,e23)=e22|op2(e22,e23)=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f3])).
% 0.17/0.54 fof(f80,plain,(
% 0.17/0.54 op2(e23,e20)=e20|op2(e23,e20)=e21|op2(e23,e20)=e22|op2(e23,e20)=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f3])).
% 0.17/0.54 fof(f85,plain,(
% 0.17/0.54 op2(e20,e20)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.54 fof(f87,plain,(
% 0.17/0.54 op2(e20,e20)=e21|op2(e21,e20)=e21|op2(e22,e20)=e21|op2(e23,e20)=e21),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.54 fof(f98,plain,(
% 0.17/0.54 op2(e21,e20)=e23|op2(e21,e21)=e23|op2(e21,e22)=e23|op2(e21,e23)=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.54 fof(f99,plain,(
% 0.17/0.54 op2(e20,e21)=e23|op2(e21,e21)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.54 fof(f102,plain,(
% 0.17/0.54 op2(e22,e20)=e21|op2(e22,e21)=e21|op2(e22,e22)=e21|op2(e22,e23)=e21),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.54 fof(f105,plain,(
% 0.17/0.54 op2(e20,e22)=e22|op2(e21,e22)=e22|op2(e22,e22)=e22|op2(e23,e22)=e22),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.54 fof(f109,plain,(
% 0.17/0.54 op2(e20,e23)=e20|op2(e21,e23)=e20|op2(e22,e23)=e20|op2(e23,e23)=e20),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.54 fof(f112,plain,(
% 0.17/0.54 op2(e23,e20)=e22|op2(e23,e21)=e22|op2(e23,e22)=e22|op2(e23,e23)=e22),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f4])).
% 0.17/0.54 fof(f118,plain,(
% 0.17/0.54 ~op1(e10,e10)=op1(e13,e10)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f129,plain,(
% 0.17/0.54 ~op1(e10,e12)=op1(e12,e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f130,plain,(
% 0.17/0.54 ~op1(e10,e12)=op1(e13,e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f131,plain,(
% 0.17/0.54 ~op1(e11,e12)=op1(e12,e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f138,plain,(
% 0.17/0.54 ~op1(e11,e13)=op1(e13,e13)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f141,plain,(
% 0.17/0.54 ~op1(e10,e10)=op1(e10,e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f142,plain,(
% 0.17/0.54 ~op1(e10,e10)=op1(e10,e13)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f143,plain,(
% 0.17/0.54 ~op1(e10,e11)=op1(e10,e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f151,plain,(
% 0.17/0.54 ~op1(e11,e12)=op1(e11,e13)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f155,plain,(
% 0.17/0.54 ~op1(e12,e11)=op1(e12,e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f159,plain,(
% 0.17/0.54 ~op1(e13,e10)=op1(e13,e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f160,plain,(
% 0.17/0.54 ~op1(e13,e10)=op1(e13,e13)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f162,plain,(
% 0.17/0.54 ~op1(e13,e11)=op1(e13,e13)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f5])).
% 0.17/0.54 fof(f166,plain,(
% 0.17/0.54 ~op2(e20,e20)=op2(e23,e20)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f177,plain,(
% 0.17/0.54 ~op2(e20,e22)=op2(e22,e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f178,plain,(
% 0.17/0.54 ~op2(e20,e22)=op2(e23,e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f179,plain,(
% 0.17/0.54 ~op2(e21,e22)=op2(e22,e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f187,plain,(
% 0.17/0.54 ~op2(e22,e23)=op2(e23,e23)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f189,plain,(
% 0.17/0.54 ~op2(e20,e20)=op2(e20,e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f194,plain,(
% 0.17/0.54 ~op2(e21,e20)=op2(e21,e21)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f198,plain,(
% 0.17/0.54 ~op2(e21,e21)=op2(e21,e23)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f202,plain,(
% 0.17/0.54 ~op2(e22,e20)=op2(e22,e23)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f203,plain,(
% 0.17/0.54 ~op2(e22,e21)=op2(e22,e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f205,plain,(
% 0.17/0.54 ~op2(e22,e22)=op2(e22,e23)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f207,plain,(
% 0.17/0.54 ~op2(e23,e20)=op2(e23,e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f208,plain,(
% 0.17/0.54 ~op2(e23,e20)=op2(e23,e23)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f211,plain,(
% 0.17/0.54 ~op2(e23,e22)=op2(e23,e23)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f6])).
% 0.17/0.54 fof(f212,plain,(
% 0.17/0.54 ~e10=e11),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f7])).
% 0.17/0.54 fof(f213,plain,(
% 0.17/0.54 ~e10=e12),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f7])).
% 0.17/0.54 fof(f214,plain,(
% 0.17/0.54 ~e10=e13),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f7])).
% 0.17/0.54 fof(f215,plain,(
% 0.17/0.54 ~e11=e12),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f7])).
% 0.17/0.54 fof(f216,plain,(
% 0.17/0.54 ~e11=e13),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f7])).
% 0.17/0.54 fof(f217,plain,(
% 0.17/0.54 ~e12=e13),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f7])).
% 0.17/0.54 fof(f218,plain,(
% 0.17/0.54 ~e20=e21),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.54 fof(f219,plain,(
% 0.17/0.54 ~e20=e22),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.54 fof(f220,plain,(
% 0.17/0.54 ~e20=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.54 fof(f221,plain,(
% 0.17/0.54 ~e21=e22),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.54 fof(f222,plain,(
% 0.17/0.54 ~e21=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.54 fof(f223,plain,(
% 0.17/0.54 ~e22=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f8])).
% 0.17/0.54 fof(f240,definition,(
% 0.17/0.54 sP0_prd<=>(((op1(e10,e10)=e10&~op1(e10,e10)=e10)|(op1(e11,e11)=e10&~op1(e10,e10)=e11))|(op1(e12,e12)=e10&~op1(e10,e10)=e12))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.17/0.54 fof(f241,definition,(
% 0.17/0.54 sP1_prd<=>(((op1(e10,e10)=e11&~op1(e11,e11)=e10)|(op1(e11,e11)=e11&~op1(e11,e11)=e11))|(op1(e12,e12)=e11&~op1(e11,e11)=e12))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.17/0.54 fof(f242,definition,(
% 0.17/0.54 sP2_prd<=>(((op1(e10,e10)=e12&~op1(e12,e12)=e10)|(op1(e11,e11)=e12&~op1(e12,e12)=e11))|(op1(e12,e12)=e12&~op1(e12,e12)=e12))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.17/0.54 fof(f243,definition,(
% 0.17/0.54 sP3_prd<=>(((op1(e10,e10)=e13&~op1(e13,e13)=e10)|(op1(e11,e11)=e13&~op1(e13,e13)=e11))|(op1(e12,e12)=e13&~op1(e13,e13)=e12))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.17/0.54 fof(f244,plain,(
% 0.17/0.54 (((sP0_prd|(op1(e13,e13)=e10&~op1(e10,e10)=e13))&(sP1_prd|(op1(e13,e13)=e11&~op1(e11,e11)=e13)))&(sP2_prd|(op1(e13,e13)=e12&~op1(e12,e12)=e13)))&(sP3_prd|(op1(e13,e13)=e13&~op1(e13,e13)=e13))),
% 0.17/0.54 inference(formula_renaming,[status(thm)],[f10,f243,f242,f241,f240])).
% 0.17/0.54 fof(f245,plain,(
% 0.17/0.54 sP0_prd|op1(e13,e13)=e10),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.17/0.54 fof(f250,plain,(
% 0.17/0.54 sP2_prd|~op1(e12,e12)=e13),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.17/0.54 fof(f253,definition,(
% 0.17/0.54 sP4_prd<=>(((op2(e20,e20)=e20&~op2(e20,e20)=e20)|(op2(e21,e21)=e20&~op2(e20,e20)=e21))|(op2(e22,e22)=e20&~op2(e20,e20)=e22))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.17/0.54 fof(f254,definition,(
% 0.17/0.54 sP5_prd<=>(((op2(e20,e20)=e21&~op2(e21,e21)=e20)|(op2(e21,e21)=e21&~op2(e21,e21)=e21))|(op2(e22,e22)=e21&~op2(e21,e21)=e22))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.17/0.54 fof(f255,definition,(
% 0.17/0.54 sP6_prd<=>(((op2(e20,e20)=e22&~op2(e22,e22)=e20)|(op2(e21,e21)=e22&~op2(e22,e22)=e21))|(op2(e22,e22)=e22&~op2(e22,e22)=e22))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.17/0.54 fof(f256,definition,(
% 0.17/0.54 sP7_prd<=>(((op2(e20,e20)=e23&~op2(e23,e23)=e20)|(op2(e21,e21)=e23&~op2(e23,e23)=e21))|(op2(e22,e22)=e23&~op2(e23,e23)=e22))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.17/0.54 fof(f257,plain,(
% 0.17/0.54 (((sP4_prd|(op2(e23,e23)=e20&~op2(e20,e20)=e23))&(sP5_prd|(op2(e23,e23)=e21&~op2(e21,e21)=e23)))&(sP6_prd|(op2(e23,e23)=e22&~op2(e22,e22)=e23)))&(sP7_prd|(op2(e23,e23)=e23&~op2(e23,e23)=e23))),
% 0.17/0.54 inference(formula_renaming,[status(thm)],[f11,f256,f255,f254,f253])).
% 0.17/0.54 fof(f258,plain,(
% 0.17/0.54 sP4_prd|op2(e23,e23)=e20),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f257])).
% 0.17/0.54 fof(f263,plain,(
% 0.17/0.54 sP6_prd|~op2(e22,e22)=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f257])).
% 0.17/0.54 fof(f266,plain,(
% 0.17/0.54 e10=op1(op1(e12,e12),e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.54 fof(f267,plain,(
% 0.17/0.54 e11=op1(op1(e12,e12),op1(e12,e12))),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.54 fof(f268,plain,(
% 0.17/0.54 e13=op1(e12,e12)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f12])).
% 0.17/0.54 fof(f269,plain,(
% 0.17/0.54 e20=op2(op2(e22,e22),e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f13])).
% 0.17/0.54 fof(f270,plain,(
% 0.17/0.54 e21=op2(op2(e22,e22),op2(e22,e22))),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f13])).
% 0.17/0.54 fof(f271,plain,(
% 0.17/0.54 e23=op2(e22,e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f13])).
% 0.17/0.54 fof(f275,plain,(
% 0.17/0.54 h1(e13)=op2(e20,e20)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f14])).
% 0.17/0.54 fof(f277,plain,(
% 0.17/0.54 h2(e10)=op2(op2(e21,e21),e21)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f15])).
% 0.17/0.54 fof(f279,plain,(
% 0.17/0.54 h2(e13)=op2(e21,e21)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f15])).
% 0.17/0.54 fof(f280,plain,(
% 0.17/0.54 h3(e12)=e22),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f16])).
% 0.17/0.54 fof(f281,plain,(
% 0.17/0.54 h3(e10)=op2(op2(e22,e22),e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f16])).
% 0.17/0.54 fof(f282,plain,(
% 0.17/0.54 h3(e11)=op2(op2(e22,e22),op2(e22,e22))),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f16])).
% 0.17/0.54 fof(f283,plain,(
% 0.17/0.54 h3(e13)=op2(e22,e22)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f16])).
% 0.17/0.54 fof(f285,plain,(
% 0.17/0.54 h4(e10)=op2(op2(e23,e23),e23)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f17])).
% 0.17/0.54 fof(f286,plain,(
% 0.17/0.54 h4(e11)=op2(op2(e23,e23),op2(e23,e23))),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f17])).
% 0.17/0.54 fof(f287,plain,(
% 0.17/0.54 h4(e13)=op2(e23,e23)),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f17])).
% 0.17/0.54 fof(f288,plain,(
% 0.17/0.54 ((((((((((((((((((((((~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.17/0.54 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.17/0.54 fof(f289,definition,(
% 0.17/0.54 sP8_prd<=>(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.17/0.54 fof(f290,definition,(
% 0.17/0.54 sP9_prd<=>(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.17/0.54 fof(f291,definition,(
% 0.17/0.54 sP10_prd<=>(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.17/0.54 fof(f292,definition,(
% 0.17/0.54 sP11_prd<=>(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.17/0.54 fof(f293,definition,(
% 0.17/0.54 sP12_prd<=>(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.17/0.54 fof(f294,definition,(
% 0.17/0.54 sP13_prd<=>(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.17/0.54 fof(f295,definition,(
% 0.17/0.54 sP14_prd<=>(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.17/0.54 fof(f296,definition,(
% 0.17/0.54 sP15_prd<=>(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.17/0.54 fof(f297,definition,(
% 0.17/0.54 sP16_prd<=>(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 0.17/0.54 fof(f298,definition,(
% 0.17/0.54 sP17_prd<=>(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP17_prd])],[])).
% 0.17/0.54 fof(f299,definition,(
% 0.17/0.54 sP18_prd<=>(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.17/0.54 fof(f300,definition,(
% 0.17/0.54 sP19_prd<=>(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22)),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.17/0.54 fof(f301,plain,(
% 0.17/0.54 (((((((((((((((((((((~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)))|sP8_prd)|sP9_prd)|sP10_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)))|sP11_prd)|sP12_prd)|sP13_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)))|sP14_prd)|sP15_prd)|sP16_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)))|sP17_prd)|sP18_prd)|sP19_prd)|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23))),
% 0.17/0.54 inference(formula_renaming,[status(thm)],[f288,f300,f299,f298,f297,f296,f295,f294,f293,f292,f291,f290,f289])).
% 0.17/0.54 fof(f313,plain,(
% 0.17/0.54 ~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f301])).
% 0.17/0.54 fof(f318,definition,(
% 0.17/0.54 sP20_prd<=>((op1(e10,e10)=e10&~op1(e10,e10)=e10)|(op1(e11,e11)=e10&~op1(e10,e10)=e11))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.17/0.54 fof(f319,plain,(
% 0.17/0.54 sP0_prd<=>(sP20_prd|(op1(e12,e12)=e10&~op1(e10,e10)=e12))),
% 0.17/0.54 inference(formula_renaming,[status(thm)],[f240,f318])).
% 0.17/0.54 fof(f320,plain,(
% 0.17/0.54 (~sP0_prd|(sP20_prd|(op1(e12,e12)=e10&~op1(e10,e10)=e12)))&(sP0_prd|(~sP20_prd&(~op1(e12,e12)=e10|op1(e10,e10)=e12)))),
% 0.17/0.54 inference(NNF_transformation,[status(thm)],[f319])).
% 0.17/0.54 fof(f321,plain,(
% 0.17/0.54 ~sP0_prd|sP20_prd|op1(e12,e12)=e10),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f320])).
% 0.17/0.54 fof(f332,definition,(
% 0.17/0.54 sP22_prd<=>((op1(e10,e10)=e12&~op1(e12,e12)=e10)|(op1(e11,e11)=e12&~op1(e12,e12)=e11))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP22_prd])],[])).
% 0.17/0.54 fof(f333,plain,(
% 0.17/0.54 sP2_prd<=>(sP22_prd|(op1(e12,e12)=e12&~op1(e12,e12)=e12))),
% 0.17/0.54 inference(formula_renaming,[status(thm)],[f242,f332])).
% 0.17/0.54 fof(f334,plain,(
% 0.17/0.54 (~sP2_prd|(sP22_prd|(op1(e12,e12)=e12&~op1(e12,e12)=e12)))&(sP2_prd|(~sP22_prd&(~op1(e12,e12)=e12|op1(e12,e12)=e12)))),
% 0.17/0.54 inference(NNF_transformation,[status(thm)],[f333])).
% 0.17/0.54 fof(f335,plain,(
% 0.17/0.54 ~sP2_prd|sP22_prd|op1(e12,e12)=e12),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f334])).
% 0.17/0.54 fof(f346,definition,(
% 0.17/0.54 sP24_prd<=>((op2(e20,e20)=e20&~op2(e20,e20)=e20)|(op2(e21,e21)=e20&~op2(e20,e20)=e21))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP24_prd])],[])).
% 0.17/0.54 fof(f347,plain,(
% 0.17/0.54 sP4_prd<=>(sP24_prd|(op2(e22,e22)=e20&~op2(e20,e20)=e22))),
% 0.17/0.54 inference(formula_renaming,[status(thm)],[f253,f346])).
% 0.17/0.54 fof(f348,plain,(
% 0.17/0.54 (~sP4_prd|(sP24_prd|(op2(e22,e22)=e20&~op2(e20,e20)=e22)))&(sP4_prd|(~sP24_prd&(~op2(e22,e22)=e20|op2(e20,e20)=e22)))),
% 0.17/0.54 inference(NNF_transformation,[status(thm)],[f347])).
% 0.17/0.54 fof(f349,plain,(
% 0.17/0.54 ~sP4_prd|sP24_prd|op2(e22,e22)=e20),
% 0.17/0.54 inference(cnf_transformation,[status(thm)],[f348])).
% 0.17/0.54 fof(f360,definition,(
% 0.17/0.54 sP26_prd<=>((op2(e20,e20)=e22&~op2(e22,e22)=e20)|(op2(e21,e21)=e22&~op2(e22,e22)=e21))),
% 0.17/0.54 introduced(definition,[new_symbols(definition,[sP26_prd])],[])).
% 0.17/0.54 fof(f361,plain,(
% 0.17/0.54 sP6_prd<=>(sP26_prd|(op2(e22,e22)=e22&~op2(e22,e22)=e22))),
% 0.17/0.54 inference(formula_renaming,[status(thm)],[f255,f360])).
% 0.17/0.54 fof(f362,plain,(
% 0.17/0.54 (~sP6_prd|(sP26_prd|(op2(e22,e22)=e22&~op2(e22,e22)=e22)))&(sP6_prd|(~sP26_prd&(~op2(e22,e22)=e22|op2(e22,e22)=e22)))),
% 0.17/0.55 inference(NNF_transformation,[status(thm)],[f361])).
% 0.17/0.55 fof(f363,plain,(
% 0.17/0.55 ~sP6_prd|sP26_prd|op2(e22,e22)=e22),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f362])).
% 0.17/0.55 fof(f410,plain,(
% 0.17/0.55 (~sP14_prd|(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20))&(sP14_prd|(((h3(e10)=e20|h3(e11)=e20)|h3(e12)=e20)|h3(e13)=e20))),
% 0.17/0.55 inference(NNF_transformation,[status(thm)],[f295])).
% 0.17/0.55 fof(f411,plain,(
% 0.17/0.55 ~sP14_prd|~h3(e10)=e20),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f410])).
% 0.17/0.55 fof(f416,plain,(
% 0.17/0.55 (~sP15_prd|(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21))&(sP15_prd|(((h3(e10)=e21|h3(e11)=e21)|h3(e12)=e21)|h3(e13)=e21))),
% 0.17/0.55 inference(NNF_transformation,[status(thm)],[f296])).
% 0.17/0.55 fof(f418,plain,(
% 0.17/0.55 ~sP15_prd|~h3(e11)=e21),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f416])).
% 0.17/0.55 fof(f422,plain,(
% 0.17/0.55 (~sP16_prd|(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22))&(sP16_prd|(((h3(e10)=e22|h3(e11)=e22)|h3(e12)=e22)|h3(e13)=e22))),
% 0.17/0.55 inference(NNF_transformation,[status(thm)],[f297])).
% 0.17/0.55 fof(f425,plain,(
% 0.17/0.55 ~sP16_prd|~h3(e12)=e22),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f422])).
% 0.17/0.55 fof(f446,plain,(
% 0.17/0.55 (~sP20_prd|((op1(e10,e10)=e10&~op1(e10,e10)=e10)|(op1(e11,e11)=e10&~op1(e10,e10)=e11)))&(sP20_prd|((~op1(e10,e10)=e10|op1(e10,e10)=e10)&(~op1(e11,e11)=e10|op1(e10,e10)=e11)))),
% 0.17/0.55 inference(NNF_transformation,[status(thm)],[f318])).
% 0.17/0.55 fof(f447,plain,(
% 0.17/0.55 ~sP20_prd|op1(e10,e10)=e10|op1(e11,e11)=e10),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f446])).
% 0.17/0.55 fof(f449,plain,(
% 0.17/0.55 ~sP20_prd|~op1(e10,e10)=e10|op1(e11,e11)=e10),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f446])).
% 0.17/0.55 fof(f460,plain,(
% 0.17/0.55 (~sP22_prd|((op1(e10,e10)=e12&~op1(e12,e12)=e10)|(op1(e11,e11)=e12&~op1(e12,e12)=e11)))&(sP22_prd|((~op1(e10,e10)=e12|op1(e12,e12)=e10)&(~op1(e11,e11)=e12|op1(e12,e12)=e11)))),
% 0.17/0.55 inference(NNF_transformation,[status(thm)],[f332])).
% 0.17/0.55 fof(f461,plain,(
% 0.17/0.55 ~sP22_prd|op1(e10,e10)=e12|op1(e11,e11)=e12),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f460])).
% 0.17/0.55 fof(f474,plain,(
% 0.17/0.55 (~sP24_prd|((op2(e20,e20)=e20&~op2(e20,e20)=e20)|(op2(e21,e21)=e20&~op2(e20,e20)=e21)))&(sP24_prd|((~op2(e20,e20)=e20|op2(e20,e20)=e20)&(~op2(e21,e21)=e20|op2(e20,e20)=e21)))),
% 0.17/0.55 inference(NNF_transformation,[status(thm)],[f346])).
% 0.17/0.55 fof(f475,plain,(
% 0.17/0.55 ~sP24_prd|op2(e20,e20)=e20|op2(e21,e21)=e20),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f474])).
% 0.17/0.55 fof(f476,plain,(
% 0.17/0.55 ~sP24_prd|op2(e20,e20)=e20|~op2(e20,e20)=e21),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f474])).
% 0.17/0.55 fof(f477,plain,(
% 0.17/0.55 ~sP24_prd|~op2(e20,e20)=e20|op2(e21,e21)=e20),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f474])).
% 0.17/0.55 fof(f478,plain,(
% 0.17/0.55 ~sP24_prd|~op2(e20,e20)=e20|~op2(e20,e20)=e21),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f474])).
% 0.17/0.55 fof(f488,plain,(
% 0.17/0.55 (~sP26_prd|((op2(e20,e20)=e22&~op2(e22,e22)=e20)|(op2(e21,e21)=e22&~op2(e22,e22)=e21)))&(sP26_prd|((~op2(e20,e20)=e22|op2(e22,e22)=e20)&(~op2(e21,e21)=e22|op2(e22,e22)=e21)))),
% 0.17/0.55 inference(NNF_transformation,[status(thm)],[f360])).
% 0.17/0.55 fof(f489,plain,(
% 0.17/0.55 ~sP26_prd|op2(e20,e20)=e22|op2(e21,e21)=e22),
% 0.17/0.55 inference(cnf_transformation,[status(thm)],[f488])).
% 0.17/0.55 fof(f504,plain,(
% 0.17/0.55 e11=op1(op1(e12,e12),e13)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f268,f267])).
% 0.17/0.55 fof(f505,plain,(
% 0.17/0.55 e10=op1(e13,e12)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f268,f266])).
% 0.17/0.55 fof(f506,plain,(
% 0.17/0.55 sP2_prd|~e13=e13),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f268,f250])).
% 0.17/0.55 fof(f508,plain,(
% 0.17/0.55 ~op1(e12,e11)=e13),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f268,f155])).
% 0.17/0.55 fof(f511,plain,(
% 0.17/0.55 ~op1(e11,e12)=e13),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f268,f131])).
% 0.17/0.55 fof(f512,plain,(
% 0.17/0.55 ~op1(e10,e12)=e13),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f268,f129])).
% 0.17/0.55 fof(f515,plain,(
% 0.17/0.55 op1(e10,e12)=e12|op1(e11,e12)=e12|e13=e12|op1(e13,e12)=e12),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f268,f57])).
% 0.17/0.55 fof(f522,plain,(
% 0.17/0.55 e21=op2(op2(e22,e22),e23)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f270])).
% 0.17/0.55 fof(f523,plain,(
% 0.17/0.55 e20=op2(e23,e22)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f269])).
% 0.17/0.55 fof(f524,plain,(
% 0.17/0.55 sP6_prd|~e23=e23),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f263])).
% 0.17/0.55 fof(f525,plain,(
% 0.17/0.55 ~e23=op2(e22,e23)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f205])).
% 0.17/0.55 fof(f526,plain,(
% 0.17/0.55 ~op2(e22,e21)=e23),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f203])).
% 0.17/0.55 fof(f529,plain,(
% 0.17/0.55 ~op2(e21,e22)=e23),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f179])).
% 0.17/0.55 fof(f530,plain,(
% 0.17/0.55 ~op2(e20,e22)=e23),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f177])).
% 0.17/0.55 fof(f533,plain,(
% 0.17/0.55 op2(e20,e22)=e22|op2(e21,e22)=e22|e23=e22|op2(e23,e22)=e22),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f105])).
% 0.17/0.55 fof(f536,plain,(
% 0.17/0.55 op2(e22,e20)=e21|op2(e22,e21)=e21|e23=e21|op2(e22,e23)=e21),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f271,f102])).
% 0.17/0.55 fof(f544,plain,(
% 0.17/0.55 ~h1(e13)=op2(e20,e22)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f275,f189])).
% 0.17/0.55 fof(f546,plain,(
% 0.17/0.55 ~h1(e13)=op2(e23,e20)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f275,f166])).
% 0.17/0.55 fof(f553,plain,(
% 0.17/0.55 h1(e13)=e21|op2(e21,e20)=e21|op2(e22,e20)=e21|op2(e23,e20)=e21),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f275,f87])).
% 0.17/0.55 fof(f555,plain,(
% 0.17/0.55 h1(e13)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f275,f85])).
% 0.17/0.55 fof(f559,plain,(
% 0.17/0.55 h2(e10)=op2(h2(e13),e21)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f279,f277])).
% 0.17/0.55 fof(f561,plain,(
% 0.17/0.55 ~h2(e13)=op2(e21,e23)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f279,f198])).
% 0.17/0.55 fof(f563,plain,(
% 0.17/0.55 ~op2(e21,e20)=h2(e13)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f279,f194])).
% 0.17/0.55 fof(f567,plain,(
% 0.17/0.55 op2(e20,e21)=e23|h2(e13)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f279,f99])).
% 0.17/0.55 fof(f568,plain,(
% 0.17/0.55 op2(e21,e20)=e23|h2(e13)=e23|op2(e21,e22)=e23|op2(e21,e23)=e23),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f279,f98])).
% 0.17/0.55 fof(f576,plain,(
% 0.17/0.55 h3(e10)=e20),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f269,f281])).
% 0.17/0.55 fof(f577,plain,(
% 0.17/0.55 h3(e11)=e21),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f270,f282])).
% 0.17/0.55 fof(f578,plain,(
% 0.17/0.55 h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f271,f283])).
% 0.17/0.55 fof(f579,plain,(
% 0.17/0.55 h4(e11)=op2(op2(e23,e23),h4(e13))),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f287,f286])).
% 0.17/0.55 fof(f580,plain,(
% 0.17/0.55 h4(e10)=op2(h4(e13),e23)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f287,f285])).
% 0.17/0.55 fof(f583,plain,(
% 0.17/0.55 sP4_prd|h4(e13)=e20),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f287,f258])).
% 0.17/0.55 fof(f584,plain,(
% 0.17/0.55 ~op2(e23,e22)=h4(e13)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f287,f211])).
% 0.17/0.55 fof(f586,plain,(
% 0.17/0.55 ~op2(e23,e20)=h4(e13)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f287,f208])).
% 0.17/0.55 fof(f587,plain,(
% 0.17/0.55 ~op2(e22,e23)=h4(e13)),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f287,f187])).
% 0.17/0.55 fof(f593,plain,(
% 0.17/0.55 op2(e23,e20)=e22|op2(e23,e21)=e22|op2(e23,e22)=e22|h4(e13)=e22),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f287,f112])).
% 0.17/0.55 fof(f596,plain,(
% 0.17/0.55 op2(e20,e23)=e20|op2(e21,e23)=e20|op2(e22,e23)=e20|h4(e13)=e20),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f287,f109])).
% 0.17/0.55 fof(f809,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=op2(e20,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f313])).
% 0.17/0.55 fof(f810,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=op2(e20,e20)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f809])).
% 0.17/0.55 fof(f811,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f275,f810])).
% 0.17/0.55 fof(f812,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f811])).
% 0.17/0.55 fof(f813,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f812])).
% 0.17/0.55 fof(f814,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f813])).
% 0.17/0.55 fof(f815,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f814])).
% 0.17/0.55 fof(f816,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f815])).
% 0.17/0.55 fof(f817,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f816])).
% 0.17/0.55 fof(f818,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f817])).
% 0.17/0.55 fof(f819,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f818])).
% 0.17/0.55 fof(f820,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=op2(e21,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f819])).
% 0.17/0.55 fof(f821,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=op2(e21,e21)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f820])).
% 0.17/0.55 fof(f822,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f279,f821])).
% 0.17/0.55 fof(f823,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f822])).
% 0.17/0.55 fof(f824,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f823])).
% 0.17/0.55 fof(f825,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f824])).
% 0.17/0.55 fof(f826,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f825])).
% 0.17/0.55 fof(f827,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f826])).
% 0.17/0.55 fof(f828,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f827])).
% 0.17/0.55 fof(f829,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f828])).
% 0.17/0.55 fof(f830,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f829])).
% 0.17/0.55 fof(f831,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(e13)=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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f268,f830])).
% 0.17/0.55 fof(f832,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f831])).
% 0.17/0.55 fof(f833,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=op2(e22,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f832])).
% 0.17/0.55 fof(f834,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=op2(e22,e22)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f833])).
% 0.17/0.55 fof(f835,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f271,f834])).
% 0.17/0.55 fof(f836,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f835])).
% 0.17/0.55 fof(f837,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f836])).
% 0.17/0.55 fof(f838,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f837])).
% 0.17/0.55 fof(f839,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~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))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f838])).
% 0.17/0.55 fof(f840,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),h3(e12))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f839])).
% 0.17/0.55 fof(f841,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(h3(e13),h3(e12))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f840])).
% 0.17/0.55 fof(f842,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,h3(e12))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f841])).
% 0.17/0.55 fof(f843,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f842])).
% 0.17/0.55 fof(f844,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=op2(e23,h3(e13))|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f843])).
% 0.17/0.55 fof(f845,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=op2(e23,e23)|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f844])).
% 0.17/0.55 fof(f846,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=h4(e13)|sP14_prd|sP15_prd|sP16_prd|~h3(e13)=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f287,f845])).
% 0.17/0.55 fof(f847,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=h4(e13)|sP14_prd|sP15_prd|sP16_prd|~e23=e23),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f578,f846])).
% 0.17/0.55 fof(f848,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=h4(e13)|sP14_prd|sP15_prd|sP16_prd),
% 0.17/0.55 inference(duplicate_literals_removal,[status(thm)],[f847])).
% 0.17/0.55 fof(f849,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=h4(e13)|sP14_prd|sP15_prd|sP16_prd),
% 0.17/0.55 inference(trivial_equality_resolution,[status(thm)],[f848])).
% 0.17/0.55 fof(f895,plain,(
% 0.17/0.55 ~sP0_prd|sP20_prd|e13=e10),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f268,f321])).
% 0.17/0.55 fof(f896,plain,(
% 0.17/0.55 ~sP0_prd|sP20_prd),
% 0.17/0.55 inference(forward_subsumption_resolution,[status(thm)],[f895,f214])).
% 0.17/0.55 fof(f901,plain,(
% 0.17/0.55 ~sP2_prd|sP22_prd|e13=e12),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f268,f335])).
% 0.17/0.55 fof(f902,plain,(
% 0.17/0.55 ~sP2_prd|sP22_prd),
% 0.17/0.55 inference(forward_subsumption_resolution,[status(thm)],[f901,f217])).
% 0.17/0.55 fof(f907,plain,(
% 0.17/0.55 ~sP4_prd|sP24_prd|e23=e20),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f271,f349])).
% 0.17/0.55 fof(f908,plain,(
% 0.17/0.55 ~sP4_prd|sP24_prd),
% 0.17/0.55 inference(forward_subsumption_resolution,[status(thm)],[f907,f220])).
% 0.17/0.55 fof(f917,plain,(
% 0.17/0.55 ~sP6_prd|sP26_prd|e23=e22),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f271,f363])).
% 0.17/0.55 fof(f918,plain,(
% 0.17/0.55 ~sP6_prd|sP26_prd),
% 0.17/0.55 inference(forward_subsumption_resolution,[status(thm)],[f917,f223])).
% 0.17/0.55 fof(f947,plain,(
% 0.17/0.55 ~sP14_prd|~e20=e20),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f576,f411])).
% 0.17/0.55 fof(f948,plain,(
% 0.17/0.55 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=h4(e13)|sP15_prd|sP16_prd),
% 0.17/0.55 inference(backward_subsumption_resolution,[status(thm)],[f849,f949])).
% 0.17/0.55 fof(f949,plain,(
% 0.17/0.55 ~sP14_prd),
% 0.17/0.55 inference(trivial_equality_resolution,[status(thm)],[f947])).
% 0.17/0.55 fof(f954,plain,(
% 0.17/0.55 ~sP15_prd|~e21=e21),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f577,f418])).
% 0.17/0.55 fof(f955,plain,(
% 0.17/0.55 ~sP15_prd),
% 0.17/0.55 inference(trivial_equality_resolution,[status(thm)],[f954])).
% 0.17/0.55 fof(f961,plain,(
% 0.17/0.55 ~sP16_prd|~e22=e22),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f280,f425])).
% 0.17/0.55 fof(f962,plain,(
% 0.17/0.55 ~sP16_prd),
% 0.17/0.55 inference(trivial_equality_resolution,[status(thm)],[f961])).
% 0.17/0.55 fof(f975,plain,(
% 0.17/0.55 ~sP20_prd|op1(e11,e11)=e10),
% 0.17/0.55 inference(forward_subsumption_resolution,[status(thm)],[f449,f447])).
% 0.17/0.55 fof(f987,plain,(
% 0.17/0.55 ~sP24_prd|h1(e13)=e20|op2(e21,e21)=e20),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f275,f475])).
% 0.17/0.55 fof(f988,plain,(
% 0.17/0.55 ~sP24_prd|h1(e13)=e20|h2(e13)=e20),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f279,f987])).
% 0.17/0.55 fof(f989,plain,(
% 0.17/0.55 ~sP24_prd|h1(e13)=e20|~op2(e20,e20)=e21),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f275,f476])).
% 0.17/0.55 fof(f990,plain,(
% 0.17/0.55 ~sP24_prd|h1(e13)=e20|~h1(e13)=e21),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f275,f989])).
% 0.17/0.55 fof(f991,plain,(
% 0.17/0.55 ~sP24_prd|~h1(e13)=e20|op2(e21,e21)=e20),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f275,f477])).
% 0.17/0.55 fof(f992,plain,(
% 0.17/0.55 ~sP24_prd|~h1(e13)=e20|h2(e13)=e20),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f279,f991])).
% 0.17/0.55 fof(f993,plain,(
% 0.17/0.55 ~sP24_prd|h2(e13)=e20),
% 0.17/0.55 inference(forward_subsumption_resolution,[status(thm)],[f992,f988])).
% 0.17/0.55 fof(f994,plain,(
% 0.17/0.55 ~sP24_prd|~h1(e13)=e20|~op2(e20,e20)=e21),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f275,f478])).
% 0.17/0.55 fof(f995,plain,(
% 0.17/0.55 ~sP24_prd|~h1(e13)=e20|~h1(e13)=e21),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f275,f994])).
% 0.17/0.55 fof(f996,plain,(
% 0.17/0.55 ~sP24_prd|~h1(e13)=e21),
% 0.17/0.55 inference(forward_subsumption_resolution,[status(thm)],[f995,f990])).
% 0.17/0.55 fof(f1011,plain,(
% 0.17/0.55 ~sP26_prd|h1(e13)=e22|op2(e21,e21)=e22),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f275,f489])).
% 0.17/0.55 fof(f1012,plain,(
% 0.17/0.55 ~sP26_prd|h1(e13)=e22|h2(e13)=e22),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f279,f1011])).
% 0.17/0.55 fof(f1046,plain,(
% 0.17/0.55 sP0_prd|e11=e10),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f1062,f245])).
% 0.17/0.55 fof(f1048,plain,(
% 0.17/0.55 ~op1(e13,e11)=e11),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f1062,f162])).
% 0.17/0.55 fof(f1049,plain,(
% 0.17/0.55 ~op1(e13,e10)=e11),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f1062,f160])).
% 0.17/0.55 fof(f1051,plain,(
% 0.17/0.55 ~op1(e11,e13)=e11),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f1062,f138])).
% 0.17/0.55 fof(f1055,plain,(
% 0.17/0.55 op1(e10,e13)=e12|op1(e11,e13)=e12|op1(e12,e13)=e12|e11=e12),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f1062,f65])).
% 0.17/0.55 fof(f1056,plain,(
% 0.17/0.55 op1(e13,e10)=e12|op1(e13,e11)=e12|op1(e13,e12)=e12|e11=e12),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f1062,f64])).
% 0.17/0.55 fof(f1062,plain,(
% 0.17/0.55 e11=op1(e13,e13)),
% 0.17/0.55 inference(forward_demodulation,[status(thm)],[f268,f504])).
% 0.17/0.55 fof(f1064,plain,(
% 0.17/0.55 ~op1(e13,e10)=e10),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f505,f159])).
% 0.17/0.55 fof(f1066,plain,(
% 0.17/0.55 ~op1(e10,e12)=e10),
% 0.17/0.55 inference(backward_demodulation,[status(thm)],[f505,f130])).
% 0.17/0.55 fof(f1068,plain,(
% 0.17/0.55 sP22_prd),
% 0.17/0.55 inference(backward_subsumption_resolution,[status(thm)],[f902,f1069])).
% 0.17/0.55 fof(f1069,plain,(
% 0.17/0.56 sP2_prd),
% 0.17/0.56 inference(trivial_equality_resolution,[status(thm)],[f506])).
% 0.17/0.56 fof(f1071,plain,(
% 0.17/0.56 op1(e10,e11)=e13|op1(e11,e11)=e13|op1(e13,e11)=e13),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f51,f508])).
% 0.17/0.56 fof(f1076,plain,(
% 0.17/0.56 op1(e11,e10)=e13|op1(e11,e11)=e13|op1(e11,e13)=e13),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f50,f511])).
% 0.17/0.56 fof(f1079,plain,(
% 0.17/0.56 op1(e10,e12)=e10|op1(e10,e12)=e11|op1(e10,e12)=e12),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f22,f512])).
% 0.17/0.56 fof(f1080,plain,(
% 0.17/0.56 op1(e10,e12)=e12|op1(e11,e12)=e12|e13=e12|e10=e12),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f505,f515])).
% 0.17/0.56 fof(f1081,plain,(
% 0.17/0.56 op1(e10,e12)=e12|op1(e11,e12)=e12|e10=e12),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1080,f217])).
% 0.17/0.56 fof(f1087,plain,(
% 0.17/0.56 h4(e13)=e21),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1088,f287])).
% 0.17/0.56 fof(f1088,plain,(
% 0.17/0.56 e21=op2(e23,e23)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f271,f522])).
% 0.17/0.56 fof(f1090,plain,(
% 0.17/0.56 ~op2(e23,e20)=e20),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f523,f207])).
% 0.17/0.56 fof(f1092,plain,(
% 0.17/0.56 ~op2(e20,e22)=e20),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f523,f178])).
% 0.17/0.56 fof(f1094,plain,(
% 0.17/0.56 sP26_prd),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f918,f1095])).
% 0.17/0.56 fof(f1095,plain,(
% 0.17/0.56 sP6_prd),
% 0.17/0.56 inference(trivial_equality_resolution,[status(thm)],[f524])).
% 0.17/0.56 fof(f1096,plain,(
% 0.17/0.56 op2(e22,e23)=e20|op2(e22,e23)=e21|op2(e22,e23)=e22),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f79,f525])).
% 0.17/0.56 fof(f1101,plain,(
% 0.17/0.56 op2(e20,e22)=e20|op2(e20,e22)=e21|op2(e20,e22)=e22),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f70,f530])).
% 0.17/0.56 fof(f1102,plain,(
% 0.17/0.56 op2(e20,e22)=e22|op2(e21,e22)=e22|e23=e22|e20=e22),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f523,f533])).
% 0.17/0.56 fof(f1103,plain,(
% 0.17/0.56 op2(e20,e22)=e22|op2(e21,e22)=e22|e20=e22),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1102,f223])).
% 0.17/0.56 fof(f1107,plain,(
% 0.17/0.56 op2(e22,e20)=e21|op2(e22,e21)=e21|op2(e22,e23)=e21),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f536,f222])).
% 0.17/0.56 fof(f1116,plain,(
% 0.17/0.56 op2(e20,e21)=e23|h2(e13)=e23|op2(e23,e21)=e23),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f567,f526])).
% 0.17/0.56 fof(f1117,plain,(
% 0.17/0.56 op2(e21,e20)=e23|h2(e13)=e23|op2(e21,e23)=e23),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f568,f529])).
% 0.17/0.56 fof(f1121,plain,(
% 0.17/0.56 h4(e11)=op2(e21,h4(e13))),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1088,f579])).
% 0.17/0.56 fof(f1122,plain,(
% 0.17/0.56 sP4_prd),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f583,f1125])).
% 0.17/0.56 fof(f1125,plain,(
% 0.17/0.56 ~e20=h4(e13)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f523,f584])).
% 0.17/0.56 fof(f1129,plain,(
% 0.17/0.56 op2(e23,e20)=e22|op2(e23,e21)=e22|e20=e22|h4(e13)=e22),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f523,f593])).
% 0.17/0.56 fof(f1130,plain,(
% 0.17/0.56 op2(e23,e20)=e22|op2(e23,e21)=e22|h4(e13)=e22),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1129,f219])).
% 0.17/0.56 fof(f1133,plain,(
% 0.17/0.56 op2(e20,e23)=e20|op2(e21,e23)=e20|op2(e22,e23)=e20),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f596,f1125])).
% 0.17/0.56 fof(f1165,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(e10)=op2(e23,e22)|~h3(op1(e13,e13))=h4(e13)|sP15_prd|sP16_prd),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f505,f948])).
% 0.17/0.56 fof(f1166,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e20=op2(e23,e22)|~h3(op1(e13,e13))=h4(e13)|sP15_prd|sP16_prd),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f576,f1165])).
% 0.17/0.56 fof(f1167,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e20=e20|~h3(op1(e13,e13))=h4(e13)|sP15_prd|sP16_prd),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f523,f1166])).
% 0.17/0.56 fof(f1168,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e20=e20|~h3(e11)=h4(e13)|sP15_prd|sP16_prd),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1062,f1167])).
% 0.17/0.56 fof(f1169,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e20=e20|~e21=h4(e13)|sP15_prd|sP16_prd),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f577,f1168])).
% 0.17/0.56 fof(f1170,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e21=h4(e13)|sP15_prd|sP16_prd),
% 0.17/0.56 inference(trivial_equality_resolution,[status(thm)],[f1169])).
% 0.17/0.56 fof(f1171,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e21=h4(e13)|sP16_prd),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1170,f955])).
% 0.17/0.56 fof(f1179,plain,(
% 0.17/0.56 sP20_prd),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f896,f1180])).
% 0.17/0.56 fof(f1180,plain,(
% 0.17/0.56 sP0_prd),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1046,f212])).
% 0.17/0.56 fof(f1182,plain,(
% 0.17/0.56 op1(e10,e11)=e11|op1(e11,e11)=e11|op1(e12,e11)=e11),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f47,f1048])).
% 0.17/0.56 fof(f1185,plain,(
% 0.17/0.56 op1(e13,e10)=e10|op1(e13,e10)=e12|op1(e13,e10)=e13),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f32,f1049])).
% 0.17/0.56 fof(f1187,plain,(
% 0.17/0.56 op1(e11,e10)=e11|op1(e11,e11)=e11|op1(e11,e12)=e11),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f46,f1051])).
% 0.17/0.56 fof(f1194,plain,(
% 0.17/0.56 op1(e10,e13)=e12|op1(e11,e13)=e12|op1(e12,e13)=e12),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1055,f215])).
% 0.17/0.56 fof(f1195,plain,(
% 0.17/0.56 op1(e13,e10)=e12|op1(e13,e11)=e12|e10=e12|e11=e12),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f505,f1056])).
% 0.17/0.56 fof(f1196,plain,(
% 0.17/0.56 op1(e13,e10)=e12|op1(e13,e11)=e12|e11=e12),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1195,f213])).
% 0.17/0.56 fof(f1200,plain,(
% 0.17/0.56 op1(e10,e10)=e10|op1(e11,e10)=e10|op1(e12,e10)=e10),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f37,f1064])).
% 0.17/0.56 fof(f1202,plain,(
% 0.17/0.56 op1(e10,e10)=e10|op1(e10,e11)=e10|op1(e10,e13)=e10),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f36,f1066])).
% 0.17/0.56 fof(f1203,plain,(
% 0.17/0.56 op1(e10,e10)=e12|op1(e11,e11)=e12),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f461,f1068])).
% 0.17/0.56 fof(f1206,plain,(
% 0.17/0.56 op1(e10,e12)=e11|op1(e10,e12)=e12),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1079,f1066])).
% 0.17/0.56 fof(f1208,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e21=e21|sP16_prd),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1087,f1171])).
% 0.17/0.56 fof(f1211,plain,(
% 0.17/0.56 op2(e23,e20)=e22|op2(e23,e21)=e22|e21=e22),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1087,f1130])).
% 0.17/0.56 fof(f1217,plain,(
% 0.17/0.56 ~op2(e22,e23)=e21),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1087,f587])).
% 0.17/0.56 fof(f1218,plain,(
% 0.17/0.56 ~op2(e23,e20)=e21),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1087,f586])).
% 0.17/0.56 fof(f1222,plain,(
% 0.17/0.56 h4(e10)=op2(e21,e23)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1087,f580])).
% 0.17/0.56 fof(f1223,plain,(
% 0.17/0.56 h4(e11)=op2(e21,e21)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1087,f1121])).
% 0.17/0.56 fof(f1233,plain,(
% 0.17/0.56 h1(e13)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f555,f1090])).
% 0.17/0.56 fof(f1234,plain,(
% 0.17/0.56 op2(e23,e20)=e21|op2(e23,e20)=e22|op2(e23,e20)=e23),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f80,f1090])).
% 0.17/0.56 fof(f1237,plain,(
% 0.17/0.56 h1(e13)=e22|h2(e13)=e22),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1012,f1094])).
% 0.17/0.56 fof(f1239,plain,(
% 0.17/0.56 op2(e20,e22)=e21|op2(e20,e22)=e22),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1101,f1092])).
% 0.17/0.56 fof(f1240,plain,(
% 0.17/0.56 sP24_prd),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f908,f1122])).
% 0.17/0.56 fof(f1242,plain,(
% 0.17/0.56 op1(e11,e11)=e10),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f975,f1179])).
% 0.17/0.56 fof(f1244,plain,(
% 0.17/0.56 op1(e13,e10)=e12|op1(e13,e10)=e13),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1185,f1064])).
% 0.17/0.56 fof(f1252,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|sP16_prd),
% 0.17/0.56 inference(trivial_equality_resolution,[status(thm)],[f1208])).
% 0.17/0.56 fof(f1253,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1252,f962])).
% 0.17/0.56 fof(f1254,plain,(
% 0.17/0.56 op2(e23,e20)=e22|op2(e23,e21)=e22),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1211,f221])).
% 0.17/0.56 fof(f1262,plain,(
% 0.17/0.56 op2(e22,e23)=e20|op2(e22,e23)=e22),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1096,f1217])).
% 0.17/0.56 fof(f1263,plain,(
% 0.17/0.56 op2(e22,e20)=e21|op2(e22,e21)=e21),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1107,f1217])).
% 0.17/0.56 fof(f1264,plain,(
% 0.17/0.56 h1(e13)=e21|op2(e21,e20)=e21|op2(e22,e20)=e21),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f553,f1218])).
% 0.17/0.56 fof(f1269,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1222,f1253])).
% 0.17/0.56 fof(f1270,plain,(
% 0.17/0.56 op2(e20,e23)=e20|h4(e10)=e20|op2(e22,e23)=e20),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1222,f1133])).
% 0.17/0.56 fof(f1272,plain,(
% 0.17/0.56 op2(e21,e20)=e23|h2(e13)=e23|h4(e10)=e23),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1222,f1117])).
% 0.17/0.56 fof(f1273,plain,(
% 0.17/0.56 ~h2(e13)=h4(e10)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1222,f561])).
% 0.17/0.56 fof(f1278,plain,(
% 0.17/0.56 h2(e13)=h4(e11)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1223,f279])).
% 0.17/0.56 fof(f1284,plain,(
% 0.17/0.56 op2(e23,e20)=e22|op2(e23,e20)=e23),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1234,f1218])).
% 0.17/0.56 fof(f1286,plain,(
% 0.17/0.56 ~h1(e13)=e21),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f996,f1240])).
% 0.17/0.56 fof(f1287,plain,(
% 0.17/0.56 h2(e13)=e20),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f993,f1240])).
% 0.17/0.56 fof(f1292,plain,(
% 0.17/0.56 op1(e10,e10)=e12|e10=e12),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1242,f1203])).
% 0.17/0.56 fof(f1295,plain,(
% 0.17/0.56 op1(e11,e10)=e11|e10=e11|op1(e11,e12)=e11),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1242,f1187])).
% 0.17/0.56 fof(f1296,plain,(
% 0.17/0.56 op1(e10,e11)=e11|e10=e11|op1(e12,e11)=e11),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1242,f1182])).
% 0.17/0.56 fof(f1297,plain,(
% 0.17/0.56 op1(e11,e10)=e13|e10=e13|op1(e11,e13)=e13),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1242,f1076])).
% 0.17/0.56 fof(f1298,plain,(
% 0.17/0.56 op1(e10,e11)=e13|e10=e13|op1(e13,e11)=e13),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1242,f1071])).
% 0.17/0.56 fof(f1319,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(e10)=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1242,f1269])).
% 0.17/0.56 fof(f1320,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e20=h2(e13)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f576,f1319])).
% 0.17/0.56 fof(f1321,plain,(
% 0.17/0.56 ~h4(e11)=h4(e10)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1278,f1273])).
% 0.17/0.56 fof(f1322,plain,(
% 0.17/0.56 op2(e21,e20)=e23|h4(e11)=e23|h4(e10)=e23),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1278,f1272])).
% 0.17/0.56 fof(f1324,plain,(
% 0.17/0.56 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e20=h4(e11)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1278,f1320])).
% 0.17/0.56 fof(f1327,plain,(
% 0.17/0.56 h1(e13)=e22|h4(e11)=e22),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1278,f1237])).
% 0.17/0.56 fof(f1332,plain,(
% 0.17/0.56 op2(e20,e21)=e23|h4(e11)=e23|op2(e23,e21)=e23),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1278,f1116])).
% 0.17/0.56 fof(f1336,plain,(
% 0.17/0.56 ~op2(e21,e20)=h4(e11)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1278,f563])).
% 0.17/0.56 fof(f1339,plain,(
% 0.17/0.56 h2(e10)=op2(h4(e11),e21)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1278,f559])).
% 0.17/0.56 fof(f1350,plain,(
% 0.17/0.56 op2(e21,e20)=e21|op2(e22,e20)=e21),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1264,f1286])).
% 0.17/0.56 fof(f1355,plain,(
% 0.17/0.56 e20=h4(e11)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1287,f1278])).
% 0.17/0.56 fof(f1360,plain,(
% 0.17/0.56 e12=e10|op1(e10,e11)=e10|op1(e10,e13)=e10),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1374,f1202])).
% 0.17/0.56 fof(f1361,plain,(
% 0.17/0.56 e12=e10|op1(e11,e10)=e10|op1(e12,e10)=e10),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1374,f1200])).
% 0.17/0.56 fof(f1366,plain,(
% 0.17/0.56 ~e12=op1(e10,e13)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1374,f142])).
% 0.17/0.56 fof(f1367,plain,(
% 0.17/0.56 ~e12=op1(e10,e12)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1374,f141])).
% 0.17/0.56 fof(f1369,plain,(
% 0.17/0.56 ~e12=op1(e13,e10)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1374,f118])).
% 0.17/0.56 fof(f1374,plain,(
% 0.17/0.56 op1(e10,e10)=e12),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1292,f213])).
% 0.17/0.56 fof(f1375,plain,(
% 0.17/0.56 op1(e11,e10)=e11|op1(e11,e12)=e11),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1295,f212])).
% 0.17/0.56 fof(f1376,plain,(
% 0.17/0.56 op1(e10,e11)=e11|op1(e12,e11)=e11),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1296,f212])).
% 0.17/0.56 fof(f1377,plain,(
% 0.17/0.56 op1(e11,e10)=e13|op1(e11,e13)=e13),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1297,f214])).
% 0.17/0.56 fof(f1378,plain,(
% 0.17/0.56 op1(e10,e11)=e13|op1(e13,e11)=e13),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1298,f214])).
% 0.17/0.56 fof(f1416,plain,(
% 0.17/0.56 ~h3(e12)=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e20=h4(e11)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1374,f1324])).
% 0.17/0.56 fof(f1417,plain,(
% 0.17/0.56 ~e22=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e20=h4(e11)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f280,f1416])).
% 0.17/0.56 fof(f1425,plain,(
% 0.17/0.56 h2(e10)=op2(e20,e21)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1355,f1339])).
% 0.17/0.56 fof(f1428,plain,(
% 0.17/0.56 ~op2(e21,e20)=e20),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1355,f1336])).
% 0.17/0.56 fof(f1432,plain,(
% 0.17/0.56 op2(e20,e21)=e23|e20=e23|op2(e23,e21)=e23),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1355,f1332])).
% 0.17/0.56 fof(f1436,plain,(
% 0.17/0.56 h1(e13)=e22|e20=e22),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1355,f1327])).
% 0.17/0.56 fof(f1439,plain,(
% 0.17/0.56 ~e22=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e20=e20|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1355,f1417])).
% 0.17/0.56 fof(f1441,plain,(
% 0.17/0.56 op2(e21,e20)=e23|e20=e23|h4(e10)=e23),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1355,f1322])).
% 0.17/0.56 fof(f1442,plain,(
% 0.17/0.56 ~e20=h4(e10)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1355,f1321])).
% 0.17/0.56 fof(f1458,plain,(
% 0.17/0.56 op1(e10,e11)=e10|op1(e10,e13)=e10),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1360,f213])).
% 0.17/0.56 fof(f1459,plain,(
% 0.17/0.56 op1(e11,e10)=e10|op1(e12,e10)=e10),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1361,f213])).
% 0.17/0.56 fof(f1464,plain,(
% 0.17/0.56 op1(e11,e13)=e12|op1(e12,e13)=e12),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1194,f1366])).
% 0.17/0.56 fof(f1465,plain,(
% 0.17/0.56 op1(e10,e12)=e11),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1206,f1367])).
% 0.17/0.56 fof(f1466,plain,(
% 0.17/0.56 op1(e11,e12)=e12|e10=e12),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1081,f1367])).
% 0.17/0.56 fof(f1468,plain,(
% 0.17/0.56 op1(e13,e10)=e13),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1244,f1369])).
% 0.17/0.56 fof(f1469,plain,(
% 0.17/0.56 op1(e13,e11)=e12|e11=e12),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1196,f1369])).
% 0.17/0.56 fof(f1490,plain,(
% 0.17/0.56 h1(e13)=e20|op2(e22,e20)=e20),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1233,f1428])).
% 0.17/0.56 fof(f1495,plain,(
% 0.17/0.56 h2(e10)=e23|e20=e23|op2(e23,e21)=e23),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1425,f1432])).
% 0.17/0.56 fof(f1496,plain,(
% 0.17/0.56 h2(e10)=e23|op2(e23,e21)=e23),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1495,f220])).
% 0.17/0.56 fof(f1510,plain,(
% 0.17/0.56 ~e22=op2(e23,e20)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1517,f546])).
% 0.17/0.56 fof(f1511,plain,(
% 0.17/0.56 ~e22=op2(e20,e22)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1517,f544])).
% 0.17/0.56 fof(f1517,plain,(
% 0.17/0.56 h1(e13)=e22),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1436,f219])).
% 0.17/0.56 fof(f1521,plain,(
% 0.17/0.56 ~e22=e22|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e20=e20|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1517,f1439])).
% 0.17/0.56 fof(f1522,plain,(
% 0.17/0.56 ~e22=e22|~h3(op1(e10,e11))=h2(e10)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e20=e20|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1425,f1521])).
% 0.17/0.56 fof(f1523,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(trivial_equality_resolution,[status(thm)],[f1522])).
% 0.17/0.56 fof(f1525,plain,(
% 0.17/0.56 op2(e21,e20)=e23|h4(e10)=e23),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1441,f220])).
% 0.17/0.56 fof(f1526,plain,(
% 0.17/0.56 op2(e20,e23)=e20|op2(e22,e23)=e20),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1270,f1442])).
% 0.17/0.56 fof(f1531,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~h3(e11)=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1465,f1523])).
% 0.17/0.56 fof(f1538,plain,(
% 0.17/0.56 ~op1(e10,e11)=e11),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1465,f143])).
% 0.17/0.56 fof(f1540,plain,(
% 0.17/0.56 op1(e11,e10)=e11|e12=e11),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1546,f1375])).
% 0.17/0.56 fof(f1544,plain,(
% 0.17/0.56 ~e12=op1(e11,e13)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1546,f151])).
% 0.17/0.56 fof(f1546,plain,(
% 0.17/0.56 op1(e11,e12)=e12),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1466,f213])).
% 0.17/0.56 fof(f1556,plain,(
% 0.17/0.56 op1(e10,e11)=e13|e12=e13),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1562,f1378])).
% 0.17/0.56 fof(f1562,plain,(
% 0.17/0.56 op1(e13,e11)=e12),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1469,f215])).
% 0.17/0.56 fof(f1593,plain,(
% 0.17/0.56 e22=e20|op2(e22,e20)=e20),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1517,f1490])).
% 0.17/0.56 fof(f1594,plain,(
% 0.17/0.56 op2(e21,e20)=e21|e20=e21),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1603,f1350])).
% 0.17/0.56 fof(f1595,plain,(
% 0.17/0.56 e20=e21|op2(e22,e21)=e21),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1603,f1263])).
% 0.17/0.56 fof(f1599,plain,(
% 0.17/0.56 ~e20=op2(e22,e23)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1603,f202])).
% 0.17/0.56 fof(f1603,plain,(
% 0.17/0.56 op2(e22,e20)=e20),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1593,f219])).
% 0.17/0.56 fof(f1644,plain,(
% 0.17/0.56 op2(e23,e20)=e23),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1284,f1510])).
% 0.17/0.56 fof(f1645,plain,(
% 0.17/0.56 op2(e23,e21)=e22),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1254,f1510])).
% 0.17/0.56 fof(f1646,plain,(
% 0.17/0.56 op2(e20,e22)=e21),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1239,f1511])).
% 0.17/0.56 fof(f1647,plain,(
% 0.17/0.56 op2(e21,e22)=e22|e20=e22),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1103,f1511])).
% 0.17/0.56 fof(f1671,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e12))=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f577,f1531])).
% 0.17/0.56 fof(f1672,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(e12)=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1546,f1671])).
% 0.17/0.56 fof(f1673,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f280,f1672])).
% 0.17/0.56 fof(f1674,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1603,f1673])).
% 0.17/0.56 fof(f1675,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~h3(e13)=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1468,f1674])).
% 0.17/0.56 fof(f1676,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f578,f1675])).
% 0.17/0.56 fof(f1677,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h3(e12)=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1562,f1676])).
% 0.17/0.56 fof(f1678,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f280,f1677])).
% 0.17/0.56 fof(f1680,plain,(
% 0.17/0.56 op1(e12,e11)=e11),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1376,f1538])).
% 0.17/0.56 fof(f1682,plain,(
% 0.17/0.56 ~h3(op1(e10,e11))=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(e11)=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1692,f1678])).
% 0.17/0.56 fof(f1686,plain,(
% 0.17/0.56 e11=e10|op1(e12,e10)=e10),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1692,f1459])).
% 0.17/0.56 fof(f1688,plain,(
% 0.17/0.56 e11=e13|op1(e11,e13)=e13),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1692,f1377])).
% 0.17/0.56 fof(f1692,plain,(
% 0.17/0.56 op1(e11,e10)=e11),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1540,f215])).
% 0.17/0.56 fof(f1693,plain,(
% 0.17/0.56 op1(e12,e13)=e12),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1464,f1544])).
% 0.17/0.56 fof(f1701,plain,(
% 0.17/0.56 e13=e10|op1(e10,e13)=e10),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1705,f1458])).
% 0.17/0.56 fof(f1705,plain,(
% 0.17/0.56 op1(e10,e11)=e13),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1556,f217])).
% 0.17/0.56 fof(f1743,plain,(
% 0.17/0.56 e21=e23|h4(e10)=e23),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1749,f1525])).
% 0.17/0.56 fof(f1749,plain,(
% 0.17/0.56 op2(e21,e20)=e21),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1594,f218])).
% 0.17/0.56 fof(f1758,plain,(
% 0.17/0.56 op2(e22,e21)=e21),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1595,f218])).
% 0.17/0.56 fof(f1761,plain,(
% 0.17/0.56 op2(e20,e23)=e20),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1526,f1599])).
% 0.17/0.56 fof(f1762,plain,(
% 0.17/0.56 op2(e22,e23)=e22),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f1262,f1599])).
% 0.17/0.56 fof(f1771,plain,(
% 0.17/0.56 h2(e10)=e23|e22=e23),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1645,f1496])).
% 0.17/0.56 fof(f1788,plain,(
% 0.17/0.56 op2(e21,e22)=e22),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1647,f219])).
% 0.17/0.56 fof(f1865,plain,(
% 0.17/0.56 ~h3(e13)=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(e11)=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1705,f1682])).
% 0.17/0.56 fof(f1866,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(e11)=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f578,f1865])).
% 0.17/0.56 fof(f1867,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~h3(e11)=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1646,f1866])).
% 0.17/0.56 fof(f1868,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e21=op2(e21,e20)|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f577,f1867])).
% 0.17/0.56 fof(f1869,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e21=e21|~e22=op2(e21,e22)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1749,f1868])).
% 0.17/0.56 fof(f1870,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e21=e21|~e22=e22|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1788,f1869])).
% 0.17/0.56 fof(f1871,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e21=e21|~e22=e22|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(e11)=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1680,f1870])).
% 0.17/0.56 fof(f1872,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e21=e21|~e22=e22|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~e21=op2(e22,e21)|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f577,f1871])).
% 0.17/0.56 fof(f1873,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e21=e21|~e22=e22|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~e21=e21|~h3(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1758,f1872])).
% 0.17/0.56 fof(f1874,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e21=e21|~e22=e22|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~e21=e21|~h3(op1(e12,e13))=op2(e22,e23)|~e23=e23|~e22=op2(e23,e21)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1644,f1873])).
% 0.17/0.56 fof(f1875,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e21=e21|~e22=e22|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~e21=e21|~h3(op1(e12,e13))=op2(e22,e23)|~e23=e23|~e22=e22),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1645,f1874])).
% 0.17/0.56 fof(f1876,plain,(
% 0.17/0.56 ~e23=h2(e10)|~e21=e21|~h3(op1(e10,e13))=op2(e20,e23)|~e22=e22|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e13))=op2(e22,e23)|~e23=e23),
% 0.17/0.56 inference(duplicate_literals_removal,[status(thm)],[f1875])).
% 0.17/0.56 fof(f1877,plain,(
% 0.17/0.56 ~e23=h2(e10)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e13))=h4(e10)|~h3(op1(e12,e10))=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.56 inference(trivial_equality_resolution,[status(thm)],[f1876])).
% 0.17/0.56 fof(f1886,plain,(
% 0.17/0.56 ~e23=h2(e10)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e13))=h4(e10)|~h3(e10)=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.56 inference(backward_demodulation,[status(thm)],[f1892,f1877])).
% 0.17/0.56 fof(f1892,plain,(
% 0.17/0.56 op1(e12,e10)=e10),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1686,f212])).
% 0.17/0.56 fof(f1899,plain,(
% 0.17/0.56 op1(e11,e13)=e13),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1688,f216])).
% 0.17/0.56 fof(f1910,plain,(
% 0.17/0.56 op1(e10,e13)=e10),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1701,f214])).
% 0.17/0.56 fof(f1937,plain,(
% 0.17/0.56 h4(e10)=e23),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1743,f222])).
% 0.17/0.56 fof(f1960,plain,(
% 0.17/0.56 h2(e10)=e23),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1771,f223])).
% 0.17/0.56 fof(f1967,plain,(
% 0.17/0.56 ~e23=e23|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e13))=h4(e10)|~h3(e10)=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1960,f1886])).
% 0.17/0.56 fof(f1968,plain,(
% 0.17/0.56 ~e23=e23|~h3(e10)=op2(e20,e23)|~h3(op1(e11,e13))=h4(e10)|~h3(e10)=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1910,f1967])).
% 0.17/0.56 fof(f1969,plain,(
% 0.17/0.56 ~e23=e23|~e20=op2(e20,e23)|~h3(op1(e11,e13))=h4(e10)|~h3(e10)=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f576,f1968])).
% 0.17/0.56 fof(f1970,plain,(
% 0.17/0.56 ~e23=e23|~e20=e20|~h3(op1(e11,e13))=h4(e10)|~h3(e10)=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1761,f1969])).
% 0.17/0.56 fof(f1971,plain,(
% 0.17/0.56 ~e23=e23|~e20=e20|~h3(e13)=h4(e10)|~h3(e10)=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.56 inference(forward_demodulation,[status(thm)],[f1899,f1970])).
% 0.17/0.57 fof(f1972,plain,(
% 0.17/0.57 ~e23=e23|~e20=e20|~e23=h4(e10)|~h3(e10)=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.57 inference(forward_demodulation,[status(thm)],[f578,f1971])).
% 0.17/0.57 fof(f1973,plain,(
% 0.17/0.57 ~e23=e23|~e20=e20|~e23=e23|~h3(e10)=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.57 inference(forward_demodulation,[status(thm)],[f1937,f1972])).
% 0.17/0.57 fof(f1974,plain,(
% 0.17/0.57 ~e23=e23|~e20=e20|~e23=e23|~e20=e20|~h3(op1(e12,e13))=op2(e22,e23)),
% 0.17/0.57 inference(forward_demodulation,[status(thm)],[f576,f1973])).
% 0.17/0.57 fof(f1975,plain,(
% 0.17/0.57 ~e23=e23|~e20=e20|~e23=e23|~e20=e20|~h3(e12)=op2(e22,e23)),
% 0.17/0.57 inference(forward_demodulation,[status(thm)],[f1693,f1974])).
% 0.17/0.57 fof(f1976,plain,(
% 0.17/0.57 ~e23=e23|~e20=e20|~e23=e23|~e20=e20|~e22=op2(e22,e23)),
% 0.17/0.57 inference(forward_demodulation,[status(thm)],[f280,f1975])).
% 0.17/0.57 fof(f1977,plain,(
% 0.17/0.57 ~e23=e23|~e20=e20|~e23=e23|~e20=e20|~e22=e22),
% 0.17/0.57 inference(forward_demodulation,[status(thm)],[f1762,f1976])).
% 0.17/0.57 fof(f1978,plain,(
% 0.17/0.57 ~e23=e23|~e20=e20|~e22=e22),
% 0.17/0.57 inference(duplicate_literals_removal,[status(thm)],[f1977])).
% 0.17/0.57 fof(f1979,plain,(
% 0.17/0.57 $false),
% 0.17/0.57 inference(trivial_equality_resolution,[status(thm)],[f1978])).
% 0.17/0.57 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.59 % Elapsed time: 0.203157 seconds
% 0.17/0.59 % CPU time: 0.727095 seconds
% 0.17/0.59 % Total memory used: 98.647 MB
% 0.17/0.59 % Net memory used: 98.422 MB
%------------------------------------------------------------------------------