%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ALG016+1 : TPTP v9.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 05:23:58 PM UTC 2025
% Result : Theorem 27.69s 11.09s
% Output : CNFRefutation 27.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 13
% Syntax : Number of formulae : 206 ( 155 unt; 0 typ; 0 def)
% Number of atoms : 1159 (1158 equ)
% Maximal formula atoms : 128 ( 5 avg)
% Number of connectives : 1558 ( 605 ~; 611 |; 342 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 5 avg)
% Maximal term depth : 4 ( 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 : 18 ( 18 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ op2 > op1 > #nlpp > inv2 > inv1 > h4 > h3 > h2 > h1 > unit2 > unit1 > 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(unit2,type,
unit2: $i ).
tff(e20,type,
e20: $i ).
tff(h3,type,
h3: $i > $i ).
tff(h2,type,
h2: $i > $i ).
tff(e13,type,
e13: $i ).
tff(e22,type,
e22: $i ).
tff(op2,type,
op2: ( $i * $i ) > $i ).
tff(unit1,type,
unit1: $i ).
tff(op1,type,
op1: ( $i * $i ) > $i ).
tff(inv2,type,
inv2: $i > $i ).
tff(h1,type,
h1: $i > $i ).
tff(e10,type,
e10: $i ).
tff(e23,type,
e23: $i ).
tff(e12,type,
e12: $i ).
tff(e11,type,
e11: $i ).
tff(inv1,type,
inv1: $i > $i ).
tff(f_1311,axiom,
( ( h3(e12) = e22 )
& ( h3(e10) = op2(op2(e22,op2(e22,e22)),e22) )
& ( h3(e11) = op2(e22,op2(e22,e22)) )
& ( h3(e13) = op2(e22,e22) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
tff(f_1290,axiom,
( ( e20 = op2(op2(e22,op2(e22,e22)),e22) )
& ( e21 = op2(e22,op2(e22,e22)) )
& ( e23 = op2(e22,e22) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
tff(f_1285,axiom,
( ( e10 = op1(op1(e12,op1(e12,e12)),e12) )
& ( e11 = op1(e12,op1(e12,e12)) )
& ( e13 = op1(e12,e12) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
tff(f_992,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/sandbox2/benchmark/theBenchmark.p',ax17) ).
tff(f_279,axiom,
( ( op1(op1(e10,e10),e10) = op1(e10,op1(e10,e10)) )
& ( op1(op1(e10,e10),e11) = op1(e10,op1(e10,e11)) )
& ( op1(op1(e10,e10),e12) = op1(e10,op1(e10,e12)) )
& ( op1(op1(e10,e10),e13) = op1(e10,op1(e10,e13)) )
& ( op1(op1(e10,e11),e10) = op1(e10,op1(e11,e10)) )
& ( op1(op1(e10,e11),e11) = op1(e10,op1(e11,e11)) )
& ( op1(op1(e10,e11),e12) = op1(e10,op1(e11,e12)) )
& ( op1(op1(e10,e11),e13) = op1(e10,op1(e11,e13)) )
& ( op1(op1(e10,e12),e10) = op1(e10,op1(e12,e10)) )
& ( op1(op1(e10,e12),e11) = op1(e10,op1(e12,e11)) )
& ( op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12)) )
& ( op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13)) )
& ( op1(op1(e10,e13),e10) = op1(e10,op1(e13,e10)) )
& ( op1(op1(e10,e13),e11) = op1(e10,op1(e13,e11)) )
& ( op1(op1(e10,e13),e12) = op1(e10,op1(e13,e12)) )
& ( op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13)) )
& ( op1(op1(e11,e10),e10) = op1(e11,op1(e10,e10)) )
& ( op1(op1(e11,e10),e11) = op1(e11,op1(e10,e11)) )
& ( op1(op1(e11,e10),e12) = op1(e11,op1(e10,e12)) )
& ( op1(op1(e11,e10),e13) = op1(e11,op1(e10,e13)) )
& ( op1(op1(e11,e11),e10) = op1(e11,op1(e11,e10)) )
& ( op1(op1(e11,e11),e11) = op1(e11,op1(e11,e11)) )
& ( op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12)) )
& ( op1(op1(e11,e11),e13) = op1(e11,op1(e11,e13)) )
& ( op1(op1(e11,e12),e10) = op1(e11,op1(e12,e10)) )
& ( op1(op1(e11,e12),e11) = op1(e11,op1(e12,e11)) )
& ( op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12)) )
& ( op1(op1(e11,e12),e13) = op1(e11,op1(e12,e13)) )
& ( op1(op1(e11,e13),e10) = op1(e11,op1(e13,e10)) )
& ( op1(op1(e11,e13),e11) = op1(e11,op1(e13,e11)) )
& ( op1(op1(e11,e13),e12) = op1(e11,op1(e13,e12)) )
& ( op1(op1(e11,e13),e13) = op1(e11,op1(e13,e13)) )
& ( op1(op1(e12,e10),e10) = op1(e12,op1(e10,e10)) )
& ( op1(op1(e12,e10),e11) = op1(e12,op1(e10,e11)) )
& ( op1(op1(e12,e10),e12) = op1(e12,op1(e10,e12)) )
& ( op1(op1(e12,e10),e13) = op1(e12,op1(e10,e13)) )
& ( op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10)) )
& ( op1(op1(e12,e11),e11) = op1(e12,op1(e11,e11)) )
& ( op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12)) )
& ( op1(op1(e12,e11),e13) = op1(e12,op1(e11,e13)) )
& ( op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10)) )
& ( op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11)) )
& ( op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)) )
& ( op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13)) )
& ( op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10)) )
& ( op1(op1(e12,e13),e11) = op1(e12,op1(e13,e11)) )
& ( op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12)) )
& ( op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13)) )
& ( op1(op1(e13,e10),e10) = op1(e13,op1(e10,e10)) )
& ( op1(op1(e13,e10),e11) = op1(e13,op1(e10,e11)) )
& ( op1(op1(e13,e10),e12) = op1(e13,op1(e10,e12)) )
& ( op1(op1(e13,e10),e13) = op1(e13,op1(e10,e13)) )
& ( op1(op1(e13,e11),e10) = op1(e13,op1(e11,e10)) )
& ( op1(op1(e13,e11),e11) = op1(e13,op1(e11,e11)) )
& ( op1(op1(e13,e11),e12) = op1(e13,op1(e11,e12)) )
& ( op1(op1(e13,e11),e13) = op1(e13,op1(e11,e13)) )
& ( op1(op1(e13,e12),e10) = op1(e13,op1(e12,e10)) )
& ( op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11)) )
& ( op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12)) )
& ( op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13)) )
& ( op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10)) )
& ( op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11)) )
& ( op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12)) )
& ( op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',ax1) ).
tff(f_1135,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/sandbox2/benchmark/theBenchmark.p',ax18) ).
tff(f_603,axiom,
( ( op2(op2(e20,e20),e20) = op2(e20,op2(e20,e20)) )
& ( op2(op2(e20,e20),e21) = op2(e20,op2(e20,e21)) )
& ( op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22)) )
& ( op2(op2(e20,e20),e23) = op2(e20,op2(e20,e23)) )
& ( op2(op2(e20,e21),e20) = op2(e20,op2(e21,e20)) )
& ( op2(op2(e20,e21),e21) = op2(e20,op2(e21,e21)) )
& ( op2(op2(e20,e21),e22) = op2(e20,op2(e21,e22)) )
& ( op2(op2(e20,e21),e23) = op2(e20,op2(e21,e23)) )
& ( op2(op2(e20,e22),e20) = op2(e20,op2(e22,e20)) )
& ( op2(op2(e20,e22),e21) = op2(e20,op2(e22,e21)) )
& ( op2(op2(e20,e22),e22) = op2(e20,op2(e22,e22)) )
& ( op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23)) )
& ( op2(op2(e20,e23),e20) = op2(e20,op2(e23,e20)) )
& ( op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21)) )
& ( op2(op2(e20,e23),e22) = op2(e20,op2(e23,e22)) )
& ( op2(op2(e20,e23),e23) = op2(e20,op2(e23,e23)) )
& ( op2(op2(e21,e20),e20) = op2(e21,op2(e20,e20)) )
& ( op2(op2(e21,e20),e21) = op2(e21,op2(e20,e21)) )
& ( op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22)) )
& ( op2(op2(e21,e20),e23) = op2(e21,op2(e20,e23)) )
& ( op2(op2(e21,e21),e20) = op2(e21,op2(e21,e20)) )
& ( op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21)) )
& ( op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22)) )
& ( op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23)) )
& ( op2(op2(e21,e22),e20) = op2(e21,op2(e22,e20)) )
& ( op2(op2(e21,e22),e21) = op2(e21,op2(e22,e21)) )
& ( op2(op2(e21,e22),e22) = op2(e21,op2(e22,e22)) )
& ( op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23)) )
& ( op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20)) )
& ( op2(op2(e21,e23),e21) = op2(e21,op2(e23,e21)) )
& ( op2(op2(e21,e23),e22) = op2(e21,op2(e23,e22)) )
& ( op2(op2(e21,e23),e23) = op2(e21,op2(e23,e23)) )
& ( op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20)) )
& ( op2(op2(e22,e20),e21) = op2(e22,op2(e20,e21)) )
& ( op2(op2(e22,e20),e22) = op2(e22,op2(e20,e22)) )
& ( op2(op2(e22,e20),e23) = op2(e22,op2(e20,e23)) )
& ( op2(op2(e22,e21),e20) = op2(e22,op2(e21,e20)) )
& ( op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21)) )
& ( op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22)) )
& ( op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23)) )
& ( op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20)) )
& ( op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21)) )
& ( op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)) )
& ( op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23)) )
& ( op2(op2(e22,e23),e20) = op2(e22,op2(e23,e20)) )
& ( op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21)) )
& ( op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22)) )
& ( op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23)) )
& ( op2(op2(e23,e20),e20) = op2(e23,op2(e20,e20)) )
& ( op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21)) )
& ( op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22)) )
& ( op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23)) )
& ( op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20)) )
& ( op2(op2(e23,e21),e21) = op2(e23,op2(e21,e21)) )
& ( op2(op2(e23,e21),e22) = op2(e23,op2(e21,e22)) )
& ( op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23)) )
& ( op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20)) )
& ( op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21)) )
& ( op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22)) )
& ( op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23)) )
& ( op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20)) )
& ( op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21)) )
& ( op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22)) )
& ( op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
tff(f_476,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/sandbox2/benchmark/theBenchmark.p',ax5) ).
tff(f_1297,axiom,
( ( h1(e12) = e20 )
& ( h1(e10) = op2(op2(e20,op2(e20,e20)),e20) )
& ( h1(e11) = op2(e20,op2(e20,e20)) )
& ( h1(e13) = op2(e20,e20) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
tff(f_1304,axiom,
( ( h2(e12) = e21 )
& ( h2(e10) = op2(op2(e21,op2(e21,e21)),e21) )
& ( h2(e11) = op2(e21,op2(e21,e21)) )
& ( h2(e13) = op2(e21,e21) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax27) ).
tff(f_1318,axiom,
( ( h4(e12) = e23 )
& ( h4(e10) = op2(op2(e23,op2(e23,e23)),e23) )
& ( h4(e11) = op2(e23,op2(e23,e23)) )
& ( h4(e13) = op2(e23,e23) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
tff(f_1574,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 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
tff(c_808,plain,
op2(e22,op2(e22,e22)) = h3(e11),
inference(cnfTransformation,[status(thm)],[f_1311]) ).
tff(c_810,plain,
op2(op2(e22,op2(e22,e22)),e22) = h3(e10),
inference(cnfTransformation,[status(thm)],[f_1311]) ).
tff(c_3703,plain,
op2(h3(e11),e22) = h3(e10),
inference(demodulation,[status(thm),theory(equality)],[c_808,c_810]) ).
tff(c_806,plain,
op2(e22,e22) = h3(e13),
inference(cnfTransformation,[status(thm)],[f_1311]) ).
tff(c_3768,plain,
op2(e22,h3(e13)) = h3(e11),
inference(demodulation,[status(thm),theory(equality)],[c_806,c_808]) ).
tff(c_788,plain,
op2(op2(e22,op2(e22,e22)),e22) = e20,
inference(cnfTransformation,[status(thm)],[f_1290]) ).
tff(c_4925,plain,
h3(e10) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_3703,c_3768,c_806,c_788]) ).
tff(c_780,plain,
op1(e12,op1(e12,e12)) = e11,
inference(cnfTransformation,[status(thm)],[f_1285]) ).
tff(c_782,plain,
op1(op1(e12,op1(e12,e12)),e12) = e10,
inference(cnfTransformation,[status(thm)],[f_1285]) ).
tff(c_5121,plain,
op1(e11,e12) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_780,c_782]) ).
tff(c_584,plain,
op1(e11,e12) != op1(e10,e12),
inference(cnfTransformation,[status(thm)],[f_992]) ).
tff(c_6323,plain,
op1(e10,e12) != e10,
inference(demodulation,[status(thm),theory(equality)],[c_5121,c_584]) ).
tff(c_778,plain,
op1(e12,e12) = e13,
inference(cnfTransformation,[status(thm)],[f_1285]) ).
tff(c_108,plain,
op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6891,plain,
op1(e11,e13) = op1(e10,e12),
inference(demodulation,[status(thm),theory(equality)],[c_778,c_5121,c_108]) ).
tff(c_5509,plain,
op1(e12,e13) = e11,
inference(demodulation,[status(thm),theory(equality)],[c_778,c_780]) ).
tff(c_566,plain,
op1(e12,e13) != op1(e11,e13),
inference(cnfTransformation,[status(thm)],[f_992]) ).
tff(c_6329,plain,
op1(e11,e13) != e11,
inference(demodulation,[status(thm),theory(equality)],[c_5509,c_566]) ).
tff(c_6894,plain,
op1(e10,e12) != e11,
inference(demodulation,[status(thm),theory(equality)],[c_6891,c_6329]) ).
tff(c_582,plain,
op1(e12,e12) != op1(e10,e12),
inference(cnfTransformation,[status(thm)],[f_992]) ).
tff(c_6324,plain,
op1(e10,e12) != e13,
inference(demodulation,[status(thm),theory(equality)],[c_778,c_582]) ).
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_7076,plain,
op1(e10,e12) = e12,
inference(negUnitSimplification,[status(thm)],[c_6323,c_6894,c_6324,c_28]) ).
tff(c_148,plain,
op1(op1(e10,e11),e12) = op1(e10,op1(e11,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6885,plain,
op1(op1(e10,e11),e12) = op1(e10,e10),
inference(demodulation,[status(thm),theory(equality)],[c_5121,c_148]) ).
tff(c_76,plain,
op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6932,plain,
op1(e13,e12) = e11,
inference(demodulation,[status(thm),theory(equality)],[c_5509,c_778,c_778,c_76]) ).
tff(c_106,plain,
op1(op1(e11,e12),e13) = op1(e11,op1(e12,e13)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6902,plain,
op1(e11,e11) = op1(e10,e13),
inference(demodulation,[status(thm),theory(equality)],[c_5509,c_5121,c_106]) ).
tff(c_116,plain,
op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6888,plain,
op1(op1(e11,e11),e12) = op1(e11,e10),
inference(demodulation,[status(thm),theory(equality)],[c_5121,c_116]) ).
tff(c_6912,plain,
op1(op1(e10,e13),e12) = op1(e11,e10),
inference(demodulation,[status(thm),theory(equality)],[c_6902,c_6888]) ).
tff(c_132,plain,
op1(op1(e10,e13),e12) = op1(e10,op1(e13,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6920,plain,
op1(e10,op1(e13,e12)) = op1(e11,e10),
inference(demodulation,[status(thm),theory(equality)],[c_6912,c_132]) ).
tff(c_6941,plain,
op1(e11,e10) = op1(e10,e11),
inference(demodulation,[status(thm),theory(equality)],[c_6932,c_6920]) ).
tff(c_130,plain,
op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_114,plain,
op1(op1(e11,e11),e13) = op1(e11,op1(e11,e13)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6901,plain,
op1(op1(e11,e11),e13) = op1(e11,op1(e10,e12)),
inference(demodulation,[status(thm),theory(equality)],[c_6891,c_114]) ).
tff(c_6916,plain,
op1(op1(e10,e13),e13) = op1(e11,op1(e10,e12)),
inference(demodulation,[status(thm),theory(equality)],[c_6902,c_6901]) ).
tff(c_6921,plain,
op1(e11,op1(e10,e12)) = op1(e10,op1(e13,e13)),
inference(demodulation,[status(thm),theory(equality)],[c_130,c_6916]) ).
tff(c_124,plain,
op1(op1(e11,e10),e12) = op1(e11,op1(e10,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6922,plain,
op1(op1(e11,e10),e12) = op1(e10,op1(e13,e13)),
inference(demodulation,[status(thm),theory(equality)],[c_6921,c_124]) ).
tff(c_6959,plain,
op1(op1(e10,e11),e12) = op1(e10,op1(e13,e13)),
inference(demodulation,[status(thm),theory(equality)],[c_6941,c_6922]) ).
tff(c_6971,plain,
op1(e10,op1(e13,e13)) = op1(e10,e10),
inference(demodulation,[status(thm),theory(equality)],[c_6885,c_6959]) ).
tff(c_6973,plain,
op1(e11,op1(e10,e12)) = op1(e10,e10),
inference(demodulation,[status(thm),theory(equality)],[c_6971,c_6921]) ).
tff(c_7089,plain,
op1(e11,e12) = op1(e10,e10),
inference(demodulation,[status(thm),theory(equality)],[c_7076,c_6973]) ).
tff(c_7132,plain,
op1(e10,e10) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_5121,c_7089]) ).
tff(c_786,plain,
op2(e22,op2(e22,e22)) = e21,
inference(cnfTransformation,[status(thm)],[f_1290]) ).
tff(c_5071,plain,
h3(e11) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_3768,c_806,c_786]) ).
tff(c_138,plain,
op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6887,plain,
op1(op1(e10,e12),e13) = op1(e10,e11),
inference(demodulation,[status(thm),theory(equality)],[c_5509,c_138]) ).
tff(c_7084,plain,
op1(e12,e13) = op1(e10,e11),
inference(demodulation,[status(thm),theory(equality)],[c_7076,c_6887]) ).
tff(c_7119,plain,
op1(e10,e11) = e11,
inference(demodulation,[status(thm),theory(equality)],[c_5509,c_7084]) ).
tff(c_812,plain,
h3(e12) = e22,
inference(cnfTransformation,[status(thm)],[f_1311]) ).
tff(c_784,plain,
op2(e22,e22) = e23,
inference(cnfTransformation,[status(thm)],[f_1290]) ).
tff(c_5110,plain,
h3(e13) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_784,c_806]) ).
tff(c_140,plain,
op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6886,plain,
op1(op1(e10,e12),e12) = op1(e10,e13),
inference(demodulation,[status(thm),theory(equality)],[c_778,c_140]) ).
tff(c_7083,plain,
op1(e12,e12) = op1(e10,e13),
inference(demodulation,[status(thm),theory(equality)],[c_7076,c_6886]) ).
tff(c_7103,plain,
op1(e10,e13) = e13,
inference(demodulation,[status(thm),theory(equality)],[c_778,c_7083]) ).
tff(c_68,plain,
op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6990,plain,
op1(e12,e11) = e10,
inference(demodulation,[status(thm),theory(equality)],[c_6932,c_5121,c_5509,c_68]) ).
tff(c_82,plain,
op1(op1(e12,e11),e13) = op1(e12,op1(e11,e13)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6929,plain,
op1(op1(e12,e11),e13) = op1(e12,op1(e10,e12)),
inference(demodulation,[status(thm),theory(equality)],[c_6891,c_82]) ).
tff(c_7000,plain,
op1(e12,op1(e10,e12)) = op1(e10,e13),
inference(demodulation,[status(thm),theory(equality)],[c_6990,c_6929]) ).
tff(c_84,plain,
op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6928,plain,
op1(op1(e12,e11),e12) = op1(e12,e10),
inference(demodulation,[status(thm),theory(equality)],[c_5121,c_84]) ).
tff(c_6999,plain,
op1(e12,e10) = op1(e10,e12),
inference(demodulation,[status(thm),theory(equality)],[c_6990,c_6928]) ).
tff(c_80,plain,
op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6930,plain,
op1(e12,op1(e12,e10)) = op1(e13,e10),
inference(demodulation,[status(thm),theory(equality)],[c_778,c_80]) ).
tff(c_7021,plain,
op1(e12,op1(e10,e12)) = op1(e13,e10),
inference(demodulation,[status(thm),theory(equality)],[c_6999,c_6930]) ).
tff(c_7042,plain,
op1(e13,e10) = op1(e10,e13),
inference(demodulation,[status(thm),theory(equality)],[c_7000,c_7021]) ).
tff(c_78,plain,
op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6931,plain,
op1(e12,op1(e12,e11)) = op1(e13,e11),
inference(demodulation,[status(thm),theory(equality)],[c_778,c_78]) ).
tff(c_7001,plain,
op1(e13,e11) = op1(e12,e10),
inference(demodulation,[status(thm),theory(equality)],[c_6990,c_6931]) ).
tff(c_7024,plain,
op1(e13,e11) = op1(e10,e12),
inference(demodulation,[status(thm),theory(equality)],[c_6999,c_7001]) ).
tff(c_74,plain,
op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13)),
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_6974,plain,
op1(e13,e13) = op1(e12,e11),
inference(demodulation,[status(thm),theory(equality)],[c_5509,c_778,c_74]) ).
tff(c_4926,plain,
op2(h3(e11),e22) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_4925,c_3703]) ).
tff(c_5074,plain,
op2(e21,e22) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_5071,c_4926]) ).
tff(c_680,plain,
op2(e21,e22) != op2(e20,e22),
inference(cnfTransformation,[status(thm)],[f_1135]) ).
tff(c_6297,plain,
op2(e20,e22) != e20,
inference(demodulation,[status(thm),theory(equality)],[c_5074,c_680]) ).
tff(c_310,plain,
op2(op2(e21,e22),e22) = op2(e21,op2(e22,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6400,plain,
op2(e21,e23) = op2(e20,e22),
inference(demodulation,[status(thm),theory(equality)],[c_784,c_5074,c_310]) ).
tff(c_5073,plain,
op2(e22,h3(e13)) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_5071,c_3768]) ).
tff(c_5111,plain,
op2(e22,e23) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_5110,c_5073]) ).
tff(c_662,plain,
op2(e22,e23) != op2(e21,e23),
inference(cnfTransformation,[status(thm)],[f_1135]) ).
tff(c_6304,plain,
op2(e21,e23) != e21,
inference(demodulation,[status(thm),theory(equality)],[c_5111,c_662]) ).
tff(c_6401,plain,
op2(e20,e22) != e21,
inference(demodulation,[status(thm),theory(equality)],[c_6400,c_6304]) ).
tff(c_678,plain,
op2(e22,e22) != op2(e20,e22),
inference(cnfTransformation,[status(thm)],[f_1135]) ).
tff(c_6298,plain,
op2(e20,e22) != e23,
inference(demodulation,[status(thm),theory(equality)],[c_784,c_678]) ).
tff(c_230,plain,
( ( op2(e20,e22) = e23 )
| ( op2(e20,e22) = e22 )
| ( op2(e20,e22) = e21 )
| ( op2(e20,e22) = e20 ) ),
inference(cnfTransformation,[status(thm)],[f_476]) ).
tff(c_6670,plain,
op2(e20,e22) = e22,
inference(negUnitSimplification,[status(thm)],[c_6297,c_6401,c_6298,c_230]) ).
tff(c_790,plain,
op2(e20,e20) = h1(e13),
inference(cnfTransformation,[status(thm)],[f_1297]) ).
tff(c_350,plain,
op2(op2(e20,e21),e22) = op2(e20,op2(e21,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6371,plain,
op2(op2(e20,e21),e22) = h1(e13),
inference(demodulation,[status(thm),theory(equality)],[c_790,c_5074,c_350]) ).
tff(c_278,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6441,plain,
op2(e23,e22) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_5111,c_784,c_784,c_278]) ).
tff(c_798,plain,
op2(e21,e21) = h2(e13),
inference(cnfTransformation,[status(thm)],[f_1304]) ).
tff(c_318,plain,
op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6396,plain,
op2(h2(e13),e22) = op2(e21,e20),
inference(demodulation,[status(thm),theory(equality)],[c_798,c_5074,c_318]) ).
tff(c_308,plain,
op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6410,plain,
op2(e20,e23) = h2(e13),
inference(demodulation,[status(thm),theory(equality)],[c_798,c_5111,c_5074,c_308]) ).
tff(c_334,plain,
op2(op2(e20,e23),e22) = op2(e20,op2(e23,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6420,plain,
op2(h2(e13),e22) = op2(e20,op2(e23,e22)),
inference(demodulation,[status(thm),theory(equality)],[c_6410,c_334]) ).
tff(c_6426,plain,
op2(e20,op2(e23,e22)) = op2(e21,e20),
inference(demodulation,[status(thm),theory(equality)],[c_6396,c_6420]) ).
tff(c_6449,plain,
op2(e21,e20) = op2(e20,e21),
inference(demodulation,[status(thm),theory(equality)],[c_6441,c_6426]) ).
tff(c_814,plain,
op2(e23,e23) = h4(e13),
inference(cnfTransformation,[status(thm)],[f_1318]) ).
tff(c_332,plain,
op2(op2(e20,e23),e23) = op2(e20,op2(e23,e23)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6374,plain,
op2(op2(e20,e23),e23) = op2(e20,h4(e13)),
inference(demodulation,[status(thm),theory(equality)],[c_814,c_332]) ).
tff(c_6421,plain,
op2(h2(e13),e23) = op2(e20,h4(e13)),
inference(demodulation,[status(thm),theory(equality)],[c_6410,c_6374]) ).
tff(c_316,plain,
op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6397,plain,
op2(h2(e13),e23) = op2(e21,op2(e21,e23)),
inference(demodulation,[status(thm),theory(equality)],[c_798,c_316]) ).
tff(c_6409,plain,
op2(h2(e13),e23) = op2(e21,op2(e20,e22)),
inference(demodulation,[status(thm),theory(equality)],[c_6400,c_6397]) ).
tff(c_6427,plain,
op2(e21,op2(e20,e22)) = op2(e20,h4(e13)),
inference(demodulation,[status(thm),theory(equality)],[c_6421,c_6409]) ).
tff(c_326,plain,
op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6429,plain,
op2(op2(e21,e20),e22) = op2(e20,h4(e13)),
inference(demodulation,[status(thm),theory(equality)],[c_6427,c_326]) ).
tff(c_6464,plain,
op2(op2(e20,e21),e22) = op2(e20,h4(e13)),
inference(demodulation,[status(thm),theory(equality)],[c_6449,c_6429]) ).
tff(c_6472,plain,
op2(e20,h4(e13)) = h1(e13),
inference(demodulation,[status(thm),theory(equality)],[c_6371,c_6464]) ).
tff(c_6474,plain,
op2(e21,op2(e20,e22)) = h1(e13),
inference(demodulation,[status(thm),theory(equality)],[c_6472,c_6427]) ).
tff(c_6681,plain,
op2(e21,e22) = h1(e13),
inference(demodulation,[status(thm),theory(equality)],[c_6670,c_6474]) ).
tff(c_6743,plain,
h1(e13) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_5074,c_6681]) ).
tff(c_340,plain,
op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6373,plain,
op2(op2(e20,e22),e23) = op2(e20,e21),
inference(demodulation,[status(thm),theory(equality)],[c_5111,c_340]) ).
tff(c_6675,plain,
op2(e22,e23) = op2(e20,e21),
inference(demodulation,[status(thm),theory(equality)],[c_6670,c_6373]) ).
tff(c_6690,plain,
op2(e20,e21) = e21,
inference(demodulation,[status(thm),theory(equality)],[c_5111,c_6675]) ).
tff(c_342,plain,
op2(op2(e20,e22),e22) = op2(e20,op2(e22,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6372,plain,
op2(op2(e20,e22),e22) = op2(e20,e23),
inference(demodulation,[status(thm),theory(equality)],[c_784,c_342]) ).
tff(c_6417,plain,
op2(op2(e20,e22),e22) = h2(e13),
inference(demodulation,[status(thm),theory(equality)],[c_6410,c_6372]) ).
tff(c_6679,plain,
op2(e22,e22) = h2(e13),
inference(demodulation,[status(thm),theory(equality)],[c_6670,c_6417]) ).
tff(c_6708,plain,
h2(e13) = e23,
inference(demodulation,[status(thm),theory(equality)],[c_784,c_6679]) ).
tff(c_276,plain,
op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6476,plain,
op2(e22,e21) = h4(e13),
inference(demodulation,[status(thm),theory(equality)],[c_814,c_784,c_5111,c_276]) ).
tff(c_270,plain,
op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6515,plain,
h4(e13) = e20,
inference(demodulation,[status(thm),theory(equality)],[c_6476,c_6441,c_5074,c_5111,c_270]) ).
tff(c_286,plain,
op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6437,plain,
op2(op2(e22,e21),e22) = op2(e22,e20),
inference(demodulation,[status(thm),theory(equality)],[c_5074,c_286]) ).
tff(c_6488,plain,
op2(h4(e13),e22) = op2(e22,e20),
inference(demodulation,[status(thm),theory(equality)],[c_6476,c_6437]) ).
tff(c_6531,plain,
op2(e22,e20) = op2(e20,e22),
inference(demodulation,[status(thm),theory(equality)],[c_6515,c_6488]) ).
tff(c_280,plain,
op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6440,plain,
op2(e22,op2(e22,e21)) = op2(e23,e21),
inference(demodulation,[status(thm),theory(equality)],[c_784,c_280]) ).
tff(c_6487,plain,
op2(e22,h4(e13)) = op2(e23,e21),
inference(demodulation,[status(thm),theory(equality)],[c_6476,c_6440]) ).
tff(c_6530,plain,
op2(e23,e21) = op2(e22,e20),
inference(demodulation,[status(thm),theory(equality)],[c_6515,c_6487]) ).
tff(c_6590,plain,
op2(e23,e21) = op2(e20,e22),
inference(demodulation,[status(thm),theory(equality)],[c_6531,c_6530]) ).
tff(c_284,plain,
op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6438,plain,
op2(op2(e22,e21),e23) = op2(e22,op2(e20,e22)),
inference(demodulation,[status(thm),theory(equality)],[c_6400,c_284]) ).
tff(c_6486,plain,
op2(h4(e13),e23) = op2(e22,op2(e20,e22)),
inference(demodulation,[status(thm),theory(equality)],[c_6476,c_6438]) ).
tff(c_6529,plain,
op2(e22,op2(e20,e22)) = op2(e20,e23),
inference(demodulation,[status(thm),theory(equality)],[c_6515,c_6486]) ).
tff(c_6571,plain,
op2(e22,op2(e20,e22)) = h2(e13),
inference(demodulation,[status(thm),theory(equality)],[c_6410,c_6529]) ).
tff(c_816,plain,
op2(e23,op2(e23,e23)) = h4(e11),
inference(cnfTransformation,[status(thm)],[f_1318]) ).
tff(c_3254,plain,
op2(e23,h4(e13)) = h4(e11),
inference(demodulation,[status(thm),theory(equality)],[c_814,c_816]) ).
tff(c_6519,plain,
op2(e23,e20) = h4(e11),
inference(demodulation,[status(thm),theory(equality)],[c_6515,c_3254]) ).
tff(c_282,plain,
op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20)),
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_6439,plain,
op2(e22,op2(e22,e20)) = op2(e23,e20),
inference(demodulation,[status(thm),theory(equality)],[c_784,c_282]) ).
tff(c_6564,plain,
op2(e22,op2(e22,e20)) = h4(e11),
inference(demodulation,[status(thm),theory(equality)],[c_6519,c_6439]) ).
tff(c_6613,plain,
h4(e11) = h2(e13),
inference(demodulation,[status(thm),theory(equality)],[c_6571,c_6531,c_6564]) ).
tff(c_1388,plain,
( ( h3(e10) != e20 )
| ( h3(e11) != e21 )
| ( h3(e12) != e22 )
| ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),h3(e12)) != h3(op1(e13,e12)) )
| ( op2(h3(e13),h3(e11)) != h3(op1(e13,e11)) )
| ( op2(h3(e13),h3(e10)) != h3(op1(e13,e10)) )
| ( op2(h3(e12),h3(e13)) != h3(op1(e12,e13)) )
| ( op2(h3(e12),h3(e12)) != h3(op1(e12,e12)) )
| ( op2(h3(e12),h3(e11)) != h3(op1(e12,e11)) )
| ( op2(h3(e12),h3(e10)) != h3(op1(e12,e10)) )
| ( op2(h3(e11),h3(e13)) != h3(op1(e11,e13)) )
| ( op2(h3(e11),h3(e12)) != h3(op1(e11,e12)) )
| ( op2(h3(e11),h3(e11)) != h3(op1(e11,e11)) )
| ( op2(h3(e11),h3(e10)) != h3(op1(e11,e10)) )
| ( op2(h3(e10),h3(e13)) != h3(op1(e10,e13)) )
| ( op2(h3(e10),h3(e12)) != h3(op1(e10,e12)) )
| ( op2(h3(e10),h3(e11)) != h3(op1(e10,e11)) )
| ( op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ) ),
inference(cnfTransformation,[status(thm)],[f_1574]) ).
tff(c_3575,plain,
( ( h3(e10) != e20 )
| ( h3(e11) != e21 )
| ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),e22) != h3(op1(e13,e12)) )
| ( op2(h3(e13),h3(e11)) != h3(op1(e13,e11)) )
| ( op2(h3(e13),h3(e10)) != h3(op1(e13,e10)) )
| ( op2(e22,h3(e13)) != h3(op1(e12,e13)) )
| ( h3(op1(e12,e12)) != op2(e22,e22) )
| ( op2(e22,h3(e11)) != h3(op1(e12,e11)) )
| ( op2(e22,h3(e10)) != h3(op1(e12,e10)) )
| ( op2(h3(e11),h3(e13)) != h3(op1(e11,e13)) )
| ( op2(h3(e11),e22) != h3(op1(e11,e12)) )
| ( op2(h3(e11),h3(e11)) != h3(op1(e11,e11)) )
| ( op2(h3(e11),h3(e10)) != h3(op1(e11,e10)) )
| ( op2(h3(e10),h3(e13)) != h3(op1(e10,e13)) )
| ( op2(h3(e10),e22) != h3(op1(e10,e12)) )
| ( op2(h3(e10),h3(e11)) != h3(op1(e10,e11)) )
| ( op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_812,c_812,c_812,c_812,c_812,c_812,c_812,c_812,c_812,c_1388]) ).
tff(c_3755,plain,
( ( h3(e10) != e20 )
| ( h3(e11) != e21 )
| ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),e22) != h3(op1(e13,e12)) )
| ( op2(h3(e13),h3(e11)) != h3(op1(e13,e11)) )
| ( op2(h3(e13),h3(e10)) != h3(op1(e13,e10)) )
| ( op2(e22,h3(e13)) != h3(op1(e12,e13)) )
| ( h3(op1(e12,e12)) != op2(e22,e22) )
| ( op2(e22,h3(e11)) != h3(op1(e12,e11)) )
| ( op2(e22,h3(e10)) != h3(op1(e12,e10)) )
| ( op2(h3(e11),h3(e13)) != h3(op1(e11,e13)) )
| ( h3(op1(e11,e12)) != h3(e10) )
| ( op2(h3(e11),h3(e11)) != h3(op1(e11,e11)) )
| ( op2(h3(e11),h3(e10)) != h3(op1(e11,e10)) )
| ( op2(h3(e10),h3(e13)) != h3(op1(e10,e13)) )
| ( op2(h3(e10),e22) != h3(op1(e10,e12)) )
| ( op2(h3(e10),h3(e11)) != h3(op1(e10,e11)) )
| ( op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3703,c_3575]) ).
tff(c_3827,plain,
( ( h3(e10) != e20 )
| ( h3(e11) != e21 )
| ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),e22) != h3(op1(e13,e12)) )
| ( op2(h3(e13),h3(e11)) != h3(op1(e13,e11)) )
| ( op2(h3(e13),h3(e10)) != h3(op1(e13,e10)) )
| ( op2(e22,h3(e13)) != h3(op1(e12,e13)) )
| ( h3(op1(e12,e12)) != h3(e13) )
| ( op2(e22,h3(e11)) != h3(op1(e12,e11)) )
| ( op2(e22,h3(e10)) != h3(op1(e12,e10)) )
| ( op2(h3(e11),h3(e13)) != h3(op1(e11,e13)) )
| ( h3(op1(e11,e12)) != h3(e10) )
| ( op2(h3(e11),h3(e11)) != h3(op1(e11,e11)) )
| ( op2(h3(e11),h3(e10)) != h3(op1(e11,e10)) )
| ( op2(h3(e10),h3(e13)) != h3(op1(e10,e13)) )
| ( op2(h3(e10),e22) != h3(op1(e10,e12)) )
| ( op2(h3(e10),h3(e11)) != h3(op1(e10,e11)) )
| ( op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_806,c_3755]) ).
tff(c_3891,plain,
( ( h3(e10) != e20 )
| ( h3(e11) != e21 )
| ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),e22) != h3(op1(e13,e12)) )
| ( op2(h3(e13),h3(e11)) != h3(op1(e13,e11)) )
| ( op2(h3(e13),h3(e10)) != h3(op1(e13,e10)) )
| ( h3(op1(e12,e13)) != h3(e11) )
| ( h3(op1(e12,e12)) != h3(e13) )
| ( op2(e22,h3(e11)) != h3(op1(e12,e11)) )
| ( op2(e22,h3(e10)) != h3(op1(e12,e10)) )
| ( op2(h3(e11),h3(e13)) != h3(op1(e11,e13)) )
| ( h3(op1(e11,e12)) != h3(e10) )
| ( op2(h3(e11),h3(e11)) != h3(op1(e11,e11)) )
| ( op2(h3(e11),h3(e10)) != h3(op1(e11,e10)) )
| ( op2(h3(e10),h3(e13)) != h3(op1(e10,e13)) )
| ( op2(h3(e10),e22) != h3(op1(e10,e12)) )
| ( op2(h3(e10),h3(e11)) != h3(op1(e10,e11)) )
| ( op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3768,c_3827]) ).
tff(c_4989,plain,
( ( h3(e11) != e21 )
| ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),e22) != h3(op1(e13,e12)) )
| ( op2(h3(e13),h3(e11)) != h3(op1(e13,e11)) )
| ( op2(h3(e13),e20) != h3(op1(e13,e10)) )
| ( h3(op1(e12,e13)) != h3(e11) )
| ( h3(op1(e12,e12)) != h3(e13) )
| ( op2(e22,h3(e11)) != h3(op1(e12,e11)) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( op2(h3(e11),h3(e13)) != h3(op1(e11,e13)) )
| ( h3(op1(e11,e12)) != e20 )
| ( op2(h3(e11),h3(e11)) != h3(op1(e11,e11)) )
| ( op2(h3(e11),e20) != h3(op1(e11,e10)) )
| ( op2(e20,h3(e13)) != h3(op1(e10,e13)) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( op2(e20,h3(e11)) != h3(op1(e10,e11)) )
| ( h3(op1(e10,e10)) != op2(e20,e20) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4925,c_4925,c_4925,c_4925,c_4925,c_4925,c_4925,c_4925,c_4925,c_4925,c_3891]) ).
tff(c_5057,plain,
( ( h3(e11) != e21 )
| ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),e22) != h3(op1(e13,e12)) )
| ( op2(h3(e13),h3(e11)) != h3(op1(e13,e11)) )
| ( op2(h3(e13),e20) != h3(op1(e13,e10)) )
| ( h3(op1(e12,e13)) != h3(e11) )
| ( h3(op1(e12,e12)) != h3(e13) )
| ( op2(e22,h3(e11)) != h3(op1(e12,e11)) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( op2(h3(e11),h3(e13)) != h3(op1(e11,e13)) )
| ( h3(op1(e11,e12)) != e20 )
| ( op2(h3(e11),h3(e11)) != h3(op1(e11,e11)) )
| ( op2(h3(e11),e20) != h3(op1(e11,e10)) )
| ( op2(e20,h3(e13)) != h3(op1(e10,e13)) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( op2(e20,h3(e11)) != h3(op1(e10,e11)) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_790,c_4989]) ).
tff(c_5087,plain,
( ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),e22) != h3(op1(e13,e12)) )
| ( op2(h3(e13),e21) != h3(op1(e13,e11)) )
| ( op2(h3(e13),e20) != h3(op1(e13,e10)) )
| ( h3(op1(e12,e13)) != e21 )
| ( h3(op1(e12,e12)) != h3(e13) )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( op2(e21,h3(e13)) != h3(op1(e11,e13)) )
| ( h3(op1(e11,e12)) != e20 )
| ( h3(op1(e11,e11)) != op2(e21,e21) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( op2(e20,h3(e13)) != h3(op1(e10,e13)) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5071,c_5071,c_5071,c_5071,c_5071,c_5071,c_5071,c_5071,c_5071,c_5057]) ).
tff(c_5105,plain,
( ( h3(e13) != e23 )
| ( op2(h3(e13),h3(e13)) != h3(op1(e13,e13)) )
| ( op2(h3(e13),e22) != h3(op1(e13,e12)) )
| ( op2(h3(e13),e21) != h3(op1(e13,e11)) )
| ( op2(h3(e13),e20) != h3(op1(e13,e10)) )
| ( h3(op1(e12,e13)) != e21 )
| ( h3(op1(e12,e12)) != h3(e13) )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( op2(e21,h3(e13)) != h3(op1(e11,e13)) )
| ( h3(op1(e11,e12)) != e20 )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( op2(e20,h3(e13)) != h3(op1(e10,e13)) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_798,c_5087]) ).
tff(c_5116,plain,
( ( h3(op1(e13,e13)) != op2(e23,e23) )
| ( h3(op1(e13,e12)) != op2(e23,e22) )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e13)) != e21 )
| ( h3(op1(e12,e12)) != e23 )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e21,e23) )
| ( h3(op1(e11,e12)) != e20 )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != op2(e20,e23) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5110,c_5110,c_5110,c_5110,c_5110,c_5110,c_5110,c_5110,c_5110,c_5105]) ).
tff(c_5120,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != op2(e23,e22) )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e13)) != e21 )
| ( h3(op1(e12,e12)) != e23 )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e21,e23) )
| ( h3(op1(e11,e12)) != e20 )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != op2(e20,e23) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_814,c_5116]) ).
tff(c_5290,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != op2(e23,e22) )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e13)) != e21 )
| ( h3(op1(e12,e12)) != e23 )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e21,e23) )
| ( h3(e10) != e20 )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != op2(e20,e23) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5121,c_5120]) ).
tff(c_5508,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != op2(e23,e22) )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e13)) != e21 )
| ( h3(op1(e12,e12)) != e23 )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e21,e23) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != op2(e20,e23) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4925,c_5290]) ).
tff(c_5518,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != op2(e23,e22) )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e13)) != e21 )
| ( h3(e13) != e23 )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e21,e23) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != op2(e20,e23) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_778,c_5508]) ).
tff(c_5904,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != op2(e23,e22) )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e21,e23) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != op2(e20,e23) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5110,c_5071,c_5509,c_5518]) ).
tff(c_6406,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != op2(e23,e22) )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != op2(e20,e23) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6400,c_5904]) ).
tff(c_6423,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != op2(e23,e22) )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6410,c_6406]) ).
tff(c_6450,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e21,e20) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6441,c_6423]) ).
tff(c_6466,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e11)) != op2(e22,e21) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e20,e21) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6449,c_6450]) ).
tff(c_6490,plain,
( ( h3(op1(e13,e13)) != h4(e13) )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e11)) != h4(e13) )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e20,e21) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6476,c_6466]) ).
tff(c_6533,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != op2(e23,e20) )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != op2(e22,e20) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e20,e21) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6515,c_6515,c_6490]) ).
tff(c_6591,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != h4(e11) )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != op2(e20,e22) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e20,e21) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6531,c_6519,c_6533]) ).
tff(c_6618,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != op2(e23,e21) )
| ( h3(op1(e13,e10)) != h2(e13) )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != op2(e20,e22) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e20,e21) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_6591]) ).
tff(c_6643,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != op2(e20,e22) )
| ( h3(op1(e13,e10)) != h2(e13) )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != op2(e20,e22) )
| ( h3(op1(e11,e13)) != op2(e20,e22) )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e20,e21) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != op2(e20,e22) )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6590,c_6618]) ).
tff(c_6687,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != h2(e13) )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e11,e13)) != e22 )
| ( h3(op1(e11,e11)) != h2(e13) )
| ( h3(op1(e11,e10)) != op2(e20,e21) )
| ( h3(op1(e10,e13)) != h2(e13) )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != op2(e20,e21) )
| ( h3(op1(e10,e10)) != h1(e13) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6670,c_6670,c_6670,c_6670,c_6643]) ).
tff(c_6770,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != e23 )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e11,e13)) != e22 )
| ( h3(op1(e11,e11)) != e23 )
| ( h3(op1(e11,e10)) != e21 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6743,c_6690,c_6708,c_6690,c_6708,c_6708,c_6687]) ).
tff(c_6898,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != e23 )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e11,e11)) != e23 )
| ( h3(op1(e11,e10)) != e21 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6891,c_6770]) ).
tff(c_6914,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e12)) != e21 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != e23 )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e11,e10)) != e21 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6902,c_6898]) ).
tff(c_6939,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(e11) != e21 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != e23 )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e11,e10)) != e21 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6932,c_6914]) ).
tff(c_6944,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != e23 )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e11,e10)) != e21 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5071,c_6939]) ).
tff(c_6961,plain,
( ( h3(op1(e13,e13)) != e20 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != e23 )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6941,c_6944]) ).
tff(c_6983,plain,
( ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != e23 )
| ( h3(op1(e12,e11)) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6974,c_6961]) ).
tff(c_7007,plain,
( ( h3(e10) != e20 )
| ( h3(op1(e13,e11)) != e22 )
| ( h3(op1(e13,e10)) != e23 )
| ( h3(e10) != e20 )
| ( h3(op1(e12,e10)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6990,c_6990,c_6983]) ).
tff(c_7034,plain,
( ( h3(op1(e13,e10)) != e23 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6999,c_4925,c_7024,c_4925,c_7007]) ).
tff(c_7049,plain,
( ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e12)) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7042,c_7034]) ).
tff(c_7097,plain,
( ( h3(op1(e10,e13)) != e23 )
| ( h3(op1(e10,e13)) != e23 )
| ( h3(e12) != e22 )
| ( h3(op1(e10,e11)) != e21 )
| ( h3(op1(e10,e10)) != e20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_7076,c_7049]) ).
tff(c_7143,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4925,c_7132,c_5071,c_7119,c_812,c_5110,c_7103,c_5110,c_7103,c_7097]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : ALG016+1 : TPTP v9.0.0. Released v2.7.0.
% 0.08/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.15/0.36 % Computer : n022.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Sun Apr 6 06:53:35 EDT 2025
% 0.15/0.36 % CPUTime :
% 27.69/11.09 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.84/11.13
% 27.84/11.13 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------