%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM795+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 : n018.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:17:05 PM UTC 2026
% Result : Theorem 62.17s 17.83s
% Output : Refutation 120.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 37
% Syntax : Number of formulae : 219 ( 61 unt; 6 def)
% Number of atoms : 537 ( 21 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 567 ( 249 ~; 229 |; 46 &)
% ( 33 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 7 prp; 0-2 aty)
% Number of functors : 40 ( 40 usr; 22 con; 0-2 aty)
% Number of variables : 220 ( 0 sgn 218 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f35,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1))
<=> pp(aa_bool_bool(scratc1202795191d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1725338564_rt_is,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__rt__lessis) ).
fof(f50,axiom,
scratc1725338564_rt_is = scratc1815386167d_e_is(scratc515485325nd_rat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__rt__is) ).
fof(f131,axiom,
scratc1334046528d_n_is = scratc1815386167d_e_is(scratc482439305nd_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__is) ).
fof(f178,axiom,
! [X0] : scratc1815386167d_e_is(X0) = fequal_TPTP_ind,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__e__is) ).
fof(f188,axiom,
! [X0] : scratc1202795191d_l_or(X0) = aa_boo1142376798l_bool(scratc441918964nd_imp,scratc627990855_d_not(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__l__or) ).
fof(f193,axiom,
! [X0] :
( pp(scratc627990855_d_not(X0))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc441918964nd_imp,X0),fFalse)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__not) ).
fof(f194,axiom,
scratc441918964nd_imp = fimplies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__imp) ).
fof(f225,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc1533070073_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f229,axiom,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_cq)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz98a) ).
fof(f234,axiom,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_dg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz96f) ).
fof(f256,axiom,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_fl)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz81j) ).
fof(f262,axiom,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_fx)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz81c) ).
fof(f801,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_fx,X0))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fw,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__238) ).
fof(f807,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_fl,X0))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fk,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__244) ).
fof(f827,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_dg,X0))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__264) ).
fof(f832,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cq,X0))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cp,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__269) ).
fof(f835,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__272) ).
fof(f904,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1))
=> pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__341) ).
fof(f924,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,X0),X1))
<=> ( pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1)))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__361) ).
fof(f1100,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__537) ).
fof(f1105,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cp,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_co(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__542) ).
fof(f1108,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__545) ).
fof(f1170,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__607) ).
fof(f1297,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_co(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__734) ).
fof(f1300,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc1717941280all_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__737) ).
fof(f1322,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(scratc932059261lessis,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__759) ).
fof(f1325,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__762) ).
fof(f1403,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(f1405,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(f1408,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(f1412,conjecture,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_ad)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1413,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(negated_conjecture,[status(cth)],[f1412]) ).
fof(f1414,plain,
~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(flattening,[],[f1413]) ).
fof(f1431,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1533070073_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f225]) ).
fof(f1432,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1533070073_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f1431]) ).
fof(f1524,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,X0),X1))
<=> ( pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f904]) ).
fof(f1536,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1))) ) ),
inference(ennf_transformation,[],[f924]) ).
fof(f1590,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)) ) ),
inference(ennf_transformation,[],[f1170]) ).
fof(f1671,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(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1)) ) ),
inference(ennf_transformation,[],[f1322]) ).
fof(f1672,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(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1)) ) ),
inference(flattening,[],[f1671]) ).
fof(f1677,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)) ) ),
inference(ennf_transformation,[],[f1325]) ).
fof(f1678,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)) ) ),
inference(flattening,[],[f1677]) ).
fof(f1798,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,[],[f1408]) ).
fof(f1799,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,[],[f1798]) ).
fof(f1800,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1))
| ~ pp(aa_bool_bool(scratc1202795191d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1725338564_rt_is,X0),X1))) )
& ( pp(aa_bool_bool(scratc1202795191d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1725338564_rt_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1)) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f1865,plain,
! [X0] :
( ( pp(scratc627990855_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc441918964nd_imp,X0),fFalse)) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc441918964nd_imp,X0),fFalse))
| ~ pp(scratc627990855_d_not(X0)) ) ),
inference(nnf_transformation,[],[f193]) ).
fof(f1888,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1533070073_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1533070073_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f1432]) ).
fof(f1889,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1533070073_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1533070073_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1)) ) ),
inference(rectify,[],[f1888]) ).
fof(f1890,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc1533070073_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1533070073_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1889]) ).
fof(f2147,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_fx,X0))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fw,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fw,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_fx,X0)) ) ),
inference(nnf_transformation,[],[f801]) ).
fof(f2153,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_fl,X0))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fk,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fk,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_fl,X0)) ) ),
inference(nnf_transformation,[],[f807]) ).
fof(f2173,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dg,X0))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dg,X0)) ) ),
inference(nnf_transformation,[],[f827]) ).
fof(f2178,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cq,X0))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cp,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cp,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cq,X0)) ) ),
inference(nnf_transformation,[],[f832]) ).
fof(f2181,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0)) ) ),
inference(nnf_transformation,[],[f835]) ).
fof(f2281,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,X0),X1))
| ( ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1)) ) )
& ( pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,X0),X1)) ) ),
inference(nnf_transformation,[],[f1524]) ).
fof(f2282,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,X0),X1))
| ( ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1)) ) )
& ( pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,X0),X1)) ) ),
inference(flattening,[],[f2281]) ).
fof(f2311,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
& pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,X0),X1)) ) ),
inference(nnf_transformation,[],[f1536]) ).
fof(f2312,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
& pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,X0),X1)) ) ),
inference(flattening,[],[f2311]) ).
fof(f2498,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1)) ) ),
inference(nnf_transformation,[],[f1100]) ).
fof(f2503,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cp,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_co(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_co(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cp,X0),X1)) ) ),
inference(nnf_transformation,[],[f1105]) ).
fof(f2506,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_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,[],[f1108]) ).
fof(f2600,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f1590]) ).
fof(f2601,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1),X2)) ) ),
inference(flattening,[],[f2600]) ).
fof(f2781,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_co(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_co(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f1297]) ).
fof(f2784,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc1717941280all_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,[],[f1300]) ).
fof(f2811,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(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f1672]) ).
fof(f2812,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(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f2811]) ).
fof(f2817,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f1678]) ).
fof(f2818,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f2817]) ).
fof(f2976,plain,
! [X0,X1] :
( pp(aa_bool_bool(scratc1202795191d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1725338564_rt_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1)) ),
inference(cnf_transformation,[],[f1800]) ).
fof(f2998,plain,
scratc1725338564_rt_is = scratc1815386167d_e_is(scratc515485325nd_rat),
inference(cnf_transformation,[],[f50]) ).
fof(f3111,plain,
scratc1334046528d_n_is = scratc1815386167d_e_is(scratc482439305nd_nat),
inference(cnf_transformation,[],[f131]) ).
fof(f3175,plain,
! [X0] : scratc1815386167d_e_is(X0) = fequal_TPTP_ind,
inference(cnf_transformation,[],[f178]) ).
fof(f3189,plain,
! [X0] : aa_boo1142376798l_bool(scratc441918964nd_imp,scratc627990855_d_not(X0)) = scratc1202795191d_l_or(X0),
inference(cnf_transformation,[],[f188]) ).
fof(f3196,plain,
! [X0] :
( pp(scratc627990855_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc441918964nd_imp,X0),fFalse)) ),
inference(cnf_transformation,[],[f1865]) ).
fof(f3197,plain,
scratc441918964nd_imp = fimplies,
inference(cnf_transformation,[],[f194]) ).
fof(f3259,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1533070073_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1890]) ).
fof(f3260,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f1890]) ).
fof(f3261,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
| scratc1533070073_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f1890]) ).
fof(f3262,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f1890]) ).
fof(f3267,plain,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_cq)),
inference(cnf_transformation,[],[f229]) ).
fof(f3272,plain,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_dg)),
inference(cnf_transformation,[],[f234]) ).
fof(f3294,plain,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_fl)),
inference(cnf_transformation,[],[f256]) ).
fof(f3300,plain,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_fx)),
inference(cnf_transformation,[],[f262]) ).
fof(f4106,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fw,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_fx,X0)) ),
inference(cnf_transformation,[],[f2147]) ).
fof(f4118,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fk,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_fl,X0)) ),
inference(cnf_transformation,[],[f2153]) ).
fof(f4158,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dg,X0)) ),
inference(cnf_transformation,[],[f2173]) ).
fof(f4168,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cp,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cq,X0)) ),
inference(cnf_transformation,[],[f2178]) ).
fof(f4175,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
inference(cnf_transformation,[],[f2181]) ).
fof(f4341,plain,
! [X0,X1] :
( pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,X0),X1)) ),
inference(cnf_transformation,[],[f2282]) ).
fof(f4391,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,X0),X1)) ),
inference(cnf_transformation,[],[f2312]) ).
fof(f4754,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1)) ),
inference(cnf_transformation,[],[f2498]) ).
fof(f4764,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_co(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cp,X0),X1)) ),
inference(cnf_transformation,[],[f2503]) ).
fof(f4771,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
inference(cnf_transformation,[],[f2506]) ).
fof(f4931,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(X0),X1),X2)) ),
inference(cnf_transformation,[],[f2601]) ).
fof(f5255,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_co(X0),X1),X2)) ),
inference(cnf_transformation,[],[f2781]) ).
fof(f5262,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
inference(cnf_transformation,[],[f2784]) ).
fof(f5317,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(scratc932059261lessis,X0),X1)) ),
inference(cnf_transformation,[],[f2812]) ).
fof(f5318,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(scratc610510771t_less,X2),X3)) ),
inference(cnf_transformation,[],[f2812]) ).
fof(f5319,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(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3))) ),
inference(cnf_transformation,[],[f2812]) ).
fof(f5328,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(X0),X1),X2),X3)) ),
inference(cnf_transformation,[],[f2818]) ).
fof(f5593,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
inference(cnf_transformation,[],[f1403]) ).
fof(f5595,plain,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f1405]) ).
fof(f5598,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,[],[f1799]) ).
fof(f5602,plain,
~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(cnf_transformation,[],[f1414]) ).
fof(f5604,plain,
! [X0] : scratc1202795191d_l_or(X0) = aa_boo1142376798l_bool(fimplies,scratc627990855_d_not(X0)),
inference(definition_unfolding,[],[f3189,f3197]) ).
fof(f5610,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1725338564_rt_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,X0),X1)) ),
inference(definition_unfolding,[],[f2976,f5604]) ).
fof(f5617,plain,
scratc1725338564_rt_is = fequal_TPTP_ind,
inference(definition_unfolding,[],[f2998,f3175]) ).
fof(f5675,plain,
scratc1334046528d_n_is = fequal_TPTP_ind,
inference(definition_unfolding,[],[f3111,f3175]) ).
fof(f5702,plain,
! [X0] :
( pp(scratc627990855_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse)) ),
inference(definition_unfolding,[],[f3196,f3197]) ).
fof(f5953,plain,
gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad)),
inference(resolution,[],[f5602,f3260]) ).
fof(f5954,plain,
scratc1533070073_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a),
inference(resolution,[],[f5602,f3261]) ).
fof(f5955,plain,
~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad))),
inference(resolution,[],[f5602,f3262]) ).
fof(f5968,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(scratc1717941280all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f5954,f3259]) ).
fof(f5969,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f5968,f5953]) ).
fof(f5970,plain,
~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(resolution,[],[f5955,f4175]) ).
fof(f6048,plain,
gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(resolution,[],[f5970,f3260]) ).
fof(f6049,plain,
scratc1533070073_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a),
inference(resolution,[],[f5970,f3261]) ).
fof(f6050,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))))),
inference(resolution,[],[f5970,f3262]) ).
fof(f6062,plain,
~ pp(aa_fun171081125l_bool(scratc1717941280all_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)))))),
inference(resolution,[],[f6050,f4771]) ).
fof(f6148,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)))))),
inference(resolution,[],[f6062,f3260]) ).
fof(f6149,plain,
scratc1533070073_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),
inference(resolution,[],[f6062,f3261]) ).
fof(f6150,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))))))),
inference(resolution,[],[f6062,f3262]) ).
fof(f6163,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f6149,f3259]) ).
fof(f6164,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f6163,f6148]) ).
fof(f9671,plain,
! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),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_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))) = X0
| ~ gg_TPTP_ind(X0) ),
inference(resolution,[],[f6048,f5598]) ).
fof(f9684,plain,
! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1334046528d_n_is,X0),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_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))) = X0
| ~ gg_TPTP_ind(X0) ),
inference(forward_demodulation,[],[f9671,f5675]) ).
fof(f9751,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(scratc1717941280all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f6049,f3259]) ).
fof(f9752,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(scratc1717941280all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f9751,f6048]) ).
fof(f10793,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_cq))
| pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cp,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
inference(resolution,[],[f5969,f4168]) ).
fof(f10820,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_fl))
| pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fk,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
inference(resolution,[],[f5969,f4118]) ).
fof(f10826,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_fx))
| pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fw,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
inference(resolution,[],[f5969,f4106]) ).
fof(f11115,plain,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fw,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(forward_subsumption_resolution,[],[f10826,f3300]) ).
fof(f11121,plain,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fk,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(forward_subsumption_resolution,[],[f10820,f3294]) ).
fof(f11148,plain,
pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cp,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(forward_subsumption_resolution,[],[f10793,f3267]) ).
fof(f11391,plain,
~ pp(aa_fun171081125l_bool(scratc1717941280all_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)))))))),
inference(resolution,[],[f6150,f5262]) ).
fof(f12505,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)))))))),
inference(resolution,[],[f11391,f3260]) ).
fof(f12506,plain,
scratc1533070073_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),
inference(resolution,[],[f11391,f3261]) ).
fof(f12507,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))))))))),
inference(resolution,[],[f11391,f3262]) ).
fof(f16498,definition,
( spl25_804
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,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,[spl25_804])],[avatar_definition]) ).
fof(f16499,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl25_804 ),
inference(avatar_component_clause,[],[f16498]) ).
fof(f16506,plain,
( ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,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(aTP_Lamm_fk,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl25_804 ),
inference(resolution,[],[f16499,f4391]) ).
fof(f16573,definition,
( spl25_807
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,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,[spl25_807])],[avatar_definition]) ).
fof(f16574,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fk,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl25_807 ),
inference(avatar_component_clause,[],[f16573]) ).
fof(f16576,definition,
( spl25_808
<=> pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,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,[spl25_808])],[avatar_definition]) ).
fof(f16577,plain,
( ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl25_808 ),
inference(avatar_component_clause,[],[f16576]) ).
fof(f16578,plain,
( ~ spl25_807
| ~ spl25_808
| spl25_804 ),
inference(avatar_split_clause,[],[f16506,f16498,f16576,f16573]) ).
fof(f16716,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fk,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl25_807 ),
inference(resolution,[],[f16574,f9752]) ).
fof(f16761,plain,
( $false
| spl25_807 ),
inference(forward_subsumption_resolution,[],[f16716,f11121]) ).
fof(f16762,plain,
spl25_807,
inference(avatar_contradiction_clause,[],[f16761]) ).
fof(f16766,plain,
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),fFalse))
| spl25_808 ),
inference(resolution,[],[f16577,f5702]) ).
fof(f16779,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1066042873moreis,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl25_808 ),
inference(resolution,[],[f16766,f5595]) ).
fof(f16825,plain,
( pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,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(aTP_Lamm_fw,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl25_808 ),
inference(resolution,[],[f16779,f4341]) ).
fof(f16866,definition,
( spl25_821
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,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,[spl25_821])],[avatar_definition]) ).
fof(f16867,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fw,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl25_821 ),
inference(avatar_component_clause,[],[f16866]) ).
fof(f16869,definition,
( spl25_822
<=> pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,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,[spl25_822])],[avatar_definition]) ).
fof(f16870,plain,
( pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl25_822 ),
inference(avatar_component_clause,[],[f16869]) ).
fof(f16871,plain,
( ~ spl25_821
| spl25_822
| spl25_808 ),
inference(avatar_split_clause,[],[f16825,f16576,f16869,f16866]) ).
fof(f16888,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_fw,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl25_821 ),
inference(resolution,[],[f16867,f9752]) ).
fof(f16933,plain,
( $false
| spl25_821 ),
inference(forward_subsumption_resolution,[],[f16888,f11115]) ).
fof(f16934,plain,
spl25_821,
inference(avatar_contradiction_clause,[],[f16933]) ).
fof(f17248,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc932059261lessis,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),
inference(resolution,[],[f12507,f5317]) ).
fof(f17249,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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))))))))),
inference(resolution,[],[f12507,f5318]) ).
fof(f17250,plain,
~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(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(scratc1725797750_rt_pl(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)))))))))),
inference(resolution,[],[f12507,f5319]) ).
fof(f17329,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,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_cn(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))))))))) ),
inference(resolution,[],[f17250,f5328]) ).
fof(f17449,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,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_cn(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))))))))) ),
inference(forward_subsumption_resolution,[],[f17329,f17249]) ).
fof(f17451,definition,
( spl25_873
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(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,[spl25_873])],[avatar_definition]) ).
fof(f17452,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(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)))))))))
| spl25_873 ),
inference(avatar_component_clause,[],[f17451]) ).
fof(f17453,plain,
( ~ spl25_873
| ~ spl25_804 ),
inference(avatar_split_clause,[],[f17449,f16498,f17451]) ).
fof(f17537,plain,
pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1725338564_rt_is,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),
inference(resolution,[],[f17248,f5610]) ).
fof(f17570,plain,
pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),
inference(forward_demodulation,[],[f17537,f5617]) ).
fof(f17585,plain,
pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1334046528d_n_is,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),
inference(forward_demodulation,[],[f17570,f5675]) ).
fof(f17601,plain,
( ! [X0] :
( ~ scratc1533070073_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(scratc1717941280all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(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)))))))) )
| spl25_873 ),
inference(resolution,[],[f17452,f3259]) ).
fof(f17660,plain,
( ! [X0] :
( ~ scratc1533070073_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(scratc1717941280all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(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)))))))) )
| spl25_873 ),
inference(forward_subsumption_resolution,[],[f17601,f12505]) ).
fof(f17674,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cn(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))))))))
| spl25_873 ),
inference(resolution,[],[f17660,f12506]) ).
fof(f17676,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_co(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)))))))
| spl25_873 ),
inference(resolution,[],[f17674,f5255]) ).
fof(f17698,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_co(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl25_873 ),
inference(resolution,[],[f17676,f6164]) ).
fof(f17743,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cp,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl25_873 ),
inference(resolution,[],[f17698,f4764]) ).
fof(f17768,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cp,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl25_873 ),
inference(resolution,[],[f17743,f9752]) ).
fof(f17813,plain,
( $false
| spl25_873 ),
inference(forward_subsumption_resolution,[],[f17768,f11148]) ).
fof(f17814,plain,
spl25_873,
inference(avatar_contradiction_clause,[],[f17813]) ).
fof(f18020,plain,
( ~ pp(scratc627990855_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,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(scratc1334046528d_n_is,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))) ),
inference(resolution,[],[f17585,f5593]) ).
fof(f18030,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1334046528d_n_is,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18020,f16870]) ).
fof(f18031,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,aTP_Lamm_ad))
| ~ spl25_822 ),
inference(resolution,[],[f18030,f9684]) ).
fof(f18081,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)))
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18031,f5953]) ).
fof(f18085,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl25_822 ),
inference(superposition,[],[f6062,f18081]) ).
fof(f18087,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,aTP_Lamm_ad))))
| ~ spl25_822 ),
inference(superposition,[],[f6148,f18081]) ).
fof(f18093,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,aTP_Lamm_ad))))))
| ~ spl25_822 ),
inference(superposition,[],[f11391,f18081]) ).
fof(f18096,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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl25_822 ),
inference(superposition,[],[f12505,f18081]) ).
fof(f18107,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ spl25_822 ),
inference(superposition,[],[f17249,f18081]) ).
fof(f18108,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(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,aTP_Lamm_ad))))),aa_TPTP_ind_TPTP_ind(scratc1725797750_rt_pl(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ spl25_822 ),
inference(superposition,[],[f17250,f18081]) ).
fof(f18302,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc610510771t_less,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ spl25_822 ),
inference(resolution,[],[f18108,f4931]) ).
fof(f18423,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_de(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18302,f18107]) ).
fof(f18436,plain,
( ! [X0] :
( ~ scratc1533070073_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_de(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) )
| ~ spl25_822 ),
inference(resolution,[],[f18423,f3259]) ).
fof(f18476,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_de(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ scratc1533070073_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),X0) )
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18436,f5953]) ).
fof(f18477,plain,
( ~ scratc1533070073_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ spl25_822 ),
inference(resolution,[],[f18476,f4754]) ).
fof(f18498,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18477,f5954]) ).
fof(f18509,plain,
( ! [X0] :
( ~ scratc1533070073_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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_df,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) )
| ~ spl25_822 ),
inference(resolution,[],[f18498,f3259]) ).
fof(f18568,plain,
( ! [X0] :
( ~ scratc1533070073_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,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_df,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) )
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18509,f18096]) ).
fof(f18581,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,aTP_Lamm_ad))))))
| ~ spl25_822 ),
inference(resolution,[],[f18568,f3261]) ).
fof(f18583,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18581,f18093]) ).
fof(f18584,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dg,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ spl25_822 ),
inference(resolution,[],[f18583,f4158]) ).
fof(f18603,plain,
( ! [X0] :
( ~ scratc1533070073_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,aTP_Lamm_ad))))
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),aTP_Lamm_dg)) )
| ~ spl25_822 ),
inference(resolution,[],[f18584,f3259]) ).
fof(f18660,plain,
( ! [X0] :
( ~ scratc1533070073_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))),X0)
| ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(X0),aTP_Lamm_dg)) )
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18603,f18087]) ).
fof(f18673,plain,
( ~ pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aTP_Lamm_dg))
| pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl25_822 ),
inference(resolution,[],[f18660,f3261]) ).
fof(f18675,plain,
( pp(aa_fun171081125l_bool(scratc1717941280all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18673,f3272]) ).
fof(f18676,plain,
( $false
| ~ spl25_822 ),
inference(forward_subsumption_resolution,[],[f18675,f18085]) ).
fof(f18677,plain,
~ spl25_822,
inference(avatar_contradiction_clause,[],[f18676]) ).
cnf(s481,plain,
( spl25_804
| ~ spl25_807
| ~ spl25_808 ),
inference(sat_conversion,[],[f16578]) ).
cnf(s488,plain,
spl25_807,
inference(sat_conversion,[],[f16762]) ).
cnf(s489,plain,
( spl25_808
| ~ spl25_821
| spl25_822 ),
inference(sat_conversion,[],[f16871]) ).
cnf(s492,plain,
spl25_821,
inference(sat_conversion,[],[f16934]) ).
cnf(s528,plain,
( ~ spl25_804
| ~ spl25_873 ),
inference(sat_conversion,[],[f17453]) ).
cnf(s544,plain,
spl25_873,
inference(sat_conversion,[],[f17814]) ).
cnf(s599,plain,
~ spl25_822,
inference(sat_conversion,[],[f18677]) ).
cnf(s600,plain,
~ spl25_804,
inference(rat,[],[s528,s544]) ).
cnf(s604,plain,
spl25_808,
inference(rat,[],[s489,s599,s492]) ).
cnf(s606,plain,
$false,
inference(rat,[],[s481,s604,s488,s600]) ).
fof(f18678,plain,
$false,
inference(avatar_sat_refutation,[],[s606]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM795+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.35 % Computer : n018.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 27 21:28:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 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
% 19.73/3.71 % (2737909)Detected formulas, will run a generic FOF schedule.
% 19.73/3.71 % (2738011)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3583966217:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 19.73/3.71 % (2738011)Refutation not found, incomplete strategy
% 19.73/3.71 % (2738011)------------------------------
% 19.73/3.71 % (2738011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.73/3.71 % (2738011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.73/3.71 % (2738011)CaDiCaL version: 2.1.3
% 19.73/3.71 % (2738011)Termination reason: Refutation not found, incomplete strategy
% 19.73/3.71 % (2738011)Time elapsed: 0.005 s
% 19.73/3.71 % (2738011)Peak memory usage: 89 MB
% 19.73/3.71 % (2738011)Instructions burned: 7 (million)
% 19.73/3.71 % (2738009)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=887742143:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 19.73/3.71 % (2738010)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=948780640:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 19.73/3.71 % (2738007)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=4196549887:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 19.73/3.71 % (2738012)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=916722959:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 19.73/3.71 % (2738008)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=1969481992:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 19.73/3.71 % (2738010)Refutation not found, incomplete strategy
% 19.73/3.71 % (2738010)------------------------------
% 19.73/3.71 % (2738010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.73/3.71 % (2738010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.73/3.71 % (2738010)CaDiCaL version: 2.1.3
% 19.73/3.71 % (2738010)Termination reason: Refutation not found, incomplete strategy
% 19.73/3.71 % (2738010)Time elapsed: 0.008 s
% 19.73/3.71 % (2738010)Peak memory usage: 89 MB
% 19.73/3.71 % (2738010)Instructions burned: 6 (million)
% 19.73/3.71 % (2738013)dis-21_1_sil=8000:lcm=predicate:random_seed=3825639241: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)
% 19.73/3.71 % (2738012)Instruction limit reached!
% 19.73/3.71 % (2738012)------------------------------
% 19.73/3.71 % (2738012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.73/3.71 % (2738012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.73/3.71 % (2738012)CaDiCaL version: 2.1.3
% 19.73/3.71 % (2738012)Termination reason: Instruction limit
% 19.73/3.71 % (2738012)Termination phase: Saturation
% 19.73/3.71 % (2738012)Time elapsed: 0.113 s
% 19.73/3.71 % (2738012)Peak memory usage: 90 MB
% 19.73/3.71 % (2738012)Instructions burned: 139 (million)
% 19.73/3.71 % (2738013)Instruction limit reached!
% 19.73/3.71 % (2738013)------------------------------
% 19.73/3.71 % (2738013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.73/3.71 % (2738013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.73/3.71 % (2738013)CaDiCaL version: 2.1.3
% 19.73/3.71 % (2738013)Termination reason: Instruction limit
% 19.73/3.71 % (2738013)Termination phase: Property scanning
% 19.73/3.71 % (2738013)Time elapsed: 0.105 s
% 19.73/3.71 % (2738013)Peak memory usage: 89 MB
% 19.73/3.71 % (2738013)Instructions burned: 130 (million)
% 19.73/3.71 % (2738011)------------------------------
% 19.73/3.71 % (2738011)------------------------------
% 19.73/3.71 % (2738045)lrs+10_1_sil=8000:sp=occurrence:random_seed=2765762647:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 19.73/3.71 % (2738045)Refutation not found, incomplete strategy
% 19.73/3.71 % (2738045)------------------------------
% 19.73/3.71 % (2738045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.73/3.71 % (2738045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.73/3.71 % (2738045)CaDiCaL version: 2.1.3
% 19.73/3.71 % (2738045)Termination reason: Refutation not found, incomplete strategy
% 19.73/3.71 % (2738045)Time elapsed: 0.008 s
% 32.52/5.52 % (2738045)Peak memory usage: 89 MB
% 32.52/5.52 % (2738045)Instructions burned: 6 (million)
% 32.52/5.52 % (2738049)lrs+1011_1_sil=32000:sp=occurrence:random_seed=262595921:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 32.52/5.52 % (2738048)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2192832918:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 32.52/5.52 % (2738049)Refutation not found, incomplete strategy
% 32.52/5.52 % (2738049)------------------------------
% 32.52/5.52 % (2738049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.52 % (2738049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.52 % (2738049)CaDiCaL version: 2.1.3
% 32.52/5.52 % (2738049)Termination reason: Refutation not found, incomplete strategy
% 32.52/5.52 % (2738049)Time elapsed: 0.006 s
% 32.52/5.52 % (2738049)Peak memory usage: 90 MB
% 32.52/5.52 % (2738049)Instructions burned: 8 (million)
% 32.52/5.52 % (2738010)------------------------------
% 32.52/5.52 % (2738010)------------------------------
% 32.52/5.52 % (2738048)Refutation not found, incomplete strategy
% 32.52/5.52 % (2738048)------------------------------
% 32.52/5.52 % (2738048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.52 % (2738048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.52 % (2738048)CaDiCaL version: 2.1.3
% 32.52/5.52 % (2738048)Termination reason: Refutation not found, incomplete strategy
% 32.52/5.52 % (2738048)Time elapsed: 0.021 s
% 32.52/5.52 % (2738048)Peak memory usage: 89 MB
% 32.52/5.52 % (2738048)Instructions burned: 23 (million)
% 32.52/5.52 % (2738049)------------------------------
% 32.52/5.52 % (2738049)------------------------------
% 32.52/5.52 % (2738059)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=2982911980:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 32.52/5.52 % (2738045)------------------------------
% 32.52/5.52 % (2738045)------------------------------
% 32.52/5.52 % (2738048)------------------------------
% 32.52/5.52 % (2738048)------------------------------
% 32.52/5.52 % (2738061)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2707975203:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 32.52/5.52 % (2738061)Refutation not found, incomplete strategy
% 32.52/5.52 % (2738061)------------------------------
% 32.52/5.52 % (2738061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.52 % (2738061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.52 % (2738061)CaDiCaL version: 2.1.3
% 32.52/5.52 % (2738061)Termination reason: Refutation not found, incomplete strategy
% 32.52/5.52 % (2738061)Time elapsed: 0.008 s
% 32.52/5.52 % (2738061)Peak memory usage: 90 MB
% 32.52/5.52 % (2738061)Instructions burned: 14 (million)
% 32.52/5.52 % (2738059)Instruction limit reached!
% 32.52/5.52 % (2738059)------------------------------
% 32.52/5.52 % (2738059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.52 % (2738059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.52 % (2738059)CaDiCaL version: 2.1.3
% 32.52/5.52 % (2738059)Termination reason: Instruction limit
% 32.52/5.52 % (2738059)Termination phase: Saturation
% 32.52/5.52 % (2738059)Time elapsed: 0.202 s
% 32.52/5.52 % (2738059)Peak memory usage: 95 MB
% 32.52/5.52 % (2738059)Instructions burned: 248 (million)
% 32.52/5.52 % (2738064)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3844843547:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 32.52/5.52 % (2738061)------------------------------
% 32.52/5.52 % (2738061)------------------------------
% 32.52/5.52 % (2738066)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4216525174:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 32.52/5.52 % (2738069)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3532142578:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 32.52/5.52 % (2738066)Instruction limit reached!
% 32.52/5.52 % (2738066)------------------------------
% 32.52/5.52 % (2738066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.52/5.52 % (2738066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.52/5.52 % (2738066)CaDiCaL version: 2.1.3
% 32.52/5.52 % (2738066)Termination reason: Instruction limit
% 32.52/5.52 % (2738066)Termination phase: Saturation
% 77.65/11.89 % (2738066)Time elapsed: 0.095 s
% 77.65/11.89 % (2738066)Peak memory usage: 90 MB
% 77.65/11.89 % (2738066)Instructions burned: 113 (million)
% 77.65/11.89 % (2738069)Instruction limit reached!
% 77.65/11.89 % (2738069)------------------------------
% 77.65/11.89 % (2738069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.65/11.89 % (2738069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.65/11.89 % (2738069)CaDiCaL version: 2.1.3
% 77.65/11.89 % (2738069)Termination reason: Instruction limit
% 77.65/11.89 % (2738069)Termination phase: Property scanning
% 77.65/11.89 % (2738069)Time elapsed: 0.107 s
% 77.65/11.89 % (2738069)Peak memory usage: 90 MB
% 77.65/11.89 % (2738069)Instructions burned: 128 (million)
% 77.65/11.89 % (2738073)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2631527665:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 77.65/11.89 % (2738073)Instruction limit reached!
% 77.65/11.89 % (2738073)------------------------------
% 77.65/11.89 % (2738073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.65/11.89 % (2738073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.65/11.89 % (2738073)CaDiCaL version: 2.1.3
% 77.65/11.89 % (2738073)Termination reason: Instruction limit
% 77.65/11.89 % (2738073)Termination phase: Saturation
% 77.65/11.89 % (2738073)Time elapsed: 0.055 s
% 77.65/11.89 % (2738073)Peak memory usage: 90 MB
% 77.65/11.89 % (2738073)Instructions burned: 116 (million)
% 77.65/11.89 % (2738079)lrs+10_1_sil=8000:sp=occurrence:random_seed=102155069:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 77.65/11.89 % (2738081)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3178418975:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 77.65/11.89 % (2738083)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2826746104:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 77.65/11.89 % (2738081)Refutation not found, incomplete strategy
% 77.65/11.89 % (2738081)------------------------------
% 77.65/11.89 % (2738081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.65/11.89 % (2738081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.65/11.89 % (2738081)CaDiCaL version: 2.1.3
% 77.65/11.89 % (2738081)Termination reason: Refutation not found, incomplete strategy
% 77.65/11.89 % (2738081)Time elapsed: 0.182 s
% 77.65/11.89 % (2738081)Peak memory usage: 94 MB
% 77.65/11.89 % (2738081)Instructions burned: 211 (million)
% 77.65/11.89 % (2738081)------------------------------
% 77.65/11.89 % (2738081)------------------------------
% 77.65/11.89 % (2738079)Instruction limit reached!
% 77.65/11.89 % (2738079)------------------------------
% 77.65/11.89 % (2738079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.65/11.89 % (2738079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.65/11.89 % (2738079)CaDiCaL version: 2.1.3
% 77.65/11.89 % (2738079)Termination reason: Instruction limit
% 77.65/11.89 % (2738079)Termination phase: Saturation
% 77.65/11.89 % (2738079)Time elapsed: 0.854 s
% 77.65/11.89 % (2738079)Peak memory usage: 101 MB
% 77.65/11.89 % (2738079)Instructions burned: 907 (million)
% 77.65/11.89 % (2738089)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=915804350:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 77.65/11.90 % (2738089)Instruction limit reached!
% 77.65/11.90 % (2738089)------------------------------
% 77.65/11.90 % (2738089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.65/11.90 % (2738089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.65/11.90 % (2738089)CaDiCaL version: 2.1.3
% 77.65/11.90 % (2738089)Termination reason: Instruction limit
% 77.65/11.90 % (2738089)Termination phase: Saturation
% 77.65/11.90 % (2738089)Time elapsed: 0.109 s
% 77.65/11.90 % (2738089)Peak memory usage: 92 MB
% 77.65/11.90 % (2738089)Instructions burned: 134 (million)
% 77.65/11.90 % (2738090)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3126422831:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi)
% 77.65/11.90 % (2738090)Refutation not found, incomplete strategy
% 77.65/11.90 % (2738090)------------------------------
% 77.65/11.90 % (2738090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.65/11.90 % (2738090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.65/11.90 % (2738090)CaDiCaL version: 2.1.3
% 93.51/14.09 % (2738090)Termination reason: Refutation not found, incomplete strategy
% 93.51/14.09 % (2738090)Time elapsed: 0.037 s
% 93.51/14.09 % (2738090)Peak memory usage: 90 MB
% 93.51/14.09 % (2738090)Instructions burned: 41 (million)
% 93.51/14.09 % (2738092)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2491145750:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 93.51/14.09 % (2738090)------------------------------
% 93.51/14.09 % (2738090)------------------------------
% 93.51/14.09 % (2738064)Instruction limit reached!
% 93.51/14.09 % (2738064)------------------------------
% 93.51/14.09 % (2738064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.51/14.09 % (2738064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.51/14.09 % (2738064)CaDiCaL version: 2.1.3
% 93.51/14.09 % (2738064)Termination reason: Instruction limit
% 93.51/14.09 % (2738064)Termination phase: Saturation
% 93.51/14.09 % (2738064)Time elapsed: 2.056 s
% 93.51/14.09 % (2738064)Peak memory usage: 157 MB
% 93.51/14.09 % (2738064)Instructions burned: 2350 (million)
% 93.51/14.09 % (2738097)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=3157966789:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/125Mi)
% 93.51/14.09 % (2738097)Refutation not found, incomplete strategy
% 93.51/14.09 % (2738097)------------------------------
% 93.51/14.09 % (2738097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.51/14.09 % (2738097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.51/14.09 % (2738097)CaDiCaL version: 2.1.3
% 93.51/14.09 % (2738097)Termination reason: Refutation not found, incomplete strategy
% 93.51/14.09 % (2738097)Time elapsed: 0.026 s
% 93.51/14.09 % (2738097)Peak memory usage: 90 MB
% 93.51/14.09 % (2738097)Instructions burned: 29 (million)
% 93.51/14.09 % (2738098)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=843102511:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 93.51/14.09 % (2738098)Instruction limit reached!
% 93.51/14.09 % (2738098)------------------------------
% 93.51/14.09 % (2738098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.51/14.09 % (2738098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.51/14.09 % (2738098)CaDiCaL version: 2.1.3
% 93.51/14.09 % (2738098)Termination reason: Instruction limit
% 93.51/14.09 % (2738098)Termination phase: Twee Goal Transformation
% 93.51/14.09 % (2738098)Time elapsed: 0.114 s
% 93.51/14.09 % (2738098)Peak memory usage: 91 MB
% 93.51/14.09 % (2738098)Instructions burned: 135 (million)
% 93.51/14.09 % (2738097)------------------------------
% 93.51/14.09 % (2738097)------------------------------
% 93.51/14.09 % (2738101)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2821795761:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/141Mi)
% 93.51/14.09 % (2738101)Refutation not found, incomplete strategy
% 93.51/14.09 % (2738101)------------------------------
% 93.51/14.09 % (2738101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.51/14.09 % (2738101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.51/14.09 % (2738101)CaDiCaL version: 2.1.3
% 93.51/14.09 % (2738101)Termination reason: Refutation not found, incomplete strategy
% 93.51/14.09 % (2738101)Time elapsed: 0.008 s
% 93.51/14.09 % (2738101)Peak memory usage: 90 MB
% 93.51/14.09 % (2738101)Instructions burned: 6 (million)
% 93.51/14.09 % (2738102)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2438938008:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2960 on theBenchmark for (2960ds/431Mi)
% 93.51/14.09 % (2738102)Refutation not found, incomplete strategy
% 93.51/14.09 % (2738102)------------------------------
% 93.51/14.09 % (2738102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.51/14.09 % (2738102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.51/14.09 % (2738102)CaDiCaL version: 2.1.3
% 93.51/14.09 % (2738102)Termination reason: Refutation not found, incomplete strategy
% 93.51/14.09 % (2738102)Time elapsed: 0.008 s
% 93.51/14.09 % (2738102)Peak memory usage: 89 MB
% 93.51/14.09 % (2738102)Instructions burned: 6 (million)
% 93.51/14.09 % (2738101)------------------------------
% 93.51/14.09 % (2738101)------------------------------
% 93.51/14.09 % (2738102)------------------------------
% 93.51/14.09 % (2738102)------------------------------
% 93.51/14.09 % (2738105)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=2478174610:i=6060:aac=none:ins=25_2955 on theBenchmark for (2955ds/6060Mi)
% 62.17/17.83 % (2738083)Instruction limit reached!
% 62.17/17.83 % (2738083)------------------------------
% 62.17/17.83 % (2738083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738083)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738083)Termination reason: Instruction limit
% 62.17/17.83 % (2738083)Termination phase: Saturation
% 62.17/17.83 % (2738083)Time elapsed: 2.902 s
% 62.17/17.83 % (2738083)Peak memory usage: 164 MB
% 62.17/17.83 % (2738083)Instructions burned: 5203 (million)
% 62.17/17.83 % (2738108)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=521994339:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2954 on theBenchmark for (2954ds/150Mi)
% 62.17/17.83 % (2738110)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3734948395:i=14155:bd=all_2952 on theBenchmark for (2952ds/14155Mi)
% 62.17/17.83 % (2738108)Instruction limit reached!
% 62.17/17.83 % (2738108)------------------------------
% 62.17/17.83 % (2738108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738108)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738108)Termination reason: Instruction limit
% 62.17/17.83 % (2738108)Termination phase: Saturation
% 62.17/17.83 % (2738108)Time elapsed: 0.125 s
% 62.17/17.83 % (2738108)Peak memory usage: 92 MB
% 62.17/17.83 % (2738108)Instructions burned: 151 (million)
% 62.17/17.83 % (2738113)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3510855365:i=667:av=off:fsr=off_2950 on theBenchmark for (2950ds/667Mi)
% 62.17/17.83 % (2738113)Instruction limit reached!
% 62.17/17.83 % (2738113)------------------------------
% 62.17/17.83 % (2738113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738113)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738113)Termination reason: Instruction limit
% 62.17/17.83 % (2738113)Termination phase: Saturation
% 62.17/17.83 % (2738113)Time elapsed: 0.564 s
% 62.17/17.83 % (2738113)Peak memory usage: 99 MB
% 62.17/17.83 % (2738113)Instructions burned: 668 (million)
% 62.17/17.83 % (2738115)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1304137195:s2a=on:i=185:s2at=1.8:fdi=4_2942 on theBenchmark for (2942ds/185Mi)
% 62.17/17.83 % (2738115)Instruction limit reached!
% 62.17/17.83 % (2738115)------------------------------
% 62.17/17.83 % (2738115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738115)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738115)Termination reason: Instruction limit
% 62.17/17.83 % (2738115)Termination phase: Saturation
% 62.17/17.83 % (2738115)Time elapsed: 0.148 s
% 62.17/17.83 % (2738115)Peak memory usage: 92 MB
% 62.17/17.83 % (2738115)Instructions burned: 186 (million)
% 62.17/17.83 % (2738119)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1583808484:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2938 on theBenchmark for (2938ds/193Mi)
% 62.17/17.83 % (2738119)Refutation not found, incomplete strategy
% 62.17/17.83 % (2738119)------------------------------
% 62.17/17.83 % (2738119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738119)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738119)Termination reason: Refutation not found, incomplete strategy
% 62.17/17.83 % (2738119)Time elapsed: 0.013 s
% 62.17/17.83 % (2738119)Peak memory usage: 90 MB
% 62.17/17.83 % (2738119)Instructions burned: 12 (million)
% 62.17/17.83 % (2738119)------------------------------
% 62.17/17.83 % (2738119)------------------------------
% 62.17/17.83 % (2738127)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3928988830:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2931 on theBenchmark for (2931ds/4850Mi)
% 62.17/17.83 % (2738105)Instruction limit reached!
% 62.17/17.83 % (2738105)------------------------------
% 62.17/17.83 % (2738105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738105)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738105)Termination reason: Instruction limit
% 62.17/17.83 % (2738105)Termination phase: Saturation
% 62.17/17.83 % (2738105)Time elapsed: 6.378 s
% 62.17/17.83 % (2738105)Peak memory usage: 176 MB
% 62.17/17.83 % (2738105)Instructions burned: 6061 (million)
% 62.17/17.83 % (2738136)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2571457135:i=12111:sd=1:ss=included_2889 on theBenchmark for (2889ds/12111Mi)
% 62.17/17.83 % (2738127)Instruction limit reached!
% 62.17/17.83 % (2738127)------------------------------
% 62.17/17.83 % (2738127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738127)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738127)Termination reason: Instruction limit
% 62.17/17.83 % (2738127)Termination phase: Saturation
% 62.17/17.83 % (2738127)Time elapsed: 4.712 s
% 62.17/17.83 % (2738127)Peak memory usage: 154 MB
% 62.17/17.83 % (2738127)Instructions burned: 4851 (million)
% 62.17/17.83 % (2738110)Instruction limit reached!
% 62.17/17.83 % (2738110)------------------------------
% 62.17/17.83 % (2738110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738110)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738110)Termination reason: Instruction limit
% 62.17/17.83 % (2738110)Termination phase: Saturation
% 62.17/17.83 % (2738110)Time elapsed: 7.125 s
% 62.17/17.83 % (2738110)Peak memory usage: 255 MB
% 62.17/17.83 % (2738110)Instructions burned: 14156 (million)
% 62.17/17.83 % (2738139)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=469482769:i=319:kws=precedence:fsr=off_2881 on theBenchmark for (2881ds/319Mi)
% 62.17/17.83 % (2738140)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3221945579:i=2064:ep=RST_2879 on theBenchmark for (2879ds/2064Mi)
% 62.17/17.83 % (2738139)Instruction limit reached!
% 62.17/17.83 % (2738139)------------------------------
% 62.17/17.83 % (2738139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738139)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738139)Termination reason: Instruction limit
% 62.17/17.83 % (2738139)Termination phase: Saturation
% 62.17/17.83 % (2738139)Time elapsed: 0.274 s
% 62.17/17.83 % (2738139)Peak memory usage: 95 MB
% 62.17/17.83 % (2738139)Instructions burned: 321 (million)
% 62.17/17.83 % (2738140)Refutation not found, incomplete strategy
% 62.17/17.83 % (2738140)------------------------------
% 62.17/17.83 % (2738140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738140)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738140)Termination reason: Refutation not found, incomplete strategy
% 62.17/17.83 % (2738140)Time elapsed: 0.080 s
% 62.17/17.83 % (2738140)Peak memory usage: 92 MB
% 62.17/17.83 % (2738140)Instructions burned: 182 (million)
% 62.17/17.83 % (2738140)------------------------------
% 62.17/17.83 % (2738140)------------------------------
% 62.17/17.83 % (2738143)dis-1011_128_sil=32000:random_seed=3247373935:i=3706:ep=RST:av=off_2876 on theBenchmark for (2876ds/3706Mi)
% 62.17/17.83 % (2738144)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1369848365:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2874 on theBenchmark for (2874ds/757Mi)
% 62.17/17.83 % (2738144)Refutation not found, incomplete strategy
% 62.17/17.83 % (2738144)------------------------------
% 62.17/17.83 % (2738144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738144)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738144)Termination reason: Refutation not found, incomplete strategy
% 62.17/17.83 % (2738144)Time elapsed: 0.010 s
% 62.17/17.83 % (2738144)Peak memory usage: 90 MB
% 62.17/17.83 % (2738144)Instructions burned: 18 (million)
% 62.17/17.83 % (2738144)------------------------------
% 62.17/17.83 % (2738144)------------------------------
% 62.17/17.83 % (2738147)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2336457788:i=13913:ss=axioms:sgt=8_2869 on theBenchmark for (2869ds/13913Mi)
% 62.17/17.83 % (2738147)Refutation not found, incomplete strategy
% 62.17/17.83 % (2738147)------------------------------
% 62.17/17.83 % (2738147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738147)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738147)Termination reason: Refutation not found, incomplete strategy
% 62.17/17.83 % (2738147)Time elapsed: 0.539 s
% 62.17/17.83 % (2738147)Peak memory usage: 132 MB
% 62.17/17.83 % (2738147)Instructions burned: 897 (million)
% 62.17/17.83 % (2738147)------------------------------
% 62.17/17.83 % (2738147)------------------------------
% 62.17/17.83 % (2738151)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=501950345:i=9925:aac=none_2859 on theBenchmark for (2859ds/9925Mi)
% 62.17/17.83 % (2738143)Instruction limit reached!
% 62.17/17.83 % (2738143)------------------------------
% 62.17/17.83 % (2738143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738143)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738143)Termination reason: Instruction limit
% 62.17/17.83 % (2738143)Termination phase: Saturation
% 62.17/17.83 % (2738143)Time elapsed: 3.245 s
% 62.17/17.83 % (2738143)Peak memory usage: 111 MB
% 62.17/17.83 % (2738143)Instructions burned: 3706 (million)
% 62.17/17.83 % (2738155)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1328739076:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2841 on theBenchmark for (2841ds/2479Mi)
% 62.17/17.83 % (2738155)Refutation not found, incomplete strategy
% 62.17/17.83 % (2738155)------------------------------
% 62.17/17.83 % (2738155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738155)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738155)Termination reason: Refutation not found, incomplete strategy
% 62.17/17.83 % (2738155)Time elapsed: 0.013 s
% 62.17/17.83 % (2738155)Peak memory usage: 89 MB
% 62.17/17.83 % (2738155)Instructions burned: 12 (million)
% 62.17/17.83 % (2738092)Instruction limit reached!
% 62.17/17.83 % (2738092)------------------------------
% 62.17/17.83 % (2738092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.17/17.83 % (2738092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.17/17.83 % (2738092)CaDiCaL version: 2.1.3
% 62.17/17.83 % (2738092)Termination reason: Instruction limit
% 62.17/17.83 % (2738092)Termination phase: Saturation
% 62.17/17.83 % (2738092)Time elapsed: 13.417 s
% 62.17/17.83 % (2738092)Peak memory usage: 223 MB
% 62.17/17.83 % (2738092)Instructions burned: 13193 (million)
% 62.17/17.83 % (2738155)------------------------------
% 62.17/17.83 % (2738155)------------------------------
% 62.17/17.83 % (2738151)First to succeed.
% 62.17/17.83 % (2738151)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2737909"
% 62.17/17.83 % (2738157)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2897852790:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2835 on theBenchmark for (2835ds/440Mi)
% 62.17/17.83 % (2738158)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2089424687:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2834 on theBenchmark for (2834ds/11145Mi)
% 62.17/17.83 % (2738151)Refutation found. Thanks to Tanya!
% 62.17/17.83 % SZS status Theorem for theBenchmark
% 62.17/17.83 % SZS output start Proof for theBenchmark
% See solution above
% 120.60/18.06 % (2738151)------------------------------
% 120.60/18.06 % (2738151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.60/18.06 % (2738151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.60/18.06 % (2738151)CaDiCaL version: 2.1.3
% 120.60/18.06 % (2738151)Termination reason: Refutation
% 120.60/18.06 % (2738151)Time elapsed: 2.447 s
% 120.60/18.06 % (2738151)Peak memory usage: 174 MB
% 120.60/18.06 % (2738151)Instructions burned: 4929 (million)
% 120.60/18.06 % (2738151)------------------------------
% 120.60/18.06 % (2738151)------------------------------
% 120.60/18.06 % (2737909)Success in time 16.983 s
% 120.60/18.06 % Vampire exiting
%------------------------------------------------------------------------------