Vampire---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : ARI711_1 : TPTP v9.3.1. Released v6.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n013.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 09:33:42 AM UTC 2026

% Result   : Theorem 10.64s 2.61s
% Output   : Refutation 0.27s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   67
%            Number of leaves      :    8
% Syntax   : Number of formulae    :   82 (  80 unt;   0 typ;   2 def)
%            Number of atoms       :   84 (  79 equ)
%            Maximal formula atoms :    2 (   1 avg)
%            Number of connectives :   68 (  66   ~;   0   |;   0   &)
%                                         (   2 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    4 (   2 avg)
%            Maximal term depth    :   40 (   4 avg)
%            Number of FOOLs       :    2 (   2 fml;   0 var)
%            Number arithmetic     : 11785 (   0 atm;9533 fun;2242 num;  10 var)
%            Number of types       :    1 (   0 usr;   1 ari;   0 dat;   0 cdt)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :    4 (   2 usr;   3 prp; 0-2 aty)
%            Number of functors    :   15 (   3 usr;  11 con; 0-2 aty)
%            Number of variables   :   10 (  10   !;   0   ?;  10   :)

% Comments : 
%------------------------------------------------------------------------------
tff(func_def_0,type,
    a: $int ).

tff(func_def_1,type,
    b: $int ).

tff(func_def_2,type,
    c: $int ).

tff(f1,axiom,
    $product($product($product($sum($sum($sum(a,b),c),1),$sum($sum($sum(a,b),c),1)),$sum($sum($sum(a,b),c),1)),$sum($sum($sum(a,b),c),1)) = 0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq) ).

tff(f2,conjecture,
    $sum($product($product($product(c,c),c),c),$product(-1,$sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($difference($sum($sum($sum($sum($sum($sum($sum($sum($sum($difference($sum($sum($sum($difference($product(-1,1),$product(4,a)),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$product(-1,$product($product($product(a,a),a),a))),$product(4,b)),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$product(-1,$product($product($product(b,b),b),b))),$product(4,c)),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$product(-12,$product($product($product(c,c),b),a))),$product(-6,$product($product($product(c,c),b),b))),$product(-4,$product($product($product(c,c),c),a))),$product(-4,$product($product($product(c,c),c),b))))) = 0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj) ).

tff(f3,negated_conjecture,
    ( ( ~ $sum($product($product($product(c,c),c),c),$product(-1,$sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($difference($sum($sum($sum($sum($sum($sum($sum($sum($sum($difference($sum($sum($sum($difference($product(-1,1),$product(4,a)),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$product(-1,$product($product($product(a,a),a),a))),$product(4,b)),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$product(-1,$product($product($product(b,b),b),b))),$product(4,c)),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$product(-12,$product($product($product(c,c),b),a))),$product(-6,$product($product($product(c,c),b),b))),$product(-4,$product($product($product(c,c),c),a))),$product(-4,$product($product($product(c,c),c),b))))) ) = 0 ),
    inference(negated_conjecture,[status(cth)],[f2]) ).

tff(f4,plain,
    ( ( ~ 0 ) = $sum($product($product($product(c,c),c),c),$product(-1,$sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($product(-1,1),$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$product(-1,$product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$product(-1,$product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$product(-12,$product($product($product(c,c),b),a))),$product(-6,$product($product($product(c,c),b),b))),$product(-4,$product($product($product(c,c),c),a))),$product(-4,$product($product($product(c,c),c),b))))) ),
    inference(theory_normalization,[],[f3]) ).

tff(f5,plain,
    ! [X0: $int,X1: $int] : ( $sum(X1,X0) = $sum(X0,X1) ),
    introduced(definition,[],[tha_commutativity]) ).

tff(f6,plain,
    ! [X2: $int,X0: $int,X1: $int] : ( $sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2) ),
    introduced(definition,[],[tha_associativity]) ).

tff(f16,plain,
    ! [X0: $int,X1: $int] : ( $product(X1,X0) = $product(X0,X1) ),
    introduced(definition,[],[tha_commutativity]) ).

tff(f20,plain,
    ! [X2: $int,X0: $int,X1: $int] : ( $product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2)) ),
    introduced(definition,[],[tha_distributivity]) ).

tff(f23,plain,
    0 != $sum($product($product($product(c,c),c),c),$product(-1,$sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($product(-1,1),$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$product(-1,$product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$product(-1,$product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$product(-12,$product($product($product(c,c),b),a))),$product(-6,$product($product($product(c,c),b),b))),$product(-4,$product($product($product(c,c),c),a))),$product(-4,$product($product($product(c,c),c),b))))),
    inference(flattening,[],[f4]) ).

tff(f24,plain,
    0 != $sum($product($product($product(c,c),c),c),$product(-1,$sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($product(-1,1),$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$product(-1,$product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$product(-1,$product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$product(-12,$product($product($product(c,c),b),a))),$product(-6,$product($product($product(c,c),b),b))),$product(-4,$product($product($product(c,c),c),a))),$product(-4,$product($product($product(c,c),c),b))))),
    inference(cnf_transformation,[],[f23]) ).

tff(f25,plain,
    $product($product($product($sum($sum($sum(a,b),c),1),$sum($sum($sum(a,b),c),1)),$sum($sum($sum(a,b),c),1)),$sum($sum($sum(a,b),c),1)) = 0,
    inference(cnf_transformation,[],[f1]) ).

tff(f26,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$product(-12,$product($product($product(c,c),b),a))),$product(-6,$product($product($product(c,c),b),b))),$product(-4,$product($product($product(c,c),c),a))),$product(-4,$product($product($product(c,c),c),b))))),
    inference(evaluation,[],[f24]) ).

tff(f27,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$product(-12,$product($product($product(c,c),b),a))),$product(-6,$product($product($product(c,c),b),b))),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))),
    inference(forward_demodulation,[],[f26,f6]) ).

