Vampire---5.0.1.THM-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : NUM688+4 : TPTP v9.3.1. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n014.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 12:16:29 PM UTC 2026

% Result   : Theorem 64.92s 11.55s
% Output   : Refutation 76.14s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   24
%            Number of leaves      :   58
% Syntax   : Number of formulae    :  323 (  53 unt;  35 def)
%            Number of atoms       :  803 (   7 equ)
%            Maximal formula atoms :    8 (   2 avg)
%            Number of connectives :  822 ( 342   ~; 376   |;  38   &)
%                                         (  58 <=>;   8  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   10 (   4 avg)
%            Maximal term depth    :   12 (   2 avg)
%            Number of predicates  :   40 (  38 usr;  36 prp; 0-2 aty)
%            Number of functors    :   34 (  34 usr;  15 con; 0-2 aty)
%            Number of variables   :  228 (   0 sgn 226   !;   2   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f26,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X0),X1))
    <=> pp(aa_bool_bool(scratc1668515442d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__moreis) ).

fof(f35,axiom,
    ! [X0] : scratc1800225965d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__pl) ).

fof(f110,axiom,
    ! [X0] : scratc1668515442d_l_or(X0) = aa_boo1142376798l_bool(scratc1771857711nd_imp,scratc1308359756_d_not(X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__l__or) ).

fof(f115,axiom,
    ! [X0] :
      ( pp(scratc1308359756_d_not(X0))
    <=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1771857711nd_imp,X0),fFalse)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__not) ).

fof(f116,axiom,
    scratc1771857711nd_imp = fimplies,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__imp) ).

fof(f147,axiom,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
    <=> ! [X2] :
          ( gg_TPTP_ind(X2)
         => ( scratc65955326_is_of(X2,X0)
           => pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).

fof(f151,axiom,
    pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_cd)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz21) ).

fof(f164,axiom,
    pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_dt)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz19h) ).

fof(f345,axiom,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_dt,X0))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ds,X0))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__61) ).

fof(f358,axiom,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__74) ).

fof(f361,axiom,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__77) ).

fof(f422,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ds,X0),X1))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dr(X0),X1))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__138) ).

fof(f435,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__151) ).

fof(f438,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__154) ).

fof(f493,axiom,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dr(X0),X1),X2))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__209) ).

fof(f496,axiom,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__212) ).

fof(f499,axiom,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
    <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__215) ).

fof(f513,axiom,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))
       => ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
         => pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3))) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__229) ).

fof(f514,axiom,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))
       => ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X2),X3))
         => pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3))) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__230) ).

fof(f517,axiom,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1))
       => ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
         => pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X3),X1))) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__233) ).

fof(f541,axiom,
    ! [X0,X1] :
      ( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
      | ~ pp(X0)
      | pp(X1) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_3_1_U) ).

fof(f543,axiom,
    ! [X0,X1] :
      ( pp(X0)
      | pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_1_1_U) ).

fof(f550,conjecture,
    pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_ad)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

fof(f551,negated_conjecture,
    ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_ad)),
    inference(negated_conjecture,[status(cth)],[f550]) ).

fof(f552,plain,
    ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_ad)),
    inference(flattening,[],[f551]) ).

fof(f569,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
    <=> ! [X2] :
          ( pp(aa_TPTP_ind_bool(X1,X2))
          | ~ scratc65955326_is_of(X2,X0)
          | ~ gg_TPTP_ind(X2) ) ),
    inference(ennf_transformation,[],[f147]) ).

fof(f570,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
    <=> ! [X2] :
          ( pp(aa_TPTP_ind_bool(X1,X2))
          | ~ scratc65955326_is_of(X2,X0)
          | ~ gg_TPTP_ind(X2) ) ),
    inference(flattening,[],[f569]) ).

fof(f686,plain,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ) ),
    inference(ennf_transformation,[],[f513]) ).

fof(f687,plain,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ) ),
    inference(flattening,[],[f686]) ).

fof(f688,plain,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ) ),
    inference(ennf_transformation,[],[f514]) ).

fof(f689,plain,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ) ),
    inference(flattening,[],[f688]) ).

fof(f694,plain,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X3),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1)) ) ),
    inference(ennf_transformation,[],[f517]) ).

fof(f695,plain,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X3),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1)) ) ),
    inference(flattening,[],[f694]) ).

fof(f715,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X0),X1))
        | ~ pp(aa_bool_bool(scratc1668515442d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1))) )
      & ( pp(aa_bool_bool(scratc1668515442d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X0),X1)) ) ),
    inference(nnf_transformation,[],[f26]) ).

fof(f758,plain,
    ! [X0] :
      ( ( pp(scratc1308359756_d_not(X0))
        | ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1771857711nd_imp,X0),fFalse)) )
      & ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1771857711nd_imp,X0),fFalse))
        | ~ pp(scratc1308359756_d_not(X0)) ) ),
    inference(nnf_transformation,[],[f115]) ).

fof(f781,plain,
    ! [X0,X1] :
      ( ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
        | ? [X2] :
            ( ~ pp(aa_TPTP_ind_bool(X1,X2))
            & scratc65955326_is_of(X2,X0)
            & gg_TPTP_ind(X2) ) )
      & ( ! [X2] :
            ( pp(aa_TPTP_ind_bool(X1,X2))
            | ~ scratc65955326_is_of(X2,X0)
            | ~ gg_TPTP_ind(X2) )
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1)) ) ),
    inference(nnf_transformation,[],[f570]) ).

fof(f782,plain,
    ! [X0,X1] :
      ( ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
        | ? [X2] :
            ( ~ pp(aa_TPTP_ind_bool(X1,X2))
            & scratc65955326_is_of(X2,X0)
            & gg_TPTP_ind(X2) ) )
      & ( ! [X3] :
            ( pp(aa_TPTP_ind_bool(X1,X3))
            | ~ scratc65955326_is_of(X3,X0)
            | ~ gg_TPTP_ind(X3) )
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1)) ) ),
    inference(rectify,[],[f781]) ).

fof(f783,plain,
    ! [X0,X1] :
      ( ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
        | ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
          & scratc65955326_is_of(sK12(X0,X1),X0)
          & gg_TPTP_ind(sK12(X0,X1)) ) )
      & ( ! [X3] :
            ( pp(aa_TPTP_ind_bool(X1,X3))
            | ~ scratc65955326_is_of(X3,X0)
            | ~ gg_TPTP_ind(X3) )
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1)) ) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f782]) ).

fof(f863,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dt,X0))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ds,X0))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ds,X0)))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dt,X0)) ) ),
    inference(nnf_transformation,[],[f345]) ).

fof(f876,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0)))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0)) ) ),
    inference(nnf_transformation,[],[f358]) ).

fof(f879,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0)))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0)) ) ),
    inference(nnf_transformation,[],[f361]) ).

fof(f955,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ds,X0),X1))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dr(X0),X1))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dr(X0),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ds,X0),X1)) ) ),
    inference(nnf_transformation,[],[f422]) ).

fof(f968,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1)) ) ),
    inference(nnf_transformation,[],[f435]) ).

fof(f971,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1)) ) ),
    inference(nnf_transformation,[],[f438]) ).

fof(f1052,plain,
    ! [X0,X1,X2] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dr(X0),X1),X2))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dr(X0),X1),X2)) ) ),
    inference(nnf_transformation,[],[f493]) ).

fof(f1055,plain,
    ! [X0,X1,X2] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2)) ) ),
    inference(nnf_transformation,[],[f496]) ).

fof(f1058,plain,
    ! [X0,X1,X2] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) )
      & ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2)) ) ),
    inference(nnf_transformation,[],[f499]) ).

fof(f1075,plain,
    ! [X0,X1,X2,X3] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3)) ) ),
    inference(nnf_transformation,[],[f687]) ).

fof(f1076,plain,
    ! [X0,X1,X2,X3] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3)) ) ),
    inference(flattening,[],[f1075]) ).

fof(f1077,plain,
    ! [X0,X1,X2,X3] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X2),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
    inference(nnf_transformation,[],[f689]) ).

fof(f1078,plain,
    ! [X0,X1,X2,X3] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X2),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
    inference(flattening,[],[f1077]) ).

fof(f1083,plain,
    ! [X0,X1,X2,X3] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X3),X1)))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X3),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3)) ) ),
    inference(nnf_transformation,[],[f695]) ).

fof(f1084,plain,
    ! [X0,X1,X2,X3] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X3),X1)))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X3),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3)) ) ),
    inference(flattening,[],[f1083]) ).

fof(f1132,plain,
    ! [X0,X1] :
      ( pp(aa_bool_bool(scratc1668515442d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X0),X1)) ),
    inference(cnf_transformation,[],[f715]) ).

fof(f1150,plain,
    ! [X0] : scratc1800225965d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,X0)),
    inference(cnf_transformation,[],[f35]) ).

fof(f1254,plain,
    ! [X0] : aa_boo1142376798l_bool(scratc1771857711nd_imp,scratc1308359756_d_not(X0)) = scratc1668515442d_l_or(X0),
    inference(cnf_transformation,[],[f110]) ).

