%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ALG105+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 : n027.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:15 PM UTC 2025
% Result : Theorem 170.35s 144.75s
% Output : CNFRefutation 170.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 24
% Syntax : Number of formulae : 377 ( 246 unt; 0 typ; 0 def)
% Number of atoms : 1931 (1917 equ)
% Maximal formula atoms : 384 ( 5 avg)
% Number of connectives : 2161 ( 607 ~;1039 |; 515 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 3 ( 2 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 : 22 ( 22 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ op2 > op1 > #nlpp > h9 > h8 > h7 > h6 > h5 > h4 > h3 > h2 > h12 > h11 > h10 > h1 > e23 > e22 > e21 > e20 > e13 > e12 > e11 > e10
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(e21,type,
e21: $i ).
tff(h4,type,
h4: $i > $i ).
tff(e20,type,
e20: $i ).
tff(h7,type,
h7: $i > $i ).
tff(h3,type,
h3: $i > $i ).
tff(h2,type,
h2: $i > $i ).
tff(e13,type,
e13: $i ).
tff(h8,type,
h8: $i > $i ).
tff(e22,type,
e22: $i ).
tff(op2,type,
op2: ( $i * $i ) > $i ).
tff(h6,type,
h6: $i > $i ).
tff(op1,type,
op1: ( $i * $i ) > $i ).
tff(h1,type,
h1: $i > $i ).
tff(h9,type,
h9: $i > $i ).
tff(h5,type,
h5: $i > $i ).
tff(e10,type,
e10: $i ).
tff(h12,type,
h12: $i > $i ).
tff(h10,type,
h10: $i > $i ).
tff(e23,type,
e23: $i ).
tff(e12,type,
e12: $i ).
tff(e11,type,
e11: $i ).
tff(h11,type,
h11: $i > $i ).
tff(f_1109,axiom,
( ( e20 != e21 )
& ( e20 != e22 )
& ( e20 != e23 )
& ( e21 != e22 )
& ( e21 != e23 )
& ( e22 != e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
tff(f_1302,axiom,
( ( h2(e11) = e20 )
& ( h2(e12) = e22 )
& ( h2(e10) = op2(op2(e22,e20),op2(e22,e20)) )
& ( h2(e13) = op2(e22,e20) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
tff(f_1288,axiom,
( ( e20 = op2(op2(e22,e21),op2(e22,e21)) )
& ( e23 = op2(e22,e21) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
tff(f_1365,axiom,
( ( h11(e11) = e23 )
& ( h11(e12) = e21 )
& ( h11(e10) = op2(op2(e21,e23),op2(e21,e23)) )
& ( h11(e13) = op2(e21,e23) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
tff(f_1351,axiom,
( ( h9(e11) = e22 )
& ( h9(e12) = e23 )
& ( h9(e10) = op2(op2(e23,e22),op2(e23,e22)) )
& ( h9(e13) = op2(e23,e22) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
tff(f_1282,axiom,
( ( op2(op2(e20,e20),e20) = e20 )
& ( op2(op2(e20,e21),e20) = e21 )
& ( op2(op2(e20,e22),e20) = e22 )
& ( op2(op2(e20,e23),e20) = e23 )
& ( op2(op2(e21,e20),e21) = e20 )
& ( op2(op2(e21,e21),e21) = e21 )
& ( op2(op2(e21,e22),e21) = e22 )
& ( op2(op2(e21,e23),e21) = e23 )
& ( op2(op2(e22,e20),e22) = e20 )
& ( op2(op2(e22,e21),e22) = e21 )
& ( op2(op2(e22,e22),e22) = e22 )
& ( op2(op2(e22,e23),e22) = e23 )
& ( op2(op2(e23,e20),e23) = e20 )
& ( op2(op2(e23,e21),e23) = e21 )
& ( op2(op2(e23,e22),e23) = e22 )
& ( op2(op2(e23,e23),e23) = e23 )
& ( ( ( op2(e20,op2(e20,e20)) = op2(e20,e20) )
& ( op2(e20,op2(e21,e20)) = op2(e21,e20) )
& ( op2(e20,op2(e22,e20)) = op2(e22,e20) )
& ( op2(e20,op2(e23,e20)) = op2(e23,e20) ) )
| ( ( op2(e21,op2(e20,e21)) = op2(e20,e21) )
& ( op2(e21,op2(e21,e21)) = op2(e21,e21) )
& ( op2(e21,op2(e22,e21)) = op2(e22,e21) )
& ( op2(e21,op2(e23,e21)) = op2(e23,e21) ) )
| ( ( op2(e22,op2(e20,e22)) = op2(e20,e22) )
& ( op2(e22,op2(e21,e22)) = op2(e21,e22) )
& ( op2(e22,op2(e22,e22)) = op2(e22,e22) )
& ( op2(e22,op2(e23,e22)) = op2(e23,e22) ) )
| ( ( op2(e23,op2(e20,e23)) = op2(e20,e23) )
& ( op2(e23,op2(e21,e23)) = op2(e21,e23) )
& ( op2(e23,op2(e22,e23)) = op2(e22,e23) )
& ( op2(e23,op2(e23,e23)) = op2(e23,e23) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
tff(f_1295,axiom,
( ( h1(e11) = e20 )
& ( h1(e12) = e21 )
& ( h1(e10) = op2(op2(e21,e20),op2(e21,e20)) )
& ( h1(e13) = op2(e21,e20) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
tff(f_1358,axiom,
( ( h10(e11) = e23 )
& ( h10(e12) = e20 )
& ( h10(e10) = op2(op2(e20,e23),op2(e20,e23)) )
& ( h10(e13) = op2(e20,e23) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
tff(f_1323,axiom,
( ( h5(e11) = e21 )
& ( h5(e12) = e22 )
& ( h5(e10) = op2(op2(e22,e21),op2(e22,e21)) )
& ( h5(e13) = op2(e22,e21) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
tff(f_1075,axiom,
( ( op2(e20,e20) != op2(e21,e20) )
& ( op2(e20,e20) != op2(e22,e20) )
& ( op2(e20,e20) != op2(e23,e20) )
& ( op2(e21,e20) != op2(e22,e20) )
& ( op2(e21,e20) != op2(e23,e20) )
& ( op2(e22,e20) != op2(e23,e20) )
& ( op2(e20,e21) != op2(e21,e21) )
& ( op2(e20,e21) != op2(e22,e21) )
& ( op2(e20,e21) != op2(e23,e21) )
& ( op2(e21,e21) != op2(e22,e21) )
& ( op2(e21,e21) != op2(e23,e21) )
& ( op2(e22,e21) != op2(e23,e21) )
& ( op2(e20,e22) != op2(e21,e22) )
& ( op2(e20,e22) != op2(e22,e22) )
& ( op2(e20,e22) != op2(e23,e22) )
& ( op2(e21,e22) != op2(e22,e22) )
& ( op2(e21,e22) != op2(e23,e22) )
& ( op2(e22,e22) != op2(e23,e22) )
& ( op2(e20,e23) != op2(e21,e23) )
& ( op2(e20,e23) != op2(e22,e23) )
& ( op2(e20,e23) != op2(e23,e23) )
& ( op2(e21,e23) != op2(e22,e23) )
& ( op2(e21,e23) != op2(e23,e23) )
& ( op2(e22,e23) != op2(e23,e23) )
& ( op2(e20,e20) != op2(e20,e21) )
& ( op2(e20,e20) != op2(e20,e22) )
& ( op2(e20,e20) != op2(e20,e23) )
& ( op2(e20,e21) != op2(e20,e22) )
& ( op2(e20,e21) != op2(e20,e23) )
& ( op2(e20,e22) != op2(e20,e23) )
& ( op2(e21,e20) != op2(e21,e21) )
& ( op2(e21,e20) != op2(e21,e22) )
& ( op2(e21,e20) != op2(e21,e23) )
& ( op2(e21,e21) != op2(e21,e22) )
& ( op2(e21,e21) != op2(e21,e23) )
& ( op2(e21,e22) != op2(e21,e23) )
& ( op2(e22,e20) != op2(e22,e21) )
& ( op2(e22,e20) != op2(e22,e22) )
& ( op2(e22,e20) != op2(e22,e23) )
& ( op2(e22,e21) != op2(e22,e22) )
& ( op2(e22,e21) != op2(e22,e23) )
& ( op2(e22,e22) != op2(e22,e23) )
& ( op2(e23,e20) != op2(e23,e21) )
& ( op2(e23,e20) != op2(e23,e22) )
& ( op2(e23,e20) != op2(e23,e23) )
& ( op2(e23,e21) != op2(e23,e22) )
& ( op2(e23,e21) != op2(e23,e23) )
& ( op2(e23,e22) != op2(e23,e23) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
tff(f_1344,axiom,
( ( h8(e11) = e22 )
& ( h8(e12) = e21 )
& ( h8(e10) = op2(op2(e21,e22),op2(e21,e22)) )
& ( h8(e13) = op2(e21,e22) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
tff(f_789,axiom,
( ( ( op2(e20,e20) = e20 )
| ( op2(e20,e21) = e20 )
| ( op2(e20,e22) = e20 )
| ( op2(e20,e23) = e20 ) )
& ( ( op2(e20,e20) = e20 )
| ( op2(e21,e20) = e20 )
| ( op2(e22,e20) = e20 )
| ( op2(e23,e20) = e20 ) )
& ( ( op2(e20,e20) = e21 )
| ( op2(e20,e21) = e21 )
| ( op2(e20,e22) = e21 )
| ( op2(e20,e23) = e21 ) )
& ( ( op2(e20,e20) = e21 )
| ( op2(e21,e20) = e21 )
| ( op2(e22,e20) = e21 )
| ( op2(e23,e20) = e21 ) )
& ( ( op2(e20,e20) = e22 )
| ( op2(e20,e21) = e22 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e23) = e22 ) )
& ( ( op2(e20,e20) = e22 )
| ( op2(e21,e20) = e22 )
| ( op2(e22,e20) = e22 )
| ( op2(e23,e20) = e22 ) )
& ( ( op2(e20,e20) = e23 )
| ( op2(e20,e21) = e23 )
| ( op2(e20,e22) = e23 )
| ( op2(e20,e23) = e23 ) )
& ( ( op2(e20,e20) = e23 )
| ( op2(e21,e20) = e23 )
| ( op2(e22,e20) = e23 )
| ( op2(e23,e20) = e23 ) )
& ( ( op2(e21,e20) = e20 )
| ( op2(e21,e21) = e20 )
| ( op2(e21,e22) = e20 )
| ( op2(e21,e23) = e20 ) )
& ( ( op2(e20,e21) = e20 )
| ( op2(e21,e21) = e20 )
| ( op2(e22,e21) = e20 )
| ( op2(e23,e21) = e20 ) )
& ( ( op2(e21,e20) = e21 )
| ( op2(e21,e21) = e21 )
| ( op2(e21,e22) = e21 )
| ( op2(e21,e23) = e21 ) )
& ( ( op2(e20,e21) = e21 )
| ( op2(e21,e21) = e21 )
| ( op2(e22,e21) = e21 )
| ( op2(e23,e21) = e21 ) )
& ( ( op2(e21,e20) = e22 )
| ( op2(e21,e21) = e22 )
| ( op2(e21,e22) = e22 )
| ( op2(e21,e23) = e22 ) )
& ( ( op2(e20,e21) = e22 )
| ( op2(e21,e21) = e22 )
| ( op2(e22,e21) = e22 )
| ( op2(e23,e21) = e22 ) )
& ( ( op2(e21,e20) = e23 )
| ( op2(e21,e21) = e23 )
| ( op2(e21,e22) = e23 )
| ( op2(e21,e23) = e23 ) )
& ( ( op2(e20,e21) = e23 )
| ( op2(e21,e21) = e23 )
| ( op2(e22,e21) = e23 )
| ( op2(e23,e21) = e23 ) )
& ( ( op2(e22,e20) = e20 )
| ( op2(e22,e21) = e20 )
| ( op2(e22,e22) = e20 )
| ( op2(e22,e23) = e20 ) )
& ( ( op2(e20,e22) = e20 )
| ( op2(e21,e22) = e20 )
| ( op2(e22,e22) = e20 )
| ( op2(e23,e22) = e20 ) )
& ( ( op2(e22,e20) = e21 )
| ( op2(e22,e21) = e21 )
| ( op2(e22,e22) = e21 )
| ( op2(e22,e23) = e21 ) )
& ( ( op2(e20,e22) = e21 )
| ( op2(e21,e22) = e21 )
| ( op2(e22,e22) = e21 )
| ( op2(e23,e22) = e21 ) )
& ( ( op2(e22,e20) = e22 )
| ( op2(e22,e21) = e22 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e23) = e22 ) )
& ( ( op2(e20,e22) = e22 )
| ( op2(e21,e22) = e22 )
| ( op2(e22,e22) = e22 )
| ( op2(e23,e22) = e22 ) )
& ( ( op2(e22,e20) = e23 )
| ( op2(e22,e21) = e23 )
| ( op2(e22,e22) = e23 )
| ( op2(e22,e23) = e23 ) )
& ( ( op2(e20,e22) = e23 )
| ( op2(e21,e22) = e23 )
| ( op2(e22,e22) = e23 )
| ( op2(e23,e22) = e23 ) )
& ( ( op2(e23,e20) = e20 )
| ( op2(e23,e21) = e20 )
| ( op2(e23,e22) = e20 )
| ( op2(e23,e23) = e20 ) )
& ( ( op2(e20,e23) = e20 )
| ( op2(e21,e23) = e20 )
| ( op2(e22,e23) = e20 )
| ( op2(e23,e23) = e20 ) )
& ( ( op2(e23,e20) = e21 )
| ( op2(e23,e21) = e21 )
| ( op2(e23,e22) = e21 )
| ( op2(e23,e23) = e21 ) )
& ( ( op2(e20,e23) = e21 )
| ( op2(e21,e23) = e21 )
| ( op2(e22,e23) = e21 )
| ( op2(e23,e23) = e21 ) )
& ( ( op2(e23,e20) = e22 )
| ( op2(e23,e21) = e22 )
| ( op2(e23,e22) = e22 )
| ( op2(e23,e23) = e22 ) )
& ( ( op2(e20,e23) = e22 )
| ( op2(e21,e23) = e22 )
| ( op2(e22,e23) = e22 )
| ( op2(e23,e23) = e22 ) )
& ( ( op2(e23,e20) = e23 )
| ( op2(e23,e21) = e23 )
| ( op2(e23,e22) = e23 )
| ( op2(e23,e23) = e23 ) )
& ( ( op2(e20,e23) = e23 )
| ( op2(e21,e23) = e23 )
| ( op2(e22,e23) = e23 )
| ( op2(e23,e23) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
tff(f_1330,axiom,
( ( h6(e11) = e21 )
& ( h6(e12) = e23 )
& ( h6(e10) = op2(op2(e23,e21),op2(e23,e21)) )
& ( h6(e13) = op2(e23,e21) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
tff(f_1092,axiom,
( ( e10 != e11 )
& ( e10 != e12 )
& ( e10 != e13 )
& ( e11 != e12 )
& ( e11 != e13 )
& ( e12 != e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
tff(f_1285,axiom,
( ( e10 = op1(op1(e12,e11),op1(e12,e11)) )
& ( e13 = op1(e12,e11) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
tff(f_1219,axiom,
( ( op1(op1(e10,e10),e10) = e10 )
& ( op1(op1(e10,e11),e10) = e11 )
& ( op1(op1(e10,e12),e10) = e12 )
& ( op1(op1(e10,e13),e10) = e13 )
& ( op1(op1(e11,e10),e11) = e10 )
& ( op1(op1(e11,e11),e11) = e11 )
& ( op1(op1(e11,e12),e11) = e12 )
& ( op1(op1(e11,e13),e11) = e13 )
& ( op1(op1(e12,e10),e12) = e10 )
& ( op1(op1(e12,e11),e12) = e11 )
& ( op1(op1(e12,e12),e12) = e12 )
& ( op1(op1(e12,e13),e12) = e13 )
& ( op1(op1(e13,e10),e13) = e10 )
& ( op1(op1(e13,e11),e13) = e11 )
& ( op1(op1(e13,e12),e13) = e12 )
& ( op1(op1(e13,e13),e13) = e13 )
& ( ( ( op1(e10,op1(e10,e10)) = op1(e10,e10) )
& ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
& ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
& ( op1(e10,op1(e13,e10)) = op1(e13,e10) ) )
| ( ( op1(e11,op1(e10,e11)) = op1(e10,e11) )
& ( op1(e11,op1(e11,e11)) = op1(e11,e11) )
& ( op1(e11,op1(e12,e11)) = op1(e12,e11) )
& ( op1(e11,op1(e13,e11)) = op1(e13,e11) ) )
| ( ( op1(e12,op1(e10,e12)) = op1(e10,e12) )
& ( op1(e12,op1(e11,e12)) = op1(e11,e12) )
& ( op1(e12,op1(e12,e12)) = op1(e12,e12) )
& ( op1(e12,op1(e13,e12)) = op1(e13,e12) ) )
| ( ( op1(e13,op1(e10,e13)) = op1(e10,e13) )
& ( op1(e13,op1(e11,e13)) = op1(e11,e13) )
& ( op1(e13,op1(e12,e13)) = op1(e12,e13) )
& ( op1(e13,op1(e13,e13)) = op1(e13,e13) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
tff(f_932,axiom,
( ( op1(e10,e10) != op1(e11,e10) )
& ( op1(e10,e10) != op1(e12,e10) )
& ( op1(e10,e10) != op1(e13,e10) )
& ( op1(e11,e10) != op1(e12,e10) )
& ( op1(e11,e10) != op1(e13,e10) )
& ( op1(e12,e10) != op1(e13,e10) )
& ( op1(e10,e11) != op1(e11,e11) )
& ( op1(e10,e11) != op1(e12,e11) )
& ( op1(e10,e11) != op1(e13,e11) )
& ( op1(e11,e11) != op1(e12,e11) )
& ( op1(e11,e11) != op1(e13,e11) )
& ( op1(e12,e11) != op1(e13,e11) )
& ( op1(e10,e12) != op1(e11,e12) )
& ( op1(e10,e12) != op1(e12,e12) )
& ( op1(e10,e12) != op1(e13,e12) )
& ( op1(e11,e12) != op1(e12,e12) )
& ( op1(e11,e12) != op1(e13,e12) )
& ( op1(e12,e12) != op1(e13,e12) )
& ( op1(e10,e13) != op1(e11,e13) )
& ( op1(e10,e13) != op1(e12,e13) )
& ( op1(e10,e13) != op1(e13,e13) )
& ( op1(e11,e13) != op1(e12,e13) )
& ( op1(e11,e13) != op1(e13,e13) )
& ( op1(e12,e13) != op1(e13,e13) )
& ( op1(e10,e10) != op1(e10,e11) )
& ( op1(e10,e10) != op1(e10,e12) )
& ( op1(e10,e10) != op1(e10,e13) )
& ( op1(e10,e11) != op1(e10,e12) )
& ( op1(e10,e11) != op1(e10,e13) )
& ( op1(e10,e12) != op1(e10,e13) )
& ( op1(e11,e10) != op1(e11,e11) )
& ( op1(e11,e10) != op1(e11,e12) )
& ( op1(e11,e10) != op1(e11,e13) )
& ( op1(e11,e11) != op1(e11,e12) )
& ( op1(e11,e11) != op1(e11,e13) )
& ( op1(e11,e12) != op1(e11,e13) )
& ( op1(e12,e10) != op1(e12,e11) )
& ( op1(e12,e10) != op1(e12,e12) )
& ( op1(e12,e10) != op1(e12,e13) )
& ( op1(e12,e11) != op1(e12,e12) )
& ( op1(e12,e11) != op1(e12,e13) )
& ( op1(e12,e12) != op1(e12,e13) )
& ( op1(e13,e10) != op1(e13,e11) )
& ( op1(e13,e10) != op1(e13,e12) )
& ( op1(e13,e10) != op1(e13,e13) )
& ( op1(e13,e11) != op1(e13,e12) )
& ( op1(e13,e11) != op1(e13,e13) )
& ( op1(e13,e12) != op1(e13,e13) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
tff(f_407,axiom,
( ( ( op1(e10,e10) = e10 )
| ( op1(e10,e11) = e10 )
| ( op1(e10,e12) = e10 )
| ( op1(e10,e13) = e10 ) )
& ( ( op1(e10,e10) = e10 )
| ( op1(e11,e10) = e10 )
| ( op1(e12,e10) = e10 )
| ( op1(e13,e10) = e10 ) )
& ( ( op1(e10,e10) = e11 )
| ( op1(e10,e11) = e11 )
| ( op1(e10,e12) = e11 )
| ( op1(e10,e13) = e11 ) )
& ( ( op1(e10,e10) = e11 )
| ( op1(e11,e10) = e11 )
| ( op1(e12,e10) = e11 )
| ( op1(e13,e10) = e11 ) )
& ( ( op1(e10,e10) = e12 )
| ( op1(e10,e11) = e12 )
| ( op1(e10,e12) = e12 )
| ( op1(e10,e13) = e12 ) )
& ( ( op1(e10,e10) = e12 )
| ( op1(e11,e10) = e12 )
| ( op1(e12,e10) = e12 )
| ( op1(e13,e10) = e12 ) )
& ( ( op1(e10,e10) = e13 )
| ( op1(e10,e11) = e13 )
| ( op1(e10,e12) = e13 )
| ( op1(e10,e13) = e13 ) )
& ( ( op1(e10,e10) = e13 )
| ( op1(e11,e10) = e13 )
| ( op1(e12,e10) = e13 )
| ( op1(e13,e10) = e13 ) )
& ( ( op1(e11,e10) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e11,e13) = e10 ) )
& ( ( op1(e10,e11) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e12,e11) = e10 )
| ( op1(e13,e11) = e10 ) )
& ( ( op1(e11,e10) = e11 )
| ( op1(e11,e11) = e11 )
| ( op1(e11,e12) = e11 )
| ( op1(e11,e13) = e11 ) )
& ( ( op1(e10,e11) = e11 )
| ( op1(e11,e11) = e11 )
| ( op1(e12,e11) = e11 )
| ( op1(e13,e11) = e11 ) )
& ( ( op1(e11,e10) = e12 )
| ( op1(e11,e11) = e12 )
| ( op1(e11,e12) = e12 )
| ( op1(e11,e13) = e12 ) )
& ( ( op1(e10,e11) = e12 )
| ( op1(e11,e11) = e12 )
| ( op1(e12,e11) = e12 )
| ( op1(e13,e11) = e12 ) )
& ( ( op1(e11,e10) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e11,e12) = e13 )
| ( op1(e11,e13) = e13 ) )
& ( ( op1(e10,e11) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e12,e11) = e13 )
| ( op1(e13,e11) = e13 ) )
& ( ( op1(e12,e10) = e10 )
| ( op1(e12,e11) = e10 )
| ( op1(e12,e12) = e10 )
| ( op1(e12,e13) = e10 ) )
& ( ( op1(e10,e12) = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e12,e12) = e10 )
| ( op1(e13,e12) = e10 ) )
& ( ( op1(e12,e10) = e11 )
| ( op1(e12,e11) = e11 )
| ( op1(e12,e12) = e11 )
| ( op1(e12,e13) = e11 ) )
& ( ( op1(e10,e12) = e11 )
| ( op1(e11,e12) = e11 )
| ( op1(e12,e12) = e11 )
| ( op1(e13,e12) = e11 ) )
& ( ( op1(e12,e10) = e12 )
| ( op1(e12,e11) = e12 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e13) = e12 ) )
& ( ( op1(e10,e12) = e12 )
| ( op1(e11,e12) = e12 )
| ( op1(e12,e12) = e12 )
| ( op1(e13,e12) = e12 ) )
& ( ( op1(e12,e10) = e13 )
| ( op1(e12,e11) = e13 )
| ( op1(e12,e12) = e13 )
| ( op1(e12,e13) = e13 ) )
& ( ( op1(e10,e12) = e13 )
| ( op1(e11,e12) = e13 )
| ( op1(e12,e12) = e13 )
| ( op1(e13,e12) = e13 ) )
& ( ( op1(e13,e10) = e10 )
| ( op1(e13,e11) = e10 )
| ( op1(e13,e12) = e10 )
| ( op1(e13,e13) = e10 ) )
& ( ( op1(e10,e13) = e10 )
| ( op1(e11,e13) = e10 )
| ( op1(e12,e13) = e10 )
| ( op1(e13,e13) = e10 ) )
& ( ( op1(e13,e10) = e11 )
| ( op1(e13,e11) = e11 )
| ( op1(e13,e12) = e11 )
| ( op1(e13,e13) = e11 ) )
& ( ( op1(e10,e13) = e11 )
| ( op1(e11,e13) = e11 )
| ( op1(e12,e13) = e11 )
| ( op1(e13,e13) = e11 ) )
& ( ( op1(e13,e10) = e12 )
| ( op1(e13,e11) = e12 )
| ( op1(e13,e12) = e12 )
| ( op1(e13,e13) = e12 ) )
& ( ( op1(e10,e13) = e12 )
| ( op1(e11,e13) = e12 )
| ( op1(e12,e13) = e12 )
| ( op1(e13,e13) = e12 ) )
& ( ( op1(e13,e10) = e13 )
| ( op1(e13,e11) = e13 )
| ( op1(e13,e12) = e13 )
| ( op1(e13,e13) = e13 ) )
& ( ( op1(e10,e13) = e13 )
| ( op1(e11,e13) = e13 )
| ( op1(e12,e13) = e13 )
| ( op1(e13,e13) = e13 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
tff(f_152,axiom,
( ( ( op1(e10,e10) = e10 )
| ( op1(e10,e10) = e11 )
| ( op1(e10,e10) = e12 )
| ( op1(e10,e10) = e13 ) )
& ( ( op1(e10,e11) = e10 )
| ( op1(e10,e11) = e11 )
| ( op1(e10,e11) = e12 )
| ( op1(e10,e11) = e13 ) )
& ( ( op1(e10,e12) = e10 )
| ( op1(e10,e12) = e11 )
| ( op1(e10,e12) = e12 )
| ( op1(e10,e12) = e13 ) )
& ( ( op1(e10,e13) = e10 )
| ( op1(e10,e13) = e11 )
| ( op1(e10,e13) = e12 )
| ( op1(e10,e13) = e13 ) )
& ( ( op1(e11,e10) = e10 )
| ( op1(e11,e10) = e11 )
| ( op1(e11,e10) = e12 )
| ( op1(e11,e10) = e13 ) )
& ( ( op1(e11,e11) = e10 )
| ( op1(e11,e11) = e11 )
| ( op1(e11,e11) = e12 )
| ( op1(e11,e11) = e13 ) )
& ( ( op1(e11,e12) = e10 )
| ( op1(e11,e12) = e11 )
| ( op1(e11,e12) = e12 )
| ( op1(e11,e12) = e13 ) )
& ( ( op1(e11,e13) = e10 )
| ( op1(e11,e13) = e11 )
| ( op1(e11,e13) = e12 )
| ( op1(e11,e13) = e13 ) )
& ( ( op1(e12,e10) = e10 )
| ( op1(e12,e10) = e11 )
| ( op1(e12,e10) = e12 )
| ( op1(e12,e10) = e13 ) )
& ( ( op1(e12,e11) = e10 )
| ( op1(e12,e11) = e11 )
| ( op1(e12,e11) = e12 )
| ( op1(e12,e11) = e13 ) )
& ( ( op1(e12,e12) = e10 )
| ( op1(e12,e12) = e11 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e12) = e13 ) )
& ( ( op1(e12,e13) = e10 )
| ( op1(e12,e13) = e11 )
| ( op1(e12,e13) = e12 )
| ( op1(e12,e13) = e13 ) )
& ( ( op1(e13,e10) = e10 )
| ( op1(e13,e10) = e11 )
| ( op1(e13,e10) = e12 )
| ( op1(e13,e10) = e13 ) )
& ( ( op1(e13,e11) = e10 )
| ( op1(e13,e11) = e11 )
| ( op1(e13,e11) = e12 )
| ( op1(e13,e11) = e13 ) )
& ( ( op1(e13,e12) = e10 )
| ( op1(e13,e12) = e11 )
| ( op1(e13,e12) = e12 )
| ( op1(e13,e12) = e13 ) )
& ( ( op1(e13,e13) = e10 )
| ( op1(e13,e13) = e11 )
| ( op1(e13,e13) = e12 )
| ( op1(e13,e13) = e13 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
tff(f_1316,axiom,
( ( h4(e11) = e21 )
& ( h4(e12) = e20 )
& ( h4(e10) = op2(op2(e20,e21),op2(e20,e21)) )
& ( h4(e13) = op2(e20,e21) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
tff(f_534,axiom,
( ( ( op2(e20,e20) = e20 )
| ( op2(e20,e20) = e21 )
| ( op2(e20,e20) = e22 )
| ( op2(e20,e20) = e23 ) )
& ( ( op2(e20,e21) = e20 )
| ( op2(e20,e21) = e21 )
| ( op2(e20,e21) = e22 )
| ( op2(e20,e21) = e23 ) )
& ( ( op2(e20,e22) = e20 )
| ( op2(e20,e22) = e21 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e22) = e23 ) )
& ( ( op2(e20,e23) = e20 )
| ( op2(e20,e23) = e21 )
| ( op2(e20,e23) = e22 )
| ( op2(e20,e23) = e23 ) )
& ( ( op2(e21,e20) = e20 )
| ( op2(e21,e20) = e21 )
| ( op2(e21,e20) = e22 )
| ( op2(e21,e20) = e23 ) )
& ( ( op2(e21,e21) = e20 )
| ( op2(e21,e21) = e21 )
| ( op2(e21,e21) = e22 )
| ( op2(e21,e21) = e23 ) )
& ( ( op2(e21,e22) = e20 )
| ( op2(e21,e22) = e21 )
| ( op2(e21,e22) = e22 )
| ( op2(e21,e22) = e23 ) )
& ( ( op2(e21,e23) = e20 )
| ( op2(e21,e23) = e21 )
| ( op2(e21,e23) = e22 )
| ( op2(e21,e23) = e23 ) )
& ( ( op2(e22,e20) = e20 )
| ( op2(e22,e20) = e21 )
| ( op2(e22,e20) = e22 )
| ( op2(e22,e20) = e23 ) )
& ( ( op2(e22,e21) = e20 )
| ( op2(e22,e21) = e21 )
| ( op2(e22,e21) = e22 )
| ( op2(e22,e21) = e23 ) )
& ( ( op2(e22,e22) = e20 )
| ( op2(e22,e22) = e21 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e22) = e23 ) )
& ( ( op2(e22,e23) = e20 )
| ( op2(e22,e23) = e21 )
| ( op2(e22,e23) = e22 )
| ( op2(e22,e23) = e23 ) )
& ( ( op2(e23,e20) = e20 )
| ( op2(e23,e20) = e21 )
| ( op2(e23,e20) = e22 )
| ( op2(e23,e20) = e23 ) )
& ( ( op2(e23,e21) = e20 )
| ( op2(e23,e21) = e21 )
| ( op2(e23,e21) = e22 )
| ( op2(e23,e21) = e23 ) )
& ( ( op2(e23,e22) = e20 )
| ( op2(e23,e22) = e21 )
| ( op2(e23,e22) = e22 )
| ( op2(e23,e22) = e23 ) )
& ( ( op2(e23,e23) = e20 )
| ( op2(e23,e23) = e21 )
| ( op2(e23,e23) = e22 )
| ( op2(e23,e23) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
tff(f_1372,axiom,
( ( h12(e11) = e23 )
& ( h12(e12) = e22 )
& ( h12(e10) = op2(op2(e22,e23),op2(e22,e23)) )
& ( h12(e13) = op2(e22,e23) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
tff(f_2140,negated_conjecture,
~ ( ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) )
& ( h1(op1(e10,e11)) = op2(h1(e10),h1(e11)) )
& ( h1(op1(e10,e12)) = op2(h1(e10),h1(e12)) )
& ( h1(op1(e10,e13)) = op2(h1(e10),h1(e13)) )
& ( h1(op1(e11,e10)) = op2(h1(e11),h1(e10)) )
& ( h1(op1(e11,e11)) = op2(h1(e11),h1(e11)) )
& ( h1(op1(e11,e12)) = op2(h1(e11),h1(e12)) )
& ( h1(op1(e11,e13)) = op2(h1(e11),h1(e13)) )
& ( h1(op1(e12,e10)) = op2(h1(e12),h1(e10)) )
& ( h1(op1(e12,e11)) = op2(h1(e12),h1(e11)) )
& ( h1(op1(e12,e12)) = op2(h1(e12),h1(e12)) )
& ( h1(op1(e12,e13)) = op2(h1(e12),h1(e13)) )
& ( h1(op1(e13,e10)) = op2(h1(e13),h1(e10)) )
& ( h1(op1(e13,e11)) = op2(h1(e13),h1(e11)) )
& ( h1(op1(e13,e12)) = op2(h1(e13),h1(e12)) )
& ( h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) )
& ( ( h1(e10) = e20 )
| ( h1(e11) = e20 )
| ( h1(e12) = e20 )
| ( h1(e13) = e20 ) )
& ( ( h1(e10) = e21 )
| ( h1(e11) = e21 )
| ( h1(e12) = e21 )
| ( h1(e13) = e21 ) )
& ( ( h1(e10) = e22 )
| ( h1(e11) = e22 )
| ( h1(e12) = e22 )
| ( h1(e13) = e22 ) )
& ( ( h1(e10) = e23 )
| ( h1(e11) = e23 )
| ( h1(e12) = e23 )
| ( h1(e13) = e23 ) ) )
| ( ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
& ( h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) )
& ( h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) )
& ( h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) )
& ( h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) )
& ( h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) )
& ( h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) )
& ( h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) )
& ( h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) )
& ( h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) )
& ( h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) )
& ( h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) )
& ( h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) )
& ( h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) )
& ( h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) )
& ( h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) )
& ( ( h2(e10) = e20 )
| ( h2(e11) = e20 )
| ( h2(e12) = e20 )
| ( h2(e13) = e20 ) )
& ( ( h2(e10) = e21 )
| ( h2(e11) = e21 )
| ( h2(e12) = e21 )
| ( h2(e13) = e21 ) )
& ( ( h2(e10) = e22 )
| ( h2(e11) = e22 )
| ( h2(e12) = e22 )
| ( h2(e13) = e22 ) )
& ( ( h2(e10) = e23 )
| ( h2(e11) = e23 )
| ( h2(e12) = e23 )
| ( h2(e13) = e23 ) ) )
| ( ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
& ( h3(op1(e10,e11)) = op2(h3(e10),h3(e11)) )
& ( h3(op1(e10,e12)) = op2(h3(e10),h3(e12)) )
& ( h3(op1(e10,e13)) = op2(h3(e10),h3(e13)) )
& ( h3(op1(e11,e10)) = op2(h3(e11),h3(e10)) )
& ( h3(op1(e11,e11)) = op2(h3(e11),h3(e11)) )
& ( h3(op1(e11,e12)) = op2(h3(e11),h3(e12)) )
& ( h3(op1(e11,e13)) = op2(h3(e11),h3(e13)) )
& ( h3(op1(e12,e10)) = op2(h3(e12),h3(e10)) )
& ( h3(op1(e12,e11)) = op2(h3(e12),h3(e11)) )
& ( h3(op1(e12,e12)) = op2(h3(e12),h3(e12)) )
& ( h3(op1(e12,e13)) = op2(h3(e12),h3(e13)) )
& ( h3(op1(e13,e10)) = op2(h3(e13),h3(e10)) )
& ( h3(op1(e13,e11)) = op2(h3(e13),h3(e11)) )
& ( h3(op1(e13,e12)) = op2(h3(e13),h3(e12)) )
& ( h3(op1(e13,e13)) = op2(h3(e13),h3(e13)) )
& ( ( h3(e10) = e20 )
| ( h3(e11) = e20 )
| ( h3(e12) = e20 )
| ( h3(e13) = e20 ) )
& ( ( h3(e10) = e21 )
| ( h3(e11) = e21 )
| ( h3(e12) = e21 )
| ( h3(e13) = e21 ) )
& ( ( h3(e10) = e22 )
| ( h3(e11) = e22 )
| ( h3(e12) = e22 )
| ( h3(e13) = e22 ) )
& ( ( h3(e10) = e23 )
| ( h3(e11) = e23 )
| ( h3(e12) = e23 )
| ( h3(e13) = e23 ) ) )
| ( ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
& ( h4(op1(e10,e11)) = op2(h4(e10),h4(e11)) )
& ( h4(op1(e10,e12)) = op2(h4(e10),h4(e12)) )
& ( h4(op1(e10,e13)) = op2(h4(e10),h4(e13)) )
& ( h4(op1(e11,e10)) = op2(h4(e11),h4(e10)) )
& ( h4(op1(e11,e11)) = op2(h4(e11),h4(e11)) )
& ( h4(op1(e11,e12)) = op2(h4(e11),h4(e12)) )
& ( h4(op1(e11,e13)) = op2(h4(e11),h4(e13)) )
& ( h4(op1(e12,e10)) = op2(h4(e12),h4(e10)) )
& ( h4(op1(e12,e11)) = op2(h4(e12),h4(e11)) )
& ( h4(op1(e12,e12)) = op2(h4(e12),h4(e12)) )
& ( h4(op1(e12,e13)) = op2(h4(e12),h4(e13)) )
& ( h4(op1(e13,e10)) = op2(h4(e13),h4(e10)) )
& ( h4(op1(e13,e11)) = op2(h4(e13),h4(e11)) )
& ( h4(op1(e13,e12)) = op2(h4(e13),h4(e12)) )
& ( h4(op1(e13,e13)) = op2(h4(e13),h4(e13)) )
& ( ( h4(e10) = e20 )
| ( h4(e11) = e20 )
| ( h4(e12) = e20 )
| ( h4(e13) = e20 ) )
& ( ( h4(e10) = e21 )
| ( h4(e11) = e21 )
| ( h4(e12) = e21 )
| ( h4(e13) = e21 ) )
& ( ( h4(e10) = e22 )
| ( h4(e11) = e22 )
| ( h4(e12) = e22 )
| ( h4(e13) = e22 ) )
& ( ( h4(e10) = e23 )
| ( h4(e11) = e23 )
| ( h4(e12) = e23 )
| ( h4(e13) = e23 ) ) )
| ( ( h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
& ( h5(op1(e10,e11)) = op2(h5(e10),h5(e11)) )
& ( h5(op1(e10,e12)) = op2(h5(e10),h5(e12)) )
& ( h5(op1(e10,e13)) = op2(h5(e10),h5(e13)) )
& ( h5(op1(e11,e10)) = op2(h5(e11),h5(e10)) )
& ( h5(op1(e11,e11)) = op2(h5(e11),h5(e11)) )
& ( h5(op1(e11,e12)) = op2(h5(e11),h5(e12)) )
& ( h5(op1(e11,e13)) = op2(h5(e11),h5(e13)) )
& ( h5(op1(e12,e10)) = op2(h5(e12),h5(e10)) )
& ( h5(op1(e12,e11)) = op2(h5(e12),h5(e11)) )
& ( h5(op1(e12,e12)) = op2(h5(e12),h5(e12)) )
& ( h5(op1(e12,e13)) = op2(h5(e12),h5(e13)) )
& ( h5(op1(e13,e10)) = op2(h5(e13),h5(e10)) )
& ( h5(op1(e13,e11)) = op2(h5(e13),h5(e11)) )
& ( h5(op1(e13,e12)) = op2(h5(e13),h5(e12)) )
& ( h5(op1(e13,e13)) = op2(h5(e13),h5(e13)) )
& ( ( h5(e10) = e20 )
| ( h5(e11) = e20 )
| ( h5(e12) = e20 )
| ( h5(e13) = e20 ) )
& ( ( h5(e10) = e21 )
| ( h5(e11) = e21 )
| ( h5(e12) = e21 )
| ( h5(e13) = e21 ) )
& ( ( h5(e10) = e22 )
| ( h5(e11) = e22 )
| ( h5(e12) = e22 )
| ( h5(e13) = e22 ) )
& ( ( h5(e10) = e23 )
| ( h5(e11) = e23 )
| ( h5(e12) = e23 )
| ( h5(e13) = e23 ) ) )
| ( ( h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
& ( h6(op1(e10,e11)) = op2(h6(e10),h6(e11)) )
& ( h6(op1(e10,e12)) = op2(h6(e10),h6(e12)) )
& ( h6(op1(e10,e13)) = op2(h6(e10),h6(e13)) )
& ( h6(op1(e11,e10)) = op2(h6(e11),h6(e10)) )
& ( h6(op1(e11,e11)) = op2(h6(e11),h6(e11)) )
& ( h6(op1(e11,e12)) = op2(h6(e11),h6(e12)) )
& ( h6(op1(e11,e13)) = op2(h6(e11),h6(e13)) )
& ( h6(op1(e12,e10)) = op2(h6(e12),h6(e10)) )
& ( h6(op1(e12,e11)) = op2(h6(e12),h6(e11)) )
& ( h6(op1(e12,e12)) = op2(h6(e12),h6(e12)) )
& ( h6(op1(e12,e13)) = op2(h6(e12),h6(e13)) )
& ( h6(op1(e13,e10)) = op2(h6(e13),h6(e10)) )
& ( h6(op1(e13,e11)) = op2(h6(e13),h6(e11)) )
& ( h6(op1(e13,e12)) = op2(h6(e13),h6(e12)) )
& ( h6(op1(e13,e13)) = op2(h6(e13),h6(e13)) )
& ( ( h6(e10) = e20 )
| ( h6(e11) = e20 )
| ( h6(e12) = e20 )
| ( h6(e13) = e20 ) )
& ( ( h6(e10) = e21 )
| ( h6(e11) = e21 )
| ( h6(e12) = e21 )
| ( h6(e13) = e21 ) )
& ( ( h6(e10) = e22 )
| ( h6(e11) = e22 )
| ( h6(e12) = e22 )
| ( h6(e13) = e22 ) )
& ( ( h6(e10) = e23 )
| ( h6(e11) = e23 )
| ( h6(e12) = e23 )
| ( h6(e13) = e23 ) ) )
| ( ( h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
& ( h7(op1(e10,e11)) = op2(h7(e10),h7(e11)) )
& ( h7(op1(e10,e12)) = op2(h7(e10),h7(e12)) )
& ( h7(op1(e10,e13)) = op2(h7(e10),h7(e13)) )
& ( h7(op1(e11,e10)) = op2(h7(e11),h7(e10)) )
& ( h7(op1(e11,e11)) = op2(h7(e11),h7(e11)) )
& ( h7(op1(e11,e12)) = op2(h7(e11),h7(e12)) )
& ( h7(op1(e11,e13)) = op2(h7(e11),h7(e13)) )
& ( h7(op1(e12,e10)) = op2(h7(e12),h7(e10)) )
& ( h7(op1(e12,e11)) = op2(h7(e12),h7(e11)) )
& ( h7(op1(e12,e12)) = op2(h7(e12),h7(e12)) )
& ( h7(op1(e12,e13)) = op2(h7(e12),h7(e13)) )
& ( h7(op1(e13,e10)) = op2(h7(e13),h7(e10)) )
& ( h7(op1(e13,e11)) = op2(h7(e13),h7(e11)) )
& ( h7(op1(e13,e12)) = op2(h7(e13),h7(e12)) )
& ( h7(op1(e13,e13)) = op2(h7(e13),h7(e13)) )
& ( ( h7(e10) = e20 )
| ( h7(e11) = e20 )
| ( h7(e12) = e20 )
| ( h7(e13) = e20 ) )
& ( ( h7(e10) = e21 )
| ( h7(e11) = e21 )
| ( h7(e12) = e21 )
| ( h7(e13) = e21 ) )
& ( ( h7(e10) = e22 )
| ( h7(e11) = e22 )
| ( h7(e12) = e22 )
| ( h7(e13) = e22 ) )
& ( ( h7(e10) = e23 )
| ( h7(e11) = e23 )
| ( h7(e12) = e23 )
| ( h7(e13) = e23 ) ) )
| ( ( h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
& ( h8(op1(e10,e11)) = op2(h8(e10),h8(e11)) )
& ( h8(op1(e10,e12)) = op2(h8(e10),h8(e12)) )
& ( h8(op1(e10,e13)) = op2(h8(e10),h8(e13)) )
& ( h8(op1(e11,e10)) = op2(h8(e11),h8(e10)) )
& ( h8(op1(e11,e11)) = op2(h8(e11),h8(e11)) )
& ( h8(op1(e11,e12)) = op2(h8(e11),h8(e12)) )
& ( h8(op1(e11,e13)) = op2(h8(e11),h8(e13)) )
& ( h8(op1(e12,e10)) = op2(h8(e12),h8(e10)) )
& ( h8(op1(e12,e11)) = op2(h8(e12),h8(e11)) )
& ( h8(op1(e12,e12)) = op2(h8(e12),h8(e12)) )
& ( h8(op1(e12,e13)) = op2(h8(e12),h8(e13)) )
& ( h8(op1(e13,e10)) = op2(h8(e13),h8(e10)) )
& ( h8(op1(e13,e11)) = op2(h8(e13),h8(e11)) )
& ( h8(op1(e13,e12)) = op2(h8(e13),h8(e12)) )
& ( h8(op1(e13,e13)) = op2(h8(e13),h8(e13)) )
& ( ( h8(e10) = e20 )
| ( h8(e11) = e20 )
| ( h8(e12) = e20 )
| ( h8(e13) = e20 ) )
& ( ( h8(e10) = e21 )
| ( h8(e11) = e21 )
| ( h8(e12) = e21 )
| ( h8(e13) = e21 ) )
& ( ( h8(e10) = e22 )
| ( h8(e11) = e22 )
| ( h8(e12) = e22 )
| ( h8(e13) = e22 ) )
& ( ( h8(e10) = e23 )
| ( h8(e11) = e23 )
| ( h8(e12) = e23 )
| ( h8(e13) = e23 ) ) )
| ( ( h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
& ( h9(op1(e10,e11)) = op2(h9(e10),h9(e11)) )
& ( h9(op1(e10,e12)) = op2(h9(e10),h9(e12)) )
& ( h9(op1(e10,e13)) = op2(h9(e10),h9(e13)) )
& ( h9(op1(e11,e10)) = op2(h9(e11),h9(e10)) )
& ( h9(op1(e11,e11)) = op2(h9(e11),h9(e11)) )
& ( h9(op1(e11,e12)) = op2(h9(e11),h9(e12)) )
& ( h9(op1(e11,e13)) = op2(h9(e11),h9(e13)) )
& ( h9(op1(e12,e10)) = op2(h9(e12),h9(e10)) )
& ( h9(op1(e12,e11)) = op2(h9(e12),h9(e11)) )
& ( h9(op1(e12,e12)) = op2(h9(e12),h9(e12)) )
& ( h9(op1(e12,e13)) = op2(h9(e12),h9(e13)) )
& ( h9(op1(e13,e10)) = op2(h9(e13),h9(e10)) )
& ( h9(op1(e13,e11)) = op2(h9(e13),h9(e11)) )
& ( h9(op1(e13,e12)) = op2(h9(e13),h9(e12)) )
& ( h9(op1(e13,e13)) = op2(h9(e13),h9(e13)) )
& ( ( h9(e10) = e20 )
| ( h9(e11) = e20 )
| ( h9(e12) = e20 )
| ( h9(e13) = e20 ) )
& ( ( h9(e10) = e21 )
| ( h9(e11) = e21 )
| ( h9(e12) = e21 )
| ( h9(e13) = e21 ) )
& ( ( h9(e10) = e22 )
| ( h9(e11) = e22 )
| ( h9(e12) = e22 )
| ( h9(e13) = e22 ) )
& ( ( h9(e10) = e23 )
| ( h9(e11) = e23 )
| ( h9(e12) = e23 )
| ( h9(e13) = e23 ) ) )
| ( ( h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
& ( h10(op1(e10,e11)) = op2(h10(e10),h10(e11)) )
& ( h10(op1(e10,e12)) = op2(h10(e10),h10(e12)) )
& ( h10(op1(e10,e13)) = op2(h10(e10),h10(e13)) )
& ( h10(op1(e11,e10)) = op2(h10(e11),h10(e10)) )
& ( h10(op1(e11,e11)) = op2(h10(e11),h10(e11)) )
& ( h10(op1(e11,e12)) = op2(h10(e11),h10(e12)) )
& ( h10(op1(e11,e13)) = op2(h10(e11),h10(e13)) )
& ( h10(op1(e12,e10)) = op2(h10(e12),h10(e10)) )
& ( h10(op1(e12,e11)) = op2(h10(e12),h10(e11)) )
& ( h10(op1(e12,e12)) = op2(h10(e12),h10(e12)) )
& ( h10(op1(e12,e13)) = op2(h10(e12),h10(e13)) )
& ( h10(op1(e13,e10)) = op2(h10(e13),h10(e10)) )
& ( h10(op1(e13,e11)) = op2(h10(e13),h10(e11)) )
& ( h10(op1(e13,e12)) = op2(h10(e13),h10(e12)) )
& ( h10(op1(e13,e13)) = op2(h10(e13),h10(e13)) )
& ( ( h10(e10) = e20 )
| ( h10(e11) = e20 )
| ( h10(e12) = e20 )
| ( h10(e13) = e20 ) )
& ( ( h10(e10) = e21 )
| ( h10(e11) = e21 )
| ( h10(e12) = e21 )
| ( h10(e13) = e21 ) )
& ( ( h10(e10) = e22 )
| ( h10(e11) = e22 )
| ( h10(e12) = e22 )
| ( h10(e13) = e22 ) )
& ( ( h10(e10) = e23 )
| ( h10(e11) = e23 )
| ( h10(e12) = e23 )
| ( h10(e13) = e23 ) ) )
| ( ( h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
& ( h11(op1(e10,e11)) = op2(h11(e10),h11(e11)) )
& ( h11(op1(e10,e12)) = op2(h11(e10),h11(e12)) )
& ( h11(op1(e10,e13)) = op2(h11(e10),h11(e13)) )
& ( h11(op1(e11,e10)) = op2(h11(e11),h11(e10)) )
& ( h11(op1(e11,e11)) = op2(h11(e11),h11(e11)) )
& ( h11(op1(e11,e12)) = op2(h11(e11),h11(e12)) )
& ( h11(op1(e11,e13)) = op2(h11(e11),h11(e13)) )
& ( h11(op1(e12,e10)) = op2(h11(e12),h11(e10)) )
& ( h11(op1(e12,e11)) = op2(h11(e12),h11(e11)) )
& ( h11(op1(e12,e12)) = op2(h11(e12),h11(e12)) )
& ( h11(op1(e12,e13)) = op2(h11(e12),h11(e13)) )
& ( h11(op1(e13,e10)) = op2(h11(e13),h11(e10)) )
& ( h11(op1(e13,e11)) = op2(h11(e13),h11(e11)) )
& ( h11(op1(e13,e12)) = op2(h11(e13),h11(e12)) )
& ( h11(op1(e13,e13)) = op2(h11(e13),h11(e13)) )
& ( ( h11(e10) = e20 )
| ( h11(e11) = e20 )
| ( h11(e12) = e20 )
| ( h11(e13) = e20 ) )
& ( ( h11(e10) = e21 )
| ( h11(e11) = e21 )
| ( h11(e12) = e21 )
| ( h11(e13) = e21 ) )
& ( ( h11(e10) = e22 )
| ( h11(e11) = e22 )
| ( h11(e12) = e22 )
| ( h11(e13) = e22 ) )
& ( ( h11(e10) = e23 )
| ( h11(e11) = e23 )
| ( h11(e12) = e23 )
| ( h11(e13) = e23 ) ) )
| ( ( h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
& ( h12(op1(e10,e11)) = op2(h12(e10),h12(e11)) )
& ( h12(op1(e10,e12)) = op2(h12(e10),h12(e12)) )
& ( h12(op1(e10,e13)) = op2(h12(e10),h12(e13)) )
& ( h12(op1(e11,e10)) = op2(h12(e11),h12(e10)) )
& ( h12(op1(e11,e11)) = op2(h12(e11),h12(e11)) )
& ( h12(op1(e11,e12)) = op2(h12(e11),h12(e12)) )
& ( h12(op1(e11,e13)) = op2(h12(e11),h12(e13)) )
& ( h12(op1(e12,e10)) = op2(h12(e12),h12(e10)) )
& ( h12(op1(e12,e11)) = op2(h12(e12),h12(e11)) )
& ( h12(op1(e12,e12)) = op2(h12(e12),h12(e12)) )
& ( h12(op1(e12,e13)) = op2(h12(e12),h12(e13)) )
& ( h12(op1(e13,e10)) = op2(h12(e13),h12(e10)) )
& ( h12(op1(e13,e11)) = op2(h12(e13),h12(e11)) )
& ( h12(op1(e13,e12)) = op2(h12(e13),h12(e12)) )
& ( h12(op1(e13,e13)) = op2(h12(e13),h12(e13)) )
& ( ( h12(e10) = e20 )
| ( h12(e11) = e20 )
| ( h12(e12) = e20 )
| ( h12(e13) = e20 ) )
& ( ( h12(e10) = e21 )
| ( h12(e11) = e21 )
| ( h12(e12) = e21 )
| ( h12(e13) = e21 ) )
& ( ( h12(e10) = e22 )
| ( h12(e11) = e22 )
| ( h12(e12) = e22 )
| ( h12(e13) = e22 ) )
& ( ( h12(e10) = e23 )
| ( h12(e11) = e23 )
| ( h12(e12) = e23 )
| ( h12(e13) = e23 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
tff(f_1337,axiom,
( ( h7(e11) = e22 )
& ( h7(e12) = e20 )
& ( h7(e10) = op2(op2(e20,e22),op2(e20,e22)) )
& ( h7(e13) = op2(e20,e22) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
tff(c_408,plain,
e21 != e20,
inference(cnfTransformation,[status(thm)],[f_1109]) ).
tff(c_406,plain,
e22 != e20,
inference(cnfTransformation,[status(thm)],[f_1109]) ).
tff(c_1546,plain,
op2(e22,e20) = h2(e13),
inference(cnfTransformation,[status(thm)],[f_1302]) ).
tff(c_398,plain,
e23 != e22,
inference(cnfTransformation,[status(thm)],[f_1109]) ).
tff(c_402,plain,
e22 != e21,
inference(cnfTransformation,[status(thm)],[f_1109]) ).
tff(c_1534,plain,
op2(e22,e21) = e23,
inference(cnfTransformation,[status(thm)],[f_1288]) ).
tff(c_1618,plain,
op2(e21,e23) = h11(e13),
inference(cnfTransformation,[status(thm)],[f_1365]) ).
tff(c_1602,plain,
op2(e23,e22) = h9(e13),
inference(cnfTransformation,[status(thm)],[f_1351]) ).
tff(c_998,plain,
op2(op2(e22,e21),e22) = e21,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14697,plain,
h9(e13) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_1534,c_998]) ).
tff(c_14698,plain,
op2(e23,e22) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_14697,c_1602]) ).
tff(c_988,plain,
op2(op2(e23,e22),e23) = e22,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_15066,plain,
h11(e13) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_1618,c_14698,c_988]) ).
tff(c_1620,plain,
op2(op2(e21,e23),op2(e21,e23)) = h11(e10),
inference(cnfTransformation,[status(thm)],[f_1365]) ).
tff(c_8610,plain,
op2(h11(e13),h11(e13)) = h11(e10),
inference(demodulation,[status(thm),theory(equality)],[c_1618,c_1618,c_1620]) ).
tff(c_15068,plain,
op2(e22,e22) = h11(e10),
inference(demodulation,[status(thm),theory(equality)],[c_15066,c_15066,c_8610]) ).
tff(c_1538,plain,
op2(e21,e20) = h1(e13),
inference(cnfTransformation,[status(thm)],[f_1295]) ).
tff(c_1610,plain,
op2(e20,e23) = h10(e13),
inference(cnfTransformation,[status(thm)],[f_1358]) ).
tff(c_1570,plain,
op2(e22,e21) = h5(e13),
inference(cnfTransformation,[status(thm)],[f_1323]) ).
tff(c_13491,plain,
h5(e13) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_1534,c_1570]) ).
tff(c_1572,plain,
op2(op2(e22,e21),op2(e22,e21)) = h5(e10),
inference(cnfTransformation,[status(thm)],[f_1323]) ).
tff(c_11434,plain,
op2(h5(e13),h5(e13)) = h5(e10),
inference(demodulation,[status(thm),theory(equality)],[c_1570,c_1570,c_1572]) ).
tff(c_1536,plain,
op2(op2(e22,e21),op2(e22,e21)) = e20,
inference(cnfTransformation,[status(thm)],[f_1288]) ).
tff(c_13453,plain,
h5(e10) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_11434,c_1570,c_1570,c_1536]) ).
tff(c_13456,plain,
op2(h5(e13),h5(e13)) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_13453,c_11434]) ).
tff(c_13502,plain,
op2(e23,e23) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_13491,c_13491,c_13456]) ).
tff(c_986,plain,
op2(op2(e23,e23),e23) = e23,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_15426,plain,
h10(e13) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_1610,c_13502,c_986]) ).
tff(c_1010,plain,
op2(op2(e20,e23),e20) = e23,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14612,plain,
op2(h10(e13),e20) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_1610,c_1010]) ).
tff(c_15430,plain,
op2(e23,e20) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_15426,c_14612]) ).
tff(c_376,plain,
op2(e23,e20) != op2(e21,e20),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17617,plain,
h1(e13) != e23,
inference(demodulation,[status(thm),theory(equality)],[c_1538,c_15430,c_376]) ).
tff(c_1604,plain,
op2(op2(e23,e22),op2(e23,e22)) = h9(e10),
inference(cnfTransformation,[status(thm)],[f_1351]) ).
tff(c_9540,plain,
op2(h9(e13),h9(e13)) = h9(e10),
inference(demodulation,[status(thm),theory(equality)],[c_1602,c_1602,c_1604]) ).
tff(c_14699,plain,
op2(e21,e21) = h9(e10),
inference(demodulation,[status(thm),theory(equality)],[c_14697,c_14697,c_9540]) ).
tff(c_366,plain,
op2(e22,e21) != op2(e21,e21),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17622,plain,
h9(e10) != e23,
inference(demodulation,[status(thm),theory(equality)],[c_1534,c_14699,c_366]) ).
tff(c_1594,plain,
op2(e21,e22) = h8(e13),
inference(cnfTransformation,[status(thm)],[f_1344]) ).
tff(c_15067,plain,
op2(e21,e23) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_15066,c_1618]) ).
tff(c_164,plain,
( ( op2(e21,e23) = e23 )
| ( op2(e21,e22) = e23 )
| ( op2(e21,e21) = e23 )
| ( op2(e21,e20) = e23 ) ),
inference(cnfTransformation,[status(thm)],[f_789]) ).
tff(c_17719,plain,
( ( e23 = e22 )
| ( h8(e13) = e23 )
| ( h9(e10) = e23 )
| ( h1(e13) = e23 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1538,c_14699,c_1594,c_15067,c_164]) ).
tff(c_17720,plain,
h8(e13) = e23,
inference(negUnitSimplification,[status(thm)],[c_17617,c_17622,c_398,c_17719]) ).
tff(c_1004,plain,
op2(op2(e21,e22),e21) = e22,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14646,plain,
op2(h8(e13),e21) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_1594,c_1004]) ).
tff(c_17723,plain,
op2(e23,e21) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_17720,c_14646]) ).
tff(c_1578,plain,
op2(e23,e21) = h6(e13),
inference(cnfTransformation,[status(thm)],[f_1330]) ).
tff(c_17740,plain,
h6(e13) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_17723,c_1578]) ).
tff(c_990,plain,
op2(op2(e23,e21),e23) = e21,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_15049,plain,
op2(h6(e13),e23) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_1578,c_990]) ).
tff(c_17756,plain,
op2(e22,e23) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_17740,c_15049]) ).
tff(c_152,plain,
( ( op2(e22,e23) = e22 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e21) = e22 )
| ( op2(e22,e20) = e22 ) ),
inference(cnfTransformation,[status(thm)],[f_789]) ).
tff(c_17825,plain,
( ( e22 = e21 )
| ( h11(e10) = e22 )
| ( e23 = e22 )
| ( h2(e13) = e22 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1546,c_1534,c_15068,c_17756,c_152]) ).
tff(c_17826,plain,
( ( h11(e10) = e22 )
| ( h2(e13) = e22 ) ),
inference(negUnitSimplification,[status(thm)],[c_398,c_402,c_17825]) ).
tff(c_18490,plain,
h2(e13) = e22,
inference(splitLeft,[status(thm)],[c_17826]) ).
tff(c_1000,plain,
op2(op2(e22,e20),e22) = e20,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14680,plain,
op2(h2(e13),e22) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_1546,c_1000]) ).
tff(c_18491,plain,
op2(e22,e22) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_18490,c_14680]) ).
tff(c_18501,plain,
h11(e10) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_18491,c_15068]) ).
tff(c_1580,plain,
op2(op2(e23,e21),op2(e23,e21)) = h6(e10),
inference(cnfTransformation,[status(thm)],[f_1330]) ).
tff(c_10919,plain,
op2(h6(e13),h6(e13)) = h6(e10),
inference(demodulation,[status(thm),theory(equality)],[c_1578,c_1578,c_1580]) ).
tff(c_17758,plain,
op2(e22,e22) = h6(e10),
inference(demodulation,[status(thm),theory(equality)],[c_17740,c_17740,c_10919]) ).
tff(c_17771,plain,
h6(e10) = h11(e10),
inference(demodulation,[status(thm),theory(equality)],[c_15068,c_17758]) ).
tff(c_18510,plain,
h6(e10) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_18501,c_17771]) ).
tff(c_396,plain,
e11 != e10,
inference(cnfTransformation,[status(thm)],[f_1092]) ).
tff(c_1530,plain,
op1(e12,e11) = e13,
inference(cnfTransformation,[status(thm)],[f_1285]) ).
tff(c_1532,plain,
op1(op1(e12,e11),op1(e12,e11)) = e10,
inference(cnfTransformation,[status(thm)],[f_1285]) ).
tff(c_13630,plain,
op1(e13,e13) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_1530,c_1532]) ).
tff(c_442,plain,
op1(op1(e13,e13),e13) = e13,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_16908,plain,
op1(e10,e13) = e13,
inference(demodulation,[status(thm),theory(equality)],[c_13630,c_442]) ).
tff(c_466,plain,
op1(op1(e10,e13),e10) = e13,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_16910,plain,
op1(e13,e10) = e13,
inference(demodulation,[status(thm),theory(equality)],[c_16908,c_466]) ).
tff(c_280,plain,
op1(e13,e10) != op1(e11,e10),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_17662,plain,
op1(e11,e10) != e13,
inference(demodulation,[status(thm),theory(equality)],[c_16910,c_280]) ).
tff(c_270,plain,
op1(e12,e11) != op1(e11,e11),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_17665,plain,
op1(e11,e11) != e13,
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_270]) ).
tff(c_386,plain,
e13 != e12,
inference(cnfTransformation,[status(thm)],[f_1092]) ).
tff(c_454,plain,
op1(op1(e12,e11),e12) = e11,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_15938,plain,
op1(e13,e12) = e11,
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_454]) ).
tff(c_444,plain,
op1(op1(e13,e12),e13) = e12,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_16454,plain,
op1(e11,e13) = e12,
inference(demodulation,[status(thm),theory(equality)],[c_15938,c_444]) ).
tff(c_68,plain,
( ( op1(e11,e13) = e13 )
| ( op1(e11,e12) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e11,e10) = e13 ) ),
inference(cnfTransformation,[status(thm)],[f_407]) ).
tff(c_17908,plain,
( ( e13 = e12 )
| ( op1(e11,e12) = e13 )
| ( op1(e11,e11) = e13 )
| ( op1(e11,e10) = e13 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16454,c_68]) ).
tff(c_17909,plain,
op1(e11,e12) = e13,
inference(negUnitSimplification,[status(thm)],[c_17662,c_17665,c_386,c_17908]) ).
tff(c_460,plain,
op1(op1(e11,e12),e11) = e12,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_17911,plain,
op1(e13,e11) = e12,
inference(demodulation,[status(thm),theory(equality)],[c_17909,c_460]) ).
tff(c_446,plain,
op1(op1(e13,e11),e13) = e11,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_17929,plain,
op1(e12,e13) = e11,
inference(demodulation,[status(thm),theory(equality)],[c_17911,c_446]) ).
tff(c_212,plain,
op1(e12,e13) != op1(e12,e10),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_17956,plain,
op1(e12,e10) != e11,
inference(demodulation,[status(thm),theory(equality)],[c_17929,c_212]) ).
tff(c_388,plain,
e13 != e11,
inference(cnfTransformation,[status(thm)],[f_1092]) ).
tff(c_90,plain,
( ( op1(e13,e10) = e11 )
| ( op1(e12,e10) = e11 )
| ( op1(e11,e10) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(cnfTransformation,[status(thm)],[f_407]) ).
tff(c_17886,plain,
( ( e13 = e11 )
| ( op1(e12,e10) = e11 )
| ( op1(e11,e10) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16910,c_90]) ).
tff(c_17887,plain,
( ( op1(e12,e10) = e11 )
| ( op1(e11,e10) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(negUnitSimplification,[status(thm)],[c_388,c_17886]) ).
tff(c_17970,plain,
( ( op1(e11,e10) = e11 )
| ( op1(e10,e10) = e11 ) ),
inference(negUnitSimplification,[status(thm)],[c_17956,c_17887]) ).
tff(c_18634,plain,
op1(e10,e10) = e11,
inference(splitLeft,[status(thm)],[c_17970]) ).
tff(c_472,plain,
op1(op1(e10,e10),e10) = e10,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_18644,plain,
op1(e11,e10) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_18634,c_472]) ).
tff(c_392,plain,
e13 != e10,
inference(cnfTransformation,[status(thm)],[f_1092]) ).
tff(c_870,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( op1(e11,op1(e12,e11)) = op1(e12,e11) )
| ( op1(e12,op1(e13,e12)) = op1(e13,e12) )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_15839,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( op1(e11,e13) = e13 )
| ( op1(e12,op1(e13,e12)) = op1(e13,e12) )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_1530,c_870]) ).
tff(c_16002,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( op1(e11,e13) = e13 )
| ( op1(e12,e11) = e11 )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15938,c_15938,c_15839]) ).
tff(c_16224,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( op1(e11,e13) = e13 )
| ( e13 = e11 )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_16002]) ).
tff(c_16457,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( e13 = e12 )
| ( e13 = e11 )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16454,c_16224]) ).
tff(c_16911,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( e13 = e12 )
| ( e13 = e11 )
| ( op1(e13,e13) = e13 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16908,c_16908,c_16457]) ).
tff(c_17202,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( e13 = e12 )
| ( e13 = e11 )
| ( e13 = e10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13630,c_16911]) ).
tff(c_17541,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( e13 = e12 )
| ( e13 = e11 ) ),
inference(negUnitSimplification,[status(thm)],[c_392,c_17202]) ).
tff(c_17594,plain,
( ( op1(e10,op1(e11,e10)) = op1(e11,e10) )
| ( e13 = e12 ) ),
inference(negUnitSimplification,[status(thm)],[c_388,c_17541]) ).
tff(c_17602,plain,
op1(e10,op1(e11,e10)) = op1(e11,e10),
inference(negUnitSimplification,[status(thm)],[c_386,c_17594]) ).
tff(c_18748,plain,
e11 = e10,
inference(demodulation,[status(thm),theory(equality)],[c_18644,c_18634,c_18644,c_17602]) ).
tff(c_18749,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_396,c_18748]) ).
tff(c_18751,plain,
op1(e10,e10) != e11,
inference(splitRight,[status(thm)],[c_17970]) ).
tff(c_394,plain,
e12 != e10,
inference(cnfTransformation,[status(thm)],[f_1092]) ).
tff(c_260,plain,
op1(e13,e12) != op1(e10,e12),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_17667,plain,
op1(e10,e12) != e11,
inference(demodulation,[status(thm),theory(equality)],[c_15938,c_260]) ).
tff(c_230,plain,
op1(e10,e13) != op1(e10,e12),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_17678,plain,
op1(e10,e12) != e13,
inference(demodulation,[status(thm),theory(equality)],[c_16908,c_230]) ).
tff(c_28,plain,
( ( op1(e10,e12) = e13 )
| ( op1(e10,e12) = e12 )
| ( op1(e10,e12) = e11 )
| ( op1(e10,e12) = e10 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_18023,plain,
( ( op1(e10,e12) = e12 )
| ( op1(e10,e12) = e10 ) ),
inference(negUnitSimplification,[status(thm)],[c_17667,c_17678,c_28]) ).
tff(c_18788,plain,
op1(e10,e12) = e10,
inference(splitLeft,[status(thm)],[c_18023]) ).
tff(c_468,plain,
op1(op1(e10,e12),e10) = e12,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_18791,plain,
op1(e10,e10) = e12,
inference(demodulation,[status(thm),theory(equality)],[c_18788,c_468]) ).
tff(c_18808,plain,
op1(e12,e10) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_18791,c_472]) ).
tff(c_868,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( op1(e11,op1(e12,e11)) = op1(e12,e11) )
| ( op1(e12,op1(e13,e12)) = op1(e13,e12) )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_15840,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( op1(e11,e13) = e13 )
| ( op1(e12,op1(e13,e12)) = op1(e13,e12) )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_1530,c_868]) ).
tff(c_15947,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( op1(e11,e13) = e13 )
| ( op1(e12,e11) = e11 )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15938,c_15938,c_15840]) ).
tff(c_16143,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( op1(e11,e13) = e13 )
| ( e13 = e11 )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_15947]) ).
tff(c_16550,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( e13 = e12 )
| ( e13 = e11 )
| ( op1(e13,op1(e10,e13)) = op1(e10,e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16454,c_16143]) ).
tff(c_16970,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( e13 = e12 )
| ( e13 = e11 )
| ( op1(e13,e13) = e13 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16908,c_16908,c_16550]) ).
tff(c_17264,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( e13 = e12 )
| ( e13 = e11 )
| ( e13 = e10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13630,c_16970]) ).
tff(c_17551,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( e13 = e12 )
| ( e13 = e11 ) ),
inference(negUnitSimplification,[status(thm)],[c_392,c_17264]) ).
tff(c_17595,plain,
( ( op1(e10,op1(e12,e10)) = op1(e12,e10) )
| ( e13 = e12 ) ),
inference(negUnitSimplification,[status(thm)],[c_388,c_17551]) ).
tff(c_17603,plain,
op1(e10,op1(e12,e10)) = op1(e12,e10),
inference(negUnitSimplification,[status(thm)],[c_386,c_17595]) ).
tff(c_18828,plain,
op1(e10,e10) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_18808,c_18808,c_17603]) ).
tff(c_18838,plain,
e12 = e10,
inference(demodulation,[status(thm),theory(equality)],[c_18828,c_18791]) ).
tff(c_18840,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_394,c_18838]) ).
tff(c_18841,plain,
op1(e10,e12) = e12,
inference(splitRight,[status(thm)],[c_18023]) ).
tff(c_238,plain,
op1(e10,e12) != op1(e10,e10),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_18843,plain,
op1(e10,e10) != e12,
inference(demodulation,[status(thm),theory(equality)],[c_18841,c_238]) ).
tff(c_284,plain,
op1(e13,e10) != op1(e10,e10),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_17661,plain,
op1(e10,e10) != e13,
inference(demodulation,[status(thm),theory(equality)],[c_16910,c_284]) ).
tff(c_32,plain,
( ( op1(e10,e10) = e13 )
| ( op1(e10,e10) = e12 )
| ( op1(e10,e10) = e11 )
| ( op1(e10,e10) = e10 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_18021,plain,
( ( op1(e10,e10) = e12 )
| ( op1(e10,e10) = e11 )
| ( op1(e10,e10) = e10 ) ),
inference(negUnitSimplification,[status(thm)],[c_17661,c_32]) ).
tff(c_18935,plain,
op1(e10,e10) = e10,
inference(negUnitSimplification,[status(thm)],[c_18751,c_18843,c_18021]) ).
tff(c_1562,plain,
op2(e20,e21) = h4(e13),
inference(cnfTransformation,[status(thm)],[f_1316]) ).
tff(c_368,plain,
op2(e23,e21) != op2(e20,e21),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17621,plain,
h6(e13) != h4(e13),
inference(demodulation,[status(thm),theory(equality)],[c_1578,c_1562,c_368]) ).
tff(c_17755,plain,
h4(e13) != e22,
inference(demodulation,[status(thm),theory(equality)],[c_17740,c_17621]) ).
tff(c_370,plain,
op2(e22,e21) != op2(e20,e21),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17620,plain,
h4(e13) != e23,
inference(demodulation,[status(thm),theory(equality)],[c_1534,c_1562,c_370]) ).
tff(c_126,plain,
( ( op2(e20,e21) = e23 )
| ( op2(e20,e21) = e22 )
| ( op2(e20,e21) = e21 )
| ( op2(e20,e21) = e20 ) ),
inference(cnfTransformation,[status(thm)],[f_534]) ).
tff(c_17850,plain,
( ( h4(e13) = e23 )
| ( h4(e13) = e22 )
| ( h4(e13) = e21 )
| ( h4(e13) = e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1562,c_1562,c_1562,c_1562,c_126]) ).
tff(c_17851,plain,
( ( h4(e13) = e21 )
| ( h4(e13) = e20 ) ),
inference(negUnitSimplification,[status(thm)],[c_17755,c_17620,c_17850]) ).
tff(c_18326,plain,
h4(e13) = e20,
inference(splitLeft,[status(thm)],[c_17851]) ).
tff(c_1014,plain,
op2(op2(e20,e21),e20) = e21,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14578,plain,
op2(h4(e13),e20) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_1562,c_1014]) ).
tff(c_18329,plain,
op2(e20,e20) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_18326,c_14578]) ).
tff(c_1016,plain,
op2(op2(e20,e20),e20) = e20,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_18414,plain,
h1(e13) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_1538,c_18329,c_1016]) ).
tff(c_400,plain,
e23 != e21,
inference(cnfTransformation,[status(thm)],[f_1109]) ).
tff(c_404,plain,
e23 != e20,
inference(cnfTransformation,[status(thm)],[f_1109]) ).
tff(c_1414,plain,
( ( op2(e20,op2(e21,e20)) = op2(e21,e20) )
| ( op2(e21,op2(e22,e21)) = op2(e22,e21) )
| ( op2(e22,op2(e23,e22)) = op2(e23,e22) )
| ( op2(e23,op2(e20,e23)) = op2(e20,e23) ) ),
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14379,plain,
( ( op2(e20,h1(e13)) = h1(e13) )
| ( h11(e13) = e23 )
| ( op2(e22,h9(e13)) = h9(e13) )
| ( op2(e23,h10(e13)) = h10(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1610,c_1610,c_1602,c_1602,c_1618,c_1534,c_1534,c_1538,c_1538,c_1414]) ).
tff(c_14702,plain,
( ( op2(e20,h1(e13)) = h1(e13) )
| ( h11(e13) = e23 )
| ( op2(e22,e21) = e21 )
| ( op2(e23,h10(e13)) = h10(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14697,c_14697,c_14379]) ).
tff(c_14932,plain,
( ( op2(e20,h1(e13)) = h1(e13) )
| ( h11(e13) = e23 )
| ( e23 = e21 )
| ( op2(e23,h10(e13)) = h10(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1534,c_14702]) ).
tff(c_15081,plain,
( ( op2(e20,h1(e13)) = h1(e13) )
| ( e23 = e22 )
| ( e23 = e21 )
| ( op2(e23,h10(e13)) = h10(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15066,c_14932]) ).
tff(c_15465,plain,
( ( op2(e20,h1(e13)) = h1(e13) )
| ( e23 = e22 )
| ( e23 = e21 )
| ( op2(e23,e23) = e23 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15426,c_15426,c_15081]) ).
tff(c_15561,plain,
( ( op2(e20,h1(e13)) = h1(e13) )
| ( e23 = e22 )
| ( e23 = e21 )
| ( e23 = e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13502,c_15465]) ).
tff(c_17462,plain,
( ( op2(e20,h1(e13)) = h1(e13) )
| ( e23 = e22 )
| ( e23 = e21 ) ),
inference(negUnitSimplification,[status(thm)],[c_404,c_15561]) ).
tff(c_17510,plain,
( ( op2(e20,h1(e13)) = h1(e13) )
| ( e23 = e22 ) ),
inference(negUnitSimplification,[status(thm)],[c_400,c_17462]) ).
tff(c_17522,plain,
op2(e20,h1(e13)) = h1(e13),
inference(negUnitSimplification,[status(thm)],[c_398,c_17510]) ).
tff(c_18434,plain,
e21 = e20,
inference(demodulation,[status(thm),theory(equality)],[c_18414,c_18329,c_18414,c_17522]) ).
tff(c_18435,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_408,c_18434]) ).
tff(c_18436,plain,
h4(e13) = e21,
inference(splitRight,[status(thm)],[c_17851]) ).
tff(c_18441,plain,
op2(e21,e20) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_18436,c_14578]) ).
tff(c_18455,plain,
h1(e13) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_18441,c_1538]) ).
tff(c_190,plain,
( ( op2(e23,e20) = e20 )
| ( op2(e22,e20) = e20 )
| ( op2(e21,e20) = e20 )
| ( op2(e20,e20) = e20 ) ),
inference(cnfTransformation,[status(thm)],[f_789]) ).
tff(c_17693,plain,
( ( e23 = e20 )
| ( h2(e13) = e20 )
| ( h1(e13) = e20 )
| ( op2(e20,e20) = e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1538,c_1546,c_15430,c_190]) ).
tff(c_17694,plain,
( ( h2(e13) = e20 )
| ( h1(e13) = e20 )
| ( op2(e20,e20) = e20 ) ),
inference(negUnitSimplification,[status(thm)],[c_404,c_17693]) ).
tff(c_18912,plain,
( ( e22 = e20 )
| ( e21 = e20 )
| ( op2(e20,e20) = e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18455,c_18490,c_17694]) ).
tff(c_18913,plain,
op2(e20,e20) = e20,
inference(negUnitSimplification,[status(thm)],[c_408,c_406,c_18912]) ).
tff(c_1584,plain,
h6(e11) = e21,
inference(cnfTransformation,[status(thm)],[f_1330]) ).
tff(c_1582,plain,
h6(e12) = e23,
inference(cnfTransformation,[status(thm)],[f_1330]) ).
tff(c_1626,plain,
op2(e22,e23) = h12(e13),
inference(cnfTransformation,[status(thm)],[f_1372]) ).
tff(c_17770,plain,
h12(e13) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_17756,c_1626]) ).
tff(c_1628,plain,
op2(op2(e22,e23),op2(e22,e23)) = h12(e10),
inference(cnfTransformation,[status(thm)],[f_1372]) ).
tff(c_8177,plain,
op2(h12(e13),h12(e13)) = h12(e10),
inference(demodulation,[status(thm),theory(equality)],[c_1626,c_1626,c_1628]) ).
tff(c_17782,plain,
op2(e21,e21) = h12(e10),
inference(demodulation,[status(thm),theory(equality)],[c_17770,c_17770,c_8177]) ).
tff(c_17796,plain,
h9(e10) = h12(e10),
inference(demodulation,[status(thm),theory(equality)],[c_17782,c_14699]) ).
tff(c_996,plain,
op2(op2(e22,e22),e22) = e22,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_15223,plain,
op2(h11(e10),e22) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_15068,c_996]) ).
tff(c_17737,plain,
op2(e21,e22) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_17720,c_1594]) ).
tff(c_4856,plain,
( ( h6(e10) != e20 )
| ( h6(e11) != e21 )
| ( h6(e13) != e22 )
| ( h6(e12) != e23 )
| ( op2(h6(e13),h6(e13)) != h6(op1(e13,e13)) )
| ( op2(h6(e13),h6(e12)) != h6(op1(e13,e12)) )
| ( op2(h6(e13),h6(e11)) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(h6(e12),h6(e13)) != h6(op1(e12,e13)) )
| ( op2(h6(e12),h6(e12)) != h6(op1(e12,e12)) )
| ( op2(h6(e12),h6(e11)) != h6(op1(e12,e11)) )
| ( op2(h6(e12),h6(e10)) != h6(op1(e12,e10)) )
| ( op2(h6(e11),h6(e13)) != h6(op1(e11,e13)) )
| ( op2(h6(e11),h6(e12)) != h6(op1(e11,e12)) )
| ( op2(h6(e11),h6(e11)) != h6(op1(e11,e11)) )
| ( op2(h6(e11),h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),h6(e12)) != h6(op1(e10,e12)) )
| ( op2(h6(e10),h6(e11)) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(cnfTransformation,[status(thm)],[f_2140]) ).
tff(c_10587,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( h6(e12) != e23 )
| ( op2(h6(e13),h6(e13)) != h6(op1(e13,e13)) )
| ( op2(h6(e13),h6(e12)) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(h6(e12),h6(e13)) != h6(op1(e12,e13)) )
| ( op2(h6(e12),h6(e12)) != h6(op1(e12,e12)) )
| ( op2(h6(e12),e21) != h6(op1(e12,e11)) )
| ( op2(h6(e12),h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( op2(e21,h6(e12)) != h6(op1(e11,e12)) )
| ( h6(op1(e11,e11)) != op2(e21,e21) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),h6(e12)) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1584,c_1584,c_1584,c_1584,c_1584,c_1584,c_1584,c_1584,c_1584,c_4856]) ).
tff(c_10847,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),h6(e13)) != h6(op1(e13,e13)) )
| ( op2(h6(e13),e23) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != op2(e23,e23) )
| ( h6(op1(e12,e11)) != op2(e23,e21) )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != op2(e21,e23) )
| ( h6(op1(e11,e11)) != op2(e21,e21) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1582,c_1582,c_1582,c_1582,c_1582,c_1582,c_1582,c_1582,c_1582,c_10587]) ).
tff(c_10914,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),h6(e13)) != h6(op1(e13,e13)) )
| ( op2(h6(e13),e23) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != op2(e23,e23) )
| ( h6(op1(e12,e11)) != op2(e23,e21) )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != h11(e13) )
| ( h6(op1(e11,e11)) != op2(e21,e21) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1618,c_10847]) ).
tff(c_10947,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),h6(e13)) != h6(op1(e13,e13)) )
| ( op2(h6(e13),e23) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != op2(e23,e23) )
| ( h6(op1(e12,e11)) != h6(e13) )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != h11(e13) )
| ( h6(op1(e11,e11)) != op2(e21,e21) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1578,c_10914]) ).
tff(c_10963,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( h6(op1(e13,e13)) != h6(e10) )
| ( op2(h6(e13),e23) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != op2(e23,e23) )
| ( h6(op1(e12,e11)) != h6(e13) )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != h11(e13) )
| ( h6(op1(e11,e11)) != op2(e21,e21) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10919,c_10947]) ).
tff(c_13570,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( h6(op1(e13,e13)) != h6(e10) )
| ( op2(h6(e13),e23) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( h6(op1(e12,e11)) != h6(e13) )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != h11(e13) )
| ( h6(op1(e11,e11)) != op2(e21,e21) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13502,c_10963]) ).
tff(c_13885,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( h6(op1(e13,e13)) != h6(e10) )
| ( op2(h6(e13),e23) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != h11(e13) )
| ( h6(op1(e11,e11)) != op2(e21,e21) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_13570]) ).
tff(c_14239,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),e23) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != h11(e13) )
| ( h6(op1(e11,e11)) != op2(e21,e21) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13630,c_13885]) ).
tff(c_14840,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),e23) != h6(op1(e13,e12)) )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != h11(e13) )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14699,c_14239]) ).
tff(c_15057,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( h6(op1(e13,e12)) != e21 )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != h11(e13) )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15049,c_14840]) ).
tff(c_15215,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( h6(op1(e13,e12)) != e21 )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15066,c_15057]) ).
tff(c_15992,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( h6(e11) != e21 )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15938,c_15215]) ).
tff(c_16209,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(op1(e11,e13)) )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1584,c_15992]) ).
tff(c_16582,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != h6(e12) )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16454,c_16209]) ).
tff(c_16795,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != e23 )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(op1(e10,e13)) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1582,c_16582]) ).
tff(c_16992,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(op1(e13,e10)) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != e23 )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(e13) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16908,c_16795]) ).
tff(c_17296,plain,
( ( h6(e10) != e20 )
| ( h6(e13) != e22 )
| ( op2(h6(e13),e21) != h6(op1(e13,e11)) )
| ( op2(h6(e13),h6(e10)) != h6(e13) )
| ( op2(e23,h6(e13)) != h6(op1(e12,e13)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,h6(e13)) != e23 )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),h6(e13)) != h6(e13) )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16910,c_16992]) ).
tff(c_17754,plain,
( ( h6(e10) != e20 )
| ( h6(op1(e13,e11)) != op2(e22,e21) )
| ( op2(e22,h6(e10)) != e22 )
| ( h6(op1(e12,e13)) != op2(e23,e22) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( op2(e21,e22) != e23 )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),e22) != e22 )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17740,c_17740,c_17740,c_17740,c_17740,c_17740,c_17740,c_17740,c_17296]) ).
tff(c_17768,plain,
( ( h6(e10) != e20 )
| ( h6(op1(e13,e11)) != e23 )
| ( op2(e22,h6(e10)) != e22 )
| ( h6(op1(e12,e13)) != e21 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h6(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h6(e10)) != h6(op1(e11,e10)) )
| ( op2(h6(e10),e22) != e22 )
| ( op2(h6(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h6(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h6(e10),h6(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17737,c_14698,c_1534,c_17754]) ).
tff(c_17772,plain,
( ( h11(e10) != e20 )
| ( h6(op1(e13,e11)) != e23 )
| ( op2(e22,h11(e10)) != e22 )
| ( h6(op1(e12,e13)) != e21 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( op2(h11(e10),e22) != e22 )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h11(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h11(e10),h11(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17771,c_17771,c_17771,c_17771,c_17771,c_17771,c_17771,c_17771,c_17771,c_17768]) ).
tff(c_17789,plain,
( ( h11(e10) != e20 )
| ( h6(op1(e13,e11)) != e23 )
| ( op2(e22,h11(e10)) != e22 )
| ( h6(op1(e12,e13)) != e21 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h9(e10) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h11(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h11(e10),h11(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15223,c_17772]) ).
tff(c_17808,plain,
( ( h11(e10) != e20 )
| ( h6(op1(e13,e11)) != e23 )
| ( op2(e22,h11(e10)) != e22 )
| ( h6(op1(e12,e13)) != e21 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e11,e12)) != e22 )
| ( h6(op1(e11,e11)) != h12(e10) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h11(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h11(e10),h11(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17796,c_17789]) ).
tff(c_17919,plain,
( ( h11(e10) != e20 )
| ( h6(op1(e13,e11)) != e23 )
| ( op2(e22,h11(e10)) != e22 )
| ( h6(op1(e12,e13)) != e21 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(e13) != e22 )
| ( h6(op1(e11,e11)) != h12(e10) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h11(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h11(e10),h11(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17909,c_17808]) ).
tff(c_17938,plain,
( ( h11(e10) != e20 )
| ( op2(e22,h11(e10)) != e22 )
| ( h6(op1(e12,e13)) != e21 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e11,e11)) != h12(e10) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h11(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h11(e10),h11(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17740,c_1582,c_17911,c_17919]) ).
tff(c_17960,plain,
( ( h11(e10) != e20 )
| ( op2(e22,h11(e10)) != e22 )
| ( h6(e11) != e21 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e11,e11)) != h12(e10) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h11(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h11(e10),h11(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17929,c_17938]) ).
tff(c_17974,plain,
( ( h11(e10) != e20 )
| ( op2(e22,h11(e10)) != e22 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e11,e11)) != h12(e10) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h11(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h11(e10),h11(e10)) != h6(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1584,c_17960]) ).
tff(c_18231,plain,
op2(h11(e10),h11(e10)) != h6(op1(e10,e10)),
inference(splitLeft,[status(thm)],[c_17974]) ).
tff(c_18508,plain,
h6(op1(e10,e10)) != op2(e20,e20),
inference(demodulation,[status(thm),theory(equality)],[c_18501,c_18501,c_18231]) ).
tff(c_18922,plain,
h6(op1(e10,e10)) != e20,
inference(demodulation,[status(thm),theory(equality)],[c_18913,c_18508]) ).
tff(c_18936,plain,
h6(e10) != e20,
inference(demodulation,[status(thm),theory(equality)],[c_18935,c_18922]) ).
tff(c_18953,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18510,c_18936]) ).
tff(c_18954,plain,
h11(e10) = e22,
inference(splitRight,[status(thm)],[c_17826]) ).
tff(c_1586,plain,
op2(e20,e22) = h7(e13),
inference(cnfTransformation,[status(thm)],[f_1337]) ).
tff(c_358,plain,
op2(e22,e22) != op2(e20,e22),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17626,plain,
h7(e13) != h11(e10),
inference(demodulation,[status(thm),theory(equality)],[c_1586,c_15068,c_358]) ).
tff(c_18959,plain,
h7(e13) != e22,
inference(demodulation,[status(thm),theory(equality)],[c_18954,c_17626]) ).
tff(c_356,plain,
op2(e23,e22) != op2(e20,e22),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17627,plain,
h7(e13) != e21,
inference(demodulation,[status(thm),theory(equality)],[c_1586,c_14698,c_356]) ).
tff(c_15427,plain,
op2(e20,e23) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_15426,c_1610]) ).
tff(c_326,plain,
op2(e20,e23) != op2(e20,e22),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17642,plain,
h7(e13) != e23,
inference(demodulation,[status(thm),theory(equality)],[c_15427,c_1586,c_326]) ).
tff(c_124,plain,
( ( op2(e20,e22) = e23 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e22) = e21 )
| ( op2(e20,e22) = e20 ) ),
inference(cnfTransformation,[status(thm)],[f_534]) ).
tff(c_17852,plain,
( ( h7(e13) = e23 )
| ( h7(e13) = e22 )
| ( h7(e13) = e21 )
| ( h7(e13) = e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1586,c_1586,c_1586,c_1586,c_124]) ).
tff(c_17853,plain,
( ( h7(e13) = e22 )
| ( h7(e13) = e20 ) ),
inference(negUnitSimplification,[status(thm)],[c_17627,c_17642,c_17852]) ).
tff(c_18983,plain,
h7(e13) = e20,
inference(negUnitSimplification,[status(thm)],[c_18959,c_17853]) ).
tff(c_1012,plain,
op2(op2(e20,e22),e20) = e22,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14595,plain,
op2(h7(e13),e20) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_1586,c_1012]) ).
tff(c_18986,plain,
op2(e20,e20) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_18983,c_14595]) ).
tff(c_19010,plain,
h2(e13) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_1546,c_18986,c_1016]) ).
tff(c_1412,plain,
( ( op2(e20,op2(e22,e20)) = op2(e22,e20) )
| ( op2(e21,op2(e22,e21)) = op2(e22,e21) )
| ( op2(e22,op2(e23,e22)) = op2(e23,e22) )
| ( op2(e23,op2(e20,e23)) = op2(e20,e23) ) ),
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14380,plain,
( ( op2(e20,h2(e13)) = h2(e13) )
| ( h11(e13) = e23 )
| ( op2(e22,h9(e13)) = h9(e13) )
| ( op2(e23,h10(e13)) = h10(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1610,c_1610,c_1602,c_1602,c_1618,c_1534,c_1534,c_1546,c_1546,c_1412]) ).
tff(c_14703,plain,
( ( op2(e20,h2(e13)) = h2(e13) )
| ( h11(e13) = e23 )
| ( op2(e22,e21) = e21 )
| ( op2(e23,h10(e13)) = h10(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14697,c_14697,c_14380]) ).
tff(c_14933,plain,
( ( op2(e20,h2(e13)) = h2(e13) )
| ( h11(e13) = e23 )
| ( e23 = e21 )
| ( op2(e23,h10(e13)) = h10(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1534,c_14703]) ).
tff(c_15116,plain,
( ( op2(e20,h2(e13)) = h2(e13) )
| ( e23 = e22 )
| ( e23 = e21 )
| ( op2(e23,h10(e13)) = h10(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15066,c_14933]) ).
tff(c_15440,plain,
( ( op2(e20,h2(e13)) = h2(e13) )
| ( e23 = e22 )
| ( e23 = e21 )
| ( op2(e23,e23) = e23 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_15426,c_15426,c_15116]) ).
tff(c_15539,plain,
( ( op2(e20,h2(e13)) = h2(e13) )
| ( e23 = e22 )
| ( e23 = e21 )
| ( e23 = e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_13502,c_15440]) ).
tff(c_17461,plain,
( ( op2(e20,h2(e13)) = h2(e13) )
| ( e23 = e22 )
| ( e23 = e21 ) ),
inference(negUnitSimplification,[status(thm)],[c_404,c_15539]) ).
tff(c_17509,plain,
( ( op2(e20,h2(e13)) = h2(e13) )
| ( e23 = e22 ) ),
inference(negUnitSimplification,[status(thm)],[c_400,c_17461]) ).
tff(c_17521,plain,
op2(e20,h2(e13)) = h2(e13),
inference(negUnitSimplification,[status(thm)],[c_398,c_17509]) ).
tff(c_19044,plain,
e22 = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19010,c_18986,c_19010,c_17521]) ).
tff(c_19045,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_406,c_19044]) ).
tff(c_19046,plain,
( ( op2(h11(e10),e21) != h6(op1(e10,e11)) )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( h6(op1(e11,e11)) != h12(e10) )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e22,h11(e10)) != e22 )
| ( h11(e10) != e20 ) ),
inference(splitRight,[status(thm)],[c_17974]) ).
tff(c_19113,plain,
h11(e10) != e20,
inference(splitLeft,[status(thm)],[c_19046]) ).
tff(c_19261,plain,
h7(e13) = e20,
inference(splitLeft,[status(thm)],[c_17853]) ).
tff(c_19263,plain,
op2(e20,e20) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_19261,c_14595]) ).
tff(c_19276,plain,
op2(e22,e20) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19263,c_1016]) ).
tff(c_19287,plain,
h2(e13) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19276,c_1546]) ).
tff(c_19340,plain,
e22 = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19287,c_19263,c_19287,c_17521]) ).
tff(c_19341,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_406,c_19340]) ).
tff(c_19342,plain,
h7(e13) = e22,
inference(splitRight,[status(thm)],[c_17853]) ).
tff(c_19345,plain,
op2(e22,e20) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_19342,c_14595]) ).
tff(c_19355,plain,
h2(e13) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_19345,c_1546]) ).
tff(c_19361,plain,
op2(e22,e22) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19355,c_14680]) ).
tff(c_19373,plain,
h11(e10) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19361,c_15068]) ).
tff(c_19375,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19113,c_19373]) ).
tff(c_19377,plain,
h11(e10) = e20,
inference(splitRight,[status(thm)],[c_19046]) ).
tff(c_19383,plain,
h6(e10) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19377,c_17771]) ).
tff(c_256,plain,
op1(e13,e12) != op1(e11,e12),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_17668,plain,
op1(e11,e12) != e11,
inference(demodulation,[status(thm),theory(equality)],[c_15938,c_256]) ).
tff(c_390,plain,
e12 != e11,
inference(cnfTransformation,[status(thm)],[f_1092]) ).
tff(c_76,plain,
( ( op1(e11,e13) = e11 )
| ( op1(e11,e12) = e11 )
| ( op1(e11,e11) = e11 )
| ( op1(e11,e10) = e11 ) ),
inference(cnfTransformation,[status(thm)],[f_407]) ).
tff(c_17900,plain,
( ( e12 = e11 )
| ( op1(e11,e12) = e11 )
| ( op1(e11,e11) = e11 )
| ( op1(e11,e10) = e11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16454,c_76]) ).
tff(c_17901,plain,
( ( op1(e11,e11) = e11 )
| ( op1(e11,e10) = e11 ) ),
inference(negUnitSimplification,[status(thm)],[c_17668,c_390,c_17900]) ).
tff(c_19901,plain,
op1(e11,e10) = e11,
inference(splitLeft,[status(thm)],[c_17901]) ).
tff(c_464,plain,
op1(op1(e11,e10),e11) = e10,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_19903,plain,
op1(e11,e11) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_19901,c_464]) ).
tff(c_380,plain,
op2(e23,e20) != op2(e20,e20),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17615,plain,
op2(e20,e20) != e23,
inference(demodulation,[status(thm),theory(equality)],[c_15430,c_380]) ).
tff(c_64,plain,
( ( op1(e12,e13) = e10 )
| ( op1(e12,e12) = e10 )
| ( op1(e12,e11) = e10 )
| ( op1(e12,e10) = e10 ) ),
inference(cnfTransformation,[status(thm)],[f_407]) ).
tff(c_17989,plain,
( ( e11 = e10 )
| ( op1(e12,e12) = e10 )
| ( e13 = e10 )
| ( op1(e12,e10) = e10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1530,c_17929,c_64]) ).
tff(c_17990,plain,
( ( op1(e12,e12) = e10 )
| ( op1(e12,e10) = e10 ) ),
inference(negUnitSimplification,[status(thm)],[c_392,c_396,c_17989]) ).
tff(c_19797,plain,
op1(e12,e10) = e10,
inference(splitLeft,[status(thm)],[c_17990]) ).
tff(c_456,plain,
op1(op1(e12,e10),e12) = e10,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_19801,plain,
op1(e10,e12) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_19797,c_456]) ).
tff(c_19812,plain,
op1(e10,e10) = e12,
inference(demodulation,[status(thm),theory(equality)],[c_19801,c_468]) ).
tff(c_19047,plain,
op2(h11(e10),h11(e10)) = h6(op1(e10,e10)),
inference(splitRight,[status(thm)],[c_17974]) ).
tff(c_19380,plain,
h6(op1(e10,e10)) = op2(e20,e20),
inference(demodulation,[status(thm),theory(equality)],[c_19377,c_19377,c_19047]) ).
tff(c_19831,plain,
op2(e20,e20) = h6(e12),
inference(demodulation,[status(thm),theory(equality)],[c_19812,c_19380]) ).
tff(c_19842,plain,
op2(e20,e20) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_1582,c_19831]) ).
tff(c_19844,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17615,c_19842]) ).
tff(c_19845,plain,
op1(e12,e12) = e10,
inference(splitRight,[status(thm)],[c_17990]) ).
tff(c_452,plain,
op1(op1(e12,e12),e12) = e12,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_19849,plain,
op1(e10,e12) = e12,
inference(demodulation,[status(thm),theory(equality)],[c_19845,c_452]) ).
tff(c_19859,plain,
op1(e12,e10) = e12,
inference(demodulation,[status(thm),theory(equality)],[c_19849,c_468]) ).
tff(c_19469,plain,
h4(e13) = e20,
inference(splitLeft,[status(thm)],[c_17851]) ).
tff(c_19471,plain,
op2(e20,e20) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_19469,c_14578]) ).
tff(c_19500,plain,
h1(e13) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_1538,c_19471,c_1016]) ).
tff(c_19502,plain,
op2(e20,e20) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19500,c_19500,c_17522]) ).
tff(c_19520,plain,
e21 = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19502,c_19471]) ).
tff(c_19522,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_408,c_19520]) ).
tff(c_19523,plain,
h4(e13) = e21,
inference(splitRight,[status(thm)],[c_17851]) ).
tff(c_336,plain,
op2(e20,e21) != op2(e20,e20),
inference(cnfTransformation,[status(thm)],[f_1075]) ).
tff(c_17637,plain,
op2(e20,e20) != h4(e13),
inference(demodulation,[status(thm),theory(equality)],[c_1562,c_336]) ).
tff(c_19527,plain,
op2(e20,e20) != e21,
inference(demodulation,[status(thm),theory(equality)],[c_19523,c_17637]) ).
tff(c_80,plain,
( ( op1(e11,e13) = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e11,e10) = e10 ) ),
inference(cnfTransformation,[status(thm)],[f_407]) ).
tff(c_17896,plain,
( ( e12 = e10 )
| ( op1(e11,e12) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e11,e10) = e10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16454,c_80]) ).
tff(c_17897,plain,
( ( op1(e11,e12) = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e11,e10) = e10 ) ),
inference(negUnitSimplification,[status(thm)],[c_394,c_17896]) ).
tff(c_17927,plain,
( ( e13 = e10 )
| ( op1(e11,e11) = e10 )
| ( op1(e11,e10) = e10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_17909,c_17897]) ).
tff(c_17951,plain,
( ( op1(e11,e11) = e10 )
| ( op1(e11,e10) = e10 ) ),
inference(negUnitSimplification,[status(thm)],[c_392,c_17927]) ).
tff(c_19667,plain,
op1(e11,e10) = e10,
inference(splitLeft,[status(thm)],[c_17951]) ).
tff(c_19670,plain,
op1(e10,e11) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_19667,c_464]) ).
tff(c_470,plain,
op1(op1(e10,e11),e10) = e11,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_19681,plain,
op1(e10,e10) = e11,
inference(demodulation,[status(thm),theory(equality)],[c_19670,c_470]) ).
tff(c_19702,plain,
op2(e20,e20) = h6(e11),
inference(demodulation,[status(thm),theory(equality)],[c_19681,c_19380]) ).
tff(c_19713,plain,
op2(e20,e20) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_1584,c_19702]) ).
tff(c_19715,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19527,c_19713]) ).
tff(c_19716,plain,
op1(e11,e11) = e10,
inference(splitRight,[status(thm)],[c_17951]) ).
tff(c_462,plain,
op1(op1(e11,e11),e11) = e11,
inference(cnfTransformation,[status(thm)],[f_1219]) ).
tff(c_19718,plain,
op1(e10,e11) = e11,
inference(demodulation,[status(thm),theory(equality)],[c_19716,c_462]) ).
tff(c_19525,plain,
op2(e20,e21) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_19523,c_1562]) ).
tff(c_19526,plain,
op2(e21,e20) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_19523,c_14578]) ).
tff(c_19540,plain,
h1(e13) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_19526,c_1538]) ).
tff(c_1008,plain,
op2(op2(e21,e20),e21) = e20,
inference(cnfTransformation,[status(thm)],[f_1282]) ).
tff(c_14629,plain,
op2(h1(e13),e21) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_1538,c_1008]) ).
tff(c_19546,plain,
op2(e21,e21) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19540,c_14629]) ).
tff(c_19556,plain,
h12(e10) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19546,c_17782]) ).
tff(c_19417,plain,
h7(e13) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_1586,c_19377,c_15223]) ).
tff(c_19418,plain,
op2(e22,e20) = e22,
inference(demodulation,[status(thm),theory(equality)],[c_19417,c_14595]) ).
tff(c_19376,plain,
( ( op2(e22,h11(e10)) != e22 )
| ( h6(op1(e12,e12)) != e20 )
| ( op2(e23,h11(e10)) != h6(op1(e12,e10)) )
| ( h6(op1(e11,e11)) != h12(e10) )
| ( op2(e21,h11(e10)) != h6(op1(e11,e10)) )
| ( op2(h11(e10),e23) != h6(op1(e10,e12)) )
| ( op2(h11(e10),e21) != h6(op1(e10,e11)) ) ),
inference(splitRight,[status(thm)],[c_19046]) ).
tff(c_19611,plain,
( ( h6(op1(e12,e12)) != e20 )
| ( h6(op1(e12,e10)) != e23 )
| ( h6(op1(e11,e11)) != e20 )
| ( h6(op1(e11,e10)) != e21 )
| ( h6(op1(e10,e12)) != e23 )
| ( h6(op1(e10,e11)) != e21 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_19525,c_19377,c_15427,c_19377,c_19526,c_19377,c_19556,c_15430,c_19377,c_19418,c_19377,c_19376]) ).
tff(c_19612,plain,
h6(op1(e10,e11)) != e21,
inference(splitLeft,[status(thm)],[c_19611]) ).
tff(c_19727,plain,
h6(e11) != e21,
inference(demodulation,[status(thm),theory(equality)],[c_19718,c_19612]) ).
tff(c_19735,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1584,c_19727]) ).
tff(c_19736,plain,
( ( h6(op1(e10,e12)) != e23 )
| ( h6(op1(e11,e10)) != e21 )
| ( h6(op1(e11,e11)) != e20 )
| ( h6(op1(e12,e10)) != e23 )
| ( h6(op1(e12,e12)) != e20 ) ),
inference(splitRight,[status(thm)],[c_19611]) ).
tff(c_19867,plain,
( ( h6(op1(e11,e10)) != e21 )
| ( h6(op1(e11,e11)) != e20 )
| ( h6(op1(e12,e10)) != e23 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_19383,c_19845,c_1582,c_19849,c_19736]) ).
tff(c_19868,plain,
h6(op1(e12,e10)) != e23,
inference(splitLeft,[status(thm)],[c_19867]) ).
tff(c_19881,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1582,c_19859,c_19868]) ).
tff(c_19882,plain,
( ( h6(op1(e11,e11)) != e20 )
| ( h6(op1(e11,e10)) != e21 ) ),
inference(splitRight,[status(thm)],[c_19867]) ).
tff(c_19935,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1584,c_19901,c_19383,c_19903,c_19882]) ).
tff(c_19937,plain,
op1(e11,e10) != e11,
inference(splitRight,[status(thm)],[c_17901]) ).
tff(c_224,plain,
op1(e11,e13) != op1(e11,e10),
inference(cnfTransformation,[status(thm)],[f_932]) ).
tff(c_17679,plain,
op1(e11,e10) != e12,
inference(demodulation,[status(thm),theory(equality)],[c_16454,c_224]) ).
tff(c_24,plain,
( ( op1(e11,e10) = e13 )
| ( op1(e11,e10) = e12 )
| ( op1(e11,e10) = e11 )
| ( op1(e11,e10) = e10 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_18026,plain,
( ( op1(e11,e10) = e11 )
| ( op1(e11,e10) = e10 ) ),
inference(negUnitSimplification,[status(thm)],[c_17679,c_17662,c_24]) ).
tff(c_19949,plain,
op1(e11,e10) = e10,
inference(negUnitSimplification,[status(thm)],[c_19937,c_18026]) ).
tff(c_19951,plain,
op1(e10,e11) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_19949,c_464]) ).
tff(c_19737,plain,
h6(op1(e10,e11)) = e21,
inference(splitRight,[status(thm)],[c_19611]) ).
tff(c_19960,plain,
h6(e10) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_19951,c_19737]) ).
tff(c_19965,plain,
e21 = e20,
inference(demodulation,[status(thm),theory(equality)],[c_19383,c_19960]) ).
tff(c_19967,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_408,c_19965]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.07 % Problem : ALG105+1 : TPTP v9.0.0. Released v2.7.0.
% 0.06/0.07 % 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.07/0.26 % Computer : n027.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % WCLimit : 300
% 0.07/0.26 % DateTime : Sun Apr 6 07:01:05 EDT 2025
% 0.07/0.26 % CPUTime :
% 170.35/144.75 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 170.35/144.80
% 170.35/144.80 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------