%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM691+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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:16:30 PM UTC 2026
% Result : Theorem 91.66s 25.35s
% Output : Refutation 174.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 28
% Syntax : Number of formulae : 182 ( 52 unt; 2 def)
% Number of atoms : 441 ( 20 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 477 ( 218 ~; 192 |; 36 &)
% ( 23 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 17 con; 0-2 aty)
% Number of variables : 213 ( 0 sgn 211 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
<=> pp(aa_bool_bool(scratc1108106884d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_n_is,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__moreis) ).
fof(f35,axiom,
! [X0] : scratc1239817407d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__pl) ).
fof(f53,axiom,
scratc1239358221d_n_is = scratc1720697860d_e_is(scratc1708323542nd_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__is) ).
fof(f100,axiom,
! [X0] : scratc1720697860d_e_is(X0) = fequal_TPTP_ind,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__e__is) ).
fof(f110,axiom,
! [X0] : scratc1108106884d_l_or(X0) = aa_boo1142376798l_bool(scratc1667803201nd_imp,scratc1839933626_d_not(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__l__or) ).
fof(f115,axiom,
! [X0] :
( pp(scratc1839933626_d_not(X0))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1667803201nd_imp,X0),fFalse)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__not) ).
fof(f116,axiom,
scratc1667803201nd_imp = fimplies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__imp) ).
fof(f147,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc597529196_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f151,axiom,
pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_cd)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz22b) ).
fof(f163,axiom,
pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_dq)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz19m) ).
fof(f352,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_dq,X0))
<=> pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__65) ).
fof(f364,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0))
<=> pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__77) ).
fof(f367,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
<=> pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__80) ).
fof(f432,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__145) ).
fof(f444,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__157) ).
fof(f447,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__160) ).
fof(f474,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__187) ).
fof(f508,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__221) ).
fof(f511,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc1959643501all_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__224) ).
fof(f526,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__239) ).
fof(f528,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(scratc1670214954moreis,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__241) ).
fof(f555,axiom,
~ pp(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f556,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(f558,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(f561,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(f565,conjecture,
pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_ad)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f566,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(negated_conjecture,[status(cth)],[f565]) ).
fof(f567,plain,
~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(flattening,[],[f566]) ).
fof(f584,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc597529196_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f147]) ).
fof(f585,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc597529196_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f584]) ).
fof(f676,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f474]) ).
fof(f703,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)) ) ),
inference(ennf_transformation,[],[f526]) ).
fof(f704,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)) ) ),
inference(flattening,[],[f703]) ).
fof(f707,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(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f528]) ).
fof(f708,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(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ) ),
inference(flattening,[],[f707]) ).
fof(f733,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,[],[f561]) ).
fof(f734,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,[],[f733]) ).
fof(f736,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_bool_bool(scratc1108106884d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_n_is,X0),X1))) )
& ( pp(aa_bool_bool(scratc1108106884d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f779,plain,
! [X0] :
( ( pp(scratc1839933626_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1667803201nd_imp,X0),fFalse)) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1667803201nd_imp,X0),fFalse))
| ~ pp(scratc1839933626_d_not(X0)) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f802,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc597529196_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc597529196_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f585]) ).
fof(f803,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc597529196_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc597529196_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1)) ) ),
inference(rectify,[],[f802]) ).
fof(f804,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc597529196_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc597529196_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f803]) ).
fof(f888,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dq,X0))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dq,X0)) ) ),
inference(nnf_transformation,[],[f352]) ).
fof(f900,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0)) ) ),
inference(nnf_transformation,[],[f364]) ).
fof(f903,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0)) ) ),
inference(nnf_transformation,[],[f367]) ).
fof(f983,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1)) ) ),
inference(nnf_transformation,[],[f432]) ).
fof(f995,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1)) ) ),
inference(nnf_transformation,[],[f444]) ).
fof(f998,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1959643501all_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,[],[f447]) ).
fof(f1036,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f676]) ).
fof(f1037,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1),X2)) ) ),
inference(flattening,[],[f1036]) ).
fof(f1085,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f508]) ).
fof(f1088,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc1959643501all_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,[],[f511]) ).
fof(f1107,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f704]) ).
fof(f1108,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f1107]) ).
fof(f1111,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(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f708]) ).
fof(f1112,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(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f1111]) ).
fof(f1168,plain,
! [X0,X1] :
( pp(aa_bool_bool(scratc1108106884d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ),
inference(cnf_transformation,[],[f736]) ).
fof(f1169,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_bool_bool(scratc1108106884d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_n_is,X0),X1))) ),
inference(cnf_transformation,[],[f736]) ).
fof(f1186,plain,
! [X0] : scratc1239817407d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,X0)),
inference(cnf_transformation,[],[f35]) ).
fof(f1212,plain,
scratc1239358221d_n_is = scratc1720697860d_e_is(scratc1708323542nd_nat),
inference(cnf_transformation,[],[f53]) ).
fof(f1276,plain,
! [X0] : scratc1720697860d_e_is(X0) = fequal_TPTP_ind,
inference(cnf_transformation,[],[f100]) ).
fof(f1290,plain,
! [X0] : aa_boo1142376798l_bool(scratc1667803201nd_imp,scratc1839933626_d_not(X0)) = scratc1108106884d_l_or(X0),
inference(cnf_transformation,[],[f110]) ).
fof(f1296,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1667803201nd_imp,X0),fFalse))
| ~ pp(scratc1839933626_d_not(X0)) ),
inference(cnf_transformation,[],[f779]) ).
fof(f1297,plain,
! [X0] :
( pp(scratc1839933626_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1667803201nd_imp,X0),fFalse)) ),
inference(cnf_transformation,[],[f779]) ).
fof(f1298,plain,
scratc1667803201nd_imp = fimplies,
inference(cnf_transformation,[],[f116]) ).
fof(f1360,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc597529196_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1)) ),
inference(cnf_transformation,[],[f804]) ).
fof(f1361,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f804]) ).
fof(f1362,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
| scratc597529196_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f804]) ).
fof(f1363,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f804]) ).
fof(f1368,plain,
pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_cd)),
inference(cnf_transformation,[],[f151]) ).
fof(f1380,plain,
pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_dq)),
inference(cnf_transformation,[],[f163]) ).
fof(f1663,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dq,X0)) ),
inference(cnf_transformation,[],[f888]) ).
fof(f1687,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cd,X0)) ),
inference(cnf_transformation,[],[f900]) ).
fof(f1694,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
inference(cnf_transformation,[],[f903]) ).
fof(f1836,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1)) ),
inference(cnf_transformation,[],[f983]) ).
fof(f1860,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,X0),X1)) ),
inference(cnf_transformation,[],[f995]) ).
fof(f1867,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
inference(cnf_transformation,[],[f998]) ).
fof(f1932,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1),X2)) ),
inference(cnf_transformation,[],[f1037]) ).
fof(f2020,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(X0),X1),X2)) ),
inference(cnf_transformation,[],[f1085]) ).
fof(f2027,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
inference(cnf_transformation,[],[f1088]) ).
fof(f2064,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3)) ),
inference(cnf_transformation,[],[f1108]) ).
fof(f2073,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(scratc1670214954moreis,X0),X1)) ),
inference(cnf_transformation,[],[f1112]) ).
fof(f2074,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(scratc1670214954moreis,X2),X3)) ),
inference(cnf_transformation,[],[f1112]) ).
fof(f2075,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(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1239817407d_n_pl(X1),X3))) ),
inference(cnf_transformation,[],[f1112]) ).
fof(f2141,plain,
~ pp(fFalse),
inference(cnf_transformation,[],[f555]) ).
fof(f2142,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
inference(cnf_transformation,[],[f556]) ).
fof(f2144,plain,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f558]) ).
fof(f2147,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,[],[f734]) ).
fof(f2151,plain,
~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(cnf_transformation,[],[f567]) ).
fof(f2154,plain,
! [X0] : scratc1108106884d_l_or(X0) = aa_boo1142376798l_bool(fimplies,scratc1839933626_d_not(X0)),
inference(definition_unfolding,[],[f1290,f1298]) ).
fof(f2159,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1839933626_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_n_is,X0),X1))) ),
inference(definition_unfolding,[],[f1169,f2154]) ).
fof(f2160,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1839933626_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1)) ),
inference(definition_unfolding,[],[f1168,f2154]) ).
fof(f2176,plain,
scratc1239358221d_n_is = fequal_TPTP_ind,
inference(definition_unfolding,[],[f1212,f1276]) ).
fof(f2203,plain,
! [X0] :
( pp(scratc1839933626_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse)) ),
inference(definition_unfolding,[],[f1297,f1298]) ).
fof(f2204,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse))
| ~ pp(scratc1839933626_d_not(X0)) ),
inference(definition_unfolding,[],[f1296,f1298]) ).
fof(f2273,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,X2)),X0)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,X2)),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(X0),X1),X2)) ),
inference(definition_unfolding,[],[f1932,f1186,f1186]) ).
fof(f2315,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,X1)),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(X0),X1),X2),X3)) ),
inference(definition_unfolding,[],[f2064,f1186,f1186]) ).
fof(f2318,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(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,X1)),X3))) ),
inference(definition_unfolding,[],[f2075,f1186,f1186]) ).
fof(f2356,plain,
gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad)),
inference(resolution,[],[f2151,f1361]) ).
fof(f2357,plain,
scratc597529196_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a),
inference(resolution,[],[f2151,f1362]) ).
fof(f2358,plain,
~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad))),
inference(resolution,[],[f2151,f1363]) ).
fof(f2371,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(scratc1959643501all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f2357,f1360]) ).
fof(f2372,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f2371,f2356]) ).
fof(f2373,plain,
~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(resolution,[],[f2358,f1694]) ).
fof(f2451,plain,
gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(resolution,[],[f2373,f1361]) ).
fof(f2452,plain,
scratc597529196_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a),
inference(resolution,[],[f2373,f1362]) ).
fof(f2453,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,[],[f2373,f1363]) ).
fof(f2465,plain,
~ pp(aa_fun171081125l_bool(scratc1959643501all_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,[],[f2453,f1867]) ).
fof(f2551,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,[],[f2465,f1361]) ).
fof(f2552,plain,
scratc597529196_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,[],[f2465,f1362]) ).
fof(f2553,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,[],[f2465,f1363]) ).
fof(f2633,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,[],[f2451,f2147]) ).
fof(f2646,plain,
! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_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,[],[f2633,f2176]) ).
fof(f2713,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(scratc1959643501all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f2552,f1360]) ).
fof(f2714,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(scratc1959643501all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f2713,f2551]) ).
fof(f2717,plain,
~ pp(aa_fun171081125l_bool(scratc1959643501all_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,[],[f2553,f2027]) ).
fof(f3243,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_cd))
| pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
inference(resolution,[],[f2372,f1687]) ).
fof(f3432,plain,
pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(forward_subsumption_resolution,[],[f3243,f1368]) ).
fof(f4154,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,[],[f2717,f1361]) ).
fof(f4155,plain,
scratc597529196_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,[],[f2717,f1362]) ).
fof(f4156,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,[],[f2717,f1363]) ).
fof(f5650,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,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,[],[f4156,f2073]) ).
fof(f5651,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,[],[f4156,f2074]) ).
fof(f5652,plain,
~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))),
inference(resolution,[],[f4156,f2318]) ).
fof(f5744,plain,
~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1839933626_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))),
inference(resolution,[],[f5652,f2159]) ).
fof(f5908,plain,
pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc1839933626_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_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,[],[f5650,f2160]) ).
fof(f6109,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f4155,f1360]) ).
fof(f6110,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f6109,f4154]) ).
fof(f6267,plain,
( ~ pp(scratc1839933626_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_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,[],[f5908,f2142]) ).
fof(f6278,definition,
( spl25_287
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_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))))) ),
introduced(definition,[new_symbols(definition,[spl25_287])],[avatar_definition]) ).
fof(f6279,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1239358221d_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_287 ),
inference(avatar_component_clause,[],[f6278]) ).
fof(f6281,definition,
( spl25_288
<=> pp(scratc1839933626_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) ),
introduced(definition,[new_symbols(definition,[spl25_288])],[avatar_definition]) ).
fof(f6282,plain,
( ~ pp(scratc1839933626_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl25_288 ),
inference(avatar_component_clause,[],[f6281]) ).
fof(f6283,plain,
( spl25_287
| ~ spl25_288 ),
inference(avatar_split_clause,[],[f6267,f6281,f6278]) ).
fof(f6407,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(scratc1959643501all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f2452,f1360]) ).
fof(f6408,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(scratc1959643501all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f6407,f2451]) ).
fof(f6580,plain,
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),fFalse))
| spl25_288 ),
inference(resolution,[],[f6282,f2203]) ).
fof(f6795,plain,
pp(scratc1839933626_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))),
inference(resolution,[],[f5744,f2144]) ).
fof(f9792,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl25_288 ),
inference(resolution,[],[f6580,f2144]) ).
fof(f9926,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_287 ),
inference(resolution,[],[f6279,f2646]) ).
fof(f9969,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_287 ),
inference(forward_subsumption_resolution,[],[f9926,f2356]) ).
fof(f9973,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_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_287 ),
inference(superposition,[],[f2465,f9969]) ).
fof(f9974,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_287 ),
inference(superposition,[],[f2551,f9969]) ).
fof(f9979,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_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_287 ),
inference(superposition,[],[f2717,f9969]) ).
fof(f9982,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_287 ),
inference(superposition,[],[f4154,f9969]) ).
fof(f9986,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,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_287 ),
inference(superposition,[],[f5651,f9969]) ).
fof(f9987,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,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_287 ),
inference(superposition,[],[f5652,f9969]) ).
fof(f10336,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,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_do(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_287 ),
inference(resolution,[],[f9987,f2273]) ).
fof(f10434,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_do(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_287 ),
inference(forward_subsumption_resolution,[],[f10336,f9986]) ).
fof(f10447,plain,
( ! [X0] :
( ~ scratc597529196_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
| ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_do(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_287 ),
inference(resolution,[],[f10434,f1360]) ).
fof(f10487,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_do(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))))))))
| ~ scratc597529196_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),X0) )
| ~ spl25_287 ),
inference(forward_subsumption_resolution,[],[f10447,f2356]) ).
fof(f10488,plain,
( ~ scratc597529196_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,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_287 ),
inference(resolution,[],[f10487,f1836]) ).
fof(f10511,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,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_287 ),
inference(forward_subsumption_resolution,[],[f10488,f2357]) ).
fof(f10522,plain,
( ! [X0] :
( ~ scratc597529196_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(scratc1959643501all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dp,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_287 ),
inference(resolution,[],[f10511,f1360]) ).
fof(f10581,plain,
( ! [X0] :
( ~ scratc597529196_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(scratc1959643501all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_dp,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_287 ),
inference(forward_subsumption_resolution,[],[f10522,f9982]) ).
fof(f10594,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,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(scratc1959643501all_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_287 ),
inference(resolution,[],[f10581,f1362]) ).
fof(f10596,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,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_287 ),
inference(forward_subsumption_resolution,[],[f10594,f9979]) ).
fof(f10597,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ spl25_287 ),
inference(resolution,[],[f10596,f1663]) ).
fof(f10616,plain,
( ! [X0] :
( ~ scratc597529196_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(scratc1959643501all_of(X0),aTP_Lamm_dq)) )
| ~ spl25_287 ),
inference(resolution,[],[f10597,f1360]) ).
fof(f10673,plain,
( ! [X0] :
( ~ scratc597529196_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(scratc1959643501all_of(X0),aTP_Lamm_dq)) )
| ~ spl25_287 ),
inference(forward_subsumption_resolution,[],[f10616,f9974]) ).
fof(f10686,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aTP_Lamm_dq))
| pp(aa_fun171081125l_bool(scratc1959643501all_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_287 ),
inference(resolution,[],[f10673,f1362]) ).
fof(f10688,plain,
( pp(aa_fun171081125l_bool(scratc1959643501all_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_287 ),
inference(forward_subsumption_resolution,[],[f10686,f1380]) ).
fof(f10689,plain,
( $false
| ~ spl25_287 ),
inference(forward_subsumption_resolution,[],[f10688,f9973]) ).
fof(f10690,plain,
~ spl25_287,
inference(avatar_contradiction_clause,[],[f10689]) ).
fof(f19302,plain,
pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))),fFalse)),
inference(resolution,[],[f6795,f2204]) ).
fof(f19455,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| pp(fFalse) ),
inference(resolution,[],[f19302,f2142]) ).
fof(f19466,plain,
~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1196642810bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1681461093d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))),
inference(forward_subsumption_resolution,[],[f19455,f2141]) ).
fof(f19910,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1670214954moreis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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(scratc2030397760_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
inference(resolution,[],[f19466,f2315]) ).
fof(f20028,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2030397760_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
inference(forward_subsumption_resolution,[],[f19910,f5651]) ).
fof(f20037,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl25_288 ),
inference(forward_subsumption_resolution,[],[f20028,f9792]) ).
fof(f20052,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_ca(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl25_288 ),
inference(resolution,[],[f20037,f6110]) ).
fof(f20100,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl25_288 ),
inference(resolution,[],[f20052,f2020]) ).
fof(f20122,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl25_288 ),
inference(resolution,[],[f20100,f2714]) ).
fof(f20170,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc,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_288 ),
inference(resolution,[],[f20122,f1860]) ).
fof(f20192,plain,
( ~ pp(aa_fun171081125l_bool(scratc1959643501all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl25_288 ),
inference(resolution,[],[f20170,f6408]) ).
fof(f20237,plain,
( $false
| spl25_288 ),
inference(forward_subsumption_resolution,[],[f20192,f3432]) ).
fof(f20238,plain,
spl25_288,
inference(avatar_contradiction_clause,[],[f20237]) ).
cnf(s208,plain,
( spl25_287
| ~ spl25_288 ),
inference(sat_conversion,[],[f6283]) ).
cnf(s365,plain,
~ spl25_287,
inference(sat_conversion,[],[f10690]) ).
cnf(s586,plain,
spl25_288,
inference(sat_conversion,[],[f20238]) ).
cnf(s594,plain,
$false,
inference(rat,[],[s208,s586,s365]) ).
fof(f20239,plain,
$false,
inference(avatar_sat_refutation,[],[s594]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM691+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.38 % Computer : n009.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 21:06:30 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.85/3.38 % (2390127)Detected formulas, will run a generic FOF schedule.
% 16.85/3.38 % (2390234)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2798076800:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 16.85/3.38 % (2390234)Refutation not found, incomplete strategy
% 16.85/3.38 % (2390234)------------------------------
% 16.85/3.38 % (2390234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.85/3.38 % (2390234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.85/3.38 % (2390234)CaDiCaL version: 2.1.3
% 16.85/3.38 % (2390234)Termination reason: Refutation not found, incomplete strategy
% 16.85/3.38 % (2390234)Time elapsed: 0.003 s
% 16.85/3.38 % (2390234)Peak memory usage: 88 MB
% 16.85/3.38 % (2390234)Instructions burned: 3 (million)
% 16.85/3.38 % (2390232)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=1134274287:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 16.85/3.38 % (2390229)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=533941740:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 16.85/3.38 % (2390233)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=290938036:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 16.85/3.38 % (2390233)Refutation not found, incomplete strategy
% 16.85/3.38 % (2390233)------------------------------
% 16.85/3.38 % (2390233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.85/3.38 % (2390233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.85/3.38 % (2390233)CaDiCaL version: 2.1.3
% 16.85/3.38 % (2390233)Termination reason: Refutation not found, incomplete strategy
% 16.85/3.38 % (2390233)Time elapsed: 0.003 s
% 16.85/3.38 % (2390233)Peak memory usage: 88 MB
% 16.85/3.38 % (2390233)Instructions burned: 2 (million)
% 16.85/3.38 % (2390231)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=2897033706:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 16.85/3.38 % (2390236)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1586625355:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 16.85/3.38 % (2390237)dis-21_1_sil=8000:lcm=predicate:random_seed=3809740730: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)
% 16.85/3.38 % (2390237)Instruction limit reached!
% 16.85/3.38 % (2390237)------------------------------
% 16.85/3.38 % (2390237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.85/3.38 % (2390237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.85/3.38 % (2390237)CaDiCaL version: 2.1.3
% 16.85/3.38 % (2390237)Termination reason: Instruction limit
% 16.85/3.38 % (2390237)Termination phase: Saturation
% 16.85/3.38 % (2390237)Time elapsed: 0.071 s
% 16.85/3.38 % (2390237)Peak memory usage: 90 MB
% 16.85/3.38 % (2390237)Instructions burned: 130 (million)
% 16.85/3.38 % (2390236)Instruction limit reached!
% 16.85/3.38 % (2390236)------------------------------
% 16.85/3.38 % (2390236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.85/3.38 % (2390236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.85/3.38 % (2390236)CaDiCaL version: 2.1.3
% 16.85/3.38 % (2390236)Termination reason: Instruction limit
% 16.85/3.38 % (2390236)Termination phase: Saturation
% 16.85/3.38 % (2390236)Time elapsed: 0.081 s
% 16.85/3.38 % (2390236)Peak memory usage: 90 MB
% 16.85/3.38 % (2390236)Instructions burned: 140 (million)
% 16.85/3.38 % (2390234)------------------------------
% 16.85/3.38 % (2390234)------------------------------
% 16.85/3.38 % (2390247)lrs+10_1_sil=8000:sp=occurrence:random_seed=3177606505:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 16.85/3.38 % (2390250)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1023382554:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 16.85/3.38 % (2390247)Refutation not found, incomplete strategy
% 16.85/3.38 % (2390247)------------------------------
% 16.85/3.38 % (2390247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.85/3.38 % (2390247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.30/5.39 % (2390247)CaDiCaL version: 2.1.3
% 31.30/5.39 % (2390247)Termination reason: Refutation not found, incomplete strategy
% 31.30/5.39 % (2390247)Time elapsed: 0.004 s
% 31.30/5.39 % (2390247)Peak memory usage: 88 MB
% 31.30/5.39 % (2390247)Instructions burned: 2 (million)
% 31.30/5.39 % (2390250)Refutation not found, incomplete strategy
% 31.30/5.39 % (2390250)------------------------------
% 31.30/5.39 % (2390250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.30/5.39 % (2390250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.30/5.39 % (2390250)CaDiCaL version: 2.1.3
% 31.30/5.39 % (2390250)Termination reason: Refutation not found, incomplete strategy
% 31.30/5.39 % (2390250)Time elapsed: 0.009 s
% 31.30/5.39 % (2390250)Peak memory usage: 88 MB
% 31.30/5.39 % (2390250)Instructions burned: 9 (million)
% 31.30/5.39 % (2390233)------------------------------
% 31.30/5.39 % (2390233)------------------------------
% 31.30/5.39 % (2390276)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2426813445:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 31.30/5.39 % (2390276)Refutation not found, incomplete strategy
% 31.30/5.39 % (2390276)------------------------------
% 31.30/5.39 % (2390276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.30/5.39 % (2390276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.30/5.39 % (2390276)CaDiCaL version: 2.1.3
% 31.30/5.39 % (2390276)Termination reason: Refutation not found, incomplete strategy
% 31.30/5.39 % (2390276)Time elapsed: 0.008 s
% 31.30/5.39 % (2390276)Peak memory usage: 89 MB
% 31.30/5.39 % (2390276)Instructions burned: 5 (million)
% 31.30/5.39 % (2390286)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=4175489762:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 31.30/5.39 % (2390247)------------------------------
% 31.30/5.39 % (2390247)------------------------------
% 31.30/5.39 % (2390250)------------------------------
% 31.30/5.39 % (2390250)------------------------------
% 31.30/5.39 % (2390286)Instruction limit reached!
% 31.30/5.39 % (2390286)------------------------------
% 31.30/5.39 % (2390286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.30/5.39 % (2390286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.30/5.39 % (2390286)CaDiCaL version: 2.1.3
% 31.30/5.39 % (2390286)Termination reason: Instruction limit
% 31.30/5.39 % (2390286)Termination phase: Saturation
% 31.30/5.39 % (2390286)Time elapsed: 0.208 s
% 31.30/5.39 % (2390286)Peak memory usage: 95 MB
% 31.30/5.39 % (2390286)Instructions burned: 249 (million)
% 31.30/5.39 % (2390296)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=407433649:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 31.30/5.39 % (2390296)Refutation not found, incomplete strategy
% 31.30/5.39 % (2390296)------------------------------
% 31.30/5.39 % (2390296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.30/5.39 % (2390296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.30/5.39 % (2390296)CaDiCaL version: 2.1.3
% 31.30/5.39 % (2390296)Termination reason: Refutation not found, incomplete strategy
% 31.30/5.39 % (2390296)Time elapsed: 0.008 s
% 31.30/5.39 % (2390296)Peak memory usage: 88 MB
% 31.30/5.39 % (2390296)Instructions burned: 6 (million)
% 31.30/5.39 % (2390276)------------------------------
% 31.30/5.39 % (2390276)------------------------------
% 31.30/5.39 % (2390297)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=729598219:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 31.30/5.39 % (2390304)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=899567784:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 31.30/5.39 % (2390304)Instruction limit reached!
% 31.30/5.39 % (2390304)------------------------------
% 31.30/5.39 % (2390304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.30/5.39 % (2390304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.30/5.39 % (2390304)CaDiCaL version: 2.1.3
% 31.30/5.39 % (2390304)Termination reason: Instruction limit
% 31.30/5.39 % (2390304)Termination phase: Saturation
% 31.30/5.39 % (2390304)Time elapsed: 0.103 s
% 31.30/5.39 % (2390304)Peak memory usage: 91 MB
% 31.30/5.39 % (2390304)Instructions burned: 113 (million)
% 31.30/5.39 % (2390306)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3206938453:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 67.48/10.41 % (2390296)------------------------------
% 67.48/10.41 % (2390296)------------------------------
% 67.48/10.41 % (2390306)Instruction limit reached!
% 67.48/10.41 % (2390306)------------------------------
% 67.48/10.41 % (2390306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.48/10.41 % (2390306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.48/10.41 % (2390306)CaDiCaL version: 2.1.3
% 67.48/10.41 % (2390306)Termination reason: Instruction limit
% 67.48/10.41 % (2390306)Termination phase: Saturation
% 67.48/10.41 % (2390306)Time elapsed: 0.107 s
% 67.48/10.41 % (2390306)Peak memory usage: 89 MB
% 67.48/10.41 % (2390306)Instructions burned: 127 (million)
% 67.48/10.41 % (2390312)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=967638228:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 67.48/10.41 % (2390312)Instruction limit reached!
% 67.48/10.41 % (2390312)------------------------------
% 67.48/10.41 % (2390312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.48/10.41 % (2390312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.48/10.41 % (2390312)CaDiCaL version: 2.1.3
% 67.48/10.41 % (2390312)Termination reason: Instruction limit
% 67.48/10.41 % (2390312)Termination phase: Saturation
% 67.48/10.41 % (2390312)Time elapsed: 0.107 s
% 67.48/10.41 % (2390312)Peak memory usage: 89 MB
% 67.48/10.41 % (2390312)Instructions burned: 115 (million)
% 67.48/10.41 % (2390318)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=864025007:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 67.48/10.41 % (2390317)lrs+10_1_sil=8000:sp=occurrence:random_seed=3483751658:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 67.48/10.41 % (2390317)Refutation not found, incomplete strategy
% 67.48/10.41 % (2390317)------------------------------
% 67.48/10.41 % (2390317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.48/10.41 % (2390317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.48/10.41 % (2390317)CaDiCaL version: 2.1.3
% 67.48/10.41 % (2390317)Termination reason: Refutation not found, incomplete strategy
% 67.48/10.41 % (2390317)Time elapsed: 0.005 s
% 67.48/10.41 % (2390317)Peak memory usage: 88 MB
% 67.48/10.41 % (2390317)Instructions burned: 3 (million)
% 67.48/10.41 % (2390318)Refutation not found, incomplete strategy
% 67.48/10.41 % (2390318)------------------------------
% 67.48/10.41 % (2390318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.48/10.41 % (2390318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.48/10.41 % (2390318)CaDiCaL version: 2.1.3
% 67.48/10.41 % (2390318)Termination reason: Refutation not found, incomplete strategy
% 67.48/10.41 % (2390318)Time elapsed: 0.071 s
% 67.48/10.41 % (2390318)Peak memory usage: 90 MB
% 67.48/10.41 % (2390318)Instructions burned: 80 (million)
% 67.48/10.41 % (2390322)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3475527780:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 67.48/10.41 % (2390317)------------------------------
% 67.48/10.41 % (2390317)------------------------------
% 67.48/10.41 % (2390318)------------------------------
% 67.48/10.41 % (2390318)------------------------------
% 67.48/10.41 % (2390328)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1105147578:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 67.48/10.41 % (2390329)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1205711078:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 67.48/10.41 % (2390329)Refutation not found, incomplete strategy
% 67.48/10.41 % (2390329)------------------------------
% 67.48/10.41 % (2390329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.48/10.41 % (2390329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.48/10.41 % (2390329)CaDiCaL version: 2.1.3
% 67.48/10.41 % (2390329)Termination reason: Refutation not found, incomplete strategy
% 67.48/10.41 % (2390329)Time elapsed: 0.027 s
% 67.48/10.41 % (2390329)Peak memory usage: 89 MB
% 67.48/10.41 % (2390329)Instructions burned: 29 (million)
% 67.48/10.41 % (2390328)Instruction limit reached!
% 67.48/10.41 % (2390328)------------------------------
% 67.48/10.41 % (2390328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.48/10.41 % (2390328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.67/16.35 % (2390328)CaDiCaL version: 2.1.3
% 109.67/16.35 % (2390328)Termination reason: Instruction limit
% 109.67/16.35 % (2390328)Termination phase: Saturation
% 109.67/16.35 % (2390328)Time elapsed: 0.118 s
% 109.67/16.35 % (2390328)Peak memory usage: 94 MB
% 109.67/16.35 % (2390328)Instructions burned: 134 (million)
% 109.67/16.35 % (2390332)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3216415626:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 109.67/16.35 % (2390329)------------------------------
% 109.67/16.35 % (2390329)------------------------------
% 109.67/16.35 % (2390336)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=3965899865:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/125Mi)
% 109.67/16.35 % (2390336)Refutation not found, incomplete strategy
% 109.67/16.35 % (2390336)------------------------------
% 109.67/16.35 % (2390336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.67/16.35 % (2390336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.67/16.35 % (2390336)CaDiCaL version: 2.1.3
% 109.67/16.35 % (2390336)Termination reason: Refutation not found, incomplete strategy
% 109.67/16.35 % (2390336)Time elapsed: 0.012 s
% 109.67/16.35 % (2390336)Peak memory usage: 89 MB
% 109.67/16.35 % (2390336)Instructions burned: 12 (million)
% 109.67/16.35 % (2390336)------------------------------
% 109.67/16.35 % (2390336)------------------------------
% 109.67/16.35 % (2390297)Instruction limit reached!
% 109.67/16.35 % (2390297)------------------------------
% 109.67/16.35 % (2390297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.67/16.35 % (2390297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.67/16.35 % (2390297)CaDiCaL version: 2.1.3
% 109.67/16.35 % (2390297)Termination reason: Instruction limit
% 109.67/16.35 % (2390297)Termination phase: Saturation
% 109.67/16.35 % (2390297)Time elapsed: 2.458 s
% 109.67/16.35 % (2390297)Peak memory usage: 142 MB
% 109.67/16.35 % (2390297)Instructions burned: 2350 (million)
% 109.67/16.35 % (2390342)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2662240080:i=134:gtgl=5:slsql=off:gtg=exists_sym_2964 on theBenchmark for (2964ds/134Mi)
% 109.67/16.35 % (2390343)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2393292150:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/141Mi)
% 109.67/16.36 % (2390343)Refutation not found, incomplete strategy
% 109.67/16.36 % (2390343)------------------------------
% 109.67/16.36 % (2390343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.67/16.36 % (2390343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.67/16.36 % (2390343)CaDiCaL version: 2.1.3
% 109.67/16.36 % (2390343)Termination reason: Refutation not found, incomplete strategy
% 109.67/16.36 % (2390343)Time elapsed: 0.004 s
% 109.67/16.36 % (2390343)Peak memory usage: 88 MB
% 109.67/16.36 % (2390343)Instructions burned: 2 (million)
% 109.67/16.36 % (2390342)Instruction limit reached!
% 109.67/16.36 % (2390342)------------------------------
% 109.67/16.36 % (2390342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.67/16.36 % (2390342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.67/16.36 % (2390342)CaDiCaL version: 2.1.3
% 109.67/16.36 % (2390342)Termination reason: Instruction limit
% 109.67/16.36 % (2390342)Termination phase: Saturation
% 109.67/16.36 % (2390342)Time elapsed: 0.115 s
% 109.67/16.36 % (2390342)Peak memory usage: 92 MB
% 109.67/16.36 % (2390342)Instructions burned: 134 (million)
% 109.67/16.36 % (2390346)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3231824488:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2960 on theBenchmark for (2960ds/431Mi)
% 109.67/16.36 % (2390346)Refutation not found, incomplete strategy
% 109.67/16.36 % (2390346)------------------------------
% 109.67/16.36 % (2390346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.67/16.36 % (2390346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.67/16.36 % (2390346)CaDiCaL version: 2.1.3
% 109.67/16.36 % (2390346)Termination reason: Refutation not found, incomplete strategy
% 109.67/16.36 % (2390346)Time elapsed: 0.005 s
% 109.67/16.36 % (2390346)Peak memory usage: 89 MB
% 109.67/16.36 % (2390346)Instructions burned: 2 (million)
% 109.67/16.36 % (2390343)------------------------------
% 109.67/16.36 % (2390343)------------------------------
% 109.67/16.36 % (2390346)------------------------------
% 109.67/16.36 % (2390346)------------------------------
% 139.51/20.54 % (2390350)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=462555342:i=6060:aac=none:ins=25_2957 on theBenchmark for (2957ds/6060Mi)
% 139.51/20.54 % (2390356)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=622049059:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2954 on theBenchmark for (2954ds/150Mi)
% 139.51/20.54 % (2390356)Instruction limit reached!
% 139.51/20.54 % (2390356)------------------------------
% 139.51/20.54 % (2390356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.51/20.54 % (2390356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.51/20.54 % (2390356)CaDiCaL version: 2.1.3
% 139.51/20.54 % (2390356)Termination reason: Instruction limit
% 139.51/20.54 % (2390356)Termination phase: Saturation
% 139.51/20.54 % (2390356)Time elapsed: 0.083 s
% 139.51/20.54 % (2390356)Peak memory usage: 91 MB
% 139.51/20.54 % (2390356)Instructions burned: 151 (million)
% 139.51/20.54 % (2390360)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3718217723:i=14155:bd=all_2951 on theBenchmark for (2951ds/14155Mi)
% 139.51/20.54 % (2390322)Instruction limit reached!
% 139.51/20.54 % (2390322)------------------------------
% 139.51/20.54 % (2390322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.51/20.54 % (2390322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.51/20.54 % (2390322)CaDiCaL version: 2.1.3
% 139.51/20.54 % (2390322)Termination reason: Instruction limit
% 139.51/20.54 % (2390322)Termination phase: Saturation
% 139.51/20.54 % (2390322)Time elapsed: 5.317 s
% 139.51/20.54 % (2390322)Peak memory usage: 159 MB
% 139.51/20.54 % (2390322)Instructions burned: 5203 (million)
% 139.51/20.54 % (2390372)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3434575262:i=667:av=off:fsr=off_2926 on theBenchmark for (2926ds/667Mi)
% 139.51/20.54 % (2390372)Instruction limit reached!
% 139.51/20.54 % (2390372)------------------------------
% 139.51/20.54 % (2390372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.51/20.54 % (2390372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.51/20.54 % (2390372)CaDiCaL version: 2.1.3
% 139.51/20.54 % (2390372)Termination reason: Instruction limit
% 139.51/20.54 % (2390372)Termination phase: Saturation
% 139.51/20.54 % (2390372)Time elapsed: 0.543 s
% 139.51/20.54 % (2390372)Peak memory usage: 100 MB
% 139.51/20.54 % (2390372)Instructions burned: 667 (million)
% 139.51/20.54 % (2390378)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=1376290347:s2a=on:i=185:s2at=1.8:fdi=4_2918 on theBenchmark for (2918ds/185Mi)
% 139.51/20.54 % (2390378)Instruction limit reached!
% 139.51/20.54 % (2390378)------------------------------
% 139.51/20.54 % (2390378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.51/20.54 % (2390378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.51/20.54 % (2390378)CaDiCaL version: 2.1.3
% 139.51/20.54 % (2390378)Termination reason: Instruction limit
% 139.51/20.54 % (2390378)Termination phase: Saturation
% 139.51/20.54 % (2390378)Time elapsed: 0.146 s
% 139.51/20.54 % (2390378)Peak memory usage: 91 MB
% 139.51/20.54 % (2390378)Instructions burned: 185 (million)
% 139.51/20.54 % (2390380)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2140898557:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2914 on theBenchmark for (2914ds/193Mi)
% 139.51/20.54 % (2390380)Refutation not found, incomplete strategy
% 139.51/20.54 % (2390380)------------------------------
% 139.51/20.54 % (2390380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.51/20.54 % (2390380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.51/20.54 % (2390380)CaDiCaL version: 2.1.3
% 139.51/20.54 % (2390380)Termination reason: Refutation not found, incomplete strategy
% 139.51/20.54 % (2390380)Time elapsed: 0.007 s
% 139.51/20.54 % (2390380)Peak memory usage: 89 MB
% 139.51/20.54 % (2390380)Instructions burned: 5 (million)
% 139.51/20.54 % (2390380)------------------------------
% 139.51/20.54 % (2390380)------------------------------
% 139.51/20.54 % (2390384)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2505193197:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2907 on theBenchmark for (2907ds/4850Mi)
% 91.66/25.35 % (2390350)Instruction limit reached!
% 91.66/25.35 % (2390350)------------------------------
% 91.66/25.35 % (2390350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390350)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390350)Termination reason: Instruction limit
% 91.66/25.35 % (2390350)Termination phase: Saturation
% 91.66/25.35 % (2390350)Time elapsed: 6.123 s
% 91.66/25.35 % (2390350)Peak memory usage: 191 MB
% 91.66/25.35 % (2390350)Instructions burned: 6060 (million)
% 91.66/25.35 % (2390388)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=830784844:i=12111:sd=1:ss=included_2893 on theBenchmark for (2893ds/12111Mi)
% 91.66/25.35 % (2390332)Instruction limit reached!
% 91.66/25.35 % (2390332)------------------------------
% 91.66/25.35 % (2390332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390332)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390332)Termination reason: Instruction limit
% 91.66/25.35 % (2390332)Termination phase: Saturation
% 91.66/25.35 % (2390332)Time elapsed: 10.686 s
% 91.66/25.35 % (2390332)Peak memory usage: 187 MB
% 91.66/25.35 % (2390332)Instructions burned: 13194 (million)
% 91.66/25.35 % (2390396)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1307516106:i=319:kws=precedence:fsr=off_2864 on theBenchmark for (2864ds/319Mi)
% 91.66/25.35 % (2390396)Instruction limit reached!
% 91.66/25.35 % (2390396)------------------------------
% 91.66/25.35 % (2390396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390396)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390396)Termination reason: Instruction limit
% 91.66/25.35 % (2390396)Termination phase: Saturation
% 91.66/25.35 % (2390396)Time elapsed: 0.278 s
% 91.66/25.35 % (2390396)Peak memory usage: 93 MB
% 91.66/25.35 % (2390396)Instructions burned: 320 (million)
% 91.66/25.35 % (2390384)Instruction limit reached!
% 91.66/25.35 % (2390384)------------------------------
% 91.66/25.35 % (2390384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390384)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390384)Termination reason: Instruction limit
% 91.66/25.35 % (2390384)Termination phase: Saturation
% 91.66/25.35 % (2390384)Time elapsed: 4.762 s
% 91.66/25.35 % (2390384)Peak memory usage: 152 MB
% 91.66/25.35 % (2390384)Instructions burned: 4851 (million)
% 91.66/25.35 % (2390400)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=689934913:i=2064:ep=RST_2859 on theBenchmark for (2859ds/2064Mi)
% 91.66/25.35 % (2390400)Refutation not found, incomplete strategy
% 91.66/25.35 % (2390400)------------------------------
% 91.66/25.35 % (2390400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390400)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390400)Termination reason: Refutation not found, incomplete strategy
% 91.66/25.35 % (2390400)Time elapsed: 0.060 s
% 91.66/25.35 % (2390400)Peak memory usage: 90 MB
% 91.66/25.35 % (2390400)Instructions burned: 69 (million)
% 91.66/25.35 % (2390401)dis-1011_128_sil=32000:random_seed=282496498:i=3706:ep=RST:av=off_2856 on theBenchmark for (2856ds/3706Mi)
% 91.66/25.35 % (2390400)------------------------------
% 91.66/25.35 % (2390400)------------------------------
% 91.66/25.35 % (2390404)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3321425583:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2851 on theBenchmark for (2851ds/757Mi)
% 91.66/25.35 % (2390404)Refutation not found, incomplete strategy
% 91.66/25.35 % (2390404)------------------------------
% 91.66/25.35 % (2390404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390404)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390404)Termination reason: Refutation not found, incomplete strategy
% 91.66/25.35 % (2390404)Time elapsed: 0.011 s
% 91.66/25.35 % (2390404)Peak memory usage: 89 MB
% 91.66/25.35 % (2390404)Instructions burned: 9 (million)
% 91.66/25.35 % (2390404)------------------------------
% 91.66/25.35 % (2390404)------------------------------
% 91.66/25.35 % (2390408)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1403534642:i=13913:ss=axioms:sgt=8_2844 on theBenchmark for (2844ds/13913Mi)
% 91.66/25.35 % (2390408)Refutation not found, incomplete strategy
% 91.66/25.35 % (2390408)------------------------------
% 91.66/25.35 % (2390408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390408)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390408)Termination reason: Refutation not found, incomplete strategy
% 91.66/25.35 % (2390408)Time elapsed: 0.912 s
% 91.66/25.35 % (2390408)Peak memory usage: 128 MB
% 91.66/25.35 % (2390408)Instructions burned: 876 (million)
% 91.66/25.35 % (2390408)------------------------------
% 91.66/25.35 % (2390408)------------------------------
% 91.66/25.35 % (2390410)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=408203100:i=9925:aac=none_2829 on theBenchmark for (2829ds/9925Mi)
% 91.66/25.35 % (2390360)Instruction limit reached!
% 91.66/25.35 % (2390360)------------------------------
% 91.66/25.35 % (2390360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390360)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390360)Termination reason: Instruction limit
% 91.66/25.35 % (2390360)Termination phase: Saturation
% 91.66/25.35 % (2390360)Time elapsed: 12.818 s
% 91.66/25.35 % (2390360)Peak memory usage: 199 MB
% 91.66/25.35 % (2390360)Instructions burned: 14155 (million)
% 91.66/25.35 % (2390401)Instruction limit reached!
% 91.66/25.35 % (2390401)------------------------------
% 91.66/25.35 % (2390401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390401)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390401)Termination reason: Instruction limit
% 91.66/25.35 % (2390401)Termination phase: Saturation
% 91.66/25.35 % (2390401)Time elapsed: 3.266 s
% 91.66/25.35 % (2390401)Peak memory usage: 113 MB
% 91.66/25.35 % (2390401)Instructions burned: 3707 (million)
% 91.66/25.35 % (2390414)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3017782770:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2821 on theBenchmark for (2821ds/2479Mi)
% 91.66/25.35 % (2390414)Refutation not found, incomplete strategy
% 91.66/25.35 % (2390414)------------------------------
% 91.66/25.35 % (2390414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390414)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390414)Termination reason: Refutation not found, incomplete strategy
% 91.66/25.35 % (2390414)Time elapsed: 0.006 s
% 91.66/25.35 % (2390414)Peak memory usage: 88 MB
% 91.66/25.35 % (2390414)Instructions burned: 5 (million)
% 91.66/25.35 % (2390415)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2011605251:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2820 on theBenchmark for (2820ds/440Mi)
% 91.66/25.35 % (2390415)Instruction limit reached!
% 91.66/25.35 % (2390415)------------------------------
% 91.66/25.35 % (2390415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390415)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390415)Termination reason: Instruction limit
% 91.66/25.35 % (2390415)Termination phase: Saturation
% 91.66/25.35 % (2390415)Time elapsed: 0.324 s
% 91.66/25.35 % (2390415)Peak memory usage: 91 MB
% 91.66/25.35 % (2390415)Instructions burned: 440 (million)
% 91.66/25.35 % (2390414)------------------------------
% 91.66/25.35 % (2390414)------------------------------
% 91.66/25.35 % (2390418)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=50668807:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2814 on theBenchmark for (2814ds/11145Mi)
% 91.66/25.35 % (2390419)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4002801827:cts=off:i=3034:av=off:er=known:fsd=on_2814 on theBenchmark for (2814ds/3034Mi)
% 91.66/25.35 % (2390418)Refutation not found, incomplete strategy
% 91.66/25.35 % (2390418)------------------------------
% 91.66/25.35 % (2390418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390418)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390418)Termination reason: Refutation not found, incomplete strategy
% 91.66/25.35 % (2390418)Time elapsed: 0.920 s
% 91.66/25.35 % (2390418)Peak memory usage: 129 MB
% 91.66/25.35 % (2390418)Instructions burned: 913 (million)
% 91.66/25.35 % (2390418)------------------------------
% 91.66/25.35 % (2390418)------------------------------
% 91.66/25.35 % (2390424)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1670178280:st=2:s2a=on:i=524:s2at=2:ss=axioms_2799 on theBenchmark for (2799ds/524Mi)
% 91.66/25.35 % (2390424)Refutation not found, incomplete strategy
% 91.66/25.35 % (2390424)------------------------------
% 91.66/25.35 % (2390424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390424)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390424)Termination reason: Refutation not found, incomplete strategy
% 91.66/25.35 % (2390424)Time elapsed: 0.009 s
% 91.66/25.35 % (2390424)Peak memory usage: 88 MB
% 91.66/25.35 % (2390424)Instructions burned: 7 (million)
% 91.66/25.35 % (2390424)------------------------------
% 91.66/25.35 % (2390424)------------------------------
% 91.66/25.35 % (2390426)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4042465661:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2792 on theBenchmark for (2792ds/1016Mi)
% 91.66/25.35 % (2390426)Refutation not found, incomplete strategy
% 91.66/25.35 % (2390426)------------------------------
% 91.66/25.35 % (2390426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390426)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390426)Termination reason: Refutation not found, incomplete strategy
% 91.66/25.35 % (2390426)Time elapsed: 0.005 s
% 91.66/25.35 % (2390426)Peak memory usage: 89 MB
% 91.66/25.35 % (2390426)Instructions burned: 2 (million)
% 91.66/25.35 % (2390426)------------------------------
% 91.66/25.35 % (2390426)------------------------------
% 91.66/25.35 % (2390419)Instruction limit reached!
% 91.66/25.35 % (2390419)------------------------------
% 91.66/25.35 % (2390419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390419)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390419)Termination reason: Instruction limit
% 91.66/25.35 % (2390419)Termination phase: Saturation
% 91.66/25.35 % (2390419)Time elapsed: 2.882 s
% 91.66/25.35 % (2390419)Peak memory usage: 150 MB
% 91.66/25.35 % (2390419)Instructions burned: 3035 (million)
% 91.66/25.35 % (2390428)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3462751080:i=14123:bd=preordered:ins=4_2785 on theBenchmark for (2785ds/14123Mi)
% 91.66/25.35 % (2390429)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2214602368:i=5781:kws=precedence:bd=all:rawr=on_2783 on theBenchmark for (2783ds/5781Mi)
% 91.66/25.35 % (2390388)Instruction limit reached!
% 91.66/25.35 % (2390388)------------------------------
% 91.66/25.35 % (2390388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.66/25.35 % (2390388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.66/25.35 % (2390388)CaDiCaL version: 2.1.3
% 91.66/25.35 % (2390388)Termination reason: Instruction limit
% 91.66/25.35 % (2390388)Termination phase: Saturation
% 91.66/25.35 % (2390388)Time elapsed: 11.359 s
% 91.66/25.35 % (2390388)Peak memory usage: 301 MB
% 91.66/25.35 % (2390388)Instructions burned: 12111 (million)
% 91.66/25.35 % (2390432)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1000165785:i=2448:gtgl=5:bd=preordered:gtg=all_2776 on theBenchmark for (2776ds/2448Mi)
% 91.66/25.35 % (2390410)First to succeed.
% 91.66/25.35 % (2390410)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2390127"
% 91.66/25.35 % (2390410)Refutation found. Thanks to Tanya!
% 91.66/25.35 % SZS status Theorem for theBenchmark
% 91.66/25.35 % SZS output start Proof for theBenchmark
% See solution above
% 174.06/25.62 % (2390410)------------------------------
% 174.06/25.62 % (2390410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 174.06/25.62 % (2390410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.06/25.62 % (2390410)CaDiCaL version: 2.1.3
% 174.06/25.62 % (2390410)Termination reason: Refutation
% 174.06/25.62 % (2390410)Time elapsed: 6.593 s
% 174.06/25.62 % (2390410)Peak memory usage: 184 MB
% 174.06/25.62 % (2390410)Instructions burned: 6773 (million)
% 174.06/25.62 % (2390410)------------------------------
% 174.06/25.62 % (2390410)------------------------------
% 174.06/25.62 % (2390127)Success in time 24.48 s
% 174.06/25.62 % Vampire exiting
%------------------------------------------------------------------------------