%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM687+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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:16:28 PM UTC 2026
% Result : Theorem 26.22s 4.67s
% Output : Refutation 27.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 74
% Syntax : Number of formulae : 410 ( 68 unt; 43 def)
% Number of atoms : 1015 ( 22 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1060 ( 455 ~; 478 |; 46 &)
% ( 71 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 48 ( 46 usr; 44 prp; 0-2 aty)
% Number of functors : 43 ( 43 usr; 22 con; 0-2 aty)
% Number of variables : 268 ( 0 sgn 266 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X0),X1))
<=> pp(aa_bool_bool(scratc1226302079d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__lessis) ).
fof(f28,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__iii) ).
fof(f29,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f35,axiom,
! [X0] : scratc1358012602d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__pl) ).
fof(f53,axiom,
scratc1357553416d_n_is = scratc1838893055d_e_is(scratc42304593nd_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__is) ).
fof(f100,axiom,
! [X0] : scratc1838893055d_e_is(X0) = fequal_TPTP_ind,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__e__is) ).
fof(f110,axiom,
! [X0] : scratc1226302079d_l_or(X0) = aa_boo1142376798l_bool(scratc1784252nd_imp,scratc763077503_d_not(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__l__or) ).
fof(f115,axiom,
! [X0] :
( pp(scratc763077503_d_not(X0))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1784252nd_imp,X0),fFalse)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__not) ).
fof(f116,axiom,
scratc1784252nd_imp = fimplies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__imp) ).
fof(f147,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc1668156721_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f149,axiom,
pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_bv)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz21a) ).
fof(f162,axiom,
pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_dl)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz19j) ).
fof(f190,axiom,
pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_gd)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz13) ).
fof(f319,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_gd,X0))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_gc,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__36) ).
fof(f345,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_dl,X0))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__62) ).
fof(f358,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_bv,X0))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__75) ).
fof(f359,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__76) ).
fof(f380,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__97) ).
fof(f421,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dj(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__138) ).
fof(f434,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bt(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__151) ).
fof(f435,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__152) ).
fof(f491,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dj(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__208) ).
fof(f494,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bt(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__211) ).
fof(f495,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__212) ).
fof(f510,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__227) ).
fof(f513,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__230) ).
fof(f515,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__232) ).
fof(f536,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(f538,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(f541,axiom,
! [X0,X1] :
( ( gg_TPTP_ind(X0)
& gg_TPTP_ind(X1) )
=> ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1))
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fequal_1_1_fequal_001t__TPTP____Interpret__Oind_T) ).
fof(f545,conjecture,
pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_ad)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f546,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(negated_conjecture,[status(cth)],[f545]) ).
fof(f547,plain,
~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(flattening,[],[f546]) ).
fof(f564,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1668156721_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f147]) ).
fof(f565,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1668156721_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f564]) ).
fof(f629,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f380]) ).
fof(f683,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f510]) ).
fof(f684,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1)) ) ),
inference(flattening,[],[f683]) ).
fof(f689,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1)) ) ),
inference(ennf_transformation,[],[f513]) ).
fof(f690,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1)) ) ),
inference(flattening,[],[f689]) ).
fof(f693,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)) ) ),
inference(ennf_transformation,[],[f515]) ).
fof(f694,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)) ) ),
inference(flattening,[],[f693]) ).
fof(f705,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(ennf_transformation,[],[f541]) ).
fof(f706,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(flattening,[],[f705]) ).
fof(f707,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X0),X1))
| ~ pp(aa_bool_bool(scratc1226302079d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1))) )
& ( pp(aa_bool_bool(scratc1226302079d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X0),X1)) ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f710,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f711,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f751,plain,
! [X0] :
( ( pp(scratc763077503_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1784252nd_imp,X0),fFalse)) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1784252nd_imp,X0),fFalse))
| ~ pp(scratc763077503_d_not(X0)) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f774,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1668156721_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1668156721_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f565]) ).
fof(f775,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1668156721_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1668156721_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1)) ) ),
inference(rectify,[],[f774]) ).
fof(f776,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc1668156721_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1668156721_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f775]) ).
fof(f831,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_gd,X0))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_gc,X0))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_gc,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_gd,X0)) ) ),
inference(nnf_transformation,[],[f319]) ).
fof(f857,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dl,X0))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,X0))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dl,X0)) ) ),
inference(nnf_transformation,[],[f345]) ).
fof(f870,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_bv,X0))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu,X0))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bv,X0)) ) ),
inference(nnf_transformation,[],[f358]) ).
fof(f871,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0)) ) ),
inference(nnf_transformation,[],[f359]) ).
fof(f898,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,X0),X1)) ) ),
inference(nnf_transformation,[],[f629]) ).
fof(f899,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,X0),X1)) ) ),
inference(flattening,[],[f898]) ).
fof(f948,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dj(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dj(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1)) ) ),
inference(nnf_transformation,[],[f421]) ).
fof(f961,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bt(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bt(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu,X0),X1)) ) ),
inference(nnf_transformation,[],[f434]) ).
fof(f962,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1)) ) ),
inference(nnf_transformation,[],[f435]) ).
fof(f1044,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dj(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dj(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f491]) ).
fof(f1047,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bt(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bt(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f494]) ).
fof(f1048,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f495]) ).
fof(f1067,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f684]) ).
fof(f1068,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f1067]) ).
fof(f1073,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f690]) ).
fof(f1074,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f1073]) ).
fof(f1077,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f694]) ).
fof(f1078,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f1077]) ).
fof(f1118,plain,
! [X0,X1] :
( pp(aa_bool_bool(scratc1226302079d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X0),X1)) ),
inference(cnf_transformation,[],[f707]) ).
fof(f1124,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f710]) ).
fof(f1125,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X1),X0))) ),
inference(cnf_transformation,[],[f710]) ).
fof(f1126,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f711]) ).
fof(f1127,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(X0),X1))) ),
inference(cnf_transformation,[],[f711]) ).
fof(f1138,plain,
! [X0] : scratc1358012602d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,X0)),
inference(cnf_transformation,[],[f35]) ).
fof(f1164,plain,
scratc1357553416d_n_is = scratc1838893055d_e_is(scratc42304593nd_nat),
inference(cnf_transformation,[],[f53]) ).
fof(f1228,plain,
! [X0] : scratc1838893055d_e_is(X0) = fequal_TPTP_ind,
inference(cnf_transformation,[],[f100]) ).
fof(f1242,plain,
! [X0] : aa_boo1142376798l_bool(scratc1784252nd_imp,scratc763077503_d_not(X0)) = scratc1226302079d_l_or(X0),
inference(cnf_transformation,[],[f110]) ).
fof(f1249,plain,
! [X0] :
( pp(scratc763077503_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1784252nd_imp,X0),fFalse)) ),
inference(cnf_transformation,[],[f751]) ).
fof(f1250,plain,
scratc1784252nd_imp = fimplies,
inference(cnf_transformation,[],[f116]) ).
fof(f1312,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1668156721_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1)) ),
inference(cnf_transformation,[],[f776]) ).
fof(f1313,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f776]) ).
fof(f1314,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
| scratc1668156721_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f776]) ).
fof(f1315,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f776]) ).
fof(f1318,plain,
pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_bv)),
inference(cnf_transformation,[],[f149]) ).
fof(f1331,plain,
pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_dl)),
inference(cnf_transformation,[],[f162]) ).
fof(f1359,plain,
pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_gd)),
inference(cnf_transformation,[],[f190]) ).
fof(f1553,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_gc,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_gd,X0)) ),
inference(cnf_transformation,[],[f831]) ).
fof(f1605,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dl,X0)) ),
inference(cnf_transformation,[],[f857]) ).
fof(f1631,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bv,X0)) ),
inference(cnf_transformation,[],[f870]) ).
fof(f1634,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
inference(cnf_transformation,[],[f871]) ).
fof(f1679,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,X0),X1)) ),
inference(cnf_transformation,[],[f899]) ).
fof(f1770,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dj(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1)) ),
inference(cnf_transformation,[],[f948]) ).
fof(f1796,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bt(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu,X0),X1)) ),
inference(cnf_transformation,[],[f961]) ).
fof(f1799,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
inference(cnf_transformation,[],[f962]) ).
fof(f1942,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dj(X0),X1),X2)) ),
inference(cnf_transformation,[],[f1044]) ).
fof(f1948,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bt(X0),X1),X2)) ),
inference(cnf_transformation,[],[f1047]) ).
fof(f1951,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
inference(cnf_transformation,[],[f1048]) ).
fof(f1989,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,X0),X1)) ),
inference(cnf_transformation,[],[f1068]) ).
fof(f1990,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,X2),X3)) ),
inference(cnf_transformation,[],[f1068]) ).
fof(f1991,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3))) ),
inference(cnf_transformation,[],[f1068]) ).
fof(f2000,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3)) ),
inference(cnf_transformation,[],[f1074]) ).
fof(f2008,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1358012602d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3)) ),
inference(cnf_transformation,[],[f1078]) ).
fof(f2050,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
inference(cnf_transformation,[],[f536]) ).
fof(f2052,plain,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f538]) ).
fof(f2055,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(cnf_transformation,[],[f706]) ).
fof(f2059,plain,
~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(cnf_transformation,[],[f547]) ).
fof(f2062,plain,
! [X0] : scratc1226302079d_l_or(X0) = aa_boo1142376798l_bool(fimplies,scratc763077503_d_not(X0)),
inference(definition_unfolding,[],[f1242,f1250]) ).
fof(f2066,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc763077503_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,X0),X1)) ),
inference(definition_unfolding,[],[f1118,f2062]) ).
fof(f2084,plain,
scratc1357553416d_n_is = fequal_TPTP_ind,
inference(definition_unfolding,[],[f1164,f1228]) ).
fof(f2111,plain,
! [X0] :
( pp(scratc763077503_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse)) ),
inference(definition_unfolding,[],[f1249,f1250]) ).
fof(f2222,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,X1)),X3))) ),
inference(definition_unfolding,[],[f1991,f1138,f1138]) ).
fof(f2229,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,X1)),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(X0),X1),X2),X3)) ),
inference(definition_unfolding,[],[f2000,f1138,f1138]) ).
fof(f2233,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,X1)),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(X0),X1),X2),X3)) ),
inference(definition_unfolding,[],[f2008,f1138,f1138]) ).
fof(f2265,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_ad)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f2267,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_ad))
| spl29_1 ),
inference(avatar_component_clause,[],[f2265]) ).
fof(f2268,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f2059,f2265]) ).
fof(f2269,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
| spl29_1 ),
inference(resolution,[],[f2267,f1313]) ).
fof(f2270,plain,
( scratc1668156721_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f2267,f1314]) ).
fof(f2271,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_1 ),
inference(resolution,[],[f2267,f1315]) ).
fof(f2284,definition,
( spl29_2
<=> scratc1668156721_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f2286,plain,
( scratc1668156721_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f2284]) ).
fof(f2287,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f2270,f2265,f2284]) ).
fof(f2289,definition,
( spl29_3
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f2291,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_3 ),
inference(avatar_component_clause,[],[f2289]) ).
fof(f2292,plain,
( ~ spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f2271,f2265,f2289]) ).
fof(f2293,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_3 ),
inference(resolution,[],[f2291,f1634]) ).
fof(f2331,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f2286,f1312]) ).
fof(f2332,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),X0)) )
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f2331,f2269]) ).
fof(f2334,definition,
( spl29_4
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f2335,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),X0)) )
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f2334]) ).
fof(f2336,plain,
( spl29_4
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f2332,f2284,f2265,f2334]) ).
fof(f2710,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_dl))
| pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_4 ),
inference(resolution,[],[f2335,f1605]) ).
fof(f2738,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_gd))
| pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_gc,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_4 ),
inference(resolution,[],[f2335,f1553]) ).
fof(f2816,plain,
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_gc,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_4 ),
inference(forward_subsumption_resolution,[],[f2738,f1359]) ).
fof(f2844,plain,
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_4 ),
inference(forward_subsumption_resolution,[],[f2710,f1331]) ).
fof(f2921,definition,
( spl29_5
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad)) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f2923,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
| ~ spl29_5 ),
inference(avatar_component_clause,[],[f2921]) ).
fof(f2924,plain,
( spl29_5
| spl29_1 ),
inference(avatar_split_clause,[],[f2269,f2265,f2921]) ).
fof(f2926,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
fof(f2928,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_6 ),
inference(avatar_component_clause,[],[f2926]) ).
fof(f2929,plain,
( ~ spl29_6
| spl29_3 ),
inference(avatar_split_clause,[],[f2293,f2289,f2926]) ).
fof(f2931,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_6 ),
inference(resolution,[],[f2928,f1313]) ).
fof(f2932,plain,
( scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a)
| spl29_6 ),
inference(resolution,[],[f2928,f1314]) ).
fof(f2933,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_6 ),
inference(resolution,[],[f2928,f1315]) ).
fof(f2946,definition,
( spl29_7
<=> scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
fof(f2948,plain,
( scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a)
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f2946]) ).
fof(f2949,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f2932,f2926,f2946]) ).
fof(f2951,definition,
( spl29_8
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))) ),
introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).
fof(f2953,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_8 ),
inference(avatar_component_clause,[],[f2951]) ).
fof(f2954,plain,
( ~ spl29_8
| spl29_6 ),
inference(avatar_split_clause,[],[f2933,f2926,f2951]) ).
fof(f2955,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl29_8 ),
inference(resolution,[],[f2953,f1799]) ).
fof(f3001,definition,
( spl29_9
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f3003,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl29_9 ),
inference(avatar_component_clause,[],[f3001]) ).
fof(f3004,plain,
( ~ spl29_9
| spl29_8 ),
inference(avatar_split_clause,[],[f2955,f2951,f3001]) ).
fof(f3006,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl29_9 ),
inference(resolution,[],[f3003,f1313]) ).
fof(f3007,plain,
( scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
| spl29_9 ),
inference(resolution,[],[f3003,f1314]) ).
fof(f3008,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_9 ),
inference(resolution,[],[f3003,f1315]) ).
fof(f3021,definition,
( spl29_10
<=> scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_10])],[avatar_definition]) ).
fof(f3023,plain,
( scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
| ~ spl29_10 ),
inference(avatar_component_clause,[],[f3021]) ).
fof(f3024,plain,
( spl29_10
| spl29_9 ),
inference(avatar_split_clause,[],[f3007,f3001,f3021]) ).
fof(f3029,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f2948,f1312]) ).
fof(f3030,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f3029,f2931]) ).
fof(f3032,definition,
( spl29_11
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f3033,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),X0)) )
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f3032]) ).
fof(f3034,plain,
( spl29_11
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f3030,f2946,f2926,f3032]) ).
fof(f3396,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aTP_Lamm_bv))
| pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl29_11 ),
inference(resolution,[],[f3033,f1631]) ).
fof(f3555,plain,
( pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f3396,f1318]) ).
fof(f3623,definition,
( spl29_13
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f3625,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_13 ),
inference(avatar_component_clause,[],[f3623]) ).
fof(f3626,plain,
( spl29_13
| spl29_6 ),
inference(avatar_split_clause,[],[f2931,f2926,f3623]) ).
fof(f3790,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| sK12(aTP_Lamm_a,aTP_Lamm_ad) = X0
| ~ gg_TPTP_ind(X0) )
| ~ spl29_5 ),
inference(resolution,[],[f2923,f2055]) ).
fof(f3805,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| sK12(aTP_Lamm_a,aTP_Lamm_ad) = X0
| ~ gg_TPTP_ind(X0) )
| ~ spl29_5 ),
inference(forward_demodulation,[],[f3790,f2084]) ).
fof(f3810,definition,
( spl29_15
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))) ),
introduced(definition,[new_symbols(definition,[spl29_15])],[avatar_definition]) ).
fof(f3812,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_15 ),
inference(avatar_component_clause,[],[f3810]) ).
fof(f3813,plain,
( ~ spl29_15
| spl29_9 ),
inference(avatar_split_clause,[],[f3008,f3001,f3810]) ).
fof(f3814,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_15 ),
inference(resolution,[],[f3812,f1951]) ).
fof(f3860,definition,
( spl29_16
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_16])],[avatar_definition]) ).
fof(f3862,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_16 ),
inference(avatar_component_clause,[],[f3860]) ).
fof(f3863,plain,
( ~ spl29_16
| spl29_15 ),
inference(avatar_split_clause,[],[f3814,f3810,f3860]) ).
fof(f3865,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_16 ),
inference(resolution,[],[f3862,f1313]) ).
fof(f3866,plain,
( scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a)
| spl29_16 ),
inference(resolution,[],[f3862,f1314]) ).
fof(f3867,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_16 ),
inference(resolution,[],[f3862,f1315]) ).
fof(f3880,definition,
( spl29_17
<=> scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_17])],[avatar_definition]) ).
fof(f3882,plain,
( scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a)
| ~ spl29_17 ),
inference(avatar_component_clause,[],[f3880]) ).
fof(f3883,plain,
( spl29_17
| spl29_16 ),
inference(avatar_split_clause,[],[f3866,f3860,f3880]) ).
fof(f3895,definition,
( spl29_19
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_19])],[avatar_definition]) ).
fof(f3897,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_19 ),
inference(avatar_component_clause,[],[f3895]) ).
fof(f3898,plain,
( ~ spl29_19
| spl29_16 ),
inference(avatar_split_clause,[],[f3867,f3860,f3895]) ).
fof(f3899,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_19 ),
inference(resolution,[],[f3897,f1989]) ).
fof(f3900,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_19 ),
inference(resolution,[],[f3897,f1990]) ).
fof(f3901,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| spl29_19 ),
inference(resolution,[],[f3897,f2222]) ).
fof(f3947,definition,
( spl29_20
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).
fof(f3949,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| spl29_20 ),
inference(avatar_component_clause,[],[f3947]) ).
fof(f3950,plain,
( ~ spl29_20
| spl29_19 ),
inference(avatar_split_clause,[],[f3901,f3895,f3947]) ).
fof(f3955,plain,
( ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))))
| spl29_20 ),
inference(resolution,[],[f3949,f1127]) ).
fof(f4261,definition,
( spl29_28
<=> pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) ),
introduced(definition,[new_symbols(definition,[spl29_28])],[avatar_definition]) ).
fof(f4262,plain,
( pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl29_28 ),
inference(avatar_component_clause,[],[f4261]) ).
fof(f4263,plain,
( ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl29_28 ),
inference(avatar_component_clause,[],[f4261]) ).
fof(f4266,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_28 ),
inference(resolution,[],[f4263,f1124]) ).
fof(f4385,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ spl29_28 ),
inference(resolution,[],[f4262,f1125]) ).
fof(f4541,definition,
( spl29_32
<=> pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_32])],[avatar_definition]) ).
fof(f4543,plain,
( ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))))
| spl29_32 ),
inference(avatar_component_clause,[],[f4541]) ).
fof(f4544,plain,
( ~ spl29_32
| spl29_20 ),
inference(avatar_split_clause,[],[f3955,f3947,f4541]) ).
fof(f4546,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_32 ),
inference(resolution,[],[f4543,f1124]) ).
fof(f4605,definition,
( spl29_35
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_35])],[avatar_definition]) ).
fof(f4607,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_35 ),
inference(avatar_component_clause,[],[f4605]) ).
fof(f4608,plain,
( ~ spl29_35
| spl29_32 ),
inference(avatar_split_clause,[],[f4546,f4541,f4605]) ).
fof(f4609,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_35 ),
inference(resolution,[],[f4607,f2233]) ).
fof(f4679,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ spl29_28
| spl29_35 ),
inference(forward_subsumption_resolution,[],[f4609,f4385]) ).
fof(f4682,definition,
( spl29_36
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))) ),
introduced(definition,[new_symbols(definition,[spl29_36])],[avatar_definition]) ).
fof(f4684,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_36 ),
inference(avatar_component_clause,[],[f4682]) ).
fof(f4686,definition,
( spl29_37
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))) ),
introduced(definition,[new_symbols(definition,[spl29_37])],[avatar_definition]) ).
fof(f4687,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ spl29_37 ),
inference(avatar_component_clause,[],[f4686]) ).
fof(f4688,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_37 ),
inference(avatar_component_clause,[],[f4686]) ).
fof(f4689,plain,
( ~ spl29_36
| ~ spl29_37
| ~ spl29_28
| spl29_35 ),
inference(avatar_split_clause,[],[f4679,f4605,f4261,f4686,f4682]) ).
fof(f4702,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) )
| spl29_36 ),
inference(resolution,[],[f4684,f1312]) ).
fof(f4736,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) )
| spl29_9
| spl29_36 ),
inference(forward_subsumption_resolution,[],[f4702,f3006]) ).
fof(f4739,definition,
( spl29_38
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))) ),
introduced(definition,[new_symbols(definition,[spl29_38])],[avatar_definition]) ).
fof(f4740,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ spl29_38 ),
inference(avatar_component_clause,[],[f4739]) ).
fof(f4741,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_38 ),
inference(avatar_component_clause,[],[f4739]) ).
fof(f4743,definition,
( spl29_39
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_39])],[avatar_definition]) ).
fof(f4744,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ spl29_39 ),
inference(avatar_component_clause,[],[f4743]) ).
fof(f4745,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_39 ),
inference(avatar_component_clause,[],[f4743]) ).
fof(f4852,definition,
( spl29_42
<=> ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_42])],[avatar_definition]) ).
fof(f4853,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bs(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0) )
| ~ spl29_42 ),
inference(avatar_component_clause,[],[f4852]) ).
fof(f4854,plain,
( spl29_42
| spl29_9
| spl29_36 ),
inference(avatar_split_clause,[],[f4736,f4682,f3001,f4852]) ).
fof(f4857,plain,
( ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| spl29_37 ),
inference(resolution,[],[f4688,f1125]) ).
fof(f4974,definition,
( spl29_44
<=> pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_44])],[avatar_definition]) ).
fof(f4976,plain,
( ~ pp(aa_fun171081125l_bool(scratc456433586n_some,aa_TPT43085870d_bool(scratc702456632ffprop(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| spl29_44 ),
inference(avatar_component_clause,[],[f4974]) ).
fof(f4977,plain,
( ~ spl29_44
| spl29_37 ),
inference(avatar_split_clause,[],[f4857,f4686,f4974]) ).
fof(f4978,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc577704507_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_44 ),
inference(resolution,[],[f4976,f1126]) ).
fof(f4991,plain,
( $false
| spl29_19
| spl29_44 ),
inference(forward_subsumption_resolution,[],[f4978,f3900]) ).
fof(f4992,plain,
( spl29_19
| spl29_44 ),
inference(avatar_contradiction_clause,[],[f4991]) ).
fof(f5145,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) )
| spl29_38 ),
inference(resolution,[],[f4741,f1312]) ).
fof(f5179,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) )
| spl29_9
| spl29_38 ),
inference(forward_subsumption_resolution,[],[f5145,f3006]) ).
fof(f5181,definition,
( spl29_46
<=> ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_46])],[avatar_definition]) ).
fof(f5182,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_di(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0) )
| ~ spl29_46 ),
inference(avatar_component_clause,[],[f5181]) ).
fof(f5183,plain,
( spl29_46
| spl29_9
| spl29_38 ),
inference(avatar_split_clause,[],[f5179,f4739,f3001,f5181]) ).
fof(f5238,plain,
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ spl29_42 ),
inference(resolution,[],[f4853,f1948]) ).
fof(f5254,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ spl29_10
| ~ spl29_42 ),
inference(forward_subsumption_resolution,[],[f5238,f3023]) ).
fof(f5256,definition,
( spl29_47
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_47])],[avatar_definition]) ).
fof(f5258,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_47 ),
inference(avatar_component_clause,[],[f5256]) ).
fof(f5259,plain,
( ~ spl29_47
| ~ spl29_10
| ~ spl29_42 ),
inference(avatar_split_clause,[],[f5254,f4852,f3021,f5256]) ).
fof(f5270,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| spl29_47 ),
inference(resolution,[],[f5258,f1312]) ).
fof(f5304,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| spl29_16
| spl29_47 ),
inference(forward_subsumption_resolution,[],[f5270,f3865]) ).
fof(f5322,definition,
( spl29_49
<=> ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ) ),
introduced(definition,[new_symbols(definition,[spl29_49])],[avatar_definition]) ).
fof(f5323,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| ~ spl29_49 ),
inference(avatar_component_clause,[],[f5322]) ).
fof(f5324,plain,
( spl29_49
| spl29_16
| spl29_47 ),
inference(avatar_split_clause,[],[f5304,f5256,f3860,f5322]) ).
fof(f5968,definition,
( spl29_56
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_56])],[avatar_definition]) ).
fof(f5970,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_56 ),
inference(avatar_component_clause,[],[f5968]) ).
fof(f5971,plain,
( ~ spl29_56
| spl29_28 ),
inference(avatar_split_clause,[],[f4266,f4261,f5968]) ).
fof(f6179,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1962783167bnd_ap,aa_TPTP_ind_TPTP_ind(scratc94756010d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ spl29_38 ),
inference(resolution,[],[f4740,f2229]) ).
fof(f6297,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_17
| ~ spl29_49 ),
inference(resolution,[],[f5323,f3882]) ).
fof(f6300,definition,
( spl29_62
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_62])],[avatar_definition]) ).
fof(f6302,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bt(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_62 ),
inference(avatar_component_clause,[],[f6300]) ).
fof(f6303,plain,
( ~ spl29_62
| ~ spl29_17
| ~ spl29_49 ),
inference(avatar_split_clause,[],[f6297,f5322,f3880,f6300]) ).
fof(f6889,definition,
( spl29_63
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_63])],[avatar_definition]) ).
fof(f6891,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ spl29_63 ),
inference(avatar_component_clause,[],[f6889]) ).
fof(f6892,plain,
( spl29_63
| spl29_16 ),
inference(avatar_split_clause,[],[f3865,f3860,f6889]) ).
fof(f6894,definition,
( spl29_64
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))) ),
introduced(definition,[new_symbols(definition,[spl29_64])],[avatar_definition]) ).
fof(f6896,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc593358831moreis,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ spl29_64 ),
inference(avatar_component_clause,[],[f6894]) ).
fof(f6897,plain,
( spl29_64
| spl29_19 ),
inference(avatar_split_clause,[],[f3899,f3895,f6894]) ).
fof(f6898,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ spl29_64 ),
inference(resolution,[],[f6896,f1679]) ).
fof(f7117,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_62 ),
inference(resolution,[],[f6302,f1796]) ).
fof(f7234,definition,
( spl29_74
<=> ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| sK12(aTP_Lamm_a,aTP_Lamm_ad) = X0
| ~ gg_TPTP_ind(X0) ) ),
introduced(definition,[new_symbols(definition,[spl29_74])],[avatar_definition]) ).
fof(f7235,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,X0),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| sK12(aTP_Lamm_a,aTP_Lamm_ad) = X0
| ~ gg_TPTP_ind(X0) )
| ~ spl29_74 ),
inference(avatar_component_clause,[],[f7234]) ).
fof(f7236,plain,
( spl29_74
| ~ spl29_5 ),
inference(avatar_split_clause,[],[f3805,f2921,f7234]) ).
fof(f7725,definition,
( spl29_81
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))) ),
introduced(definition,[new_symbols(definition,[spl29_81])],[avatar_definition]) ).
fof(f7727,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_gc,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_81 ),
inference(avatar_component_clause,[],[f7725]) ).
fof(f7729,definition,
( spl29_82
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_82])],[avatar_definition]) ).
fof(f7731,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc459375219lessis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ spl29_82 ),
inference(avatar_component_clause,[],[f7729]) ).
fof(f7732,plain,
( ~ spl29_81
| spl29_82
| ~ spl29_64 ),
inference(avatar_split_clause,[],[f6898,f6894,f7729,f7725]) ).
fof(f7741,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_gc,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_11
| spl29_81 ),
inference(resolution,[],[f7727,f3033]) ).
fof(f7780,plain,
( $false
| ~ spl29_4
| ~ spl29_11
| spl29_81 ),
inference(forward_subsumption_resolution,[],[f7741,f2816]) ).
fof(f7781,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_81 ),
inference(avatar_contradiction_clause,[],[f7780]) ).
fof(f7791,plain,
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc763077503_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_82 ),
inference(resolution,[],[f7731,f2066]) ).
fof(f8840,plain,
( ! [X0] : pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))),X0))
| spl29_56 ),
inference(resolution,[],[f5970,f2052]) ).
fof(f9378,definition,
( spl29_102
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc763077503_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_102])],[avatar_definition]) ).
fof(f9380,plain,
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc763077503_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_102 ),
inference(avatar_component_clause,[],[f9378]) ).
fof(f9381,plain,
( spl29_102
| ~ spl29_82 ),
inference(avatar_split_clause,[],[f7791,f7729,f9378]) ).
fof(f9434,plain,
( ~ pp(scratc763077503_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ spl29_102 ),
inference(resolution,[],[f9380,f2050]) ).
fof(f9444,plain,
( ~ pp(scratc763077503_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_39
| ~ spl29_102 ),
inference(forward_subsumption_resolution,[],[f9434,f4745]) ).
fof(f9446,definition,
( spl29_105
<=> pp(scratc763077503_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_105])],[avatar_definition]) ).
fof(f9448,plain,
( ~ pp(scratc763077503_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_105 ),
inference(avatar_component_clause,[],[f9446]) ).
fof(f9449,plain,
( ~ spl29_105
| spl29_39
| ~ spl29_102 ),
inference(avatar_split_clause,[],[f9444,f9378,f4743,f9446]) ).
fof(f9453,plain,
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))),fFalse))
| spl29_105 ),
inference(resolution,[],[f9448,f2111]) ).
fof(f9465,plain,
( $false
| spl29_56
| spl29_105 ),
inference(forward_subsumption_resolution,[],[f9453,f8840]) ).
fof(f9466,plain,
( spl29_56
| spl29_105 ),
inference(avatar_contradiction_clause,[],[f9465]) ).
fof(f9474,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1521849nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_35
| ~ spl29_38 ),
inference(forward_subsumption_resolution,[],[f6179,f4607]) ).
fof(f9476,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1357553416d_n_is,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_35
| ~ spl29_37
| ~ spl29_38 ),
inference(forward_subsumption_resolution,[],[f9474,f4687]) ).
fof(f9528,plain,
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ spl29_46 ),
inference(resolution,[],[f5182,f1942]) ).
fof(f9544,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ spl29_10
| ~ spl29_46 ),
inference(forward_subsumption_resolution,[],[f9528,f3023]) ).
fof(f9546,definition,
( spl29_106
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_106])],[avatar_definition]) ).
fof(f9548,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_106 ),
inference(avatar_component_clause,[],[f9546]) ).
fof(f9549,plain,
( ~ spl29_106
| ~ spl29_10
| ~ spl29_46 ),
inference(avatar_split_clause,[],[f9544,f5181,f3021,f9546]) ).
fof(f9560,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| spl29_106 ),
inference(resolution,[],[f9548,f1312]) ).
fof(f9594,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| ~ spl29_63
| spl29_106 ),
inference(forward_subsumption_resolution,[],[f9560,f6891]) ).
fof(f9596,definition,
( spl29_107
<=> ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ) ),
introduced(definition,[new_symbols(definition,[spl29_107])],[avatar_definition]) ).
fof(f9597,plain,
( ! [X0] :
( ~ scratc1668156721_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc601948136all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| ~ spl29_107 ),
inference(avatar_component_clause,[],[f9596]) ).
fof(f9598,plain,
( spl29_107
| ~ spl29_63
| spl29_106 ),
inference(avatar_split_clause,[],[f9594,f9546,f6889,f9596]) ).
fof(f9599,plain,
( sK12(aTP_Lamm_a,aTP_Lamm_ad) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_39
| ~ spl29_74 ),
inference(resolution,[],[f4744,f7235]) ).
fof(f9642,plain,
( sK12(aTP_Lamm_a,aTP_Lamm_ad) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ spl29_13
| ~ spl29_39
| ~ spl29_74 ),
inference(forward_subsumption_resolution,[],[f9599,f3625]) ).
fof(f9644,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_17
| ~ spl29_107 ),
inference(resolution,[],[f9597,f3882]) ).
fof(f9647,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_13
| ~ spl29_17
| ~ spl29_39
| ~ spl29_74
| ~ spl29_107 ),
inference(forward_demodulation,[],[f9644,f9642]) ).
fof(f9652,definition,
( spl29_108
<=> pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_108])],[avatar_definition]) ).
fof(f9654,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dj(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_108 ),
inference(avatar_component_clause,[],[f9652]) ).
fof(f9655,plain,
( ~ spl29_108
| ~ spl29_13
| ~ spl29_17
| ~ spl29_39
| ~ spl29_74
| ~ spl29_107 ),
inference(avatar_split_clause,[],[f9647,f9596,f7234,f4743,f3880,f3623,f9652]) ).
fof(f9656,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_108 ),
inference(resolution,[],[f9654,f1770]) ).
fof(f11743,plain,
( ~ spl29_39
| spl29_35
| ~ spl29_37
| ~ spl29_38 ),
inference(avatar_split_clause,[],[f9476,f4739,f4686,f4605,f4743]) ).
fof(f20218,definition,
( spl29_127
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_127])],[avatar_definition]) ).
fof(f20220,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_127 ),
inference(avatar_component_clause,[],[f20218]) ).
fof(f20221,plain,
( ~ spl29_127
| spl29_108 ),
inference(avatar_split_clause,[],[f9656,f9652,f20218]) ).
fof(f20313,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_4
| spl29_127 ),
inference(resolution,[],[f20220,f2335]) ).
fof(f20314,plain,
( $false
| ~ spl29_4
| spl29_127 ),
inference(forward_subsumption_resolution,[],[f20313,f2844]) ).
fof(f20315,plain,
( ~ spl29_4
| spl29_127 ),
inference(avatar_contradiction_clause,[],[f20314]) ).
fof(f20467,definition,
( spl29_158
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_158])],[avatar_definition]) ).
fof(f20469,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_158 ),
inference(avatar_component_clause,[],[f20467]) ).
fof(f20470,plain,
( ~ spl29_158
| spl29_62 ),
inference(avatar_split_clause,[],[f7117,f6300,f20467]) ).
fof(f21007,plain,
( ~ pp(aa_fun171081125l_bool(scratc601948136all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl29_4
| spl29_158 ),
inference(resolution,[],[f20469,f2335]) ).
fof(f21008,plain,
( $false
| ~ spl29_4
| ~ spl29_11
| spl29_158 ),
inference(forward_subsumption_resolution,[],[f21007,f3555]) ).
fof(f21009,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_158 ),
inference(avatar_contradiction_clause,[],[f21008]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f2268]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f2287]) ).
cnf(s3,plain,
( spl29_1
| ~ spl29_3 ),
inference(sat_conversion,[],[f2292]) ).
cnf(s4,plain,
( spl29_1
| ~ spl29_2
| spl29_4 ),
inference(sat_conversion,[],[f2336]) ).
cnf(s5,plain,
( spl29_1
| spl29_5 ),
inference(sat_conversion,[],[f2924]) ).
cnf(s6,plain,
( spl29_3
| ~ spl29_6 ),
inference(sat_conversion,[],[f2929]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f2949]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_8 ),
inference(sat_conversion,[],[f2954]) ).
cnf(s9,plain,
( spl29_8
| ~ spl29_9 ),
inference(sat_conversion,[],[f3004]) ).
cnf(s10,plain,
( spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f3024]) ).
cnf(s11,plain,
( spl29_6
| ~ spl29_7
| spl29_11 ),
inference(sat_conversion,[],[f3034]) ).
cnf(s13,plain,
( spl29_6
| spl29_13 ),
inference(sat_conversion,[],[f3626]) ).
cnf(s15,plain,
( spl29_9
| ~ spl29_15 ),
inference(sat_conversion,[],[f3813]) ).
cnf(s16,plain,
( spl29_15
| ~ spl29_16 ),
inference(sat_conversion,[],[f3863]) ).
cnf(s17,plain,
( spl29_16
| spl29_17 ),
inference(sat_conversion,[],[f3883]) ).
cnf(s19,plain,
( spl29_16
| ~ spl29_19 ),
inference(sat_conversion,[],[f3898]) ).
cnf(s20,plain,
( spl29_19
| ~ spl29_20 ),
inference(sat_conversion,[],[f3950]) ).
cnf(s31,plain,
( spl29_20
| ~ spl29_32 ),
inference(sat_conversion,[],[f4544]) ).
cnf(s34,plain,
( spl29_32
| ~ spl29_35 ),
inference(sat_conversion,[],[f4608]) ).
cnf(s35,plain,
( ~ spl29_28
| spl29_35
| ~ spl29_36
| ~ spl29_37 ),
inference(sat_conversion,[],[f4689]) ).
cnf(s38,plain,
( spl29_9
| spl29_36
| spl29_42 ),
inference(sat_conversion,[],[f4854]) ).
cnf(s41,plain,
( spl29_37
| ~ spl29_44 ),
inference(sat_conversion,[],[f4977]) ).
cnf(s42,plain,
( spl29_19
| spl29_44 ),
inference(sat_conversion,[],[f4992]) ).
cnf(s45,plain,
( spl29_9
| spl29_38
| spl29_46 ),
inference(sat_conversion,[],[f5183]) ).
cnf(s46,plain,
( ~ spl29_10
| ~ spl29_42
| ~ spl29_47 ),
inference(sat_conversion,[],[f5259]) ).
cnf(s48,plain,
( spl29_16
| spl29_47
| spl29_49 ),
inference(sat_conversion,[],[f5324]) ).
cnf(s59,plain,
( spl29_28
| ~ spl29_56 ),
inference(sat_conversion,[],[f5971]) ).
cnf(s69,plain,
( ~ spl29_17
| ~ spl29_49
| ~ spl29_62 ),
inference(sat_conversion,[],[f6303]) ).
cnf(s70,plain,
( spl29_16
| spl29_63 ),
inference(sat_conversion,[],[f6892]) ).
cnf(s71,plain,
( spl29_19
| spl29_64 ),
inference(sat_conversion,[],[f6897]) ).
cnf(s81,plain,
( ~ spl29_5
| spl29_74 ),
inference(sat_conversion,[],[f7236]) ).
cnf(s89,plain,
( ~ spl29_64
| ~ spl29_81
| spl29_82 ),
inference(sat_conversion,[],[f7732]) ).
cnf(s90,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_81 ),
inference(sat_conversion,[],[f7781]) ).
cnf(s119,plain,
( ~ spl29_82
| spl29_102 ),
inference(sat_conversion,[],[f9381]) ).
cnf(s122,plain,
( spl29_39
| ~ spl29_102
| ~ spl29_105 ),
inference(sat_conversion,[],[f9449]) ).
cnf(s123,plain,
( spl29_56
| spl29_105 ),
inference(sat_conversion,[],[f9466]) ).
cnf(s126,plain,
( ~ spl29_10
| ~ spl29_46
| ~ spl29_106 ),
inference(sat_conversion,[],[f9549]) ).
cnf(s127,plain,
( ~ spl29_63
| spl29_106
| spl29_107 ),
inference(sat_conversion,[],[f9598]) ).
cnf(s128,plain,
( ~ spl29_13
| ~ spl29_17
| ~ spl29_39
| ~ spl29_74
| ~ spl29_107
| ~ spl29_108 ),
inference(sat_conversion,[],[f9655]) ).
cnf(s411,plain,
( spl29_35
| ~ spl29_37
| ~ spl29_38
| ~ spl29_39 ),
inference(sat_conversion,[],[f11743]) ).
cnf(s1535,plain,
( spl29_108
| ~ spl29_127 ),
inference(sat_conversion,[],[f20221]) ).
cnf(s1551,plain,
( ~ spl29_4
| spl29_127 ),
inference(sat_conversion,[],[f20315]) ).
cnf(s1570,plain,
( spl29_62
| ~ spl29_158 ),
inference(sat_conversion,[],[f20470]) ).
cnf(s1635,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_158 ),
inference(sat_conversion,[],[f21009]) ).
cnf(s1637,plain,
spl29_5,
inference(rat,[],[s5,s1]) ).
cnf(s1638,plain,
~ spl29_3,
inference(rat,[],[s3,s1]) ).
cnf(s1639,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s1641,plain,
spl29_74,
inference(rat,[],[s81,s1637]) ).
cnf(s1645,plain,
~ spl29_6,
inference(rat,[],[s6,s1638]) ).
cnf(s1646,plain,
spl29_4,
inference(rat,[],[s4,s1,s1639]) ).
cnf(s1647,plain,
spl29_13,
inference(rat,[],[s13,s1645]) ).
cnf(s1648,plain,
~ spl29_8,
inference(rat,[],[s8,s1645]) ).
cnf(s1649,plain,
spl29_7,
inference(rat,[],[s7,s1645]) ).
cnf(s1706,plain,
spl29_127,
inference(rat,[],[s1551,s1646]) ).
cnf(s1711,plain,
~ spl29_9,
inference(rat,[],[s9,s1648]) ).
cnf(s1712,plain,
spl29_11,
inference(rat,[],[s11,s1645,s1649]) ).
cnf(s1713,plain,
spl29_108,
inference(rat,[],[s1535,s1706]) ).
cnf(s1715,plain,
~ spl29_15,
inference(rat,[],[s15,s1711]) ).
cnf(s1716,plain,
spl29_10,
inference(rat,[],[s10,s1711]) ).
cnf(s1717,plain,
spl29_158,
inference(rat,[],[s1635,s1646,s1712]) ).
cnf(s1723,plain,
spl29_81,
inference(rat,[],[s90,s1646,s1712]) ).
cnf(s1730,plain,
~ spl29_16,
inference(rat,[],[s16,s1715]) ).
cnf(s1732,plain,
spl29_62,
inference(rat,[],[s1570,s1717]) ).
cnf(s1733,plain,
spl29_63,
inference(rat,[],[s70,s1730]) ).
cnf(s1734,plain,
~ spl29_19,
inference(rat,[],[s19,s1730]) ).
cnf(s1735,plain,
spl29_17,
inference(rat,[],[s17,s1730]) ).
cnf(s1738,plain,
spl29_64,
inference(rat,[],[s71,s1734]) ).
cnf(s1740,plain,
spl29_44,
inference(rat,[],[s42,s1734]) ).
cnf(s1741,plain,
~ spl29_20,
inference(rat,[],[s20,s1734]) ).
cnf(s1744,plain,
~ spl29_49,
inference(rat,[],[s69,s1732,s1735]) ).
cnf(s1746,plain,
spl29_82,
inference(rat,[],[s89,s1723,s1738]) ).
cnf(s1750,plain,
spl29_37,
inference(rat,[],[s41,s1740]) ).
cnf(s1753,plain,
~ spl29_32,
inference(rat,[],[s31,s1741]) ).
cnf(s1756,plain,
spl29_47,
inference(rat,[],[s48,s1730,s1744]) ).
cnf(s1757,plain,
spl29_102,
inference(rat,[],[s119,s1746]) ).
cnf(s1759,plain,
~ spl29_35,
inference(rat,[],[s34,s1753]) ).
cnf(s1761,plain,
~ spl29_42,
inference(rat,[],[s46,s1716,s1756]) ).
cnf(s1766,plain,
spl29_36,
inference(rat,[],[s38,s1711,s1761]) ).
cnf(s1768,plain,
~ spl29_28,
inference(rat,[],[s35,s1750,s1759,s1766]) ).
cnf(s1769,plain,
~ spl29_56,
inference(rat,[],[s59,s1768]) ).
cnf(s1772,plain,
spl29_105,
inference(rat,[],[s123,s1769]) ).
cnf(s1777,plain,
spl29_39,
inference(rat,[],[s122,s1757,s1772]) ).
cnf(s1787,plain,
~ spl29_107,
inference(rat,[],[s128,s1713,s1735,s1641,s1647,s1777]) ).
cnf(s1788,plain,
~ spl29_38,
inference(rat,[],[s411,s1759,s1750,s1777]) ).
cnf(s1793,plain,
spl29_106,
inference(rat,[],[s127,s1733,s1787]) ).
cnf(s1795,plain,
spl29_46,
inference(rat,[],[s45,s1711,s1788]) ).
cnf(s1798,plain,
$false,
inference(rat,[],[s126,s1716,s1793,s1795]) ).
fof(f21010,plain,
$false,
inference(avatar_sat_refutation,[],[s1798]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM687+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.09/0.37 % Computer : n013.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 21:05:21 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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
% 11.05/2.48 % (546127)Detected formulas, will run a generic FOF schedule.
% 11.05/2.48 % (546138)dis-21_1_sil=8000:lcm=predicate:random_seed=3872515624: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)
% 11.05/2.48 % (546134)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=984562097:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.05/2.48 % (546137)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2899064173:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.05/2.48 % (546136)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3467601583:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.05/2.48 % (546135)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=567644867:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.05/2.48 % (546133)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=571442046:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.05/2.48 % (546132)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=834267735:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.05/2.48 % (546135)Refutation not found, incomplete strategy
% 11.05/2.48 % (546135)------------------------------
% 11.05/2.48 % (546135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.48 % (546135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.48 % (546135)CaDiCaL version: 2.1.3
% 11.05/2.48 % (546135)Termination reason: Refutation not found, incomplete strategy
% 11.05/2.48 % (546135)Time elapsed: 0.003 s
% 11.05/2.48 % (546135)Peak memory usage: 87 MB
% 11.05/2.48 % (546135)Instructions burned: 2 (million)
% 11.05/2.48 % (546138)Instruction limit reached!
% 11.05/2.48 % (546138)------------------------------
% 11.05/2.48 % (546138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.48 % (546138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.48 % (546138)CaDiCaL version: 2.1.3
% 11.05/2.48 % (546138)Termination reason: Instruction limit
% 11.05/2.48 % (546138)Termination phase: Saturation
% 11.05/2.48 % (546138)Time elapsed: 0.040 s
% 11.05/2.48 % (546138)Peak memory usage: 90 MB
% 11.05/2.48 % (546138)Instructions burned: 129 (million)
% 11.05/2.48 % (546136)Refutation not found, incomplete strategy
% 11.05/2.48 % (546136)------------------------------
% 11.05/2.48 % (546136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.48 % (546136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.48 % (546136)CaDiCaL version: 2.1.3
% 11.05/2.48 % (546136)Termination reason: Refutation not found, incomplete strategy
% 11.05/2.48 % (546136)Time elapsed: 0.003 s
% 11.05/2.48 % (546136)Peak memory usage: 88 MB
% 11.05/2.48 % (546136)Instructions burned: 3 (million)
% 11.05/2.48 % (546137)Instruction limit reached!
% 11.05/2.48 % (546137)------------------------------
% 11.05/2.48 % (546137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.48 % (546137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.48 % (546137)CaDiCaL version: 2.1.3
% 11.05/2.48 % (546137)Termination reason: Instruction limit
% 11.05/2.48 % (546137)Termination phase: Saturation
% 11.05/2.48 % (546137)Time elapsed: 0.082 s
% 11.05/2.48 % (546137)Peak memory usage: 90 MB
% 11.05/2.48 % (546137)Instructions burned: 140 (million)
% 11.05/2.48 % (546146)lrs+10_1_sil=8000:sp=occurrence:random_seed=2834965807:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.05/2.48 % (546146)Refutation not found, incomplete strategy
% 11.05/2.48 % (546146)------------------------------
% 11.05/2.48 % (546146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.48 % (546146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.48 % (546146)CaDiCaL version: 2.1.3
% 11.05/2.48 % (546146)Termination reason: Refutation not found, incomplete strategy
% 11.05/2.48 % (546146)Time elapsed: 0.002 s
% 11.05/2.48 % (546146)Peak memory usage: 88 MB
% 11.05/2.48 % (546146)Instructions burned: 2 (million)
% 11.05/2.48 % (546135)------------------------------
% 11.05/2.48 % (546135)------------------------------
% 21.56/3.94 % (546136)------------------------------
% 21.56/3.94 % (546136)------------------------------
% 21.56/3.94 % (546147)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1402466343:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 21.56/3.94 % (546147)Refutation not found, incomplete strategy
% 21.56/3.94 % (546147)------------------------------
% 21.56/3.94 % (546147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.94 % (546147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.94 % (546147)CaDiCaL version: 2.1.3
% 21.56/3.94 % (546147)Termination reason: Refutation not found, incomplete strategy
% 21.56/3.94 % (546147)Time elapsed: 0.005 s
% 21.56/3.94 % (546147)Peak memory usage: 88 MB
% 21.56/3.94 % (546147)Instructions burned: 8 (million)
% 21.56/3.94 % (546146)------------------------------
% 21.56/3.94 % (546146)------------------------------
% 21.56/3.94 % (546152)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2132626621:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 21.56/3.94 % (546150)lrs+1011_1_sil=32000:sp=occurrence:random_seed=906278344:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 21.56/3.94 % (546151)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=2501578927:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 21.56/3.94 % (546152)Refutation not found, incomplete strategy
% 21.56/3.94 % (546152)------------------------------
% 21.56/3.94 % (546152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.94 % (546152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.94 % (546152)CaDiCaL version: 2.1.3
% 21.56/3.94 % (546152)Termination reason: Refutation not found, incomplete strategy
% 21.56/3.94 % (546152)Time elapsed: 0.003 s
% 21.56/3.94 % (546152)Peak memory usage: 88 MB
% 21.56/3.94 % (546152)Instructions burned: 6 (million)
% 21.56/3.94 % (546150)Refutation not found, incomplete strategy
% 21.56/3.94 % (546150)------------------------------
% 21.56/3.94 % (546150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.94 % (546150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.94 % (546150)CaDiCaL version: 2.1.3
% 21.56/3.94 % (546150)Termination reason: Refutation not found, incomplete strategy
% 21.56/3.94 % (546150)Time elapsed: 0.005 s
% 21.56/3.94 % (546150)Peak memory usage: 89 MB
% 21.56/3.94 % (546150)Instructions burned: 5 (million)
% 21.56/3.94 % (546147)------------------------------
% 21.56/3.94 % (546147)------------------------------
% 21.56/3.94 % (546151)Instruction limit reached!
% 21.56/3.94 % (546151)------------------------------
% 21.56/3.94 % (546151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.94 % (546151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.94 % (546151)CaDiCaL version: 2.1.3
% 21.56/3.94 % (546151)Termination reason: Instruction limit
% 21.56/3.94 % (546151)Termination phase: Saturation
% 21.56/3.94 % (546151)Time elapsed: 0.125 s
% 21.56/3.94 % (546151)Peak memory usage: 95 MB
% 21.56/3.94 % (546151)Instructions burned: 248 (million)
% 21.56/3.94 % (546152)------------------------------
% 21.56/3.94 % (546152)------------------------------
% 21.56/3.94 % (546150)------------------------------
% 21.56/3.94 % (546150)------------------------------
% 21.56/3.94 % (546156)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2260521332:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 21.56/3.94 % (546157)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1154885599:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 21.56/3.94 % (546158)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1802988811:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 21.56/3.94 % (546158)Instruction limit reached!
% 21.56/3.94 % (546158)------------------------------
% 21.56/3.94 % (546158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.94 % (546158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.94 % (546158)CaDiCaL version: 2.1.3
% 21.56/3.94 % (546158)Termination reason: Instruction limit
% 21.56/3.94 % (546158)Termination phase: Saturation
% 21.56/3.94 % (546158)Time elapsed: 0.033 s
% 21.56/3.94 % (546158)Peak memory usage: 89 MB
% 21.56/3.94 % (546158)Instructions burned: 129 (million)
% 21.56/3.94 % (546157)Instruction limit reached!
% 26.22/4.67 % (546157)------------------------------
% 26.22/4.67 % (546157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546157)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546157)Termination reason: Instruction limit
% 26.22/4.67 % (546157)Termination phase: Saturation
% 26.22/4.67 % (546157)Time elapsed: 0.061 s
% 26.22/4.67 % (546157)Peak memory usage: 91 MB
% 26.22/4.67 % (546157)Instructions burned: 114 (million)
% 26.22/4.67 % (546159)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1498159013:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 26.22/4.67 % (546163)lrs+10_1_sil=8000:sp=occurrence:random_seed=4271275556:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 26.22/4.67 % (546159)Instruction limit reached!
% 26.22/4.67 % (546159)------------------------------
% 26.22/4.67 % (546159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546159)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546159)Termination reason: Instruction limit
% 26.22/4.67 % (546159)Termination phase: Saturation
% 26.22/4.67 % (546159)Time elapsed: 0.064 s
% 26.22/4.67 % (546159)Peak memory usage: 90 MB
% 26.22/4.67 % (546159)Instructions burned: 115 (million)
% 26.22/4.67 % (546164)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=687234311:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 26.22/4.67 % (546164)Refutation not found, incomplete strategy
% 26.22/4.67 % (546164)------------------------------
% 26.22/4.67 % (546164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546164)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546164)Termination reason: Refutation not found, incomplete strategy
% 26.22/4.67 % (546164)Time elapsed: 0.039 s
% 26.22/4.67 % (546164)Peak memory usage: 90 MB
% 26.22/4.67 % (546164)Instructions burned: 76 (million)
% 26.22/4.67 % (546167)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=152949781:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 26.22/4.67 % (546163)Instruction limit reached!
% 26.22/4.67 % (546163)------------------------------
% 26.22/4.67 % (546163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546163)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546163)Termination reason: Instruction limit
% 26.22/4.67 % (546163)Termination phase: Saturation
% 26.22/4.67 % (546163)Time elapsed: 0.281 s
% 26.22/4.67 % (546163)Peak memory usage: 99 MB
% 26.22/4.67 % (546163)Instructions burned: 910 (million)
% 26.22/4.67 % (546164)------------------------------
% 26.22/4.67 % (546164)------------------------------
% 26.22/4.67 % (546170)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3552524462:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 26.22/4.67 % (546170)Instruction limit reached!
% 26.22/4.67 % (546170)------------------------------
% 26.22/4.67 % (546170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546170)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546170)Termination reason: Instruction limit
% 26.22/4.67 % (546170)Termination phase: Saturation
% 26.22/4.67 % (546170)Time elapsed: 0.039 s
% 26.22/4.67 % (546170)Peak memory usage: 94 MB
% 26.22/4.67 % (546170)Instructions burned: 138 (million)
% 26.22/4.67 % (546171)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2233046988:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 26.22/4.67 % (546171)Refutation not found, incomplete strategy
% 26.22/4.67 % (546171)------------------------------
% 26.22/4.67 % (546171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546171)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546171)Termination reason: Refutation not found, incomplete strategy
% 26.22/4.67 % (546171)Time elapsed: 0.016 s
% 26.22/4.67 % (546171)Peak memory usage: 89 MB
% 26.22/4.67 % (546171)Instructions burned: 28 (million)
% 26.22/4.67 % (546173)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4122350747:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 26.22/4.67 % (546171)------------------------------
% 26.22/4.67 % (546171)------------------------------
% 26.22/4.67 % (546176)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=1374037041:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 26.22/4.67 % (546176)Refutation not found, incomplete strategy
% 26.22/4.67 % (546176)------------------------------
% 26.22/4.67 % (546176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546176)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546176)Termination reason: Refutation not found, incomplete strategy
% 26.22/4.67 % (546176)Time elapsed: 0.007 s
% 26.22/4.67 % (546176)Peak memory usage: 88 MB
% 26.22/4.67 % (546176)Instructions burned: 11 (million)
% 26.22/4.67 % (546176)------------------------------
% 26.22/4.67 % (546176)------------------------------
% 26.22/4.67 % (546178)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3122729873:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 26.22/4.67 % (546156)Instruction limit reached!
% 26.22/4.67 % (546156)------------------------------
% 26.22/4.67 % (546156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546156)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546156)Termination reason: Instruction limit
% 26.22/4.67 % (546156)Termination phase: Saturation
% 26.22/4.67 % (546156)Time elapsed: 1.591 s
% 26.22/4.67 % (546156)Peak memory usage: 142 MB
% 26.22/4.67 % (546156)Instructions burned: 2351 (million)
% 26.22/4.67 % (546178)Instruction limit reached!
% 26.22/4.67 % (546178)------------------------------
% 26.22/4.67 % (546178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546178)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546178)Termination reason: Instruction limit
% 26.22/4.67 % (546178)Termination phase: Saturation
% 26.22/4.67 % (546178)Time elapsed: 0.065 s
% 26.22/4.67 % (546178)Peak memory usage: 92 MB
% 26.22/4.67 % (546178)Instructions burned: 135 (million)
% 26.22/4.67 % (546180)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3127266652:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/141Mi)
% 26.22/4.67 % (546180)Refutation not found, incomplete strategy
% 26.22/4.67 % (546180)------------------------------
% 26.22/4.67 % (546180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546180)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546180)Termination reason: Refutation not found, incomplete strategy
% 26.22/4.67 % (546180)Time elapsed: 0.003 s
% 26.22/4.67 % (546180)Peak memory usage: 88 MB
% 26.22/4.67 % (546180)Instructions burned: 2 (million)
% 26.22/4.67 % (546181)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2904446338:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 26.22/4.67 % (546181)Refutation not found, incomplete strategy
% 26.22/4.67 % (546181)------------------------------
% 26.22/4.67 % (546181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546181)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546181)Termination reason: Refutation not found, incomplete strategy
% 26.22/4.67 % (546181)Time elapsed: 0.003 s
% 26.22/4.67 % (546181)Peak memory usage: 89 MB
% 26.22/4.67 % (546181)Instructions burned: 2 (million)
% 26.22/4.67 % (546180)------------------------------
% 26.22/4.67 % (546180)------------------------------
% 26.22/4.67 % (546181)------------------------------
% 26.22/4.67 % (546181)------------------------------
% 26.22/4.67 % (546184)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=532103264:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 26.22/4.67 % (546185)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=871831408:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 26.22/4.67 % (546185)Instruction limit reached!
% 26.22/4.67 % (546185)------------------------------
% 26.22/4.67 % (546185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.22/4.67 % (546185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.67 % (546185)CaDiCaL version: 2.1.3
% 26.22/4.67 % (546185)Termination reason: Instruction limit
% 26.22/4.67 % (546185)Termination phase: Saturation
% 26.22/4.67 % (546185)Time elapsed: 0.079 s
% 26.22/4.67 % (546185)Peak memory usage: 91 MB
% 26.22/4.67 % (546185)Instructions burned: 152 (million)
% 26.22/4.67 % (546188)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1427039283:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 26.22/4.67 % (546134)First to succeed.
% 26.22/4.67 % (546134)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-546127"
% 26.22/4.67 % (546134)Refutation found. Thanks to Tanya!
% 26.22/4.67 % SZS status Theorem for theBenchmark
% 26.22/4.67 % SZS output start Proof for theBenchmark
% See solution above
% 27.40/4.87 % (546134)------------------------------
% 27.40/4.87 % (546134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.40/4.87 % (546134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.40/4.87 % (546134)CaDiCaL version: 2.1.3
% 27.40/4.87 % (546134)Termination reason: Refutation
% 27.40/4.87 % (546134)Time elapsed: 3.343 s
% 27.40/4.87 % (546134)Peak memory usage: 167 MB
% 27.40/4.87 % (546134)Instructions burned: 5560 (million)
% 27.40/4.87 % (546134)------------------------------
% 27.40/4.87 % (546134)------------------------------
% 27.40/4.87 % (546127)Success in time 3.815 s
% 27.40/4.87 % Vampire exiting
%------------------------------------------------------------------------------