Vampire---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : NUM743+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 : n005.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:46 PM UTC 2026

% Result   : Theorem 89.86s 13.88s
% Output   : Refutation 90.76s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   22
%            Number of leaves      :   68
% Syntax   : Number of formulae    :  365 (  62 unt;  40 def)
%            Number of atoms       :  972 (   5 equ)
%            Maximal formula atoms :   10 (   2 avg)
%            Number of connectives : 1072 ( 465   ~; 479   |;  49   &)
%                                         (  68 <=>;  11  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   11 (   4 avg)
%            Maximal term depth    :   10 (   2 avg)
%            Number of predicates  :   45 (  43 usr;  41 prp; 0-2 aty)
%            Number of functors    :   33 (  33 usr;  19 con; 0-2 aty)
%            Number of variables   :  240 (   0 sgn 238   !;   2   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f31,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X0),X1))
    <=> pp(aa_bool_bool(scratc1229951240d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__lesseq) ).

fof(f161,axiom,
    ! [X0] : scratc1229951240d_l_or(X0) = aa_boo1142376798l_bool(scratc218488005nd_imp,scratc1773705014_d_not(X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__l__or) ).

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

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

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

fof(f201,axiom,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_cd)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz50) ).

fof(f215,axiom,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dn)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz44) ).

fof(f216,axiom,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dp)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz43) ).

fof(f217,axiom,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dr)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz42) ).

fof(f227,axiom,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_eo)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz37) ).

fof(f440,axiom,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_eo,X0))
    <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X0)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__21) ).

fof(f559,axiom,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_dr,X0))
    <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dq,X0))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__140) ).

fof(f560,axiom,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_dp,X0))
    <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do,X0))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__141) ).

fof(f561,axiom,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_dn,X0))
    <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,X0))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__142) ).

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

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

fof(f621,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,X0),X1))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1))
       => pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X0)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__202) ).

fof(f622,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,X0),X1))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
       => pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),X0)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__203) ).

fof(f724,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm,X0),X1))
    <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(X0),X1))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__305) ).

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

fof(f730,axiom,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
    <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__311) ).

fof(f778,axiom,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
       => ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X1),X2))
         => pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2)) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__359) ).

fof(f779,axiom,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
       => ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X2))
         => pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2)) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__360) ).

fof(f830,axiom,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dl(X0),X1),X2))
    <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__411) ).

fof(f862,axiom,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1))
       => ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X2))
         => ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X3))
           => pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X2),X3)) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__443) ).

fof(f899,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(f901,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(f908,conjecture,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_ac)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

fof(f909,negated_conjecture,
    ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_ac)),
    inference(negated_conjecture,[status(cth)],[f908]) ).

fof(f910,plain,
    ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_ac)),
    inference(flattening,[],[f909]) ).

fof(f927,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1))
    <=> ! [X2] :
          ( pp(aa_TPTP_ind_bool(X1,X2))
          | ~ scratc531300584_is_of(X2,X0)
          | ~ gg_TPTP_ind(X2) ) ),
    inference(ennf_transformation,[],[f198]) ).

fof(f928,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1))
    <=> ! [X2] :
          ( pp(aa_TPTP_ind_bool(X1,X2))
          | ~ scratc531300584_is_of(X2,X0)
          | ~ gg_TPTP_ind(X2) ) ),
    inference(flattening,[],[f927]) ).

fof(f1006,plain,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,X0),X1))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1)) ) ),
    inference(ennf_transformation,[],[f621]) ).

fof(f1007,plain,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,X0),X1))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) ),
    inference(ennf_transformation,[],[f622]) ).

fof(f1062,plain,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X1),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) ),
    inference(ennf_transformation,[],[f778]) ).

fof(f1063,plain,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X1),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) ),
    inference(flattening,[],[f1062]) ).

fof(f1064,plain,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) ),
    inference(ennf_transformation,[],[f779]) ).

fof(f1065,plain,
    ! [X0,X1,X2] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) ),
    inference(flattening,[],[f1064]) ).

fof(f1116,plain,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1)) ) ),
    inference(ennf_transformation,[],[f862]) ).

fof(f1117,plain,
    ! [X0,X1,X2,X3] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2),X3))
    <=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1)) ) ),
    inference(flattening,[],[f1116]) ).

fof(f1157,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X0),X1))
        | ~ pp(aa_bool_bool(scratc1229951240d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))) )
      & ( pp(aa_bool_bool(scratc1229951240d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X0),X1)) ) ),
    inference(nnf_transformation,[],[f31]) ).

fof(f1215,plain,
    ! [X0] :
      ( ( pp(scratc1773705014_d_not(X0))
        | ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc218488005nd_imp,X0),fFalse)) )
      & ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc218488005nd_imp,X0),fFalse))
        | ~ pp(scratc1773705014_d_not(X0)) ) ),
    inference(nnf_transformation,[],[f166]) ).

fof(f1238,plain,
    ! [X0,X1] :
      ( ( pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1))
        | ? [X2] :
            ( ~ pp(aa_TPTP_ind_bool(X1,X2))
            & scratc531300584_is_of(X2,X0)
            & gg_TPTP_ind(X2) ) )
      & ( ! [X2] :
            ( pp(aa_TPTP_ind_bool(X1,X2))
            | ~ scratc531300584_is_of(X2,X0)
            | ~ gg_TPTP_ind(X2) )
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1)) ) ),
    inference(nnf_transformation,[],[f928]) ).

fof(f1239,plain,
    ! [X0,X1] :
      ( ( pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1))
        | ? [X2] :
            ( ~ pp(aa_TPTP_ind_bool(X1,X2))
            & scratc531300584_is_of(X2,X0)
            & gg_TPTP_ind(X2) ) )
      & ( ! [X3] :
            ( pp(aa_TPTP_ind_bool(X1,X3))
            | ~ scratc531300584_is_of(X3,X0)
            | ~ gg_TPTP_ind(X3) )
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1)) ) ),
    inference(rectify,[],[f1238]) ).

fof(f1240,plain,
    ! [X0,X1] :
      ( ( pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1))
        | ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
          & scratc531300584_is_of(sK12(X0,X1),X0)
          & gg_TPTP_ind(sK12(X0,X1)) ) )
      & ( ! [X3] :
            ( pp(aa_TPTP_ind_bool(X1,X3))
            | ~ scratc531300584_is_of(X3,X0)
            | ~ gg_TPTP_ind(X3) )
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1)) ) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1239]) ).

fof(f1280,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_eo,X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X0)) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X0))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_eo,X0)) ) ),
    inference(nnf_transformation,[],[f440]) ).

fof(f1399,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dr,X0))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dq,X0))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dq,X0)))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dr,X0)) ) ),
    inference(nnf_transformation,[],[f559]) ).

fof(f1400,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dp,X0))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do,X0))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do,X0)))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dp,X0)) ) ),
    inference(nnf_transformation,[],[f560]) ).

fof(f1401,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dn,X0))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,X0))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,X0)))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dn,X0)) ) ),
    inference(nnf_transformation,[],[f561]) ).

fof(f1415,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0)))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0)) ) ),
    inference(nnf_transformation,[],[f575]) ).

fof(f1417,plain,
    ! [X0] :
      ( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
        | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ) ),
    inference(nnf_transformation,[],[f577]) ).

fof(f1479,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,X0),X1))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X0))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,X0),X1)) ) ),
    inference(nnf_transformation,[],[f1006]) ).

fof(f1480,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,X0),X1))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X0))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,X0),X1)) ) ),
    inference(flattening,[],[f1479]) ).

fof(f1481,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,X0),X1))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),X0))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,X0),X1)) ) ),
    inference(nnf_transformation,[],[f1007]) ).

fof(f1482,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,X0),X1))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),X0))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,X0),X1)) ) ),
    inference(flattening,[],[f1481]) ).

fof(f1599,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm,X0),X1))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(X0),X1))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(X0),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm,X0),X1)) ) ),
    inference(nnf_transformation,[],[f724]) ).

fof(f1603,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_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,[],[f728]) ).

fof(f1605,plain,
    ! [X0,X1] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1)) ) ),
    inference(nnf_transformation,[],[f730]) ).

fof(f1680,plain,
    ! [X0,X1,X2] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X1),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X1),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
    inference(nnf_transformation,[],[f1063]) ).

fof(f1681,plain,
    ! [X0,X1,X2] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X1),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X1),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
    inference(flattening,[],[f1680]) ).

fof(f1682,plain,
    ! [X0,X1,X2] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2)) ) ),
    inference(nnf_transformation,[],[f1065]) ).

fof(f1683,plain,
    ! [X0,X1,X2] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2)) ) ),
    inference(flattening,[],[f1682]) ).

fof(f1748,plain,
    ! [X0,X1,X2] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dl(X0),X1),X2))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2))) )
      & ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dl(X0),X1),X2)) ) ),
    inference(nnf_transformation,[],[f830]) ).

