%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM761+4 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:53 PM UTC 2026
% Result : Theorem 97.06s 25.61s
% Output : Refutation 175.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 26
% Syntax : Number of formulae : 159 ( 42 unt; 4 def)
% Number of atoms : 395 ( 5 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 405 ( 169 ~; 163 |; 38 &)
% ( 27 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 13 con; 0-2 aty)
% Number of variables : 196 ( 0 sgn 194 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f33,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1))
<=> pp(aa_bool_bool(scratc230981372d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__moreq) ).
fof(f162,axiom,
! [X0] : scratc230981372d_l_or(X0) = aa_boo1142376798l_bool(scratc1706525881nd_imp,scratc812852802_d_not(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__l__or) ).
fof(f167,axiom,
! [X0] :
( pp(scratc812852802_d_not(X0))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1706525881nd_imp,X0),fFalse)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__d__not) ).
fof(f168,axiom,
scratc1706525881nd_imp = fimplies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__imp) ).
fof(f199,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc1717932020_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f202,axiom,
pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_cg)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz64) ).
fof(f212,axiom,
pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_do)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz62g) ).
fof(f628,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_do,X0))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dn,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__176) ).
fof(f638,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cg,X0))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cf,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__186) ).
fof(f640,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__188) ).
fof(f815,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dn,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__363) ).
fof(f825,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cf,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ce(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__373) ).
fof(f827,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__375) ).
fof(f951,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__499) ).
fof(f955,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ce(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__503) ).
fof(f957,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__505) ).
fof(f985,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(scratc1131351561_moreq,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__533) ).
fof(f987,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__535) ).
fof(f999,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__547) ).
fof(f1031,axiom,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fimplies_3_1_U) ).
fof(f1033,axiom,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fimplies_1_1_U) ).
fof(f1040,conjecture,
pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_ad)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1041,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(negated_conjecture,[status(cth)],[f1040]) ).
fof(f1042,plain,
~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(flattening,[],[f1041]) ).
fof(f1059,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1717932020_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f199]) ).
fof(f1060,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1717932020_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f1059]) ).
fof(f1265,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(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1)) ) ),
inference(ennf_transformation,[],[f985]) ).
fof(f1266,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(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1)) ) ),
inference(flattening,[],[f1265]) ).
fof(f1269,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1)) ) ),
inference(ennf_transformation,[],[f987]) ).
fof(f1270,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1)) ) ),
inference(flattening,[],[f1269]) ).
fof(f1293,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1)) ) ),
inference(ennf_transformation,[],[f999]) ).
fof(f1294,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1)) ) ),
inference(flattening,[],[f1293]) ).
fof(f1325,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1))
| ~ pp(aa_bool_bool(scratc230981372d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1))) )
& ( pp(aa_bool_bool(scratc230981372d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1)) ) ),
inference(nnf_transformation,[],[f33]) ).
fof(f1382,plain,
! [X0] :
( ( pp(scratc812852802_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1706525881nd_imp,X0),fFalse)) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1706525881nd_imp,X0),fFalse))
| ~ pp(scratc812852802_d_not(X0)) ) ),
inference(nnf_transformation,[],[f167]) ).
fof(f1405,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1717932020_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1717932020_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f1060]) ).
fof(f1406,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1717932020_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1717932020_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1)) ) ),
inference(rectify,[],[f1405]) ).
fof(f1407,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc1717932020_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1717932020_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1406]) ).
fof(f1602,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_do,X0))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dn,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dn,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_do,X0)) ) ),
inference(nnf_transformation,[],[f628]) ).
fof(f1612,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cg,X0))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cf,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cf,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cg,X0)) ) ),
inference(nnf_transformation,[],[f638]) ).
fof(f1614,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0)) ) ),
inference(nnf_transformation,[],[f640]) ).
fof(f1825,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dn,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dn,X0),X1)) ) ),
inference(nnf_transformation,[],[f815]) ).
fof(f1835,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cf,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ce(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ce(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cf,X0),X1)) ) ),
inference(nnf_transformation,[],[f825]) ).
fof(f1837,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_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,[],[f827]) ).
fof(f2019,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f951]) ).
fof(f2023,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ce(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ce(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f955]) ).
fof(f2025,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc1636642277all_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,[],[f957]) ).
fof(f2068,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(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f1266]) ).
fof(f2069,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(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f2068]) ).
fof(f2072,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f1270]) ).
fof(f2073,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f2072]) ).
fof(f2096,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f1294]) ).
fof(f2097,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f2096]) ).
fof(f2162,plain,
! [X0,X1] :
( pp(aa_bool_bool(scratc230981372d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1)) ),
inference(cnf_transformation,[],[f1325]) ).
fof(f2343,plain,
! [X0] : aa_boo1142376798l_bool(scratc1706525881nd_imp,scratc812852802_d_not(X0)) = scratc230981372d_l_or(X0),
inference(cnf_transformation,[],[f162]) ).
fof(f2350,plain,
! [X0] :
( pp(scratc812852802_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1706525881nd_imp,X0),fFalse)) ),
inference(cnf_transformation,[],[f1382]) ).
fof(f2351,plain,
scratc1706525881nd_imp = fimplies,
inference(cnf_transformation,[],[f168]) ).
fof(f2413,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1717932020_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1407]) ).
fof(f2414,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f1407]) ).
fof(f2415,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
| scratc1717932020_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f1407]) ).
fof(f2416,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f1407]) ).
fof(f2420,plain,
pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_cg)),
inference(cnf_transformation,[],[f202]) ).
fof(f2430,plain,
pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_do)),
inference(cnf_transformation,[],[f212]) ).
fof(f3051,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dn,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_do,X0)) ),
inference(cnf_transformation,[],[f1602]) ).
fof(f3071,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cf,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cg,X0)) ),
inference(cnf_transformation,[],[f1612]) ).
fof(f3076,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
inference(cnf_transformation,[],[f1614]) ).
fof(f3459,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dn,X0),X1)) ),
inference(cnf_transformation,[],[f1825]) ).
fof(f3479,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ce(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cf,X0),X1)) ),
inference(cnf_transformation,[],[f1835]) ).
fof(f3484,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
inference(cnf_transformation,[],[f1837]) ).
fof(f3802,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm(X0),X1),X2)) ),
inference(cnf_transformation,[],[f2019]) ).
fof(f3810,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ce(X0),X1),X2)) ),
inference(cnf_transformation,[],[f2023]) ).
fof(f3815,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
inference(cnf_transformation,[],[f2025]) ).
fof(f3903,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(scratc1131351561_moreq,X0),X1)) ),
inference(cnf_transformation,[],[f2069]) ).
fof(f3904,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(scratc1131351550_moref,X2),X3)) ),
inference(cnf_transformation,[],[f2069]) ).
fof(f3905,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(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3))) ),
inference(cnf_transformation,[],[f2069]) ).
fof(f3911,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(X0),X1),X2),X3)) ),
inference(cnf_transformation,[],[f2073]) ).
fof(f3961,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(X0),X1),X2),X3)) ),
inference(cnf_transformation,[],[f2097]) ).
fof(f4038,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
inference(cnf_transformation,[],[f1031]) ).
fof(f4040,plain,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f1033]) ).
fof(f4047,plain,
~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(cnf_transformation,[],[f1042]) ).
fof(f4050,plain,
! [X0] : scratc230981372d_l_or(X0) = aa_boo1142376798l_bool(fimplies,scratc812852802_d_not(X0)),
inference(definition_unfolding,[],[f2343,f2351]) ).
fof(f4058,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc812852802_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,X0),X1)) ),
inference(definition_unfolding,[],[f2162,f4050]) ).
fof(f4132,plain,
! [X0] :
( pp(scratc812852802_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse)) ),
inference(definition_unfolding,[],[f2350,f2351]) ).
fof(f4383,plain,
gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad)),
inference(resolution,[],[f4047,f2414]) ).
fof(f4384,plain,
scratc1717932020_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a),
inference(resolution,[],[f4047,f2415]) ).
fof(f4385,plain,
~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad))),
inference(resolution,[],[f4047,f2416]) ).
fof(f4398,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(scratc1636642277all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f4384,f2413]) ).
fof(f4399,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f4398,f4383]) ).
fof(f4400,plain,
~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(resolution,[],[f4385,f3076]) ).
fof(f4478,plain,
gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(resolution,[],[f4400,f2414]) ).
fof(f4479,plain,
scratc1717932020_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a),
inference(resolution,[],[f4400,f2415]) ).
fof(f4480,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,[],[f4400,f2416]) ).
fof(f4492,plain,
~ pp(aa_fun171081125l_bool(scratc1636642277all_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,[],[f4480,f3484]) ).
fof(f4578,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,[],[f4492,f2414]) ).
fof(f4579,plain,
scratc1717932020_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,[],[f4492,f2415]) ).
fof(f4580,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,[],[f4492,f2416]) ).
fof(f4741,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(scratc1636642277all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f4579,f2413]) ).
fof(f4742,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(scratc1636642277all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f4741,f4578]) ).
fof(f5477,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_cg))
| pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cf,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
inference(resolution,[],[f4399,f3071]) ).
fof(f5487,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aTP_Lamm_do))
| pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dn,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
inference(resolution,[],[f4399,f3051]) ).
fof(f6669,plain,
pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dn,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(forward_subsumption_resolution,[],[f5487,f2430]) ).
fof(f6679,plain,
pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cf,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),
inference(forward_subsumption_resolution,[],[f5477,f2420]) ).
fof(f7038,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(scratc1636642277all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f4479,f2413]) ).
fof(f7039,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(scratc1636642277all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f7038,f4478]) ).
fof(f7165,plain,
~ pp(aa_fun171081125l_bool(scratc1636642277all_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,[],[f4580,f3815]) ).
fof(f8219,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,[],[f7165,f2414]) ).
fof(f8220,plain,
scratc1717932020_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,[],[f7165,f2415]) ).
fof(f8221,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,[],[f7165,f2416]) ).
fof(f13689,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351561_moreq,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,[],[f8221,f3903]) ).
fof(f13690,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,[],[f8221,f3904]) ).
fof(f13691,plain,
~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,aa_TPTP_ind_TPTP_ind(scratc362691889d_n_pf(sK12(aTP_Lamm_a,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(scratc362691889d_n_pf(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,[],[f8221,f3905]) ).
fof(f13771,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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(scratc361970311d_n_eq,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_dl(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,[],[f13691,f3961]) ).
fof(f13772,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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(scratc1131351550_moref,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_cd(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,[],[f13691,f3911]) ).
fof(f13893,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,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_cd(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,[],[f13772,f13690]) ).
fof(f13894,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,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_dl(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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,[],[f13771,f13690]) ).
fof(f13902,definition,
( spl25_646
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,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_646])],[avatar_definition]) ).
fof(f13903,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,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_646 ),
inference(avatar_component_clause,[],[f13902]) ).
fof(f13906,definition,
( spl25_647
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl25_647])],[avatar_definition]) ).
fof(f13907,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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_647 ),
inference(avatar_component_clause,[],[f13906]) ).
fof(f13908,plain,
( ~ spl25_647
| ~ spl25_646 ),
inference(avatar_split_clause,[],[f13893,f13902,f13906]) ).
fof(f13910,definition,
( spl25_648
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl25_648])],[avatar_definition]) ).
fof(f13911,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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_648 ),
inference(avatar_component_clause,[],[f13910]) ).
fof(f13913,definition,
( spl25_649
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,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_649])],[avatar_definition]) ).
fof(f13914,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc361970311d_n_eq,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_649 ),
inference(avatar_component_clause,[],[f13913]) ).
fof(f13915,plain,
( ~ spl25_648
| ~ spl25_649 ),
inference(avatar_split_clause,[],[f13894,f13913,f13910]) ).
fof(f13992,plain,
pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc812852802_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,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(scratc361970311d_n_eq,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,[],[f13689,f4058]) ).
fof(f14051,plain,
( ! [X0] :
( ~ scratc1717932020_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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_648 ),
inference(resolution,[],[f13911,f2413]) ).
fof(f14110,plain,
( ! [X0] :
( ~ scratc1717932020_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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_648 ),
inference(forward_subsumption_resolution,[],[f14051,f8219]) ).
fof(f14123,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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(scratc1636642277all_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))))))))
| spl25_648 ),
inference(resolution,[],[f14110,f2415]) ).
fof(f14125,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_dl(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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_648 ),
inference(forward_subsumption_resolution,[],[f14123,f7165]) ).
fof(f14126,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dm(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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_648 ),
inference(resolution,[],[f14125,f3802]) ).
fof(f14143,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(scratc1636642277all_of(aTP_Lamm_a),X0)) ),
inference(resolution,[],[f8220,f2413]) ).
fof(f14144,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(scratc1636642277all_of(aTP_Lamm_a),X0)) ),
inference(forward_subsumption_resolution,[],[f14143,f8219]) ).
fof(f16418,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dm(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_648 ),
inference(resolution,[],[f14126,f4742]) ).
fof(f16466,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dn,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_648 ),
inference(resolution,[],[f16418,f3459]) ).
fof(f16488,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dn,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl25_648 ),
inference(resolution,[],[f16466,f7039]) ).
fof(f16533,plain,
( $false
| spl25_648 ),
inference(forward_subsumption_resolution,[],[f16488,f6669]) ).
fof(f16534,plain,
spl25_648,
inference(avatar_contradiction_clause,[],[f16533]) ).
fof(f16708,plain,
( ~ pp(scratc812852802_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,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(scratc361970311d_n_eq,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,[],[f13992,f4038]) ).
fof(f16718,plain,
( ~ pp(scratc812852802_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,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_649 ),
inference(forward_subsumption_resolution,[],[f16708,f13914]) ).
fof(f16722,plain,
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,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_649 ),
inference(resolution,[],[f16718,f4132]) ).
fof(f16829,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1131351550_moref,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_649 ),
inference(resolution,[],[f16722,f4040]) ).
fof(f16843,plain,
( $false
| spl25_646
| spl25_649 ),
inference(forward_subsumption_resolution,[],[f16829,f13903]) ).
fof(f16844,plain,
( spl25_646
| spl25_649 ),
inference(avatar_contradiction_clause,[],[f16843]) ).
fof(f19878,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cd(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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_647 ),
inference(resolution,[],[f13907,f14144]) ).
fof(f19926,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ce(sK12(aTP_Lamm_a,aTP_Lamm_ad)),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_647 ),
inference(resolution,[],[f19878,f3810]) ).
fof(f19975,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ce(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_647 ),
inference(resolution,[],[f19926,f4742]) ).
fof(f20020,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cf,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_647 ),
inference(resolution,[],[f19975,f3479]) ).
fof(f20045,plain,
( ~ pp(aa_fun171081125l_bool(scratc1636642277all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cf,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl25_647 ),
inference(resolution,[],[f20020,f7039]) ).
fof(f20090,plain,
( $false
| spl25_647 ),
inference(forward_subsumption_resolution,[],[f20045,f6679]) ).
fof(f20091,plain,
spl25_647,
inference(avatar_contradiction_clause,[],[f20090]) ).
cnf(s406,plain,
( ~ spl25_646
| ~ spl25_647 ),
inference(sat_conversion,[],[f13908]) ).
cnf(s407,plain,
( ~ spl25_648
| ~ spl25_649 ),
inference(sat_conversion,[],[f13915]) ).
cnf(s431,plain,
spl25_648,
inference(sat_conversion,[],[f16534]) ).
cnf(s439,plain,
( spl25_646
| spl25_649 ),
inference(sat_conversion,[],[f16844]) ).
cnf(s566,plain,
spl25_647,
inference(sat_conversion,[],[f20091]) ).
cnf(s576,plain,
~ spl25_649,
inference(rat,[],[s407,s431]) ).
cnf(s579,plain,
spl25_646,
inference(rat,[],[s439,s576]) ).
cnf(s581,plain,
$false,
inference(rat,[],[s406,s566,s579]) ).
fof(f20092,plain,
$false,
inference(avatar_sat_refutation,[],[s581]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM761+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n006.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 21:18:40 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.28/4.02 % (3323465)Detected formulas, will run a generic FOF schedule.
% 21.28/4.02 % (3323516)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=332207857:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 21.28/4.02 % (3323515)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=1271550886:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 21.28/4.02 % (3323519)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4162890318:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 21.28/4.02 % (3323517)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=3006255682:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 21.28/4.02 % (3323520)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1095746079:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 21.28/4.02 % (3323521)dis-21_1_sil=8000:lcm=predicate:random_seed=483158904:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 21.28/4.02 % (3323518)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2208579400:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 21.28/4.02 % (3323518)Refutation not found, incomplete strategy
% 21.28/4.02 % (3323518)------------------------------
% 21.28/4.02 % (3323518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.28/4.02 % (3323518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.28/4.02 % (3323518)CaDiCaL version: 2.1.3
% 21.28/4.02 % (3323518)Termination reason: Refutation not found, incomplete strategy
% 21.28/4.02 % (3323518)Time elapsed: 0.006 s
% 21.28/4.02 % (3323518)Peak memory usage: 88 MB
% 21.28/4.02 % (3323518)Instructions burned: 5 (million)
% 21.28/4.02 % (3323519)Refutation not found, incomplete strategy
% 21.28/4.02 % (3323519)------------------------------
% 21.28/4.02 % (3323519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.28/4.02 % (3323519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.28/4.02 % (3323519)CaDiCaL version: 2.1.3
% 21.28/4.02 % (3323519)Termination reason: Refutation not found, incomplete strategy
% 21.28/4.02 % (3323519)Time elapsed: 0.007 s
% 21.28/4.02 % (3323519)Peak memory usage: 88 MB
% 21.28/4.02 % (3323519)Instructions burned: 5 (million)
% 21.28/4.02 % (3323521)Instruction limit reached!
% 21.28/4.02 % (3323521)------------------------------
% 21.28/4.02 % (3323521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.28/4.02 % (3323521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.28/4.02 % (3323521)CaDiCaL version: 2.1.3
% 21.28/4.02 % (3323521)Termination reason: Instruction limit
% 21.28/4.02 % (3323521)Termination phase: Saturation
% 21.28/4.02 % (3323521)Time elapsed: 0.110 s
% 21.28/4.02 % (3323521)Peak memory usage: 90 MB
% 21.28/4.02 % (3323521)Instructions burned: 130 (million)
% 21.28/4.02 % (3323520)Instruction limit reached!
% 21.28/4.02 % (3323520)------------------------------
% 21.28/4.02 % (3323520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.28/4.02 % (3323520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.28/4.02 % (3323520)CaDiCaL version: 2.1.3
% 21.28/4.02 % (3323520)Termination reason: Instruction limit
% 21.28/4.02 % (3323520)Termination phase: Saturation
% 21.28/4.02 % (3323520)Time elapsed: 0.124 s
% 21.28/4.02 % (3323520)Peak memory usage: 91 MB
% 21.28/4.02 % (3323520)Instructions burned: 139 (million)
% 21.28/4.02 % (3323518)------------------------------
% 21.28/4.02 % (3323518)------------------------------
% 21.28/4.02 % (3323533)lrs+10_1_sil=8000:sp=occurrence:random_seed=199751102:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 21.28/4.02 % (3323534)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3080069225:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 21.28/4.02 % (3323519)------------------------------
% 21.28/4.02 % (3323519)------------------------------
% 21.28/4.02 % (3323533)Refutation not found, incomplete strategy
% 21.28/4.02 % (3323533)------------------------------
% 21.28/4.02 % (3323533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.28/4.02 % (3323533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.68/6.06 % (3323533)CaDiCaL version: 2.1.3
% 36.68/6.06 % (3323533)Termination reason: Refutation not found, incomplete strategy
% 36.68/6.06 % (3323533)Time elapsed: 0.006 s
% 36.68/6.06 % (3323533)Peak memory usage: 89 MB
% 36.68/6.06 % (3323533)Instructions burned: 4 (million)
% 36.68/6.06 % (3323534)Refutation not found, incomplete strategy
% 36.68/6.06 % (3323534)------------------------------
% 36.68/6.06 % (3323534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.68/6.06 % (3323534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.68/6.06 % (3323534)CaDiCaL version: 2.1.3
% 36.68/6.06 % (3323534)Termination reason: Refutation not found, incomplete strategy
% 36.68/6.06 % (3323534)Time elapsed: 0.015 s
% 36.68/6.06 % (3323534)Peak memory usage: 89 MB
% 36.68/6.06 % (3323534)Instructions burned: 17 (million)
% 36.68/6.06 % (3323541)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1839186720:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 36.68/6.06 % (3323544)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=3353699601:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 36.68/6.06 % (3323541)Refutation not found, incomplete strategy
% 36.68/6.06 % (3323541)------------------------------
% 36.68/6.06 % (3323541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.68/6.06 % (3323541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.68/6.06 % (3323541)CaDiCaL version: 2.1.3
% 36.68/6.06 % (3323541)Termination reason: Refutation not found, incomplete strategy
% 36.68/6.06 % (3323541)Time elapsed: 0.010 s
% 36.68/6.06 % (3323541)Peak memory usage: 90 MB
% 36.68/6.06 % (3323541)Instructions burned: 7 (million)
% 36.68/6.06 % (3323533)------------------------------
% 36.68/6.06 % (3323533)------------------------------
% 36.68/6.06 % (3323534)------------------------------
% 36.68/6.06 % (3323534)------------------------------
% 36.68/6.06 % (3323544)Instruction limit reached!
% 36.68/6.06 % (3323544)------------------------------
% 36.68/6.06 % (3323544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.68/6.06 % (3323544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.68/6.06 % (3323544)CaDiCaL version: 2.1.3
% 36.68/6.06 % (3323544)Termination reason: Instruction limit
% 36.68/6.06 % (3323544)Termination phase: Saturation
% 36.68/6.06 % (3323544)Time elapsed: 0.222 s
% 36.68/6.06 % (3323544)Peak memory usage: 97 MB
% 36.68/6.06 % (3323544)Instructions burned: 249 (million)
% 36.68/6.06 % (3323541)------------------------------
% 36.68/6.06 % (3323541)------------------------------
% 36.68/6.06 % (3323549)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3260694827:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 36.68/6.06 % (3323549)Refutation not found, incomplete strategy
% 36.68/6.06 % (3323549)------------------------------
% 36.68/6.06 % (3323549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.68/6.06 % (3323549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.68/6.06 % (3323549)CaDiCaL version: 2.1.3
% 36.68/6.06 % (3323549)Termination reason: Refutation not found, incomplete strategy
% 36.68/6.06 % (3323549)Time elapsed: 0.012 s
% 36.68/6.06 % (3323549)Peak memory usage: 89 MB
% 36.68/6.06 % (3323549)Instructions burned: 10 (million)
% 36.68/6.06 % (3323550)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3401307235:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 36.68/6.06 % (3323551)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=219014759:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 36.68/6.06 % (3323551)Instruction limit reached!
% 36.68/6.06 % (3323551)------------------------------
% 36.68/6.06 % (3323551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.68/6.06 % (3323551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.68/6.06 % (3323551)CaDiCaL version: 2.1.3
% 36.68/6.06 % (3323551)Termination reason: Instruction limit
% 36.68/6.06 % (3323551)Termination phase: Saturation
% 36.68/6.06 % (3323551)Time elapsed: 0.098 s
% 36.68/6.06 % (3323551)Peak memory usage: 90 MB
% 36.68/6.06 % (3323551)Instructions burned: 113 (million)
% 36.68/6.06 % (3323556)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1051252699:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 84.08/12.78 % (3323556)Instruction limit reached!
% 84.08/12.78 % (3323556)------------------------------
% 84.08/12.78 % (3323556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.08/12.78 % (3323556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.08/12.78 % (3323556)CaDiCaL version: 2.1.3
% 84.08/12.78 % (3323556)Termination reason: Instruction limit
% 84.08/12.78 % (3323556)Termination phase: Saturation
% 84.08/12.78 % (3323556)Time elapsed: 0.104 s
% 84.08/12.78 % (3323556)Peak memory usage: 90 MB
% 84.08/12.78 % (3323556)Instructions burned: 127 (million)
% 84.08/12.78 % (3323549)------------------------------
% 84.08/12.78 % (3323549)------------------------------
% 84.08/12.78 % (3323562)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2228861619:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 84.08/12.78 % (3323562)Instruction limit reached!
% 84.08/12.78 % (3323562)------------------------------
% 84.08/12.78 % (3323562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.08/12.78 % (3323562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.08/12.78 % (3323562)CaDiCaL version: 2.1.3
% 84.08/12.78 % (3323562)Termination reason: Instruction limit
% 84.08/12.78 % (3323562)Termination phase: Saturation
% 84.08/12.78 % (3323562)Time elapsed: 0.106 s
% 84.08/12.78 % (3323562)Peak memory usage: 90 MB
% 84.08/12.78 % (3323562)Instructions burned: 114 (million)
% 84.08/12.78 % (3323566)lrs+10_1_sil=8000:sp=occurrence:random_seed=996551074:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 84.08/12.78 % (3323567)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2913585992:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 84.08/12.78 % (3323567)Refutation not found, incomplete strategy
% 84.08/12.78 % (3323567)------------------------------
% 84.08/12.78 % (3323567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.08/12.78 % (3323567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.08/12.78 % (3323567)CaDiCaL version: 2.1.3
% 84.08/12.78 % (3323567)Termination reason: Refutation not found, incomplete strategy
% 84.08/12.78 % (3323567)Time elapsed: 0.131 s
% 84.08/12.78 % (3323567)Peak memory usage: 92 MB
% 84.08/12.78 % (3323567)Instructions burned: 152 (million)
% 84.08/12.78 % (3323569)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3634141429:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 84.08/12.78 % (3323567)------------------------------
% 84.08/12.78 % (3323567)------------------------------
% 84.08/12.78 % (3323566)Instruction limit reached!
% 84.08/12.78 % (3323566)------------------------------
% 84.08/12.78 % (3323566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.08/12.78 % (3323566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.08/12.78 % (3323566)CaDiCaL version: 2.1.3
% 84.08/12.78 % (3323566)Termination reason: Instruction limit
% 84.08/12.78 % (3323566)Termination phase: Saturation
% 84.08/12.78 % (3323566)Time elapsed: 0.861 s
% 84.08/12.78 % (3323566)Peak memory usage: 101 MB
% 84.08/12.78 % (3323566)Instructions burned: 907 (million)
% 84.08/12.78 % (3323575)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=10091295:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2974 on theBenchmark for (2974ds/134Mi)
% 84.08/12.78 % (3323575)Instruction limit reached!
% 84.08/12.78 % (3323575)------------------------------
% 84.08/12.78 % (3323575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.08/12.78 % (3323575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.08/12.78 % (3323575)CaDiCaL version: 2.1.3
% 84.08/12.78 % (3323575)Termination reason: Instruction limit
% 84.08/12.78 % (3323575)Termination phase: Saturation
% 84.08/12.78 % (3323575)Time elapsed: 0.116 s
% 84.08/12.78 % (3323575)Peak memory usage: 92 MB
% 84.08/12.78 % (3323575)Instructions burned: 134 (million)
% 84.08/12.78 % (3323577)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3559546183:st=8:i=592:sd=3:ep=RST:ss=axioms_2971 on theBenchmark for (2971ds/592Mi)
% 84.08/12.78 % (3323577)Refutation not found, incomplete strategy
% 84.08/12.78 % (3323577)------------------------------
% 84.08/12.78 % (3323577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.08/12.78 % (3323577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.08/12.78 % (3323577)CaDiCaL version: 2.1.3
% 84.08/12.78 % (3323577)Termination reason: Refutation not found, incomplete strategy
% 120.96/18.02 % (3323577)Time elapsed: 0.030 s
% 120.96/18.02 % (3323577)Peak memory usage: 90 MB
% 120.96/18.02 % (3323577)Instructions burned: 31 (million)
% 120.96/18.02 % (3323578)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1452547706:st=3:i=13193:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/13193Mi)
% 120.96/18.02 % (3323577)------------------------------
% 120.96/18.02 % (3323577)------------------------------
% 120.96/18.02 % (3323583)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=3783063380:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/125Mi)
% 120.96/18.02 % (3323583)Refutation not found, incomplete strategy
% 120.96/18.02 % (3323583)------------------------------
% 120.96/18.02 % (3323583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.96/18.02 % (3323583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.96/18.02 % (3323583)CaDiCaL version: 2.1.3
% 120.96/18.02 % (3323583)Termination reason: Refutation not found, incomplete strategy
% 120.96/18.02 % (3323583)Time elapsed: 0.020 s
% 120.96/18.02 % (3323583)Peak memory usage: 89 MB
% 120.96/18.02 % (3323583)Instructions burned: 21 (million)
% 120.96/18.02 % (3323550)Instruction limit reached!
% 120.96/18.02 % (3323550)------------------------------
% 120.96/18.02 % (3323550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.96/18.02 % (3323550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.96/18.02 % (3323550)CaDiCaL version: 2.1.3
% 120.96/18.02 % (3323550)Termination reason: Instruction limit
% 120.96/18.02 % (3323550)Termination phase: Saturation
% 120.96/18.02 % (3323550)Time elapsed: 2.430 s
% 120.96/18.02 % (3323550)Peak memory usage: 154 MB
% 120.96/18.02 % (3323550)Instructions burned: 2350 (million)
% 120.96/18.02 % (3323585)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2512938638:i=134:gtgl=5:slsql=off:gtg=exists_sym_2961 on theBenchmark for (2961ds/134Mi)
% 120.96/18.02 % (3323583)------------------------------
% 120.96/18.02 % (3323583)------------------------------
% 120.96/18.02 % (3323585)Instruction limit reached!
% 120.96/18.02 % (3323585)------------------------------
% 120.96/18.02 % (3323585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.96/18.02 % (3323585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.96/18.02 % (3323585)CaDiCaL version: 2.1.3
% 120.96/18.02 % (3323585)Termination reason: Instruction limit
% 120.96/18.02 % (3323585)Termination phase: Property scanning
% 120.96/18.02 % (3323585)Time elapsed: 0.116 s
% 120.96/18.02 % (3323585)Peak memory usage: 91 MB
% 120.96/18.02 % (3323585)Instructions burned: 134 (million)
% 120.96/18.02 % (3323589)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=965824362:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/141Mi)
% 120.96/18.02 % (3323589)Refutation not found, incomplete strategy
% 120.96/18.02 % (3323589)------------------------------
% 120.96/18.02 % (3323589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.96/18.02 % (3323589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.96/18.02 % (3323589)CaDiCaL version: 2.1.3
% 120.96/18.02 % (3323589)Termination reason: Refutation not found, incomplete strategy
% 120.96/18.02 % (3323589)Time elapsed: 0.006 s
% 120.96/18.02 % (3323589)Peak memory usage: 89 MB
% 120.96/18.02 % (3323589)Instructions burned: 4 (million)
% 120.96/18.02 % (3323590)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=637601694:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2957 on theBenchmark for (2957ds/431Mi)
% 120.96/18.02 % (3323590)Refutation not found, incomplete strategy
% 120.96/18.02 % (3323590)------------------------------
% 120.96/18.02 % (3323590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.96/18.02 % (3323590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.96/18.02 % (3323590)CaDiCaL version: 2.1.3
% 120.96/18.02 % (3323590)Termination reason: Refutation not found, incomplete strategy
% 120.96/18.02 % (3323590)Time elapsed: 0.007 s
% 120.96/18.02 % (3323590)Peak memory usage: 89 MB
% 120.96/18.02 % (3323590)Instructions burned: 4 (million)
% 120.96/18.02 % (3323589)------------------------------
% 120.96/18.02 % (3323589)------------------------------
% 120.96/18.02 % (3323590)------------------------------
% 120.96/18.02 % (3323590)------------------------------
% 120.96/18.02 % (3323593)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=4039520693:i=6060:aac=none:ins=25_2950 on theBenchmark for (2950ds/6060Mi)
% 148.94/21.99 % (3323594)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=2332604821:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2950 on theBenchmark for (2950ds/150Mi)
% 148.94/21.99 % (3323594)Instruction limit reached!
% 148.94/21.99 % (3323594)------------------------------
% 148.94/21.99 % (3323594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.94/21.99 % (3323594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.94/21.99 % (3323594)CaDiCaL version: 2.1.3
% 148.94/21.99 % (3323594)Termination reason: Instruction limit
% 148.94/21.99 % (3323594)Termination phase: Saturation
% 148.94/21.99 % (3323594)Time elapsed: 0.126 s
% 148.94/21.99 % (3323594)Peak memory usage: 91 MB
% 148.94/21.99 % (3323594)Instructions burned: 150 (million)
% 148.94/21.99 % (3323597)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2121105526:i=14155:bd=all_2946 on theBenchmark for (2946ds/14155Mi)
% 148.94/21.99 % (3323569)Instruction limit reached!
% 148.94/21.99 % (3323569)------------------------------
% 148.94/21.99 % (3323569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.94/21.99 % (3323569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.94/21.99 % (3323569)CaDiCaL version: 2.1.3
% 148.94/21.99 % (3323569)Termination reason: Instruction limit
% 148.94/21.99 % (3323569)Termination phase: Saturation
% 148.94/21.99 % (3323569)Time elapsed: 5.457 s
% 148.94/21.99 % (3323569)Peak memory usage: 161 MB
% 148.94/21.99 % (3323569)Instructions burned: 5202 (million)
% 148.94/21.99 % (3323605)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2772862229:i=667:av=off:fsr=off_2923 on theBenchmark for (2923ds/667Mi)
% 148.94/21.99 % (3323605)Instruction limit reached!
% 148.94/21.99 % (3323605)------------------------------
% 148.94/21.99 % (3323605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.94/21.99 % (3323605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.94/21.99 % (3323605)CaDiCaL version: 2.1.3
% 148.94/21.99 % (3323605)Termination reason: Instruction limit
% 148.94/21.99 % (3323605)Termination phase: Saturation
% 148.94/21.99 % (3323605)Time elapsed: 0.556 s
% 148.94/21.99 % (3323605)Peak memory usage: 100 MB
% 148.94/21.99 % (3323605)Instructions burned: 667 (million)
% 148.94/21.99 % (3323609)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=1030801033:s2a=on:i=185:s2at=1.8:fdi=4_2914 on theBenchmark for (2914ds/185Mi)
% 148.94/21.99 % (3323609)Instruction limit reached!
% 148.94/21.99 % (3323609)------------------------------
% 148.94/21.99 % (3323609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.94/21.99 % (3323609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.94/21.99 % (3323609)CaDiCaL version: 2.1.3
% 148.94/21.99 % (3323609)Termination reason: Instruction limit
% 148.94/21.99 % (3323609)Termination phase: Saturation
% 148.94/21.99 % (3323609)Time elapsed: 0.148 s
% 148.94/21.99 % (3323609)Peak memory usage: 91 MB
% 148.94/21.99 % (3323609)Instructions burned: 186 (million)
% 148.94/21.99 % (3323611)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3035626787:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2910 on theBenchmark for (2910ds/193Mi)
% 148.94/21.99 % (3323611)Refutation not found, incomplete strategy
% 148.94/21.99 % (3323611)------------------------------
% 148.94/21.99 % (3323611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.94/21.99 % (3323611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.94/21.99 % (3323611)CaDiCaL version: 2.1.3
% 148.94/21.99 % (3323611)Termination reason: Refutation not found, incomplete strategy
% 148.94/21.99 % (3323611)Time elapsed: 0.011 s
% 148.94/21.99 % (3323611)Peak memory usage: 89 MB
% 148.94/21.99 % (3323611)Instructions burned: 9 (million)
% 148.94/21.99 % (3323611)------------------------------
% 148.94/21.99 % (3323611)------------------------------
% 148.94/21.99 % (3323613)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=173252307:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2903 on theBenchmark for (2903ds/4850Mi)
% 148.94/21.99 % (3323593)Instruction limit reached!
% 148.94/21.99 % (3323593)------------------------------
% 97.06/25.61 % (3323593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323593)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323593)Termination reason: Instruction limit
% 97.06/25.61 % (3323593)Termination phase: Saturation
% 97.06/25.61 % (3323593)Time elapsed: 6.717 s
% 97.06/25.61 % (3323593)Peak memory usage: 168 MB
% 97.06/25.61 % (3323593)Instructions burned: 6061 (million)
% 97.06/25.61 % (3323619)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=90602001:i=12111:sd=1:ss=included_2880 on theBenchmark for (2880ds/12111Mi)
% 97.06/25.61 % (3323613)Instruction limit reached!
% 97.06/25.61 % (3323613)------------------------------
% 97.06/25.61 % (3323613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323613)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323613)Termination reason: Instruction limit
% 97.06/25.61 % (3323613)Termination phase: Saturation
% 97.06/25.61 % (3323613)Time elapsed: 4.937 s
% 97.06/25.61 % (3323613)Peak memory usage: 153 MB
% 97.06/25.61 % (3323613)Instructions burned: 4852 (million)
% 97.06/25.61 % (3323624)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2827932684:i=319:kws=precedence:fsr=off_2850 on theBenchmark for (2850ds/319Mi)
% 97.06/25.61 % (3323578)Instruction limit reached!
% 97.06/25.61 % (3323578)------------------------------
% 97.06/25.61 % (3323578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323578)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323578)Termination reason: Instruction limit
% 97.06/25.61 % (3323578)Termination phase: Saturation
% 97.06/25.61 % (3323578)Time elapsed: 12.170 s
% 97.06/25.61 % (3323578)Peak memory usage: 172 MB
% 97.06/25.61 % (3323578)Instructions burned: 13194 (million)
% 97.06/25.61 % (3323624)Instruction limit reached!
% 97.06/25.61 % (3323624)------------------------------
% 97.06/25.61 % (3323624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323624)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323624)Termination reason: Instruction limit
% 97.06/25.61 % (3323624)Termination phase: Saturation
% 97.06/25.61 % (3323624)Time elapsed: 0.282 s
% 97.06/25.61 % (3323624)Peak memory usage: 94 MB
% 97.06/25.61 % (3323624)Instructions burned: 319 (million)
% 97.06/25.61 % (3323627)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=43314212:i=2064:ep=RST_2846 on theBenchmark for (2846ds/2064Mi)
% 97.06/25.61 % (3323628)dis-1011_128_sil=32000:random_seed=659307064:i=3706:ep=RST:av=off_2845 on theBenchmark for (2845ds/3706Mi)
% 97.06/25.61 % (3323627)Refutation not found, incomplete strategy
% 97.06/25.61 % (3323627)------------------------------
% 97.06/25.61 % (3323627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323627)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323627)Termination reason: Refutation not found, incomplete strategy
% 97.06/25.61 % (3323627)Time elapsed: 0.111 s
% 97.06/25.61 % (3323627)Peak memory usage: 91 MB
% 97.06/25.61 % (3323627)Instructions burned: 132 (million)
% 97.06/25.61 % (3323627)------------------------------
% 97.06/25.61 % (3323627)------------------------------
% 97.06/25.61 % (3323631)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4159309641:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2838 on theBenchmark for (2838ds/757Mi)
% 97.06/25.61 % (3323631)Refutation not found, incomplete strategy
% 97.06/25.61 % (3323631)------------------------------
% 97.06/25.61 % (3323631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323631)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323631)Termination reason: Refutation not found, incomplete strategy
% 97.06/25.61 % (3323631)Time elapsed: 0.015 s
% 97.06/25.61 % (3323631)Peak memory usage: 89 MB
% 97.06/25.61 % (3323631)Instructions burned: 14 (million)
% 97.06/25.61 % (3323631)------------------------------
% 97.06/25.61 % (3323631)------------------------------
% 97.06/25.61 % (3323633)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=307653031:i=13913:ss=axioms:sgt=8_2831 on theBenchmark for (2831ds/13913Mi)
% 97.06/25.61 % (3323633)Refutation not found, incomplete strategy
% 97.06/25.61 % (3323633)------------------------------
% 97.06/25.61 % (3323633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323633)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323633)Termination reason: Refutation not found, incomplete strategy
% 97.06/25.61 % (3323633)Time elapsed: 0.923 s
% 97.06/25.61 % (3323633)Peak memory usage: 129 MB
% 97.06/25.61 % (3323633)Instructions burned: 883 (million)
% 97.06/25.61 % (3323633)------------------------------
% 97.06/25.61 % (3323633)------------------------------
% 97.06/25.61 % (3323637)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4191666295:i=9925:aac=none_2815 on theBenchmark for (2815ds/9925Mi)
% 97.06/25.61 % (3323628)Instruction limit reached!
% 97.06/25.61 % (3323628)------------------------------
% 97.06/25.61 % (3323628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323628)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323628)Termination reason: Instruction limit
% 97.06/25.61 % (3323628)Termination phase: Saturation
% 97.06/25.61 % (3323628)Time elapsed: 3.336 s
% 97.06/25.61 % (3323628)Peak memory usage: 113 MB
% 97.06/25.61 % (3323628)Instructions burned: 3707 (million)
% 97.06/25.61 % (3323639)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=907310012:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2809 on theBenchmark for (2809ds/2479Mi)
% 97.06/25.61 % (3323639)Refutation not found, incomplete strategy
% 97.06/25.61 % (3323639)------------------------------
% 97.06/25.61 % (3323639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323639)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323639)Termination reason: Refutation not found, incomplete strategy
% 97.06/25.61 % (3323639)Time elapsed: 0.010 s
% 97.06/25.61 % (3323639)Peak memory usage: 89 MB
% 97.06/25.61 % (3323639)Instructions burned: 8 (million)
% 97.06/25.61 % (3323639)------------------------------
% 97.06/25.61 % (3323639)------------------------------
% 97.06/25.61 % (3323597)Instruction limit reached!
% 97.06/25.61 % (3323597)------------------------------
% 97.06/25.61 % (3323597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323597)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323597)Termination reason: Instruction limit
% 97.06/25.61 % (3323597)Termination phase: Saturation
% 97.06/25.61 % (3323597)Time elapsed: 14.132 s
% 97.06/25.61 % (3323597)Peak memory usage: 225 MB
% 97.06/25.61 % (3323597)Instructions burned: 14156 (million)
% 97.06/25.61 % (3323643)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3704495356:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2802 on theBenchmark for (2802ds/440Mi)
% 97.06/25.61 % (3323644)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1994669919:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2801 on theBenchmark for (2801ds/11145Mi)
% 97.06/25.61 % (3323643)Instruction limit reached!
% 97.06/25.61 % (3323643)------------------------------
% 97.06/25.61 % (3323643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323643)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323643)Termination reason: Instruction limit
% 97.06/25.61 % (3323643)Termination phase: Saturation
% 97.06/25.61 % (3323643)Time elapsed: 0.322 s
% 97.06/25.61 % (3323643)Peak memory usage: 91 MB
% 97.06/25.61 % (3323643)Instructions burned: 440 (million)
% 97.06/25.61 % (3323647)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=395819176:cts=off:i=3034:av=off:er=known:fsd=on_2795 on theBenchmark for (2795ds/3034Mi)
% 97.06/25.61 % (3323644)Refutation not found, incomplete strategy
% 97.06/25.61 % (3323644)------------------------------
% 97.06/25.61 % (3323644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323644)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323644)Termination reason: Refutation not found, incomplete strategy
% 97.06/25.61 % (3323644)Time elapsed: 0.985 s
% 97.06/25.61 % (3323644)Peak memory usage: 130 MB
% 97.06/25.61 % (3323644)Instructions burned: 925 (million)
% 97.06/25.61 % (3323644)------------------------------
% 97.06/25.61 % (3323644)------------------------------
% 97.06/25.61 % (3323649)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=931398542:st=2:s2a=on:i=524:s2at=2:ss=axioms_2784 on theBenchmark for (2784ds/524Mi)
% 97.06/25.61 % (3323649)Instruction limit reached!
% 97.06/25.61 % (3323649)------------------------------
% 97.06/25.61 % (3323649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323649)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323649)Termination reason: Instruction limit
% 97.06/25.61 % (3323649)Termination phase: Saturation
% 97.06/25.61 % (3323649)Time elapsed: 0.487 s
% 97.06/25.61 % (3323649)Peak memory usage: 94 MB
% 97.06/25.61 % (3323649)Instructions burned: 524 (million)
% 97.06/25.61 % (3323651)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=284864969:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2776 on theBenchmark for (2776ds/1016Mi)
% 97.06/25.61 % (3323651)Refutation not found, incomplete strategy
% 97.06/25.61 % (3323651)------------------------------
% 97.06/25.61 % (3323651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323651)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323651)Termination reason: Refutation not found, incomplete strategy
% 97.06/25.61 % (3323651)Time elapsed: 0.007 s
% 97.06/25.61 % (3323651)Peak memory usage: 89 MB
% 97.06/25.61 % (3323651)Instructions burned: 5 (million)
% 97.06/25.61 % (3323651)------------------------------
% 97.06/25.61 % (3323651)------------------------------
% 97.06/25.61 % (3323655)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3303488078:i=14123:bd=preordered:ins=4_2769 on theBenchmark for (2769ds/14123Mi)
% 97.06/25.61 % (3323647)Instruction limit reached!
% 97.06/25.61 % (3323647)------------------------------
% 97.06/25.61 % (3323647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323647)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323647)Termination reason: Instruction limit
% 97.06/25.61 % (3323647)Termination phase: Saturation
% 97.06/25.61 % (3323647)Time elapsed: 2.709 s
% 97.06/25.61 % (3323647)Peak memory usage: 157 MB
% 97.06/25.61 % (3323647)Instructions burned: 3034 (million)
% 97.06/25.61 % (3323657)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2037426293:i=5781:kws=precedence:bd=all:rawr=on_2766 on theBenchmark for (2766ds/5781Mi)
% 97.06/25.61 % (3323619)Instruction limit reached!
% 97.06/25.61 % (3323619)------------------------------
% 97.06/25.61 % (3323619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.06/25.61 % (3323619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.06/25.61 % (3323619)CaDiCaL version: 2.1.3
% 97.06/25.61 % (3323619)Termination reason: Instruction limit
% 97.06/25.61 % (3323619)Termination phase: Saturation
% 97.06/25.61 % (3323619)Time elapsed: 12.010 s
% 97.06/25.61 % (3323619)Peak memory usage: 241 MB
% 97.06/25.61 % (3323619)Instructions burned: 12111 (million)
% 97.06/25.61 % (3323637)First to succeed.
% 97.06/25.61 % (3323637)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3323465"
% 97.06/25.61 % (3323659)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=51146729:i=2448:gtgl=5:bd=preordered:gtg=all_2757 on theBenchmark for (2757ds/2448Mi)
% 97.06/25.61 % (3323637)Refutation found. Thanks to Tanya!
% 97.06/25.61 % SZS status Theorem for theBenchmark
% 97.06/25.61 % SZS output start Proof for theBenchmark
% See solution above
% 175.79/25.87 % (3323637)------------------------------
% 175.79/25.87 % (3323637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.79/25.87 % (3323637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.79/25.87 % (3323637)CaDiCaL version: 2.1.3
% 175.79/25.87 % (3323637)Termination reason: Refutation
% 175.79/25.87 % (3323637)Time elapsed: 5.450 s
% 175.79/25.87 % (3323637)Peak memory usage: 182 MB
% 175.79/25.87 % (3323637)Instructions burned: 5752 (million)
% 175.79/25.87 % (3323637)------------------------------
% 175.79/25.87 % (3323637)------------------------------
% 175.79/25.87 % (3323465)Success in time 24.721 s
% 175.79/25.87 % Vampire exiting
%------------------------------------------------------------------------------