fof(f1261,plain,
    ! [X0] :
      ( pp(scratc1308359756_d_not(X0))
      | ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1771857711nd_imp,X0),fFalse)) ),
    inference(cnf_transformation,[],[f758]) ).

fof(f1262,plain,
    scratc1771857711nd_imp = fimplies,
    inference(cnf_transformation,[],[f116]) ).

fof(f1324,plain,
    ! [X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(X1,X3))
      | ~ scratc65955326_is_of(X3,X0)
      | ~ gg_TPTP_ind(X3)
      | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1)) ),
    inference(cnf_transformation,[],[f783]) ).

fof(f1325,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
      | gg_TPTP_ind(sK12(X0,X1)) ),
    inference(cnf_transformation,[],[f783]) ).

fof(f1326,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
      | scratc65955326_is_of(sK12(X0,X1),X0) ),
    inference(cnf_transformation,[],[f783]) ).

fof(f1327,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),X1))
      | ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
    inference(cnf_transformation,[],[f783]) ).

fof(f1332,plain,
    pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_cd)),
    inference(cnf_transformation,[],[f151]) ).

fof(f1345,plain,
    pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_dt)),
    inference(cnf_transformation,[],[f164]) ).

fof(f1616,plain,
    ! [X0] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ds,X0)))
      | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dt,X0)) ),
    inference(cnf_transformation,[],[f863]) ).

fof(f1642,plain,
    ! [X0] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0)))
      | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0)) ),
    inference(cnf_transformation,[],[f876]) ).

fof(f1649,plain,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
      | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
    inference(cnf_transformation,[],[f879]) ).

fof(f1783,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dr(X0),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ds,X0),X1)) ),
    inference(cnf_transformation,[],[f955]) ).

fof(f1809,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1)) ),
    inference(cnf_transformation,[],[f968]) ).

fof(f1816,plain,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
      | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
    inference(cnf_transformation,[],[f971]) ).

fof(f1957,plain,
    ! [X2,X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dr(X0),X1),X2)) ),
    inference(cnf_transformation,[],[f1052]) ).

fof(f1963,plain,
    ! [X2,X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2)) ),
    inference(cnf_transformation,[],[f1055]) ).

fof(f1970,plain,
    ! [X2,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
      | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
    inference(cnf_transformation,[],[f1058]) ).

fof(f2003,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3)) ),
    inference(cnf_transformation,[],[f1076]) ).

fof(f2008,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
      | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1)) ),
    inference(cnf_transformation,[],[f1078]) ).

fof(f2009,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
      | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X2),X3)) ),
    inference(cnf_transformation,[],[f1078]) ).

fof(f2010,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X1),X3))) ),
    inference(cnf_transformation,[],[f1078]) ).

fof(f2019,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1800225965d_n_pl(X3),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3)) ),
    inference(cnf_transformation,[],[f1084]) ).

fof(f2073,plain,
    ! [X0,X1] :
      ( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
      | ~ pp(X0)
      | pp(X1) ),
    inference(cnf_transformation,[],[f541]) ).

fof(f2075,plain,
    ! [X0,X1] :
      ( pp(X0)
      | pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
    inference(cnf_transformation,[],[f543]) ).

fof(f2082,plain,
    ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_ad)),
    inference(cnf_transformation,[],[f552]) ).

fof(f2085,plain,
    ! [X0] : scratc1668515442d_l_or(X0) = aa_boo1142376798l_bool(fimplies,scratc1308359756_d_not(X0)),
    inference(definition_unfolding,[],[f1254,f1262]) ).

fof(f2091,plain,
    ! [X0,X1] :
      ( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1308359756_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,X0),X1)) ),
    inference(definition_unfolding,[],[f1132,f2085]) ).

fof(f2134,plain,
    ! [X0] :
      ( pp(scratc1308359756_d_not(X0))
      | ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse)) ),
    inference(definition_unfolding,[],[f1261,f1262]) ).

fof(f2244,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,X1)),X3)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X0),X1))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3)) ),
    inference(definition_unfolding,[],[f2003,f1150,f1150]) ).

fof(f2245,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,X1)),X3))) ),
    inference(definition_unfolding,[],[f2010,f1150,f1150]) ).

fof(f2252,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,X2)),X0)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,X3)),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,X2),X3))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,X0),X1))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(X0),X1),X2),X3)) ),
    inference(definition_unfolding,[],[f2019,f1150,f1150]) ).

fof(f2290,definition,
    ( spl29_1
  <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_ad)) ),
    introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).

fof(f2292,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_ad))
    | spl29_1 ),
    inference(avatar_component_clause,[],[f2290]) ).

fof(f2293,plain,
    ~ spl29_1,
    inference(avatar_split_clause,[],[f2082,f2290]) ).

fof(f2294,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
    | spl29_1 ),
    inference(resolution,[],[f2292,f1325]) ).

fof(f2295,plain,
    ( scratc65955326_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
    | spl29_1 ),
    inference(resolution,[],[f2292,f1326]) ).

fof(f2296,plain,
    ( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
    | spl29_1 ),
    inference(resolution,[],[f2292,f1327]) ).

fof(f2309,definition,
    ( spl29_2
  <=> scratc65955326_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a) ),
    introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).

fof(f2311,plain,
    ( scratc65955326_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
    | ~ spl29_2 ),
    inference(avatar_component_clause,[],[f2309]) ).

fof(f2312,plain,
    ( spl29_2
    | spl29_1 ),
    inference(avatar_split_clause,[],[f2295,f2290,f2309]) ).

fof(f2314,definition,
    ( spl29_3
  <=> pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
    introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).

fof(f2316,plain,
    ( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
    | spl29_3 ),
    inference(avatar_component_clause,[],[f2314]) ).

fof(f2317,plain,
    ( ~ spl29_3
    | spl29_1 ),
    inference(avatar_split_clause,[],[f2296,f2290,f2314]) ).

fof(f2318,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | spl29_3 ),
    inference(resolution,[],[f2316,f1649]) ).

fof(f2356,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_2 ),
    inference(resolution,[],[f2311,f1324]) ).

fof(f2357,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | spl29_1
    | ~ spl29_2 ),
    inference(forward_subsumption_resolution,[],[f2356,f2294]) ).

fof(f2359,definition,
    ( spl29_4
  <=> ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) ) ),
    introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).

fof(f2360,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_4 ),
    inference(avatar_component_clause,[],[f2359]) ).

fof(f2361,plain,
    ( spl29_4
    | spl29_1
    | ~ spl29_2 ),
    inference(avatar_split_clause,[],[f2357,f2309,f2290,f2359]) ).

fof(f2729,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_cd))
    | pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | ~ spl29_4 ),
    inference(resolution,[],[f2360,f1642]) ).

fof(f2887,plain,
    ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | ~ spl29_4 ),
    inference(forward_subsumption_resolution,[],[f2729,f1332]) ).

fof(f2953,definition,
    ( spl29_5
  <=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad)) ),
    introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).

fof(f2955,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
    | ~ spl29_5 ),
    inference(avatar_component_clause,[],[f2953]) ).

fof(f2956,plain,
    ( spl29_5
    | spl29_1 ),
    inference(avatar_split_clause,[],[f2294,f2290,f2953]) ).

fof(f2958,definition,
    ( spl29_6
  <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
    introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).

fof(f2960,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | spl29_6 ),
    inference(avatar_component_clause,[],[f2958]) ).

fof(f2961,plain,
    ( ~ spl29_6
    | spl29_3 ),
    inference(avatar_split_clause,[],[f2318,f2314,f2958]) ).

fof(f2963,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | spl29_6 ),
    inference(resolution,[],[f2960,f1325]) ).

fof(f2964,plain,
    ( scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a)
    | spl29_6 ),
    inference(resolution,[],[f2960,f1326]) ).

fof(f2965,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
    | spl29_6 ),
    inference(resolution,[],[f2960,f1327]) ).

fof(f2978,definition,
    ( spl29_7
  <=> scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a) ),
    introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).

fof(f2980,plain,
    ( scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a)
    | ~ spl29_7 ),
    inference(avatar_component_clause,[],[f2978]) ).

fof(f2981,plain,
    ( spl29_7
    | spl29_6 ),
    inference(avatar_split_clause,[],[f2964,f2958,f2978]) ).

fof(f2983,definition,
    ( spl29_8
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))) ),
    introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).

fof(f2985,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
    | spl29_8 ),
    inference(avatar_component_clause,[],[f2983]) ).

fof(f2986,plain,
    ( ~ spl29_8
    | spl29_6 ),
    inference(avatar_split_clause,[],[f2965,f2958,f2983]) ).

fof(f2987,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
    | spl29_8 ),
    inference(resolution,[],[f2985,f1816]) ).

fof(f3033,definition,
    ( spl29_9
  <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) ),
    introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).

fof(f3035,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
    | spl29_9 ),
    inference(avatar_component_clause,[],[f3033]) ).

fof(f3036,plain,
    ( ~ spl29_9
    | spl29_8 ),
    inference(avatar_split_clause,[],[f2987,f2983,f3033]) ).

fof(f3038,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
    | spl29_9 ),
    inference(resolution,[],[f3035,f1325]) ).