fof(f1796,plain,
    ! [X0,X1,X2,X3] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2),X3))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X2),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2),X3)) ) ),
    inference(nnf_transformation,[],[f1117]) ).

fof(f1797,plain,
    ! [X0,X1,X2,X3] :
      ( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2),X3))
        | ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X2),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X3))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X2))
          & pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1)) ) )
      & ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X2),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X3))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X2))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2),X3)) ) ),
    inference(flattening,[],[f1796]) ).

fof(f1869,plain,
    ! [X0,X1] :
      ( pp(aa_bool_bool(scratc1229951240d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X0),X1)) ),
    inference(cnf_transformation,[],[f1157]) ).

fof(f2052,plain,
    ! [X0] : aa_boo1142376798l_bool(scratc218488005nd_imp,scratc1773705014_d_not(X0)) = scratc1229951240d_l_or(X0),
    inference(cnf_transformation,[],[f161]) ).

fof(f2059,plain,
    ! [X0] :
      ( pp(scratc1773705014_d_not(X0))
      | ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc218488005nd_imp,X0),fFalse)) ),
    inference(cnf_transformation,[],[f1215]) ).

fof(f2060,plain,
    scratc218488005nd_imp = fimplies,
    inference(cnf_transformation,[],[f167]) ).

fof(f2122,plain,
    ! [X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(X1,X3))
      | ~ scratc531300584_is_of(X3,X0)
      | ~ gg_TPTP_ind(X3)
      | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1)) ),
    inference(cnf_transformation,[],[f1240]) ).

fof(f2123,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1))
      | gg_TPTP_ind(sK12(X0,X1)) ),
    inference(cnf_transformation,[],[f1240]) ).

fof(f2124,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1))
      | scratc531300584_is_of(sK12(X0,X1),X0) ),
    inference(cnf_transformation,[],[f1240]) ).

fof(f2125,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),X1))
      | ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
    inference(cnf_transformation,[],[f1240]) ).

fof(f2129,plain,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_cd)),
    inference(cnf_transformation,[],[f201]) ).

fof(f2143,plain,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dn)),
    inference(cnf_transformation,[],[f215]) ).

fof(f2144,plain,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dp)),
    inference(cnf_transformation,[],[f216]) ).

fof(f2145,plain,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dr)),
    inference(cnf_transformation,[],[f217]) ).

fof(f2155,plain,
    pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_eo)),
    inference(cnf_transformation,[],[f227]) ).

fof(f2418,plain,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X0))
      | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_eo,X0)) ),
    inference(cnf_transformation,[],[f1280]) ).

fof(f2656,plain,
    ! [X0] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dq,X0)))
      | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dr,X0)) ),
    inference(cnf_transformation,[],[f1399]) ).

fof(f2658,plain,
    ! [X0] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do,X0)))
      | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dp,X0)) ),
    inference(cnf_transformation,[],[f1400]) ).

fof(f2660,plain,
    ! [X0] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,X0)))
      | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dn,X0)) ),
    inference(cnf_transformation,[],[f1401]) ).

fof(f2688,plain,
    ! [X0] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0)))
      | ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0)) ),
    inference(cnf_transformation,[],[f1415]) ).

fof(f2693,plain,
    ! [X0] :
      ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
      | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
    inference(cnf_transformation,[],[f1417]) ).

fof(f2796,plain,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X0))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,X0),X1)) ),
    inference(cnf_transformation,[],[f1480]) ).

fof(f2799,plain,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),X0))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,X0),X1)) ),
    inference(cnf_transformation,[],[f1482]) ).

fof(f3019,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(X0),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm,X0),X1)) ),
    inference(cnf_transformation,[],[f1599]) ).

fof(f3027,plain,
    ! [X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_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,[],[f1603]) ).

fof(f3032,plain,
    ! [X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
      | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
    inference(cnf_transformation,[],[f1605]) ).

fof(f3160,plain,
    ! [X2,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
      | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1)) ),
    inference(cnf_transformation,[],[f1681]) ).

fof(f3161,plain,
    ! [X2,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
      | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X1),X2)) ),
    inference(cnf_transformation,[],[f1681]) ).

fof(f3162,plain,
    ! [X2,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2)) ),
    inference(cnf_transformation,[],[f1681]) ).

fof(f3163,plain,
    ! [X2,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X2))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X1),X2))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2)) ),
    inference(cnf_transformation,[],[f1683]) ).

fof(f3284,plain,
    ! [X2,X0,X1] :
      ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dl(X0),X1),X2)) ),
    inference(cnf_transformation,[],[f1748]) ).

fof(f3383,plain,
    ! [X2,X3,X0,X1] :
      ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X2),X3))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X3))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X2))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),X1))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),X1),X2),X3)) ),
    inference(cnf_transformation,[],[f1797]) ).

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

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

fof(f3491,plain,
    ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_ac)),
    inference(cnf_transformation,[],[f910]) ).

fof(f3495,plain,
    ! [X0] : scratc1229951240d_l_or(X0) = aa_boo1142376798l_bool(fimplies,scratc1773705014_d_not(X0)),
    inference(definition_unfolding,[],[f2052,f2060]) ).

fof(f3499,plain,
    ! [X0,X1] :
      ( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1773705014_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1)))
      | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,X0),X1)) ),
    inference(definition_unfolding,[],[f1869,f3495]) ).

fof(f3575,plain,
    ! [X0] :
      ( pp(scratc1773705014_d_not(X0))
      | ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse)) ),
    inference(definition_unfolding,[],[f2059,f2060]) ).

fof(f3831,definition,
    ( spl29_1
  <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_ac)) ),
    introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).

fof(f3833,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_ac))
    | spl29_1 ),
    inference(avatar_component_clause,[],[f3831]) ).

fof(f3834,plain,
    ~ spl29_1,
    inference(avatar_split_clause,[],[f3491,f3831]) ).

fof(f3835,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
    | spl29_1 ),
    inference(resolution,[],[f3833,f2123]) ).

fof(f3836,plain,
    ( scratc531300584_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
    | spl29_1 ),
    inference(resolution,[],[f3833,f2124]) ).

fof(f3837,plain,
    ( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | spl29_1 ),
    inference(resolution,[],[f3833,f2125]) ).

fof(f3850,definition,
    ( spl29_2
  <=> scratc531300584_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a) ),
    introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).

fof(f3852,plain,
    ( scratc531300584_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
    | ~ spl29_2 ),
    inference(avatar_component_clause,[],[f3850]) ).

fof(f3853,plain,
    ( spl29_2
    | spl29_1 ),
    inference(avatar_split_clause,[],[f3836,f3831,f3850]) ).

fof(f3855,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_2 ),
    inference(resolution,[],[f3852,f2122]) ).

fof(f3856,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | spl29_1
    | ~ spl29_2 ),
    inference(forward_subsumption_resolution,[],[f3855,f3835]) ).

fof(f3858,definition,
    ( spl29_3
  <=> ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) ) ),
    introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).

fof(f3859,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_3 ),
    inference(avatar_component_clause,[],[f3858]) ).

fof(f3860,plain,
    ( spl29_3
    | spl29_1
    | ~ spl29_2 ),
    inference(avatar_split_clause,[],[f3856,f3850,f3831,f3858]) ).

fof(f4485,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_cd))
    | pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_3 ),
    inference(resolution,[],[f3859,f2688]) ).

fof(f4500,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dp))
    | pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_3 ),
    inference(resolution,[],[f3859,f2658]) ).

fof(f4512,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_eo))
    | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | ~ spl29_3 ),
    inference(resolution,[],[f3859,f2418]) ).

fof(f4655,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | ~ spl29_3 ),
    inference(forward_subsumption_resolution,[],[f4512,f2155]) ).

fof(f4664,plain,
    ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_3 ),
    inference(forward_subsumption_resolution,[],[f4500,f2144]) ).

fof(f4679,plain,
    ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_3 ),
    inference(forward_subsumption_resolution,[],[f4485,f2129]) ).

fof(f4752,definition,
    ( spl29_4
  <=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac)) ),
    introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).

fof(f4754,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
    | ~ spl29_4 ),
    inference(avatar_component_clause,[],[f4752]) ).

fof(f4755,plain,
    ( spl29_4
    | spl29_1 ),
    inference(avatar_split_clause,[],[f3835,f3831,f4752]) ).

fof(f4757,definition,
    ( spl29_5
  <=> pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
    introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).

fof(f4759,plain,
    ( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | spl29_5 ),
    inference(avatar_component_clause,[],[f4757]) ).

fof(f4760,plain,
    ( ~ spl29_5
    | spl29_1 ),
    inference(avatar_split_clause,[],[f3837,f3831,f4757]) ).

fof(f4761,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | spl29_5 ),
    inference(resolution,[],[f4759,f2693]) ).

fof(f4800,definition,
    ( spl29_6
  <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
    introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).

fof(f4802,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | spl29_6 ),
    inference(avatar_component_clause,[],[f4800]) ).

fof(f4803,plain,
    ( ~ spl29_6
    | spl29_5 ),
    inference(avatar_split_clause,[],[f4761,f4757,f4800]) ).

