%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ALG061+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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 05:24:05 PM UTC 2025
% Result : Theorem 11.15s 3.52s
% Output : CNFRefutation 11.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 7
% Syntax : Number of formulae : 323 ( 236 unt; 0 typ; 0 def)
% Number of atoms : 1108 (1066 equ)
% Maximal formula atoms : 250 ( 3 avg)
% Number of connectives : 989 ( 204 ~; 557 |; 228 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ op > #nlpp > unit > e4 > e3 > e2 > e1 > e0
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(e1,type,
e1: $i ).
tff(e0,type,
e0: $i ).
tff(e2,type,
e2: $i ).
tff(op,type,
op: ( $i * $i ) > $i ).
tff(unit,type,
unit: $i ).
tff(e4,type,
e4: $i ).
tff(e3,type,
e3: $i ).
tff(f_1130,axiom,
( ( e0 != e1 )
& ( e0 != e2 )
& ( e0 != e3 )
& ( e0 != e4 )
& ( e1 != e2 )
& ( e1 != e3 )
& ( e1 != e4 )
& ( e2 != e3 )
& ( e2 != e4 )
& ( e3 != e4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
tff(f_1137,axiom,
( ( e0 = op(e1,op(op(e1,e1),op(e1,e1))) )
& ( e2 = op(op(e1,e1),op(e1,e1)) )
& ( e3 = op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) )
& ( e4 = op(e1,e1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
tff(f_1101,axiom,
( ( op(e0,e0) != op(e1,e0) )
& ( op(e0,e0) != op(e2,e0) )
& ( op(e0,e0) != op(e3,e0) )
& ( op(e0,e0) != op(e4,e0) )
& ( op(e1,e0) != op(e2,e0) )
& ( op(e1,e0) != op(e3,e0) )
& ( op(e1,e0) != op(e4,e0) )
& ( op(e2,e0) != op(e3,e0) )
& ( op(e2,e0) != op(e4,e0) )
& ( op(e3,e0) != op(e4,e0) )
& ( op(e0,e1) != op(e1,e1) )
& ( op(e0,e1) != op(e2,e1) )
& ( op(e0,e1) != op(e3,e1) )
& ( op(e0,e1) != op(e4,e1) )
& ( op(e1,e1) != op(e2,e1) )
& ( op(e1,e1) != op(e3,e1) )
& ( op(e1,e1) != op(e4,e1) )
& ( op(e2,e1) != op(e3,e1) )
& ( op(e2,e1) != op(e4,e1) )
& ( op(e3,e1) != op(e4,e1) )
& ( op(e0,e2) != op(e1,e2) )
& ( op(e0,e2) != op(e2,e2) )
& ( op(e0,e2) != op(e3,e2) )
& ( op(e0,e2) != op(e4,e2) )
& ( op(e1,e2) != op(e2,e2) )
& ( op(e1,e2) != op(e3,e2) )
& ( op(e1,e2) != op(e4,e2) )
& ( op(e2,e2) != op(e3,e2) )
& ( op(e2,e2) != op(e4,e2) )
& ( op(e3,e2) != op(e4,e2) )
& ( op(e0,e3) != op(e1,e3) )
& ( op(e0,e3) != op(e2,e3) )
& ( op(e0,e3) != op(e3,e3) )
& ( op(e0,e3) != op(e4,e3) )
& ( op(e1,e3) != op(e2,e3) )
& ( op(e1,e3) != op(e3,e3) )
& ( op(e1,e3) != op(e4,e3) )
& ( op(e2,e3) != op(e3,e3) )
& ( op(e2,e3) != op(e4,e3) )
& ( op(e3,e3) != op(e4,e3) )
& ( op(e0,e4) != op(e1,e4) )
& ( op(e0,e4) != op(e2,e4) )
& ( op(e0,e4) != op(e3,e4) )
& ( op(e0,e4) != op(e4,e4) )
& ( op(e1,e4) != op(e2,e4) )
& ( op(e1,e4) != op(e3,e4) )
& ( op(e1,e4) != op(e4,e4) )
& ( op(e2,e4) != op(e3,e4) )
& ( op(e2,e4) != op(e4,e4) )
& ( op(e3,e4) != op(e4,e4) )
& ( op(e0,e0) != op(e0,e1) )
& ( op(e0,e0) != op(e0,e2) )
& ( op(e0,e0) != op(e0,e3) )
& ( op(e0,e0) != op(e0,e4) )
& ( op(e0,e1) != op(e0,e2) )
& ( op(e0,e1) != op(e0,e3) )
& ( op(e0,e1) != op(e0,e4) )
& ( op(e0,e2) != op(e0,e3) )
& ( op(e0,e2) != op(e0,e4) )
& ( op(e0,e3) != op(e0,e4) )
& ( op(e1,e0) != op(e1,e1) )
& ( op(e1,e0) != op(e1,e2) )
& ( op(e1,e0) != op(e1,e3) )
& ( op(e1,e0) != op(e1,e4) )
& ( op(e1,e1) != op(e1,e2) )
& ( op(e1,e1) != op(e1,e3) )
& ( op(e1,e1) != op(e1,e4) )
& ( op(e1,e2) != op(e1,e3) )
& ( op(e1,e2) != op(e1,e4) )
& ( op(e1,e3) != op(e1,e4) )
& ( op(e2,e0) != op(e2,e1) )
& ( op(e2,e0) != op(e2,e2) )
& ( op(e2,e0) != op(e2,e3) )
& ( op(e2,e0) != op(e2,e4) )
& ( op(e2,e1) != op(e2,e2) )
& ( op(e2,e1) != op(e2,e3) )
& ( op(e2,e1) != op(e2,e4) )
& ( op(e2,e2) != op(e2,e3) )
& ( op(e2,e2) != op(e2,e4) )
& ( op(e2,e3) != op(e2,e4) )
& ( op(e3,e0) != op(e3,e1) )
& ( op(e3,e0) != op(e3,e2) )
& ( op(e3,e0) != op(e3,e3) )
& ( op(e3,e0) != op(e3,e4) )
& ( op(e3,e1) != op(e3,e2) )
& ( op(e3,e1) != op(e3,e3) )
& ( op(e3,e1) != op(e3,e4) )
& ( op(e3,e2) != op(e3,e3) )
& ( op(e3,e2) != op(e3,e4) )
& ( op(e3,e3) != op(e3,e4) )
& ( op(e4,e0) != op(e4,e1) )
& ( op(e4,e0) != op(e4,e2) )
& ( op(e4,e0) != op(e4,e3) )
& ( op(e4,e0) != op(e4,e4) )
& ( op(e4,e1) != op(e4,e2) )
& ( op(e4,e1) != op(e4,e3) )
& ( op(e4,e1) != op(e4,e4) )
& ( op(e4,e2) != op(e4,e3) )
& ( op(e4,e2) != op(e4,e4) )
& ( op(e4,e3) != op(e4,e4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
tff(f_274,axiom,
( ( ( op(e0,e0) = e0 )
| ( op(e0,e0) = e1 )
| ( op(e0,e0) = e2 )
| ( op(e0,e0) = e3 )
| ( op(e0,e0) = e4 ) )
& ( ( op(e0,e1) = e0 )
| ( op(e0,e1) = e1 )
| ( op(e0,e1) = e2 )
| ( op(e0,e1) = e3 )
| ( op(e0,e1) = e4 ) )
& ( ( op(e0,e2) = e0 )
| ( op(e0,e2) = e1 )
| ( op(e0,e2) = e2 )
| ( op(e0,e2) = e3 )
| ( op(e0,e2) = e4 ) )
& ( ( op(e0,e3) = e0 )
| ( op(e0,e3) = e1 )
| ( op(e0,e3) = e2 )
| ( op(e0,e3) = e3 )
| ( op(e0,e3) = e4 ) )
& ( ( op(e0,e4) = e0 )
| ( op(e0,e4) = e1 )
| ( op(e0,e4) = e2 )
| ( op(e0,e4) = e3 )
| ( op(e0,e4) = e4 ) )
& ( ( op(e1,e0) = e0 )
| ( op(e1,e0) = e1 )
| ( op(e1,e0) = e2 )
| ( op(e1,e0) = e3 )
| ( op(e1,e0) = e4 ) )
& ( ( op(e1,e1) = e0 )
| ( op(e1,e1) = e1 )
| ( op(e1,e1) = e2 )
| ( op(e1,e1) = e3 )
| ( op(e1,e1) = e4 ) )
& ( ( op(e1,e2) = e0 )
| ( op(e1,e2) = e1 )
| ( op(e1,e2) = e2 )
| ( op(e1,e2) = e3 )
| ( op(e1,e2) = e4 ) )
& ( ( op(e1,e3) = e0 )
| ( op(e1,e3) = e1 )
| ( op(e1,e3) = e2 )
| ( op(e1,e3) = e3 )
| ( op(e1,e3) = e4 ) )
& ( ( op(e1,e4) = e0 )
| ( op(e1,e4) = e1 )
| ( op(e1,e4) = e2 )
| ( op(e1,e4) = e3 )
| ( op(e1,e4) = e4 ) )
& ( ( op(e2,e0) = e0 )
| ( op(e2,e0) = e1 )
| ( op(e2,e0) = e2 )
| ( op(e2,e0) = e3 )
| ( op(e2,e0) = e4 ) )
& ( ( op(e2,e1) = e0 )
| ( op(e2,e1) = e1 )
| ( op(e2,e1) = e2 )
| ( op(e2,e1) = e3 )
| ( op(e2,e1) = e4 ) )
& ( ( op(e2,e2) = e0 )
| ( op(e2,e2) = e1 )
| ( op(e2,e2) = e2 )
| ( op(e2,e2) = e3 )
| ( op(e2,e2) = e4 ) )
& ( ( op(e2,e3) = e0 )
| ( op(e2,e3) = e1 )
| ( op(e2,e3) = e2 )
| ( op(e2,e3) = e3 )
| ( op(e2,e3) = e4 ) )
& ( ( op(e2,e4) = e0 )
| ( op(e2,e4) = e1 )
| ( op(e2,e4) = e2 )
| ( op(e2,e4) = e3 )
| ( op(e2,e4) = e4 ) )
& ( ( op(e3,e0) = e0 )
| ( op(e3,e0) = e1 )
| ( op(e3,e0) = e2 )
| ( op(e3,e0) = e3 )
| ( op(e3,e0) = e4 ) )
& ( ( op(e3,e1) = e0 )
| ( op(e3,e1) = e1 )
| ( op(e3,e1) = e2 )
| ( op(e3,e1) = e3 )
| ( op(e3,e1) = e4 ) )
& ( ( op(e3,e2) = e0 )
| ( op(e3,e2) = e1 )
| ( op(e3,e2) = e2 )
| ( op(e3,e2) = e3 )
| ( op(e3,e2) = e4 ) )
& ( ( op(e3,e3) = e0 )
| ( op(e3,e3) = e1 )
| ( op(e3,e3) = e2 )
| ( op(e3,e3) = e3 )
| ( op(e3,e3) = e4 ) )
& ( ( op(e3,e4) = e0 )
| ( op(e3,e4) = e1 )
| ( op(e3,e4) = e2 )
| ( op(e3,e4) = e3 )
| ( op(e3,e4) = e4 ) )
& ( ( op(e4,e0) = e0 )
| ( op(e4,e0) = e1 )
| ( op(e4,e0) = e2 )
| ( op(e4,e0) = e3 )
| ( op(e4,e0) = e4 ) )
& ( ( op(e4,e1) = e0 )
| ( op(e4,e1) = e1 )
| ( op(e4,e1) = e2 )
| ( op(e4,e1) = e3 )
| ( op(e4,e1) = e4 ) )
& ( ( op(e4,e2) = e0 )
| ( op(e4,e2) = e1 )
| ( op(e4,e2) = e2 )
| ( op(e4,e2) = e3 )
| ( op(e4,e2) = e4 ) )
& ( ( op(e4,e3) = e0 )
| ( op(e4,e3) = e1 )
| ( op(e4,e3) = e2 )
| ( op(e4,e3) = e3 )
| ( op(e4,e3) = e4 ) )
& ( ( op(e4,e4) = e0 )
| ( op(e4,e4) = e1 )
| ( op(e4,e4) = e2 )
| ( op(e4,e4) = e3 )
| ( op(e4,e4) = e4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
tff(f_1313,negated_conjecture,
~ ~ ( ( ( op(e0,e0) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e3,e3) = e0 )
| ( op(e4,e4) = e0 ) )
& ( ( op(e0,e0) = e1 )
| ( op(e1,e1) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e3,e3) = e1 )
| ( op(e4,e4) = e1 ) )
& ( ( op(e0,e0) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e2,e2) = e2 )
| ( op(e3,e3) = e2 )
| ( op(e4,e4) = e2 ) )
& ( ( op(e0,e0) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e3,e3) = e3 )
| ( op(e4,e4) = e3 ) )
& ( ( op(e0,e0) = e4 )
| ( op(e1,e1) = e4 )
| ( op(e2,e2) = e4 )
| ( op(e3,e3) = e4 )
| ( op(e4,e4) = e4 ) )
& ( ( ( op(e0,op(e0,e0)) != e0 )
& ( op(e0,op(e0,e0)) = e0 ) )
| ( ( op(e1,op(e1,e0)) != e0 )
& ( op(e0,op(e1,e0)) = e1 ) )
| ( ( op(e2,op(e2,e0)) != e0 )
& ( op(e0,op(e2,e0)) = e2 ) )
| ( ( op(e3,op(e3,e0)) != e0 )
& ( op(e0,op(e3,e0)) = e3 ) )
| ( ( op(e4,op(e4,e0)) != e0 )
& ( op(e0,op(e4,e0)) = e4 ) ) )
& ( ( ( op(e0,op(e0,e1)) != e1 )
& ( op(e1,op(e0,e1)) = e0 ) )
| ( ( op(e1,op(e1,e1)) != e1 )
& ( op(e1,op(e1,e1)) = e1 ) )
| ( ( op(e2,op(e2,e1)) != e1 )
& ( op(e1,op(e2,e1)) = e2 ) )
| ( ( op(e3,op(e3,e1)) != e1 )
& ( op(e1,op(e3,e1)) = e3 ) )
| ( ( op(e4,op(e4,e1)) != e1 )
& ( op(e1,op(e4,e1)) = e4 ) ) )
& ( ( ( op(e0,op(e0,e2)) != e2 )
& ( op(e2,op(e0,e2)) = e0 ) )
| ( ( op(e1,op(e1,e2)) != e2 )
& ( op(e2,op(e1,e2)) = e1 ) )
| ( ( op(e2,op(e2,e2)) != e2 )
& ( op(e2,op(e2,e2)) = e2 ) )
| ( ( op(e3,op(e3,e2)) != e2 )
& ( op(e2,op(e3,e2)) = e3 ) )
| ( ( op(e4,op(e4,e2)) != e2 )
& ( op(e2,op(e4,e2)) = e4 ) ) )
& ( ( ( op(e0,op(e0,e3)) != e3 )
& ( op(e3,op(e0,e3)) = e0 ) )
| ( ( op(e1,op(e1,e3)) != e3 )
& ( op(e3,op(e1,e3)) = e1 ) )
| ( ( op(e2,op(e2,e3)) != e3 )
& ( op(e3,op(e2,e3)) = e2 ) )
| ( ( op(e3,op(e3,e3)) != e3 )
& ( op(e3,op(e3,e3)) = e3 ) )
| ( ( op(e4,op(e4,e3)) != e3 )
& ( op(e3,op(e4,e3)) = e4 ) ) )
& ( ( ( op(e0,op(e0,e4)) != e4 )
& ( op(e4,op(e0,e4)) = e0 ) )
| ( ( op(e1,op(e1,e4)) != e4 )
& ( op(e4,op(e1,e4)) = e1 ) )
| ( ( op(e2,op(e2,e4)) != e4 )
& ( op(e4,op(e2,e4)) = e2 ) )
| ( ( op(e3,op(e3,e4)) != e4 )
& ( op(e4,op(e3,e4)) = e3 ) )
| ( ( op(e4,op(e4,e4)) != e4 )
& ( op(e4,op(e4,e4)) = e4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
tff(f_802,axiom,
( ( ( op(e0,e0) = e0 )
| ( op(e0,e1) = e0 )
| ( op(e0,e2) = e0 )
| ( op(e0,e3) = e0 )
| ( op(e0,e4) = e0 ) )
& ( ( op(e0,e0) = e0 )
| ( op(e1,e0) = e0 )
| ( op(e2,e0) = e0 )
| ( op(e3,e0) = e0 )
| ( op(e4,e0) = e0 ) )
& ( ( op(e0,e0) = e1 )
| ( op(e0,e1) = e1 )
| ( op(e0,e2) = e1 )
| ( op(e0,e3) = e1 )
| ( op(e0,e4) = e1 ) )
& ( ( op(e0,e0) = e1 )
| ( op(e1,e0) = e1 )
| ( op(e2,e0) = e1 )
| ( op(e3,e0) = e1 )
| ( op(e4,e0) = e1 ) )
& ( ( op(e0,e0) = e2 )
| ( op(e0,e1) = e2 )
| ( op(e0,e2) = e2 )
| ( op(e0,e3) = e2 )
| ( op(e0,e4) = e2 ) )
& ( ( op(e0,e0) = e2 )
| ( op(e1,e0) = e2 )
| ( op(e2,e0) = e2 )
| ( op(e3,e0) = e2 )
| ( op(e4,e0) = e2 ) )
& ( ( op(e0,e0) = e3 )
| ( op(e0,e1) = e3 )
| ( op(e0,e2) = e3 )
| ( op(e0,e3) = e3 )
| ( op(e0,e4) = e3 ) )
& ( ( op(e0,e0) = e3 )
| ( op(e1,e0) = e3 )
| ( op(e2,e0) = e3 )
| ( op(e3,e0) = e3 )
| ( op(e4,e0) = e3 ) )
& ( ( op(e0,e0) = e4 )
| ( op(e0,e1) = e4 )
| ( op(e0,e2) = e4 )
| ( op(e0,e3) = e4 )
| ( op(e0,e4) = e4 ) )
& ( ( op(e0,e0) = e4 )
| ( op(e1,e0) = e4 )
| ( op(e2,e0) = e4 )
| ( op(e3,e0) = e4 )
| ( op(e4,e0) = e4 ) )
& ( ( op(e1,e0) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e1,e2) = e0 )
| ( op(e1,e3) = e0 )
| ( op(e1,e4) = e0 ) )
& ( ( op(e0,e1) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e2,e1) = e0 )
| ( op(e3,e1) = e0 )
| ( op(e4,e1) = e0 ) )
& ( ( op(e1,e0) = e1 )
| ( op(e1,e1) = e1 )
| ( op(e1,e2) = e1 )
| ( op(e1,e3) = e1 )
| ( op(e1,e4) = e1 ) )
& ( ( op(e0,e1) = e1 )
| ( op(e1,e1) = e1 )
| ( op(e2,e1) = e1 )
| ( op(e3,e1) = e1 )
| ( op(e4,e1) = e1 ) )
& ( ( op(e1,e0) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e1,e2) = e2 )
| ( op(e1,e3) = e2 )
| ( op(e1,e4) = e2 ) )
& ( ( op(e0,e1) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e2,e1) = e2 )
| ( op(e3,e1) = e2 )
| ( op(e4,e1) = e2 ) )
& ( ( op(e1,e0) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e1,e2) = e3 )
| ( op(e1,e3) = e3 )
| ( op(e1,e4) = e3 ) )
& ( ( op(e0,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e3,e1) = e3 )
| ( op(e4,e1) = e3 ) )
& ( ( op(e1,e0) = e4 )
| ( op(e1,e1) = e4 )
| ( op(e1,e2) = e4 )
| ( op(e1,e3) = e4 )
| ( op(e1,e4) = e4 ) )
& ( ( op(e0,e1) = e4 )
| ( op(e1,e1) = e4 )
| ( op(e2,e1) = e4 )
| ( op(e3,e1) = e4 )
| ( op(e4,e1) = e4 ) )
& ( ( op(e2,e0) = e0 )
| ( op(e2,e1) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e2,e3) = e0 )
| ( op(e2,e4) = e0 ) )
& ( ( op(e0,e2) = e0 )
| ( op(e1,e2) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e3,e2) = e0 )
| ( op(e4,e2) = e0 ) )
& ( ( op(e2,e0) = e1 )
| ( op(e2,e1) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e2,e3) = e1 )
| ( op(e2,e4) = e1 ) )
& ( ( op(e0,e2) = e1 )
| ( op(e1,e2) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e3,e2) = e1 )
| ( op(e4,e2) = e1 ) )
& ( ( op(e2,e0) = e2 )
| ( op(e2,e1) = e2 )
| ( op(e2,e2) = e2 )
| ( op(e2,e3) = e2 )
| ( op(e2,e4) = e2 ) )
& ( ( op(e0,e2) = e2 )
| ( op(e1,e2) = e2 )
| ( op(e2,e2) = e2 )
| ( op(e3,e2) = e2 )
| ( op(e4,e2) = e2 ) )
& ( ( op(e2,e0) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e2,e3) = e3 )
| ( op(e2,e4) = e3 ) )
& ( ( op(e0,e2) = e3 )
| ( op(e1,e2) = e3 )
| ( op(e2,e2) = e3 )
| ( op(e3,e2) = e3 )
| ( op(e4,e2) = e3 ) )
& ( ( op(e2,e0) = e4 )
| ( op(e2,e1) = e4 )
| ( op(e2,e2) = e4 )
| ( op(e2,e3) = e4 )
| ( op(e2,e4) = e4 ) )
& ( ( op(e0,e2) = e4 )
| ( op(e1,e2) = e4 )
| ( op(e2,e2) = e4 )
| ( op(e3,e2) = e4 )
| ( op(e4,e2) = e4 ) )
& ( ( op(e3,e0) = e0 )
| ( op(e3,e1) = e0 )
| ( op(e3,e2) = e0 )
| ( op(e3,e3) = e0 )
| ( op(e3,e4) = e0 ) )
& ( ( op(e0,e3) = e0 )
| ( op(e1,e3) = e0 )
| ( op(e2,e3) = e0 )
| ( op(e3,e3) = e0 )
| ( op(e4,e3) = e0 ) )
& ( ( op(e3,e0) = e1 )
| ( op(e3,e1) = e1 )
| ( op(e3,e2) = e1 )
| ( op(e3,e3) = e1 )
| ( op(e3,e4) = e1 ) )
& ( ( op(e0,e3) = e1 )
| ( op(e1,e3) = e1 )
| ( op(e2,e3) = e1 )
| ( op(e3,e3) = e1 )
| ( op(e4,e3) = e1 ) )
& ( ( op(e3,e0) = e2 )
| ( op(e3,e1) = e2 )
| ( op(e3,e2) = e2 )
| ( op(e3,e3) = e2 )
| ( op(e3,e4) = e2 ) )
& ( ( op(e0,e3) = e2 )
| ( op(e1,e3) = e2 )
| ( op(e2,e3) = e2 )
| ( op(e3,e3) = e2 )
| ( op(e4,e3) = e2 ) )
& ( ( op(e3,e0) = e3 )
| ( op(e3,e1) = e3 )
| ( op(e3,e2) = e3 )
| ( op(e3,e3) = e3 )
| ( op(e3,e4) = e3 ) )
& ( ( op(e0,e3) = e3 )
| ( op(e1,e3) = e3 )
| ( op(e2,e3) = e3 )
| ( op(e3,e3) = e3 )
| ( op(e4,e3) = e3 ) )
& ( ( op(e3,e0) = e4 )
| ( op(e3,e1) = e4 )
| ( op(e3,e2) = e4 )
| ( op(e3,e3) = e4 )
| ( op(e3,e4) = e4 ) )
& ( ( op(e0,e3) = e4 )
| ( op(e1,e3) = e4 )
| ( op(e2,e3) = e4 )
| ( op(e3,e3) = e4 )
| ( op(e4,e3) = e4 ) )
& ( ( op(e4,e0) = e0 )
| ( op(e4,e1) = e0 )
| ( op(e4,e2) = e0 )
| ( op(e4,e3) = e0 )
| ( op(e4,e4) = e0 ) )
& ( ( op(e0,e4) = e0 )
| ( op(e1,e4) = e0 )
| ( op(e2,e4) = e0 )
| ( op(e3,e4) = e0 )
| ( op(e4,e4) = e0 ) )
& ( ( op(e4,e0) = e1 )
| ( op(e4,e1) = e1 )
| ( op(e4,e2) = e1 )
| ( op(e4,e3) = e1 )
| ( op(e4,e4) = e1 ) )
& ( ( op(e0,e4) = e1 )
| ( op(e1,e4) = e1 )
| ( op(e2,e4) = e1 )
| ( op(e3,e4) = e1 )
| ( op(e4,e4) = e1 ) )
& ( ( op(e4,e0) = e2 )
| ( op(e4,e1) = e2 )
| ( op(e4,e2) = e2 )
| ( op(e4,e3) = e2 )
| ( op(e4,e4) = e2 ) )
& ( ( op(e0,e4) = e2 )
| ( op(e1,e4) = e2 )
| ( op(e2,e4) = e2 )
| ( op(e3,e4) = e2 )
| ( op(e4,e4) = e2 ) )
& ( ( op(e4,e0) = e3 )
| ( op(e4,e1) = e3 )
| ( op(e4,e2) = e3 )
| ( op(e4,e3) = e3 )
| ( op(e4,e4) = e3 ) )
& ( ( op(e0,e4) = e3 )
| ( op(e1,e4) = e3 )
| ( op(e2,e4) = e3 )
| ( op(e3,e4) = e3 )
| ( op(e4,e4) = e3 ) )
& ( ( op(e4,e0) = e4 )
| ( op(e4,e1) = e4 )
| ( op(e4,e2) = e4 )
| ( op(e4,e3) = e4 )
| ( op(e4,e4) = e4 ) )
& ( ( op(e0,e4) = e4 )
| ( op(e1,e4) = e4 )
| ( op(e2,e4) = e4 )
| ( op(e3,e4) = e4 )
| ( op(e4,e4) = e4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
tff(f_303,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 )
& ( op(unit,e4) = e4 )
& ( op(e4,unit) = e4 )
& ( ( unit = e0 )
| ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
tff(c_378,plain,
e3 != e2,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_398,plain,
op(op(e1,e1),op(e1,e1)) = e2,
inference(cnfTransformation,[status(thm)],[f_1137]) ).
tff(c_396,plain,
op(op(op(e1,e1),op(e1,e1)),op(op(e1,e1),op(e1,e1))) = e3,
inference(cnfTransformation,[status(thm)],[f_1137]) ).
tff(c_764,plain,
op(e2,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_398,c_398,c_396]) ).
tff(c_318,plain,
op(e3,e2) != op(e2,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_889,plain,
op(e3,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_764,c_318]) ).
tff(c_380,plain,
e4 != e1,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_400,plain,
op(e1,op(op(e1,e1),op(e1,e1))) = e0,
inference(cnfTransformation,[status(thm)],[f_1137]) ).
tff(c_731,plain,
op(e1,e2) = e0,
inference(demodulation,[status(thm),theory(equality)],[c_398,c_400]) ).
tff(c_320,plain,
op(e4,e2) != op(e1,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_888,plain,
op(e4,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_731,c_320]) ).
tff(c_394,plain,
op(e1,e1) = e4,
inference(cnfTransformation,[status(thm)],[f_1137]) ).
tff(c_802,plain,
op(e4,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_394,c_394,c_398]) ).
tff(c_176,plain,
op(e4,e4) != op(e4,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_908,plain,
op(e4,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_802,c_176]) ).
tff(c_316,plain,
op(e4,e2) != op(e2,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_890,plain,
op(e4,e2) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_764,c_316]) ).
tff(c_6,plain,
( ( op(e4,e2) = e4 )
| ( op(e4,e2) = e3 )
| ( op(e4,e2) = e2 )
| ( op(e4,e2) = e1 )
| ( op(e4,e2) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_1007,plain,
( ( op(e4,e2) = e4 )
| ( op(e4,e2) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_888,c_908,c_890,c_6]) ).
tff(c_1151,plain,
op(e4,e2) = e1,
inference(splitLeft,[status(thm)],[c_1007]) ).
tff(c_388,plain,
e3 != e0,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_392,plain,
e1 != e0,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_382,plain,
e3 != e1,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_384,plain,
e2 != e1,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_408,plain,
( ( op(e4,e4) = e1 )
| ( op(e3,e3) = e1 )
| ( op(e2,e2) = e1 )
| ( op(e1,e1) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(cnfTransformation,[status(thm)],[f_1313]) ).
tff(c_766,plain,
( ( op(e4,e4) = e1 )
| ( op(e3,e3) = e1 )
| ( e3 = e1 )
| ( op(e1,e1) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_764,c_408]) ).
tff(c_804,plain,
( ( op(e4,e4) = e1 )
| ( op(e3,e3) = e1 )
| ( e3 = e1 )
| ( e4 = e1 )
| ( op(e0,e0) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_394,c_766]) ).
tff(c_872,plain,
( ( e2 = e1 )
| ( op(e3,e3) = e1 )
| ( e3 = e1 )
| ( e4 = e1 )
| ( op(e0,e0) = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_802,c_804]) ).
tff(c_877,plain,
( ( op(e3,e3) = e1 )
| ( e3 = e1 )
| ( e4 = e1 )
| ( op(e0,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_384,c_872]) ).
tff(c_878,plain,
( ( op(e3,e3) = e1 )
| ( e4 = e1 )
| ( op(e0,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_382,c_877]) ).
tff(c_879,plain,
( ( op(e3,e3) = e1 )
| ( op(e0,e0) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_380,c_878]) ).
tff(c_1082,plain,
op(e0,e0) = e1,
inference(splitLeft,[status(thm)],[c_879]) ).
tff(c_386,plain,
e4 != e0,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_390,plain,
e2 != e0,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_410,plain,
( ( op(e4,e4) = e0 )
| ( op(e3,e3) = e0 )
| ( op(e2,e2) = e0 )
| ( op(e1,e1) = e0 )
| ( op(e0,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_1313]) ).
tff(c_765,plain,
( ( op(e4,e4) = e0 )
| ( op(e3,e3) = e0 )
| ( e3 = e0 )
| ( op(e1,e1) = e0 )
| ( op(e0,e0) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_764,c_410]) ).
tff(c_803,plain,
( ( op(e4,e4) = e0 )
| ( op(e3,e3) = e0 )
| ( e3 = e0 )
| ( e4 = e0 )
| ( op(e0,e0) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_394,c_765]) ).
tff(c_871,plain,
( ( e2 = e0 )
| ( op(e3,e3) = e0 )
| ( e3 = e0 )
| ( e4 = e0 )
| ( op(e0,e0) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_802,c_803]) ).
tff(c_874,plain,
( ( op(e3,e3) = e0 )
| ( e3 = e0 )
| ( e4 = e0 )
| ( op(e0,e0) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_390,c_871]) ).
tff(c_875,plain,
( ( op(e3,e3) = e0 )
| ( e4 = e0 )
| ( op(e0,e0) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_388,c_874]) ).
tff(c_876,plain,
( ( op(e3,e3) = e0 )
| ( op(e0,e0) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_386,c_875]) ).
tff(c_1095,plain,
( ( op(e3,e3) = e0 )
| ( e1 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1082,c_876]) ).
tff(c_1096,plain,
op(e3,e3) = e0,
inference(negUnitSimplification,[status(thm)],[c_392,c_1095]) ).
tff(c_340,plain,
op(e4,e1) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_883,plain,
op(e4,e1) != e4,
inference(demodulation,[status(thm),theory(equality)],[c_394,c_340]) ).
tff(c_276,plain,
op(e4,e4) != op(e2,e4),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_893,plain,
op(e2,e4) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_802,c_276]) ).
tff(c_376,plain,
e4 != e2,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_280,plain,
op(e4,e4) != op(e1,e4),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_892,plain,
op(e1,e4) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_802,c_280]) ).
tff(c_144,plain,
( ( op(e1,e4) = e2 )
| ( op(e1,e3) = e2 )
| ( op(e1,e2) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e1,e0) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_802]) ).
tff(c_926,plain,
( ( op(e1,e4) = e2 )
| ( op(e1,e3) = e2 )
| ( e2 = e0 )
| ( e4 = e2 )
| ( op(e1,e0) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_394,c_731,c_144]) ).
tff(c_927,plain,
( ( op(e1,e3) = e2 )
| ( op(e1,e0) = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_376,c_390,c_892,c_926]) ).
tff(c_1111,plain,
op(e1,e0) = e2,
inference(splitLeft,[status(thm)],[c_927]) ).
tff(c_364,plain,
op(e2,e0) != op(e1,e0),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_1117,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_1111,c_364]) ).
tff(c_52,plain,
( ( unit = e4 )
| ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_1165,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_62,plain,
op(e2,unit) = e2,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_1166,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1165,c_62]) ).
tff(c_1177,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1117,c_1166]) ).
tff(c_1178,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_1180,plain,
unit = e4,
inference(splitLeft,[status(thm)],[c_1178]) ).
tff(c_1182,plain,
op(e2,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1180,c_62]) ).
tff(c_1193,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_893,c_1182]) ).
tff(c_1194,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_1178]) ).
tff(c_1198,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_1194]) ).
tff(c_54,plain,
op(e4,unit) = e4,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_1203,plain,
op(e4,e1) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_1198,c_54]) ).
tff(c_1212,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_883,c_1203]) ).
tff(c_1213,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_1194]) ).
tff(c_1215,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_1213]) ).
tff(c_58,plain,
op(e3,unit) = e3,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_1223,plain,
op(e3,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_1215,c_58]) ).
tff(c_1229,plain,
e3 = e0,
inference(demodulation,[status(thm),theory(equality)],[c_1096,c_1223]) ).
tff(c_1231,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_388,c_1229]) ).
tff(c_1232,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_1213]) ).
tff(c_1240,plain,
op(e4,e2) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_1232,c_54]) ).
tff(c_1248,plain,
e4 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_1151,c_1240]) ).
tff(c_1250,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_380,c_1248]) ).
tff(c_1251,plain,
op(e4,e2) = e4,
inference(splitRight,[status(thm)],[c_1007]) ).
tff(c_178,plain,
op(e4,e3) != op(e4,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_1254,plain,
op(e4,e3) != e4,
inference(demodulation,[status(thm),theory(equality)],[c_1251,c_178]) ).
tff(c_1267,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_1268,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1267,c_62]) ).
tff(c_1279,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1117,c_1268]) ).
tff(c_1280,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_1282,plain,
unit = e4,
inference(splitLeft,[status(thm)],[c_1280]) ).
tff(c_1284,plain,
op(e2,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1282,c_62]) ).
tff(c_1295,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_893,c_1284]) ).
tff(c_1296,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_1280]) ).
tff(c_1300,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_1296]) ).
tff(c_1305,plain,
op(e4,e1) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_1300,c_54]) ).
tff(c_1314,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_883,c_1305]) ).
tff(c_1315,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_1296]) ).
tff(c_1317,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_1315]) ).
tff(c_1323,plain,
op(e4,e3) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_1317,c_54]) ).
tff(c_1332,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1254,c_1323]) ).
tff(c_1333,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_1315]) ).
tff(c_1342,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_1333,c_58]) ).
tff(c_1350,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_889,c_1342]) ).
tff(c_1351,plain,
op(e1,e3) = e2,
inference(splitRight,[status(thm)],[c_927]) ).
tff(c_304,plain,
op(e2,e3) != op(e1,e3),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_1357,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_1351,c_304]) ).
tff(c_272,plain,
op(e0,e1) != op(e0,e0),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_1086,plain,
op(e0,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_1082,c_272]) ).
tff(c_1504,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_68,plain,
op(unit,e1) = e1,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_1506,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_1504,c_68]) ).
tff(c_1516,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1086,c_1506]) ).
tff(c_1517,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_1519,plain,
unit = e4,
inference(splitLeft,[status(thm)],[c_1517]) ).
tff(c_1522,plain,
op(e2,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1519,c_62]) ).
tff(c_1533,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_893,c_1522]) ).
tff(c_1534,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_1517]) ).
tff(c_1536,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_1534]) ).
tff(c_1541,plain,
op(e4,e1) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_1536,c_54]) ).
tff(c_1550,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_883,c_1541]) ).
tff(c_1551,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_1534]) ).
tff(c_1553,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_1551]) ).
tff(c_1557,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1553,c_62]) ).
tff(c_1568,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1357,c_1557]) ).
tff(c_1569,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_1551]) ).
tff(c_1578,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_1569,c_58]) ).
tff(c_1586,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_889,c_1578]) ).
tff(c_1587,plain,
op(e3,e3) = e1,
inference(splitRight,[status(thm)],[c_879]) ).
tff(c_202,plain,
op(e3,e3) != op(e3,e1),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_1596,plain,
op(e3,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_1587,c_202]) ).
tff(c_1604,plain,
op(e1,e0) = e2,
inference(splitLeft,[status(thm)],[c_927]) ).
tff(c_1609,plain,
op(e2,e0) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_1604,c_364]) ).
tff(c_1781,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_1782,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1781,c_62]) ).
tff(c_1793,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1609,c_1782]) ).
tff(c_1794,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_1796,plain,
unit = e4,
inference(splitLeft,[status(thm)],[c_1794]) ).
tff(c_1798,plain,
op(e2,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1796,c_62]) ).
tff(c_1809,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_893,c_1798]) ).
tff(c_1810,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_1794]) ).
tff(c_1812,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_1810]) ).
tff(c_1818,plain,
op(e4,e1) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_1812,c_54]) ).
tff(c_1827,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_883,c_1818]) ).
tff(c_1828,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_1810]) ).
tff(c_1830,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_1828]) ).
tff(c_1835,plain,
op(e3,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_1830,c_68]) ).
tff(c_1845,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1596,c_1835]) ).
tff(c_1846,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_1828]) ).
tff(c_1856,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_1846,c_58]) ).
tff(c_1864,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_889,c_1856]) ).
tff(c_1865,plain,
op(e1,e3) = e2,
inference(splitRight,[status(thm)],[c_927]) ).
tff(c_1872,plain,
op(e2,e3) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_1865,c_304]) ).
tff(c_1911,plain,
op(e4,e2) = e1,
inference(splitLeft,[status(thm)],[c_1007]) ).
tff(c_374,plain,
e4 != e3,
inference(cnfTransformation,[status(thm)],[f_1130]) ).
tff(c_2038,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_2043,plain,
op(e3,e0) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_2038,c_58]) ).
tff(c_2041,plain,
op(e4,e0) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2038,c_54]) ).
tff(c_2040,plain,
op(e0,e1) = e1,
inference(demodulation,[status(thm),theory(equality)],[c_2038,c_68]) ).
tff(c_2039,plain,
op(e2,e0) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2038,c_62]) ).
tff(c_232,plain,
op(e2,e1) != op(e2,e0),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_2058,plain,
op(e2,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_2039,c_232]) ).
tff(c_180,plain,
op(e4,e4) != op(e4,e1),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_907,plain,
op(e4,e1) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_802,c_180]) ).
tff(c_142,plain,
( ( op(e4,e1) = e2 )
| ( op(e3,e1) = e2 )
| ( op(e2,e1) = e2 )
| ( op(e1,e1) = e2 )
| ( op(e0,e1) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_802]) ).
tff(c_928,plain,
( ( op(e4,e1) = e2 )
| ( op(e3,e1) = e2 )
| ( op(e2,e1) = e2 )
| ( e4 = e2 )
| ( op(e0,e1) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_394,c_142]) ).
tff(c_929,plain,
( ( op(e3,e1) = e2 )
| ( op(e2,e1) = e2 )
| ( op(e0,e1) = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_376,c_907,c_928]) ).
tff(c_2141,plain,
( ( op(e3,e1) = e2 )
| ( op(e2,e1) = e2 )
| ( e2 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2040,c_929]) ).
tff(c_2142,plain,
op(e3,e1) = e2,
inference(negUnitSimplification,[status(thm)],[c_384,c_2058,c_2141]) ).
tff(c_184,plain,
op(e4,e2) != op(e4,e1),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_1914,plain,
op(e4,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_1911,c_184]) ).
tff(c_8,plain,
( ( op(e4,e1) = e4 )
| ( op(e4,e1) = e3 )
| ( op(e4,e1) = e2 )
| ( op(e4,e1) = e1 )
| ( op(e4,e1) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_1006,plain,
( ( op(e4,e1) = e3 )
| ( op(e4,e1) = e1 )
| ( op(e4,e1) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_907,c_883,c_8]) ).
tff(c_2154,plain,
( ( op(e4,e1) = e3 )
| ( op(e4,e1) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_1914,c_1006]) ).
tff(c_2155,plain,
op(e4,e1) = e0,
inference(splitLeft,[status(thm)],[c_2154]) ).
tff(c_224,plain,
op(e2,e2) != op(e2,e1),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_903,plain,
op(e2,e1) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_764,c_224]) ).
tff(c_138,plain,
( ( op(e4,e1) = e3 )
| ( op(e3,e1) = e3 )
| ( op(e2,e1) = e3 )
| ( op(e1,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(cnfTransformation,[status(thm)],[f_802]) ).
tff(c_932,plain,
( ( op(e4,e1) = e3 )
| ( op(e3,e1) = e3 )
| ( op(e2,e1) = e3 )
| ( e4 = e3 )
| ( op(e0,e1) = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_394,c_138]) ).
tff(c_933,plain,
( ( op(e4,e1) = e3 )
| ( op(e3,e1) = e3 )
| ( op(e0,e1) = e3 ) ),
inference(negUnitSimplification,[status(thm)],[c_374,c_903,c_932]) ).
tff(c_2177,plain,
( ( e3 = e0 )
| ( e3 = e2 )
| ( e3 = e1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2040,c_2142,c_2155,c_933]) ).
tff(c_2178,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_382,c_378,c_388,c_2177]) ).
tff(c_2179,plain,
op(e4,e1) = e3,
inference(splitRight,[status(thm)],[c_2154]) ).
tff(c_92,plain,
( ( op(e4,e4) = e0 )
| ( op(e4,e3) = e0 )
| ( op(e4,e2) = e0 )
| ( op(e4,e1) = e0 )
| ( op(e4,e0) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_802]) ).
tff(c_966,plain,
( ( e2 = e0 )
| ( op(e4,e3) = e0 )
| ( op(e4,e2) = e0 )
| ( op(e4,e1) = e0 )
| ( op(e4,e0) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_802,c_92]) ).
tff(c_967,plain,
( ( op(e4,e3) = e0 )
| ( op(e4,e1) = e0 )
| ( op(e4,e0) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_888,c_390,c_966]) ).
tff(c_2280,plain,
( ( op(e4,e3) = e0 )
| ( e3 = e0 )
| ( e4 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2041,c_2179,c_967]) ).
tff(c_2281,plain,
op(e4,e3) = e0,
inference(negUnitSimplification,[status(thm)],[c_386,c_388,c_2280]) ).
tff(c_56,plain,
op(unit,e4) = e4,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_2042,plain,
op(e0,e4) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2038,c_56]) ).
tff(c_290,plain,
op(e2,e4) != op(e0,e4),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_2102,plain,
op(e2,e4) != e4,
inference(demodulation,[status(thm),theory(equality)],[c_2042,c_290]) ).
tff(c_216,plain,
op(e2,e4) != op(e2,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_905,plain,
op(e2,e4) != e3,
inference(demodulation,[status(thm),theory(equality)],[c_764,c_216]) ).
tff(c_22,plain,
( ( op(e2,e4) = e4 )
| ( op(e2,e4) = e3 )
| ( op(e2,e4) = e2 )
| ( op(e2,e4) = e1 )
| ( op(e2,e4) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_1001,plain,
( ( op(e2,e4) = e4 )
| ( op(e2,e4) = e1 )
| ( op(e2,e4) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_893,c_905,c_22]) ).
tff(c_2191,plain,
( ( op(e2,e4) = e1 )
| ( op(e2,e4) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_2102,c_1001]) ).
tff(c_2192,plain,
op(e2,e4) = e0,
inference(splitLeft,[status(thm)],[c_2191]) ).
tff(c_220,plain,
op(e2,e4) != op(e2,e1),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_2195,plain,
op(e2,e1) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_2192,c_220]) ).
tff(c_350,plain,
op(e2,e1) != op(e0,e1),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_2075,plain,
op(e2,e1) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_2040,c_350]) ).
tff(c_344,plain,
op(e2,e1) != op(e1,e1),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_881,plain,
op(e2,e1) != e4,
inference(demodulation,[status(thm),theory(equality)],[c_394,c_344]) ).
tff(c_28,plain,
( ( op(e2,e1) = e4 )
| ( op(e2,e1) = e3 )
| ( op(e2,e1) = e2 )
| ( op(e2,e1) = e1 )
| ( op(e2,e1) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_997,plain,
( ( op(e2,e1) = e2 )
| ( op(e2,e1) = e1 )
| ( op(e2,e1) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_903,c_881,c_28]) ).
tff(c_2211,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2195,c_2075,c_2058,c_997]) ).
tff(c_2212,plain,
op(e2,e4) = e1,
inference(splitRight,[status(thm)],[c_2191]) ).
tff(c_236,plain,
op(e1,e4) != op(e1,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_901,plain,
op(e1,e4) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_731,c_236]) ).
tff(c_90,plain,
( ( op(e4,e4) = e0 )
| ( op(e3,e4) = e0 )
| ( op(e2,e4) = e0 )
| ( op(e1,e4) = e0 )
| ( op(e0,e4) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_802]) ).
tff(c_968,plain,
( ( e2 = e0 )
| ( op(e3,e4) = e0 )
| ( op(e2,e4) = e0 )
| ( op(e1,e4) = e0 )
| ( op(e0,e4) = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_802,c_90]) ).
tff(c_969,plain,
( ( op(e3,e4) = e0 )
| ( op(e2,e4) = e0 )
| ( op(e0,e4) = e0 ) ),
inference(negUnitSimplification,[status(thm)],[c_901,c_390,c_968]) ).
tff(c_2270,plain,
( ( op(e3,e4) = e0 )
| ( e1 = e0 )
| ( e4 = e0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2042,c_2212,c_969]) ).
tff(c_2271,plain,
op(e3,e4) = e0,
inference(negUnitSimplification,[status(thm)],[c_386,c_392,c_2270]) ).
tff(c_116,plain,
( ( op(e2,e4) = e4 )
| ( op(e2,e3) = e4 )
| ( op(e2,e2) = e4 )
| ( op(e2,e1) = e4 )
| ( op(e2,e0) = e4 ) ),
inference(cnfTransformation,[status(thm)],[f_802]) ).
tff(c_954,plain,
( ( op(e2,e4) = e4 )
| ( op(e2,e3) = e4 )
| ( e4 = e3 )
| ( op(e2,e1) = e4 )
| ( op(e2,e0) = e4 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_764,c_116]) ).
tff(c_955,plain,
( ( op(e2,e4) = e4 )
| ( op(e2,e3) = e4 )
| ( op(e2,e0) = e4 ) ),
inference(negUnitSimplification,[status(thm)],[c_881,c_374,c_954]) ).
tff(c_2233,plain,
( ( e4 = e1 )
| ( op(e2,e3) = e4 )
| ( e4 = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2039,c_2212,c_955]) ).
tff(c_2234,plain,
op(e2,e3) = e4,
inference(negUnitSimplification,[status(thm)],[c_376,c_380,c_2233]) ).
tff(c_198,plain,
op(e3,e3) != op(e3,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_1595,plain,
op(e3,e2) != e1,
inference(demodulation,[status(thm),theory(equality)],[c_1587,c_198]) ).
tff(c_122,plain,
( ( op(e4,e2) = e2 )
| ( op(e3,e2) = e2 )
| ( op(e2,e2) = e2 )
| ( op(e1,e2) = e2 )
| ( op(e0,e2) = e2 ) ),
inference(cnfTransformation,[status(thm)],[f_802]) ).
tff(c_948,plain,
( ( op(e4,e2) = e2 )
| ( op(e3,e2) = e2 )
| ( e3 = e2 )
| ( e2 = e0 )
| ( op(e0,e2) = e2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_731,c_764,c_122]) ).
tff(c_949,plain,
( ( op(e3,e2) = e2 )
| ( op(e0,e2) = e2 ) ),
inference(negUnitSimplification,[status(thm)],[c_390,c_378,c_908,c_948]) ).
tff(c_1899,plain,
op(e0,e2) = e2,
inference(splitLeft,[status(thm)],[c_949]) ).
tff(c_328,plain,
op(e3,e2) != op(e0,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_1903,plain,
op(e3,e2) != e2,
inference(demodulation,[status(thm),theory(equality)],[c_1899,c_328]) ).
tff(c_322,plain,
op(e3,e2) != op(e1,e2),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_887,plain,
op(e3,e2) != e0,
inference(demodulation,[status(thm),theory(equality)],[c_731,c_322]) ).
tff(c_16,plain,
( ( op(e3,e2) = e4 )
| ( op(e3,e2) = e3 )
| ( op(e3,e2) = e2 )
| ( op(e3,e2) = e1 )
| ( op(e3,e2) = e0 ) ),
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_1003,plain,
( ( op(e3,e2) = e4 )
| ( op(e3,e2) = e2 )
| ( op(e3,e2) = e1 ) ),
inference(negUnitSimplification,[status(thm)],[c_887,c_889,c_16]) ).
tff(c_2246,plain,
op(e3,e2) = e4,
inference(negUnitSimplification,[status(thm)],[c_1595,c_1903,c_1003]) ).
tff(c_60,plain,
op(unit,e3) = e3,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_2044,plain,
op(e0,e3) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_2038,c_60]) ).
tff(c_478,plain,
( ( op(e0,op(e0,e3)) != e3 )
| ( op(e3,op(e1,e3)) = e1 )
| ( op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) = e3 )
| ( op(e3,op(e4,e3)) = e4 ) ),
inference(cnfTransformation,[status(thm)],[f_1313]) ).
tff(c_2374,plain,
( ( e4 = e1 )
| ( e2 = e0 )
| ( e3 = e2 )
| ( e4 = e3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2043,c_2281,c_2142,c_1587,c_2271,c_2234,c_2246,c_1865,c_2044,c_2044,c_478]) ).
tff(c_2375,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_374,c_378,c_390,c_380,c_2374]) ).
tff(c_2376,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_2378,plain,
unit = e4,
inference(splitLeft,[status(thm)],[c_2376]) ).
tff(c_2380,plain,
op(e2,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2378,c_62]) ).
tff(c_2391,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_893,c_2380]) ).
tff(c_2392,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_2376]) ).
tff(c_2394,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_2392]) ).
tff(c_2399,plain,
op(e4,e1) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2394,c_54]) ).
tff(c_2408,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_883,c_2399]) ).
tff(c_2409,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_2392]) ).
tff(c_2411,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_2409]) ).
tff(c_2415,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2411,c_62]) ).
tff(c_2426,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1872,c_2415]) ).
tff(c_2427,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_2409]) ).
tff(c_2437,plain,
op(e4,e2) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2427,c_54]) ).
tff(c_2445,plain,
e4 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_1911,c_2437]) ).
tff(c_2447,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_380,c_2445]) ).
tff(c_2448,plain,
op(e4,e2) = e4,
inference(splitRight,[status(thm)],[c_1007]) ).
tff(c_190,plain,
op(e4,e2) != op(e4,e0),
inference(cnfTransformation,[status(thm)],[f_1101]) ).
tff(c_2453,plain,
op(e4,e0) != e4,
inference(demodulation,[status(thm),theory(equality)],[c_2448,c_190]) ).
tff(c_2476,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_2479,plain,
op(e4,e0) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2476,c_54]) ).
tff(c_2488,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2453,c_2479]) ).
tff(c_2489,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_2491,plain,
unit = e4,
inference(splitLeft,[status(thm)],[c_2489]) ).
tff(c_2493,plain,
op(e2,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2491,c_62]) ).
tff(c_2504,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_893,c_2493]) ).
tff(c_2505,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_2489]) ).
tff(c_2509,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_2505]) ).
tff(c_2514,plain,
op(e4,e1) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2509,c_54]) ).
tff(c_2523,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_883,c_2514]) ).
tff(c_2524,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_2505]) ).
tff(c_2526,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_2524]) ).
tff(c_2530,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2526,c_62]) ).
tff(c_2541,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1872,c_2530]) ).
tff(c_2542,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_2524]) ).
tff(c_2552,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_2542,c_58]) ).
tff(c_2560,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_889,c_2552]) ).
tff(c_2561,plain,
op(e3,e2) = e2,
inference(splitRight,[status(thm)],[c_949]) ).
tff(c_2588,plain,
op(e4,e2) = e1,
inference(splitLeft,[status(thm)],[c_1007]) ).
tff(c_2562,plain,
op(e0,e2) != e2,
inference(splitRight,[status(thm)],[c_949]) ).
tff(c_2601,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_64,plain,
op(unit,e2) = e2,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_2608,plain,
op(e0,e2) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2601,c_64]) ).
tff(c_2613,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2562,c_2608]) ).
tff(c_2614,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_2616,plain,
unit = e4,
inference(splitLeft,[status(thm)],[c_2614]) ).
tff(c_2618,plain,
op(e2,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2616,c_62]) ).
tff(c_2629,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_893,c_2618]) ).
tff(c_2630,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_2614]) ).
tff(c_2633,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_2630]) ).
tff(c_2638,plain,
op(e4,e1) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2633,c_54]) ).
tff(c_2647,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_883,c_2638]) ).
tff(c_2648,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_2630]) ).
tff(c_2650,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_2648]) ).
tff(c_2654,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2650,c_62]) ).
tff(c_2665,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1872,c_2654]) ).
tff(c_2666,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_2648]) ).
tff(c_2673,plain,
op(e4,e2) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2666,c_54]) ).
tff(c_2681,plain,
e4 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_2588,c_2673]) ).
tff(c_2683,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_380,c_2681]) ).
tff(c_2684,plain,
op(e4,e2) = e4,
inference(splitRight,[status(thm)],[c_1007]) ).
tff(c_2689,plain,
op(e4,e0) != e4,
inference(demodulation,[status(thm),theory(equality)],[c_2684,c_190]) ).
tff(c_2700,plain,
unit = e0,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_2703,plain,
op(e4,e0) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2700,c_54]) ).
tff(c_2712,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2689,c_2703]) ).
tff(c_2713,plain,
( ( unit = e1 )
| ( unit = e2 )
| ( unit = e3 )
| ( unit = e4 ) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_2715,plain,
unit = e4,
inference(splitLeft,[status(thm)],[c_2713]) ).
tff(c_2717,plain,
op(e2,e4) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2715,c_62]) ).
tff(c_2728,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_893,c_2717]) ).
tff(c_2729,plain,
( ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 ) ),
inference(splitRight,[status(thm)],[c_2713]) ).
tff(c_2733,plain,
unit = e1,
inference(splitLeft,[status(thm)],[c_2729]) ).
tff(c_2738,plain,
op(e4,e1) = e4,
inference(demodulation,[status(thm),theory(equality)],[c_2733,c_54]) ).
tff(c_2747,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_883,c_2738]) ).
tff(c_2748,plain,
( ( unit = e2 )
| ( unit = e3 ) ),
inference(splitRight,[status(thm)],[c_2729]) ).
tff(c_2750,plain,
unit = e3,
inference(splitLeft,[status(thm)],[c_2748]) ).
tff(c_2754,plain,
op(e2,e3) = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2750,c_62]) ).
tff(c_2765,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1872,c_2754]) ).
tff(c_2766,plain,
unit = e2,
inference(splitRight,[status(thm)],[c_2748]) ).
tff(c_2775,plain,
op(e3,e2) = e3,
inference(demodulation,[status(thm),theory(equality)],[c_2766,c_58]) ).
tff(c_2782,plain,
e3 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_2561,c_2775]) ).
tff(c_2784,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_378,c_2782]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.11 % Problem : ALG061+1 : TPTP v9.0.0. Released v2.7.0.
% 0.02/0.12 % 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.33 % Computer : n005.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Sun Apr 6 06:58:12 EDT 2025
% 0.13/0.33 % CPUTime :
% 11.15/3.52 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.51/3.57
% 11.51/3.57 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------