%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ALG023+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n003.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:23:59 PM UTC 2025
% Result : Unsatisfiable 23.01s 9.67s
% Output : CNFRefutation 23.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 30
% Syntax : Number of formulae : 1398 (1180 unt; 0 typ; 0 def)
% Number of atoms : 2005 (1803 equ)
% Maximal formula atoms : 64 ( 1 avg)
% Number of connectives : 1008 ( 401 ~; 390 |; 201 &)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 2 avg)
% Maximal term depth : 3 ( 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 : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ op > #nlpp > inv > 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(inv,type,
inv: $i > $i ).
tff(op,type,
op: ( $i * $i ) > $i ).
tff(unit,type,
unit: $i ).
tff(e3,type,
e3: $i ).
tff(f_597,axiom,
( ( e0 != e1 )
& ( e0 != e2 )
& ( e0 != e3 )
& ( e1 != e2 )
& ( e1 != e3 )
& ( e2 != e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
tff(f_660,axiom,
~ ( ( e1 = op(e2,e2) )
& ( e0 = op(e3,e2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
tff(f_664,axiom,
~ ( ( e1 = op(e3,e3) )
& ( e2 = op(e0,e3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
tff(f_720,axiom,
~ ( ( e3 = op(e1,e1) )
& ( e2 = op(e0,e1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax34) ).
tff(f_688,axiom,
~ ( ( e2 = op(e3,e3) )
& ( e1 = op(e0,e3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
tff(f_420,axiom,
( ( ( inv(e0) = e0 )
=> ( inv(e0) = e0 ) )
& ( ( inv(e0) = e1 )
=> ( inv(e1) = e0 ) )
& ( ( inv(e0) = e2 )
=> ( inv(e2) = e0 ) )
& ( ( inv(e0) = e3 )
=> ( inv(e3) = e0 ) )
& ( ( inv(e1) = e0 )
=> ( inv(e0) = e1 ) )
& ( ( inv(e1) = e1 )
=> ( inv(e1) = e1 ) )
& ( ( inv(e1) = e2 )
=> ( inv(e2) = e1 ) )
& ( ( inv(e1) = e3 )
=> ( inv(e3) = e1 ) )
& ( ( inv(e2) = e0 )
=> ( inv(e0) = e2 ) )
& ( ( inv(e2) = e1 )
=> ( inv(e1) = e2 ) )
& ( ( inv(e2) = e2 )
=> ( inv(e2) = e2 ) )
& ( ( inv(e2) = e3 )
=> ( inv(e3) = e2 ) )
& ( ( inv(e3) = e0 )
=> ( inv(e0) = e3 ) )
& ( ( inv(e3) = e1 )
=> ( inv(e1) = e3 ) )
& ( ( inv(e3) = e2 )
=> ( inv(e2) = e3 ) )
& ( ( inv(e3) = e3 )
=> ( inv(e3) = e3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
tff(f_349,axiom,
( ( op(e0,inv(e0)) = unit )
& ( op(inv(e0),e0) = unit )
& ( op(e1,inv(e1)) = unit )
& ( op(inv(e1),e1) = unit )
& ( op(e2,inv(e2)) = unit )
& ( op(inv(e2),e2) = unit )
& ( op(e3,inv(e3)) = unit )
& ( op(inv(e3),e3) = unit )
& ( ( inv(e0) = e0 )
| ( inv(e0) = e1 )
| ( inv(e0) = e2 )
| ( inv(e0) = e3 ) )
& ( ( inv(e1) = e0 )
| ( inv(e1) = e1 )
| ( inv(e1) = e2 )
| ( inv(e1) = e3 ) )
& ( ( inv(e2) = e0 )
| ( inv(e2) = e1 )
| ( inv(e2) = e2 )
| ( inv(e2) = e3 ) )
& ( ( inv(e3) = e0 )
| ( inv(e3) = e1 )
| ( inv(e3) = e2 )
| ( inv(e3) = e3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
tff(f_708,axiom,
~ ( ( e3 = op(e1,e1) )
& ( e0 = op(e2,e1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax31) ).
tff(f_696,axiom,
~ ( ( e2 = op(e1,e1) )
& ( e3 = op(e0,e1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
tff(f_700,axiom,
~ ( ( e2 = op(e0,e0) )
& ( e3 = op(e1,e0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
tff(f_668,axiom,
~ ( ( e1 = op(e0,e0) )
& ( e2 = op(e3,e0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
tff(f_716,axiom,
~ ( ( e3 = op(e0,e0) )
& ( e1 = op(e2,e0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax33) ).
tff(f_632,axiom,
~ ( ( e0 = op(e3,e3) )
& ( e1 = op(e2,e3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
tff(f_302,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/sandbox/benchmark/theBenchmark.p',ax3) ).
tff(f_580,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/sandbox/benchmark/theBenchmark.p',ax9) ).
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/sandbox/benchmark/theBenchmark.p',ax1) ).
tff(f_704,axiom,
~ ( ( e3 = op(e2,e2) )
& ( e0 = op(e1,e2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax30) ).
tff(f_712,axiom,
~ ( ( e3 = op(e2,e2) )
& ( e1 = op(e0,e2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax32) ).
tff(f_680,axiom,
~ ( ( e2 = op(e3,e3) )
& ( e0 = op(e1,e3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
tff(f_656,axiom,
~ ( ( e1 = op(e3,e3) )
& ( e0 = op(e2,e3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
tff(f_672,axiom,
~ ( ( e1 = op(e2,e2) )
& ( e3 = op(e0,e2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
tff(f_676,axiom,
~ ( ( e1 = op(e0,e0) )
& ( e3 = op(e2,e0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
tff(f_437,axiom,
( ( inv(e0) != inv(e1) )
& ( inv(e0) != inv(e2) )
& ( inv(e0) != inv(e3) )
& ( inv(e1) != inv(e2) )
& ( inv(e1) != inv(e3) )
& ( inv(e2) != inv(e3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
tff(f_350,axiom,
inv(unit) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
tff(f_628,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/sandbox/benchmark/theBenchmark.p',ax11) ).
tff(f_692,axiom,
~ ( ( e2 = op(e0,e0) )
& ( e1 = op(e3,e0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
tff(f_652,axiom,
~ ( ( e0 = op(e1,e1) )
& ( e3 = op(e2,e1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
tff(f_279,axiom,
( ( op(op(e0,e0),e0) = op(e0,op(e0,e0)) )
& ( op(op(e0,e0),e1) = op(e0,op(e0,e1)) )
& ( op(op(e0,e0),e2) = op(e0,op(e0,e2)) )
& ( op(op(e0,e0),e3) = op(e0,op(e0,e3)) )
& ( op(op(e0,e1),e0) = op(e0,op(e1,e0)) )
& ( op(op(e0,e1),e1) = op(e0,op(e1,e1)) )
& ( op(op(e0,e1),e2) = op(e0,op(e1,e2)) )
& ( op(op(e0,e1),e3) = op(e0,op(e1,e3)) )
& ( op(op(e0,e2),e0) = op(e0,op(e2,e0)) )
& ( op(op(e0,e2),e1) = op(e0,op(e2,e1)) )
& ( op(op(e0,e2),e2) = op(e0,op(e2,e2)) )
& ( op(op(e0,e2),e3) = op(e0,op(e2,e3)) )
& ( op(op(e0,e3),e0) = op(e0,op(e3,e0)) )
& ( op(op(e0,e3),e1) = op(e0,op(e3,e1)) )
& ( op(op(e0,e3),e2) = op(e0,op(e3,e2)) )
& ( op(op(e0,e3),e3) = op(e0,op(e3,e3)) )
& ( op(op(e1,e0),e0) = op(e1,op(e0,e0)) )
& ( op(op(e1,e0),e1) = op(e1,op(e0,e1)) )
& ( op(op(e1,e0),e2) = op(e1,op(e0,e2)) )
& ( op(op(e1,e0),e3) = op(e1,op(e0,e3)) )
& ( op(op(e1,e1),e0) = op(e1,op(e1,e0)) )
& ( op(op(e1,e1),e1) = op(e1,op(e1,e1)) )
& ( op(op(e1,e1),e2) = op(e1,op(e1,e2)) )
& ( op(op(e1,e1),e3) = op(e1,op(e1,e3)) )
& ( op(op(e1,e2),e0) = op(e1,op(e2,e0)) )
& ( op(op(e1,e2),e1) = op(e1,op(e2,e1)) )
& ( op(op(e1,e2),e2) = op(e1,op(e2,e2)) )
& ( op(op(e1,e2),e3) = op(e1,op(e2,e3)) )
& ( op(op(e1,e3),e0) = op(e1,op(e3,e0)) )
& ( op(op(e1,e3),e1) = op(e1,op(e3,e1)) )
& ( op(op(e1,e3),e2) = op(e1,op(e3,e2)) )
& ( op(op(e1,e3),e3) = op(e1,op(e3,e3)) )
& ( op(op(e2,e0),e0) = op(e2,op(e0,e0)) )
& ( op(op(e2,e0),e1) = op(e2,op(e0,e1)) )
& ( op(op(e2,e0),e2) = op(e2,op(e0,e2)) )
& ( op(op(e2,e0),e3) = op(e2,op(e0,e3)) )
& ( op(op(e2,e1),e0) = op(e2,op(e1,e0)) )
& ( op(op(e2,e1),e1) = op(e2,op(e1,e1)) )
& ( op(op(e2,e1),e2) = op(e2,op(e1,e2)) )
& ( op(op(e2,e1),e3) = op(e2,op(e1,e3)) )
& ( op(op(e2,e2),e0) = op(e2,op(e2,e0)) )
& ( op(op(e2,e2),e1) = op(e2,op(e2,e1)) )
& ( op(op(e2,e2),e2) = op(e2,op(e2,e2)) )
& ( op(op(e2,e2),e3) = op(e2,op(e2,e3)) )
& ( op(op(e2,e3),e0) = op(e2,op(e3,e0)) )
& ( op(op(e2,e3),e1) = op(e2,op(e3,e1)) )
& ( op(op(e2,e3),e2) = op(e2,op(e3,e2)) )
& ( op(op(e2,e3),e3) = op(e2,op(e3,e3)) )
& ( op(op(e3,e0),e0) = op(e3,op(e0,e0)) )
& ( op(op(e3,e0),e1) = op(e3,op(e0,e1)) )
& ( op(op(e3,e0),e2) = op(e3,op(e0,e2)) )
& ( op(op(e3,e0),e3) = op(e3,op(e0,e3)) )
& ( op(op(e3,e1),e0) = op(e3,op(e1,e0)) )
& ( op(op(e3,e1),e1) = op(e3,op(e1,e1)) )
& ( op(op(e3,e1),e2) = op(e3,op(e1,e2)) )
& ( op(op(e3,e1),e3) = op(e3,op(e1,e3)) )
& ( op(op(e3,e2),e0) = op(e3,op(e2,e0)) )
& ( op(op(e3,e2),e1) = op(e3,op(e2,e1)) )
& ( op(op(e3,e2),e2) = op(e3,op(e2,e2)) )
& ( op(op(e3,e2),e3) = op(e3,op(e2,e3)) )
& ( op(op(e3,e3),e0) = op(e3,op(e3,e0)) )
& ( op(op(e3,e3),e1) = op(e3,op(e3,e1)) )
& ( op(op(e3,e3),e2) = op(e3,op(e3,e2)) )
& ( op(op(e3,e3),e3) = op(e3,op(e3,e3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
tff(f_648,axiom,
~ ( ( e0 = op(e2,e2) )
& ( e3 = op(e1,e2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
tff(f_644,axiom,
~ ( ( e0 = op(e1,e1) )
& ( e2 = op(e3,e1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
tff(c_354,plain,
e3 != e2,
inference(cnfTransformation,[status(thm)],[f_597]) ).
tff(c_364,plain,
e1 != e0,
inference(cnfTransformation,[status(thm)],[f_597]) ).
tff(c_356,plain,
e3 != e1,
inference(cnfTransformation,[status(thm)],[f_597]) ).
tff(c_358,plain,
e2 != e1,
inference(cnfTransformation,[status(thm)],[f_597]) ).
tff(c_362,plain,
e2 != e0,
inference(cnfTransformation,[status(thm)],[f_597]) ).
tff(c_360,plain,
e3 != e0,
inference(cnfTransformation,[status(thm)],[f_597]) ).
tff(c_892,plain,
( ( op(e3,e2) != e0 )
| ( op(e2,e2) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_660]) ).
tff(c_31772,plain,
op(e2,e2) != e1,
inference(splitLeft,[status(thm)],[c_892]) ).
tff(c_894,plain,
( ( op(e0,e3) != e2 )
| ( op(e3,e3) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_664]) ).
tff(c_22487,plain,
op(e3,e3) != e1,
inference(splitLeft,[status(thm)],[c_894]) ).
tff(c_922,plain,
( ( op(e0,e1) != e2 )
| ( op(e1,e1) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_720]) ).
tff(c_22491,plain,
op(e1,e1) != e3,
inference(splitLeft,[status(thm)],[c_922]) ).
tff(c_906,plain,
( ( op(e0,e3) != e1 )
| ( op(e3,e3) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_688]) ).
tff(c_23861,plain,
op(e3,e3) != e2,
inference(splitLeft,[status(thm)],[c_906]) ).
tff(c_236,plain,
( ( inv(e0) = e1 )
| ( inv(e1) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1015,plain,
inv(e1) != e0,
inference(splitLeft,[status(thm)],[c_236]) ).
tff(c_242,plain,
( ( inv(e1) = e0 )
| ( inv(e0) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1016,plain,
inv(e0) != e1,
inference(negUnitSimplification,[status(thm)],[c_1015,c_242]) ).
tff(c_228,plain,
( ( inv(e0) = e2 )
| ( inv(e2) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1012,plain,
inv(e2) != e0,
inference(splitLeft,[status(thm)],[c_228]) ).
tff(c_240,plain,
( ( inv(e2) = e0 )
| ( inv(e0) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1017,plain,
inv(e0) != e2,
inference(negUnitSimplification,[status(thm)],[c_1012,c_240]) ).
tff(c_220,plain,
( ( inv(e0) = e3 )
| ( inv(e3) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1010,plain,
inv(e3) != e0,
inference(splitLeft,[status(thm)],[c_220]) ).
tff(c_238,plain,
( ( inv(e3) = e0 )
| ( inv(e0) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1018,plain,
inv(e0) != e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_238]) ).
tff(c_186,plain,
( ( inv(e0) = e3 )
| ( inv(e0) = e2 )
| ( inv(e0) = e1 )
| ( inv(e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_9394,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_8138,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_1022,plain,
op(e3,e3) != e1,
inference(splitLeft,[status(thm)],[c_894]) ).
tff(c_230,plain,
( ( inv(e3) = e1 )
| ( inv(e1) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1014,plain,
inv(e1) != e3,
inference(splitLeft,[status(thm)],[c_230]) ).
tff(c_218,plain,
( ( inv(e1) = e3 )
| ( inv(e3) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1019,plain,
inv(e3) != e1,
inference(negUnitSimplification,[status(thm)],[c_1014,c_218]) ).
tff(c_216,plain,
( ( inv(e2) = e3 )
| ( inv(e3) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1009,plain,
inv(e3) != e2,
inference(splitLeft,[status(thm)],[c_216]) ).
tff(c_180,plain,
( ( inv(e3) = e3 )
| ( inv(e3) = e2 )
| ( inv(e3) = e1 )
| ( inv(e3) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_7733,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_916,plain,
( ( op(e2,e1) != e0 )
| ( op(e1,e1) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_708]) ).
tff(c_6631,plain,
op(e1,e1) != e3,
inference(splitLeft,[status(thm)],[c_916]) ).
tff(c_226,plain,
( ( inv(e1) = e2 )
| ( inv(e2) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1011,plain,
inv(e2) != e1,
inference(splitLeft,[status(thm)],[c_226]) ).
tff(c_232,plain,
( ( inv(e2) = e1 )
| ( inv(e1) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1013,plain,
inv(e1) != e2,
inference(negUnitSimplification,[status(thm)],[c_1011,c_232]) ).
tff(c_184,plain,
( ( inv(e1) = e3 )
| ( inv(e1) = e2 )
| ( inv(e1) = e1 )
| ( inv(e1) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_7352,plain,
inv(e1) = e1,
inference(negUnitSimplification,[status(thm)],[c_1015,c_1013,c_1014,c_184]) ).
tff(c_910,plain,
( ( op(e0,e1) != e3 )
| ( op(e1,e1) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_696]) ).
tff(c_1023,plain,
op(e1,e1) != e2,
inference(splitLeft,[status(thm)],[c_910]) ).
tff(c_6607,plain,
inv(e1) = e1,
inference(negUnitSimplification,[status(thm)],[c_1015,c_1013,c_1014,c_184]) ).
tff(c_6238,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_4630,plain,
op(e3,e3) != e2,
inference(splitLeft,[status(thm)],[c_906]) ).
tff(c_5777,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_5401,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_912,plain,
( ( op(e1,e0) != e3 )
| ( op(e0,e0) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_700]) ).
tff(c_1026,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_912]) ).
tff(c_4605,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_896,plain,
( ( op(e3,e0) != e2 )
| ( op(e0,e0) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_668]) ).
tff(c_1021,plain,
op(e0,e0) != e1,
inference(splitLeft,[status(thm)],[c_896]) ).
tff(c_4236,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_2766,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_2120,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_920,plain,
( ( op(e2,e0) != e1 )
| ( op(e0,e0) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_716]) ).
tff(c_1025,plain,
op(e0,e0) != e3,
inference(splitLeft,[status(thm)],[c_920]) ).
tff(c_1754,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_878,plain,
( ( op(e2,e3) != e1 )
| ( op(e3,e3) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_632]) ).
tff(c_1028,plain,
op(e3,e3) != e0,
inference(splitLeft,[status(thm)],[c_878]) ).
tff(c_1388,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_162,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_1031,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_188,plain,
op(inv(e3),e3) = unit,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_1038,plain,
op(inv(e3),e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_1031,c_188]) ).
tff(c_1389,plain,
op(e3,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_1388,c_1038]) ).
tff(c_1398,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1028,c_1389]) ).
tff(c_1399,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_1401,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_1399]) ).
tff(c_200,plain,
op(inv(e0),e0) = unit,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_1406,plain,
op(inv(e0),e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_1401,c_200]) ).
tff(c_1755,plain,
op(e0,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_1754,c_1406]) ).
tff(c_1764,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1025,c_1755]) ).
tff(c_1765,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_1399]) ).
tff(c_1767,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_1765]) ).
tff(c_202,plain,
op(e0,inv(e0)) = unit,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_1777,plain,
op(e0,inv(e0)) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_1767,c_202]) ).
tff(c_2121,plain,
op(e0,e0) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_2120,c_1777]) ).
tff(c_2130,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1021,c_2121]) ).
tff(c_2131,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_1765]) ).
tff(c_2143,plain,
op(e0,inv(e0)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2131,c_202]) ).
tff(c_2767,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2766,c_2143]) ).
tff(c_2776,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1026,c_2767]) ).
tff(c_2778,plain,
op(e3,e3) = e0,
inference(splitRight,[status(thm)],[c_878]) ).
tff(c_312,plain,
op(e3,e3) != op(e0,e3),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_2781,plain,
op(e0,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2778,c_312]) ).
tff(c_306,plain,
op(e3,e3) != op(e2,e3),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_2782,plain,
op(e2,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2778,c_306]) ).
tff(c_2777,plain,
op(e2,e3) != e1,
inference(splitRight,[status(thm)],[c_878]) ).
tff(c_2792,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_168,plain,
op(e2,unit) = e2,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_2805,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2792,c_168]) ).
tff(c_276,plain,
op(e2,e3) != op(e2,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_3157,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_2805,c_276]) ).
tff(c_166,plain,
op(unit,e3) = e3,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_2807,plain,
op(e0,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_2792,c_166]) ).
tff(c_314,plain,
op(e2,e3) != op(e0,e3),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_2849,plain,
op(e2,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_2807,c_314]) ).
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_3855,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2782,c_2777,c_3157,c_2849,c_10]) ).
tff(c_3856,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_3858,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_3856]) ).
tff(c_176,plain,
op(e0,unit) = e0,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_3868,plain,
op(e0,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_3858,c_176]) ).
tff(c_3878,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2781,c_3868]) ).
tff(c_3879,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_3856]) ).
tff(c_3881,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_3879]) ).
tff(c_3891,plain,
op(e0,inv(e0)) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_3881,c_202]) ).
tff(c_4237,plain,
op(e0,e0) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_4236,c_3891]) ).
tff(c_4246,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1021,c_4237]) ).
tff(c_4247,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_3879]) ).
tff(c_4254,plain,
op(inv(e0),e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_4247,c_200]) ).
tff(c_4606,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_4605,c_4254]) ).
tff(c_4615,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1026,c_4606]) ).
tff(c_4617,plain,
op(e0,e0) = e2,
inference(splitRight,[status(thm)],[c_912]) ).
tff(c_5018,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_350,plain,
op(e2,e0) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_4624,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_4617,c_350]) ).
tff(c_4635,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_4648,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_4635,c_168]) ).
tff(c_4654,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4624,c_4648]) ).
tff(c_4655,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_4657,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_4655]) ).
tff(c_4666,plain,
op(e0,inv(e0)) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_4657,c_202]) ).
tff(c_5019,plain,
op(e0,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_5018,c_4666]) ).
tff(c_5027,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_4617,c_5019]) ).
tff(c_5029,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_5027]) ).
tff(c_5030,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_4655]) ).
tff(c_5032,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_5030]) ).
tff(c_5041,plain,
op(inv(e3),e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_5032,c_188]) ).
tff(c_5402,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_5401,c_5041]) ).
tff(c_5411,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1022,c_5402]) ).
tff(c_5412,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_5030]) ).
tff(c_5425,plain,
op(inv(e3),e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_5412,c_188]) ).
tff(c_5778,plain,
op(e3,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_5777,c_5425]) ).
tff(c_5786,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4630,c_5778]) ).
tff(c_5788,plain,
op(e3,e3) = e2,
inference(splitRight,[status(thm)],[c_906]) ).
tff(c_5791,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_5788,c_306]) ).
tff(c_5809,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_5822,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_5809,c_168]) ).
tff(c_5828,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4624,c_5822]) ).
tff(c_5829,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_5831,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_5829]) ).
tff(c_5845,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_5831,c_168]) ).
tff(c_5851,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5791,c_5845]) ).
tff(c_5852,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_5829]) ).
tff(c_5855,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_5852]) ).
tff(c_190,plain,
op(e3,inv(e3)) = unit,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_5863,plain,
op(e3,inv(e3)) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_5855,c_190]) ).
tff(c_6239,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_6238,c_5863]) ).
tff(c_6251,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_6239,c_5788]) ).
tff(c_6253,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_6251]) ).
tff(c_6254,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_5852]) ).
tff(c_198,plain,
op(e1,inv(e1)) = unit,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_6259,plain,
op(e1,inv(e1)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_6254,c_198]) ).
tff(c_6608,plain,
op(e1,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_6607,c_6259]) ).
tff(c_6616,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1023,c_6608]) ).
tff(c_6618,plain,
op(e0,e0) = e3,
inference(splitRight,[status(thm)],[c_920]) ).
tff(c_300,plain,
op(e0,e3) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_6622,plain,
op(e0,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_6618,c_300]) ).
tff(c_6636,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_6652,plain,
op(e0,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_6636,c_166]) ).
tff(c_6656,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6622,c_6652]) ).
tff(c_6657,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_6659,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_6657]) ).
tff(c_196,plain,
op(inv(e1),e1) = unit,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_6661,plain,
op(inv(e1),e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_6659,c_196]) ).
tff(c_7353,plain,
op(e1,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_7352,c_6661]) ).
tff(c_7361,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6631,c_7353]) ).
tff(c_7362,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_6657]) ).
tff(c_7364,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_7362]) ).
tff(c_7373,plain,
op(inv(e3),e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_7364,c_188]) ).
tff(c_7734,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_7733,c_7373]) ).
tff(c_7743,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1022,c_7734]) ).
tff(c_7744,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_7362]) ).
tff(c_7756,plain,
op(e0,inv(e0)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_7744,c_202]) ).
tff(c_8139,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_8138,c_7756]) ).
tff(c_8151,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_8139,c_6618]) ).
tff(c_8153,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_8151]) ).
tff(c_8155,plain,
op(e1,e1) = e3,
inference(splitRight,[status(thm)],[c_916]) ).
tff(c_284,plain,
op(e1,e3) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_8158,plain,
op(e1,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_8155,c_284]) ).
tff(c_914,plain,
( ( op(e1,e2) != e0 )
| ( op(e2,e2) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_704]) ).
tff(c_8598,plain,
op(e2,e2) != e3,
inference(splitLeft,[status(thm)],[c_914]) ).
tff(c_918,plain,
( ( op(e0,e2) != e1 )
| ( op(e2,e2) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_712]) ).
tff(c_8248,plain,
op(e2,e2) != e3,
inference(splitLeft,[status(thm)],[c_918]) ).
tff(c_222,plain,
( ( inv(e3) = e2 )
| ( inv(e2) != e3 ) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_1020,plain,
inv(e2) != e3,
inference(negUnitSimplification,[status(thm)],[c_1009,c_222]) ).
tff(c_182,plain,
( ( inv(e2) = e3 )
| ( inv(e2) = e2 )
| ( inv(e2) = e1 )
| ( inv(e2) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_8538,plain,
inv(e2) = e2,
inference(negUnitSimplification,[status(thm)],[c_1012,c_1011,c_1020,c_182]) ).
tff(c_8171,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_8186,plain,
op(e0,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_8171,c_166]) ).
tff(c_8190,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6622,c_8186]) ).
tff(c_8191,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_8193,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_8191]) ).
tff(c_192,plain,
op(inv(e2),e2) = unit,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_8199,plain,
op(inv(e2),e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_8193,c_192]) ).
tff(c_8539,plain,
op(e2,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_8538,c_8199]) ).
tff(c_8548,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8248,c_8539]) ).
tff(c_8550,plain,
op(e2,e2) = e3,
inference(splitRight,[status(thm)],[c_918]) ).
tff(c_8600,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8598,c_8550]) ).
tff(c_8601,plain,
op(e1,e2) != e0,
inference(splitRight,[status(thm)],[c_914]) ).
tff(c_172,plain,
op(e1,unit) = e1,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_8206,plain,
op(e1,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_8193,c_172]) ).
tff(c_282,plain,
op(e1,e3) != op(e1,e2),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_8564,plain,
op(e1,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_8206,c_282]) ).
tff(c_170,plain,
op(unit,e2) = e2,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_8208,plain,
op(e3,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_8193,c_170]) ).
tff(c_320,plain,
op(e3,e2) != op(e1,e2),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_8242,plain,
op(e1,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_8208,c_320]) ).
tff(c_286,plain,
op(e1,e2) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_8159,plain,
op(e1,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_8155,c_286]) ).
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_8939,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8601,c_8564,c_8242,c_8159,c_20]) ).
tff(c_8940,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_8191]) ).
tff(c_8942,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_8940]) ).
tff(c_8959,plain,
op(e1,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_8942,c_166]) ).
tff(c_8963,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8158,c_8959]) ).
tff(c_8964,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_8940]) ).
tff(c_8975,plain,
op(e0,inv(e0)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_8964,c_202]) ).
tff(c_9395,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_9394,c_8975]) ).
tff(c_9407,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_9395,c_6618]) ).
tff(c_9409,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_9407]) ).
tff(c_9411,plain,
op(e1,e1) = e2,
inference(splitRight,[status(thm)],[c_910]) ).
tff(c_334,plain,
op(e2,e1) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_9415,plain,
op(e2,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_9411,c_334]) ).
tff(c_11464,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_11059,plain,
inv(e1) = e1,
inference(negUnitSimplification,[status(thm)],[c_1015,c_1013,c_1014,c_184]) ).
tff(c_9424,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_912]) ).
tff(c_10605,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_9425,plain,
op(e0,e0) != e3,
inference(splitLeft,[status(thm)],[c_920]) ).
tff(c_10218,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_9423,plain,
op(e3,e3) != e0,
inference(splitLeft,[status(thm)],[c_878]) ).
tff(c_9816,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_9427,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_9434,plain,
op(inv(e3),e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_9427,c_188]) ).
tff(c_9817,plain,
op(e3,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_9816,c_9434]) ).
tff(c_9826,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9423,c_9817]) ).
tff(c_9827,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_9829,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_9827]) ).
tff(c_9833,plain,
op(inv(e0),e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_9829,c_200]) ).
tff(c_10219,plain,
op(e0,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_10218,c_9833]) ).
tff(c_10228,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9425,c_10219]) ).
tff(c_10229,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_9827]) ).
tff(c_10231,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_10229]) ).
tff(c_10246,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_10231,c_168]) ).
tff(c_10252,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9415,c_10246]) ).
tff(c_10253,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_10229]) ).
tff(c_10265,plain,
op(e0,inv(e0)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_10253,c_202]) ).
tff(c_10606,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_10605,c_10265]) ).
tff(c_10615,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9424,c_10606]) ).
tff(c_10617,plain,
op(e0,e0) = e3,
inference(splitRight,[status(thm)],[c_920]) ).
tff(c_10622,plain,
op(e0,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_10617,c_300]) ).
tff(c_10638,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_10653,plain,
op(e0,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_10638,c_166]) ).
tff(c_10657,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10622,c_10653]) ).
tff(c_10658,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_10660,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_10658]) ).
tff(c_10662,plain,
op(inv(e1),e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_10660,c_196]) ).
tff(c_11060,plain,
op(e1,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_11059,c_10662]) ).
tff(c_11067,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_9411,c_11060]) ).
tff(c_11069,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_11067]) ).
tff(c_11070,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_10658]) ).
tff(c_11074,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_11070]) ).
tff(c_11089,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_11074,c_168]) ).
tff(c_11095,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9415,c_11089]) ).
tff(c_11096,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_11070]) ).
tff(c_11108,plain,
op(e0,inv(e0)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_11096,c_202]) ).
tff(c_11465,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_11464,c_11108]) ).
tff(c_11477,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_11465,c_10617]) ).
tff(c_11479,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_11477]) ).
tff(c_11481,plain,
op(e0,e0) = e2,
inference(splitRight,[status(thm)],[c_912]) ).
tff(c_11913,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_11487,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_11481,c_350]) ).
tff(c_11495,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_11508,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_11495,c_168]) ).
tff(c_11514,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11487,c_11508]) ).
tff(c_11515,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_11517,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_11515]) ).
tff(c_11526,plain,
op(e0,inv(e0)) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_11517,c_202]) ).
tff(c_11914,plain,
op(e0,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_11913,c_11526]) ).
tff(c_11922,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_11481,c_11914]) ).
tff(c_11924,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_11922]) ).
tff(c_11925,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_11515]) ).
tff(c_11927,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_11925]) ).
tff(c_11942,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_11927,c_168]) ).
tff(c_11948,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9415,c_11942]) ).
tff(c_11949,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_11925]) ).
tff(c_11962,plain,
op(e0,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_11949,c_176]) ).
tff(c_294,plain,
op(e0,e3) != op(e0,e2),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_11992,plain,
op(e0,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_11962,c_294]) ).
tff(c_902,plain,
( ( op(e1,e3) != e0 )
| ( op(e3,e3) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_680]) ).
tff(c_12024,plain,
op(e3,e3) != e2,
inference(splitLeft,[status(thm)],[c_902]) ).
tff(c_12329,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_11960,plain,
op(inv(e3),e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_11949,c_188]) ).
tff(c_12330,plain,
op(e3,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_12329,c_11960]) ).
tff(c_12337,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12024,c_12330]) ).
tff(c_12339,plain,
op(e3,e3) = e2,
inference(splitRight,[status(thm)],[c_902]) ).
tff(c_12398,plain,
op(e0,e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_12339,c_906]) ).
tff(c_11485,plain,
op(e0,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_11481,c_300]) ).
tff(c_11968,plain,
op(e2,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_11949,c_166]) ).
tff(c_12369,plain,
op(e0,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_11968,c_314]) ).
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_12672,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11992,c_12398,c_11485,c_12369,c_26]) ).
tff(c_12674,plain,
op(e3,e3) = e0,
inference(splitRight,[status(thm)],[c_878]) ).
tff(c_14308,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_13836,plain,
op(e0,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_12674,c_312]) ).
tff(c_12675,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_912]) ).
tff(c_13822,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_12677,plain,
op(e0,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_12674,c_312]) ).
tff(c_13385,plain,
inv(e1) = e1,
inference(negUnitSimplification,[status(thm)],[c_1015,c_1013,c_1014,c_184]) ).
tff(c_12688,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_12690,plain,
op(e1,inv(e1)) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_12688,c_198]) ).
tff(c_13386,plain,
op(e1,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_13385,c_12690]) ).
tff(c_13396,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_13386,c_9411]) ).
tff(c_13398,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_13396]) ).
tff(c_13399,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_13402,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_13399]) ).
tff(c_13412,plain,
op(e0,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_13402,c_176]) ).
tff(c_13422,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12677,c_13412]) ).
tff(c_13423,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_13399]) ).
tff(c_13425,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_13423]) ).
tff(c_13440,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_13425,c_168]) ).
tff(c_13446,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9415,c_13440]) ).
tff(c_13447,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_13423]) ).
tff(c_13453,plain,
op(inv(e0),e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_13447,c_200]) ).
tff(c_13823,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_13822,c_13453]) ).
tff(c_13832,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12675,c_13823]) ).
tff(c_13834,plain,
op(e0,e0) = e2,
inference(splitRight,[status(thm)],[c_912]) ).
tff(c_13851,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_13834,c_350]) ).
tff(c_13868,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_13881,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_13868,c_168]) ).
tff(c_13887,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13851,c_13881]) ).
tff(c_13888,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_13892,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_13888]) ).
tff(c_13902,plain,
op(e0,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_13892,c_176]) ).
tff(c_13912,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13836,c_13902]) ).
tff(c_13913,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_13888]) ).
tff(c_13915,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_13913]) ).
tff(c_13930,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_13915,c_168]) ).
tff(c_13936,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9415,c_13930]) ).
tff(c_13937,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_13913]) ).
tff(c_13947,plain,
op(inv(e3),e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_13937,c_188]) ).
tff(c_14309,plain,
op(e3,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_14308,c_13947]) ).
tff(c_14315,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_12674,c_14309]) ).
tff(c_14317,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_14315]) ).
tff(c_14319,plain,
op(e3,e3) = e1,
inference(splitRight,[status(thm)],[c_894]) ).
tff(c_15776,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_15394,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_260,plain,
op(e3,e3) != op(e3,e1),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_14323,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_14319,c_260]) ).
tff(c_14994,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_14330,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_14336,plain,
op(e3,inv(e3)) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_14330,c_190]) ).
tff(c_14995,plain,
op(e3,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_14994,c_14336]) ).
tff(c_15007,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_14995,c_14319]) ).
tff(c_15009,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_15007]) ).
tff(c_15010,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_15013,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_15010]) ).
tff(c_174,plain,
op(unit,e1) = e1,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_15025,plain,
op(e3,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_15013,c_174]) ).
tff(c_15033,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14323,c_15025]) ).
tff(c_15034,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_15010]) ).
tff(c_15036,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_15034]) ).
tff(c_15046,plain,
op(e0,inv(e0)) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_15036,c_202]) ).
tff(c_15395,plain,
op(e0,e0) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_15394,c_15046]) ).
tff(c_15404,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1021,c_15395]) ).
tff(c_15405,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_15034]) ).
tff(c_15416,plain,
op(e3,inv(e3)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_15405,c_190]) ).
tff(c_15777,plain,
op(e3,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_15776,c_15416]) ).
tff(c_15785,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_14319,c_15777]) ).
tff(c_15787,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_15785]) ).
tff(c_15789,plain,
op(e0,e0) = e1,
inference(splitRight,[status(thm)],[c_896]) ).
tff(c_16976,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_890,plain,
( ( op(e2,e3) != e0 )
| ( op(e3,e3) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_656]) ).
tff(c_15804,plain,
op(e3,e3) != e1,
inference(splitLeft,[status(thm)],[c_890]) ).
tff(c_16581,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_16211,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_304,plain,
op(e0,e1) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_15790,plain,
op(e0,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_15789,c_304]) ).
tff(c_15805,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_15816,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_15805,c_174]) ).
tff(c_15824,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15790,c_15816]) ).
tff(c_15825,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_15827,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_15825]) ).
tff(c_15836,plain,
op(e0,inv(e0)) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_15827,c_202]) ).
tff(c_16212,plain,
op(e0,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_16211,c_15836]) ).
tff(c_16220,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_15789,c_16212]) ).
tff(c_16222,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_16220]) ).
tff(c_16223,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_15825]) ).
tff(c_16225,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_16223]) ).
tff(c_16233,plain,
op(e3,inv(e3)) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_16225,c_190]) ).
tff(c_16582,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_16581,c_16233]) ).
tff(c_16591,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15804,c_16582]) ).
tff(c_16592,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_16223]) ).
tff(c_16599,plain,
op(inv(e0),e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_16592,c_200]) ).
tff(c_16977,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_16976,c_16599]) ).
tff(c_16985,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_15789,c_16977]) ).
tff(c_16987,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_16985]) ).
tff(c_16989,plain,
op(e3,e3) = e1,
inference(splitRight,[status(thm)],[c_890]) ).
tff(c_17808,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_898,plain,
( ( op(e0,e2) != e3 )
| ( op(e2,e2) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_672]) ).
tff(c_15800,plain,
op(e2,e2) != e1,
inference(splitLeft,[status(thm)],[c_898]) ).
tff(c_17423,plain,
inv(e2) = e2,
inference(negUnitSimplification,[status(thm)],[c_1012,c_1011,c_1020,c_182]) ).
tff(c_16993,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_16989,c_260]) ).
tff(c_17008,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_17019,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_17008,c_174]) ).
tff(c_17027,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15790,c_17019]) ).
tff(c_17028,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_17030,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_17028]) ).
tff(c_17042,plain,
op(e3,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_17030,c_174]) ).
tff(c_17050,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16993,c_17042]) ).
tff(c_17051,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_17028]) ).
tff(c_17053,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_17051]) ).
tff(c_17060,plain,
op(inv(e2),e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_17053,c_192]) ).
tff(c_17424,plain,
op(e2,e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_17423,c_17060]) ).
tff(c_17431,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15800,c_17424]) ).
tff(c_17432,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_17051]) ).
tff(c_17442,plain,
op(e3,inv(e3)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_17432,c_190]) ).
tff(c_17809,plain,
op(e3,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_17808,c_17442]) ).
tff(c_17817,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_16989,c_17809]) ).
tff(c_17819,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_17817]) ).
tff(c_17821,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_898]) ).
tff(c_274,plain,
op(e2,e2) != op(e2,e1),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_17823,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_17821,c_274]) ).
tff(c_17833,plain,
op(e3,e3) != e1,
inference(splitLeft,[status(thm)],[c_890]) ).
tff(c_18627,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_1019,c_1009,c_180]) ).
tff(c_18247,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_1016,c_1017,c_1018,c_186]) ).
tff(c_17849,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_17860,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_17849,c_174]) ).
tff(c_17868,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15790,c_17860]) ).
tff(c_17869,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_17872,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_17869]) ).
tff(c_17876,plain,
op(inv(e0),e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_17872,c_200]) ).
tff(c_18248,plain,
op(e0,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_18247,c_17876]) ).
tff(c_18256,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_15789,c_18248]) ).
tff(c_18258,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_18256]) ).
tff(c_18259,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_17869]) ).
tff(c_18261,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_18259]) ).
tff(c_18270,plain,
op(inv(e3),e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_18261,c_188]) ).
tff(c_18628,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_18627,c_18270]) ).
tff(c_18635,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17833,c_18628]) ).
tff(c_18636,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_18259]) ).
tff(c_18651,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_18636,c_174]) ).
tff(c_18659,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17823,c_18651]) ).
tff(c_18661,plain,
op(e3,e3) = e1,
inference(splitRight,[status(thm)],[c_890]) ).
tff(c_18665,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_18661,c_260]) ).
tff(c_18691,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_18703,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_18691,c_174]) ).
tff(c_18711,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15790,c_18703]) ).
tff(c_18712,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_18714,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_18712]) ).
tff(c_18726,plain,
op(e3,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_18714,c_174]) ).
tff(c_18734,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18665,c_18726]) ).
tff(c_18735,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_18712]) ).
tff(c_18737,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_18735]) ).
tff(c_178,plain,
op(unit,e0) = e0,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_18749,plain,
op(e1,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_18737,c_178]) ).
tff(c_346,plain,
op(e2,e0) != op(e1,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_18788,plain,
op(e2,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_18749,c_346]) ).
tff(c_15794,plain,
op(e2,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_15789,c_350]) ).
tff(c_18752,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_18737,c_168]) ).
tff(c_280,plain,
op(e2,e1) != op(e2,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_18845,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_18752,c_280]) ).
tff(c_900,plain,
( ( op(e2,e0) != e3 )
| ( op(e0,e0) != e1 ) ),
inference(cnfTransformation,[status(thm)],[f_676]) ).
tff(c_18689,plain,
op(e2,e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_15789,c_900]) ).
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_19201,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18788,c_15794,c_18845,c_18689,c_16]) ).
tff(c_19202,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_18735]) ).
tff(c_19216,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_19202,c_174]) ).
tff(c_19224,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17823,c_19216]) ).
tff(c_19226,plain,
inv(e1) = e0,
inference(splitRight,[status(thm)],[c_236]) ).
tff(c_19239,plain,
op(e0,e1) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_19226,c_196]) ).
tff(c_19283,plain,
( ( unit != e3 )
| ( op(e1,e1) != e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_19239,c_910]) ).
tff(c_19284,plain,
op(e1,e1) != e2,
inference(splitLeft,[status(thm)],[c_19283]) ).
tff(c_19296,plain,
op(e3,e3) != e2,
inference(splitLeft,[status(thm)],[c_902]) ).
tff(c_19225,plain,
inv(e0) = e1,
inference(splitRight,[status(thm)],[c_236]) ).
tff(c_252,plain,
inv(e3) != inv(e0),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_19231,plain,
inv(e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_19225,c_252]) ).
tff(c_20058,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_19231,c_1009,c_180]) ).
tff(c_19295,plain,
op(e2,e2) != e3,
inference(splitLeft,[status(thm)],[c_914]) ).
tff(c_19278,plain,
inv(e2) != e3,
inference(negUnitSimplification,[status(thm)],[c_1009,c_222]) ).
tff(c_19675,plain,
inv(e2) = e2,
inference(negUnitSimplification,[status(thm)],[c_1012,c_1011,c_19278,c_182]) ).
tff(c_19297,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_204,plain,
inv(unit) = unit,
inference(cnfTransformation,[status(thm)],[f_350]) ).
tff(c_19322,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_19297,c_19297,c_204]) ).
tff(c_19327,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_19322,c_19225]) ).
tff(c_19329,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_19327]) ).
tff(c_19330,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_19333,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_19330]) ).
tff(c_194,plain,
op(e2,inv(e2)) = unit,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_19347,plain,
op(e2,inv(e2)) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_19333,c_194]) ).
tff(c_19676,plain,
op(e2,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_19675,c_19347]) ).
tff(c_19683,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19295,c_19676]) ).
tff(c_19684,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_19330]) ).
tff(c_19686,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_19684]) ).
tff(c_19713,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_19686,c_19686,c_204]) ).
tff(c_19714,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_19226,c_19713]) ).
tff(c_19716,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_19714]) ).
tff(c_19717,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_19684]) ).
tff(c_19736,plain,
op(e3,inv(e3)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_19717,c_190]) ).
tff(c_20059,plain,
op(e3,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_20058,c_19736]) ).
tff(c_20066,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19296,c_20059]) ).
tff(c_20068,plain,
op(e3,e3) = e2,
inference(splitRight,[status(thm)],[c_902]) ).
tff(c_20071,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_20068,c_306]) ).
tff(c_20083,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_20108,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_20083,c_20083,c_204]) ).
tff(c_20113,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_20108,c_19225]) ).
tff(c_20115,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_20113]) ).
tff(c_20116,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_20118,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_20116]) ).
tff(c_20141,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_20118,c_168]) ).
tff(c_20147,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20071,c_20141]) ).
tff(c_20148,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_20116]) ).
tff(c_20150,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_20148]) ).
tff(c_20177,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_20150,c_20150,c_204]) ).
tff(c_20178,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_19226,c_20177]) ).
tff(c_20180,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_20178]) ).
tff(c_20181,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_20148]) ).
tff(c_20204,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_20181,c_174]) ).
tff(c_20277,plain,
op(e1,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_20204,c_334]) ).
tff(c_20203,plain,
op(e2,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_20181,c_178]) ).
tff(c_20242,plain,
op(e0,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_20203,c_350]) ).
tff(c_20207,plain,
op(e2,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_20181,c_170]) ).
tff(c_580,plain,
( ( op(e0,e0) = e0 )
| ( op(e1,e1) = e1 )
| ( op(e1,e1) = e2 )
| ( op(e2,e2) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_20533,plain,
( ( op(e0,e0) = e0 )
| ( op(e1,e1) = e1 )
| ( op(e1,e1) = e2 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_20207,c_580]) ).
tff(c_20534,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_19284,c_20277,c_20242,c_20533]) ).
tff(c_20536,plain,
op(e2,e2) = e3,
inference(splitRight,[status(thm)],[c_914]) ).
tff(c_270,plain,
op(e2,e3) != op(e2,e2),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_20539,plain,
op(e2,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_20536,c_270]) ).
tff(c_19287,plain,
op(e1,e1) != e3,
inference(splitLeft,[status(thm)],[c_916]) ).
tff(c_908,plain,
( ( op(e3,e0) != e1 )
| ( op(e0,e0) != e2 ) ),
inference(cnfTransformation,[status(thm)],[f_692]) ).
tff(c_19288,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_908]) ).
tff(c_19285,plain,
op(e0,e0) != e1,
inference(splitLeft,[status(thm)],[c_896]) ).
tff(c_20553,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_20578,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_20553,c_20553,c_204]) ).
tff(c_20583,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_20578,c_19225]) ).
tff(c_20585,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_20583]) ).
tff(c_20586,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_20588,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_20586]) ).
tff(c_20612,plain,
op(e3,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_20588,c_166]) ).
tff(c_742,plain,
( ( op(e3,e3) = e0 )
| ( op(e0,e0) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_20945,plain,
( ( e3 = e0 )
| ( op(e0,e0) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_20612,c_742]) ).
tff(c_20946,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19287,c_19288,c_19285,c_360,c_20945]) ).
tff(c_20947,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_20586]) ).
tff(c_20949,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_20947]) ).
tff(c_20976,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_20949,c_20949,c_204]) ).
tff(c_20977,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_19226,c_20976]) ).
tff(c_20979,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_20977]) ).
tff(c_20980,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_20947]) ).
tff(c_21007,plain,
op(e2,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_20980,c_166]) ).
tff(c_21011,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20539,c_21007]) ).
tff(c_21013,plain,
op(e0,e0) = e2,
inference(splitRight,[status(thm)],[c_908]) ).
tff(c_21024,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_21013,c_350]) ).
tff(c_19227,plain,
op(e1,e0) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_19225,c_200]) ).
tff(c_352,plain,
op(e1,e0) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_19252,plain,
op(e0,e0) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_19227,c_352]) ).
tff(c_21022,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_21013,c_19252]) ).
tff(c_21014,plain,
( ( unit != e3 )
| ( op(e0,e0) != e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_19227,c_912]) ).
tff(c_21015,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_21014]) ).
tff(c_21016,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21015,c_21013]) ).
tff(c_21017,plain,
unit != e3,
inference(splitRight,[status(thm)],[c_21014]) ).
tff(c_21036,plain,
( ( unit = e1 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_21022,c_21017,c_162]) ).
tff(c_21037,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_21036]) ).
tff(c_21059,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_21037,c_168]) ).
tff(c_21065,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21024,c_21059]) ).
tff(c_21066,plain,
unit = e1,
inference(splitRight,[status(thm)],[c_21036]) ).
tff(c_21093,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_21066,c_21066,c_204]) ).
tff(c_21094,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_19226,c_21093]) ).
tff(c_21096,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_21094]) ).
tff(c_21098,plain,
op(e1,e1) = e3,
inference(splitRight,[status(thm)],[c_916]) ).
tff(c_21102,plain,
op(e1,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_21098,c_284]) ).
tff(c_21120,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_21098,c_19239,c_922]) ).
tff(c_292,plain,
op(e1,e1) != op(e1,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_19265,plain,
op(e1,e1) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_19227,c_292]) ).
tff(c_21104,plain,
unit != e3,
inference(demodulation,[status(thm),theory(equality)],[c_21098,c_19265]) ).
tff(c_21122,plain,
( ( unit = e1 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_21120,c_21104,c_162]) ).
tff(c_21123,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_21122]) ).
tff(c_21149,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_21123,c_21123,c_204]) ).
tff(c_21154,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_21149,c_19225]) ).
tff(c_21156,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_21154]) ).
tff(c_21157,plain,
unit = e1,
inference(splitRight,[status(thm)],[c_21122]) ).
tff(c_21183,plain,
op(e1,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_21157,c_166]) ).
tff(c_21187,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21102,c_21183]) ).
tff(c_21189,plain,
op(e0,e0) = e1,
inference(splitRight,[status(thm)],[c_896]) ).
tff(c_888,plain,
( ( op(e2,e1) != e3 )
| ( op(e1,e1) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_652]) ).
tff(c_21201,plain,
op(e1,e1) != e0,
inference(splitLeft,[status(thm)],[c_888]) ).
tff(c_21192,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_21189,c_19252]) ).
tff(c_21210,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_21192,c_162]) ).
tff(c_21211,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_21210]) ).
tff(c_21236,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_21211,c_21211,c_204]) ).
tff(c_21241,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_21236,c_19225]) ).
tff(c_21243,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_21241]) ).
tff(c_21244,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_21210]) ).
tff(c_21246,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_21244]) ).
tff(c_21265,plain,
op(e3,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_21246,c_178]) ).
tff(c_21259,plain,
op(e1,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_21246,c_19227]) ).
tff(c_128,plain,
op(op(e1,e0),e0) = op(e1,op(e0,e0)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_21397,plain,
op(e1,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_21265,c_21259,c_21189,c_128]) ).
tff(c_21398,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21201,c_21397]) ).
tff(c_21399,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_21244]) ).
tff(c_21419,plain,
op(e2,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_21399,c_178]) ).
tff(c_21413,plain,
op(e1,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_21399,c_19227]) ).
tff(c_21570,plain,
op(e1,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_21419,c_21413,c_21189,c_128]) ).
tff(c_21571,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21201,c_21570]) ).
tff(c_21573,plain,
op(e1,e1) = e0,
inference(splitRight,[status(thm)],[c_888]) ).
tff(c_21907,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_19231,c_1009,c_180]) ).
tff(c_21580,plain,
unit != e0,
inference(demodulation,[status(thm),theory(equality)],[c_21573,c_19265]) ).
tff(c_21596,plain,
( ( unit = e3 )
| ( unit = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_21580,c_21192,c_162]) ).
tff(c_21597,plain,
unit = e2,
inference(splitLeft,[status(thm)],[c_21596]) ).
tff(c_21612,plain,
op(e3,inv(e3)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_21597,c_190]) ).
tff(c_21908,plain,
op(e3,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_21907,c_21612]) ).
tff(c_21619,plain,
op(e2,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_21597,c_170]) ).
tff(c_848,plain,
( ( op(e2,e2) = e0 )
| ( op(e3,e3) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e0,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_21968,plain,
( ( e2 = e0 )
| ( e2 = e1 )
| ( e2 = e1 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21189,c_21189,c_21908,c_21619,c_848]) ).
tff(c_21969,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_358,c_358,c_362,c_21968]) ).
tff(c_21970,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_21596]) ).
tff(c_164,plain,
op(e3,unit) = e3,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_21995,plain,
op(e3,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_21970,c_164]) ).
tff(c_22273,plain,
inv(e2) = e2,
inference(negUnitSimplification,[status(thm)],[c_1012,c_1011,c_19278,c_182]) ).
tff(c_21984,plain,
op(e2,inv(e2)) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_21970,c_194]) ).
tff(c_22274,plain,
op(e2,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_22273,c_21984]) ).
tff(c_816,plain,
( ( op(e2,e2) = e0 )
| ( op(e3,e3) = e1 )
| ( op(e1,e1) = e2 )
| ( op(e0,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_22336,plain,
( ( e3 = e0 )
| ( e3 = e1 )
| ( e2 = e0 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21189,c_21573,c_21995,c_22274,c_816]) ).
tff(c_22337,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_362,c_356,c_360,c_22336]) ).
tff(c_22339,plain,
op(e1,e1) = e2,
inference(splitRight,[status(thm)],[c_19283]) ).
tff(c_22342,plain,
op(e2,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_22339,c_334]) ).
tff(c_22345,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_22339,c_19265]) ).
tff(c_22338,plain,
unit != e3,
inference(splitRight,[status(thm)],[c_19283]) ).
tff(c_22362,plain,
( ( unit = e1 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_22345,c_22338,c_162]) ).
tff(c_22363,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_22362]) ).
tff(c_22389,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_22363,c_22363,c_204]) ).
tff(c_22394,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_22389,c_19225]) ).
tff(c_22396,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_22394]) ).
tff(c_22397,plain,
unit = e1,
inference(splitRight,[status(thm)],[c_22362]) ).
tff(c_22420,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_22397,c_168]) ).
tff(c_22426,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22342,c_22420]) ).
tff(c_22427,plain,
inv(e3) = e1,
inference(splitRight,[status(thm)],[c_230]) ).
tff(c_22493,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_912]) ).
tff(c_22436,plain,
inv(e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_22427,c_252]) ).
tff(c_22469,plain,
inv(e0) != e2,
inference(negUnitSimplification,[status(thm)],[c_1012,c_240]) ).
tff(c_22428,plain,
inv(e1) = e3,
inference(splitRight,[status(thm)],[c_230]) ).
tff(c_256,plain,
inv(e1) != inv(e0),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_22445,plain,
inv(e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_22428,c_256]) ).
tff(c_23263,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_22436,c_22469,c_22445,c_186]) ).
tff(c_886,plain,
( ( op(e1,e2) != e3 )
| ( op(e2,e2) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_648]) ).
tff(c_22496,plain,
op(e2,e2) != e0,
inference(splitLeft,[status(thm)],[c_886]) ).
tff(c_250,plain,
inv(e2) != inv(e1),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_22446,plain,
inv(e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_22428,c_250]) ).
tff(c_22841,plain,
inv(e2) = e2,
inference(negUnitSimplification,[status(thm)],[c_1012,c_1011,c_22446,c_182]) ).
tff(c_22501,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_22516,plain,
op(inv(e2),e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_22501,c_192]) ).
tff(c_22842,plain,
op(e2,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_22841,c_22516]) ).
tff(c_22849,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22496,c_22842]) ).
tff(c_22850,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_22852,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_22850]) ).
tff(c_22878,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_22852,c_22852,c_204]) ).
tff(c_22879,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_22427,c_22878]) ).
tff(c_22881,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_22879]) ).
tff(c_22882,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_22850]) ).
tff(c_22884,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_22882]) ).
tff(c_22911,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_22884,c_22884,c_204]) ).
tff(c_22917,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_22911,c_22428]) ).
tff(c_22919,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_22917]) ).
tff(c_22920,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_22882]) ).
tff(c_22940,plain,
op(e0,inv(e0)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_22920,c_202]) ).
tff(c_23264,plain,
op(e0,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_23263,c_22940]) ).
tff(c_23271,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22493,c_23264]) ).
tff(c_23273,plain,
op(e2,e2) = e0,
inference(splitRight,[status(thm)],[c_886]) ).
tff(c_326,plain,
op(e2,e2) != op(e0,e2),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_23276,plain,
op(e0,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_23273,c_326]) ).
tff(c_23285,plain,
op(e3,e3) != e2,
inference(splitLeft,[status(thm)],[c_906]) ).
tff(c_22492,plain,
op(e1,e1) != e0,
inference(splitLeft,[status(thm)],[c_888]) ).
tff(c_23294,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_23311,plain,
op(e0,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_23294,c_176]) ).
tff(c_650,plain,
( ( op(e1,e1) = e0 )
| ( op(e0,e0) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_23653,plain,
( ( op(e1,e1) = e0 )
| ( e1 = e0 )
| ( op(e3,e3) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_23311,c_650]) ).
tff(c_23654,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22491,c_23285,c_364,c_22492,c_23653]) ).
tff(c_23655,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_23657,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_23655]) ).
tff(c_23683,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_23657,c_23657,c_204]) ).
tff(c_23684,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_22427,c_23683]) ).
tff(c_23686,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_23684]) ).
tff(c_23687,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_23655]) ).
tff(c_23689,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_23687]) ).
tff(c_23720,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_23689,c_23689,c_204]) ).
tff(c_23725,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_23720,c_22428]) ).
tff(c_23727,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_23725]) ).
tff(c_23728,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_23687]) ).
tff(c_23749,plain,
op(e0,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_23728,c_176]) ).
tff(c_23759,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23276,c_23749]) ).
tff(c_23761,plain,
op(e3,e3) = e2,
inference(splitRight,[status(thm)],[c_906]) ).
tff(c_23765,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_23761,c_306]) ).
tff(c_22443,plain,
op(e1,e3) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_22428,c_198]) ).
tff(c_23777,plain,
unit != e0,
inference(demodulation,[status(thm),theory(equality)],[c_23761,c_22443,c_902]) ).
tff(c_22431,plain,
op(e3,e1) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_22427,c_190]) ).
tff(c_22478,plain,
op(e3,e3) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_22431,c_260]) ).
tff(c_23767,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_23761,c_22478]) ).
tff(c_23781,plain,
( ( unit = e3 )
| ( unit = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_23777,c_23767,c_162]) ).
tff(c_23782,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_23781]) ).
tff(c_23808,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_23782,c_23782,c_204]) ).
tff(c_23813,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_23808,c_22428]) ).
tff(c_23815,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_23813]) ).
tff(c_23816,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_23781]) ).
tff(c_23840,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_23816,c_168]) ).
tff(c_23846,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23765,c_23840]) ).
tff(c_23848,plain,
op(e0,e0) = e2,
inference(splitRight,[status(thm)],[c_912]) ).
tff(c_23854,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_23848,c_350]) ).
tff(c_23868,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_23889,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_23868,c_168]) ).
tff(c_23895,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23854,c_23889]) ).
tff(c_23896,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_23898,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_23896]) ).
tff(c_23924,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_23898,c_23898,c_204]) ).
tff(c_23925,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_22427,c_23924]) ).
tff(c_23927,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_23925]) ).
tff(c_23928,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_23896]) ).
tff(c_23930,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_23928]) ).
tff(c_23957,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_23930,c_23930,c_204]) ).
tff(c_23962,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_23957,c_22428]) ).
tff(c_23964,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_23962]) ).
tff(c_23965,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_23928]) ).
tff(c_23989,plain,
op(e1,e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_23965,c_172]) ).
tff(c_24031,plain,
op(e1,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_23989,c_286]) ).
tff(c_23991,plain,
op(e2,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_23965,c_170]) ).
tff(c_640,plain,
( ( op(e2,e2) = e0 )
| ( op(e1,e1) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_24319,plain,
( ( e2 = e0 )
| ( op(e1,e1) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_23991,c_640]) ).
tff(c_24320,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22491,c_23861,c_24031,c_362,c_24319]) ).
tff(c_24322,plain,
op(e3,e3) = e2,
inference(splitRight,[status(thm)],[c_906]) ).
tff(c_24326,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_24322,c_306]) ).
tff(c_24328,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_24322,c_22478]) ).
tff(c_24338,plain,
( ( unit = e3 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_24328,c_162]) ).
tff(c_24339,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_24338]) ).
tff(c_24360,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_24339,c_168]) ).
tff(c_24366,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23854,c_24360]) ).
tff(c_24367,plain,
( ( unit = e1 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_24338]) ).
tff(c_24371,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_24367]) ).
tff(c_24393,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_24371,c_168]) ).
tff(c_24399,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24326,c_24393]) ).
tff(c_24400,plain,
unit = e1,
inference(splitRight,[status(thm)],[c_24367]) ).
tff(c_24427,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_24400,c_24400,c_204]) ).
tff(c_24433,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_24427,c_22428]) ).
tff(c_24435,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_24433]) ).
tff(c_24437,plain,
op(e1,e1) = e0,
inference(splitRight,[status(thm)],[c_888]) ).
tff(c_884,plain,
( ( op(e3,e1) != e2 )
| ( op(e1,e1) != e0 ) ),
inference(cnfTransformation,[status(thm)],[f_644]) ).
tff(c_24621,plain,
op(e3,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_24437,c_884]) ).
tff(c_340,plain,
op(e1,e1) != op(e0,e1),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_24444,plain,
op(e0,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_24437,c_340]) ).
tff(c_22454,plain,
op(e1,e1) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_22443,c_284]) ).
tff(c_24443,plain,
unit != e0,
inference(demodulation,[status(thm),theory(equality)],[c_24437,c_22454]) ).
tff(c_24451,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_24443,c_162]) ).
tff(c_24452,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_24451]) ).
tff(c_24469,plain,
op(e0,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_24452,c_176]) ).
tff(c_24479,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24444,c_24469]) ).
tff(c_24480,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_24451]) ).
tff(c_24482,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_24480]) ).
tff(c_24509,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_24482,c_24482,c_204]) ).
tff(c_24510,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_22427,c_24509]) ).
tff(c_24512,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_24510]) ).
tff(c_24513,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_24480]) ).
tff(c_24527,plain,
op(e3,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_24513,c_22431]) ).
tff(c_24631,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24621,c_24527]) ).
tff(c_24633,plain,
op(e1,e1) = e3,
inference(splitRight,[status(thm)],[c_922]) ).
tff(c_24638,plain,
unit != e3,
inference(demodulation,[status(thm),theory(equality)],[c_24633,c_22454]) ).
tff(c_24647,plain,
( ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_24638,c_162]) ).
tff(c_24648,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_24647]) ).
tff(c_24667,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_24648,c_174]) ).
tff(c_24659,plain,
op(e3,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_24648,c_22431]) ).
tff(c_54,plain,
op(op(e3,e1),e1) = op(e3,op(e1,e1)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_24834,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_24667,c_24659,c_24633,c_54]) ).
tff(c_24835,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22487,c_24834]) ).
tff(c_24836,plain,
( ( unit = e1 )
| ( unit = e2 ) ),
inference(splitRight,[status(thm)],[c_24647]) ).
tff(c_24838,plain,
unit = e2,
inference(splitLeft,[status(thm)],[c_24836]) ).
tff(c_24858,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_24838,c_174]) ).
tff(c_24850,plain,
op(e3,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_24838,c_22431]) ).
tff(c_25038,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_24858,c_24850,c_24633,c_54]) ).
tff(c_25039,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22487,c_25038]) ).
tff(c_25040,plain,
unit = e1,
inference(splitRight,[status(thm)],[c_24836]) ).
tff(c_25067,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_25040,c_25040,c_204]) ).
tff(c_25073,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_25067,c_22428]) ).
tff(c_25075,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_25073]) ).
tff(c_25077,plain,
op(e3,e3) = e1,
inference(splitRight,[status(thm)],[c_894]) ).
tff(c_25783,plain,
inv(e2) = e2,
inference(negUnitSimplification,[status(thm)],[c_1012,c_1011,c_22446,c_182]) ).
tff(c_25082,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_25077,c_22478]) ).
tff(c_25089,plain,
op(e1,e1) != e3,
inference(splitLeft,[status(thm)],[c_922]) ).
tff(c_25096,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_25082,c_162]) ).
tff(c_25097,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_25096]) ).
tff(c_25121,plain,
op(e3,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_25097,c_164]) ).
tff(c_25108,plain,
op(e3,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_25097,c_22431]) ).
tff(c_38,plain,
op(op(e3,e3),e1) = op(e3,op(e3,e1)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_25253,plain,
op(e1,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_25121,c_25108,c_25077,c_38]) ).
tff(c_25254,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25089,c_25253]) ).
tff(c_25255,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_25096]) ).
tff(c_25257,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_25255]) ).
tff(c_25281,plain,
op(e3,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_25257,c_166]) ).
tff(c_25284,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_25077,c_25281]) ).
tff(c_25286,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_25284]) ).
tff(c_25287,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_25255]) ).
tff(c_25314,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_25287,c_164]) ).
tff(c_25301,plain,
op(e3,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_25287,c_22431]) ).
tff(c_25454,plain,
op(e1,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_25314,c_25301,c_25077,c_38]) ).
tff(c_25455,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25089,c_25454]) ).
tff(c_25457,plain,
op(e1,e1) = e3,
inference(splitRight,[status(thm)],[c_922]) ).
tff(c_25463,plain,
unit != e3,
inference(demodulation,[status(thm),theory(equality)],[c_25457,c_22454]) ).
tff(c_25478,plain,
( ( unit = e2 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_25082,c_25463,c_162]) ).
tff(c_25479,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_25478]) ).
tff(c_25494,plain,
op(inv(e2),e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_25479,c_192]) ).
tff(c_25784,plain,
op(e2,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_25783,c_25494]) ).
tff(c_506,plain,
( ( op(e1,e1) = e0 )
| ( op(e2,e2) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e2,e2) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_25842,plain,
( ( e3 = e0 )
| ( e1 = e0 )
| ( e2 = e1 )
| ( e3 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_25784,c_25077,c_25784,c_25457,c_506]) ).
tff(c_25843,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_358,c_364,c_360,c_25842]) ).
tff(c_25844,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_25478]) ).
tff(c_25869,plain,
op(e2,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_25844,c_170]) ).
tff(c_376,plain,
( ( op(e2,e2) = e0 )
| ( op(e2,e2) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e3,e3) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_26219,plain,
( ( e2 = e0 )
| ( e2 = e1 )
| ( e2 = e1 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_25077,c_25077,c_25869,c_25869,c_376]) ).
tff(c_26220,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_358,c_358,c_362,c_26219]) ).
tff(c_26222,plain,
inv(e2) = e0,
inference(splitRight,[status(thm)],[c_228]) ).
tff(c_26282,plain,
op(e3,e3) != e1,
inference(splitLeft,[status(thm)],[c_894]) ).
tff(c_26265,plain,
inv(e1) != e3,
inference(splitLeft,[status(thm)],[c_230]) ).
tff(c_26279,plain,
inv(e3) != e1,
inference(negUnitSimplification,[status(thm)],[c_26265,c_218]) ).
tff(c_27296,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_26279,c_1009,c_180]) ).
tff(c_26234,plain,
op(e2,e0) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_26222,c_194]) ).
tff(c_26291,plain,
( ( unit != e1 )
| ( op(e0,e0) != e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26234,c_920]) ).
tff(c_26292,plain,
op(e0,e0) != e3,
inference(splitLeft,[status(thm)],[c_26291]) ).
tff(c_26289,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_912]) ).
tff(c_26284,plain,
op(e0,e0) != e1,
inference(splitLeft,[status(thm)],[c_896]) ).
tff(c_26293,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_26318,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_26293,c_26293,c_204]) ).
tff(c_26221,plain,
inv(e0) = e2,
inference(splitRight,[status(thm)],[c_228]) ).
tff(c_26324,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_26318,c_26221]) ).
tff(c_26326,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_26324]) ).
tff(c_26327,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_26329,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_26327]) ).
tff(c_26347,plain,
op(e0,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_26329,c_176]) ).
tff(c_26371,plain,
op(e0,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_26347,c_300]) ).
tff(c_876,plain,
( ( op(e0,e0) = e0 )
| ( op(e0,e0) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e0,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_26947,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26292,c_26289,c_26284,c_26371,c_876]) ).
tff(c_26948,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_26327]) ).
tff(c_26950,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_26948]) ).
tff(c_26967,plain,
op(e3,inv(e3)) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_26950,c_190]) ).
tff(c_27297,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_27296,c_26967]) ).
tff(c_27304,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26282,c_27297]) ).
tff(c_27305,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_26948]) ).
tff(c_27334,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_27305,c_27305,c_204]) ).
tff(c_27335,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_26222,c_27334]) ).
tff(c_27337,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_27335]) ).
tff(c_27339,plain,
op(e0,e0) = e3,
inference(splitRight,[status(thm)],[c_26291]) ).
tff(c_27343,plain,
op(e0,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_27339,c_300]) ).
tff(c_27338,plain,
unit != e1,
inference(splitRight,[status(thm)],[c_26291]) ).
tff(c_26252,plain,
op(e0,e0) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_26234,c_350]) ).
tff(c_27344,plain,
unit != e3,
inference(demodulation,[status(thm),theory(equality)],[c_27339,c_26252]) ).
tff(c_27356,plain,
( ( unit = e2 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_27338,c_27344,c_162]) ).
tff(c_27357,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_27356]) ).
tff(c_27381,plain,
op(e0,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_27357,c_166]) ).
tff(c_27385,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27343,c_27381]) ).
tff(c_27386,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_27356]) ).
tff(c_27413,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_27386,c_27386,c_204]) ).
tff(c_27414,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_26222,c_27413]) ).
tff(c_27416,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_27414]) ).
tff(c_27418,plain,
op(e0,e0) = e2,
inference(splitRight,[status(thm)],[c_912]) ).
tff(c_27431,plain,
op(e2,e2) != e0,
inference(splitLeft,[status(thm)],[c_886]) ).
tff(c_27422,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_27418,c_26252]) ).
tff(c_27433,plain,
( ( unit = e3 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_27422,c_162]) ).
tff(c_27434,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_27433]) ).
tff(c_27459,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_27434,c_27434,c_204]) ).
tff(c_27464,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_27459,c_26221]) ).
tff(c_27466,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_27464]) ).
tff(c_27467,plain,
( ( unit = e1 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_27433]) ).
tff(c_27469,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_27467]) ).
tff(c_27489,plain,
op(e3,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_27469,c_178]) ).
tff(c_27482,plain,
op(e2,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_27469,c_26234]) ).
tff(c_96,plain,
op(op(e2,e0),e0) = op(e2,op(e0,e0)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_27610,plain,
op(e2,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_27489,c_27482,c_27418,c_96]) ).
tff(c_27611,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27431,c_27610]) ).
tff(c_27612,plain,
unit = e1,
inference(splitRight,[status(thm)],[c_27467]) ).
tff(c_27632,plain,
op(e1,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_27612,c_178]) ).
tff(c_27625,plain,
op(e2,e0) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_27612,c_26234]) ).
tff(c_27780,plain,
op(e2,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_27632,c_27625,c_27418,c_96]) ).
tff(c_27781,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_27431,c_27780]) ).
tff(c_27783,plain,
op(e2,e2) = e0,
inference(splitRight,[status(thm)],[c_886]) ).
tff(c_28107,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_26279,c_1009,c_180]) ).
tff(c_26235,plain,
op(e0,e2) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_26222,c_192]) ).
tff(c_26269,plain,
op(e2,e2) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_26235,c_326]) ).
tff(c_27790,plain,
unit != e0,
inference(demodulation,[status(thm),theory(equality)],[c_27783,c_26269]) ).
tff(c_27796,plain,
( ( unit = e3 )
| ( unit = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_27790,c_27422,c_162]) ).
tff(c_27797,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_27796]) ).
tff(c_27814,plain,
op(e3,inv(e3)) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_27797,c_190]) ).
tff(c_28108,plain,
op(e3,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_28107,c_27814]) ).
tff(c_28115,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26282,c_28108]) ).
tff(c_28116,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_27796]) ).
tff(c_28142,plain,
op(e3,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_28116,c_164]) ).
tff(c_806,plain,
( ( op(e3,e3) = e0 )
| ( op(e0,e0) = e1 )
| ( op(e2,e2) = e2 )
| ( op(e0,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_28466,plain,
( ( e3 = e0 )
| ( e2 = e1 )
| ( e2 = e0 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_27418,c_27783,c_27418,c_28142,c_806]) ).
tff(c_28467,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_362,c_358,c_360,c_28466]) ).
tff(c_28469,plain,
op(e0,e0) = e1,
inference(splitRight,[status(thm)],[c_896]) ).
tff(c_28470,plain,
op(e0,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_28469,c_304]) ).
tff(c_28472,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_28469,c_26252]) ).
tff(c_28481,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_28472,c_162]) ).
tff(c_28482,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_28481]) ).
tff(c_28501,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_28482,c_174]) ).
tff(c_28509,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28470,c_28501]) ).
tff(c_28510,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_28481]) ).
tff(c_28512,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_28510]) ).
tff(c_28524,plain,
op(e2,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_28512,c_26234]) ).
tff(c_28657,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28469,c_28524,c_900]) ).
tff(c_28658,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_28510]) ).
tff(c_28685,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_28658,c_28658,c_204]) ).
tff(c_28686,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_26222,c_28685]) ).
tff(c_28688,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_28686]) ).
tff(c_28690,plain,
op(e3,e3) = e1,
inference(splitRight,[status(thm)],[c_894]) ).
tff(c_28694,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_28690,c_260]) ).
tff(c_28704,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_28729,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_28704,c_28704,c_204]) ).
tff(c_28734,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_28729,c_26221]) ).
tff(c_28736,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_28734]) ).
tff(c_28737,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_28739,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_28737]) ).
tff(c_28759,plain,
op(e3,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_28739,c_174]) ).
tff(c_28767,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28694,c_28759]) ).
tff(c_28768,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_28737]) ).
tff(c_28770,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_28768]) ).
tff(c_28784,plain,
op(e0,e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_28770,c_26235]) ).
tff(c_28914,plain,
op(e2,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_28784,c_918]) ).
tff(c_28811,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_912]) ).
tff(c_28781,plain,
op(e0,e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_28770,c_26252]) ).
tff(c_28792,plain,
op(e1,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_28770,c_172]) ).
tff(c_618,plain,
( ( op(e1,e1) = e0 )
| ( op(e0,e0) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e2,e2) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_29132,plain,
( ( e1 = e0 )
| ( op(e0,e0) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e2,e2) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28792,c_618]) ).
tff(c_29133,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28914,c_28811,c_28781,c_364,c_29132]) ).
tff(c_29135,plain,
op(e0,e0) = e2,
inference(splitRight,[status(thm)],[c_912]) ).
tff(c_780,plain,
( ( op(e0,e0) = e0 )
| ( op(e0,e0) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e0,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_29581,plain,
( ( e2 = e0 )
| ( e2 = e1 )
| ( e2 = e1 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29135,c_28690,c_29135,c_29135,c_780]) ).
tff(c_29582,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_358,c_358,c_362,c_29581]) ).
tff(c_29583,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_28768]) ).
tff(c_29611,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_29583,c_29583,c_204]) ).
tff(c_29612,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_26222,c_29611]) ).
tff(c_29614,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_29612]) ).
tff(c_29615,plain,
inv(e3) = e1,
inference(splitRight,[status(thm)],[c_230]) ).
tff(c_29692,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_29717,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_29692,c_29692,c_204]) ).
tff(c_29722,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_29717,c_26221]) ).
tff(c_29724,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_29722]) ).
tff(c_29725,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_29727,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_29725]) ).
tff(c_29753,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_29727,c_29727,c_204]) ).
tff(c_29754,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_29615,c_29753]) ).
tff(c_29756,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_29754]) ).
tff(c_29757,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_29725]) ).
tff(c_29759,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_29757]) ).
tff(c_29786,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_29759,c_29759,c_204]) ).
tff(c_29616,plain,
inv(e1) = e3,
inference(splitRight,[status(thm)],[c_230]) ).
tff(c_29791,plain,
e3 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_29786,c_29616]) ).
tff(c_29793,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_29791]) ).
tff(c_29794,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_29757]) ).
tff(c_29822,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_29794,c_29794,c_204]) ).
tff(c_29823,plain,
e2 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_26222,c_29822]) ).
tff(c_29825,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_29823]) ).
tff(c_29827,plain,
inv(e2) = e1,
inference(splitRight,[status(thm)],[c_226]) ).
tff(c_29826,plain,
inv(e1) = e2,
inference(splitRight,[status(thm)],[c_226]) ).
tff(c_29838,plain,
op(e2,e1) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_29826,c_196]) ).
tff(c_29897,plain,
( ( unit != e0 )
| ( op(e1,e1) != e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29838,c_916]) ).
tff(c_29898,plain,
op(e1,e1) != e3,
inference(splitLeft,[status(thm)],[c_29897]) ).
tff(c_29891,plain,
op(e1,e1) != e2,
inference(splitLeft,[status(thm)],[c_910]) ).
tff(c_29892,plain,
op(e2,e2) != e1,
inference(splitLeft,[status(thm)],[c_892]) ).
tff(c_29895,plain,
( ( unit != e3 )
| ( op(e1,e1) != e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_29838,c_888]) ).
tff(c_29896,plain,
op(e1,e1) != e0,
inference(splitLeft,[status(thm)],[c_29895]) ).
tff(c_698,plain,
( ( op(e1,e1) = e0 )
| ( op(e2,e2) = e1 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_31042,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_29898,c_29891,c_29892,c_29896,c_698]) ).
tff(c_31044,plain,
op(e1,e1) = e3,
inference(splitRight,[status(thm)],[c_29897]) ).
tff(c_31050,plain,
op(e1,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_31044,c_284]) ).
tff(c_31043,plain,
unit != e0,
inference(splitRight,[status(thm)],[c_29897]) ).
tff(c_29829,plain,
op(e1,e2) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_29827,c_192]) ).
tff(c_29872,plain,
op(e1,e1) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_29829,c_286]) ).
tff(c_31048,plain,
unit != e3,
inference(demodulation,[status(thm),theory(equality)],[c_31044,c_29872]) ).
tff(c_31057,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_31043,c_31048,c_162]) ).
tff(c_31058,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_31057]) ).
tff(c_31082,plain,
op(e1,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_31058,c_166]) ).
tff(c_31086,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31050,c_31082]) ).
tff(c_31087,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_31057]) ).
tff(c_31115,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_31087,c_31087,c_204]) ).
tff(c_31116,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_29827,c_31115]) ).
tff(c_31118,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_31116]) ).
tff(c_31120,plain,
op(e1,e1) = e0,
inference(splitRight,[status(thm)],[c_29895]) ).
tff(c_31126,plain,
op(e0,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_31120,c_340]) ).
tff(c_31123,plain,
unit != e0,
inference(demodulation,[status(thm),theory(equality)],[c_31120,c_29872]) ).
tff(c_31119,plain,
unit != e3,
inference(splitRight,[status(thm)],[c_29895]) ).
tff(c_31139,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_31123,c_31119,c_162]) ).
tff(c_31140,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_31139]) ).
tff(c_31158,plain,
op(e0,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_31140,c_176]) ).
tff(c_31168,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31126,c_31158]) ).
tff(c_31169,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_31139]) ).
tff(c_31196,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_31169,c_31169,c_204]) ).
tff(c_31197,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_29827,c_31196]) ).
tff(c_31199,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_31197]) ).
tff(c_31201,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_892]) ).
tff(c_29867,plain,
op(e2,e2) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_29838,c_274]) ).
tff(c_31207,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_31201,c_29867]) ).
tff(c_31222,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_31207,c_162]) ).
tff(c_31223,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_31222]) ).
tff(c_31244,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_31223,c_168]) ).
tff(c_31235,plain,
op(e2,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_31223,c_29838]) ).
tff(c_78,plain,
op(op(e2,e2),e1) = op(e2,op(e2,e1)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_31509,plain,
op(e1,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_31244,c_31235,c_31201,c_78]) ).
tff(c_31510,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_29891,c_31509]) ).
tff(c_31511,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_31222]) ).
tff(c_31513,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_31511]) ).
tff(c_31535,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_31513,c_168]) ).
tff(c_31526,plain,
op(e2,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_31513,c_29838]) ).
tff(c_31737,plain,
op(e1,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_31535,c_31526,c_31201,c_78]) ).
tff(c_31738,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_29891,c_31737]) ).
tff(c_31739,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_31511]) ).
tff(c_31762,plain,
op(e2,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_31739,c_168]) ).
tff(c_31767,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_31201,c_31762]) ).
tff(c_31769,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_31767]) ).
tff(c_31771,plain,
op(e1,e1) = e2,
inference(splitRight,[status(thm)],[c_910]) ).
tff(c_31774,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_31771,c_29872]) ).
tff(c_31785,plain,
( ( unit = e3 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_31774,c_162]) ).
tff(c_31786,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_31785]) ).
tff(c_31806,plain,
op(e1,e0) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_31786,c_172]) ).
tff(c_31796,plain,
op(e1,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_31786,c_29829]) ).
tff(c_116,plain,
op(op(e1,e1),e2) = op(e1,op(e1,e2)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_32073,plain,
op(e2,e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_31806,c_31796,c_31771,c_116]) ).
tff(c_32074,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31772,c_32073]) ).
tff(c_32075,plain,
( ( unit = e1 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_31785]) ).
tff(c_32077,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_32075]) ).
tff(c_32097,plain,
op(e3,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_32077,c_174]) ).
tff(c_32090,plain,
op(e2,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_32077,c_29838]) ).
tff(c_86,plain,
op(op(e2,e1),e1) = op(e2,op(e1,e1)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_32359,plain,
op(e2,e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_32097,c_32090,c_31771,c_86]) ).
tff(c_32360,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31772,c_32359]) ).
tff(c_32361,plain,
unit = e1,
inference(splitRight,[status(thm)],[c_32075]) ).
tff(c_32388,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_32361,c_32361,c_204]) ).
tff(c_32394,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_32388,c_29826]) ).
tff(c_32396,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_32394]) ).
tff(c_32398,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_892]) ).
tff(c_254,plain,
inv(e2) != inv(e0),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_29833,plain,
inv(e0) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_29827,c_254]) ).
tff(c_29841,plain,
inv(e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_29826,c_256]) ).
tff(c_29873,plain,
inv(e0) != e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_238]) ).
tff(c_33109,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_29833,c_29841,c_29873,c_186]) ).
tff(c_246,plain,
inv(e3) != inv(e2),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_29831,plain,
inv(e3) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_29827,c_246]) ).
tff(c_32734,plain,
inv(e3) = e3,
inference(negUnitSimplification,[status(thm)],[c_1010,c_29831,c_1009,c_180]) ).
tff(c_32413,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_32398,c_29867]) ).
tff(c_32401,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_31771,c_29872]) ).
tff(c_32421,plain,
( ( unit = e3 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_32413,c_32401,c_162]) ).
tff(c_32422,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_32421]) ).
tff(c_32437,plain,
op(inv(e3),e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_32422,c_188]) ).
tff(c_32735,plain,
op(e3,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_32734,c_32437]) ).
tff(c_384,plain,
( ( op(e2,e2) = e0 )
| ( op(e1,e1) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e3,e3) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_32793,plain,
( ( e1 = e0 )
| ( e2 = e1 )
| ( e2 = e0 )
| ( e3 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_32735,c_32735,c_31771,c_32398,c_384]) ).
tff(c_32794,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_362,c_358,c_364,c_32793]) ).
tff(c_32795,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_32421]) ).
tff(c_32812,plain,
op(e0,inv(e0)) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_32795,c_202]) ).
tff(c_33110,plain,
op(e0,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_33109,c_32812]) ).
tff(c_33174,plain,
( ( e2 = e0 )
| ( e3 = e1 )
| ( e3 = e2 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_32398,c_33110,c_33110,c_31771,c_618]) ).
tff(c_33175,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_354,c_356,c_362,c_33174]) ).
tff(c_33177,plain,
inv(e3) = e0,
inference(splitRight,[status(thm)],[c_220]) ).
tff(c_33245,plain,
op(e1,e1) != e2,
inference(splitLeft,[status(thm)],[c_910]) ).
tff(c_248,plain,
inv(e3) != inv(e1),
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_33194,plain,
inv(e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_248]) ).
tff(c_33178,plain,
inv(e2) != e1,
inference(splitLeft,[status(thm)],[c_226]) ).
tff(c_33222,plain,
inv(e1) != e2,
inference(negUnitSimplification,[status(thm)],[c_33178,c_232]) ).
tff(c_33176,plain,
inv(e0) = e3,
inference(splitRight,[status(thm)],[c_220]) ).
tff(c_33182,plain,
inv(e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_33176,c_256]) ).
tff(c_34039,plain,
inv(e1) = e1,
inference(negUnitSimplification,[status(thm)],[c_33194,c_33222,c_33182,c_184]) ).
tff(c_33247,plain,
op(e2,e2) != e1,
inference(splitLeft,[status(thm)],[c_898]) ).
tff(c_33193,plain,
inv(e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_246]) ).
tff(c_33184,plain,
inv(e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_33176,c_254]) ).
tff(c_33679,plain,
inv(e2) = e2,
inference(negUnitSimplification,[status(thm)],[c_33193,c_33178,c_33184,c_182]) ).
tff(c_33257,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_33282,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_33257,c_33257,c_204]) ).
tff(c_33287,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_33282,c_33176]) ).
tff(c_33289,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_33287]) ).
tff(c_33290,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_33296,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_33290]) ).
tff(c_33322,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_33296,c_33296,c_204]) ).
tff(c_33323,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_33322]) ).
tff(c_33325,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_33323]) ).
tff(c_33326,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_33290]) ).
tff(c_33328,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_33326]) ).
tff(c_33345,plain,
op(e2,inv(e2)) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_33328,c_194]) ).
tff(c_33680,plain,
op(e2,e2) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_33679,c_33345]) ).
tff(c_33687,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33247,c_33680]) ).
tff(c_33688,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_33326]) ).
tff(c_33705,plain,
op(e1,inv(e1)) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_33688,c_198]) ).
tff(c_34040,plain,
op(e1,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_34039,c_33705]) ).
tff(c_34047,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33245,c_34040]) ).
tff(c_34049,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_898]) ).
tff(c_34056,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_34049,c_274]) ).
tff(c_34063,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_34088,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_34063,c_34063,c_204]) ).
tff(c_34093,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_34088,c_33176]) ).
tff(c_34095,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_34093]) ).
tff(c_34096,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_34098,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_34096]) ).
tff(c_34124,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_34098,c_34098,c_204]) ).
tff(c_34125,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_34124]) ).
tff(c_34127,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_34125]) ).
tff(c_34128,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_34096]) ).
tff(c_34130,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_34128]) ).
tff(c_33191,plain,
op(e0,e3) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_188]) ).
tff(c_34144,plain,
op(e0,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_34130,c_33191]) ).
tff(c_34156,plain,
op(e3,e1) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_34130,c_164]) ).
tff(c_34180,plain,
op(e3,e3) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_34156,c_260]) ).
tff(c_34238,plain,
op(e3,e3) != e2,
inference(splitLeft,[status(thm)],[c_906]) ).
tff(c_33243,plain,
( ( unit != e2 )
| ( op(e3,e3) != e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_33191,c_894]) ).
tff(c_33244,plain,
op(e3,e3) != e1,
inference(splitLeft,[status(thm)],[c_33243]) ).
tff(c_34152,plain,
op(e1,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_34130,c_172]) ).
tff(c_370,plain,
( ( op(e1,e1) = e0 )
| ( op(e3,e3) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e3,e3) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_34489,plain,
( ( e1 = e0 )
| ( op(e3,e3) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e3,e3) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34152,c_370]) ).
tff(c_34490,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34180,c_34238,c_33244,c_364,c_34489]) ).
tff(c_34491,plain,
op(e0,e3) != e1,
inference(splitRight,[status(thm)],[c_906]) ).
tff(c_34512,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34144,c_34491]) ).
tff(c_34513,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_34128]) ).
tff(c_34535,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_34513,c_174]) ).
tff(c_34543,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34056,c_34535]) ).
tff(c_34545,plain,
op(e1,e1) = e2,
inference(splitRight,[status(thm)],[c_910]) ).
tff(c_34561,plain,
op(e3,e3) != e0,
inference(splitLeft,[status(thm)],[c_878]) ).
tff(c_34559,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_912]) ).
tff(c_33179,plain,
op(e3,e0) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_33176,c_200]) ).
tff(c_33241,plain,
( ( unit != e2 )
| ( op(e0,e0) != e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_33179,c_896]) ).
tff(c_33242,plain,
op(e0,e0) != e1,
inference(splitLeft,[status(thm)],[c_33241]) ).
tff(c_34550,plain,
op(e2,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_34545,c_334]) ).
tff(c_34568,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_34593,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_34568,c_34568,c_204]) ).
tff(c_34598,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_34593,c_33176]) ).
tff(c_34600,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_34598]) ).
tff(c_34601,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_34604,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_34601]) ).
tff(c_34630,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_34604,c_34604,c_204]) ).
tff(c_34631,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_34630]) ).
tff(c_34633,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_34631]) ).
tff(c_34634,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_34601]) ).
tff(c_34636,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_34634]) ).
tff(c_34659,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_34636,c_168]) ).
tff(c_34665,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34550,c_34659]) ).
tff(c_34666,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_34634]) ).
tff(c_34687,plain,
op(e2,e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_34666,c_178]) ).
tff(c_34731,plain,
op(e0,e0) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_34687,c_350]) ).
tff(c_35014,plain,
op(e0,e0) = e3,
inference(negUnitSimplification,[status(thm)],[c_34559,c_33242,c_34731,c_876]) ).
tff(c_34686,plain,
op(e0,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_34666,c_176]) ).
tff(c_34681,plain,
op(e0,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_34666,c_33191]) ).
tff(c_154,plain,
op(op(e0,e0),e3) = op(e0,op(e0,e3)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_34897,plain,
op(op(e0,e0),e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_34686,c_34681,c_154]) ).
tff(c_35016,plain,
op(e3,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_35014,c_34897]) ).
tff(c_35028,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34561,c_35016]) ).
tff(c_35030,plain,
op(e3,e3) = e0,
inference(splitRight,[status(thm)],[c_878]) ).
tff(c_264,plain,
op(e3,e3) != op(e3,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_33231,plain,
op(e3,e3) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_33179,c_264]) ).
tff(c_35035,plain,
unit != e0,
inference(demodulation,[status(thm),theory(equality)],[c_35030,c_33231]) ).
tff(c_35041,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_35035,c_162]) ).
tff(c_35042,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_35041]) ).
tff(c_35064,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35042,c_168]) ).
tff(c_35070,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34550,c_35064]) ).
tff(c_35071,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_35041]) ).
tff(c_35073,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_35071]) ).
tff(c_35097,plain,
op(e3,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_35073,c_166]) ).
tff(c_35100,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_35030,c_35097]) ).
tff(c_35102,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_35100]) ).
tff(c_35103,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_35071]) ).
tff(c_35129,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_35103,c_164]) ).
tff(c_35116,plain,
op(e3,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35103,c_33179]) ).
tff(c_40,plain,
op(op(e3,e3),e0) = op(e3,op(e3,e0)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_35335,plain,
op(e0,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_35129,c_35116,c_35030,c_40]) ).
tff(c_35127,plain,
op(e2,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35103,c_170]) ).
tff(c_736,plain,
( ( op(e2,e2) = e0 )
| ( op(e1,e1) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_35466,plain,
( ( e2 = e0 )
| ( e2 = e1 )
| ( e3 = e2 )
| ( e3 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_34545,c_35335,c_34545,c_35127,c_736]) ).
tff(c_35467,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_354,c_358,c_362,c_35466]) ).
tff(c_35469,plain,
op(e0,e0) = e2,
inference(splitRight,[status(thm)],[c_912]) ).
tff(c_35479,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_35469,c_350]) ).
tff(c_35470,plain,
( ( unit != e1 )
| ( op(e0,e0) != e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_33179,c_908]) ).
tff(c_35471,plain,
op(e0,e0) != e2,
inference(splitLeft,[status(thm)],[c_35470]) ).
tff(c_35472,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35471,c_35469]) ).
tff(c_35473,plain,
unit != e1,
inference(splitRight,[status(thm)],[c_35470]) ).
tff(c_348,plain,
op(e3,e0) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_33207,plain,
op(e0,e0) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_33179,c_348]) ).
tff(c_35478,plain,
unit != e2,
inference(demodulation,[status(thm),theory(equality)],[c_35469,c_33207]) ).
tff(c_35491,plain,
( ( unit = e3 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_35473,c_35478,c_162]) ).
tff(c_35492,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_35491]) ).
tff(c_35514,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35492,c_168]) ).
tff(c_35520,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35479,c_35514]) ).
tff(c_35521,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_35491]) ).
tff(c_35548,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_35521,c_35521,c_204]) ).
tff(c_35549,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_35548]) ).
tff(c_35551,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_35549]) ).
tff(c_35553,plain,
op(e3,e3) = e1,
inference(splitRight,[status(thm)],[c_33243]) ).
tff(c_35556,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_35553,c_260]) ).
tff(c_35558,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_35553,c_33231]) ).
tff(c_35552,plain,
unit != e2,
inference(splitRight,[status(thm)],[c_33243]) ).
tff(c_35573,plain,
( ( unit = e3 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_35558,c_35552,c_162]) ).
tff(c_35574,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_35573]) ).
tff(c_35600,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_35574,c_35574,c_204]) ).
tff(c_35605,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_35600,c_33176]) ).
tff(c_35607,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_35605]) ).
tff(c_35608,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_35573]) ).
tff(c_35630,plain,
op(e3,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_35608,c_174]) ).
tff(c_35638,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35556,c_35630]) ).
tff(c_35640,plain,
op(e0,e0) = e1,
inference(splitRight,[status(thm)],[c_33241]) ).
tff(c_35642,plain,
op(e0,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_35640,c_304]) ).
tff(c_35644,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_35640,c_33207]) ).
tff(c_35639,plain,
unit != e2,
inference(splitRight,[status(thm)],[c_33241]) ).
tff(c_35653,plain,
( ( unit = e3 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_35644,c_35639,c_162]) ).
tff(c_35654,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_35653]) ).
tff(c_35674,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_35654,c_174]) ).
tff(c_35682,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35642,c_35674]) ).
tff(c_35683,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_35653]) ).
tff(c_35710,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_35683,c_35683,c_204]) ).
tff(c_35711,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_35710]) ).
tff(c_35713,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_35711]) ).
tff(c_35715,plain,
inv(e2) = e1,
inference(splitRight,[status(thm)],[c_226]) ).
tff(c_35830,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_35855,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_35830,c_35830,c_204]) ).
tff(c_35861,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_35855,c_33176]) ).
tff(c_35863,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_35861]) ).
tff(c_35864,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_35866,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_35864]) ).
tff(c_35892,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_35866,c_35866,c_204]) ).
tff(c_35893,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_33177,c_35892]) ).
tff(c_35895,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_35893]) ).
tff(c_35896,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_35864]) ).
tff(c_35898,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_35896]) ).
tff(c_35925,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_35898,c_35898,c_204]) ).
tff(c_35714,plain,
inv(e1) = e2,
inference(splitRight,[status(thm)],[c_226]) ).
tff(c_35930,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_35925,c_35714]) ).
tff(c_35932,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_35930]) ).
tff(c_35933,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_35896]) ).
tff(c_35961,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35933,c_35933,c_204]) ).
tff(c_35962,plain,
e2 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_35715,c_35961]) ).
tff(c_35964,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_358,c_35962]) ).
tff(c_35966,plain,
inv(e3) = e2,
inference(splitRight,[status(thm)],[c_216]) ).
tff(c_36035,plain,
op(e2,e2) != e1,
inference(splitLeft,[status(thm)],[c_898]) ).
tff(c_35965,plain,
inv(e2) = e3,
inference(splitRight,[status(thm)],[c_216]) ).
tff(c_35968,plain,
op(e2,e3) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_35965,c_194]) ).
tff(c_36856,plain,
( ( unit != e1 )
| ( op(e3,e3) != e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_35968,c_878]) ).
tff(c_36857,plain,
op(e3,e3) != e0,
inference(splitLeft,[status(thm)],[c_36856]) ).
tff(c_36031,plain,
op(e0,e0) != e1,
inference(splitLeft,[status(thm)],[c_896]) ).
tff(c_36012,plain,
inv(e1) != e0,
inference(splitLeft,[status(thm)],[c_236]) ).
tff(c_36015,plain,
inv(e0) != e1,
inference(negUnitSimplification,[status(thm)],[c_36012,c_242]) ).
tff(c_35982,plain,
inv(e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_35966,c_252]) ).
tff(c_35973,plain,
inv(e0) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_35965,c_254]) ).
tff(c_36797,plain,
inv(e0) = e0,
inference(negUnitSimplification,[status(thm)],[c_36015,c_35982,c_35973,c_186]) ).
tff(c_36038,plain,
op(e1,e1) != e0,
inference(splitLeft,[status(thm)],[c_888]) ).
tff(c_35981,plain,
inv(e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_35966,c_248]) ).
tff(c_35972,plain,
inv(e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_35965,c_250]) ).
tff(c_36400,plain,
inv(e1) = e1,
inference(negUnitSimplification,[status(thm)],[c_36012,c_35981,c_35972,c_184]) ).
tff(c_36047,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_36061,plain,
op(e1,inv(e1)) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_36047,c_198]) ).
tff(c_36401,plain,
op(e1,e1) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_36400,c_36061]) ).
tff(c_36408,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_36038,c_36401]) ).
tff(c_36409,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_36411,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_36409]) ).
tff(c_36437,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_36411,c_36411,c_204]) ).
tff(c_36438,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35966,c_36437]) ).
tff(c_36440,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_36438]) ).
tff(c_36441,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_36409]) ).
tff(c_36443,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_36441]) ).
tff(c_36460,plain,
op(inv(e0),e0) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_36443,c_200]) ).
tff(c_36798,plain,
op(e0,e0) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_36797,c_36460]) ).
tff(c_36805,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_36031,c_36798]) ).
tff(c_36806,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_36441]) ).
tff(c_36835,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_36806,c_36806,c_204]) ).
tff(c_36840,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_36835,c_35965]) ).
tff(c_36842,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_36840]) ).
tff(c_36844,plain,
op(e1,e1) = e0,
inference(splitRight,[status(thm)],[c_888]) ).
tff(c_694,plain,
( ( op(e3,e3) = e0 )
| ( op(e2,e2) = e1 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_37210,plain,
( ( op(e3,e3) = e0 )
| ( op(e2,e2) = e1 )
| ( e2 = e0 )
| ( e3 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_36844,c_36844,c_694]) ).
tff(c_37211,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_360,c_362,c_36035,c_36857,c_37210]) ).
tff(c_37213,plain,
op(e3,e3) = e0,
inference(splitRight,[status(thm)],[c_36856]) ).
tff(c_37215,plain,
op(e0,e3) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_37213,c_312]) ).
tff(c_35978,plain,
op(e3,e2) = unit,
inference(demodulation,[status(thm),theory(equality)],[c_35966,c_190]) ).
tff(c_258,plain,
op(e3,e3) != op(e3,e2),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_36020,plain,
op(e3,e3) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_35978,c_258]) ).
tff(c_37216,plain,
unit != e0,
inference(demodulation,[status(thm),theory(equality)],[c_37213,c_36020]) ).
tff(c_37212,plain,
unit != e1,
inference(splitRight,[status(thm)],[c_36856]) ).
tff(c_37228,plain,
( ( unit = e3 )
| ( unit = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_37216,c_37212,c_162]) ).
tff(c_37229,plain,
unit = e2,
inference(splitLeft,[status(thm)],[c_37228]) ).
tff(c_37255,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_37229,c_37229,c_204]) ).
tff(c_37260,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_37255,c_35965]) ).
tff(c_37262,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_37260]) ).
tff(c_37263,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_37228]) ).
tff(c_37284,plain,
op(e0,e3) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_37263,c_176]) ).
tff(c_37294,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37215,c_37284]) ).
tff(c_37296,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_898]) ).
tff(c_37302,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_37296,c_274]) ).
tff(c_37309,plain,
unit != e0,
inference(demodulation,[status(thm),theory(equality)],[c_37296,c_35978,c_892]) ).
tff(c_318,plain,
op(e3,e2) != op(e2,e2),
inference(cnfTransformation,[status(thm)],[f_580]) ).
tff(c_36017,plain,
op(e2,e2) != unit,
inference(demodulation,[status(thm),theory(equality)],[c_35978,c_318]) ).
tff(c_37300,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_37296,c_36017]) ).
tff(c_37312,plain,
( ( unit = e3 )
| ( unit = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_37309,c_37300,c_162]) ).
tff(c_37313,plain,
unit = e2,
inference(splitLeft,[status(thm)],[c_37312]) ).
tff(c_37333,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_37313,c_174]) ).
tff(c_37341,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37302,c_37333]) ).
tff(c_37342,plain,
unit = e3,
inference(splitRight,[status(thm)],[c_37312]) ).
tff(c_37369,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_37342,c_37342,c_204]) ).
tff(c_37370,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35966,c_37369]) ).
tff(c_37372,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_37370]) ).
tff(c_37374,plain,
op(e0,e0) = e1,
inference(splitRight,[status(thm)],[c_896]) ).
tff(c_37376,plain,
op(e0,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_37374,c_304]) ).
tff(c_37389,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_37408,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_37389,c_174]) ).
tff(c_37416,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37376,c_37408]) ).
tff(c_37417,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_37419,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_37417]) ).
tff(c_37445,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_37419,c_37419,c_204]) ).
tff(c_37446,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35966,c_37445]) ).
tff(c_37448,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_37446]) ).
tff(c_37449,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_37417]) ).
tff(c_37451,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_37449]) ).
tff(c_37474,plain,
op(e2,e1) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_37451,c_168]) ).
tff(c_37526,plain,
op(e2,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_37474,c_274]) ).
tff(c_37385,plain,
op(e2,e2) != e1,
inference(splitLeft,[status(thm)],[c_898]) ).
tff(c_37472,plain,
op(e1,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_37451,c_174]) ).
tff(c_538,plain,
( ( op(e1,e1) = e0 )
| ( op(e2,e2) = e1 )
| ( op(e2,e2) = e2 )
| ( op(e2,e2) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_37813,plain,
( ( e1 = e0 )
| ( op(e2,e2) = e1 )
| ( op(e2,e2) = e2 )
| ( op(e2,e2) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_37472,c_538]) ).
tff(c_37814,plain,
op(e2,e2) = e3,
inference(negUnitSimplification,[status(thm)],[c_37526,c_37385,c_364,c_37813]) ).
tff(c_37464,plain,
op(e2,e3) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_37451,c_35968]) ).
tff(c_74,plain,
op(op(e2,e2),e3) = op(e2,op(e2,e3)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_37697,plain,
op(op(e2,e2),e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_37474,c_37464,c_74]) ).
tff(c_37819,plain,
op(e3,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_37814,c_37697]) ).
tff(c_782,plain,
( ( op(e3,e3) = e0 )
| ( op(e3,e3) = e1 )
| ( op(e2,e2) = e2 )
| ( op(e0,e0) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_628]) ).
tff(c_37888,plain,
( ( e2 = e0 )
| ( e2 = e1 )
| ( e3 = e2 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_37374,c_37814,c_37819,c_37819,c_782]) ).
tff(c_37889,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_354,c_358,c_362,c_37888]) ).
tff(c_37890,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_37449]) ).
tff(c_37918,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_37890,c_37890,c_204]) ).
tff(c_37924,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_37918,c_35965]) ).
tff(c_37926,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_37924]) ).
tff(c_37928,plain,
op(e2,e2) = e1,
inference(splitRight,[status(thm)],[c_898]) ).
tff(c_37934,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_37928,c_274]) ).
tff(c_37932,plain,
unit != e1,
inference(demodulation,[status(thm),theory(equality)],[c_37928,c_36017]) ).
tff(c_37939,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_37932,c_162]) ).
tff(c_37940,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_37939]) ).
tff(c_37959,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_37940,c_174]) ).
tff(c_37967,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37376,c_37959]) ).
tff(c_37968,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_37939]) ).
tff(c_37970,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_37968]) ).
tff(c_37996,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_37970,c_37970,c_204]) ).
tff(c_37997,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35966,c_37996]) ).
tff(c_37999,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_37997]) ).
tff(c_38000,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_37968]) ).
tff(c_38022,plain,
op(e2,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_38000,c_174]) ).
tff(c_38030,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37934,c_38022]) ).
tff(c_38032,plain,
inv(e1) = e0,
inference(splitRight,[status(thm)],[c_236]) ).
tff(c_38104,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_38129,plain,
inv(e0) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_38104,c_38104,c_204]) ).
tff(c_38031,plain,
inv(e0) = e1,
inference(splitRight,[status(thm)],[c_236]) ).
tff(c_38134,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_38129,c_38031]) ).
tff(c_38136,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_38134]) ).
tff(c_38137,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_38139,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_38137]) ).
tff(c_38165,plain,
inv(e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_38139,c_38139,c_204]) ).
tff(c_38166,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_35966,c_38165]) ).
tff(c_38168,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_38166]) ).
tff(c_38169,plain,
( ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_38137]) ).
tff(c_38173,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_38169]) ).
tff(c_38200,plain,
inv(e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_38173,c_38173,c_204]) ).
tff(c_38201,plain,
e1 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_38032,c_38200]) ).
tff(c_38203,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_364,c_38201]) ).
tff(c_38204,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_38169]) ).
tff(c_38232,plain,
inv(e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_38204,c_38204,c_204]) ).
tff(c_38238,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_38232,c_35965]) ).
tff(c_38240,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_38238]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ALG023+1 : TPTP v9.0.0. Released v2.7.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Apr 6 06:55:03 EDT 2025
% 0.13/0.34 % CPUTime :
% 23.01/9.67 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.43/9.86
% 23.43/9.86 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------