%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ALG046+1 : TPTP v9.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 05:24:03 PM UTC 2025
% Result : Unsatisfiable 10.84s 3.55s
% Output : CNFRefutation 11.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 18
% Syntax : Number of formulae : 802 ( 553 unt; 0 typ; 0 def)
% Number of atoms : 1607 (1526 equ)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 1163 ( 358 ~; 663 |; 142 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ op > #nlpp > unit > e3 > e2 > e1 > e0
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(e1,type,
e1: $i ).
tff(e0,type,
e0: $i ).
tff(e2,type,
e2: $i ).
tff(op,type,
op: ( $i * $i ) > $i ).
tff(unit,type,
unit: $i ).
tff(e3,type,
e3: $i ).
tff(f_590,axiom,
( ( e0 != e1 )
& ( e0 != e2 )
& ( e0 != e3 )
& ( e1 != e2 )
& ( e1 != e3 )
& ( e2 != e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
tff(f_175,axiom,
( ( op(unit,e0) = e0 )
& ( op(e0,unit) = e0 )
& ( op(unit,e1) = e1 )
& ( op(e1,unit) = e1 )
& ( op(unit,e2) = e2 )
& ( op(e2,unit) = e2 )
& ( op(unit,e3) = e3 )
& ( op(e3,unit) = e3 )
& ( ( unit = e0 )
| ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
tff(f_573,axiom,
( ( op(e0,e0) != op(e1,e0) )
& ( op(e0,e0) != op(e2,e0) )
& ( op(e0,e0) != op(e3,e0) )
& ( op(e1,e0) != op(e2,e0) )
& ( op(e1,e0) != op(e3,e0) )
& ( op(e2,e0) != op(e3,e0) )
& ( op(e0,e1) != op(e1,e1) )
& ( op(e0,e1) != op(e2,e1) )
& ( op(e0,e1) != op(e3,e1) )
& ( op(e1,e1) != op(e2,e1) )
& ( op(e1,e1) != op(e3,e1) )
& ( op(e2,e1) != op(e3,e1) )
& ( op(e0,e2) != op(e1,e2) )
& ( op(e0,e2) != op(e2,e2) )
& ( op(e0,e2) != op(e3,e2) )
& ( op(e1,e2) != op(e2,e2) )
& ( op(e1,e2) != op(e3,e2) )
& ( op(e2,e2) != op(e3,e2) )
& ( op(e0,e3) != op(e1,e3) )
& ( op(e0,e3) != op(e2,e3) )
& ( op(e0,e3) != op(e3,e3) )
& ( op(e1,e3) != op(e2,e3) )
& ( op(e1,e3) != op(e3,e3) )
& ( op(e2,e3) != op(e3,e3) )
& ( op(e0,e0) != op(e0,e1) )
& ( op(e0,e0) != op(e0,e2) )
& ( op(e0,e0) != op(e0,e3) )
& ( op(e0,e1) != op(e0,e2) )
& ( op(e0,e1) != op(e0,e3) )
& ( op(e0,e2) != op(e0,e3) )
& ( op(e1,e0) != op(e1,e1) )
& ( op(e1,e0) != op(e1,e2) )
& ( op(e1,e0) != op(e1,e3) )
& ( op(e1,e1) != op(e1,e2) )
& ( op(e1,e1) != op(e1,e3) )
& ( op(e1,e2) != op(e1,e3) )
& ( op(e2,e0) != op(e2,e1) )
& ( op(e2,e0) != op(e2,e2) )
& ( op(e2,e0) != op(e2,e3) )
& ( op(e2,e1) != op(e2,e2) )
& ( op(e2,e1) != op(e2,e3) )
& ( op(e2,e2) != op(e2,e3) )
& ( op(e3,e0) != op(e3,e1) )
& ( op(e3,e0) != op(e3,e2) )
& ( op(e3,e0) != op(e3,e3) )
& ( op(e3,e1) != op(e3,e2) )
& ( op(e3,e1) != op(e3,e3) )
& ( op(e3,e2) != op(e3,e3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
tff(f_152,axiom,
( ( ( op(e0,e0) = e0 )
| ( op(e0,e0) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e0,e0) = e3 ) )
& ( ( op(e0,e1) = e0 )
| ( op(e0,e1) = e1 )
| ( op(e0,e1) = e2 )
| ( op(e0,e1) = e3 ) )
& ( ( op(e0,e2) = e0 )
| ( op(e0,e2) = e1 )
| ( op(e0,e2) = e2 )
| ( op(e0,e2) = e3 ) )
& ( ( op(e0,e3) = e0 )
| ( op(e0,e3) = e1 )
| ( op(e0,e3) = e2 )
| ( op(e0,e3) = e3 ) )
& ( ( op(e1,e0) = e0 )
| ( op(e1,e0) = e1 )
| ( op(e1,e0) = e2 )
| ( op(e1,e0) = e3 ) )
& ( ( op(e1,e1) = e0 )
| ( op(e1,e1) = e1 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e3 ) )
& ( ( op(e1,e2) = e0 )
| ( op(e1,e2) = e1 )
| ( op(e1,e2) = e2 )
| ( op(e1,e2) = e3 ) )
& ( ( op(e1,e3) = e0 )
| ( op(e1,e3) = e1 )
| ( op(e1,e3) = e2 )
| ( op(e1,e3) = e3 ) )
& ( ( op(e2,e0) = e0 )
| ( op(e2,e0) = e1 )
| ( op(e2,e0) = e2 )
| ( op(e2,e0) = e3 ) )
& ( ( op(e2,e1) = e0 )
| ( op(e2,e1) = e1 )
| ( op(e2,e1) = e2 )
| ( op(e2,e1) = e3 ) )
& ( ( op(e2,e2) = e0 )
| ( op(e2,e2) = e1 )
| ( op(e2,e2) = e2 )
| ( op(e2,e2) = e3 ) )
& ( ( op(e2,e3) = e0 )
| ( op(e2,e3) = e1 )
| ( op(e2,e3) = e2 )
| ( op(e2,e3) = e3 ) )
& ( ( op(e3,e0) = e0 )
| ( op(e3,e0) = e1 )
| ( op(e3,e0) = e2 )
| ( op(e3,e0) = e3 ) )
& ( ( op(e3,e1) = e0 )
| ( op(e3,e1) = e1 )
| ( op(e3,e1) = e2 )
| ( op(e3,e1) = e3 ) )
& ( ( op(e3,e2) = e0 )
| ( op(e3,e2) = e1 )
| ( op(e3,e2) = e2 )
| ( op(e3,e2) = e3 ) )
& ( ( op(e3,e3) = e0 )
| ( op(e3,e3) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e3,e3) = e3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
tff(f_430,axiom,
( ( ( op(e0,e0) = e0 )
| ( op(e0,e1) = e0 )
| ( op(e0,e2) = e0 )
| ( op(e0,e3) = e0 ) )
& ( ( op(e0,e0) = e0 )
| ( op(e1,e0) = e0 )
| ( op(e2,e0) = e0 )
| ( op(e3,e0) = e0 ) )
& ( ( op(e0,e0) = e1 )
| ( op(e0,e1) = e1 )
| ( op(e0,e2) = e1 )
| ( op(e0,e3) = e1 ) )
& ( ( op(e0,e0) = e1 )
| ( op(e1,e0) = e1 )
| ( op(e2,e0) = e1 )
| ( op(e3,e0) = e1 ) )
& ( ( op(e0,e0) = e2 )
| ( op(e0,e1) = e2 )
| ( op(e0,e2) = e2 )
| ( op(e0,e3) = e2 ) )
& ( ( op(e0,e0) = e2 )
| ( op(e1,e0) = e2 )
| ( op(e2,e0) = e2 )
| ( op(e3,e0) = e2 ) )
& ( ( op(e0,e0) = e3 )
| ( op(e0,e1) = e3 )
| ( op(e0,e2) = e3 )
| ( op(e0,e3) = e3 ) )
& ( ( op(e0,e0) = e3 )
| ( op(e1,e0) = e3 )
| ( op(e2,e0) = e3 )
| ( op(e3,e0) = e3 ) )
& ( ( op(e1,e0) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e1,e2) = e0 )
| ( op(e1,e3) = e0 ) )
& ( ( op(e0,e1) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e2,e1) = e0 )
| ( op(e3,e1) = e0 ) )
& ( ( op(e1,e0) = e1 )
| ( op(e1,e1) = e1 )
| ( op(e1,e2) = e1 )
| ( op(e1,e3) = e1 ) )
& ( ( op(e0,e1) = e1 )
| ( op(e1,e1) = e1 )
| ( op(e2,e1) = e1 )
| ( op(e3,e1) = e1 ) )
& ( ( op(e1,e0) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e1,e2) = e2 )
| ( op(e1,e3) = e2 ) )
& ( ( op(e0,e1) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e2,e1) = e2 )
| ( op(e3,e1) = e2 ) )
& ( ( op(e1,e0) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e1,e2) = e3 )
| ( op(e1,e3) = e3 ) )
& ( ( op(e0,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e3,e1) = e3 ) )
& ( ( op(e2,e0) = e0 )
| ( op(e2,e1) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e2,e3) = e0 ) )
& ( ( op(e0,e2) = e0 )
| ( op(e1,e2) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e3,e2) = e0 ) )
& ( ( op(e2,e0) = e1 )
| ( op(e2,e1) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e2,e3) = e1 ) )
& ( ( op(e0,e2) = e1 )
| ( op(e1,e2) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e3,e2) = e1 ) )
& ( ( op(e2,e0) = e2 )
| ( op(e2,e1) = e2 )
| ( op(e2,e2) = e2 )
| ( op(e2,e3) = e2 ) )
& ( ( op(e0,e2) = e2 )
| ( op(e1,e2) = e2 )
| ( op(e2,e2) = e2 )
| ( op(e3,e2) = e2 ) )
& ( ( op(e2,e0) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e2,e3) = e3 ) )
& ( ( op(e0,e2) = e3 )
| ( op(e1,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e3,e2) = e3 ) )
& ( ( op(e3,e0) = e0 )
| ( op(e3,e1) = e0 )
| ( op(e3,e2) = e0 )
| ( op(e3,e3) = e0 ) )
& ( ( op(e0,e3) = e0 )
| ( op(e1,e3) = e0 )
| ( op(e2,e3) = e0 )
| ( op(e3,e3) = e0 ) )
& ( ( op(e3,e0) = e1 )
| ( op(e3,e1) = e1 )
| ( op(e3,e2) = e1 )
| ( op(e3,e3) = e1 ) )
& ( ( op(e0,e3) = e1 )
| ( op(e1,e3) = e1 )
| ( op(e2,e3) = e1 )
| ( op(e3,e3) = e1 ) )
& ( ( op(e3,e0) = e2 )
| ( op(e3,e1) = e2 )
| ( op(e3,e2) = e2 )
| ( op(e3,e3) = e2 ) )
& ( ( op(e0,e3) = e2 )
| ( op(e1,e3) = e2 )
| ( op(e2,e3) = e2 )
| ( op(e3,e3) = e2 ) )
& ( ( op(e3,e0) = e3 )
| ( op(e3,e1) = e3 )
| ( op(e3,e2) = e3 )
| ( op(e3,e3) = e3 ) )
& ( ( op(e0,e3) = e3 )
| ( op(e1,e3) = e3 )
| ( op(e2,e3) = e3 )
| ( op(e3,e3) = e3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
tff(f_652,axiom,
~ ( ( e0 = op(e3,op(e3,op(e3,e3))) )
& ( e1 = op(e3,op(e3,e3)) )
& ( e2 = op(e3,e3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
tff(f_640,axiom,
~ ( ( e0 = op(e2,op(e2,op(e2,e2))) )
& ( e1 = op(e2,op(e2,e2)) )
& ( e3 = op(e2,e2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
tff(f_622,axiom,
~ ( ( ( op(e0,e0) = e0 )
& ( op(e1,e1) = e0 )
& ( op(e2,e2) = e0 )
& ( op(e3,e3) = e0 ) )
| ( ( op(e0,e0) = e1 )
& ( op(e1,e1) = e1 )
& ( op(e2,e2) = e1 )
& ( op(e3,e3) = e1 ) )
| ( ( op(e0,e0) = e2 )
& ( op(e1,e1) = e2 )
& ( op(e2,e2) = e2 )
& ( op(e3,e3) = e2 ) )
| ( ( op(e0,e0) = e3 )
& ( op(e1,e1) = e3 )
& ( op(e2,e2) = e3 )
& ( op(e3,e3) = e3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
tff(f_658,axiom,
~ ( ( e0 = op(e3,op(e3,op(e3,e3))) )
& ( e2 = op(e3,op(e3,e3)) )
& ( e1 = op(e3,e3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
tff(f_760,axiom,
~ ( ( e3 = op(e2,op(e2,op(e2,e2))) )
& ( e0 = op(e2,op(e2,e2)) )
& ( e1 = op(e2,e2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
tff(f_754,axiom,
~ ( ( e3 = op(e1,op(e1,op(e1,e1))) )
& ( e2 = op(e1,op(e1,e1)) )
& ( e0 = op(e1,e1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
tff(f_736,axiom,
~ ( ( e3 = op(e0,op(e0,op(e0,e0))) )
& ( e1 = op(e0,op(e0,e0)) )
& ( e2 = op(e0,e0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
tff(f_670,axiom,
~ ( ( e1 = op(e0,op(e0,op(e0,e0))) )
& ( e3 = op(e0,op(e0,e0)) )
& ( e2 = op(e0,e0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
tff(f_676,axiom,
~ ( ( e1 = op(e2,op(e2,op(e2,e2))) )
& ( e0 = op(e2,op(e2,e2)) )
& ( e3 = op(e2,e2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
tff(f_712,axiom,
~ ( ( e2 = op(e1,op(e1,op(e1,e1))) )
& ( e0 = op(e1,op(e1,e1)) )
& ( e3 = op(e1,e1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
tff(f_682,axiom,
~ ( ( e1 = op(e2,op(e2,op(e2,e2))) )
& ( e3 = op(e2,op(e2,e2)) )
& ( e0 = op(e2,e2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
tff(f_706,axiom,
~ ( ( e2 = op(e0,op(e0,op(e0,e0))) )
& ( e3 = op(e0,op(e0,e0)) )
& ( e1 = op(e0,e0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
tff(f_730,axiom,
~ ( ( e2 = op(e3,op(e3,op(e3,e3))) )
& ( e1 = op(e3,op(e3,e3)) )
& ( e0 = op(e3,e3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
tff(c_216,plain,
e2 != e1,
inference(cnfTransformation,[status(thm)],[f_590]) ).
tff(c_34,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_311,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_46,plain,
op(unit,e1) = e1,
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_316,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_311,c_46]) ).
tff(c_194,plain,
op(e3,e1) != op(e0,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1705,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_316,c_194]) ).
tff(c_220,plain,
e2 != e0,
inference(cnfTransformation,[status(thm)],[f_590]) ).
tff(c_218,plain,
e3 != e0,
inference(cnfTransformation,[status(thm)],[f_590]) ).
tff(c_222,plain,
e1 != e0,
inference(cnfTransformation,[status(thm)],[f_590]) ).
tff(c_212,plain,
e3 != e2,
inference(cnfTransformation,[status(thm)],[f_590]) ).
tff(c_214,plain,
e3 != e1,
inference(cnfTransformation,[status(thm)],[f_590]) ).
tff(c_36,plain,
op(e3,unit) = e3,
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_312,plain,
op(e3,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_311,c_36]) ).
tff(c_124,plain,
op(e3,e2) != op(e3,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_326,plain,
op(e3,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_312,c_124]) ).
tff(c_42,plain,
op(unit,e2) = e2,
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_318,plain,
op(e0,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_311,c_42]) ).
tff(c_126,plain,
op(e3,e1) != op(e3,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_328,plain,
op(e3,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_312,c_126]) ).
tff(c_6,plain,
( ( op(e3,e1) = e3 )
| ( op(e3,e1) = e2 )
| ( op(e3,e1) = e1 )
| ( op(e3,e1) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_344,plain,
( ( op(e3,e1) = e2 )
| ( op(e3,e1) = e1 )
| ( op(e3,e1) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_328,c_6]) ).
tff(c_345,plain,
op(e3,e1) = e0,
inference(splitLeft,[status(thm)],[c_344]) ).
tff(c_190,plain,
op(e3,e1) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_351,plain,
op(e1,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_190]) ).
tff(c_50,plain,
op(unit,e0) = e0,
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_315,plain,
op(e0,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_311,c_50]) ).
tff(c_40,plain,
op(e2,unit) = e2,
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_319,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_311,c_40]) ).
tff(c_108,plain,
( ( op(e3,e0) = e1 )
| ( op(e2,e0) = e1 )
| ( op(e1,e0) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_377,plain,
( ( e3 = e1 )
| ( e2 = e1 )
| ( op(e1,e0) = e1 )
| ( e1 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_315,c_319,c_312,c_108]) ).
tff(c_378,plain,
op(e1,e0) = e1,
inference(negUnitSimplification,[status(thm)],[c_222,c_216,c_214,c_377]) ).
tff(c_98,plain,
( ( op(e1,e3) = e0 )
| ( op(e1,e2) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e1,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_846,plain,
( ( op(e1,e3) = e0 )
| ( op(e1,e2) = e0 )
| ( op(e1,e1) = e0 )
| ( e1 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_378,c_98]) ).
tff(c_847,plain,
( ( op(e1,e3) = e0 )
| ( op(e1,e2) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_222,c_351,c_846]) ).
tff(c_848,plain,
op(e1,e2) = e0,
inference(splitLeft,[status(thm)],[c_847]) ).
tff(c_148,plain,
op(e1,e2) != op(e1,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_380,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_378,c_148]) ).
tff(c_76,plain,
( ( op(e3,e2) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e1,e2) = e1 )
| ( op(e0,e2) = e1 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_399,plain,
( ( op(e3,e2) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e0,e2) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_380,c_76]) ).
tff(c_400,plain,
op(e0,e2) = e1,
inference(splitLeft,[status(thm)],[c_399]) ).
tff(c_411,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_400,c_318]) ).
tff(c_413,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216,c_411]) ).
tff(c_414,plain,
( ( op(e2,e2) = e1 )
| ( op(e3,e2) = e1 ) ),
inference(splitRight,[status(thm)],[c_399]) ).
tff(c_428,plain,
op(e3,e2) = e1,
inference(splitLeft,[status(thm)],[c_414]) ).
tff(c_38,plain,
op(unit,e3) = e3,
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_313,plain,
op(e0,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_311,c_38]) ).
tff(c_176,plain,
op(e3,e2) != op(e2,e2),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_505,plain,
op(e2,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_428,c_176]) ).
tff(c_188,plain,
op(e3,e1) != op(e2,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_347,plain,
op(e2,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_188]) ).
tff(c_196,plain,
op(e2,e1) != op(e0,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_392,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_316,c_196]) ).
tff(c_138,plain,
op(e2,e1) != op(e2,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_372,plain,
op(e2,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_319,c_138]) ).
tff(c_84,plain,
( ( op(e3,e1) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_429,plain,
( ( e3 = e0 )
| ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_316,c_345,c_84]) ).
tff(c_430,plain,
( ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_218,c_429]) ).
tff(c_431,plain,
op(e1,e1) = e3,
inference(splitLeft,[status(thm)],[c_430]) ).
tff(c_192,plain,
op(e2,e1) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_444,plain,
op(e2,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_431,c_192]) ).
tff(c_14,plain,
( ( op(e2,e1) = e3 )
| ( op(e2,e1) = e2 )
| ( op(e2,e1) = e1 )
| ( op(e2,e1) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_498,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_347,c_392,c_372,c_444,c_14]) ).
tff(c_499,plain,
op(e2,e1) = e3,
inference(splitRight,[status(thm)],[c_430]) ).
tff(c_523,plain,
( ( op(e1,e3) = e0 )
| ( op(e1,e2) = e0 )
| ( op(e1,e1) = e0 )
| ( e1 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_378,c_98]) ).
tff(c_524,plain,
( ( op(e1,e3) = e0 )
| ( op(e1,e2) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_222,c_351,c_523]) ).
tff(c_525,plain,
op(e1,e2) = e0,
inference(splitLeft,[status(thm)],[c_524]) ).
tff(c_180,plain,
op(e2,e2) != op(e1,e2),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_528,plain,
op(e2,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_525,c_180]) ).
tff(c_82,plain,
( ( op(e2,e3) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e2,e1) = e0 )
| ( op(e2,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_551,plain,
( ( op(e2,e3) = e0 )
| ( op(e2,e2) = e0 )
| ( e3 = e0 )
| ( e2 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_499,c_82]) ).
tff(c_552,plain,
op(e2,e3) = e0,
inference(negUnitSimplification,[status(thm)],[c_220,c_218,c_528,c_551]) ).
tff(c_78,plain,
( ( op(e2,e3) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e2,e1) = e1 )
| ( op(e2,e0) = e1 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_581,plain,
( ( e1 = e0 )
| ( op(e2,e2) = e1 )
| ( e3 = e1 )
| ( e2 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_499,c_552,c_78]) ).
tff(c_582,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216,c_214,c_505,c_222,c_581]) ).
tff(c_583,plain,
op(e1,e3) = e0,
inference(splitRight,[status(thm)],[c_524]) ).
tff(c_116,plain,
op(e3,e3) != op(e3,e2),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_504,plain,
op(e3,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_428,c_116]) ).
tff(c_60,plain,
( ( op(e3,e3) = e1 )
| ( op(e2,e3) = e1 )
| ( op(e1,e3) = e1 )
| ( op(e0,e3) = e1 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_622,plain,
( ( op(e3,e3) = e1 )
| ( op(e2,e3) = e1 )
| ( e1 = e0 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_313,c_583,c_60]) ).
tff(c_623,plain,
op(e2,e3) = e1,
inference(negUnitSimplification,[status(thm)],[c_214,c_222,c_504,c_622]) ).
tff(c_56,plain,
( ( op(e3,e3) = e2 )
| ( op(e2,e3) = e2 )
| ( op(e1,e3) = e2 )
| ( op(e0,e3) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_634,plain,
( ( op(e3,e3) = e2 )
| ( e2 = e1 )
| ( e2 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_313,c_583,c_623,c_56]) ).
tff(c_635,plain,
op(e3,e3) = e2,
inference(negUnitSimplification,[status(thm)],[c_212,c_220,c_216,c_634]) ).
tff(c_240,plain,
( ( op(e3,e3) != e2 )
| ( op(e3,op(e3,e3)) != e1 )
| ( op(e3,op(e3,op(e3,e3))) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_652]) ).
tff(c_746,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_428,c_635,c_428,c_635,c_635,c_240]) ).
tff(c_747,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_414]) ).
tff(c_68,plain,
( ( op(e3,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e1,e2) = e3 )
| ( op(e0,e2) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_858,plain,
( ( op(e3,e2) = e3 )
| ( e3 = e1 )
| ( e3 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_318,c_848,c_747,c_68]) ).
tff(c_859,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_214,c_326,c_858]) ).
tff(c_860,plain,
op(e1,e3) = e0,
inference(splitRight,[status(thm)],[c_847]) ).
tff(c_168,plain,
op(e2,e3) != op(e1,e3),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_864,plain,
op(e2,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_860,c_168]) ).
tff(c_760,plain,
( ( e3 = e0 )
| ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_316,c_345,c_84]) ).
tff(c_761,plain,
( ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_218,c_760]) ).
tff(c_762,plain,
op(e1,e1) = e3,
inference(splitLeft,[status(thm)],[c_761]) ).
tff(c_765,plain,
op(e2,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_762,c_192]) ).
tff(c_832,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_347,c_392,c_372,c_765,c_14]) ).
tff(c_833,plain,
op(e2,e1) = e3,
inference(splitRight,[status(thm)],[c_761]) ).
tff(c_905,plain,
( ( op(e2,e3) = e0 )
| ( e1 = e0 )
| ( e3 = e0 )
| ( e2 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_833,c_747,c_82]) ).
tff(c_906,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_220,c_218,c_222,c_864,c_905]) ).
tff(c_907,plain,
( ( op(e3,e1) = e1 )
| ( op(e3,e1) = e2 ) ),
inference(splitRight,[status(thm)],[c_344]) ).
tff(c_1877,plain,
op(e3,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_1705,c_907]) ).
tff(c_1884,plain,
op(e1,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_190]) ).
tff(c_970,plain,
op(e2,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_319,c_138]) ).
tff(c_1691,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_316,c_196]) ).
tff(c_1683,plain,
( ( op(e2,e3) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e2,e1) = e1 )
| ( e2 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_78]) ).
tff(c_1684,plain,
( ( op(e2,e3) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e2,e1) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_216,c_1683]) ).
tff(c_1685,plain,
op(e2,e1) = e1,
inference(splitLeft,[status(thm)],[c_1684]) ).
tff(c_1696,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1691,c_1685]) ).
tff(c_1698,plain,
op(e2,e1) != e1,
inference(splitRight,[status(thm)],[c_1684]) ).
tff(c_1541,plain,
op(e2,e1) = e0,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_1573,plain,
op(e1,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_1541,c_192]) ).
tff(c_44,plain,
op(e1,unit) = e1,
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_317,plain,
op(e1,e0) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_311,c_44]) ).
tff(c_150,plain,
op(e1,e1) != op(e1,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1546,plain,
op(e1,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_317,c_150]) ).
tff(c_1589,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_316,c_194]) ).
tff(c_1604,plain,
op(e3,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_1589,c_907]) ).
tff(c_1609,plain,
op(e1,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_1604,c_190]) ).
tff(c_186,plain,
op(e1,e2) != op(e0,e2),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1554,plain,
op(e1,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_318,c_186]) ).
tff(c_1544,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_317,c_148]) ).
tff(c_1024,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_316,c_196]) ).
tff(c_1023,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_316,c_194]) ).
tff(c_1032,plain,
op(e3,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_1023,c_907]) ).
tff(c_1046,plain,
( ( e3 = e2 )
| ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_316,c_1032,c_84]) ).
tff(c_1047,plain,
( ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_212,c_1046]) ).
tff(c_1048,plain,
op(e1,e1) = e3,
inference(splitLeft,[status(thm)],[c_1047]) ).
tff(c_1052,plain,
op(e2,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_1048,c_192]) ).
tff(c_1138,plain,
op(e2,e1) = e0,
inference(negUnitSimplification,[status(thm)],[c_1024,c_970,c_1052,c_14]) ).
tff(c_134,plain,
op(e2,e3) != op(e2,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_967,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_319,c_134]) ).
tff(c_172,plain,
op(e2,e3) != op(e0,e3),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_334,plain,
op(e2,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_313,c_172]) ).
tff(c_10,plain,
( ( op(e2,e3) = e3 )
| ( op(e2,e3) = e2 )
| ( op(e2,e3) = e1 )
| ( op(e2,e3) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_1060,plain,
( ( op(e2,e3) = e1 )
| ( op(e2,e3) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_967,c_334,c_10]) ).
tff(c_1061,plain,
op(e2,e3) = e0,
inference(splitLeft,[status(thm)],[c_1060]) ).
tff(c_130,plain,
op(e2,e3) != op(e2,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1075,plain,
op(e2,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_1061,c_130]) ).
tff(c_1099,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1075,c_1024,c_970,c_1052,c_14]) ).
tff(c_1100,plain,
op(e2,e3) = e1,
inference(splitRight,[status(thm)],[c_1060]) ).
tff(c_70,plain,
( ( op(e2,e3) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e2,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_1113,plain,
( ( e3 = e1 )
| ( op(e2,e2) = e3 )
| ( op(e2,e1) = e3 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_319,c_1100,c_70]) ).
tff(c_1114,plain,
op(e2,e2) = e3,
inference(negUnitSimplification,[status(thm)],[c_212,c_1052,c_214,c_1113]) ).
tff(c_236,plain,
( ( op(e2,e2) != e3 )
| ( op(e2,op(e2,e2)) != e1 )
| ( op(e2,op(e2,op(e2,e2))) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_640]) ).
tff(c_1237,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1138,c_1100,c_1114,c_1100,c_1114,c_1114,c_236]) ).
tff(c_1238,plain,
op(e2,e1) = e3,
inference(splitRight,[status(thm)],[c_1047]) ).
tff(c_132,plain,
op(e2,e2) != op(e2,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1244,plain,
op(e2,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_1238,c_132]) ).
tff(c_20,plain,
( ( op(e1,e2) = e3 )
| ( op(e1,e2) = e2 )
| ( op(e1,e2) = e1 )
| ( op(e1,e2) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_975,plain,
op(e1,e2) = e0,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_1262,plain,
( ( op(e3,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( e3 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_318,c_975,c_68]) ).
tff(c_1263,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_1244,c_326,c_1262]) ).
tff(c_1264,plain,
( ( op(e1,e2) = e1 )
| ( op(e1,e2) = e2 )
| ( op(e1,e2) = e3 ) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_1628,plain,
op(e1,e2) = e3,
inference(negUnitSimplification,[status(thm)],[c_1554,c_1544,c_1264]) ).
tff(c_144,plain,
op(e1,e2) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1634,plain,
op(e1,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_1628,c_144]) ).
tff(c_22,plain,
( ( op(e1,e1) = e3 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e1 )
| ( op(e1,e1) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_1649,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1573,c_1546,c_1609,c_1634,c_22]) ).
tff(c_1650,plain,
( ( op(e2,e1) = e1 )
| ( op(e2,e1) = e2 )
| ( op(e2,e1) = e3 ) ),
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_1757,plain,
op(e2,e1) = e3,
inference(negUnitSimplification,[status(thm)],[c_970,c_1698,c_1650]) ).
tff(c_1761,plain,
op(e2,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_1757,c_132]) ).
tff(c_48,plain,
op(e0,unit) = e0,
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_314,plain,
op(e0,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_311,c_48]) ).
tff(c_1656,plain,
op(e1,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_317,c_150]) ).
tff(c_1722,plain,
( ( op(e1,e1) = e3 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_1656,c_22]) ).
tff(c_1723,plain,
op(e1,e1) = e0,
inference(splitLeft,[status(thm)],[c_1722]) ).
tff(c_146,plain,
op(e1,e3) != op(e1,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1655,plain,
op(e1,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_317,c_146]) ).
tff(c_1699,plain,
( ( op(e3,e3) = e1 )
| ( op(e2,e3) = e1 )
| ( op(e1,e3) = e1 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_313,c_60]) ).
tff(c_1700,plain,
( ( op(e3,e3) = e1 )
| ( op(e2,e3) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_1655,c_1699]) ).
tff(c_1701,plain,
op(e2,e3) = e1,
inference(splitLeft,[status(thm)],[c_1700]) ).
tff(c_128,plain,
op(e2,e3) != op(e2,e2),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1714,plain,
op(e2,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_1701,c_128]) ).
tff(c_136,plain,
op(e2,e2) != op(e2,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_969,plain,
op(e2,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_319,c_136]) ).
tff(c_12,plain,
( ( op(e2,e2) = e3 )
| ( op(e2,e2) = e2 )
| ( op(e2,e2) = e1 )
| ( op(e2,e2) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_1766,plain,
( ( op(e2,e2) = e3 )
| ( op(e2,e2) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_1714,c_969,c_12]) ).
tff(c_1767,plain,
op(e2,e2) = e0,
inference(splitLeft,[status(thm)],[c_1766]) ).
tff(c_154,plain,
op(e0,e3) != op(e0,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_338,plain,
op(e0,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_313,c_154]) ).
tff(c_1287,plain,
( ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_338,c_328,c_84]) ).
tff(c_1288,plain,
op(e1,e1) = e3,
inference(splitLeft,[status(thm)],[c_1287]) ).
tff(c_1304,plain,
op(e1,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_1288,c_144]) ).
tff(c_1292,plain,
op(e1,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_318,c_186]) ).
tff(c_1271,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_317,c_148]) ).
tff(c_1357,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1304,c_1292,c_1271,c_1264]) ).
tff(c_1358,plain,
op(e2,e1) = e3,
inference(splitRight,[status(thm)],[c_1287]) ).
tff(c_1507,plain,
op(e2,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_1358,c_130]) ).
tff(c_1409,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_316,c_194]) ).
tff(c_1414,plain,
op(e3,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_1409,c_907]) ).
tff(c_118,plain,
op(e3,e3) != op(e3,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_1418,plain,
op(e3,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_1414,c_118]) ).
tff(c_64,plain,
( ( op(e3,e3) = e0 )
| ( op(e2,e3) = e0 )
| ( op(e1,e3) = e0 )
| ( op(e0,e3) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_1266,plain,
( ( op(e3,e3) = e0 )
| ( op(e2,e3) = e0 )
| ( op(e1,e3) = e0 )
| ( e3 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_313,c_64]) ).
tff(c_1267,plain,
( ( op(e3,e3) = e0 )
| ( op(e2,e3) = e0 )
| ( op(e1,e3) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_218,c_1266]) ).
tff(c_1268,plain,
op(e1,e3) = e0,
inference(splitLeft,[status(thm)],[c_1267]) ).
tff(c_1279,plain,
op(e2,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_1268,c_168]) ).
tff(c_1371,plain,
( ( op(e2,e3) = e3 )
| ( op(e2,e3) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_1279,c_967,c_10]) ).
tff(c_1372,plain,
op(e2,e3) = e1,
inference(splitLeft,[status(thm)],[c_1371]) ).
tff(c_1451,plain,
( ( op(e3,e3) = e2 )
| ( e2 = e1 )
| ( e2 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_313,c_1268,c_1372,c_56]) ).
tff(c_1452,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_212,c_220,c_216,c_1418,c_1451]) ).
tff(c_1453,plain,
op(e2,e3) = e3,
inference(splitRight,[status(thm)],[c_1371]) ).
tff(c_1538,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1507,c_1453]) ).
tff(c_1539,plain,
( ( op(e2,e3) = e0 )
| ( op(e3,e3) = e0 ) ),
inference(splitRight,[status(thm)],[c_1267]) ).
tff(c_1746,plain,
( ( e1 = e0 )
| ( op(e3,e3) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1701,c_1539]) ).
tff(c_1747,plain,
op(e3,e3) = e0,
inference(negUnitSimplification,[status(thm)],[c_222,c_1746]) ).
tff(c_230,plain,
( ( op(e3,e3) != e0 )
| ( op(e2,e2) != e0 )
| ( op(e1,e1) != e0 )
| ( op(e0,e0) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_622]) ).
tff(c_1871,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_314,c_1723,c_1767,c_1747,c_230]) ).
tff(c_1872,plain,
op(e2,e2) = e3,
inference(splitRight,[status(thm)],[c_1766]) ).
tff(c_1874,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1761,c_1872]) ).
tff(c_1875,plain,
( ( op(e1,e1) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(splitRight,[status(thm)],[c_1722]) ).
tff(c_1903,plain,
op(e1,e1) = e3,
inference(negUnitSimplification,[status(thm)],[c_1884,c_1875]) ).
tff(c_1909,plain,
op(e1,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_1903,c_144]) ).
tff(c_1666,plain,
op(e1,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_318,c_186]) ).
tff(c_1654,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_317,c_148]) ).
tff(c_1916,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1909,c_1666,c_1654,c_1264]) ).
tff(c_1918,plain,
op(e2,e3) != e1,
inference(splitRight,[status(thm)],[c_1700]) ).
tff(c_1919,plain,
( ( op(e3,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e1,e2) = e3 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_318,c_68]) ).
tff(c_1920,plain,
( ( op(e2,e2) = e3 )
| ( op(e1,e2) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_212,c_326,c_1919]) ).
tff(c_1921,plain,
op(e1,e2) = e3,
inference(splitLeft,[status(thm)],[c_1920]) ).
tff(c_1697,plain,
( ( op(e2,e2) = e1 )
| ( op(e2,e3) = e1 ) ),
inference(splitRight,[status(thm)],[c_1684]) ).
tff(c_1965,plain,
op(e2,e2) = e1,
inference(negUnitSimplification,[status(thm)],[c_1918,c_1697]) ).
tff(c_80,plain,
( ( op(e3,e2) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e1,e2) = e0 )
| ( op(e0,e2) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_2003,plain,
( ( op(e3,e2) = e0 )
| ( e1 = e0 )
| ( e3 = e0 )
| ( e2 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_318,c_1921,c_1965,c_80]) ).
tff(c_2004,plain,
op(e3,e2) = e0,
inference(negUnitSimplification,[status(thm)],[c_220,c_218,c_222,c_2003]) ).
tff(c_1917,plain,
op(e3,e3) = e1,
inference(splitRight,[status(thm)],[c_1700]) ).
tff(c_1923,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_1917,c_118]) ).
tff(c_1954,plain,
op(e3,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_1923,c_907]) ).
tff(c_242,plain,
( ( op(e3,e3) != e1 )
| ( op(e3,op(e3,e3)) != e2 )
| ( op(e3,op(e3,op(e3,e3))) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_658]) ).
tff(c_2108,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2004,c_1954,c_1917,c_1954,c_1917,c_1917,c_242]) ).
tff(c_2109,plain,
op(e2,e2) = e3,
inference(splitRight,[status(thm)],[c_1920]) ).
tff(c_2152,plain,
( ( e3 = e1 )
| ( op(e2,e3) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2109,c_1697]) ).
tff(c_2153,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1918,c_214,c_2152]) ).
tff(c_2154,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_2156,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_2154]) ).
tff(c_2162,plain,
op(e3,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_2156,c_46]) ).
tff(c_3287,plain,
op(e3,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2162,c_126]) ).
tff(c_8,plain,
( ( op(e3,e0) = e3 )
| ( op(e3,e0) = e2 )
| ( op(e3,e0) = e1 )
| ( op(e3,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_3292,plain,
( ( op(e3,e0) = e3 )
| ( op(e3,e0) = e2 )
| ( op(e3,e0) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_3287,c_8]) ).
tff(c_3293,plain,
op(e3,e0) = e0,
inference(splitLeft,[status(thm)],[c_3292]) ).
tff(c_202,plain,
op(e3,e0) != op(e1,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_3295,plain,
op(e1,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_3293,c_202]) ).
tff(c_2163,plain,
op(e1,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_2156,c_44]) ).
tff(c_4644,plain,
op(e1,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_146]) ).
tff(c_2180,plain,
op(e0,e2) = e3,
inference(splitLeft,[status(thm)],[c_68]) ).
tff(c_2772,plain,
op(e1,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_186]) ).
tff(c_86,plain,
( ( op(e1,e3) = e3 )
| ( op(e1,e2) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e1,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_2913,plain,
( ( e3 = e1 )
| ( op(e1,e2) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e1,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_86]) ).
tff(c_2914,plain,
( ( op(e1,e1) = e3 )
| ( op(e1,e0) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_2772,c_214,c_2913]) ).
tff(c_2915,plain,
op(e1,e0) = e3,
inference(splitLeft,[status(thm)],[c_2914]) ).
tff(c_204,plain,
op(e2,e0) != op(e1,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_2917,plain,
op(e2,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_2915,c_204]) ).
tff(c_2165,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2156,c_40]) ).
tff(c_2788,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_2165,c_134]) ).
tff(c_2161,plain,
op(e3,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_2156,c_50]) ).
tff(c_200,plain,
op(e3,e0) != op(e2,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_2183,plain,
op(e2,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2161,c_200]) ).
tff(c_16,plain,
( ( op(e2,e0) = e3 )
| ( op(e2,e0) = e2 )
| ( op(e2,e0) = e1 )
| ( op(e2,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_2192,plain,
op(e2,e0) = e0,
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_2203,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2183,c_2192]) ).
tff(c_2204,plain,
( ( op(e2,e0) = e1 )
| ( op(e2,e0) = e2 )
| ( op(e2,e0) = e3 ) ),
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_2963,plain,
op(e2,e0) = e1,
inference(negUnitSimplification,[status(thm)],[c_2917,c_2788,c_2204]) ).
tff(c_2968,plain,
op(e2,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2963,c_136]) ).
tff(c_2184,plain,
op(e3,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2161,c_124]) ).
tff(c_2780,plain,
( ( op(e3,e2) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e1,e2) = e0 )
| ( e3 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_80]) ).
tff(c_2781,plain,
( ( op(e2,e2) = e0 )
| ( op(e1,e2) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_218,c_2184,c_2780]) ).
tff(c_2782,plain,
op(e1,e2) = e0,
inference(splitLeft,[status(thm)],[c_2781]) ).
tff(c_2164,plain,
op(e3,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2156,c_42]) ).
tff(c_3007,plain,
( ( e2 = e1 )
| ( op(e2,e2) = e1 )
| ( e1 = e0 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_2782,c_2164,c_76]) ).
tff(c_3008,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_214,c_222,c_2968,c_216,c_3007]) ).
tff(c_3009,plain,
op(e1,e1) = e3,
inference(splitRight,[status(thm)],[c_2914]) ).
tff(c_3149,plain,
op(e2,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3009,c_192]) ).
tff(c_184,plain,
op(e2,e2) != op(e0,e2),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_2771,plain,
op(e2,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_184]) ).
tff(c_2811,plain,
( ( e3 = e2 )
| ( op(e2,e2) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e2,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2165,c_70]) ).
tff(c_2812,plain,
( ( op(e2,e1) = e3 )
| ( op(e2,e0) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_2771,c_212,c_2811]) ).
tff(c_2813,plain,
op(e2,e0) = e3,
inference(splitLeft,[status(thm)],[c_2812]) ).
tff(c_2833,plain,
( ( e3 = e1 )
| ( e3 = e0 )
| ( op(e1,e1) = e3 )
| ( op(e1,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2782,c_2163,c_86]) ).
tff(c_2834,plain,
( ( op(e1,e1) = e3 )
| ( op(e1,e0) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_218,c_214,c_2833]) ).
tff(c_2835,plain,
op(e1,e0) = e3,
inference(splitLeft,[status(thm)],[c_2834]) ).
tff(c_2840,plain,
op(e2,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_2835,c_204]) ).
tff(c_2860,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2813,c_2840]) ).
tff(c_2861,plain,
op(e1,e1) = e3,
inference(splitRight,[status(thm)],[c_2834]) ).
tff(c_160,plain,
op(e0,e2) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_2287,plain,
op(e0,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_160]) ).
tff(c_90,plain,
( ( op(e1,e3) = e2 )
| ( op(e1,e2) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e1,e0) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_2283,plain,
op(e1,e0) = e2,
inference(splitLeft,[status(thm)],[c_90]) ).
tff(c_100,plain,
( ( op(e3,e0) = e3 )
| ( op(e2,e0) = e3 )
| ( op(e1,e0) = e3 )
| ( op(e0,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_2559,plain,
( ( e3 = e0 )
| ( op(e2,e0) = e3 )
| ( e3 = e2 )
| ( op(e0,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2283,c_2161,c_100]) ).
tff(c_2560,plain,
op(e2,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_2287,c_212,c_218,c_2559]) ).
tff(c_2158,plain,
op(e3,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_2156,c_36]) ).
tff(c_164,plain,
op(e3,e3) != op(e2,e3),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_2175,plain,
op(e2,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_2158,c_164]) ).
tff(c_2324,plain,
( ( op(e2,e2) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e2,e0) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_2175,c_70]) ).
tff(c_2325,plain,
op(e2,e0) = e3,
inference(splitLeft,[status(thm)],[c_2324]) ).
tff(c_2160,plain,
op(e0,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_2156,c_48]) ).
tff(c_2371,plain,
op(e0,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2160,c_154]) ).
tff(c_2304,plain,
( ( op(e3,e2) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e1,e2) = e0 )
| ( e3 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_80]) ).
tff(c_2305,plain,
( ( op(e2,e2) = e0 )
| ( op(e1,e2) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_218,c_2184,c_2304]) ).
tff(c_2306,plain,
op(e1,e2) = e0,
inference(splitLeft,[status(thm)],[c_2305]) ).
tff(c_2311,plain,
op(e1,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2306,c_144]) ).
tff(c_142,plain,
op(e1,e3) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_2340,plain,
op(e1,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_142]) ).
tff(c_2298,plain,
op(e1,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_2283,c_150]) ).
tff(c_2390,plain,
op(e1,e1) = e3,
inference(negUnitSimplification,[status(thm)],[c_2311,c_2340,c_2298,c_22]) ).
tff(c_96,plain,
( ( op(e3,e1) = e0 )
| ( op(e2,e1) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e0,e1) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_2400,plain,
( ( e1 = e0 )
| ( op(e2,e1) = e0 )
| ( e3 = e0 )
| ( op(e0,e1) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2390,c_2162,c_96]) ).
tff(c_2401,plain,
op(e2,e1) = e0,
inference(negUnitSimplification,[status(thm)],[c_2371,c_218,c_222,c_2400]) ).
tff(c_2359,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2162,c_188]) ).
tff(c_2376,plain,
( ( e2 = e1 )
| ( op(e2,e2) = e1 )
| ( op(e2,e1) = e1 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2325,c_2165,c_78]) ).
tff(c_2377,plain,
op(e2,e2) = e1,
inference(negUnitSimplification,[status(thm)],[c_214,c_2359,c_216,c_2376]) ).
tff(c_276,plain,
( ( op(e2,e2) != e1 )
| ( op(e2,op(e2,e2)) != e0 )
| ( op(e2,op(e2,op(e2,e2))) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_760]) ).
tff(c_2508,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2325,c_2401,c_2377,c_2401,c_2377,c_2377,c_276]) ).
tff(c_2510,plain,
op(e2,e0) != e3,
inference(splitRight,[status(thm)],[c_2324]) ).
tff(c_2591,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2560,c_2510]) ).
tff(c_2592,plain,
op(e2,e2) = e0,
inference(splitRight,[status(thm)],[c_2305]) ).
tff(c_140,plain,
op(e1,e3) != op(e1,e2),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_2714,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_140]) ).
tff(c_2697,plain,
( ( e2 = e1 )
| ( op(e2,e2) = e1 )
| ( op(e1,e2) = e1 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_2164,c_76]) ).
tff(c_2698,plain,
( ( op(e2,e2) = e1 )
| ( op(e1,e2) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_216,c_2697]) ).
tff(c_2699,plain,
op(e1,e2) = e1,
inference(splitLeft,[status(thm)],[c_2698]) ).
tff(c_2721,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2714,c_2699]) ).
tff(c_2722,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_2698]) ).
tff(c_2765,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_2592,c_2722]) ).
tff(c_2767,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_222,c_2765]) ).
tff(c_2768,plain,
( ( op(e1,e1) = e2 )
| ( op(e1,e2) = e2 )
| ( op(e1,e3) = e2 ) ),
inference(splitRight,[status(thm)],[c_90]) ).
tff(c_2901,plain,
( ( e3 = e2 )
| ( e2 = e0 )
| ( e2 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_2782,c_2861,c_2768]) ).
tff(c_2902,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216,c_220,c_212,c_2901]) ).
tff(c_2903,plain,
op(e2,e1) = e3,
inference(splitRight,[status(thm)],[c_2812]) ).
tff(c_3157,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3149,c_2903]) ).
tff(c_3158,plain,
op(e2,e2) = e0,
inference(splitRight,[status(thm)],[c_2781]) ).
tff(c_3191,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_140]) ).
tff(c_3213,plain,
( ( e2 = e1 )
| ( op(e2,e2) = e1 )
| ( op(e1,e2) = e1 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_2164,c_76]) ).
tff(c_3214,plain,
( ( op(e2,e2) = e1 )
| ( op(e1,e2) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_216,c_3213]) ).
tff(c_3215,plain,
op(e1,e2) = e1,
inference(splitLeft,[status(thm)],[c_3214]) ).
tff(c_3217,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3191,c_3215]) ).
tff(c_3218,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_3214]) ).
tff(c_3244,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_3158,c_3218]) ).
tff(c_3246,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_222,c_3244]) ).
tff(c_3248,plain,
op(e0,e2) != e3,
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_102,plain,
( ( op(e0,e3) = e3 )
| ( op(e0,e2) = e3 )
| ( op(e0,e1) = e3 )
| ( op(e0,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_4416,plain,
( ( e3 = e0 )
| ( op(e0,e2) = e3 )
| ( op(e0,e1) = e3 )
| ( op(e0,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2160,c_102]) ).
tff(c_4417,plain,
( ( op(e0,e1) = e3 )
| ( op(e0,e0) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_3248,c_218,c_4416]) ).
tff(c_4418,plain,
op(e0,e0) = e3,
inference(splitLeft,[status(thm)],[c_4417]) ).
tff(c_162,plain,
op(e0,e1) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_4431,plain,
op(e0,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4418,c_162]) ).
tff(c_3859,plain,
op(e1,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_146]) ).
tff(c_3286,plain,
op(e1,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2162,c_190]) ).
tff(c_3832,plain,
( ( op(e1,e1) = e3 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_3286,c_22]) ).
tff(c_3833,plain,
op(e1,e1) = e0,
inference(splitLeft,[status(thm)],[c_3832]) ).
tff(c_3864,plain,
( ( e3 = e1 )
| ( op(e2,e1) = e3 )
| ( e3 = e0 )
| ( op(e0,e1) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3833,c_2162,c_84]) ).
tff(c_3865,plain,
( ( op(e2,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_218,c_214,c_3864]) ).
tff(c_3866,plain,
op(e0,e1) = e3,
inference(splitLeft,[status(thm)],[c_3865]) ).
tff(c_3872,plain,
op(e0,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3866,c_162]) ).
tff(c_158,plain,
op(e0,e3) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_3276,plain,
op(e0,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2160,c_158]) ).
tff(c_32,plain,
( ( op(e0,e0) = e3 )
| ( op(e0,e0) = e2 )
| ( op(e0,e0) = e1 )
| ( op(e0,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_3304,plain,
( ( op(e0,e0) = e3 )
| ( op(e0,e0) = e2 )
| ( op(e0,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_3276,c_32]) ).
tff(c_3305,plain,
op(e0,e0) = e1,
inference(splitLeft,[status(thm)],[c_3304]) ).
tff(c_3817,plain,
( ( e3 = e0 )
| ( op(e0,e2) = e3 )
| ( op(e0,e1) = e3 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3305,c_2160,c_102]) ).
tff(c_3818,plain,
op(e0,e1) = e3,
inference(negUnitSimplification,[status(thm)],[c_214,c_3248,c_218,c_3817]) ).
tff(c_3311,plain,
op(e1,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_146]) ).
tff(c_3519,plain,
( ( e3 = e1 )
| ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2162,c_84]) ).
tff(c_3520,plain,
( ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_3519]) ).
tff(c_3521,plain,
op(e0,e1) = e3,
inference(splitLeft,[status(thm)],[c_3520]) ).
tff(c_198,plain,
op(e1,e1) != op(e0,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_3545,plain,
op(e1,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3521,c_198]) ).
tff(c_3552,plain,
( ( op(e1,e1) = e3 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_3286,c_22]) ).
tff(c_3553,plain,
op(e1,e1) = e0,
inference(splitLeft,[status(thm)],[c_3552]) ).
tff(c_3556,plain,
op(e2,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_3553,c_192]) ).
tff(c_3296,plain,
op(e2,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_3293,c_200]) ).
tff(c_208,plain,
op(e2,e0) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_3318,plain,
op(e2,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_3305,c_208]) ).
tff(c_3528,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_2165,c_134]) ).
tff(c_3612,plain,
op(e2,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_3296,c_3318,c_3528,c_16]) ).
tff(c_3247,plain,
( ( op(e1,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e3,e2) = e3 ) ),
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_3567,plain,
( ( op(e1,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_3247]) ).
tff(c_3568,plain,
( ( op(e1,e2) = e3 )
| ( op(e2,e2) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_212,c_3567]) ).
tff(c_3569,plain,
op(e2,e2) = e3,
inference(splitLeft,[status(thm)],[c_3568]) ).
tff(c_3575,plain,
op(e2,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3569,c_136]) ).
tff(c_3584,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3296,c_3318,c_3528,c_3575,c_16]) ).
tff(c_3586,plain,
op(e2,e2) != e3,
inference(splitRight,[status(thm)],[c_3568]) ).
tff(c_3527,plain,
op(e2,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_2165,c_128]) ).
tff(c_3355,plain,
( ( e3 = e1 )
| ( op(e1,e2) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e1,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_86]) ).
tff(c_3356,plain,
( ( op(e1,e2) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e1,e0) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_3355]) ).
tff(c_3357,plain,
op(e1,e0) = e3,
inference(splitLeft,[status(thm)],[c_3356]) ).
tff(c_3363,plain,
op(e1,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3357,c_148]) ).
tff(c_3327,plain,
op(e2,e2) = e0,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_3383,plain,
( ( op(e1,e2) = e3 )
| ( e3 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_3327,c_3247]) ).
tff(c_3384,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_3363,c_3383]) ).
tff(c_3385,plain,
( ( op(e1,e1) = e3 )
| ( op(e1,e2) = e3 ) ),
inference(splitRight,[status(thm)],[c_3356]) ).
tff(c_3467,plain,
op(e1,e2) = e3,
inference(splitLeft,[status(thm)],[c_3385]) ).
tff(c_3472,plain,
op(e1,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3467,c_144]) ).
tff(c_3321,plain,
op(e0,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_3305,c_160]) ).
tff(c_3388,plain,
( ( op(e1,e1) = e3 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_3286,c_22]) ).
tff(c_3389,plain,
op(e1,e1) = e0,
inference(splitLeft,[status(thm)],[c_3388]) ).
tff(c_3401,plain,
( ( e3 = e0 )
| ( op(e1,e2) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3389,c_3385]) ).
tff(c_3402,plain,
op(e1,e2) = e3,
inference(negUnitSimplification,[status(thm)],[c_218,c_3401]) ).
tff(c_3459,plain,
( ( e2 = e1 )
| ( e1 = e0 )
| ( e3 = e1 )
| ( op(e0,e2) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3402,c_3327,c_2164,c_76]) ).
tff(c_3460,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3321,c_214,c_222,c_216,c_3459]) ).
tff(c_3461,plain,
( ( op(e1,e1) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(splitRight,[status(thm)],[c_3388]) ).
tff(c_3478,plain,
op(e1,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_3472,c_3461]) ).
tff(c_3489,plain,
( ( e1 = e0 )
| ( e3 = e0 )
| ( e2 = e0 )
| ( op(e1,e0) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3478,c_3467,c_2163,c_98]) ).
tff(c_3490,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3295,c_220,c_218,c_222,c_3489]) ).
tff(c_3492,plain,
op(e1,e2) != e3,
inference(splitRight,[status(thm)],[c_3385]) ).
tff(c_3515,plain,
( ( op(e1,e2) = e3 )
| ( e3 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_3327,c_3247]) ).
tff(c_3516,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_3492,c_3515]) ).
tff(c_3517,plain,
( ( op(e2,e2) = e1 )
| ( op(e2,e2) = e2 )
| ( op(e2,e2) = e3 ) ),
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_3597,plain,
op(e2,e2) = e1,
inference(negUnitSimplification,[status(thm)],[c_3586,c_3527,c_3517]) ).
tff(c_3665,plain,
( ( e2 = e0 )
| ( e1 = e0 )
| ( op(e2,e1) = e0 )
| ( e3 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3612,c_3597,c_2165,c_82]) ).
tff(c_3666,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_218,c_3556,c_222,c_220,c_3665]) ).
tff(c_3667,plain,
( ( op(e1,e1) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(splitRight,[status(thm)],[c_3552]) ).
tff(c_3671,plain,
op(e1,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_3545,c_3667]) ).
tff(c_3677,plain,
op(e1,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_3671,c_150]) ).
tff(c_3310,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_140]) ).
tff(c_3682,plain,
( ( e2 = e1 )
| ( op(e2,e2) = e1 )
| ( op(e1,e2) = e1 )
| ( op(e0,e2) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_76]) ).
tff(c_3683,plain,
op(e2,e2) = e1,
inference(negUnitSimplification,[status(thm)],[c_3321,c_3310,c_216,c_3682]) ).
tff(c_3696,plain,
( ( op(e1,e2) = e3 )
| ( e3 = e1 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_3683,c_3247]) ).
tff(c_3697,plain,
op(e1,e2) = e3,
inference(negUnitSimplification,[status(thm)],[c_212,c_214,c_3696]) ).
tff(c_3701,plain,
op(e1,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3697,c_148]) ).
tff(c_24,plain,
( ( op(e1,e0) = e3 )
| ( op(e1,e0) = e2 )
| ( op(e1,e0) = e1 )
| ( op(e1,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_3732,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3295,c_3311,c_3677,c_3701,c_24]) ).
tff(c_3734,plain,
op(e0,e1) != e3,
inference(splitRight,[status(thm)],[c_3520]) ).
tff(c_3829,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3818,c_3734]) ).
tff(c_3830,plain,
( ( op(e0,e0) = e2 )
| ( op(e0,e0) = e3 ) ),
inference(splitRight,[status(thm)],[c_3304]) ).
tff(c_3899,plain,
op(e0,e0) = e2,
inference(negUnitSimplification,[status(thm)],[c_3872,c_3830]) ).
tff(c_210,plain,
op(e1,e0) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_3904,plain,
op(e1,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_3899,c_210]) ).
tff(c_152,plain,
op(e0,e3) != op(e0,e2),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_3278,plain,
op(e0,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2160,c_152]) ).
tff(c_3850,plain,
op(e1,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_3833,c_144]) ).
tff(c_3297,plain,
op(e3,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_3293,c_124]) ).
tff(c_3878,plain,
op(e2,e2) = e0,
inference(negUnitSimplification,[status(thm)],[c_3278,c_3850,c_3297,c_80]) ).
tff(c_3914,plain,
( ( op(e1,e2) = e3 )
| ( e3 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_3878,c_3247]) ).
tff(c_3915,plain,
op(e1,e2) = e3,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_3914]) ).
tff(c_3920,plain,
op(e1,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3915,c_148]) ).
tff(c_3954,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3295,c_3859,c_3904,c_3920,c_24]) ).
tff(c_3955,plain,
op(e2,e1) = e3,
inference(splitRight,[status(thm)],[c_3865]) ).
tff(c_3984,plain,
op(e2,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3955,c_138]) ).
tff(c_3959,plain,
op(e2,e2) = e0,
inference(negUnitSimplification,[status(thm)],[c_3278,c_3850,c_3297,c_80]) ).
tff(c_4013,plain,
( ( op(e1,e2) = e3 )
| ( e3 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_3959,c_3247]) ).
tff(c_4014,plain,
op(e1,e2) = e3,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_4013]) ).
tff(c_3989,plain,
( ( e3 = e0 )
| ( op(e2,e0) = e3 )
| ( op(e1,e0) = e3 )
| ( op(e0,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3293,c_100]) ).
tff(c_3990,plain,
( ( op(e2,e0) = e3 )
| ( op(e1,e0) = e3 )
| ( op(e0,e0) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_218,c_3989]) ).
tff(c_3991,plain,
op(e0,e0) = e3,
inference(splitLeft,[status(thm)],[c_3990]) ).
tff(c_3996,plain,
op(e1,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_3991,c_210]) ).
tff(c_4026,plain,
op(e1,e0) = e2,
inference(negUnitSimplification,[status(thm)],[c_3295,c_3859,c_3996,c_24]) ).
tff(c_274,plain,
( ( op(e1,e1) != e0 )
| ( op(e1,op(e1,e1)) != e2 )
| ( op(e1,op(e1,op(e1,e1))) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_754]) ).
tff(c_4138,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4014,c_4026,c_3833,c_4026,c_3833,c_3833,c_274]) ).
tff(c_4139,plain,
( ( op(e1,e0) = e3 )
| ( op(e2,e0) = e3 ) ),
inference(splitRight,[status(thm)],[c_3990]) ).
tff(c_4164,plain,
op(e1,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_3984,c_4139]) ).
tff(c_4169,plain,
op(e1,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4164,c_148]) ).
tff(c_4174,plain,
( ( op(e1,e2) = e3 )
| ( e3 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_3959,c_3247]) ).
tff(c_4175,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_4169,c_4174]) ).
tff(c_4176,plain,
( ( op(e1,e1) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(splitRight,[status(thm)],[c_3832]) ).
tff(c_4452,plain,
op(e1,e1) = e3,
inference(splitLeft,[status(thm)],[c_4176]) ).
tff(c_4457,plain,
op(e1,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4452,c_144]) ).
tff(c_4465,plain,
( ( op(e1,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_3247]) ).
tff(c_4466,plain,
op(e2,e2) = e3,
inference(negUnitSimplification,[status(thm)],[c_212,c_4457,c_4465]) ).
tff(c_224,plain,
( ( op(e3,e3) != e3 )
| ( op(e2,e2) != e3 )
| ( op(e1,e1) != e3 )
| ( op(e0,e0) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_622]) ).
tff(c_4598,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4418,c_4452,c_4466,c_2158,c_224]) ).
tff(c_4599,plain,
op(e1,e1) = e2,
inference(splitRight,[status(thm)],[c_4176]) ).
tff(c_4604,plain,
op(e0,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_4599,c_198]) ).
tff(c_3284,plain,
op(e0,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2162,c_194]) ).
tff(c_3254,plain,
op(e0,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2160,c_154]) ).
tff(c_30,plain,
( ( op(e0,e1) = e3 )
| ( op(e0,e1) = e2 )
| ( op(e0,e1) = e1 )
| ( op(e0,e1) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_3250,plain,
op(e0,e1) = e0,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_3271,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3254,c_3250]) ).
tff(c_3272,plain,
( ( op(e0,e1) = e1 )
| ( op(e0,e1) = e2 )
| ( op(e0,e1) = e3 ) ),
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_4636,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4431,c_4604,c_3284,c_3272]) ).
tff(c_4637,plain,
op(e0,e1) = e3,
inference(splitRight,[status(thm)],[c_4417]) ).
tff(c_4867,plain,
op(e1,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4637,c_198]) ).
tff(c_4897,plain,
op(e1,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_4867,c_4176]) ).
tff(c_4903,plain,
op(e1,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_4897,c_150]) ).
tff(c_4868,plain,
op(e2,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4637,c_196]) ).
tff(c_4643,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2163,c_140]) ).
tff(c_4649,plain,
( ( e2 = e1 )
| ( op(e2,e2) = e1 )
| ( op(e1,e2) = e1 )
| ( op(e0,e2) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2164,c_76]) ).
tff(c_4650,plain,
( ( op(e2,e2) = e1 )
| ( op(e0,e2) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_4643,c_216,c_4649]) ).
tff(c_4651,plain,
op(e0,e2) = e1,
inference(splitLeft,[status(thm)],[c_4650]) ).
tff(c_4638,plain,
op(e0,e0) != e3,
inference(splitRight,[status(thm)],[c_4417]) ).
tff(c_4672,plain,
op(e0,e0) = e2,
inference(negUnitSimplification,[status(thm)],[c_4638,c_3830]) ).
tff(c_268,plain,
( ( op(e0,e0) != e2 )
| ( op(e0,op(e0,e0)) != e1 )
| ( op(e0,op(e0,op(e0,e0))) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_736]) ).
tff(c_4862,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4637,c_4651,c_4672,c_4651,c_4672,c_4672,c_268]) ).
tff(c_4863,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_4650]) ).
tff(c_4885,plain,
( ( e3 = e2 )
| ( e3 = e1 )
| ( op(e2,e1) = e3 )
| ( op(e2,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4863,c_2165,c_70]) ).
tff(c_4886,plain,
op(e2,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_4868,c_214,c_212,c_4885]) ).
tff(c_4889,plain,
op(e1,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4886,c_204]) ).
tff(c_4950,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3295,c_4644,c_4903,c_4889,c_24]) ).
tff(c_4952,plain,
op(e3,e0) != e0,
inference(splitRight,[status(thm)],[c_3292]) ).
tff(c_4975,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4952,c_2161]) ).
tff(c_4976,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_2154]) ).
tff(c_6125,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_4976]) ).
tff(c_6128,plain,
op(e3,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_6125,c_36]) ).
tff(c_120,plain,
op(e3,e2) != op(e3,e1),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_6858,plain,
op(e3,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_6128,c_120]) ).
tff(c_6134,plain,
op(e1,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_6125,c_42]) ).
tff(c_6876,plain,
op(e2,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_6134,c_180]) ).
tff(c_7177,plain,
( ( op(e2,e2) = e3 )
| ( op(e2,e2) = e1 )
| ( op(e2,e2) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_6876,c_12]) ).
tff(c_7178,plain,
op(e2,e2) = e0,
inference(splitLeft,[status(thm)],[c_7177]) ).
tff(c_6135,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_6125,c_40]) ).
tff(c_6152,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_6135,c_130]) ).
tff(c_6129,plain,
op(e1,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_6125,c_38]) ).
tff(c_6130,plain,
op(e0,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_6125,c_48]) ).
tff(c_6226,plain,
op(e0,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_6130,c_154]) ).
tff(c_6288,plain,
( ( op(e3,e3) = e1 )
| ( op(e2,e3) = e1 )
| ( e3 = e1 )
| ( op(e0,e3) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6129,c_60]) ).
tff(c_6289,plain,
( ( op(e3,e3) = e1 )
| ( op(e2,e3) = e1 )
| ( op(e0,e3) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_6288]) ).
tff(c_6290,plain,
op(e0,e3) = e1,
inference(splitLeft,[status(thm)],[c_6289]) ).
tff(c_6140,plain,
op(e0,e2) = e3,
inference(splitLeft,[status(thm)],[c_68]) ).
tff(c_106,plain,
( ( op(e0,e3) = e2 )
| ( op(e0,e2) = e2 )
| ( op(e0,e1) = e2 )
| ( op(e0,e0) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_6371,plain,
( ( e2 = e1 )
| ( e3 = e2 )
| ( e2 = e0 )
| ( op(e0,e0) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6130,c_6140,c_6290,c_106]) ).
tff(c_6372,plain,
op(e0,e0) = e2,
inference(negUnitSimplification,[status(thm)],[c_220,c_212,c_216,c_6371]) ).
tff(c_246,plain,
( ( op(e0,e0) != e2 )
| ( op(e0,op(e0,e0)) != e3 )
| ( op(e0,op(e0,op(e0,e0))) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_670]) ).
tff(c_6466,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6290,c_6140,c_6372,c_6140,c_6372,c_6372,c_246]) ).
tff(c_6468,plain,
op(e0,e3) != e1,
inference(splitRight,[status(thm)],[c_6289]) ).
tff(c_6131,plain,
op(e1,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_6125,c_50]) ).
tff(c_6178,plain,
op(e3,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_6131,c_202]) ).
tff(c_66,plain,
( ( op(e3,e3) = e0 )
| ( op(e3,e2) = e0 )
| ( op(e3,e1) = e0 )
| ( op(e3,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_6255,plain,
( ( op(e3,e3) = e0 )
| ( op(e3,e2) = e0 )
| ( e3 = e0 )
| ( op(e3,e0) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6128,c_66]) ).
tff(c_6256,plain,
( ( op(e3,e3) = e0 )
| ( op(e3,e2) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_6178,c_218,c_6255]) ).
tff(c_6257,plain,
op(e3,e2) = e0,
inference(splitLeft,[status(thm)],[c_6256]) ).
tff(c_6263,plain,
op(e3,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_6257,c_116]) ).
tff(c_6146,plain,
op(e3,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_6128,c_126]) ).
tff(c_4978,plain,
op(e0,e0) = e3,
inference(splitLeft,[status(thm)],[c_100]) ).
tff(c_4979,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_4976]) ).
tff(c_4985,plain,
op(e1,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_4979,c_50]) ).
tff(c_5295,plain,
( ( op(e3,e0) = e1 )
| ( op(e2,e0) = e1 )
| ( e1 = e0 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4978,c_4985,c_108]) ).
tff(c_5296,plain,
( ( op(e3,e0) = e1 )
| ( op(e2,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_222,c_5295]) ).
tff(c_5297,plain,
op(e2,e0) = e1,
inference(splitLeft,[status(thm)],[c_5296]) ).
tff(c_5303,plain,
op(e2,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_5297,c_134]) ).
tff(c_4989,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_4979,c_40]) ).
tff(c_5288,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_4989,c_130]) ).
tff(c_4983,plain,
op(e1,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_4979,c_38]) ).
tff(c_5014,plain,
op(e2,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4983,c_168]) ).
tff(c_5375,plain,
op(e2,e3) = e0,
inference(negUnitSimplification,[status(thm)],[c_5303,c_5288,c_5014,c_10]) ).
tff(c_4982,plain,
op(e3,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_4979,c_36]) ).
tff(c_5004,plain,
op(e2,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4982,c_188]) ).
tff(c_5122,plain,
( ( op(e2,e2) = e3 )
| ( op(e2,e0) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_5004,c_5014,c_70]) ).
tff(c_5123,plain,
op(e2,e0) = e3,
inference(splitLeft,[status(thm)],[c_5122]) ).
tff(c_4995,plain,
op(e2,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4978,c_208]) ).
tff(c_5154,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5123,c_4995]) ).
tff(c_5155,plain,
op(e2,e2) = e3,
inference(splitRight,[status(thm)],[c_5122]) ).
tff(c_248,plain,
( ( op(e2,e2) != e3 )
| ( op(e2,op(e2,e2)) != e0 )
| ( op(e2,op(e2,op(e2,e2))) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_676]) ).
tff(c_5463,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5297,c_5375,c_5155,c_5375,c_5155,c_5155,c_248]) ).
tff(c_5464,plain,
op(e3,e0) = e1,
inference(splitRight,[status(thm)],[c_5296]) ).
tff(c_5115,plain,
op(e2,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_4985,c_204]) ).
tff(c_5114,plain,
op(e3,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_4985,c_202]) ).
tff(c_5009,plain,
op(e3,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4982,c_126]) ).
tff(c_5168,plain,
( ( op(e3,e0) = e2 )
| ( op(e3,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_5114,c_5009,c_8]) ).
tff(c_5169,plain,
op(e3,e0) = e1,
inference(splitLeft,[status(thm)],[c_5168]) ).
tff(c_5182,plain,
op(e2,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_5169,c_200]) ).
tff(c_5175,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_4989,c_138]) ).
tff(c_5156,plain,
op(e2,e0) != e3,
inference(splitRight,[status(thm)],[c_5122]) ).
tff(c_5282,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5115,c_5182,c_5175,c_5156,c_16]) ).
tff(c_5284,plain,
op(e3,e0) != e1,
inference(splitRight,[status(thm)],[c_5168]) ).
tff(c_5488,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5464,c_5284]) ).
tff(c_5489,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_4976]) ).
tff(c_5493,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_5489,c_36]) ).
tff(c_5816,plain,
op(e3,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_5493,c_120]) ).
tff(c_5498,plain,
op(e1,e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_5489,c_44]) ).
tff(c_5561,plain,
( ( op(e1,e3) = e0 )
| ( e1 = e0 )
| ( op(e1,e1) = e0 )
| ( op(e1,e0) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5498,c_98]) ).
tff(c_5562,plain,
( ( op(e1,e3) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e1,e0) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_222,c_5561]) ).
tff(c_5563,plain,
op(e1,e0) = e0,
inference(splitLeft,[status(thm)],[c_5562]) ).
tff(c_5496,plain,
op(e2,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_5489,c_50]) ).
tff(c_5568,plain,
op(e1,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_5496,c_204]) ).
tff(c_5612,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5563,c_5568]) ).
tff(c_5614,plain,
op(e1,e0) != e0,
inference(splitRight,[status(thm)],[c_5562]) ).
tff(c_5521,plain,
op(e1,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_5498,c_148]) ).
tff(c_5795,plain,
op(e1,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4978,c_210]) ).
tff(c_6025,plain,
op(e1,e0) = e2,
inference(negUnitSimplification,[status(thm)],[c_5614,c_5521,c_5795,c_24]) ).
tff(c_5613,plain,
( ( op(e1,e1) = e0 )
| ( op(e1,e3) = e0 ) ),
inference(splitRight,[status(thm)],[c_5562]) ).
tff(c_5823,plain,
op(e1,e3) = e0,
inference(splitLeft,[status(thm)],[c_5613]) ).
tff(c_5497,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_5489,c_46]) ).
tff(c_5615,plain,
( ( op(e3,e1) = e3 )
| ( e3 = e1 )
| ( op(e1,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5497,c_84]) ).
tff(c_5616,plain,
( ( op(e3,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_5615]) ).
tff(c_5617,plain,
op(e0,e1) = e3,
inference(splitLeft,[status(thm)],[c_5616]) ).
tff(c_5641,plain,
op(e0,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_4978,c_162]) ).
tff(c_5660,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5617,c_5641]) ).
tff(c_5661,plain,
( ( op(e1,e1) = e3 )
| ( op(e3,e1) = e3 ) ),
inference(splitRight,[status(thm)],[c_5616]) ).
tff(c_5836,plain,
op(e1,e1) = e3,
inference(negUnitSimplification,[status(thm)],[c_5816,c_5661]) ).
tff(c_260,plain,
( ( op(e1,e1) != e3 )
| ( op(e1,op(e1,e1)) != e0 )
| ( op(e1,op(e1,op(e1,e1))) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_712]) ).
tff(c_6109,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6025,c_5823,c_5836,c_5823,c_5836,c_5836,c_260]) ).
tff(c_6110,plain,
op(e1,e1) = e0,
inference(splitRight,[status(thm)],[c_5613]) ).
tff(c_6121,plain,
( ( e3 = e0 )
| ( op(e3,e1) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6110,c_5661]) ).
tff(c_6122,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5816,c_218,c_6121]) ).
tff(c_6123,plain,
( ( op(e1,e0) = e3 )
| ( op(e2,e0) = e3 )
| ( op(e3,e0) = e3 ) ),
inference(splitRight,[status(thm)],[c_100]) ).
tff(c_6274,plain,
( ( e3 = e0 )
| ( op(e2,e0) = e3 )
| ( op(e3,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6131,c_6123]) ).
tff(c_6275,plain,
op(e2,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_6146,c_218,c_6274]) ).
tff(c_6467,plain,
( ( op(e2,e3) = e1 )
| ( op(e3,e3) = e1 ) ),
inference(splitRight,[status(thm)],[c_6289]) ).
tff(c_6469,plain,
op(e3,e3) = e1,
inference(splitLeft,[status(thm)],[c_6467]) ).
tff(c_58,plain,
( ( op(e3,e3) = e2 )
| ( op(e3,e2) = e2 )
| ( op(e3,e1) = e2 )
| ( op(e3,e0) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_6539,plain,
( ( e2 = e1 )
| ( e2 = e0 )
| ( e3 = e2 )
| ( op(e3,e0) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6128,c_6257,c_6469,c_58]) ).
tff(c_6540,plain,
op(e3,e0) = e2,
inference(negUnitSimplification,[status(thm)],[c_212,c_220,c_216,c_6539]) ).
tff(c_6565,plain,
( ( e2 = e1 )
| ( e3 = e1 )
| ( e1 = e0 )
| ( op(e0,e0) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6131,c_6275,c_6540,c_108]) ).
tff(c_6566,plain,
op(e0,e0) = e1,
inference(negUnitSimplification,[status(thm)],[c_222,c_214,c_216,c_6565]) ).
tff(c_6133,plain,
op(e1,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_6125,c_44]) ).
tff(c_6265,plain,
op(e2,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_6257,c_176]) ).
tff(c_6162,plain,
op(e2,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_6134,c_180]) ).
tff(c_6248,plain,
op(e2,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_6140,c_184]) ).
tff(c_6494,plain,
op(e2,e2) = e1,
inference(negUnitSimplification,[status(thm)],[c_6265,c_6162,c_6248,c_12]) ).
tff(c_228,plain,
( ( op(e3,e3) != e1 )
| ( op(e2,e2) != e1 )
| ( op(e1,e1) != e1 )
| ( op(e0,e0) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_622]) ).
tff(c_6577,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6566,c_6133,c_6494,c_6469,c_228]) ).
tff(c_6578,plain,
op(e2,e3) = e1,
inference(splitRight,[status(thm)],[c_6467]) ).
tff(c_6589,plain,
( ( op(e3,e3) = e2 )
| ( e2 = e1 )
| ( e3 = e2 )
| ( op(e0,e3) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6129,c_6578,c_56]) ).
tff(c_6590,plain,
( ( op(e3,e3) = e2 )
| ( op(e0,e3) = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_212,c_216,c_6589]) ).
tff(c_6591,plain,
op(e0,e3) = e2,
inference(splitLeft,[status(thm)],[c_6590]) ).
tff(c_6606,plain,
( ( op(e3,e3) = e0 )
| ( e1 = e0 )
| ( e3 = e0 )
| ( e2 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6591,c_6129,c_6578,c_64]) ).
tff(c_6607,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_220,c_218,c_222,c_6263,c_6606]) ).
tff(c_6609,plain,
op(e0,e3) != e2,
inference(splitRight,[status(thm)],[c_6590]) ).
tff(c_52,plain,
( ( op(e3,e3) = e3 )
| ( op(e2,e3) = e3 )
| ( op(e1,e3) = e3 )
| ( op(e0,e3) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_6187,plain,
op(e0,e3) = e3,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_174,plain,
op(e1,e3) != op(e0,e3),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_6191,plain,
op(e1,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_6187,c_174]) ).
tff(c_6218,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6191,c_6129]) ).
tff(c_6220,plain,
op(e0,e3) != e3,
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_26,plain,
( ( op(e0,e3) = e3 )
| ( op(e0,e3) = e2 )
| ( op(e0,e3) = e1 )
| ( op(e0,e3) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_6619,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6226,c_6468,c_6609,c_6220,c_26]) ).
tff(c_6620,plain,
op(e3,e3) = e0,
inference(splitRight,[status(thm)],[c_6256]) ).
tff(c_6651,plain,
( ( e1 = e0 )
| ( op(e2,e3) = e1 )
| ( e3 = e1 )
| ( op(e0,e3) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6129,c_6620,c_60]) ).
tff(c_6652,plain,
( ( op(e2,e3) = e1 )
| ( op(e0,e3) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_214,c_222,c_6651]) ).
tff(c_6653,plain,
op(e0,e3) = e1,
inference(splitLeft,[status(thm)],[c_6652]) ).
tff(c_6691,plain,
( ( e2 = e0 )
| ( op(e2,e3) = e2 )
| ( e3 = e2 )
| ( e2 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6653,c_6129,c_6620,c_56]) ).
tff(c_6692,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216,c_212,c_6152,c_220,c_6691]) ).
tff(c_6693,plain,
op(e2,e3) = e1,
inference(splitRight,[status(thm)],[c_6652]) ).
tff(c_6637,plain,
( ( e3 = e0 )
| ( op(e2,e0) = e3 )
| ( op(e3,e0) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6131,c_6123]) ).
tff(c_6638,plain,
op(e2,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_6146,c_218,c_6637]) ).
tff(c_6699,plain,
op(e2,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_6693,c_128]) ).
tff(c_6706,plain,
op(e2,e2) = e0,
inference(negUnitSimplification,[status(thm)],[c_6699,c_6162,c_6248,c_12]) ).
tff(c_250,plain,
( ( op(e2,e2) != e0 )
| ( op(e2,op(e2,e2)) != e3 )
| ( op(e2,op(e2,op(e2,e2))) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_682]) ).
tff(c_6852,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6693,c_6638,c_6706,c_6638,c_6706,c_6706,c_250]) ).
tff(c_6853,plain,
( ( op(e1,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e3,e2) = e3 ) ),
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_7211,plain,
( ( e3 = e2 )
| ( e3 = e0 )
| ( op(e3,e2) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7178,c_6134,c_6853]) ).
tff(c_7212,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6858,c_218,c_212,c_7211]) ).
tff(c_7213,plain,
( ( op(e2,e2) = e1 )
| ( op(e2,e2) = e3 ) ),
inference(splitRight,[status(thm)],[c_7177]) ).
tff(c_7215,plain,
op(e2,e2) = e3,
inference(splitLeft,[status(thm)],[c_7213]) ).
tff(c_7224,plain,
op(e2,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_7215,c_136]) ).
tff(c_6860,plain,
op(e3,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_6128,c_126]) ).
tff(c_7056,plain,
( ( op(e3,e0) = e2 )
| ( op(e3,e0) = e1 )
| ( op(e3,e0) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_6860,c_8]) ).
tff(c_7057,plain,
op(e3,e0) = e0,
inference(splitLeft,[status(thm)],[c_7056]) ).
tff(c_7040,plain,
op(e3,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_6131,c_202]) ).
tff(c_7070,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7057,c_7040]) ).
tff(c_7071,plain,
( ( op(e3,e0) = e1 )
| ( op(e3,e0) = e2 ) ),
inference(splitRight,[status(thm)],[c_7056]) ).
tff(c_7077,plain,
op(e3,e0) = e2,
inference(splitLeft,[status(thm)],[c_7071]) ).
tff(c_7138,plain,
( ( e3 = e0 )
| ( op(e2,e0) = e3 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7077,c_6131,c_6123]) ).
tff(c_7139,plain,
op(e2,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_7138]) ).
tff(c_7144,plain,
op(e2,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_7139,c_136]) ).
tff(c_7162,plain,
( ( e3 = e2 )
| ( op(e2,e2) = e3 )
| ( op(e3,e2) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6134,c_6853]) ).
tff(c_7163,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6858,c_7144,c_212,c_7162]) ).
tff(c_7164,plain,
op(e3,e0) = e1,
inference(splitRight,[status(thm)],[c_7071]) ).
tff(c_7239,plain,
( ( e3 = e0 )
| ( op(e2,e0) = e3 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7164,c_6131,c_6123]) ).
tff(c_7240,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_214,c_7224,c_218,c_7239]) ).
tff(c_7241,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_7213]) ).
tff(c_7303,plain,
( ( e3 = e2 )
| ( e3 = e1 )
| ( op(e3,e2) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7241,c_6134,c_6853]) ).
tff(c_7304,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6858,c_214,c_212,c_7303]) ).
tff(c_7305,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_4976]) ).
tff(c_7312,plain,
op(e2,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_7305,c_50]) ).
tff(c_8086,plain,
op(e3,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_7312,c_200]) ).
tff(c_7402,plain,
op(e3,e1) = e0,
inference(splitLeft,[status(thm)],[c_6]) ).
tff(c_7965,plain,
op(e1,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_7402,c_190]) ).
tff(c_7313,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_7305,c_46]) ).
tff(c_7414,plain,
op(e1,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7313,c_192]) ).
tff(c_7963,plain,
op(e3,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_7402,c_118]) ).
tff(c_7314,plain,
op(e1,e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_7305,c_44]) ).
tff(c_7945,plain,
op(e1,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7314,c_148]) ).
tff(c_7310,plain,
op(e2,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_7305,c_38]) ).
tff(c_7333,plain,
op(e0,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_7310,c_172]) ).
tff(c_7616,plain,
op(e3,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_7402,c_118]) ).
tff(c_7430,plain,
op(e1,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7314,c_148]) ).
tff(c_7436,plain,
( ( op(e3,e0) = e1 )
| ( e1 = e0 )
| ( op(e1,e0) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7312,c_108]) ).
tff(c_7437,plain,
( ( op(e3,e0) = e1 )
| ( op(e1,e0) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_222,c_7436]) ).
tff(c_7438,plain,
op(e0,e0) = e1,
inference(splitLeft,[status(thm)],[c_7437]) ).
tff(c_7311,plain,
op(e0,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_7305,c_48]) ).
tff(c_7423,plain,
( ( op(e0,e3) = e2 )
| ( e2 = e0 )
| ( op(e0,e1) = e2 )
| ( op(e0,e0) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7311,c_106]) ).
tff(c_7424,plain,
( ( op(e0,e3) = e2 )
| ( op(e0,e1) = e2 )
| ( op(e0,e0) = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_220,c_7423]) ).
tff(c_7425,plain,
op(e0,e0) = e2,
inference(splitLeft,[status(thm)],[c_7424]) ).
tff(c_7458,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_7438,c_7425]) ).
tff(c_7459,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216,c_7458]) ).
tff(c_7460,plain,
( ( op(e1,e0) = e1 )
| ( op(e3,e0) = e1 ) ),
inference(splitRight,[status(thm)],[c_7437]) ).
tff(c_7637,plain,
op(e3,e0) = e1,
inference(negUnitSimplification,[status(thm)],[c_7430,c_7460]) ).
tff(c_122,plain,
op(e3,e3) != op(e3,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_7642,plain,
op(e3,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7637,c_122]) ).
tff(c_7428,plain,
op(e1,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7314,c_140]) ).
tff(c_7500,plain,
op(e0,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_7425,c_158]) ).
tff(c_7346,plain,
op(e0,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_7311,c_152]) ).
tff(c_7351,plain,
op(e0,e3) = e0,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_7399,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7346,c_7351]) ).
tff(c_7400,plain,
( ( op(e0,e3) = e1 )
| ( op(e0,e3) = e2 )
| ( op(e0,e3) = e3 ) ),
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_7528,plain,
op(e0,e3) = e1,
inference(negUnitSimplification,[status(thm)],[c_7333,c_7500,c_7400]) ).
tff(c_7546,plain,
( ( e3 = e1 )
| ( e3 = e0 )
| ( op(e0,e1) = e3 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7425,c_7311,c_7528,c_102]) ).
tff(c_7547,plain,
op(e0,e1) = e3,
inference(negUnitSimplification,[status(thm)],[c_212,c_218,c_214,c_7546]) ).
tff(c_88,plain,
( ( op(e3,e1) = e2 )
| ( op(e2,e1) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e0,e1) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_7566,plain,
( ( e2 = e0 )
| ( e2 = e1 )
| ( op(e1,e1) = e2 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7547,c_7313,c_7402,c_88]) ).
tff(c_7567,plain,
op(e1,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_212,c_216,c_220,c_7566]) ).
tff(c_7316,plain,
op(e2,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_7305,c_40]) ).
tff(c_7335,plain,
op(e1,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_7310,c_168]) ).
tff(c_18,plain,
( ( op(e1,e3) = e3 )
| ( op(e1,e3) = e2 )
| ( op(e1,e3) = e1 )
| ( op(e1,e3) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_7462,plain,
( ( op(e1,e3) = e2 )
| ( op(e1,e3) = e1 )
| ( op(e1,e3) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_7335,c_18]) ).
tff(c_7463,plain,
op(e1,e3) = e0,
inference(splitLeft,[status(thm)],[c_7462]) ).
tff(c_166,plain,
op(e3,e3) != op(e1,e3),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_7475,plain,
op(e3,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_7463,c_166]) ).
tff(c_7508,plain,
op(e3,e0) = e1,
inference(negUnitSimplification,[status(thm)],[c_7430,c_7460]) ).
tff(c_7513,plain,
op(e3,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7508,c_122]) ).
tff(c_7337,plain,
op(e3,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_7310,c_164]) ).
tff(c_2,plain,
( ( op(e3,e3) = e3 )
| ( op(e3,e3) = e2 )
| ( op(e3,e3) = e1 )
| ( op(e3,e3) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_7556,plain,
op(e3,e3) = e2,
inference(negUnitSimplification,[status(thm)],[c_7475,c_7513,c_7337,c_2]) ).
tff(c_226,plain,
( ( op(e3,e3) != e2 )
| ( op(e2,e2) != e2 )
| ( op(e1,e1) != e2 )
| ( op(e0,e0) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_622]) ).
tff(c_7600,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7425,c_7567,c_7316,c_7556,c_226]) ).
tff(c_7601,plain,
( ( op(e1,e3) = e1 )
| ( op(e1,e3) = e2 ) ),
inference(splitRight,[status(thm)],[c_7462]) ).
tff(c_7647,plain,
op(e1,e3) = e2,
inference(negUnitSimplification,[status(thm)],[c_7428,c_7601]) ).
tff(c_7651,plain,
op(e3,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_7647,c_166]) ).
tff(c_7701,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7616,c_7642,c_7651,c_7337,c_2]) ).
tff(c_7702,plain,
( ( op(e0,e1) = e2 )
| ( op(e0,e3) = e2 ) ),
inference(splitRight,[status(thm)],[c_7424]) ).
tff(c_7749,plain,
op(e0,e3) = e2,
inference(splitLeft,[status(thm)],[c_7702]) ).
tff(c_7704,plain,
( ( op(e3,e0) = e1 )
| ( e1 = e0 )
| ( op(e1,e0) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7312,c_108]) ).
tff(c_7705,plain,
( ( op(e3,e0) = e1 )
| ( op(e1,e0) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_222,c_7704]) ).
tff(c_7706,plain,
op(e0,e0) = e1,
inference(splitLeft,[status(thm)],[c_7705]) ).
tff(c_7825,plain,
( ( e3 = e2 )
| ( e3 = e0 )
| ( op(e0,e1) = e3 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7706,c_7311,c_7749,c_102]) ).
tff(c_7826,plain,
op(e0,e1) = e3,
inference(negUnitSimplification,[status(thm)],[c_214,c_218,c_212,c_7825]) ).
tff(c_258,plain,
( ( op(e0,e0) != e1 )
| ( op(e0,op(e0,e0)) != e3 )
| ( op(e0,op(e0,op(e0,e0))) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_706]) ).
tff(c_7904,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7749,c_7826,c_7706,c_7826,c_7706,c_7706,c_258]) ).
tff(c_7906,plain,
op(e0,e3) != e2,
inference(splitRight,[status(thm)],[c_7702]) ).
tff(c_7743,plain,
op(e0,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7706,c_158]) ).
tff(c_7937,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7333,c_7906,c_7743,c_7400]) ).
tff(c_7938,plain,
( ( op(e1,e0) = e1 )
| ( op(e3,e0) = e1 ) ),
inference(splitRight,[status(thm)],[c_7705]) ).
tff(c_7971,plain,
op(e3,e0) = e1,
inference(negUnitSimplification,[status(thm)],[c_7945,c_7938]) ).
tff(c_7975,plain,
op(e3,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7971,c_122]) ).
tff(c_7981,plain,
op(e0,e3) = e2,
inference(splitLeft,[status(thm)],[c_7702]) ).
tff(c_170,plain,
op(e3,e3) != op(e0,e3),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_7986,plain,
op(e3,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_7981,c_170]) ).
tff(c_8019,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7963,c_7975,c_7986,c_7337,c_2]) ).
tff(c_8020,plain,
op(e0,e1) = e2,
inference(splitRight,[status(thm)],[c_7702]) ).
tff(c_8024,plain,
op(e1,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_8020,c_198]) ).
tff(c_8042,plain,
( ( op(e1,e0) = e3 )
| ( e3 = e0 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7971,c_7312,c_6123]) ).
tff(c_8043,plain,
op(e1,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_214,c_218,c_8042]) ).
tff(c_8048,plain,
op(e1,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_8043,c_150]) ).
tff(c_8082,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7965,c_7414,c_8024,c_8048,c_22]) ).
tff(c_8084,plain,
op(e3,e1) != e0,
inference(splitRight,[status(thm)],[c_6]) ).
tff(c_7309,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_7305,c_36]) ).
tff(c_8322,plain,
( ( op(e3,e3) = e0 )
| ( e3 = e0 )
| ( op(e3,e1) = e0 )
| ( op(e3,e0) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7309,c_66]) ).
tff(c_8323,plain,
( ( op(e3,e3) = e0 )
| ( op(e3,e0) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_8084,c_218,c_8322]) ).
tff(c_8324,plain,
op(e3,e0) = e0,
inference(splitLeft,[status(thm)],[c_8323]) ).
tff(c_8360,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8086,c_8324]) ).
tff(c_8361,plain,
op(e3,e3) = e0,
inference(splitRight,[status(thm)],[c_8323]) ).
tff(c_8480,plain,
op(e1,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_8361,c_166]) ).
tff(c_8315,plain,
op(e1,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7314,c_140]) ).
tff(c_8521,plain,
op(e1,e3) = e2,
inference(negUnitSimplification,[status(thm)],[c_8480,c_8315,c_7335,c_18]) ).
tff(c_8526,plain,
op(e1,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_8521,c_146]) ).
tff(c_8389,plain,
( ( e1 = e0 )
| ( e3 = e1 )
| ( op(e1,e3) = e1 )
| ( op(e0,e3) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7310,c_8361,c_60]) ).
tff(c_8390,plain,
op(e0,e3) = e1,
inference(negUnitSimplification,[status(thm)],[c_8315,c_214,c_222,c_8389]) ).
tff(c_8394,plain,
op(e0,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_8390,c_158]) ).
tff(c_8317,plain,
op(e1,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7314,c_148]) ).
tff(c_8363,plain,
( ( op(e3,e0) = e1 )
| ( e1 = e0 )
| ( op(e1,e0) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7312,c_108]) ).
tff(c_8364,plain,
( ( op(e3,e0) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_8317,c_222,c_8363]) ).
tff(c_8365,plain,
op(e0,e0) = e1,
inference(splitLeft,[status(thm)],[c_8364]) ).
tff(c_8408,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8394,c_8365]) ).
tff(c_8409,plain,
op(e3,e0) = e1,
inference(splitRight,[status(thm)],[c_8364]) ).
tff(c_7323,plain,
op(e3,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_7309,c_120]) ).
tff(c_8113,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_7313,c_188]) ).
tff(c_8083,plain,
( ( op(e3,e1) = e1 )
| ( op(e3,e1) = e2 )
| ( op(e3,e1) = e3 ) ),
inference(splitRight,[status(thm)],[c_6]) ).
tff(c_8167,plain,
op(e3,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_7323,c_8113,c_8083]) ).
tff(c_8095,plain,
( ( op(e0,e3) = e2 )
| ( e2 = e0 )
| ( op(e0,e1) = e2 )
| ( op(e0,e0) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7311,c_106]) ).
tff(c_8096,plain,
( ( op(e0,e3) = e2 )
| ( op(e0,e1) = e2 )
| ( op(e0,e0) = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_220,c_8095]) ).
tff(c_8097,plain,
op(e0,e0) = e2,
inference(splitLeft,[status(thm)],[c_8096]) ).
tff(c_206,plain,
op(e3,e0) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_8134,plain,
op(e3,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_8097,c_206]) ).
tff(c_7325,plain,
op(e3,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_7309,c_124]) ).
tff(c_8191,plain,
op(e3,e0) = e1,
inference(negUnitSimplification,[status(thm)],[c_8086,c_8134,c_7325,c_8]) ).
tff(c_8137,plain,
op(e0,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_8097,c_158]) ).
tff(c_8144,plain,
op(e0,e3) = e1,
inference(negUnitSimplification,[status(thm)],[c_7333,c_8137,c_7400]) ).
tff(c_8148,plain,
op(e3,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_8144,c_170]) ).
tff(c_8171,plain,
op(e3,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_8167,c_118]) ).
tff(c_8179,plain,
op(e3,e3) = e0,
inference(negUnitSimplification,[status(thm)],[c_8148,c_8171,c_7337,c_2]) ).
tff(c_266,plain,
( ( op(e3,e3) != e0 )
| ( op(e3,op(e3,e3)) != e1 )
| ( op(e3,op(e3,op(e3,e3))) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_730]) ).
tff(c_8309,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8167,c_8191,c_8179,c_8191,c_8179,c_8179,c_266]) ).
tff(c_8311,plain,
op(e0,e0) != e2,
inference(splitRight,[status(thm)],[c_8096]) ).
tff(c_104,plain,
( ( op(e3,e0) = e2 )
| ( op(e2,e0) = e2 )
| ( op(e1,e0) = e2 )
| ( op(e0,e0) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_8411,plain,
( ( op(e3,e0) = e2 )
| ( e2 = e0 )
| ( op(e1,e0) = e2 )
| ( op(e0,e0) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7312,c_104]) ).
tff(c_8412,plain,
( ( op(e3,e0) = e2 )
| ( op(e1,e0) = e2 )
| ( op(e0,e0) = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_220,c_8411]) ).
tff(c_8413,plain,
op(e0,e0) = e2,
inference(splitLeft,[status(thm)],[c_8412]) ).
tff(c_8459,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8311,c_8413]) ).
tff(c_8460,plain,
( ( op(e1,e0) = e2 )
| ( op(e3,e0) = e2 ) ),
inference(splitRight,[status(thm)],[c_8412]) ).
tff(c_8542,plain,
( ( op(e1,e0) = e2 )
| ( e2 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8409,c_8460]) ).
tff(c_8543,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216,c_8526,c_8542]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : ALG046+1 : TPTP v9.0.0. Released v2.7.0.
% 0.04/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.15/0.36 % Computer : n023.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Sun Apr 6 06:57:09 EDT 2025
% 0.15/0.36 % CPUTime :
% 10.84/3.55 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.35/3.62
% 11.35/3.62 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------