%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ALG059+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 : n026.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:19 PM UTC 2026
% Result : Theorem 2.42s 1.29s
% Output : CNFRefutation 2.42s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f159ERROR: Could not build tree for root c_6742ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = e1
| op(e4,e4) = e0 )
& ( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = e0 )
& ( op(e4,e2) = e4
| op(e4,e2) = e3
| op(e4,e2) = e2
| op(e4,e2) = e1
| op(e4,e2) = e0 )
& ( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,e1) = e0 )
& ( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1
| op(e4,e0) = e0 )
& ( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2
| op(e3,e4) = e1
| op(e3,e4) = e0 )
& ( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e4
| op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e4
| op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e4
| op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2
| op(e2,e4) = e1
| op(e2,e4) = e0 )
& ( op(e2,e3) = e4
| op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e4
| op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 )
& ( op(e1,e3) = e4
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e4
| op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e4
| op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e4
| op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e2
| op(e0,e4) = e1
| op(e0,e4) = e0 )
& ( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e4
| op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( unit = e4
| unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e4,unit) = e4
& op(unit,e4) = e4
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op(e4,e4) = e4
| op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 )
& ( op(e4,e4) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e1) = e4
| op(e4,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e4) = e3
| op(e2,e4) = e3
| op(e1,e4) = e3
| op(e0,e4) = e3 )
& ( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 )
& ( op(e4,e4) = e2
| op(e4,e3) = e2
| op(e4,e2) = e2
| op(e4,e1) = e2
| op(e4,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 )
& ( op(e4,e4) = e1
| op(e4,e3) = e1
| op(e4,e2) = e1
| op(e4,e1) = e1
| op(e4,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 )
& ( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 )
& ( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(e0,e3) = e4 )
& ( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(e3,e0) = e4 )
& ( op(e4,e3) = e3
| op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e4) = e3
| op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e4,e3) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e4) = e2
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e4,e3) = e1
| op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e4) = e1
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e4,e3) = e0
| op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e2,e2) = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 )
& ( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e2) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 )
& ( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e4) = e3
| op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e4,e2) = e2
| op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e4,e2) = e0
| op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(e0,e1) = e4 )
& ( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(e1,e0) = e4 )
& ( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e4,e1) = e0
| op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e4) = e0
| op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e1,e0) = e4
| op(e0,e0) = e4 )
& ( op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e0) = e3
| op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e4) = e3
| op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e0) = e2
| op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e4) = e2
| op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e4,e3) != op(e4,e4)
& op(e4,e2) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e2)
& op(e4,e0) != op(e4,e4)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e1)
& op(e3,e3) != op(e3,e4)
& op(e3,e2) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e4)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e3) != op(e2,e4)
& op(e2,e2) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e4)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e3) != op(e1,e4)
& op(e1,e2) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e4)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e3) != op(e0,e4)
& op(e0,e2) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e4)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e3,e4) != op(e4,e4)
& op(e2,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e2,e4)
& op(e0,e4) != op(e4,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e1,e4)
& op(e3,e3) != op(e4,e3)
& op(e2,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e4,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e3,e2) != op(e4,e2)
& op(e2,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e4,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e3,e1) != op(e4,e1)
& op(e2,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e4,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e3,e0) != op(e4,e0)
& op(e2,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e4,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e4 = op(op(e2,e2),op(e2,e2))
& e3 = op(e2,e2)
& e1 = op(op(e2,e2),e2)
& e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f165,plain,
( ~ sP153
| ( sP124
& sP125
& sP126
& sP127
& sP128
& sP129
& sP130
& sP131
& sP132
& sP133
& sP134
& sP135
& sP136
& sP137
& sP138
& sP139
& sP140
& sP141
& sP142
& sP143
& sP144
& sP145
& sP146
& sP147
& sP148 ) ),
inference(nnf_transformation,[],[f163]) ).
fof(f166,plain,
( ~ sP152
| ( sP99
& sP100
& sP101
& sP102
& sP103
& sP104
& sP105
& sP106
& sP107
& sP108
& sP109
& sP110
& sP111
& sP112
& sP113
& sP114
& sP115
& sP116
& sP117
& sP118
& sP119
& sP120
& sP121
& sP122
& sP123 ) ),
inference(nnf_transformation,[],[f162]) ).
fof(f167,plain,
( ~ sP151
| ( sP74
& sP75
& sP76
& sP77
& sP78
& sP79
& sP80
& sP81
& sP82
& sP83
& sP84
& sP85
& sP86
& sP87
& sP88
& sP89
& sP90
& sP91
& sP92
& sP93
& sP94
& sP95
& sP96
& sP97
& sP98 ) ),
inference(nnf_transformation,[],[f161]) ).
fof(f168,plain,
( ~ sP150
| ( sP49
& sP50
& sP51
& sP52
& sP53
& sP54
& sP55
& sP56
& sP57
& sP58
& sP59
& sP60
& sP61
& sP62
& sP63
& sP64
& sP65
& sP66
& sP67
& sP68
& sP69
& sP70
& sP71
& sP72
& sP73 ) ),
inference(nnf_transformation,[],[f160]) ).
fof(f169,plain,
( ~ sP149
| ( sP24
& sP25
& sP26
& sP27
& sP28
& sP29
& sP30
& sP31
& sP32
& sP33
& sP34
& sP35
& sP36
& sP37
& sP38
& sP39
& sP40
& sP41
& sP42
& sP43
& sP44
& sP45
& sP46
& sP47
& sP48 ) ),
inference(nnf_transformation,[],[f159]) ).
fof(f170,plain,
( ~ sP148
| ( e0 != unit
& op(e0,e0) = e0 )
| op(e0,e0) != e0 ),
inference(nnf_transformation,[],[f158]) ).
fof(f174,plain,
( ~ sP144
| ( e0 != unit
& op(e0,e0) = e4 )
| op(e0,e4) != e0 ),
inference(nnf_transformation,[],[f154]) ).
fof(f179,plain,
( ~ sP139
| ( e0 != unit
& op(e1,e0) = e4 )
| op(e1,e4) != e0 ),
inference(nnf_transformation,[],[f149]) ).
fof(f184,plain,
( ~ sP134
| ( e0 != unit
& op(e2,e0) = e4 )
| op(e2,e4) != e0 ),
inference(nnf_transformation,[],[f144]) ).
fof(f189,plain,
( ~ sP129
| ( e0 != unit
& op(e3,e0) = e4 )
| op(e3,e4) != e0 ),
inference(nnf_transformation,[],[f139]) ).
fof(f194,plain,
( ~ sP124
| ( e0 != unit
& op(e4,e0) = e4 )
| op(e4,e4) != e0 ),
inference(nnf_transformation,[],[f134]) ).
fof(f208,plain,
( ~ sP110
| ( e1 != unit
& op(e2,e1) = e3 )
| op(e2,e3) != e1 ),
inference(nnf_transformation,[],[f120]) ).
fof(f230,plain,
( ~ sP88
| ( e2 != unit
& op(e2,e2) = e0 )
| op(e2,e0) != e2 ),
inference(nnf_transformation,[],[f98]) ).
fof(f260,plain,
( ~ sP58
| ( e3 != unit
& op(e3,e3) = e0 )
| op(e3,e0) != e3 ),
inference(nnf_transformation,[],[f68]) ).
fof(f290,plain,
( ~ sP28
| ( e4 != unit
& op(e4,e4) = e0 )
| op(e4,e0) != e4 ),
inference(nnf_transformation,[],[f38]) ).
fof(f295,plain,
( ~ sP23
| ( op(op(e0,e1),e0) != e1
& op(op(e0,e1),e1) = e0
& op(e1,e0) != op(e0,e1) ) ),
inference(nnf_transformation,[],[f33]) ).
fof(f296,plain,
( ~ sP22
| ( op(op(e0,e2),e0) != e2
& op(op(e0,e2),e2) = e0
& op(e2,e0) != op(e0,e2) ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f297,plain,
( ~ sP21
| ( op(op(e0,e3),e0) != e3
& op(op(e0,e3),e3) = e0
& op(e3,e0) != op(e0,e3) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f298,plain,
( ~ sP20
| ( op(op(e0,e4),e0) != e4
& op(op(e0,e4),e4) = e0
& op(e4,e0) != op(e0,e4) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f299,plain,
( ~ sP19
| ( op(op(e1,e0),e1) != e0
& op(op(e1,e0),e0) = e1
& op(e0,e1) != op(e1,e0) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f301,plain,
( ~ sP17
| ( op(op(e1,e2),e1) != e2
& op(op(e1,e2),e2) = e1
& op(e2,e1) != op(e1,e2) ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f302,plain,
( ~ sP16
| ( op(op(e1,e3),e1) != e3
& op(op(e1,e3),e3) = e1
& op(e3,e1) != op(e1,e3) ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f303,plain,
( ~ sP15
| ( op(op(e1,e4),e1) != e4
& op(op(e1,e4),e4) = e1
& op(e4,e1) != op(e1,e4) ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f304,plain,
( ~ sP14
| ( op(op(e2,e0),e2) != e0
& op(op(e2,e0),e0) = e2
& op(e0,e2) != op(e2,e0) ) ),
inference(nnf_transformation,[],[f24]) ).
fof(f305,plain,
( ~ sP13
| ( op(op(e2,e1),e2) != e1
& op(op(e2,e1),e1) = e2
& op(e1,e2) != op(e2,e1) ) ),
inference(nnf_transformation,[],[f23]) ).
fof(f307,plain,
( ~ sP11
| ( op(op(e2,e3),e2) != e3
& op(op(e2,e3),e3) = e2
& op(e3,e2) != op(e2,e3) ) ),
inference(nnf_transformation,[],[f21]) ).
fof(f308,plain,
( ~ sP10
| ( op(op(e2,e4),e2) != e4
& op(op(e2,e4),e4) = e2
& op(e4,e2) != op(e2,e4) ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f309,plain,
( ~ sP9
| ( op(op(e3,e0),e3) != e0
& op(op(e3,e0),e0) = e3
& op(e0,e3) != op(e3,e0) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f310,plain,
( ~ sP8
| ( op(op(e3,e1),e3) != e1
& op(op(e3,e1),e1) = e3
& op(e1,e3) != op(e3,e1) ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f311,plain,
( ~ sP7
| ( op(op(e3,e2),e3) != e2
& op(op(e3,e2),e2) = e3
& op(e2,e3) != op(e3,e2) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f313,plain,
( ~ sP5
| ( op(op(e3,e4),e3) != e4
& op(op(e3,e4),e4) = e3
& op(e4,e3) != op(e3,e4) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f314,plain,
( ~ sP4
| ( op(op(e4,e0),e4) != e0
& op(op(e4,e0),e0) = e4
& op(e0,e4) != op(e4,e0) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f315,plain,
( ~ sP3
| ( op(op(e4,e1),e4) != e1
& op(op(e4,e1),e1) = e4
& op(e1,e4) != op(e4,e1) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f316,plain,
( ~ sP2
| ( op(op(e4,e2),e4) != e2
& op(op(e4,e2),e2) = e4
& op(e2,e4) != op(e4,e2) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f317,plain,
( ~ sP1
| ( op(op(e4,e3),e4) != e3
& op(op(e4,e3),e3) = e4
& op(e3,e4) != op(e4,e3) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f321,plain,
( e4 = op(e4,e2)
| e3 = op(e4,e2)
| e2 = op(e4,e2)
| e1 = op(e4,e2)
| e0 = op(e4,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f329,plain,
( e4 = op(e2,e4)
| e3 = op(e2,e4)
| e2 = op(e2,e4)
| e1 = op(e2,e4)
| e0 = op(e2,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f335,plain,
( e4 = op(e1,e3)
| e3 = op(e1,e3)
| e2 = op(e1,e3)
| e1 = op(e1,e3)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f344,plain,
( e4 = unit
| e3 = unit
| e2 = unit
| e1 = unit
| e0 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f345,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f346,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f347,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f348,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f349,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f350,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f351,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f352,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f354,plain,
e0 = op(unit,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f363,plain,
( e0 = op(e4,e4)
| e0 = op(e3,e4)
| e0 = op(e2,e4)
| e0 = op(e1,e4)
| e0 = op(e0,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f370,plain,
( e2 = op(e3,e4)
| e2 = op(e3,e3)
| e2 = op(e3,e2)
| e2 = op(e3,e1)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f371,plain,
( e1 = op(e4,e3)
| e1 = op(e3,e3)
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f374,plain,
( e0 = op(e3,e4)
| e0 = op(e3,e3)
| e0 = op(e3,e2)
| e0 = op(e3,e1)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f375,plain,
( e4 = op(e4,e2)
| e4 = op(e3,e2)
| e4 = op(e2,e2)
| e4 = op(e1,e2)
| e4 = op(e0,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f376,plain,
( e4 = op(e2,e4)
| e4 = op(e2,e3)
| e4 = op(e2,e2)
| e4 = op(e2,e1)
| e4 = op(e2,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f384,plain,
( e0 = op(e2,e4)
| e0 = op(e2,e3)
| e0 = op(e2,e2)
| e0 = op(e2,e1)
| e0 = op(e2,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f387,plain,
( e3 = op(e4,e1)
| e3 = op(e3,e1)
| e3 = op(e2,e1)
| e3 = op(e1,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f388,plain,
( e3 = op(e1,e4)
| e3 = op(e1,e3)
| e3 = op(e1,e2)
| e3 = op(e1,e1)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f413,plain,
op(e4,e0) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f417,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f424,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f426,plain,
op(e2,e2) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f430,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f431,plain,
op(e2,e0) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f439,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f442,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f446,plain,
op(e0,e2) != op(e0,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f449,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f455,plain,
op(e3,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f457,plain,
op(e2,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f463,plain,
op(e0,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f465,plain,
op(e3,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f467,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f469,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f474,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f475,plain,
op(e3,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f476,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f480,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f481,plain,
op(e0,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f489,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f490,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f495,plain,
op(e3,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f496,plain,
op(e2,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f499,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f505,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f506,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f507,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f508,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f509,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f510,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f511,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f512,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f513,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f514,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f515,plain,
e4 = op(op(e2,e2),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f516,plain,
e3 = op(e2,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f517,plain,
e1 = op(op(e2,e2),e2),
inference(cnf_transformation,[],[f6]) ).
fof(f518,plain,
e0 = op(op(op(e2,e2),e2),op(op(e2,e2),e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f519,plain,
( ~ sP153
| sP124 ),
inference(cnf_transformation,[],[f165]) ).
fof(f524,plain,
( ~ sP153
| sP129 ),
inference(cnf_transformation,[],[f165]) ).
fof(f529,plain,
( ~ sP153
| sP134 ),
inference(cnf_transformation,[],[f165]) ).
fof(f534,plain,
( ~ sP153
| sP139 ),
inference(cnf_transformation,[],[f165]) ).
fof(f539,plain,
( ~ sP153
| sP144 ),
inference(cnf_transformation,[],[f165]) ).
fof(f543,plain,
( ~ sP153
| sP148 ),
inference(cnf_transformation,[],[f165]) ).
fof(f555,plain,
( ~ sP152
| sP110 ),
inference(cnf_transformation,[],[f166]) ).
fof(f583,plain,
( ~ sP151
| sP88 ),
inference(cnf_transformation,[],[f167]) ).
fof(f603,plain,
( ~ sP150
| sP58 ),
inference(cnf_transformation,[],[f168]) ).
fof(f623,plain,
( ~ sP149
| sP28 ),
inference(cnf_transformation,[],[f169]) ).
fof(f644,plain,
( ~ sP148
| e0 != unit
| e0 != op(e0,e0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f652,plain,
( ~ sP144
| e0 != unit
| e0 != op(e0,e4) ),
inference(cnf_transformation,[],[f174]) ).
fof(f662,plain,
( ~ sP139
| e0 != unit
| e0 != op(e1,e4) ),
inference(cnf_transformation,[],[f179]) ).
fof(f672,plain,
( ~ sP134
| e0 != unit
| e0 != op(e2,e4) ),
inference(cnf_transformation,[],[f184]) ).
fof(f682,plain,
( ~ sP129
| e0 != unit
| e0 != op(e3,e4) ),
inference(cnf_transformation,[],[f189]) ).
fof(f692,plain,
( ~ sP124
| e0 != unit
| e0 != op(e4,e4) ),
inference(cnf_transformation,[],[f194]) ).
fof(f721,plain,
( ~ sP110
| e3 = op(e2,e1)
| e1 != op(e2,e3) ),
inference(cnf_transformation,[],[f208]) ).
fof(f765,plain,
( ~ sP88
| e0 = op(e2,e2)
| e2 != op(e2,e0) ),
inference(cnf_transformation,[],[f230]) ).
fof(f825,plain,
( ~ sP58
| e0 = op(e3,e3)
| e3 != op(e3,e0) ),
inference(cnf_transformation,[],[f260]) ).
fof(f885,plain,
( ~ sP28
| e0 = op(e4,e4)
| e4 != op(e4,e0) ),
inference(cnf_transformation,[],[f290]) ).
fof(f896,plain,
( ~ sP23
| op(e0,e1) != op(e1,e0) ),
inference(cnf_transformation,[],[f295]) ).
fof(f899,plain,
( ~ sP22
| op(e0,e2) != op(e2,e0) ),
inference(cnf_transformation,[],[f296]) ).
fof(f902,plain,
( ~ sP21
| op(e0,e3) != op(e3,e0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f905,plain,
( ~ sP20
| op(e0,e4) != op(e4,e0) ),
inference(cnf_transformation,[],[f298]) ).
fof(f906,plain,
( ~ sP19
| e0 != op(op(e1,e0),e1) ),
inference(cnf_transformation,[],[f299]) ).
fof(f914,plain,
( ~ sP17
| op(e1,e2) != op(e2,e1) ),
inference(cnf_transformation,[],[f301]) ).
fof(f917,plain,
( ~ sP16
| op(e1,e3) != op(e3,e1) ),
inference(cnf_transformation,[],[f302]) ).
fof(f920,plain,
( ~ sP15
| op(e1,e4) != op(e4,e1) ),
inference(cnf_transformation,[],[f303]) ).
fof(f923,plain,
( ~ sP14
| op(e0,e2) != op(e2,e0) ),
inference(cnf_transformation,[],[f304]) ).
fof(f926,plain,
( ~ sP13
| op(e1,e2) != op(e2,e1) ),
inference(cnf_transformation,[],[f305]) ).
fof(f931,plain,
( ~ sP11
| e2 = op(op(e2,e3),e3) ),
inference(cnf_transformation,[],[f307]) ).
fof(f933,plain,
( ~ sP10
| e4 != op(op(e2,e4),e2) ),
inference(cnf_transformation,[],[f308]) ).
fof(f938,plain,
( ~ sP9
| op(e0,e3) != op(e3,e0) ),
inference(cnf_transformation,[],[f309]) ).
fof(f941,plain,
( ~ sP8
| op(e1,e3) != op(e3,e1) ),
inference(cnf_transformation,[],[f310]) ).
fof(f943,plain,
( ~ sP7
| e3 = op(op(e3,e2),e2) ),
inference(cnf_transformation,[],[f311]) ).
fof(f949,plain,
( ~ sP5
| e3 = op(op(e3,e4),e4) ),
inference(cnf_transformation,[],[f313]) ).
fof(f953,plain,
( ~ sP4
| op(e0,e4) != op(e4,e0) ),
inference(cnf_transformation,[],[f314]) ).
fof(f956,plain,
( ~ sP3
| op(e1,e4) != op(e4,e1) ),
inference(cnf_transformation,[],[f315]) ).
fof(f958,plain,
( ~ sP2
| e4 = op(op(e4,e2),e2) ),
inference(cnf_transformation,[],[f316]) ).
fof(f960,plain,
( ~ sP1
| e3 != op(op(e4,e3),e4) ),
inference(cnf_transformation,[],[f317]) ).
fof(f966,plain,
( sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| e0 != op(op(e0,e0),e0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f969,plain,
( sP149
| sP150
| sP151
| sP152
| sP153 ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_57,plain,
( ( op(e1,e3) = e4 )
| ( op(e1,e3) = e3 )
| ( op(e1,e3) = e2 )
| ( op(e1,e3) = e1 )
| ( op(e1,e3) = e0 ) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_63,plain,
( ( op(e2,e4) = e4 )
| ( op(e2,e4) = e3 )
| ( op(e2,e4) = e2 )
| ( op(e2,e4) = e1 )
| ( op(e2,e4) = e0 ) ),
inference(cnf_transformation,[],[f329]) ).
tcf(c_71,plain,
( ( op(e4,e2) = e4 )
| ( op(e4,e2) = e3 )
| ( op(e4,e2) = e2 )
| ( op(e4,e2) = e1 )
| ( op(e4,e2) = e0 ) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_74,plain,
op(unit,e0) = e0,
inference(cnf_transformation,[],[f354]) ).
tcf(c_76,plain,
op(unit,e1) = e1,
inference(cnf_transformation,[],[f352]) ).
tcf(c_77,plain,
op(e1,unit) = e1,
inference(cnf_transformation,[],[f351]) ).
tcf(c_78,plain,
op(unit,e2) = e2,
inference(cnf_transformation,[],[f350]) ).
tcf(c_79,plain,
op(e2,unit) = e2,
inference(cnf_transformation,[],[f349]) ).
tcf(c_80,plain,
op(unit,e3) = e3,
inference(cnf_transformation,[],[f348]) ).
tcf(c_81,plain,
op(e3,unit) = e3,
inference(cnf_transformation,[],[f347]) ).
tcf(c_82,plain,
op(unit,e4) = e4,
inference(cnf_transformation,[],[f346]) ).
tcf(c_83,plain,
op(e4,unit) = e4,
inference(cnf_transformation,[],[f345]) ).
tcf(c_84,plain,
( ( e4 = unit )
| ( e3 = unit )
| ( e2 = unit )
| ( e1 = unit )
| ( e0 = unit ) ),
inference(cnf_transformation,[],[f344]) ).
tcf(c_101,plain,
( ( op(e1,e4) = e3 )
| ( op(e1,e3) = e3 )
| ( op(e1,e2) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e1,e0) = e3 ) ),
inference(cnf_transformation,[],[f388]) ).
tcf(c_102,plain,
( ( op(e4,e1) = e3 )
| ( op(e3,e1) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(cnf_transformation,[],[f387]) ).
tcf(c_105,plain,
( ( op(e2,e4) = e0 )
| ( op(e2,e3) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e2,e1) = e0 )
| ( op(e2,e0) = e0 ) ),
inference(cnf_transformation,[],[f384]) ).
tcf(c_113,plain,
( ( op(e2,e4) = e4 )
| ( op(e2,e3) = e4 )
| ( op(e2,e2) = e4 )
| ( op(e2,e1) = e4 )
| ( op(e2,e0) = e4 ) ),
inference(cnf_transformation,[],[f376]) ).
tcf(c_114,plain,
( ( op(e4,e2) = e4 )
| ( op(e3,e2) = e4 )
| ( op(e2,e2) = e4 )
| ( op(e1,e2) = e4 )
| ( op(e0,e2) = e4 ) ),
inference(cnf_transformation,[],[f375]) ).
tcf(c_115,plain,
( ( op(e3,e4) = e0 )
| ( op(e3,e3) = e0 )
| ( op(e3,e2) = e0 )
| ( op(e3,e1) = e0 )
| ( op(e3,e0) = e0 ) ),
inference(cnf_transformation,[],[f374]) ).
tcf(c_118,plain,
( ( op(e4,e3) = e1 )
| ( op(e3,e3) = e1 )
| ( op(e2,e3) = e1 )
| ( op(e1,e3) = e1 )
| ( op(e0,e3) = e1 ) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_119,plain,
( ( op(e3,e4) = e2 )
| ( op(e3,e3) = e2 )
| ( op(e3,e2) = e2 )
| ( op(e3,e1) = e2 )
| ( op(e3,e0) = e2 ) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_126,plain,
( ( op(e4,e4) = e0 )
| ( op(e3,e4) = e0 )
| ( op(e2,e4) = e0 )
| ( op(e1,e4) = e0 )
| ( op(e0,e4) = e0 ) ),
inference(cnf_transformation,[],[f363]) ).
tcf(c_140,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f499]) ).
tcf(c_143,plain,
op(e2,e0) != op(e4,e0),
inference(cnf_transformation,[],[f496]) ).
tcf(c_144,plain,
op(e3,e0) != op(e4,e0),
inference(cnf_transformation,[],[f495]) ).
tcf(c_149,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f490]) ).
tcf(c_150,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f489]) ).
tcf(c_158,plain,
op(e0,e2) != op(e4,e2),
inference(cnf_transformation,[],[f481]) ).
tcf(c_159,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f480]) ).
tcf(c_163,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f476]) ).
tcf(c_164,plain,
op(e3,e2) != op(e4,e2),
inference(cnf_transformation,[],[f475]) ).
tcf(c_165,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f474]) ).
tcf(c_170,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f469]) ).
tcf(c_172,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f467]) ).
tcf(c_174,plain,
op(e3,e3) != op(e4,e3),
inference(cnf_transformation,[],[f465]) ).
tcf(c_176,plain,
op(e0,e4) != op(e2,e4),
inference(cnf_transformation,[],[f463]) ).
tcf(c_182,plain,
op(e2,e4) != op(e3,e4),
inference(cnf_transformation,[],[f457]) ).
tcf(c_184,plain,
op(e3,e4) != op(e4,e4),
inference(cnf_transformation,[],[f455]) ).
tcf(c_190,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f449]) ).
tcf(c_193,plain,
op(e0,e2) != op(e0,e4),
inference(cnf_transformation,[],[f446]) ).
tcf(c_197,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f442]) ).
tcf(c_200,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f439]) ).
tcf(c_208,plain,
op(e2,e0) != op(e2,e4),
inference(cnf_transformation,[],[f431]) ).
tcf(c_209,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f430]) ).
tcf(c_213,plain,
op(e2,e2) != op(e2,e4),
inference(cnf_transformation,[],[f426]) ).
tcf(c_215,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f424]) ).
tcf(c_222,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f417]) ).
tcf(c_226,plain,
op(e4,e0) != op(e4,e2),
inference(cnf_transformation,[],[f413]) ).
tcf(c_235,plain,
e0 != e1,
inference(cnf_transformation,[],[f514]) ).
tcf(c_236,plain,
e0 != e2,
inference(cnf_transformation,[],[f513]) ).
tcf(c_237,plain,
e0 != e3,
inference(cnf_transformation,[],[f512]) ).
tcf(c_238,plain,
e0 != e4,
inference(cnf_transformation,[],[f511]) ).
tcf(c_239,plain,
e1 != e2,
inference(cnf_transformation,[],[f510]) ).
tcf(c_240,plain,
e1 != e3,
inference(cnf_transformation,[],[f509]) ).
tcf(c_241,plain,
e1 != e4,
inference(cnf_transformation,[],[f508]) ).
tcf(c_242,plain,
e2 != e3,
inference(cnf_transformation,[],[f507]) ).
tcf(c_243,plain,
e2 != e4,
inference(cnf_transformation,[],[f506]) ).
tcf(c_244,plain,
e3 != e4,
inference(cnf_transformation,[],[f505]) ).
tcf(c_245,plain,
op(op(op(e2,e2),e2),op(op(e2,e2),e2)) = e0,
inference(cnf_transformation,[],[f518]) ).
tcf(c_246,plain,
op(op(e2,e2),e2) = e1,
inference(cnf_transformation,[],[f517]) ).
tcf(c_247,plain,
op(e2,e2) = e3,
inference(cnf_transformation,[],[f516]) ).
tcf(c_248,plain,
op(op(e2,e2),op(e2,e2)) = e4,
inference(cnf_transformation,[],[f515]) ).
tcf(c_249,plain,
( sP148
| ~ sP153 ),
inference(cnf_transformation,[],[f543]) ).
tcf(c_253,plain,
( sP144
| ~ sP153 ),
inference(cnf_transformation,[],[f539]) ).
tcf(c_258,plain,
( sP139
| ~ sP153 ),
inference(cnf_transformation,[],[f534]) ).
tcf(c_263,plain,
( sP134
| ~ sP153 ),
inference(cnf_transformation,[],[f529]) ).
tcf(c_268,plain,
( sP129
| ~ sP153 ),
inference(cnf_transformation,[],[f524]) ).
tcf(c_273,plain,
( sP124
| ~ sP153 ),
inference(cnf_transformation,[],[f519]) ).
tcf(c_287,plain,
( sP110
| ~ sP152 ),
inference(cnf_transformation,[],[f555]) ).
tcf(c_309,plain,
( sP88
| ~ sP151 ),
inference(cnf_transformation,[],[f583]) ).
tcf(c_339,plain,
( sP58
| ~ sP150 ),
inference(cnf_transformation,[],[f603]) ).
tcf(c_369,plain,
( sP28
| ~ sP149 ),
inference(cnf_transformation,[],[f623]) ).
tcf(c_374,plain,
( ~ sP148
| ( e0 != unit )
| ( op(e0,e0) != e0 ) ),
inference(cnf_transformation,[],[f644]) ).
tcf(c_382,plain,
( ~ sP144
| ( e0 != unit )
| ( op(e0,e4) != e0 ) ),
inference(cnf_transformation,[],[f652]) ).
tcf(c_391,plain,
( ~ sP139
| ( e0 != unit )
| ( op(e1,e4) != e0 ) ),
inference(cnf_transformation,[],[f662]) ).
tcf(c_400,plain,
( ~ sP134
| ( e0 != unit )
| ( op(e2,e4) != e0 ) ),
inference(cnf_transformation,[],[f672]) ).
tcf(c_409,plain,
( ~ sP129
| ( e0 != unit )
| ( op(e3,e4) != e0 ) ),
inference(cnf_transformation,[],[f682]) ).
tcf(c_418,plain,
( ~ sP124
| ( e0 != unit )
| ( op(e4,e4) != e0 ) ),
inference(cnf_transformation,[],[f692]) ).
tcf(c_442,plain,
( ( op(e2,e1) = e3 )
| ~ sP110
| ( op(e2,e3) != e1 ) ),
inference(cnf_transformation,[],[f721]) ).
tcf(c_482,plain,
( ( op(e2,e2) = e0 )
| ~ sP88
| ( op(e2,e0) != e2 ) ),
inference(cnf_transformation,[],[f765]) ).
tcf(c_536,plain,
( ( op(e3,e3) = e0 )
| ~ sP58
| ( op(e3,e0) != e3 ) ),
inference(cnf_transformation,[],[f825]) ).
tcf(c_590,plain,
( ( op(e4,e4) = e0 )
| ~ sP28
| ( op(e4,e0) != e4 ) ),
inference(cnf_transformation,[],[f885]) ).
tcf(c_599,plain,
( ~ sP23
| ( op(e0,e1) != op(e1,e0) ) ),
inference(cnf_transformation,[],[f896]) ).
tcf(c_602,plain,
( ~ sP22
| ( op(e0,e2) != op(e2,e0) ) ),
inference(cnf_transformation,[],[f899]) ).
tcf(c_605,plain,
( ~ sP21
| ( op(e0,e3) != op(e3,e0) ) ),
inference(cnf_transformation,[],[f902]) ).
tcf(c_608,plain,
( ~ sP20
| ( op(e0,e4) != op(e4,e0) ) ),
inference(cnf_transformation,[],[f905]) ).
tcf(c_613,plain,
( ~ sP19
| ( op(op(e1,e0),e1) != e0 ) ),
inference(cnf_transformation,[],[f906]) ).
tcf(c_614,plain,
~ sP18,
inference(cnf_transformation,[],[f970]) ).
tcf(c_617,plain,
( ~ sP17
| ( op(e1,e2) != op(e2,e1) ) ),
inference(cnf_transformation,[],[f914]) ).
tcf(c_620,plain,
( ~ sP16
| ( op(e1,e3) != op(e3,e1) ) ),
inference(cnf_transformation,[],[f917]) ).
tcf(c_623,plain,
( ~ sP15
| ( op(e1,e4) != op(e4,e1) ) ),
inference(cnf_transformation,[],[f920]) ).
tcf(c_626,plain,
( ~ sP14
| ( op(e0,e2) != op(e2,e0) ) ),
inference(cnf_transformation,[],[f923]) ).
tcf(c_629,plain,
( ~ sP13
| ( op(e1,e2) != op(e2,e1) ) ),
inference(cnf_transformation,[],[f926]) ).
tcf(c_632,plain,
~ sP12,
inference(cnf_transformation,[],[f971]) ).
tcf(c_636,plain,
( ( op(op(e2,e3),e3) = e2 )
| ~ sP11 ),
inference(cnf_transformation,[],[f931]) ).
tcf(c_640,plain,
( ~ sP10
| ( op(op(e2,e4),e2) != e4 ) ),
inference(cnf_transformation,[],[f933]) ).
tcf(c_641,plain,
( ~ sP9
| ( op(e0,e3) != op(e3,e0) ) ),
inference(cnf_transformation,[],[f938]) ).
tcf(c_644,plain,
( ~ sP8
| ( op(e1,e3) != op(e3,e1) ) ),
inference(cnf_transformation,[],[f941]) ).
tcf(c_648,plain,
( ( op(op(e3,e2),e2) = e3 )
| ~ sP7 ),
inference(cnf_transformation,[],[f943]) ).
tcf(c_650,plain,
~ sP6,
inference(cnf_transformation,[],[f972]) ).
tcf(c_654,plain,
( ( op(op(e3,e4),e4) = e3 )
| ~ sP5 ),
inference(cnf_transformation,[],[f949]) ).
tcf(c_656,plain,
( ~ sP4
| ( op(e0,e4) != op(e4,e0) ) ),
inference(cnf_transformation,[],[f953]) ).
tcf(c_659,plain,
( ~ sP3
| ( op(e1,e4) != op(e4,e1) ) ),
inference(cnf_transformation,[],[f956]) ).
tcf(c_663,plain,
( ( op(op(e4,e2),e2) = e4 )
| ~ sP2 ),
inference(cnf_transformation,[],[f958]) ).
tcf(c_667,plain,
( ~ sP1
| ( op(op(e4,e3),e4) != e3 ) ),
inference(cnf_transformation,[],[f960]) ).
tcf(c_668,plain,
~ sP0,
inference(cnf_transformation,[],[f973]) ).
tcf(c_671,negated_conjecture,
( sP149
| sP150
| sP151
| sP152
| sP153 ),
inference(cnf_transformation,[],[f969]) ).
tcf(c_672,negated_conjecture,
( sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(cnf_transformation,[],[f974]) ).
tcf(c_674,negated_conjecture,
( sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| ( op(op(e0,e0),e0) != e0 ) ),
inference(cnf_transformation,[],[f966]) ).
tcf(c_697,plain,
( sP7
| sP8
| sP9
| sP10
| sP11
| sP19
| sP20
| sP21
| sP22
| sP23
| sP17
| sP16
| sP15
| sP14
| sP13
| sP5
| sP4
| sP3
| sP2
| sP1 ),
inference(global_subsumption_just,[status(thm)],[c_672,c_668,c_650,c_632,c_614,c_672]) ).
tcf(c_698,negated_conjecture,
( sP1
| sP2
| sP3
| sP4
| sP5
| sP7
| sP8
| sP9
| sP10
| sP11
| sP13
| sP14
| sP15
| sP16
| sP17
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(renaming,[status(thm)],[c_697]) ).
tcf(c_707,plain,
( sP7
| sP8
| sP9
| sP10
| sP11
| sP19
| sP20
| sP21
| sP22
| sP23
| sP17
| sP16
| sP15
| sP14
| sP13
| sP5
| sP4
| sP3
| sP2
| sP1 ),
inference(global_subsumption_just,[status(thm)],[c_674,c_698]) ).
tcf(c_708,negated_conjecture,
( sP1
| sP2
| sP3
| sP4
| sP5
| sP7
| sP8
| sP9
| sP10
| sP11
| sP13
| sP14
| sP15
| sP16
| sP17
| sP19
| sP20
| sP21
| sP22
| sP23 ),
inference(renaming,[status(thm)],[c_707]) ).
tcf(c_3828,plain,
( ~ sP153
| ( e0 != unit )
| ( op(e0,e0) != e0 ) ),
inference(resolution,[status(thm)],[c_249,c_374]) ).
tcf(c_3829,plain,
( ~ sP153
| ( e0 != unit ) ),
inference(global_subsumption_just,[status(thm)],[c_3828,c_273,c_268,c_263,c_258,c_253,c_418,c_409,c_400,c_391,c_382,c_126]) ).
tcf(c_4335,plain,
( ( op(e2,e1) = e3 )
| ~ sP152
| ( op(e2,e3) != e1 ) ),
inference(resolution,[status(thm)],[c_287,c_442]) ).
tcf(c_4587,plain,
( ( op(e2,e2) = e0 )
| ~ sP151
| ( op(e2,e0) != e2 ) ),
inference(resolution,[status(thm)],[c_309,c_482]) ).
tcf(c_4895,plain,
( ( op(e3,e3) = e0 )
| ~ sP150
| ( op(e3,e0) != e3 ) ),
inference(resolution,[status(thm)],[c_339,c_536]) ).
tcf(c_5231,plain,
( ( op(e4,e4) = e0 )
| ~ sP149
| ( op(e4,e0) != e4 ) ),
inference(resolution,[status(thm)],[c_369,c_590]) ).
tcf(c_6742,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_5231,c_4895,c_4587,c_4335,c_3829,c_708,c_671,c_667,c_663,c_659,c_656,c_654,c_648,c_644,c_641,c_640,c_636,c_629,c_626,c_623,c_620,c_617,c_613,c_608,c_605,c_602,c_599,c_248,c_247,c_246,c_245,c_244,c_243,c_242,c_241,c_240,c_239,c_238,c_237,c_236,c_235,c_226,c_222,c_215,c_213,c_209,c_208,c_200,c_197,c_193,c_190,c_184,c_182,c_176,c_174,c_172,c_170,c_165,c_164,c_163,c_159,c_158,c_150,c_149,c_144,c_143,c_140,c_119,c_118,c_115,c_114,c_113,c_105,c_102,c_101,c_84,c_83,c_82,c_81,c_80,c_79,c_78,c_77,c_76,c_74,c_71,c_63,c_57]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG059+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Fri Sep 25 04:42:41 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.39 Running first-order theorem proving
% 0.11/0.39 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.11/0.40
% 0.11/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.40
% 0.11/0.41 % Detected problem language: tptp
% 0.11/0.42 % Proving...
% 2.42/1.29 % SZS status Started for theBenchmark.p
% 2.42/1.29 % SZS status Theorem for theBenchmark.p
% 2.42/1.29
% 2.42/1.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.42/1.29
% 2.42/1.29 % ------ iProver source info
% 2.42/1.29
% 2.42/1.29 % git: date: 2026-07-19 20:42:38 +0200
% 2.42/1.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.42/1.29 % git: non_committed_changes: false
% 2.42/1.29
% 2.42/1.29 % ------ Parsing...
% 2.42/1.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.42/1.29
% 2.42/1.29 % ------ Preprocessing... sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s pe:64:0s pe_e %
% 2.42/1.29
% 2.42/1.29 % ------ Preprocessing...%
% 2.42/1.29
% 2.42/1.29 % SZS status Theorem for theBenchmark.p
% 2.42/1.29
% 2.42/1.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.42/1.29
% 2.42/1.29
%------------------------------------------------------------------------------