%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG111+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 : n011.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.13s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG111+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 12:56:55 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.46 % Refutation found
% 0.13/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.46 fof(f1,axiom,(
% 0.13/0.46 ( ( 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.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f2,axiom,(
% 0.13/0.46 ( ( 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.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f3,axiom,(
% 0.13/0.46 ( ( 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.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f4,axiom,(
% 0.13/0.46 ( ( 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.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f5,axiom,(
% 0.13/0.46 ( 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.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f6,axiom,(
% 0.13/0.46 ( 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.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f7,axiom,(
% 0.13/0.46 ( e10 != e11& e10 != e12& e10 != e13& e11 != e12& e11 != e13& e12 != e13 ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f8,axiom,(
% 0.13/0.46 ( e20 != e21& e20 != e22& e20 != e23& e21 != e22& e21 != e23& e22 != e23 ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f10,axiom,(
% 0.13/0.46 ( ( op1(e10,e10) != e10| op1(e10,e10) != e10 )& ( op1(e10,e10) != e10| op1(e11,e11) != e10 )& ( op1(e10,e10) != e10| op1(e12,e12) != e10 )& ( op1(e10,e10) != e10| op1(e13,e13) != e10 )& ( op1(e10,e11) != e10| op1(e10,e10) != e11 )& ( op1(e10,e11) != e10| op1(e11,e11) != e11 )& ( op1(e10,e11) != e10| op1(e12,e12) != e11 )& ( op1(e10,e11) != e10| op1(e13,e13) != e11 )& ( op1(e10,e12) != e10| op1(e10,e10) != e12 )& ( op1(e10,e12) != e10| op1(e11,e11) != e12 )& ( op1(e10,e12) != e10| op1(e12,e12) != e12 )& ( op1(e10,e12) != e10| op1(e13,e13) != e12 )& ( op1(e10,e13) != e10| op1(e10,e10) != e13 )& ( op1(e10,e13) != e10| op1(e11,e11) != e13 )& ( op1(e10,e13) != e10| op1(e12,e12) != e13 )& ( op1(e10,e13) != e10| op1(e13,e13) != e13 )& ( op1(e11,e10) != e11| op1(e10,e10) != e10 )& ( op1(e11,e10) != e11| op1(e11,e11) != e10 )& ( op1(e11,e10) != e11| op1(e12,e12) != e10 )& ( op1(e11,e10) != e11| op1(e13,e13) != e10 )& ( op1(e11,e11) != e11| op1(e10,e10) != e11 )& ( op1(e11,e11) != e11| op1(e11,e11) != e11 )& ( op1(e11,e11) != e11| op1(e12,e12) != e11 )& ( op1(e11,e11) != e11| op1(e13,e13) != e11 )& ( op1(e11,e12) != e11| op1(e10,e10) != e12 )& ( op1(e11,e12) != e11| op1(e11,e11) != e12 )& ( op1(e11,e12) != e11| op1(e12,e12) != e12 )& ( op1(e11,e12) != e11| op1(e13,e13) != e12 )& ( op1(e11,e13) != e11| op1(e10,e10) != e13 )& ( op1(e11,e13) != e11| op1(e11,e11) != e13 )& ( op1(e11,e13) != e11| op1(e12,e12) != e13 )& ( op1(e11,e13) != e11| op1(e13,e13) != e13 )& ( op1(e12,e10) != e12| op1(e10,e10) != e10 )& ( op1(e12,e10) != e12| op1(e11,e11) != e10 )& ( op1(e12,e10) != e12| op1(e12,e12) != e10 )& ( op1(e12,e10) != e12| op1(e13,e13) != e10 )& ( op1(e12,e11) != e12| op1(e10,e10) != e11 )& ( op1(e12,e11) != e12| op1(e11,e11) != e11 )& ( op1(e12,e11) != e12| op1(e12,e12) != e11 )& ( op1(e12,e11) != e12| op1(e13,e13) != e11 )& ( op1(e12,e12) != e12| op1(e10,e10) != e12 )& ( op1(e12,e12) != e12| op1(e11,e11) != e12 )& ( op1(e12,e12) != e12| op1(e12,e12) != e12 )& ( op1(e12,e12) != e12| op1(e13,e13) != e12 )& ( op1(e12,e13) != e12| op1(e10,e10) != e13 )& ( op1(e12,e13) != e12| op1(e11,e11) != e13 )& ( op1(e12,e13) != e12| op1(e12,e12) != e13 )& ( op1(e12,e13) != e12| op1(e13,e13) != e13 )& ( op1(e13,e10) != e13| op1(e10,e10) != e10 )& ( op1(e13,e10) != e13| op1(e11,e11) != e10 )& ( op1(e13,e10) != e13| op1(e12,e12) != e10 )& ( op1(e13,e10) != e13| op1(e13,e13) != e10 )& ( op1(e13,e11) != e13| op1(e10,e10) != e11 )& ( op1(e13,e11) != e13| op1(e11,e11) != e11 )& ( op1(e13,e11) != e13| op1(e12,e12) != e11 )& ( op1(e13,e11) != e13| op1(e13,e13) != e11 )& ( op1(e13,e12) != e13| op1(e10,e10) != e12 )& ( op1(e13,e12) != e13| op1(e11,e11) != e12 )& ( op1(e13,e12) != e13| op1(e12,e12) != e12 )& ( op1(e13,e12) != e13| op1(e13,e13) != e12 )& ( op1(e13,e13) != e13| op1(e10,e10) != e13 )& ( op1(e13,e13) != e13| op1(e11,e11) != e13 )& ( op1(e13,e13) != e13| op1(e12,e12) != e13 )& ( op1(e13,e13) != e13| op1(e13,e13) != e13 ) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f11,axiom,(
% 0.13/0.46 ( ( op2(e20,e20) != e20| op2(e20,e20) != e20 )& ( op2(e20,e20) != e20| op2(e21,e21) != e20 )& ( op2(e20,e20) != e20| op2(e22,e22) != e20 )& ( op2(e20,e20) != e20| op2(e23,e23) != e20 )& ( op2(e20,e21) != e20| op2(e20,e20) != e21 )& ( op2(e20,e21) != e20| op2(e21,e21) != e21 )& ( op2(e20,e21) != e20| op2(e22,e22) != e21 )& ( op2(e20,e21) != e20| op2(e23,e23) != e21 )& ( op2(e20,e22) != e20| op2(e20,e20) != e22 )& ( op2(e20,e22) != e20| op2(e21,e21) != e22 )& ( op2(e20,e22) != e20| op2(e22,e22) != e22 )& ( op2(e20,e22) != e20| op2(e23,e23) != e22 )& ( op2(e20,e23) != e20| op2(e20,e20) != e23 )& ( op2(e20,e23) != e20| op2(e21,e21) != e23 )& ( op2(e20,e23) != e20| op2(e22,e22) != e23 )& ( op2(e20,e23) != e20| op2(e23,e23) != e23 )& ( op2(e21,e20) != e21| op2(e20,e20) != e20 )& ( op2(e21,e20) != e21| op2(e21,e21) != e20 )& ( op2(e21,e20) != e21| op2(e22,e22) != e20 )& ( op2(e21,e20) != e21| op2(e23,e23) != e20 )& ( op2(e21,e21) != e21| op2(e20,e20) != e21 )& ( op2(e21,e21) != e21| op2(e21,e21) != e21 )& ( op2(e21,e21) != e21| op2(e22,e22) != e21 )& ( op2(e21,e21) != e21| op2(e23,e23) != e21 )& ( op2(e21,e22) != e21| op2(e20,e20) != e22 )& ( op2(e21,e22) != e21| op2(e21,e21) != e22 )& ( op2(e21,e22) != e21| op2(e22,e22) != e22 )& ( op2(e21,e22) != e21| op2(e23,e23) != e22 )& ( op2(e21,e23) != e21| op2(e20,e20) != e23 )& ( op2(e21,e23) != e21| op2(e21,e21) != e23 )& ( op2(e21,e23) != e21| op2(e22,e22) != e23 )& ( op2(e21,e23) != e21| op2(e23,e23) != e23 )& ( op2(e22,e20) != e22| op2(e20,e20) != e20 )& ( op2(e22,e20) != e22| op2(e21,e21) != e20 )& ( op2(e22,e20) != e22| op2(e22,e22) != e20 )& ( op2(e22,e20) != e22| op2(e23,e23) != e20 )& ( op2(e22,e21) != e22| op2(e20,e20) != e21 )& ( op2(e22,e21) != e22| op2(e21,e21) != e21 )& ( op2(e22,e21) != e22| op2(e22,e22) != e21 )& ( op2(e22,e21) != e22| op2(e23,e23) != e21 )& ( op2(e22,e22) != e22| op2(e20,e20) != e22 )& ( op2(e22,e22) != e22| op2(e21,e21) != e22 )& ( op2(e22,e22) != e22| op2(e22,e22) != e22 )& ( op2(e22,e22) != e22| op2(e23,e23) != e22 )& ( op2(e22,e23) != e22| op2(e20,e20) != e23 )& ( op2(e22,e23) != e22| op2(e21,e21) != e23 )& ( op2(e22,e23) != e22| op2(e22,e22) != e23 )& ( op2(e22,e23) != e22| op2(e23,e23) != e23 )& ( op2(e23,e20) != e23| op2(e20,e20) != e20 )& ( op2(e23,e20) != e23| op2(e21,e21) != e20 )& ( op2(e23,e20) != e23| op2(e22,e22) != e20 )& ( op2(e23,e20) != e23| op2(e23,e23) != e20 )& ( op2(e23,e21) != e23| op2(e20,e20) != e21 )& ( op2(e23,e21) != e23| op2(e21,e21) != e21 )& ( op2(e23,e21) != e23| op2(e22,e22) != e21 )& ( op2(e23,e21) != e23| op2(e23,e23) != e21 )& ( op2(e23,e22) != e23| op2(e20,e20) != e22 )& ( op2(e23,e22) != e23| op2(e21,e21) != e22 )& ( op2(e23,e22) != e23| op2(e22,e22) != e22 )& ( op2(e23,e22) != e23| op2(e23,e23) != e22 )& ( op2(e23,e23) != e23| op2(e20,e20) != e23 )& ( op2(e23,e23) != e23| op2(e21,e21) != e23 )& ( op2(e23,e23) != e23| op2(e22,e22) != e23 )& ( op2(e23,e23) != e23| op2(e23,e23) != e23 ) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f12,axiom,(
% 0.13/0.46 ( e10 = op1(e13,op1(e13,e13))& e11 = op1(e13,e13)& e12 = op1(op1(e13,op1(e13,e13)),op1(e13,e13)) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f13,axiom,(
% 0.13/0.46 ( e20 = op2(e23,op2(e23,e23))& e21 = op2(e23,e23)& e22 = op2(op2(e23,op2(e23,e23)),op2(e23,e23)) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f14,axiom,(
% 0.13/0.46 ( h1(e13) = e20& h1(e10) = op2(e20,op2(e20,e20))& h1(e11) = op2(e20,e20)& h1(e12) = op2(op2(e20,op2(e20,e20)),op2(e20,e20)) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f15,axiom,(
% 0.13/0.46 ( h2(e13) = e21& h2(e10) = op2(e21,op2(e21,e21))& h2(e11) = op2(e21,e21)& h2(e12) = op2(op2(e21,op2(e21,e21)),op2(e21,e21)) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f16,axiom,(
% 0.13/0.46 ( h3(e13) = e22& h3(e10) = op2(e22,op2(e22,e22))& h3(e11) = op2(e22,e22)& h3(e12) = op2(op2(e22,op2(e22,e22)),op2(e22,e22)) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f17,axiom,(
% 0.13/0.46 ( h4(e13) = e23& h4(e10) = op2(e23,op2(e23,e23))& h4(e11) = op2(e23,e23)& h4(e12) = op2(op2(e23,op2(e23,e23)),op2(e23,e23)) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f18,conjecture,(
% 0.13/0.46 ( ( 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.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f19,negated_conjecture,(
% 0.13/0.46 ~(( ( 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.13/0.46 inference(negated_conjecture,[status(cth)],[f18])).
% 0.13/0.46 fof(f23,plain,(
% 0.13/0.46 op1(e10,e13)=e10|op1(e10,e13)=e11|op1(e10,e13)=e12|op1(e10,e13)=e13),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.46 fof(f25,plain,(
% 0.13/0.46 op1(e11,e11)=e10|op1(e11,e11)=e11|op1(e11,e11)=e12|op1(e11,e11)=e13),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.46 fof(f30,plain,(
% 0.13/0.46 op1(e12,e12)=e10|op1(e12,e12)=e11|op1(e12,e12)=e12|op1(e12,e12)=e13),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.46 fof(f32,plain,(
% 0.13/0.46 op1(e13,e10)=e10|op1(e13,e10)=e11|op1(e13,e10)=e12|op1(e13,e10)=e13),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.46 fof(f36,plain,(
% 0.13/0.46 op1(e10,e10)=e10|op1(e10,e11)=e10|op1(e10,e12)=e10|op1(e10,e13)=e10),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f37,plain,(
% 0.13/0.46 op1(e10,e10)=e10|op1(e11,e10)=e10|op1(e12,e10)=e10|op1(e13,e10)=e10),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f39,plain,(
% 0.13/0.46 op1(e10,e10)=e11|op1(e11,e10)=e11|op1(e12,e10)=e11|op1(e13,e10)=e11),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f47,plain,(
% 0.13/0.46 op1(e10,e11)=e11|op1(e11,e11)=e11|op1(e12,e11)=e11|op1(e13,e11)=e11),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f55,plain,(
% 0.13/0.46 op1(e10,e12)=e11|op1(e11,e12)=e11|op1(e12,e12)=e11|op1(e13,e12)=e11),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f56,plain,(
% 0.13/0.46 op1(e12,e10)=e12|op1(e12,e11)=e12|op1(e12,e12)=e12|op1(e12,e13)=e12),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f57,plain,(
% 0.13/0.46 op1(e10,e12)=e12|op1(e11,e12)=e12|op1(e12,e12)=e12|op1(e13,e12)=e12),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f61,plain,(
% 0.13/0.46 op1(e10,e13)=e10|op1(e11,e13)=e10|op1(e12,e13)=e10|op1(e13,e13)=e10),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f65,plain,(
% 0.13/0.46 op1(e10,e13)=e12|op1(e11,e13)=e12|op1(e12,e13)=e12|op1(e13,e13)=e12),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f68,plain,(
% 0.13/0.46 op2(e20,e20)=e20|op2(e20,e20)=e21|op2(e20,e20)=e22|op2(e20,e20)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.46 fof(f71,plain,(
% 0.13/0.46 op2(e20,e23)=e20|op2(e20,e23)=e21|op2(e20,e23)=e22|op2(e20,e23)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.46 fof(f73,plain,(
% 0.13/0.46 op2(e21,e21)=e20|op2(e21,e21)=e21|op2(e21,e21)=e22|op2(e21,e21)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.46 fof(f78,plain,(
% 0.13/0.46 op2(e22,e22)=e20|op2(e22,e22)=e21|op2(e22,e22)=e22|op2(e22,e22)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.46 fof(f79,plain,(
% 0.13/0.46 op2(e22,e23)=e20|op2(e22,e23)=e21|op2(e22,e23)=e22|op2(e22,e23)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.46 fof(f80,plain,(
% 0.13/0.46 op2(e23,e20)=e20|op2(e23,e20)=e21|op2(e23,e20)=e22|op2(e23,e20)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.46 fof(f84,plain,(
% 0.13/0.46 op2(e20,e20)=e20|op2(e20,e21)=e20|op2(e20,e22)=e20|op2(e20,e23)=e20),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.46 fof(f85,plain,(
% 0.13/0.46 op2(e20,e20)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.46 fof(f95,plain,(
% 0.13/0.46 op2(e20,e21)=e21|op2(e21,e21)=e21|op2(e22,e21)=e21|op2(e23,e21)=e21),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.46 fof(f103,plain,(
% 0.13/0.46 op2(e20,e22)=e21|op2(e21,e22)=e21|op2(e22,e22)=e21|op2(e23,e22)=e21),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.46 fof(f104,plain,(
% 0.13/0.46 op2(e22,e20)=e22|op2(e22,e21)=e22|op2(e22,e22)=e22|op2(e22,e23)=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.46 fof(f105,plain,(
% 0.13/0.46 op2(e20,e22)=e22|op2(e21,e22)=e22|op2(e22,e22)=e22|op2(e23,e22)=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.46 fof(f113,plain,(
% 0.13/0.46 op2(e20,e23)=e22|op2(e21,e23)=e22|op2(e22,e23)=e22|op2(e23,e23)=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.46 fof(f121,plain,(
% 0.13/0.46 ~op1(e12,e10)=op1(e13,e10)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f122,plain,(
% 0.13/0.46 ~op1(e10,e11)=op1(e11,e11)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f126,plain,(
% 0.13/0.46 ~op1(e11,e11)=op1(e13,e11)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f136,plain,(
% 0.13/0.46 ~op1(e10,e13)=op1(e13,e13)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f143,plain,(
% 0.13/0.46 ~op1(e10,e11)=op1(e10,e12)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f144,plain,(
% 0.13/0.46 ~op1(e10,e11)=op1(e10,e13)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f151,plain,(
% 0.13/0.46 ~op1(e11,e12)=op1(e11,e13)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f152,plain,(
% 0.13/0.46 ~op1(e12,e10)=op1(e12,e11)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f155,plain,(
% 0.13/0.46 ~op1(e12,e11)=op1(e12,e12)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f158,plain,(
% 0.13/0.46 ~op1(e13,e10)=op1(e13,e11)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f160,plain,(
% 0.13/0.46 ~op1(e13,e10)=op1(e13,e13)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f163,plain,(
% 0.13/0.46 ~op1(e13,e12)=op1(e13,e13)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f169,plain,(
% 0.13/0.46 ~op2(e22,e20)=op2(e23,e20)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f170,plain,(
% 0.13/0.46 ~op2(e20,e21)=op2(e21,e21)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f174,plain,(
% 0.13/0.46 ~op2(e21,e21)=op2(e23,e21)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f177,plain,(
% 0.13/0.46 ~op2(e20,e22)=op2(e22,e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f183,plain,(
% 0.13/0.46 ~op2(e20,e23)=op2(e22,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f184,plain,(
% 0.13/0.46 ~op2(e20,e23)=op2(e23,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f187,plain,(
% 0.13/0.46 ~op2(e22,e23)=op2(e23,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f188,plain,(
% 0.13/0.46 ~op2(e20,e20)=op2(e20,e21)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f190,plain,(
% 0.13/0.46 ~op2(e20,e20)=op2(e20,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f191,plain,(
% 0.13/0.46 ~op2(e20,e21)=op2(e20,e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f192,plain,(
% 0.13/0.46 ~op2(e20,e21)=op2(e20,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f203,plain,(
% 0.13/0.46 ~op2(e22,e21)=op2(e22,e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f206,plain,(
% 0.13/0.46 ~op2(e23,e20)=op2(e23,e21)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f208,plain,(
% 0.13/0.46 ~op2(e23,e20)=op2(e23,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f211,plain,(
% 0.13/0.46 ~op2(e23,e22)=op2(e23,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f212,plain,(
% 0.13/0.46 ~e10=e11),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.46 fof(f213,plain,(
% 0.13/0.46 ~e10=e12),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.46 fof(f215,plain,(
% 0.13/0.46 ~e11=e12),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.46 fof(f218,plain,(
% 0.13/0.46 ~e20=e21),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.46 fof(f219,plain,(
% 0.13/0.46 ~e20=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.46 fof(f221,plain,(
% 0.13/0.46 ~e21=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.46 fof(f240,plain,(
% 0.13/0.46 ~op1(e10,e10)=e10|~op1(e10,e10)=e10),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.46 fof(f253,plain,(
% 0.13/0.46 ~op1(e10,e13)=e10|~op1(e11,e11)=e13),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.46 fof(f261,plain,(
% 0.13/0.46 ~op1(e11,e11)=e11|~op1(e11,e11)=e11),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.46 fof(f274,plain,(
% 0.13/0.46 ~op1(e12,e10)=e12|~op1(e12,e12)=e10),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.46 fof(f279,plain,(
% 0.13/0.46 ~op1(e12,e11)=e12|~op1(e13,e13)=e11),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.46 fof(f282,plain,(
% 0.13/0.46 ~op1(e12,e12)=e12|~op1(e12,e12)=e12),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.46 fof(f285,plain,(
% 0.13/0.46 ~op1(e12,e13)=e12|~op1(e11,e11)=e13),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.46 fof(f304,plain,(
% 0.13/0.46 ~op2(e20,e20)=e20|~op2(e20,e20)=e20),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.46 fof(f317,plain,(
% 0.13/0.46 ~op2(e20,e23)=e20|~op2(e21,e21)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.46 fof(f325,plain,(
% 0.13/0.46 ~op2(e21,e21)=e21|~op2(e21,e21)=e21),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.46 fof(f343,plain,(
% 0.13/0.46 ~op2(e22,e21)=e22|~op2(e23,e23)=e21),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.46 fof(f346,plain,(
% 0.13/0.46 ~op2(e22,e22)=e22|~op2(e22,e22)=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.46 fof(f349,plain,(
% 0.13/0.46 ~op2(e22,e23)=e22|~op2(e21,e21)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.46 fof(f368,plain,(
% 0.13/0.46 e10=op1(e13,op1(e13,e13))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.46 fof(f369,plain,(
% 0.13/0.46 e11=op1(e13,e13)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.46 fof(f370,plain,(
% 0.13/0.46 e12=op1(op1(e13,op1(e13,e13)),op1(e13,e13))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.46 fof(f371,plain,(
% 0.13/0.46 e20=op2(e23,op2(e23,e23))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.46 fof(f372,plain,(
% 0.13/0.46 e21=op2(e23,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.46 fof(f373,plain,(
% 0.13/0.46 e22=op2(op2(e23,op2(e23,e23)),op2(e23,e23))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.46 fof(f376,plain,(
% 0.13/0.46 h1(e11)=op2(e20,e20)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.46 fof(f379,plain,(
% 0.13/0.46 h2(e10)=op2(e21,op2(e21,e21))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.46 fof(f380,plain,(
% 0.13/0.46 h2(e11)=op2(e21,e21)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.46 fof(f384,plain,(
% 0.13/0.46 h3(e11)=op2(e22,e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.46 fof(f386,plain,(
% 0.13/0.46 h4(e13)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.46 fof(f387,plain,(
% 0.13/0.46 h4(e10)=op2(e23,op2(e23,e23))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.46 fof(f388,plain,(
% 0.13/0.46 h4(e11)=op2(e23,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.46 fof(f389,plain,(
% 0.13/0.46 h4(e12)=op2(op2(e23,op2(e23,e23)),op2(e23,e23))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.46 fof(f390,plain,(
% 0.13/0.46 ((((((((((((((((((((((~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.13/0.46 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.13/0.46 fof(f391,definition,(
% 0.13/0.46 sP0_prd<=>(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.46 fof(f392,definition,(
% 0.13/0.46 sP1_prd<=>(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.13/0.46 fof(f393,definition,(
% 0.13/0.46 sP2_prd<=>(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.13/0.46 fof(f394,definition,(
% 0.13/0.46 sP3_prd<=>(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.13/0.46 fof(f395,definition,(
% 0.13/0.46 sP4_prd<=>(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.13/0.46 fof(f396,definition,(
% 0.13/0.46 sP5_prd<=>(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.13/0.46 fof(f397,definition,(
% 0.13/0.46 sP6_prd<=>(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.13/0.46 fof(f398,definition,(
% 0.13/0.46 sP7_prd<=>(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.13/0.46 fof(f399,definition,(
% 0.13/0.46 sP8_prd<=>(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.13/0.46 fof(f400,definition,(
% 0.13/0.46 sP9_prd<=>(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.13/0.46 fof(f401,definition,(
% 0.13/0.46 sP10_prd<=>(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.13/0.46 fof(f402,definition,(
% 0.13/0.46 sP11_prd<=>(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.13/0.46 fof(f403,plain,(
% 0.13/0.46 (((((((((((((((((((((~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)))|sP0_prd)|sP1_prd)|sP2_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)))|sP3_prd)|sP4_prd)|sP5_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)))|sP6_prd)|sP7_prd)|sP8_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)))|sP9_prd)|sP10_prd)|sP11_prd)|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23))),
% 0.13/0.46 inference(formula_renaming,[status(thm)],[f390,f402,f401,f400,f399,f398,f397,f396,f395,f394,f393,f392,f391])).
% 0.13/0.46 fof(f419,plain,(
% 0.13/0.46 ~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))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f403])).
% 0.13/0.46 fof(f474,plain,(
% 0.13/0.46 (~sP9_prd|(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20))&(sP9_prd|(((h4(e10)=e20|h4(e11)=e20)|h4(e12)=e20)|h4(e13)=e20))),
% 0.13/0.46 inference(NNF_transformation,[status(thm)],[f400])).
% 0.13/0.46 fof(f475,plain,(
% 0.13/0.46 ~sP9_prd|~h4(e10)=e20),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f474])).
% 0.13/0.46 fof(f480,plain,(
% 0.13/0.46 (~sP10_prd|(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21))&(sP10_prd|(((h4(e10)=e21|h4(e11)=e21)|h4(e12)=e21)|h4(e13)=e21))),
% 0.13/0.46 inference(NNF_transformation,[status(thm)],[f401])).
% 0.13/0.46 fof(f482,plain,(
% 0.13/0.46 ~sP10_prd|~h4(e11)=e21),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f480])).
% 0.13/0.46 fof(f486,plain,(
% 0.13/0.46 (~sP11_prd|(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22))&(sP11_prd|(((h4(e10)=e22|h4(e11)=e22)|h4(e12)=e22)|h4(e13)=e22))),
% 0.13/0.46 inference(NNF_transformation,[status(thm)],[f402])).
% 0.13/0.46 fof(f489,plain,(
% 0.13/0.46 ~sP11_prd|~h4(e12)=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f486])).
% 0.13/0.46 fof(f492,plain,(
% 0.13/0.46 op1(e11,e10)=e10|op1(e12,e10)=e10|op1(e13,e10)=e10),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f37,f495])).
% 0.13/0.46 fof(f493,plain,(
% 0.13/0.46 op1(e10,e11)=e10|op1(e10,e12)=e10|op1(e10,e13)=e10),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f36,f495])).
% 0.13/0.46 fof(f495,plain,(
% 0.13/0.46 ~op1(e10,e10)=e10),
% 0.13/0.46 inference(duplicate_literals_removal,[status(thm)],[f240])).
% 0.13/0.46 fof(f496,plain,(
% 0.13/0.46 op1(e10,e11)=e11|op1(e12,e11)=e11|op1(e13,e11)=e11),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f47,f499])).
% 0.13/0.46 fof(f498,plain,(
% 0.13/0.46 op1(e11,e11)=e10|op1(e11,e11)=e12|op1(e11,e11)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f25,f499])).
% 0.13/0.46 fof(f499,plain,(
% 0.13/0.46 ~op1(e11,e11)=e11),
% 0.13/0.46 inference(duplicate_literals_removal,[status(thm)],[f261])).
% 0.13/0.46 fof(f500,plain,(
% 0.13/0.46 op1(e10,e12)=e12|op1(e11,e12)=e12|op1(e13,e12)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f57,f503])).
% 0.13/0.46 fof(f501,plain,(
% 0.13/0.46 op1(e12,e10)=e12|op1(e12,e11)=e12|op1(e12,e13)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f56,f503])).
% 0.13/0.46 fof(f502,plain,(
% 0.13/0.46 op1(e12,e12)=e10|op1(e12,e12)=e11|op1(e12,e12)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f30,f503])).
% 0.13/0.46 fof(f503,plain,(
% 0.13/0.46 ~op1(e12,e12)=e12),
% 0.13/0.46 inference(duplicate_literals_removal,[status(thm)],[f282])).
% 0.13/0.46 fof(f508,plain,(
% 0.13/0.46 op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f85,f511])).
% 0.13/0.46 fof(f509,plain,(
% 0.13/0.46 op2(e20,e21)=e20|op2(e20,e22)=e20|op2(e20,e23)=e20),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f84,f511])).
% 0.13/0.46 fof(f510,plain,(
% 0.13/0.46 op2(e20,e20)=e21|op2(e20,e20)=e22|op2(e20,e20)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f68,f511])).
% 0.13/0.46 fof(f511,plain,(
% 0.13/0.46 ~op2(e20,e20)=e20),
% 0.13/0.46 inference(duplicate_literals_removal,[status(thm)],[f304])).
% 0.13/0.46 fof(f512,plain,(
% 0.13/0.46 op2(e20,e21)=e21|op2(e22,e21)=e21|op2(e23,e21)=e21),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f95,f515])).
% 0.13/0.46 fof(f514,plain,(
% 0.13/0.46 op2(e21,e21)=e20|op2(e21,e21)=e22|op2(e21,e21)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f73,f515])).
% 0.13/0.46 fof(f515,plain,(
% 0.13/0.46 ~op2(e21,e21)=e21),
% 0.13/0.46 inference(duplicate_literals_removal,[status(thm)],[f325])).
% 0.13/0.46 fof(f516,plain,(
% 0.13/0.46 op2(e20,e22)=e22|op2(e21,e22)=e22|op2(e23,e22)=e22),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f105,f519])).
% 0.13/0.46 fof(f517,plain,(
% 0.13/0.46 op2(e22,e20)=e22|op2(e22,e21)=e22|op2(e22,e23)=e22),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f104,f519])).
% 0.13/0.46 fof(f518,plain,(
% 0.13/0.46 op2(e22,e22)=e20|op2(e22,e22)=e21|op2(e22,e22)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f78,f519])).
% 0.13/0.46 fof(f519,plain,(
% 0.13/0.46 ~op2(e22,e22)=e22),
% 0.13/0.46 inference(duplicate_literals_removal,[status(thm)],[f346])).
% 0.13/0.46 fof(f524,plain,(
% 0.13/0.46 e10=op1(e13,e11)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f369,f368])).
% 0.13/0.46 fof(f529,plain,(
% 0.13/0.46 ~op1(e12,e11)=e12|~e11=e11),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f369,f279])).
% 0.13/0.46 fof(f535,plain,(
% 0.13/0.46 ~op1(e13,e12)=e11),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f369,f163])).
% 0.13/0.46 fof(f537,plain,(
% 0.13/0.46 ~op1(e13,e10)=e11),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f369,f160])).
% 0.13/0.46 fof(f540,plain,(
% 0.13/0.46 ~op1(e10,e13)=e11),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f369,f136])).
% 0.13/0.46 fof(f541,plain,(
% 0.13/0.46 op1(e10,e13)=e12|op1(e11,e13)=e12|op1(e12,e13)=e12|e11=e12),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f369,f65])).
% 0.13/0.46 fof(f545,plain,(
% 0.13/0.46 op1(e10,e13)=e10|op1(e11,e13)=e10|op1(e12,e13)=e10|e11=e10),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f369,f61])).
% 0.13/0.46 fof(f547,plain,(
% 0.13/0.46 e12=op1(e10,op1(e13,e13))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f368,f370])).
% 0.13/0.46 fof(f550,plain,(
% 0.13/0.46 ~e12=op1(e10,e13)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f563,f144])).
% 0.13/0.46 fof(f551,plain,(
% 0.13/0.46 ~e12=op1(e10,e12)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f563,f143])).
% 0.13/0.46 fof(f555,plain,(
% 0.13/0.46 ~e12=op1(e11,e11)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f563,f122])).
% 0.13/0.46 fof(f563,plain,(
% 0.13/0.46 e12=op1(e10,e11)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f369,f547])).
% 0.13/0.46 fof(f564,plain,(
% 0.13/0.46 e20=op2(e23,e21)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f372,f371])).
% 0.13/0.46 fof(f569,plain,(
% 0.13/0.46 ~op2(e22,e21)=e22|~e21=e21),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f372,f343])).
% 0.13/0.46 fof(f575,plain,(
% 0.13/0.46 ~op2(e23,e22)=e21),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f372,f211])).
% 0.13/0.46 fof(f577,plain,(
% 0.13/0.46 ~op2(e23,e20)=e21),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f372,f208])).
% 0.13/0.46 fof(f578,plain,(
% 0.13/0.46 ~op2(e22,e23)=e21),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f372,f187])).
% 0.13/0.46 fof(f580,plain,(
% 0.13/0.46 ~op2(e20,e23)=e21),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f372,f184])).
% 0.13/0.46 fof(f581,plain,(
% 0.13/0.46 op2(e20,e23)=e22|op2(e21,e23)=e22|op2(e22,e23)=e22|e21=e22),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f372,f113])).
% 0.13/0.46 fof(f587,plain,(
% 0.13/0.46 e22=op2(e20,op2(e23,e23))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f371,f373])).
% 0.13/0.46 fof(f590,plain,(
% 0.13/0.46 ~e22=op2(e20,e23)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f603,f192])).
% 0.13/0.46 fof(f591,plain,(
% 0.13/0.46 ~e22=op2(e20,e22)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f603,f191])).
% 0.13/0.46 fof(f592,plain,(
% 0.13/0.46 ~op2(e20,e20)=e22),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f603,f188])).
% 0.13/0.46 fof(f595,plain,(
% 0.13/0.46 ~e22=op2(e21,e21)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f603,f170])).
% 0.13/0.46 fof(f603,plain,(
% 0.13/0.46 e22=op2(e20,e21)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f372,f587])).
% 0.13/0.46 fof(f614,plain,(
% 0.13/0.46 ~h1(e11)=op2(e20,e23)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f376,f190])).
% 0.13/0.46 fof(f624,plain,(
% 0.13/0.46 h2(e10)=op2(e21,h2(e11))),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f380,f379])).
% 0.13/0.46 fof(f627,plain,(
% 0.13/0.46 ~op2(e22,e23)=e22|~h2(e11)=e23),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f380,f349])).
% 0.13/0.46 fof(f633,plain,(
% 0.13/0.46 ~op2(e20,e23)=e20|~h2(e11)=e23),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f380,f317])).
% 0.13/0.46 fof(f638,plain,(
% 0.13/0.46 ~h2(e11)=op2(e23,e21)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f380,f174])).
% 0.13/0.46 fof(f656,plain,(
% 0.13/0.46 ~op2(e22,e21)=h3(e11)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f384,f203])).
% 0.13/0.46 fof(f660,plain,(
% 0.13/0.46 ~op2(e20,e22)=h3(e11)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f384,f177])).
% 0.13/0.46 fof(f663,plain,(
% 0.13/0.46 op2(e20,e22)=e21|op2(e21,e22)=e21|h3(e11)=e21|op2(e23,e22)=e21),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f384,f103])).
% 0.13/0.46 fof(f669,plain,(
% 0.13/0.46 h4(e10)=e20),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f371,f387])).
% 0.13/0.46 fof(f670,plain,(
% 0.13/0.46 h4(e11)=e21),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f372,f388])).
% 0.13/0.46 fof(f671,plain,(
% 0.13/0.46 h4(e12)=op2(e20,op2(e23,e23))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f371,f389])).
% 0.13/0.46 fof(f672,plain,(
% 0.13/0.46 h4(e12)=op2(e20,e21)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f372,f671])).
% 0.13/0.46 fof(f673,plain,(
% 0.13/0.46 h4(e12)=e22),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f603,f672])).
% 0.13/0.46 fof(f962,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=op2(e20,h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f419])).
% 0.13/0.46 fof(f963,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=op2(e20,e20)|~h4(op1(e10,e11))=op2(h4(e10),h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f962])).
% 0.13/0.46 fof(f964,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~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))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f376,f963])).
% 0.13/0.46 fof(f965,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(e12)=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))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f563,f964])).
% 0.13/0.46 fof(f966,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=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))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f965])).
% 0.13/0.46 fof(f967,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=op2(e20,h4(e11))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f966])).
% 0.13/0.46 fof(f968,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=op2(e20,e21)|~h4(op1(e10,e12))=op2(h4(e10),h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f967])).
% 0.13/0.46 fof(f969,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~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))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f603,f968])).
% 0.13/0.46 fof(f970,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,h4(e12))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f969])).
% 0.13/0.46 fof(f971,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(h4(e10),h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f970])).
% 0.13/0.46 fof(f972,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,h4(e13))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f971])).
% 0.13/0.46 fof(f973,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(h4(e11),h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f972])).
% 0.13/0.46 fof(f974,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,h4(e10))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f973])).
% 0.13/0.46 fof(f975,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=op2(h4(e11),h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f974])).
% 0.13/0.46 fof(f976,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=op2(e21,h4(e11))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f975])).
% 0.13/0.46 fof(f977,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=op2(e21,e21)|~h4(op1(e11,e12))=op2(h4(e11),h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f976])).
% 0.13/0.46 fof(f978,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(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))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f380,f977])).
% 0.13/0.46 fof(f979,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,h4(e12))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f978])).
% 0.13/0.46 fof(f980,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(h4(e11),h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f979])).
% 0.13/0.46 fof(f981,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,h4(e13))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f980])).
% 0.13/0.46 fof(f982,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(h4(e12),h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f981])).
% 0.13/0.46 fof(f983,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,h4(e10))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f982])).
% 0.13/0.46 fof(f984,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(h4(e12),h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f983])).
% 0.13/0.46 fof(f985,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,h4(e11))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f984])).
% 0.13/0.46 fof(f986,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=op2(h4(e12),h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f985])).
% 0.13/0.46 fof(f987,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=op2(e22,h4(e12))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f986])).
% 0.13/0.46 fof(f988,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=op2(e22,e22)|~h4(op1(e12,e13))=op2(h4(e12),h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f987])).
% 0.13/0.46 fof(f989,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~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))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f384,f988])).
% 0.13/0.46 fof(f990,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,h4(e13))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f989])).
% 0.13/0.46 fof(f991,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(h4(e13),h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f990])).
% 0.13/0.46 fof(f992,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,h4(e10))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f991])).
% 0.13/0.46 fof(f993,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(h4(e13),h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f992])).
% 0.13/0.46 fof(f994,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,h4(e11))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f993])).
% 0.13/0.46 fof(f995,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(h4(e13),h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f994])).
% 0.13/0.46 fof(f996,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,h4(e12))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f995])).
% 0.13/0.46 fof(f997,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~h4(op1(e13,e13))=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f996])).
% 0.13/0.46 fof(f998,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~h4(e11)=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f369,f997])).
% 0.13/0.46 fof(f999,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e21=op2(h4(e13),h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f998])).
% 0.13/0.46 fof(f1000,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e21=op2(e23,h4(e13))|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f999])).
% 0.13/0.46 fof(f1001,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e21=op2(e23,e23)|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f1000])).
% 0.13/0.46 fof(f1002,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e21=e21|sP9_prd|sP10_prd|sP11_prd|~h4(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f372,f1001])).
% 0.13/0.46 fof(f1003,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e22=e22|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|~e21=e21|sP9_prd|sP10_prd|sP11_prd|~e23=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f1002])).
% 0.13/0.46 fof(f1004,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP9_prd|sP10_prd|sP11_prd),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1003])).
% 0.13/0.46 fof(f1038,plain,(
% 0.13/0.46 ~sP9_prd|~e20=e20),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f475])).
% 0.13/0.46 fof(f1039,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e11))=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP10_prd|sP11_prd),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1004,f1040])).
% 0.13/0.46 fof(f1040,plain,(
% 0.13/0.46 ~sP9_prd),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1038])).
% 0.13/0.46 fof(f1045,plain,(
% 0.13/0.46 ~sP10_prd|~e21=e21),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f482])).
% 0.13/0.46 fof(f1046,plain,(
% 0.13/0.46 ~sP10_prd),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1045])).
% 0.13/0.46 fof(f1052,plain,(
% 0.13/0.46 ~sP11_prd|~e22=e22),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f489])).
% 0.13/0.46 fof(f1053,plain,(
% 0.13/0.46 ~sP11_prd),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1052])).
% 0.13/0.46 fof(f1057,plain,(
% 0.13/0.46 e12=e10|op1(e10,e12)=e10|op1(e10,e13)=e10),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f563,f493])).
% 0.13/0.46 fof(f1058,plain,(
% 0.13/0.46 op1(e10,e12)=e10|op1(e10,e13)=e10),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1057,f213])).
% 0.13/0.46 fof(f1059,plain,(
% 0.13/0.46 e12=e11|op1(e12,e11)=e11|op1(e13,e11)=e11),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f563,f496])).
% 0.13/0.46 fof(f1060,plain,(
% 0.13/0.46 op1(e12,e11)=e11|op1(e13,e11)=e11),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1059,f215])).
% 0.13/0.46 fof(f1062,plain,(
% 0.13/0.46 e22=e20|op2(e20,e22)=e20|op2(e20,e23)=e20),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f603,f509])).
% 0.13/0.46 fof(f1063,plain,(
% 0.13/0.46 op2(e20,e22)=e20|op2(e20,e23)=e20),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1062,f219])).
% 0.13/0.46 fof(f1064,plain,(
% 0.13/0.46 h1(e11)=e21|op2(e20,e20)=e22|op2(e20,e20)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f376,f510])).
% 0.13/0.46 fof(f1065,plain,(
% 0.13/0.46 h1(e11)=e21|h1(e11)=e22|op2(e20,e20)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f376,f1064])).
% 0.13/0.46 fof(f1066,plain,(
% 0.13/0.46 h1(e11)=e21|h1(e11)=e22|h1(e11)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f376,f1065])).
% 0.13/0.46 fof(f1067,plain,(
% 0.13/0.46 e22=e21|op2(e22,e21)=e21|op2(e23,e21)=e21),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f603,f512])).
% 0.13/0.46 fof(f1068,plain,(
% 0.13/0.46 op2(e22,e21)=e21|op2(e23,e21)=e21),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1067,f221])).
% 0.13/0.46 fof(f1069,plain,(
% 0.13/0.46 h2(e11)=e20|op2(e21,e21)=e22|op2(e21,e21)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f380,f514])).
% 0.13/0.46 fof(f1070,plain,(
% 0.13/0.46 h2(e11)=e20|h2(e11)=e22|op2(e21,e21)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f380,f1069])).
% 0.13/0.46 fof(f1071,plain,(
% 0.13/0.46 h2(e11)=e20|h2(e11)=e22|h2(e11)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f380,f1070])).
% 0.13/0.46 fof(f1072,plain,(
% 0.13/0.46 h3(e11)=e20|op2(e22,e22)=e21|op2(e22,e22)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f384,f518])).
% 0.13/0.46 fof(f1073,plain,(
% 0.13/0.46 h3(e11)=e20|h3(e11)=e21|op2(e22,e22)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f384,f1072])).
% 0.13/0.46 fof(f1074,plain,(
% 0.13/0.46 h3(e11)=e20|h3(e11)=e21|h3(e11)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f384,f1073])).
% 0.13/0.46 fof(f1077,plain,(
% 0.13/0.46 op1(e12,e11)=e11|e10=e11),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f524,f1060])).
% 0.13/0.46 fof(f1081,plain,(
% 0.13/0.46 ~op1(e13,e10)=e10),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f524,f158])).
% 0.13/0.46 fof(f1083,plain,(
% 0.13/0.46 ~op1(e11,e11)=e10),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f524,f126])).
% 0.13/0.46 fof(f1087,plain,(
% 0.13/0.46 op1(e12,e10)=e12|op1(e12,e13)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f501,f1089])).
% 0.13/0.46 fof(f1089,plain,(
% 0.13/0.46 ~op1(e12,e11)=e12),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f529])).
% 0.13/0.46 fof(f1092,plain,(
% 0.13/0.46 op1(e10,e12)=e11|op1(e11,e12)=e11|op1(e12,e12)=e11),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f55,f535])).
% 0.13/0.46 fof(f1095,plain,(
% 0.13/0.46 op1(e10,e10)=e11|op1(e11,e10)=e11|op1(e12,e10)=e11),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f39,f537])).
% 0.13/0.46 fof(f1096,plain,(
% 0.13/0.46 op1(e13,e10)=e10|op1(e13,e10)=e12|op1(e13,e10)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f32,f537])).
% 0.13/0.46 fof(f1101,plain,(
% 0.13/0.46 op1(e10,e13)=e10|op1(e10,e13)=e12|op1(e10,e13)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f23,f540])).
% 0.13/0.46 fof(f1102,plain,(
% 0.13/0.46 op1(e10,e13)=e12|op1(e11,e13)=e12|op1(e12,e13)=e12),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f541,f215])).
% 0.13/0.46 fof(f1105,plain,(
% 0.13/0.46 op1(e10,e13)=e10|op1(e11,e13)=e10|op1(e12,e13)=e10),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f545,f212])).
% 0.13/0.46 fof(f1106,plain,(
% 0.13/0.46 op1(e11,e13)=e12|op1(e12,e13)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1102,f550])).
% 0.13/0.46 fof(f1107,plain,(
% 0.13/0.46 op1(e11,e12)=e12|op1(e13,e12)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f500,f551])).
% 0.13/0.46 fof(f1112,plain,(
% 0.13/0.46 op1(e11,e11)=e10|op1(e11,e11)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f498,f555])).
% 0.13/0.46 fof(f1121,plain,(
% 0.13/0.46 op2(e22,e21)=e21|e20=e21),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f564,f1068])).
% 0.13/0.46 fof(f1123,plain,(
% 0.13/0.46 ~op2(e23,e20)=e20),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f564,f206])).
% 0.13/0.46 fof(f1128,plain,(
% 0.13/0.46 op2(e22,e20)=e22|op2(e22,e23)=e22),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f517,f1130])).
% 0.13/0.46 fof(f1130,plain,(
% 0.13/0.46 ~op2(e22,e21)=e22),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f569])).
% 0.13/0.46 fof(f1135,plain,(
% 0.13/0.46 op2(e23,e20)=e20|op2(e23,e20)=e22|op2(e23,e20)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f80,f577])).
% 0.13/0.46 fof(f1136,plain,(
% 0.13/0.46 op2(e22,e23)=e20|op2(e22,e23)=e22|op2(e22,e23)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f79,f578])).
% 0.13/0.46 fof(f1139,plain,(
% 0.13/0.46 op2(e20,e23)=e20|op2(e20,e23)=e22|op2(e20,e23)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f71,f580])).
% 0.13/0.46 fof(f1140,plain,(
% 0.13/0.46 op2(e20,e23)=e22|op2(e21,e23)=e22|op2(e22,e23)=e22),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f581,f221])).
% 0.13/0.46 fof(f1146,plain,(
% 0.13/0.46 op2(e21,e23)=e22|op2(e22,e23)=e22),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1140,f590])).
% 0.13/0.46 fof(f1147,plain,(
% 0.13/0.46 op2(e21,e22)=e22|op2(e23,e22)=e22),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f516,f591])).
% 0.13/0.46 fof(f1149,plain,(
% 0.13/0.46 h1(e11)=e21|h1(e11)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1066,f1151])).
% 0.13/0.46 fof(f1151,plain,(
% 0.13/0.46 ~h1(e11)=e22),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f376,f592])).
% 0.13/0.46 fof(f1153,plain,(
% 0.13/0.46 h2(e11)=e20|h2(e11)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1071,f1155])).
% 0.13/0.46 fof(f1155,plain,(
% 0.13/0.46 ~e22=h2(e11)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f380,f595])).
% 0.13/0.46 fof(f1170,plain,(
% 0.13/0.46 ~h2(e11)=e20),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f564,f638])).
% 0.13/0.46 fof(f1174,plain,(
% 0.13/0.46 op2(e20,e22)=e21|op2(e21,e22)=e21|h3(e11)=e21),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f663,f575])).
% 0.13/0.46 fof(f1203,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(e10)=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP10_prd|sP11_prd),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f524,f1039])).
% 0.13/0.46 fof(f1204,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e20=op2(e23,e21)|~h4(op1(e13,e12))=op2(e23,e22)|sP10_prd|sP11_prd),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f1203])).
% 0.13/0.46 fof(f1205,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e20=e20|~h4(op1(e13,e12))=op2(e23,e22)|sP10_prd|sP11_prd),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f564,f1204])).
% 0.13/0.46 fof(f1206,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP10_prd|sP11_prd),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1205])).
% 0.13/0.46 fof(f1207,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e11))=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1206,f1046])).
% 0.13/0.46 fof(f1209,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e11))=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(e11)=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1227,f1207])).
% 0.13/0.46 fof(f1222,plain,(
% 0.13/0.46 ~e11=op1(e12,e12)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1227,f155])).
% 0.13/0.46 fof(f1223,plain,(
% 0.13/0.46 ~op1(e12,e10)=e11),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1227,f152])).
% 0.13/0.46 fof(f1227,plain,(
% 0.13/0.46 op1(e12,e11)=e11),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1077,f212])).
% 0.13/0.46 fof(f1229,plain,(
% 0.13/0.46 op1(e11,e10)=e10|op1(e12,e10)=e10),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f492,f1081])).
% 0.13/0.46 fof(f1234,plain,(
% 0.13/0.46 op1(e13,e10)=e12|op1(e13,e10)=e13),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1096,f1081])).
% 0.13/0.46 fof(f1235,plain,(
% 0.13/0.46 op1(e10,e13)=e10|op1(e10,e13)=e13),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1101,f550])).
% 0.13/0.46 fof(f1238,plain,(
% 0.13/0.46 ~op1(e12,e13)=e12|~e13=e13),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1245,f285])).
% 0.13/0.46 fof(f1240,plain,(
% 0.13/0.46 ~op1(e10,e13)=e10|~e13=e13),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1245,f253])).
% 0.13/0.46 fof(f1245,plain,(
% 0.13/0.46 op1(e11,e11)=e13),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1112,f1083])).
% 0.13/0.46 fof(f1250,plain,(
% 0.13/0.46 ~e21=h3(e11)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1256,f656])).
% 0.13/0.46 fof(f1256,plain,(
% 0.13/0.46 op2(e22,e21)=e21),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1121,f218])).
% 0.13/0.46 fof(f1258,plain,(
% 0.13/0.46 op2(e21,e20)=e20|op2(e22,e20)=e20),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f508,f1123])).
% 0.13/0.46 fof(f1262,plain,(
% 0.13/0.46 op2(e23,e20)=e22|op2(e23,e20)=e23),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1135,f1123])).
% 0.13/0.46 fof(f1263,plain,(
% 0.13/0.46 op2(e20,e23)=e20|op2(e20,e23)=e23),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1139,f590])).
% 0.13/0.46 fof(f1269,plain,(
% 0.13/0.46 ~op2(e20,e23)=e20|~e23=e23),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1276,f633])).
% 0.13/0.46 fof(f1271,plain,(
% 0.13/0.46 ~op2(e22,e23)=e22|~e23=e23),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1276,f627])).
% 0.13/0.46 fof(f1272,plain,(
% 0.13/0.46 h2(e10)=op2(e21,e23)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1276,f624])).
% 0.13/0.46 fof(f1276,plain,(
% 0.13/0.46 h2(e11)=e23),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1153,f1170])).
% 0.13/0.46 fof(f1277,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(e13)=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(e11)=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1245,f1209])).
% 0.13/0.46 fof(f1278,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~e23=h2(e11)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(e11)=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f1277])).
% 0.13/0.46 fof(f1279,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~e23=e23|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(e11)=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1276,f1278])).
% 0.13/0.46 fof(f1280,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~e23=e23|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~e21=op2(e22,e21)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f1279])).
% 0.13/0.46 fof(f1281,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~e23=e23|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~e21=e21|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1256,f1280])).
% 0.13/0.46 fof(f1282,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)|sP11_prd),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1281])).
% 0.13/0.46 fof(f1283,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=op2(e21,e23)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1282,f1053])).
% 0.13/0.46 fof(f1333,plain,(
% 0.13/0.46 op1(e10,e12)=e11|op1(e11,e12)=e11),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1092,f1222])).
% 0.13/0.46 fof(f1334,plain,(
% 0.13/0.46 op1(e12,e12)=e10|op1(e12,e12)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f502,f1222])).
% 0.13/0.46 fof(f1335,plain,(
% 0.13/0.46 op1(e10,e10)=e11|op1(e11,e10)=e11),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1095,f1223])).
% 0.13/0.46 fof(f1340,plain,(
% 0.13/0.46 op1(e11,e13)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1106,f1343])).
% 0.13/0.46 fof(f1342,plain,(
% 0.13/0.46 op1(e12,e10)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1087,f1343])).
% 0.13/0.46 fof(f1343,plain,(
% 0.13/0.46 ~op1(e12,e13)=e12),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1238])).
% 0.13/0.46 fof(f1344,plain,(
% 0.13/0.46 op1(e10,e13)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1235,f1347])).
% 0.13/0.46 fof(f1345,plain,(
% 0.13/0.46 op1(e11,e13)=e10|op1(e12,e13)=e10),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1105,f1347])).
% 0.13/0.46 fof(f1346,plain,(
% 0.13/0.46 op1(e10,e12)=e10),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1058,f1347])).
% 0.13/0.46 fof(f1347,plain,(
% 0.13/0.46 ~op1(e10,e13)=e10),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1240])).
% 0.13/0.46 fof(f1356,plain,(
% 0.13/0.46 op2(e20,e22)=e21|op2(e21,e22)=e21),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1174,f1250])).
% 0.13/0.46 fof(f1357,plain,(
% 0.13/0.46 h3(e11)=e20|h3(e11)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1074,f1250])).
% 0.13/0.46 fof(f1368,plain,(
% 0.13/0.46 op2(e20,e23)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1263,f1371])).
% 0.13/0.46 fof(f1370,plain,(
% 0.13/0.46 op2(e20,e22)=e20),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1063,f1371])).
% 0.13/0.46 fof(f1371,plain,(
% 0.13/0.46 ~op2(e20,e23)=e20),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1269])).
% 0.13/0.46 fof(f1372,plain,(
% 0.13/0.46 op2(e21,e23)=e22),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1146,f1375])).
% 0.13/0.46 fof(f1373,plain,(
% 0.13/0.46 op2(e22,e23)=e20|op2(e22,e23)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1136,f1375])).
% 0.13/0.46 fof(f1374,plain,(
% 0.13/0.46 op2(e22,e20)=e22),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1128,f1375])).
% 0.13/0.46 fof(f1375,plain,(
% 0.13/0.46 ~op2(e22,e23)=e22),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1271])).
% 0.13/0.46 fof(f1377,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e10,e12))=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1272,f1283])).
% 0.13/0.46 fof(f1396,plain,(
% 0.13/0.46 ~op1(e11,e12)=e12),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1340,f151])).
% 0.13/0.46 fof(f1401,plain,(
% 0.13/0.46 op1(e11,e10)=e10|e12=e10),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1342,f1229])).
% 0.13/0.46 fof(f1406,plain,(
% 0.13/0.46 ~e12=e12|~op1(e12,e12)=e10),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1342,f274])).
% 0.13/0.46 fof(f1409,plain,(
% 0.13/0.46 ~e12=op1(e13,e10)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1342,f121])).
% 0.13/0.46 fof(f1420,plain,(
% 0.13/0.46 e12=e10|op1(e12,e13)=e10),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1340,f1345])).
% 0.13/0.46 fof(f1425,plain,(
% 0.13/0.46 op1(e12,e13)=e10),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1420,f213])).
% 0.13/0.46 fof(f1426,plain,(
% 0.13/0.46 e10=e11|op1(e11,e12)=e11),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1346,f1333])).
% 0.13/0.46 fof(f1443,plain,(
% 0.13/0.46 ~h1(e11)=e23),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1368,f614])).
% 0.13/0.46 fof(f1449,plain,(
% 0.13/0.46 ~e23=op2(e22,e23)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1368,f183])).
% 0.13/0.46 fof(f1452,plain,(
% 0.13/0.46 e20=e21|op2(e21,e22)=e21),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1370,f1356])).
% 0.13/0.46 fof(f1455,plain,(
% 0.13/0.46 ~e20=h3(e11)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1370,f660])).
% 0.13/0.46 fof(f1460,plain,(
% 0.13/0.46 h2(e10)=e22),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1372,f1272])).
% 0.13/0.46 fof(f1463,plain,(
% 0.13/0.46 op2(e21,e20)=e20|e22=e20),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1374,f1258])).
% 0.13/0.46 fof(f1472,plain,(
% 0.13/0.46 ~e22=op2(e23,e20)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1374,f169])).
% 0.13/0.46 fof(f1474,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(e10)=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1346,f1377])).
% 0.13/0.46 fof(f1475,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=op2(e20,e22)|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f1474])).
% 0.13/0.46 fof(f1476,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~h4(op1(e10,e13))=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1370,f1475])).
% 0.13/0.46 fof(f1477,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~h4(e13)=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1344,f1476])).
% 0.13/0.46 fof(f1478,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=op2(e20,e23)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f386,f1477])).
% 0.13/0.46 fof(f1479,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=e23|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(op1(e11,e13))=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1368,f1478])).
% 0.13/0.46 fof(f1480,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=e23|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~h4(e12)=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1340,f1479])).
% 0.13/0.46 fof(f1481,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=e23|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~h4(op1(e12,e10))=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f1480])).
% 0.13/0.46 fof(f1482,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=e23|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~h4(e12)=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1342,f1481])).
% 0.13/0.46 fof(f1483,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=e23|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~e22=op2(e22,e20)|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f1482])).
% 0.13/0.46 fof(f1484,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=e23|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~e22=e22|~h4(op1(e12,e12))=h3(e11)|~h4(op1(e12,e13))=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1374,f1483])).
% 0.13/0.46 fof(f1485,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=e23|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~e22=e22|~h4(op1(e12,e12))=h3(e11)|~h4(e10)=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1425,f1484])).
% 0.13/0.46 fof(f1486,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e23=e23|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~e22=e22|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f1485])).
% 0.13/0.46 fof(f1487,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e11,e10))=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1486])).
% 0.13/0.46 fof(f1527,plain,(
% 0.13/0.46 op1(e13,e12)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1107,f1396])).
% 0.13/0.46 fof(f1541,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(e10)=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1549,f1487])).
% 0.13/0.46 fof(f1542,plain,(
% 0.13/0.46 op1(e10,e10)=e11|e10=e11),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1549,f1335])).
% 0.13/0.46 fof(f1549,plain,(
% 0.13/0.46 op1(e11,e10)=e10),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1401,f213])).
% 0.13/0.46 fof(f1552,plain,(
% 0.13/0.46 op1(e12,e12)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1334,f1553])).
% 0.13/0.46 fof(f1553,plain,(
% 0.13/0.46 ~op1(e12,e12)=e10),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1406])).
% 0.13/0.46 fof(f1555,plain,(
% 0.13/0.46 op1(e13,e10)=e13),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1234,f1409])).
% 0.13/0.46 fof(f1568,plain,(
% 0.13/0.46 op1(e11,e12)=e11),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1426,f212])).
% 0.13/0.46 fof(f1570,plain,(
% 0.13/0.46 h1(e11)=e21),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1149,f1443])).
% 0.13/0.46 fof(f1574,plain,(
% 0.13/0.46 op2(e22,e23)=e20),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1373,f1449])).
% 0.13/0.46 fof(f1581,plain,(
% 0.13/0.46 e21=e22|op2(e23,e22)=e22),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1586,f1147])).
% 0.13/0.46 fof(f1586,plain,(
% 0.13/0.46 op2(e21,e22)=e21),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1452,f218])).
% 0.13/0.46 fof(f1587,plain,(
% 0.13/0.46 h3(e11)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1357,f1455])).
% 0.13/0.46 fof(f1608,plain,(
% 0.13/0.46 op2(e21,e20)=e20),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1463,f219])).
% 0.13/0.46 fof(f1612,plain,(
% 0.13/0.46 op2(e23,e20)=e23),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f1262,f1472])).
% 0.13/0.46 fof(f1652,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=op2(e21,e20)|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f669,f1541])).
% 0.13/0.46 fof(f1653,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~h4(op1(e11,e12))=op2(e21,e22)|~e22=h2(e10)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1608,f1652])).
% 0.13/0.46 fof(f1654,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~h4(e11)=op2(e21,e22)|~e22=h2(e10)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1568,f1653])).
% 0.13/0.46 fof(f1655,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e21=op2(e21,e22)|~e22=h2(e10)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f1654])).
% 0.13/0.46 fof(f1656,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e21=e21|~e22=h2(e10)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1586,f1655])).
% 0.13/0.46 fof(f1657,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e21=e21|~e22=e22|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(op1(e13,e12))=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1460,f1656])).
% 0.13/0.46 fof(f1658,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e21=e21|~e22=e22|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~h4(e12)=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1527,f1657])).
% 0.13/0.46 fof(f1659,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~e20=e20|~e21=e21|~e22=e22|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f673,f1658])).
% 0.13/0.46 fof(f1660,plain,(
% 0.13/0.46 ~h4(op1(e10,e10))=h1(e11)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f1659])).
% 0.13/0.46 fof(f1661,plain,(
% 0.13/0.46 ~h4(e11)=h1(e11)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1673,f1660])).
% 0.13/0.46 fof(f1673,plain,(
% 0.13/0.46 op1(e10,e10)=e11),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1542,f212])).
% 0.13/0.46 fof(f1711,plain,(
% 0.13/0.46 op2(e23,e22)=e22),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1581,f221])).
% 0.13/0.46 fof(f1733,plain,(
% 0.13/0.46 ~e21=h1(e11)|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f670,f1661])).
% 0.13/0.46 fof(f1734,plain,(
% 0.13/0.46 ~e21=e21|~h4(op1(e12,e12))=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1570,f1733])).
% 0.13/0.47 fof(f1735,plain,(
% 0.13/0.47 ~e21=e21|~h4(e13)=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1552,f1734])).
% 0.13/0.47 fof(f1736,plain,(
% 0.13/0.47 ~e21=e21|~e23=h3(e11)|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f386,f1735])).
% 0.13/0.47 fof(f1737,plain,(
% 0.13/0.47 ~e21=e21|~e23=e23|~e20=op2(e22,e23)|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1587,f1736])).
% 0.13/0.47 fof(f1738,plain,(
% 0.13/0.47 ~e21=e21|~e23=e23|~e20=e20|~h4(op1(e13,e10))=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1574,f1737])).
% 0.13/0.47 fof(f1739,plain,(
% 0.13/0.47 ~e21=e21|~e23=e23|~e20=e20|~h4(e13)=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1555,f1738])).
% 0.13/0.47 fof(f1740,plain,(
% 0.13/0.47 ~e21=e21|~e23=e23|~e20=e20|~e23=op2(e23,e20)|~e22=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f386,f1739])).
% 0.13/0.47 fof(f1741,plain,(
% 0.13/0.47 ~e21=e21|~e23=e23|~e20=e20|~e23=e23|~e22=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1612,f1740])).
% 0.13/0.47 fof(f1742,plain,(
% 0.13/0.47 ~e21=e21|~e23=e23|~e20=e20|~e23=e23|~e22=e22),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1711,f1741])).
% 0.13/0.47 fof(f1743,plain,(
% 0.13/0.47 ~e21=e21|~e23=e23|~e20=e20|~e22=e22),
% 0.13/0.47 inference(duplicate_literals_removal,[status(thm)],[f1742])).
% 0.13/0.47 fof(f1744,plain,(
% 0.13/0.47 $false),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f1743])).
% 0.13/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.47 % Elapsed time: 0.120420 seconds
% 0.13/0.47 % CPU time: 0.585100 seconds
% 0.13/0.47 % Total memory used: 137.893 MB
% 0.13/0.47 % Net memory used: 137.531 MB
%------------------------------------------------------------------------------