tff(f28,plain,
    0 = $product($sum($sum($sum(a,b),c),1),$product($product($sum($sum($sum(a,b),c),1),$sum($sum($sum(a,b),c),1)),$sum($sum($sum(a,b),c),1))),
    inference(forward_demodulation,[],[f25,f16]) ).

tff(f29,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$product(-12,$product($product($product(c,c),b),a))),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))),
    inference(forward_demodulation,[],[f27,f6]) ).

tff(f30,plain,
    0 = $product($sum($sum($sum(a,b),c),1),$product($sum($sum($sum(a,b),c),1),$product($sum($sum($sum(a,b),c),1),$sum($sum($sum(a,b),c),1)))),
    inference(forward_demodulation,[],[f28,f16]) ).

tff(f31,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$product(-6,$product($product($product(c,c),a),a))),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))),
    inference(forward_demodulation,[],[f29,f6]) ).

tff(f32,plain,
    0 = $product($sum($sum(a,b),$sum(c,1)),$product($sum($sum(a,b),$sum(c,1)),$product($sum($sum(a,b),$sum(c,1)),$sum($sum(a,b),$sum(c,1))))),
    inference(forward_demodulation,[],[f30,f6]) ).

tff(f33,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$product(-4,$product($product($product(c,b),b),b))),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))),
    inference(forward_demodulation,[],[f31,f6]) ).

tff(f34,plain,
    0 = $product($sum(a,$sum(b,$sum(c,1))),$product($sum(a,$sum(b,$sum(c,1))),$product($sum(a,$sum(b,$sum(c,1))),$sum(a,$sum(b,$sum(c,1)))))),
    inference(forward_demodulation,[],[f32,f6]) ).

tff(f35,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$product(-12,$product($product($product(c,b),b),a))),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))),
    inference(forward_demodulation,[],[f33,f6]) ).

tff(f36,plain,
    0 = $product($sum(a,$sum(b,$sum(1,c))),$product($sum(a,$sum(b,$sum(1,c))),$product($sum(a,$sum(b,$sum(1,c))),$sum(a,$sum(b,$sum(1,c)))))),
    inference(forward_demodulation,[],[f34,f5]) ).

tff(f37,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$product(-12,$product($product($product(c,b),a),a))),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))),
    inference(forward_demodulation,[],[f35,f6]) ).

tff(f39,definition,
    ( spl0_1
  <=> ( 0 = $product($sum(a,$sum(b,$sum(1,c))),$product($sum(a,$sum(b,$sum(1,c))),$product($sum(a,$sum(b,$sum(1,c))),$sum(a,$sum(b,$sum(1,c)))))) ) ),
    introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).

tff(f42,plain,
    spl0_1,
    inference(avatar_split_clause,[],[f36,f39]) ).

tff(f43,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$product(-4,$product($product($product(c,a),a),a))),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))),
    inference(forward_demodulation,[],[f37,f6]) ).

tff(f44,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$product(-4,$product($product(c,c),c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))),
    inference(forward_demodulation,[],[f43,f6]) ).

tff(f45,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$product(-12,$product($product(c,c),b))),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))),
    inference(forward_demodulation,[],[f44,f6]) ).

tff(f46,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$product(-12,$product($product(c,c),a))),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))),
    inference(forward_demodulation,[],[f45,f6]) ).

tff(f47,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$product(-12,$product($product(c,b),b))),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))),
    inference(forward_demodulation,[],[f46,f6]) ).

tff(f48,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$product(-24,$product($product(c,b),a))),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))),
    inference(forward_demodulation,[],[f47,f6]) ).

tff(f49,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$product(-12,$product($product(c,a),a))),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))),
    inference(forward_demodulation,[],[f48,f6]) ).

tff(f50,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$product(-6,$product(c,c))),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))),
    inference(forward_demodulation,[],[f49,f6]) ).

tff(f51,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$product(-12,$product(c,b))),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))),
    inference(forward_demodulation,[],[f50,f6]) ).

tff(f52,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$product(-12,$product(c,a))),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))),
    inference(forward_demodulation,[],[f51,f6]) ).

tff(f53,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$uminus($product(4,c))),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))))),
    inference(forward_demodulation,[],[f52,f6]) ).