fof(f4805,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | spl29_6 ),
    inference(resolution,[],[f4802,f2123]) ).

fof(f4806,plain,
    ( scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a)
    | spl29_6 ),
    inference(resolution,[],[f4802,f2124]) ).

fof(f4807,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
    | spl29_6 ),
    inference(resolution,[],[f4802,f2125]) ).

fof(f4820,definition,
    ( spl29_7
  <=> scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a) ),
    introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).

fof(f4822,plain,
    ( scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a)
    | ~ spl29_7 ),
    inference(avatar_component_clause,[],[f4820]) ).

fof(f4823,plain,
    ( spl29_7
    | spl29_6 ),
    inference(avatar_split_clause,[],[f4806,f4800,f4820]) ).

fof(f4825,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_7 ),
    inference(resolution,[],[f4822,f2122]) ).

fof(f4826,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | spl29_6
    | ~ spl29_7 ),
    inference(forward_subsumption_resolution,[],[f4825,f4805]) ).

fof(f4828,definition,
    ( spl29_8
  <=> ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) ) ),
    introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).

fof(f4829,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_8 ),
    inference(avatar_component_clause,[],[f4828]) ).

fof(f4830,plain,
    ( spl29_8
    | spl29_6
    | ~ spl29_7 ),
    inference(avatar_split_clause,[],[f4826,f4820,f4800,f4828]) ).

fof(f5469,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dn))
    | pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | ~ spl29_8 ),
    inference(resolution,[],[f4829,f2660]) ).

fof(f5635,plain,
    ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | ~ spl29_8 ),
    inference(forward_subsumption_resolution,[],[f5469,f2143]) ).

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

fof(f5724,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
    | spl29_9 ),
    inference(avatar_component_clause,[],[f5722]) ).

fof(f5725,plain,
    ( ~ spl29_9
    | spl29_6 ),
    inference(avatar_split_clause,[],[f4807,f4800,f5722]) ).

fof(f5726,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | spl29_9 ),
    inference(resolution,[],[f5724,f3032]) ).

fof(f5773,definition,
    ( spl29_10
  <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
    introduced(definition,[new_symbols(definition,[spl29_10])],[avatar_definition]) ).

fof(f5775,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | spl29_10 ),
    inference(avatar_component_clause,[],[f5773]) ).

fof(f5776,plain,
    ( ~ spl29_10
    | spl29_9 ),
    inference(avatar_split_clause,[],[f5726,f5722,f5773]) ).

fof(f5778,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | spl29_10 ),
    inference(resolution,[],[f5775,f2123]) ).

fof(f5779,plain,
    ( scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a)
    | spl29_10 ),
    inference(resolution,[],[f5775,f2124]) ).

fof(f5780,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | spl29_10 ),
    inference(resolution,[],[f5775,f2125]) ).

fof(f5793,definition,
    ( spl29_11
  <=> scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a) ),
    introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).

fof(f5795,plain,
    ( scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a)
    | ~ spl29_11 ),
    inference(avatar_component_clause,[],[f5793]) ).

fof(f5796,plain,
    ( spl29_11
    | spl29_10 ),
    inference(avatar_split_clause,[],[f5779,f5773,f5793]) ).

fof(f5798,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_11 ),
    inference(resolution,[],[f5795,f2122]) ).

fof(f5799,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | spl29_10
    | ~ spl29_11 ),
    inference(forward_subsumption_resolution,[],[f5798,f5778]) ).

fof(f5806,definition,
    ( spl29_13
  <=> ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) ) ),
    introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).

fof(f5807,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),X0)) )
    | ~ spl29_13 ),
    inference(avatar_component_clause,[],[f5806]) ).

fof(f5808,plain,
    ( spl29_13
    | spl29_10
    | ~ spl29_11 ),
    inference(avatar_split_clause,[],[f5799,f5793,f5773,f5806]) ).

fof(f5994,definition,
    ( spl29_15
  <=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
    introduced(definition,[new_symbols(definition,[spl29_15])],[avatar_definition]) ).

fof(f5996,plain,
    ( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | ~ spl29_15 ),
    inference(avatar_component_clause,[],[f5994]) ).

fof(f5997,plain,
    ( spl29_15
    | spl29_10 ),
    inference(avatar_split_clause,[],[f5778,f5773,f5994]) ).

fof(f6638,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aTP_Lamm_dr))
    | pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
    | ~ spl29_13 ),
    inference(resolution,[],[f5807,f2656]) ).

fof(f6800,plain,
    ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
    | ~ spl29_13 ),
    inference(forward_subsumption_resolution,[],[f6638,f2145]) ).

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

fof(f6891,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | spl29_16 ),
    inference(avatar_component_clause,[],[f6889]) ).

fof(f6892,plain,
    ( ~ spl29_16
    | spl29_10 ),
    inference(avatar_split_clause,[],[f5780,f5773,f6889]) ).

fof(f6893,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
    | spl29_16 ),
    inference(resolution,[],[f6891,f3160]) ).

fof(f6894,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | spl29_16 ),
    inference(resolution,[],[f6891,f3161]) ).

fof(f6895,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | spl29_16 ),
    inference(resolution,[],[f6891,f3162]) ).

fof(f6942,definition,
    ( spl29_17
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_17])],[avatar_definition]) ).

fof(f6944,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | spl29_17 ),
    inference(avatar_component_clause,[],[f6942]) ).

fof(f6945,plain,
    ( ~ spl29_17
    | spl29_16 ),
    inference(avatar_split_clause,[],[f6895,f6889,f6942]) ).

fof(f6953,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | spl29_17 ),
    inference(resolution,[],[f6944,f2796]) ).

fof(f6961,plain,
    ( ! [X0] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) )
    | spl29_17 ),
    inference(resolution,[],[f6944,f3163]) ).

fof(f7017,definition,
    ( spl29_20
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
    introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).

fof(f7019,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
    | ~ spl29_20 ),
    inference(avatar_component_clause,[],[f7017]) ).

fof(f7020,plain,
    ( spl29_20
    | spl29_16 ),
    inference(avatar_split_clause,[],[f6893,f6889,f7017]) ).

fof(f7022,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
    | ~ spl29_20 ),
    inference(resolution,[],[f7019,f2799]) ).

fof(f7226,definition,
    ( spl29_23
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_23])],[avatar_definition]) ).

fof(f7228,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1469740332lesseq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | ~ spl29_23 ),
    inference(avatar_component_clause,[],[f7226]) ).

fof(f7229,plain,
    ( spl29_23
    | spl29_16 ),
    inference(avatar_split_clause,[],[f6894,f6889,f7226]) ).

fof(f7238,plain,
    ( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1773705014_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
    | ~ spl29_23 ),
    inference(resolution,[],[f7228,f3499]) ).

fof(f7272,definition,
    ( spl29_24
  <=> pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1773705014_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_24])],[avatar_definition]) ).

fof(f7274,plain,
    ( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1773705014_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
    | ~ spl29_24 ),
    inference(avatar_component_clause,[],[f7272]) ).

fof(f7275,plain,
    ( spl29_24
    | ~ spl29_23 ),
    inference(avatar_split_clause,[],[f7238,f7226,f7272]) ).

fof(f7277,plain,
    ( ~ pp(scratc1773705014_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
    | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | ~ spl29_24 ),
    inference(resolution,[],[f7274,f3482]) ).

fof(f7706,definition,
    ( spl29_35
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
    introduced(definition,[new_symbols(definition,[spl29_35])],[avatar_definition]) ).

fof(f7708,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | spl29_35 ),
    inference(avatar_component_clause,[],[f7706]) ).

fof(f7710,definition,
    ( spl29_36
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
    introduced(definition,[new_symbols(definition,[spl29_36])],[avatar_definition]) ).

fof(f7712,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | spl29_36 ),
    inference(avatar_component_clause,[],[f7710]) ).

fof(f7713,plain,
    ( ~ spl29_35
    | ~ spl29_36
    | spl29_17 ),
    inference(avatar_split_clause,[],[f6953,f6942,f7710,f7706]) ).

fof(f7722,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
    | ~ spl29_3
    | spl29_35 ),
    inference(resolution,[],[f7708,f3859]) ).

fof(f7761,plain,
    ( $false
    | ~ spl29_3
    | ~ spl29_13
    | spl29_35 ),
    inference(forward_subsumption_resolution,[],[f7722,f6800]) ).

fof(f7762,plain,
    ( ~ spl29_3
    | ~ spl29_13
    | spl29_35 ),
    inference(avatar_contradiction_clause,[],[f7761]) ).

fof(f7831,definition,
    ( spl29_37
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
    introduced(definition,[new_symbols(definition,[spl29_37])],[avatar_definition]) ).

fof(f7833,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
    | spl29_37 ),
    inference(avatar_component_clause,[],[f7831]) ).

