%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ALG117+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n015.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:29 PM UTC 2026
% Result : Theorem 3.41s 6.30s
% Output : CNFRefutation 4.52s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f33ERROR: Could not build tree for root c_3032ERROR: 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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
( ( ( 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,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(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(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 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
( ( ( 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,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(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(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 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
( e12 = op1(e13,e13)
& e11 = op1(op1(e13,e13),e13)
& e10 = op1(e13,op1(e13,e13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( e22 = op2(e23,e23)
& e21 = op2(op2(e23,e23),e23)
& e20 = op2(e23,op2(e23,e23)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( h1(e12) = op2(e20,e20)
& h1(e11) = op2(op2(e20,e20),e20)
& h1(e10) = op2(e20,op2(e20,e20))
& h1(e13) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( h2(e12) = op2(e21,e21)
& h2(e11) = op2(op2(e21,e21),e21)
& h2(e10) = op2(e21,op2(e21,e21))
& h2(e13) = e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h3(e12) = op2(e22,e22)
& h3(e11) = op2(op2(e22,e22),e22)
& h3(e10) = op2(e22,op2(e22,e22))
& h3(e13) = e22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f44,plain,
( ~ sP11
| ( e21 != h1(e13)
& e21 != h1(e12)
& e21 != h1(e11)
& e21 != h1(e10) ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f45,plain,
( ~ sP10
| ( e22 != h1(e13)
& e22 != h1(e12)
& e22 != h1(e11)
& e22 != h1(e10) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f46,plain,
( ~ sP9
| ( e23 != h1(e13)
& e23 != h1(e12)
& e23 != h1(e11)
& e23 != h1(e10) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f56,plain,
( ~ sP15
| ( op1(e13,e10) != e13
& op1(e13,e13) = e10 ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f57,plain,
( ~ sP14
| ( op1(e13,e11) != e13
& op1(e13,e13) = e11 ) ),
inference(nnf_transformation,[],[f36]) ).
fof(f60,plain,
( ~ sP19
| ( op2(e23,e20) != e23
& op2(e23,e23) = e20 ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f61,plain,
( ~ sP18
| ( op2(e23,e21) != e23
& op2(e23,e23) = e21 ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f65,plain,
( ~ sP11
| e21 != h1(e12) ),
inference(cnf_transformation,[],[f44]) ).
fof(f70,plain,
( ~ sP10
| e22 != h1(e11) ),
inference(cnf_transformation,[],[f45]) ).
fof(f75,plain,
( ~ sP9
| e23 != h1(e10) ),
inference(cnf_transformation,[],[f46]) ).
fof(f124,plain,
( sP9
| sP10
| sP11
| e20 != h1(e13)
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f127,plain,
( sP9
| sP10
| sP11
| e20 != h1(e10)
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f129,plain,
e11 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f130,plain,
e11 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f131,plain,
e10 != e13,
inference(cnf_transformation,[],[f7]) ).
fof(f132,plain,
e10 != e12,
inference(cnf_transformation,[],[f7]) ).
fof(f150,plain,
e12 = op1(e13,e13),
inference(cnf_transformation,[],[f12]) ).
fof(f151,plain,
e11 = op1(op1(e13,e13),e13),
inference(cnf_transformation,[],[f12]) ).
fof(f152,plain,
e10 = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f154,plain,
( ~ sP15
| e10 = op1(e13,e13) ),
inference(cnf_transformation,[],[f56]) ).
fof(f156,plain,
( ~ sP14
| e11 = op1(e13,e13) ),
inference(cnf_transformation,[],[f57]) ).
fof(f168,plain,
( sP12
| e13 = op1(e12,e12)
| e13 = op1(e11,e11)
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[],[f38]) ).
fof(f182,plain,
( sP14
| e11 = op1(e12,e12)
| e11 != op1(e11,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f38]) ).
fof(f184,plain,
( sP14
| e11 = op1(e12,e12)
| e11 = op1(e11,e11)
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[],[f38]) ).
fof(f188,plain,
( sP15
| e10 = op1(e12,e12)
| e10 = op1(e11,e11)
| e10 != op1(e10,e10) ),
inference(cnf_transformation,[],[f38]) ).
fof(f192,plain,
( sP15
| e10 = op1(e12,e12)
| e10 = op1(e11,e11)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f38]) ).
fof(f194,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f195,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f196,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f202,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f203,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f204,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f206,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f209,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f210,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f215,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f216,plain,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f218,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f219,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f220,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f221,plain,
op1(e10,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f222,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f5]) ).
fof(f223,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f224,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f225,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f226,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f227,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f5]) ).
fof(f231,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f233,plain,
op1(e10,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f234,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f5]) ).
fof(f236,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f238,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f240,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f5]) ).
fof(f244,plain,
( e12 = op1(e13,e13)
| e12 = op1(e13,e12)
| e12 = op1(e13,e11)
| e12 = op1(e13,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f275,plain,
( e13 = op1(e13,e11)
| e12 = op1(e13,e11)
| e11 = op1(e13,e11)
| e10 = op1(e13,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f276,plain,
( e13 = op1(e13,e10)
| e12 = op1(e13,e10)
| e11 = op1(e13,e10)
| e10 = op1(e13,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f279,plain,
( e13 = op1(e12,e11)
| e12 = op1(e12,e11)
| e11 = op1(e12,e11)
| e10 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f280,plain,
( e13 = op1(e12,e10)
| e12 = op1(e12,e10)
| e11 = op1(e12,e10)
| e10 = op1(e12,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f281,plain,
( e13 = op1(e11,e13)
| e12 = op1(e11,e13)
| e11 = op1(e11,e13)
| e10 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f282,plain,
( e13 = op1(e11,e12)
| e12 = op1(e11,e12)
| e11 = op1(e11,e12)
| e10 = op1(e11,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f284,plain,
( e13 = op1(e11,e10)
| e12 = op1(e11,e10)
| e11 = op1(e11,e10)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f285,plain,
( e13 = op1(e10,e13)
| e12 = op1(e10,e13)
| e11 = op1(e10,e13)
| e10 = op1(e10,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f286,plain,
( e13 = op1(e10,e12)
| e12 = op1(e10,e12)
| e11 = op1(e10,e12)
| e10 = op1(e10,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f287,plain,
( e13 = op1(e10,e11)
| e12 = op1(e10,e11)
| e11 = op1(e10,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f289,plain,
e22 = op2(e23,e23),
inference(cnf_transformation,[],[f13]) ).
fof(f290,plain,
e21 = op2(op2(e23,e23),e23),
inference(cnf_transformation,[],[f13]) ).
fof(f291,plain,
e20 = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f293,plain,
( ~ sP19
| e20 = op2(e23,e23) ),
inference(cnf_transformation,[],[f60]) ).
fof(f295,plain,
( ~ sP18
| e21 = op2(e23,e23) ),
inference(cnf_transformation,[],[f61]) ).
fof(f307,plain,
( sP16
| e23 = op2(e22,e22)
| e23 = op2(e21,e21)
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[],[f43]) ).
fof(f321,plain,
( sP18
| e21 = op2(e22,e22)
| e21 != op2(e21,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f43]) ).
fof(f323,plain,
( sP18
| e21 = op2(e22,e22)
| e21 = op2(e21,e21)
| op2(e20,e20) = e21 ),
inference(cnf_transformation,[],[f43]) ).
fof(f327,plain,
( sP19
| e20 = op2(e22,e22)
| e20 = op2(e21,e21)
| e20 != op2(e20,e20) ),
inference(cnf_transformation,[],[f43]) ).
fof(f331,plain,
( sP19
| e20 = op2(e22,e22)
| e20 = op2(e21,e21)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f43]) ).
fof(f333,plain,
e21 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f334,plain,
e21 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f335,plain,
e20 != e23,
inference(cnf_transformation,[],[f8]) ).
fof(f336,plain,
e20 != e22,
inference(cnf_transformation,[],[f8]) ).
fof(f339,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f340,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f341,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f342,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f343,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f344,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f345,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f346,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f347,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f348,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f349,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f351,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f354,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f355,plain,
op2(e21,e20) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f360,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f361,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f363,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f364,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f365,plain,
op2(e20,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f366,plain,
op2(e20,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f367,plain,
op2(e20,e23) != op2(e21,e23),
inference(cnf_transformation,[],[f6]) ).
fof(f368,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f369,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f370,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f371,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f372,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f6]) ).
fof(f376,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f378,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f379,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f6]) ).
fof(f381,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f383,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f385,plain,
op2(e20,e20) != op2(e21,e20),
inference(cnf_transformation,[],[f6]) ).
fof(f389,plain,
( e22 = op2(e23,e23)
| e22 = op2(e23,e22)
| e22 = op2(e23,e21)
| e22 = op2(e23,e20) ),
inference(cnf_transformation,[],[f4]) ).
fof(f420,plain,
( e23 = op2(e23,e21)
| e22 = op2(e23,e21)
| e21 = op2(e23,e21)
| e20 = op2(e23,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f421,plain,
( e23 = op2(e23,e20)
| e22 = op2(e23,e20)
| e21 = op2(e23,e20)
| e20 = op2(e23,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f424,plain,
( e23 = op2(e22,e21)
| e22 = op2(e22,e21)
| e21 = op2(e22,e21)
| e20 = op2(e22,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f425,plain,
( e23 = op2(e22,e20)
| e22 = op2(e22,e20)
| e21 = op2(e22,e20)
| e20 = op2(e22,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f426,plain,
( e23 = op2(e21,e23)
| e22 = op2(e21,e23)
| e21 = op2(e21,e23)
| e20 = op2(e21,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f427,plain,
( e23 = op2(e21,e22)
| e22 = op2(e21,e22)
| e21 = op2(e21,e22)
| e20 = op2(e21,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f429,plain,
( e23 = op2(e21,e20)
| e22 = op2(e21,e20)
| e21 = op2(e21,e20)
| e20 = op2(e21,e20) ),
inference(cnf_transformation,[],[f3]) ).
fof(f430,plain,
( e23 = op2(e20,e23)
| e22 = op2(e20,e23)
| e21 = op2(e20,e23)
| e20 = op2(e20,e23) ),
inference(cnf_transformation,[],[f3]) ).
fof(f431,plain,
( e23 = op2(e20,e22)
| e22 = op2(e20,e22)
| e21 = op2(e20,e22)
| e20 = op2(e20,e22) ),
inference(cnf_transformation,[],[f3]) ).
fof(f432,plain,
( e23 = op2(e20,e21)
| e22 = op2(e20,e21)
| e21 = op2(e20,e21)
| e20 = op2(e20,e21) ),
inference(cnf_transformation,[],[f3]) ).
fof(f434,plain,
op2(e20,e20) = h1(e12),
inference(cnf_transformation,[],[f14]) ).
fof(f435,plain,
h1(e11) = op2(op2(e20,e20),e20),
inference(cnf_transformation,[],[f14]) ).
fof(f436,plain,
h1(e10) = op2(e20,op2(e20,e20)),
inference(cnf_transformation,[],[f14]) ).
fof(f437,plain,
e20 = h1(e13),
inference(cnf_transformation,[],[f14]) ).
fof(f438,plain,
op2(e21,e21) = h2(e12),
inference(cnf_transformation,[],[f15]) ).
fof(f439,plain,
h2(e11) = op2(op2(e21,e21),e21),
inference(cnf_transformation,[],[f15]) ).
fof(f440,plain,
h2(e10) = op2(e21,op2(e21,e21)),
inference(cnf_transformation,[],[f15]) ).
fof(f442,plain,
op2(e22,e22) = h3(e12),
inference(cnf_transformation,[],[f16]) ).
tcf(c_51,plain,
( ~ sP11
| ( h1(e12) != e21 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_54,plain,
( ~ sP10
| ( h1(e11) != e22 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_57,plain,
( ~ sP9
| ( h1(e10) != e23 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_97,negated_conjecture,
( sP9
| sP10
| sP11
| ( h1(e10) != e20 )
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_100,negated_conjecture,
( sP9
| sP10
| sP11
| ( h1(e13) != e20 )
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_114,plain,
e10 != e12,
inference(cnf_transformation,[],[f132]) ).
tcf(c_115,plain,
e10 != e13,
inference(cnf_transformation,[],[f131]) ).
tcf(c_116,plain,
e11 != e12,
inference(cnf_transformation,[],[f130]) ).
tcf(c_117,plain,
e11 != e13,
inference(cnf_transformation,[],[f129]) ).
tcf(c_135,plain,
op1(e13,op1(e13,e13)) = e10,
inference(cnf_transformation,[],[f152]) ).
tcf(c_136,plain,
op1(op1(e13,e13),e13) = e11,
inference(cnf_transformation,[],[f151]) ).
tcf(c_137,plain,
op1(e13,e13) = e12,
inference(cnf_transformation,[],[f150]) ).
tcf(c_138,plain,
( ( op1(e13,e13) = e10 )
| ~ sP15 ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_140,plain,
( ( op1(e13,e13) = e11 )
| ~ sP14 ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_146,plain,
( sP15
| ( op1(e12,e12) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e10,e10) = e10 ) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_150,plain,
( sP15
| ( op1(e12,e12) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e10,e10) != e10 ) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_154,plain,
( sP14
| ( op1(e12,e12) = e11 )
| ( op1(e11,e11) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_156,plain,
( sP14
| ( op1(e12,e12) = e11 )
| ( op1(e10,e10) = e11 )
| ( op1(e11,e11) != e11 ) ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_170,plain,
( sP12
| ( op1(e12,e12) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e10,e10) = e13 ) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_178,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f240]) ).
tcf(c_180,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f238]) ).
tcf(c_182,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f236]) ).
tcf(c_184,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f234]) ).
tcf(c_185,plain,
op1(e10,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f233]) ).
tcf(c_187,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f231]) ).
tcf(c_191,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f227]) ).
tcf(c_192,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f226]) ).
tcf(c_193,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f225]) ).
tcf(c_194,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f224]) ).
tcf(c_195,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f223]) ).
tcf(c_196,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f222]) ).
tcf(c_197,plain,
op1(e10,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f221]) ).
tcf(c_198,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f220]) ).
tcf(c_199,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f219]) ).
tcf(c_200,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f218]) ).
tcf(c_202,plain,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f216]) ).
tcf(c_203,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[],[f215]) ).
tcf(c_208,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[],[f210]) ).
tcf(c_209,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f209]) ).
tcf(c_212,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f206]) ).
tcf(c_214,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f204]) ).
tcf(c_215,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f203]) ).
tcf(c_216,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f202]) ).
tcf(c_217,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f201]) ).
tcf(c_218,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f200]) ).
tcf(c_219,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f199]) ).
tcf(c_220,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f198]) ).
tcf(c_221,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[],[f197]) ).
tcf(c_222,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f196]) ).
tcf(c_223,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f195]) ).
tcf(c_224,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f194]) ).
tcf(c_254,plain,
( ( op1(e13,e13) = e12 )
| ( op1(e13,e12) = e12 )
| ( op1(e13,e11) = e12 )
| ( op1(e13,e10) = e12 ) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_259,plain,
( ( op1(e10,e11) = e13 )
| ( op1(e10,e11) = e12 )
| ( op1(e10,e11) = e11 )
| ( op1(e10,e11) = e10 ) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_260,plain,
( ( op1(e10,e12) = e13 )
| ( op1(e10,e12) = e12 )
| ( op1(e10,e12) = e11 )
| ( op1(e10,e12) = e10 ) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_261,plain,
( ( op1(e10,e13) = e13 )
| ( op1(e10,e13) = e12 )
| ( op1(e10,e13) = e11 )
| ( op1(e10,e13) = e10 ) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_262,plain,
( ( op1(e11,e10) = e13 )
| ( op1(e11,e10) = e12 )
| ( op1(e11,e10) = e11 )
| ( op1(e11,e10) = e10 ) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_264,plain,
( ( op1(e11,e12) = e13 )
| ( op1(e11,e12) = e12 )
| ( op1(e11,e12) = e11 )
| ( op1(e11,e12) = e10 ) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_265,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e13) = e12 )
| ( op1(e11,e13) = e11 )
| ( op1(e11,e13) = e10 ) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_266,plain,
( ( op1(e12,e10) = e13 )
| ( op1(e12,e10) = e12 )
| ( op1(e12,e10) = e11 )
| ( op1(e12,e10) = e10 ) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_267,plain,
( ( op1(e12,e11) = e13 )
| ( op1(e12,e11) = e12 )
| ( op1(e12,e11) = e11 )
| ( op1(e12,e11) = e10 ) ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_270,plain,
( ( op1(e13,e10) = e13 )
| ( op1(e13,e10) = e12 )
| ( op1(e13,e10) = e11 )
| ( op1(e13,e10) = e10 ) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_271,plain,
( ( op1(e13,e11) = e13 )
| ( op1(e13,e11) = e12 )
| ( op1(e13,e11) = e11 )
| ( op1(e13,e11) = e10 ) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_274,plain,
op2(e23,op2(e23,e23)) = e20,
inference(cnf_transformation,[],[f291]) ).
tcf(c_275,plain,
op2(op2(e23,e23),e23) = e21,
inference(cnf_transformation,[],[f290]) ).
tcf(c_276,plain,
op2(e23,e23) = e22,
inference(cnf_transformation,[],[f289]) ).
tcf(c_277,plain,
( ( op2(e23,e23) = e20 )
| ~ sP19 ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_279,plain,
( ( op2(e23,e23) = e21 )
| ~ sP18 ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_285,plain,
( sP19
| ( op2(e20,e20) = e20 )
| ( op2(e22,e22) = e20 )
| ( op2(e21,e21) = e20 ) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_289,plain,
( sP19
| ( op2(e22,e22) = e20 )
| ( op2(e21,e21) = e20 )
| ( op2(e20,e20) != e20 ) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_293,plain,
( sP18
| ( op2(e20,e20) = e21 )
| ( op2(e22,e22) = e21 )
| ( op2(e21,e21) = e21 ) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_295,plain,
( sP18
| ( op2(e20,e20) = e21 )
| ( op2(e22,e22) = e21 )
| ( op2(e21,e21) != e21 ) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_309,plain,
( sP16
| ( op2(e20,e20) = e23 )
| ( op2(e22,e22) = e23 )
| ( op2(e21,e21) = e23 ) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_318,plain,
e22 != e20,
inference(cnf_transformation,[],[f336]) ).
tcf(c_319,plain,
e23 != e20,
inference(cnf_transformation,[],[f335]) ).
tcf(c_320,plain,
e21 != e22,
inference(cnf_transformation,[],[f334]) ).
tcf(c_321,plain,
e21 != e23,
inference(cnf_transformation,[],[f333]) ).
tcf(c_323,plain,
op2(e21,e20) != op2(e20,e20),
inference(cnf_transformation,[],[f385]) ).
tcf(c_325,plain,
op2(e23,e20) != op2(e20,e20),
inference(cnf_transformation,[],[f383]) ).
tcf(c_327,plain,
op2(e21,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f381]) ).
tcf(c_329,plain,
op2(e21,e21) != op2(e20,e21),
inference(cnf_transformation,[],[f379]) ).
tcf(c_330,plain,
op2(e22,e21) != op2(e20,e21),
inference(cnf_transformation,[],[f378]) ).
tcf(c_332,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f376]) ).
tcf(c_336,plain,
op2(e22,e22) != op2(e20,e22),
inference(cnf_transformation,[],[f372]) ).
tcf(c_337,plain,
op2(e23,e22) != op2(e20,e22),
inference(cnf_transformation,[],[f371]) ).
tcf(c_338,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[],[f370]) ).
tcf(c_339,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f369]) ).
tcf(c_340,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f368]) ).
tcf(c_341,plain,
op2(e21,e23) != op2(e20,e23),
inference(cnf_transformation,[],[f367]) ).
tcf(c_342,plain,
op2(e22,e23) != op2(e20,e23),
inference(cnf_transformation,[],[f366]) ).
tcf(c_343,plain,
op2(e23,e23) != op2(e20,e23),
inference(cnf_transformation,[],[f365]) ).
tcf(c_344,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f364]) ).
tcf(c_345,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f363]) ).
tcf(c_347,plain,
op2(e20,e21) != op2(e20,e20),
inference(cnf_transformation,[],[f361]) ).
tcf(c_348,plain,
op2(e20,e22) != op2(e20,e20),
inference(cnf_transformation,[],[f360]) ).
tcf(c_353,plain,
op2(e21,e21) != op2(e21,e20),
inference(cnf_transformation,[],[f355]) ).
tcf(c_354,plain,
op2(e21,e22) != op2(e21,e20),
inference(cnf_transformation,[],[f354]) ).
tcf(c_357,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f351]) ).
tcf(c_359,plain,
op2(e22,e21) != op2(e22,e20),
inference(cnf_transformation,[],[f349]) ).
tcf(c_360,plain,
op2(e22,e22) != op2(e22,e20),
inference(cnf_transformation,[],[f348]) ).
tcf(c_361,plain,
op2(e22,e23) != op2(e22,e20),
inference(cnf_transformation,[],[f347]) ).
tcf(c_362,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f346]) ).
tcf(c_363,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f345]) ).
tcf(c_364,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f344]) ).
tcf(c_365,plain,
op2(e23,e21) != op2(e23,e20),
inference(cnf_transformation,[],[f343]) ).
tcf(c_366,plain,
op2(e23,e22) != op2(e23,e20),
inference(cnf_transformation,[],[f342]) ).
tcf(c_367,plain,
op2(e23,e23) != op2(e23,e20),
inference(cnf_transformation,[],[f341]) ).
tcf(c_368,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f340]) ).
tcf(c_369,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f339]) ).
tcf(c_399,plain,
( ( op2(e23,e20) = e22 )
| ( op2(e23,e23) = e22 )
| ( op2(e23,e22) = e22 )
| ( op2(e23,e21) = e22 ) ),
inference(cnf_transformation,[],[f389]) ).
tcf(c_404,plain,
( ( op2(e20,e21) = e20 )
| ( op2(e20,e21) = e23 )
| ( op2(e20,e21) = e22 )
| ( op2(e20,e21) = e21 ) ),
inference(cnf_transformation,[],[f432]) ).
tcf(c_405,plain,
( ( op2(e20,e22) = e20 )
| ( op2(e20,e22) = e23 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e22) = e21 ) ),
inference(cnf_transformation,[],[f431]) ).
tcf(c_406,plain,
( ( op2(e20,e23) = e20 )
| ( op2(e20,e23) = e23 )
| ( op2(e20,e23) = e22 )
| ( op2(e20,e23) = e21 ) ),
inference(cnf_transformation,[],[f430]) ).
tcf(c_407,plain,
( ( op2(e21,e20) = e20 )
| ( op2(e21,e20) = e23 )
| ( op2(e21,e20) = e22 )
| ( op2(e21,e20) = e21 ) ),
inference(cnf_transformation,[],[f429]) ).
tcf(c_409,plain,
( ( op2(e21,e22) = e20 )
| ( op2(e21,e22) = e23 )
| ( op2(e21,e22) = e22 )
| ( op2(e21,e22) = e21 ) ),
inference(cnf_transformation,[],[f427]) ).
tcf(c_410,plain,
( ( op2(e21,e23) = e20 )
| ( op2(e21,e23) = e23 )
| ( op2(e21,e23) = e22 )
| ( op2(e21,e23) = e21 ) ),
inference(cnf_transformation,[],[f426]) ).
tcf(c_411,plain,
( ( op2(e22,e20) = e20 )
| ( op2(e22,e20) = e23 )
| ( op2(e22,e20) = e22 )
| ( op2(e22,e20) = e21 ) ),
inference(cnf_transformation,[],[f425]) ).
tcf(c_412,plain,
( ( op2(e22,e21) = e20 )
| ( op2(e22,e21) = e23 )
| ( op2(e22,e21) = e22 )
| ( op2(e22,e21) = e21 ) ),
inference(cnf_transformation,[],[f424]) ).
tcf(c_415,plain,
( ( op2(e23,e20) = e20 )
| ( op2(e23,e20) = e23 )
| ( op2(e23,e20) = e22 )
| ( op2(e23,e20) = e21 ) ),
inference(cnf_transformation,[],[f421]) ).
tcf(c_416,plain,
( ( op2(e23,e21) = e20 )
| ( op2(e23,e21) = e23 )
| ( op2(e23,e21) = e22 )
| ( op2(e23,e21) = e21 ) ),
inference(cnf_transformation,[],[f420]) ).
tcf(c_419,plain,
h1(e13) = e20,
inference(cnf_transformation,[],[f437]) ).
tcf(c_420,plain,
op2(e20,op2(e20,e20)) = h1(e10),
inference(cnf_transformation,[],[f436]) ).
tcf(c_421,plain,
op2(op2(e20,e20),e20) = h1(e11),
inference(cnf_transformation,[],[f435]) ).
tcf(c_422,plain,
op2(e20,e20) = h1(e12),
inference(cnf_transformation,[],[f434]) ).
tcf(c_424,plain,
op2(e21,op2(e21,e21)) = h2(e10),
inference(cnf_transformation,[],[f440]) ).
tcf(c_425,plain,
op2(op2(e21,e21),e21) = h2(e11),
inference(cnf_transformation,[],[f439]) ).
tcf(c_426,plain,
op2(e21,e21) = h2(e12),
inference(cnf_transformation,[],[f438]) ).
tcf(c_430,plain,
op2(e22,e22) = h3(e12),
inference(cnf_transformation,[],[f442]) ).
tcf(c_475,plain,
( sP18
| ( op2(e20,e20) = e21 )
| ( op2(e22,e22) = e21 ) ),
inference(global_subsumption_just,[status(thm)],[c_293,c_293,c_295]) ).
tcf(c_477,plain,
( sP19
| ( op2(e21,e21) = e20 )
| ( op2(e22,e22) = e20 ) ),
inference(global_subsumption_just,[status(thm)],[c_285,c_285,c_289]) ).
tcf(c_478,plain,
( sP19
| ( op2(e22,e22) = e20 )
| ( op2(e21,e21) = e20 ) ),
inference(renaming,[status(thm)],[c_477]) ).
tcf(c_483,plain,
( sP14
| ( op1(e12,e12) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(global_subsumption_just,[status(thm)],[c_154,c_154,c_156]) ).
tcf(c_485,plain,
( sP15
| ( op1(e12,e12) = e10 )
| ( op1(e11,e11) = e10 ) ),
inference(global_subsumption_just,[status(thm)],[c_146,c_146,c_150]) ).
tcf(c_501,plain,
( sP18
| ( op2(e20,e20) = e21 )
| ( op2(e22,e22) = e21 ) ),
inference(global_subsumption_just,[status(thm)],[c_295,c_475]) ).
tcf(c_505,plain,
( sP19
| ( op2(e22,e22) = e20 )
| ( op2(e21,e21) = e20 ) ),
inference(global_subsumption_just,[status(thm)],[c_289,c_478]) ).
tcf(c_525,plain,
( sP14
| ( op1(e12,e12) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(global_subsumption_just,[status(thm)],[c_156,c_483]) ).
tcf(c_529,plain,
( sP15
| ( op1(e12,e12) = e10 )
| ( op1(e11,e11) = e10 ) ),
inference(global_subsumption_just,[status(thm)],[c_150,c_485]) ).
tcf(c_603,plain,
op2(e23,e23) = e22,
inference(global_subsumption_just,[status(thm)],[c_399,c_276]) ).
tcf(c_609,plain,
op1(e13,e13) = e12,
inference(global_subsumption_just,[status(thm)],[c_254,c_137]) ).
tcf(c_635,plain,
( sP9
| sP10
| sP11
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) ) ),
inference(global_subsumption_just,[status(thm)],[c_100,c_419,c_100]) ).
tcf(c_636,negated_conjecture,
( sP9
| sP10
| sP11
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(renaming,[status(thm)],[c_635]) ).
tcf(c_641,plain,
( sP9
| sP10
| sP11
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) ) ),
inference(global_subsumption_just,[status(thm)],[c_97,c_636]) ).
tcf(c_642,negated_conjecture,
( sP9
| sP10
| sP11
| ( op2(h1(e13),h1(e13)) != h1(op1(e13,e13)) )
| ( op2(h1(e13),h1(e12)) != h1(op1(e13,e12)) )
| ( op2(h1(e13),h1(e11)) != h1(op1(e13,e11)) )
| ( op2(h1(e13),h1(e10)) != h1(op1(e13,e10)) )
| ( op2(h1(e12),h1(e13)) != h1(op1(e12,e13)) )
| ( op2(h1(e12),h1(e12)) != h1(op1(e12,e12)) )
| ( op2(h1(e12),h1(e11)) != h1(op1(e12,e11)) )
| ( op2(h1(e12),h1(e10)) != h1(op1(e12,e10)) )
| ( op2(h1(e11),h1(e13)) != h1(op1(e11,e13)) )
| ( op2(h1(e11),h1(e12)) != h1(op1(e11,e12)) )
| ( op2(h1(e11),h1(e11)) != h1(op1(e11,e11)) )
| ( op2(h1(e11),h1(e10)) != h1(op1(e11,e10)) )
| ( op2(h1(e10),h1(e13)) != h1(op1(e10,e13)) )
| ( op2(h1(e10),h1(e12)) != h1(op1(e10,e12)) )
| ( op2(h1(e10),h1(e11)) != h1(op1(e10,e11)) )
| ( op2(h1(e10),h1(e10)) != h1(op1(e10,e10)) ) ),
inference(renaming,[status(thm)],[c_641]) ).
tcf(c_2584,plain,
( ( e21 = e22 )
| ~ sP18 ),
inference(light_normalisation,[status(thm)],[c_279,c_603]) ).
tcf(c_2585,plain,
~ sP18,
inference(forward_subsumption_resolution,[status(thm)],[c_2584,c_320]) ).
tcf(c_2586,plain,
( ( e22 = e20 )
| ~ sP19 ),
inference(light_normalisation,[status(thm)],[c_277,c_603]) ).
tcf(c_2587,plain,
~ sP19,
inference(forward_subsumption_resolution,[status(thm)],[c_2586,c_318]) ).
tcf(c_2588,plain,
op2(e22,e23) = e21,
inference(light_normalisation,[status(thm)],[c_275,c_603]) ).
tcf(c_2589,plain,
op2(e23,e22) = e20,
inference(light_normalisation,[status(thm)],[c_274,c_603]) ).
tcf(c_2590,plain,
( ( e11 = e12 )
| ~ sP14 ),
inference(light_normalisation,[status(thm)],[c_140,c_609]) ).
tcf(c_2591,plain,
~ sP14,
inference(forward_subsumption_resolution,[status(thm)],[c_2590,c_116]) ).
tcf(c_2592,plain,
( ( e10 = e12 )
| ~ sP15 ),
inference(light_normalisation,[status(thm)],[c_138,c_609]) ).
tcf(c_2593,plain,
~ sP15,
inference(forward_subsumption_resolution,[status(thm)],[c_2592,c_114]) ).
tcf(c_2594,plain,
op1(e12,e13) = e11,
inference(light_normalisation,[status(thm)],[c_136,c_609]) ).
tcf(c_2595,plain,
op1(e13,e12) = e10,
inference(light_normalisation,[status(thm)],[c_135,c_609]) ).
tcf(c_2704,plain,
op2(h2(e12),e21) = h2(e11),
inference(light_normalisation,[status(thm)],[c_425,c_426]) ).
tcf(c_2705,plain,
op2(e21,h2(e12)) = h2(e10),
inference(light_normalisation,[status(thm)],[c_424,c_426]) ).
tcf(c_2706,plain,
op2(h1(e12),e20) = h1(e11),
inference(light_normalisation,[status(thm)],[c_421,c_422]) ).
tcf(c_2707,plain,
op2(e20,h1(e12)) = h1(e10),
inference(light_normalisation,[status(thm)],[c_420,c_422]) ).
tcf(c_2709,plain,
op2(e23,e21) != e22,
inference(light_normalisation,[status(thm)],[c_369,c_603]) ).
tcf(c_2710,plain,
op2(e23,e21) != e20,
inference(light_normalisation,[status(thm)],[c_368,c_2589]) ).
tcf(c_2711,plain,
op2(e23,e20) != e22,
inference(light_normalisation,[status(thm)],[c_367,c_603]) ).
tcf(c_2712,plain,
op2(e23,e20) != e20,
inference(light_normalisation,[status(thm)],[c_366,c_2589]) ).
tcf(c_2713,plain,
h3(e12) != e21,
inference(light_normalisation,[status(thm)],[c_364,c_430,c_2588]) ).
tcf(c_2714,plain,
op2(e22,e21) != e21,
inference(light_normalisation,[status(thm)],[c_363,c_2588]) ).
tcf(c_2715,plain,
op2(e22,e21) != h3(e12),
inference(light_normalisation,[status(thm)],[c_362,c_430]) ).
tcf(c_2716,plain,
op2(e22,e20) != e21,
inference(light_normalisation,[status(thm)],[c_361,c_2588]) ).
tcf(c_2717,plain,
op2(e22,e20) != h3(e12),
inference(light_normalisation,[status(thm)],[c_360,c_430]) ).
tcf(c_2718,plain,
op2(e21,e23) != h2(e12),
inference(light_normalisation,[status(thm)],[c_357,c_426]) ).
tcf(c_2720,plain,
op2(e21,e20) != h2(e12),
inference(light_normalisation,[status(thm)],[c_353,c_426]) ).
tcf(c_2722,plain,
op2(e20,e22) != h1(e12),
inference(light_normalisation,[status(thm)],[c_348,c_422]) ).
tcf(c_2723,plain,
op2(e20,e21) != h1(e12),
inference(light_normalisation,[status(thm)],[c_347,c_422]) ).
tcf(c_2725,plain,
op2(e21,e23) != e22,
inference(light_normalisation,[status(thm)],[c_345,c_603]) ).
tcf(c_2726,plain,
op2(e21,e23) != e21,
inference(light_normalisation,[status(thm)],[c_344,c_2588]) ).
tcf(c_2727,plain,
op2(e20,e23) != e22,
inference(light_normalisation,[status(thm)],[c_343,c_603]) ).
tcf(c_2728,plain,
op2(e20,e23) != e21,
inference(light_normalisation,[status(thm)],[c_342,c_2588]) ).
tcf(c_2729,plain,
h3(e12) != e20,
inference(light_normalisation,[status(thm)],[c_340,c_430,c_2589]) ).
tcf(c_2730,plain,
op2(e21,e22) != e20,
inference(light_normalisation,[status(thm)],[c_339,c_2589]) ).
tcf(c_2731,plain,
op2(e21,e22) != h3(e12),
inference(light_normalisation,[status(thm)],[c_338,c_430]) ).
tcf(c_2732,plain,
op2(e20,e22) != e20,
inference(light_normalisation,[status(thm)],[c_337,c_2589]) ).
tcf(c_2733,plain,
op2(e20,e22) != h3(e12),
inference(light_normalisation,[status(thm)],[c_336,c_430]) ).
tcf(c_2735,plain,
op2(e22,e21) != h2(e12),
inference(light_normalisation,[status(thm)],[c_332,c_426]) ).
tcf(c_2736,plain,
op2(e20,e21) != h2(e12),
inference(light_normalisation,[status(thm)],[c_329,c_426]) ).
tcf(c_2737,plain,
op2(e23,e20) != h1(e12),
inference(light_normalisation,[status(thm)],[c_325,c_422]) ).
tcf(c_2739,plain,
op2(e21,e20) != h1(e12),
inference(light_normalisation,[status(thm)],[c_323,c_422]) ).
tcf(c_2742,plain,
op1(e13,e11) != e12,
inference(light_normalisation,[status(thm)],[c_224,c_609]) ).
tcf(c_2743,plain,
op1(e13,e11) != e10,
inference(light_normalisation,[status(thm)],[c_223,c_2595]) ).
tcf(c_2744,plain,
op1(e13,e10) != e12,
inference(light_normalisation,[status(thm)],[c_222,c_609]) ).
tcf(c_2745,plain,
op1(e13,e10) != e10,
inference(light_normalisation,[status(thm)],[c_221,c_2595]) ).
tcf(c_2746,plain,
op1(e12,e12) != e11,
inference(light_normalisation,[status(thm)],[c_219,c_2594]) ).
tcf(c_2747,plain,
op1(e12,e11) != e11,
inference(light_normalisation,[status(thm)],[c_218,c_2594]) ).
tcf(c_2748,plain,
op1(e12,e10) != e11,
inference(light_normalisation,[status(thm)],[c_216,c_2594]) ).
tcf(c_2750,plain,
op1(e11,e13) != e12,
inference(light_normalisation,[status(thm)],[c_200,c_609]) ).
tcf(c_2751,plain,
op1(e11,e13) != e11,
inference(light_normalisation,[status(thm)],[c_199,c_2594]) ).
tcf(c_2752,plain,
op1(e10,e13) != e12,
inference(light_normalisation,[status(thm)],[c_198,c_609]) ).
tcf(c_2753,plain,
op1(e10,e13) != e11,
inference(light_normalisation,[status(thm)],[c_197,c_2594]) ).
tcf(c_2754,plain,
op1(e12,e12) != e10,
inference(light_normalisation,[status(thm)],[c_195,c_2595]) ).
tcf(c_2755,plain,
op1(e11,e12) != e10,
inference(light_normalisation,[status(thm)],[c_194,c_2595]) ).
tcf(c_2756,plain,
op1(e10,e12) != e10,
inference(light_normalisation,[status(thm)],[c_192,c_2595]) ).
tcf(c_2758,plain,
op1(e11,e11) = e10,
inference(forward_subsumption_resolution,[status(thm)],[c_529,c_2593,c_2754]) ).
tcf(c_2759,plain,
op1(e10,e11) != e10,
inference(demodulation,[status(thm)],[c_184,c_2758]) ).
tcf(c_2760,plain,
op1(e12,e11) != e10,
inference(demodulation,[status(thm)],[c_187,c_2758]) ).
tcf(c_2762,plain,
op1(e11,e10) != e10,
inference(demodulation,[status(thm)],[c_208,c_2758]) ).
tcf(c_2764,plain,
op1(e11,e13) != e10,
inference(demodulation,[status(thm)],[c_212,c_2758]) ).
tcf(c_2765,plain,
op1(e10,e10) = e11,
inference(forward_subsumption_resolution,[status(thm)],[c_525,c_2591,c_2746]) ).
tcf(c_2766,plain,
op1(e11,e10) != e11,
inference(demodulation,[status(thm)],[c_178,c_2765]) ).
tcf(c_2768,plain,
op1(e13,e10) != e11,
inference(demodulation,[status(thm)],[c_180,c_2765]) ).
tcf(c_2769,plain,
op1(e10,e11) != e11,
inference(demodulation,[status(thm)],[c_202,c_2765]) ).
tcf(c_2770,plain,
op1(e10,e12) != e11,
inference(demodulation,[status(thm)],[c_203,c_2765]) ).
tcf(c_2774,plain,
( sP19
| ( h3(e12) = e20 )
| ( h2(e12) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_505,c_426,c_430]) ).
tcf(c_2775,plain,
h2(e12) = e20,
inference(forward_subsumption_resolution,[status(thm)],[c_2774,c_2587,c_2729]) ).
tcf(c_2776,plain,
op2(e20,e21) != e20,
inference(demodulation,[status(thm)],[c_2736,c_2775]) ).
tcf(c_2777,plain,
op2(e22,e21) != e20,
inference(demodulation,[status(thm)],[c_2735,c_2775]) ).
tcf(c_2779,plain,
op2(e21,e20) != e20,
inference(demodulation,[status(thm)],[c_2720,c_2775]) ).
tcf(c_2781,plain,
op2(e21,e23) != e20,
inference(demodulation,[status(thm)],[c_2718,c_2775]) ).
tcf(c_2782,plain,
op2(e21,e20) = h2(e10),
inference(demodulation,[status(thm)],[c_2705,c_2775]) ).
tcf(c_2783,plain,
op2(e20,e21) = h2(e11),
inference(demodulation,[status(thm)],[c_2704,c_2775]) ).
tcf(c_2786,plain,
op2(e21,e21) = e20,
inference(demodulation,[status(thm)],[c_426,c_2775]) ).
tcf(c_2787,plain,
op2(e22,e21) != h2(e11),
inference(demodulation,[status(thm)],[c_330,c_2783]) ).
tcf(c_2789,plain,
h1(e12) != h2(e11),
inference(demodulation,[status(thm)],[c_2723,c_2783]) ).
tcf(c_2792,plain,
h1(e12) != h2(e10),
inference(demodulation,[status(thm)],[c_2739,c_2782]) ).
tcf(c_2794,plain,
op2(e23,e20) != h2(e10),
inference(demodulation,[status(thm)],[c_327,c_2782]) ).
tcf(c_2795,plain,
op2(e21,e22) != h2(e10),
inference(demodulation,[status(thm)],[c_354,c_2782]) ).
tcf(c_2797,plain,
h2(e10) != e20,
inference(light_normalisation,[status(thm)],[c_2779,c_2782]) ).
tcf(c_2798,plain,
h2(e11) != e20,
inference(light_normalisation,[status(thm)],[c_2776,c_2783]) ).
tcf(c_2799,plain,
( sP18
| ( h3(e12) = e21 )
| ( h1(e12) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_501,c_422,c_430]) ).
tcf(c_2800,plain,
h1(e12) = e21,
inference(forward_subsumption_resolution,[status(thm)],[c_2799,c_2585,c_2713]) ).
tcf(c_2801,plain,
h2(e10) != e21,
inference(demodulation,[status(thm)],[c_2792,c_2800]) ).
tcf(c_2802,plain,
h2(e11) != e21,
inference(demodulation,[status(thm)],[c_2789,c_2800]) ).
tcf(c_2804,plain,
op2(e23,e20) != e21,
inference(demodulation,[status(thm)],[c_2737,c_2800]) ).
tcf(c_2805,plain,
op2(e20,e22) != e21,
inference(demodulation,[status(thm)],[c_2722,c_2800]) ).
tcf(c_2807,plain,
op2(e20,e21) = h1(e10),
inference(demodulation,[status(thm)],[c_2707,c_2800]) ).
tcf(c_2808,plain,
op2(e21,e20) = h1(e11),
inference(demodulation,[status(thm)],[c_2706,c_2800]) ).
tcf(c_2809,plain,
( ~ sP11
| ( e21 != e21 ) ),
inference(demodulation,[status(thm)],[c_51,c_2800]) ).
tcf(c_2812,plain,
op2(e20,e20) = e21,
inference(demodulation,[status(thm)],[c_422,c_2800]) ).
tcf(c_2813,plain,
~ sP11,
inference(equality_resolution_simp,[status(thm)],[c_2809]) ).
tcf(c_2814,plain,
h1(e11) = h2(e10),
inference(demodulation,[status(thm)],[c_2782,c_2808]) ).
tcf(c_2815,plain,
h1(e11) != e20,
inference(demodulation,[status(thm)],[c_2797,c_2814]) ).
tcf(c_2817,plain,
op2(e23,e20) != h1(e11),
inference(demodulation,[status(thm)],[c_2794,c_2814]) ).
tcf(c_2818,plain,
op2(e21,e22) != h1(e11),
inference(demodulation,[status(thm)],[c_2795,c_2814]) ).
tcf(c_2830,plain,
h1(e10) = h2(e11),
inference(demodulation,[status(thm)],[c_2783,c_2807]) ).
tcf(c_2831,plain,
h1(e10) != e20,
inference(demodulation,[status(thm)],[c_2798,c_2830]) ).
tcf(c_2832,plain,
op2(e22,e21) != h1(e10),
inference(demodulation,[status(thm)],[c_2787,c_2830]) ).
tcf(c_2846,plain,
h1(e10) != e21,
inference(light_normalisation,[status(thm)],[c_2802,c_2830]) ).
tcf(c_2847,plain,
h1(e11) != e21,
inference(light_normalisation,[status(thm)],[c_2801,c_2814]) ).
tcf(c_2884,plain,
( ( op2(e23,e21) = e23 )
| ( op2(e23,e21) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_416,c_2710,c_2709]) ).
tcf(c_2891,plain,
op2(e23,e20) = e23,
inference(forward_subsumption_resolution,[status(thm)],[c_415,c_2712,c_2711,c_2804]) ).
tcf(c_2893,plain,
h1(e11) != e23,
inference(demodulation,[status(thm)],[c_2817,c_2891]) ).
tcf(c_2895,plain,
op2(e23,e21) != e23,
inference(demodulation,[status(thm)],[c_365,c_2891]) ).
tcf(c_2898,plain,
op2(e23,e21) = e21,
inference(backward_subsumption_resolution,[status(thm)],[c_2884,c_2895]) ).
tcf(c_2915,plain,
op2(e21,e23) = e23,
inference(forward_subsumption_resolution,[status(thm)],[c_410,c_2781,c_2725,c_2726]) ).
tcf(c_2918,plain,
op2(e20,e23) != e23,
inference(demodulation,[status(thm)],[c_341,c_2915]) ).
tcf(c_2929,plain,
( ( h1(e11) = e20 )
| ( h1(e11) = e23 )
| ( h1(e11) = e22 )
| ( h1(e11) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_407,c_2808]) ).
tcf(c_2930,plain,
h1(e11) = e22,
inference(forward_subsumption_resolution,[status(thm)],[c_2929,c_2815,c_2893,c_2847]) ).
tcf(c_2934,plain,
op2(e21,e22) != e22,
inference(demodulation,[status(thm)],[c_2818,c_2930]) ).
tcf(c_2937,plain,
op2(e21,e20) = e22,
inference(demodulation,[status(thm)],[c_2808,c_2930]) ).
tcf(c_2938,plain,
( ~ sP10
| ( e22 != e22 ) ),
inference(demodulation,[status(thm)],[c_54,c_2930]) ).
tcf(c_2939,plain,
~ sP10,
inference(equality_resolution_simp,[status(thm)],[c_2938]) ).
tcf(c_2946,plain,
op2(e20,e23) = e20,
inference(forward_subsumption_resolution,[status(thm)],[c_406,c_2918,c_2727,c_2728]) ).
tcf(c_2957,plain,
( ( h1(e10) = e20 )
| ( h1(e10) = e23 )
| ( h1(e10) = e22 )
| ( h1(e10) = e21 ) ),
inference(light_normalisation,[status(thm)],[c_404,c_2807]) ).
tcf(c_2968,plain,
( ( op1(e13,e11) = e13 )
| ( op1(e13,e11) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_271,c_2742,c_2743]) ).
tcf(c_2971,plain,
op1(e13,e10) = e13,
inference(forward_subsumption_resolution,[status(thm)],[c_270,c_2744,c_2768,c_2745]) ).
tcf(c_2973,plain,
op1(e11,e10) != e13,
inference(demodulation,[status(thm)],[c_182,c_2971]) ).
tcf(c_2975,plain,
op1(e13,e11) != e13,
inference(demodulation,[status(thm)],[c_220,c_2971]) ).
tcf(c_2978,plain,
op1(e13,e11) = e11,
inference(backward_subsumption_resolution,[status(thm)],[c_2968,c_2975]) ).
tcf(c_2995,plain,
op1(e11,e13) = e13,
inference(forward_subsumption_resolution,[status(thm)],[c_265,c_2750,c_2751,c_2764]) ).
tcf(c_2997,plain,
op1(e10,e13) != e13,
inference(demodulation,[status(thm)],[c_196,c_2995]) ).
tcf(c_3005,plain,
op1(e11,e10) = e12,
inference(forward_subsumption_resolution,[status(thm)],[c_262,c_2973,c_2766,c_2762]) ).
tcf(c_3009,plain,
op1(e11,e12) != e12,
inference(demodulation,[status(thm)],[c_209,c_3005]) ).
tcf(c_3015,plain,
op1(e10,e13) = e10,
inference(forward_subsumption_resolution,[status(thm)],[c_261,c_2997,c_2752,c_2753]) ).
fof(f34,definition,
( ~ sP12
| ( op1(e13,e13) != e13
& op1(e13,e13) = e13 ) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ~ sP13
| ( op1(e13,e12) != e13
& op1(e13,e13) = e12 ) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ~ sP14
| ( op1(e13,e11) != e13
& op1(e13,e13) = e11 ) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ~ sP15
| ( op1(e13,e10) != e13
& op1(e13,e13) = e10 ) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f38,plain,
( ( sP12
| ( op1(e12,e13) != e12
& op1(e12,e12) = e13 )
| ( op1(e11,e13) != e11
& op1(e11,e11) = e13 )
| ( op1(e10,e13) != e10
& op1(e10,e10) = e13 ) )
& ( sP13
| ( op1(e12,e12) != e12
& op1(e12,e12) = e12 )
| ( op1(e11,e12) != e11
& op1(e11,e11) = e12 )
| ( op1(e10,e12) != e10
& op1(e10,e10) = e12 ) )
& ( sP14
| ( op1(e12,e11) != e12
& op1(e12,e12) = e11 )
| ( op1(e11,e11) != e11
& op1(e11,e11) = e11 )
| ( op1(e10,e11) != e10
& op1(e10,e10) = e11 ) )
& ( sP15
| ( op1(e12,e10) != e12
& op1(e12,e12) = e10 )
| ( op1(e11,e10) != e11
& op1(e11,e11) = e10 )
| ( op1(e10,e10) != e10
& op1(e10,e10) = e10 ) ) ),
inference(definition_folding,[],[f10,f37,f36,f35,f34]) ).
fof(f39,definition,
( ~ sP16
| ( op2(e23,e23) != e23
& op2(e23,e23) = e23 ) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ~ sP17
| ( op2(e23,e22) != e23
& op2(e23,e23) = e22 ) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ~ sP18
| ( op2(e23,e21) != e23
& op2(e23,e23) = e21 ) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ~ sP19
| ( op2(e23,e20) != e23
& op2(e23,e23) = e20 ) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f43,plain,
( ( sP16
| ( op2(e22,e23) != e22
& op2(e22,e22) = e23 )
| ( op2(e21,e23) != e21
& op2(e21,e21) = e23 )
| ( op2(e20,e23) != e20
& op2(e20,e20) = e23 ) )
& ( sP17
| ( op2(e22,e22) != e22
& op2(e22,e22) = e22 )
| ( op2(e21,e22) != e21
& op2(e21,e21) = e22 )
| ( op2(e20,e22) != e20
& op2(e20,e20) = e22 ) )
& ( sP18
| ( op2(e22,e21) != e22
& op2(e22,e22) = e21 )
| ( op2(e21,e21) != e21
& op2(e21,e21) = e21 )
| ( op2(e20,e21) != e20
& op2(e20,e20) = e21 ) )
& ( sP19
| ( op2(e22,e20) != e22
& op2(e22,e22) = e20 )
| ( op2(e21,e20) != e21
& op2(e21,e21) = e20 )
| ( op2(e20,e20) != e20
& op2(e20,e20) = e20 ) ) ),
inference(definition_folding,[],[f11,f42,f41,f40,f39]) ).
fof(f59,plain,
( ~ sP12
| ( op1(e13,e13) != e13
& op1(e13,e13) = e13 ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f63,plain,
( ~ sP16
| ( op2(e23,e23) != e23
& op2(e23,e23) = e23 ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f159,plain,
( ~ sP12
| e13 != op1(e13,e13) ),
inference(cnf_transformation,[],[f59]) ).
fof(f160,plain,
( ~ sP12
| e13 = op1(e13,e13) ),
inference(cnf_transformation,[],[f59]) ).
fof(f298,plain,
( ~ sP16
| e23 != op2(e23,e23) ),
inference(cnf_transformation,[],[f63]) ).
fof(f299,plain,
( ~ sP16
| e23 = op2(e23,e23) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_144,plain,
( ( op1(e13,e13) = e13 )
| ~ sP12 ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_145,plain,
( ~ sP12
| ( op1(e13,e13) != e13 ) ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_283,plain,
( ( op2(e23,e23) = e23 )
| ~ sP16 ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_284,plain,
( ~ sP16
| ( op2(e23,e23) != e23 ) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_435,plain,
~ sP16,
inference(global_subsumption_just,[status(thm)],[c_283,c_283,c_284]) ).
tcf(c_439,plain,
~ sP12,
inference(global_subsumption_just,[status(thm)],[c_144,c_144,c_145]) ).
tcf(c_471,plain,
( ( op2(e21,e21) = e23 )
| ( op2(e22,e22) = e23 )
| ( op2(e20,e20) = e23 ) ),
inference(global_subsumption_just,[status(thm)],[c_309,c_309,c_435]) ).
tcf(c_472,plain,
( ( op2(e20,e20) = e23 )
| ( op2(e22,e22) = e23 )
| ( op2(e21,e21) = e23 ) ),
inference(renaming,[status(thm)],[c_471]) ).
tcf(c_479,plain,
( ( op1(e10,e10) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e12,e12) = e13 ) ),
inference(global_subsumption_just,[status(thm)],[c_170,c_170,c_439]) ).
tcf(c_480,plain,
( ( op1(e12,e12) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e10,e10) = e13 ) ),
inference(renaming,[status(thm)],[c_479]) ).
tcf(c_2854,plain,
( ( e11 = e13 )
| ( e10 = e13 )
| ( op1(e12,e12) = e13 ) ),
inference(light_normalisation,[status(thm)],[c_480,c_2758,c_2765]) ).
tcf(c_2855,plain,
op1(e12,e12) = e13,
inference(forward_subsumption_resolution,[status(thm)],[c_2854,c_117,c_115]) ).
tcf(c_2856,plain,
op1(e10,e12) != e13,
inference(demodulation,[status(thm)],[c_191,c_2855]) ).
tcf(c_2857,plain,
op1(e11,e12) != e13,
inference(demodulation,[status(thm)],[c_193,c_2855]) ).
tcf(c_2859,plain,
op1(e12,e10) != e13,
inference(demodulation,[status(thm)],[c_215,c_2855]) ).
tcf(c_2860,plain,
op1(e12,e11) != e13,
inference(demodulation,[status(thm)],[c_217,c_2855]) ).
tcf(c_2862,plain,
( ( e23 = e20 )
| ( e21 = e23 )
| ( h3(e12) = e23 ) ),
inference(light_normalisation,[status(thm)],[c_472,c_430,c_2786,c_2812]) ).
tcf(c_2863,plain,
h3(e12) = e23,
inference(forward_subsumption_resolution,[status(thm)],[c_2862,c_319,c_321]) ).
tcf(c_2864,plain,
op2(e20,e22) != e23,
inference(demodulation,[status(thm)],[c_2733,c_2863]) ).
tcf(c_2865,plain,
op2(e21,e22) != e23,
inference(demodulation,[status(thm)],[c_2731,c_2863]) ).
tcf(c_2867,plain,
op2(e22,e20) != e23,
inference(demodulation,[status(thm)],[c_2717,c_2863]) ).
tcf(c_2868,plain,
op2(e22,e21) != e23,
inference(demodulation,[status(thm)],[c_2715,c_2863]) ).
tcf(c_2873,plain,
op2(e22,e22) = e23,
inference(demodulation,[status(thm)],[c_430,c_2863]) ).
tcf(c_2904,plain,
op2(e22,e21) = e22,
inference(forward_subsumption_resolution,[status(thm)],[c_412,c_2777,c_2868,c_2714]) ).
tcf(c_2906,plain,
h1(e10) != e22,
inference(demodulation,[status(thm)],[c_2832,c_2904]) ).
tcf(c_2908,plain,
op2(e22,e20) != e22,
inference(demodulation,[status(thm)],[c_359,c_2904]) ).
tcf(c_2910,plain,
op2(e22,e20) = e20,
inference(forward_subsumption_resolution,[status(thm)],[c_411,c_2867,c_2908,c_2716]) ).
tcf(c_2922,plain,
( ( op2(e21,e22) = e22 )
| ( op2(e21,e22) = e21 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_409,c_2730,c_2865]) ).
tcf(c_2941,plain,
op2(e21,e22) = e21,
inference(backward_subsumption_resolution,[status(thm)],[c_2922,c_2934]) ).
tcf(c_2952,plain,
op2(e20,e22) = e22,
inference(forward_subsumption_resolution,[status(thm)],[c_405,c_2732,c_2864,c_2805]) ).
tcf(c_2958,plain,
h1(e10) = e23,
inference(forward_subsumption_resolution,[status(thm)],[c_2957,c_2831,c_2906,c_2846]) ).
tcf(c_2964,plain,
op2(e20,e21) = e23,
inference(demodulation,[status(thm)],[c_2807,c_2958]) ).
tcf(c_2965,plain,
( ~ sP9
| ( e23 != e23 ) ),
inference(demodulation,[status(thm)],[c_57,c_2958]) ).
tcf(c_2966,plain,
~ sP9,
inference(equality_resolution_simp,[status(thm)],[c_2965]) ).
tcf(c_2984,plain,
op1(e12,e11) = e12,
inference(forward_subsumption_resolution,[status(thm)],[c_267,c_2860,c_2747,c_2760]) ).
tcf(c_2987,plain,
op1(e10,e11) != e12,
inference(demodulation,[status(thm)],[c_185,c_2984]) ).
tcf(c_2988,plain,
op1(e12,e10) != e12,
inference(demodulation,[status(thm)],[c_214,c_2984]) ).
tcf(c_2990,plain,
op1(e12,e10) = e10,
inference(forward_subsumption_resolution,[status(thm)],[c_266,c_2859,c_2988,c_2748]) ).
tcf(c_3002,plain,
( ( op1(e11,e12) = e12 )
| ( op1(e11,e12) = e11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_264,c_2857,c_2755]) ).
tcf(c_3010,plain,
op1(e11,e12) = e11,
inference(backward_subsumption_resolution,[status(thm)],[c_3002,c_3009]) ).
tcf(c_3021,plain,
op1(e10,e12) = e12,
inference(forward_subsumption_resolution,[status(thm)],[c_260,c_2856,c_2770,c_2756]) ).
tcf(c_3026,plain,
op1(e10,e11) = e13,
inference(forward_subsumption_resolution,[status(thm)],[c_259,c_2987,c_2769,c_2759]) ).
tcf(c_3030,plain,
( sP9
| sP10
| sP11
| ( e20 != e20 )
| ( e23 != e23 )
| ( e22 != e22 )
| ( e21 != e21 ) ),
inference(light_normalisation,[status(thm)],[c_642,c_609,c_603,c_419,c_2588,c_2589,c_2594,c_2595,c_2758,c_2765,c_2786,c_2800,c_2812,c_2855,c_2873,c_2891,c_2898,c_2904,c_2910,c_2915,c_2930,c_2937,c_2941,c_2946,c_2952,c_2958,c_2964,c_2971,c_2978,c_2984,c_2990,c_2995,c_3005,c_3010,c_3015,c_3021,c_3026]) ).
tcf(c_3031,plain,
( sP9
| sP10
| sP11 ),
inference(equality_resolution_simp,[status(thm)],[c_3030]) ).
tcf(c_3032,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_3031,c_2966,c_2939,c_2813]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG117+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/5.42 % Computer : n015.cluster.edu
% 0.15/5.42 % Model : x86_64 x86_64
% 0.15/5.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.42 % Memory : 8046.5625MB
% 0.15/5.42 % OS : Linux 6.8.0-71-generic
% 0.15/5.42 % CPULimit : 300
% 0.15/5.42 % WCLimit : 300
% 0.15/5.42 % DateTime : Fri Sep 25 04:52:17 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.15/5.43 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/5.49 Running first-order theorem proving
% 0.15/5.49 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/5.50
% 0.19/5.50 % ======== iProver multi-core TPTP/SMT =========
% 0.19/5.50
% 0.19/5.51 % Detected problem language: tptp
% 0.19/5.52 % Proving...
% 3.41/6.30 % SZS status Started for theBenchmark.p
% 3.41/6.30 % SZS status Theorem for theBenchmark.p
% 3.41/6.30
% 3.41/6.30 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.41/6.30
% 3.41/6.30 % ------ iProver source info
% 3.41/6.30
% 3.41/6.30 % git: date: 2026-07-19 20:42:38 +0200
% 3.41/6.30 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.41/6.30 % git: non_committed_changes: false
% 3.41/6.30
% 3.41/6.30 % ------ Parsing...
% 3.41/6.30 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.41/6.30
% 3.41/6.30 % ------ Preprocessing...%
% 3.41/6.30
% 3.41/6.30 % SZS status Theorem for theBenchmark.p
% 3.41/6.30
% 3.41/6.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.52/6.31
% 4.52/6.31
%------------------------------------------------------------------------------