tff(f54,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$uminus($product($product($product(b,b),b),b))),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))))),
    inference(forward_demodulation,[],[f53,f6]) ).

tff(f55,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$product(-4,$product($product($product(b,b),b),a))),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))))))),
    inference(forward_demodulation,[],[f54,f6]) ).

tff(f56,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$product(-6,$product($product($product(b,b),a),a))),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f55,f6]) ).

tff(f57,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$product(-4,$product($product($product(b,a),a),a))),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f56,f6]) ).

tff(f58,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$product(-4,$product($product(b,b),b))),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f57,f6]) ).

tff(f59,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$product(-12,$product($product(b,b),a))),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f58,f6]) ).

tff(f60,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$product(-12,$product($product(b,a),a))),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f59,f6]) ).

tff(f61,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$product(-6,$product(b,b))),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f60,f6]) ).

tff(f62,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$product(-12,$product(b,a))),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f61,f6]) ).

tff(f63,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$uminus($product(4,b))),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f62,f6]) ).

tff(f64,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$uminus($product($product($product(a,a),a),a))),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f63,f6]) ).

tff(f65,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$product(-4,$product($product(a,a),a))),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f64,f6]) ).

tff(f66,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum($sum(-1,$uminus($product(4,a))),$product(-6,$product(a,a))),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f65,f6]) ).

tff(f67,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum($sum(-1,$uminus($product(4,a))),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b)))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f66,f6]) ).

tff(f68,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$sum($product(-4,$product($product($product(c,c),c),a)),$product(-4,$product($product($product(c,c),c),b))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f67,f6]) ).

tff(f69,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$product(-4,$sum($product($product($product(c,c),c),a),$product($product($product(c,c),c),b))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f68,f20]) ).

tff(f70,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$product(-4,$product($product($product(c,c),c),$sum(a,b))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f69,f20]) ).

tff(f71,plain,
    0 != $sum($product($product($product(c,c),c),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product($product(c,c),c)),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$product(-4,$product($sum(a,b),$product($product(c,c),c))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f70,f16]) ).

tff(f72,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product($product($product(c,c),b),b)),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f71,f16]) ).

tff(f73,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product($product(c,c),b)),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product($product(c,c),b),a)),$sum($product(-6,$product(b,$product($product(c,c),b))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f72,f16]) ).

tff(f74,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product($product(b,$product(c,c)),a)),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f73,f16]) ).

tff(f75,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product($product($product(c,c),a),a)),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f74,f16]) ).

tff(f76,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product($product(c,c),a)),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product(a,$product($product(c,c),a))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f75,f16]) ).

tff(f77,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product($product($product(c,b),b),b)),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f76,f16]) ).

tff(f78,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product($product(c,b),b)),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product($product(c,b),b),a)),$sum($product(-4,$product(b,$product($product(c,b),b))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f77,f16]) ).

tff(f79,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product($product(b,$product(c,b)),a)),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f78,f16]) ).

tff(f80,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product($product($product(c,b),a),a)),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f79,f16]) ).

tff(f81,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product($product(c,b),a)),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product(a,$product($product(c,b),a))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f80,f16]) ).

tff(f82,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product($product($product(c,a),a),a)),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f81,f16]) ).

tff(f83,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product($product(c,a),a)),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product($product(c,a),a))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f82,f16]) ).

tff(f84,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(c,a)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(c,a))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(c,a)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f83,f16]) ).

tff(f85,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product($product($product(b,b),b),b)),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f84,f16]) ).

tff(f86,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product($product(b,b),b)),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product($product(b,b),b),a)),$sum($uminus($product(b,$product($product(b,b),b))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f85,f16]) ).

tff(f87,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product($product(b,$product(b,b)),a)),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f86,f16]) ).

tff(f88,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product($product($product(b,b),a),a)),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f87,f16]) ).

tff(f89,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product($product(b,b),a)),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product(a,$product($product(b,b),a))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f88,f16]) ).

tff(f90,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product(a,$product(b,b))),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product($product($product(b,a),a),a)),$sum($product(-6,$product(a,$product(a,$product(b,b)))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f89,f16]) ).

tff(f91,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product($product(b,a),a)),$sum($product(-12,$product(a,$product(b,b))),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product(a,$product($product(b,a),a))),$sum($product(-6,$product(a,$product(a,$product(b,b)))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f90,f16]) ).

tff(f92,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(b,a)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product(a,$product(b,a))),$sum($product(-12,$product(a,$product(b,b))),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product(a,$product(a,$product(b,a)))),$sum($product(-6,$product(a,$product(a,$product(b,b)))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f91,f16]) ).