fof(f7835,definition,
    ( spl29_38
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
    introduced(definition,[new_symbols(definition,[spl29_38])],[avatar_definition]) ).

fof(f7837,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | ~ spl29_38 ),
    inference(avatar_component_clause,[],[f7835]) ).

fof(f7838,plain,
    ( ~ spl29_37
    | spl29_38
    | ~ spl29_20 ),
    inference(avatar_split_clause,[],[f7022,f7017,f7835,f7831]) ).

fof(f7847,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_8
    | spl29_37 ),
    inference(resolution,[],[f7833,f4829]) ).

fof(f7886,plain,
    ( $false
    | ~ spl29_3
    | ~ spl29_8
    | spl29_37 ),
    inference(forward_subsumption_resolution,[],[f7847,f4664]) ).

fof(f7887,plain,
    ( ~ spl29_3
    | ~ spl29_8
    | spl29_37 ),
    inference(avatar_contradiction_clause,[],[f7886]) ).

fof(f8331,definition,
    ( spl29_52
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
    introduced(definition,[new_symbols(definition,[spl29_52])],[avatar_definition]) ).

fof(f8333,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | ~ spl29_52 ),
    inference(avatar_component_clause,[],[f8331]) ).

fof(f8334,plain,
    ( spl29_52
    | ~ spl29_3 ),
    inference(avatar_split_clause,[],[f4655,f3858,f8331]) ).

fof(f8345,plain,
    ( ! [X0,X1] :
        ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
    | ~ spl29_52 ),
    inference(resolution,[],[f8333,f3383]) ).

fof(f8522,definition,
    ( spl29_59
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_59])],[avatar_definition]) ).

fof(f8524,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | ~ spl29_59 ),
    inference(avatar_component_clause,[],[f8522]) ).

fof(f8526,definition,
    ( spl29_60
  <=> pp(scratc1773705014_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_60])],[avatar_definition]) ).

fof(f8528,plain,
    ( ~ pp(scratc1773705014_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
    | spl29_60 ),
    inference(avatar_component_clause,[],[f8526]) ).

fof(f8529,plain,
    ( spl29_59
    | ~ spl29_60
    | ~ spl29_24 ),
    inference(avatar_split_clause,[],[f7277,f7272,f8526,f8522]) ).

fof(f8533,plain,
    ( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),fFalse))
    | spl29_60 ),
    inference(resolution,[],[f8528,f3575]) ).

fof(f8546,definition,
    ( spl29_61
  <=> pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),fFalse)) ),
    introduced(definition,[new_symbols(definition,[spl29_61])],[avatar_definition]) ).

fof(f8548,plain,
    ( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),fFalse))
    | spl29_61 ),
    inference(avatar_component_clause,[],[f8546]) ).

fof(f8549,plain,
    ( ~ spl29_61
    | spl29_60 ),
    inference(avatar_split_clause,[],[f8533,f8526,f8546]) ).

fof(f8551,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | spl29_61 ),
    inference(resolution,[],[f8548,f3484]) ).

fof(f9260,definition,
    ( spl29_90
  <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
    introduced(definition,[new_symbols(definition,[spl29_90])],[avatar_definition]) ).

fof(f9262,plain,
    ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_90 ),
    inference(avatar_component_clause,[],[f9260]) ).

fof(f9263,plain,
    ( spl29_90
    | ~ spl29_3 ),
    inference(avatar_split_clause,[],[f4679,f3858,f9260]) ).

fof(f9508,definition,
    ( spl29_100
  <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
    introduced(definition,[new_symbols(definition,[spl29_100])],[avatar_definition]) ).

fof(f9510,plain,
    ( pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | ~ spl29_100 ),
    inference(avatar_component_clause,[],[f9508]) ).

fof(f9511,plain,
    ( spl29_100
    | ~ spl29_8 ),
    inference(avatar_split_clause,[],[f5635,f4828,f9508]) ).

fof(f10006,definition,
    ( spl29_119
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
    introduced(definition,[new_symbols(definition,[spl29_119])],[avatar_definition]) ).

fof(f10007,plain,
    ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
    | ~ spl29_119 ),
    inference(avatar_component_clause,[],[f10006]) ).

fof(f13564,definition,
    ( spl29_207
  <=> ! [X0,X1] :
        ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_207])],[avatar_definition]) ).

fof(f13565,plain,
    ( ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X1),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
    | ~ spl29_207 ),
    inference(avatar_component_clause,[],[f13564]) ).

fof(f13566,plain,
    ( spl29_207
    | ~ spl29_52 ),
    inference(avatar_split_clause,[],[f8345,f8331,f13564]) ).

fof(f13581,plain,
    ( ! [X2,X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X2)
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X2),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X1))) )
    | ~ spl29_207 ),
    inference(resolution,[],[f13565,f2122]) ).

fof(f13616,plain,
    ( ! [X2,X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X2)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X2),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X1))) )
    | ~ spl29_4
    | ~ spl29_207 ),
    inference(forward_subsumption_resolution,[],[f13581,f4754]) ).

fof(f13621,definition,
    ( spl29_208
  <=> ! [X2,X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X2)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X2),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X1))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_208])],[avatar_definition]) ).

fof(f13622,plain,
    ( ! [X2,X0,X1] :
        ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X2),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dk(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X1)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X2)
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1)) )
    | ~ spl29_208 ),
    inference(avatar_component_clause,[],[f13621]) ).

fof(f13623,plain,
    ( spl29_208
    | ~ spl29_4
    | ~ spl29_207 ),
    inference(avatar_split_clause,[],[f13616,f13564,f4752,f13621]) ).

fof(f13624,plain,
    ( ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dl(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X1)) )
    | ~ spl29_208 ),
    inference(resolution,[],[f13622,f3284]) ).

fof(f13640,plain,
    ( ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dl(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X1)) )
    | ~ spl29_2
    | ~ spl29_208 ),
    inference(forward_subsumption_resolution,[],[f13624,f3852]) ).

fof(f16597,definition,
    ( spl29_289
  <=> ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dl(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X1)) ) ),
    introduced(definition,[new_symbols(definition,[spl29_289])],[avatar_definition]) ).

fof(f16598,plain,
    ( ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dl(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X1))
        | pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X1),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),X1))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
    | ~ spl29_289 ),
    inference(avatar_component_clause,[],[f16597]) ).

fof(f16599,plain,
    ( spl29_289
    | ~ spl29_2
    | ~ spl29_208 ),
    inference(avatar_split_clause,[],[f13640,f13621,f3850,f16597]) ).

fof(f16635,plain,
    ( ! [X0] :
        ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) )
    | ~ spl29_13
    | ~ spl29_289 ),
    inference(resolution,[],[f16598,f5807]) ).

fof(f16648,plain,
    ( ! [X0] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) )
    | ~ spl29_13
    | spl29_36
    | ~ spl29_289 ),
    inference(forward_subsumption_resolution,[],[f16635,f7712]) ).

fof(f16655,definition,
    ( spl29_290
  <=> ! [X0] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_290])],[avatar_definition]) ).

fof(f16656,plain,
    ( ! [X0] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1360940179d_n_eq,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) )
    | ~ spl29_290 ),
    inference(avatar_component_clause,[],[f16655]) ).

fof(f16657,plain,
    ( spl29_290
    | ~ spl29_13
    | spl29_36
    | ~ spl29_289 ),
    inference(avatar_split_clause,[],[f16648,f16597,f7710,f5806,f16655]) ).

fof(f16674,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2130321418_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_59
    | ~ spl29_290 ),
    inference(resolution,[],[f16656,f8524]) ).

fof(f16723,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_38
    | ~ spl29_59
    | ~ spl29_290 ),
    inference(forward_subsumption_resolution,[],[f16674,f7837]) ).

fof(f16725,definition,
    ( spl29_291
  <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
    introduced(definition,[new_symbols(definition,[spl29_291])],[avatar_definition]) ).

fof(f16727,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | spl29_291 ),
    inference(avatar_component_clause,[],[f16725]) ).

fof(f16728,plain,
    ( ~ spl29_291
    | ~ spl29_38
    | ~ spl29_59
    | ~ spl29_290 ),
    inference(avatar_split_clause,[],[f16723,f16655,f8522,f7835,f16725]) ).

fof(f16729,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | spl29_291 ),
    inference(resolution,[],[f16727,f3019]) ).

fof(f16746,definition,
    ( spl29_292
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
    introduced(definition,[new_symbols(definition,[spl29_292])],[avatar_definition]) ).

fof(f16748,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
    | spl29_292 ),
    inference(avatar_component_clause,[],[f16746]) ).

fof(f16749,plain,
    ( ~ spl29_292
    | spl29_291 ),
    inference(avatar_split_clause,[],[f16729,f16725,f16746]) ).

fof(f16757,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | ~ spl29_3
    | spl29_292 ),
    inference(resolution,[],[f16748,f3859]) ).

fof(f16797,plain,
    ( $false
    | ~ spl29_3
    | ~ spl29_100
    | spl29_292 ),
    inference(forward_subsumption_resolution,[],[f16757,f9510]) ).