fof(f3039,plain,
    ( scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
    | spl29_9 ),
    inference(resolution,[],[f3035,f1326]) ).

fof(f3040,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
    | spl29_9 ),
    inference(resolution,[],[f3035,f1327]) ).

fof(f3053,definition,
    ( spl29_10
  <=> scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a) ),
    introduced(definition,[new_symbols(definition,[spl29_10])],[avatar_definition]) ).

fof(f3055,plain,
    ( scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
    | ~ spl29_10 ),
    inference(avatar_component_clause,[],[f3053]) ).

fof(f3056,plain,
    ( spl29_10
    | spl29_9 ),
    inference(avatar_split_clause,[],[f3039,f3033,f3053]) ).

fof(f3058,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_10 ),
    inference(resolution,[],[f3055,f1324]) ).

fof(f3059,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | spl29_9
    | ~ spl29_10 ),
    inference(forward_subsumption_resolution,[],[f3058,f3038]) ).

fof(f3061,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_7 ),
    inference(resolution,[],[f2980,f1324]) ).

fof(f3062,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | spl29_6
    | ~ spl29_7 ),
    inference(forward_subsumption_resolution,[],[f3061,f2963]) ).

fof(f3064,definition,
    ( spl29_11
  <=> ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) ) ),
    introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).

fof(f3065,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_11 ),
    inference(avatar_component_clause,[],[f3064]) ).

fof(f3066,plain,
    ( spl29_11
    | spl29_6
    | ~ spl29_7 ),
    inference(avatar_split_clause,[],[f3062,f2978,f2958,f3064]) ).

fof(f3340,plain,
    ( ! [X0] :
        ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0)))
        | pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) )
    | ~ spl29_11 ),
    inference(resolution,[],[f3065,f1809]) ).

fof(f3658,definition,
    ( spl29_12
  <=> ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) ) ),
    introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).

fof(f3659,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_12 ),
    inference(avatar_component_clause,[],[f3658]) ).

fof(f3660,plain,
    ( spl29_12
    | spl29_9
    | ~ spl29_10 ),
    inference(avatar_split_clause,[],[f3059,f3053,f3033,f3658]) ).

fof(f3854,definition,
    ( spl29_16
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_16])],[avatar_definition]) ).

fof(f3856,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
    | spl29_16 ),
    inference(avatar_component_clause,[],[f3854]) ).

fof(f3857,plain,
    ( ~ spl29_16
    | spl29_9 ),
    inference(avatar_split_clause,[],[f3040,f3033,f3854]) ).

fof(f3858,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
    | spl29_16 ),
    inference(resolution,[],[f3856,f1970]) ).

fof(f3904,definition,
    ( spl29_17
  <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_17])],[avatar_definition]) ).

fof(f3906,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
    | spl29_17 ),
    inference(avatar_component_clause,[],[f3904]) ).

fof(f3907,plain,
    ( ~ spl29_17
    | spl29_16 ),
    inference(avatar_split_clause,[],[f3858,f3854,f3904]) ).

fof(f3909,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
    | spl29_17 ),
    inference(resolution,[],[f3906,f1325]) ).

fof(f3910,plain,
    ( scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a)
    | spl29_17 ),
    inference(resolution,[],[f3906,f1326]) ).

fof(f3911,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_17 ),
    inference(resolution,[],[f3906,f1327]) ).

fof(f3924,definition,
    ( spl29_18
  <=> scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a) ),
    introduced(definition,[new_symbols(definition,[spl29_18])],[avatar_definition]) ).

fof(f3926,plain,
    ( scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a)
    | ~ spl29_18 ),
    inference(avatar_component_clause,[],[f3924]) ).

fof(f3927,plain,
    ( spl29_18
    | spl29_17 ),
    inference(avatar_split_clause,[],[f3910,f3904,f3924]) ).

fof(f3929,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_18 ),
    inference(resolution,[],[f3926,f1324]) ).

fof(f3930,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | spl29_17
    | ~ spl29_18 ),
    inference(forward_subsumption_resolution,[],[f3929,f3909]) ).

fof(f3939,definition,
    ( spl29_20
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).

fof(f3941,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_20 ),
    inference(avatar_component_clause,[],[f3939]) ).

fof(f3942,plain,
    ( ~ spl29_20
    | spl29_17 ),
    inference(avatar_split_clause,[],[f3911,f3904,f3939]) ).

fof(f3943,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
    | spl29_20 ),
    inference(resolution,[],[f3941,f2008]) ).

fof(f3944,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_20 ),
    inference(resolution,[],[f3941,f2009]) ).

fof(f3945,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
    | spl29_20 ),
    inference(resolution,[],[f3941,f2245]) ).

fof(f3991,definition,
    ( spl29_21
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_21])],[avatar_definition]) ).

fof(f3993,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc949680012bnd_ap,aa_TPTP_ind_TPTP_ind(scratc702745591d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
    | spl29_21 ),
    inference(avatar_component_clause,[],[f3991]) ).

fof(f3994,plain,
    ( ~ spl29_21
    | spl29_20 ),
    inference(avatar_split_clause,[],[f3945,f3939,f3991]) ).

fof(f3995,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
    | spl29_21 ),
    inference(resolution,[],[f3993,f2252]) ).

fof(f3999,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_21 ),
    inference(resolution,[],[f3993,f2244]) ).

fof(f4064,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_20
    | spl29_21 ),
    inference(forward_subsumption_resolution,[],[f3999,f3943]) ).

fof(f4065,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
    | spl29_20
    | spl29_21 ),
    inference(forward_subsumption_resolution,[],[f3995,f3943]) ).

fof(f4068,definition,
    ( spl29_22
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_22])],[avatar_definition]) ).

fof(f4070,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_22 ),
    inference(avatar_component_clause,[],[f4068]) ).

fof(f4072,definition,
    ( spl29_23
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_23])],[avatar_definition]) ).

fof(f4074,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_23 ),
    inference(avatar_component_clause,[],[f4072]) ).

fof(f4075,plain,
    ( ~ spl29_22
    | ~ spl29_23
    | spl29_20
    | spl29_21 ),
    inference(avatar_split_clause,[],[f4064,f3991,f3939,f4072,f4068]) ).

fof(f4088,plain,
    ( ! [X0] :
        ( ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) )
    | spl29_22 ),
    inference(resolution,[],[f4070,f1324]) ).

fof(f4122,plain,
    ( ! [X0] :
        ( ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) )
    | spl29_17
    | spl29_22 ),
    inference(forward_subsumption_resolution,[],[f4088,f3909]) ).

fof(f4144,definition,
    ( spl29_28
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))) ),
    introduced(definition,[new_symbols(definition,[spl29_28])],[avatar_definition]) ).

fof(f4146,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
    | spl29_28 ),
    inference(avatar_component_clause,[],[f4144]) ).

fof(f4148,definition,
    ( spl29_29
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_29])],[avatar_definition]) ).

fof(f4150,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_29 ),
    inference(avatar_component_clause,[],[f4148]) ).

fof(f4151,plain,
    ( ~ spl29_28
    | ~ spl29_29
    | spl29_20
    | spl29_21 ),
    inference(avatar_split_clause,[],[f4065,f3991,f3939,f4148,f4144]) ).

fof(f4161,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | ~ spl29_11
    | spl29_28 ),
    inference(resolution,[],[f4146,f3065]) ).

fof(f4295,definition,
    ( spl29_30
  <=> ! [X0] :
        ( ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_30])],[avatar_definition]) ).

fof(f4296,plain,
    ( ! [X0] :
        ( ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) )
    | ~ spl29_30 ),
    inference(avatar_component_clause,[],[f4295]) ).

fof(f4297,plain,
    ( spl29_30
    | spl29_17
    | spl29_22 ),
    inference(avatar_split_clause,[],[f4122,f4068,f3904,f4295]) ).

fof(f4545,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
    | ~ spl29_18
    | ~ spl29_30 ),
    inference(resolution,[],[f4296,f3926]) ).

fof(f4548,definition,
    ( spl29_35
  <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_35])],[avatar_definition]) ).

fof(f4550,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
    | spl29_35 ),
    inference(avatar_component_clause,[],[f4548]) ).

fof(f4551,plain,
    ( ~ spl29_35
    | ~ spl29_18
    | ~ spl29_30 ),
    inference(avatar_split_clause,[],[f4545,f4295,f3924,f4548]) ).

fof(f4561,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
    | spl29_35 ),
    inference(resolution,[],[f4550,f1963]) ).

fof(f4999,definition,
    ( spl29_43
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dr(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
    introduced(definition,[new_symbols(definition,[spl29_43])],[avatar_definition]) ).

fof(f5000,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dr(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
    | ~ spl29_43 ),
    inference(avatar_component_clause,[],[f4999]) ).

fof(f5001,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dr(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
    | spl29_43 ),
    inference(avatar_component_clause,[],[f4999]) ).

fof(f5014,plain,
    ( ! [X0] :
        ( ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),X0)
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dr(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) )
    | spl29_43 ),
    inference(resolution,[],[f5001,f1324]) ).

