%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ALG126+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 : n020.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:31 PM UTC 2026
% Result : Theorem 6.52s 1.63s
% Output : CNFRefutation 6.52s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f713ERROR: Could not build tree for root c_16734ERROR: 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(f10,axiom,
( ( ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e10) = e10
& op1(e10,e10) = e10 ) )
& ( ( ( op1(e13,e13) = e13
| op1(e13,e13) != e13 )
& ( op1(e12,e13) = e12
| op1(e12,e12) != e13 )
& ( op1(e11,e13) = e11
| op1(e11,e11) != e13 )
& ( op1(e10,e13) = e10
| op1(e10,e10) != e13 )
& op1(e13,op1(e13,e13)) = e13
& op1(e13,op1(e13,e12)) = e12
& op1(e13,op1(e13,e11)) = e11
& op1(e13,op1(e13,e10)) = e10 )
| ( ( op1(e13,e12) = e13
| op1(e13,e13) != e12 )
& ( op1(e12,e12) = e12
| op1(e12,e12) != e12 )
& ( op1(e11,e12) = e11
| op1(e11,e11) != e12 )
& ( op1(e10,e12) = e10
| op1(e10,e10) != e12 )
& op1(e12,op1(e12,e13)) = e13
& op1(e12,op1(e12,e12)) = e12
& op1(e12,op1(e12,e11)) = e11
& op1(e12,op1(e12,e10)) = e10 )
| ( ( op1(e13,e11) = e13
| op1(e13,e13) != e11 )
& ( op1(e12,e11) = e12
| op1(e12,e12) != e11 )
& ( op1(e11,e11) = e11
| op1(e11,e11) != e11 )
& ( op1(e10,e11) = e10
| op1(e10,e10) != e11 )
& op1(e11,op1(e11,e13)) = e13
& op1(e11,op1(e11,e12)) = e12
& op1(e11,op1(e11,e11)) = e11
& op1(e11,op1(e11,e10)) = e10 )
| ( ( op1(e13,e10) = e13
| op1(e13,e13) != e10 )
& ( op1(e12,e10) = e12
| op1(e12,e12) != e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) != e10 )
& ( op1(e10,e10) = e10
| op1(e10,e10) != e10 )
& op1(e10,op1(e10,e13)) = e13
& op1(e10,op1(e10,e12)) = e12
& op1(e10,op1(e10,e11)) = e11
& op1(e10,op1(e10,e10)) = e10 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e20) = e20
& op2(e20,e20) = e20 ) )
& ( ( ( op2(e23,e23) = e23
| op2(e23,e23) != e23 )
& ( op2(e22,e23) = e22
| op2(e22,e22) != e23 )
& ( op2(e21,e23) = e21
| op2(e21,e21) != e23 )
& ( op2(e20,e23) = e20
| op2(e20,e20) != e23 )
& op2(e23,op2(e23,e23)) = e23
& op2(e23,op2(e23,e22)) = e22
& op2(e23,op2(e23,e21)) = e21
& op2(e23,op2(e23,e20)) = e20 )
| ( ( op2(e23,e22) = e23
| op2(e23,e23) != e22 )
& ( op2(e22,e22) = e22
| op2(e22,e22) != e22 )
& ( op2(e21,e22) = e21
| op2(e21,e21) != e22 )
& ( op2(e20,e22) = e20
| op2(e20,e20) != e22 )
& op2(e22,op2(e22,e23)) = e23
& op2(e22,op2(e22,e22)) = e22
& op2(e22,op2(e22,e21)) = e21
& op2(e22,op2(e22,e20)) = e20 )
| ( ( op2(e23,e21) = e23
| op2(e23,e23) != e21 )
& ( op2(e22,e21) = e22
| op2(e22,e22) != e21 )
& ( op2(e21,e21) = e21
| op2(e21,e21) != e21 )
& ( op2(e20,e21) = e20
| op2(e20,e20) != e21 )
& op2(e21,op2(e21,e23)) = e23
& op2(e21,op2(e21,e22)) = e22
& op2(e21,op2(e21,e21)) = e21
& op2(e21,op2(e21,e20)) = e20 )
| ( ( op2(e23,e20) = e23
| op2(e23,e23) != e20 )
& ( op2(e22,e20) = e22
| op2(e22,e22) != e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) != e20 )
& ( op2(e20,e20) = e20
| op2(e20,e20) != e20 )
& op2(e20,op2(e20,e23)) = e23
& op2(e20,op2(e20,e22)) = e22
& op2(e20,op2(e20,e21)) = e21
& op2(e20,op2(e20,e20)) = e20 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e13 = op1(op1(e11,e11),op1(e11,e11))
& e12 = op1(op1(op1(e11,e11),op1(e11,e11)),op1(e11,e11))
& e10 = op1(e11,e11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e23 = op2(op2(e21,e21),op2(e21,e21))
& e22 = op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21))
& e20 = op2(e21,e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e13) = op2(op2(e20,e20),op2(e20,e20))
& h1(e12) = op2(op2(op2(e20,e20),op2(e20,e20)),op2(e20,e20))
& h1(e10) = op2(e20,e20)
& h1(e11) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e13) = op2(op2(e21,e21),op2(e21,e21))
& h2(e12) = op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21))
& h2(e10) = op2(e21,e21)
& h2(e11) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h3(e13) = op2(op2(e22,e22),op2(e22,e22))
& h3(e12) = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22))
& h3(e10) = op2(e22,e22)
& h3(e11) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( h4(e13) = op2(op2(e23,e23),op2(e23,e23))
& h4(e12) = op2(op2(op2(e23,e23),op2(e23,e23)),op2(e23,e23))
& h4(e10) = op2(e23,e23)
& h4(e11) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f75,plain,
( ~ sP8
| ( e21 != h2(e13)
& e21 != h2(e12)
& e21 != h2(e11)
& e21 != h2(e10) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f76,plain,
( ~ sP7
| ( e22 != h2(e13)
& e22 != h2(e12)
& e22 != h2(e11)
& e22 != h2(e10) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f77,plain,
( ~ sP6
| ( e23 != h2(e13)
& e23 != h2(e12)
& e23 != h2(e11)
& e23 != h2(e10) ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f84,plain,
( ~ sP29
| ( ( op1(e13,e11) = e13
| op1(e13,e13) != e11 )
& ( op1(e12,e11) = e12
| op1(e12,e12) != e11 )
& ( op1(e11,e11) = e11
| op1(e11,e11) != e11 )
& ( op1(e10,e11) = e10
| op1(e10,e10) != e11 )
& 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(nnf_transformation,[],[f51]) ).
fof(f85,plain,
( ~ sP28
| ( ( op1(e13,e12) = e13
| op1(e13,e13) != e12 )
& ( op1(e12,e12) = e12
| op1(e12,e12) != e12 )
& ( op1(e11,e12) = e11
| op1(e11,e11) != e12 )
& ( op1(e10,e12) = e10
| op1(e10,e10) != e12 )
& 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(nnf_transformation,[],[f50]) ).
fof(f86,plain,
( ~ sP27
| ( ( op1(e13,e13) = e13
| op1(e13,e13) != e13 )
& ( op1(e12,e13) = e12
| op1(e12,e12) != e13 )
& ( op1(e11,e13) = e11
| op1(e11,e11) != e13 )
& ( op1(e10,e13) = e10
| op1(e10,e10) != e13 )
& op1(e13,op1(e13,e13)) = e13
& op1(e13,op1(e13,e12)) = e12
& op1(e13,op1(e13,e11)) = e11
& op1(e13,op1(e13,e10)) = e10 ) ),
inference(nnf_transformation,[],[f49]) ).
fof(f87,plain,
( ~ sP26
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e10) = e10
& op1(e10,e11) = e10 ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f88,plain,
( ~ sP25
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e10) = e10
& op1(e10,e12) = e10 ) ),
inference(nnf_transformation,[],[f47]) ).
fof(f89,plain,
( ~ sP24
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e10) = e10
& op1(e10,e13) = e10 ) ),
inference(nnf_transformation,[],[f46]) ).
fof(f90,plain,
( ~ sP23
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e11) = e11
& op1(e11,e10) = e11 ) ),
inference(nnf_transformation,[],[f45]) ).
fof(f91,plain,
( ~ sP22
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e11) = e11
& op1(e11,e11) = e11 ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f92,plain,
( ~ sP21
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e11) = e11
& op1(e11,e12) = e11 ) ),
inference(nnf_transformation,[],[f43]) ).
fof(f93,plain,
( ~ sP20
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e11) = e11
& op1(e11,e13) = e11 ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f94,plain,
( ~ sP19
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e12) = e12
& op1(e12,e10) = e12 ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f95,plain,
( ~ sP18
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e12) = e12
& op1(e12,e11) = e12 ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f96,plain,
( ~ sP17
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e12) = e12
& op1(e12,e12) = e12 ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f97,plain,
( ~ sP16
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e12) = e12
& op1(e12,e13) = e12 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f98,plain,
( ~ sP15
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e13) = e13
& op1(e13,e10) = e13 ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f99,plain,
( ~ sP14
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e13) = e13
& op1(e13,e11) = e13 ) ),
inference(nnf_transformation,[],[f36]) ).
fof(f100,plain,
( ~ sP13
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e13) = e13
& op1(e13,e12) = e13 ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f102,plain,
( ~ sP47
| ( ( op2(e23,e21) = e23
| op2(e23,e23) != e21 )
& ( op2(e22,e21) = e22
| op2(e22,e22) != e21 )
& ( op2(e21,e21) = e21
| op2(e21,e21) != e21 )
& ( op2(e20,e21) = e20
| op2(e20,e20) != e21 )
& 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(nnf_transformation,[],[f70]) ).
fof(f103,plain,
( ~ sP46
| ( ( op2(e23,e22) = e23
| op2(e23,e23) != e22 )
& ( op2(e22,e22) = e22
| op2(e22,e22) != e22 )
& ( op2(e21,e22) = e21
| op2(e21,e21) != e22 )
& ( op2(e20,e22) = e20
| op2(e20,e20) != e22 )
& 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(nnf_transformation,[],[f69]) ).
fof(f104,plain,
( ~ sP45
| ( ( op2(e23,e23) = e23
| op2(e23,e23) != e23 )
& ( op2(e22,e23) = e22
| op2(e22,e22) != e23 )
& ( op2(e21,e23) = e21
| op2(e21,e21) != e23 )
& ( op2(e20,e23) = e20
| op2(e20,e20) != e23 )
& op2(e23,op2(e23,e23)) = e23
& op2(e23,op2(e23,e22)) = e22
& op2(e23,op2(e23,e21)) = e21
& op2(e23,op2(e23,e20)) = e20 ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f105,plain,
( ~ sP44
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e20) = e20
& op2(e20,e21) = e20 ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f106,plain,
( ~ sP43
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e20) = e20
& op2(e20,e22) = e20 ) ),
inference(nnf_transformation,[],[f66]) ).
fof(f107,plain,
( ~ sP42
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e20) = e20
& op2(e20,e23) = e20 ) ),
inference(nnf_transformation,[],[f65]) ).
fof(f108,plain,
( ~ sP41
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e21) = e21
& op2(e21,e20) = e21 ) ),
inference(nnf_transformation,[],[f64]) ).
fof(f109,plain,
( ~ sP40
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e21) = e21
& op2(e21,e21) = e21 ) ),
inference(nnf_transformation,[],[f63]) ).
fof(f110,plain,
( ~ sP39
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e21) = e21
& op2(e21,e22) = e21 ) ),
inference(nnf_transformation,[],[f62]) ).
fof(f111,plain,
( ~ sP38
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e21) = e21
& op2(e21,e23) = e21 ) ),
inference(nnf_transformation,[],[f61]) ).
fof(f112,plain,
( ~ sP37
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e22) = e22
& op2(e22,e20) = e22 ) ),
inference(nnf_transformation,[],[f60]) ).
fof(f113,plain,
( ~ sP36
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e22) = e22
& op2(e22,e21) = e22 ) ),
inference(nnf_transformation,[],[f59]) ).
fof(f114,plain,
( ~ sP35
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e22) = e22
& op2(e22,e22) = e22 ) ),
inference(nnf_transformation,[],[f58]) ).
fof(f115,plain,
( ~ sP34
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e22) = e22
& op2(e22,e23) = e22 ) ),
inference(nnf_transformation,[],[f57]) ).
fof(f116,plain,
( ~ sP33
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e23) = e23
& op2(e23,e20) = e23 ) ),
inference(nnf_transformation,[],[f56]) ).
fof(f117,plain,
( ~ sP32
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e23) = e23
& op2(e23,e21) = e23 ) ),
inference(nnf_transformation,[],[f55]) ).
fof(f118,plain,
( ~ sP31
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e23) = e23
& op2(e23,e22) = e23 ) ),
inference(nnf_transformation,[],[f54]) ).
fof(f134,plain,
( ~ sP8
| e21 != h2(e11) ),
inference(cnf_transformation,[],[f75]) ).
fof(f137,plain,
( ~ sP7
| e22 != h2(e12) ),
inference(cnf_transformation,[],[f76]) ).
fof(f140,plain,
( ~ sP6
| e23 != h2(e13) ),
inference(cnf_transformation,[],[f77]) ).
fof(f179,plain,
( sP6
| sP7
| sP8
| e20 != h2(e10)
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f184,plain,
e12 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f185,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f186,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f187,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f188,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f189,plain,
e10 != e11,
inference(cnf_transformation,[],[f7]) ).
fof(f206,plain,
e13 = op1(op1(e11,e11),op1(e11,e11)),
inference(cnf_transformation,[],[f12]) ).
fof(f207,plain,
e12 = op1(op1(op1(e11,e11),op1(e11,e11)),op1(e11,e11)),
inference(cnf_transformation,[],[f12]) ).
fof(f208,plain,
e10 = op1(e11,e11),
inference(cnf_transformation,[],[f12]) ).
fof(f210,plain,
( ~ sP29
| e12 = op1(e12,e11)
| e11 != op1(e12,e12) ),
inference(cnf_transformation,[],[f84]) ).
fof(f222,plain,
( ~ sP28
| e12 = op1(e12,op1(e12,e12)) ),
inference(cnf_transformation,[],[f85]) ).
fof(f228,plain,
( ~ sP27
| e10 = op1(e10,e13)
| op1(e10,e10) != e13 ),
inference(cnf_transformation,[],[f86]) ).
fof(f237,plain,
( ~ sP26
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f87]) ).
fof(f239,plain,
( ~ sP25
| e13 != op1(e12,e12)
| e12 != op1(e12,e13) ),
inference(cnf_transformation,[],[f88]) ).
fof(f244,plain,
( ~ sP25
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f88]) ).
fof(f249,plain,
( ~ sP24
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f89]) ).
fof(f251,plain,
( ~ sP23
| op1(e10,e10) != e13
| e10 != op1(e10,e13) ),
inference(cnf_transformation,[],[f90]) ).
fof(f255,plain,
( ~ sP23
| e11 = op1(e10,e11) ),
inference(cnf_transformation,[],[f90]) ).
fof(f261,plain,
( ~ sP22
| e11 = op1(e11,e11) ),
inference(cnf_transformation,[],[f91]) ).
fof(f268,plain,
( ~ sP21
| e11 = op1(e11,e12) ),
inference(cnf_transformation,[],[f92]) ).
fof(f274,plain,
( ~ sP20
| e11 = op1(e11,e13) ),
inference(cnf_transformation,[],[f93]) ).
fof(f280,plain,
( ~ sP19
| e12 = op1(e12,e10) ),
inference(cnf_transformation,[],[f94]) ).
fof(f284,plain,
( ~ sP18
| e10 != op1(e11,e11)
| e11 != op1(e11,e10) ),
inference(cnf_transformation,[],[f95]) ).
fof(f291,plain,
( ~ sP17
| e12 = op1(e12,e12) ),
inference(cnf_transformation,[],[f96]) ).
fof(f297,plain,
( ~ sP16
| e12 = op1(e13,e12) ),
inference(cnf_transformation,[],[f97]) ).
fof(f303,plain,
( ~ sP15
| e13 = op1(e10,e13) ),
inference(cnf_transformation,[],[f98]) ).
fof(f308,plain,
( ~ sP14
| e10 != op1(e11,e11)
| e11 != op1(e11,e10) ),
inference(cnf_transformation,[],[f99]) ).
fof(f316,plain,
( ~ sP13
| e13 = op1(e13,e12) ),
inference(cnf_transformation,[],[f100]) ).
fof(f325,plain,
( sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| op1(e10,e10) != e11
| e10 != op1(e10,e11) ),
inference(cnf_transformation,[],[f52]) ).
fof(f327,plain,
( sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f52]) ).
fof(f336,plain,
( sP27
| sP28
| sP29
| e10 = op1(e10,op1(e10,e10)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f339,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f341,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f342,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f345,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f346,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f347,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f350,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f351,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f352,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f353,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f354,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f355,plain,
op1(e10,e12) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f356,plain,
op1(e10,e11) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f358,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f360,plain,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f366,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f367,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f370,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f378,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f379,plain,
op1(e12,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f380,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f381,plain,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f383,plain,
op1(e10,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f384,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f386,plain,
( e13 = op1(e13,e13)
| e13 = op1(e13,e12)
| e13 = op1(e13,e11)
| e13 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f389,plain,
( e11 = op1(e13,e13)
| e11 = op1(e12,e13)
| e11 = op1(e11,e13)
| e11 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f391,plain,
( e10 = op1(e13,e13)
| e10 = op1(e12,e13)
| e10 = op1(e11,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f2]) ).
fof(f396,plain,
( e12 = op1(e12,e13)
| e12 = op1(e12,e12)
| e12 = op1(e12,e11)
| e12 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f397,plain,
( e11 = op1(e13,e12)
| e11 = op1(e12,e12)
| e11 = op1(e11,e12)
| e11 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f399,plain,
( e10 = op1(e13,e12)
| e10 = op1(e12,e12)
| e10 = op1(e11,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f2]) ).
fof(f401,plain,
( e13 = op1(e13,e11)
| e13 = op1(e12,e11)
| e13 = op1(e11,e11)
| e13 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f403,plain,
( e12 = op1(e13,e11)
| e12 = op1(e12,e11)
| e12 = op1(e11,e11)
| e12 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f404,plain,
( e12 = op1(e11,e13)
| e12 = op1(e11,e12)
| e12 = op1(e11,e11)
| e12 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f405,plain,
( e11 = op1(e13,e11)
| e11 = op1(e12,e11)
| e11 = op1(e11,e11)
| e11 = op1(e10,e11) ),
inference(cnf_transformation,[],[f2]) ).
fof(f408,plain,
( e10 = op1(e11,e13)
| e10 = op1(e11,e12)
| e10 = op1(e11,e11)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f412,plain,
( e12 = op1(e10,e13)
| e12 = op1(e10,e12)
| e12 = op1(e10,e11)
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[],[f2]) ).
fof(f416,plain,
( e10 = op1(e10,e13)
| e10 = op1(e10,e12)
| e10 = op1(e10,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f418,plain,
( e13 = op1(e13,e12)
| e12 = op1(e13,e12)
| e11 = op1(e13,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f422,plain,
( e13 = op1(e12,e12)
| e12 = op1(e12,e12)
| e11 = op1(e12,e12)
| e10 = op1(e12,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f424,plain,
( e13 = op1(e12,e10)
| e12 = op1(e12,e10)
| e11 = op1(e12,e10)
| e10 = op1(e12,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f425,plain,
( e13 = op1(e11,e13)
| e12 = op1(e11,e13)
| e11 = op1(e11,e13)
| e10 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f428,plain,
( e13 = op1(e11,e10)
| e12 = op1(e11,e10)
| e11 = op1(e11,e10)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f433,plain,
e23 = op2(op2(e21,e21),op2(e21,e21)),
inference(cnf_transformation,[],[f13]) ).
fof(f434,plain,
e22 = op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21)),
inference(cnf_transformation,[],[f13]) ).
fof(f435,plain,
e20 = op2(e21,e21),
inference(cnf_transformation,[],[f13]) ).
fof(f437,plain,
( ~ sP47
| e22 = op2(e22,e21)
| e21 != op2(e22,e22) ),
inference(cnf_transformation,[],[f102]) ).
fof(f449,plain,
( ~ sP46
| e22 = op2(e22,op2(e22,e22)) ),
inference(cnf_transformation,[],[f103]) ).
fof(f455,plain,
( ~ sP45
| e20 = op2(e20,e23)
| op2(e20,e20) != e23 ),
inference(cnf_transformation,[],[f104]) ).
fof(f464,plain,
( ~ sP44
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f105]) ).
fof(f466,plain,
( ~ sP43
| e23 != op2(e22,e22)
| e22 != op2(e22,e23) ),
inference(cnf_transformation,[],[f106]) ).
fof(f471,plain,
( ~ sP43
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f106]) ).
fof(f476,plain,
( ~ sP42
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f107]) ).
fof(f478,plain,
( ~ sP41
| op2(e20,e20) != e23
| e20 != op2(e20,e23) ),
inference(cnf_transformation,[],[f108]) ).
fof(f482,plain,
( ~ sP41
| e21 = op2(e20,e21) ),
inference(cnf_transformation,[],[f108]) ).
fof(f488,plain,
( ~ sP40
| e21 = op2(e21,e21) ),
inference(cnf_transformation,[],[f109]) ).
fof(f495,plain,
( ~ sP39
| e21 = op2(e21,e22) ),
inference(cnf_transformation,[],[f110]) ).
fof(f501,plain,
( ~ sP38
| e21 = op2(e21,e23) ),
inference(cnf_transformation,[],[f111]) ).
fof(f507,plain,
( ~ sP37
| e22 = op2(e22,e20) ),
inference(cnf_transformation,[],[f112]) ).
fof(f511,plain,
( ~ sP36
| e20 != op2(e21,e21)
| e21 != op2(e21,e20) ),
inference(cnf_transformation,[],[f113]) ).
fof(f518,plain,
( ~ sP35
| e22 = op2(e22,e22) ),
inference(cnf_transformation,[],[f114]) ).
fof(f524,plain,
( ~ sP34
| e22 = op2(e23,e22) ),
inference(cnf_transformation,[],[f115]) ).
fof(f530,plain,
( ~ sP33
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f116]) ).
fof(f535,plain,
( ~ sP32
| e20 != op2(e21,e21)
| e21 != op2(e21,e20) ),
inference(cnf_transformation,[],[f117]) ).
fof(f543,plain,
( ~ sP31
| e23 = op2(e23,e22) ),
inference(cnf_transformation,[],[f118]) ).
fof(f552,plain,
( sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| op2(e20,e20) != e21
| e20 != op2(e20,e21) ),
inference(cnf_transformation,[],[f71]) ).
fof(f554,plain,
( sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f71]) ).
fof(f563,plain,
( sP45
| sP46
| sP47
| e20 = op2(e20,op2(e20,e20)) ),
inference(cnf_transformation,[],[f71]) ).
fof(f564,plain,
e22 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f565,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f566,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f567,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f568,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f569,plain,
e20 != e21,
inference(cnf_transformation,[],[f8]) ).
fof(f570,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f572,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f574,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f575,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f578,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f579,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f580,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f583,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f584,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f585,plain,
op2(e21,e20) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f586,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f587,plain,
op2(e21,e20) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f591,plain,
op2(e20,e20) != op2(e20,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f593,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f597,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f600,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f603,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f607,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f610,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f612,plain,
op2(e22,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f613,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f614,plain,
op2(e21,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f616,plain,
op2(e20,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f617,plain,
op2(e20,e20) != op2(e21,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f618,plain,
( e23 = op2(e23,e23)
| e23 = op2(e22,e23)
| e23 = op2(e21,e23)
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f619,plain,
( e23 = op2(e23,e23)
| e23 = op2(e23,e22)
| e23 = op2(e23,e21)
| e23 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f624,plain,
( e20 = op2(e23,e23)
| e20 = op2(e22,e23)
| e20 = op2(e21,e23)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f625,plain,
( e20 = op2(e23,e23)
| e20 = op2(e23,e22)
| e20 = op2(e23,e21)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f628,plain,
( e22 = op2(e23,e22)
| e22 = op2(e22,e22)
| e22 = op2(e21,e22)
| e22 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f629,plain,
( e22 = op2(e22,e23)
| e22 = op2(e22,e22)
| e22 = op2(e22,e21)
| e22 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f630,plain,
( e21 = op2(e23,e22)
| e21 = op2(e22,e22)
| e21 = op2(e21,e22)
| e21 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f631,plain,
( e21 = op2(e22,e23)
| e21 = op2(e22,e22)
| e21 = op2(e22,e21)
| e21 = op2(e22,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f632,plain,
( e20 = op2(e23,e22)
| e20 = op2(e22,e22)
| e20 = op2(e21,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f4]) ).
fof(f634,plain,
( e23 = op2(e23,e21)
| e23 = op2(e22,e21)
| e23 = op2(e21,e21)
| e23 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f636,plain,
( e22 = op2(e23,e21)
| e22 = op2(e22,e21)
| e22 = op2(e21,e21)
| e22 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f638,plain,
( e21 = op2(e23,e21)
| e21 = op2(e22,e21)
| e21 = op2(e21,e21)
| e21 = op2(e20,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f641,plain,
( e20 = op2(e21,e23)
| e20 = op2(e21,e22)
| e20 = op2(e21,e21)
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f645,plain,
( e22 = op2(e20,e23)
| e22 = op2(e20,e22)
| e22 = op2(e20,e21)
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[],[f4]) ).
fof(f651,plain,
( e23 = op2(e23,e22)
| e22 = op2(e23,e22)
| e21 = op2(e23,e22)
| e20 = op2(e23,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f655,plain,
( e23 = op2(e22,e22)
| e22 = op2(e22,e22)
| e21 = op2(e22,e22)
| e20 = op2(e22,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f657,plain,
( e23 = op2(e22,e20)
| e22 = op2(e22,e20)
| e21 = op2(e22,e20)
| e20 = op2(e22,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f661,plain,
( e23 = op2(e21,e20)
| e22 = op2(e21,e20)
| e21 = op2(e21,e20)
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f666,plain,
op2(op2(e20,e20),op2(e20,e20)) = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f668,plain,
op2(e20,e20) = h1(e10),
inference(cnf_transformation,[],[f14]) ).
fof(f670,plain,
op2(op2(e21,e21),op2(e21,e21)) = h2(e13),
inference(cnf_transformation,[],[f15]) ).
fof(f671,plain,
op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21)) = h2(e12),
inference(cnf_transformation,[],[f15]) ).
fof(f672,plain,
op2(e21,e21) = h2(e10),
inference(cnf_transformation,[],[f15]) ).
fof(f673,plain,
e21 = h2(e11),
inference(cnf_transformation,[],[f15]) ).
fof(f676,plain,
op2(e22,e22) = h3(e10),
inference(cnf_transformation,[],[f16]) ).
fof(f680,plain,
op2(e23,e23) = h4(e10),
inference(cnf_transformation,[],[f17]) ).
tcf(c_62,plain,
( ~ sP8
| ( h2(e11) != e21 ) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_67,plain,
( ~ sP7
| ( h2(e12) != e22 ) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_72,plain,
( ~ sP6
| ( h2(e13) != e23 ) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_101,negated_conjecture,
( sP6
| sP7
| sP8
| ( h2(e10) != e20 )
| ( op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) )
| ( op2(h2(e13),h2(e12)) != h2(op1(e13,e12)) )
| ( op2(h2(e13),h2(e11)) != h2(op1(e13,e11)) )
| ( op2(h2(e13),h2(e10)) != h2(op1(e13,e10)) )
| ( op2(h2(e12),h2(e13)) != h2(op1(e12,e13)) )
| ( op2(h2(e12),h2(e12)) != h2(op1(e12,e12)) )
| ( op2(h2(e12),h2(e11)) != h2(op1(e12,e11)) )
| ( op2(h2(e12),h2(e10)) != h2(op1(e12,e10)) )
| ( op2(h2(e11),h2(e13)) != h2(op1(e11,e13)) )
| ( op2(h2(e11),h2(e12)) != h2(op1(e11,e12)) )
| ( op2(h2(e11),h2(e11)) != h2(op1(e11,e11)) )
| ( op2(h2(e11),h2(e10)) != h2(op1(e11,e10)) )
| ( op2(h2(e10),h2(e13)) != h2(op1(e10,e13)) )
| ( op2(h2(e10),h2(e12)) != h2(op1(e10,e12)) )
| ( op2(h2(e10),h2(e11)) != h2(op1(e10,e11)) )
| ( op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_113,plain,
e10 != e11,
inference(cnf_transformation,[],[f189]) ).
tcf(c_114,plain,
e10 != e12,
inference(cnf_transformation,[],[f188]) ).
tcf(c_115,plain,
e10 != e13,
inference(cnf_transformation,[],[f187]) ).
tcf(c_116,plain,
e11 != e12,
inference(cnf_transformation,[],[f186]) ).
tcf(c_117,plain,
e11 != e13,
inference(cnf_transformation,[],[f185]) ).
tcf(c_118,plain,
e12 != e13,
inference(cnf_transformation,[],[f184]) ).
tcf(c_135,plain,
op1(e11,e11) = e10,
inference(cnf_transformation,[],[f208]) ).
tcf(c_136,plain,
op1(op1(op1(e11,e11),op1(e11,e11)),op1(e11,e11)) = e12,
inference(cnf_transformation,[],[f207]) ).
tcf(c_137,plain,
op1(op1(e11,e11),op1(e11,e11)) = e13,
inference(cnf_transformation,[],[f206]) ).
tcf(c_143,plain,
( ( op1(e12,e11) = e12 )
| ~ sP29
| ( op1(e12,e12) != e11 ) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_147,plain,
( ( op1(e12,op1(e12,e12)) = e12 )
| ~ sP28 ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_156,plain,
( ( op1(e10,e13) = e10 )
| ~ sP27
| ( op1(e10,e10) != e13 ) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_160,plain,
( ( op1(e11,e10) = e10 )
| ~ sP26 ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_165,plain,
( ( op1(e10,e12) = e10 )
| ~ sP25 ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_169,plain,
( ~ sP25
| ( op1(e12,e12) != e12 ) ),
inference(cnf_transformation,[],[f683]) ).
tcf(c_170,plain,
( ~ sP25
| ( op1(e12,e13) != e12 )
| ( op1(e12,e12) != e13 ) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_172,plain,
( ( op1(e13,e10) = e10 )
| ~ sP24 ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_178,plain,
( ( op1(e10,e11) = e11 )
| ~ sP23 ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_182,plain,
( ~ sP23
| ( op1(e10,e13) != e10 )
| ( op1(e10,e10) != e13 ) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_184,plain,
( ( op1(e11,e11) = e11 )
| ~ sP22 ),
inference(cnf_transformation,[],[f261]) ).
tcf(c_186,plain,
( ~ sP22
| ( op1(e11,e11) != e11 ) ),
inference(cnf_transformation,[],[f686]) ).
tcf(c_189,plain,
( ( op1(e11,e12) = e11 )
| ~ sP21 ),
inference(cnf_transformation,[],[f268]) ).
tcf(c_195,plain,
( ( op1(e11,e13) = e11 )
| ~ sP20 ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_201,plain,
( ( op1(e12,e10) = e12 )
| ~ sP19 ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_209,plain,
( ~ sP18
| ( op1(e11,e11) != e10 )
| ( op1(e11,e10) != e11 ) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_214,plain,
( ( op1(e12,e12) = e12 )
| ~ sP17 ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_217,plain,
( ~ sP17
| ( op1(e12,e12) != e12 ) ),
inference(cnf_transformation,[],[f691]) ).
tcf(c_220,plain,
( ( op1(e13,e12) = e12 )
| ~ sP16 ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_226,plain,
( ( op1(e10,e13) = e13 )
| ~ sP15 ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_233,plain,
( ~ sP14
| ( op1(e11,e11) != e10 )
| ( op1(e11,e10) != e11 ) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_237,plain,
( ( op1(e13,e12) = e13 )
| ~ sP13 ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_248,plain,
( ~ sP12
| ( op1(e13,e13) != e13 ) ),
inference(cnf_transformation,[],[f696]) ).
tcf(c_249,plain,
( sP27
| sP28
| sP29
| ( op1(e10,op1(e10,e10)) = e10 ) ),
inference(cnf_transformation,[],[f336]) ).
tcf(c_257,plain,
( sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| ( op1(e10,e10) = e10 ) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_258,plain,
( sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| ( op1(e10,e10) != e10 ) ),
inference(cnf_transformation,[],[f697]) ).
tcf(c_259,plain,
( sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| ( op1(e10,e11) != e10 )
| ( op1(e10,e10) != e11 ) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_262,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f384]) ).
tcf(c_263,plain,
op1(e10,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f383]) ).
tcf(c_265,plain,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f381]) ).
tcf(c_266,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f380]) ).
tcf(c_267,plain,
op1(e12,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f379]) ).
tcf(c_268,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f378]) ).
tcf(c_276,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f370]) ).
tcf(c_279,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f367]) ).
tcf(c_280,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f366]) ).
tcf(c_286,plain,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f360]) ).
tcf(c_288,plain,
op1(e10,e10) != op1(e10,e13),
inference(cnf_transformation,[],[f358]) ).
tcf(c_290,plain,
op1(e10,e11) != op1(e10,e13),
inference(cnf_transformation,[],[f356]) ).
tcf(c_291,plain,
op1(e10,e12) != op1(e10,e13),
inference(cnf_transformation,[],[f355]) ).
tcf(c_292,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f354]) ).
tcf(c_293,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f353]) ).
tcf(c_294,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[],[f352]) ).
tcf(c_295,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[],[f351]) ).
tcf(c_296,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f350]) ).
tcf(c_299,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f347]) ).
tcf(c_300,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f346]) ).
tcf(c_301,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f345]) ).
tcf(c_304,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f342]) ).
tcf(c_305,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f341]) ).
tcf(c_307,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f339]) ).
tcf(c_310,plain,
( ( op1(e10,e13) = e10 )
| ( op1(e10,e12) = e10 )
| ( op1(e10,e11) = e10 )
| ( op1(e10,e10) = e10 ) ),
inference(cnf_transformation,[],[f416]) ).
tcf(c_314,plain,
( ( op1(e10,e13) = e12 )
| ( op1(e10,e12) = e12 )
| ( op1(e10,e11) = e12 )
| ( op1(e10,e10) = e12 ) ),
inference(cnf_transformation,[],[f412]) ).
tcf(c_318,plain,
( ( op1(e11,e13) = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e11,e10) = e10 ) ),
inference(cnf_transformation,[],[f408]) ).
tcf(c_321,plain,
( ( op1(e13,e11) = e11 )
| ( op1(e12,e11) = e11 )
| ( op1(e11,e11) = e11 )
| ( op1(e10,e11) = e11 ) ),
inference(cnf_transformation,[],[f405]) ).
tcf(c_322,plain,
( ( op1(e11,e13) = e12 )
| ( op1(e11,e12) = e12 )
| ( op1(e11,e11) = e12 )
| ( op1(e11,e10) = e12 ) ),
inference(cnf_transformation,[],[f404]) ).
tcf(c_323,plain,
( ( op1(e13,e11) = e12 )
| ( op1(e12,e11) = e12 )
| ( op1(e11,e11) = e12 )
| ( op1(e10,e11) = e12 ) ),
inference(cnf_transformation,[],[f403]) ).
tcf(c_325,plain,
( ( op1(e13,e11) = e13 )
| ( op1(e12,e11) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e10,e11) = e13 ) ),
inference(cnf_transformation,[],[f401]) ).
tcf(c_327,plain,
( ( op1(e13,e12) = e10 )
| ( op1(e12,e12) = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e10,e12) = e10 ) ),
inference(cnf_transformation,[],[f399]) ).
tcf(c_329,plain,
( ( op1(e13,e12) = e11 )
| ( op1(e12,e12) = e11 )
| ( op1(e11,e12) = e11 )
| ( op1(e10,e12) = e11 ) ),
inference(cnf_transformation,[],[f397]) ).
tcf(c_330,plain,
( ( op1(e12,e13) = e12 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e11) = e12 )
| ( op1(e12,e10) = e12 ) ),
inference(cnf_transformation,[],[f396]) ).
tcf(c_335,plain,
( ( op1(e13,e13) = e10 )
| ( op1(e12,e13) = e10 )
| ( op1(e11,e13) = e10 )
| ( op1(e10,e13) = e10 ) ),
inference(cnf_transformation,[],[f391]) ).
tcf(c_337,plain,
( ( op1(e13,e13) = e11 )
| ( op1(e12,e13) = e11 )
| ( op1(e11,e13) = e11 )
| ( op1(e10,e13) = e11 ) ),
inference(cnf_transformation,[],[f389]) ).
tcf(c_340,plain,
( ( op1(e13,e13) = e13 )
| ( op1(e13,e12) = e13 )
| ( op1(e13,e11) = e13 )
| ( op1(e13,e10) = e13 ) ),
inference(cnf_transformation,[],[f386]) ).
tcf(c_346,plain,
( ( op1(e11,e10) = e13 )
| ( op1(e11,e10) = e12 )
| ( op1(e11,e10) = e11 )
| ( op1(e11,e10) = e10 ) ),
inference(cnf_transformation,[],[f428]) ).
tcf(c_349,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e13) = e12 )
| ( op1(e11,e13) = e11 )
| ( op1(e11,e13) = e10 ) ),
inference(cnf_transformation,[],[f425]) ).
tcf(c_350,plain,
( ( op1(e12,e10) = e13 )
| ( op1(e12,e10) = e12 )
| ( op1(e12,e10) = e11 )
| ( op1(e12,e10) = e10 ) ),
inference(cnf_transformation,[],[f424]) ).
tcf(c_352,plain,
( ( op1(e12,e12) = e13 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e12) = e11 )
| ( op1(e12,e12) = e10 ) ),
inference(cnf_transformation,[],[f422]) ).
tcf(c_356,plain,
( ( op1(e13,e12) = e13 )
| ( op1(e13,e12) = e12 )
| ( op1(e13,e12) = e11 )
| ( op1(e13,e12) = e10 ) ),
inference(cnf_transformation,[],[f418]) ).
tcf(c_358,plain,
op2(e21,e21) = e20,
inference(cnf_transformation,[],[f435]) ).
tcf(c_359,plain,
op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21)) = e22,
inference(cnf_transformation,[],[f434]) ).
tcf(c_360,plain,
op2(op2(e21,e21),op2(e21,e21)) = e23,
inference(cnf_transformation,[],[f433]) ).
tcf(c_366,plain,
( ( op2(e22,e21) = e22 )
| ~ sP47
| ( op2(e22,e22) != e21 ) ),
inference(cnf_transformation,[],[f437]) ).
tcf(c_370,plain,
( ( op2(e22,op2(e22,e22)) = e22 )
| ~ sP46 ),
inference(cnf_transformation,[],[f449]) ).
tcf(c_379,plain,
( ( op2(e20,e23) = e20 )
| ~ sP45
| ( op2(e20,e20) != e23 ) ),
inference(cnf_transformation,[],[f455]) ).
tcf(c_383,plain,
( ( op2(e21,e20) = e20 )
| ~ sP44 ),
inference(cnf_transformation,[],[f464]) ).
tcf(c_388,plain,
( ( op2(e20,e22) = e20 )
| ~ sP43 ),
inference(cnf_transformation,[],[f471]) ).
tcf(c_392,plain,
( ~ sP43
| ( op2(e22,e22) != e22 ) ),
inference(cnf_transformation,[],[f699]) ).
tcf(c_393,plain,
( ~ sP43
| ( op2(e22,e23) != e22 )
| ( op2(e22,e22) != e23 ) ),
inference(cnf_transformation,[],[f466]) ).
tcf(c_395,plain,
( ( op2(e23,e20) = e20 )
| ~ sP42 ),
inference(cnf_transformation,[],[f476]) ).
tcf(c_401,plain,
( ( op2(e20,e21) = e21 )
| ~ sP41 ),
inference(cnf_transformation,[],[f482]) ).
tcf(c_405,plain,
( ~ sP41
| ( op2(e20,e20) != e23 )
| ( op2(e20,e23) != e20 ) ),
inference(cnf_transformation,[],[f478]) ).
tcf(c_407,plain,
( ( op2(e21,e21) = e21 )
| ~ sP40 ),
inference(cnf_transformation,[],[f488]) ).
tcf(c_409,plain,
( ~ sP40
| ( op2(e21,e21) != e21 ) ),
inference(cnf_transformation,[],[f702]) ).
tcf(c_412,plain,
( ( op2(e21,e22) = e21 )
| ~ sP39 ),
inference(cnf_transformation,[],[f495]) ).
tcf(c_418,plain,
( ( op2(e21,e23) = e21 )
| ~ sP38 ),
inference(cnf_transformation,[],[f501]) ).
tcf(c_424,plain,
( ( op2(e22,e20) = e22 )
| ~ sP37 ),
inference(cnf_transformation,[],[f507]) ).
tcf(c_432,plain,
( ~ sP36
| ( op2(e21,e20) != e21 )
| ( op2(e21,e21) != e20 ) ),
inference(cnf_transformation,[],[f511]) ).
tcf(c_437,plain,
( ( op2(e22,e22) = e22 )
| ~ sP35 ),
inference(cnf_transformation,[],[f518]) ).
tcf(c_440,plain,
( ~ sP35
| ( op2(e22,e22) != e22 ) ),
inference(cnf_transformation,[],[f707]) ).
tcf(c_443,plain,
( ( op2(e23,e22) = e22 )
| ~ sP34 ),
inference(cnf_transformation,[],[f524]) ).
tcf(c_449,plain,
( ( op2(e20,e23) = e23 )
| ~ sP33 ),
inference(cnf_transformation,[],[f530]) ).
tcf(c_456,plain,
( ~ sP32
| ( op2(e21,e20) != e21 )
| ( op2(e21,e21) != e20 ) ),
inference(cnf_transformation,[],[f535]) ).
tcf(c_460,plain,
( ( op2(e23,e22) = e23 )
| ~ sP31 ),
inference(cnf_transformation,[],[f543]) ).
tcf(c_471,plain,
( ~ sP30
| ( op2(e23,e23) != e23 ) ),
inference(cnf_transformation,[],[f712]) ).
tcf(c_472,plain,
( sP45
| sP46
| sP47
| ( op2(e20,op2(e20,e20)) = e20 ) ),
inference(cnf_transformation,[],[f563]) ).
tcf(c_480,plain,
( sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| ( op2(e20,e20) = e20 ) ),
inference(cnf_transformation,[],[f554]) ).
tcf(c_481,plain,
( sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| ( op2(e20,e20) != e20 ) ),
inference(cnf_transformation,[],[f713]) ).
tcf(c_482,plain,
( sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| ( op2(e20,e20) != e21 )
| ( op2(e20,e21) != e20 ) ),
inference(cnf_transformation,[],[f552]) ).
tcf(c_485,plain,
e21 != e20,
inference(cnf_transformation,[],[f569]) ).
tcf(c_486,plain,
e22 != e20,
inference(cnf_transformation,[],[f568]) ).
tcf(c_487,plain,
e23 != e20,
inference(cnf_transformation,[],[f567]) ).
tcf(c_488,plain,
e21 != e22,
inference(cnf_transformation,[],[f566]) ).
tcf(c_489,plain,
e21 != e23,
inference(cnf_transformation,[],[f565]) ).
tcf(c_490,plain,
e22 != e23,
inference(cnf_transformation,[],[f564]) ).
tcf(c_491,plain,
op2(e21,e20) != op2(e20,e20),
inference(cnf_transformation,[],[f617]) ).
tcf(c_492,plain,
op2(e22,e20) != op2(e20,e20),
inference(cnf_transformation,[],[f616]) ).
tcf(c_494,plain,
op2(e21,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f614]) ).
tcf(c_495,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f613]) ).
tcf(c_496,plain,
op2(e22,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f612]) ).
tcf(c_498,plain,
op2(e22,e21) != op2(e20,e21),
inference(cnf_transformation,[],[f610]) ).
tcf(c_501,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f607]) ).
tcf(c_505,plain,
op2(e23,e22) != op2(e20,e22),
inference(cnf_transformation,[],[f603]) ).
tcf(c_508,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f600]) ).
tcf(c_511,plain,
op2(e23,e23) != op2(e20,e23),
inference(cnf_transformation,[],[f597]) ).
tcf(c_515,plain,
op2(e20,e21) != op2(e20,e20),
inference(cnf_transformation,[],[f593]) ).
tcf(c_517,plain,
op2(e20,e23) != op2(e20,e20),
inference(cnf_transformation,[],[f591]) ).
tcf(c_521,plain,
op2(e21,e21) != op2(e21,e20),
inference(cnf_transformation,[],[f587]) ).
tcf(c_522,plain,
op2(e21,e22) != op2(e21,e20),
inference(cnf_transformation,[],[f586]) ).
tcf(c_523,plain,
op2(e21,e23) != op2(e21,e20),
inference(cnf_transformation,[],[f585]) ).
tcf(c_524,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f584]) ).
tcf(c_525,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f583]) ).
tcf(c_528,plain,
op2(e22,e22) != op2(e22,e20),
inference(cnf_transformation,[],[f580]) ).
tcf(c_529,plain,
op2(e22,e23) != op2(e22,e20),
inference(cnf_transformation,[],[f579]) ).
tcf(c_530,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f578]) ).
tcf(c_533,plain,
op2(e23,e21) != op2(e23,e20),
inference(cnf_transformation,[],[f575]) ).
tcf(c_534,plain,
op2(e23,e22) != op2(e23,e20),
inference(cnf_transformation,[],[f574]) ).
tcf(c_536,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f572]) ).
tcf(c_538,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f570]) ).
tcf(c_543,plain,
( ( op2(e20,e20) = e22 )
| ( op2(e20,e23) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e21) = e22 ) ),
inference(cnf_transformation,[],[f645]) ).
tcf(c_547,plain,
( ( op2(e21,e20) = e20 )
| ( op2(e21,e23) = e20 )
| ( op2(e21,e22) = e20 )
| ( op2(e21,e21) = e20 ) ),
inference(cnf_transformation,[],[f641]) ).
tcf(c_550,plain,
( ( op2(e20,e21) = e21 )
| ( op2(e23,e21) = e21 )
| ( op2(e22,e21) = e21 )
| ( op2(e21,e21) = e21 ) ),
inference(cnf_transformation,[],[f638]) ).
tcf(c_552,plain,
( ( op2(e20,e21) = e22 )
| ( op2(e23,e21) = e22 )
| ( op2(e22,e21) = e22 )
| ( op2(e21,e21) = e22 ) ),
inference(cnf_transformation,[],[f636]) ).
tcf(c_554,plain,
( ( op2(e20,e21) = e23 )
| ( op2(e23,e21) = e23 )
| ( op2(e22,e21) = e23 )
| ( op2(e21,e21) = e23 ) ),
inference(cnf_transformation,[],[f634]) ).
tcf(c_556,plain,
( ( op2(e20,e22) = e20 )
| ( op2(e23,e22) = e20 )
| ( op2(e22,e22) = e20 )
| ( op2(e21,e22) = e20 ) ),
inference(cnf_transformation,[],[f632]) ).
tcf(c_557,plain,
( ( op2(e22,e20) = e21 )
| ( op2(e22,e23) = e21 )
| ( op2(e22,e22) = e21 )
| ( op2(e22,e21) = e21 ) ),
inference(cnf_transformation,[],[f631]) ).
tcf(c_558,plain,
( ( op2(e20,e22) = e21 )
| ( op2(e23,e22) = e21 )
| ( op2(e22,e22) = e21 )
| ( op2(e21,e22) = e21 ) ),
inference(cnf_transformation,[],[f630]) ).
tcf(c_559,plain,
( ( op2(e22,e20) = e22 )
| ( op2(e22,e23) = e22 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e21) = e22 ) ),
inference(cnf_transformation,[],[f629]) ).
tcf(c_560,plain,
( ( op2(e20,e22) = e22 )
| ( op2(e23,e22) = e22 )
| ( op2(e22,e22) = e22 )
| ( op2(e21,e22) = e22 ) ),
inference(cnf_transformation,[],[f628]) ).
tcf(c_563,plain,
( ( op2(e23,e20) = e20 )
| ( op2(e23,e23) = e20 )
| ( op2(e23,e22) = e20 )
| ( op2(e23,e21) = e20 ) ),
inference(cnf_transformation,[],[f625]) ).
tcf(c_564,plain,
( ( op2(e20,e23) = e20 )
| ( op2(e23,e23) = e20 )
| ( op2(e22,e23) = e20 )
| ( op2(e21,e23) = e20 ) ),
inference(cnf_transformation,[],[f624]) ).
tcf(c_569,plain,
( ( op2(e23,e20) = e23 )
| ( op2(e23,e23) = e23 )
| ( op2(e23,e22) = e23 )
| ( op2(e23,e21) = e23 ) ),
inference(cnf_transformation,[],[f619]) ).
tcf(c_570,plain,
( ( op2(e20,e23) = e23 )
| ( op2(e23,e23) = e23 )
| ( op2(e22,e23) = e23 )
| ( op2(e21,e23) = e23 ) ),
inference(cnf_transformation,[],[f618]) ).
tcf(c_575,plain,
( ( op2(e21,e20) = e20 )
| ( op2(e21,e20) = e23 )
| ( op2(e21,e20) = e22 )
| ( op2(e21,e20) = e21 ) ),
inference(cnf_transformation,[],[f661]) ).
tcf(c_579,plain,
( ( op2(e22,e20) = e20 )
| ( op2(e22,e20) = e23 )
| ( op2(e22,e20) = e22 )
| ( op2(e22,e20) = e21 ) ),
inference(cnf_transformation,[],[f657]) ).
tcf(c_581,plain,
( ( op2(e22,e22) = e20 )
| ( op2(e22,e22) = e23 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e22) = e21 ) ),
inference(cnf_transformation,[],[f655]) ).
tcf(c_585,plain,
( ( op2(e23,e22) = e20 )
| ( op2(e23,e22) = e23 )
| ( op2(e23,e22) = e22 )
| ( op2(e23,e22) = e21 ) ),
inference(cnf_transformation,[],[f651]) ).
tcf(c_588,plain,
op2(e20,e20) = h1(e10),
inference(cnf_transformation,[],[f668]) ).
tcf(c_590,plain,
op2(op2(e20,e20),op2(e20,e20)) = h1(e13),
inference(cnf_transformation,[],[f666]) ).
tcf(c_591,plain,
h2(e11) = e21,
inference(cnf_transformation,[],[f673]) ).
tcf(c_592,plain,
op2(e21,e21) = h2(e10),
inference(cnf_transformation,[],[f672]) ).
tcf(c_593,plain,
op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21)) = h2(e12),
inference(cnf_transformation,[],[f671]) ).
tcf(c_594,plain,
op2(op2(e21,e21),op2(e21,e21)) = h2(e13),
inference(cnf_transformation,[],[f670]) ).
tcf(c_596,plain,
op2(e22,e22) = h3(e10),
inference(cnf_transformation,[],[f676]) ).
tcf(c_600,plain,
op2(e23,e23) = h4(e10),
inference(cnf_transformation,[],[f680]) ).
tcf(c_607,plain,
~ sP35,
inference(global_subsumption_just,[status(thm)],[c_437,c_437,c_440]) ).
tcf(c_611,plain,
~ sP40,
inference(global_subsumption_just,[status(thm)],[c_407,c_407,c_409]) ).
tcf(c_619,plain,
~ sP17,
inference(global_subsumption_just,[status(thm)],[c_214,c_214,c_217]) ).
tcf(c_623,plain,
~ sP22,
inference(global_subsumption_just,[status(thm)],[c_184,c_184,c_186]) ).
tcf(c_671,plain,
( ~ sP32
| ( op2(e21,e20) != e21 ) ),
inference(global_subsumption_just,[status(thm)],[c_456,c_358,c_456]) ).
tcf(c_679,plain,
( ~ sP36
| ( op2(e21,e20) != e21 ) ),
inference(global_subsumption_just,[status(thm)],[c_432,c_358,c_432]) ).
tcf(c_697,plain,
( ~ sP14
| ( op1(e11,e10) != e11 ) ),
inference(global_subsumption_just,[status(thm)],[c_233,c_135,c_233]) ).
tcf(c_705,plain,
( ~ sP18
| ( op1(e11,e10) != e11 ) ),
inference(global_subsumption_just,[status(thm)],[c_209,c_135,c_209]) ).
tcf(c_731,plain,
op2(e21,e21) = e20,
inference(global_subsumption_just,[status(thm)],[c_547,c_358]) ).
tcf(c_737,plain,
op1(e11,e11) = e10,
inference(global_subsumption_just,[status(thm)],[c_318,c_135]) ).
tcf(c_773,plain,
( sP6
| sP7
| ( op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) )
| ( op2(h2(e10),h2(e11)) != h2(op1(e10,e11)) )
| ( op2(h2(e10),h2(e12)) != h2(op1(e10,e12)) )
| ( op2(h2(e10),h2(e13)) != h2(op1(e10,e13)) )
| ( op2(h2(e11),h2(e10)) != h2(op1(e11,e10)) )
| ( op2(h2(e11),h2(e11)) != h2(op1(e11,e11)) )
| ( op2(h2(e11),h2(e12)) != h2(op1(e11,e12)) )
| ( op2(h2(e11),h2(e13)) != h2(op1(e11,e13)) )
| ( op2(h2(e12),h2(e10)) != h2(op1(e12,e10)) )
| ( op2(h2(e12),h2(e11)) != h2(op1(e12,e11)) )
| ( op2(h2(e12),h2(e12)) != h2(op1(e12,e12)) )
| ( op2(h2(e12),h2(e13)) != h2(op1(e12,e13)) )
| ( op2(h2(e13),h2(e10)) != h2(op1(e13,e10)) )
| ( op2(h2(e13),h2(e11)) != h2(op1(e13,e11)) )
| ( op2(h2(e13),h2(e12)) != h2(op1(e13,e12)) )
| ( op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) )
| ( h2(e10) != e20 ) ),
inference(global_subsumption_just,[status(thm)],[c_101,c_591,c_62,c_101]) ).
tcf(c_774,negated_conjecture,
( sP6
| sP7
| ( h2(e10) != e20 )
| ( op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) )
| ( op2(h2(e13),h2(e12)) != h2(op1(e13,e12)) )
| ( op2(h2(e13),h2(e11)) != h2(op1(e13,e11)) )
| ( op2(h2(e13),h2(e10)) != h2(op1(e13,e10)) )
| ( op2(h2(e12),h2(e13)) != h2(op1(e12,e13)) )
| ( op2(h2(e12),h2(e12)) != h2(op1(e12,e12)) )
| ( op2(h2(e12),h2(e11)) != h2(op1(e12,e11)) )
| ( op2(h2(e12),h2(e10)) != h2(op1(e12,e10)) )
| ( op2(h2(e11),h2(e13)) != h2(op1(e11,e13)) )
| ( op2(h2(e11),h2(e12)) != h2(op1(e11,e12)) )
| ( op2(h2(e11),h2(e11)) != h2(op1(e11,e11)) )
| ( op2(h2(e11),h2(e10)) != h2(op1(e11,e10)) )
| ( op2(h2(e10),h2(e13)) != h2(op1(e10,e13)) )
| ( op2(h2(e10),h2(e12)) != h2(op1(e10,e12)) )
| ( op2(h2(e10),h2(e11)) != h2(op1(e10,e11)) )
| ( op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ) ),
inference(renaming,[status(thm)],[c_773]) ).
tcf(c_3531,plain,
h2(e10) = e20,
inference(light_normalisation,[status(thm)],[c_592,c_731]) ).
tcf(c_3873,plain,
op2(e23,e22) != h4(e10),
inference(light_normalisation,[status(thm)],[c_538,c_600]) ).
tcf(c_3877,plain,
op2(e22,e21) != h3(e10),
inference(light_normalisation,[status(thm)],[c_530,c_596]) ).
tcf(c_3878,plain,
op2(e22,e20) != h3(e10),
inference(light_normalisation,[status(thm)],[c_528,c_596]) ).
tcf(c_3879,plain,
op2(e21,e23) != e20,
inference(light_normalisation,[status(thm)],[c_525,c_731]) ).
tcf(c_3880,plain,
op2(e21,e22) != e20,
inference(light_normalisation,[status(thm)],[c_524,c_731]) ).
tcf(c_3881,plain,
op2(e21,e20) != e20,
inference(light_normalisation,[status(thm)],[c_521,c_731]) ).
tcf(c_3882,plain,
~ sP44,
inference(backward_subsumption_resolution,[status(thm)],[c_383,c_3881]) ).
tcf(c_3883,plain,
op2(e20,e23) != h1(e10),
inference(light_normalisation,[status(thm)],[c_517,c_588]) ).
tcf(c_3885,plain,
op2(e20,e21) != h1(e10),
inference(light_normalisation,[status(thm)],[c_515,c_588]) ).
tcf(c_3888,plain,
op2(e20,e23) != h4(e10),
inference(light_normalisation,[status(thm)],[c_511,c_600]) ).
tcf(c_3889,plain,
op2(e23,e22) != h3(e10),
inference(light_normalisation,[status(thm)],[c_508,c_596]) ).
tcf(c_3892,plain,
op2(e23,e21) != e20,
inference(light_normalisation,[status(thm)],[c_501,c_731]) ).
tcf(c_3896,plain,
op2(e22,e20) != h1(e10),
inference(light_normalisation,[status(thm)],[c_492,c_588]) ).
tcf(c_3897,plain,
op2(e21,e20) != h1(e10),
inference(light_normalisation,[status(thm)],[c_491,c_588]) ).
tcf(c_3956,plain,
( ~ sP43
| ( h3(e10) != e22 ) ),
inference(light_normalisation,[status(thm)],[c_392,c_596]) ).
tcf(c_3963,plain,
op1(e11,e13) != e10,
inference(light_normalisation,[status(thm)],[c_296,c_737]) ).
tcf(c_3964,plain,
op1(e11,e12) != e10,
inference(light_normalisation,[status(thm)],[c_295,c_737]) ).
tcf(c_3965,plain,
op1(e11,e10) != e10,
inference(light_normalisation,[status(thm)],[c_292,c_737]) ).
tcf(c_3966,plain,
~ sP26,
inference(backward_subsumption_resolution,[status(thm)],[c_160,c_3965]) ).
tcf(c_3969,plain,
op1(e10,e11) != e10,
inference(light_normalisation,[status(thm)],[c_268,c_737]) ).
tcf(c_4031,plain,
( ( op2(e22,h3(e10)) = e22 )
| ~ sP46 ),
inference(light_normalisation,[status(thm)],[c_370,c_596]) ).
tcf(c_4072,plain,
h1(e10) = e23,
inference(light_normalisation,[status(thm)],[c_360,c_731,c_588]) ).
tcf(c_4076,plain,
op2(e21,e20) != e23,
inference(demodulation,[status(thm)],[c_3897,c_4072]) ).
tcf(c_4077,plain,
op2(e22,e20) != e23,
inference(demodulation,[status(thm)],[c_3896,c_4072]) ).
tcf(c_4079,plain,
op2(e20,e21) != e23,
inference(demodulation,[status(thm)],[c_3885,c_4072]) ).
tcf(c_4081,plain,
op2(e20,e23) != e23,
inference(demodulation,[status(thm)],[c_3883,c_4072]) ).
tcf(c_4085,plain,
op2(e20,e20) = e23,
inference(demodulation,[status(thm)],[c_588,c_4072]) ).
tcf(c_4087,plain,
~ sP33,
inference(backward_subsumption_resolution,[status(thm)],[c_449,c_4081]) ).
tcf(c_4146,plain,
op1(e10,e10) = e13,
inference(light_normalisation,[status(thm)],[c_137,c_737]) ).
tcf(c_4150,plain,
op1(e11,e10) != e13,
inference(demodulation,[status(thm)],[c_262,c_4146]) ).
tcf(c_4151,plain,
op1(e12,e10) != e13,
inference(demodulation,[status(thm)],[c_263,c_4146]) ).
tcf(c_4153,plain,
op1(e10,e11) != e13,
inference(demodulation,[status(thm)],[c_286,c_4146]) ).
tcf(c_4155,plain,
op1(e10,e13) != e13,
inference(demodulation,[status(thm)],[c_288,c_4146]) ).
tcf(c_4156,plain,
~ sP15,
inference(backward_subsumption_resolution,[status(thm)],[c_226,c_4155]) ).
tcf(c_4159,plain,
h2(e13) = e23,
inference(light_normalisation,[status(thm)],[c_594,c_731,c_4085]) ).
tcf(c_4161,plain,
( ~ sP6
| ( e23 != e23 ) ),
inference(demodulation,[status(thm)],[c_72,c_4159]) ).
tcf(c_4162,plain,
~ sP6,
inference(equality_resolution_simp,[status(thm)],[c_4161]) ).
tcf(c_4163,plain,
h1(e13) = h4(e10),
inference(light_normalisation,[status(thm)],[c_590,c_600,c_4085]) ).
tcf(c_4169,plain,
op2(e20,e23) != h1(e13),
inference(demodulation,[status(thm)],[c_3888,c_4163]) ).
tcf(c_4174,plain,
op2(e23,e22) != h1(e13),
inference(demodulation,[status(thm)],[c_3873,c_4163]) ).
tcf(c_4177,plain,
op2(e23,e23) = h1(e13),
inference(demodulation,[status(thm)],[c_600,c_4163]) ).
tcf(c_4226,plain,
( sP45
| sP46
| sP47
| ( op2(e20,e23) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_472,c_4085]) ).
tcf(c_4263,plain,
( sP27
| sP28
| sP29
| ( op1(e10,e13) = e10 ) ),
inference(light_normalisation,[status(thm)],[c_249,c_4146]) ).
tcf(c_4338,plain,
op2(e23,e20) = e22,
inference(light_normalisation,[status(thm)],[c_359,c_731,c_4085]) ).
tcf(c_4342,plain,
op2(e21,e20) != e22,
inference(demodulation,[status(thm)],[c_495,c_4338]) ).
tcf(c_4343,plain,
op2(e22,e20) != e22,
inference(demodulation,[status(thm)],[c_496,c_4338]) ).
tcf(c_4344,plain,
op2(e23,e21) != e22,
inference(demodulation,[status(thm)],[c_533,c_4338]) ).
tcf(c_4345,plain,
op2(e23,e22) != e22,
inference(demodulation,[status(thm)],[c_534,c_4338]) ).
tcf(c_4346,plain,
( ( e22 = e20 )
| ~ sP42 ),
inference(demodulation,[status(thm)],[c_395,c_4338]) ).
tcf(c_4347,plain,
~ sP42,
inference(forward_subsumption_resolution,[status(thm)],[c_4346,c_486]) ).
tcf(c_4367,plain,
~ sP34,
inference(backward_subsumption_resolution,[status(thm)],[c_443,c_4345]) ).
tcf(c_4385,plain,
~ sP37,
inference(backward_subsumption_resolution,[status(thm)],[c_424,c_4343]) ).
tcf(c_4405,plain,
op1(e13,e10) = e12,
inference(light_normalisation,[status(thm)],[c_136,c_737,c_4146]) ).
tcf(c_4408,plain,
op1(e11,e10) != e12,
inference(demodulation,[status(thm)],[c_266,c_4405]) ).
tcf(c_4409,plain,
op1(e12,e10) != e12,
inference(demodulation,[status(thm)],[c_267,c_4405]) ).
tcf(c_4410,plain,
op1(e13,e11) != e12,
inference(demodulation,[status(thm)],[c_304,c_4405]) ).
tcf(c_4411,plain,
op1(e13,e12) != e12,
inference(demodulation,[status(thm)],[c_305,c_4405]) ).
tcf(c_4413,plain,
( ( e10 = e12 )
| ~ sP24 ),
inference(demodulation,[status(thm)],[c_172,c_4405]) ).
tcf(c_4414,plain,
~ sP24,
inference(forward_subsumption_resolution,[status(thm)],[c_4413,c_114]) ).
tcf(c_4434,plain,
~ sP16,
inference(backward_subsumption_resolution,[status(thm)],[c_220,c_4411]) ).
tcf(c_4452,plain,
~ sP19,
inference(backward_subsumption_resolution,[status(thm)],[c_201,c_4409]) ).
tcf(c_4474,plain,
h2(e12) = e22,
inference(light_normalisation,[status(thm)],[c_593,c_731,c_4085,c_4338]) ).
tcf(c_4475,plain,
( ~ sP7
| ( e22 != e22 ) ),
inference(demodulation,[status(thm)],[c_67,c_4474]) ).
tcf(c_4476,plain,
~ sP7,
inference(equality_resolution_simp,[status(thm)],[c_4475]) ).
tcf(c_4489,plain,
( ( op2(e20,e23) = e20 )
| ~ sP45
| ( e23 != e23 ) ),
inference(demodulation,[status(thm)],[c_379,c_4085]) ).
tcf(c_4490,plain,
( ( op2(e20,e23) = e20 )
| ~ sP45 ),
inference(equality_resolution_simp,[status(thm)],[c_4489]) ).
tcf(c_4497,plain,
( sP46
| sP47
| ( op2(e20,e23) = e20 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4226,c_4490]) ).
tcf(c_4517,plain,
( ( op2(e22,e21) = e22 )
| ~ sP47
| ( h3(e10) != e21 ) ),
inference(light_normalisation,[status(thm)],[c_366,c_596]) ).
tcf(c_4535,plain,
( ( op1(e10,e13) = e10 )
| ~ sP27
| ( e13 != e13 ) ),
inference(demodulation,[status(thm)],[c_156,c_4146]) ).
tcf(c_4536,plain,
( ( op1(e10,e13) = e10 )
| ~ sP27 ),
inference(equality_resolution_simp,[status(thm)],[c_4535]) ).
tcf(c_4543,plain,
( sP28
| sP29
| ( op1(e10,e13) = e10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4263,c_4536]) ).
tcf(c_4649,plain,
( ~ sP41
| ( e23 != e23 )
| ( op2(e20,e23) != e20 ) ),
inference(demodulation,[status(thm)],[c_405,c_4085]) ).
tcf(c_4650,plain,
( ~ sP41
| ( op2(e20,e23) != e20 ) ),
inference(equality_resolution_simp,[status(thm)],[c_4649]) ).
tcf(c_4658,plain,
( ~ sP43
| ( h3(e10) != e23 )
| ( op2(e22,e23) != e22 ) ),
inference(light_normalisation,[status(thm)],[c_393,c_596]) ).
tcf(c_4740,plain,
( ~ sP23
| ( e13 != e13 )
| ( op1(e10,e13) != e10 ) ),
inference(demodulation,[status(thm)],[c_182,c_4146]) ).
tcf(c_4741,plain,
( ~ sP23
| ( op1(e10,e13) != e10 ) ),
inference(equality_resolution_simp,[status(thm)],[c_4740]) ).
tcf(c_4772,plain,
( ( op2(e23,e22) = e20 )
| ( op2(e23,e22) = e23 )
| ( op2(e23,e22) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_585,c_4345]) ).
tcf(c_4797,plain,
( ( h3(e10) = e20 )
| ( h3(e10) = e23 )
| ( h3(e10) = e22 )
| ( h3(e10) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_581,c_596]) ).
tcf(c_4820,plain,
( ( op2(e22,e20) = e20 )
| ( op2(e22,e20) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_579,c_4077,c_4343]) ).
tcf(c_4847,plain,
op2(e21,e20) = e21,
inference(forward_subsumption_resolution,[status(thm)],[c_575,c_3881,c_4076,c_4342]) ).
tcf(c_4852,plain,
op2(e22,e20) != e21,
inference(demodulation,[status(thm)],[c_494,c_4847]) ).
tcf(c_4854,plain,
op2(e21,e22) != e21,
inference(demodulation,[status(thm)],[c_522,c_4847]) ).
tcf(c_4855,plain,
op2(e21,e23) != e21,
inference(demodulation,[status(thm)],[c_523,c_4847]) ).
tcf(c_4856,plain,
( ~ sP32
| ( e21 != e21 ) ),
inference(demodulation,[status(thm)],[c_671,c_4847]) ).
tcf(c_4857,plain,
( ~ sP36
| ( e21 != e21 ) ),
inference(demodulation,[status(thm)],[c_679,c_4847]) ).
tcf(c_4859,plain,
~ sP36,
inference(equality_resolution_simp,[status(thm)],[c_4857]) ).
tcf(c_4873,plain,
~ sP32,
inference(equality_resolution_simp,[status(thm)],[c_4856]) ).
tcf(c_4886,plain,
~ sP38,
inference(backward_subsumption_resolution,[status(thm)],[c_418,c_4855]) ).
tcf(c_4901,plain,
~ sP39,
inference(backward_subsumption_resolution,[status(thm)],[c_412,c_4854]) ).
tcf(c_4913,plain,
op2(e22,e20) = e20,
inference(backward_subsumption_resolution,[status(thm)],[c_4820,c_4852]) ).
tcf(c_4919,plain,
h3(e10) != e20,
inference(demodulation,[status(thm)],[c_3878,c_4913]) ).
tcf(c_4920,plain,
op2(e22,e23) != e20,
inference(demodulation,[status(thm)],[c_529,c_4913]) ).
tcf(c_4929,plain,
( ( h3(e10) = e23 )
| ( h3(e10) = e22 )
| ( h3(e10) = e21 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4797,c_4919]) ).
tcf(c_4963,plain,
( ( h1(e13) = e23 )
| ( op2(e20,e23) = e23 )
| ( op2(e22,e23) = e23 )
| ( op2(e21,e23) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_570,c_4177]) ).
tcf(c_4964,plain,
( ( h1(e13) = e23 )
| ( op2(e22,e23) = e23 )
| ( op2(e21,e23) = e23 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4963,c_4081]) ).
tcf(c_4974,plain,
( ( e22 = e23 )
| ( h1(e13) = e23 )
| ( op2(e23,e22) = e23 )
| ( op2(e23,e21) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_569,c_4177,c_4338]) ).
tcf(c_4975,plain,
( ( h1(e13) = e23 )
| ( op2(e23,e22) = e23 )
| ( op2(e23,e21) = e23 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4974,c_490]) ).
tcf(c_5018,plain,
( ( h1(e13) = e20 )
| ( op2(e20,e23) = e20 )
| ( op2(e22,e23) = e20 )
| ( op2(e21,e23) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_564,c_4177]) ).
tcf(c_5019,plain,
( ( h1(e13) = e20 )
| ( op2(e20,e23) = e20 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5018,c_4920,c_3879]) ).
tcf(c_5026,plain,
( ( e22 = e20 )
| ( h1(e13) = e20 )
| ( op2(e23,e22) = e20 )
| ( op2(e23,e21) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_563,c_4177,c_4338]) ).
tcf(c_5027,plain,
( ( h1(e13) = e20 )
| ( op2(e23,e22) = e20 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5026,c_486,c_3892]) ).
tcf(c_5056,plain,
( ( h3(e10) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e23,e22) = e22 )
| ( op2(e21,e22) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_560,c_596]) ).
tcf(c_5057,plain,
( ( h3(e10) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e21,e22) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5056,c_4345]) ).
tcf(c_5067,plain,
( ( e22 = e20 )
| ( h3(e10) = e22 )
| ( op2(e22,e23) = e22 )
| ( op2(e22,e21) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_559,c_596,c_4913]) ).
tcf(c_5068,plain,
( ( h3(e10) = e22 )
| ( op2(e22,e23) = e22 )
| ( op2(e22,e21) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5067,c_486]) ).
tcf(c_5078,plain,
( ( h3(e10) = e21 )
| ( op2(e20,e22) = e21 )
| ( op2(e23,e22) = e21 )
| ( op2(e21,e22) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_558,c_596]) ).
tcf(c_5079,plain,
( ( h3(e10) = e21 )
| ( op2(e20,e22) = e21 )
| ( op2(e23,e22) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5078,c_4854]) ).
tcf(c_5089,plain,
( ( e21 = e20 )
| ( h3(e10) = e21 )
| ( op2(e22,e23) = e21 )
| ( op2(e22,e21) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_557,c_596,c_4913]) ).
tcf(c_5090,plain,
( ( h3(e10) = e21 )
| ( op2(e22,e23) = e21 )
| ( op2(e22,e21) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5089,c_485]) ).
tcf(c_5100,plain,
( ( h3(e10) = e20 )
| ( op2(e20,e22) = e20 )
| ( op2(e23,e22) = e20 )
| ( op2(e21,e22) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_556,c_596]) ).
tcf(c_5101,plain,
( ( op2(e20,e22) = e20 )
| ( op2(e23,e22) = e20 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5100,c_4919,c_3880]) ).
tcf(c_5108,plain,
( ( e23 = e20 )
| ( op2(e20,e21) = e23 )
| ( op2(e23,e21) = e23 )
| ( op2(e22,e21) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_554,c_731]) ).
tcf(c_5109,plain,
( ( op2(e23,e21) = e23 )
| ( op2(e22,e21) = e23 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5108,c_487,c_4079]) ).
tcf(c_5124,plain,
( ( e22 = e20 )
| ( op2(e20,e21) = e22 )
| ( op2(e23,e21) = e22 )
| ( op2(e22,e21) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_552,c_731]) ).
tcf(c_5125,plain,
( ( op2(e20,e21) = e22 )
| ( op2(e22,e21) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5124,c_486,c_4344]) ).
tcf(c_5140,plain,
( ( e21 = e20 )
| ( op2(e20,e21) = e21 )
| ( op2(e23,e21) = e21 )
| ( op2(e22,e21) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_550,c_731]) ).
tcf(c_5141,plain,
( ( op2(e20,e21) = e21 )
| ( op2(e23,e21) = e21 )
| ( op2(e22,e21) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5140,c_485]) ).
tcf(c_5151,plain,
( ( e22 = e23 )
| ( op2(e20,e23) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e21) = e22 ) ),
inference(light_normalisation,[status(thm)],[c_543,c_4085]) ).
tcf(c_5152,plain,
( ( op2(e20,e23) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e21) = e22 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5151,c_490]) ).
tcf(c_5191,plain,
( ( op1(e13,e12) = e13 )
| ( op1(e13,e12) = e11 )
| ( op1(e13,e12) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_356,c_4411]) ).
tcf(c_5234,plain,
( ( op1(e12,e10) = e11 )
| ( op1(e12,e10) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_350,c_4151,c_4409]) ).
tcf(c_5241,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e13) = e12 )
| ( op1(e11,e13) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_349,c_3963]) ).
tcf(c_5261,plain,
op1(e11,e10) = e11,
inference(forward_subsumption_resolution,[status(thm)],[c_346,c_4150,c_4408,c_3965]) ).
tcf(c_5266,plain,
op1(e12,e10) != e11,
inference(demodulation,[status(thm)],[c_265,c_5261]) ).
tcf(c_5268,plain,
op1(e11,e12) != e11,
inference(demodulation,[status(thm)],[c_293,c_5261]) ).
tcf(c_5269,plain,
op1(e11,e13) != e11,
inference(demodulation,[status(thm)],[c_294,c_5261]) ).
tcf(c_5270,plain,
( ~ sP14
| ( e11 != e11 ) ),
inference(demodulation,[status(thm)],[c_697,c_5261]) ).
tcf(c_5271,plain,
( ~ sP18
| ( e11 != e11 ) ),
inference(demodulation,[status(thm)],[c_705,c_5261]) ).
tcf(c_5273,plain,
~ sP18,
inference(equality_resolution_simp,[status(thm)],[c_5271]) ).
tcf(c_5287,plain,
~ sP14,
inference(equality_resolution_simp,[status(thm)],[c_5270]) ).
tcf(c_5299,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e13) = e12 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5241,c_5269]) ).
tcf(c_5300,plain,
~ sP20,
inference(backward_subsumption_resolution,[status(thm)],[c_195,c_5269]) ).
tcf(c_5315,plain,
~ sP21,
inference(backward_subsumption_resolution,[status(thm)],[c_189,c_5268]) ).
tcf(c_5327,plain,
op1(e12,e10) = e10,
inference(backward_subsumption_resolution,[status(thm)],[c_5234,c_5266]) ).
tcf(c_5333,plain,
op1(e12,e12) != e10,
inference(demodulation,[status(thm)],[c_299,c_5327]) ).
tcf(c_5334,plain,
op1(e12,e13) != e10,
inference(demodulation,[status(thm)],[c_300,c_5327]) ).
tcf(c_5343,plain,
( ( op1(e12,e12) = e13 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e12) = e11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_352,c_5333]) ).
tcf(c_5387,plain,
( ( e12 = e13 )
| ( op1(e13,e13) = e13 )
| ( op1(e13,e12) = e13 )
| ( op1(e13,e11) = e13 ) ),
inference(light_normalisation,[status(thm)],[c_340,c_4405]) ).
tcf(c_5388,plain,
( ( op1(e13,e13) = e13 )
| ( op1(e13,e12) = e13 )
| ( op1(e13,e11) = e13 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5387,c_118]) ).
tcf(c_5408,plain,
( ( op1(e13,e13) = e11 )
| ( op1(e12,e13) = e11 )
| ( op1(e10,e13) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_337,c_5269]) ).
tcf(c_5429,plain,
( ( op1(e13,e13) = e10 )
| ( op1(e10,e13) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_335,c_5334,c_3963]) ).
tcf(c_5475,plain,
( ( e10 = e12 )
| ( op1(e12,e13) = e12 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e11) = e12 ) ),
inference(light_normalisation,[status(thm)],[c_330,c_5327]) ).
tcf(c_5476,plain,
( ( op1(e12,e13) = e12 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e11) = e12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5475,c_114]) ).
tcf(c_5486,plain,
( ( op1(e13,e12) = e11 )
| ( op1(e12,e12) = e11 )
| ( op1(e10,e12) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_329,c_5268]) ).
tcf(c_5507,plain,
( ( op1(e13,e12) = e10 )
| ( op1(e10,e12) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_327,c_5333,c_3964]) ).
tcf(c_5514,plain,
( ( e10 = e13 )
| ( op1(e13,e11) = e13 )
| ( op1(e12,e11) = e13 )
| ( op1(e10,e11) = e13 ) ),
inference(light_normalisation,[status(thm)],[c_325,c_737]) ).
tcf(c_5515,plain,
( ( op1(e13,e11) = e13 )
| ( op1(e12,e11) = e13 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5514,c_115,c_4153]) ).
tcf(c_5530,plain,
( ( e10 = e12 )
| ( op1(e13,e11) = e12 )
| ( op1(e12,e11) = e12 )
| ( op1(e10,e11) = e12 ) ),
inference(light_normalisation,[status(thm)],[c_323,c_737]) ).
tcf(c_5531,plain,
( ( op1(e12,e11) = e12 )
| ( op1(e10,e11) = e12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5530,c_114,c_4410]) ).
tcf(c_5538,plain,
( ( e11 = e12 )
| ( e10 = e12 )
| ( op1(e11,e13) = e12 )
| ( op1(e11,e12) = e12 ) ),
inference(light_normalisation,[status(thm)],[c_322,c_737,c_5261]) ).
tcf(c_5539,plain,
( ( op1(e11,e13) = e12 )
| ( op1(e11,e12) = e12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5538,c_116,c_114]) ).
tcf(c_5546,plain,
( ( e10 = e11 )
| ( op1(e13,e11) = e11 )
| ( op1(e12,e11) = e11 )
| ( op1(e10,e11) = e11 ) ),
inference(light_normalisation,[status(thm)],[c_321,c_737]) ).
tcf(c_5547,plain,
( ( op1(e13,e11) = e11 )
| ( op1(e12,e11) = e11 )
| ( op1(e10,e11) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5546,c_113]) ).
tcf(c_5557,plain,
( ( e12 = e13 )
| ( op1(e10,e13) = e12 )
| ( op1(e10,e12) = e12 )
| ( op1(e10,e11) = e12 ) ),
inference(light_normalisation,[status(thm)],[c_314,c_4146]) ).
tcf(c_5558,plain,
( ( op1(e10,e13) = e12 )
| ( op1(e10,e12) = e12 )
| ( op1(e10,e11) = e12 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5557,c_118]) ).
tcf(c_5579,plain,
( ( e10 = e13 )
| ( op1(e10,e13) = e10 )
| ( op1(e10,e12) = e10 )
| ( op1(e10,e11) = e10 ) ),
inference(light_normalisation,[status(thm)],[c_310,c_4146]) ).
tcf(c_5580,plain,
( ( op1(e10,e13) = e10 )
| ( op1(e10,e12) = e10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5579,c_115,c_3969]) ).
tcf(c_5635,plain,
( sP6
| sP7
| ( e20 != e20 )
| ( e23 != e23 )
| ( e22 != e22 )
| ( e21 != e21 )
| ( h2(e10) != e20 )
| ( h2(op1(e13,e13)) != h1(e13) )
| ( h2(op1(e13,e12)) != op2(e23,e22) )
| ( h2(op1(e13,e11)) != op2(e23,e21) )
| ( h2(op1(e12,e13)) != op2(e22,e23) )
| ( h2(op1(e12,e12)) != h3(e10) )
| ( h2(op1(e12,e11)) != op2(e22,e21) )
| ( h2(op1(e11,e13)) != op2(e21,e23) )
| ( h2(op1(e11,e12)) != op2(e21,e22) )
| ( h2(op1(e10,e13)) != op2(e20,e23) )
| ( h2(op1(e10,e12)) != op2(e20,e22) )
| ( h2(op1(e10,e11)) != op2(e20,e21) ) ),
inference(light_normalisation,[status(thm)],[c_774,c_737,c_731,c_591,c_596,c_3531,c_4085,c_4146,c_4159,c_4177,c_4338,c_4405,c_4474,c_4847,c_4913,c_5261,c_5327]) ).
tcf(c_5636,plain,
( sP6
| sP7
| ( h2(e10) != e20 )
| ( h2(op1(e13,e13)) != h1(e13) )
| ( h2(op1(e13,e12)) != op2(e23,e22) )
| ( h2(op1(e13,e11)) != op2(e23,e21) )
| ( h2(op1(e12,e13)) != op2(e22,e23) )
| ( h2(op1(e12,e12)) != h3(e10) )
| ( h2(op1(e12,e11)) != op2(e22,e21) )
| ( h2(op1(e11,e13)) != op2(e21,e23) )
| ( h2(op1(e11,e12)) != op2(e21,e22) )
| ( h2(op1(e10,e13)) != op2(e20,e23) )
| ( h2(op1(e10,e12)) != op2(e20,e22) )
| ( h2(op1(e10,e11)) != op2(e20,e21) ) ),
inference(equality_resolution_simp,[status(thm)],[c_5635]) ).
tcf(c_5637,plain,
( sP6
| sP7
| ( e20 != e20 )
| ( h2(op1(e13,e13)) != h1(e13) )
| ( h2(op1(e13,e12)) != op2(e23,e22) )
| ( h2(op1(e13,e11)) != op2(e23,e21) )
| ( h2(op1(e12,e13)) != op2(e22,e23) )
| ( h2(op1(e12,e12)) != h3(e10) )
| ( h2(op1(e12,e11)) != op2(e22,e21) )
| ( h2(op1(e11,e13)) != op2(e21,e23) )
| ( h2(op1(e11,e12)) != op2(e21,e22) )
| ( h2(op1(e10,e13)) != op2(e20,e23) )
| ( h2(op1(e10,e12)) != op2(e20,e22) )
| ( h2(op1(e10,e11)) != op2(e20,e21) ) ),
inference(demodulation,[status(thm)],[c_5636,c_3531]) ).
tcf(c_5638,plain,
( sP6
| sP7
| ( h2(op1(e13,e13)) != h1(e13) )
| ( h2(op1(e13,e12)) != op2(e23,e22) )
| ( h2(op1(e13,e11)) != op2(e23,e21) )
| ( h2(op1(e12,e13)) != op2(e22,e23) )
| ( h2(op1(e12,e12)) != h3(e10) )
| ( h2(op1(e12,e11)) != op2(e22,e21) )
| ( h2(op1(e11,e13)) != op2(e21,e23) )
| ( h2(op1(e11,e12)) != op2(e21,e22) )
| ( h2(op1(e10,e13)) != op2(e20,e23) )
| ( h2(op1(e10,e12)) != op2(e20,e22) )
| ( h2(op1(e10,e11)) != op2(e20,e21) ) ),
inference(equality_resolution_simp,[status(thm)],[c_5637]) ).
tcf(c_5639,plain,
( ( h2(op1(e13,e13)) != h1(e13) )
| ( h2(op1(e13,e12)) != op2(e23,e22) )
| ( h2(op1(e13,e11)) != op2(e23,e21) )
| ( h2(op1(e12,e13)) != op2(e22,e23) )
| ( h2(op1(e12,e12)) != h3(e10) )
| ( h2(op1(e12,e11)) != op2(e22,e21) )
| ( h2(op1(e11,e13)) != op2(e21,e23) )
| ( h2(op1(e11,e12)) != op2(e21,e22) )
| ( h2(op1(e10,e13)) != op2(e20,e23) )
| ( h2(op1(e10,e12)) != op2(e20,e22) )
| ( h2(op1(e10,e11)) != op2(e20,e21) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5638,c_4162,c_4476]) ).
fof(f34,definition,
( ~ sP12
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e13) = e13
& op1(e13,e13) = e13 ) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ~ sP13
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e13) = e13
& op1(e13,e12) = e13 ) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ~ sP14
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e13) = e13
& op1(e13,e11) = e13 ) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ~ sP15
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e13) = e13
& op1(e13,e10) = e13 ) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ~ sP16
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e12) = e12
& op1(e12,e13) = e12 ) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ~ sP17
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e12) = e12
& op1(e12,e12) = e12 ) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ~ sP18
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e12) = e12
& op1(e12,e11) = e12 ) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ~ sP19
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e12) = e12
& op1(e12,e10) = e12 ) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ~ sP20
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e11) = e11
& op1(e11,e13) = e11 ) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f43,definition,
( ~ sP21
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e11) = e11
& op1(e11,e12) = e11 ) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f44,definition,
( ~ sP22
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e11) = e11
& op1(e11,e11) = e11 ) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f45,definition,
( ~ sP23
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e11) = e11
& op1(e11,e10) = e11 ) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f46,definition,
( ~ sP24
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e10) = e10
& op1(e10,e13) = e10 ) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f47,definition,
( ~ sP25
| ( ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& op1(e12,e10) = e10
& op1(e10,e12) = e10 ) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f48,definition,
( ~ sP26
| ( ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& op1(e11,e10) = e10
& op1(e10,e11) = e10 ) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f49,definition,
( ~ sP27
| ( ( op1(e13,e13) = e13
| op1(e13,e13) != e13 )
& ( op1(e12,e13) = e12
| op1(e12,e12) != e13 )
& ( op1(e11,e13) = e11
| op1(e11,e11) != e13 )
& ( op1(e10,e13) = e10
| op1(e10,e10) != e13 )
& op1(e13,op1(e13,e13)) = e13
& op1(e13,op1(e13,e12)) = e12
& op1(e13,op1(e13,e11)) = e11
& op1(e13,op1(e13,e10)) = e10 ) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f50,definition,
( ~ sP28
| ( ( op1(e13,e12) = e13
| op1(e13,e13) != e12 )
& ( op1(e12,e12) = e12
| op1(e12,e12) != e12 )
& ( op1(e11,e12) = e11
| op1(e11,e11) != e12 )
& ( op1(e10,e12) = e10
| op1(e10,e10) != e12 )
& op1(e12,op1(e12,e13)) = e13
& op1(e12,op1(e12,e12)) = e12
& op1(e12,op1(e12,e11)) = e11
& op1(e12,op1(e12,e10)) = e10 ) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f51,definition,
( ~ sP29
| ( ( op1(e13,e11) = e13
| op1(e13,e13) != e11 )
& ( op1(e12,e11) = e12
| op1(e12,e12) != e11 )
& ( op1(e11,e11) = e11
| op1(e11,e11) != e11 )
& ( op1(e10,e11) = e10
| op1(e10,e10) != e11 )
& op1(e11,op1(e11,e13)) = e13
& op1(e11,op1(e11,e12)) = e12
& op1(e11,op1(e11,e11)) = e11
& op1(e11,op1(e11,e10)) = e10 ) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f52,plain,
( ( sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| ( ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e10
| op1(e10,e10) != e10 )
& op1(e10,e10) = e10
& op1(e10,e10) = e10 ) )
& ( sP27
| sP28
| sP29
| ( ( op1(e13,e10) = e13
| op1(e13,e13) != e10 )
& ( op1(e12,e10) = e12
| op1(e12,e12) != e10 )
& ( op1(e11,e10) = e11
| op1(e11,e11) != e10 )
& ( op1(e10,e10) = e10
| op1(e10,e10) != e10 )
& 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(definition_folding,[],[f10,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34]) ).
fof(f53,definition,
( ~ sP30
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e23) = e23
& op2(e23,e23) = e23 ) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f54,definition,
( ~ sP31
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e23) = e23
& op2(e23,e22) = e23 ) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ~ sP32
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e23) = e23
& op2(e23,e21) = e23 ) ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ~ sP33
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e23) = e23
& op2(e23,e20) = e23 ) ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ~ sP34
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e22) = e22
& op2(e22,e23) = e22 ) ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f58,definition,
( ~ sP35
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e22) = e22
& op2(e22,e22) = e22 ) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f59,definition,
( ~ sP36
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e22) = e22
& op2(e22,e21) = e22 ) ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f60,definition,
( ~ sP37
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e22) = e22
& op2(e22,e20) = e22 ) ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f61,definition,
( ~ sP38
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e21) = e21
& op2(e21,e23) = e21 ) ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f62,definition,
( ~ sP39
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e21) = e21
& op2(e21,e22) = e21 ) ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f63,definition,
( ~ sP40
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e21) = e21
& op2(e21,e21) = e21 ) ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f64,definition,
( ~ sP41
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e21) = e21
& op2(e21,e20) = e21 ) ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f65,definition,
( ~ sP42
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e20) = e20
& op2(e20,e23) = e20 ) ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f66,definition,
( ~ sP43
| ( ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& op2(e22,e20) = e20
& op2(e20,e22) = e20 ) ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f67,definition,
( ~ sP44
| ( ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& op2(e21,e20) = e20
& op2(e20,e21) = e20 ) ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f68,definition,
( ~ sP45
| ( ( op2(e23,e23) = e23
| op2(e23,e23) != e23 )
& ( op2(e22,e23) = e22
| op2(e22,e22) != e23 )
& ( op2(e21,e23) = e21
| op2(e21,e21) != e23 )
& ( op2(e20,e23) = e20
| op2(e20,e20) != e23 )
& op2(e23,op2(e23,e23)) = e23
& op2(e23,op2(e23,e22)) = e22
& op2(e23,op2(e23,e21)) = e21
& op2(e23,op2(e23,e20)) = e20 ) ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f69,definition,
( ~ sP46
| ( ( op2(e23,e22) = e23
| op2(e23,e23) != e22 )
& ( op2(e22,e22) = e22
| op2(e22,e22) != e22 )
& ( op2(e21,e22) = e21
| op2(e21,e21) != e22 )
& ( op2(e20,e22) = e20
| op2(e20,e20) != e22 )
& op2(e22,op2(e22,e23)) = e23
& op2(e22,op2(e22,e22)) = e22
& op2(e22,op2(e22,e21)) = e21
& op2(e22,op2(e22,e20)) = e20 ) ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f70,definition,
( ~ sP47
| ( ( op2(e23,e21) = e23
| op2(e23,e23) != e21 )
& ( op2(e22,e21) = e22
| op2(e22,e22) != e21 )
& ( op2(e21,e21) = e21
| op2(e21,e21) != e21 )
& ( op2(e20,e21) = e20
| op2(e20,e20) != e21 )
& op2(e21,op2(e21,e23)) = e23
& op2(e21,op2(e21,e22)) = e22
& op2(e21,op2(e21,e21)) = e21
& op2(e21,op2(e21,e20)) = e20 ) ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f71,plain,
( ( sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| ( ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 )
& op2(e20,e20) = e20
& op2(e20,e20) = e20 ) )
& ( sP45
| sP46
| sP47
| ( ( op2(e23,e20) = e23
| op2(e23,e23) != e20 )
& ( op2(e22,e20) = e22
| op2(e22,e22) != e20 )
& ( op2(e21,e20) = e21
| op2(e21,e21) != e20 )
& ( op2(e20,e20) = e20
| op2(e20,e20) != e20 )
& 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(definition_folding,[],[f11,f70,f69,f68,f67,f66,f65,f64,f63,f62,f61,f60,f59,f58,f57,f56,f55,f54,f53]) ).
fof(f101,plain,
( ~ sP12
| ( ( op1(e13,e13) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& op1(e13,e13) = e13
& op1(e13,e13) = e13 ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f119,plain,
( ~ sP30
| ( ( op2(e23,e23) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& op2(e23,e23) = e23
& op2(e23,e23) = e23 ) ),
inference(nnf_transformation,[],[f53]) ).
fof(f321,plain,
( ~ sP12
| e13 = op1(e13,e13) ),
inference(cnf_transformation,[],[f101]) ).
fof(f548,plain,
( ~ sP30
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_244,plain,
( ( op1(e13,e13) = e13 )
| ~ sP12 ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_467,plain,
( ( op2(e23,e23) = e23 )
| ~ sP30 ),
inference(cnf_transformation,[],[f548]) ).
tcf(c_603,plain,
~ sP30,
inference(global_subsumption_just,[status(thm)],[c_467,c_467,c_471]) ).
tcf(c_615,plain,
~ sP12,
inference(global_subsumption_just,[status(thm)],[c_244,c_244,c_248]) ).
tcf(c_715,plain,
( sP36
| sP37
| sP38
| sP39
| sP44
| sP43
| sP42
| sP41
| sP34
| sP33
| sP32
| sP31 ),
inference(global_subsumption_just,[status(thm)],[c_480,c_480,c_481,c_603,c_607,c_611]) ).
tcf(c_716,plain,
( sP31
| sP32
| sP33
| sP34
| sP36
| sP37
| sP38
| sP39
| sP41
| sP42
| sP43
| sP44 ),
inference(renaming,[status(thm)],[c_715]) ).
tcf(c_719,plain,
( sP18
| sP19
| sP20
| sP21
| sP26
| sP25
| sP24
| sP23
| sP16
| sP15
| sP14
| sP13 ),
inference(global_subsumption_just,[status(thm)],[c_257,c_257,c_258,c_615,c_619,c_623]) ).
tcf(c_720,plain,
( sP13
| sP14
| sP15
| sP16
| sP18
| sP19
| sP20
| sP21
| sP23
| sP24
| sP25
| sP26 ),
inference(renaming,[status(thm)],[c_719]) ).
tcf(c_743,plain,
( sP36
| sP37
| sP38
| sP39
| sP44
| sP43
| sP42
| sP41
| sP34
| sP33
| sP32
| sP31 ),
inference(global_subsumption_just,[status(thm)],[c_482,c_716]) ).
tcf(c_744,plain,
( sP31
| sP32
| sP33
| sP34
| sP36
| sP37
| sP38
| sP39
| sP41
| sP42
| sP43
| sP44 ),
inference(renaming,[status(thm)],[c_743]) ).
tcf(c_749,plain,
( sP18
| sP19
| sP20
| sP21
| sP26
| sP25
| sP24
| sP23
| sP16
| sP15
| sP14
| sP13 ),
inference(global_subsumption_just,[status(thm)],[c_259,c_720]) ).
tcf(c_750,plain,
( sP13
| sP14
| sP15
| sP16
| sP18
| sP19
| sP20
| sP21
| sP23
| sP24
| sP25
| sP26 ),
inference(renaming,[status(thm)],[c_749]) ).
tcf(c_4276,plain,
( sP13
| sP14
| sP16
| sP18
| sP19
| sP20
| sP21
| sP23
| sP24
| sP25 ),
inference(forward_subsumption_resolution,[status(thm)],[c_750,c_4156,c_3966]) ).
tcf(c_4307,plain,
( sP31
| sP32
| sP34
| sP36
| sP37
| sP38
| sP39
| sP41
| sP42
| sP43 ),
inference(forward_subsumption_resolution,[status(thm)],[c_744,c_4087,c_3882]) ).
tcf(c_4348,plain,
( sP31
| sP32
| sP34
| sP36
| sP37
| sP38
| sP39
| sP41
| sP43 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4307,c_4347]) ).
tcf(c_4368,plain,
( sP31
| sP32
| sP36
| sP37
| sP38
| sP39
| sP41
| sP43 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4348,c_4367]) ).
tcf(c_4386,plain,
( sP31
| sP32
| sP36
| sP38
| sP39
| sP41
| sP43 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4368,c_4385]) ).
tcf(c_4415,plain,
( sP13
| sP14
| sP16
| sP18
| sP19
| sP20
| sP21
| sP23
| sP25 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4276,c_4414]) ).
tcf(c_4435,plain,
( sP13
| sP14
| sP18
| sP19
| sP20
| sP21
| sP23
| sP25 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4415,c_4434]) ).
tcf(c_4453,plain,
( sP13
| sP14
| sP18
| sP20
| sP21
| sP23
| sP25 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4435,c_4452]) ).
tcf(c_4860,plain,
( sP31
| sP32
| sP38
| sP39
| sP41
| sP43 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4386,c_4859]) ).
tcf(c_4874,plain,
( sP31
| sP38
| sP39
| sP41
| sP43 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4860,c_4873]) ).
tcf(c_4891,plain,
( sP31
| sP39
| sP41
| sP43 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4874,c_4886]) ).
tcf(c_4906,plain,
( sP31
| sP41
| sP43 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4891,c_4901]) ).
tcf(c_5274,plain,
( sP13
| sP14
| sP20
| sP21
| sP23
| sP25 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4453,c_5273]) ).
tcf(c_5288,plain,
( sP13
| sP20
| sP21
| sP23
| sP25 ),
inference(backward_subsumption_resolution,[status(thm)],[c_5274,c_5287]) ).
tcf(c_5305,plain,
( sP13
| sP21
| sP23
| sP25 ),
inference(backward_subsumption_resolution,[status(thm)],[c_5288,c_5300]) ).
tcf(c_5320,plain,
( sP13
| sP23
| sP25 ),
inference(backward_subsumption_resolution,[status(thm)],[c_5305,c_5315]) ).
tcf(c_5941,plain,
( sP13
| sP25
| ( op1(e10,e13) != e10 ) ),
inference(resolution,[status(thm)],[c_5320,c_4741]) ).
tcf(c_5951,plain,
( sP13
| sP25
| ( op1(e10,e11) = e11 ) ),
inference(resolution,[status(thm)],[c_5320,c_178]) ).
tcf(c_5967,plain,
( sP31
| sP43
| ( op2(e20,e23) != e20 ) ),
inference(resolution,[status(thm)],[c_4906,c_4650]) ).
tcf(c_5977,plain,
( sP31
| sP43
| ( op2(e20,e21) = e21 ) ),
inference(resolution,[status(thm)],[c_4906,c_401]) ).
tcf(c_16734,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_5977,c_5967,c_5951,c_5941,c_5639,c_5580,c_5558,c_5547,c_5539,c_5531,c_5515,c_5507,c_5486,c_5476,c_5429,c_5408,c_5388,c_5343,c_5299,c_5191,c_5152,c_5141,c_5125,c_5109,c_5101,c_5090,c_5079,c_5068,c_5057,c_5027,c_5019,c_4975,c_4964,c_4929,c_4772,c_4658,c_4543,c_4517,c_4497,c_4474,c_4174,c_4169,c_4159,c_4031,c_3956,c_3889,c_3877,c_3531,c_591,c_536,c_505,c_498,c_490,c_489,c_488,c_487,c_486,c_485,c_460,c_388,c_307,c_301,c_291,c_290,c_280,c_279,c_276,c_237,c_170,c_169,c_165,c_147,c_143,c_118,c_117,c_116,c_115,c_114,c_113]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG126+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.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Fri Sep 25 04:51:50 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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.12/0.43
% 0.12/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.43
% 0.12/0.44 % Detected problem language: tptp
% 0.12/0.45 % Proving...
% 6.52/1.63 % SZS status Started for theBenchmark.p
% 6.52/1.63 % SZS status Theorem for theBenchmark.p
% 6.52/1.63
% 6.52/1.63 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.52/1.63
% 6.52/1.63 % ------ iProver source info
% 6.52/1.63
% 6.52/1.63 % git: date: 2026-07-19 20:42:38 +0200
% 6.52/1.63 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.52/1.63 % git: non_committed_changes: false
% 6.52/1.63
% 6.52/1.63 % ------ Parsing...
% 6.52/1.63 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.52/1.63
% 6.52/1.63 % ------ Preprocessing... sup_sim: 451 sf_s rm: 30 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.52/1.63
% 6.52/1.63 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.52/1.63
% 6.52/1.63 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.52/1.63 % ------ Proving...
% 6.52/1.63 % ------ Problem Properties
% 6.52/1.63
% 6.52/1.63 %
% 6.52/1.63 % clauses 278
% 6.52/1.63 % conjectures 0
% 6.52/1.63 % EPR 28
% 6.52/1.63 % Horn 193
% 6.52/1.63 % unary 134
% 6.52/1.63 % binary 69
% 6.52/1.63 % lits 590
% 6.52/1.63 % lits eq 486
% 6.52/1.63 % fd_pure 0
% 6.52/1.63 % fd_pseudo 0
% 6.52/1.63 % fd_cond 0
% 6.52/1.63 % fd_pseudo_cond 0
% 6.52/1.63 % AC symbols 0
% 6.52/1.63
% 6.52/1.63 % ------ Schedule dynamic 5 is on
% 6.52/1.63
% 6.52/1.63 % ------ no conjectures: strip conj schedule
% 6.52/1.63
% 6.52/1.63 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 6.52/1.63
% 6.52/1.63
% 6.52/1.63 % ------
% 6.52/1.63 % Current options:
% 6.52/1.63 % ------
% 6.52/1.63
% 6.52/1.63
% 6.52/1.63 %
% 6.52/1.63
% 6.52/1.63 % ------ Proving...
% 6.52/1.63 %
% 6.52/1.63
% 6.52/1.63 % SZS status Theorem for theBenchmark.p
% 6.52/1.63
% 6.52/1.63 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.52/1.64
% 6.52/1.64
%------------------------------------------------------------------------------