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

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : ALG038+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 : n005.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:30 AM UTC 2026

% Result   : Theorem 0.26s 0.73s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04  % Problem  : ALG038+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42  % Computer : n005.cluster.edu
% 0.16/0.42  % Model    : x86_64 x86_64
% 0.16/0.42  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42  % Memory   : 8046.5625MB
% 0.16/0.42  % OS       : Linux 6.8.0-71-generic
% 0.16/0.42  % CPULimit : 300
% 0.16/0.42  % WCLimit  : 300
% 0.16/0.42  % DateTime : Mon Sep 21 12:54:03 UTC 2026
% 0.16/0.42  % CPUTime  : 
% 0.16/0.45  % Drodi V4.1.1
% 0.26/0.73  % Refutation found
% 0.26/0.73  % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.73  % SZS output start CNFRefutation for theBenchmark
% 0.26/0.73  fof(f1,axiom,(
% 0.26/0.73    ( ( 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.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f2,axiom,(
% 0.26/0.73    ( op1(unit1,e10) = e10& op1(e10,unit1) = e10& op1(unit1,e11) = e11& op1(e11,unit1) = e11& op1(unit1,e12) = e12& op1(e12,unit1) = e12& op1(unit1,e13) = e13& op1(e13,unit1) = e13& ( unit1 = e10| unit1 = e11| unit1 = e12| unit1 = e13 ) ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f3,axiom,(
% 0.26/0.73    ( ( 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.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f4,axiom,(
% 0.26/0.73    ( ( 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.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f5,axiom,(
% 0.26/0.73    ( op2(unit2,e20) = e20& op2(e20,unit2) = e20& op2(unit2,e21) = e21& op2(e21,unit2) = e21& op2(unit2,e22) = e22& op2(e22,unit2) = e22& op2(unit2,e23) = e23& op2(e23,unit2) = e23& ( unit2 = e20| unit2 = e21| unit2 = e22| unit2 = e23 ) ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f6,axiom,(
% 0.26/0.73    ( ( 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.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f7,axiom,(
% 0.26/0.73    ( 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.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f8,axiom,(
% 0.26/0.73    ( 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.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f9,axiom,(
% 0.26/0.73    ( e10 != e11& e10 != e12& e10 != e13& e11 != e12& e11 != e13& e12 != e13 ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f10,axiom,(
% 0.26/0.73    ( e20 != e21& e20 != e22& e20 != e23& e21 != e22& e21 != e23& e22 != e23 ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f14,axiom,(
% 0.26/0.73    ( e10 = op1(e11,op1(e11,op1(e11,e11)))& e12 = op1(e11,op1(e11,e11))& e13 = op1(e11,e11) ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f15,axiom,(
% 0.26/0.73    ( e20 = op2(e21,op2(e21,op2(e21,e21)))& e22 = op2(e21,op2(e21,e21))& e23 = op2(e21,e21) ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f16,axiom,(
% 0.26/0.73    ( h1(e11) = e20& h1(e10) = op2(e20,op2(e20,op2(e20,e20)))& h1(e12) = op2(e20,op2(e20,e20))& h1(e13) = op2(e20,e20) ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f17,axiom,(
% 0.26/0.73    ( h2(e11) = e21& h2(e10) = op2(e21,op2(e21,op2(e21,e21)))& h2(e12) = op2(e21,op2(e21,e21))& h2(e13) = op2(e21,e21) ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f18,axiom,(
% 0.26/0.73    ( h3(e11) = e22& h3(e10) = op2(e22,op2(e22,op2(e22,e22)))& h3(e12) = op2(e22,op2(e22,e22))& h3(e13) = op2(e22,e22) ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f19,axiom,(
% 0.26/0.73    ( h4(e11) = e23& h4(e10) = op2(e23,op2(e23,op2(e23,e23)))& h4(e12) = op2(e23,op2(e23,e23))& h4(e13) = op2(e23,e23) ) ),
% 0.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f20,conjecture,(
% 0.26/0.73    ( ( 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.26/0.73    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.26/0.73  fof(f21,negated_conjecture,(
% 0.26/0.73    ~(( ( 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.26/0.73    inference(negated_conjecture,[status(cth)],[f20])).
% 0.26/0.73  fof(f26,plain,(
% 0.26/0.73    op1(e11,e10)=e10|op1(e11,e10)=e11|op1(e11,e10)=e12|op1(e11,e10)=e13),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f1])).
% 0.26/0.73  fof(f39,plain,(
% 0.26/0.73    op1(e10,unit1)=e10),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f2])).
% 0.26/0.73  fof(f40,plain,(
% 0.26/0.73    op1(unit1,e11)=e11),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f2])).
% 0.26/0.73  fof(f41,plain,(
% 0.26/0.73    op1(e11,unit1)=e11),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f2])).
% 0.26/0.73  fof(f42,plain,(
% 0.26/0.73    op1(unit1,e12)=e12),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f2])).
% 0.26/0.73  fof(f43,plain,(
% 0.26/0.73    op1(e12,unit1)=e12),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f2])).
% 0.26/0.73  fof(f44,plain,(
% 0.26/0.73    op1(unit1,e13)=e13),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f2])).
% 0.26/0.73  fof(f45,plain,(
% 0.26/0.73    op1(e13,unit1)=e13),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f2])).
% 0.26/0.73  fof(f46,plain,(
% 0.26/0.73    unit1=e10|unit1=e11|unit1=e12|unit1=e13),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f2])).
% 0.26/0.73  fof(f56,plain,(
% 0.26/0.73    op1(e10,e11)=e10|op1(e11,e11)=e10|op1(e12,e11)=e10|op1(e13,e11)=e10),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f3])).
% 0.26/0.73  fof(f60,plain,(
% 0.26/0.73    op1(e10,e11)=e12|op1(e11,e11)=e12|op1(e12,e11)=e12|op1(e13,e11)=e12),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f3])).
% 0.26/0.73  fof(f65,plain,(
% 0.26/0.73    op1(e12,e10)=e11|op1(e12,e11)=e11|op1(e12,e12)=e11|op1(e12,e13)=e11),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f3])).
% 0.26/0.73  fof(f66,plain,(
% 0.26/0.73    op1(e10,e12)=e11|op1(e11,e12)=e11|op1(e12,e12)=e11|op1(e13,e12)=e11),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f3])).
% 0.26/0.73  fof(f69,plain,(
% 0.26/0.73    op1(e12,e10)=e13|op1(e12,e11)=e13|op1(e12,e12)=e13|op1(e12,e13)=e13),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f3])).
% 0.26/0.73  fof(f71,plain,(
% 0.26/0.73    op1(e13,e10)=e10|op1(e13,e11)=e10|op1(e13,e12)=e10|op1(e13,e13)=e10),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f3])).
% 0.26/0.73  fof(f94,plain,(
% 0.26/0.73    op2(e23,e23)=e20|op2(e23,e23)=e21|op2(e23,e23)=e22|op2(e23,e23)=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f4])).
% 0.26/0.73  fof(f97,plain,(
% 0.26/0.73    op2(unit2,e21)=e21),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f5])).
% 0.26/0.73  fof(f98,plain,(
% 0.26/0.73    op2(e21,unit2)=e21),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f5])).
% 0.26/0.73  fof(f99,plain,(
% 0.26/0.73    op2(unit2,e22)=e22),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f5])).
% 0.26/0.73  fof(f100,plain,(
% 0.26/0.73    op2(e22,unit2)=e22),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f5])).
% 0.26/0.73  fof(f101,plain,(
% 0.26/0.73    op2(unit2,e23)=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f5])).
% 0.26/0.73  fof(f102,plain,(
% 0.26/0.73    op2(e23,unit2)=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f5])).
% 0.26/0.73  fof(f103,plain,(
% 0.26/0.73    unit2=e20|unit2=e21|unit2=e22|unit2=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f5])).
% 0.26/0.73  fof(f105,plain,(
% 0.26/0.73    op2(e20,e20)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f6])).
% 0.26/0.73  fof(f113,plain,(
% 0.26/0.73    op2(e20,e21)=e20|op2(e21,e21)=e20|op2(e22,e21)=e20|op2(e23,e21)=e20),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f6])).
% 0.26/0.73  fof(f114,plain,(
% 0.26/0.73    op2(e21,e20)=e21|op2(e21,e21)=e21|op2(e21,e22)=e21|op2(e21,e23)=e21),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f6])).
% 0.26/0.73  fof(f117,plain,(
% 0.26/0.73    op2(e20,e21)=e22|op2(e21,e21)=e22|op2(e22,e21)=e22|op2(e23,e21)=e22),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f6])).
% 0.26/0.73  fof(f122,plain,(
% 0.26/0.73    op2(e22,e20)=e21|op2(e22,e21)=e21|op2(e22,e22)=e21|op2(e22,e23)=e21),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f6])).
% 0.26/0.73  fof(f123,plain,(
% 0.26/0.73    op2(e20,e22)=e21|op2(e21,e22)=e21|op2(e22,e22)=e21|op2(e23,e22)=e21),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f6])).
% 0.26/0.73  fof(f126,plain,(
% 0.26/0.73    op2(e22,e20)=e23|op2(e22,e21)=e23|op2(e22,e22)=e23|op2(e22,e23)=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f6])).
% 0.26/0.73  fof(f139,plain,(
% 0.26/0.73    ~op1(e11,e10)=op1(e12,e10)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f145,plain,(
% 0.26/0.73    ~op1(e11,e11)=op1(e12,e11)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f146,plain,(
% 0.26/0.73    ~op1(e11,e11)=op1(e13,e11)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f152,plain,(
% 0.26/0.73    ~op1(e11,e12)=op1(e13,e12)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f155,plain,(
% 0.26/0.73    ~op1(e10,e13)=op1(e12,e13)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f157,plain,(
% 0.26/0.73    ~op1(e11,e13)=op1(e12,e13)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f166,plain,(
% 0.26/0.73    ~op1(e11,e10)=op1(e11,e11)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f167,plain,(
% 0.26/0.73    ~op1(e11,e10)=op1(e11,e12)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f168,plain,(
% 0.26/0.73    ~op1(e11,e10)=op1(e11,e13)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f172,plain,(
% 0.26/0.73    ~op1(e12,e10)=op1(e12,e11)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f7])).
% 0.26/0.73  fof(f187,plain,(
% 0.26/0.73    ~op2(e21,e20)=op2(e22,e20)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f193,plain,(
% 0.26/0.73    ~op2(e21,e21)=op2(e22,e21)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f194,plain,(
% 0.26/0.73    ~op2(e21,e21)=op2(e23,e21)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f203,plain,(
% 0.26/0.73    ~op2(e20,e23)=op2(e22,e23)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f205,plain,(
% 0.26/0.73    ~op2(e21,e23)=op2(e22,e23)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f206,plain,(
% 0.26/0.73    ~op2(e21,e23)=op2(e23,e23)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f215,plain,(
% 0.26/0.73    ~op2(e21,e20)=op2(e21,e22)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f220,plain,(
% 0.26/0.73    ~op2(e22,e20)=op2(e22,e21)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f228,plain,(
% 0.26/0.73    ~op2(e23,e20)=op2(e23,e23)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f231,plain,(
% 0.26/0.73    ~op2(e23,e22)=op2(e23,e23)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f8])).
% 0.26/0.73  fof(f232,plain,(
% 0.26/0.73    ~e10=e11),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f9])).
% 0.26/0.73  fof(f233,plain,(
% 0.26/0.73    ~e10=e12),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f9])).
% 0.26/0.73  fof(f234,plain,(
% 0.26/0.73    ~e10=e13),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f9])).
% 0.26/0.73  fof(f235,plain,(
% 0.26/0.73    ~e11=e12),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f9])).
% 0.26/0.73  fof(f236,plain,(
% 0.26/0.73    ~e11=e13),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f9])).
% 0.26/0.73  fof(f237,plain,(
% 0.26/0.73    ~e12=e13),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f9])).
% 0.26/0.73  fof(f238,plain,(
% 0.26/0.73    ~e20=e21),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f10])).
% 0.26/0.73  fof(f239,plain,(
% 0.26/0.73    ~e20=e22),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f10])).
% 0.26/0.73  fof(f240,plain,(
% 0.26/0.73    ~e20=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f10])).
% 0.26/0.73  fof(f241,plain,(
% 0.26/0.73    ~e21=e22),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f10])).
% 0.26/0.73  fof(f242,plain,(
% 0.26/0.73    ~e21=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f10])).
% 0.26/0.73  fof(f243,plain,(
% 0.26/0.73    ~e22=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f10])).
% 0.26/0.73  fof(f270,plain,(
% 0.26/0.73    e10=op1(e11,op1(e11,op1(e11,e11)))),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f14])).
% 0.26/0.73  fof(f271,plain,(
% 0.26/0.73    e12=op1(e11,op1(e11,e11))),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f14])).
% 0.26/0.73  fof(f272,plain,(
% 0.26/0.73    e13=op1(e11,e11)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f14])).
% 0.26/0.73  fof(f273,plain,(
% 0.26/0.73    e20=op2(e21,op2(e21,op2(e21,e21)))),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f15])).
% 0.26/0.73  fof(f274,plain,(
% 0.26/0.73    e22=op2(e21,op2(e21,e21))),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f15])).
% 0.26/0.73  fof(f275,plain,(
% 0.26/0.73    e23=op2(e21,e21)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f15])).
% 0.26/0.73  fof(f279,plain,(
% 0.26/0.73    h1(e13)=op2(e20,e20)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f16])).
% 0.26/0.73  fof(f280,plain,(
% 0.26/0.73    h2(e11)=e21),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f17])).
% 0.26/0.73  fof(f281,plain,(
% 0.26/0.73    h2(e10)=op2(e21,op2(e21,op2(e21,e21)))),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f17])).
% 0.26/0.73  fof(f282,plain,(
% 0.26/0.73    h2(e12)=op2(e21,op2(e21,e21))),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f17])).
% 0.26/0.73  fof(f283,plain,(
% 0.26/0.73    h2(e13)=op2(e21,e21)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f17])).
% 0.26/0.73  fof(f287,plain,(
% 0.26/0.73    h3(e13)=op2(e22,e22)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f18])).
% 0.26/0.73  fof(f291,plain,(
% 0.26/0.73    h4(e13)=op2(e23,e23)),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f19])).
% 0.26/0.73  fof(f292,plain,(
% 0.26/0.73    ((((((((((((((((((((((~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.26/0.73    inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.26/0.73  fof(f293,definition,(
% 0.26/0.73    sP0_prd<=>(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.26/0.73  fof(f294,definition,(
% 0.26/0.73    sP1_prd<=>(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.26/0.73  fof(f295,definition,(
% 0.26/0.73    sP2_prd<=>(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.26/0.73  fof(f296,definition,(
% 0.26/0.73    sP3_prd<=>(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.26/0.73  fof(f297,definition,(
% 0.26/0.73    sP4_prd<=>(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.26/0.73  fof(f298,definition,(
% 0.26/0.73    sP5_prd<=>(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.26/0.73  fof(f299,definition,(
% 0.26/0.73    sP6_prd<=>(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.26/0.73  fof(f300,definition,(
% 0.26/0.73    sP7_prd<=>(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.26/0.73  fof(f301,definition,(
% 0.26/0.73    sP8_prd<=>(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.26/0.73  fof(f302,definition,(
% 0.26/0.73    sP9_prd<=>(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.26/0.73  fof(f303,definition,(
% 0.26/0.73    sP10_prd<=>(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.26/0.73  fof(f304,definition,(
% 0.26/0.73    sP11_prd<=>(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22)),
% 0.26/0.73    introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.26/0.73  fof(f305,plain,(
% 0.26/0.73    (((((((((((((((((((((~h1(op1(e10,e10))=op2(h1(e10),h1(e10))|~h1(op1(e10,e11))=op2(h1(e10),h1(e11)))|~h1(op1(e10,e12))=op2(h1(e10),h1(e12)))|~h1(op1(e10,e13))=op2(h1(e10),h1(e13)))|~h1(op1(e11,e10))=op2(h1(e11),h1(e10)))|~h1(op1(e11,e11))=op2(h1(e11),h1(e11)))|~h1(op1(e11,e12))=op2(h1(e11),h1(e12)))|~h1(op1(e11,e13))=op2(h1(e11),h1(e13)))|~h1(op1(e12,e10))=op2(h1(e12),h1(e10)))|~h1(op1(e12,e11))=op2(h1(e12),h1(e11)))|~h1(op1(e12,e12))=op2(h1(e12),h1(e12)))|~h1(op1(e12,e13))=op2(h1(e12),h1(e13)))|~h1(op1(e13,e10))=op2(h1(e13),h1(e10)))|~h1(op1(e13,e11))=op2(h1(e13),h1(e11)))|~h1(op1(e13,e12))=op2(h1(e13),h1(e12)))|~h1(op1(e13,e13))=op2(h1(e13),h1(e13)))|sP0_prd)|sP1_prd)|sP2_prd)|(((~h1(e10)=e23&~h1(e11)=e23)&~h1(e12)=e23)&~h1(e13)=e23))&(((((((((((((((((((~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11)))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12)))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13)))|~h2(op1(e11,e10))=op2(h2(e11),h2(e10)))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11)))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12)))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13)))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10)))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11)))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12)))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13)))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10)))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11)))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12)))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13)))|sP3_prd)|sP4_prd)|sP5_prd)|(((~h2(e10)=e23&~h2(e11)=e23)&~h2(e12)=e23)&~h2(e13)=e23)))&(((((((((((((((((((~h3(op1(e10,e10))=op2(h3(e10),h3(e10))|~h3(op1(e10,e11))=op2(h3(e10),h3(e11)))|~h3(op1(e10,e12))=op2(h3(e10),h3(e12)))|~h3(op1(e10,e13))=op2(h3(e10),h3(e13)))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10)))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11)))|~h3(op1(e11,e12))=op2(h3(e11),h3(e12)))|~h3(op1(e11,e13))=op2(h3(e11),h3(e13)))|~h3(op1(e12,e10))=op2(h3(e12),h3(e10)))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11)))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12)))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13)))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10)))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11)))|~h3(op1(e13,e12))=op2(h3(e13),h3(e12)))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13)))|sP6_prd)|sP7_prd)|sP8_prd)|(((~h3(e10)=e23&~h3(e11)=e23)&~h3(e12)=e23)&~h3(e13)=e23)))&(((((((((((((((((((~h4(op1(e10,e10))=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11)))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12)))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13)))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10)))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11)))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12)))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13)))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10)))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11)))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12)))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13)))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10)))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11)))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12)))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13)))|sP9_prd)|sP10_prd)|sP11_prd)|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23))),
% 0.26/0.73    inference(formula_renaming,[status(thm)],[f292,f304,f303,f302,f301,f300,f299,f298,f297,f296,f295,f294,f293])).
% 0.26/0.73  fof(f313,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13))|~h2(op1(e11,e10))=op2(h2(e11),h2(e10))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f305])).
% 0.26/0.73  fof(f340,plain,(
% 0.26/0.73    (~sP3_prd|(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20))&(sP3_prd|(((h2(e10)=e20|h2(e11)=e20)|h2(e12)=e20)|h2(e13)=e20))),
% 0.26/0.73    inference(NNF_transformation,[status(thm)],[f296])).
% 0.26/0.73  fof(f341,plain,(
% 0.26/0.73    ~sP3_prd|~h2(e10)=e20),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f340])).
% 0.26/0.73  fof(f346,plain,(
% 0.26/0.73    (~sP4_prd|(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21))&(sP4_prd|(((h2(e10)=e21|h2(e11)=e21)|h2(e12)=e21)|h2(e13)=e21))),
% 0.26/0.73    inference(NNF_transformation,[status(thm)],[f297])).
% 0.26/0.73  fof(f348,plain,(
% 0.26/0.73    ~sP4_prd|~h2(e11)=e21),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f346])).
% 0.26/0.73  fof(f352,plain,(
% 0.26/0.73    (~sP5_prd|(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22))&(sP5_prd|(((h2(e10)=e22|h2(e11)=e22)|h2(e12)=e22)|h2(e13)=e22))),
% 0.26/0.73    inference(NNF_transformation,[status(thm)],[f298])).
% 0.26/0.73  fof(f355,plain,(
% 0.26/0.73    ~sP5_prd|~h2(e12)=e22),
% 0.26/0.73    inference(cnf_transformation,[status(thm)],[f352])).
% 0.26/0.73  fof(f460,plain,(
% 0.26/0.73    op1(e12,e13)=e12|unit1=e10|unit1=e11|unit1=e12),
% 0.26/0.73    inference(paramodulation,[status(thm)],[f46,f43])).
% 0.26/0.73  fof(f810,plain,(
% 0.26/0.73    ~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f280,f313])).
% 0.26/0.73  fof(f814,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f280,f810])).
% 0.26/0.73  fof(f815,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13))|~h2(op1(e11,e10))=op2(e21,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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f280,f814])).
% 0.26/0.73  fof(f816,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13))|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e11))=op2(e21,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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f280,f815])).
% 0.26/0.73  fof(f817,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13))|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e11))=op2(e21,e21)|~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f280,f816])).
% 0.26/0.73  fof(f818,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13))|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e11))=op2(e21,e21)|~h2(op1(e11,e12))=op2(e21,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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f280,f817])).
% 0.26/0.73  fof(f819,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13))|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e11))=op2(e21,e21)|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f280,f818])).
% 0.26/0.73  fof(f820,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13))|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e11))=op2(e21,e21)|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,h2(e13))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f280,f819])).
% 0.26/0.73  fof(f944,plain,(
% 0.26/0.73    op1(e10,e11)=e12|e13=e12|op1(e12,e11)=e12|op1(e13,e11)=e12),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f272,f60])).
% 0.26/0.73  fof(f948,plain,(
% 0.26/0.73    op1(e10,e11)=e10|e13=e10|op1(e12,e11)=e10|op1(e13,e11)=e10),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f272,f56])).
% 0.26/0.73  fof(f951,plain,(
% 0.26/0.73    op1(e10,e11)=e12|op1(e12,e11)=e12|op1(e13,e11)=e12),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f944,f237])).
% 0.26/0.73  fof(f955,plain,(
% 0.26/0.73    op1(e10,e11)=e10|op1(e12,e11)=e10|op1(e13,e11)=e10),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f948,f234])).
% 0.26/0.73  fof(f971,plain,(
% 0.26/0.73    op2(e22,e23)=e22|unit2=e20|unit2=e21|unit2=e22),
% 0.26/0.73    inference(paramodulation,[status(thm)],[f103,f100])).
% 0.26/0.73  fof(f1053,plain,(
% 0.26/0.73    op2(e20,e21)=e20|e23=e20|op2(e22,e21)=e20|op2(e23,e21)=e20),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f113])).
% 0.26/0.73  fof(f1054,plain,(
% 0.26/0.73    op2(e20,e21)=e20|op2(e22,e21)=e20|op2(e23,e21)=e20),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f1053,f240])).
% 0.26/0.73  fof(f1057,plain,(
% 0.26/0.73    op2(e21,e20)=e21|e23=e21|op2(e21,e22)=e21|op2(e21,e23)=e21),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f114])).
% 0.26/0.73  fof(f1058,plain,(
% 0.26/0.73    op2(e21,e20)=e21|op2(e21,e22)=e21|op2(e21,e23)=e21),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f1057,f242])).
% 0.26/0.73  fof(f1090,plain,(
% 0.26/0.73    ~sP4_prd|~e21=e21),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f280,f348])).
% 0.26/0.73  fof(f1091,plain,(
% 0.26/0.73    ~sP4_prd),
% 0.26/0.73    inference(trivial_equality_resolution,[status(thm)],[f1090])).
% 0.26/0.73  fof(f1092,plain,(
% 0.26/0.73    op2(e20,e21)=e22|e23=e22|op2(e22,e21)=e22|op2(e23,e21)=e22),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f117])).
% 0.26/0.73  fof(f1093,plain,(
% 0.26/0.73    op2(e20,e21)=e22|op2(e22,e21)=e22|op2(e23,e21)=e22),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f1092,f243])).
% 0.26/0.73  fof(f1329,plain,(
% 0.26/0.73    op1(e12,e10)=e13|op1(e12,e12)=e13|op1(e12,e13)=e13),
% 0.26/0.73    inference(backward_subsumption_resolution,[status(thm)],[f69,f1331])).
% 0.26/0.73  fof(f1331,plain,(
% 0.26/0.73    ~e13=op1(e12,e11)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f272,f145])).
% 0.26/0.73  fof(f1334,plain,(
% 0.26/0.73    ~e13=op1(e13,e11)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f272,f146])).
% 0.26/0.73  fof(f1416,plain,(
% 0.26/0.73    op1(e11,e10)=e10|op1(e11,e10)=e11|op1(e11,e10)=e12),
% 0.26/0.73    inference(backward_subsumption_resolution,[status(thm)],[f26,f1417])).
% 0.26/0.73  fof(f1417,plain,(
% 0.26/0.73    ~op1(e11,e10)=e13),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f272,f166])).
% 0.26/0.73  fof(f1429,plain,(
% 0.26/0.73    h1(e13)=e20|op2(e21,e20)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f279,f105])).
% 0.26/0.73  fof(f1439,plain,(
% 0.26/0.73    h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f283])).
% 0.26/0.73  fof(f1451,plain,(
% 0.26/0.73    op2(e22,e20)=e23|op2(e22,e21)=e23|h3(e13)=e23|op2(e22,e23)=e23),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f287,f126])).
% 0.26/0.73  fof(f1454,plain,(
% 0.26/0.73    op2(e20,e22)=e21|op2(e21,e22)=e21|h3(e13)=e21|op2(e23,e22)=e21),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f287,f123])).
% 0.26/0.73  fof(f1455,plain,(
% 0.26/0.73    op2(e22,e20)=e21|op2(e22,e21)=e21|h3(e13)=e21|op2(e22,e23)=e21),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f287,f122])).
% 0.26/0.73  fof(f1470,plain,(
% 0.26/0.73    op2(e23,e23)=e20|op2(e23,e23)=e21|op2(e23,e23)=e22|h4(e13)=e23),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f291,f94])).
% 0.26/0.73  fof(f1471,plain,(
% 0.26/0.73    h4(e13)=e20|op2(e23,e23)=e21|op2(e23,e23)=e22|h4(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f291,f1470])).
% 0.26/0.73  fof(f1472,plain,(
% 0.26/0.73    h4(e13)=e20|h4(e13)=e21|op2(e23,e23)=e22|h4(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f291,f1471])).
% 0.26/0.73  fof(f1473,plain,(
% 0.26/0.73    h4(e13)=e20|h4(e13)=e21|h4(e13)=e22|h4(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f291,f1472])).
% 0.26/0.73  fof(f1555,plain,(
% 0.26/0.73    ~e23=op2(e22,e21)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f193])).
% 0.26/0.73  fof(f1557,plain,(
% 0.26/0.73    ~e23=op2(e23,e21)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f194])).
% 0.26/0.73  fof(f1581,plain,(
% 0.26/0.73    ~op2(e21,e23)=h4(e13)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f291,f206])).
% 0.26/0.73  fof(f1591,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e11))=op2(e21,e21)|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,h2(e13))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f820])).
% 0.26/0.73  fof(f1592,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(e13)=op2(e21,e21)|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,h2(e13))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f272,f1591])).
% 0.26/0.73  fof(f1593,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=op2(e21,e21)|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,h2(e13))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1592])).
% 0.26/0.73  fof(f1594,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,h2(e13))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f1593])).
% 0.26/0.73  fof(f1595,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~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),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1594])).
% 0.26/0.73  fof(f1596,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(h2(e13),h2(e10))|~h2(op1(e13,e11))=op2(h2(e13),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1595])).
% 0.26/0.73  fof(f1597,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(h2(e13),e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1596])).
% 0.26/0.73  fof(f1598,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(h2(e13),h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1597])).
% 0.26/0.73  fof(f1599,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1598])).
% 0.26/0.73  fof(f1600,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=op2(e23,h2(e13))|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1599])).
% 0.26/0.73  fof(f1601,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=op2(e23,e23)|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1600])).
% 0.26/0.73  fof(f1602,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP4_prd|sP5_prd|~h2(e13)=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f291,f1601])).
% 0.26/0.73  fof(f1603,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP4_prd|sP5_prd|~e23=e23),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1439,f1602])).
% 0.26/0.73  fof(f1604,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~e23=e23|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP4_prd|sP5_prd),
% 0.26/0.73    inference(duplicate_literals_removal,[status(thm)],[f1603])).
% 0.26/0.73  fof(f1605,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP4_prd|sP5_prd),
% 0.26/0.73    inference(trivial_equality_resolution,[status(thm)],[f1604])).
% 0.26/0.73  fof(f1606,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(op1(e11,e13))=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f1605,f1091])).
% 0.26/0.73  fof(f1675,plain,(
% 0.26/0.73    ~op2(e23,e20)=h4(e13)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f291,f228])).
% 0.26/0.73  fof(f1682,plain,(
% 0.26/0.73    ~op2(e23,e22)=h4(e13)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f291,f231])).
% 0.26/0.73  fof(f1713,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1727,f1606])).
% 0.26/0.73  fof(f1720,plain,(
% 0.26/0.73    ~op1(e11,e10)=e12),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1727,f168])).
% 0.26/0.73  fof(f1722,plain,(
% 0.26/0.73    ~e12=op1(e12,e13)),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1727,f157])).
% 0.26/0.73  fof(f1727,plain,(
% 0.26/0.73    e12=op1(e11,e13)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f272,f271])).
% 0.26/0.73  fof(f1740,plain,(
% 0.26/0.73    e10=op1(e11,op1(e11,e13))),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f272,f270])).
% 0.26/0.73  fof(f1743,plain,(
% 0.26/0.73    ~op1(e11,e10)=e10),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1749,f167])).
% 0.26/0.73  fof(f1744,plain,(
% 0.26/0.73    ~e10=op1(e13,e12)),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1749,f152])).
% 0.26/0.73  fof(f1747,plain,(
% 0.26/0.73    op1(e10,e12)=e11|e10=e11|op1(e12,e12)=e11|op1(e13,e12)=e11),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1749,f66])).
% 0.26/0.73  fof(f1749,plain,(
% 0.26/0.73    e10=op1(e11,e12)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1727,f1740])).
% 0.26/0.73  fof(f1750,plain,(
% 0.26/0.73    op1(e10,e12)=e11|op1(e12,e12)=e11|op1(e13,e12)=e11),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f1747,f232])).
% 0.26/0.73  fof(f1751,plain,(
% 0.26/0.73    e20=op2(e21,op2(e21,e23))),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f273])).
% 0.26/0.73  fof(f1753,plain,(
% 0.26/0.73    e20=op2(e21,e21)|op2(e21,e20)=e21|op2(e21,e22)=e21),
% 0.26/0.73    inference(paramodulation,[status(thm)],[f1058,f1751])).
% 0.26/0.73  fof(f1755,plain,(
% 0.26/0.73    e20=e23|op2(e21,e20)=e21|op2(e21,e22)=e21),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f1753])).
% 0.26/0.73  fof(f1756,plain,(
% 0.26/0.73    op2(e21,e20)=e21|op2(e21,e22)=e21),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f1755,f240])).
% 0.26/0.73  fof(f1767,plain,(
% 0.26/0.73    e20=op2(e21,e22)),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1777,f1751])).
% 0.26/0.73  fof(f1771,plain,(
% 0.26/0.73    ~e22=h4(e13)),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1777,f1581])).
% 0.26/0.73  fof(f1772,plain,(
% 0.26/0.73    ~e22=op2(e22,e23)),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1777,f205])).
% 0.26/0.73  fof(f1777,plain,(
% 0.26/0.73    e22=op2(e21,e23)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f274])).
% 0.26/0.73  fof(f1783,plain,(
% 0.26/0.73    h2(e10)=op2(e21,op2(e21,e23))),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f281])).
% 0.26/0.73  fof(f1785,plain,(
% 0.26/0.73    ~op2(e21,e20)=h2(e10)),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1789,f215])).
% 0.26/0.73  fof(f1789,plain,(
% 0.26/0.73    h2(e10)=op2(e21,e22)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1777,f1783])).
% 0.26/0.73  fof(f1790,plain,(
% 0.26/0.73    h2(e12)=op2(e21,e23)),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f275,f282])).
% 0.26/0.73  fof(f1793,plain,(
% 0.26/0.73    ~sP5_prd|~e22=e22),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1795,f355])).
% 0.26/0.73  fof(f1795,plain,(
% 0.26/0.73    h2(e12)=e22),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1777,f1790])).
% 0.26/0.73  fof(f1797,plain,(
% 0.26/0.73    ~sP5_prd),
% 0.26/0.73    inference(trivial_equality_resolution,[status(thm)],[f1793])).
% 0.26/0.73  fof(f1824,plain,(
% 0.26/0.73    op1(e13,e10)=e10|op1(e13,e11)=e10|op1(e13,e13)=e10),
% 0.26/0.73    inference(backward_subsumption_resolution,[status(thm)],[f71,f1744])).
% 0.26/0.73  fof(f1907,plain,(
% 0.26/0.73    h2(e10)=e20),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1767,f1789])).
% 0.26/0.73  fof(f1910,plain,(
% 0.26/0.73    ~sP3_prd|~e20=e20),
% 0.26/0.73    inference(backward_demodulation,[status(thm)],[f1907,f341])).
% 0.26/0.73  fof(f1911,plain,(
% 0.26/0.73    ~sP3_prd),
% 0.26/0.73    inference(trivial_equality_resolution,[status(thm)],[f1910])).
% 0.26/0.73  fof(f1933,plain,(
% 0.26/0.73    op1(e11,e10)=e11|op1(e11,e10)=e12),
% 0.26/0.73    inference(forward_subsumption_resolution,[status(thm)],[f1416,f1743])).
% 0.26/0.73  fof(f1934,plain,(
% 0.26/0.73    op1(e11,e10)=e11),
% 0.26/0.73    inference(resolution,[status(thm)],[f1933,f1720])).
% 0.26/0.73  fof(f1971,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(e20,h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1907,f1713])).
% 0.26/0.73  fof(f1972,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=op2(e20,e20)|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.73    inference(forward_demodulation,[status(thm)],[f1907,f1971])).
% 0.26/0.73  fof(f1973,plain,(
% 0.26/0.73    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(h2(e10),e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f279,f1972])).
% 0.26/0.74  fof(f1974,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(h2(e10),h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f1973])).
% 0.26/0.74  fof(f1975,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,h2(e12))|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f1974])).
% 0.26/0.74  fof(f1976,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(h2(e10),e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1975])).
% 0.26/0.74  fof(f1977,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,h2(e10))|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f1976])).
% 0.26/0.74  fof(f1978,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~h2(op1(e11,e12))=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f1977])).
% 0.26/0.74  fof(f1979,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~h2(e10)=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1749,f1978])).
% 0.26/0.74  fof(f1980,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=op2(e21,h2(e12))|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f1979])).
% 0.26/0.74  fof(f1981,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=op2(e21,e22)|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1980])).
% 0.26/0.74  fof(f1982,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~h2(e12)=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1767,f1981])).
% 0.26/0.74  fof(f1983,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=op2(e21,e23)|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1982])).
% 0.26/0.74  fof(f1984,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(h2(e12),h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1777,f1983])).
% 0.26/0.74  fof(f1985,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,h2(e10))|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1984])).
% 0.26/0.74  fof(f1986,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(h2(e12),e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f1985])).
% 0.26/0.74  fof(f1987,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=op2(h2(e12),h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1986])).
% 0.26/0.74  fof(f1988,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=op2(e22,h2(e12))|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1987])).
% 0.26/0.74  fof(f1989,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=op2(e22,e22)|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1988])).
% 0.26/0.74  fof(f1990,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(h2(e12),e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f287,f1989])).
% 0.26/0.74  fof(f1991,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,h2(e10))|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1990])).
% 0.26/0.74  fof(f1992,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,h2(e12))|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f1991])).
% 0.26/0.74  fof(f1993,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~e20=e20|~e22=e22|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f1992])).
% 0.26/0.74  fof(f1994,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)|sP3_prd|sP5_prd),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f1993])).
% 0.26/0.74  fof(f1995,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e11,e10))=op2(e21,e20)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)|sP5_prd),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f1994,f1911])).
% 0.26/0.74  fof(f2107,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(e11)=op2(e21,e20)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)|sP5_prd),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f1934,f1995])).
% 0.26/0.74  fof(f2116,plain,(
% 0.26/0.74    ~e11=op1(e12,e10)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f1934,f139])).
% 0.26/0.74  fof(f2121,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~e21=op2(e21,e20)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)|sP5_prd),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f280,f2107])).
% 0.26/0.74  fof(f2122,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~e21=op2(e21,e20)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f2121,f1797])).
% 0.26/0.74  fof(f2134,plain,(
% 0.26/0.74    op2(e22,e20)=e23|h3(e13)=e23|op2(e22,e23)=e23),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f1451,f1555])).
% 0.26/0.74  fof(f2162,plain,(
% 0.26/0.74    op1(e12,e11)=e11|op1(e12,e12)=e11|op1(e12,e13)=e11),
% 0.26/0.74    inference(backward_subsumption_resolution,[status(thm)],[f65,f2116])).
% 0.26/0.74  fof(f2164,plain,(
% 0.26/0.74    op2(e20,e22)=e21|e20=e21|h3(e13)=e21|op2(e23,e22)=e21),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1767,f1454])).
% 0.26/0.74  fof(f2165,plain,(
% 0.26/0.74    op2(e20,e22)=e21|h3(e13)=e21|op2(e23,e22)=e21),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f2164,f238])).
% 0.26/0.74  fof(f2241,plain,(
% 0.26/0.74    h1(e13)=e20|op2(e22,e20)=e20|op2(e23,e20)=e20),
% 0.26/0.74    inference(backward_subsumption_resolution,[status(thm)],[f1429,f2242])).
% 0.26/0.74  fof(f2242,plain,(
% 0.26/0.74    ~op2(e21,e20)=e20),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f1785])).
% 0.26/0.74  fof(f2381,plain,(
% 0.26/0.74    h4(e13)=e20|h4(e13)=e21|h4(e13)=e23),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f1473,f1771])).
% 0.26/0.74  fof(f2408,plain,(
% 0.26/0.74    op2(e21,e20)=e21|e20=e21),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1767,f1756])).
% 0.26/0.74  fof(f2410,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~e21=e21|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2417,f2122])).
% 0.26/0.74  fof(f2415,plain,(
% 0.26/0.74    ~e21=op2(e22,e20)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2417,f187])).
% 0.26/0.74  fof(f2417,plain,(
% 0.26/0.74    op2(e21,e20)=e21),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f2408,f238])).
% 0.26/0.74  fof(f2418,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(op1(e13,e10))=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f2410])).
% 0.26/0.74  fof(f2443,plain,(
% 0.26/0.74    op2(e22,e21)=e21|h3(e13)=e21|op2(e22,e23)=e21),
% 0.26/0.74    inference(backward_subsumption_resolution,[status(thm)],[f1455,f2415])).
% 0.26/0.74  fof(f2693,plain,(
% 0.26/0.74    unit1=e10|unit1=e11|unit1=e12),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f460,f1722])).
% 0.26/0.74  fof(f2698,plain,(
% 0.26/0.74    op1(e11,e12)=e11|unit1=e10|unit1=e11),
% 0.26/0.74    inference(paramodulation,[status(thm)],[f2693,f41])).
% 0.26/0.74  fof(f2704,plain,(
% 0.26/0.74    e10=e11|unit1=e10|unit1=e11),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1749,f2698])).
% 0.26/0.74  fof(f2705,plain,(
% 0.26/0.74    unit1=e10|unit1=e11),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f2704,f232])).
% 0.26/0.74  fof(f2707,plain,(
% 0.26/0.74    op1(e13,e11)=e13|unit1=e10),
% 0.26/0.74    inference(paramodulation,[status(thm)],[f2705,f45])).
% 0.26/0.74  fof(f2716,plain,(
% 0.26/0.74    unit1=e10),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f2707,f1334])).
% 0.26/0.74  fof(f2786,plain,(
% 0.26/0.74    op1(e13,e10)=e13),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2716,f45])).
% 0.26/0.74  fof(f2787,plain,(
% 0.26/0.74    op1(e10,e13)=e13),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2716,f44])).
% 0.26/0.74  fof(f2788,plain,(
% 0.26/0.74    op1(e12,e10)=e12),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2716,f43])).
% 0.26/0.74  fof(f2789,plain,(
% 0.26/0.74    op1(e10,e12)=e12),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2716,f42])).
% 0.26/0.74  fof(f2791,plain,(
% 0.26/0.74    op1(e10,e11)=e11),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2716,f40])).
% 0.26/0.74  fof(f2792,plain,(
% 0.26/0.74    op1(e10,e10)=e10),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2716,f39])).
% 0.26/0.74  fof(f3004,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~h2(e13)=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2786,f2418])).
% 0.26/0.74  fof(f3005,plain,(
% 0.26/0.74    e13=e10|op1(e13,e11)=e10|op1(e13,e13)=e10),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2786,f1824])).
% 0.26/0.74  fof(f3022,plain,(
% 0.26/0.74    ~h2(op1(e10,e10))=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1439,f3004])).
% 0.26/0.74  fof(f3023,plain,(
% 0.26/0.74    op1(e13,e11)=e10|op1(e13,e13)=e10),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3005,f234])).
% 0.26/0.74  fof(f3039,plain,(
% 0.26/0.74    ~e13=op1(e12,e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2787,f155])).
% 0.26/0.74  fof(f3048,plain,(
% 0.26/0.74    e12=e13|op1(e12,e12)=e13|op1(e12,e13)=e13),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2788,f1329])).
% 0.26/0.74  fof(f3051,plain,(
% 0.26/0.74    ~e12=op1(e12,e11)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2788,f172])).
% 0.26/0.74  fof(f3055,plain,(
% 0.26/0.74    op1(e12,e12)=e13|op1(e12,e13)=e13),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3048,f237])).
% 0.26/0.74  fof(f3058,plain,(
% 0.26/0.74    e12=e11|op1(e12,e12)=e11|op1(e13,e12)=e11),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2789,f1750])).
% 0.26/0.74  fof(f3067,plain,(
% 0.26/0.74    op1(e12,e12)=e11|op1(e13,e12)=e11),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3058,f235])).
% 0.26/0.74  fof(f3070,plain,(
% 0.26/0.74    e11=e10|op1(e12,e11)=e10|op1(e13,e11)=e10),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2791,f955])).
% 0.26/0.74  fof(f3072,plain,(
% 0.26/0.74    e11=e12|op1(e12,e11)=e12|op1(e13,e11)=e12),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f2791,f951])).
% 0.26/0.74  fof(f3078,plain,(
% 0.26/0.74    op1(e12,e11)=e10|op1(e13,e11)=e10),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3070,f232])).
% 0.26/0.74  fof(f3079,plain,(
% 0.26/0.74    op1(e12,e11)=e12|op1(e13,e11)=e12),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3072,f235])).
% 0.26/0.74  fof(f3095,plain,(
% 0.26/0.74    ~h2(e10)=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f2792,f3022])).
% 0.26/0.74  fof(f3096,plain,(
% 0.26/0.74    ~e20=h1(e13)|~h2(op1(e10,e11))=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f3095])).
% 0.26/0.74  fof(f3097,plain,(
% 0.26/0.74    ~e20=h1(e13)|~h2(e11)=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f2791,f3096])).
% 0.26/0.74  fof(f3098,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~h2(op1(e10,e12))=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f280,f3097])).
% 0.26/0.74  fof(f3099,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~h2(e12)=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f2789,f3098])).
% 0.26/0.74  fof(f3100,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~h2(op1(e10,e13))=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f3099])).
% 0.26/0.74  fof(f3101,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~h2(e13)=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f2787,f3100])).
% 0.26/0.74  fof(f3102,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~h2(op1(e12,e10))=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1439,f3101])).
% 0.26/0.74  fof(f3103,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~h2(e12)=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f2788,f3102])).
% 0.26/0.74  fof(f3104,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(op1(e12,e12))=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f3103])).
% 0.26/0.74  fof(f3223,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~h2(e13)=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3232,f3104])).
% 0.26/0.74  fof(f3226,plain,(
% 0.26/0.74    op1(e12,e11)=e11|e13=e11|op1(e12,e13)=e11),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3232,f2162])).
% 0.26/0.74  fof(f3232,plain,(
% 0.26/0.74    op1(e12,e12)=e13),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3055,f3039])).
% 0.26/0.74  fof(f3234,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~e23=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(op1(e13,e12))=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1439,f3223])).
% 0.26/0.74  fof(f3235,plain,(
% 0.26/0.74    op1(e12,e11)=e11|op1(e12,e13)=e11),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3226,f236])).
% 0.26/0.74  fof(f3239,plain,(
% 0.26/0.74    e13=e11|op1(e13,e12)=e11),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3232,f3067])).
% 0.26/0.74  fof(f3246,plain,(
% 0.26/0.74    op1(e13,e12)=e11),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3239,f236])).
% 0.26/0.74  fof(f3252,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~e23=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~h2(e11)=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3246,f3234])).
% 0.26/0.74  fof(f3253,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~e23=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(op1(e13,e11))=op2(e23,e21)|~e21=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f280,f3252])).
% 0.26/0.74  fof(f3268,plain,(
% 0.26/0.74    op1(e12,e11)=e10|e12=e10),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3277,f3078])).
% 0.26/0.74  fof(f3272,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~e23=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~h2(e12)=op2(e23,e21)|~e21=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3277,f3253])).
% 0.26/0.74  fof(f3273,plain,(
% 0.26/0.74    e12=e10|op1(e13,e13)=e10),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3277,f3023])).
% 0.26/0.74  fof(f3277,plain,(
% 0.26/0.74    op1(e13,e11)=e12),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3079,f3051])).
% 0.26/0.74  fof(f3278,plain,(
% 0.26/0.74    op1(e12,e11)=e10),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3268,f233])).
% 0.26/0.74  fof(f3279,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~h2(op1(e12,e11))=op2(e22,e21)|~e23=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1795,f3272])).
% 0.26/0.74  fof(f3280,plain,(
% 0.26/0.74    op1(e13,e13)=e10),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3273,f233])).
% 0.26/0.74  fof(f3318,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~h2(e10)=op2(e22,e21)|~e23=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3278,f3279])).
% 0.26/0.74  fof(f3329,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~h2(op1(e12,e13))=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f3318])).
% 0.26/0.74  fof(f3335,plain,(
% 0.26/0.74    e10=e11|op1(e12,e13)=e11),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3278,f3235])).
% 0.26/0.74  fof(f3339,plain,(
% 0.26/0.74    op1(e12,e13)=e11),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3335,f232])).
% 0.26/0.74  fof(f3349,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~h2(e11)=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3339,f3329])).
% 0.26/0.74  fof(f3350,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~h2(op1(e13,e13))=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f280,f3349])).
% 0.26/0.74  fof(f3351,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~h2(e10)=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3280,f3350])).
% 0.26/0.74  fof(f3352,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e23=op2(e23,e20)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1907,f3351])).
% 0.26/0.74  fof(f3613,plain,(
% 0.26/0.74    unit2=e20|unit2=e21|unit2=e22),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f971,f1772])).
% 0.26/0.74  fof(f3618,plain,(
% 0.26/0.74    op2(e21,e22)=e21|unit2=e20|unit2=e21),
% 0.26/0.74    inference(paramodulation,[status(thm)],[f3613,f98])).
% 0.26/0.74  fof(f3626,plain,(
% 0.26/0.74    e20=e21|unit2=e20|unit2=e21),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f1767,f3618])).
% 0.26/0.74  fof(f3627,plain,(
% 0.26/0.74    unit2=e20|unit2=e21),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3626,f238])).
% 0.26/0.74  fof(f3629,plain,(
% 0.26/0.74    op2(e23,e21)=e23|unit2=e20),
% 0.26/0.74    inference(paramodulation,[status(thm)],[f3627,f102])).
% 0.26/0.74  fof(f3638,plain,(
% 0.26/0.74    unit2=e20),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3629,f1557])).
% 0.26/0.74  fof(f3650,plain,(
% 0.26/0.74    op2(e23,e20)=e23),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3638,f102])).
% 0.26/0.74  fof(f3651,plain,(
% 0.26/0.74    op2(e20,e23)=e23),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3638,f101])).
% 0.26/0.74  fof(f3652,plain,(
% 0.26/0.74    op2(e22,e20)=e22),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3638,f100])).
% 0.26/0.74  fof(f3653,plain,(
% 0.26/0.74    op2(e20,e22)=e22),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3638,f99])).
% 0.26/0.74  fof(f3655,plain,(
% 0.26/0.74    op2(e20,e21)=e21),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3638,f97])).
% 0.26/0.74  fof(f3658,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e23=e23|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3650,f3352])).
% 0.26/0.74  fof(f3660,plain,(
% 0.26/0.74    h1(e13)=e20|op2(e22,e20)=e20|e23=e20),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3650,f2241])).
% 0.26/0.74  fof(f3667,plain,(
% 0.26/0.74    ~e23=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3650,f1675])).
% 0.26/0.74  fof(f3672,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=op2(e20,e21)|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f3658])).
% 0.26/0.74  fof(f3673,plain,(
% 0.26/0.74    h1(e13)=e20|op2(e22,e20)=e20),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3660,f240])).
% 0.26/0.74  fof(f3689,plain,(
% 0.26/0.74    ~e23=op2(e22,e23)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3651,f203])).
% 0.26/0.74  fof(f3700,plain,(
% 0.26/0.74    e22=e23|h3(e13)=e23|op2(e22,e23)=e23),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3652,f2134])).
% 0.26/0.74  fof(f3703,plain,(
% 0.26/0.74    ~e22=op2(e22,e21)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3652,f220])).
% 0.26/0.74  fof(f3709,plain,(
% 0.26/0.74    h3(e13)=e23|op2(e22,e23)=e23),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3700,f243])).
% 0.26/0.74  fof(f3715,plain,(
% 0.26/0.74    e22=e21|h3(e13)=e21|op2(e23,e22)=e21),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3653,f2165])).
% 0.26/0.74  fof(f3725,plain,(
% 0.26/0.74    h3(e13)=e21|op2(e23,e22)=e21),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3715,f241])).
% 0.26/0.74  fof(f3732,plain,(
% 0.26/0.74    e21=e22|op2(e22,e21)=e22|op2(e23,e21)=e22),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3655,f1093])).
% 0.26/0.74  fof(f3734,plain,(
% 0.26/0.74    e21=e20|op2(e22,e21)=e20|op2(e23,e21)=e20),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3655,f1054])).
% 0.26/0.74  fof(f3736,plain,(
% 0.26/0.74    op2(e22,e21)=e22|op2(e23,e21)=e22),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3732,f241])).
% 0.26/0.74  fof(f3737,plain,(
% 0.26/0.74    op2(e22,e21)=e20|op2(e23,e21)=e20),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3734,f238])).
% 0.26/0.74  fof(f3739,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=e21|~e22=op2(e20,e22)|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3655,f3672])).
% 0.26/0.74  fof(f3740,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=e21|~e22=e22|~e23=op2(e20,e23)|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3653,f3739])).
% 0.26/0.74  fof(f3741,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=e21|~e22=e22|~e23=e23|~e22=op2(e22,e20)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3651,f3740])).
% 0.26/0.74  fof(f3742,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=e21|~e22=e22|~e23=e23|~e22=e22|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3652,f3741])).
% 0.26/0.74  fof(f3743,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e21=e21|~e22=e22|~e23=e23|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(duplicate_literals_removal,[status(thm)],[f3742])).
% 0.26/0.74  fof(f3744,plain,(
% 0.26/0.74    ~e20=h1(e13)|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f3743])).
% 0.26/0.74  fof(f3784,plain,(
% 0.26/0.74    h1(e13)=e20|e22=e20),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3652,f3673])).
% 0.26/0.74  fof(f3785,plain,(
% 0.26/0.74    ~e20=e20|~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3795,f3744])).
% 0.26/0.74  fof(f3795,plain,(
% 0.26/0.74    h1(e13)=e20),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3784,f239])).
% 0.26/0.74  fof(f3796,plain,(
% 0.26/0.74    ~e20=op2(e22,e21)|~e23=h3(e13)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f3785])).
% 0.26/0.74  fof(f3855,plain,(
% 0.26/0.74    h4(e13)=e20|h4(e13)=e21),
% 0.26/0.74    inference(backward_subsumption_resolution,[status(thm)],[f2381,f3667])).
% 0.26/0.74  fof(f3910,plain,(
% 0.26/0.74    ~e20=op2(e22,e21)|~e23=e23|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3923,f3796])).
% 0.26/0.74  fof(f3914,plain,(
% 0.26/0.74    op2(e22,e21)=e21|e23=e21|op2(e22,e23)=e21),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3923,f2443])).
% 0.26/0.74  fof(f3923,plain,(
% 0.26/0.74    h3(e13)=e23),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3709,f3689])).
% 0.26/0.74  fof(f3924,plain,(
% 0.26/0.74    ~e20=op2(e22,e21)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=op2(e23,e22)|~e20=h4(e13)),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f3910])).
% 0.26/0.74  fof(f3957,plain,(
% 0.26/0.74    op2(e22,e21)=e21|op2(e22,e23)=e21),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3914,f242])).
% 0.26/0.74  fof(f3960,plain,(
% 0.26/0.74    e23=e21|op2(e23,e22)=e21),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3923,f3725])).
% 0.26/0.74  fof(f3965,plain,(
% 0.26/0.74    ~e21=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f3967,f1682])).
% 0.26/0.74  fof(f3967,plain,(
% 0.26/0.74    op2(e23,e22)=e21),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3960,f242])).
% 0.26/0.74  fof(f3971,plain,(
% 0.26/0.74    ~e20=op2(e22,e21)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e21=e21|~e20=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f3967,f3924])).
% 0.26/0.74  fof(f3972,plain,(
% 0.26/0.74    ~e20=op2(e22,e21)|~e21=op2(e22,e23)|~e22=op2(e23,e21)|~e20=h4(e13)),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f3971])).
% 0.26/0.74  fof(f4020,plain,(
% 0.26/0.74    ~e20=op2(e22,e21)|~e21=op2(e22,e23)|~e22=e22|~e20=h4(e13)),
% 0.26/0.74    inference(backward_demodulation,[status(thm)],[f4025,f3972])).
% 0.26/0.74  fof(f4025,plain,(
% 0.26/0.74    op2(e23,e21)=e22),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3736,f3703])).
% 0.26/0.74  fof(f4026,plain,(
% 0.26/0.74    ~e20=op2(e22,e21)|~e21=op2(e22,e23)|~e20=h4(e13)),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f4020])).
% 0.26/0.74  fof(f4028,plain,(
% 0.26/0.74    op2(e22,e21)=e20|e22=e20),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f4025,f3737])).
% 0.26/0.74  fof(f4034,plain,(
% 0.26/0.74    op2(e22,e21)=e20),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f4028,f239])).
% 0.26/0.74  fof(f4045,plain,(
% 0.26/0.74    h4(e13)=e20),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f3855,f3965])).
% 0.26/0.74  fof(f4076,plain,(
% 0.26/0.74    e20=e21|op2(e22,e23)=e21),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f4034,f3957])).
% 0.26/0.74  fof(f4080,plain,(
% 0.26/0.74    op2(e22,e23)=e21),
% 0.26/0.74    inference(forward_subsumption_resolution,[status(thm)],[f4076,f238])).
% 0.26/0.74  fof(f4129,plain,(
% 0.26/0.74    ~e20=e20|~e21=op2(e22,e23)|~e20=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f4034,f4026])).
% 0.26/0.74  fof(f4130,plain,(
% 0.26/0.74    ~e20=e20|~e21=e21|~e20=h4(e13)),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f4080,f4129])).
% 0.26/0.74  fof(f4131,plain,(
% 0.26/0.74    ~e20=e20|~e21=e21|~e20=e20),
% 0.26/0.74    inference(forward_demodulation,[status(thm)],[f4045,f4130])).
% 0.26/0.74  fof(f4132,plain,(
% 0.26/0.74    ~e20=e20|~e21=e21),
% 0.26/0.74    inference(duplicate_literals_removal,[status(thm)],[f4131])).
% 0.26/0.74  fof(f4133,plain,(
% 0.26/0.74    $false),
% 0.26/0.74    inference(trivial_equality_resolution,[status(thm)],[f4132])).
% 0.26/0.74  % SZS output end CNFRefutation for theBenchmark.p
% 0.26/0.76  % Elapsed time: 0.329897 seconds
% 0.26/0.76  % CPU time: 2.171426 seconds
% 0.26/0.76  % Total memory used: 148.242 MB
% 0.26/0.76  % Net memory used: 147.069 MB
%------------------------------------------------------------------------------