fof(f5048,plain,
    ( ! [X0] :
        ( ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),X0)
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dr(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) )
    | ~ spl29_5
    | spl29_43 ),
    inference(forward_subsumption_resolution,[],[f5014,f2955]) ).

fof(f5096,definition,
    ( spl29_44
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_44])],[avatar_definition]) ).

fof(f5098,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1138641084moreis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | ~ spl29_44 ),
    inference(avatar_component_clause,[],[f5096]) ).

fof(f5099,plain,
    ( spl29_44
    | spl29_20 ),
    inference(avatar_split_clause,[],[f3944,f3939,f5096]) ).

fof(f5106,plain,
    ( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1308359756_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
    | ~ spl29_44 ),
    inference(resolution,[],[f5098,f2091]) ).

fof(f5144,definition,
    ( spl29_45
  <=> pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1308359756_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_45])],[avatar_definition]) ).

fof(f5146,plain,
    ( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1308359756_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
    | ~ spl29_45 ),
    inference(avatar_component_clause,[],[f5144]) ).

fof(f5147,plain,
    ( spl29_45
    | ~ spl29_44 ),
    inference(avatar_split_clause,[],[f5106,f5096,f5144]) ).

fof(f5149,plain,
    ( ~ pp(scratc1308359756_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
    | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1799766779d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | ~ spl29_45 ),
    inference(resolution,[],[f5146,f2073]) ).

fof(f5675,plain,
    ( ! [X0] : pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),X0))
    | spl29_23 ),
    inference(resolution,[],[f4074,f2075]) ).

fof(f6367,definition,
    ( spl29_67
  <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
    introduced(definition,[new_symbols(definition,[spl29_67])],[avatar_definition]) ).

fof(f6369,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | spl29_67 ),
    inference(avatar_component_clause,[],[f6367]) ).

fof(f6370,plain,
    ( ~ spl29_67
    | ~ spl29_11
    | spl29_28 ),
    inference(avatar_split_clause,[],[f4161,f4144,f3064,f6367]) ).

fof(f6930,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aTP_Lamm_dt))
    | pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ds,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
    | ~ spl29_12 ),
    inference(resolution,[],[f3659,f1616]) ).

fof(f7061,plain,
    ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ds,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
    | ~ spl29_12 ),
    inference(forward_subsumption_resolution,[],[f6930,f1345]) ).

fof(f7654,definition,
    ( spl29_80
  <=> ! [X0] :
        ( ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),X0)
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dr(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_80])],[avatar_definition]) ).

fof(f7655,plain,
    ( ! [X0] :
        ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dr(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
        | ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),X0) )
    | ~ spl29_80 ),
    inference(avatar_component_clause,[],[f7654]) ).

fof(f7656,plain,
    ( spl29_80
    | ~ spl29_5
    | spl29_43 ),
    inference(avatar_split_clause,[],[f5048,f4999,f2953,f7654]) ).

fof(f7657,plain,
    ( ~ pp(scratc1308359756_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
    | spl29_29
    | ~ spl29_45 ),
    inference(forward_subsumption_resolution,[],[f5149,f4150]) ).

fof(f7712,definition,
    ( spl29_81
  <=> pp(scratc1308359756_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_81])],[avatar_definition]) ).

fof(f7714,plain,
    ( ~ pp(scratc1308359756_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
    | spl29_81 ),
    inference(avatar_component_clause,[],[f7712]) ).

fof(f7715,plain,
    ( ~ spl29_81
    | spl29_29
    | ~ spl29_45 ),
    inference(avatar_split_clause,[],[f7657,f5144,f4148,f7712]) ).

fof(f7755,plain,
    ( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2074469166_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),fFalse))
    | spl29_81 ),
    inference(resolution,[],[f7714,f2134]) ).

fof(f7767,plain,
    ( $false
    | spl29_23
    | spl29_81 ),
    inference(forward_subsumption_resolution,[],[f7755,f5675]) ).

fof(f7768,plain,
    ( spl29_23
    | spl29_81 ),
    inference(avatar_contradiction_clause,[],[f7767]) ).

fof(f7986,plain,
    ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dq(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | ~ spl29_43 ),
    inference(resolution,[],[f5000,f1957]) ).

fof(f8019,plain,
    ( $false
    | ~ spl29_43
    | spl29_67 ),
    inference(forward_subsumption_resolution,[],[f7986,f6369]) ).

fof(f8020,plain,
    ( ~ spl29_43
    | spl29_67 ),
    inference(avatar_contradiction_clause,[],[f8019]) ).

fof(f8610,definition,
    ( spl29_87
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_87])],[avatar_definition]) ).

fof(f8612,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
    | spl29_87 ),
    inference(avatar_component_clause,[],[f8610]) ).

fof(f8613,plain,
    ( ~ spl29_87
    | spl29_35 ),
    inference(avatar_split_clause,[],[f4561,f4548,f8610]) ).

fof(f8728,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
    | ~ spl29_12
    | spl29_87 ),
    inference(resolution,[],[f8612,f3659]) ).

fof(f8782,plain,
    ( ~ scratc65955326_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ds,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | ~ spl29_80 ),
    inference(resolution,[],[f7655,f1783]) ).

fof(f8798,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ds,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | ~ spl29_2
    | ~ spl29_80 ),
    inference(forward_subsumption_resolution,[],[f8782,f2311]) ).

fof(f8800,definition,
    ( spl29_93
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ds,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_93])],[avatar_definition]) ).

fof(f8802,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ds,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
    | spl29_93 ),
    inference(avatar_component_clause,[],[f8800]) ).

fof(f8803,plain,
    ( ~ spl29_93
    | ~ spl29_2
    | ~ spl29_80 ),
    inference(avatar_split_clause,[],[f8798,f7654,f2309,f8800]) ).

fof(f12780,definition,
    ( spl29_112
  <=> ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) ) ),
    introduced(definition,[new_symbols(definition,[spl29_112])],[avatar_definition]) ).

fof(f12781,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_112 ),
    inference(avatar_component_clause,[],[f12780]) ).

fof(f12782,plain,
    ( spl29_112
    | spl29_17
    | ~ spl29_18 ),
    inference(avatar_split_clause,[],[f3930,f3924,f3904,f12780]) ).

fof(f13073,definition,
    ( spl29_121
  <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) ),
    introduced(definition,[new_symbols(definition,[spl29_121])],[avatar_definition]) ).

fof(f13075,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
    | spl29_121 ),
    inference(avatar_component_clause,[],[f13073]) ).

fof(f13076,plain,
    ( ~ spl29_121
    | ~ spl29_12
    | spl29_87 ),
    inference(avatar_split_clause,[],[f8728,f8610,f3658,f13073]) ).

fof(f19510,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ds,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
    | spl29_93
    | ~ spl29_112 ),
    inference(resolution,[],[f12781,f8802]) ).

fof(f19524,plain,
    ( $false
    | ~ spl29_12
    | spl29_93
    | ~ spl29_112 ),
    inference(forward_subsumption_resolution,[],[f19510,f7061]) ).

fof(f19525,plain,
    ( ~ spl29_12
    | spl29_93
    | ~ spl29_112 ),
    inference(avatar_contradiction_clause,[],[f19524]) ).

fof(f20072,definition,
    ( spl29_220
  <=> pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
    introduced(definition,[new_symbols(definition,[spl29_220])],[avatar_definition]) ).

fof(f20074,plain,
    ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | ~ spl29_220 ),
    inference(avatar_component_clause,[],[f20072]) ).

fof(f20075,plain,
    ( spl29_220
    | ~ spl29_4 ),
    inference(avatar_split_clause,[],[f2887,f2359,f20072]) ).

fof(f84330,definition,
    ( spl29_2388
  <=> ! [X0] :
        ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0)))
        | pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_2388])],[avatar_definition]) ).

fof(f84331,plain,
    ( ! [X0] :
        ( pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
        | ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0))) )
    | ~ spl29_2388 ),
    inference(avatar_component_clause,[],[f84330]) ).

fof(f84332,plain,
    ( spl29_2388
    | ~ spl29_11 ),
    inference(avatar_split_clause,[],[f3340,f3064,f84330]) ).

fof(f84333,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc2084821595all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
    | spl29_121
    | ~ spl29_2388 ),
    inference(resolution,[],[f84331,f13075]) ).

fof(f84342,plain,
    ( $false
    | spl29_121
    | ~ spl29_220
    | ~ spl29_2388 ),
    inference(forward_subsumption_resolution,[],[f84333,f20074]) ).

fof(f84343,plain,
    ( spl29_121
    | ~ spl29_220
    | ~ spl29_2388 ),
    inference(avatar_contradiction_clause,[],[f84342]) ).

cnf(s1,plain,
    ~ spl29_1,
    inference(sat_conversion,[],[f2293]) ).

cnf(s2,plain,
    ( spl29_1
    | spl29_2 ),
    inference(sat_conversion,[],[f2312]) ).

cnf(s3,plain,
    ( spl29_1
    | ~ spl29_3 ),
    inference(sat_conversion,[],[f2317]) ).

cnf(s4,plain,
    ( spl29_1
    | ~ spl29_2
    | spl29_4 ),
    inference(sat_conversion,[],[f2361]) ).

