%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG016+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 : n007.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:27 AM UTC 2026
% Result : Theorem 0.13s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 12:51:21 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 0.13/0.46 % Refutation found
% 0.13/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.46 fof(f1,axiom,(
% 0.13/0.46 ( ( op1(e10,e10) = e10| op1(e10,e10) = e11| op1(e10,e10) = e12| op1(e10,e10) = e13 )& ( op1(e10,e11) = e10| op1(e10,e11) = e11| op1(e10,e11) = e12| op1(e10,e11) = e13 )& ( op1(e10,e12) = e10| op1(e10,e12) = e11| op1(e10,e12) = e12| op1(e10,e12) = e13 )& ( op1(e10,e13) = e10| op1(e10,e13) = e11| op1(e10,e13) = e12| op1(e10,e13) = e13 )& ( op1(e11,e10) = e10| op1(e11,e10) = e11| op1(e11,e10) = e12| op1(e11,e10) = e13 )& ( op1(e11,e11) = e10| op1(e11,e11) = e11| op1(e11,e11) = e12| op1(e11,e11) = e13 )& ( op1(e11,e12) = e10| op1(e11,e12) = e11| op1(e11,e12) = e12| op1(e11,e12) = e13 )& ( op1(e11,e13) = e10| op1(e11,e13) = e11| op1(e11,e13) = e12| op1(e11,e13) = e13 )& ( op1(e12,e10) = e10| op1(e12,e10) = e11| op1(e12,e10) = e12| op1(e12,e10) = e13 )& ( op1(e12,e11) = e10| op1(e12,e11) = e11| op1(e12,e11) = e12| op1(e12,e11) = e13 )& ( op1(e12,e12) = e10| op1(e12,e12) = e11| op1(e12,e12) = e12| op1(e12,e12) = e13 )& ( op1(e12,e13) = e10| op1(e12,e13) = e11| op1(e12,e13) = e12| op1(e12,e13) = e13 )& ( op1(e13,e10) = e10| op1(e13,e10) = e11| op1(e13,e10) = e12| op1(e13,e10) = e13 )& ( op1(e13,e11) = e10| op1(e13,e11) = e11| op1(e13,e11) = e12| op1(e13,e11) = e13 )& ( op1(e13,e12) = e10| op1(e13,e12) = e11| op1(e13,e12) = e12| op1(e13,e12) = e13 )& ( op1(e13,e13) = e10| op1(e13,e13) = e11| op1(e13,e13) = e12| op1(e13,e13) = e13 ) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f2,axiom,(
% 0.13/0.46 ( op1(op1(e10,e10),e10) = op1(e10,op1(e10,e10))& op1(op1(e10,e10),e11) = op1(e10,op1(e10,e11))& op1(op1(e10,e10),e12) = op1(e10,op1(e10,e12))& op1(op1(e10,e10),e13) = op1(e10,op1(e10,e13))& op1(op1(e10,e11),e10) = op1(e10,op1(e11,e10))& op1(op1(e10,e11),e11) = op1(e10,op1(e11,e11))& op1(op1(e10,e11),e12) = op1(e10,op1(e11,e12))& op1(op1(e10,e11),e13) = op1(e10,op1(e11,e13))& op1(op1(e10,e12),e10) = op1(e10,op1(e12,e10))& op1(op1(e10,e12),e11) = op1(e10,op1(e12,e11))& op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12))& op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13))& op1(op1(e10,e13),e10) = op1(e10,op1(e13,e10))& op1(op1(e10,e13),e11) = op1(e10,op1(e13,e11))& op1(op1(e10,e13),e12) = op1(e10,op1(e13,e12))& op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13))& op1(op1(e11,e10),e10) = op1(e11,op1(e10,e10))& op1(op1(e11,e10),e11) = op1(e11,op1(e10,e11))& op1(op1(e11,e10),e12) = op1(e11,op1(e10,e12))& op1(op1(e11,e10),e13) = op1(e11,op1(e10,e13))& op1(op1(e11,e11),e10) = op1(e11,op1(e11,e10))& op1(op1(e11,e11),e11) = op1(e11,op1(e11,e11))& op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12))& op1(op1(e11,e11),e13) = op1(e11,op1(e11,e13))& op1(op1(e11,e12),e10) = op1(e11,op1(e12,e10))& op1(op1(e11,e12),e11) = op1(e11,op1(e12,e11))& op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12))& op1(op1(e11,e12),e13) = op1(e11,op1(e12,e13))& op1(op1(e11,e13),e10) = op1(e11,op1(e13,e10))& op1(op1(e11,e13),e11) = op1(e11,op1(e13,e11))& op1(op1(e11,e13),e12) = op1(e11,op1(e13,e12))& op1(op1(e11,e13),e13) = op1(e11,op1(e13,e13))& op1(op1(e12,e10),e10) = op1(e12,op1(e10,e10))& op1(op1(e12,e10),e11) = op1(e12,op1(e10,e11))& op1(op1(e12,e10),e12) = op1(e12,op1(e10,e12))& op1(op1(e12,e10),e13) = op1(e12,op1(e10,e13))& op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10))& op1(op1(e12,e11),e11) = op1(e12,op1(e11,e11))& op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12))& op1(op1(e12,e11),e13) = op1(e12,op1(e11,e13))& op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10))& op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11))& op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12))& op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13))& op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10))& op1(op1(e12,e13),e11) = op1(e12,op1(e13,e11))& op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12))& op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13))& op1(op1(e13,e10),e10) = op1(e13,op1(e10,e10))& op1(op1(e13,e10),e11) = op1(e13,op1(e10,e11))& op1(op1(e13,e10),e12) = op1(e13,op1(e10,e12))& op1(op1(e13,e10),e13) = op1(e13,op1(e10,e13))& op1(op1(e13,e11),e10) = op1(e13,op1(e11,e10))& op1(op1(e13,e11),e11) = op1(e13,op1(e11,e11))& op1(op1(e13,e11),e12) = op1(e13,op1(e11,e12))& op1(op1(e13,e11),e13) = op1(e13,op1(e11,e13))& op1(op1(e13,e12),e10) = op1(e13,op1(e12,e10))& op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11))& op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12))& op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13))& op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10))& op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11))& op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12))& op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f5,axiom,(
% 0.13/0.46 ( ( op2(e20,e20) = e20| op2(e20,e20) = e21| op2(e20,e20) = e22| op2(e20,e20) = e23 )& ( op2(e20,e21) = e20| op2(e20,e21) = e21| op2(e20,e21) = e22| op2(e20,e21) = e23 )& ( op2(e20,e22) = e20| op2(e20,e22) = e21| op2(e20,e22) = e22| op2(e20,e22) = e23 )& ( op2(e20,e23) = e20| op2(e20,e23) = e21| op2(e20,e23) = e22| op2(e20,e23) = e23 )& ( op2(e21,e20) = e20| op2(e21,e20) = e21| op2(e21,e20) = e22| op2(e21,e20) = e23 )& ( op2(e21,e21) = e20| op2(e21,e21) = e21| op2(e21,e21) = e22| op2(e21,e21) = e23 )& ( op2(e21,e22) = e20| op2(e21,e22) = e21| op2(e21,e22) = e22| op2(e21,e22) = e23 )& ( op2(e21,e23) = e20| op2(e21,e23) = e21| op2(e21,e23) = e22| op2(e21,e23) = e23 )& ( op2(e22,e20) = e20| op2(e22,e20) = e21| op2(e22,e20) = e22| op2(e22,e20) = e23 )& ( op2(e22,e21) = e20| op2(e22,e21) = e21| op2(e22,e21) = e22| op2(e22,e21) = e23 )& ( op2(e22,e22) = e20| op2(e22,e22) = e21| op2(e22,e22) = e22| op2(e22,e22) = e23 )& ( op2(e22,e23) = e20| op2(e22,e23) = e21| op2(e22,e23) = e22| op2(e22,e23) = e23 )& ( op2(e23,e20) = e20| op2(e23,e20) = e21| op2(e23,e20) = e22| op2(e23,e20) = e23 )& ( op2(e23,e21) = e20| op2(e23,e21) = e21| op2(e23,e21) = e22| op2(e23,e21) = e23 )& ( op2(e23,e22) = e20| op2(e23,e22) = e21| op2(e23,e22) = e22| op2(e23,e22) = e23 )& ( op2(e23,e23) = e20| op2(e23,e23) = e21| op2(e23,e23) = e22| op2(e23,e23) = e23 ) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f6,axiom,(
% 0.13/0.46 ( op2(op2(e20,e20),e20) = op2(e20,op2(e20,e20))& op2(op2(e20,e20),e21) = op2(e20,op2(e20,e21))& op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22))& op2(op2(e20,e20),e23) = op2(e20,op2(e20,e23))& op2(op2(e20,e21),e20) = op2(e20,op2(e21,e20))& op2(op2(e20,e21),e21) = op2(e20,op2(e21,e21))& op2(op2(e20,e21),e22) = op2(e20,op2(e21,e22))& op2(op2(e20,e21),e23) = op2(e20,op2(e21,e23))& op2(op2(e20,e22),e20) = op2(e20,op2(e22,e20))& op2(op2(e20,e22),e21) = op2(e20,op2(e22,e21))& op2(op2(e20,e22),e22) = op2(e20,op2(e22,e22))& op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23))& op2(op2(e20,e23),e20) = op2(e20,op2(e23,e20))& op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21))& op2(op2(e20,e23),e22) = op2(e20,op2(e23,e22))& op2(op2(e20,e23),e23) = op2(e20,op2(e23,e23))& op2(op2(e21,e20),e20) = op2(e21,op2(e20,e20))& op2(op2(e21,e20),e21) = op2(e21,op2(e20,e21))& op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22))& op2(op2(e21,e20),e23) = op2(e21,op2(e20,e23))& op2(op2(e21,e21),e20) = op2(e21,op2(e21,e20))& op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21))& op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22))& op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23))& op2(op2(e21,e22),e20) = op2(e21,op2(e22,e20))& op2(op2(e21,e22),e21) = op2(e21,op2(e22,e21))& op2(op2(e21,e22),e22) = op2(e21,op2(e22,e22))& op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23))& op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20))& op2(op2(e21,e23),e21) = op2(e21,op2(e23,e21))& op2(op2(e21,e23),e22) = op2(e21,op2(e23,e22))& op2(op2(e21,e23),e23) = op2(e21,op2(e23,e23))& op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20))& op2(op2(e22,e20),e21) = op2(e22,op2(e20,e21))& op2(op2(e22,e20),e22) = op2(e22,op2(e20,e22))& op2(op2(e22,e20),e23) = op2(e22,op2(e20,e23))& op2(op2(e22,e21),e20) = op2(e22,op2(e21,e20))& op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21))& op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22))& op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23))& op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20))& op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21))& op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22))& op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23))& op2(op2(e22,e23),e20) = op2(e22,op2(e23,e20))& op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21))& op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22))& op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23))& op2(op2(e23,e20),e20) = op2(e23,op2(e20,e20))& op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21))& op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22))& op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23))& op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20))& op2(op2(e23,e21),e21) = op2(e23,op2(e21,e21))& op2(op2(e23,e21),e22) = op2(e23,op2(e21,e22))& op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23))& op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20))& op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21))& op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22))& op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23))& op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20))& op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21))& op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22))& op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f17,axiom,(
% 0.13/0.46 ( op1(e10,e10) != op1(e11,e10)& op1(e10,e10) != op1(e12,e10)& op1(e10,e10) != op1(e13,e10)& op1(e11,e10) != op1(e12,e10)& op1(e11,e10) != op1(e13,e10)& op1(e12,e10) != op1(e13,e10)& op1(e10,e11) != op1(e11,e11)& op1(e10,e11) != op1(e12,e11)& op1(e10,e11) != op1(e13,e11)& op1(e11,e11) != op1(e12,e11)& op1(e11,e11) != op1(e13,e11)& op1(e12,e11) != op1(e13,e11)& op1(e10,e12) != op1(e11,e12)& op1(e10,e12) != op1(e12,e12)& op1(e10,e12) != op1(e13,e12)& op1(e11,e12) != op1(e12,e12)& op1(e11,e12) != op1(e13,e12)& op1(e12,e12) != op1(e13,e12)& op1(e10,e13) != op1(e11,e13)& op1(e10,e13) != op1(e12,e13)& op1(e10,e13) != op1(e13,e13)& op1(e11,e13) != op1(e12,e13)& op1(e11,e13) != op1(e13,e13)& op1(e12,e13) != op1(e13,e13)& op1(e10,e10) != op1(e10,e11)& op1(e10,e10) != op1(e10,e12)& op1(e10,e10) != op1(e10,e13)& op1(e10,e11) != op1(e10,e12)& op1(e10,e11) != op1(e10,e13)& op1(e10,e12) != op1(e10,e13)& op1(e11,e10) != op1(e11,e11)& op1(e11,e10) != op1(e11,e12)& op1(e11,e10) != op1(e11,e13)& op1(e11,e11) != op1(e11,e12)& op1(e11,e11) != op1(e11,e13)& op1(e11,e12) != op1(e11,e13)& op1(e12,e10) != op1(e12,e11)& op1(e12,e10) != op1(e12,e12)& op1(e12,e10) != op1(e12,e13)& op1(e12,e11) != op1(e12,e12)& op1(e12,e11) != op1(e12,e13)& op1(e12,e12) != op1(e12,e13)& op1(e13,e10) != op1(e13,e11)& op1(e13,e10) != op1(e13,e12)& op1(e13,e10) != op1(e13,e13)& op1(e13,e11) != op1(e13,e12)& op1(e13,e11) != op1(e13,e13)& op1(e13,e12) != op1(e13,e13) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f18,axiom,(
% 0.13/0.46 ( op2(e20,e20) != op2(e21,e20)& op2(e20,e20) != op2(e22,e20)& op2(e20,e20) != op2(e23,e20)& op2(e21,e20) != op2(e22,e20)& op2(e21,e20) != op2(e23,e20)& op2(e22,e20) != op2(e23,e20)& op2(e20,e21) != op2(e21,e21)& op2(e20,e21) != op2(e22,e21)& op2(e20,e21) != op2(e23,e21)& op2(e21,e21) != op2(e22,e21)& op2(e21,e21) != op2(e23,e21)& op2(e22,e21) != op2(e23,e21)& op2(e20,e22) != op2(e21,e22)& op2(e20,e22) != op2(e22,e22)& op2(e20,e22) != op2(e23,e22)& op2(e21,e22) != op2(e22,e22)& op2(e21,e22) != op2(e23,e22)& op2(e22,e22) != op2(e23,e22)& op2(e20,e23) != op2(e21,e23)& op2(e20,e23) != op2(e22,e23)& op2(e20,e23) != op2(e23,e23)& op2(e21,e23) != op2(e22,e23)& op2(e21,e23) != op2(e23,e23)& op2(e22,e23) != op2(e23,e23)& op2(e20,e20) != op2(e20,e21)& op2(e20,e20) != op2(e20,e22)& op2(e20,e20) != op2(e20,e23)& op2(e20,e21) != op2(e20,e22)& op2(e20,e21) != op2(e20,e23)& op2(e20,e22) != op2(e20,e23)& op2(e21,e20) != op2(e21,e21)& op2(e21,e20) != op2(e21,e22)& op2(e21,e20) != op2(e21,e23)& op2(e21,e21) != op2(e21,e22)& op2(e21,e21) != op2(e21,e23)& op2(e21,e22) != op2(e21,e23)& op2(e22,e20) != op2(e22,e21)& op2(e22,e20) != op2(e22,e22)& op2(e22,e20) != op2(e22,e23)& op2(e22,e21) != op2(e22,e22)& op2(e22,e21) != op2(e22,e23)& op2(e22,e22) != op2(e22,e23)& op2(e23,e20) != op2(e23,e21)& op2(e23,e20) != op2(e23,e22)& op2(e23,e20) != op2(e23,e23)& op2(e23,e21) != op2(e23,e22)& op2(e23,e21) != op2(e23,e23)& op2(e23,e22) != op2(e23,e23) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f24,axiom,(
% 0.13/0.46 ( e10 = op1(op1(e12,op1(e12,e12)),e12)& e11 = op1(e12,op1(e12,e12))& e13 = op1(e12,e12) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f25,axiom,(
% 0.13/0.46 ( e20 = op2(op2(e22,op2(e22,e22)),e22)& e21 = op2(e22,op2(e22,e22))& e23 = op2(e22,e22) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f26,axiom,(
% 0.13/0.46 ( h1(e12) = e20& h1(e10) = op2(op2(e20,op2(e20,e20)),e20)& h1(e11) = op2(e20,op2(e20,e20))& h1(e13) = op2(e20,e20) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f27,axiom,(
% 0.13/0.46 ( h2(e12) = e21& h2(e10) = op2(op2(e21,op2(e21,e21)),e21)& h2(e11) = op2(e21,op2(e21,e21))& h2(e13) = op2(e21,e21) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f28,axiom,(
% 0.13/0.46 ( h3(e12) = e22& h3(e10) = op2(op2(e22,op2(e22,e22)),e22)& h3(e11) = op2(e22,op2(e22,e22))& h3(e13) = op2(e22,e22) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f29,axiom,(
% 0.13/0.46 ( h4(e12) = e23& h4(e10) = op2(op2(e23,op2(e23,e23)),e23)& h4(e11) = op2(e23,op2(e23,e23))& h4(e13) = op2(e23,e23) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f30,conjecture,(
% 0.13/0.46 ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))& ( h1(e10) = e20| h1(e11) = e20| h1(e12) = e20| h1(e13) = e20 )& ( h1(e10) = e21| h1(e11) = e21| h1(e12) = e21| h1(e13) = e21 )& ( h1(e10) = e22| h1(e11) = e22| h1(e12) = e22| h1(e13) = e22 )& ( h1(e10) = e23| h1(e11) = e23| h1(e12) = e23| h1(e13) = e23 ) )| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))& ( h2(e10) = e20| h2(e11) = e20| h2(e12) = e20| h2(e13) = e20 )& ( h2(e10) = e21| h2(e11) = e21| h2(e12) = e21| h2(e13) = e21 )& ( h2(e10) = e22| h2(e11) = e22| h2(e12) = e22| h2(e13) = e22 )& ( h2(e10) = e23| h2(e11) = e23| h2(e12) = e23| h2(e13) = e23 ) )| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))& ( h3(e10) = e20| h3(e11) = e20| h3(e12) = e20| h3(e13) = e20 )& ( h3(e10) = e21| h3(e11) = e21| h3(e12) = e21| h3(e13) = e21 )& ( h3(e10) = e22| h3(e11) = e22| h3(e12) = e22| h3(e13) = e22 )& ( h3(e10) = e23| h3(e11) = e23| h3(e12) = e23| h3(e13) = e23 ) )| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))& ( h4(e10) = e20| h4(e11) = e20| h4(e12) = e20| h4(e13) = e20 )& ( h4(e10) = e21| h4(e11) = e21| h4(e12) = e21| h4(e13) = e21 )& ( h4(e10) = e22| h4(e11) = e22| h4(e12) = e22| h4(e13) = e22 )& ( h4(e10) = e23| h4(e11) = e23| h4(e12) = e23| h4(e13) = e23 ) ) ) ),
% 0.13/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.46 fof(f31,negated_conjecture,(
% 0.13/0.46 ~(( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))& ( h1(e10) = e20| h1(e11) = e20| h1(e12) = e20| h1(e13) = e20 )& ( h1(e10) = e21| h1(e11) = e21| h1(e12) = e21| h1(e13) = e21 )& ( h1(e10) = e22| h1(e11) = e22| h1(e12) = e22| h1(e13) = e22 )& ( h1(e10) = e23| h1(e11) = e23| h1(e12) = e23| h1(e13) = e23 ) )| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))& ( h2(e10) = e20| h2(e11) = e20| h2(e12) = e20| h2(e13) = e20 )& ( h2(e10) = e21| h2(e11) = e21| h2(e12) = e21| h2(e13) = e21 )& ( h2(e10) = e22| h2(e11) = e22| h2(e12) = e22| h2(e13) = e22 )& ( h2(e10) = e23| h2(e11) = e23| h2(e12) = e23| h2(e13) = e23 ) )| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))& ( h3(e10) = e20| h3(e11) = e20| h3(e12) = e20| h3(e13) = e20 )& ( h3(e10) = e21| h3(e11) = e21| h3(e12) = e21| h3(e13) = e21 )& ( h3(e10) = e22| h3(e11) = e22| h3(e12) = e22| h3(e13) = e22 )& ( h3(e10) = e23| h3(e11) = e23| h3(e12) = e23| h3(e13) = e23 ) )| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))& ( h4(e10) = e20| h4(e11) = e20| h4(e12) = e20| h4(e13) = e20 )& ( h4(e10) = e21| h4(e11) = e21| h4(e12) = e21| h4(e13) = e21 )& ( h4(e10) = e22| h4(e11) = e22| h4(e12) = e22| h4(e13) = e22 )& ( h4(e10) = e23| h4(e11) = e23| h4(e12) = e23| h4(e13) = e23 ) ) ) )),
% 0.13/0.46 inference(negated_conjecture,[status(cth)],[f30])).
% 0.13/0.46 fof(f34,plain,(
% 0.13/0.46 op1(e10,e12)=e10|op1(e10,e12)=e11|op1(e10,e12)=e12|op1(e10,e12)=e13),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.46 fof(f57,plain,(
% 0.13/0.46 op1(op1(e10,e12),e11)=op1(e10,op1(e12,e11))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f58,plain,(
% 0.13/0.46 op1(op1(e10,e12),e12)=op1(e10,op1(e12,e12))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f59,plain,(
% 0.13/0.46 op1(op1(e10,e12),e13)=op1(e10,op1(e12,e13))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f73,plain,(
% 0.13/0.46 op1(op1(e11,e12),e11)=op1(e11,op1(e12,e11))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f74,plain,(
% 0.13/0.46 op1(op1(e11,e12),e12)=op1(e11,op1(e12,e12))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f75,plain,(
% 0.13/0.46 op1(op1(e11,e12),e13)=op1(e11,op1(e12,e13))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f77,plain,(
% 0.13/0.46 op1(op1(e11,e13),e11)=op1(e11,op1(e13,e11))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f86,plain,(
% 0.13/0.46 op1(op1(e12,e11),e12)=op1(e12,op1(e11,e12))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f87,plain,(
% 0.13/0.46 op1(op1(e12,e11),e13)=op1(e12,op1(e11,e13))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f90,plain,(
% 0.13/0.46 op1(op1(e12,e12),e12)=op1(e12,op1(e12,e12))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f91,plain,(
% 0.13/0.46 op1(op1(e12,e12),e13)=op1(e12,op1(e12,e13))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f94,plain,(
% 0.13/0.46 op1(op1(e12,e13),e12)=op1(e12,op1(e13,e12))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f102,plain,(
% 0.13/0.46 op1(op1(e13,e11),e12)=op1(e13,op1(e11,e12))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f107,plain,(
% 0.13/0.46 op1(op1(e13,e12),e13)=op1(e13,op1(e12,e13))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f110,plain,(
% 0.13/0.46 op1(op1(e13,e13),e12)=op1(e13,op1(e13,e12))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.46 fof(f141,plain,(
% 0.13/0.46 op2(e22,e20)=e20|op2(e22,e20)=e21|op2(e22,e20)=e22|op2(e22,e20)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.46 fof(f173,plain,(
% 0.13/0.46 op2(op2(e21,e22),e20)=op2(e21,op2(e22,e20))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f174,plain,(
% 0.13/0.46 op2(op2(e21,e22),e21)=op2(e21,op2(e22,e21))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f175,plain,(
% 0.13/0.46 op2(op2(e21,e22),e22)=op2(e21,op2(e22,e22))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f176,plain,(
% 0.13/0.46 op2(op2(e21,e22),e23)=op2(e21,op2(e22,e23))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f179,plain,(
% 0.13/0.46 op2(op2(e21,e23),e22)=op2(e21,op2(e23,e22))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f187,plain,(
% 0.13/0.46 op2(op2(e22,e21),e22)=op2(e22,op2(e21,e22))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f191,plain,(
% 0.13/0.46 op2(op2(e22,e22),e22)=op2(e22,op2(e22,e22))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f192,plain,(
% 0.13/0.46 op2(op2(e22,e22),e23)=op2(e22,op2(e22,e23))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f194,plain,(
% 0.13/0.46 op2(op2(e22,e23),e21)=op2(e22,op2(e23,e21))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f195,plain,(
% 0.13/0.46 op2(op2(e22,e23),e22)=op2(e22,op2(e23,e22))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f196,plain,(
% 0.13/0.46 op2(op2(e22,e23),e23)=op2(e22,op2(e23,e23))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f206,plain,(
% 0.13/0.46 op2(op2(e23,e22),e21)=op2(e23,op2(e22,e21))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f208,plain,(
% 0.13/0.46 op2(op2(e23,e22),e23)=op2(e23,op2(e22,e23))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f210,plain,(
% 0.13/0.46 op2(op2(e23,e23),e21)=op2(e23,op2(e23,e21))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f211,plain,(
% 0.13/0.46 op2(op2(e23,e23),e22)=op2(e23,op2(e23,e22))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.46 fof(f302,plain,(
% 0.13/0.46 ~op1(e10,e12)=op1(e11,e12)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.46 fof(f303,plain,(
% 0.13/0.46 ~op1(e10,e12)=op1(e12,e12)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.46 fof(f304,plain,(
% 0.13/0.46 ~op1(e10,e12)=op1(e13,e12)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.46 fof(f374,plain,(
% 0.13/0.46 ~op2(e22,e20)=op2(e22,e21)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.46 fof(f375,plain,(
% 0.13/0.46 ~op2(e22,e20)=op2(e22,e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.46 fof(f376,plain,(
% 0.13/0.46 ~op2(e22,e20)=op2(e22,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.46 fof(f424,plain,(
% 0.13/0.46 e10=op1(op1(e12,op1(e12,e12)),e12)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/0.46 fof(f425,plain,(
% 0.13/0.46 e11=op1(e12,op1(e12,e12))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/0.46 fof(f426,plain,(
% 0.13/0.46 e13=op1(e12,e12)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/0.46 fof(f427,plain,(
% 0.13/0.46 e20=op2(op2(e22,op2(e22,e22)),e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.46 fof(f428,plain,(
% 0.13/0.46 e21=op2(e22,op2(e22,e22))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.46 fof(f429,plain,(
% 0.13/0.46 e23=op2(e22,e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.46 fof(f433,plain,(
% 0.13/0.46 h1(e13)=op2(e20,e20)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/0.46 fof(f437,plain,(
% 0.13/0.46 h2(e13)=op2(e21,e21)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f27])).
% 0.13/0.46 fof(f438,plain,(
% 0.13/0.46 h3(e12)=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/0.46 fof(f439,plain,(
% 0.13/0.46 h3(e10)=op2(op2(e22,op2(e22,e22)),e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/0.46 fof(f440,plain,(
% 0.13/0.46 h3(e11)=op2(e22,op2(e22,e22))),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/0.46 fof(f441,plain,(
% 0.13/0.46 h3(e13)=op2(e22,e22)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/0.46 fof(f445,plain,(
% 0.13/0.46 h4(e13)=op2(e23,e23)),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.46 fof(f446,plain,(
% 0.13/0.46 ((((((((((((((((((((((~h1(op1(e10,e10))=op2(h1(e10),h1(e10))|~h1(op1(e10,e11))=op2(h1(e10),h1(e11)))|~h1(op1(e10,e12))=op2(h1(e10),h1(e12)))|~h1(op1(e10,e13))=op2(h1(e10),h1(e13)))|~h1(op1(e11,e10))=op2(h1(e11),h1(e10)))|~h1(op1(e11,e11))=op2(h1(e11),h1(e11)))|~h1(op1(e11,e12))=op2(h1(e11),h1(e12)))|~h1(op1(e11,e13))=op2(h1(e11),h1(e13)))|~h1(op1(e12,e10))=op2(h1(e12),h1(e10)))|~h1(op1(e12,e11))=op2(h1(e12),h1(e11)))|~h1(op1(e12,e12))=op2(h1(e12),h1(e12)))|~h1(op1(e12,e13))=op2(h1(e12),h1(e13)))|~h1(op1(e13,e10))=op2(h1(e13),h1(e10)))|~h1(op1(e13,e11))=op2(h1(e13),h1(e11)))|~h1(op1(e13,e12))=op2(h1(e13),h1(e12)))|~h1(op1(e13,e13))=op2(h1(e13),h1(e13)))|(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20))|(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21))|(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22))|(((~h1(e10)=e23&~h1(e11)=e23)&~h1(e12)=e23)&~h1(e13)=e23))&(((((((((((((((((((~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11)))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12)))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13)))|~h2(op1(e11,e10))=op2(h2(e11),h2(e10)))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11)))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12)))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13)))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10)))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11)))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12)))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13)))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10)))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11)))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12)))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13)))|(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20))|(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21))|(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22))|(((~h2(e10)=e23&~h2(e11)=e23)&~h2(e12)=e23)&~h2(e13)=e23)))&(((((((((((((((((((~h3(op1(e10,e10))=op2(h3(e10),h3(e10))|~h3(op1(e10,e11))=op2(h3(e10),h3(e11)))|~h3(op1(e10,e12))=op2(h3(e10),h3(e12)))|~h3(op1(e10,e13))=op2(h3(e10),h3(e13)))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10)))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11)))|~h3(op1(e11,e12))=op2(h3(e11),h3(e12)))|~h3(op1(e11,e13))=op2(h3(e11),h3(e13)))|~h3(op1(e12,e10))=op2(h3(e12),h3(e10)))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11)))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12)))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13)))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10)))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11)))|~h3(op1(e13,e12))=op2(h3(e13),h3(e12)))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13)))|(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20))|(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21))|(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22))|(((~h3(e10)=e23&~h3(e11)=e23)&~h3(e12)=e23)&~h3(e13)=e23)))&(((((((((((((((((((~h4(op1(e10,e10))=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11)))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12)))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13)))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10)))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11)))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12)))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13)))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10)))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11)))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12)))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13)))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10)))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11)))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12)))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13)))|(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20))|(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21))|(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22))|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23)))),
% 0.13/0.46 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.13/0.46 fof(f447,definition,(
% 0.13/0.46 sP0_prd<=>(((~h1(e10)=e20&~h1(e11)=e20)&~h1(e12)=e20)&~h1(e13)=e20)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.46 fof(f448,definition,(
% 0.13/0.46 sP1_prd<=>(((~h1(e10)=e21&~h1(e11)=e21)&~h1(e12)=e21)&~h1(e13)=e21)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.13/0.46 fof(f449,definition,(
% 0.13/0.46 sP2_prd<=>(((~h1(e10)=e22&~h1(e11)=e22)&~h1(e12)=e22)&~h1(e13)=e22)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.13/0.46 fof(f450,definition,(
% 0.13/0.46 sP3_prd<=>(((~h2(e10)=e20&~h2(e11)=e20)&~h2(e12)=e20)&~h2(e13)=e20)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.13/0.46 fof(f451,definition,(
% 0.13/0.46 sP4_prd<=>(((~h2(e10)=e21&~h2(e11)=e21)&~h2(e12)=e21)&~h2(e13)=e21)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.13/0.46 fof(f452,definition,(
% 0.13/0.46 sP5_prd<=>(((~h2(e10)=e22&~h2(e11)=e22)&~h2(e12)=e22)&~h2(e13)=e22)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.13/0.46 fof(f453,definition,(
% 0.13/0.46 sP6_prd<=>(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.13/0.46 fof(f454,definition,(
% 0.13/0.46 sP7_prd<=>(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.13/0.46 fof(f455,definition,(
% 0.13/0.46 sP8_prd<=>(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.13/0.46 fof(f456,definition,(
% 0.13/0.46 sP9_prd<=>(((~h4(e10)=e20&~h4(e11)=e20)&~h4(e12)=e20)&~h4(e13)=e20)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.13/0.46 fof(f457,definition,(
% 0.13/0.46 sP10_prd<=>(((~h4(e10)=e21&~h4(e11)=e21)&~h4(e12)=e21)&~h4(e13)=e21)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.13/0.46 fof(f458,definition,(
% 0.13/0.46 sP11_prd<=>(((~h4(e10)=e22&~h4(e11)=e22)&~h4(e12)=e22)&~h4(e13)=e22)),
% 0.13/0.46 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.13/0.46 fof(f459,plain,(
% 0.13/0.46 (((((((((((((((((((((~h1(op1(e10,e10))=op2(h1(e10),h1(e10))|~h1(op1(e10,e11))=op2(h1(e10),h1(e11)))|~h1(op1(e10,e12))=op2(h1(e10),h1(e12)))|~h1(op1(e10,e13))=op2(h1(e10),h1(e13)))|~h1(op1(e11,e10))=op2(h1(e11),h1(e10)))|~h1(op1(e11,e11))=op2(h1(e11),h1(e11)))|~h1(op1(e11,e12))=op2(h1(e11),h1(e12)))|~h1(op1(e11,e13))=op2(h1(e11),h1(e13)))|~h1(op1(e12,e10))=op2(h1(e12),h1(e10)))|~h1(op1(e12,e11))=op2(h1(e12),h1(e11)))|~h1(op1(e12,e12))=op2(h1(e12),h1(e12)))|~h1(op1(e12,e13))=op2(h1(e12),h1(e13)))|~h1(op1(e13,e10))=op2(h1(e13),h1(e10)))|~h1(op1(e13,e11))=op2(h1(e13),h1(e11)))|~h1(op1(e13,e12))=op2(h1(e13),h1(e12)))|~h1(op1(e13,e13))=op2(h1(e13),h1(e13)))|sP0_prd)|sP1_prd)|sP2_prd)|(((~h1(e10)=e23&~h1(e11)=e23)&~h1(e12)=e23)&~h1(e13)=e23))&(((((((((((((((((((~h2(op1(e10,e10))=op2(h2(e10),h2(e10))|~h2(op1(e10,e11))=op2(h2(e10),h2(e11)))|~h2(op1(e10,e12))=op2(h2(e10),h2(e12)))|~h2(op1(e10,e13))=op2(h2(e10),h2(e13)))|~h2(op1(e11,e10))=op2(h2(e11),h2(e10)))|~h2(op1(e11,e11))=op2(h2(e11),h2(e11)))|~h2(op1(e11,e12))=op2(h2(e11),h2(e12)))|~h2(op1(e11,e13))=op2(h2(e11),h2(e13)))|~h2(op1(e12,e10))=op2(h2(e12),h2(e10)))|~h2(op1(e12,e11))=op2(h2(e12),h2(e11)))|~h2(op1(e12,e12))=op2(h2(e12),h2(e12)))|~h2(op1(e12,e13))=op2(h2(e12),h2(e13)))|~h2(op1(e13,e10))=op2(h2(e13),h2(e10)))|~h2(op1(e13,e11))=op2(h2(e13),h2(e11)))|~h2(op1(e13,e12))=op2(h2(e13),h2(e12)))|~h2(op1(e13,e13))=op2(h2(e13),h2(e13)))|sP3_prd)|sP4_prd)|sP5_prd)|(((~h2(e10)=e23&~h2(e11)=e23)&~h2(e12)=e23)&~h2(e13)=e23)))&(((((((((((((((((((~h3(op1(e10,e10))=op2(h3(e10),h3(e10))|~h3(op1(e10,e11))=op2(h3(e10),h3(e11)))|~h3(op1(e10,e12))=op2(h3(e10),h3(e12)))|~h3(op1(e10,e13))=op2(h3(e10),h3(e13)))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10)))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11)))|~h3(op1(e11,e12))=op2(h3(e11),h3(e12)))|~h3(op1(e11,e13))=op2(h3(e11),h3(e13)))|~h3(op1(e12,e10))=op2(h3(e12),h3(e10)))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11)))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12)))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13)))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10)))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11)))|~h3(op1(e13,e12))=op2(h3(e13),h3(e12)))|~h3(op1(e13,e13))=op2(h3(e13),h3(e13)))|sP6_prd)|sP7_prd)|sP8_prd)|(((~h3(e10)=e23&~h3(e11)=e23)&~h3(e12)=e23)&~h3(e13)=e23)))&(((((((((((((((((((~h4(op1(e10,e10))=op2(h4(e10),h4(e10))|~h4(op1(e10,e11))=op2(h4(e10),h4(e11)))|~h4(op1(e10,e12))=op2(h4(e10),h4(e12)))|~h4(op1(e10,e13))=op2(h4(e10),h4(e13)))|~h4(op1(e11,e10))=op2(h4(e11),h4(e10)))|~h4(op1(e11,e11))=op2(h4(e11),h4(e11)))|~h4(op1(e11,e12))=op2(h4(e11),h4(e12)))|~h4(op1(e11,e13))=op2(h4(e11),h4(e13)))|~h4(op1(e12,e10))=op2(h4(e12),h4(e10)))|~h4(op1(e12,e11))=op2(h4(e12),h4(e11)))|~h4(op1(e12,e12))=op2(h4(e12),h4(e12)))|~h4(op1(e12,e13))=op2(h4(e12),h4(e13)))|~h4(op1(e13,e10))=op2(h4(e13),h4(e10)))|~h4(op1(e13,e11))=op2(h4(e13),h4(e11)))|~h4(op1(e13,e12))=op2(h4(e13),h4(e12)))|~h4(op1(e13,e13))=op2(h4(e13),h4(e13)))|sP9_prd)|sP10_prd)|sP11_prd)|(((~h4(e10)=e23&~h4(e11)=e23)&~h4(e12)=e23)&~h4(e13)=e23))),
% 0.13/0.46 inference(formula_renaming,[status(thm)],[f446,f458,f457,f456,f455,f454,f453,f452,f451,f450,f449,f448,f447])).
% 0.13/0.46 fof(f471,plain,(
% 0.13/0.46 ~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(e13)=e23),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f459])).
% 0.13/0.46 fof(f512,plain,(
% 0.13/0.46 (~sP6_prd|(((~h3(e10)=e20&~h3(e11)=e20)&~h3(e12)=e20)&~h3(e13)=e20))&(sP6_prd|(((h3(e10)=e20|h3(e11)=e20)|h3(e12)=e20)|h3(e13)=e20))),
% 0.13/0.46 inference(NNF_transformation,[status(thm)],[f453])).
% 0.13/0.46 fof(f513,plain,(
% 0.13/0.46 ~sP6_prd|~h3(e10)=e20),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f512])).
% 0.13/0.46 fof(f518,plain,(
% 0.13/0.46 (~sP7_prd|(((~h3(e10)=e21&~h3(e11)=e21)&~h3(e12)=e21)&~h3(e13)=e21))&(sP7_prd|(((h3(e10)=e21|h3(e11)=e21)|h3(e12)=e21)|h3(e13)=e21))),
% 0.13/0.46 inference(NNF_transformation,[status(thm)],[f454])).
% 0.13/0.46 fof(f520,plain,(
% 0.13/0.46 ~sP7_prd|~h3(e11)=e21),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f518])).
% 0.13/0.46 fof(f524,plain,(
% 0.13/0.46 (~sP8_prd|(((~h3(e10)=e22&~h3(e11)=e22)&~h3(e12)=e22)&~h3(e13)=e22))&(sP8_prd|(((h3(e10)=e22|h3(e11)=e22)|h3(e12)=e22)|h3(e13)=e22))),
% 0.13/0.46 inference(NNF_transformation,[status(thm)],[f455])).
% 0.13/0.46 fof(f527,plain,(
% 0.13/0.46 ~sP8_prd|~h3(e12)=e22),
% 0.13/0.46 inference(cnf_transformation,[status(thm)],[f524])).
% 0.13/0.46 fof(f713,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f438,f471])).
% 0.13/0.46 fof(f717,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),h3(e13))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),h3(e12))|~h3(op1(e11,e13))=op2(h3(e11),h3(e13))|~h3(op1(e12,e10))=op2(h3(e12),h3(e10))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f438,f713])).
% 0.13/0.46 fof(f718,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),h3(e13))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),h3(e13))|~h3(op1(e12,e10))=op2(h3(e12),h3(e10))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f438,f717])).
% 0.13/0.46 fof(f719,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),h3(e13))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),h3(e13))|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(h3(e12),h3(e11))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f438,f718])).
% 0.13/0.46 fof(f720,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),h3(e13))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),h3(e13))|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(op1(e12,e12))=op2(h3(e12),h3(e12))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f438,f719])).
% 0.13/0.46 fof(f721,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),h3(e13))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),h3(e13))|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(op1(e12,e12))=op2(e22,h3(e12))|~h3(op1(e12,e13))=op2(h3(e12),h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f438,f720])).
% 0.13/0.46 fof(f722,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),h3(e13))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),h3(e13))|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(op1(e12,e12))=op2(e22,e22)|~h3(op1(e12,e13))=op2(h3(e12),h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f438,f721])).
% 0.13/0.46 fof(f723,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),h3(e13))|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),h3(e13))|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(op1(e12,e12))=op2(e22,e22)|~h3(op1(e12,e13))=op2(e22,h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f438,f722])).
% 0.13/0.46 fof(f787,plain,(
% 0.13/0.46 op1(e13,e13)=op1(e12,op1(e12,e13))),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f426,f91])).
% 0.13/0.46 fof(f788,plain,(
% 0.13/0.46 op1(op1(e12,e12),e12)=op1(e12,e13)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f426,f90])).
% 0.13/0.46 fof(f791,plain,(
% 0.13/0.46 op1(op1(e11,e12),e12)=op1(e11,e13)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f426,f74])).
% 0.13/0.46 fof(f792,plain,(
% 0.13/0.46 op1(op1(e10,e12),e12)=op1(e10,e13)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f426,f58])).
% 0.13/0.46 fof(f794,plain,(
% 0.13/0.46 op1(e13,e12)=op1(e12,e13)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f426,f788])).
% 0.13/0.46 fof(f952,plain,(
% 0.13/0.46 op2(op2(e21,e22),e22)=op2(e21,e23)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f429,f175])).
% 0.13/0.46 fof(f961,plain,(
% 0.13/0.46 ~sP8_prd|~e22=e22),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f438,f527])).
% 0.13/0.46 fof(f962,plain,(
% 0.13/0.46 ~sP8_prd),
% 0.13/0.46 inference(trivial_equality_resolution,[status(thm)],[f961])).
% 0.13/0.46 fof(f982,plain,(
% 0.13/0.46 op2(e23,e22)=op2(e22,op2(e22,e22))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f429,f191])).
% 0.13/0.46 fof(f983,plain,(
% 0.13/0.46 op2(op2(e21,e23),e22)=op2(e21,op2(e22,e23))),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f986,f179])).
% 0.13/0.46 fof(f986,plain,(
% 0.13/0.46 op2(e23,e22)=op2(e22,e23)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f429,f982])).
% 0.13/0.46 fof(f990,plain,(
% 0.13/0.46 op2(e23,e23)=op2(e22,op2(e22,e23))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f429,f192])).
% 0.13/0.46 fof(f994,plain,(
% 0.13/0.46 op2(op2(e22,e23),e22)=op2(e22,op2(e22,e23))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f986,f195])).
% 0.13/0.46 fof(f995,plain,(
% 0.13/0.46 op2(op2(e22,e23),e22)=op2(e23,e23)),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f990,f994])).
% 0.13/0.46 fof(f1018,plain,(
% 0.13/0.46 op2(op2(e22,e23),e21)=op2(e23,op2(e22,e21))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f986,f206])).
% 0.13/0.46 fof(f1019,plain,(
% 0.13/0.46 op2(e22,op2(e23,e21))=op2(e23,op2(e22,e21))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f194,f1018])).
% 0.13/0.46 fof(f1029,plain,(
% 0.13/0.46 op2(op2(e22,e23),e23)=op2(e23,op2(e22,e23))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f986,f208])).
% 0.13/0.46 fof(f1030,plain,(
% 0.13/0.46 op2(e22,op2(e23,e23))=op2(e23,op2(e22,e23))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f196,f1029])).
% 0.13/0.46 fof(f1034,plain,(
% 0.13/0.46 op2(op2(e23,e23),e22)=op2(e23,op2(e22,e23))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f986,f211])).
% 0.13/0.46 fof(f1035,plain,(
% 0.13/0.46 op2(op2(e23,e23),e22)=op2(e22,op2(e23,e23))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1030,f1034])).
% 0.13/0.46 fof(f1133,plain,(
% 0.13/0.46 h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f429,f441])).
% 0.13/0.46 fof(f1137,plain,(
% 0.13/0.46 op2(op2(e23,e23),e22)=op2(e22,h4(e13))),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f445,f1035])).
% 0.13/0.46 fof(f1138,plain,(
% 0.13/0.46 op2(h4(e13),e21)=op2(e23,op2(e23,e21))),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f445,f210])).
% 0.13/0.46 fof(f1140,plain,(
% 0.13/0.46 op2(e22,h4(e13))=op2(e23,op2(e22,e23))),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f445,f1030])).
% 0.13/0.46 fof(f1142,plain,(
% 0.13/0.46 op2(op2(e22,e23),e22)=h4(e13)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f445,f995])).
% 0.13/0.46 fof(f1143,plain,(
% 0.13/0.46 h4(e13)=op2(e22,op2(e22,e23))),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f445,f990])).
% 0.13/0.46 fof(f1148,plain,(
% 0.13/0.46 op2(h4(e13),e22)=op2(e22,h4(e13))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f445,f1137])).
% 0.13/0.46 fof(f1181,plain,(
% 0.13/0.46 op1(e10,e12)=e10|op1(e10,e12)=e11|op1(e10,e12)=e12),
% 0.13/0.46 inference(backward_subsumption_resolution,[status(thm)],[f34,f1182])).
% 0.13/0.46 fof(f1182,plain,(
% 0.13/0.46 ~op1(e10,e12)=e13),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f426,f303])).
% 0.13/0.46 fof(f1206,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),h3(e13))|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(op1(e12,e12))=op2(e22,e22)|~h3(op1(e12,e13))=op2(e22,h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1133,f723])).
% 0.13/0.46 fof(f1207,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(op1(e12,e12))=op2(e22,e22)|~h3(op1(e12,e13))=op2(e22,h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1133,f1206])).
% 0.13/0.46 fof(f1208,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e13)=op2(e22,e22)|~h3(op1(e12,e13))=op2(e22,h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f426,f1207])).
% 0.13/0.46 fof(f1209,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=op2(e22,e22)|~h3(op1(e12,e13))=op2(e22,h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1133,f1208])).
% 0.13/0.46 fof(f1210,plain,(
% 0.13/0.46 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,h3(e13))|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f429,f1209])).
% 0.13/0.47 fof(f1211,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(h3(e13),h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f1210])).
% 0.13/0.47 fof(f1212,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(h3(e13),h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f1211])).
% 0.13/0.47 fof(f1213,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(h3(e13),e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f1212])).
% 0.13/0.47 fof(f1214,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e23,e22)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f1213])).
% 0.13/0.47 fof(f1215,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=op2(h3(e13),h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f986,f1214])).
% 0.13/0.47 fof(f1216,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=op2(e23,h3(e13))|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f1215])).
% 0.13/0.47 fof(f1217,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=op2(e23,e23)|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f1216])).
% 0.13/0.47 fof(f1218,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd|sP8_prd|~h3(e13)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f445,f1217])).
% 0.13/0.47 fof(f1219,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd|sP8_prd|~e23=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f1218])).
% 0.13/0.47 fof(f1220,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~e23=e23|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd|sP8_prd),
% 0.13/0.47 inference(duplicate_literals_removal,[status(thm)],[f1219])).
% 0.13/0.47 fof(f1221,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd|sP8_prd),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f1220])).
% 0.13/0.47 fof(f1222,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(op1(e12,e13))=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1221,f962])).
% 0.13/0.47 fof(f1353,plain,(
% 0.13/0.47 op2(e22,e20)=e20|op2(e22,e20)=e21|op2(e22,e20)=e22),
% 0.13/0.47 inference(backward_subsumption_resolution,[status(thm)],[f141,f1354])).
% 0.13/0.47 fof(f1354,plain,(
% 0.13/0.47 ~op2(e22,e20)=e23),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f429,f375])).
% 0.13/0.47 fof(f1379,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(op1(e11,e12))=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1393,f1222])).
% 0.13/0.47 fof(f1386,plain,(
% 0.13/0.47 op1(op1(e13,e12),e13)=op1(e13,e11)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1393,f107])).
% 0.13/0.47 fof(f1388,plain,(
% 0.13/0.47 op1(e11,e12)=op1(e12,op1(e13,e12))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1393,f94])).
% 0.13/0.47 fof(f1391,plain,(
% 0.13/0.47 op1(op1(e11,e12),e13)=op1(e11,e11)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1393,f75])).
% 0.13/0.47 fof(f1392,plain,(
% 0.13/0.47 op1(op1(e10,e12),e13)=op1(e10,e11)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1393,f59])).
% 0.13/0.47 fof(f1393,plain,(
% 0.13/0.47 e11=op1(e12,e13)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f426,f425])).
% 0.13/0.47 fof(f1420,plain,(
% 0.13/0.47 e10=op1(op1(e12,e13),e12)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f426,f424])).
% 0.13/0.47 fof(f1423,plain,(
% 0.13/0.47 ~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),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1436,f1379])).
% 0.13/0.47 fof(f1429,plain,(
% 0.13/0.47 ~op1(e10,e12)=e10),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1436,f302])).
% 0.13/0.47 fof(f1430,plain,(
% 0.13/0.47 op1(op1(e13,e11),e12)=op1(e13,e10)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1436,f102])).
% 0.13/0.47 fof(f1431,plain,(
% 0.13/0.47 op1(op1(e12,e11),e12)=op1(e12,e10)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1436,f86])).
% 0.13/0.47 fof(f1432,plain,(
% 0.13/0.47 op1(e10,e11)=op1(e11,op1(e12,e11))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1436,f73])).
% 0.13/0.47 fof(f1436,plain,(
% 0.13/0.47 e10=op1(e11,e12)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1393,f1420])).
% 0.13/0.47 fof(f1437,plain,(
% 0.13/0.47 e20=op2(op2(e22,e23),e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f429,f427])).
% 0.13/0.47 fof(f1438,plain,(
% 0.13/0.47 e20=op2(e21,e22)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1454,f1437])).
% 0.13/0.47 fof(f1442,plain,(
% 0.13/0.47 ~op2(e22,e20)=e21),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1454,f376])).
% 0.13/0.47 fof(f1451,plain,(
% 0.13/0.47 op2(e23,e22)=e21),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1454,f986])).
% 0.13/0.47 fof(f1452,plain,(
% 0.13/0.47 op2(op2(e21,e22),e23)=op2(e21,e21)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1454,f176])).
% 0.13/0.47 fof(f1454,plain,(
% 0.13/0.47 e21=op2(e22,e23)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f429,f428])).
% 0.13/0.47 fof(f1456,plain,(
% 0.13/0.47 op2(op2(e21,e22),e23)=h2(e13)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f437,f1452])).
% 0.13/0.47 fof(f1465,plain,(
% 0.13/0.47 h3(e10)=op2(op2(e22,e23),e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f429,f439])).
% 0.13/0.47 fof(f1472,plain,(
% 0.13/0.47 op2(op2(e22,e21),e22)=op2(e22,h3(e10))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1477,f187])).
% 0.13/0.47 fof(f1473,plain,(
% 0.13/0.47 op2(h3(e10),e22)=op2(e21,e23)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1477,f952])).
% 0.13/0.47 fof(f1474,plain,(
% 0.13/0.47 op2(h3(e10),e21)=op2(e21,op2(e22,e21))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1477,f174])).
% 0.13/0.47 fof(f1475,plain,(
% 0.13/0.47 op2(h3(e10),e20)=op2(e21,op2(e22,e20))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1477,f173])).
% 0.13/0.47 fof(f1477,plain,(
% 0.13/0.47 h3(e10)=op2(e21,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1454,f1465])).
% 0.13/0.47 fof(f1478,plain,(
% 0.13/0.47 h3(e11)=op2(e22,e23)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f429,f440])).
% 0.13/0.47 fof(f1481,plain,(
% 0.13/0.47 ~sP7_prd|~e21=e21),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1483,f520])).
% 0.13/0.47 fof(f1483,plain,(
% 0.13/0.47 h3(e11)=e21),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1454,f1478])).
% 0.13/0.47 fof(f1485,plain,(
% 0.13/0.47 ~sP7_prd),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f1481])).
% 0.13/0.47 fof(f1506,plain,(
% 0.13/0.47 op1(op1(e12,e11),e12)=op1(e13,op1(e13,e12))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1512,f110])).
% 0.13/0.47 fof(f1512,plain,(
% 0.13/0.47 op1(e13,e13)=op1(e12,e11)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1393,f787])).
% 0.13/0.47 fof(f1520,plain,(
% 0.13/0.47 ~op1(e10,e12)=e11),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1525,f304])).
% 0.13/0.47 fof(f1525,plain,(
% 0.13/0.47 op1(e13,e12)=e11),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1393,f794])).
% 0.13/0.47 fof(f1534,plain,(
% 0.13/0.47 op1(op1(e12,e11),e13)=op1(e12,op1(e10,e12))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1539,f87])).
% 0.13/0.47 fof(f1535,plain,(
% 0.13/0.47 op1(op1(e10,e12),e11)=op1(e11,op1(e13,e11))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1539,f77])).
% 0.13/0.47 fof(f1539,plain,(
% 0.13/0.47 op1(e10,e12)=op1(e11,e13)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1436,f791])).
% 0.13/0.47 fof(f1540,plain,(
% 0.13/0.47 op1(e10,op1(e12,e11))=op1(e11,op1(e13,e11))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f57,f1535])).
% 0.13/0.47 fof(f1542,plain,(
% 0.13/0.47 op2(op2(e21,e23),e22)=op2(e21,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1454,f983])).
% 0.13/0.47 fof(f1543,plain,(
% 0.13/0.47 op2(op2(e21,e23),e22)=h2(e13)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f437,f1542])).
% 0.13/0.47 fof(f1560,plain,(
% 0.13/0.47 h3(e10)=e20),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1438,f1477])).
% 0.13/0.47 fof(f1563,plain,(
% 0.13/0.47 ~sP6_prd|~e20=e20),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1560,f513])).
% 0.13/0.47 fof(f1564,plain,(
% 0.13/0.47 ~sP6_prd),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f1563])).
% 0.13/0.47 fof(f1623,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=op2(e20,h3(e10))|~h3(op1(e10,e11))=op2(h3(e10),h3(e11))|~h3(op1(e10,e12))=op2(h3(e10),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1423])).
% 0.13/0.47 fof(f1624,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=op2(e20,e20)|~h3(op1(e10,e11))=op2(h3(e10),h3(e11))|~h3(op1(e10,e12))=op2(h3(e10),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1623])).
% 0.13/0.47 fof(f1625,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(h3(e10),h3(e11))|~h3(op1(e10,e12))=op2(h3(e10),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f433,f1624])).
% 0.13/0.47 fof(f1626,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,h3(e11))|~h3(op1(e10,e12))=op2(h3(e10),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1625])).
% 0.13/0.47 fof(f1627,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(h3(e10),e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1626])).
% 0.13/0.47 fof(f1628,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(h3(e10),e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1627])).
% 0.13/0.47 fof(f1629,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(h3(e11),h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1628])).
% 0.13/0.47 fof(f1630,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,h3(e10))|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1629])).
% 0.13/0.47 fof(f1631,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=op2(h3(e11),h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1630])).
% 0.13/0.47 fof(f1632,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=op2(e21,h3(e11))|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1631])).
% 0.13/0.47 fof(f1633,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=op2(e21,e21)|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1632])).
% 0.13/0.47 fof(f1634,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(e10)=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f437,f1633])).
% 0.13/0.47 fof(f1635,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=op2(h3(e11),e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1634])).
% 0.13/0.47 fof(f1636,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=op2(e21,e22)|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1635])).
% 0.13/0.47 fof(f1637,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e11,e13))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1438,f1636])).
% 0.13/0.47 fof(f1638,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(h3(e11),e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1539,f1637])).
% 0.13/0.47 fof(f1639,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,h3(e10))|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1638])).
% 0.13/0.47 fof(f1640,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,h3(e11))|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1639])).
% 0.13/0.47 fof(f1641,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1640])).
% 0.13/0.47 fof(f1642,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=op2(e22,e23)|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1641])).
% 0.13/0.47 fof(f1643,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=e21|~h3(op1(e13,e10))=op2(e23,h3(e10))|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1454,f1642])).
% 0.13/0.47 fof(f1644,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=e21|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,h3(e11))|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1643])).
% 0.13/0.47 fof(f1645,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=e21|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e13,e12))=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1644])).
% 0.13/0.47 fof(f1646,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=e21|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(e11)=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1525,f1645])).
% 0.13/0.47 fof(f1647,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=e21|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e21=op2(e22,e23)|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f1646])).
% 0.13/0.47 fof(f1648,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=e21|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e21=e21|~h3(op1(e13,e13))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1454,f1647])).
% 0.13/0.47 fof(f1649,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=e21|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~e21=e21|~h3(op1(e12,e11))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1512,f1648])).
% 0.13/0.47 fof(f1650,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~e20=e20|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~e21=e21|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(duplicate_literals_removal,[status(thm)],[f1649])).
% 0.13/0.47 fof(f1651,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=h4(e13)|sP6_prd|sP7_prd),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f1650])).
% 0.13/0.47 fof(f1652,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=h4(e13)|sP7_prd),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1651,f1564])).
% 0.13/0.47 fof(f1654,plain,(
% 0.13/0.47 op2(h4(e13),e22)=op2(e23,e21)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1655,f1148])).
% 0.13/0.47 fof(f1655,plain,(
% 0.13/0.47 op2(e22,h4(e13))=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1454,f1140])).
% 0.13/0.47 fof(f1658,plain,(
% 0.13/0.47 op2(e21,e22)=h4(e13)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1454,f1142])).
% 0.13/0.47 fof(f1660,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20|sP7_prd),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1677,f1652])).
% 0.13/0.47 fof(f1663,plain,(
% 0.13/0.47 op2(e20,e21)=op2(e23,op2(e23,e21))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1677,f1138])).
% 0.13/0.47 fof(f1677,plain,(
% 0.13/0.47 e20=h4(e13)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1438,f1658])).
% 0.13/0.47 fof(f1678,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e11,e10))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1660,f1485])).
% 0.13/0.47 fof(f1688,plain,(
% 0.13/0.47 e20=op2(e22,op2(e22,e23))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1677,f1143])).
% 0.13/0.47 fof(f1692,plain,(
% 0.13/0.47 ~op2(e22,e20)=e20),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1701,f374])).
% 0.13/0.47 fof(f1696,plain,(
% 0.13/0.47 op2(e22,op2(e23,e21))=op2(e23,e20)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1701,f1019])).
% 0.13/0.47 fof(f1701,plain,(
% 0.13/0.47 e20=op2(e22,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1454,f1688])).
% 0.13/0.47 fof(f1710,plain,(
% 0.13/0.47 op1(e10,e12)=e11|op1(e10,e12)=e12),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1181,f1429])).
% 0.13/0.47 fof(f1769,plain,(
% 0.13/0.47 op1(e10,e12)=e12),
% 0.13/0.47 inference(backward_subsumption_resolution,[status(thm)],[f1710,f1520])).
% 0.13/0.47 fof(f1771,plain,(
% 0.13/0.47 op2(e22,e20)=e20|op2(e22,e20)=e22),
% 0.13/0.47 inference(forward_subsumption_resolution,[status(thm)],[f1353,f1442])).
% 0.13/0.47 fof(f1788,plain,(
% 0.13/0.47 op1(e11,e13)=op1(e13,e11)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1525,f1386])).
% 0.13/0.47 fof(f1802,plain,(
% 0.13/0.47 op1(e10,e12)=op1(e13,e11)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1539,f1788])).
% 0.13/0.47 fof(f1814,plain,(
% 0.13/0.47 e10=op1(e12,op1(e13,e12))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1436,f1388])).
% 0.13/0.47 fof(f1828,plain,(
% 0.13/0.47 e10=op1(e12,e11)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1525,f1814])).
% 0.13/0.47 fof(f1840,plain,(
% 0.13/0.47 op1(e10,e13)=op1(e11,e11)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1436,f1391])).
% 0.13/0.47 fof(f1843,plain,(
% 0.13/0.47 op2(e22,e20)=e22),
% 0.13/0.47 inference(backward_subsumption_resolution,[status(thm)],[f1771,f1692])).
% 0.13/0.47 fof(f1863,plain,(
% 0.13/0.47 op1(op1(e10,e12),e12)=op1(e13,e10)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1802,f1430])).
% 0.13/0.47 fof(f1875,plain,(
% 0.13/0.47 op1(e10,e13)=op1(e13,e10)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f792,f1863])).
% 0.13/0.47 fof(f1885,plain,(
% 0.13/0.47 op1(e10,e12)=op1(e12,e10)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1828,f1431])).
% 0.13/0.47 fof(f1896,plain,(
% 0.13/0.47 op1(e10,e11)=op1(e11,e10)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1828,f1432])).
% 0.13/0.47 fof(f1897,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e11,e11))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1896,f1678])).
% 0.13/0.47 fof(f1898,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e12,e10))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1840,f1897])).
% 0.13/0.47 fof(f1899,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~h3(op1(e12,e11))=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1885,f1898])).
% 0.13/0.47 fof(f1900,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~h3(e10)=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1828,f1899])).
% 0.13/0.47 fof(f1901,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~e20=op2(e22,e21)|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1900])).
% 0.13/0.47 fof(f1902,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~e20=e20|~h3(op1(e13,e10))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1701,f1901])).
% 0.13/0.47 fof(f1903,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~e20=e20|~h3(op1(e10,e13))=op2(e23,e20)|~h3(op1(e13,e11))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1875,f1902])).
% 0.13/0.47 fof(f1904,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~e20=e20|~h3(op1(e10,e13))=op2(e23,e20)|~h3(op1(e10,e12))=op2(e23,e21)|~h3(op1(e12,e11))=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1802,f1903])).
% 0.13/0.47 fof(f1905,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~e20=e20|~h3(op1(e10,e13))=op2(e23,e20)|~h3(op1(e10,e12))=op2(e23,e21)|~h3(e10)=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1828,f1904])).
% 0.13/0.47 fof(f1906,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~e20=e20|~h3(op1(e10,e13))=op2(e23,e20)|~h3(op1(e10,e12))=op2(e23,e21)|~e20=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1905])).
% 0.13/0.47 fof(f1907,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~e20=e20|~h3(op1(e10,e13))=op2(e23,e20)|~h3(op1(e10,e12))=op2(e23,e21)),
% 0.13/0.47 inference(duplicate_literals_removal,[status(thm)],[f1906])).
% 0.13/0.47 fof(f1908,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~h3(op1(e10,e12))=op2(e23,e21)),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f1907])).
% 0.13/0.47 fof(f1935,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e12))=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~h3(e12)=op2(e23,e21)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1769,f1908])).
% 0.13/0.47 fof(f1938,plain,(
% 0.13/0.47 op1(e12,e13)=op1(e10,e11)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1769,f1392])).
% 0.13/0.47 fof(f1964,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~h3(e12)=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~h3(e12)=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1769,f1935])).
% 0.13/0.47 fof(f1965,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e12))=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~h3(e12)=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f438,f1964])).
% 0.13/0.47 fof(f1966,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~h3(e12)=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~h3(e12)=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1769,f1965])).
% 0.13/0.47 fof(f1967,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~e22=op2(e21,e23)|~h3(op1(e10,e12))=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~h3(e12)=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f438,f1966])).
% 0.13/0.47 fof(f1968,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~e22=op2(e21,e23)|~h3(e12)=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~h3(e12)=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1769,f1967])).
% 0.13/0.47 fof(f1969,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~e22=op2(e21,e23)|~e22=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~h3(e12)=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f438,f1968])).
% 0.13/0.47 fof(f1970,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=op2(e20,e23)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~e22=op2(e21,e23)|~e22=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f438,f1969])).
% 0.13/0.47 fof(f1971,plain,(
% 0.13/0.47 e11=op1(e10,e11)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1393,f1938])).
% 0.13/0.47 fof(f1991,plain,(
% 0.13/0.47 op2(e20,e23)=h2(e13)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1438,f1456])).
% 0.13/0.47 fof(f2003,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e11))=op2(e21,e20)|~h3(op1(e10,e13))=h2(e13)|~e22=op2(e21,e23)|~e22=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1991,f1970])).
% 0.13/0.47 fof(f2004,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e11))=op2(e21,e20)|~e22=op2(e21,e23)|~e22=op2(e22,e20)|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(duplicate_literals_removal,[status(thm)],[f2003])).
% 0.13/0.47 fof(f2041,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e11))=op2(e21,e20)|~e22=op2(e21,e23)|~e22=e22|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f1843,f2004])).
% 0.13/0.47 fof(f2053,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=h1(e13)|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e11))=op2(e21,e20)|~e22=op2(e21,e23)|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f2041])).
% 0.13/0.47 fof(f2058,plain,(
% 0.13/0.47 op2(e20,e22)=op2(e22,h3(e10))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1701,f1472])).
% 0.13/0.47 fof(f2059,plain,(
% 0.13/0.47 op2(e20,e22)=op2(e22,e20)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f2058])).
% 0.13/0.47 fof(f2069,plain,(
% 0.13/0.47 op2(e20,e22)=e22),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1843,f2059])).
% 0.13/0.47 fof(f2074,plain,(
% 0.13/0.47 op2(e20,e22)=op2(e21,e23)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1473])).
% 0.13/0.47 fof(f2079,plain,(
% 0.13/0.47 op2(e22,e22)=h2(e13)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f2086,f1543])).
% 0.13/0.47 fof(f2086,plain,(
% 0.13/0.47 e22=op2(e21,e23)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2069,f2074])).
% 0.13/0.47 fof(f2089,plain,(
% 0.13/0.47 e23=h2(e13)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f429,f2079])).
% 0.13/0.47 fof(f2094,plain,(
% 0.13/0.47 op2(e20,e21)=op2(e21,op2(e22,e21))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1474])).
% 0.13/0.47 fof(f2106,plain,(
% 0.13/0.47 op2(e20,e21)=op2(e21,e20)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1701,f2094])).
% 0.13/0.47 fof(f2109,plain,(
% 0.13/0.47 op2(e20,e20)=op2(e21,op2(e22,e20))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f1475])).
% 0.13/0.47 fof(f2110,plain,(
% 0.13/0.47 h1(e13)=op2(e21,op2(e22,e20))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f433,f2109])).
% 0.13/0.47 fof(f2111,plain,(
% 0.13/0.47 h1(e13)=op2(e21,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1843,f2110])).
% 0.13/0.47 fof(f2125,plain,(
% 0.13/0.47 h1(e13)=e20),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1438,f2111])).
% 0.13/0.47 fof(f2232,plain,(
% 0.13/0.47 op1(e10,e12)=op1(e13,op1(e13,e12))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1828,f1506])).
% 0.13/0.47 fof(f2233,plain,(
% 0.13/0.47 e12=op1(e13,op1(e13,e12))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1769,f2232])).
% 0.13/0.47 fof(f2234,plain,(
% 0.13/0.47 e12=op1(e13,e11)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1525,f2233])).
% 0.13/0.47 fof(f2318,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e20,e22)|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e11))=op2(e21,e20)|~e22=op2(e21,e23)|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2125,f2053])).
% 0.13/0.47 fof(f2319,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e22=e22|~h3(op1(e10,e13))=h2(e13)|~h3(op1(e10,e11))=op2(e21,e20)|~e22=op2(e21,e23)|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2069,f2318])).
% 0.13/0.47 fof(f2320,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e22=e22|~h3(op1(e10,e13))=e23|~h3(op1(e10,e11))=op2(e21,e20)|~e22=op2(e21,e23)|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2089,f2319])).
% 0.13/0.47 fof(f2321,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e22=e22|~h3(op1(e10,e13))=e23|~h3(op1(e10,e11))=op2(e20,e21)|~e22=op2(e21,e23)|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2106,f2320])).
% 0.13/0.47 fof(f2322,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e22=e22|~h3(op1(e10,e13))=e23|~h3(op1(e10,e11))=op2(e20,e21)|~e22=e22|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2086,f2321])).
% 0.13/0.47 fof(f2323,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e22=e22|~h3(op1(e10,e13))=e23|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(duplicate_literals_removal,[status(thm)],[f2322])).
% 0.13/0.47 fof(f2324,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e13))=e23|~h3(op1(e10,e13))=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f2323])).
% 0.13/0.47 fof(f2325,plain,(
% 0.13/0.47 op1(e10,e13)=op1(e12,op1(e10,e12))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1828,f1534])).
% 0.13/0.47 fof(f2326,plain,(
% 0.13/0.47 op1(e10,e13)=op1(e12,e12)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1769,f2325])).
% 0.13/0.47 fof(f2327,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~h3(op1(e10,e13))=e23|~h3(e13)=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f2344,f2324])).
% 0.13/0.47 fof(f2344,plain,(
% 0.13/0.47 op1(e10,e13)=e13),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f426,f2326])).
% 0.13/0.47 fof(f2345,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~h3(e13)=e23|~h3(e13)=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2344,f2327])).
% 0.13/0.47 fof(f2346,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e23=e23|~h3(e13)=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f2345])).
% 0.13/0.47 fof(f2347,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e23=e23|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1133,f2346])).
% 0.13/0.47 fof(f2348,plain,(
% 0.13/0.47 ~h3(op1(e10,e10))=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f2347])).
% 0.13/0.47 fof(f2364,plain,(
% 0.13/0.47 op1(e10,e10)=op1(e11,op1(e13,e11))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1828,f1540])).
% 0.13/0.47 fof(f2365,plain,(
% 0.13/0.47 op1(e10,e10)=op1(e11,e12)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2234,f2364])).
% 0.13/0.47 fof(f2371,plain,(
% 0.13/0.47 op1(e10,e10)=e10),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1436,f2365])).
% 0.13/0.47 fof(f2398,plain,(
% 0.13/0.47 op2(e20,e22)=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1677,f1654])).
% 0.13/0.47 fof(f2405,plain,(
% 0.13/0.47 e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2069,f2398])).
% 0.13/0.47 fof(f2467,plain,(
% 0.13/0.47 op2(e20,e21)=op2(e23,e22)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2405,f1663])).
% 0.13/0.47 fof(f2472,plain,(
% 0.13/0.47 op2(e20,e21)=e21),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1451,f2467])).
% 0.13/0.47 fof(f2487,plain,(
% 0.13/0.47 op2(e22,e22)=op2(e23,e20)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2405,f1696])).
% 0.13/0.47 fof(f2489,plain,(
% 0.13/0.47 e23=op2(e23,e20)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f429,f2487])).
% 0.13/0.47 fof(f2572,plain,(
% 0.13/0.47 ~h3(e10)=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2371,f2348])).
% 0.13/0.47 fof(f2573,plain,(
% 0.13/0.47 ~e20=e20|~h3(op1(e10,e11))=op2(e20,e21)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1560,f2572])).
% 0.13/0.47 fof(f2574,plain,(
% 0.13/0.47 ~e20=e20|~h3(e11)=op2(e20,e21)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1971,f2573])).
% 0.13/0.47 fof(f2575,plain,(
% 0.13/0.47 ~e20=e20|~e21=op2(e20,e21)|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f1483,f2574])).
% 0.13/0.47 fof(f2576,plain,(
% 0.13/0.47 ~e20=e20|~e21=e21|~e23=op2(e23,e20)|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2472,f2575])).
% 0.13/0.47 fof(f2577,plain,(
% 0.13/0.47 ~e20=e20|~e21=e21|~e23=e23|~e22=op2(e23,e21)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2489,f2576])).
% 0.13/0.47 fof(f2578,plain,(
% 0.13/0.47 ~e20=e20|~e21=e21|~e23=e23|~e22=e22),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f2405,f2577])).
% 0.13/0.47 fof(f2579,plain,(
% 0.13/0.47 $false),
% 0.13/0.47 inference(trivial_equality_resolution,[status(thm)],[f2578])).
% 0.13/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.52 % Elapsed time: 0.150188 seconds
% 0.13/0.52 % CPU time: 0.544225 seconds
% 0.13/0.52 % Total memory used: 102.762 MB
% 0.13/0.52 % Net memory used: 102.500 MB
%------------------------------------------------------------------------------