tff(f93,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product($product($product(a,a),a),a)),$sum($uminus($product(4,b)),$sum($product(-12,$product(a,b)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product(a,$product(a,b))),$sum($product(-12,$product(a,$product(b,b))),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product(a,$product(a,$product(a,b)))),$sum($product(-6,$product(a,$product(a,$product(b,b)))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f92,f16]) ).

tff(f94,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product($product(a,a),a)),$sum($uminus($product(a,$product($product(a,a),a))),$sum($uminus($product(4,b)),$sum($product(-12,$product(a,b)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product(a,$product(a,b))),$sum($product(-12,$product(a,$product(b,b))),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product(a,$product(a,$product(a,b)))),$sum($product(-6,$product(a,$product(a,$product(b,b)))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f93,f16]) ).

tff(f95,plain,
    0 != $sum($product($product(c,$product(c,c)),c),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product(a,$product(a,a))),$sum($uminus($product(a,$product(a,$product(a,a)))),$sum($uminus($product(4,b)),$sum($product(-12,$product(a,b)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product(a,$product(a,b))),$sum($product(-12,$product(a,$product(b,b))),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product(a,$product(a,$product(a,b)))),$sum($product(-6,$product(a,$product(a,$product(b,b)))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f94,f16]) ).

tff(f96,plain,
    0 != $sum($product(c,$product(c,$product(c,c))),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product(a,$product(a,a))),$sum($uminus($product(a,$product(a,$product(a,a)))),$sum($uminus($product(4,b)),$sum($product(-12,$product(a,b)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product(a,$product(a,b))),$sum($product(-12,$product(a,$product(b,b))),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product(a,$product(a,$product(a,b)))),$sum($product(-6,$product(a,$product(a,$product(b,b)))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))),
    inference(forward_demodulation,[],[f95,f16]) ).

tff(f98,definition,
    ( spl0_2
  <=> ( 0 = $sum($product(c,$product(c,$product(c,c))),$uminus($sum(-1,$sum($uminus($product(4,a)),$sum($product(-6,$product(a,a)),$sum($product(-4,$product(a,$product(a,a))),$sum($uminus($product(a,$product(a,$product(a,a)))),$sum($uminus($product(4,b)),$sum($product(-12,$product(a,b)),$sum($product(-6,$product(b,b)),$sum($product(-12,$product(a,$product(a,b))),$sum($product(-12,$product(a,$product(b,b))),$sum($product(-4,$product(b,$product(b,b))),$sum($product(-4,$product(a,$product(a,$product(a,b)))),$sum($product(-6,$product(a,$product(a,$product(b,b)))),$sum($product(-4,$product(a,$product(b,$product(b,b)))),$sum($uminus($product(b,$product(b,$product(b,b)))),$sum($uminus($product(4,c)),$sum($product(-12,$product(a,c)),$sum($product(-12,$product(c,b)),$sum($product(-6,$product(c,c)),$sum($product(-12,$product(a,$product(a,c))),$sum($product(-24,$product(a,$product(c,b))),$sum($product(-12,$product(b,$product(c,b))),$sum($product(-12,$product(a,$product(c,c))),$sum($product(-12,$product(b,$product(c,c))),$sum($product(-4,$product(c,$product(c,c))),$sum($product(-4,$product(a,$product(a,$product(a,c)))),$sum($product(-12,$product(a,$product(a,$product(c,b)))),$sum($product(-12,$product(a,$product(b,$product(c,b)))),$sum($product(-4,$product(b,$product(b,$product(c,b)))),$sum($product(-6,$product(a,$product(a,$product(c,c)))),$sum($product(-12,$product(a,$product(b,$product(c,c)))),$sum($product(-6,$product(b,$product(b,$product(c,c)))),$product(-4,$product($sum(a,b),$product(c,$product(c,c)))))))))))))))))))))))))))))))))))))) ) ),
    introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).

tff(f101,plain,
    ~ spl0_2,
    inference(avatar_split_clause,[],[f96,f98]) ).

tff(f102,plain,
    $false,
    inference(avatar_smt_refutation,[],[f101,f42]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ARI711_1 : TPTP v9.3.1. Released v6.3.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24  % Computer : n013.cluster.edu
% 0.10/0.24  % Model    : x86_64 x86_64
% 0.10/0.24  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.24  % Memory   : 8046.5625MB
% 0.10/0.24  % OS       : Linux 6.8.0-71-generic
% 0.10/0.25  % CPULimit : 300
% 0.10/0.25  % WCLimit  : 300
% 0.10/0.25  % DateTime : Mon Sep 28 20:57:36 UTC 2026
% 0.10/0.25  % CPUTime  : 
% 0.10/0.25  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.30  Running first-order theorem proving
% 0.23/0.30  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.71/1.80  % (1572032)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.71/1.80  % (1572039)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1407793918:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.71/1.80  % (1572042)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2930527660:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.71/1.80  % (1572043)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3690022786:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.71/1.80  % (1572040)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3066169374:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.71/1.80  % (1572041)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2269741263:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.71/1.80  % (1572038)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2337211520:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.71/1.80  % (1572037)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1245477488:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.71/1.80  % (1572041)Instruction limit reached! 
% 4.71/1.80  % (1572041)------------------------------
% 4.71/1.80  % (1572041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.80  % (1572041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.80  % (1572041)CaDiCaL version: 2.1.3
% 4.71/1.80  % (1572041)Termination reason: Instruction limit
% 4.71/1.80  % (1572041)Termination phase: Saturation
% 4.71/1.80  % (1572041)Time elapsed: 0.005 s
% 4.71/1.80  % (1572041)Peak memory usage: 88 MB
% 4.71/1.80  % (1572041)Instructions burned: 4 (million)
% 4.71/1.80  % (1572040)Instruction limit reached! 
% 4.71/1.80  % (1572040)------------------------------
% 4.71/1.80  % (1572040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.80  % (1572040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.80  % (1572040)CaDiCaL version: 2.1.3
% 4.71/1.80  % (1572040)Termination reason: Instruction limit
% 4.71/1.80  % (1572040)Termination phase: Saturation
% 4.71/1.80  % (1572040)Time elapsed: 0.009 s
% 4.71/1.80  % (1572040)Peak memory usage: 88 MB
% 4.71/1.80  % (1572040)Instructions burned: 9 (million)
% 4.71/1.80  % (1572042)Instruction limit reached! 
% 4.71/1.80  % (1572042)------------------------------
% 4.71/1.80  % (1572042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.80  % (1572042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.80  % (1572042)CaDiCaL version: 2.1.3
% 4.71/1.80  % (1572042)Termination reason: Instruction limit
% 4.71/1.80  % (1572042)Termination phase: Saturation
% 4.71/1.80  % (1572042)Time elapsed: 0.039 s
% 4.71/1.80  % (1572042)Peak memory usage: 117 MB
% 4.71/1.80  % (1572042)Instructions burned: 46 (million)
% 4.71/1.80  % (1572037)Instruction limit reached! 
% 4.71/1.80  % (1572037)------------------------------
% 4.71/1.80  % (1572037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.80  % (1572037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.80  % (1572037)CaDiCaL version: 2.1.3
% 4.71/1.80  % (1572037)Termination reason: Instruction limit
% 4.71/1.80  % (1572037)Termination phase: Saturation
% 4.71/1.80  % (1572037)Time elapsed: 0.040 s
% 4.71/1.80  % (1572037)Peak memory usage: 114 MB
% 4.71/1.80  % (1572037)Instructions burned: 12 (million)
% 4.71/1.80  % (1572043)Instruction limit reached! 
% 4.71/1.80  % (1572043)------------------------------
% 4.71/1.80  % (1572043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.80  % (1572043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.80  % (1572043)CaDiCaL version: 2.1.3
% 4.71/1.80  % (1572043)Termination reason: Instruction limit
% 4.71/1.80  % (1572043)Termination phase: Saturation
% 4.71/1.80  % (1572043)Time elapsed: 0.062 s
% 4.71/1.80  % (1572043)Peak memory usage: 117 MB
% 4.71/1.80  % (1572043)Instructions burned: 33 (million)
% 4.71/1.80  % (1572039)Instruction limit reached! 
% 4.71/1.80  % (1572039)------------------------------
% 4.71/1.80  % (1572039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.80  % (1572039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.12  % (1572039)CaDiCaL version: 2.1.3
% 8.57/2.12  % (1572039)Termination reason: Instruction limit
% 8.57/2.12  % (1572039)Termination phase: Saturation
% 8.57/2.12  % (1572039)Time elapsed: 0.173 s
% 8.57/2.12  % (1572039)Peak memory usage: 113 MB
% 8.57/2.12  % (1572039)Instructions burned: 201 (million)
% 8.57/2.12  % (1572054)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2055637160:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 8.57/2.12  % (1572051)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1436929248:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 8.57/2.12  % (1572052)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=3354670073:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 8.57/2.12  % (1572051)Refutation not found, incomplete strategy
% 8.57/2.12  % (1572051)------------------------------
% 8.57/2.12  % (1572051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.12  % (1572051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.12  % (1572051)CaDiCaL version: 2.1.3
% 8.57/2.12  % (1572051)Termination reason: Refutation not found, incomplete strategy
% 8.57/2.12  % (1572051)Time elapsed: 0.004 s
% 8.57/2.12  % (1572051)Peak memory usage: 88 MB
% 8.57/2.12  % (1572051)Instructions burned: 3 (million)
% 8.57/2.12  % (1572054)Instruction limit reached! 
% 8.57/2.12  % (1572054)------------------------------
% 8.57/2.12  % (1572054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.12  % (1572054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.12  % (1572054)CaDiCaL version: 2.1.3
% 8.57/2.12  % (1572054)Termination reason: Instruction limit
% 8.57/2.12  % (1572054)Termination phase: Saturation
% 8.57/2.12  % (1572054)Time elapsed: 0.012 s
% 8.57/2.12  % (1572054)Peak memory usage: 89 MB
% 8.57/2.12  % (1572054)Instructions burned: 26 (million)
% 8.57/2.12  % (1572052)Instruction limit reached! 
% 8.57/2.12  % (1572052)------------------------------
% 8.57/2.12  % (1572052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.12  % (1572052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.12  % (1572052)CaDiCaL version: 2.1.3
% 8.57/2.12  % (1572052)Termination reason: Instruction limit
% 8.57/2.12  % (1572052)Termination phase: Saturation
% 8.57/2.12  % (1572052)Time elapsed: 0.026 s
% 8.57/2.12  % (1572052)Peak memory usage: 88 MB
% 8.57/2.12  % (1572052)Instructions burned: 30 (million)
% 8.57/2.12  % (1572053)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1297509009:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 8.57/2.12  % (1572038)Instruction limit reached! 
% 8.57/2.12  % (1572038)------------------------------
% 8.57/2.12  % (1572038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.12  % (1572038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.12  % (1572038)CaDiCaL version: 2.1.3
% 8.57/2.12  % (1572038)Termination reason: Instruction limit
% 8.57/2.12  % (1572038)Termination phase: Saturation
% 8.57/2.12  % (1572038)Time elapsed: 0.297 s
% 8.57/2.12  % (1572038)Peak memory usage: 119 MB
% 8.57/2.12  % (1572038)Instructions burned: 307 (million)
% 8.57/2.12  % (1572053)Instruction limit reached! 
% 8.57/2.12  % (1572053)------------------------------
% 8.57/2.12  % (1572053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.12  % (1572053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/2.12  % (1572053)CaDiCaL version: 2.1.3
% 8.57/2.12  % (1572053)Termination reason: Instruction limit
% 8.57/2.12  % (1572053)Termination phase: Saturation
% 8.57/2.12  % (1572053)Time elapsed: 0.016 s
% 8.57/2.12  % (1572053)Peak memory usage: 90 MB
% 8.57/2.12  % (1572053)Instructions burned: 16 (million)
% 8.57/2.12  % (1572055)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=1327867818:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 8.57/2.12  % (1572055)Instruction limit reached! 
% 8.57/2.12  % (1572055)------------------------------
% 8.57/2.12  % (1572055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.57/2.12  % (1572055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.41  % (1572055)CaDiCaL version: 2.1.3
% 9.87/2.41  % (1572055)Termination reason: Instruction limit
% 9.87/2.41  % (1572055)Termination phase: Saturation
% 9.87/2.41  % (1572055)Time elapsed: 0.023 s
% 9.87/2.41  % (1572055)Peak memory usage: 89 MB
% 9.87/2.41  % (1572055)Instructions burned: 28 (million)
% 9.87/2.41  % (1572056)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4256990047:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 9.87/2.41  % (1572060)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=593300973:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 9.87/2.41  % (1572060)Instruction limit reached! 
% 9.87/2.41  % (1572060)------------------------------
% 9.87/2.41  % (1572060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.41  % (1572060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.41  % (1572060)CaDiCaL version: 2.1.3
% 9.87/2.41  % (1572060)Termination reason: Instruction limit
% 9.87/2.41  % (1572060)Termination phase: Saturation
% 9.87/2.41  % (1572060)Time elapsed: 0.002 s
% 9.87/2.41  % (1572060)Peak memory usage: 88 MB
% 9.87/2.41  % (1572060)Instructions burned: 3 (million)
% 9.87/2.41  % (1572056)Instruction limit reached! 
% 9.87/2.41  % (1572056)------------------------------
% 9.87/2.41  % (1572056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.41  % (1572056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.41  % (1572056)CaDiCaL version: 2.1.3
% 9.87/2.41  % (1572056)Termination reason: Instruction limit
% 9.87/2.41  % (1572056)Termination phase: Saturation
% 9.87/2.41  % (1572056)Time elapsed: 0.082 s
% 9.87/2.41  % (1572056)Peak memory usage: 89 MB
% 9.87/2.41  % (1572056)Instructions burned: 86 (million)
% 9.87/2.41  % (1572061)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1020230693:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.87/2.41  % (1572061)Refutation not found, incomplete strategy
% 9.87/2.41  % (1572061)------------------------------
% 9.87/2.41  % (1572061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.41  % (1572061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.41  % (1572061)CaDiCaL version: 2.1.3
% 9.87/2.41  % (1572061)Termination reason: Refutation not found, incomplete strategy
% 9.87/2.41  % (1572061)Time elapsed: 0.024 s
% 9.87/2.41  % (1572061)Peak memory usage: 89 MB
% 9.87/2.41  % (1572061)Instructions burned: 20 (million)
% 9.87/2.41  % (1572064)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1775689939:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.87/2.41  % (1572066)lrs+10_1_thi=all:si=on:fd=off:random_seed=678674675:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 9.87/2.41  % (1572063)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=854456878:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.87/2.41  % (1572063)Refutation not found, incomplete strategy
% 9.87/2.41  % (1572063)------------------------------
% 9.87/2.41  % (1572063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.41  % (1572063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.41  % (1572063)CaDiCaL version: 2.1.3
% 9.87/2.41  % (1572063)Termination reason: Refutation not found, incomplete strategy
% 9.87/2.41  % (1572063)Time elapsed: 0.005 s
% 9.87/2.41  % (1572063)Peak memory usage: 89 MB
% 9.87/2.41  % (1572063)Instructions burned: 4 (million)
% 9.87/2.41  % (1572051)------------------------------
% 9.87/2.41  % (1572051)------------------------------
% 9.87/2.41  % (1572066)Instruction limit reached! 
% 9.87/2.41  % (1572066)------------------------------
% 9.87/2.41  % (1572066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.41  % (1572066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.41  % (1572066)CaDiCaL version: 2.1.3
% 9.87/2.41  % (1572066)Termination reason: Instruction limit
% 9.87/2.41  % (1572066)Termination phase: Saturation
% 9.87/2.41  % (1572066)Time elapsed: 0.072 s
% 9.87/2.41  % (1572066)Peak memory usage: 112 MB
% 9.87/2.41  % (1572066)Instructions burned: 54 (million)
% 9.87/2.41  % (1572069)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=2421937126:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 10.64/2.61  % (1572069)Instruction limit reached! 
% 10.64/2.61  % (1572069)------------------------------
% 10.64/2.61  % (1572069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572069)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572069)Termination reason: Instruction limit
% 10.64/2.61  % (1572069)Termination phase: Saturation
% 10.64/2.61  % (1572069)Time elapsed: 0.005 s
% 10.64/2.61  % (1572069)Peak memory usage: 88 MB
% 10.64/2.61  % (1572069)Instructions burned: 10 (million)
% 10.64/2.61  % (1572064)Instruction limit reached! 
% 10.64/2.61  % (1572064)------------------------------
% 10.64/2.61  % (1572064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572064)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572064)Termination reason: Instruction limit
% 10.64/2.61  % (1572064)Termination phase: Saturation
% 10.64/2.61  % (1572064)Time elapsed: 0.122 s
% 10.64/2.61  % (1572064)Peak memory usage: 135 MB
% 10.64/2.61  % (1572064)Instructions burned: 66 (million)
% 10.64/2.61  % (1572070)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=145681504:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 10.64/2.61  % (1572070)Instruction limit reached! 
% 10.64/2.61  % (1572070)------------------------------
% 10.64/2.61  % (1572070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572070)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572070)Termination reason: Instruction limit
% 10.64/2.61  % (1572070)Termination phase: Saturation
% 10.64/2.61  % (1572070)Time elapsed: 0.003 s
% 10.64/2.61  % (1572070)Peak memory usage: 88 MB
% 10.64/2.61  % (1572070)Instructions burned: 2 (million)
% 10.64/2.61  % (1572076)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=412392712:i=2:doe=on:canc=force:asg=cautious:rtra=on_2991 on theBenchmark for (2991ds/2Mi)
% 10.64/2.61  % (1572076)Instruction limit reached! 
% 10.64/2.61  % (1572076)------------------------------
% 10.64/2.61  % (1572076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572076)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572076)Termination reason: Instruction limit
% 10.64/2.61  % (1572076)Termination phase: Saturation
% 10.64/2.61  % (1572076)Time elapsed: 0.003 s
% 10.64/2.61  % (1572076)Peak memory usage: 89 MB
% 10.64/2.61  % (1572076)Instructions burned: 5 (million)
% 10.64/2.61  % (1572078)dis+10_1_si=on:random_seed=1153569883:i=10:ep=R:rtra=on_2990 on theBenchmark for (2990ds/10Mi)
% 10.64/2.61  % (1572078)Instruction limit reached! 
% 10.64/2.61  % (1572078)------------------------------
% 10.64/2.61  % (1572078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572078)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572078)Termination reason: Instruction limit
% 10.64/2.61  % (1572078)Termination phase: Saturation
% 10.64/2.61  % (1572078)Time elapsed: 0.011 s
% 10.64/2.61  % (1572078)Peak memory usage: 88 MB
% 10.64/2.61  % (1572078)Instructions burned: 10 (million)
% 10.64/2.61  % (1572077)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1795614931:i=127:doe=on:rtra=on_2990 on theBenchmark for (2990ds/127Mi)
% 10.64/2.61  % (1572061)------------------------------
% 10.64/2.61  % (1572061)------------------------------
% 10.64/2.61  % (1572079)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1062307698:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi)
% 10.64/2.61  % (1572081)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4204532827:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi)
% 10.64/2.61  % (1572063)------------------------------
% 10.64/2.61  % (1572063)------------------------------
% 10.64/2.61  % (1572079)Instruction limit reached! 
% 10.64/2.61  % (1572079)------------------------------
% 10.64/2.61  % (1572079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572079)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572079)Termination reason: Instruction limit
% 10.64/2.61  % (1572079)Termination phase: Saturation
% 10.64/2.61  % (1572079)Time elapsed: 0.021 s
% 10.64/2.61  % (1572079)Peak memory usage: 88 MB
% 10.64/2.61  % (1572079)Instructions burned: 26 (million)
% 10.64/2.61  % (1572081)Instruction limit reached! 
% 10.64/2.61  % (1572081)------------------------------
% 10.64/2.61  % (1572081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572081)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572081)Termination reason: Instruction limit
% 10.64/2.61  % (1572081)Termination phase: Saturation
% 10.64/2.61  % (1572081)Time elapsed: 0.037 s
% 10.64/2.61  % (1572081)Peak memory usage: 89 MB
% 10.64/2.61  % (1572081)Instructions burned: 35 (million)
% 10.64/2.61  % (1572077)First to succeed.
% 10.64/2.61  % (1572077)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1572032"
% 10.64/2.61  % (1572083)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1884456335:i=2:fsr=off:rtra=on:inst=on_2989 on theBenchmark for (2989ds/2Mi)
% 10.64/2.61  % (1572083)Instruction limit reached! 
% 10.64/2.61  % (1572083)------------------------------
% 10.64/2.61  % (1572083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572083)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572083)Termination reason: Instruction limit
% 10.64/2.61  % (1572083)Termination phase: Saturation
% 10.64/2.61  % (1572083)Time elapsed: 0.002 s
% 10.64/2.61  % (1572083)Peak memory usage: 88 MB
% 10.64/2.61  % (1572083)Instructions burned: 3 (million)
% 10.64/2.61  % (1572086)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1804432444:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2988 on theBenchmark for (2988ds/8Mi)
% 10.64/2.61  % (1572086)Instruction limit reached! 
% 10.64/2.61  % (1572086)------------------------------
% 10.64/2.61  % (1572086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572086)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572086)Termination reason: Instruction limit
% 10.64/2.61  % (1572086)Termination phase: Saturation
% 10.64/2.61  % (1572086)Time elapsed: 0.009 s
% 10.64/2.61  % (1572086)Peak memory usage: 88 MB
% 10.64/2.61  % (1572086)Instructions burned: 8 (million)
% 10.64/2.61  % (1572091)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3191579184:i=226:rtra=on:gtg=position:ss=axioms_2987 on theBenchmark for (2987ds/226Mi)
% 10.64/2.61  % (1572089)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3528247072:i=370:ep=RS:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/370Mi)
% 10.64/2.61  % (1572091)Refutation not found, incomplete strategy
% 10.64/2.61  % (1572091)------------------------------
% 10.64/2.61  % (1572091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572091)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572091)Termination reason: Refutation not found, incomplete strategy
% 10.64/2.61  % (1572091)Time elapsed: 0.035 s
% 10.64/2.61  % (1572091)Peak memory usage: 117 MB
% 10.64/2.61  % (1572091)Instructions burned: 15 (million)
% 10.64/2.61  % (1572090)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2720093016:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/13Mi)
% 10.64/2.61  % (1572092)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3789590465:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi)
% 10.64/2.61  % (1572092)Refutation not found, incomplete strategy
% 10.64/2.61  % (1572092)------------------------------
% 10.64/2.61  % (1572092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572092)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572092)Termination reason: Refutation not found, incomplete strategy
% 10.64/2.61  % (1572092)Time elapsed: 0.004 s
% 10.64/2.61  % (1572092)Peak memory usage: 88 MB
% 10.64/2.61  % (1572092)Instructions burned: 3 (million)
% 10.64/2.61  % (1572096)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2171556839:i=71:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/71Mi)
% 10.64/2.61  % (1572090)Instruction limit reached! 
% 10.64/2.61  % (1572090)------------------------------
% 10.64/2.61  % (1572090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572090)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572090)Termination reason: Instruction limit
% 10.64/2.61  % (1572090)Termination phase: Saturation
% 10.64/2.61  % (1572090)Time elapsed: 0.040 s
% 10.64/2.61  % (1572090)Peak memory usage: 112 MB
% 10.64/2.61  % (1572090)Instructions burned: 13 (million)
% 10.64/2.61  % (1572096)Instruction limit reached! 
% 10.64/2.61  % (1572096)------------------------------
% 10.64/2.61  % (1572096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.64/2.61  % (1572096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.64/2.61  % (1572096)CaDiCaL version: 2.1.3
% 10.64/2.61  % (1572096)Termination reason: Instruction limit
% 10.64/2.61  % (1572096)Termination phase: Saturation
% 10.64/2.61  % (1572096)Time elapsed: 0.064 s
% 10.64/2.61  % (1572096)Peak memory usage: 134 MB
% 10.64/2.61  % (1572096)Instructions burned: 72 (million)
% 10.64/2.61  % (1572099)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=4048154645:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2986 on theBenchmark for (2986ds/75Mi)
% 10.64/2.61  % (1572077)Refutation found. Thanks to Tanya!
% 10.64/2.61  % SZS status Theorem for theBenchmark
% 10.64/2.61  % SZS output start Proof for theBenchmark
% See solution above
% 0.27/2.80  % (1572077)------------------------------
% 0.27/2.80  % (1572077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.27/2.80  % (1572077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.27/2.80  % (1572077)CaDiCaL version: 2.1.3
% 0.27/2.80  % (1572077)Termination reason: Refutation
% 0.27/2.80  % (1572077)Time elapsed: 0.138 s
% 0.27/2.80  % (1572077)Peak memory usage: 119 MB
% 0.27/2.80  % (1572077)Instructions burned: 131 (million)
% 0.27/2.80  % (1572077)------------------------------
% 0.27/2.80  % (1572077)------------------------------
% 0.27/2.80  % (1572032)Success in time 1.697 s
% 0.27/2.80  % Vampire exiting
%------------------------------------------------------------------------------