cnf(s5,plain,
    ( spl29_1
    | spl29_5 ),
    inference(sat_conversion,[],[f2956]) ).

cnf(s6,plain,
    ( spl29_3
    | ~ spl29_6 ),
    inference(sat_conversion,[],[f2961]) ).

cnf(s7,plain,
    ( spl29_6
    | spl29_7 ),
    inference(sat_conversion,[],[f2981]) ).

cnf(s8,plain,
    ( spl29_6
    | ~ spl29_8 ),
    inference(sat_conversion,[],[f2986]) ).

cnf(s9,plain,
    ( spl29_8
    | ~ spl29_9 ),
    inference(sat_conversion,[],[f3036]) ).

cnf(s10,plain,
    ( spl29_9
    | spl29_10 ),
    inference(sat_conversion,[],[f3056]) ).

cnf(s11,plain,
    ( spl29_6
    | ~ spl29_7
    | spl29_11 ),
    inference(sat_conversion,[],[f3066]) ).

cnf(s12,plain,
    ( spl29_9
    | ~ spl29_10
    | spl29_12 ),
    inference(sat_conversion,[],[f3660]) ).

cnf(s16,plain,
    ( spl29_9
    | ~ spl29_16 ),
    inference(sat_conversion,[],[f3857]) ).

cnf(s17,plain,
    ( spl29_16
    | ~ spl29_17 ),
    inference(sat_conversion,[],[f3907]) ).

cnf(s18,plain,
    ( spl29_17
    | spl29_18 ),
    inference(sat_conversion,[],[f3927]) ).

cnf(s20,plain,
    ( spl29_17
    | ~ spl29_20 ),
    inference(sat_conversion,[],[f3942]) ).

cnf(s21,plain,
    ( spl29_20
    | ~ spl29_21 ),
    inference(sat_conversion,[],[f3994]) ).

cnf(s22,plain,
    ( spl29_20
    | spl29_21
    | ~ spl29_22
    | ~ spl29_23 ),
    inference(sat_conversion,[],[f4075]) ).

cnf(s25,plain,
    ( spl29_20
    | spl29_21
    | ~ spl29_28
    | ~ spl29_29 ),
    inference(sat_conversion,[],[f4151]) ).

cnf(s26,plain,
    ( spl29_17
    | spl29_22
    | spl29_30 ),
    inference(sat_conversion,[],[f4297]) ).

cnf(s33,plain,
    ( ~ spl29_18
    | ~ spl29_30
    | ~ spl29_35 ),
    inference(sat_conversion,[],[f4551]) ).

cnf(s42,plain,
    ( spl29_20
    | spl29_44 ),
    inference(sat_conversion,[],[f5099]) ).

cnf(s43,plain,
    ( ~ spl29_44
    | spl29_45 ),
    inference(sat_conversion,[],[f5147]) ).

cnf(s68,plain,
    ( ~ spl29_11
    | spl29_28
    | ~ spl29_67 ),
    inference(sat_conversion,[],[f6370]) ).

cnf(s82,plain,
    ( ~ spl29_5
    | spl29_43
    | spl29_80 ),
    inference(sat_conversion,[],[f7656]) ).

cnf(s83,plain,
    ( spl29_29
    | ~ spl29_45
    | ~ spl29_81 ),
    inference(sat_conversion,[],[f7715]) ).

cnf(s84,plain,
    ( spl29_23
    | spl29_81 ),
    inference(sat_conversion,[],[f7768]) ).

cnf(s86,plain,
    ( ~ spl29_43
    | spl29_67 ),
    inference(sat_conversion,[],[f8020]) ).

cnf(s99,plain,
    ( spl29_35
    | ~ spl29_87 ),
    inference(sat_conversion,[],[f8613]) ).

cnf(s105,plain,
    ( ~ spl29_2
    | ~ spl29_80
    | ~ spl29_93 ),
    inference(sat_conversion,[],[f8803]) ).

cnf(s410,plain,
    ( spl29_17
    | ~ spl29_18
    | spl29_112 ),
    inference(sat_conversion,[],[f12782]) ).

cnf(s420,plain,
    ( ~ spl29_12
    | spl29_87
    | ~ spl29_121 ),
    inference(sat_conversion,[],[f13076]) ).

cnf(s1448,plain,
    ( ~ spl29_12
    | spl29_93
    | ~ spl29_112 ),
    inference(sat_conversion,[],[f19525]) ).

cnf(s1520,plain,
    ( ~ spl29_4
    | spl29_220 ),
    inference(sat_conversion,[],[f20075]) ).

cnf(s5606,plain,
    ( ~ spl29_11
    | spl29_2388 ),
    inference(sat_conversion,[],[f84332]) ).

cnf(s5607,plain,
    ( spl29_121
    | ~ spl29_220
    | ~ spl29_2388 ),
    inference(sat_conversion,[],[f84343]) ).

cnf(s5735,plain,
    spl29_5,
    inference(rat,[],[s5,s1]) ).

cnf(s5736,plain,
    ~ spl29_3,
    inference(rat,[],[s3,s1]) ).

cnf(s5737,plain,
    spl29_2,
    inference(rat,[],[s2,s1]) ).

cnf(s5768,plain,
    ~ spl29_6,
    inference(rat,[],[s6,s5736]) ).

cnf(s5770,plain,
    spl29_4,
    inference(rat,[],[s4,s1,s5737]) ).

cnf(s5805,plain,
    ~ spl29_8,
    inference(rat,[],[s8,s5768]) ).

cnf(s5806,plain,
    spl29_7,
    inference(rat,[],[s7,s5768]) ).

cnf(s5883,plain,
    spl29_220,
    inference(rat,[],[s1520,s5770]) ).

cnf(s5965,plain,
    ~ spl29_9,
    inference(rat,[],[s9,s5805]) ).

cnf(s5967,plain,
    spl29_11,
    inference(rat,[],[s11,s5768,s5806]) ).

cnf(s6050,plain,
    ~ spl29_16,
    inference(rat,[],[s16,s5965]) ).

cnf(s6052,plain,
    spl29_10,
    inference(rat,[],[s10,s5965]) ).

cnf(s6053,plain,
    spl29_2388,
    inference(rat,[],[s5606,s5967]) ).

cnf(s6331,plain,
    ~ spl29_17,
    inference(rat,[],[s17,s6050]) ).

cnf(s6339,plain,
    spl29_12,
    inference(rat,[],[s12,s5965,s6052]) ).

cnf(s6340,plain,
    spl29_121,
    inference(rat,[],[s5607,s5883,s6053]) ).

cnf(s6516,plain,
    ~ spl29_20,
    inference(rat,[],[s20,s6331]) ).

cnf(s6517,plain,
    spl29_18,
    inference(rat,[],[s18,s6331]) ).

cnf(s6622,plain,
    spl29_87,
    inference(rat,[],[s420,s6340,s6339]) ).

cnf(s6724,plain,
    spl29_44,
    inference(rat,[],[s42,s6516]) ).

cnf(s6725,plain,
    ~ spl29_21,
    inference(rat,[],[s21,s6516]) ).

cnf(s6727,plain,
    spl29_112,
    inference(rat,[],[s410,s6331,s6517]) ).

cnf(s6795,plain,
    spl29_35,
    inference(rat,[],[s99,s6622]) ).

cnf(s6830,plain,
    spl29_45,
    inference(rat,[],[s43,s6724]) ).

cnf(s6867,plain,
    spl29_93,
    inference(rat,[],[s1448,s6339,s6727]) ).

cnf(s6931,plain,
    ~ spl29_30,
    inference(rat,[],[s33,s6517,s6795]) ).

cnf(s6960,plain,
    ~ spl29_80,
    inference(rat,[],[s105,s5737,s6867]) ).

cnf(s6963,plain,
    spl29_22,
    inference(rat,[],[s26,s6331,s6931]) ).

cnf(s7021,plain,
    spl29_43,
    inference(rat,[],[s82,s5735,s6960]) ).

cnf(s7024,plain,
    ~ spl29_23,
    inference(rat,[],[s22,s6725,s6516,s6963]) ).

cnf(s7053,plain,
    spl29_67,
    inference(rat,[],[s86,s7021]) ).

cnf(s7058,plain,
    spl29_81,
    inference(rat,[],[s84,s7024]) ).

cnf(s7078,plain,
    spl29_28,
    inference(rat,[],[s68,s5967,s7053]) ).

cnf(s7082,plain,
    spl29_29,
    inference(rat,[],[s83,s6830,s7058]) ).

cnf(s7110,plain,
    $false,
    inference(rat,[],[s25,s6725,s6516,s7082,s7078]) ).

