%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ALG119+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 12:53:30 PM UTC 2026
% Result : Theorem 6.94s 1.73s
% Output : CNFRefutation 6.94s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f167ERROR: Could not build tree for root c_13749ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 )
& ( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 )
& ( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 )
& ( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 )
& ( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 )
& ( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 )
& ( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 )
& ( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 )
& ( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 )
& ( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 )
& ( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 )
& ( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 )
& ( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 )
& ( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 )
& ( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 )
& ( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 )
& ( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 )
& ( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 )
& ( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 )
& ( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 )
& ( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 )
& ( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 )
& ( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 )
& ( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 )
& ( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 )
& ( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 )
& ( op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 )
& ( op2(e22,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e22) = e21
| op2(e22,e22) = e20 )
& ( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 )
& ( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 )
& ( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 )
& ( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 )
& ( op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e21) = e20 )
& ( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 )
& ( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| op2(e20,e20) = e20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 )
& ( op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| op2(e23,e20) = e23 )
& ( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 )
& ( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 )
& ( op2(e23,e23) = e21
| op2(e22,e23) = e21
| op2(e21,e23) = e21
| op2(e20,e23) = e21 )
& ( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 )
& ( op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 )
& ( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 )
& ( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 )
& ( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 )
& ( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 )
& ( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 )
& ( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 )
& ( op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 )
& ( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 )
& ( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 )
& ( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 )
& ( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 )
& ( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 )
& ( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 )
& ( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 )
& ( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 )
& ( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 )
& ( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 )
& ( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| op2(e20,e20) = e21 )
& ( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 )
& ( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 )
& ( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e11)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e11)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e11)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e11)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e11,e13)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e11,e12)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e11,e11)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e11,e10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e21)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e21)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e21)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e21)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e21,e23)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e21,e22)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e21,e21)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e21,e20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f12,axiom,
( e12 = op1(e13,e13)
& e11 = op1(e13,op1(e13,e13))
& e10 = op1(op1(e13,e13),op1(e13,op1(e13,e13))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e22 = op2(e23,e23)
& e21 = op2(e23,op2(e23,e23))
& e20 = op2(op2(e23,e23),op2(e23,op2(e23,e23))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e12) = op2(e20,e20)
& h1(e11) = op2(e20,op2(e20,e20))
& h1(e10) = op2(op2(e20,e20),op2(e20,op2(e20,e20)))
& h1(e13) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e12) = op2(e21,e21)
& h2(e11) = op2(e21,op2(e21,e21))
& h2(e10) = op2(op2(e21,e21),op2(e21,op2(e21,e21)))
& h2(e13) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h3(e12) = op2(e22,e22)
& h3(e11) = op2(e22,op2(e22,e22))
& h3(e10) = op2(op2(e22,e22),op2(e22,op2(e22,e22)))
& h3(e13) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f168,plain,
( ~ sP65
| ( op1(e13,e11) != e13
& op1(e12,e11) != e12
& op1(e11,e11) != e11
& op1(e10,e11) != e10 ) ),
inference(nnf_transformation,[],[f86]) ).
fof(f169,plain,
( ~ sP64
| ( op1(e13,e12) != e13
& op1(e12,e12) != e12
& op1(e11,e12) != e11
& op1(e10,e12) != e10 ) ),
inference(nnf_transformation,[],[f85]) ).
fof(f170,plain,
( ~ sP63
| ( op1(e13,e13) != e13
& op1(e12,e13) != e12
& op1(e11,e13) != e11
& op1(e10,e13) != e10 ) ),
inference(nnf_transformation,[],[f84]) ).
fof(f234,plain,
( ~ sP131
| ( op2(e23,e21) != e23
& op2(e22,e21) != e22
& op2(e21,e21) != e21
& op2(e20,e21) != e20 ) ),
inference(nnf_transformation,[],[f153]) ).
fof(f235,plain,
( ~ sP130
| ( op2(e23,e22) != e23
& op2(e22,e22) != e22
& op2(e21,e22) != e21
& op2(e20,e22) != e20 ) ),
inference(nnf_transformation,[],[f152]) ).
fof(f236,plain,
( ~ sP129
| ( op2(e23,e23) != e23
& op2(e22,e23) != e22
& op2(e21,e23) != e21
& op2(e20,e23) != e20 ) ),
inference(nnf_transformation,[],[f151]) ).
fof(f300,plain,
( ~ sP143
| ( e21 != h1(e13)
& e21 != h1(e12)
& e21 != h1(e11)
& e21 != h1(e10) ) ),
inference(nnf_transformation,[],[f166]) ).
fof(f301,plain,
( ~ sP142
| ( e22 != h1(e13)
& e22 != h1(e12)
& e22 != h1(e11)
& e22 != h1(e10) ) ),
inference(nnf_transformation,[],[f165]) ).
fof(f302,plain,
( ~ sP141
| ( e23 != h1(e13)
& e23 != h1(e12)
& e23 != h1(e11)
& e23 != h1(e10) ) ),
inference(nnf_transformation,[],[f164]) ).
fof(f312,plain,
( e13 = op1(e13,e13)
| e12 = op1(e13,e13)
| e11 = op1(e13,e13)
| e10 = op1(e13,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f316,plain,
( e13 = op1(e12,e13)
| e12 = op1(e12,e13)
| e11 = op1(e12,e13)
| e10 = op1(e12,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f317,plain,
( e13 = op1(e12,e12)
| e12 = op1(e12,e12)
| e11 = op1(e12,e12)
| e10 = op1(e12,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f320,plain,
( e13 = op1(e11,e13)
| e12 = op1(e11,e13)
| e11 = op1(e11,e13)
| e10 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f321,plain,
( e13 = op1(e11,e12)
| e12 = op1(e11,e12)
| e11 = op1(e11,e12)
| e10 = op1(e11,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f322,plain,
( e13 = op1(e11,e11)
| e12 = op1(e11,e11)
| e11 = op1(e11,e11)
| e10 = op1(e11,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f323,plain,
( e13 = op1(e11,e10)
| e12 = op1(e11,e10)
| e11 = op1(e11,e10)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f327,plain,
( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f329,plain,
( e13 = op1(e13,e13)
| e13 = op1(e13,e12)
| e13 = op1(e13,e11)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f332,plain,
( e11 = op1(e13,e13)
| e11 = op1(e12,e13)
| e11 = op1(e11,e13)
| e11 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f334,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e13)
| e10 = op1(e11,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f335,plain,
( e10 = op1(e13,e13)
| e10 = op1(e13,e12)
| e10 = op1(e13,e11)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f336,plain,
( e13 = op1(e13,e12)
| e13 = op1(e12,e12)
| e13 = op1(e11,e12)
| e13 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f339,plain,
( e12 = op1(e12,e13)
| e12 = op1(e12,e12)
| e12 = op1(e12,e11)
| e12 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f341,plain,
( e11 = op1(e12,e13)
| e11 = op1(e12,e12)
| e11 = op1(e12,e11)
| e11 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f342,plain,
( e10 = op1(e13,e12)
| e10 = op1(e12,e12)
| e10 = op1(e11,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f345,plain,
( e13 = op1(e11,e13)
| e13 = op1(e11,e12)
| e13 = op1(e11,e11)
| e13 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f346,plain,
( e12 = op1(e13,e11)
| e12 = op1(e12,e11)
| e12 = op1(e11,e11)
| e12 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f351,plain,
( e10 = op1(e11,e13)
| e10 = op1(e11,e12)
| e10 = op1(e11,e11)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f352,plain,
( e13 = op1(e13,e10)
| e13 = op1(e12,e10)
| e13 = op1(e11,e10)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f353,plain,
( e13 = op1(e10,e13)
| e13 = op1(e10,e12)
| e13 = op1(e10,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f2]) ).
fof(f357,plain,
( e11 = op1(e10,e13)
| e11 = op1(e10,e12)
| e11 = op1(e10,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f2]) ).
fof(f360,plain,
( e23 = op2(e23,e23)
| e22 = op2(e23,e23)
| e21 = op2(e23,e23)
| e20 = op2(e23,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f364,plain,
( e23 = op2(e22,e23)
| e22 = op2(e22,e23)
| e21 = op2(e22,e23)
| e20 = op2(e22,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f365,plain,
( e23 = op2(e22,e22)
| e22 = op2(e22,e22)
| e21 = op2(e22,e22)
| e20 = op2(e22,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f367,plain,
( e23 = op2(e22,e20)
| e22 = op2(e22,e20)
| e21 = op2(e22,e20)
| e20 = op2(e22,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f369,plain,
( e23 = op2(e21,e22)
| e22 = op2(e21,e22)
| e21 = op2(e21,e22)
| e20 = op2(e21,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f370,plain,
( e23 = op2(e21,e21)
| e22 = op2(e21,e21)
| e21 = op2(e21,e21)
| e20 = op2(e21,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f372,plain,
( e23 = op2(e20,e23)
| e22 = op2(e20,e23)
| e21 = op2(e20,e23)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f375,plain,
( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f377,plain,
( e23 = op2(e23,e23)
| e23 = op2(e23,e22)
| e23 = op2(e23,e21)
| e23 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f380,plain,
( e21 = op2(e23,e23)
| e21 = op2(e22,e23)
| e21 = op2(e21,e23)
| e21 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f382,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e23)
| e20 = op2(e21,e23)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f383,plain,
( e20 = op2(e23,e23)
| e20 = op2(e23,e22)
| e20 = op2(e23,e21)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f384,plain,
( e23 = op2(e23,e22)
| e23 = op2(e22,e22)
| e23 = op2(e21,e22)
| e23 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f385,plain,
( e23 = op2(e22,e23)
| e23 = op2(e22,e22)
| e23 = op2(e22,e21)
| e23 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f387,plain,
( e22 = op2(e22,e23)
| e22 = op2(e22,e22)
| e22 = op2(e22,e21)
| e22 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f389,plain,
( e21 = op2(e22,e23)
| e21 = op2(e22,e22)
| e21 = op2(e22,e21)
| e21 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f394,plain,
( e22 = op2(e23,e21)
| e22 = op2(e22,e21)
| e22 = op2(e21,e21)
| e22 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f395,plain,
( e22 = op2(e21,e23)
| e22 = op2(e21,e22)
| e22 = op2(e21,e21)
| e22 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f396,plain,
( e21 = op2(e23,e21)
| e21 = op2(e22,e21)
| e21 = op2(e21,e21)
| e21 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f400,plain,
( e23 = op2(e23,e20)
| e23 = op2(e22,e20)
| e23 = op2(e21,e20)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f4]) ).
fof(f401,plain,
( e23 = op2(e20,e23)
| e23 = op2(e20,e22)
| e23 = op2(e20,e21)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f4]) ).
fof(f402,plain,
( e22 = op2(e23,e20)
| e22 = op2(e22,e20)
| e22 = op2(e21,e20)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f403,plain,
( e22 = op2(e20,e23)
| e22 = op2(e20,e22)
| e22 = op2(e20,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f404,plain,
( e21 = op2(e23,e20)
| e21 = op2(e22,e20)
| e21 = op2(e21,e20)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f4]) ).
fof(f405,plain,
( e21 = op2(e20,e23)
| e21 = op2(e20,e22)
| e21 = op2(e20,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f4]) ).
fof(f407,plain,
( e20 = op2(e20,e23)
| e20 = op2(e20,e22)
| e20 = op2(e20,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f414,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f415,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f416,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f420,plain,
op1(e11,e12) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f421,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f423,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f424,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f425,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f429,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f430,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f432,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f433,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f438,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f439,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f440,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f441,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f443,plain,
op1(e10,e12) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f444,plain,
op1(e12,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f445,plain,
op1(e11,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f446,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f447,plain,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f449,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f451,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f452,plain,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f453,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f455,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f462,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f463,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f464,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f465,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f466,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f467,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f472,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f474,plain,
op2(e20,e22) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f475,plain,
op2(e20,e21) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f477,plain,
op2(e20,e20) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f478,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f479,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f480,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f481,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f483,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f486,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f487,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f488,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f489,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f490,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f492,plain,
op2(e22,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f493,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f494,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f495,plain,
op2(e20,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f496,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f497,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f501,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f502,plain,
op2(e20,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f503,plain,
op2(e20,e20) != op2(e21,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f504,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f505,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f506,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f507,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f508,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f509,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f510,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f511,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f512,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f513,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f514,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f515,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f532,plain,
( ~ sP65
| e13 != op1(e13,e11) ),
inference(cnf_transformation,[],[f168]) ).
fof(f537,plain,
( ~ sP64
| e12 != op1(e12,e12) ),
inference(cnf_transformation,[],[f169]) ).
fof(f543,plain,
( ~ sP63
| e10 != op1(e10,e13) ),
inference(cnf_transformation,[],[f170]) ).
fof(f801,plain,
( e13 = op1(e12,op1(e12,e13))
| e12 = op1(e12,op1(e12,e12))
| e11 = op1(e12,op1(e12,e11))
| e10 = op1(e12,op1(e12,e10)) ),
inference(cnf_transformation,[],[f87]) ).
fof(f802,plain,
( e13 = op1(e11,op1(e11,e13))
| e12 = op1(e11,op1(e11,e12))
| e11 = op1(e11,op1(e11,e11))
| e10 = op1(e11,op1(e11,e10)) ),
inference(cnf_transformation,[],[f87]) ).
fof(f803,plain,
( e13 = op1(e10,op1(e10,e13))
| e12 = op1(e10,op1(e10,e12))
| e11 = op1(e10,op1(e10,e11))
| e10 = op1(e10,op1(e10,e10)) ),
inference(cnf_transformation,[],[f87]) ).
fof(f806,plain,
( sP63
| sP64
| sP65
| e11 != op1(e11,e10) ),
inference(cnf_transformation,[],[f87]) ).
fof(f808,plain,
( ~ sP131
| e23 != op2(e23,e21) ),
inference(cnf_transformation,[],[f234]) ).
fof(f813,plain,
( ~ sP130
| e22 != op2(e22,e22) ),
inference(cnf_transformation,[],[f235]) ).
fof(f819,plain,
( ~ sP129
| e20 != op2(e20,e23) ),
inference(cnf_transformation,[],[f236]) ).
fof(f1077,plain,
( e23 = op2(e22,op2(e22,e23))
| e22 = op2(e22,op2(e22,e22))
| e21 = op2(e22,op2(e22,e21))
| e20 = op2(e22,op2(e22,e20)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f1078,plain,
( e23 = op2(e21,op2(e21,e23))
| e22 = op2(e21,op2(e21,e22))
| e21 = op2(e21,op2(e21,e21))
| e20 = op2(e21,op2(e21,e20)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f1079,plain,
( e23 = op2(e20,op2(e20,e23))
| e22 = op2(e20,op2(e20,e22))
| e21 = op2(e20,op2(e20,e21))
| e20 = op2(e20,op2(e20,e20)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f1082,plain,
( sP129
| sP130
| sP131
| e21 != op2(e21,e20) ),
inference(cnf_transformation,[],[f154]) ).
fof(f1084,plain,
e12 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f1085,plain,
e11 = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f1086,plain,
e10 = op1(op1(e13,e13),op1(e13,op1(e13,e13))),
inference(cnf_transformation,[],[f12]) ).
fof(f1087,plain,
e22 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f1088,plain,
e21 = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f1089,plain,
e20 = op2(op2(e23,e23),op2(e23,op2(e23,e23))),
inference(cnf_transformation,[],[f13]) ).
fof(f1090,plain,
op2(e20,e20) = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f1091,plain,
op2(e20,op2(e20,e20)) = h1(e11),
inference(cnf_transformation,[],[f14]) ).
fof(f1092,plain,
h1(e10) = op2(op2(e20,e20),op2(e20,op2(e20,e20))),
inference(cnf_transformation,[],[f14]) ).
fof(f1093,plain,
e20 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f1094,plain,
op2(e21,e21) = h2(e12),
inference(cnf_transformation,[],[f15]) ).
fof(f1095,plain,
op2(e21,op2(e21,e21)) = h2(e11),
inference(cnf_transformation,[],[f15]) ).
fof(f1098,plain,
op2(e22,e22) = h3(e12),
inference(cnf_transformation,[],[f16]) ).
fof(f1099,plain,
op2(e22,op2(e22,e22)) = h3(e11),
inference(cnf_transformation,[],[f16]) ).
fof(f1107,plain,
( ~ sP143
| e21 != h1(e12) ),
inference(cnf_transformation,[],[f300]) ).
fof(f1112,plain,
( ~ sP142
| e22 != h1(e11) ),
inference(cnf_transformation,[],[f301]) ).
fof(f1117,plain,
( ~ sP141
| e23 != h1(e10) ),
inference(cnf_transformation,[],[f302]) ).
fof(f1166,plain,
( sP141
| sP142
| sP143
| e20 != h1(e13)
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(cnf_transformation,[],[f167]) ).
fof(f1169,plain,
( sP141
| sP142
| sP143
| e20 != h1(e10)
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_49,plain,
( ( op1(e10,e10) = e13 )
| ( op1(e10,e10) = e12 )
| ( op1(e10,e10) = e11 )
| ( op1(e10,e10) = e10 ) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_53,plain,
( ( op1(e11,e10) = e13 )
| ( op1(e11,e10) = e12 )
| ( op1(e11,e10) = e11 )
| ( op1(e11,e10) = e10 ) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_54,plain,
( ( op1(e11,e11) = e13 )
| ( op1(e11,e11) = e12 )
| ( op1(e11,e11) = e11 )
| ( op1(e11,e11) = e10 ) ),
inference(cnf_transformation,[],[f322]) ).
tcf(c_55,plain,
( ( op1(e11,e12) = e13 )
| ( op1(e11,e12) = e12 )
| ( op1(e11,e12) = e11 )
| ( op1(e11,e12) = e10 ) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_56,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e13) = e12 )
| ( op1(e11,e13) = e11 )
| ( op1(e11,e13) = e10 ) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_59,plain,
( ( op1(e12,e12) = e13 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e12) = e11 )
| ( op1(e12,e12) = e10 ) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_60,plain,
( ( op1(e12,e13) = e13 )
| ( op1(e12,e13) = e12 )
| ( op1(e12,e13) = e11 )
| ( op1(e12,e13) = e10 ) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_64,plain,
( ( op1(e13,e13) = e13 )
| ( op1(e13,e13) = e12 )
| ( op1(e13,e13) = e11 )
| ( op1(e13,e13) = e10 ) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_67,plain,
( ( op1(e10,e13) = e11 )
| ( op1(e10,e12) = e11 )
| ( op1(e10,e11) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(cnf_transformation,[],[f357]) ).
tcf(c_71,plain,
( ( op1(e10,e13) = e13 )
| ( op1(e10,e12) = e13 )
| ( op1(e10,e11) = e13 )
| ( op1(e10,e10) = e13 ) ),
inference(cnf_transformation,[],[f353]) ).
tcf(c_72,plain,
( ( op1(e13,e10) = e13 )
| ( op1(e12,e10) = e13 )
| ( op1(e11,e10) = e13 )
| ( op1(e10,e10) = e13 ) ),
inference(cnf_transformation,[],[f352]) ).
tcf(c_73,plain,
( ( op1(e11,e13) = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e11,e10) = e10 ) ),
inference(cnf_transformation,[],[f351]) ).
tcf(c_78,plain,
( ( op1(e13,e11) = e12 )
| ( op1(e12,e11) = e12 )
| ( op1(e11,e11) = e12 )
| ( op1(e10,e11) = e12 ) ),
inference(cnf_transformation,[],[f346]) ).
tcf(c_79,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e12) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e11,e10) = e13 ) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_82,plain,
( ( op1(e13,e12) = e10 )
| ( op1(e12,e12) = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e10,e12) = e10 ) ),
inference(cnf_transformation,[],[f342]) ).
tcf(c_83,plain,
( ( op1(e12,e13) = e11 )
| ( op1(e12,e12) = e11 )
| ( op1(e12,e11) = e11 )
| ( op1(e12,e10) = e11 ) ),
inference(cnf_transformation,[],[f341]) ).
tcf(c_85,plain,
( ( op1(e12,e13) = e12 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e11) = e12 )
| ( op1(e12,e10) = e12 ) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_88,plain,
( ( op1(e13,e12) = e13 )
| ( op1(e12,e12) = e13 )
| ( op1(e11,e12) = e13 )
| ( op1(e10,e12) = e13 ) ),
inference(cnf_transformation,[],[f336]) ).
tcf(c_89,plain,
( ( op1(e13,e13) = e10 )
| ( op1(e13,e12) = e10 )
| ( op1(e13,e11) = e10 )
| ( op1(e13,e10) = e10 ) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_90,plain,
( ( op1(e13,e13) = e10 )
| ( op1(e12,e13) = e10 )
| ( op1(e11,e13) = e10 )
| ( op1(e10,e13) = e10 ) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_92,plain,
( ( op1(e13,e13) = e11 )
| ( op1(e12,e13) = e11 )
| ( op1(e11,e13) = e11 )
| ( op1(e10,e13) = e11 ) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_95,plain,
( ( op1(e13,e13) = e13 )
| ( op1(e13,e12) = e13 )
| ( op1(e13,e11) = e13 )
| ( op1(e13,e10) = e13 ) ),
inference(cnf_transformation,[],[f329]) ).
tcf(c_97,plain,
( ( op2(e20,e20) = e23 )
| ( op2(e20,e20) = e22 )
| ( op2(e20,e20) = e21 )
| ( op2(e20,e20) = e20 ) ),
inference(cnf_transformation,[],[f375]) ).
tcf(c_100,plain,
( ( op2(e20,e23) = e23 )
| ( op2(e20,e23) = e22 )
| ( op2(e20,e23) = e21 )
| ( op2(e20,e23) = e20 ) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_102,plain,
( ( op2(e21,e21) = e23 )
| ( op2(e21,e21) = e22 )
| ( op2(e21,e21) = e21 )
| ( op2(e21,e21) = e20 ) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_103,plain,
( ( op2(e21,e22) = e23 )
| ( op2(e21,e22) = e22 )
| ( op2(e21,e22) = e21 )
| ( op2(e21,e22) = e20 ) ),
inference(cnf_transformation,[],[f369]) ).
tcf(c_105,plain,
( ( op2(e22,e20) = e23 )
| ( op2(e22,e20) = e22 )
| ( op2(e22,e20) = e21 )
| ( op2(e22,e20) = e20 ) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_107,plain,
( ( op2(e22,e22) = e23 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e22) = e21 )
| ( op2(e22,e22) = e20 ) ),
inference(cnf_transformation,[],[f365]) ).
tcf(c_108,plain,
( ( op2(e22,e23) = e23 )
| ( op2(e22,e23) = e22 )
| ( op2(e22,e23) = e21 )
| ( op2(e22,e23) = e20 ) ),
inference(cnf_transformation,[],[f364]) ).
tcf(c_112,plain,
( ( op2(e23,e23) = e23 )
| ( op2(e23,e23) = e22 )
| ( op2(e23,e23) = e21 )
| ( op2(e23,e23) = e20 ) ),
inference(cnf_transformation,[],[f360]) ).
tcf(c_113,plain,
( ( op2(e20,e23) = e20 )
| ( op2(e20,e22) = e20 )
| ( op2(e20,e21) = e20 )
| ( op2(e20,e20) = e20 ) ),
inference(cnf_transformation,[],[f407]) ).
tcf(c_115,plain,
( ( op2(e20,e23) = e21 )
| ( op2(e20,e22) = e21 )
| ( op2(e20,e21) = e21 )
| ( op2(e20,e20) = e21 ) ),
inference(cnf_transformation,[],[f405]) ).
tcf(c_116,plain,
( ( op2(e23,e20) = e21 )
| ( op2(e22,e20) = e21 )
| ( op2(e21,e20) = e21 )
| ( op2(e20,e20) = e21 ) ),
inference(cnf_transformation,[],[f404]) ).
tcf(c_117,plain,
( ( op2(e20,e23) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e21) = e22 )
| ( op2(e20,e20) = e22 ) ),
inference(cnf_transformation,[],[f403]) ).
tcf(c_118,plain,
( ( op2(e23,e20) = e22 )
| ( op2(e22,e20) = e22 )
| ( op2(e21,e20) = e22 )
| ( op2(e20,e20) = e22 ) ),
inference(cnf_transformation,[],[f402]) ).
tcf(c_119,plain,
( ( op2(e20,e23) = e23 )
| ( op2(e20,e22) = e23 )
| ( op2(e20,e21) = e23 )
| ( op2(e20,e20) = e23 ) ),
inference(cnf_transformation,[],[f401]) ).
tcf(c_120,plain,
( ( op2(e23,e20) = e23 )
| ( op2(e22,e20) = e23 )
| ( op2(e21,e20) = e23 )
| ( op2(e20,e20) = e23 ) ),
inference(cnf_transformation,[],[f400]) ).
tcf(c_124,plain,
( ( op2(e23,e21) = e21 )
| ( op2(e22,e21) = e21 )
| ( op2(e21,e21) = e21 )
| ( op2(e20,e21) = e21 ) ),
inference(cnf_transformation,[],[f396]) ).
tcf(c_125,plain,
( ( op2(e21,e23) = e22 )
| ( op2(e21,e22) = e22 )
| ( op2(e21,e21) = e22 )
| ( op2(e21,e20) = e22 ) ),
inference(cnf_transformation,[],[f395]) ).
tcf(c_126,plain,
( ( op2(e23,e21) = e22 )
| ( op2(e22,e21) = e22 )
| ( op2(e21,e21) = e22 )
| ( op2(e20,e21) = e22 ) ),
inference(cnf_transformation,[],[f394]) ).
tcf(c_131,plain,
( ( op2(e22,e23) = e21 )
| ( op2(e22,e22) = e21 )
| ( op2(e22,e21) = e21 )
| ( op2(e22,e20) = e21 ) ),
inference(cnf_transformation,[],[f389]) ).
tcf(c_133,plain,
( ( op2(e22,e23) = e22 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e21) = e22 )
| ( op2(e22,e20) = e22 ) ),
inference(cnf_transformation,[],[f387]) ).
tcf(c_135,plain,
( ( op2(e22,e23) = e23 )
| ( op2(e22,e22) = e23 )
| ( op2(e22,e21) = e23 )
| ( op2(e22,e20) = e23 ) ),
inference(cnf_transformation,[],[f385]) ).
tcf(c_136,plain,
( ( op2(e23,e22) = e23 )
| ( op2(e22,e22) = e23 )
| ( op2(e21,e22) = e23 )
| ( op2(e20,e22) = e23 ) ),
inference(cnf_transformation,[],[f384]) ).
tcf(c_137,plain,
( ( op2(e23,e23) = e20 )
| ( op2(e23,e22) = e20 )
| ( op2(e23,e21) = e20 )
| ( op2(e23,e20) = e20 ) ),
inference(cnf_transformation,[],[f383]) ).
tcf(c_138,plain,
( ( op2(e23,e23) = e20 )
| ( op2(e22,e23) = e20 )
| ( op2(e21,e23) = e20 )
| ( op2(e20,e23) = e20 ) ),
inference(cnf_transformation,[],[f382]) ).
tcf(c_140,plain,
( ( op2(e23,e23) = e21 )
| ( op2(e22,e23) = e21 )
| ( op2(e21,e23) = e21 )
| ( op2(e20,e23) = e21 ) ),
inference(cnf_transformation,[],[f380]) ).
tcf(c_143,plain,
( ( op2(e23,e23) = e23 )
| ( op2(e23,e22) = e23 )
| ( op2(e23,e21) = e23 )
| ( op2(e23,e20) = e23 ) ),
inference(cnf_transformation,[],[f377]) ).
tcf(c_145,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f455]) ).
tcf(c_147,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f453]) ).
tcf(c_148,plain,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f452]) ).
tcf(c_149,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f451]) ).
tcf(c_151,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f449]) ).
tcf(c_153,plain,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f447]) ).
tcf(c_154,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f446]) ).
tcf(c_155,plain,
op1(e11,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f445]) ).
tcf(c_156,plain,
op1(e12,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f444]) ).
tcf(c_157,plain,
op1(e10,e12) != op1(e11,e12),
inference(cnf_transformation,[],[f443]) ).
tcf(c_159,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f441]) ).
tcf(c_160,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f440]) ).
tcf(c_161,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f439]) ).
tcf(c_162,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f438]) ).
tcf(c_167,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f433]) ).
tcf(c_168,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f432]) ).
tcf(c_170,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f430]) ).
tcf(c_171,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f429]) ).
tcf(c_175,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f425]) ).
tcf(c_176,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f424]) ).
tcf(c_177,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f423]) ).
tcf(c_179,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f421]) ).
tcf(c_180,plain,
op1(e11,e12) != op1(e11,e13),
inference(cnf_transformation,[],[f420]) ).
tcf(c_184,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f416]) ).
tcf(c_185,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f415]) ).
tcf(c_186,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f414]) ).
tcf(c_193,plain,
op2(e20,e20) != op2(e21,e20),
inference(cnf_transformation,[],[f503]) ).
tcf(c_194,plain,
op2(e20,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f502]) ).
tcf(c_195,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f501]) ).
tcf(c_199,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f497]) ).
tcf(c_200,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f496]) ).
tcf(c_201,plain,
op2(e20,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f495]) ).
tcf(c_202,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f494]) ).
tcf(c_203,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f493]) ).
tcf(c_204,plain,
op2(e22,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f492]) ).
tcf(c_206,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f490]) ).
tcf(c_207,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f489]) ).
tcf(c_208,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f488]) ).
tcf(c_209,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f487]) ).
tcf(c_210,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f486]) ).
tcf(c_213,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f483]) ).
tcf(c_215,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f481]) ).
tcf(c_216,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f480]) ).
tcf(c_217,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f479]) ).
tcf(c_218,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f478]) ).
tcf(c_219,plain,
op2(e20,e20) != op2(e20,e23),
inference(cnf_transformation,[],[f477]) ).
tcf(c_221,plain,
op2(e20,e21) != op2(e20,e23),
inference(cnf_transformation,[],[f475]) ).
tcf(c_222,plain,
op2(e20,e22) != op2(e20,e23),
inference(cnf_transformation,[],[f474]) ).
tcf(c_224,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f472]) ).
tcf(c_229,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f467]) ).
tcf(c_230,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f466]) ).
tcf(c_231,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f465]) ).
tcf(c_232,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f464]) ).
tcf(c_233,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f463]) ).
tcf(c_234,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f462]) ).
tcf(c_241,plain,
e10 != e11,
inference(cnf_transformation,[],[f509]) ).
tcf(c_242,plain,
e10 != e12,
inference(cnf_transformation,[],[f508]) ).
tcf(c_243,plain,
e10 != e13,
inference(cnf_transformation,[],[f507]) ).
tcf(c_244,plain,
e11 != e12,
inference(cnf_transformation,[],[f506]) ).
tcf(c_245,plain,
e11 != e13,
inference(cnf_transformation,[],[f505]) ).
tcf(c_246,plain,
e12 != e13,
inference(cnf_transformation,[],[f504]) ).
tcf(c_247,plain,
e20 != e21,
inference(cnf_transformation,[],[f515]) ).
tcf(c_248,plain,
e20 != e22,
inference(cnf_transformation,[],[f514]) ).
tcf(c_249,plain,
e20 != e23,
inference(cnf_transformation,[],[f513]) ).
tcf(c_250,plain,
e21 != e22,
inference(cnf_transformation,[],[f512]) ).
tcf(c_251,plain,
e21 != e23,
inference(cnf_transformation,[],[f511]) ).
tcf(c_252,plain,
e22 != e23,
inference(cnf_transformation,[],[f510]) ).
tcf(c_272,plain,
( ~ sP65
| ( op1(e13,e11) != e13 ) ),
inference(cnf_transformation,[],[f532]) ).
tcf(c_275,plain,
( ~ sP64
| ( op1(e12,e12) != e12 ) ),
inference(cnf_transformation,[],[f537]) ).
tcf(c_277,plain,
( ~ sP63
| ( op1(e10,e13) != e10 ) ),
inference(cnf_transformation,[],[f543]) ).
tcf(c_534,plain,
( sP63
| sP64
| sP65
| ( op1(e11,e10) != e11 ) ),
inference(cnf_transformation,[],[f806]) ).
tcf(c_537,plain,
( ( op1(e10,op1(e10,e13)) = e13 )
| ( op1(e10,op1(e10,e12)) = e12 )
| ( op1(e10,op1(e10,e11)) = e11 )
| ( op1(e10,op1(e10,e10)) = e10 ) ),
inference(cnf_transformation,[],[f803]) ).
tcf(c_538,plain,
( ( op1(e11,op1(e11,e13)) = e13 )
| ( op1(e11,op1(e11,e12)) = e12 )
| ( op1(e11,op1(e11,e11)) = e11 )
| ( op1(e11,op1(e11,e10)) = e10 ) ),
inference(cnf_transformation,[],[f802]) ).
tcf(c_539,plain,
( ( op1(e12,op1(e12,e13)) = e13 )
| ( op1(e12,op1(e12,e12)) = e12 )
| ( op1(e12,op1(e12,e11)) = e11 )
| ( op1(e12,op1(e12,e10)) = e10 ) ),
inference(cnf_transformation,[],[f801]) ).
tcf(c_548,plain,
( ~ sP131
| ( op2(e23,e21) != e23 ) ),
inference(cnf_transformation,[],[f808]) ).
tcf(c_551,plain,
( ~ sP130
| ( op2(e22,e22) != e22 ) ),
inference(cnf_transformation,[],[f813]) ).
tcf(c_553,plain,
( ~ sP129
| ( op2(e20,e23) != e20 ) ),
inference(cnf_transformation,[],[f819]) ).
tcf(c_810,plain,
( sP129
| sP130
| sP131
| ( op2(e21,e20) != e21 ) ),
inference(cnf_transformation,[],[f1082]) ).
tcf(c_813,plain,
( ( op2(e20,op2(e20,e23)) = e23 )
| ( op2(e20,op2(e20,e22)) = e22 )
| ( op2(e20,op2(e20,e21)) = e21 )
| ( op2(e20,op2(e20,e20)) = e20 ) ),
inference(cnf_transformation,[],[f1079]) ).
tcf(c_814,plain,
( ( op2(e21,op2(e21,e23)) = e23 )
| ( op2(e21,op2(e21,e22)) = e22 )
| ( op2(e21,op2(e21,e21)) = e21 )
| ( op2(e21,op2(e21,e20)) = e20 ) ),
inference(cnf_transformation,[],[f1078]) ).
tcf(c_815,plain,
( ( op2(e22,op2(e22,e23)) = e23 )
| ( op2(e22,op2(e22,e22)) = e22 )
| ( op2(e22,op2(e22,e21)) = e21 )
| ( op2(e22,op2(e22,e20)) = e20 ) ),
inference(cnf_transformation,[],[f1077]) ).
tcf(c_821,plain,
op1(op1(e13,e13),op1(e13,op1(e13,e13))) = e10,
inference(cnf_transformation,[],[f1086]) ).
tcf(c_822,plain,
op1(e13,op1(e13,e13)) = e11,
inference(cnf_transformation,[],[f1085]) ).
tcf(c_823,plain,
op1(e13,e13) = e12,
inference(cnf_transformation,[],[f1084]) ).
tcf(c_824,plain,
op2(op2(e23,e23),op2(e23,op2(e23,e23))) = e20,
inference(cnf_transformation,[],[f1089]) ).
tcf(c_825,plain,
op2(e23,op2(e23,e23)) = e21,
inference(cnf_transformation,[],[f1088]) ).
tcf(c_826,plain,
op2(e23,e23) = e22,
inference(cnf_transformation,[],[f1087]) ).
tcf(c_827,plain,
h1(e13) = e20,
inference(cnf_transformation,[],[f1093]) ).
tcf(c_828,plain,
op2(op2(e20,e20),op2(e20,op2(e20,e20))) = h1(e10),
inference(cnf_transformation,[],[f1092]) ).
tcf(c_829,plain,
op2(e20,op2(e20,e20)) = h1(e11),
inference(cnf_transformation,[],[f1091]) ).
tcf(c_830,plain,
op2(e20,e20) = h1(e12),
inference(cnf_transformation,[],[f1090]) ).
tcf(c_833,plain,
op2(e21,op2(e21,e21)) = h2(e11),
inference(cnf_transformation,[],[f1095]) ).
tcf(c_834,plain,
op2(e21,e21) = h2(e12),
inference(cnf_transformation,[],[f1094]) ).
tcf(c_837,plain,
op2(e22,op2(e22,e22)) = h3(e11),
inference(cnf_transformation,[],[f1099]) ).
tcf(c_838,plain,
op2(e22,e22) = h3(e12),
inference(cnf_transformation,[],[f1098]) ).
tcf(c_845,plain,
( ~ sP143
| ( h1(e12) != e21 ) ),
inference(cnf_transformation,[],[f1107]) ).
tcf(c_848,plain,
( ~ sP142
| ( h1(e11) != e22 ) ),
inference(cnf_transformation,[],[f1112]) ).
tcf(c_851,plain,
( ~ sP141
| ( h1(e10) != e23 ) ),
inference(cnf_transformation,[],[f1117]) ).
tcf(c_891,negated_conjecture,
( sP141
| sP142
| sP143
| ( h1(e10) != e20 )
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(cnf_transformation,[],[f1169]) ).
tcf(c_894,negated_conjecture,
( sP141
| sP142
| sP143
| ( h1(e13) != e20 )
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(cnf_transformation,[],[f1166]) ).
tcf(c_1379,plain,
op2(e23,e23) = e22,
inference(global_subsumption_just,[status(thm)],[c_112,c_826]) ).
tcf(c_1385,plain,
op1(e13,e13) = e12,
inference(global_subsumption_just,[status(thm)],[c_64,c_823]) ).
tcf(c_1427,plain,
( sP141
| sP142
| sP143
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) ) ),
inference(global_subsumption_just,[status(thm)],[c_894,c_827,c_894]) ).
tcf(c_1428,negated_conjecture,
( sP141
| sP142
| sP143
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(renaming,[status(thm)],[c_1427]) ).
tcf(c_1433,plain,
( sP141
| sP142
| sP143
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) ) ),
inference(global_subsumption_just,[status(thm)],[c_891,c_1428]) ).
tcf(c_1434,negated_conjecture,
( sP141
| sP142
| sP143
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(renaming,[status(thm)],[c_1433]) ).
tcf(c_4702,plain,
op2(e23,e22) = e21,
inference(light_normalisation,[status(thm)],[c_825,c_1379]) ).
tcf(c_4703,plain,
op1(e13,e12) = e11,
inference(light_normalisation,[status(thm)],[c_822,c_1385]) ).
tcf(c_5405,plain,
op2(e22,h3(e12)) = h3(e11),
inference(light_normalisation,[status(thm)],[c_837,c_838]) ).
tcf(c_5406,plain,
op2(e21,h2(e12)) = h2(e11),
inference(light_normalisation,[status(thm)],[c_833,c_834]) ).
tcf(c_5407,plain,
op2(e20,h1(e12)) = h1(e11),
inference(light_normalisation,[status(thm)],[c_829,c_830]) ).
tcf(c_5505,plain,
( ~ sP130
| ( h3(e12) != e22 ) ),
inference(light_normalisation,[status(thm)],[c_551,c_838]) ).
tcf(c_5671,plain,
op2(e22,e23) != h3(e12),
inference(light_normalisation,[status(thm)],[c_234,c_838]) ).
tcf(c_5672,plain,
op2(e22,e21) != h3(e12),
inference(light_normalisation,[status(thm)],[c_232,c_838]) ).
tcf(c_5673,plain,
op2(e22,e20) != h3(e12),
inference(light_normalisation,[status(thm)],[c_230,c_838]) ).
tcf(c_5677,plain,
op2(e20,e23) != h1(e12),
inference(light_normalisation,[status(thm)],[c_219,c_830]) ).
tcf(c_5678,plain,
op2(e20,e22) != h1(e12),
inference(light_normalisation,[status(thm)],[c_218,c_830]) ).
tcf(c_5679,plain,
op2(e20,e21) != h1(e12),
inference(light_normalisation,[status(thm)],[c_217,c_830]) ).
tcf(c_5680,plain,
op2(e22,e23) != e22,
inference(light_normalisation,[status(thm)],[c_216,c_1379]) ).
tcf(c_5681,plain,
op2(e21,e23) != e22,
inference(light_normalisation,[status(thm)],[c_215,c_1379]) ).
tcf(c_5682,plain,
op2(e20,e23) != e22,
inference(light_normalisation,[status(thm)],[c_213,c_1379]) ).
tcf(c_5683,plain,
h3(e12) != e21,
inference(light_normalisation,[status(thm)],[c_210,c_838,c_4702]) ).
tcf(c_5687,plain,
op2(e21,e22) != e21,
inference(light_normalisation,[status(thm)],[c_209,c_4702]) ).
tcf(c_5690,plain,
op2(e21,e22) != h3(e12),
inference(light_normalisation,[status(thm)],[c_208,c_838]) ).
tcf(c_5691,plain,
op2(e20,e22) != e21,
inference(light_normalisation,[status(thm)],[c_207,c_4702]) ).
tcf(c_5692,plain,
op2(e20,e22) != h3(e12),
inference(light_normalisation,[status(thm)],[c_206,c_838]) ).
tcf(c_5693,plain,
op2(e23,e21) != h2(e12),
inference(light_normalisation,[status(thm)],[c_203,c_834]) ).
tcf(c_5694,plain,
op2(e22,e21) != h2(e12),
inference(light_normalisation,[status(thm)],[c_202,c_834]) ).
tcf(c_5695,plain,
op2(e20,e21) != h2(e12),
inference(light_normalisation,[status(thm)],[c_199,c_834]) ).
tcf(c_5696,plain,
op2(e23,e20) != h1(e12),
inference(light_normalisation,[status(thm)],[c_195,c_830]) ).
tcf(c_5697,plain,
op2(e22,e20) != h1(e12),
inference(light_normalisation,[status(thm)],[c_194,c_830]) ).
tcf(c_5698,plain,
op2(e21,e20) != h1(e12),
inference(light_normalisation,[status(thm)],[c_193,c_830]) ).
tcf(c_5706,plain,
op1(e12,e13) != e12,
inference(light_normalisation,[status(thm)],[c_168,c_1385]) ).
tcf(c_5707,plain,
op1(e11,e13) != e12,
inference(light_normalisation,[status(thm)],[c_167,c_1385]) ).
tcf(c_5709,plain,
op1(e12,e12) != e11,
inference(light_normalisation,[status(thm)],[c_162,c_4703]) ).
tcf(c_5713,plain,
op1(e11,e12) != e11,
inference(light_normalisation,[status(thm)],[c_161,c_4703]) ).
tcf(c_5716,plain,
op1(e10,e12) != e11,
inference(light_normalisation,[status(thm)],[c_159,c_4703]) ).
tcf(c_5786,plain,
op2(e22,e21) = e20,
inference(light_normalisation,[status(thm)],[c_824,c_1379,c_4702]) ).
tcf(c_5787,plain,
op2(e20,e21) != e20,
inference(demodulation,[status(thm)],[c_200,c_5786]) ).
tcf(c_5788,plain,
h2(e12) != e20,
inference(demodulation,[status(thm)],[c_5694,c_5786]) ).
tcf(c_5789,plain,
op2(e23,e21) != e20,
inference(demodulation,[status(thm)],[c_204,c_5786]) ).
tcf(c_5790,plain,
op2(e22,e20) != e20,
inference(demodulation,[status(thm)],[c_229,c_5786]) ).
tcf(c_5791,plain,
h3(e12) != e20,
inference(demodulation,[status(thm)],[c_5672,c_5786]) ).
tcf(c_5792,plain,
op2(e22,e23) != e20,
inference(demodulation,[status(thm)],[c_233,c_5786]) ).
tcf(c_5804,plain,
op1(e12,e11) = e10,
inference(light_normalisation,[status(thm)],[c_821,c_1385,c_4703]) ).
tcf(c_5806,plain,
op1(e11,e11) != e10,
inference(demodulation,[status(thm)],[c_154,c_5804]) ).
tcf(c_5807,plain,
op1(e13,e11) != e10,
inference(demodulation,[status(thm)],[c_156,c_5804]) ).
tcf(c_5809,plain,
op1(e12,e12) != e10,
inference(demodulation,[status(thm)],[c_184,c_5804]) ).
tcf(c_5810,plain,
op1(e12,e13) != e10,
inference(demodulation,[status(thm)],[c_185,c_5804]) ).
tcf(c_5825,plain,
op2(h1(e12),h1(e11)) = h1(e10),
inference(light_normalisation,[status(thm)],[c_828,c_830,c_5407]) ).
tcf(c_5837,plain,
( ( e22 = e23 )
| ( e21 = e23 )
| ( op2(e23,e21) = e23 )
| ( op2(e23,e20) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_143,c_1379,c_4702]) ).
tcf(c_5838,plain,
( ( op2(e23,e21) = e23 )
| ( op2(e23,e20) = e23 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5837,c_252,c_251]) ).
tcf(c_5845,plain,
( ( e21 = e22 )
| ( op2(e22,e23) = e21 )
| ( op2(e21,e23) = e21 )
| ( op2(e20,e23) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_140,c_1379]) ).
tcf(c_5846,plain,
( ( op2(e22,e23) = e21 )
| ( op2(e21,e23) = e21 )
| ( op2(e20,e23) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5845,c_250]) ).
tcf(c_5856,plain,
( ( e20 = e22 )
| ( op2(e22,e23) = e20 )
| ( op2(e21,e23) = e20 )
| ( op2(e20,e23) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_138,c_1379]) ).
tcf(c_5857,plain,
( ( op2(e21,e23) = e20 )
| ( op2(e20,e23) = e20 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5856,c_248,c_5792]) ).
tcf(c_5864,plain,
( ( e20 = e22 )
| ( e20 = e21 )
| ( op2(e23,e21) = e20 )
| ( op2(e23,e20) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_137,c_1379,c_4702]) ).
tcf(c_5865,plain,
op2(e23,e20) = e20,
inference(forward_subsumption_resolution,[status(thm)],[c_5864,c_248,c_247,c_5789]) ).
tcf(c_5866,plain,
( ( e20 = e23 )
| ( op2(e23,e21) = e23 ) ),
inference(demodulation,[status(thm)],[c_5838,c_5865]) ).
tcf(c_5868,plain,
h1(e12) != e20,
inference(demodulation,[status(thm)],[c_5696,c_5865]) ).
tcf(c_5876,plain,
op2(e23,e21) = e23,
inference(forward_subsumption_resolution,[status(thm)],[c_5866,c_249]) ).
tcf(c_5878,plain,
op2(e20,e21) != e23,
inference(demodulation,[status(thm)],[c_201,c_5876]) ).
tcf(c_5879,plain,
h2(e12) != e23,
inference(demodulation,[status(thm)],[c_5693,c_5876]) ).
tcf(c_5882,plain,
( ~ sP131
| ( e23 != e23 ) ),
inference(demodulation,[status(thm)],[c_548,c_5876]) ).
tcf(c_5884,plain,
~ sP131,
inference(equality_resolution_simp,[status(thm)],[c_5882]) ).
tcf(c_5886,plain,
( sP129
| sP130
| ( op2(e21,e20) != e21 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_810,c_5884]) ).
tcf(c_5900,plain,
( ( e21 = e23 )
| ( h3(e12) = e23 )
| ( op2(e21,e22) = e23 )
| ( op2(e20,e22) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_136,c_838,c_4702]) ).
tcf(c_5901,plain,
( ( h3(e12) = e23 )
| ( op2(e21,e22) = e23 )
| ( op2(e20,e22) = e23 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5900,c_251]) ).
tcf(c_5911,plain,
( ( e20 = e23 )
| ( h3(e12) = e23 )
| ( op2(e22,e23) = e23 )
| ( op2(e22,e20) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_135,c_838,c_5786]) ).
tcf(c_5912,plain,
( ( h3(e12) = e23 )
| ( op2(e22,e23) = e23 )
| ( op2(e22,e20) = e23 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5911,c_249]) ).
tcf(c_5933,plain,
( ( e20 = e22 )
| ( h3(e12) = e22 )
| ( op2(e22,e23) = e22 )
| ( op2(e22,e20) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_133,c_838,c_5786]) ).
tcf(c_5934,plain,
( ( h3(e12) = e22 )
| ( op2(e22,e20) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5933,c_248,c_5680]) ).
tcf(c_5941,plain,
( ( e20 = e21 )
| ( h3(e12) = e21 )
| ( op2(e22,e23) = e21 )
| ( op2(e22,e20) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_131,c_838,c_5786]) ).
tcf(c_5942,plain,
( ( op2(e22,e23) = e21 )
| ( op2(e22,e20) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5941,c_247,c_5683]) ).
tcf(c_5968,plain,
( ( e22 = e23 )
| ( e20 = e22 )
| ( h2(e12) = e22 )
| ( op2(e20,e21) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_126,c_834,c_5786,c_5876]) ).
tcf(c_5969,plain,
( ( h2(e12) = e22 )
| ( op2(e20,e21) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5968,c_252,c_248]) ).
tcf(c_5976,plain,
( ( h2(e12) = e22 )
| ( op2(e21,e23) = e22 )
| ( op2(e21,e22) = e22 )
| ( op2(e21,e20) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_125,c_834]) ).
tcf(c_5977,plain,
( ( h2(e12) = e22 )
| ( op2(e21,e22) = e22 )
| ( op2(e21,e20) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5976,c_5681]) ).
tcf(c_5987,plain,
( ( e21 = e23 )
| ( e20 = e21 )
| ( h2(e12) = e21 )
| ( op2(e20,e21) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_124,c_834,c_5786,c_5876]) ).
tcf(c_5988,plain,
( ( h2(e12) = e21 )
| ( op2(e20,e21) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5987,c_251,c_247]) ).
tcf(c_6014,plain,
( ( e20 = e23 )
| ( h1(e12) = e23 )
| ( op2(e22,e20) = e23 )
| ( op2(e21,e20) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_120,c_830,c_5865]) ).
tcf(c_6015,plain,
( ( h1(e12) = e23 )
| ( op2(e22,e20) = e23 )
| ( op2(e21,e20) = e23 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6014,c_249]) ).
tcf(c_6025,plain,
( ( h1(e12) = e23 )
| ( op2(e20,e23) = e23 )
| ( op2(e20,e22) = e23 )
| ( op2(e20,e21) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_119,c_830]) ).
tcf(c_6026,plain,
( ( h1(e12) = e23 )
| ( op2(e20,e23) = e23 )
| ( op2(e20,e22) = e23 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6025,c_5878]) ).
tcf(c_6036,plain,
( ( e20 = e22 )
| ( h1(e12) = e22 )
| ( op2(e22,e20) = e22 )
| ( op2(e21,e20) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_118,c_830,c_5865]) ).
tcf(c_6037,plain,
( ( h1(e12) = e22 )
| ( op2(e22,e20) = e22 )
| ( op2(e21,e20) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6036,c_248]) ).
tcf(c_6047,plain,
( ( h1(e12) = e22 )
| ( op2(e20,e23) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e21) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_117,c_830]) ).
tcf(c_6048,plain,
( ( h1(e12) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e21) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6047,c_5682]) ).
tcf(c_6058,plain,
( ( e20 = e21 )
| ( h1(e12) = e21 )
| ( op2(e22,e20) = e21 )
| ( op2(e21,e20) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_116,c_830,c_5865]) ).
tcf(c_6059,plain,
( ( h1(e12) = e21 )
| ( op2(e22,e20) = e21 )
| ( op2(e21,e20) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6058,c_247]) ).
tcf(c_6069,plain,
( ( h1(e12) = e21 )
| ( op2(e20,e23) = e21 )
| ( op2(e20,e22) = e21 )
| ( op2(e20,e21) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_115,c_830]) ).
tcf(c_6070,plain,
( ( h1(e12) = e21 )
| ( op2(e20,e23) = e21 )
| ( op2(e20,e21) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6069,c_5691]) ).
tcf(c_6080,plain,
( ( h1(e12) = e20 )
| ( op2(e20,e23) = e20 )
| ( op2(e20,e22) = e20 )
| ( op2(e20,e21) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_113,c_830]) ).
tcf(c_6081,plain,
( ( op2(e20,e23) = e20 )
| ( op2(e20,e22) = e20 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6080,c_5868,c_5787]) ).
tcf(c_6088,plain,
( ( op2(e22,e23) = e23 )
| ( op2(e22,e23) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_108,c_5680,c_5792]) ).
tcf(c_6095,plain,
( ( h3(e12) = e23 )
| ( h3(e12) = e22 )
| ( h3(e12) = e21 )
| ( h3(e12) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_107,c_838]) ).
tcf(c_6096,plain,
( ( h3(e12) = e23 )
| ( h3(e12) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6095,c_5683,c_5791]) ).
tcf(c_6103,plain,
( ( op2(e22,e20) = e23 )
| ( op2(e22,e20) = e22 )
| ( op2(e22,e20) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_105,c_5790]) ).
tcf(c_6123,plain,
( ( op2(e21,e22) = e23 )
| ( op2(e21,e22) = e22 )
| ( op2(e21,e22) = e20 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_103,c_5687]) ).
tcf(c_6133,plain,
( ( h2(e12) = e23 )
| ( h2(e12) = e22 )
| ( h2(e12) = e21 )
| ( h2(e12) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_102,c_834]) ).
tcf(c_6134,plain,
( ( h2(e12) = e22 )
| ( h2(e12) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6133,c_5879,c_5788]) ).
tcf(c_6151,plain,
( ( op2(e20,e23) = e23 )
| ( op2(e20,e23) = e21 )
| ( op2(e20,e23) = e20 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_100,c_5682]) ).
tcf(c_6178,plain,
( ( h1(e12) = e23 )
| ( h1(e12) = e22 )
| ( h1(e12) = e21 )
| ( h1(e12) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_97,c_830]) ).
tcf(c_6179,plain,
( ( h1(e12) = e23 )
| ( h1(e12) = e22 )
| ( h1(e12) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6178,c_5868]) ).
tcf(c_6200,plain,
( ( e12 = e13 )
| ( e11 = e13 )
| ( op1(e13,e11) = e13 )
| ( op1(e13,e10) = e13 ) ),
inference(light_normalisation,[status(thm)],[c_95,c_1385,c_4703]) ).
tcf(c_6201,plain,
( ( op1(e13,e11) = e13 )
| ( op1(e13,e10) = e13 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6200,c_246,c_245]) ).
tcf(c_6208,plain,
( ( e11 = e12 )
| ( op1(e12,e13) = e11 )
| ( op1(e11,e13) = e11 )
| ( op1(e10,e13) = e11 ) ),
inference(light_normalisation,[status(thm)],[c_92,c_1385]) ).
tcf(c_6209,plain,
( ( op1(e12,e13) = e11 )
| ( op1(e11,e13) = e11 )
| ( op1(e10,e13) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6208,c_244]) ).
tcf(c_6219,plain,
( ( e10 = e12 )
| ( op1(e12,e13) = e10 )
| ( op1(e11,e13) = e10 )
| ( op1(e10,e13) = e10 ) ),
inference(light_normalisation,[status(thm)],[c_90,c_1385]) ).
tcf(c_6220,plain,
( ( op1(e11,e13) = e10 )
| ( op1(e10,e13) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6219,c_242,c_5810]) ).
tcf(c_6227,plain,
( ( e10 = e12 )
| ( e10 = e11 )
| ( op1(e13,e11) = e10 )
| ( op1(e13,e10) = e10 ) ),
inference(light_normalisation,[status(thm)],[c_89,c_1385,c_4703]) ).
tcf(c_6228,plain,
op1(e13,e10) = e10,
inference(forward_subsumption_resolution,[status(thm)],[c_6227,c_242,c_241,c_5807]) ).
tcf(c_6229,plain,
( ( e10 = e13 )
| ( op1(e13,e11) = e13 ) ),
inference(demodulation,[status(thm)],[c_6201,c_6228]) ).
tcf(c_6231,plain,
op1(e10,e10) != e10,
inference(demodulation,[status(thm)],[c_147,c_6228]) ).
tcf(c_6232,plain,
op1(e11,e10) != e10,
inference(demodulation,[status(thm)],[c_149,c_6228]) ).
tcf(c_6239,plain,
op1(e13,e11) = e13,
inference(forward_subsumption_resolution,[status(thm)],[c_6229,c_243]) ).
tcf(c_6241,plain,
op1(e10,e11) != e13,
inference(demodulation,[status(thm)],[c_153,c_6239]) ).
tcf(c_6242,plain,
op1(e11,e11) != e13,
inference(demodulation,[status(thm)],[c_155,c_6239]) ).
tcf(c_6245,plain,
( ~ sP65
| ( e13 != e13 ) ),
inference(demodulation,[status(thm)],[c_272,c_6239]) ).
tcf(c_6247,plain,
~ sP65,
inference(equality_resolution_simp,[status(thm)],[c_6245]) ).
tcf(c_6249,plain,
( sP63
| sP64
| ( op1(e11,e10) != e11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_534,c_6247]) ).
tcf(c_6263,plain,
( ( e11 = e13 )
| ( op1(e12,e12) = e13 )
| ( op1(e11,e12) = e13 )
| ( op1(e10,e12) = e13 ) ),
inference(light_normalisation,[status(thm)],[c_88,c_4703]) ).
tcf(c_6264,plain,
( ( op1(e12,e12) = e13 )
| ( op1(e11,e12) = e13 )
| ( op1(e10,e12) = e13 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6263,c_245]) ).
tcf(c_6296,plain,
( ( e10 = e12 )
| ( op1(e12,e13) = e12 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e10) = e12 ) ),
inference(light_normalisation,[status(thm)],[c_85,c_5804]) ).
tcf(c_6297,plain,
( ( op1(e12,e12) = e12 )
| ( op1(e12,e10) = e12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6296,c_242,c_5706]) ).
tcf(c_6304,plain,
( ( e10 = e11 )
| ( op1(e12,e13) = e11 )
| ( op1(e12,e12) = e11 )
| ( op1(e12,e10) = e11 ) ),
inference(light_normalisation,[status(thm)],[c_83,c_5804]) ).
tcf(c_6305,plain,
( ( op1(e12,e13) = e11 )
| ( op1(e12,e10) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6304,c_241,c_5709]) ).
tcf(c_6312,plain,
( ( e10 = e11 )
| ( op1(e12,e12) = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e10,e12) = e10 ) ),
inference(light_normalisation,[status(thm)],[c_82,c_4703]) ).
tcf(c_6313,plain,
( ( op1(e11,e12) = e10 )
| ( op1(e10,e12) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6312,c_241,c_5809]) ).
tcf(c_6320,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e12) = e13 )
| ( op1(e11,e10) = e13 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_79,c_6242]) ).
tcf(c_6330,plain,
( ( e12 = e13 )
| ( e10 = e12 )
| ( op1(e11,e11) = e12 )
| ( op1(e10,e11) = e12 ) ),
inference(light_normalisation,[status(thm)],[c_78,c_5804,c_6239]) ).
tcf(c_6331,plain,
( ( op1(e11,e11) = e12 )
| ( op1(e10,e11) = e12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6330,c_246,c_242]) ).
tcf(c_6366,plain,
( ( op1(e11,e13) = e10 )
| ( op1(e11,e12) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_73,c_5806,c_6232]) ).
tcf(c_6373,plain,
( ( e10 = e13 )
| ( op1(e12,e10) = e13 )
| ( op1(e11,e10) = e13 )
| ( op1(e10,e10) = e13 ) ),
inference(light_normalisation,[status(thm)],[c_72,c_6228]) ).
tcf(c_6374,plain,
( ( op1(e12,e10) = e13 )
| ( op1(e11,e10) = e13 )
| ( op1(e10,e10) = e13 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6373,c_243]) ).
tcf(c_6384,plain,
( ( op1(e10,e13) = e13 )
| ( op1(e10,e12) = e13 )
| ( op1(e10,e10) = e13 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_71,c_6241]) ).
tcf(c_6426,plain,
( ( op1(e10,e13) = e11 )
| ( op1(e10,e11) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_67,c_5716]) ).
tcf(c_6443,plain,
( ( op1(e12,e13) = e13 )
| ( op1(e12,e13) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_60,c_5706,c_5810]) ).
tcf(c_6450,plain,
( ( op1(e12,e12) = e13 )
| ( op1(e12,e12) = e12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_59,c_5709,c_5809]) ).
tcf(c_6467,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e13) = e11 )
| ( op1(e11,e13) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_56,c_5707]) ).
tcf(c_6477,plain,
( ( op1(e11,e12) = e13 )
| ( op1(e11,e12) = e12 )
| ( op1(e11,e12) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_55,c_5713]) ).
tcf(c_6487,plain,
( ( op1(e11,e11) = e12 )
| ( op1(e11,e11) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_54,c_6242,c_5806]) ).
tcf(c_6494,plain,
( ( op1(e11,e10) = e13 )
| ( op1(e11,e10) = e12 )
| ( op1(e11,e10) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_53,c_6232]) ).
tcf(c_6531,plain,
( ( op1(e10,e10) = e13 )
| ( op1(e10,e10) = e12 )
| ( op1(e10,e10) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_49,c_6231]) ).
tcf(c_6542,plain,
( ( h3(e11) = e22 )
| ( op2(e22,e20) = e21 )
| ( op2(e22,op2(e22,e23)) = e23 )
| ( op2(e22,op2(e22,e20)) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_815,c_838,c_5405,c_5786]) ).
tcf(c_6555,plain,
( ( h2(e11) = e21 )
| ( op2(e21,op2(e21,e23)) = e23 )
| ( op2(e21,op2(e21,e22)) = e22 )
| ( op2(e21,op2(e21,e20)) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_814,c_834,c_5406]) ).
tcf(c_6568,plain,
( ( h1(e11) = e20 )
| ( op2(e20,op2(e20,e23)) = e23 )
| ( op2(e20,op2(e20,e22)) = e22 )
| ( op2(e20,op2(e20,e21)) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_813,c_830,c_5407]) ).
tcf(c_6582,plain,
( ( op1(e12,e10) = e11 )
| ( op1(e12,op1(e12,e13)) = e13 )
| ( op1(e12,op1(e12,e12)) = e12 )
| ( op1(e12,op1(e12,e10)) = e10 ) ),
inference(light_normalisation,[status(thm)],[c_539,c_5804]) ).
tcf(c_6649,plain,
( sP141
| sP142
| sP143
| ( h1(e12) != h1(e12) )
| ( h1(e11) != h1(e11) )
| ( h1(e10) != h1(e10) )
| ( op2(e20,h1(e11)) != e20 )
| ( op2(e20,h1(e10)) != h1(e10) )
| ( op2(h1(e12),e20) != h1(op1(e12,e13)) )
| ( op2(h1(e11),e20) != h1(op1(e11,e13)) )
| ( op2(h1(e10),e20) != h1(op1(e10,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(light_normalisation,[status(thm)],[c_1434,c_1385,c_827,c_830,c_4703,c_5407,c_5804,c_5825,c_6228,c_6239]) ).
tcf(c_6650,plain,
( sP141
| sP142
| sP143
| ( op2(e20,h1(e11)) != e20 )
| ( op2(e20,h1(e10)) != h1(e10) )
| ( op2(h1(e12),e20) != h1(op1(e12,e13)) )
| ( op2(h1(e11),e20) != h1(op1(e11,e13)) )
| ( op2(h1(e10),e20) != h1(op1(e10,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(equality_resolution_simp,[status(thm)],[c_6649]) ).
tcf(c_12333,definition,
iPr_def_10 = op1(e10,e10),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_12335,definition,
iPr_def_12 = h1(e12),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_12336,definition,
iPr_def_13 = op1(e10,e11),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_12339,definition,
iPr_def_16 = op1(e10,e12),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_12342,definition,
iPr_def_19 = op1(e10,e13),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_12345,definition,
iPr_def_22 = op1(e11,e10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_12348,definition,
iPr_def_25 = op1(e11,e11),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_12351,definition,
iPr_def_28 = op1(e11,e12),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_12354,definition,
iPr_def_31 = op1(e11,e13),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_12357,definition,
iPr_def_34 = op1(e12,e10),
introduced(definition,[new_symbols(definition,[iPr_def_34])],[]) ).
tcf(c_12360,definition,
iPr_def_37 = op1(e12,e12),
introduced(definition,[new_symbols(definition,[iPr_def_37])],[]) ).
tcf(c_12363,definition,
iPr_def_40 = op1(e12,e13),
introduced(definition,[new_symbols(definition,[iPr_def_40])],[]) ).
tcf(c_12369,definition,
iPr_def_46 = h3(e11),
introduced(definition,[new_symbols(definition,[iPr_def_46])],[]) ).
tcf(c_12395,definition,
iPr_def_72 = h2(e11),
introduced(definition,[new_symbols(definition,[iPr_def_72])],[]) ).
tcf(c_12418,definition,
iPr_def_95 = h1(e10),
introduced(definition,[new_symbols(definition,[iPr_def_95])],[]) ).
tcf(c_12419,definition,
iPr_def_96 = op2(iPr_def_95,iPr_def_95),
introduced(definition,[new_symbols(definition,[iPr_def_96])],[]) ).
tcf(c_12420,definition,
iPr_def_97 = h1(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_97])],[]) ).
tcf(c_12421,definition,
iPr_def_98 = h1(e11),
introduced(definition,[new_symbols(definition,[iPr_def_98])],[]) ).
tcf(c_12422,definition,
iPr_def_99 = op2(iPr_def_95,iPr_def_98),
introduced(definition,[new_symbols(definition,[iPr_def_99])],[]) ).
tcf(c_12423,definition,
iPr_def_100 = h1(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_100])],[]) ).
tcf(c_12424,definition,
iPr_def_101 = op2(iPr_def_95,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_101])],[]) ).
tcf(c_12425,definition,
iPr_def_102 = h1(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_102])],[]) ).
tcf(c_12426,definition,
iPr_def_103 = op2(iPr_def_98,iPr_def_95),
introduced(definition,[new_symbols(definition,[iPr_def_103])],[]) ).
tcf(c_12427,definition,
iPr_def_104 = h1(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_104])],[]) ).
tcf(c_12428,definition,
iPr_def_105 = op2(iPr_def_98,iPr_def_98),
introduced(definition,[new_symbols(definition,[iPr_def_105])],[]) ).
tcf(c_12429,definition,
iPr_def_106 = h1(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_106])],[]) ).
tcf(c_12430,definition,
iPr_def_107 = op2(iPr_def_98,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_107])],[]) ).
tcf(c_12431,definition,
iPr_def_108 = h1(iPr_def_28),
introduced(definition,[new_symbols(definition,[iPr_def_108])],[]) ).
tcf(c_12432,definition,
iPr_def_109 = op2(iPr_def_12,iPr_def_95),
introduced(definition,[new_symbols(definition,[iPr_def_109])],[]) ).
tcf(c_12433,definition,
iPr_def_110 = h1(iPr_def_34),
introduced(definition,[new_symbols(definition,[iPr_def_110])],[]) ).
tcf(c_12434,definition,
iPr_def_111 = op2(iPr_def_12,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_111])],[]) ).
tcf(c_12435,definition,
iPr_def_112 = h1(iPr_def_37),
introduced(definition,[new_symbols(definition,[iPr_def_112])],[]) ).
tcf(c_12436,definition,
iPr_def_113 = op2(iPr_def_95,e20),
introduced(definition,[new_symbols(definition,[iPr_def_113])],[]) ).
tcf(c_12437,definition,
iPr_def_114 = h1(iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_114])],[]) ).
tcf(c_12438,definition,
iPr_def_115 = op2(iPr_def_98,e20),
introduced(definition,[new_symbols(definition,[iPr_def_115])],[]) ).
tcf(c_12439,definition,
iPr_def_116 = h1(iPr_def_31),
introduced(definition,[new_symbols(definition,[iPr_def_116])],[]) ).
tcf(c_12440,definition,
iPr_def_117 = op2(iPr_def_12,e20),
introduced(definition,[new_symbols(definition,[iPr_def_117])],[]) ).
tcf(c_12441,definition,
iPr_def_118 = h1(iPr_def_40),
introduced(definition,[new_symbols(definition,[iPr_def_118])],[]) ).
tcf(c_12442,definition,
iPr_def_119 = op2(e20,iPr_def_95),
introduced(definition,[new_symbols(definition,[iPr_def_119])],[]) ).
tcf(c_12443,definition,
iPr_def_120 = op2(e20,iPr_def_98),
introduced(definition,[new_symbols(definition,[iPr_def_120])],[]) ).
tcf(c_12449,plain,
( sP141
| sP142
| sP143
| ( iPr_def_120 != e20 )
| ( iPr_def_119 != iPr_def_95 )
| ( iPr_def_117 != iPr_def_118 )
| ( iPr_def_115 != iPr_def_116 )
| ( iPr_def_113 != iPr_def_114 )
| ( iPr_def_111 != iPr_def_112 )
| ( iPr_def_109 != iPr_def_110 )
| ( iPr_def_107 != iPr_def_108 )
| ( iPr_def_105 != iPr_def_106 )
| ( iPr_def_103 != iPr_def_104 )
| ( iPr_def_101 != iPr_def_102 )
| ( iPr_def_99 != iPr_def_100 )
| ( iPr_def_96 != iPr_def_97 ) ),
inference(demodulation,[status(thm)],[c_6650,c_12443,c_12442,c_12441,c_12440,c_12439,c_12438,c_12437,c_12436,c_12435,c_12434,c_12433,c_12432,c_12431,c_12430,c_12429,c_12428,c_12427,c_12426,c_12425,c_12424,c_12423,c_12421,c_12422,c_12420,c_12418,c_12419]) ).
tcf(c_13749,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_12449,c_12443,c_12442,c_12441,c_12440,c_12439,c_12438,c_12437,c_12436,c_12435,c_12434,c_12433,c_12432,c_12431,c_12430,c_12429,c_12428,c_12427,c_12426,c_12425,c_12424,c_12423,c_12422,c_12421,c_12420,c_12419,c_12418,c_12395,c_12369,c_12363,c_12360,c_12357,c_12354,c_12351,c_12348,c_12345,c_12342,c_12339,c_12336,c_12335,c_12333,c_6582,c_6568,c_6555,c_6542,c_6531,c_6494,c_6487,c_6477,c_6467,c_6450,c_6443,c_6426,c_6384,c_6374,c_6366,c_6331,c_6320,c_6313,c_6305,c_6297,c_6264,c_6249,c_6242,c_6220,c_6209,c_6179,c_6151,c_6134,c_6123,c_6103,c_6096,c_6088,c_6081,c_6070,c_6059,c_6048,c_6037,c_6026,c_6015,c_5988,c_5977,c_5969,c_5942,c_5934,c_5912,c_5901,c_5886,c_5876,c_5865,c_5857,c_5846,c_5825,c_5806,c_5804,c_5787,c_5786,c_5716,c_5713,c_5706,c_5698,c_5697,c_5695,c_5692,c_5691,c_5690,c_5687,c_5680,c_5679,c_5678,c_5677,c_5673,c_5671,c_5505,c_5407,c_5406,c_5405,c_4702,c_851,c_848,c_845,c_838,c_834,c_830,c_827,c_826,c_553,c_538,c_537,c_277,c_275,c_252,c_251,c_250,c_249,c_248,c_247,c_246,c_245,c_244,c_243,c_242,c_241,c_231,c_224,c_222,c_221,c_186,c_180,c_179,c_177,c_176,c_175,c_171,c_170,c_160,c_157,c_151,c_148,c_145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG119+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 04:49:28 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 6.94/1.73 % SZS status Started for theBenchmark.p
% 6.94/1.73 % SZS status Theorem for theBenchmark.p
% 6.94/1.73
% 6.94/1.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.94/1.73
% 6.94/1.73 % ------ iProver source info
% 6.94/1.73
% 6.94/1.73 % git: date: 2026-07-19 20:42:38 +0200
% 6.94/1.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.94/1.73 % git: non_committed_changes: false
% 6.94/1.73
% 6.94/1.73 % ------ Parsing...
% 6.94/1.73 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.94/1.73
% 6.94/1.73 % ------ Preprocessing... sup_sim: 448 sf_s rm: 121 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.94/1.73
% 6.94/1.73 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.94/1.73
% 6.94/1.73 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.94/1.73 % ------ Proving...
% 6.94/1.73 % ------ Problem Properties
% 6.94/1.73
% 6.94/1.73 %
% 6.94/1.73 % clauses 364
% 6.94/1.73 % conjectures 0
% 6.94/1.73 % EPR 34
% 6.94/1.73 % Horn 281
% 6.94/1.73 % unary 245
% 6.94/1.73 % binary 59
% 6.94/1.73 % lits 624
% 6.94/1.73 % lits eq 566
% 6.94/1.73 % fd_pure 0
% 6.94/1.73 % fd_pseudo 0
% 6.94/1.73 % fd_cond 0
% 6.94/1.73 % fd_pseudo_cond 0
% 6.94/1.73 % AC symbols 0
% 6.94/1.73
% 6.94/1.73 % ------ Schedule dynamic 5 is on
% 6.94/1.73
% 6.94/1.73 % ------ no conjectures: strip conj schedule
% 6.94/1.73
% 6.94/1.73 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 6.94/1.73
% 6.94/1.73
% 6.94/1.73 % ------
% 6.94/1.73 % Current options:
% 6.94/1.73 % ------
% 6.94/1.73
% 6.94/1.73
% 6.94/1.73 %
% 6.94/1.73
% 6.94/1.73 % ------ Proving...
% 6.94/1.73 %
% 6.94/1.73
% 6.94/1.73 % SZS status Theorem for theBenchmark.p
% 6.94/1.73
% 6.94/1.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.94/1.75
% 6.94/1.75
%------------------------------------------------------------------------------