%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG117+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 : n026.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.10s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG117+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.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 12:59:06 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 0.10/0.49 % Refutation found
% 0.10/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.49 fof(f1,axiom,(
% 0.10/0.49 ( ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f2,axiom,(
% 0.10/0.49 ( ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f3,axiom,(
% 0.10/0.49 ( ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f4,axiom,(
% 0.10/0.49 ( ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f5,axiom,(
% 0.10/0.49 ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f6,axiom,(
% 0.10/0.49 ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f7,axiom,(
% 0.10/0.49 ( e10 != e11& e10 != e12& e10 != e13& e11 != e12& e11 != e13& e12 != e13 ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f8,axiom,(
% 0.10/0.49 ( e20 != e21& e20 != e22& e20 != e23& e21 != e22& e21 != e23& e22 != e23 ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f10,axiom,(
% 0.10/0.49 ( ( ( op1(e10,e10) = e10& op1(e10,e10) != e10 )| ( op1(e11,e11) = e10& op1(e11,e10) != e11 )| ( op1(e12,e12) = e10& op1(e12,e10) != e12 )| ( op1(e13,e13) = e10& op1(e13,e10) != e13 ) )& ( ( op1(e10,e10) = e11& op1(e10,e11) != e10 )| ( op1(e11,e11) = e11& op1(e11,e11) != e11 )| ( op1(e12,e12) = e11& op1(e12,e11) != e12 )| ( op1(e13,e13) = e11& op1(e13,e11) != e13 ) )& ( ( op1(e10,e10) = e12& op1(e10,e12) != e10 )| ( op1(e11,e11) = e12& op1(e11,e12) != e11 )| ( op1(e12,e12) = e12& op1(e12,e12) != e12 )| ( op1(e13,e13) = e12& op1(e13,e12) != e13 ) )& ( ( op1(e10,e10) = e13& op1(e10,e13) != e10 )| ( op1(e11,e11) = e13& op1(e11,e13) != e11 )| ( op1(e12,e12) = e13& op1(e12,e13) != e12 )| ( op1(e13,e13) = e13& op1(e13,e13) != e13 ) ) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f11,axiom,(
% 0.10/0.49 ( ( ( op2(e20,e20) = e20& op2(e20,e20) != e20 )| ( op2(e21,e21) = e20& op2(e21,e20) != e21 )| ( op2(e22,e22) = e20& op2(e22,e20) != e22 )| ( op2(e23,e23) = e20& op2(e23,e20) != e23 ) )& ( ( op2(e20,e20) = e21& op2(e20,e21) != e20 )| ( op2(e21,e21) = e21& op2(e21,e21) != e21 )| ( op2(e22,e22) = e21& op2(e22,e21) != e22 )| ( op2(e23,e23) = e21& op2(e23,e21) != e23 ) )& ( ( op2(e20,e20) = e22& op2(e20,e22) != e20 )| ( op2(e21,e21) = e22& op2(e21,e22) != e21 )| ( op2(e22,e22) = e22& op2(e22,e22) != e22 )| ( op2(e23,e23) = e22& op2(e23,e22) != e23 ) )& ( ( op2(e20,e20) = e23& op2(e20,e23) != e20 )| ( op2(e21,e21) = e23& op2(e21,e23) != e21 )| ( op2(e22,e22) = e23& op2(e22,e23) != e22 )| ( op2(e23,e23) = e23& op2(e23,e23) != e23 ) ) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f12,axiom,(
% 0.10/0.49 ( e10 = op1(e13,op1(e13,e13))& e11 = op1(op1(e13,e13),e13)& e12 = op1(e13,e13) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f13,axiom,(
% 0.10/0.49 ( e20 = op2(e23,op2(e23,e23))& e21 = op2(op2(e23,e23),e23)& e22 = op2(e23,e23) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f14,axiom,(
% 0.10/0.49 ( h1(e13) = e20& h1(e10) = op2(e20,op2(e20,e20))& h1(e11) = op2(op2(e20,e20),e20)& h1(e12) = op2(e20,e20) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f15,axiom,(
% 0.10/0.49 ( h2(e13) = e21& h2(e10) = op2(e21,op2(e21,e21))& h2(e11) = op2(op2(e21,e21),e21)& h2(e12) = op2(e21,e21) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f16,axiom,(
% 0.10/0.49 ( h3(e13) = e22& h3(e10) = op2(e22,op2(e22,e22))& h3(e11) = op2(op2(e22,e22),e22)& h3(e12) = op2(e22,e22) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f18,conjecture,(
% 0.10/0.49 ( ( 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.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f19,negated_conjecture,(
% 0.10/0.49 ~(( ( 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.10/0.49 inference(negated_conjecture,[status(cth)],[f18])).
% 0.10/0.49 fof(f27,plain,(
% 0.10/0.49 op1(e11,e13)=e10|op1(e11,e13)=e11|op1(e11,e13)=e12|op1(e11,e13)=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.49 fof(f32,plain,(
% 0.10/0.49 op1(e13,e10)=e10|op1(e13,e10)=e11|op1(e13,e10)=e12|op1(e13,e10)=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.49 fof(f36,plain,(
% 0.10/0.49 op1(e10,e10)=e10|op1(e10,e11)=e10|op1(e10,e12)=e10|op1(e10,e13)=e10),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.49 fof(f37,plain,(
% 0.10/0.49 op1(e10,e10)=e10|op1(e11,e10)=e10|op1(e12,e10)=e10|op1(e13,e10)=e10),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.49 fof(f41,plain,(
% 0.10/0.49 op1(e10,e10)=e12|op1(e11,e10)=e12|op1(e12,e10)=e12|op1(e13,e10)=e12),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.49 fof(f46,plain,(
% 0.10/0.49 op1(e11,e10)=e11|op1(e11,e11)=e11|op1(e11,e12)=e11|op1(e11,e13)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.49 fof(f51,plain,(
% 0.10/0.49 op1(e10,e11)=e13|op1(e11,e11)=e13|op1(e12,e11)=e13|op1(e13,e11)=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.49 fof(f56,plain,(
% 0.10/0.49 op1(e12,e10)=e12|op1(e12,e11)=e12|op1(e12,e12)=e12|op1(e12,e13)=e12),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.49 fof(f57,plain,(
% 0.10/0.49 op1(e10,e12)=e12|op1(e11,e12)=e12|op1(e12,e12)=e12|op1(e13,e12)=e12),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.49 fof(f62,plain,(
% 0.10/0.49 op1(e13,e10)=e11|op1(e13,e11)=e11|op1(e13,e12)=e11|op1(e13,e13)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.49 fof(f72,plain,(
% 0.10/0.49 op2(e21,e20)=e20|op2(e21,e20)=e21|op2(e21,e20)=e22|op2(e21,e20)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.49 fof(f75,plain,(
% 0.10/0.49 op2(e21,e23)=e20|op2(e21,e23)=e21|op2(e21,e23)=e22|op2(e21,e23)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.49 fof(f80,plain,(
% 0.10/0.49 op2(e23,e20)=e20|op2(e23,e20)=e21|op2(e23,e20)=e22|op2(e23,e20)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.49 fof(f84,plain,(
% 0.10/0.49 op2(e20,e20)=e20|op2(e20,e21)=e20|op2(e20,e22)=e20|op2(e20,e23)=e20),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f85,plain,(
% 0.10/0.49 op2(e20,e20)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f94,plain,(
% 0.10/0.49 op2(e21,e20)=e21|op2(e21,e21)=e21|op2(e21,e22)=e21|op2(e21,e23)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f99,plain,(
% 0.10/0.49 op2(e20,e21)=e23|op2(e21,e21)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f104,plain,(
% 0.10/0.49 op2(e22,e20)=e22|op2(e22,e21)=e22|op2(e22,e22)=e22|op2(e22,e23)=e22),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f105,plain,(
% 0.10/0.49 op2(e20,e22)=e22|op2(e21,e22)=e22|op2(e22,e22)=e22|op2(e23,e22)=e22),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f110,plain,(
% 0.10/0.49 op2(e23,e20)=e21|op2(e23,e21)=e21|op2(e23,e22)=e21|op2(e23,e23)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.49 fof(f118,plain,(
% 0.10/0.49 ~op1(e10,e10)=op1(e13,e10)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f130,plain,(
% 0.10/0.49 ~op1(e10,e12)=op1(e13,e12)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f133,plain,(
% 0.10/0.49 ~op1(e12,e12)=op1(e13,e12)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f137,plain,(
% 0.10/0.49 ~op1(e11,e13)=op1(e12,e13)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f138,plain,(
% 0.10/0.49 ~op1(e11,e13)=op1(e13,e13)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f146,plain,(
% 0.10/0.49 ~op1(e11,e10)=op1(e11,e11)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f150,plain,(
% 0.10/0.49 ~op1(e11,e11)=op1(e11,e13)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f155,plain,(
% 0.10/0.49 ~op1(e12,e11)=op1(e12,e12)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f157,plain,(
% 0.10/0.49 ~op1(e12,e12)=op1(e12,e13)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f159,plain,(
% 0.10/0.49 ~op1(e13,e10)=op1(e13,e12)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f160,plain,(
% 0.10/0.49 ~op1(e13,e10)=op1(e13,e13)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f166,plain,(
% 0.10/0.49 ~op2(e20,e20)=op2(e23,e20)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f168,plain,(
% 0.10/0.49 ~op2(e21,e20)=op2(e23,e20)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f178,plain,(
% 0.10/0.49 ~op2(e20,e22)=op2(e23,e22)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f181,plain,(
% 0.10/0.49 ~op2(e22,e22)=op2(e23,e22)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f185,plain,(
% 0.10/0.49 ~op2(e21,e23)=op2(e22,e23)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f186,plain,(
% 0.10/0.49 ~op2(e21,e23)=op2(e23,e23)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f194,plain,(
% 0.10/0.49 ~op2(e21,e20)=op2(e21,e21)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f198,plain,(
% 0.10/0.49 ~op2(e21,e21)=op2(e21,e23)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f205,plain,(
% 0.10/0.49 ~op2(e22,e22)=op2(e22,e23)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f207,plain,(
% 0.10/0.49 ~op2(e23,e20)=op2(e23,e22)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f208,plain,(
% 0.10/0.49 ~op2(e23,e20)=op2(e23,e23)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.49 fof(f212,plain,(
% 0.10/0.49 ~e10=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.49 fof(f213,plain,(
% 0.10/0.49 ~e10=e12),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.49 fof(f214,plain,(
% 0.10/0.49 ~e10=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.49 fof(f215,plain,(
% 0.10/0.49 ~e11=e12),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.49 fof(f216,plain,(
% 0.10/0.49 ~e11=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.49 fof(f217,plain,(
% 0.10/0.49 ~e12=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.49 fof(f218,plain,(
% 0.10/0.49 ~e20=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.49 fof(f219,plain,(
% 0.10/0.49 ~e20=e22),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.49 fof(f220,plain,(
% 0.10/0.49 ~e20=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.49 fof(f221,plain,(
% 0.10/0.49 ~e21=e22),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.49 fof(f222,plain,(
% 0.10/0.49 ~e21=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.49 fof(f223,plain,(
% 0.10/0.49 ~e22=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.49 fof(f240,definition,(
% 0.10/0.49 sP0_prd<=>(((op1(e10,e10)=e10&~op1(e10,e10)=e10)|(op1(e11,e11)=e10&~op1(e11,e10)=e11))|(op1(e12,e12)=e10&~op1(e12,e10)=e12))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.10/0.49 fof(f241,definition,(
% 0.10/0.49 sP1_prd<=>(((op1(e10,e10)=e11&~op1(e10,e11)=e10)|(op1(e11,e11)=e11&~op1(e11,e11)=e11))|(op1(e12,e12)=e11&~op1(e12,e11)=e12))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.10/0.49 fof(f242,definition,(
% 0.10/0.49 sP2_prd<=>(((op1(e10,e10)=e12&~op1(e10,e12)=e10)|(op1(e11,e11)=e12&~op1(e11,e12)=e11))|(op1(e12,e12)=e12&~op1(e12,e12)=e12))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.10/0.49 fof(f243,definition,(
% 0.10/0.49 sP3_prd<=>(((op1(e10,e10)=e13&~op1(e10,e13)=e10)|(op1(e11,e11)=e13&~op1(e11,e13)=e11))|(op1(e12,e12)=e13&~op1(e12,e13)=e12))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.10/0.49 fof(f244,plain,(
% 0.10/0.49 (((sP0_prd|(op1(e13,e13)=e10&~op1(e13,e10)=e13))&(sP1_prd|(op1(e13,e13)=e11&~op1(e13,e11)=e13)))&(sP2_prd|(op1(e13,e13)=e12&~op1(e13,e12)=e13)))&(sP3_prd|(op1(e13,e13)=e13&~op1(e13,e13)=e13))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f10,f243,f242,f241,f240])).
% 0.10/0.49 fof(f245,plain,(
% 0.10/0.49 sP0_prd|op1(e13,e13)=e10),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f244])).
% 0.10/0.49 fof(f247,plain,(
% 0.10/0.49 sP1_prd|op1(e13,e13)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f244])).
% 0.10/0.49 fof(f251,plain,(
% 0.10/0.49 sP3_prd|op1(e13,e13)=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f244])).
% 0.10/0.49 fof(f252,plain,(
% 0.10/0.49 sP3_prd|~op1(e13,e13)=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f244])).
% 0.10/0.49 fof(f253,definition,(
% 0.10/0.49 sP4_prd<=>(((op2(e20,e20)=e20&~op2(e20,e20)=e20)|(op2(e21,e21)=e20&~op2(e21,e20)=e21))|(op2(e22,e22)=e20&~op2(e22,e20)=e22))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.10/0.49 fof(f254,definition,(
% 0.10/0.49 sP5_prd<=>(((op2(e20,e20)=e21&~op2(e20,e21)=e20)|(op2(e21,e21)=e21&~op2(e21,e21)=e21))|(op2(e22,e22)=e21&~op2(e22,e21)=e22))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.10/0.49 fof(f255,definition,(
% 0.10/0.49 sP6_prd<=>(((op2(e20,e20)=e22&~op2(e20,e22)=e20)|(op2(e21,e21)=e22&~op2(e21,e22)=e21))|(op2(e22,e22)=e22&~op2(e22,e22)=e22))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.10/0.49 fof(f256,definition,(
% 0.10/0.49 sP7_prd<=>(((op2(e20,e20)=e23&~op2(e20,e23)=e20)|(op2(e21,e21)=e23&~op2(e21,e23)=e21))|(op2(e22,e22)=e23&~op2(e22,e23)=e22))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.10/0.49 fof(f257,plain,(
% 0.10/0.49 (((sP4_prd|(op2(e23,e23)=e20&~op2(e23,e20)=e23))&(sP5_prd|(op2(e23,e23)=e21&~op2(e23,e21)=e23)))&(sP6_prd|(op2(e23,e23)=e22&~op2(e23,e22)=e23)))&(sP7_prd|(op2(e23,e23)=e23&~op2(e23,e23)=e23))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f11,f256,f255,f254,f253])).
% 0.10/0.49 fof(f258,plain,(
% 0.10/0.49 sP4_prd|op2(e23,e23)=e20),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f257])).
% 0.10/0.49 fof(f260,plain,(
% 0.10/0.49 sP5_prd|op2(e23,e23)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f257])).
% 0.10/0.49 fof(f264,plain,(
% 0.10/0.49 sP7_prd|op2(e23,e23)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f257])).
% 0.10/0.49 fof(f265,plain,(
% 0.10/0.49 sP7_prd|~op2(e23,e23)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f257])).
% 0.10/0.49 fof(f266,plain,(
% 0.10/0.49 e10=op1(e13,op1(e13,e13))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.49 fof(f267,plain,(
% 0.10/0.49 e11=op1(op1(e13,e13),e13)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.49 fof(f268,plain,(
% 0.10/0.49 e12=op1(e13,e13)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.49 fof(f269,plain,(
% 0.10/0.49 e20=op2(e23,op2(e23,e23))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.49 fof(f270,plain,(
% 0.10/0.49 e21=op2(op2(e23,e23),e23)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.49 fof(f271,plain,(
% 0.10/0.49 e22=op2(e23,e23)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.49 fof(f273,plain,(
% 0.10/0.49 h1(e10)=op2(e20,op2(e20,e20))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.49 fof(f274,plain,(
% 0.10/0.49 h1(e11)=op2(op2(e20,e20),e20)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.49 fof(f275,plain,(
% 0.10/0.49 h1(e12)=op2(e20,e20)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.49 fof(f276,plain,(
% 0.10/0.49 h2(e13)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.49 fof(f277,plain,(
% 0.10/0.49 h2(e10)=op2(e21,op2(e21,e21))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.49 fof(f278,plain,(
% 0.10/0.49 h2(e11)=op2(op2(e21,e21),e21)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.49 fof(f279,plain,(
% 0.10/0.49 h2(e12)=op2(e21,e21)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.49 fof(f283,plain,(
% 0.10/0.49 h3(e12)=op2(e22,e22)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f16])).
% 0.10/0.49 fof(f288,plain,(
% 0.10/0.49 ((((((((((((((((((((((~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.10/0.49 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.10/0.49 fof(f289,definition,(
% 0.10/0.49 sP8_prd<=>(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.10/0.49 fof(f290,definition,(
% 0.10/0.49 sP9_prd<=>(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.10/0.49 fof(f291,definition,(
% 0.10/0.49 sP10_prd<=>(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.10/0.49 fof(f292,definition,(
% 0.10/0.49 sP11_prd<=>(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.10/0.49 fof(f293,definition,(
% 0.10/0.49 sP12_prd<=>(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.10/0.49 fof(f294,definition,(
% 0.10/0.49 sP13_prd<=>(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.10/0.49 fof(f295,definition,(
% 0.10/0.49 sP14_prd<=>(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.10/0.49 fof(f296,definition,(
% 0.10/0.49 sP15_prd<=>(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP15_prd])],[])).
% 0.10/0.49 fof(f297,definition,(
% 0.10/0.49 sP16_prd<=>(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 0.10/0.49 fof(f298,definition,(
% 0.10/0.49 sP17_prd<=>(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP17_prd])],[])).
% 0.10/0.49 fof(f299,definition,(
% 0.10/0.49 sP18_prd<=>(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP18_prd])],[])).
% 0.10/0.49 fof(f300,definition,(
% 0.10/0.49 sP19_prd<=>(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP19_prd])],[])).
% 0.10/0.49 fof(f301,plain,(
% 0.10/0.49 (((((((((((((((((((((~h1(op1(e10,e10))=op2(h1(e10),h1(e10))|~h1(op1(e10,e11))=op2(h1(e10),h1(e11)))|~h1(op1(e10,e12))=op2(h1(e10),h1(e12)))|~h1(op1(e10,e13))=op2(h1(e10),h1(e13)))|~h1(op1(e11,e10))=op2(h1(e11),h1(e10)))|~h1(op1(e11,e11))=op2(h1(e11),h1(e11)))|~h1(op1(e11,e12))=op2(h1(e11),h1(e12)))|~h1(op1(e11,e13))=op2(h1(e11),h1(e13)))|~h1(op1(e12,e10))=op2(h1(e12),h1(e10)))|~h1(op1(e12,e11))=op2(h1(e12),h1(e11)))|~h1(op1(e12,e12))=op2(h1(e12),h1(e12)))|~h1(op1(e12,e13))=op2(h1(e12),h1(e13)))|~h1(op1(e13,e10))=op2(h1(e13),h1(e10)))|~h1(op1(e13,e11))=op2(h1(e13),h1(e11)))|~h1(op1(e13,e12))=op2(h1(e13),h1(e12)))|~h1(op1(e13,e13))=op2(h1(e13),h1(e13)))|sP8_prd)|sP9_prd)|sP10_prd)|(((~h1(e10)=e23&~h1(e11)=e23)&~h1(e12)=e23)&~h1(e13)=e23))&(((((((((((((((((((~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11)))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12)))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13)))|~h2(op1(e11,e10))=op2(h2(e11),h2(e10)))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11)))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12)))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13)))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10)))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11)))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12)))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13)))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10)))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11)))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12)))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13)))|sP11_prd)|sP12_prd)|sP13_prd)|(((~h2(e10)=e23&~h2(e11)=e23)&~h2(e12)=e23)&~h2(e13)=e23)))&(((((((((((((((((((~h3(op1(e10,e10))=op2(h3(e10),h3(e10))|~h3(op1(e10,e11))=op2(h3(e10),h3(e11)))|~h3(op1(e10,e12))=op2(h3(e10),h3(e12)))|~h3(op1(e10,e13))=op2(h3(e10),h3(e13)))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10)))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11)))|~h3(op1(e11,e12))=op2(h3(e11),h3(e12)))|~h3(op1(e11,e13))=op2(h3(e11),h3(e13)))|~h3(op1(e12,e10))=op2(h3(e12),h3(e10)))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11)))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12)))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13)))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10)))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11)))|~h3(op1(e13,e12))=op2(h3(e13),h3(e12)))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13)))|sP14_prd)|sP15_prd)|sP16_prd)|(((~h3(e10)=e23&~h3(e11)=e23)&~h3(e12)=e23)&~h3(e13)=e23)))&(((((((((((((((((((~h4(op1(e10,e10))=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11)))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12)))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13)))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10)))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11)))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12)))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13)))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10)))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11)))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12)))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13)))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10)))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11)))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12)))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13)))|sP17_prd)|sP18_prd)|sP19_prd)|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f288,f300,f299,f298,f297,f296,f295,f294,f293,f292,f291,f290,f289])).
% 0.10/0.49 fof(f307,plain,(
% 0.10/0.49 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13))|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f301])).
% 0.10/0.49 fof(f318,definition,(
% 0.10/0.49 sP20_prd<=>((op1(e10,e10)=e10&~op1(e10,e10)=e10)|(op1(e11,e11)=e10&~op1(e11,e10)=e11))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP20_prd])],[])).
% 0.10/0.49 fof(f319,plain,(
% 0.10/0.49 sP0_prd<=>(sP20_prd|(op1(e12,e12)=e10&~op1(e12,e10)=e12))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f240,f318])).
% 0.10/0.49 fof(f320,plain,(
% 0.10/0.49 (~sP0_prd|(sP20_prd|(op1(e12,e12)=e10&~op1(e12,e10)=e12)))&(sP0_prd|(~sP20_prd&(~op1(e12,e12)=e10|op1(e12,e10)=e12)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f319])).
% 0.10/0.49 fof(f321,plain,(
% 0.10/0.49 ~sP0_prd|sP20_prd|op1(e12,e12)=e10),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f320])).
% 0.10/0.49 fof(f325,definition,(
% 0.10/0.49 sP21_prd<=>((op1(e10,e10)=e11&~op1(e10,e11)=e10)|(op1(e11,e11)=e11&~op1(e11,e11)=e11))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP21_prd])],[])).
% 0.10/0.49 fof(f326,plain,(
% 0.10/0.49 sP1_prd<=>(sP21_prd|(op1(e12,e12)=e11&~op1(e12,e11)=e12))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f241,f325])).
% 0.10/0.49 fof(f327,plain,(
% 0.10/0.49 (~sP1_prd|(sP21_prd|(op1(e12,e12)=e11&~op1(e12,e11)=e12)))&(sP1_prd|(~sP21_prd&(~op1(e12,e12)=e11|op1(e12,e11)=e12)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f326])).
% 0.10/0.49 fof(f328,plain,(
% 0.10/0.49 ~sP1_prd|sP21_prd|op1(e12,e12)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f327])).
% 0.10/0.49 fof(f339,definition,(
% 0.10/0.49 sP23_prd<=>((op1(e10,e10)=e13&~op1(e10,e13)=e10)|(op1(e11,e11)=e13&~op1(e11,e13)=e11))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP23_prd])],[])).
% 0.10/0.49 fof(f340,plain,(
% 0.10/0.49 sP3_prd<=>(sP23_prd|(op1(e12,e12)=e13&~op1(e12,e13)=e12))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f243,f339])).
% 0.10/0.49 fof(f341,plain,(
% 0.10/0.49 (~sP3_prd|(sP23_prd|(op1(e12,e12)=e13&~op1(e12,e13)=e12)))&(sP3_prd|(~sP23_prd&(~op1(e12,e12)=e13|op1(e12,e13)=e12)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f340])).
% 0.10/0.49 fof(f342,plain,(
% 0.10/0.49 ~sP3_prd|sP23_prd|op1(e12,e12)=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f341])).
% 0.10/0.49 fof(f346,definition,(
% 0.10/0.49 sP24_prd<=>((op2(e20,e20)=e20&~op2(e20,e20)=e20)|(op2(e21,e21)=e20&~op2(e21,e20)=e21))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP24_prd])],[])).
% 0.10/0.49 fof(f347,plain,(
% 0.10/0.49 sP4_prd<=>(sP24_prd|(op2(e22,e22)=e20&~op2(e22,e20)=e22))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f253,f346])).
% 0.10/0.49 fof(f348,plain,(
% 0.10/0.49 (~sP4_prd|(sP24_prd|(op2(e22,e22)=e20&~op2(e22,e20)=e22)))&(sP4_prd|(~sP24_prd&(~op2(e22,e22)=e20|op2(e22,e20)=e22)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f347])).
% 0.10/0.49 fof(f349,plain,(
% 0.10/0.49 ~sP4_prd|sP24_prd|op2(e22,e22)=e20),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f348])).
% 0.10/0.49 fof(f353,definition,(
% 0.10/0.49 sP25_prd<=>((op2(e20,e20)=e21&~op2(e20,e21)=e20)|(op2(e21,e21)=e21&~op2(e21,e21)=e21))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP25_prd])],[])).
% 0.10/0.49 fof(f354,plain,(
% 0.10/0.49 sP5_prd<=>(sP25_prd|(op2(e22,e22)=e21&~op2(e22,e21)=e22))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f254,f353])).
% 0.10/0.49 fof(f355,plain,(
% 0.10/0.49 (~sP5_prd|(sP25_prd|(op2(e22,e22)=e21&~op2(e22,e21)=e22)))&(sP5_prd|(~sP25_prd&(~op2(e22,e22)=e21|op2(e22,e21)=e22)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f354])).
% 0.10/0.49 fof(f356,plain,(
% 0.10/0.49 ~sP5_prd|sP25_prd|op2(e22,e22)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f355])).
% 0.10/0.49 fof(f367,definition,(
% 0.10/0.49 sP27_prd<=>((op2(e20,e20)=e23&~op2(e20,e23)=e20)|(op2(e21,e21)=e23&~op2(e21,e23)=e21))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP27_prd])],[])).
% 0.10/0.49 fof(f368,plain,(
% 0.10/0.49 sP7_prd<=>(sP27_prd|(op2(e22,e22)=e23&~op2(e22,e23)=e22))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f256,f367])).
% 0.10/0.49 fof(f369,plain,(
% 0.10/0.49 (~sP7_prd|(sP27_prd|(op2(e22,e22)=e23&~op2(e22,e23)=e22)))&(sP7_prd|(~sP27_prd&(~op2(e22,e22)=e23|op2(e22,e23)=e22)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f368])).
% 0.10/0.49 fof(f370,plain,(
% 0.10/0.49 ~sP7_prd|sP27_prd|op2(e22,e22)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f369])).
% 0.10/0.49 fof(f392,plain,(
% 0.10/0.49 (~sP11_prd|(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20))&(sP11_prd|(((h2(e10)=e20|h2(e11)=e20)|h2(e12)=e20)|h2(e13)=e20))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f292])).
% 0.10/0.49 fof(f395,plain,(
% 0.10/0.49 ~sP11_prd|~h2(e12)=e20),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f392])).
% 0.10/0.49 fof(f398,plain,(
% 0.10/0.49 (~sP12_prd|(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21))&(sP12_prd|(((h2(e10)=e21|h2(e11)=e21)|h2(e12)=e21)|h2(e13)=e21))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f293])).
% 0.10/0.49 fof(f402,plain,(
% 0.10/0.49 ~sP12_prd|~h2(e13)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f398])).
% 0.10/0.49 fof(f404,plain,(
% 0.10/0.49 (~sP13_prd|(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22))&(sP13_prd|(((h2(e10)=e22|h2(e11)=e22)|h2(e12)=e22)|h2(e13)=e22))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f294])).
% 0.10/0.49 fof(f405,plain,(
% 0.10/0.49 ~sP13_prd|~h2(e10)=e22),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f404])).
% 0.10/0.49 fof(f446,plain,(
% 0.10/0.49 (~sP20_prd|((op1(e10,e10)=e10&~op1(e10,e10)=e10)|(op1(e11,e11)=e10&~op1(e11,e10)=e11)))&(sP20_prd|((~op1(e10,e10)=e10|op1(e10,e10)=e10)&(~op1(e11,e11)=e10|op1(e11,e10)=e11)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f318])).
% 0.10/0.49 fof(f447,plain,(
% 0.10/0.49 ~sP20_prd|op1(e10,e10)=e10|op1(e11,e11)=e10),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f446])).
% 0.10/0.49 fof(f448,plain,(
% 0.10/0.49 ~sP20_prd|op1(e10,e10)=e10|~op1(e11,e10)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f446])).
% 0.10/0.49 fof(f449,plain,(
% 0.10/0.49 ~sP20_prd|~op1(e10,e10)=e10|op1(e11,e11)=e10),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f446])).
% 0.10/0.49 fof(f450,plain,(
% 0.10/0.49 ~sP20_prd|~op1(e10,e10)=e10|~op1(e11,e10)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f446])).
% 0.10/0.49 fof(f453,plain,(
% 0.10/0.49 (~sP21_prd|((op1(e10,e10)=e11&~op1(e10,e11)=e10)|(op1(e11,e11)=e11&~op1(e11,e11)=e11)))&(sP21_prd|((~op1(e10,e10)=e11|op1(e10,e11)=e10)&(~op1(e11,e11)=e11|op1(e11,e11)=e11)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f325])).
% 0.10/0.49 fof(f454,plain,(
% 0.10/0.49 ~sP21_prd|op1(e10,e10)=e11|op1(e11,e11)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f453])).
% 0.10/0.49 fof(f455,plain,(
% 0.10/0.49 ~sP21_prd|op1(e10,e10)=e11|~op1(e11,e11)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f453])).
% 0.10/0.49 fof(f456,plain,(
% 0.10/0.49 ~sP21_prd|~op1(e10,e11)=e10|op1(e11,e11)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f453])).
% 0.10/0.49 fof(f457,plain,(
% 0.10/0.49 ~sP21_prd|~op1(e10,e11)=e10|~op1(e11,e11)=e11),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f453])).
% 0.10/0.49 fof(f467,plain,(
% 0.10/0.49 (~sP23_prd|((op1(e10,e10)=e13&~op1(e10,e13)=e10)|(op1(e11,e11)=e13&~op1(e11,e13)=e11)))&(sP23_prd|((~op1(e10,e10)=e13|op1(e10,e13)=e10)&(~op1(e11,e11)=e13|op1(e11,e13)=e11)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f339])).
% 0.10/0.49 fof(f468,plain,(
% 0.10/0.49 ~sP23_prd|op1(e10,e10)=e13|op1(e11,e11)=e13),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f467])).
% 0.10/0.49 fof(f474,plain,(
% 0.10/0.49 (~sP24_prd|((op2(e20,e20)=e20&~op2(e20,e20)=e20)|(op2(e21,e21)=e20&~op2(e21,e20)=e21)))&(sP24_prd|((~op2(e20,e20)=e20|op2(e20,e20)=e20)&(~op2(e21,e21)=e20|op2(e21,e20)=e21)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f346])).
% 0.10/0.49 fof(f475,plain,(
% 0.10/0.49 ~sP24_prd|op2(e20,e20)=e20|op2(e21,e21)=e20),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f474])).
% 0.10/0.49 fof(f476,plain,(
% 0.10/0.49 ~sP24_prd|op2(e20,e20)=e20|~op2(e21,e20)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f474])).
% 0.10/0.49 fof(f477,plain,(
% 0.10/0.49 ~sP24_prd|~op2(e20,e20)=e20|op2(e21,e21)=e20),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f474])).
% 0.10/0.49 fof(f478,plain,(
% 0.10/0.49 ~sP24_prd|~op2(e20,e20)=e20|~op2(e21,e20)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f474])).
% 0.10/0.49 fof(f481,plain,(
% 0.10/0.49 (~sP25_prd|((op2(e20,e20)=e21&~op2(e20,e21)=e20)|(op2(e21,e21)=e21&~op2(e21,e21)=e21)))&(sP25_prd|((~op2(e20,e20)=e21|op2(e20,e21)=e20)&(~op2(e21,e21)=e21|op2(e21,e21)=e21)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f353])).
% 0.10/0.49 fof(f482,plain,(
% 0.10/0.49 ~sP25_prd|op2(e20,e20)=e21|op2(e21,e21)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f481])).
% 0.10/0.49 fof(f483,plain,(
% 0.10/0.49 ~sP25_prd|op2(e20,e20)=e21|~op2(e21,e21)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f481])).
% 0.10/0.49 fof(f484,plain,(
% 0.10/0.49 ~sP25_prd|~op2(e20,e21)=e20|op2(e21,e21)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f481])).
% 0.10/0.49 fof(f485,plain,(
% 0.10/0.49 ~sP25_prd|~op2(e20,e21)=e20|~op2(e21,e21)=e21),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f481])).
% 0.10/0.49 fof(f495,plain,(
% 0.10/0.49 (~sP27_prd|((op2(e20,e20)=e23&~op2(e20,e23)=e20)|(op2(e21,e21)=e23&~op2(e21,e23)=e21)))&(sP27_prd|((~op2(e20,e20)=e23|op2(e20,e23)=e20)&(~op2(e21,e21)=e23|op2(e21,e23)=e21)))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f367])).
% 0.10/0.49 fof(f496,plain,(
% 0.10/0.49 ~sP27_prd|op2(e20,e20)=e23|op2(e21,e21)=e23),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f495])).
% 0.10/0.49 fof(f502,plain,(
% 0.10/0.49 sP3_prd),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f252,f251])).
% 0.10/0.49 fof(f503,plain,(
% 0.10/0.49 sP7_prd),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f265,f264])).
% 0.10/0.49 fof(f504,plain,(
% 0.10/0.49 e11=op1(e12,e13)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f268,f267])).
% 0.10/0.49 fof(f505,plain,(
% 0.10/0.49 e10=op1(e13,e12)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f268,f266])).
% 0.10/0.49 fof(f507,plain,(
% 0.10/0.49 sP1_prd|e12=e11),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f268,f247])).
% 0.10/0.49 fof(f508,plain,(
% 0.10/0.49 sP0_prd|e12=e10),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f268,f245])).
% 0.10/0.49 fof(f511,plain,(
% 0.10/0.49 ~op1(e13,e10)=e12),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f268,f160])).
% 0.10/0.49 fof(f513,plain,(
% 0.10/0.49 ~op1(e11,e13)=e12),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f268,f138])).
% 0.10/0.49 fof(f520,plain,(
% 0.10/0.49 op1(e13,e10)=e11|op1(e13,e11)=e11|op1(e13,e12)=e11|e12=e11),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f268,f62])).
% 0.10/0.49 fof(f524,plain,(
% 0.10/0.49 e21=op2(e22,e23)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f271,f270])).
% 0.10/0.49 fof(f525,plain,(
% 0.10/0.49 e20=op2(e23,e22)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f271,f269])).
% 0.10/0.49 fof(f527,plain,(
% 0.10/0.49 sP5_prd|e22=e21),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f271,f260])).
% 0.10/0.49 fof(f528,plain,(
% 0.10/0.49 sP4_prd|e22=e20),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f271,f258])).
% 0.10/0.49 fof(f531,plain,(
% 0.10/0.49 ~op2(e23,e20)=e22),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f271,f208])).
% 0.10/0.49 fof(f533,plain,(
% 0.10/0.49 ~op2(e21,e23)=e22),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f271,f186])).
% 0.10/0.49 fof(f540,plain,(
% 0.10/0.49 op2(e23,e20)=e21|op2(e23,e21)=e21|op2(e23,e22)=e21|e22=e21),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f271,f110])).
% 0.10/0.49 fof(f544,plain,(
% 0.10/0.49 h1(e11)=op2(h1(e12),e20)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f275,f274])).
% 0.10/0.49 fof(f545,plain,(
% 0.10/0.49 h1(e10)=op2(e20,h1(e12))),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f275,f273])).
% 0.10/0.49 fof(f549,plain,(
% 0.10/0.49 ~h1(e12)=op2(e23,e20)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f275,f166])).
% 0.10/0.49 fof(f558,plain,(
% 0.10/0.49 h1(e12)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f275,f85])).
% 0.10/0.49 fof(f559,plain,(
% 0.10/0.49 h1(e12)=e20|op2(e20,e21)=e20|op2(e20,e22)=e20|op2(e20,e23)=e20),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f275,f84])).
% 0.10/0.49 fof(f561,plain,(
% 0.10/0.49 h2(e11)=op2(h2(e12),e21)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f279,f278])).
% 0.10/0.49 fof(f562,plain,(
% 0.10/0.49 h2(e10)=op2(e21,h2(e12))),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f279,f277])).
% 0.10/0.49 fof(f563,plain,(
% 0.10/0.49 ~h2(e12)=op2(e21,e23)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f279,f198])).
% 0.10/0.49 fof(f565,plain,(
% 0.10/0.49 ~op2(e21,e20)=h2(e12)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f279,f194])).
% 0.10/0.49 fof(f569,plain,(
% 0.10/0.49 op2(e20,e21)=e23|h2(e12)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f279,f99])).
% 0.10/0.49 fof(f574,plain,(
% 0.10/0.49 op2(e21,e20)=e21|h2(e12)=e21|op2(e21,e22)=e21|op2(e21,e23)=e21),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f279,f94])).
% 0.10/0.49 fof(f580,plain,(
% 0.10/0.49 ~h3(e12)=op2(e22,e23)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f283,f205])).
% 0.10/0.49 fof(f583,plain,(
% 0.10/0.49 ~h3(e12)=op2(e23,e22)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f283,f181])).
% 0.10/0.49 fof(f588,plain,(
% 0.10/0.49 op2(e20,e22)=e22|op2(e21,e22)=e22|h3(e12)=e22|op2(e23,e22)=e22),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f283,f105])).
% 0.10/0.49 fof(f589,plain,(
% 0.10/0.49 op2(e22,e20)=e22|op2(e22,e21)=e22|h3(e12)=e22|op2(e22,e23)=e22),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f283,f104])).
% 0.10/0.49 fof(f654,plain,(
% 0.10/0.49 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f276,f307])).
% 0.10/0.49 fof(f655,plain,(
% 0.10/0.49 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f276,f654])).
% 0.10/0.49 fof(f656,plain,(
% 0.10/0.49 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(h2(e13),h2(e10))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f276,f655])).
% 0.10/0.49 fof(f657,plain,(
% 0.10/0.49 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f276,f656])).
% 0.10/0.50 fof(f658,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f276,f657])).
% 0.10/0.50 fof(f659,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f276,f658])).
% 0.10/0.50 fof(f660,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(e12)=op2(h2(e13),h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f268,f659])).
% 0.10/0.50 fof(f661,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,h2(e13))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f276,f660])).
% 0.10/0.50 fof(f662,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e21)|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f276,f661])).
% 0.10/0.50 fof(f663,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|~h2(e12)=h2(e12)|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f279,f662])).
% 0.10/0.50 fof(f664,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP11_prd|sP12_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(trivial_equality_resolution,[status(thm)],[f663])).
% 0.10/0.50 fof(f894,plain,(
% 0.10/0.50 sP23_prd|op1(e12,e12)=e13),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f342,f502])).
% 0.10/0.50 fof(f896,plain,(
% 0.10/0.50 ~sP4_prd|sP24_prd|h3(e12)=e20),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f283,f349])).
% 0.10/0.50 fof(f898,plain,(
% 0.10/0.50 ~sP5_prd|sP25_prd|h3(e12)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f283,f356])).
% 0.10/0.50 fof(f903,plain,(
% 0.10/0.50 ~sP7_prd|sP27_prd|h3(e12)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f283,f370])).
% 0.10/0.50 fof(f904,plain,(
% 0.10/0.50 sP27_prd|h3(e12)=e23),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f903,f503])).
% 0.10/0.50 fof(f921,plain,(
% 0.10/0.50 ~sP12_prd|~e21=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f276,f402])).
% 0.10/0.50 fof(f923,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f664,f925])).
% 0.10/0.50 fof(f925,plain,(
% 0.10/0.50 ~sP12_prd),
% 0.10/0.50 inference(trivial_equality_resolution,[status(thm)],[f921])).
% 0.10/0.50 fof(f959,plain,(
% 0.10/0.50 ~sP20_prd|op1(e11,e11)=e10),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f449,f447])).
% 0.10/0.50 fof(f960,plain,(
% 0.10/0.50 ~sP20_prd|~op1(e11,e10)=e11),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f450,f448])).
% 0.10/0.50 fof(f961,plain,(
% 0.10/0.50 ~sP21_prd|op1(e10,e10)=e11),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f455,f454])).
% 0.10/0.50 fof(f962,plain,(
% 0.10/0.50 ~sP21_prd|~op1(e10,e11)=e10),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f457,f456])).
% 0.10/0.50 fof(f963,plain,(
% 0.10/0.50 ~sP24_prd|h1(e12)=e20|op2(e21,e21)=e20),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f275,f475])).
% 0.10/0.50 fof(f964,plain,(
% 0.10/0.50 ~sP24_prd|h1(e12)=e20|h2(e12)=e20),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f279,f963])).
% 0.10/0.50 fof(f965,plain,(
% 0.10/0.50 ~sP24_prd|h1(e12)=e20|~op2(e21,e20)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f275,f476])).
% 0.10/0.50 fof(f966,plain,(
% 0.10/0.50 ~sP24_prd|~h1(e12)=e20|op2(e21,e21)=e20),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f275,f477])).
% 0.10/0.50 fof(f967,plain,(
% 0.10/0.50 ~sP24_prd|~h1(e12)=e20|h2(e12)=e20),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f279,f966])).
% 0.10/0.50 fof(f968,plain,(
% 0.10/0.50 ~sP24_prd|h2(e12)=e20),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f967,f964])).
% 0.10/0.50 fof(f969,plain,(
% 0.10/0.50 ~sP24_prd|~h1(e12)=e20|~op2(e21,e20)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f275,f478])).
% 0.10/0.50 fof(f970,plain,(
% 0.10/0.50 ~sP24_prd|~op2(e21,e20)=e21),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f969,f965])).
% 0.10/0.50 fof(f972,plain,(
% 0.10/0.50 ~sP25_prd|h1(e12)=e21|op2(e21,e21)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f275,f482])).
% 0.10/0.50 fof(f973,plain,(
% 0.10/0.50 ~sP25_prd|h1(e12)=e21|h2(e12)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f279,f972])).
% 0.10/0.50 fof(f974,plain,(
% 0.10/0.50 ~sP25_prd|h1(e12)=e21|~op2(e21,e21)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f275,f483])).
% 0.10/0.50 fof(f975,plain,(
% 0.10/0.50 ~sP25_prd|h1(e12)=e21|~h2(e12)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f279,f974])).
% 0.10/0.50 fof(f976,plain,(
% 0.10/0.50 ~sP25_prd|h1(e12)=e21),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f975,f973])).
% 0.10/0.50 fof(f977,plain,(
% 0.10/0.50 ~sP25_prd|~op2(e20,e21)=e20|h2(e12)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f279,f484])).
% 0.10/0.50 fof(f978,plain,(
% 0.10/0.50 ~sP25_prd|~op2(e20,e21)=e20|~h2(e12)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f279,f485])).
% 0.10/0.50 fof(f979,plain,(
% 0.10/0.50 ~sP25_prd|~op2(e20,e21)=e20),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f978,f977])).
% 0.10/0.50 fof(f987,plain,(
% 0.10/0.50 ~sP27_prd|h1(e12)=e23|op2(e21,e21)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f275,f496])).
% 0.10/0.50 fof(f988,plain,(
% 0.10/0.50 ~sP27_prd|h1(e12)=e23|h2(e12)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f279,f987])).
% 0.10/0.50 fof(f994,plain,(
% 0.10/0.50 ~op1(e12,e12)=e11),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f504,f157])).
% 0.10/0.50 fof(f997,plain,(
% 0.10/0.50 ~op1(e11,e13)=e11),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f504,f137])).
% 0.10/0.50 fof(f1000,plain,(
% 0.10/0.50 op1(e12,e10)=e12|op1(e12,e11)=e12|op1(e12,e12)=e12|e11=e12),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f504,f56])).
% 0.10/0.50 fof(f1006,plain,(
% 0.10/0.50 ~op1(e13,e10)=e10),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f505,f159])).
% 0.10/0.50 fof(f1007,plain,(
% 0.10/0.50 ~op1(e12,e12)=e10),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f505,f133])).
% 0.10/0.50 fof(f1009,plain,(
% 0.10/0.50 ~op1(e10,e12)=e10),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f505,f130])).
% 0.10/0.50 fof(f1011,plain,(
% 0.10/0.50 op1(e10,e12)=e12|op1(e11,e12)=e12|op1(e12,e12)=e12|e10=e12),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f505,f57])).
% 0.10/0.50 fof(f1016,plain,(
% 0.10/0.50 sP21_prd|op1(e12,e12)=e11),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f328,f1017])).
% 0.10/0.50 fof(f1017,plain,(
% 0.10/0.50 sP1_prd),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f507,f215])).
% 0.10/0.50 fof(f1019,plain,(
% 0.10/0.50 sP20_prd|op1(e12,e12)=e10),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f321,f1020])).
% 0.10/0.50 fof(f1020,plain,(
% 0.10/0.50 sP0_prd),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f508,f213])).
% 0.10/0.50 fof(f1024,plain,(
% 0.10/0.50 op1(e10,e10)=e12|op1(e11,e10)=e12|op1(e12,e10)=e12),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f41,f511])).
% 0.10/0.50 fof(f1025,plain,(
% 0.10/0.50 op1(e13,e10)=e10|op1(e13,e10)=e11|op1(e13,e10)=e13),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f32,f511])).
% 0.10/0.50 fof(f1028,plain,(
% 0.10/0.50 op1(e11,e13)=e10|op1(e11,e13)=e11|op1(e11,e13)=e13),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f27,f513])).
% 0.10/0.50 fof(f1035,plain,(
% 0.10/0.50 op1(e13,e10)=e11|op1(e13,e11)=e11|e10=e11|e12=e11),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f505,f520])).
% 0.10/0.50 fof(f1036,plain,(
% 0.10/0.50 op1(e13,e10)=e11|op1(e13,e11)=e11|e12=e11),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1035,f212])).
% 0.10/0.50 fof(f1044,plain,(
% 0.10/0.50 ~op2(e21,e23)=e21),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f524,f185])).
% 0.10/0.50 fof(f1049,plain,(
% 0.10/0.50 ~op2(e23,e20)=e20),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f525,f207])).
% 0.10/0.50 fof(f1051,plain,(
% 0.10/0.50 ~op2(e20,e22)=e20),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f525,f178])).
% 0.10/0.50 fof(f1054,plain,(
% 0.10/0.50 sP25_prd|h3(e12)=e21),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f898,f1055])).
% 0.10/0.50 fof(f1055,plain,(
% 0.10/0.50 sP5_prd),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f527,f221])).
% 0.10/0.50 fof(f1057,plain,(
% 0.10/0.50 sP24_prd|h3(e12)=e20),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f896,f1058])).
% 0.10/0.50 fof(f1058,plain,(
% 0.10/0.50 sP4_prd),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f528,f219])).
% 0.10/0.50 fof(f1061,plain,(
% 0.10/0.50 op2(e23,e20)=e20|op2(e23,e20)=e21|op2(e23,e20)=e23),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f80,f531])).
% 0.10/0.50 fof(f1063,plain,(
% 0.10/0.50 op2(e21,e23)=e20|op2(e21,e23)=e21|op2(e21,e23)=e23),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f75,f533])).
% 0.10/0.50 fof(f1069,plain,(
% 0.10/0.50 op2(e23,e20)=e21|op2(e23,e21)=e21|e20=e21|e22=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f525,f540])).
% 0.10/0.50 fof(f1070,plain,(
% 0.10/0.50 op2(e23,e20)=e21|op2(e23,e21)=e21|e22=e21),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1069,f218])).
% 0.10/0.50 fof(f1086,plain,(
% 0.10/0.50 ~h3(e12)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f524,f580])).
% 0.10/0.50 fof(f1088,plain,(
% 0.10/0.50 ~h3(e12)=e20),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f525,f583])).
% 0.10/0.50 fof(f1093,plain,(
% 0.10/0.50 op2(e20,e22)=e22|op2(e21,e22)=e22|h3(e12)=e22|e20=e22),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f525,f588])).
% 0.10/0.50 fof(f1094,plain,(
% 0.10/0.50 op2(e20,e22)=e22|op2(e21,e22)=e22|h3(e12)=e22),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1093,f219])).
% 0.10/0.50 fof(f1095,plain,(
% 0.10/0.50 op2(e22,e20)=e22|op2(e22,e21)=e22|h3(e12)=e22|e21=e22),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f524,f589])).
% 0.10/0.50 fof(f1096,plain,(
% 0.10/0.50 op2(e22,e20)=e22|op2(e22,e21)=e22|h3(e12)=e22),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1095,f221])).
% 0.10/0.50 fof(f1125,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(e11)=op2(h2(e12),e21)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f504,f923])).
% 0.10/0.50 fof(f1126,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(e11)=h2(e11)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(op1(e13,e12))=op2(e21,h2(e12))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f561,f1125])).
% 0.10/0.50 fof(f1127,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(e11)=h2(e11)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(e10)=op2(e21,h2(e12))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f505,f1126])).
% 0.10/0.50 fof(f1128,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(e11)=h2(e11)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|~h2(e10)=h2(e10)|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f562,f1127])).
% 0.10/0.50 fof(f1129,plain,(
% 0.10/0.50 ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(trivial_equality_resolution,[status(thm)],[f1128])).
% 0.10/0.50 fof(f1164,plain,(
% 0.10/0.50 op1(e11,e10)=e11|op1(e11,e11)=e11|op1(e11,e12)=e11),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f46,f997])).
% 0.10/0.50 fof(f1167,plain,(
% 0.10/0.50 op1(e12,e10)=e12|op1(e12,e11)=e12|op1(e12,e12)=e12),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1000,f215])).
% 0.10/0.50 fof(f1171,plain,(
% 0.10/0.50 op1(e10,e10)=e10|op1(e11,e10)=e10|op1(e12,e10)=e10),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f37,f1006])).
% 0.10/0.50 fof(f1176,plain,(
% 0.10/0.50 op1(e10,e10)=e10|op1(e10,e11)=e10|op1(e10,e13)=e10),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f36,f1009])).
% 0.10/0.50 fof(f1179,plain,(
% 0.10/0.50 op1(e10,e12)=e12|op1(e11,e12)=e12|op1(e12,e12)=e12),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1011,f213])).
% 0.10/0.50 fof(f1181,plain,(
% 0.10/0.50 ~op1(e10,e11)=e10),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f962,f1183])).
% 0.10/0.50 fof(f1182,plain,(
% 0.10/0.50 op1(e10,e10)=e11),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f961,f1183])).
% 0.10/0.50 fof(f1183,plain,(
% 0.10/0.50 sP21_prd),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1016,f994])).
% 0.10/0.50 fof(f1184,plain,(
% 0.10/0.50 ~op1(e11,e10)=e11),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f960,f1186])).
% 0.10/0.50 fof(f1185,plain,(
% 0.10/0.50 op1(e11,e11)=e10),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f959,f1186])).
% 0.10/0.50 fof(f1186,plain,(
% 0.10/0.50 sP20_prd),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1019,f1007])).
% 0.10/0.50 fof(f1188,plain,(
% 0.10/0.50 op1(e13,e10)=e11|op1(e13,e10)=e13),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1025,f1006])).
% 0.10/0.50 fof(f1189,plain,(
% 0.10/0.50 op1(e11,e13)=e10|op1(e11,e13)=e13),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1028,f997])).
% 0.10/0.50 fof(f1195,plain,(
% 0.10/0.50 op2(e21,e20)=e21|h2(e12)=e21|op2(e21,e22)=e21),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f574,f1044])).
% 0.10/0.50 fof(f1200,plain,(
% 0.10/0.50 h1(e12)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f558,f1049])).
% 0.10/0.50 fof(f1203,plain,(
% 0.10/0.50 h1(e12)=e20|op2(e20,e21)=e20|op2(e20,e23)=e20),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f559,f1051])).
% 0.10/0.50 fof(f1206,plain,(
% 0.10/0.50 ~op2(e20,e21)=e20),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f979,f1208])).
% 0.10/0.50 fof(f1207,plain,(
% 0.10/0.50 h1(e12)=e21),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f976,f1208])).
% 0.10/0.50 fof(f1208,plain,(
% 0.10/0.50 sP25_prd),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1054,f1086])).
% 0.10/0.50 fof(f1209,plain,(
% 0.10/0.50 ~op2(e21,e20)=e21),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f970,f1211])).
% 0.10/0.50 fof(f1210,plain,(
% 0.10/0.50 h2(e12)=e20),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f968,f1211])).
% 0.10/0.50 fof(f1211,plain,(
% 0.10/0.50 sP24_prd),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1057,f1088])).
% 0.10/0.50 fof(f1213,plain,(
% 0.10/0.50 op2(e23,e20)=e21|op2(e23,e20)=e23),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1061,f1049])).
% 0.10/0.50 fof(f1214,plain,(
% 0.10/0.50 op2(e21,e23)=e20|op2(e21,e23)=e23),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1063,f1044])).
% 0.10/0.50 fof(f1217,plain,(
% 0.10/0.50 op1(e10,e10)=e10|op1(e10,e13)=e10),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1176,f1181])).
% 0.10/0.50 fof(f1221,plain,(
% 0.10/0.50 e11=e10|op1(e11,e10)=e10|op1(e12,e10)=e10),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1182,f1171])).
% 0.10/0.50 fof(f1225,plain,(
% 0.10/0.50 e11=e12|op1(e11,e10)=e12|op1(e12,e10)=e12),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1182,f1024])).
% 0.10/0.50 fof(f1231,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1182,f1129])).
% 0.10/0.50 fof(f1237,plain,(
% 0.10/0.50 ~sP23_prd|e11=e13|op1(e11,e11)=e13),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1182,f468])).
% 0.10/0.50 fof(f1243,plain,(
% 0.10/0.50 ~e11=op1(e13,e10)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1182,f118])).
% 0.10/0.50 fof(f1249,plain,(
% 0.10/0.50 op1(e11,e11)=e11|op1(e11,e12)=e11),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1164,f1184])).
% 0.10/0.50 fof(f1258,plain,(
% 0.10/0.50 ~e10=op1(e11,e13)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1185,f150])).
% 0.10/0.50 fof(f1260,plain,(
% 0.10/0.50 ~op1(e11,e10)=e10),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1185,f146])).
% 0.10/0.50 fof(f1264,plain,(
% 0.10/0.50 op1(e10,e11)=e13|e10=e13|op1(e12,e11)=e13|op1(e13,e11)=e13),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1185,f51])).
% 0.10/0.50 fof(f1267,plain,(
% 0.10/0.50 h1(e12)=e20|op2(e20,e23)=e20),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1203,f1206])).
% 0.10/0.50 fof(f1271,plain,(
% 0.10/0.50 e21=e20|op2(e21,e20)=e20|op2(e22,e20)=e20),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1207,f1200])).
% 0.10/0.50 fof(f1281,plain,(
% 0.10/0.50 ~e21=op2(e23,e20)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1207,f549])).
% 0.10/0.50 fof(f1285,plain,(
% 0.10/0.50 h1(e10)=op2(e20,e21)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1207,f545])).
% 0.10/0.50 fof(f1286,plain,(
% 0.10/0.50 h1(e11)=op2(e21,e20)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1207,f544])).
% 0.10/0.50 fof(f1288,plain,(
% 0.10/0.50 ~sP27_prd|e21=e23|h2(e12)=e23),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1207,f988])).
% 0.10/0.50 fof(f1296,plain,(
% 0.10/0.50 h2(e12)=e21|op2(e21,e22)=e21),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1195,f1209])).
% 0.10/0.50 fof(f1297,plain,(
% 0.10/0.50 op2(e21,e20)=e20|op2(e21,e20)=e22|op2(e21,e20)=e23),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f72,f1209])).
% 0.10/0.50 fof(f1305,plain,(
% 0.10/0.50 op2(e20,e21)=e23|e20=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1210,f569])).
% 0.10/0.50 fof(f1309,plain,(
% 0.10/0.50 ~op2(e21,e20)=e20),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1210,f565])).
% 0.10/0.50 fof(f1311,plain,(
% 0.10/0.50 ~e20=op2(e21,e23)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1210,f563])).
% 0.10/0.50 fof(f1312,plain,(
% 0.10/0.50 h2(e10)=op2(e21,e20)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1210,f562])).
% 0.10/0.50 fof(f1313,plain,(
% 0.10/0.50 h2(e11)=op2(e20,e21)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1210,f561])).
% 0.10/0.50 fof(f1319,plain,(
% 0.10/0.50 ~sP11_prd|~e20=e20),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1210,f395])).
% 0.10/0.50 fof(f1321,plain,(
% 0.10/0.50 e11=e10|op1(e10,e13)=e10),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1182,f1217])).
% 0.10/0.50 fof(f1330,plain,(
% 0.10/0.50 op1(e10,e13)=e10),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1321,f212])).
% 0.10/0.50 fof(f1331,plain,(
% 0.10/0.50 op1(e11,e10)=e10|op1(e12,e10)=e10),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1221,f212])).
% 0.10/0.50 fof(f1333,plain,(
% 0.10/0.50 op1(e11,e10)=e12|op1(e12,e10)=e12),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1225,f215])).
% 0.10/0.50 fof(f1359,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(op1(e10,e13))=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1210,f1231])).
% 0.10/0.50 fof(f1360,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1330,f1359])).
% 0.10/0.50 fof(f1361,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1185,f1360])).
% 0.10/0.50 fof(f1362,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1210,f1361])).
% 0.10/0.50 fof(f1363,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1210,f1362])).
% 0.10/0.50 fof(f1364,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1210,f1363])).
% 0.10/0.50 fof(f1365,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=op2(e20,h2(e12))|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1210,f1364])).
% 0.10/0.50 fof(f1366,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=op2(e20,e20)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1210,f1365])).
% 0.10/0.50 fof(f1367,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=h1(e12)|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f275,f1366])).
% 0.10/0.50 fof(f1368,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1207,f1367])).
% 0.10/0.50 fof(f1411,plain,(
% 0.10/0.50 ~sP23_prd|e11=e13|e10=e13),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1185,f1237])).
% 0.10/0.50 fof(f1412,plain,(
% 0.10/0.50 ~sP23_prd|e10=e13),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1411,f216])).
% 0.10/0.50 fof(f1420,plain,(
% 0.10/0.50 op1(e13,e10)=e13),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1188,f1243])).
% 0.10/0.50 fof(f1421,plain,(
% 0.10/0.50 op1(e13,e11)=e11|e12=e11),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1036,f1243])).
% 0.10/0.50 fof(f1426,plain,(
% 0.10/0.50 e10=e11|op1(e11,e12)=e11),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1185,f1249])).
% 0.10/0.50 fof(f1430,plain,(
% 0.10/0.50 ~h2(e11)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1444,f1368])).
% 0.10/0.50 fof(f1437,plain,(
% 0.10/0.50 op1(e10,e12)=e12|e11=e12|op1(e12,e12)=e12),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1444,f1179])).
% 0.10/0.50 fof(f1444,plain,(
% 0.10/0.50 op1(e11,e12)=e11),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1426,f212])).
% 0.10/0.50 fof(f1451,plain,(
% 0.10/0.50 op1(e11,e13)=e13),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1189,f1258])).
% 0.10/0.50 fof(f1454,plain,(
% 0.10/0.50 op1(e12,e10)=e10),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1331,f1260])).
% 0.10/0.50 fof(f1457,plain,(
% 0.10/0.50 op1(e10,e11)=e13|op1(e12,e11)=e13|op1(e13,e11)=e13),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1264,f214])).
% 0.10/0.50 fof(f1460,plain,(
% 0.10/0.50 e21=e20|op2(e20,e23)=e20),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1207,f1267])).
% 0.10/0.50 fof(f1469,plain,(
% 0.10/0.50 op2(e20,e23)=e20),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1460,f218])).
% 0.10/0.50 fof(f1470,plain,(
% 0.10/0.50 op2(e21,e20)=e20|op2(e22,e20)=e20),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1271,f218])).
% 0.10/0.50 fof(f1477,plain,(
% 0.10/0.50 op2(e23,e20)=e23),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1213,f1281])).
% 0.10/0.50 fof(f1478,plain,(
% 0.10/0.50 op2(e23,e21)=e21|e22=e21),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1070,f1281])).
% 0.10/0.50 fof(f1492,plain,(
% 0.10/0.50 h1(e11)=e20|op2(e22,e20)=e20),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1286,f1470])).
% 0.10/0.50 fof(f1496,plain,(
% 0.10/0.50 ~h1(e11)=op2(e23,e20)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1286,f168])).
% 0.10/0.50 fof(f1498,plain,(
% 0.10/0.50 ~sP27_prd|e21=e23|e20=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1210,f1288])).
% 0.10/0.50 fof(f1499,plain,(
% 0.10/0.50 ~sP27_prd|e20=e23),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1498,f222])).
% 0.10/0.50 fof(f1505,plain,(
% 0.10/0.50 e20=e21|op2(e21,e22)=e21),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1210,f1296])).
% 0.10/0.50 fof(f1509,plain,(
% 0.10/0.50 op2(e20,e22)=e22|e21=e22|h3(e12)=e22),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1514,f1094])).
% 0.10/0.50 fof(f1514,plain,(
% 0.10/0.50 op2(e21,e22)=e21),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1505,f218])).
% 0.10/0.50 fof(f1515,plain,(
% 0.10/0.50 h1(e11)=e20|op2(e21,e20)=e22|op2(e21,e20)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1286,f1297])).
% 0.10/0.50 fof(f1516,plain,(
% 0.10/0.50 h1(e11)=e20|h1(e11)=e22|op2(e21,e20)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1286,f1515])).
% 0.10/0.50 fof(f1517,plain,(
% 0.10/0.50 h1(e11)=e20|h1(e11)=e22|h1(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1286,f1516])).
% 0.10/0.50 fof(f1528,plain,(
% 0.10/0.50 h1(e10)=e23|e20=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1285,f1305])).
% 0.10/0.50 fof(f1529,plain,(
% 0.10/0.50 h1(e10)=e23|op2(e22,e21)=e23|op2(e23,e21)=e23),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1528,f220])).
% 0.10/0.50 fof(f1533,plain,(
% 0.10/0.50 h1(e11)=e22|h1(e11)=e23),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1517,f1534])).
% 0.10/0.50 fof(f1534,plain,(
% 0.10/0.50 ~h1(e11)=e20),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1286,f1309])).
% 0.10/0.50 fof(f1536,plain,(
% 0.10/0.50 op2(e21,e23)=e23),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f1214,f1311])).
% 0.10/0.50 fof(f1537,plain,(
% 0.10/0.50 ~sP13_prd|~h1(e11)=e22),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1539,f405])).
% 0.10/0.50 fof(f1539,plain,(
% 0.10/0.50 h2(e10)=h1(e11)),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1286,f1312])).
% 0.10/0.50 fof(f1542,plain,(
% 0.10/0.50 h2(e11)=h1(e10)),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1285,f1313])).
% 0.10/0.50 fof(f1548,plain,(
% 0.10/0.50 ~sP11_prd),
% 0.10/0.50 inference(trivial_equality_resolution,[status(thm)],[f1319])).
% 0.10/0.50 fof(f1558,plain,(
% 0.10/0.50 op1(e10,e11)=e13|op1(e12,e11)=e13|e11=e13),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1565,f1457])).
% 0.10/0.50 fof(f1565,plain,(
% 0.10/0.50 op1(e13,e11)=e11),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1421,f215])).
% 0.10/0.50 fof(f1576,plain,(
% 0.10/0.50 ~h1(e10)=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1430])).
% 0.10/0.50 fof(f1577,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1576])).
% 0.10/0.50 fof(f1578,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1577])).
% 0.10/0.50 fof(f1579,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1578])).
% 0.10/0.50 fof(f1580,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h2(e10),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1579])).
% 0.10/0.50 fof(f1581,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h2(e10)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1580])).
% 0.10/0.50 fof(f1582,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h2(e10),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1581])).
% 0.10/0.50 fof(f1583,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1582])).
% 0.10/0.50 fof(f1584,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h2(e10))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1583])).
% 0.10/0.50 fof(f1585,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h2(e10)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1584])).
% 0.10/0.50 fof(f1586,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h2(e11),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1585])).
% 0.10/0.50 fof(f1587,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h2(e11))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1586])).
% 0.10/0.50 fof(f1588,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h2(e11)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1587])).
% 0.10/0.50 fof(f1589,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h2(e11),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1588])).
% 0.10/0.50 fof(f1590,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h2(e11),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1589])).
% 0.10/0.50 fof(f1591,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h2(e10))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1590])).
% 0.10/0.50 fof(f1592,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h2(e11))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1591])).
% 0.10/0.50 fof(f1593,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h2(op1(e13,e10))=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1592])).
% 0.10/0.50 fof(f1594,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h2(e13)=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1420,f1593])).
% 0.10/0.50 fof(f1595,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h2(e10))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f276,f1594])).
% 0.10/0.50 fof(f1596,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h2(op1(e13,e11))=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1595])).
% 0.10/0.50 fof(f1597,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h2(e11)=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1565,f1596])).
% 0.10/0.50 fof(f1598,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h2(e11))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1597])).
% 0.10/0.50 fof(f1599,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP11_prd|sP13_prd|~h2(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1598])).
% 0.10/0.50 fof(f1600,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP11_prd|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1542,f1599])).
% 0.10/0.50 fof(f1601,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(op1(e11,e13))=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1600,f1548])).
% 0.10/0.50 fof(f1647,plain,(
% 0.10/0.50 op1(e10,e12)=e12|op1(e12,e12)=e12),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1437,f215])).
% 0.10/0.50 fof(f1654,plain,(
% 0.10/0.50 ~h1(e10)=op2(h1(e11),h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1451,f1601])).
% 0.10/0.50 fof(f1663,plain,(
% 0.10/0.50 op1(e11,e10)=e12|e10=e12),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1454,f1333])).
% 0.10/0.50 fof(f1665,plain,(
% 0.10/0.50 e10=e12|op1(e12,e11)=e12|op1(e12,e12)=e12),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1454,f1167])).
% 0.10/0.50 fof(f1679,plain,(
% 0.10/0.50 h1(e10)=e23|op2(e22,e21)=e23|e21=e23),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1685,f1529])).
% 0.10/0.50 fof(f1685,plain,(
% 0.10/0.50 op2(e23,e21)=e21),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1478,f221])).
% 0.10/0.50 fof(f1693,plain,(
% 0.10/0.50 e20=e22|op2(e22,e21)=e22|h3(e12)=e22),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f1697,f1096])).
% 0.10/0.50 fof(f1697,plain,(
% 0.10/0.50 op2(e22,e20)=e20),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1492,f1534])).
% 0.10/0.50 fof(f1700,plain,(
% 0.10/0.50 ~h1(e11)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1477,f1496])).
% 0.10/0.50 fof(f1704,plain,(
% 0.10/0.50 op2(e20,e22)=e22|h3(e12)=e22),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1509,f221])).
% 0.10/0.50 fof(f1716,plain,(
% 0.10/0.50 h1(e11)=e22),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1533,f1700])).
% 0.10/0.50 fof(f1721,plain,(
% 0.10/0.50 ~sP13_prd|~e22=e22),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1537])).
% 0.10/0.50 fof(f1722,plain,(
% 0.10/0.50 ~sP13_prd),
% 0.10/0.50 inference(trivial_equality_resolution,[status(thm)],[f1721])).
% 0.10/0.50 fof(f1727,plain,(
% 0.10/0.50 op1(e10,e11)=e13|op1(e12,e11)=e13),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1558,f216])).
% 0.10/0.50 fof(f1763,plain,(
% 0.10/0.50 ~h1(e10)=op2(e22,h1(e11))|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1654])).
% 0.10/0.50 fof(f1764,plain,(
% 0.10/0.50 ~h1(e10)=op2(e22,e22)|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1763])).
% 0.10/0.50 fof(f1765,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(h1(e11),h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f283,f1764])).
% 0.10/0.50 fof(f1766,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=op2(h1(e11),e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1765])).
% 0.10/0.50 fof(f1767,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=op2(e22,e20)|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1766])).
% 0.10/0.50 fof(f1768,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~h1(e11)=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1697,f1767])).
% 0.10/0.50 fof(f1769,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(h1(e11),e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1768])).
% 0.10/0.50 fof(f1770,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),h1(e11))|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1769])).
% 0.10/0.50 fof(f1771,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~h1(e11)=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1770])).
% 0.10/0.50 fof(f1772,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~h2(e13)=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1771])).
% 0.10/0.50 fof(f1773,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e10))=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f276,f1772])).
% 0.10/0.50 fof(f1774,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(e10)=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1454,f1773])).
% 0.10/0.50 fof(f1775,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h1(e11)=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1539,f1774])).
% 0.10/0.50 fof(f1776,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,h1(e11))|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1775])).
% 0.10/0.50 fof(f1777,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,h1(e11))|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1776])).
% 0.10/0.50 fof(f1778,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=op2(e21,e22)|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.50 inference(forward_demodulation,[status(thm)],[f1716,f1777])).
% 0.10/0.50 fof(f1779,plain,(
% 0.10/0.50 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~e21=e21|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1514,f1778])).
% 0.10/0.51 fof(f1780,plain,(
% 0.10/0.51 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))|sP13_prd|~h1(e10)=e23),
% 0.10/0.51 inference(trivial_equality_resolution,[status(thm)],[f1779])).
% 0.10/0.51 fof(f1781,plain,(
% 0.10/0.51 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(op1(e11,e10))=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))|~h1(e10)=e23),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1780,f1722])).
% 0.10/0.51 fof(f1818,plain,(
% 0.10/0.51 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~h2(e12)=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))|~h1(e10)=e23),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f1827,f1781])).
% 0.10/0.51 fof(f1827,plain,(
% 0.10/0.51 op1(e11,e10)=e12),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1663,f213])).
% 0.10/0.51 fof(f1828,plain,(
% 0.10/0.51 op1(e12,e11)=e12|op1(e12,e12)=e12),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1665,f213])).
% 0.10/0.51 fof(f1833,plain,(
% 0.10/0.51 h1(e10)=e23|op2(e22,e21)=e23),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1679,f222])).
% 0.10/0.51 fof(f1834,plain,(
% 0.10/0.51 op2(e22,e21)=e22|h3(e12)=e22),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1693,f219])).
% 0.10/0.51 fof(f1840,plain,(
% 0.10/0.51 ~h1(e10)=h3(e12)|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))|~h1(e10)=e23),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1210,f1818])).
% 0.10/0.51 fof(f1847,plain,(
% 0.10/0.51 e20=e23|h3(e12)=e23),
% 0.10/0.51 inference(resolution,[status(thm)],[f1499,f904])).
% 0.10/0.51 fof(f1853,plain,(
% 0.10/0.51 ~h1(e10)=e23|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))|~h1(e10)=e23),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f1867,f1840])).
% 0.10/0.51 fof(f1859,plain,(
% 0.10/0.51 op2(e22,e21)=e22|e23=e22),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f1867,f1834])).
% 0.10/0.51 fof(f1861,plain,(
% 0.10/0.51 op2(e20,e22)=e22|e23=e22),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f1867,f1704])).
% 0.10/0.51 fof(f1867,plain,(
% 0.10/0.51 h3(e12)=e23),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1847,f220])).
% 0.10/0.51 fof(f1884,plain,(
% 0.10/0.51 ~h1(e10)=e23|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=op2(e22,e21)|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))),
% 0.10/0.51 inference(duplicate_literals_removal,[status(thm)],[f1853])).
% 0.10/0.51 fof(f1895,plain,(
% 0.10/0.51 ~h1(e10)=e23|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=e22|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=op2(e20,e22)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f1902,f1884])).
% 0.10/0.51 fof(f1896,plain,(
% 0.10/0.51 h1(e10)=e23|e22=e23),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f1902,f1833])).
% 0.10/0.51 fof(f1902,plain,(
% 0.10/0.51 op2(e22,e21)=e22),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1859,f223])).
% 0.10/0.51 fof(f1909,plain,(
% 0.10/0.51 op2(e20,e22)=e22),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1861,f223])).
% 0.10/0.51 fof(f1925,plain,(
% 0.10/0.51 ~h1(e10)=e23|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=e22|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~e22=e22|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1909,f1895])).
% 0.10/0.51 fof(f1926,plain,(
% 0.10/0.51 ~h1(e10)=e23|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e22=e22|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))),
% 0.10/0.51 inference(duplicate_literals_removal,[status(thm)],[f1925])).
% 0.10/0.51 fof(f1927,plain,(
% 0.10/0.51 ~h1(e10)=e23|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,h1(e10))),
% 0.10/0.51 inference(trivial_equality_resolution,[status(thm)],[f1926])).
% 0.10/0.51 fof(f1928,plain,(
% 0.10/0.51 ~h1(e10)=e23|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f1936,f1927])).
% 0.10/0.51 fof(f1936,plain,(
% 0.10/0.51 h1(e10)=e23),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1896,f223])).
% 0.10/0.51 fof(f1979,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=op2(e22,h1(e10))|~h2(op1(e10,e12))=e20|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1928])).
% 0.10/0.51 fof(f1980,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=op2(e22,e23)|~h2(op1(e10,e12))=e20|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1979])).
% 0.10/0.51 fof(f1981,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=op2(h1(e10),e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f524,f1980])).
% 0.10/0.51 fof(f1982,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=op2(e23,e22)|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1981])).
% 0.10/0.51 fof(f1983,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=op2(h1(e10),h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f525,f1982])).
% 0.10/0.51 fof(f1984,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=op2(e23,h1(e10))|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1983])).
% 0.10/0.51 fof(f1985,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=op2(e23,e23)|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1984])).
% 0.10/0.51 fof(f1986,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~h1(e10)=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f271,f1985])).
% 0.10/0.51 fof(f1987,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=op2(h1(e10),e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1986])).
% 0.10/0.51 fof(f1988,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=op2(e23,e20)|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1987])).
% 0.10/0.51 fof(f1989,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=e23|~e21=op2(h1(e10),e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1477,f1988])).
% 0.10/0.51 fof(f1990,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=e23|~e21=op2(e23,e21)|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1989])).
% 0.10/0.51 fof(f1991,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=e23|~e21=e21|~h2(op1(e12,e11))=op2(e20,h1(e10))|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1685,f1990])).
% 0.10/0.51 fof(f1992,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=e23|~e21=e21|~h2(op1(e12,e11))=op2(e20,e23)|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1991])).
% 0.10/0.51 fof(f1993,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=e23|~e21=e21|~h2(op1(e12,e11))=e20|~h2(op1(e12,e12))=e21|~h1(e10)=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1469,f1992])).
% 0.10/0.51 fof(f1994,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=e23|~e21=e21|~h2(op1(e12,e11))=e20|~h2(op1(e12,e12))=e21|~e23=op2(e21,e23)),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1936,f1993])).
% 0.10/0.51 fof(f1995,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e23=e23|~e21=e21|~h2(op1(e12,e11))=e20|~h2(op1(e12,e12))=e21|~e23=e23),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1536,f1994])).
% 0.10/0.51 fof(f1996,plain,(
% 0.10/0.51 ~e23=e23|~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~e20=e20|~e22=e22|~e21=e21|~h2(op1(e12,e11))=e20|~h2(op1(e12,e12))=e21),
% 0.10/0.51 inference(duplicate_literals_removal,[status(thm)],[f1995])).
% 0.10/0.51 fof(f1997,plain,(
% 0.10/0.51 ~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~h2(op1(e12,e11))=e20|~h2(op1(e12,e12))=e21),
% 0.10/0.51 inference(trivial_equality_resolution,[status(thm)],[f1996])).
% 0.10/0.51 fof(f2017,plain,(
% 0.10/0.51 op1(e12,e12)=e13|e10=e13),
% 0.10/0.51 inference(resolution,[status(thm)],[f894,f1412])).
% 0.10/0.51 fof(f2019,plain,(
% 0.10/0.51 ~op1(e12,e11)=e13),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f2032,f155])).
% 0.10/0.51 fof(f2024,plain,(
% 0.10/0.51 ~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~h2(op1(e12,e11))=e20|~h2(e13)=e21),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f2032,f1997])).
% 0.10/0.51 fof(f2026,plain,(
% 0.10/0.51 op1(e12,e11)=e12|e13=e12),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f2032,f1828])).
% 0.10/0.51 fof(f2028,plain,(
% 0.10/0.51 op1(e10,e12)=e12|e13=e12),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f2032,f1647])).
% 0.10/0.51 fof(f2032,plain,(
% 0.10/0.51 op1(e12,e12)=e13),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2017,f214])).
% 0.10/0.51 fof(f2033,plain,(
% 0.10/0.51 op1(e10,e11)=e13),
% 0.10/0.51 inference(backward_subsumption_resolution,[status(thm)],[f1727,f2019])).
% 0.10/0.51 fof(f2043,plain,(
% 0.10/0.51 ~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~h2(op1(e12,e11))=e20|~e21=e21),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f276,f2024])).
% 0.10/0.51 fof(f2044,plain,(
% 0.10/0.51 ~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~h2(op1(e12,e11))=e20),
% 0.10/0.51 inference(trivial_equality_resolution,[status(thm)],[f2043])).
% 0.10/0.51 fof(f2046,plain,(
% 0.10/0.51 ~h2(op1(e10,e11))=e21|~h2(op1(e10,e12))=e20|~h2(e12)=e20),
% 0.10/0.51 inference(backward_demodulation,[status(thm)],[f2054,f2044])).
% 0.10/0.51 fof(f2054,plain,(
% 0.10/0.51 op1(e12,e11)=e12),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2026,f217])).
% 0.10/0.51 fof(f2060,plain,(
% 0.10/0.51 op1(e10,e12)=e12),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2028,f217])).
% 0.10/0.51 fof(f2065,plain,(
% 0.10/0.51 ~h2(e13)=e21|~h2(op1(e10,e12))=e20|~h2(e12)=e20),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f2033,f2046])).
% 0.10/0.51 fof(f2066,plain,(
% 0.10/0.51 ~e21=e21|~h2(op1(e10,e12))=e20|~h2(e12)=e20),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f276,f2065])).
% 0.10/0.51 fof(f2067,plain,(
% 0.10/0.51 ~e21=e21|~h2(e12)=e20|~h2(e12)=e20),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f2060,f2066])).
% 0.10/0.51 fof(f2068,plain,(
% 0.10/0.51 ~e21=e21|~e20=e20|~h2(e12)=e20),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1210,f2067])).
% 0.10/0.51 fof(f2069,plain,(
% 0.10/0.51 ~e21=e21|~e20=e20|~e20=e20),
% 0.10/0.51 inference(forward_demodulation,[status(thm)],[f1210,f2068])).
% 0.10/0.51 fof(f2070,plain,(
% 0.10/0.51 ~e21=e21|~e20=e20),
% 0.10/0.51 inference(duplicate_literals_removal,[status(thm)],[f2069])).
% 0.10/0.51 fof(f2071,plain,(
% 0.10/0.51 $false),
% 0.10/0.51 inference(trivial_equality_resolution,[status(thm)],[f2070])).
% 0.10/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.53 % Elapsed time: 0.149916 seconds
% 0.17/0.53 % CPU time: 0.764949 seconds
% 0.17/0.53 % Total memory used: 135.309 MB
% 0.17/0.53 % Net memory used: 134.142 MB
%------------------------------------------------------------------------------