fof(f84344,plain,
    $false,
    inference(avatar_sat_refutation,[],[s7110]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NUM688+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39  % Computer : n014.cluster.edu
% 0.12/0.39  % Model    : x86_64 x86_64
% 0.12/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39  % Memory   : 8046.5625MB
% 0.12/0.39  % OS       : Linux 6.8.0-71-generic
% 0.12/0.39  % CPULimit : 300
% 0.12/0.39  % WCLimit  : 300
% 0.12/0.39  % DateTime : Sun Sep 27 21:05:47 UTC 2026
% 0.12/0.39  % CPUTime  : 
% 0.12/0.39  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43  Running first-order theorem proving
% 0.12/0.43  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.84/2.46  % (1164797)Detected formulas, will run a generic FOF schedule.
% 10.84/2.46  % (1164804)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2367766444:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.84/2.46  % (1164806)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1483708429:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.84/2.46  % (1164806)Refutation not found, incomplete strategy
% 10.84/2.46  % (1164806)------------------------------
% 10.84/2.46  % (1164806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.46  % (1164806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.46  % (1164806)CaDiCaL version: 2.1.3
% 10.84/2.46  % (1164806)Termination reason: Refutation not found, incomplete strategy
% 10.84/2.46  % (1164806)Time elapsed: 0.003 s
% 10.84/2.46  % (1164806)Peak memory usage: 88 MB
% 10.84/2.46  % (1164806)Instructions burned: 3 (million)
% 10.84/2.46  % (1164805)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2420824228:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.84/2.46  % (1164802)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2893162640:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.84/2.46  % (1164803)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4233074753:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.84/2.46  % (1164805)Refutation not found, incomplete strategy
% 10.84/2.46  % (1164805)------------------------------
% 10.84/2.46  % (1164805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.46  % (1164805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.46  % (1164805)CaDiCaL version: 2.1.3
% 10.84/2.46  % (1164805)Termination reason: Refutation not found, incomplete strategy
% 10.84/2.46  % (1164805)Time elapsed: 0.002 s
% 10.84/2.46  % (1164805)Peak memory usage: 88 MB
% 10.84/2.46  % (1164805)Instructions burned: 2 (million)
% 10.84/2.46  % (1164807)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=237749074:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.84/2.46  % (1164808)dis-21_1_sil=8000:lcm=predicate:random_seed=2401432157:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.84/2.46  % (1164808)Instruction limit reached! 
% 10.84/2.46  % (1164808)------------------------------
% 10.84/2.46  % (1164808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.46  % (1164808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.46  % (1164808)CaDiCaL version: 2.1.3
% 10.84/2.46  % (1164808)Termination reason: Instruction limit
% 10.84/2.46  % (1164808)Termination phase: Saturation
% 10.84/2.46  % (1164808)Time elapsed: 0.071 s
% 10.84/2.46  % (1164808)Peak memory usage: 90 MB
% 10.84/2.46  % (1164808)Instructions burned: 129 (million)
% 10.84/2.46  % (1164807)Instruction limit reached! 
% 10.84/2.46  % (1164807)------------------------------
% 10.84/2.46  % (1164807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.46  % (1164807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.46  % (1164807)CaDiCaL version: 2.1.3
% 10.84/2.46  % (1164807)Termination reason: Instruction limit
% 10.84/2.46  % (1164807)Termination phase: Saturation
% 10.84/2.46  % (1164807)Time elapsed: 0.080 s
% 10.84/2.46  % (1164807)Peak memory usage: 90 MB
% 10.84/2.46  % (1164807)Instructions burned: 139 (million)
% 10.84/2.46  % (1164816)lrs+10_1_sil=8000:sp=occurrence:random_seed=3113703695:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.84/2.46  % (1164816)Refutation not found, incomplete strategy
% 10.84/2.46  % (1164816)------------------------------
% 10.84/2.46  % (1164816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.46  % (1164816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.46  % (1164816)CaDiCaL version: 2.1.3
% 10.84/2.46  % (1164816)Termination reason: Refutation not found, incomplete strategy
% 10.84/2.46  % (1164816)Time elapsed: 0.003 s
% 10.84/2.46  % (1164816)Peak memory usage: 88 MB
% 10.84/2.46  % (1164816)Instructions burned: 2 (million)
% 10.84/2.46  % (1164817)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3669822409:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 19.19/3.60  % (1164806)------------------------------
% 19.19/3.60  % (1164806)------------------------------
% 19.19/3.60  % (1164817)Refutation not found, incomplete strategy
% 19.19/3.60  % (1164817)------------------------------
% 19.19/3.60  % (1164817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.19/3.60  % (1164817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.19/3.60  % (1164817)CaDiCaL version: 2.1.3
% 19.19/3.60  % (1164817)Termination reason: Refutation not found, incomplete strategy
% 19.19/3.60  % (1164817)Time elapsed: 0.005 s
% 19.19/3.60  % (1164817)Peak memory usage: 88 MB
% 19.19/3.60  % (1164817)Instructions burned: 9 (million)
% 19.19/3.60  % (1164805)------------------------------
% 19.19/3.60  % (1164805)------------------------------
% 19.19/3.60  % (1164820)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3897429759:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 19.19/3.60  % (1164820)Refutation not found, incomplete strategy
% 19.19/3.60  % (1164820)------------------------------
% 19.19/3.60  % (1164820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.19/3.60  % (1164820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.19/3.60  % (1164820)CaDiCaL version: 2.1.3
% 19.19/3.60  % (1164820)Termination reason: Refutation not found, incomplete strategy
% 19.19/3.60  % (1164820)Time elapsed: 0.005 s
% 19.19/3.60  % (1164820)Peak memory usage: 89 MB
% 19.19/3.60  % (1164820)Instructions burned: 5 (million)
% 19.19/3.60  % (1164821)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1135668413:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.19/3.60  % (1164816)------------------------------
% 19.19/3.60  % (1164816)------------------------------
% 19.19/3.60  % (1164817)------------------------------
% 19.19/3.60  % (1164817)------------------------------
% 19.19/3.60  % (1164821)Instruction limit reached! 
% 19.19/3.60  % (1164821)------------------------------
% 19.19/3.60  % (1164821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.19/3.60  % (1164821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.19/3.60  % (1164821)CaDiCaL version: 2.1.3
% 19.19/3.60  % (1164821)Termination reason: Instruction limit
% 19.19/3.60  % (1164821)Termination phase: Saturation
% 19.19/3.60  % (1164821)Time elapsed: 0.123 s
% 19.19/3.60  % (1164821)Peak memory usage: 95 MB
% 19.19/3.60  % (1164821)Instructions burned: 249 (million)
% 19.19/3.60  % (1164825)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3783490015:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 19.19/3.60  % (1164824)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3462333517:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 19.19/3.60  % (1164820)------------------------------
% 19.19/3.60  % (1164820)------------------------------
% 19.19/3.60  % (1164824)Refutation not found, incomplete strategy
% 19.19/3.60  % (1164824)------------------------------
% 19.19/3.60  % (1164824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.19/3.60  % (1164824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.19/3.60  % (1164824)CaDiCaL version: 2.1.3
% 19.19/3.60  % (1164824)Termination reason: Refutation not found, incomplete strategy
% 19.19/3.60  % (1164824)Time elapsed: 0.005 s
% 19.19/3.60  % (1164824)Peak memory usage: 89 MB
% 19.19/3.60  % (1164824)Instructions burned: 6 (million)
% 19.19/3.60  % (1164826)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2509401360:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 19.19/3.60  % (1164826)Instruction limit reached! 
% 19.19/3.60  % (1164826)------------------------------
% 19.19/3.60  % (1164826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.19/3.60  % (1164826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.19/3.60  % (1164826)CaDiCaL version: 2.1.3
% 19.19/3.60  % (1164826)Termination reason: Instruction limit
% 19.19/3.60  % (1164826)Termination phase: Saturation
% 19.19/3.60  % (1164826)Time elapsed: 0.059 s
% 19.19/3.60  % (1164826)Peak memory usage: 91 MB
% 19.19/3.60  % (1164826)Instructions burned: 113 (million)
% 19.19/3.60  % (1164829)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1226772594:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 35.83/5.96  % (1164829)Instruction limit reached! 
% 35.83/5.96  % (1164829)------------------------------
% 35.83/5.96  % (1164829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/5.96  % (1164829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/5.96  % (1164829)CaDiCaL version: 2.1.3
% 35.83/5.96  % (1164829)Termination reason: Instruction limit
% 35.83/5.96  % (1164829)Termination phase: Saturation
% 35.83/5.96  % (1164829)Time elapsed: 0.060 s
% 35.83/5.96  % (1164829)Peak memory usage: 89 MB
% 35.83/5.96  % (1164829)Instructions burned: 129 (million)
% 35.83/5.96  % (1164831)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2665327485:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 35.83/5.96  % (1164824)------------------------------
% 35.83/5.96  % (1164824)------------------------------
% 35.83/5.96  % (1164831)Instruction limit reached! 
% 35.83/5.96  % (1164831)------------------------------
% 35.83/5.96  % (1164831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/5.96  % (1164831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/5.96  % (1164831)CaDiCaL version: 2.1.3
% 35.83/5.96  % (1164831)Termination reason: Instruction limit
% 35.83/5.96  % (1164831)Termination phase: Saturation
% 35.83/5.96  % (1164831)Time elapsed: 0.062 s
% 35.83/5.96  % (1164831)Peak memory usage: 90 MB
% 35.83/5.96  % (1164831)Instructions burned: 115 (million)
% 35.83/5.96  % (1164833)lrs+10_1_sil=8000:sp=occurrence:random_seed=148590046:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 35.83/5.96  % (1164833)Refutation not found, incomplete strategy
% 35.83/5.96  % (1164833)------------------------------
% 35.83/5.96  % (1164833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/5.96  % (1164833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/5.96  % (1164833)CaDiCaL version: 2.1.3
% 35.83/5.96  % (1164833)Termination reason: Refutation not found, incomplete strategy
% 35.83/5.96  % (1164833)Time elapsed: 0.003 s
% 35.83/5.96  % (1164833)Peak memory usage: 88 MB
% 35.83/5.96  % (1164833)Instructions burned: 3 (million)
% 35.83/5.96  % (1164835)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2945635129:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 35.83/5.96  % (1164835)Refutation not found, incomplete strategy
% 35.83/5.96  % (1164835)------------------------------
% 35.83/5.96  % (1164835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/5.96  % (1164835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/5.96  % (1164835)CaDiCaL version: 2.1.3
% 35.83/5.96  % (1164835)Termination reason: Refutation not found, incomplete strategy
% 35.83/5.96  % (1164835)Time elapsed: 0.040 s
% 35.83/5.96  % (1164835)Peak memory usage: 90 MB
% 35.83/5.96  % (1164835)Instructions burned: 77 (million)
% 35.83/5.96  % (1164836)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1415071776:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 35.83/5.96  % (1164833)------------------------------
% 35.83/5.96  % (1164833)------------------------------
% 35.83/5.96  % (1164835)------------------------------
% 35.83/5.96  % (1164835)------------------------------
% 35.83/5.96  % (1164840)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2537577373:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 35.83/5.96  % (1164840)Instruction limit reached! 
% 35.83/5.96  % (1164840)------------------------------
% 35.83/5.96  % (1164840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/5.96  % (1164840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.83/5.96  % (1164840)CaDiCaL version: 2.1.3
% 35.83/5.96  % (1164840)Termination reason: Instruction limit
% 35.83/5.96  % (1164840)Termination phase: Saturation
% 35.83/5.96  % (1164840)Time elapsed: 0.071 s
% 35.83/5.96  % (1164840)Peak memory usage: 94 MB
% 35.83/5.96  % (1164840)Instructions burned: 136 (million)
% 35.83/5.96  % (1164841)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1028554206:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 35.83/5.96  % (1164841)Refutation not found, incomplete strategy
% 35.83/5.96  % (1164841)------------------------------
% 35.83/5.96  % (1164841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.83/5.96  % (1164841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.69/9.91  % (1164841)CaDiCaL version: 2.1.3
% 63.69/9.91  % (1164841)Termination reason: Refutation not found, incomplete strategy
% 63.69/9.91  % (1164841)Time elapsed: 0.015 s
% 63.69/9.91  % (1164841)Peak memory usage: 89 MB
% 63.69/9.91  % (1164841)Instructions burned: 28 (million)
% 63.69/9.91  % (1164843)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1873183293:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 63.69/9.91  % (1164841)------------------------------
% 63.69/9.91  % (1164841)------------------------------
% 63.69/9.91  % (1164846)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=4168565930:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 63.69/9.91  % (1164846)Refutation not found, incomplete strategy
% 63.69/9.91  % (1164846)------------------------------
% 63.69/9.91  % (1164846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.69/9.91  % (1164846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.69/9.91  % (1164846)CaDiCaL version: 2.1.3
% 63.69/9.91  % (1164846)Termination reason: Refutation not found, incomplete strategy
% 63.69/9.91  % (1164846)Time elapsed: 0.007 s
% 63.69/9.91  % (1164846)Peak memory usage: 89 MB
% 63.69/9.91  % (1164846)Instructions burned: 11 (million)
% 63.69/9.91  % (1164846)------------------------------
% 63.69/9.91  % (1164846)------------------------------
% 63.69/9.91  % (1164848)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1805198517:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 63.69/9.91  % (1164825)Instruction limit reached! 
% 63.69/9.91  % (1164825)------------------------------
% 63.69/9.91  % (1164825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.69/9.91  % (1164825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.69/9.91  % (1164825)CaDiCaL version: 2.1.3
% 63.69/9.91  % (1164825)Termination reason: Instruction limit
% 63.69/9.91  % (1164825)Termination phase: Saturation
% 63.69/9.91  % (1164825)Time elapsed: 1.578 s
% 63.69/9.91  % (1164825)Peak memory usage: 144 MB
% 63.69/9.91  % (1164825)Instructions burned: 2350 (million)
% 63.69/9.91  % (1164848)Instruction limit reached! 
% 63.69/9.91  % (1164848)------------------------------
% 63.69/9.91  % (1164848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.69/9.91  % (1164848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.69/9.91  % (1164848)CaDiCaL version: 2.1.3
% 63.69/9.91  % (1164848)Termination reason: Instruction limit
% 63.69/9.91  % (1164848)Termination phase: Saturation
% 63.69/9.91  % (1164848)Time elapsed: 0.064 s
% 63.69/9.91  % (1164848)Peak memory usage: 92 MB
% 63.69/9.91  % (1164848)Instructions burned: 134 (million)
% 63.69/9.91  % (1164850)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2440867295:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 63.69/9.91  % (1164850)Refutation not found, incomplete strategy
% 63.69/9.91  % (1164850)------------------------------
% 63.69/9.91  % (1164850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.69/9.91  % (1164850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.69/9.91  % (1164850)CaDiCaL version: 2.1.3
% 63.69/9.91  % (1164850)Termination reason: Refutation not found, incomplete strategy
% 63.69/9.91  % (1164850)Time elapsed: 0.003 s
% 63.69/9.91  % (1164850)Peak memory usage: 89 MB
% 63.69/9.91  % (1164850)Instructions burned: 2 (million)
% 63.69/9.91  % (1164851)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=377659265:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 63.69/9.91  % (1164851)Refutation not found, incomplete strategy
% 63.69/9.91  % (1164851)------------------------------
% 63.69/9.91  % (1164851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.69/9.91  % (1164851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.69/9.91  % (1164851)CaDiCaL version: 2.1.3
% 63.69/9.91  % (1164851)Termination reason: Refutation not found, incomplete strategy
% 63.69/9.91  % (1164851)Time elapsed: 0.003 s
% 63.69/9.91  % (1164851)Peak memory usage: 89 MB
% 63.69/9.91  % (1164851)Instructions burned: 2 (million)
% 63.69/9.91  % (1164851)------------------------------
% 63.69/9.91  % (1164851)------------------------------
% 63.69/9.91  % (1164850)------------------------------
% 63.69/9.91  % (1164850)------------------------------
% 64.92/11.55  % (1164854)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2803642616:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 64.92/11.55  % (1164855)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=522665750:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 64.92/11.55  % (1164855)Instruction limit reached! 
% 64.92/11.55  % (1164855)------------------------------
% 64.92/11.55  % (1164855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164855)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164855)Termination reason: Instruction limit
% 64.92/11.55  % (1164855)Termination phase: Saturation
% 64.92/11.55  % (1164855)Time elapsed: 0.080 s
% 64.92/11.55  % (1164855)Peak memory usage: 91 MB
% 64.92/11.55  % (1164855)Instructions burned: 151 (million)
% 64.92/11.55  % (1164858)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1127324078:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 64.92/11.55  % (1164836)Instruction limit reached! 
% 64.92/11.55  % (1164836)------------------------------
% 64.92/11.55  % (1164836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164836)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164836)Termination reason: Instruction limit
% 64.92/11.55  % (1164836)Termination phase: Saturation
% 64.92/11.55  % (1164836)Time elapsed: 3.323 s
% 64.92/11.55  % (1164836)Peak memory usage: 161 MB
% 64.92/11.55  % (1164836)Instructions burned: 5203 (million)
% 64.92/11.55  % (1164860)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1726231167:i=667:av=off:fsr=off_2954 on theBenchmark for (2954ds/667Mi)
% 64.92/11.55  % (1164854)Instruction limit reached! 
% 64.92/11.55  % (1164854)------------------------------
% 64.92/11.55  % (1164854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164854)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164854)Termination reason: Instruction limit
% 64.92/11.55  % (1164854)Termination phase: Saturation
% 64.92/11.55  % (1164854)Time elapsed: 2.068 s
% 64.92/11.55  % (1164854)Peak memory usage: 177 MB
% 64.92/11.55  % (1164854)Instructions burned: 6064 (million)
% 64.92/11.55  % (1164862)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=888830697:s2a=on:i=185:s2at=1.8:fdi=4_2951 on theBenchmark for (2951ds/185Mi)
% 64.92/11.55  % (1164862)Instruction limit reached! 
% 64.92/11.55  % (1164862)------------------------------
% 64.92/11.55  % (1164862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164862)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164862)Termination reason: Instruction limit
% 64.92/11.55  % (1164862)Termination phase: Saturation
% 64.92/11.55  % (1164862)Time elapsed: 0.044 s
% 64.92/11.55  % (1164862)Peak memory usage: 91 MB
% 64.92/11.55  % (1164862)Instructions burned: 187 (million)
% 64.92/11.55  % (1164860)Instruction limit reached! 
% 64.92/11.55  % (1164860)------------------------------
% 64.92/11.55  % (1164860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164860)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164860)Termination reason: Instruction limit
% 64.92/11.55  % (1164860)Termination phase: Saturation
% 64.92/11.55  % (1164860)Time elapsed: 0.324 s
% 64.92/11.55  % (1164860)Peak memory usage: 100 MB
% 64.92/11.55  % (1164860)Instructions burned: 667 (million)
% 64.92/11.55  % (1164864)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4242558036:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 64.92/11.55  % (1164864)Refutation not found, incomplete strategy
% 64.92/11.55  % (1164864)------------------------------
% 64.92/11.55  % (1164864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164864)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164864)Termination reason: Refutation not found, incomplete strategy
% 64.92/11.55  % (1164864)Time elapsed: 0.003 s
% 64.92/11.55  % (1164864)Peak memory usage: 89 MB
% 64.92/11.55  % (1164864)Instructions burned: 5 (million)
% 64.92/11.55  % (1164865)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2441740649:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2950 on theBenchmark for (2950ds/4850Mi)
% 64.92/11.55  % (1164864)------------------------------
% 64.92/11.55  % (1164864)------------------------------
% 64.92/11.55  % (1164868)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=956572492:i=12111:sd=1:ss=included_2947 on theBenchmark for (2947ds/12111Mi)
% 64.92/11.55  % (1164865)Instruction limit reached! 
% 64.92/11.55  % (1164865)------------------------------
% 64.92/11.55  % (1164865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164865)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164865)Termination reason: Instruction limit
% 64.92/11.55  % (1164865)Termination phase: Saturation
% 64.92/11.55  % (1164865)Time elapsed: 3.097 s
% 64.92/11.55  % (1164865)Peak memory usage: 152 MB
% 64.92/11.55  % (1164865)Instructions burned: 4850 (million)
% 64.92/11.55  % (1164870)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=442903047:i=319:kws=precedence:fsr=off_2917 on theBenchmark for (2917ds/319Mi)
% 64.92/11.55  % (1164843)Instruction limit reached! 
% 64.92/11.55  % (1164843)------------------------------
% 64.92/11.55  % (1164843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164843)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164843)Termination reason: Instruction limit
% 64.92/11.55  % (1164843)Termination phase: Saturation
% 64.92/11.55  % (1164843)Time elapsed: 6.825 s
% 64.92/11.55  % (1164843)Peak memory usage: 190 MB
% 64.92/11.55  % (1164843)Instructions burned: 13194 (million)
% 64.92/11.55  % (1164870)Instruction limit reached! 
% 64.92/11.55  % (1164870)------------------------------
% 64.92/11.55  % (1164870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164870)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164870)Termination reason: Instruction limit
% 64.92/11.55  % (1164870)Termination phase: Saturation
% 64.92/11.55  % (1164870)Time elapsed: 0.167 s
% 64.92/11.55  % (1164870)Peak memory usage: 93 MB
% 64.92/11.55  % (1164870)Instructions burned: 320 (million)
% 64.92/11.55  % (1164872)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1581355896:i=2064:ep=RST_2914 on theBenchmark for (2914ds/2064Mi)
% 64.92/11.55  % (1164873)dis-1011_128_sil=32000:random_seed=3731648381:i=3706:ep=RST:av=off_2914 on theBenchmark for (2914ds/3706Mi)
% 64.92/11.55  % (1164872)Refutation not found, incomplete strategy
% 64.92/11.55  % (1164872)------------------------------
% 64.92/11.55  % (1164872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164872)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164872)Termination reason: Refutation not found, incomplete strategy
% 64.92/11.55  % (1164872)Time elapsed: 0.032 s
% 64.92/11.55  % (1164872)Peak memory usage: 90 MB
% 64.92/11.55  % (1164872)Instructions burned: 67 (million)
% 64.92/11.55  % (1164872)------------------------------
% 64.92/11.55  % (1164872)------------------------------
% 64.92/11.55  % (1164876)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1355770399:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2910 on theBenchmark for (2910ds/757Mi)
% 64.92/11.55  % (1164868)Instruction limit reached! 
% 64.92/11.55  % (1164868)------------------------------
% 64.92/11.55  % (1164868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164868)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164868)Termination reason: Instruction limit
% 64.92/11.55  % (1164868)Termination phase: Saturation
% 64.92/11.55  % (1164868)Time elapsed: 3.711 s
% 64.92/11.55  % (1164868)Peak memory usage: 299 MB
% 64.92/11.55  % (1164868)Instructions burned: 12113 (million)
% 64.92/11.55  % (1164876)Refutation not found, incomplete strategy
% 64.92/11.55  % (1164876)------------------------------
% 64.92/11.55  % (1164876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164876)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164876)Termination reason: Refutation not found, incomplete strategy
% 64.92/11.55  % (1164876)Time elapsed: 0.006 s
% 64.92/11.55  % (1164876)Peak memory usage: 89 MB
% 64.92/11.55  % (1164876)Instructions burned: 9 (million)
% 64.92/11.55  % (1164878)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1154598687:i=13913:ss=axioms:sgt=8_2909 on theBenchmark for (2909ds/13913Mi)
% 64.92/11.55  % (1164876)------------------------------
% 64.92/11.55  % (1164876)------------------------------
% 64.92/11.55  % (1164880)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=429825530:i=9925:aac=none_2907 on theBenchmark for (2907ds/9925Mi)
% 64.92/11.55  % (1164878)Refutation not found, incomplete strategy
% 64.92/11.55  % (1164878)------------------------------
% 64.92/11.55  % (1164878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164878)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164878)Termination reason: Refutation not found, incomplete strategy
% 64.92/11.55  % (1164878)Time elapsed: 0.321 s
% 64.92/11.55  % (1164878)Peak memory usage: 129 MB
% 64.92/11.55  % (1164878)Instructions burned: 870 (million)
% 64.92/11.55  % (1164878)------------------------------
% 64.92/11.55  % (1164878)------------------------------
% 64.92/11.55  % (1164882)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3043735399:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2903 on theBenchmark for (2903ds/2479Mi)
% 64.92/11.55  % (1164882)Refutation not found, incomplete strategy
% 64.92/11.55  % (1164882)------------------------------
% 64.92/11.55  % (1164882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164882)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164882)Termination reason: Refutation not found, incomplete strategy
% 64.92/11.55  % (1164882)Time elapsed: 0.002 s
% 64.92/11.55  % (1164882)Peak memory usage: 88 MB
% 64.92/11.55  % (1164882)Instructions burned: 4 (million)
% 64.92/11.55  % (1164882)------------------------------
% 64.92/11.55  % (1164882)------------------------------
% 64.92/11.55  % (1164884)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=393640250:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2901 on theBenchmark for (2901ds/440Mi)
% 64.92/11.55  % (1164884)Instruction limit reached! 
% 64.92/11.55  % (1164884)------------------------------
% 64.92/11.55  % (1164884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164884)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164884)Termination reason: Instruction limit
% 64.92/11.55  % (1164884)Termination phase: Saturation
% 64.92/11.55  % (1164884)Time elapsed: 0.095 s
% 64.92/11.55  % (1164884)Peak memory usage: 91 MB
% 64.92/11.55  % (1164884)Instructions burned: 442 (million)
% 64.92/11.55  % (1164886)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2831038805:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2899 on theBenchmark for (2899ds/11145Mi)
% 64.92/11.55  % (1164804)First to succeed.
% 64.92/11.55  % (1164804)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1164797"
% 64.92/11.55  % (1164886)Refutation not found, incomplete strategy
% 64.92/11.55  % (1164886)------------------------------
% 64.92/11.55  % (1164886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.92/11.55  % (1164886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.92/11.55  % (1164886)CaDiCaL version: 2.1.3
% 64.92/11.55  % (1164886)Termination reason: Refutation not found, incomplete strategy
% 64.92/11.55  % (1164886)Time elapsed: 0.372 s
% 64.92/11.55  % (1164886)Peak memory usage: 130 MB
% 64.92/11.55  % (1164886)Instructions burned: 917 (million)
% 64.92/11.55  % (1164804)Refutation found. Thanks to Tanya!
% 64.92/11.55  % SZS status Theorem for theBenchmark
% 64.92/11.55  % SZS output start Proof for theBenchmark
% See solution above
% 76.14/11.74  % (1164804)------------------------------
% 76.14/11.74  % (1164804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.14/11.74  % (1164804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.14/11.74  % (1164804)CaDiCaL version: 2.1.3
% 76.14/11.74  % (1164804)Termination reason: Refutation
% 76.14/11.74  % (1164804)Time elapsed: 10.246 s
% 76.14/11.74  % (1164804)Peak memory usage: 259 MB
% 76.14/11.74  % (1164804)Instructions burned: 18613 (million)
% 76.14/11.74  % (1164804)------------------------------
% 76.14/11.74  % (1164804)------------------------------
% 76.14/11.74  % (1164797)Success in time 10.684 s
% 76.14/11.74  % Vampire exiting
%------------------------------------------------------------------------------