fof(f16798,plain,
    ( ~ spl29_3
    | ~ spl29_100
    | spl29_292 ),
    inference(avatar_contradiction_clause,[],[f16797]) ).

fof(f17223,plain,
    ( spl29_119
    | spl29_61 ),
    inference(avatar_split_clause,[],[f8551,f8546,f10006]) ).

fof(f19518,definition,
    ( spl29_337
  <=> ! [X0] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_337])],[avatar_definition]) ).

fof(f19519,plain,
    ( ! [X0] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) )
    | ~ spl29_337 ),
    inference(avatar_component_clause,[],[f19518]) ).

fof(f19520,plain,
    ( spl29_337
    | spl29_17 ),
    inference(avatar_split_clause,[],[f6961,f6942,f19518]) ).

fof(f23215,plain,
    ( ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X1)
        | ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))) )
    | ~ spl29_337 ),
    inference(resolution,[],[f19519,f2122]) ).

fof(f23252,plain,
    ( ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X1)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))) )
    | ~ spl29_15
    | ~ spl29_337 ),
    inference(forward_subsumption_resolution,[],[f23215,f5996]) ).

fof(f32845,definition,
    ( spl29_564
  <=> ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X1)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_564])],[avatar_definition]) ).

fof(f32846,plain,
    ( ! [X0,X1] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
        | ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X1)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0))) )
    | ~ spl29_564 ),
    inference(avatar_component_clause,[],[f32845]) ).

fof(f32847,plain,
    ( spl29_564
    | ~ spl29_15
    | ~ spl29_337 ),
    inference(avatar_split_clause,[],[f23252,f19518,f5994,f32845]) ).

fof(f32849,plain,
    ( ! [X0] :
        ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1783999622_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
        | ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
    | ~ spl29_119
    | ~ spl29_564 ),
    inference(resolution,[],[f32846,f10007]) ).

fof(f32911,plain,
    ( ! [X0] :
        ( ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
    | ~ spl29_20
    | ~ spl29_119
    | ~ spl29_564 ),
    inference(forward_subsumption_resolution,[],[f32849,f7019]) ).

fof(f32913,definition,
    ( spl29_565
  <=> ! [X0] :
        ( ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ) ),
    introduced(definition,[new_symbols(definition,[spl29_565])],[avatar_definition]) ).

fof(f32914,plain,
    ( ! [X0] :
        ( ~ scratc531300584_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
        | ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
    | ~ spl29_565 ),
    inference(avatar_component_clause,[],[f32913]) ).

fof(f32915,plain,
    ( spl29_565
    | ~ spl29_20
    | ~ spl29_119
    | ~ spl29_564 ),
    inference(avatar_split_clause,[],[f32911,f32845,f10006,f7017,f32913]) ).

fof(f32917,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | ~ spl29_11
    | ~ spl29_565 ),
    inference(resolution,[],[f32914,f5795]) ).

fof(f32922,definition,
    ( spl29_566
  <=> pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
    introduced(definition,[new_symbols(definition,[spl29_566])],[avatar_definition]) ).

fof(f32924,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
    | spl29_566 ),
    inference(avatar_component_clause,[],[f32922]) ).

fof(f32925,plain,
    ( ~ spl29_566
    | ~ spl29_11
    | ~ spl29_565 ),
    inference(avatar_split_clause,[],[f32917,f32913,f5793,f32922]) ).

fof(f32926,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
    | spl29_566 ),
    inference(resolution,[],[f32924,f3027]) ).

fof(f32943,definition,
    ( spl29_567
  <=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
    introduced(definition,[new_symbols(definition,[spl29_567])],[avatar_definition]) ).

fof(f32945,plain,
    ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
    | spl29_567 ),
    inference(avatar_component_clause,[],[f32943]) ).

fof(f32946,plain,
    ( ~ spl29_567
    | spl29_566 ),
    inference(avatar_split_clause,[],[f32926,f32922,f32943]) ).

fof(f32955,plain,
    ( ~ pp(aa_fun171081125l_bool(scratc1788344817all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
    | ~ spl29_8
    | spl29_567 ),
    inference(resolution,[],[f32945,f4829]) ).

fof(f32995,plain,
    ( $false
    | ~ spl29_8
    | ~ spl29_90
    | spl29_567 ),
    inference(forward_subsumption_resolution,[],[f32955,f9262]) ).

fof(f32996,plain,
    ( ~ spl29_8
    | ~ spl29_90
    | spl29_567 ),
    inference(avatar_contradiction_clause,[],[f32995]) ).

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

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

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

cnf(s4,plain,
    ( spl29_1
    | spl29_4 ),
    inference(sat_conversion,[],[f4755]) ).

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

cnf(s6,plain,
    ( spl29_5
    | ~ spl29_6 ),
    inference(sat_conversion,[],[f4803]) ).

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

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

cnf(s9,plain,
    ( spl29_6
    | ~ spl29_9 ),
    inference(sat_conversion,[],[f5725]) ).

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

cnf(s11,plain,
    ( spl29_10
    | spl29_11 ),
    inference(sat_conversion,[],[f5796]) ).

cnf(s13,plain,
    ( spl29_10
    | ~ spl29_11
    | spl29_13 ),
    inference(sat_conversion,[],[f5808]) ).

cnf(s15,plain,
    ( spl29_10
    | spl29_15 ),
    inference(sat_conversion,[],[f5997]) ).

cnf(s16,plain,
    ( spl29_10
    | ~ spl29_16 ),
    inference(sat_conversion,[],[f6892]) ).

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

cnf(s20,plain,
    ( spl29_16
    | spl29_20 ),
    inference(sat_conversion,[],[f7020]) ).

cnf(s23,plain,
    ( spl29_16
    | spl29_23 ),
    inference(sat_conversion,[],[f7229]) ).

cnf(s24,plain,
    ( ~ spl29_23
    | spl29_24 ),
    inference(sat_conversion,[],[f7275]) ).

cnf(s35,plain,
    ( spl29_17
    | ~ spl29_35
    | ~ spl29_36 ),
    inference(sat_conversion,[],[f7713]) ).

cnf(s36,plain,
    ( ~ spl29_3
    | ~ spl29_13
    | spl29_35 ),
    inference(sat_conversion,[],[f7762]) ).

cnf(s37,plain,
    ( ~ spl29_20
    | ~ spl29_37
    | spl29_38 ),
    inference(sat_conversion,[],[f7838]) ).

cnf(s38,plain,
    ( ~ spl29_3
    | ~ spl29_8
    | spl29_37 ),
    inference(sat_conversion,[],[f7887]) ).

cnf(s51,plain,
    ( ~ spl29_3
    | spl29_52 ),
    inference(sat_conversion,[],[f8334]) ).

cnf(s59,plain,
    ( ~ spl29_24
    | spl29_59
    | ~ spl29_60 ),
    inference(sat_conversion,[],[f8529]) ).

cnf(s60,plain,
    ( spl29_60
    | ~ spl29_61 ),
    inference(sat_conversion,[],[f8549]) ).

cnf(s89,plain,
    ( ~ spl29_3
    | spl29_90 ),
    inference(sat_conversion,[],[f9263]) ).

cnf(s99,plain,
    ( ~ spl29_8
    | spl29_100 ),
    inference(sat_conversion,[],[f9511]) ).

cnf(s210,plain,
    ( ~ spl29_52
    | spl29_207 ),
    inference(sat_conversion,[],[f13566]) ).

cnf(s211,plain,
    ( ~ spl29_4
    | ~ spl29_207
    | spl29_208 ),
    inference(sat_conversion,[],[f13623]) ).

cnf(s303,plain,
    ( ~ spl29_2
    | ~ spl29_208
    | spl29_289 ),
    inference(sat_conversion,[],[f16599]) ).

cnf(s304,plain,
    ( ~ spl29_13
    | spl29_36
    | ~ spl29_289
    | spl29_290 ),
    inference(sat_conversion,[],[f16657]) ).

cnf(s305,plain,
    ( ~ spl29_38
    | ~ spl29_59
    | ~ spl29_290
    | ~ spl29_291 ),
    inference(sat_conversion,[],[f16728]) ).

cnf(s306,plain,
    ( spl29_291
    | ~ spl29_292 ),
    inference(sat_conversion,[],[f16749]) ).

cnf(s307,plain,
    ( ~ spl29_3
    | ~ spl29_100
    | spl29_292 ),
    inference(sat_conversion,[],[f16798]) ).

cnf(s310,plain,
    ( spl29_61
    | spl29_119 ),
    inference(sat_conversion,[],[f17223]) ).

cnf(s353,plain,
    ( spl29_17
    | spl29_337 ),
    inference(sat_conversion,[],[f19520]) ).

cnf(s613,plain,
    ( ~ spl29_15
    | ~ spl29_337
    | spl29_564 ),
    inference(sat_conversion,[],[f32847]) ).

cnf(s614,plain,
    ( ~ spl29_20
    | ~ spl29_119
    | ~ spl29_564
    | spl29_565 ),
    inference(sat_conversion,[],[f32915]) ).

cnf(s615,plain,
    ( ~ spl29_11
    | ~ spl29_565
    | ~ spl29_566 ),
    inference(sat_conversion,[],[f32925]) ).

cnf(s616,plain,
    ( spl29_566
    | ~ spl29_567 ),
    inference(sat_conversion,[],[f32946]) ).

cnf(s617,plain,
    ( ~ spl29_8
    | ~ spl29_90
    | spl29_567 ),
    inference(sat_conversion,[],[f32996]) ).

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

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

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

cnf(s631,plain,
    ~ spl29_6,
    inference(rat,[],[s6,s621]) ).

cnf(s639,plain,
    spl29_3,
    inference(rat,[],[s3,s1,s623]) ).

cnf(s645,plain,
    ~ spl29_9,
    inference(rat,[],[s9,s631]) ).

cnf(s646,plain,
    spl29_7,
    inference(rat,[],[s7,s631]) ).

cnf(s654,plain,
    spl29_90,
    inference(rat,[],[s89,s639]) ).

cnf(s676,plain,
    spl29_52,
    inference(rat,[],[s51,s639]) ).

cnf(s689,plain,
    ~ spl29_10,
    inference(rat,[],[s10,s645]) ).

cnf(s690,plain,
    spl29_8,
    inference(rat,[],[s8,s631,s646]) ).

cnf(s746,plain,
    spl29_207,
    inference(rat,[],[s210,s676]) ).

cnf(s753,plain,
    ~ spl29_16,
    inference(rat,[],[s16,s689]) ).

cnf(s754,plain,
    spl29_15,
    inference(rat,[],[s15,s689]) ).

cnf(s755,plain,
    spl29_11,
    inference(rat,[],[s11,s689]) ).

cnf(s756,plain,
    spl29_567,
    inference(rat,[],[s617,s654,s690]) ).

cnf(s777,plain,
    spl29_100,
    inference(rat,[],[s99,s690]) ).

cnf(s786,plain,
    spl29_37,
    inference(rat,[],[s38,s639,s690]) ).

cnf(s790,plain,
    spl29_208,
    inference(rat,[],[s211,s622,s746]) ).

cnf(s797,plain,
    spl29_23,
    inference(rat,[],[s23,s753]) ).

cnf(s798,plain,
    spl29_20,
    inference(rat,[],[s20,s753]) ).

cnf(s799,plain,
    ~ spl29_17,
    inference(rat,[],[s17,s753]) ).

cnf(s802,plain,
    spl29_13,
    inference(rat,[],[s13,s689,s755]) ).

cnf(s803,plain,
    spl29_566,
    inference(rat,[],[s616,s756]) ).

cnf(s823,plain,
    spl29_292,
    inference(rat,[],[s307,s639,s777]) ).

cnf(s864,plain,
    spl29_289,
    inference(rat,[],[s303,s623,s790]) ).

cnf(s870,plain,
    spl29_24,
    inference(rat,[],[s24,s797]) ).

cnf(s876,plain,
    spl29_38,
    inference(rat,[],[s37,s786,s798]) ).

cnf(s882,plain,
    spl29_337,
    inference(rat,[],[s353,s799]) ).

cnf(s924,plain,
    spl29_35,
    inference(rat,[],[s36,s639,s802]) ).

cnf(s928,plain,
    ~ spl29_565,
    inference(rat,[],[s615,s755,s803]) ).

cnf(s930,plain,
    spl29_291,
    inference(rat,[],[s306,s823]) ).

cnf(s948,plain,
    spl29_564,
    inference(rat,[],[s613,s754,s882]) ).

cnf(s984,plain,
    ~ spl29_36,
    inference(rat,[],[s35,s799,s924]) ).

cnf(s994,plain,
    ~ spl29_119,
    inference(rat,[],[s614,s928,s798,s948]) ).

cnf(s998,plain,
    spl29_290,
    inference(rat,[],[s304,s802,s864,s984]) ).

cnf(s1017,plain,
    spl29_61,
    inference(rat,[],[s310,s994]) ).

cnf(s1024,plain,
    ~ spl29_59,
    inference(rat,[],[s305,s930,s876,s998]) ).

cnf(s1037,plain,
    spl29_60,
    inference(rat,[],[s60,s1017]) ).

cnf(s1048,plain,
    $false,
    inference(rat,[],[s59,s870,s1037,s1024]) ).

fof(f33000,plain,
    $false,
    inference(avatar_sat_refutation,[],[s1048]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NUM743+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.14/0.41  % Computer : n005.cluster.edu
% 0.14/0.41  % Model    : x86_64 x86_64
% 0.14/0.41  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41  % Memory   : 8046.5625MB
% 0.14/0.41  % OS       : Linux 6.8.0-71-generic
% 0.14/0.41  % CPULimit : 300
% 0.14/0.41  % WCLimit  : 300
% 0.14/0.41  % DateTime : Sun Sep 27 21:15:32 UTC 2026
% 0.14/0.42  % CPUTime  : 
% 0.14/0.42  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.47  Running first-order theorem proving
% 0.14/0.47  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
% 21.80/4.23  % (174572)Detected formulas, will run a generic FOF schedule.
% 21.80/4.23  % (174583)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=2685475766:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 21.80/4.23  % (174585)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3389396352:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 21.80/4.23  % (174585)Refutation not found, incomplete strategy
% 21.80/4.23  % (174585)------------------------------
% 21.80/4.23  % (174585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.80/4.23  % (174585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/4.23  % (174585)CaDiCaL version: 2.1.3
% 21.80/4.23  % (174585)Termination reason: Refutation not found, incomplete strategy
% 21.80/4.23  % (174585)Time elapsed: 0.004 s
% 21.80/4.23  % (174585)Peak memory usage: 88 MB
% 21.80/4.23  % (174585)Instructions burned: 4 (million)
% 21.80/4.23  % (174582)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=3803973879:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 21.80/4.23  % (174581)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=2075287529:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 21.80/4.23  % (174587)dis-21_1_sil=8000:lcm=predicate:random_seed=2948004732: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)
% 21.80/4.23  % (174586)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=537547138:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 21.80/4.23  % (174584)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=342818083:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 21.80/4.23  % (174584)Refutation not found, incomplete strategy
% 21.80/4.23  % (174584)------------------------------
% 21.80/4.23  % (174584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.80/4.23  % (174584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/4.23  % (174584)CaDiCaL version: 2.1.3
% 21.80/4.23  % (174584)Termination reason: Refutation not found, incomplete strategy
% 21.80/4.23  % (174584)Time elapsed: 0.005 s
% 21.80/4.23  % (174584)Peak memory usage: 88 MB
% 21.80/4.23  % (174584)Instructions burned: 4 (million)
% 21.80/4.23  % (174587)Instruction limit reached! 
% 21.80/4.23  % (174587)------------------------------
% 21.80/4.23  % (174587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.80/4.23  % (174587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/4.23  % (174587)CaDiCaL version: 2.1.3
% 21.80/4.23  % (174587)Termination reason: Instruction limit
% 21.80/4.23  % (174587)Termination phase: Saturation
% 21.80/4.23  % (174587)Time elapsed: 0.114 s
% 21.80/4.23  % (174587)Peak memory usage: 90 MB
% 21.80/4.23  % (174587)Instructions burned: 129 (million)
% 21.80/4.23  % (174586)Instruction limit reached! 
% 21.80/4.23  % (174586)------------------------------
% 21.80/4.23  % (174586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.80/4.23  % (174586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/4.23  % (174586)CaDiCaL version: 2.1.3
% 21.80/4.23  % (174586)Termination reason: Instruction limit
% 21.80/4.23  % (174586)Termination phase: Saturation
% 21.80/4.23  % (174586)Time elapsed: 0.128 s
% 21.80/4.23  % (174586)Peak memory usage: 91 MB
% 21.80/4.23  % (174586)Instructions burned: 141 (million)
% 21.80/4.23  % (174585)------------------------------
% 21.80/4.23  % (174585)------------------------------
% 21.80/4.23  % (174595)lrs+10_1_sil=8000:sp=occurrence:random_seed=6466190:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 21.80/4.23  % (174596)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3905583292:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 21.80/4.23  % (174595)Refutation not found, incomplete strategy
% 21.80/4.23  % (174595)------------------------------
% 21.80/4.23  % (174595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.80/4.23  % (174595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/4.23  % (174595)CaDiCaL version: 2.1.3
% 21.80/4.23  % (174595)Termination reason: Refutation not found, incomplete strategy
% 32.79/5.94  % (174595)Time elapsed: 0.006 s
% 32.79/5.94  % (174595)Peak memory usage: 88 MB
% 32.79/5.94  % (174595)Instructions burned: 4 (million)
% 32.79/5.94  % (174596)Refutation not found, incomplete strategy
% 32.79/5.94  % (174596)------------------------------
% 32.79/5.94  % (174596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.79/5.94  % (174596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.79/5.94  % (174596)CaDiCaL version: 2.1.3
% 32.79/5.94  % (174596)Termination reason: Refutation not found, incomplete strategy
% 32.79/5.94  % (174596)Time elapsed: 0.014 s
% 32.79/5.94  % (174596)Peak memory usage: 89 MB
% 32.79/5.94  % (174596)Instructions burned: 14 (million)
% 32.79/5.94  % (174584)------------------------------
% 32.79/5.94  % (174584)------------------------------
% 32.79/5.94  % (174597)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1915486022:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 32.79/5.94  % (174597)Refutation not found, incomplete strategy
% 32.79/5.94  % (174597)------------------------------
% 32.79/5.94  % (174597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.79/5.94  % (174597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.79/5.94  % (174597)CaDiCaL version: 2.1.3
% 32.79/5.94  % (174597)Termination reason: Refutation not found, incomplete strategy
% 32.79/5.94  % (174597)Time elapsed: 0.010 s
% 32.79/5.94  % (174597)Peak memory usage: 89 MB
% 32.79/5.94  % (174597)Instructions burned: 6 (million)
% 32.79/5.94  % (174595)------------------------------
% 32.79/5.94  % (174595)------------------------------
% 32.79/5.94  % (174600)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=3877645583:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 32.79/5.94  % (174596)------------------------------
% 32.79/5.94  % (174596)------------------------------
% 32.79/5.94  % (174602)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2104509415:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 32.79/5.94  % (174602)Refutation not found, incomplete strategy
% 32.79/5.94  % (174602)------------------------------
% 32.79/5.94  % (174602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.79/5.94  % (174602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.79/5.94  % (174602)CaDiCaL version: 2.1.3
% 32.79/5.94  % (174602)Termination reason: Refutation not found, incomplete strategy
% 32.79/5.94  % (174602)Time elapsed: 0.006 s
% 32.79/5.94  % (174602)Peak memory usage: 89 MB
% 32.79/5.94  % (174602)Instructions burned: 9 (million)
% 32.79/5.94  % (174600)Instruction limit reached! 
% 32.79/5.94  % (174600)------------------------------
% 32.79/5.94  % (174600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.79/5.94  % (174600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.79/5.94  % (174600)CaDiCaL version: 2.1.3
% 32.79/5.94  % (174600)Termination reason: Instruction limit
% 32.79/5.94  % (174600)Termination phase: Saturation
% 32.79/5.94  % (174600)Time elapsed: 0.221 s
% 32.79/5.94  % (174600)Peak memory usage: 97 MB
% 32.79/5.94  % (174600)Instructions burned: 249 (million)
% 32.79/5.94  % (174597)------------------------------
% 32.79/5.94  % (174597)------------------------------
% 32.79/5.94  % (174604)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3346895308:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 32.79/5.94  % (174602)------------------------------
% 32.79/5.94  % (174602)------------------------------
% 32.79/5.94  % (174606)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3756886731:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 32.79/5.94  % (174607)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3787029246:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 32.79/5.94  % (174606)Instruction limit reached! 
% 32.79/5.94  % (174606)------------------------------
% 32.79/5.94  % (174606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.79/5.94  % (174606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.79/5.94  % (174606)CaDiCaL version: 2.1.3
% 32.79/5.94  % (174606)Termination reason: Instruction limit
% 32.79/5.94  % (174606)Termination phase: Saturation
% 32.79/5.94  % (174606)Time elapsed: 0.100 s
% 32.79/5.94  % (174606)Peak memory usage: 90 MB
% 32.79/5.94  % (174606)Instructions burned: 113 (million)
% 32.79/5.94  % (174609)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2514041386:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 60.13/9.62  % (174607)Instruction limit reached! 
% 60.13/9.62  % (174607)------------------------------
% 60.13/9.62  % (174607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.62  % (174607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.62  % (174607)CaDiCaL version: 2.1.3
% 60.13/9.62  % (174607)Termination reason: Instruction limit
% 60.13/9.62  % (174607)Termination phase: Saturation
% 60.13/9.62  % (174607)Time elapsed: 0.107 s
% 60.13/9.62  % (174607)Peak memory usage: 90 MB
% 60.13/9.62  % (174607)Instructions burned: 127 (million)
% 60.13/9.62  % (174609)Instruction limit reached! 
% 60.13/9.62  % (174609)------------------------------
% 60.13/9.62  % (174609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.62  % (174609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.62  % (174609)CaDiCaL version: 2.1.3
% 60.13/9.62  % (174609)Termination reason: Instruction limit
% 60.13/9.62  % (174609)Termination phase: Saturation
% 60.13/9.62  % (174609)Time elapsed: 0.060 s
% 60.13/9.62  % (174609)Peak memory usage: 90 MB
% 60.13/9.62  % (174609)Instructions burned: 116 (million)
% 60.13/9.62  % (174612)lrs+10_1_sil=8000:sp=occurrence:random_seed=3624771405:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 60.13/9.62  % (174614)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3422545698:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 60.13/9.62  % (174617)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=305911344:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 60.13/9.62  % (174614)Refutation not found, incomplete strategy
% 60.13/9.62  % (174614)------------------------------
% 60.13/9.62  % (174614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.62  % (174614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.62  % (174614)CaDiCaL version: 2.1.3
% 60.13/9.62  % (174614)Termination reason: Refutation not found, incomplete strategy
% 60.13/9.62  % (174614)Time elapsed: 0.115 s
% 60.13/9.62  % (174614)Peak memory usage: 92 MB
% 60.13/9.62  % (174614)Instructions burned: 130 (million)
% 60.13/9.62  % (174614)------------------------------
% 60.13/9.62  % (174614)------------------------------
% 60.13/9.62  % (174625)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=608362501:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 60.13/9.62  % (174612)Instruction limit reached! 
% 60.13/9.62  % (174612)------------------------------
% 60.13/9.62  % (174612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.62  % (174612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.62  % (174612)CaDiCaL version: 2.1.3
% 60.13/9.62  % (174612)Termination reason: Instruction limit
% 60.13/9.62  % (174612)Termination phase: Saturation
% 60.13/9.62  % (174612)Time elapsed: 0.866 s
% 60.13/9.62  % (174612)Peak memory usage: 100 MB
% 60.13/9.62  % (174612)Instructions burned: 907 (million)
% 60.13/9.62  % (174625)Instruction limit reached! 
% 60.13/9.62  % (174625)------------------------------
% 60.13/9.62  % (174625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.62  % (174625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.62  % (174625)CaDiCaL version: 2.1.3
% 60.13/9.62  % (174625)Termination reason: Instruction limit
% 60.13/9.62  % (174625)Termination phase: Saturation
% 60.13/9.62  % (174625)Time elapsed: 0.115 s
% 60.13/9.62  % (174625)Peak memory usage: 92 MB
% 60.13/9.62  % (174625)Instructions burned: 135 (million)
% 60.13/9.62  % (174629)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2866501575:st=8:i=592:sd=3:ep=RST:ss=axioms_2972 on theBenchmark for (2972ds/592Mi)
% 60.13/9.62  % (174629)Refutation not found, incomplete strategy
% 60.13/9.62  % (174629)------------------------------
% 60.13/9.62  % (174629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.62  % (174629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.62  % (174629)CaDiCaL version: 2.1.3
% 60.13/9.62  % (174629)Termination reason: Refutation not found, incomplete strategy
% 60.13/9.62  % (174629)Time elapsed: 0.031 s
% 60.13/9.62  % (174629)Peak memory usage: 89 MB
% 60.13/9.62  % (174629)Instructions burned: 33 (million)
% 60.13/9.62  % (174630)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3465320296:st=3:i=13193:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/13193Mi)
% 89.86/13.88  % (174629)------------------------------
% 89.86/13.88  % (174629)------------------------------
% 89.86/13.88  % (174633)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=4286328813:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/125Mi)
% 89.86/13.88  % (174633)Refutation not found, incomplete strategy
% 89.86/13.88  % (174633)------------------------------
% 89.86/13.88  % (174633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174633)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174633)Termination reason: Refutation not found, incomplete strategy
% 89.86/13.88  % (174633)Time elapsed: 0.017 s
% 89.86/13.88  % (174633)Peak memory usage: 89 MB
% 89.86/13.88  % (174633)Instructions burned: 18 (million)
% 89.86/13.88  % (174604)Instruction limit reached! 
% 89.86/13.88  % (174604)------------------------------
% 89.86/13.88  % (174604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174604)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174604)Termination reason: Instruction limit
% 89.86/13.88  % (174604)Termination phase: Saturation
% 89.86/13.88  % (174604)Time elapsed: 2.442 s
% 89.86/13.88  % (174604)Peak memory usage: 152 MB
% 89.86/13.88  % (174604)Instructions burned: 2350 (million)
% 89.86/13.88  % (174633)------------------------------
% 89.86/13.88  % (174633)------------------------------
% 89.86/13.88  % (174637)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3741254640:i=134:gtgl=5:slsql=off:gtg=exists_sym_2961 on theBenchmark for (2961ds/134Mi)
% 89.86/13.88  % (174637)Instruction limit reached! 
% 89.86/13.88  % (174637)------------------------------
% 89.86/13.88  % (174637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174637)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174637)Termination reason: Instruction limit
% 89.86/13.88  % (174637)Termination phase: Saturation
% 89.86/13.88  % (174637)Time elapsed: 0.114 s
% 89.86/13.88  % (174637)Peak memory usage: 92 MB
% 89.86/13.88  % (174637)Instructions burned: 134 (million)
% 89.86/13.88  % (174640)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4083453783:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2958 on theBenchmark for (2958ds/141Mi)
% 89.86/13.88  % (174640)Refutation not found, incomplete strategy
% 89.86/13.88  % (174640)------------------------------
% 89.86/13.88  % (174640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174640)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174640)Termination reason: Refutation not found, incomplete strategy
% 89.86/13.88  % (174640)Time elapsed: 0.006 s
% 89.86/13.88  % (174640)Peak memory usage: 89 MB
% 89.86/13.88  % (174640)Instructions burned: 4 (million)
% 89.86/13.88  % (174642)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4085197854:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2957 on theBenchmark for (2957ds/431Mi)
% 89.86/13.88  % (174642)Refutation not found, incomplete strategy
% 89.86/13.88  % (174642)------------------------------
% 89.86/13.88  % (174642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174642)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174642)Termination reason: Refutation not found, incomplete strategy
% 89.86/13.88  % (174642)Time elapsed: 0.010 s
% 89.86/13.88  % (174642)Peak memory usage: 89 MB
% 89.86/13.88  % (174642)Instructions burned: 8 (million)
% 89.86/13.88  % (174617)Instruction limit reached! 
% 89.86/13.88  % (174617)------------------------------
% 89.86/13.88  % (174617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174617)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174617)Termination reason: Instruction limit
% 89.86/13.88  % (174617)Termination phase: Saturation
% 89.86/13.88  % (174617)Time elapsed: 2.861 s
% 89.86/13.88  % (174617)Peak memory usage: 159 MB
% 89.86/13.88  % (174617)Instructions burned: 5205 (million)
% 89.86/13.88  % (174640)------------------------------
% 89.86/13.88  % (174640)------------------------------
% 89.86/13.88  % (174642)------------------------------
% 89.86/13.88  % (174642)------------------------------
% 89.86/13.88  % (174647)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=1460309784:i=6060:aac=none:ins=25_2952 on theBenchmark for (2952ds/6060Mi)
% 89.86/13.88  % (174649)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=892598764:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2951 on theBenchmark for (2951ds/150Mi)
% 89.86/13.88  % (174649)Instruction limit reached! 
% 89.86/13.88  % (174649)------------------------------
% 89.86/13.88  % (174649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174649)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174649)Termination reason: Instruction limit
% 89.86/13.88  % (174649)Termination phase: Saturation
% 89.86/13.88  % (174649)Time elapsed: 0.128 s
% 89.86/13.88  % (174649)Peak memory usage: 91 MB
% 89.86/13.88  % (174649)Instructions burned: 151 (million)
% 89.86/13.88  % (174651)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1006749913:i=14155:bd=all_2950 on theBenchmark for (2950ds/14155Mi)
% 89.86/13.88  % (174654)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1842962695:i=667:av=off:fsr=off_2948 on theBenchmark for (2948ds/667Mi)
% 89.86/13.88  % (174654)Instruction limit reached! 
% 89.86/13.88  % (174654)------------------------------
% 89.86/13.88  % (174654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174654)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174654)Termination reason: Instruction limit
% 89.86/13.88  % (174654)Termination phase: Saturation
% 89.86/13.88  % (174654)Time elapsed: 0.533 s
% 89.86/13.88  % (174654)Peak memory usage: 99 MB
% 89.86/13.88  % (174654)Instructions burned: 667 (million)
% 89.86/13.88  % (174662)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=1459784838:s2a=on:i=185:s2at=1.8:fdi=4_2939 on theBenchmark for (2939ds/185Mi)
% 89.86/13.88  % (174662)Instruction limit reached! 
% 89.86/13.88  % (174662)------------------------------
% 89.86/13.88  % (174662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174662)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174662)Termination reason: Instruction limit
% 89.86/13.88  % (174662)Termination phase: Saturation
% 89.86/13.88  % (174662)Time elapsed: 0.093 s
% 89.86/13.88  % (174662)Peak memory usage: 91 MB
% 89.86/13.88  % (174662)Instructions burned: 185 (million)
% 89.86/13.88  % (174666)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2101833716:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2936 on theBenchmark for (2936ds/193Mi)
% 89.86/13.88  % (174666)Refutation not found, incomplete strategy
% 89.86/13.88  % (174666)------------------------------
% 89.86/13.88  % (174666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174666)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174666)Termination reason: Refutation not found, incomplete strategy
% 89.86/13.88  % (174666)Time elapsed: 0.010 s
% 89.86/13.88  % (174666)Peak memory usage: 89 MB
% 89.86/13.88  % (174666)Instructions burned: 8 (million)
% 89.86/13.88  % (174666)------------------------------
% 89.86/13.88  % (174666)------------------------------
% 89.86/13.88  % (174670)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3145558111:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2929 on theBenchmark for (2929ds/4850Mi)
% 89.86/13.88  % (174647)Instruction limit reached! 
% 89.86/13.88  % (174647)------------------------------
% 89.86/13.88  % (174647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174647)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174647)Termination reason: Instruction limit
% 89.86/13.88  % (174647)Termination phase: Saturation
% 89.86/13.88  % (174647)Time elapsed: 3.474 s
% 89.86/13.88  % (174647)Peak memory usage: 194 MB
% 89.86/13.88  % (174647)Instructions burned: 6060 (million)
% 89.86/13.88  % (174674)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3714657581:i=12111:sd=1:ss=included_2915 on theBenchmark for (2915ds/12111Mi)
% 89.86/13.88  % (174670)Instruction limit reached! 
% 89.86/13.88  % (174670)------------------------------
% 89.86/13.88  % (174670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174670)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174670)Termination reason: Instruction limit
% 89.86/13.88  % (174670)Termination phase: Saturation
% 89.86/13.88  % (174670)Time elapsed: 4.802 s
% 89.86/13.88  % (174670)Peak memory usage: 153 MB
% 89.86/13.88  % (174670)Instructions burned: 4851 (million)
% 89.86/13.88  % (174691)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3342021548:i=319:kws=precedence:fsr=off_2878 on theBenchmark for (2878ds/319Mi)
% 89.86/13.88  % (174583)First to succeed.
% 89.86/13.88  % (174583)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-174572"
% 89.86/13.88  % (174691)Instruction limit reached! 
% 89.86/13.88  % (174691)------------------------------
% 89.86/13.88  % (174691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174691)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174691)Termination reason: Instruction limit
% 89.86/13.88  % (174691)Termination phase: Saturation
% 89.86/13.88  % (174691)Time elapsed: 0.165 s
% 89.86/13.88  % (174691)Peak memory usage: 93 MB
% 89.86/13.88  % (174691)Instructions burned: 319 (million)
% 89.86/13.88  % (174759)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1781553490:i=2064:ep=RST_2875 on theBenchmark for (2875ds/2064Mi)
% 89.86/13.88  % (174759)Refutation not found, incomplete strategy
% 89.86/13.88  % (174759)------------------------------
% 89.86/13.88  % (174759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.86/13.88  % (174759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.86/13.88  % (174759)CaDiCaL version: 2.1.3
% 89.86/13.88  % (174759)Termination reason: Refutation not found, incomplete strategy
% 89.86/13.88  % (174759)Time elapsed: 0.052 s
% 89.86/13.88  % (174759)Peak memory usage: 91 MB
% 89.86/13.88  % (174759)Instructions burned: 115 (million)
% 89.86/13.88  % (174583)Refutation found. Thanks to Tanya!
% 89.86/13.88  % SZS status Theorem for theBenchmark
% 89.86/13.88  % SZS output start Proof for theBenchmark
% See solution above
% 90.76/14.05  % (174583)------------------------------
% 90.76/14.05  % (174583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.76/14.05  % (174583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.76/14.05  % (174583)CaDiCaL version: 2.1.3
% 90.76/14.05  % (174583)Termination reason: Refutation
% 90.76/14.05  % (174583)Time elapsed: 12.191 s
% 90.76/14.05  % (174583)Peak memory usage: 243 MB
% 90.76/14.05  % (174583)Instructions burned: 12453 (million)
% 90.76/14.05  % (174583)------------------------------
% 90.76/14.05  % (174583)------------------------------
% 90.76/14.05  % (174572)Success in time 12.731 s
% 90.76/14.05  % Vampire exiting
%------------------------------------------------------------------------------